diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v')
-rw-r--r-- | src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v index d6b8bb2c7..fcc07a651 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded (Hx : is_bounded (fe25519_64WToZ x) = true), let args := unop_args_to_bounded x Hx 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 @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded let args := unop_args_to_bounded x Hx 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 => unopFEToZ_bounds_good bounds = true | None => False end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. + : unop_FEToZ_correct ropW op. Proof. intros x Hx. pose x as x'. |