diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v')
| -rw-r--r-- | src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v index 4143ad79b..a109ec89b 100644 --- a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Export Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations128. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Add. @@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2 (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) twice_d _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) P1 P2. -Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _ +Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF25519_64.fe25519_64 -> GF25519_64.fe25519_64 -> GF25519_64.fe25519_64) (x' y' : GF25519_64.fe25519_64) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_64 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519_64 interp_flat_type] in H. simpl @interp_base_type in *. @@ -103,14 +103,14 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe25519_64 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -121,7 +121,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519_64 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_64 add_coordinates]. intros. - unfold UnReturn at 13 14 15 16. + unfold invert_Return at 13 14 15 16. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -144,9 +144,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity |