From 0c9d07989d2e17124e15513a836139b1bd4a8748 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 7 Jan 2017 21:43:23 -0500 Subject: copy_bounds --- .../GF2213_32Reflective/Reified/LadderStep.v | 182 +++++++++++++++++++++ .../GF2519_32Reflective/Reified/LadderStep.v | 182 +++++++++++++++++++++ .../GF25519_32Reflective/Reified/LadderStep.v | 182 +++++++++++++++++++++ .../GF25519_64Reflective/Reified/LadderStep.v | 182 +++++++++++++++++++++ .../GF41417_32Reflective/Reified/LadderStep.v | 182 +++++++++++++++++++++ .../GF5211_32Reflective/Reified/LadderStep.v | 182 +++++++++++++++++++++ 6 files changed, 1092 insertions(+) create mode 100644 src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v create mode 100644 src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v create mode 100644 src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v create mode 100644 src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v create mode 100644 src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v (limited to 'src/SpecificGen') diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v new file mode 100644 index 000000000..18bbd8289 --- /dev/null +++ b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v @@ -0,0 +1,182 @@ +Require Export Coq.ZArith.ZArith. +Require Export Coq.Strings.String. +Require Export Crypto.SpecificGen.GF2213_32. +Require Export Crypto.SpecificGen.GF2213_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +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.Spec.MxDH. +Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Add. +Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Sub. +Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Mul. +Require Import Crypto.SpecificGen.GF2213_32Reflective.Common9_4Op. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.HList. +Require Import Crypto.Util.Tower. +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 + := @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) + a24 + _ + (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) + (fun v f => LetIn (UnReturn v) + (fun k => f (Return (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))). + +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). + +Definition uncurried_ladderstep + := apply9_nd + (@uncurry_unop_fe2213_32) + ladderstep. + +Local Notation rexpr_sigP T uncurried_op rexprZ := + (interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op) + (only parsing). +Local Notation rexpr_sig T uncurried_op := + { rexprZ | rexpr_sigP T uncurried_op rexprZ } + (only parsing). + +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 + let H := fresh in + pose k as k'; + assert (H : @interpf base_type interp_base_type op interp_op = k') by reflexivity; + repeat (unfold interpf_step at 1; change k with k' at 1); + 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' : GF2213_32.fe2213_32 -> GF2213_32.fe2213_32 -> GF2213_32.fe2213_32) + (x' y' : GF2213_32.fe2213_32) + (H : interp_type_gen_rel_pointwise + (fun _ => Logic.eq) + (Interp interp_op f) (uncurry_binop_fe2213_32 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'. +Proof. + cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe2213_32 interp_flat_type] in H. + simpl @interp_base_type in *. + cbv [GF2213_32.fe2213_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_fe2213_32 Apply' interp fst snd]. + rewrite <- (UnAbs_eta f). + repeat match goal with + | [ |- appcontext[UnAbs ?f ?x] ] + => generalize (UnAbs f x); clear f; + let f' := fresh "f" in + intro f'; + first [ rewrite <- (UnAbs_eta f') + | rewrite <- (UnReturn_eta f') ] + end. + reflexivity. +Qed. + +Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''. +Proof. + cbv [rladderstepZ'']. + etransitivity; [ apply Interp_Linearize | ]. + cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe2213_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32 ladderstep]. + intros; cbv beta zeta. + unfold UnReturn at 14 15 16 17. + repeat match goal with + | [ |- appcontext[@proj1_sig ?A ?B ?v] ] + => let k := fresh "f" in + let k' := fresh "f" in + let H := fresh in + set (k := v); + 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 + 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 (UnReturn (ApplyBinOp _ _ _)) = _ ] + => apply interp_helper; [ assumption | | ] + | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + => vm_compute; reflexivity + | [ |- (_, _) = (_, _) ] + => reflexivity + | _ => simpl; rewrite <- !surjective_pairing; reflexivity + end. +Time Qed. + +Definition rladderstepZ_sig : rexpr_9_4op_sig ladderstep. +Proof. + eexists. + apply rladderstepZ_sigP. +Defined. + +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. + +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 + _ _. + +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). diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v new file mode 100644 index 000000000..e5ea0e52b --- /dev/null +++ b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v @@ -0,0 +1,182 @@ +Require Export Coq.ZArith.ZArith. +Require Export Coq.Strings.String. +Require Export Crypto.SpecificGen.GF2519_32. +Require Export Crypto.SpecificGen.GF2519_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +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.Spec.MxDH. +Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Add. +Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Sub. +Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Mul. +Require Import Crypto.SpecificGen.GF2519_32Reflective.Common9_4Op. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.HList. +Require Import Crypto.Util.Tower. +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 + := @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) + a24 + _ + (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) + (fun v f => LetIn (UnReturn v) + (fun k => f (Return (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))). + +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). + +Definition uncurried_ladderstep + := apply9_nd + (@uncurry_unop_fe2519_32) + ladderstep. + +Local Notation rexpr_sigP T uncurried_op rexprZ := + (interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op) + (only parsing). +Local Notation rexpr_sig T uncurried_op := + { rexprZ | rexpr_sigP T uncurried_op rexprZ } + (only parsing). + +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 + let H := fresh in + pose k as k'; + assert (H : @interpf base_type interp_base_type op interp_op = k') by reflexivity; + repeat (unfold interpf_step at 1; change k with k' at 1); + 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' : GF2519_32.fe2519_32 -> GF2519_32.fe2519_32 -> GF2519_32.fe2519_32) + (x' y' : GF2519_32.fe2519_32) + (H : interp_type_gen_rel_pointwise + (fun _ => Logic.eq) + (Interp interp_op f) (uncurry_binop_fe2519_32 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'. +Proof. + cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe2519_32 interp_flat_type] in H. + simpl @interp_base_type in *. + cbv [GF2519_32.fe2519_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_fe2519_32 Apply' interp fst snd]. + rewrite <- (UnAbs_eta f). + repeat match goal with + | [ |- appcontext[UnAbs ?f ?x] ] + => generalize (UnAbs f x); clear f; + let f' := fresh "f" in + intro f'; + first [ rewrite <- (UnAbs_eta f') + | rewrite <- (UnReturn_eta f') ] + end. + reflexivity. +Qed. + +Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''. +Proof. + cbv [rladderstepZ'']. + etransitivity; [ apply Interp_Linearize | ]. + cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe2519_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2519_32 ladderstep]. + intros; cbv beta zeta. + unfold UnReturn at 14 15 16 17. + repeat match goal with + | [ |- appcontext[@proj1_sig ?A ?B ?v] ] + => let k := fresh "f" in + let k' := fresh "f" in + let H := fresh in + set (k := v); + 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 + 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 (UnReturn (ApplyBinOp _ _ _)) = _ ] + => apply interp_helper; [ assumption | | ] + | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + => vm_compute; reflexivity + | [ |- (_, _) = (_, _) ] + => reflexivity + | _ => simpl; rewrite <- !surjective_pairing; reflexivity + end. +Time Qed. + +Definition rladderstepZ_sig : rexpr_9_4op_sig ladderstep. +Proof. + eexists. + apply rladderstepZ_sigP. +Defined. + +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. + +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 + _ _. + +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). diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v new file mode 100644 index 000000000..9fc865d98 --- /dev/null +++ b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v @@ -0,0 +1,182 @@ +Require Export Coq.ZArith.ZArith. +Require Export Coq.Strings.String. +Require Export Crypto.SpecificGen.GF25519_32. +Require Export Crypto.SpecificGen.GF25519_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +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.Spec.MxDH. +Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Add. +Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Sub. +Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Mul. +Require Import Crypto.SpecificGen.GF25519_32Reflective.Common9_4Op. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.HList. +Require Import Crypto.Util.Tower. +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 + := @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) + a24 + _ + (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) + (fun v f => LetIn (UnReturn v) + (fun k => f (Return (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))). + +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). + +Definition uncurried_ladderstep + := apply9_nd + (@uncurry_unop_fe25519_32) + ladderstep. + +Local Notation rexpr_sigP T uncurried_op rexprZ := + (interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op) + (only parsing). +Local Notation rexpr_sig T uncurried_op := + { rexprZ | rexpr_sigP T uncurried_op rexprZ } + (only parsing). + +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 + let H := fresh in + pose k as k'; + assert (H : @interpf base_type interp_base_type op interp_op = k') by reflexivity; + repeat (unfold interpf_step at 1; change k with k' at 1); + 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' : 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 (UnReturn x) = x') + (Hy : interpf interp_op (UnReturn y) = y') + : interpf interp_op (UnReturn (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]. + rewrite <- (UnAbs_eta f). + repeat match goal with + | [ |- appcontext[UnAbs ?f ?x] ] + => generalize (UnAbs f x); clear f; + let f' := fresh "f" in + intro f'; + first [ rewrite <- (UnAbs_eta f') + | rewrite <- (UnReturn_eta f') ] + end. + reflexivity. +Qed. + +Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''. +Proof. + cbv [rladderstepZ'']. + etransitivity; [ apply Interp_Linearize | ]. + 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 UnReturn at 14 15 16 17. + repeat match goal with + | [ |- appcontext[@proj1_sig ?A ?B ?v] ] + => let k := fresh "f" in + let k' := fresh "f" in + let H := fresh in + set (k := v); + 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 + 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 (UnReturn (ApplyBinOp _ _ _)) = _ ] + => apply interp_helper; [ assumption | | ] + | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + => vm_compute; reflexivity + | [ |- (_, _) = (_, _) ] + => reflexivity + | _ => simpl; rewrite <- !surjective_pairing; reflexivity + end. +Time Qed. + +Definition rladderstepZ_sig : rexpr_9_4op_sig ladderstep. +Proof. + eexists. + apply rladderstepZ_sigP. +Defined. + +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. + +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 + _ _. + +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). diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v new file mode 100644 index 000000000..38bd20c08 --- /dev/null +++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v @@ -0,0 +1,182 @@ +Require Export Coq.ZArith.ZArith. +Require Export Coq.Strings.String. +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.Application. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Z.Interpretations128. +Require Crypto.Reflection.Z.Interpretations128.Relations. +Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. +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.Spec.MxDH. +Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Add. +Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Sub. +Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Mul. +Require Import Crypto.SpecificGen.GF25519_64Reflective.Common9_4Op. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.HList. +Require Import Crypto.Util.Tower. +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 + := @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) + a24 + _ + (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) + (fun v f => LetIn (UnReturn v) + (fun k => f (Return (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))). + +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). + +Definition uncurried_ladderstep + := apply9_nd + (@uncurry_unop_fe25519_64) + ladderstep. + +Local Notation rexpr_sigP T uncurried_op rexprZ := + (interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op) + (only parsing). +Local Notation rexpr_sig T uncurried_op := + { rexprZ | rexpr_sigP T uncurried_op rexprZ } + (only parsing). + +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 + let H := fresh in + pose k as k'; + assert (H : @interpf base_type interp_base_type op interp_op = k') by reflexivity; + repeat (unfold interpf_step at 1; change k with k' at 1); + 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' : 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'. +Proof. + cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519_64 interp_flat_type] in H. + simpl @interp_base_type in *. + cbv [GF25519_64.fe25519_64] 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_64 Apply' interp fst snd]. + rewrite <- (UnAbs_eta f). + repeat match goal with + | [ |- appcontext[UnAbs ?f ?x] ] + => generalize (UnAbs f x); clear f; + let f' := fresh "f" in + intro f'; + first [ rewrite <- (UnAbs_eta f') + | rewrite <- (UnReturn_eta f') ] + end. + reflexivity. +Qed. + +Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''. +Proof. + cbv [rladderstepZ'']. + etransitivity; [ apply Interp_Linearize | ]. + cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519_64 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_64 ladderstep]. + intros; cbv beta zeta. + unfold UnReturn at 14 15 16 17. + repeat match goal with + | [ |- appcontext[@proj1_sig ?A ?B ?v] ] + => let k := fresh "f" in + let k' := fresh "f" in + let H := fresh in + set (k := v); + 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 + 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 (UnReturn (ApplyBinOp _ _ _)) = _ ] + => apply interp_helper; [ assumption | | ] + | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + => vm_compute; reflexivity + | [ |- (_, _) = (_, _) ] + => reflexivity + | _ => simpl; rewrite <- !surjective_pairing; reflexivity + end. +Time Qed. + +Definition rladderstepZ_sig : rexpr_9_4op_sig ladderstep. +Proof. + eexists. + apply rladderstepZ_sigP. +Defined. + +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. + +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 + _ _. + +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). diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v new file mode 100644 index 000000000..7384553a5 --- /dev/null +++ b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v @@ -0,0 +1,182 @@ +Require Export Coq.ZArith.ZArith. +Require Export Coq.Strings.String. +Require Export Crypto.SpecificGen.GF41417_32. +Require Export Crypto.SpecificGen.GF41417_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +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.Spec.MxDH. +Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Add. +Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Sub. +Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Mul. +Require Import Crypto.SpecificGen.GF41417_32Reflective.Common9_4Op. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.HList. +Require Import Crypto.Util.Tower. +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 + := @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) + a24 + _ + (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) + (fun v f => LetIn (UnReturn v) + (fun k => f (Return (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))). + +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). + +Definition uncurried_ladderstep + := apply9_nd + (@uncurry_unop_fe41417_32) + ladderstep. + +Local Notation rexpr_sigP T uncurried_op rexprZ := + (interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op) + (only parsing). +Local Notation rexpr_sig T uncurried_op := + { rexprZ | rexpr_sigP T uncurried_op rexprZ } + (only parsing). + +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 + let H := fresh in + pose k as k'; + assert (H : @interpf base_type interp_base_type op interp_op = k') by reflexivity; + repeat (unfold interpf_step at 1; change k with k' at 1); + 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' : GF41417_32.fe41417_32 -> GF41417_32.fe41417_32 -> GF41417_32.fe41417_32) + (x' y' : GF41417_32.fe41417_32) + (H : interp_type_gen_rel_pointwise + (fun _ => Logic.eq) + (Interp interp_op f) (uncurry_binop_fe41417_32 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'. +Proof. + cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe41417_32 interp_flat_type] in H. + simpl @interp_base_type in *. + cbv [GF41417_32.fe41417_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_fe41417_32 Apply' interp fst snd]. + rewrite <- (UnAbs_eta f). + repeat match goal with + | [ |- appcontext[UnAbs ?f ?x] ] + => generalize (UnAbs f x); clear f; + let f' := fresh "f" in + intro f'; + first [ rewrite <- (UnAbs_eta f') + | rewrite <- (UnReturn_eta f') ] + end. + reflexivity. +Qed. + +Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''. +Proof. + cbv [rladderstepZ'']. + etransitivity; [ apply Interp_Linearize | ]. + cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe41417_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe41417_32 ladderstep]. + intros; cbv beta zeta. + unfold UnReturn at 14 15 16 17. + repeat match goal with + | [ |- appcontext[@proj1_sig ?A ?B ?v] ] + => let k := fresh "f" in + let k' := fresh "f" in + let H := fresh in + set (k := v); + 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 + 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 (UnReturn (ApplyBinOp _ _ _)) = _ ] + => apply interp_helper; [ assumption | | ] + | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + => vm_compute; reflexivity + | [ |- (_, _) = (_, _) ] + => reflexivity + | _ => simpl; rewrite <- !surjective_pairing; reflexivity + end. +Time Qed. + +Definition rladderstepZ_sig : rexpr_9_4op_sig ladderstep. +Proof. + eexists. + apply rladderstepZ_sigP. +Defined. + +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. + +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 + _ _. + +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). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v new file mode 100644 index 000000000..71cb965a9 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v @@ -0,0 +1,182 @@ +Require Export Coq.ZArith.ZArith. +Require Export Coq.Strings.String. +Require Export Crypto.SpecificGen.GF5211_32. +Require Export Crypto.SpecificGen.GF5211_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +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.Spec.MxDH. +Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Add. +Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Sub. +Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Mul. +Require Import Crypto.SpecificGen.GF5211_32Reflective.Common9_4Op. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.HList. +Require Import Crypto.Util.Tower. +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 + := @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) + a24 + _ + (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) + (fun v f => LetIn (UnReturn v) + (fun k => f (Return (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))). + +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). + +Definition uncurried_ladderstep + := apply9_nd + (@uncurry_unop_fe5211_32) + ladderstep. + +Local Notation rexpr_sigP T uncurried_op rexprZ := + (interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op) + (only parsing). +Local Notation rexpr_sig T uncurried_op := + { rexprZ | rexpr_sigP T uncurried_op rexprZ } + (only parsing). + +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 + let H := fresh in + pose k as k'; + assert (H : @interpf base_type interp_base_type op interp_op = k') by reflexivity; + repeat (unfold interpf_step at 1; change k with k' at 1); + 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' : GF5211_32.fe5211_32 -> GF5211_32.fe5211_32 -> GF5211_32.fe5211_32) + (x' y' : GF5211_32.fe5211_32) + (H : interp_type_gen_rel_pointwise + (fun _ => Logic.eq) + (Interp interp_op f) (uncurry_binop_fe5211_32 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'. +Proof. + cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe5211_32 interp_flat_type] in H. + simpl @interp_base_type in *. + cbv [GF5211_32.fe5211_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_fe5211_32 Apply' interp fst snd]. + rewrite <- (UnAbs_eta f). + repeat match goal with + | [ |- appcontext[UnAbs ?f ?x] ] + => generalize (UnAbs f x); clear f; + let f' := fresh "f" in + intro f'; + first [ rewrite <- (UnAbs_eta f') + | rewrite <- (UnReturn_eta f') ] + end. + reflexivity. +Qed. + +Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''. +Proof. + cbv [rladderstepZ'']. + etransitivity; [ apply Interp_Linearize | ]. + cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe5211_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe5211_32 ladderstep]. + intros; cbv beta zeta. + unfold UnReturn at 14 15 16 17. + repeat match goal with + | [ |- appcontext[@proj1_sig ?A ?B ?v] ] + => let k := fresh "f" in + let k' := fresh "f" in + let H := fresh in + set (k := v); + 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 + 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 (UnReturn (ApplyBinOp _ _ _)) = _ ] + => apply interp_helper; [ assumption | | ] + | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + => vm_compute; reflexivity + | [ |- (_, _) = (_, _) ] + => reflexivity + | _ => simpl; rewrite <- !surjective_pairing; reflexivity + end. +Time Qed. + +Definition rladderstepZ_sig : rexpr_9_4op_sig ladderstep. +Proof. + eexists. + apply rladderstepZ_sigP. +Defined. + +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. + +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 + _ _. + +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). -- cgit v1.2.3