diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-17 17:06:13 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-17 17:06:13 -0500 |
| commit | 81ac0147d217dfc1f37b5822c844a00639ef11c2 (patch) | |
| tree | 8bb111ec74716af9246ce149cf12e57889ef0300 /src/Specific/GF25519Reflective.v | |
| parent | f613381431f92dce54591324cde6cb954d61470d (diff) | |
Fix some problems with previous commit
Diffstat (limited to 'src/Specific/GF25519Reflective.v')
| -rw-r--r-- | src/Specific/GF25519Reflective.v | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v index 1acef4e06..b981747a1 100644 --- a/src/Specific/GF25519Reflective.v +++ b/src/Specific/GF25519Reflective.v @@ -41,15 +41,12 @@ 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. -Definition rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize end) x. - Declare Reduction asm_interp := cbv beta iota delta [id - interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr radd rsub rmul ropp rprefreeze rge_modulus rpack runpack - curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW + curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type @@ -58,9 +55,9 @@ Declare Reduction asm_interp Ltac asm_interp := cbv beta iota delta [id - interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr radd rsub rmul ropp rprefreeze rge_modulus rpack runpack - curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW + curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type |