diff options
author | Jason Gross <jagro@google.com> | 2018-07-27 23:24:51 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-07-30 10:23:21 -0400 |
commit | fedf83bf32b26197dc89f0aae9b856e2107ec5d4 (patch) | |
tree | 2fea63839c2c808a1f431a724895adb37d0e03de | |
parent | 72f95797120adf1f6447a37c8ec205092401437d (diff) |
Integrate Wf and Interp proofs
Now the only admits remaining in Toplevel1 are glue ones about
freeze/to_bytes/from_bytes/fe_nonzero. What remains (beyond those
admits, and the ones about word-by-word montgomery building blocks in
Arithmetic), are the proofs about abstract interpretation and the
rewriter.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------
12m13.17s | Total | 11m45.42s || +0m27.75s | +3.93%
--------------------------------------------------------------------------------------------------------
3m47.20s | Experiments/NewPipeline/Toplevel1 | 3m27.51s || +0m19.68s | +9.48%
0m17.98s | Experiments/NewPipeline/UnderLetsProofs | N/A || +0m17.98s | ∞
N/A | Experiments/NewPipeline/UnderLetsWf | 0m17.94s || -0m17.94s | -100.00%
4m49.57s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 4m45.22s || +0m04.34s | +1.52%
1m16.28s | Experiments/NewPipeline/Toplevel2 | 1m13.33s || +0m02.95s | +4.02%
0m02.96s | Experiments/NewPipeline/MiscCompilerPassesProofs | N/A || +0m02.96s | ∞
N/A | Experiments/NewPipeline/MiscCompilerPassesWf | 0m02.91s || -0m02.91s | -100.00%
0m58.32s | Experiments/NewPipeline/Rewriter | 0m58.58s || -0m00.25s | -0.44%
0m28.19s | Experiments/NewPipeline/LanguageInversion | 0m28.02s || +0m00.17s | +0.60%
0m13.14s | Experiments/NewPipeline/LanguageWf | 0m13.09s || +0m00.05s | +0.38%
0m10.11s | Experiments/NewPipeline/CStringification | 0m10.12s || -0m00.00s | -0.09%
0m01.21s | Experiments/NewPipeline/CLI | 0m01.19s || +0m00.02s | +1.68%
0m01.11s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.13s || -0m00.01s | -1.76%
0m01.09s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes | 0m01.08s || +0m00.01s | +0.92%
0m01.05s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.07s || -0m00.02s | -1.86%
0m00.98s | Experiments/NewPipeline/Language | 0m00.96s || +0m00.02s | +2.08%
0m00.96s | Experiments/NewPipeline/AbstractInterpretation | 0m00.90s || +0m00.05s | +6.66%
0m00.90s | Experiments/NewPipeline/CompilersTestCases | 0m00.92s || -0m00.02s | -2.17%
0m00.66s | Experiments/NewPipeline/RewriterProofs | N/A || +0m00.66s | ∞
0m00.64s | Experiments/NewPipeline/MiscCompilerPasses | 0m00.65s || -0m00.01s | -1.53%
0m00.42s | Experiments/NewPipeline/UnderLets | 0m00.38s || +0m00.03s | +10.52%
0m00.40s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m00.42s || -0m00.01s | -4.76%
-rw-r--r-- | _CoqProject | 5 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretationProofs.v | 69 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Language.v | 9 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 46 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/MiscCompilerPassesProofs.v (renamed from src/Experiments/NewPipeline/MiscCompilerPassesWf.v) | 14 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/RewriterProofs.v | 59 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 997 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 6 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/UnderLetsProofs.v (renamed from src/Experiments/NewPipeline/UnderLetsWf.v) | 6 |
9 files changed, 785 insertions, 426 deletions
diff --git a/_CoqProject b/_CoqProject index 31c52a268..fc49cbf15 100644 --- a/_CoqProject +++ b/_CoqProject @@ -253,15 +253,16 @@ src/Experiments/NewPipeline/Language.v src/Experiments/NewPipeline/LanguageInversion.v src/Experiments/NewPipeline/LanguageWf.v src/Experiments/NewPipeline/MiscCompilerPasses.v -src/Experiments/NewPipeline/MiscCompilerPassesWf.v +src/Experiments/NewPipeline/MiscCompilerPassesProofs.v src/Experiments/NewPipeline/Rewriter.v +src/Experiments/NewPipeline/RewriterProofs.v src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v src/Experiments/NewPipeline/StandaloneHaskellMain.v src/Experiments/NewPipeline/StandaloneOCamlMain.v src/Experiments/NewPipeline/Toplevel1.v src/Experiments/NewPipeline/Toplevel2.v src/Experiments/NewPipeline/UnderLets.v -src/Experiments/NewPipeline/UnderLetsWf.v +src/Experiments/NewPipeline/UnderLetsProofs.v src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.v src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.v diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v index 560f89199..60007288f 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v @@ -3,41 +3,88 @@ Require Import Crypto.Util.Sum. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Experiments.NewPipeline.LanguageInversion. +Require Import Crypto.Experiments.NewPipeline.LanguageWf. +Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. Local Open Scope Z_scope. Module Compilers. - Export Language.Compilers. - Export UnderLets.Compilers. - Export AbstractInterpretation.Compilers. + Import Language.Compilers. + Import UnderLets.Compilers. + Import AbstractInterpretation.Compilers. + Import LanguageInversion.Compilers. + Import LanguageWf.Compilers. + Import UnderLetsProofs.Compilers. Import invert_expr. Import defaults. + Module Import partial. + Import AbstractInterpretation.Compilers.partial. + Section with_var2. + Context {var1 var2 : type -> Type}. + + Lemma wf_eta_expand_with_bound G {t} e1 e2 b_in (Hwf : @expr.wf _ _ var1 var2 G t e1 e2) + : expr.wf G (eta_expand_with_bound e1 b_in) (eta_expand_with_bound e2 b_in). + Proof. + cbv [eta_expand_with_bound ident.eta_expand_with_bound eta_expand_with_bound']. + Admitted. + End with_var2. + + Lemma Wf_EtaExpandWithBound {t} (E : Expr t) b_in (Hwf : Wf E) + : Wf (EtaExpandWithBound E b_in). + Proof. repeat intro; apply wf_eta_expand_with_bound, Hwf. Qed. + End partial. + Axiom admit_pf : False. Local Notation admit := (match admit_pf with end). + Lemma Wf_PartialEvaluateWithListInfoFromBounds + {t} (E : Expr t) + (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) + (Hwf : Wf E) + : Wf (PartialEvaluateWithListInfoFromBounds E b_in). + Proof. apply Wf_EtaExpandWithBound, Hwf. Qed. + + Lemma Interp_PartialEvaluateWithListInfoFromBounds + {t} (E : Expr t) + (Hwf : Wf E) + (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) + : forall arg1 arg2 + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2) + (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true), + type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds E b_in)) arg1 = type.app_curried (Interp E) arg2. + Proof. + Admitted. + + Hint Resolve Wf_EtaExpandWithBound Wf_PartialEvaluateWithListInfoFromBounds : wf. + Theorem CheckedPartialEvaluateWithBounds_Correct (relax_zrange : zrange -> option zrange) (Hrelax : forall r r' z, is_tighter_than_bool z r = true -> relax_zrange r = Some r' -> is_tighter_than_bool z r' = true) {t} (E : Expr t) + (Hwf : Wf E) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (b_out : ZRange.type.base.option.interp (type.final_codomain t)) rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange E b_in b_out = inl rv) - : forall arg - (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg = true), - ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg) = true - /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg - = type.app_curried (Interp E) arg. + : forall arg1 arg2 + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2) + (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true), + ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg1) = true + /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1 + = type.app_curried (Interp E) arg2. Proof. cbv [CheckedPartialEvaluateWithBounds CheckPartialEvaluateWithBounds Let_In] in *; break_innermost_match_hyps; inversion_sum; subst. - intros arg Harg. + intros arg1 arg2 Harg12 Harg1. split. { eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ]. - revert Harg. + clear dependent arg2. + revert Harg1. exact admit. (* boundedness *) } - { exact admit. (* correctness of interp *) } + { intro cast_outside_of_range; revert cast_outside_of_range Harg12. + exact admit. (* correctness of interp *) } Qed. End Compilers. diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index afd028ee8..6c31dd0d9 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -143,6 +143,15 @@ Module Compilers. | arrow s d => fun x_xs y_ys => R s (fst x_xs) (fst y_ys) && @andb_bool_for_each_lhs_of_arrow _ f g R d (snd x_xs) (snd y_ys) end%bool. + Fixpoint and_for_each_lhs_of_arrow {base_type} {f g : type base_type -> Type} + (R : forall t, f t -> g t -> Prop) + {t} + : for_each_lhs_of_arrow f t -> for_each_lhs_of_arrow g t -> Prop + := match t with + | base t => fun _ _ => True + | arrow s d => fun x_xs y_ys => R s (fst x_xs) (fst y_ys) /\ @and_for_each_lhs_of_arrow _ f g R d (snd x_xs) (snd y_ys) + end. + Section interpM. Context {base_type} (M : Type -> Type) (base_interp : base_type -> Type). (** half-monadic denotation function; denote [type]s into their diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index c8b19a5f4..4f4a2f473 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -26,6 +26,10 @@ Module Compilers. Import Language.Compilers. Import LanguageInversion.Compilers. Import expr.Notations. + + Create HintDb wf discriminated. + Create HintDb interp discriminated. + Module type. Section eqv. Context {base_type} {interp_base_type : base_type -> Type}. @@ -43,6 +47,37 @@ Module Compilers. etransitivity; first [ eassumption | symmetry; eassumption ]. Qed. End eqv. + + Section app_curried_instances. + Context {base_type} {base_interp : base_type -> Type}. + (* Might want to add the following to make [app_curried_Proper] usable by [setoid_rewrite]? *) + (* See https://github.com/coq/coq/issues/8179 +<< +Lemma PER_valid_l {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R x. +Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed. +Lemma PER_valid_r {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R y. +Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed. +Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_l _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances. +Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances. +>> +*) + Lemma app_curried_Proper {t} + : Proper (@type.eqv base_type base_interp t ==> type.and_for_each_lhs_of_arrow (@type.eqv _ _) ==> eq) + (@type.app_curried base_type base_interp t). + Proof. + cbv [Proper respectful]; induction t; cbn [type.eqv type.app_curried]; cbv [Proper respectful]; [ intros; subst; reflexivity | ]. + intros f g Hfg x y [Hxy ?]; eauto. + Qed. + Global Instance and_for_each_lhs_of_arrow_Reflexive {f} {R} {_ : forall t, Reflexive (R t)} {t} + : Reflexive (@type.and_for_each_lhs_of_arrow base_type f f R t). + Proof. cbv [Reflexive] in *; induction t; cbn; repeat split; eauto. Qed. + Global Instance and_for_each_lhs_of_arrow_Symmetric {f} {R} {_ : forall t, Symmetric (R t)} {t} + : Symmetric (@type.and_for_each_lhs_of_arrow base_type f f R t). + Proof. cbv [Symmetric] in *; induction t; cbn; repeat split; intuition eauto. Qed. + Global Instance and_for_each_lhs_of_arrow_Transitive {f} {R} {_ : forall t, Transitive (R t)} {t} + : Transitive (@type.and_for_each_lhs_of_arrow base_type f f R t). + Proof. cbv [Transitive] in *; induction t; cbn; repeat split; intuition eauto. Qed. + End app_curried_instances. End type. Module ident. @@ -444,6 +479,11 @@ Module Compilers. Notation Interp_Reify := Interp_Reify_as. End expr. + Hint Resolve expr.Wf_Reify : wf. + Hint Rewrite @expr.Interp_Reify @expr.interp_reify @expr.interp_reify_list : interp. + + Notation Wf := expr.Wf. + Local Ltac destructure_step := first [ progress subst | progress inversion_option @@ -798,6 +838,10 @@ Module Compilers. Ltac prove_Wf _ := lazymatch goal with - | [ |- expr.Wf ?e ] => apply (@GeneralizeVar.Wf_via_flat _ e); vm_compute; split; reflexivity + | [ |- expr.Wf ?e ] => apply (@GeneralizeVar.Wf_via_flat _ e); vm_cast_no_check (conj (eq_refl e) (eq_refl true)) end. + + Global Hint Extern 0 (?x == ?x) => apply expr.Wf_Interp_Proper : wf interp. + Hint Resolve GeneralizeVar.Wf_FromFlat_ToFlat GeneralizeVar.Wf_GeneralizeVar : wf. + Hint Rewrite @GeneralizeVar.Interp_GeneralizeVar @GeneralizeVar.Interp_FromFlat_ToFlat : interp. End Compilers. diff --git a/src/Experiments/NewPipeline/MiscCompilerPassesWf.v b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v index 50211feb3..52101023a 100644 --- a/src/Experiments/NewPipeline/MiscCompilerPassesWf.v +++ b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v @@ -15,14 +15,6 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.ListUtil. Import ListNotations. Local Open Scope list_scope. -(* - - -Require Import Crypto.Util.ListUtil Coq.Lists.List. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Util.Notations. -Import ListNotations. Local Open Scope Z_scope. -*) Module Compilers. Import Language.Compilers. Import LanguageInversion.Compilers. @@ -122,6 +114,9 @@ Module Compilers. End with_ident. End DeadCodeElimination. + Hint Resolve DeadCodeElimination.Wf_EliminateDead : wf. + Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp. + Module Subst01. Import MiscCompilerPasses.Compilers.Subst01. @@ -201,4 +196,7 @@ Module Compilers. End interp. End with_ident. End Subst01. + + Hint Resolve Subst01.Wf_Subst01 : wf. + Hint Rewrite @Subst01.Interp_Subst01 : interp. End Compilers. diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v new file mode 100644 index 000000000..a1e31b319 --- /dev/null +++ b/src/Experiments/NewPipeline/RewriterProofs.v @@ -0,0 +1,59 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.Classes.Morphisms. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.FSets.FMapPositive. +Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Experiments.NewPipeline.LanguageInversion. +Require Import Crypto.Experiments.NewPipeline.LanguageWf. +Require Import Crypto.Experiments.NewPipeline.Rewriter. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SplitInContext. +Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.Tactics.RewriteHyp. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.ListUtil. +Import ListNotations. Local Open Scope list_scope. +Local Open Scope Z_scope. + +Module Compilers. + Import Language.Compilers. + Import LanguageInversion.Compilers. + Import LanguageWf.Compilers. + Import Rewriter.Compilers. + Import expr.Notations. + Import defaults. + + Module Import RewriteRules. + Import Rewriter.Compilers.RewriteRules. + + Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e). + Admitted. + Lemma Wf_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Wf (@RewriteArith max_const_val t e). + Admitted. + Lemma Wf_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z) {t} e (Hwf : Wf e) : Wf (@RewriteToFancy invert_low invert_high t e). + Admitted. + + Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e. + Admitted. + Lemma Interp_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Interp (@RewriteArith max_const_val t e) == Interp e. + Admitted. + + Lemma Interp_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z) + (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) + {t} e (Hwf : Wf e) + : Interp (@RewriteToFancy invert_low invert_high t e) == Interp e. + Admitted. + End RewriteRules. + + Lemma Wf_PartialEvaluate {t} e (Hwf : Wf e) : Wf (@PartialEvaluate t e). + Proof. apply Wf_RewriteNBE, Hwf. Qed. + + Lemma Interp_PartialEvaluate {t} e (Hwf : Wf e) : Interp (@PartialEvaluate t e) == Interp e. + Proof. apply Interp_RewriteNBE, Hwf. Qed. + + + Hint Resolve Wf_PartialEvaluate Wf_RewriteArith Wf_RewriteNBE Wf_RewriteToFancy : wf. + Hint Rewrite @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy : interp. +End Compilers. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 9464e270a..bec153f53 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -45,10 +45,14 @@ Require Import Crypto.Experiments.NewPipeline.Arithmetic. Require Crypto.Experiments.NewPipeline.Language. Require Crypto.Experiments.NewPipeline.UnderLets. Require Crypto.Experiments.NewPipeline.AbstractInterpretation. -Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs. Require Crypto.Experiments.NewPipeline.Rewriter. Require Crypto.Experiments.NewPipeline.MiscCompilerPasses. Require Crypto.Experiments.NewPipeline.CStringification. +Require Crypto.Experiments.NewPipeline.LanguageWf. +Require Crypto.Experiments.NewPipeline.UnderLetsProofs. +Require Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs. +Require Crypto.Experiments.NewPipeline.RewriterProofs. +Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope Z_scope. @@ -274,6 +278,10 @@ Module MontgomeryStyleRing. := (andb (is_bounded_by bounds (@fst _ unit ls)) true). Local Notation is_bounded_by2 bounds ls := (andb (is_bounded_by bounds (fst ls)) (is_bounded_by1 bounds (snd ls))). + Local Notation is_eq1 arg1 arg2 + := (and ((@fst _ unit arg1) = (@fst _ unit arg2)) True). + Local Notation is_eq2 arg1 arg2 + := (and (fst arg1 = fst arg2) (is_eq1 (snd arg1) (snd arg2))). Lemma length_is_bounded_by bounds ls : is_bounded_by bounds ls = true -> length ls = length bounds. @@ -301,50 +309,55 @@ Module MontgomeryStyleRing. (Hfrom_montgomery_mod : forall v, valid v -> valid (from_montgomery_mod v)) (Interp_rfrom_montgomeryv : list Z -> list Z) - (HInterp_rfrom_montgomeryv : forall arg, - is_bounded_by1 bounds arg = true - -> is_bounded_by bounds (Interp_rfrom_montgomeryv (fst arg)) = true - /\ Interp_rfrom_montgomeryv (fst arg) = from_montgomery_mod (fst arg)) + (HInterp_rfrom_montgomeryv : forall arg1 arg2, + is_eq1 arg1 arg2 + -> is_bounded_by1 bounds arg1 = true + -> is_bounded_by bounds (Interp_rfrom_montgomeryv (fst arg1)) = true + /\ Interp_rfrom_montgomeryv (fst arg1) = from_montgomery_mod (fst arg2)) (mulmod : list Z -> list Z -> list Z) (Hmulmod : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (mulmod a b)) mod (s - Associational.eval c) - = (eval (from_montgomery_mod a) * eval (from_montgomery_mod b)) mod (s - Associational.eval c)) + = (eval (from_montgomery_mod a) * eval (from_montgomery_mod b)) mod (s - Associational.eval c)) /\ (forall a (_ : valid a) b (_ : valid b), valid (mulmod a b))) (Interp_rmulv : list Z -> list Z -> list Z) - (HInterp_rmulv : forall arg, - is_bounded_by2 bounds arg = true - -> is_bounded_by bounds (Interp_rmulv (fst arg) (fst (snd arg))) = true - /\ Interp_rmulv (fst arg) (fst (snd arg)) = mulmod (fst arg) (fst (snd arg))) + (HInterp_rmulv : forall arg1 arg2, + is_eq2 arg1 arg2 + -> is_bounded_by2 bounds arg1 = true + -> is_bounded_by bounds (Interp_rmulv (fst arg1) (fst (snd arg1))) = true + /\ Interp_rmulv (fst arg1) (fst (snd arg1)) = mulmod (fst arg2) (fst (snd arg2))) (addmod : list Z -> list Z -> list Z) (Haddmod : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (addmod a b)) mod (s - Associational.eval c) - = (eval (from_montgomery_mod a) + eval (from_montgomery_mod b)) mod (s - Associational.eval c)) + = (eval (from_montgomery_mod a) + eval (from_montgomery_mod b)) mod (s - Associational.eval c)) /\ (forall a (_ : valid a) b (_ : valid b), valid (addmod a b))) (Interp_raddv : list Z -> list Z -> list Z) - (HInterp_raddv : forall arg, - is_bounded_by2 bounds arg = true - -> is_bounded_by bounds (Interp_raddv (fst arg) (fst (snd arg))) = true - /\ Interp_raddv (fst arg) (fst (snd arg)) = addmod (fst arg) (fst (snd arg))) + (HInterp_raddv : forall arg1 arg2, + is_eq2 arg1 arg2 + -> is_bounded_by2 bounds arg1 = true + -> is_bounded_by bounds (Interp_raddv (fst arg1) (fst (snd arg1))) = true + /\ Interp_raddv (fst arg1) (fst (snd arg1)) = addmod (fst arg2) (fst (snd arg2))) (submod : list Z -> list Z -> list Z) (Hsubmod : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (submod a b)) mod (s - Associational.eval c) - = (eval (from_montgomery_mod a) - eval (from_montgomery_mod b)) mod (s - Associational.eval c)) + = (eval (from_montgomery_mod a) - eval (from_montgomery_mod b)) mod (s - Associational.eval c)) /\ (forall a (_ : valid a) b (_ : valid b), valid (submod a b))) (Interp_rsubv : list Z -> list Z -> list Z) - (HInterp_rsubv : forall arg, - is_bounded_by2 bounds arg = true - -> is_bounded_by bounds (Interp_rsubv (fst arg) (fst (snd arg))) = true - /\ Interp_rsubv (fst arg) (fst (snd arg)) = submod (fst arg) (fst (snd arg))) + (HInterp_rsubv : forall arg1 arg2, + is_eq2 arg1 arg2 + -> is_bounded_by2 bounds arg1 = true + -> is_bounded_by bounds (Interp_rsubv (fst arg1) (fst (snd arg1))) = true + /\ Interp_rsubv (fst arg1) (fst (snd arg1)) = submod (fst arg2) (fst (snd arg2))) (oppmod : list Z -> list Z) (Hoppmod : (forall a (_ : valid a), eval (from_montgomery_mod (oppmod a)) mod (s - Associational.eval c) - = (-eval (from_montgomery_mod a)) mod (s - Associational.eval c)) + = (-eval (from_montgomery_mod a)) mod (s - Associational.eval c)) /\ (forall a (_ : valid a), valid (oppmod a))) (Interp_roppv : list Z -> list Z) - (HInterp_roppv : forall arg, - is_bounded_by1 bounds arg = true - -> is_bounded_by bounds (Interp_roppv (fst arg)) = true - /\ Interp_roppv (fst arg) = oppmod (fst arg)) + (HInterp_roppv : forall arg1 arg2, + is_eq1 arg1 arg2 + -> is_bounded_by1 bounds arg1 = true + -> is_bounded_by bounds (Interp_roppv (fst arg1)) = true + /\ Interp_roppv (fst arg1) = oppmod (fst arg2)) (zeromod : list Z) (Hzeromod : (eval (from_montgomery_mod zeromod)) mod (s - Associational.eval c) @@ -356,40 +369,37 @@ Module MontgomeryStyleRing. (onemod : list Z) (Honemod : (eval (from_montgomery_mod onemod)) mod (s - Associational.eval c) - = 1 mod (s - Associational.eval c) + = 1 mod (s - Associational.eval c) /\ valid onemod) (Interp_ronev : list Z) (HInterp_ronev : is_bounded_by bounds Interp_ronev = true - /\ Interp_ronev = onemod) + /\ Interp_ronev = onemod) (encodemod : Z -> list Z) (Hencodemod : (forall v, 0 <= v < s - Associational.eval c -> eval (from_montgomery_mod (encodemod v)) mod (s - Associational.eval c) = v mod (s - Associational.eval c)) /\ (forall v, 0 <= v < s - Associational.eval c -> valid (encodemod v))) (Interp_rencodev : Z -> list Z) - (HInterp_rencodev : forall arg, - is_bounded_by0 prime_bound (@fst _ unit arg) && true = true - -> is_bounded_by bounds (Interp_rencodev (fst arg)) = true - /\ Interp_rencodev (fst arg) = encodemod (fst arg)). + (HInterp_rencodev : forall arg1 arg2, + is_eq1 arg1 arg2 + -> is_bounded_by0 prime_bound (@fst _ unit arg1) && true = true + -> is_bounded_by bounds (Interp_rencodev (fst arg1)) = true + /\ Interp_rencodev (fst arg1) = encodemod (fst arg2)). Local Notation T := (list Z) (only parsing). Local Notation encoded_ok ls := (is_bounded_by bounds ls = true /\ valid ls) (only parsing). Local Notation encoded_okf := (fun ls => encoded_ok ls) (only parsing). - Definition Fdecode (v : T) : F m := F.of_Z m (Positional.eval weight n (Interp_rfrom_montgomeryv v)). Definition T_eq (x y : T) := Fdecode x = Fdecode y. - Definition encodedT := sig encoded_okf. - Definition ring_mul (x y : T) : T := Interp_rmulv x y. Definition ring_add (x y : T) : T := Interp_raddv x y. Definition ring_sub (x y : T) : T := Interp_rsubv x y. Definition ring_opp (x : T) : T := Interp_roppv x. Definition ring_encode (x : F m) : T := Interp_rencodev (F.to_Z x). - Definition GoodT : Prop := @subsetoid_ring (list Z) encoded_okf T_eq @@ -401,12 +411,10 @@ Module MontgomeryStyleRing. (list Z) encoded_okf T_eq Interp_ronev ring_add ring_mul (F m) (fun _ => True) eq 1%F F.add F.mul Fdecode. - Hint Rewrite ->@F.to_Z_add : push_FtoZ. Hint Rewrite ->@F.to_Z_mul : push_FtoZ. Hint Rewrite ->@F.to_Z_opp : push_FtoZ. Hint Rewrite ->@F.to_Z_of_Z : push_FtoZ. - Lemma Fm_bounded_alt (x : F m) : (0 <=? F.to_Z x) && (F.to_Z x <=? Z.pos m - 1) = true. Proof using m_eq. @@ -415,7 +423,6 @@ Module MontgomeryStyleRing. pose proof (Z.mod_pos_bound x (Z.pos m)). rewrite andb_true_iff; split; Z.ltb_to_lt; lia. Qed. - Lemma Fm_bounded_alt' (x : F m) : 0 <= F.to_Z x < Z.pos m. Proof using m_eq. @@ -424,7 +431,6 @@ Module MontgomeryStyleRing. pose proof (Z.mod_pos_bound x (Z.pos m)). split; Z.ltb_to_lt; lia. Qed. - Lemma Good : GoodT. Proof. split_and. @@ -434,8 +440,8 @@ Module MontgomeryStyleRing. eapply subsetoid_ring_by_ring_isomorphism; cbv [ring_opp ring_add ring_sub ring_mul ring_encode F.sub] in *; repeat match goal with - | [ H : forall arg : _ * unit, _ |- _ ] => specialize (fun arg => H (arg, tt)) - | [ H : forall arg : _ * (_ * unit), _ |- _ ] => specialize (fun a b => H (a, (b, tt))) + | [ H : forall arg1 arg2 : _ * unit, _ |- _ ] => specialize (fun arg => H (arg, tt) (arg, tt) ltac:(tauto)) + | [ H : forall arg arg2 : _ * (_ * unit), _ |- _ ] => specialize (fun a b => H (a, (b, tt)) (a, (b, tt)) ltac:(tauto)) | _ => progress cbn [fst snd] in * | _ => solve [ auto using andb_true_intro, conj with nocore ] | _ => progress intros @@ -489,19 +495,27 @@ End MontgomeryStyleRing. Import Associational Positional. Import + Crypto.Experiments.NewPipeline.LanguageWf + Crypto.Experiments.NewPipeline.UnderLetsProofs + Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs + Crypto.Experiments.NewPipeline.RewriterProofs + Crypto.Experiments.NewPipeline.AbstractInterpretationProofs Crypto.Experiments.NewPipeline.Language Crypto.Experiments.NewPipeline.UnderLets Crypto.Experiments.NewPipeline.AbstractInterpretation - Crypto.Experiments.NewPipeline.AbstractInterpretationProofs Crypto.Experiments.NewPipeline.Rewriter Crypto.Experiments.NewPipeline.MiscCompilerPasses Crypto.Experiments.NewPipeline.CStringification. Import + LanguageWf.Compilers + UnderLetsProofs.Compilers + MiscCompilerPassesProofs.Compilers + RewriterProofs.Compilers + AbstractInterpretationProofs.Compilers Language.Compilers UnderLets.Compilers AbstractInterpretation.Compilers - AbstractInterpretationProofs.Compilers Rewriter.Compilers MiscCompilerPasses.Compilers CStringification.Compilers. @@ -511,10 +525,6 @@ Local Coercion Z.of_nat : nat >-> Z. Local Coercion QArith_base.inject_Z : Z >-> Q. Notation "x" := (expr.Var x) (only printing, at level 9) : expr_scope. -Axiom admit_pf : False. -Notation admit := (match admit_pf with end). - - Module Pipeline. Import GeneralizeVar. Inductive ErrorMessage := @@ -749,6 +759,14 @@ Module Pipeline. | Error err => Error err end. + Local Ltac wf_interp_t := + repeat first [ progress destruct_head'_and + | progress autorewrite with interp + | solve [ auto with interp wf ] + | solve [ typeclasses eauto ] + | break_innermost_match_step + | solve [ auto 100 with wf ] ]. + Lemma BoundsPipeline_correct (with_dead_code_elimination : bool := true) (with_subst01 : bool) @@ -762,11 +780,19 @@ Module Pipeline. out_bounds rv (Hrv : BoundsPipeline (*with_dead_code_elimination*) with_subst01 translate_to_fancy relax_zrange e arg_bounds out_bounds = Success rv) - : forall arg - (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg = true), - ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg) = true - /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg - = type.app_curried (Interp e) arg. + (Hwf : Wf e) + (Hfancy : match translate_to_fancy with + | Some {| invert_low := il ; invert_high := ih |} + => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) + | None => True + end) + : forall arg1 arg2 + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2) + (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true), + ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg1) = true + /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1 + = type.app_curried (Interp e) arg2. Proof. cbv [BoundsPipeline Let_In] in *; repeat match goal with @@ -778,15 +804,25 @@ Module Pipeline. { intros; match goal with | [ H : _ = _ |- _ ] - => eapply CheckedPartialEvaluateWithBounds_Correct in H; - [ destruct H as [H0 H1] | .. ] + => let H' := fresh in + pose proof H as H'; + eapply CheckedPartialEvaluateWithBounds_Correct in H'; + [ destruct H' as [H0 H1] | .. ] end; [ - | eassumption || (try reflexivity).. ]. - subst. - split; [ assumption | ]. - { intros; rewrite H1. - exact admit. (* interp correctness *) } } + | match goal with + | [ |- Wf _ ] => idtac + | _ => eassumption || reflexivity + end.. ]. + { subst. + split; [ solve [ eauto with nocore ] | ]. + { intros; rewrite H1; clear H1. + transitivity (type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds e arg_bounds)) arg1). + { apply type.app_curried_Proper; [ | symmetry; assumption ]. + clear dependent arg1; clear dependent arg2; clear dependent out_bounds. + wf_interp_t. } + { apply Interp_PartialEvaluateWithListInfoFromBounds; auto. } } } + { wf_interp_t. } } Qed. Definition BoundsPipeline_correct_transT @@ -795,16 +831,23 @@ Module Pipeline. out_bounds (InterpE : type.interp base.interp t) (rv : Expr t) - := forall arg - (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg = true), - ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg) = true - /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg - = type.app_curried InterpE arg. + := forall arg1 arg2 + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2) + (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true), + ZRange.type.base.option.is_bounded_by out_bounds (type.app_curried (Interp rv) arg1) = true + /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1 + = type.app_curried InterpE arg2. Lemma BoundsPipeline_correct_trans (with_dead_code_elimination : bool := true) (with_subst01 : bool) (translate_to_fancy : option to_fancy_args) + (Hfancy : match translate_to_fancy with + | Some {| invert_low := il ; invert_high := ih |} + => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) + | None => True + end) relax_zrange (Hrelax : forall r r' z : zrange, @@ -813,16 +856,23 @@ Module Pipeline. (e : Expr t) arg_bounds out_bounds (InterpE : type.interp base.interp t) - (InterpE_correct - : forall arg - (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg = true), - type.app_curried (Interp e) arg = type.app_curried InterpE arg) + (InterpE_correct_and_Wf + : (forall arg1 arg2 + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2) + (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds arg1 = true), + type.app_curried (Interp e) arg1 = type.app_curried InterpE arg2) + /\ Wf e) rv (Hrv : BoundsPipeline (*with_dead_code_elimination*) with_subst01 translate_to_fancy relax_zrange e arg_bounds out_bounds = Success rv) : BoundsPipeline_correct_transT arg_bounds out_bounds InterpE rv. Proof. - intros arg Harg; rewrite <- InterpE_correct by assumption. - eapply @BoundsPipeline_correct; eassumption. + destruct InterpE_correct_and_Wf as [InterpE_correct Hwf]. + intros arg1 arg2 Harg12 Harg1; erewrite <- InterpE_correct; [ eapply @BoundsPipeline_correct | .. ]; + lazymatch goal with + | [ |- type.andb_bool_for_each_lhs_of_arrow _ _ _ = true ] => eassumption + | _ => try assumption + end; try eassumption. + etransitivity; try eassumption; symmetry; assumption. Qed. End Pipeline. @@ -873,239 +923,289 @@ Proof. Qed. Ltac cache_reify _ := - intros; - etransitivity; - [ - | repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end; - Reify_rhs (); - reflexivity ]; - subst_evars; - reflexivity. - -Create HintDb reify_gen_cache. + split; + [ intros; + etransitivity; + [ + | repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end; + Reify_rhs (); + reflexivity ]; + subst_evars; + reflexivity + | prove_Wf () ]. + +Create HintDb reify_gen_cache discriminated. +Create HintDb wf_gen_cache discriminated. +Hint Resolve conj : reify_gen_cache wf_gen_cache. +Hint Unfold Wf : wf_gen_cache. Derive carry_mul_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (f g : list Z) - (n : nat) - (s : Z) - (c : list (Z * Z)) - (idxs : list nat), - Interp (t:=reify_type_of carry_mulmod) - carry_mul_gen limbwidth_num limbwidth_den s c n idxs f g - = carry_mulmod limbwidth_num limbwidth_den s c n idxs f g) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (f g : list Z) + (n : nat) + (s : Z) + (c : list (Z * Z)) + (idxs : list nat), + Interp (t:=reify_type_of carry_mulmod) + carry_mul_gen limbwidth_num limbwidth_den s c n idxs f g + = carry_mulmod limbwidth_num limbwidth_den s c n idxs f g) + /\ Wf carry_mul_gen) As carry_mul_gen_correct. Proof. Time cache_reify (). Time Qed. -Hint Extern 1 (_ = carry_mulmod _ _ _ _ _ _ _ _) => simple apply carry_mul_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = carry_mulmod _ _ _ _ _ _ _ _) => simple apply (proj1 carry_mul_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 carry_mul_gen_correct) : wf_gen_cache. Derive carry_square_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (f : list Z) - (n : nat) - (s : Z) - (c : list (Z * Z)) - (idxs : list nat), - Interp (t:=reify_type_of carry_squaremod) - carry_square_gen limbwidth_num limbwidth_den s c n idxs f - = carry_squaremod limbwidth_num limbwidth_den s c n idxs f) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (f : list Z) + (n : nat) + (s : Z) + (c : list (Z * Z)) + (idxs : list nat), + Interp (t:=reify_type_of carry_squaremod) + carry_square_gen limbwidth_num limbwidth_den s c n idxs f + = carry_squaremod limbwidth_num limbwidth_den s c n idxs f) + /\ Wf carry_square_gen) As carry_square_gen_correct. Proof. Time cache_reify (). Time Qed. -Hint Extern 1 (_ = carry_squaremod _ _ _ _ _ _ _) => simple apply carry_square_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = carry_squaremod _ _ _ _ _ _ _) => simple apply (proj1 carry_square_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 carry_square_gen_correct) : wf_gen_cache. Derive carry_scmul_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (x : Z) (f : list Z) - (n : nat) - (s : Z) - (c : list (Z * Z)) - (idxs : list nat), - Interp (t:=reify_type_of carry_scmulmod) - carry_scmul_gen limbwidth_num limbwidth_den s c n idxs x f - = carry_scmulmod limbwidth_num limbwidth_den s c n idxs x f) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (x : Z) (f : list Z) + (n : nat) + (s : Z) + (c : list (Z * Z)) + (idxs : list nat), + Interp (t:=reify_type_of carry_scmulmod) + carry_scmul_gen limbwidth_num limbwidth_den s c n idxs x f + = carry_scmulmod limbwidth_num limbwidth_den s c n idxs x f) + /\ Wf carry_scmul_gen) As carry_scmul_gen_correct. Proof. Time cache_reify (). Time Qed. -Hint Extern 1 (_ = carry_scmulmod _ _ _ _ _ _ _ _) => simple apply carry_scmul_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = carry_scmulmod _ _ _ _ _ _ _ _) => simple apply (proj1 carry_scmul_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 carry_scmul_gen_correct) : wf_gen_cache. Derive carry_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (f : list Z) - (n : nat) - (s : Z) - (c : list (Z * Z)) - (idxs : list nat), - Interp (t:=reify_type_of carrymod) - carry_gen limbwidth_num limbwidth_den s c n idxs f - = carrymod limbwidth_num limbwidth_den s c n idxs f) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (f : list Z) + (n : nat) + (s : Z) + (c : list (Z * Z)) + (idxs : list nat), + Interp (t:=reify_type_of carrymod) + carry_gen limbwidth_num limbwidth_den s c n idxs f + = carrymod limbwidth_num limbwidth_den s c n idxs f) + /\ Wf carry_gen) As carry_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = carrymod _ _ _ _ _ _ _) => simple apply carry_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = carrymod _ _ _ _ _ _ _) => simple apply (proj1 carry_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 carry_gen_correct) : wf_gen_cache. Derive encode_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (v : Z) - (n : nat) - (s : Z) - (c : list (Z * Z)), - Interp (t:=reify_type_of encodemod) - encode_gen limbwidth_num limbwidth_den s c n v - = encodemod limbwidth_num limbwidth_den s c n v) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (v : Z) + (n : nat) + (s : Z) + (c : list (Z * Z)), + Interp (t:=reify_type_of encodemod) + encode_gen limbwidth_num limbwidth_den s c n v + = encodemod limbwidth_num limbwidth_den s c n v) + /\ Wf encode_gen) As encode_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = encodemod _ _ _ _ _ _) => simple apply encode_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = encodemod _ _ _ _ _ _) => simple apply (proj1 encode_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 encode_gen_correct) : wf_gen_cache. Derive add_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (f g : list Z) - (n : nat), - Interp (t:=reify_type_of addmod) - add_gen limbwidth_num limbwidth_den n f g - = addmod limbwidth_num limbwidth_den n f g) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (f g : list Z) + (n : nat), + Interp (t:=reify_type_of addmod) + add_gen limbwidth_num limbwidth_den n f g + = addmod limbwidth_num limbwidth_den n f g) + /\ Wf add_gen) As add_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = addmod _ _ _ _ _) => simple apply add_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = addmod _ _ _ _ _) => simple apply (proj1 add_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 add_gen_correct) : wf_gen_cache. Derive sub_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (n : nat) - (s : Z) - (c : list (Z * Z)) - (coef : Z) - (f g : list Z), - Interp (t:=reify_type_of submod) - sub_gen limbwidth_num limbwidth_den s c n coef f g - = submod limbwidth_num limbwidth_den s c n coef f g) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (n : nat) + (s : Z) + (c : list (Z * Z)) + (coef : Z) + (f g : list Z), + Interp (t:=reify_type_of submod) + sub_gen limbwidth_num limbwidth_den s c n coef f g + = submod limbwidth_num limbwidth_den s c n coef f g) + /\ Wf sub_gen) As sub_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = submod _ _ _ _ _ _ _ _) => simple apply sub_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = submod _ _ _ _ _ _ _ _) => simple apply (proj1 sub_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 sub_gen_correct) : wf_gen_cache. + Derive opp_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (n : nat) - (s : Z) - (c : list (Z * Z)) - (coef : Z) - (f : list Z), - Interp (t:=reify_type_of oppmod) - opp_gen limbwidth_num limbwidth_den s c n coef f - = oppmod limbwidth_num limbwidth_den s c n coef f) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (n : nat) + (s : Z) + (c : list (Z * Z)) + (coef : Z) + (f : list Z), + Interp (t:=reify_type_of oppmod) + opp_gen limbwidth_num limbwidth_den s c n coef f + = oppmod limbwidth_num limbwidth_den s c n coef f) + /\ Wf opp_gen) As opp_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = oppmod _ _ _ _ _ _ _) => simple apply opp_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = oppmod _ _ _ _ _ _ _) => simple apply (proj1 opp_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 opp_gen_correct) : wf_gen_cache. + Definition zeromod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 0. Definition onemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 1. Definition primemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n (s - Associational.eval c). + Derive zero_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (n : nat) - (s : Z) - (c : list (Z * Z)), - Interp (t:=reify_type_of zeromod) - zero_gen limbwidth_num limbwidth_den s c n - = zeromod limbwidth_num limbwidth_den s c n) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (n : nat) + (s : Z) + (c : list (Z * Z)), + Interp (t:=reify_type_of zeromod) + zero_gen limbwidth_num limbwidth_den s c n + = zeromod limbwidth_num limbwidth_den s c n) + /\ Wf zero_gen) As zero_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = zeromod _ _ _ _ _) => simple apply zero_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = zeromod _ _ _ _ _) => simple apply (proj1 zero_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 zero_gen_correct) : wf_gen_cache. Derive one_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (n : nat) - (s : Z) - (c : list (Z * Z)), - Interp (t:=reify_type_of onemod) - one_gen limbwidth_num limbwidth_den s c n - = onemod limbwidth_num limbwidth_den s c n) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (n : nat) + (s : Z) + (c : list (Z * Z)), + Interp (t:=reify_type_of onemod) + one_gen limbwidth_num limbwidth_den s c n + = onemod limbwidth_num limbwidth_den s c n) + /\ Wf one_gen) As one_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = onemod _ _ _ _ _) => simple apply one_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = onemod _ _ _ _ _) => simple apply (proj1 one_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 one_gen_correct) : wf_gen_cache. Derive prime_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (n : nat) - (s : Z) - (c : list (Z * Z)), - Interp (t:=reify_type_of primemod) - prime_gen limbwidth_num limbwidth_den s c n - = primemod limbwidth_num limbwidth_den s c n) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (n : nat) + (s : Z) + (c : list (Z * Z)), + Interp (t:=reify_type_of primemod) + prime_gen limbwidth_num limbwidth_den s c n + = primemod limbwidth_num limbwidth_den s c n) + /\ Wf prime_gen) As prime_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = primemod _ _ _ _ _) => simple apply prime_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = primemod _ _ _ _ _) => simple apply (proj1 prime_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 prime_gen_correct) : wf_gen_cache. Derive id_gen - SuchThat (forall (ls : list Z), - Interp (t:=reify_type_of (@id (list Z))) - id_gen ls - = id ls) + SuchThat ((forall (ls : list Z), + Interp (t:=reify_type_of (@id (list Z))) + id_gen ls + = id ls) + /\ Wf id_gen) As id_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = id _) => simple apply id_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = id _) => simple apply (proj1 id_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 id_gen_correct) : wf_gen_cache. Derive selectznz_gen - SuchThat (forall (cond : Z) (f g : list Z), - Interp (t:=reify_type_of Positional.select) - selectznz_gen cond f g - = Positional.select cond f g) + SuchThat ((forall (cond : Z) (f g : list Z), + Interp (t:=reify_type_of Positional.select) + selectznz_gen cond f g + = Positional.select cond f g) + /\ Wf selectznz_gen) As selectznz_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = Positional.select _ _ _) => simple apply selectznz_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = Positional.select _ _ _) => simple apply (proj1 selectznz_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 selectznz_gen_correct) : wf_gen_cache. Derive to_bytes_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (n : nat) - (bitwidth : Z) - (m_enc : list Z) - (f : list Z), - Interp (t:=reify_type_of freeze_to_bytesmod) - to_bytes_gen limbwidth_num limbwidth_den n bitwidth m_enc f - = freeze_to_bytesmod limbwidth_num limbwidth_den n bitwidth m_enc f) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (n : nat) + (bitwidth : Z) + (m_enc : list Z) + (f : list Z), + Interp (t:=reify_type_of freeze_to_bytesmod) + to_bytes_gen limbwidth_num limbwidth_den n bitwidth m_enc f + = freeze_to_bytesmod limbwidth_num limbwidth_den n bitwidth m_enc f) + /\ Wf to_bytes_gen) As to_bytes_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = freeze_to_bytesmod _ _ _ _ _ _) => simple apply to_bytes_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = freeze_to_bytesmod _ _ _ _ _ _) => simple apply (proj1 to_bytes_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 to_bytes_gen_correct) : wf_gen_cache. Derive from_bytes_gen - SuchThat (forall (limbwidth_num limbwidth_den : Z) - (n : nat) - (f : list Z), - Interp (t:=reify_type_of from_bytesmod) - from_bytes_gen limbwidth_num limbwidth_den n f - = from_bytesmod limbwidth_num limbwidth_den n f) + SuchThat ((forall (limbwidth_num limbwidth_den : Z) + (n : nat) + (f : list Z), + Interp (t:=reify_type_of from_bytesmod) + from_bytes_gen limbwidth_num limbwidth_den n f + = from_bytesmod limbwidth_num limbwidth_den n f) + /\ Wf from_bytes_gen) As from_bytes_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = from_bytesmod _ _ _ _) => simple apply from_bytes_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = from_bytesmod _ _ _ _) => simple apply (proj1 from_bytes_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 from_bytes_gen_correct) : wf_gen_cache. Derive mulx_gen - SuchThat (forall (s x y : Z), - Interp (t:=reify_type_of mulx) - mulx_gen s x y - = mulx s x y) + SuchThat ((forall (s x y : Z), + Interp (t:=reify_type_of mulx) + mulx_gen s x y + = mulx s x y) + /\ Wf mulx_gen) As mulx_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = mulx _ _ _) => simple apply mulx_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = mulx _ _ _) => simple apply (proj1 mulx_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 mulx_gen_correct) : wf_gen_cache. Derive addcarryx_gen - SuchThat (forall (s c x y : Z), - Interp (t:=reify_type_of addcarryx) - addcarryx_gen s c x y - = addcarryx s c x y) + SuchThat ((forall (s c x y : Z), + Interp (t:=reify_type_of addcarryx) + addcarryx_gen s c x y + = addcarryx s c x y) + /\ Wf addcarryx_gen) As addcarryx_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = addcarryx _ _ _ _) => simple apply addcarryx_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = addcarryx _ _ _ _) => simple apply (proj1 addcarryx_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 addcarryx_gen_correct) : wf_gen_cache. Derive subborrowx_gen - SuchThat (forall (s c x y : Z), - Interp (t:=reify_type_of subborrowx) - subborrowx_gen s c x y - = subborrowx s c x y) + SuchThat ((forall (s c x y : Z), + Interp (t:=reify_type_of subborrowx) + subborrowx_gen s c x y + = subborrowx s c x y) + /\ Wf subborrowx_gen) As subborrowx_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = subborrowx _ _ _ _) => simple apply subborrowx_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = subborrowx _ _ _ _) => simple apply (proj1 subborrowx_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 subborrowx_gen_correct) : wf_gen_cache. Derive cmovznz_gen - SuchThat (forall (bitwidth cond z nz : Z), - Interp (t:=reify_type_of cmovznz) - cmovznz_gen bitwidth cond z nz - = cmovznz bitwidth cond z nz) + SuchThat ((forall (bitwidth cond z nz : Z), + Interp (t:=reify_type_of cmovznz) + cmovznz_gen bitwidth cond z nz + = cmovznz bitwidth cond z nz) + /\ Wf cmovznz_gen) As cmovznz_gen_correct. Proof. cache_reify (). Qed. -Hint Extern 1 (_ = cmovznz _ _ _ _) => simple apply cmovznz_gen_correct : reify_gen_cache. +Hint Extern 1 (_ = cmovznz _ _ _ _) => simple apply (proj1 cmovznz_gen_correct) : reify_gen_cache. +Hint Immediate (proj2 cmovznz_gen_correct) : wf_gen_cache. + + +Axiom admit_pf : False. +Notation admit := (match admit_pf with end). (** XXX TODO: Translate Jade's python script *) @@ -1190,7 +1290,7 @@ Module Import UnsaturatedSolinas. Notation BoundsPipeline_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - (*false*) true None + (*false*) true None I relax_zrange (relax_zrange_gen_good _) _ @@ -1212,7 +1312,7 @@ Module Import UnsaturatedSolinas. Notation BoundsPipeline_no_subst01_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - (*false*) false None + (*false*) false None I relax_zrange (relax_zrange_gen_good _) _ @@ -1234,7 +1334,7 @@ Module Import UnsaturatedSolinas. Notation BoundsPipeline_with_bytes_no_subst01_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - (*false*) false None + (*false*) false None I relax_zrange_with_bytes (relax_zrange_gen_good _) _ @@ -1660,10 +1760,10 @@ Module Import UnsaturatedSolinas. lazymatch goal with | [ H : ?P ?rop |- context[expr.Interp _ ?rop] ] => intros; - let H1 := fresh in - let H2 := fresh in - unshelve edestruct H as [H1 H2]; [ .. | solve [ split; [ eapply H1 | eapply H2 ] ] ]; - solve [ exact tt | eassumption | reflexivity ] + let H1 := fresh "HH1" in + let H2 := fresh "HH2" in + unshelve edestruct H as [H1 H2]; [ .. | solve [ split; [ eapply H1 | refine (H2 _) ] ] ]; + solve [ exact tt | eassumption | reflexivity | repeat split ] | _ => idtac end; repeat first [ assumption @@ -1675,7 +1775,7 @@ Module Import UnsaturatedSolinas. | intros; apply eval_encodemod | apply conj ]. } { cbv zeta; intros f Hf; split. - { apply Hto_bytesv; assumption. } + { apply Hto_bytesv; solve [ assumption | repeat split ]. } { cbn [type.for_each_lhs_of_arrow type_base type.andb_bool_for_each_lhs_of_arrow ZRange.type.option.is_bounded_by fst snd] in *. rewrite Bool.andb_true_iff in *; split_and'. etransitivity; [ apply eval_freeze_to_bytesmod | f_equal; (eassumption || (symmetry; eassumption)) ]; @@ -1693,7 +1793,7 @@ Module Import UnsaturatedSolinas. split. { etransitivity; [ erewrite <- eval_zeros; [ | apply weight_0, wprops ] | apply H15 ]. apply Z.eq_le_incl; f_equal. - admit. + repeat match goal with H : _ |- _ => revert H end; exact admit. omega. } { eapply Z.le_lt_trans; [ apply H15 | ]. assert (Hlen : length (encode (weight (Qnum limbwidth) (QDen limbwidth)) n s c (s - 1)) = n) by distr_length. @@ -1704,11 +1804,11 @@ Module Import UnsaturatedSolinas. revert ls. clearbody limbwidth. induction n as [|n' IHn'], ls as [|l ls]; cbn [length]; intros; try omega. - admit. + repeat match goal with H : _ |- _ => revert H end; exact admit. cbn [map]. - admit. } - admit. } - Admitted. + repeat match goal with H : _ |- _ => revert H end; exact admit. } + repeat match goal with H : _ |- _ => revert H end; exact admit. } } } + Qed. End make_ring. Section for_stringification. @@ -1817,23 +1917,50 @@ Ltac peel_interp_app _ := end ] ] end. Ltac pre_cache_reify _ := - cbv [type.app_curried]; - let arg := fresh "arg" in - intros arg _; - peel_interp_app (); - [ lazymatch goal with - | [ |- ?R (Interp ?ev) _ ] - => (tryif is_evar ev - then let ev' := fresh "ev" in set (ev' := ev) - else idtac) - end; - cbv [pointwise_relation]; intros; clear - | .. ]. + let H' := fresh in + lazymatch goal with + | [ |- ?P /\ Wf ?e ] + => let P' := fresh in + evar (P' : Prop); + assert (H' : P' /\ Wf e); subst P' + end; + [ + | split; [ destruct H' as [H' _] | destruct H' as [_ H']; exact H' ]; + cbv [type.app_curried]; + let arg := fresh "arg" in + let arg2 := fresh in + intros arg arg2; + cbn [type.and_for_each_lhs_of_arrow type.eqv]; + let H := fresh in + intro H; + repeat match type of H with + | and _ _ => let H' := fresh in + destruct H as [H' H]; + rewrite <- H' + end; + clear dependent arg2; clear H; + intros _; + peel_interp_app (); + [ lazymatch goal with + | [ |- ?R (Interp ?ev) _ ] + => (tryif is_evar ev + then let ev' := fresh "ev" in set (ev' := ev) + else idtac) + end; + cbv [pointwise_relation]; + repeat lazymatch goal with + | [ H : _ |- _ ] => first [ constr_eq H H'; fail 1 + | revert H ] + end; + eexact H' + | .. ] ]; + [ intros; clear | .. ]. Ltac do_inline_cache_reify do_if_not_cached := pre_cache_reify (); [ try solve [ + cbv beta zeta; repeat match goal with H := ?e |- _ => is_evar e; subst H end; - eauto with nocore reify_gen_cache; + try solve [ split; [ solve [ eauto with nocore reify_gen_cache ] | solve [ eauto with wf_gen_cache; prove_Wf () ] ] ]; do_if_not_cached () ]; cache_reify () @@ -2067,185 +2194,217 @@ Abort. Module WordByWordMontgomery. Import Arithmetic.WordByWordMontgomery. Derive mul_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (m' : Z) - (f g : list Z), - Interp (t:=reify_type_of mulmod) - mul_gen bitwidth n m m' f g - = mulmod bitwidth n m m' f g) + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (m' : Z) + (f g : list Z), + Interp (t:=reify_type_of mulmod) + mul_gen bitwidth n m m' f g + = mulmod bitwidth n m m' f g) + /\ Wf mul_gen) As mul_gen_correct. Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = mulmod _ _ _ _ _ _) => simple apply mul_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = mulmod _ _ _ _ _ _) => simple apply (proj1 mul_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 mul_gen_correct) : wf_gen_cache. Derive square_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (m' : Z) - (f : list Z), - Interp (t:=reify_type_of squaremod) - square_gen bitwidth n m m' f - = squaremod bitwidth n m m' f) + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (m' : Z) + (f : list Z), + Interp (t:=reify_type_of squaremod) + square_gen bitwidth n m m' f + = squaremod bitwidth n m m' f) + /\ Wf square_gen) As square_gen_correct. Proof. Time cache_reify (). (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) (* - intros; etransitivity; [ | cbv [squaremod]; apply mul_gen_correct ]. - subst square_gen. - instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f f):list Z) in refine (r @ mul_gen)%Expr)). - reflexivity. + split. + { intros; etransitivity; [ | cbv [squaremod]; apply mul_gen_correct ]. + subst square_gen. + instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f f):list Z) in refine (r @ mul_gen)%Expr)). + reflexivity. } + { prove_Wf (). } *) Time Qed. - Hint Extern 1 (_ = squaremod _ _ _ _ _) => simple apply square_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = squaremod _ _ _ _ _) => simple apply (proj1 square_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 square_gen_correct) : wf_gen_cache. Derive encode_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (m' : Z) - (v : Z), - Interp (t:=reify_type_of encodemod) - encode_gen bitwidth n m m' v - = encodemod bitwidth n m m' v) + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (m' : Z) + (v : Z), + Interp (t:=reify_type_of encodemod) + encode_gen bitwidth n m m' v + = encodemod bitwidth n m m' v) + /\ Wf encode_gen) As encode_gen_correct. Proof. Time cache_reify (). (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) (* - intros; etransitivity; [ | cbv [encodemod]; apply mul_gen_correct ]. - subst encode_gen; revert bitwidth n m m' v. - lazymatch goal with - | [ |- forall bw n m m' v, ?interp ?ev bw n m m' v = ?interp' mul_gen bw n m m' (@?A bw n m m' v) (@?B bw n m m' v) ] - => let rv := constr:(fun F bw n m m' v => (F bw n m m' (A bw n m m' v) (B bw n m m' v)):list Z) in - intros; - instantiate (1:=ltac:(let r := Reify rv in - refine (r @ mul_gen)%Expr)) - end. - reflexivity. + split. + { intros; etransitivity; [ | cbv [encodemod]; apply mul_gen_correct ]. + subst encode_gen; revert bitwidth n m m' v. + lazymatch goal with + | [ |- forall bw n m m' v, ?interp ?ev bw n m m' v = ?interp' mul_gen bw n m m' (@?A bw n m m' v) (@?B bw n m m' v) ] + => let rv := constr:(fun F bw n m m' v => (F bw n m m' (A bw n m m' v) (B bw n m m' v)):list Z) in + intros; + instantiate (1:=ltac:(let r := Reify rv in + refine (r @ mul_gen)%Expr)) + end. + reflexivity. } + { prove_Wf (). } *) Time Qed. - Hint Extern 1 (_ = encodemod _ _ _ _ _) => simple apply encode_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = encodemod _ _ _ _ _) => simple apply (proj1 encode_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 encode_gen_correct) : wf_gen_cache. Derive add_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (f g : list Z), - Interp (t:=reify_type_of addmod) - add_gen bitwidth n m f g - = addmod bitwidth n m f g) + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (f g : list Z), + Interp (t:=reify_type_of addmod) + add_gen bitwidth n m f g + = addmod bitwidth n m f g) + /\ Wf add_gen) As add_gen_correct. Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = addmod _ _ _ _ _) => simple apply add_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = addmod _ _ _ _ _) => simple apply (proj1 add_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 add_gen_correct) : wf_gen_cache. Derive sub_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (f g : list Z), - Interp (t:=reify_type_of submod) - sub_gen bitwidth n m f g - = submod bitwidth n m f g) + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (f g : list Z), + Interp (t:=reify_type_of submod) + sub_gen bitwidth n m f g + = submod bitwidth n m f g) + /\ Wf sub_gen) As sub_gen_correct. Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = submod _ _ _ _ _) => simple apply sub_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = submod _ _ _ _ _) => simple apply (proj1 sub_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 sub_gen_correct) : wf_gen_cache. Derive opp_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (f : list Z), - Interp (t:=reify_type_of oppmod) - opp_gen bitwidth n m f - = oppmod bitwidth n m f) + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (f : list Z), + Interp (t:=reify_type_of oppmod) + opp_gen bitwidth n m f + = oppmod bitwidth n m f) + /\ Wf opp_gen) As opp_gen_correct. Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = oppmod _ _ _ _) => simple apply opp_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = oppmod _ _ _ _) => simple apply (proj1 opp_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 opp_gen_correct) : wf_gen_cache. Derive from_montgomery_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (m' : Z) - (f : list Z), - Interp (t:=reify_type_of from_montgomery_mod) - from_montgomery_gen bitwidth n m m' f - = from_montgomery_mod bitwidth n m m' f) + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (m' : Z) + (f : list Z), + Interp (t:=reify_type_of from_montgomery_mod) + from_montgomery_gen bitwidth n m m' f + = from_montgomery_mod bitwidth n m m' f) + /\ Wf from_montgomery_gen) As from_montgomery_gen_correct. Proof. Time cache_reify (). (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) (* - intros; etransitivity; [ | cbv [from_montgomery_mod]; apply mul_gen_correct ]. - subst from_montgomery_gen. - instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f (onemod bitwidth n)):list Z) in refine (r @ mul_gen)%Expr)). - reflexivity. + split. + { intros; etransitivity; [ | cbv [from_montgomery_mod]; apply mul_gen_correct ]. + subst from_montgomery_gen. + instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f (onemod bitwidth n)):list Z) in refine (r @ mul_gen)%Expr)). + reflexivity. } + { prove_Wf (). } *) Qed. - Hint Extern 1 (_ = from_montgomery_mod _ _ _ _ _) => simple apply from_montgomery_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = from_montgomery_mod _ _ _ _ _) => simple apply (proj1 from_montgomery_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 from_montgomery_gen_correct) : wf_gen_cache. Definition zeromod bitwidth n m m' := encodemod bitwidth n m m' 0. Definition onemod bitwidth n m m' := encodemod bitwidth n m m' 1. Derive zero_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (m' : Z), - Interp (t:=reify_type_of zeromod) - zero_gen bitwidth n m m' - = zeromod bitwidth n m m') + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (m' : Z), + Interp (t:=reify_type_of zeromod) + zero_gen bitwidth n m m' + = zeromod bitwidth n m m') + /\ Wf zero_gen) As zero_gen_correct. Proof. (* Time cache_reify (). *) (* we do something faster *) - intros; etransitivity; [ | cbv [zeromod]; apply encode_gen_correct ]. - subst zero_gen. - instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) => (F bitwidth n m m' 0):list Z) in refine (r @ encode_gen)%Expr)). - reflexivity. + split. + { intros; etransitivity; [ | cbv [zeromod]; apply encode_gen_correct ]. + subst zero_gen. + instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) => (F bitwidth n m m' 0):list Z) in refine (r @ encode_gen)%Expr)). + reflexivity. } + { prove_Wf (). } Qed. - Hint Extern 1 (_ = zeromod _ _ _ _) => simple apply zero_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = zeromod _ _ _ _) => simple apply (proj1 zero_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 zero_gen_correct) : wf_gen_cache. Derive one_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (m : Z) - (m' : Z), - Interp (t:=reify_type_of onemod) - one_gen bitwidth n m m' - = onemod bitwidth n m m') + SuchThat ((forall (bitwidth : Z) + (n : nat) + (m : Z) + (m' : Z), + Interp (t:=reify_type_of onemod) + one_gen bitwidth n m m' + = onemod bitwidth n m m') + /\ Wf one_gen) As one_gen_correct. Proof. (* Time cache_reify (). *) (* we do something faster *) - intros; etransitivity; [ | cbv [onemod]; apply encode_gen_correct ]. - subst one_gen. - instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) => (F bitwidth n m m' 1):list Z) in refine (r @ encode_gen)%Expr)). - reflexivity. + split. + { intros; etransitivity; [ | cbv [onemod]; apply encode_gen_correct ]. + subst one_gen. + instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) => (F bitwidth n m m' 1):list Z) in refine (r @ encode_gen)%Expr)). + reflexivity. } + { prove_Wf (). } Qed. - Hint Extern 1 (_ = onemod _ _ _ _) => simple apply one_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = onemod _ _ _ _) => simple apply (proj1 one_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 one_gen_correct) : wf_gen_cache. Derive nonzero_gen - SuchThat (forall (f : list Z), - Interp (t:=reify_type_of nonzeromod) - nonzero_gen f - = nonzeromod f) + SuchThat ((forall (f : list Z), + Interp (t:=reify_type_of nonzeromod) + nonzero_gen f + = nonzeromod f) + /\ Wf nonzero_gen) As nonzero_gen_correct. Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = nonzeromod _) => simple apply nonzero_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = nonzeromod _) => simple apply (proj1 nonzero_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 nonzero_gen_correct) : wf_gen_cache. Derive to_bytes_gen - SuchThat (forall (bitwidth : Z) - (n : nat) - (f : list Z), - Interp (t:=reify_type_of to_bytesmod) - to_bytes_gen bitwidth n f - = to_bytesmod bitwidth n f) + SuchThat ((forall (bitwidth : Z) + (n : nat) + (f : list Z), + Interp (t:=reify_type_of to_bytesmod) + to_bytes_gen bitwidth n f + = to_bytesmod bitwidth n f) + /\ Wf to_bytes_gen) As to_bytes_gen_correct. Proof. cache_reify (). Qed. - Hint Extern 1 (_ = to_bytesmod _ _ _) => simple apply to_bytes_gen_correct : reify_gen_cache. + Hint Extern 1 (_ = to_bytesmod _ _ _) => simple apply (proj1 to_bytes_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 to_bytes_gen_correct) : wf_gen_cache. Section rcarry_mul. Context (s : Z) @@ -2323,7 +2482,7 @@ Module WordByWordMontgomery. Notation BoundsPipeline_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - (*false*) true None + (*false*) true None I relax_zrange (relax_zrange_gen_good _) _ @@ -2345,7 +2504,7 @@ Module WordByWordMontgomery. Notation BoundsPipeline_no_subst01_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - (*false*) false None + (*false*) false None I relax_zrange (relax_zrange_gen_good _) _ @@ -2367,7 +2526,7 @@ Module WordByWordMontgomery. Notation BoundsPipeline_with_bytes_no_subst01_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - (*false*) false None + (*false*) false None I relax_zrange_with_bytes (relax_zrange_gen_good _) _ @@ -2690,8 +2849,8 @@ Module WordByWordMontgomery. => intros; let H1 := fresh in let H2 := fresh in - unshelve edestruct H as [H1 H2]; [ .. | solve [ split; [ eapply H1 | eapply H2 ] ] ]; - solve [ exact tt | eassumption | reflexivity ] + unshelve edestruct H as [H1 H2]; [ .. | solve [ split; [ eapply H1 | refine (H2 _) ] ] ]; + solve [ exact tt | eassumption | reflexivity | repeat split ] | _ => idtac end; repeat first [ eassumption @@ -2705,21 +2864,21 @@ Module WordByWordMontgomery. | intros; apply conj | omega ]. } { cbv zeta; intros f Hf; split. - { apply Hto_bytesv; assumption. } + { apply Hto_bytesv; solve [ assumption | repeat split ]. } { cbn [type.for_each_lhs_of_arrow type_base type.andb_bool_for_each_lhs_of_arrow ZRange.type.option.is_bounded_by fst snd] in *. rewrite Bool.andb_true_iff in *; split_and'. apply to_bytesmod_correct; eauto; []. split; cbv [small]. - admit. - admit. } } + repeat match goal with H : _ |- _ => revert H end; exact admit. + repeat match goal with H : _ |- _ => revert H end; exact admit. } } { intros. split; [ intro H'; eapply nonzeromod_correct; [ .. | rewrite <- H'; symmetry; eapply Hrnonzerov ] | etransitivity; [ apply Hrnonzerov | eapply nonzeromod_correct; [ .. | eassumption ] ] ]; - try eassumption. - admit. - admit. } - Admitted. + try solve [ eassumption | repeat split ]. + repeat match goal with H : _ |- _ => revert H end; exact admit. + repeat match goal with H : _ |- _ => revert H end; exact admit. } + Qed. End make_ring. Section for_stringification. @@ -2826,15 +2985,17 @@ Module SaturatedSolinas. End MulMod. Derive mulmod_gen - SuchThat (forall (log2base s : Z) (c : list (Z * Z)) (n nreductions : nat) - (f g : list Z), - Interp (t:=reify_type_of mulmod') - mulmod_gen s c log2base n nreductions f g - = mulmod' s c log2base n nreductions f g) + SuchThat ((forall (log2base s : Z) (c : list (Z * Z)) (n nreductions : nat) + (f g : list Z), + Interp (t:=reify_type_of mulmod') + mulmod_gen s c log2base n nreductions f g + = mulmod' s c log2base n nreductions f g) + /\ Wf mulmod_gen) As mulmod_gen_correct. Proof. Time cache_reify (). Time Qed. Module Export ReifyHints. - Global Hint Extern 1 (_ = mulmod' _ _ _ _ _ _ _) => simple apply mulmod_gen_correct : reify_gen_cache. + Global Hint Extern 1 (_ = mulmod' _ _ _ _ _ _ _) => simple apply (proj1 mulmod_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 mulmod_gen_correct) : wf_gen_cache. End ReifyHints. Section rmulmod. @@ -2884,7 +3045,7 @@ Module SaturatedSolinas. Notation BoundsPipeline_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - (*false*) false None + (*false*) false None I relax_zrange (relax_zrange_gen_good _) _ @@ -3513,16 +3674,18 @@ Module BarrettReduction. Strategy -10 [barrett_reduce reduce]. Derive barrett_red_gen - SuchThat (forall (k M muLow : Z) - (n nout: nat) - (xLow xHigh : Z), - Interp (t:=reify_type_of barrett_reduce) - barrett_red_gen k M muLow n nout xLow xHigh - = barrett_reduce k M muLow n nout xLow xHigh) + SuchThat ((forall (k M muLow : Z) + (n nout: nat) + (xLow xHigh : Z), + Interp (t:=reify_type_of barrett_reduce) + barrett_red_gen k M muLow n nout xLow xHigh + = barrett_reduce k M muLow n nout xLow xHigh) + /\ Wf barrett_red_gen) As barrett_red_gen_correct. Proof. Time cache_reify (). Time Qed. (* Now only takes ~5-10 s, because we set up [Strategy] commands correctly *) Module Export ReifyHints. - Global Hint Extern 1 (_ = barrett_reduce _ _ _ _ _ _ _) => simple apply barrett_red_gen_correct : reify_gen_cache. + Global Hint Extern 1 (_ = barrett_reduce _ _ _ _ _ _ _) => simple apply (proj1 barrett_red_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 barrett_red_gen_correct) : wf_gen_cache. End ReifyHints. Section rbarrett_red. @@ -3574,10 +3737,24 @@ Module BarrettReduction. := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list; Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list |}). + Lemma fancy_args_good + : match fancy_args with + | Some {| Pipeline.invert_low := il ; Pipeline.invert_high := ih |} + => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) + | None => True + end. + Proof. + cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right]; + split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence. + Qed. + Notation BoundsPipeline_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - false (* subst01 *) fancy_args + false (* subst01 *) + fancy_args + fancy_args_good relax_zrange relax_zrange_good _ @@ -3695,17 +3872,19 @@ Module MontgomeryReduction. End MontRed'. Derive montred_gen - SuchThat (forall (N R N' : Z) - (Zlog2R : Z) - (n nout: nat) - (lo_hi : Z * Z), - Interp (t:=reify_type_of montred') - montred_gen N R N' Zlog2R n nout lo_hi - = montred' N R N' Zlog2R n nout lo_hi) + SuchThat ((forall (N R N' : Z) + (Zlog2R : Z) + (n nout: nat) + (lo_hi : Z * Z), + Interp (t:=reify_type_of montred') + montred_gen N R N' Zlog2R n nout lo_hi + = montred' N R N' Zlog2R n nout lo_hi) + /\ Wf montred_gen) As montred_gen_correct. Proof. Time cache_reify (). Time Qed. Module Export ReifyHints. - Global Hint Extern 1 (_ = montred' _ _ _ _ _ _ _) => simple apply montred_gen_correct : reify_gen_cache. + Global Hint Extern 1 (_ = montred' _ _ _ _ _ _ _) => simple apply (proj1 montred_gen_correct) : reify_gen_cache. + Hint Immediate (proj2 montred_gen_correct) : wf_gen_cache. End ReifyHints. Section rmontred. @@ -3729,10 +3908,24 @@ Module MontgomeryReduction. := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list; Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list |}). + Lemma fancy_args_good + : match fancy_args with + | Some {| Pipeline.invert_low := il ; Pipeline.invert_high := ih |} + => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) + | None => True + end. + Proof. + cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right]; + split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence. + Qed. + Notation BoundsPipeline_correct in_bounds out_bounds op := (fun rv (rop : Expr (reify_type_of op)) Hrop => @Pipeline.BoundsPipeline_correct_trans - false (* subst01 *) fancy_args + false (* subst01 *) + fancy_args + fancy_args_good relax_zrange (relax_zrange_gen_good _) _ diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index ab8f6d3e9..83afb62fb 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -2464,7 +2464,8 @@ Module Barrett256. Proof. intros. rewrite <-barrett_reduce_correct_specialized by assumption. - destruct (barrett_red256_correct (xLow, (xHigh, tt))) as [H1 H2]. + destruct (barrett_red256_correct (xLow, (xHigh, tt)) (xLow, (xHigh, tt))) as [H1 H2]. + { repeat split. } { cbn -[Z.pow]. rewrite !andb_true_iff. assert (M < 2^machine_wordsize) by (vm_compute; reflexivity). @@ -2930,7 +2931,8 @@ Module Montgomery256. Proof. intros. rewrite <-montred'_correct_specialized by assumption. - destruct (montred256_correct ((lo, hi), tt)) as [H2 H3]. + destruct (montred256_correct ((lo, hi), tt) ((lo, hi), tt)) as [H2 H3]. + { repeat split. } { cbn -[Z.pow]. rewrite !andb_true_iff. repeat apply conj; Z.ltb_to_lt; trivial; cbv [R N machine_wordsize] in *; lia. } diff --git a/src/Experiments/NewPipeline/UnderLetsWf.v b/src/Experiments/NewPipeline/UnderLetsProofs.v index 7d0e1aa6b..5a806ef9f 100644 --- a/src/Experiments/NewPipeline/UnderLetsWf.v +++ b/src/Experiments/NewPipeline/UnderLetsProofs.v @@ -146,6 +146,9 @@ Module Compilers. Proof. apply Interp_SubstVarOrIdent, Hwf. Qed. End SubstVarLike. + Hint Resolve SubstVarLike.Wf_SubstVar SubstVarLike.Wf_SubstVarFstSndPairOpp SubstVarLike.Wf_SubstVarLike SubstVarLike.Wf_SubstVarOrIdent : wf. + Hint Rewrite @SubstVarLike.Interp_SubstVar @SubstVarLike.Interp_SubstVarFstSndPairOpp @SubstVarLike.Interp_SubstVarLike @SubstVarLike.Interp_SubstVarOrIdent : interp. + Module UnderLets. Import UnderLets.Compilers.UnderLets. Section with_ident. @@ -456,4 +459,7 @@ Module Compilers. Qed. End reify. End UnderLets. + + Hint Resolve UnderLets.Wf_LetBindReturn : wf. + Hint Rewrite @UnderLets.Interp_LetBindReturn : interp. End Compilers. |