diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-10 18:31:41 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-11-11 16:07:28 -0500 |
| commit | 188c1cb99886853d452925ae513a44d3da6151dd (patch) | |
| tree | 98617ce17df26ee3f5e314a6b85b92a94cdeec07 /src/Specific/GF25519Reflective.v | |
| parent | 20482796154100307af995bc8445ec6f674531d0 (diff) | |
Freeze stubs
Diffstat (limited to 'src/Specific/GF25519Reflective.v')
| -rw-r--r-- | src/Specific/GF25519Reflective.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v index 4405eefa9..5e306d61d 100644 --- a/src/Specific/GF25519Reflective.v +++ b/src/Specific/GF25519Reflective.v @@ -36,7 +36,7 @@ Definition radd : ExprBinOp := Eval vm_compute in rcarry_addW. Definition rsub : ExprBinOp := Eval vm_compute in rcarry_subW. Definition rmul : ExprBinOp := Eval vm_compute in rmulW. Definition ropp : ExprUnOp := Eval vm_compute in rcarry_oppW. -Definition rfreeze : ExprUnOp := Eval vm_compute in rfreezeW. +Definition rprefreeze : ExprUnOp := Eval vm_compute in rprefreezeW. Definition rge_modulus : ExprUnOpFEToZ := Eval vm_compute in rge_modulusW. Definition rpack : ExprUnOpFEToWire := Eval vm_compute in rpackW. Definition runpack : ExprUnOpWireToFE := Eval vm_compute in runpackW. @@ -48,7 +48,7 @@ Declare Reduction asm_interp := cbv beta iota delta [id interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE - radd rsub rmul ropp rfreeze rge_modulus rpack runpack + radd rsub rmul ropp rprefreeze rge_modulus rpack runpack curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW Word64.interp_op Word64.interp_base_type Z.interp_op Z.interp_base_type @@ -59,7 +59,7 @@ Ltac asm_interp := cbv beta iota delta [id interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE - radd rsub rmul ropp rfreeze rge_modulus rpack runpack + radd rsub rmul ropp rprefreeze rge_modulus rpack runpack curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW Word64.interp_op Word64.interp_base_type Z.interp_op Z.interp_base_type @@ -84,10 +84,10 @@ Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25 := Eval asm_interp in interp_uexpr (rword64ize ropp). (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. -Definition interp_rfreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W - := Eval asm_interp in interp_uexpr (rword64ize rfreeze). -(*Print interp_rfreeze.*) -Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl. +Definition interp_rprefreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). +(*Print interp_rprefreeze.*) +Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64 := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). @@ -109,8 +109,8 @@ Lemma rmul_correct_and_bounded : binop_correct_and_bounded rmul mul. Proof. exact rmulW_correct_and_bounded. Qed. Lemma ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp. Proof. exact rcarry_oppW_correct_and_bounded. Qed. -Lemma rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze. -Proof. exact rfreezeW_correct_and_bounded. Qed. +Lemma rprefreeze_correct_and_bounded : unop_correct_and_bounded rprefreeze prefreeze. +Proof. exact rprefreezeW_correct_and_bounded. Qed. Lemma rge_modulus_correct_and_bounded : unop_FEToZ_correct rge_modulus ge_modulus. Proof. exact rge_modulusW_correct_and_bounded. Qed. Lemma rpack_correct_and_bounded : unop_FEToWire_correct_and_bounded rpack pack. |