diff options
Diffstat (limited to 'src/Specific/GF25519Reflective/Common9_4Op.v')
-rw-r--r-- | src/Specific/GF25519Reflective/Common9_4Op.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/Specific/GF25519Reflective/Common9_4Op.v b/src/Specific/GF25519Reflective/Common9_4Op.v index 5754b8c54..5fbb72c26 100644 --- a/src/Specific/GF25519Reflective/Common9_4Op.v +++ b/src/Specific/GF25519Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.Specific.GF25519BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded let (Hx7, Hx8) := (eta_and Hx78) in let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => op9_4_bounds_good bounds = true | None => False end) - : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : op9_4_correct_and_bounded ropW op. Proof. intros x0 x1 x2 x3 x4 x5 x6 x7 x8. intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8. |