diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64Reflective')
| -rw-r--r-- | src/SpecificGen/GF25519_64Reflective/Common.v | 3 | ||||
| -rw-r--r-- | src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v | 6 |
2 files changed, 6 insertions, 3 deletions
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v index c5fff2698..ec73e09be 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common.v +++ b/src/SpecificGen/GF25519_64Reflective/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 rword128ize {t} (x : Expr t) : Expr t + := MapInterp (fun t => match t with TZ => word128ize end) x. + Notation compute_bounds opW bounds := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) (only parsing). diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v index c9c639773..4143ad79b 100644 --- a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF25519_64Reflective/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). |