From 6b3048c37ad348dc88ecc03ef892ecfb121bfa7f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 11 Jan 2017 21:02:50 -0500 Subject: Switch to fully uncurried form for reflection This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes. --- .../GF25519_32Reflective/Reified/LadderStep.v | 207 +++++++++++---------- 1 file changed, 106 insertions(+), 101 deletions(-) (limited to 'src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v') diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v index ae71337fd..36919539d 100644 --- a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v @@ -7,8 +7,9 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.SmartMap. Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.ExprInversion. -Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Eta. +Require Import Crypto.Reflection.EtaInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -18,6 +19,7 @@ Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Spec.MxDH. +Require Import Crypto.SpecificGen.GF25519_32Reflective.Common. Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Add. Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Sub. Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Mul. @@ -30,50 +32,80 @@ Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. Require Import Bedrock.Word. -(* XXX FIXME: Remove dummy code *) -Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2 +Definition rladderstepZ' var (T:=_) (a24 x0 : T) P1 P2 := @MxDH.ladderstep_gen _ - (fun x y => ApplyBinOp (proj1_sig raddZ_sig var) x y) - (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) - (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) + (fun x y => LetIn (Pair x y) (invert_Abs (proj1_sig raddZ_sig var))) + (fun x y => LetIn (Pair x y) (invert_Abs (proj1_sig rsubZ_sig var))) + (fun x y => LetIn (Pair x y) (invert_Abs (proj1_sig rmulZ_sig var))) a24 _ - (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)))) + (fun x y z w => (x, y, z, w)%expr) + (fun v f => LetIn v + (fun k => f (SmartVarf k))) x0 P1 P2. Definition rladderstepZ'' : Syntax.Expr _ _ _ - := Linearize (fun var - => apply9 - (fun A B => SmartAbs (A := A) (B := B)) - (fun dummy0 dummy1 dummy2 a24 x0 P10 P11 P20 P21 - => rladderstepZ' - var (Return dummy0) (Return dummy1) (Return dummy2) - (Return a24) (Return x0) - (Return P10, Return P11) - (Return P20, Return P21))). + := Linearize + (ExprEta + (fun var + => Abs (fun a24_x0_P1_P2 : interp_flat_type _ (_ * _ * ((_ * _) * (_ * _))) + => let '(a24, x0, ((P10, P11), (P20, P21))) + := a24_x0_P1_P2 in + rladderstepZ' + var (SmartVarf a24) (SmartVarf x0) + (SmartVarf P10, SmartVarf P11) + (SmartVarf P20, SmartVarf P21)))). -Definition ladderstep (T := _) - := fun (dummy0 dummy1 dummy2 a24 x0 P10 P11 P20 P21 : T) - => @MxDH.ladderstep_other_assoc - _ add sub mul - a24 x0 (P10, P11) (P20, P21). +Local Notation eta x := (fst x, snd x). + +Definition ladderstep_other_assoc {F Fadd Fsub Fmul} a24 (X1:F) (P1 P2:F*F) : F*F*F*F := + Eval cbv beta delta [MxDH.ladderstep_gen] in + @MxDH.ladderstep_gen + F Fadd Fsub Fmul a24 + (F*F*F*F) + (fun X3 Y3 Z3 T3 => (X3, Y3, Z3, T3)) + (fun x f => dlet y := x in f y) + X1 P1 P2. Definition uncurried_ladderstep - := apply9_nd - (@uncurry_unop_fe25519_32) - ladderstep. + := fun (a24_x0_P1_P2 : _ * _ * ((_ * _) * (_ * _))) + => let a24 := fst (fst a24_x0_P1_P2) in + let x0 := snd (fst a24_x0_P1_P2) in + let '(P1, P2) := eta (snd a24_x0_P1_P2) in + let '((P10, P11), (P20, P21)) := (eta P1, eta P2) in + @ladderstep_other_assoc + _ add sub mul + a24 x0 (P10, P11) (P20, P21). +Local Notation rexpr_sigPf T uncurried_op rexprZ x := + (Interp interp_op (t:=T) rexprZ x = uncurried_op x) + (only parsing). Local Notation rexpr_sigP T uncurried_op rexprZ := - (interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op) + (forall x, rexpr_sigPf T uncurried_op rexprZ x) (only parsing). Local Notation rexpr_sig T uncurried_op := { rexprZ | rexpr_sigP T uncurried_op rexprZ } (only parsing). +Local Ltac fold_interpf' := + let k := (eval unfold interpf, interpf_step in (@interpf base_type interp_base_type op interp_op)) in + let k' := fresh in + let H := fresh in + pose k as k'; + assert (H : @interpf base_type interp_base_type op interp_op = k') by reflexivity; + change k with k'; clearbody k'; subst k'. + +Local Ltac fold_interpf := + let k := (eval unfold interpf in (@interpf base_type interp_base_type op interp_op)) in + let k' := fresh in + let H := fresh in + pose k as k'; + assert (H : @interpf base_type interp_base_type op interp_op = k') by reflexivity; + change k with k'; clearbody k'; subst k'; + fold_interpf'. + Local Ltac repeat_step_interpf := let k := (eval unfold interpf in (@interpf base_type interp_base_type op interp_op)) in let k' := fresh in @@ -83,51 +115,14 @@ Local Ltac repeat_step_interpf := repeat (unfold interpf_step at 1; change k with k' at 1); clearbody k'; subst k'. -Lemma interp_helper - (f : Syntax.Expr base_type op ExprBinOpT) - (x y : exprArg interp_base_type) - (f' : GF25519_32.fe25519_32 -> GF25519_32.fe25519_32 -> GF25519_32.fe25519_32) - (x' y' : GF25519_32.fe25519_32) - (H : interp_type_gen_rel_pointwise - (fun _ => Logic.eq) - (Interp interp_op f) (uncurry_binop_fe25519_32 f')) - (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_32 interp_flat_type] in H. - simpl @interp_base_type in *. - cbv [GF25519_32.fe25519_32] in x', y'. - destruct_head' prod. - rewrite <- H; clear H. - cbv [ExprArgT] in *; simpl in *. - rewrite Hx, Hy; clear Hx Hy. - unfold Let_In; simpl. - cbv [Interp]. - simpl @interp_type. - 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_32 Apply' interp fst snd]. - let f := match goal with f : expr _ _ _ |- _ => f end in - rewrite (invert_Abs_Some (e:=f) eq_refl). - repeat match goal with - | [ |- appcontext[invert_Abs ?f ?x] ] - => generalize (invert_Abs f x); clear f; - let f' := fresh "f" in - intro f'; - first [ rewrite (invert_Abs_Some (e:=f') eq_refl) - | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] - end. - reflexivity. -Qed. - -Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''. +Lemma rladderstepZ_sigP' : rexpr_sigP _ uncurried_ladderstep rladderstepZ''. Proof. cbv [rladderstepZ'']. - etransitivity; [ apply InterpLinearize | ]. - cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_32 ladderstep]. - intros; cbv beta zeta. - unfold invert_Return at 14 15 16 17. + intro x; rewrite InterpLinearize, InterpExprEta. + cbv [domain interp_flat_type interp_base_type] in x. + destruct_head' prod. + cbv [invert_Abs domain codomain Interp interp SmartVarf smart_interp_flat_map fst snd]. + cbv [rladderstepZ' MxDH.ladderstep_gen uncurried_ladderstep SmartVarf smart_interp_flat_map]; simpl @fst; simpl @snd. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -137,48 +132,58 @@ Proof. set (k' := @proj1_sig A B k); pose proof (proj2_sig k) as H; change (proj1_sig k) with k' in H; - clearbody k'; clear k + clearbody k'; clear k; + cbv beta in * end. - unfold interpf; repeat_step_interpf. - unfold interpf at 14 15 16; unfold interpf_step. - cbv beta iota delta [MxDH.ladderstep_other_assoc]. - repeat match goal with - | [ |- (dlet x := ?y in @?z x) = (let x' := ?y' in @?z' x') ] - => refine ((fun pf0 pf1 => @Proper_Let_In_nd_changebody _ _ Logic.eq _ y y' pf0 z z' pf1) - (_ : y = y') - (_ : forall x, z x = z' x)); - cbv beta; intros - end; - repeat match goal with - | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] - => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] - => vm_compute; reflexivity - | [ |- (_, _) = (_, _) ] - => reflexivity - | _ => simpl; rewrite <- !surjective_pairing; reflexivity - end. -Time Qed. - -Definition rladderstepZ_sig : rexpr_9_4op_sig ladderstep. + cbv [Interp Curry.curry2] in *. + unfold interpf, interpf_step; fold_interpf. + cbv [ladderstep_other_assoc interp_flat_type GF25519_32.fe25519_32]. + Time + abstract ( + repeat match goal with + | [ |- (dlet x := ?y in @?z x) = (dlet x' := ?y' in @?z' x') ] + => refine ((fun pf0 pf1 => @Proper_Let_In_nd_changebody _ _ Logic.eq _ y y' pf0 z z' pf1) + (_ : y = y') + (_ : forall x, z x = z' x)); + cbv beta; intros; + [ cbv [Let_In Common.ExprBinOpT] | ] + end; + repeat match goal with + | _ => rewrite !interpf_invert_Abs + | _ => rewrite_hyp !* + | _ => progress cbv [interp_base_type] + | [ |- ?x = ?x ] => reflexivity + | _ => rewrite <- !surjective_pairing + end + ). +Time Defined. +Lemma rladderstepZ_sigP : rexpr_sigP _ uncurried_ladderstep rladderstepZ''. Proof. - eexists. - apply rladderstepZ_sigP. -Defined. + exact rladderstepZ_sigP'. +Qed. +Definition rladderstepZ_sig + := exist (fun v => rexpr_sigP _ _ v) rladderstepZ'' rladderstepZ_sigP. + +Definition rladderstep_input_bounds + := (ExprUnOp_bounds, ExprUnOp_bounds, + ((ExprUnOp_bounds, ExprUnOp_bounds), + (ExprUnOp_bounds, ExprUnOp_bounds))). Time Definition rladderstepW := Eval vm_compute in rword_of_Z rladderstepZ_sig. Lemma rladderstepW_correct_and_bounded_gen : correct_and_bounded_genT rladderstepW rladderstepZ_sig. Proof. Time rexpr_correct. Time Qed. -Definition rladderstep_output_bounds := Eval vm_compute in compute_bounds rladderstepW Expr9Op_bounds. +Definition rladderstep_output_bounds := Eval vm_compute in compute_bounds rladderstepW rladderstep_input_bounds. Local Obligation Tactic := intros; vm_compute; constructor. +(* Program Definition rladderstepW_correct_and_bounded := Expr9_4Op_correct_and_bounded - rladderstepW ladderstep rladderstepZ_sig rladderstepW_correct_and_bounded_gen + rladderstepW uncurried_ladderstep rladderstepZ_sig rladderstepW_correct_and_bounded_gen _ _. + *) Local Open Scope string_scope. -Compute ("Ladderstep", compute_bounds_for_display rladderstepW Expr9Op_bounds). -Compute ("Ladderstep overflows? ", sanity_compute rladderstepW Expr9Op_bounds). -Compute ("Ladderstep overflows (error if it does)? ", sanity_check rladderstepW Expr9Op_bounds). +Compute ("Ladderstep", compute_bounds_for_display rladderstepW rladderstep_input_bounds). +Compute ("Ladderstep overflows? ", sanity_compute rladderstepW rladderstep_input_bounds). +Compute ("Ladderstep overflows (error if it does)? ", sanity_check rladderstepW rladderstep_input_bounds). -- cgit v1.2.3