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 | |
| parent | f613381431f92dce54591324cde6cb954d61470d (diff) | |
Fix some problems with previous commit
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519Reflective.v | 11 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/AddCoordinates.v | 6 |
3 files changed, 10 insertions, 10 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 diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index ea42499f7..916fbde6b 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -533,6 +533,9 @@ Ltac rexpr_correct := Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). +Definition rword64ize {t} (x : Expr t) : Expr t + := MapInterp (fun t => match t with TZ => word64ize end) x. + Notation compute_bounds opW bounds := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) (only parsing). diff --git a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v index d27fa8b50..c5becbcca 100644 --- a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v +++ b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v @@ -173,6 +173,6 @@ Program Definition radd_coordinatesW_correct_and_bounded _ _. Local Open Scope string_scope. -Compute ("Add_Coordinates", compute_bounds_for_display radd_coordinatesW ExprAC_bounds). -Compute ("Add_Coordinates overflows? ", sanity_compute radd_coordinatesW ExprAC_bounds). -Compute ("Add_Coordinates overflows (error if it does)? ", sanity_check radd_coordinatesW ExprAC_bounds). +Compute ("Add_Coordinates", compute_bounds_for_display radd_coordinatesW Expr9Op_bounds). +Compute ("Add_Coordinates overflows? ", sanity_compute radd_coordinatesW Expr9Op_bounds). +Compute ("Add_Coordinates overflows (error if it does)? ", sanity_check radd_coordinatesW Expr9Op_bounds). |