diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-31 11:20:00 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-31 13:54:42 -0400 |
| commit | ac46ff22a9f6a279068ebdb897498e8dd14b1916 (patch) | |
| tree | d0a74b1bb3bcf48e53c43303da3fe73447d7ee6f /src/Specific/GF25519Reflective | |
| parent | 6a4f573de04234ff8d8da44ea9b48cf3f7093f1a (diff) | |
Switch from word to Z
Diffstat (limited to 'src/Specific/GF25519Reflective')
| -rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 951ce89cf..752f186d1 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -13,7 +13,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Notation Expr := (Expr base_type Word64.interp_base_type op). +Notation Expr := (Expr base_type Z.interp_base_type op). Local Ltac make_type_from uncurried_op := let T := (type of uncurried_op) in @@ -38,15 +38,15 @@ Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W - := fun e => curry_binop_fe25519W (Interp (@Word64.interp_op) e). + := fun e => curry_binop_fe25519W (Interp (@Z.interp_op) e). Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W - := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e). + := fun e => curry_unop_fe25519W (Interp (@Z.interp_op) e). Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64 - := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e). + := fun e => curry_unop_fe25519W (Interp (@Z.interp_op) e). Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW - := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e). + := fun e => curry_unop_fe25519W (Interp (@Z.interp_op) e). Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W - := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e). + := fun e => curry_unop_wire_digitsW (Interp (@Z.interp_op) e). Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). @@ -84,7 +84,7 @@ Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_uno Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). Notation correct_and_bounded_genT ropW'v ropZ_sigv - := (let ropW' := ropW'v in + := (let ropW' := MapInterp Word64.of_Z ropW'v in let ropZ_sig := ropZ_sigv in let ropW := MapInterp (fun _ x => x) ropW' in let ropZ := MapInterp Word64.to_Z ropW' in @@ -108,4 +108,4 @@ Ltac rexpr_correct := [ | apply @RelWfMapInterp, wf_ropW ].. ]; auto with interp_related. -Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing). +Notation rword_of_Z rexprZ_sig := ((*MapInterp Word64.of_Z*) (proj1_sig rexprZ_sig)) (only parsing). |