diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64Reflective.v')
| -rw-r--r-- | src/SpecificGen/GF25519_64Reflective.v | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/src/SpecificGen/GF25519_64Reflective.v b/src/SpecificGen/GF25519_64Reflective.v index 86b8735d6..620c96713 100644 --- a/src/SpecificGen/GF25519_64Reflective.v +++ b/src/SpecificGen/GF25519_64Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations128. Require Crypto.Reflection.Z.Interpretations128.Relations. Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr (rword128ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr (rword128ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.word128 - := Eval asm_interp in interp_uexpr_FEToZ (rword128ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword128ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF25519_64BoundedCommon.wire_digitsW -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr_WireToFE (rword128ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. |