From 43c5265c24bd1df125f8de00d1f89379a920659a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Nov 2016 21:46:40 -0500 Subject: Support for 128-bit words I haven't found a good way to genericize the proofs of relatedness things, mostly because Modules and functors are annoying. --- src/SpecificGen/GF25519_64Reflective/CommonBinOp.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/SpecificGen/GF25519_64Reflective/CommonBinOp.v') diff --git a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v index cd4a5031b..c8872efc5 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v @@ -1,6 +1,6 @@ Require Export Crypto.SpecificGen.GF25519_64Reflective.Common. Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. -Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.MapInterp. @@ -18,7 +18,7 @@ Lemma ExprBinOp_correct_and_bounded let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded xy Hx Hy in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) (LiftOption.to' (Some args))) with | Some _ => True @@ -31,9 +31,9 @@ Lemma ExprBinOp_correct_and_bounded let Hx := let (Hx, Hy) := Hxy in Hx in let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) with | Some bounds => binop_bounds_good bounds = true | None => False -- cgit v1.2.3