From fedf83bf32b26197dc89f0aae9b856e2107ec5d4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 27 Jul 2018 23:24:51 -0400 Subject: Integrate Wf and Interp proofs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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% --- _CoqProject | 5 +- .../NewPipeline/AbstractInterpretationProofs.v | 69 +- src/Experiments/NewPipeline/Language.v | 9 + src/Experiments/NewPipeline/LanguageWf.v | 46 +- .../NewPipeline/MiscCompilerPassesProofs.v | 202 +++++ src/Experiments/NewPipeline/MiscCompilerPassesWf.v | 204 ----- src/Experiments/NewPipeline/RewriterProofs.v | 59 ++ src/Experiments/NewPipeline/Toplevel1.v | 997 ++++++++++++--------- src/Experiments/NewPipeline/Toplevel2.v | 6 +- src/Experiments/NewPipeline/UnderLetsProofs.v | 465 ++++++++++ src/Experiments/NewPipeline/UnderLetsWf.v | 459 ---------- 11 files changed, 1440 insertions(+), 1081 deletions(-) create mode 100644 src/Experiments/NewPipeline/MiscCompilerPassesProofs.v delete mode 100644 src/Experiments/NewPipeline/MiscCompilerPassesWf.v create mode 100644 src/Experiments/NewPipeline/RewriterProofs.v create mode 100644 src/Experiments/NewPipeline/UnderLetsProofs.v delete mode 100644 src/Experiments/NewPipeline/UnderLetsWf.v 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/MiscCompilerPassesProofs.v b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v new file mode 100644 index 000000000..52101023a --- /dev/null +++ b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v @@ -0,0 +1,202 @@ +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.MiscCompilerPasses. +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. + +Module Compilers. + Import Language.Compilers. + Import LanguageInversion.Compilers. + Import LanguageWf.Compilers. + Import MiscCompilerPasses.Compilers. + Import expr.Notations. + Import invert_expr. + Import defaults. + + Module DeadCodeElimination. + Import MiscCompilerPasses.Compilers.DeadCodeElimination. + + (** Rather than proving correctness of the computation of live + variables and requiring something about [live], we instead + rely on the fact that DCE in fact just inlines code it + believes to be dead. *) + Local Transparent OUGHT_TO_BE_UNUSED. + Lemma OUGHT_TO_BE_UNUSED_id {T1 T2} (v : T1) (v' : T2) : OUGHT_TO_BE_UNUSED v v' = v. + Proof. exact eq_refl. Qed. + Local Opaque OUGHT_TO_BE_UNUSED. + + Local Ltac simplifier_t_step := + first [ progress cbn [fst snd] in * + | progress eta_expand + | rewrite OUGHT_TO_BE_UNUSED_id ]. + + Section with_ident. + Context {base_type : Type}. + Local Notation type := (type.type base_type). + Context {ident : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + + Section with_var. + Context {var1 var2 : type -> Type} + (live : PositiveSet.t). + Local Notation expr1 := (@expr.expr base_type ident var1). + Local Notation expr2 := (@expr.expr base_type ident var2). + Local Notation eliminate_dead'1 := (@eliminate_dead' base_type ident var1 live). + Local Notation eliminate_dead'2 := (@eliminate_dead' base_type ident var2 live). + Local Notation eliminate_dead1 := (@eliminate_dead base_type ident var1 live). + Local Notation eliminate_dead2 := (@eliminate_dead base_type ident var2 live). + + Lemma wf_eliminate_dead' G1 G2 t e1 e2 p + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) + : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (eliminate_dead'1 e1 p)) (snd (eliminate_dead'2 e2 p)) + /\ fst (eliminate_dead'1 e1 p) = fst (eliminate_dead'2 e2 p). + Proof. + intro Hwf; revert dependent G2; revert p; induction Hwf; + cbn [eliminate_dead']; + repeat first [ progress wf_safe_t + | simplifier_t_step + | progress split_and + | apply conj + | match goal with + | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto + end + | break_innermost_match_step + | solve [ wf_t ] ]. + Qed. + + Lemma wf_eliminate_dead t e1 e2 + : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (eliminate_dead1 e1) (eliminate_dead2 e2). + Proof. intro Hwf; apply wf_eliminate_dead' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. + End with_var. + + Lemma Wf_EliminateDead {t} (e : @expr.Expr base_type ident t) + : expr.Wf e -> expr.Wf (EliminateDead e). + Proof. intros Hwf var1 var2; eapply wf_eliminate_dead, Hwf. Qed. + + Section interp. + Context {base_interp : base_type -> Type} + {interp_ident : forall t, ident t -> type.interp base_interp t} + {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. + + Lemma interp_eliminate_dead'_gen (live : PositiveSet.t) G t (e1 e2 : expr t) + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) + (Hwf : expr.wf G e1 e2) + p + : expr.interp interp_ident (snd (eliminate_dead' live e1 p)) == expr.interp interp_ident e2. + Proof. + revert p; induction Hwf; cbn [eliminate_dead']; cbv [Proper respectful] in *; + repeat first [ progress interp_safe_t + | simplifier_t_step + | break_innermost_match_step + | interp_unsafe_t_step ]. + Qed. + + Lemma interp_eliminate_dead live t (e1 e2 : expr t) + (Hwf : expr.wf nil e1 e2) + : expr.interp interp_ident (eliminate_dead live e1) == expr.interp interp_ident e2. + Proof. apply interp_eliminate_dead'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. + + Lemma Interp_EliminateDead {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (EliminateDead e) == expr.Interp interp_ident e. + Proof. apply interp_eliminate_dead, Hwf. Qed. + End interp. + End with_ident. + End DeadCodeElimination. + + Hint Resolve DeadCodeElimination.Wf_EliminateDead : wf. + Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp. + + Module Subst01. + Import MiscCompilerPasses.Compilers.Subst01. + + Local Ltac simplifier_t_step := + first [ progress cbn [fst snd] in * + | progress eta_expand ]. + + Section with_ident. + Context {base_type : Type}. + Local Notation type := (type.type base_type). + Context {ident : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + + Section with_var. + Context {var1 var2 : type -> Type} + (live : PositiveMap.t nat). + Local Notation expr1 := (@expr.expr base_type ident var1). + Local Notation expr2 := (@expr.expr base_type ident var2). + Local Notation subst01'1 := (@subst01' base_type ident var1 live). + Local Notation subst01'2 := (@subst01' base_type ident var2 live). + Local Notation subst011 := (@subst01 base_type ident var1 live). + Local Notation subst012 := (@subst01 base_type ident var2 live). + + Lemma wf_subst01' G1 G2 t e1 e2 p + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) + : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (subst01'1 e1 p)) (snd (subst01'2 e2 p)) + /\ fst (subst01'1 e1 p) = fst (subst01'2 e2 p). + Proof. + intro Hwf; revert dependent G2; revert p; induction Hwf; + cbn [subst01']; + repeat first [ progress wf_safe_t + | simplifier_t_step + | progress split_and + | apply conj + | match goal with + | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto + end + | break_innermost_match_step + | solve [ wf_t ] ]. + Qed. + + Lemma wf_subst01 t e1 e2 + : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst011 e1) (subst012 e2). + Proof. intro Hwf; apply wf_subst01' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. + End with_var. + + Lemma Wf_Subst01 {t} (e : @expr.Expr base_type ident t) + : expr.Wf e -> expr.Wf (Subst01 e). + Proof. intros Hwf var1 var2; eapply wf_subst01, Hwf. Qed. + + Section interp. + Context {base_interp : base_type -> Type} + {interp_ident : forall t, ident t -> type.interp base_interp t} + {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. + + Lemma interp_subst01'_gen (live : PositiveMap.t nat) G t (e1 e2 : expr t) + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) + (Hwf : expr.wf G e1 e2) + p + : expr.interp interp_ident (snd (subst01' live e1 p)) == expr.interp interp_ident e2. + Proof. + revert p; induction Hwf; cbn [subst01']; cbv [Proper respectful] in *; + repeat first [ progress interp_safe_t + | simplifier_t_step + | break_innermost_match_step + | interp_unsafe_t_step ]. + Qed. + + Lemma interp_subst01 live t (e1 e2 : expr t) + (Hwf : expr.wf nil e1 e2) + : expr.interp interp_ident (subst01 live e1) == expr.interp interp_ident e2. + Proof. apply interp_subst01'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. + + Lemma Interp_Subst01 {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (Subst01 e) == expr.Interp interp_ident e. + Proof. apply interp_subst01, Hwf. Qed. + 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/MiscCompilerPassesWf.v b/src/Experiments/NewPipeline/MiscCompilerPassesWf.v deleted file mode 100644 index 50211feb3..000000000 --- a/src/Experiments/NewPipeline/MiscCompilerPassesWf.v +++ /dev/null @@ -1,204 +0,0 @@ -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.MiscCompilerPasses. -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. - -(* - - -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. - Import LanguageWf.Compilers. - Import MiscCompilerPasses.Compilers. - Import expr.Notations. - Import invert_expr. - Import defaults. - - Module DeadCodeElimination. - Import MiscCompilerPasses.Compilers.DeadCodeElimination. - - (** Rather than proving correctness of the computation of live - variables and requiring something about [live], we instead - rely on the fact that DCE in fact just inlines code it - believes to be dead. *) - Local Transparent OUGHT_TO_BE_UNUSED. - Lemma OUGHT_TO_BE_UNUSED_id {T1 T2} (v : T1) (v' : T2) : OUGHT_TO_BE_UNUSED v v' = v. - Proof. exact eq_refl. Qed. - Local Opaque OUGHT_TO_BE_UNUSED. - - Local Ltac simplifier_t_step := - first [ progress cbn [fst snd] in * - | progress eta_expand - | rewrite OUGHT_TO_BE_UNUSED_id ]. - - Section with_ident. - Context {base_type : Type}. - Local Notation type := (type.type base_type). - Context {ident : type -> Type}. - Local Notation expr := (@expr.expr base_type ident). - - Section with_var. - Context {var1 var2 : type -> Type} - (live : PositiveSet.t). - Local Notation expr1 := (@expr.expr base_type ident var1). - Local Notation expr2 := (@expr.expr base_type ident var2). - Local Notation eliminate_dead'1 := (@eliminate_dead' base_type ident var1 live). - Local Notation eliminate_dead'2 := (@eliminate_dead' base_type ident var2 live). - Local Notation eliminate_dead1 := (@eliminate_dead base_type ident var1 live). - Local Notation eliminate_dead2 := (@eliminate_dead base_type ident var2 live). - - Lemma wf_eliminate_dead' G1 G2 t e1 e2 p - (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) - : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (eliminate_dead'1 e1 p)) (snd (eliminate_dead'2 e2 p)) - /\ fst (eliminate_dead'1 e1 p) = fst (eliminate_dead'2 e2 p). - Proof. - intro Hwf; revert dependent G2; revert p; induction Hwf; - cbn [eliminate_dead']; - repeat first [ progress wf_safe_t - | simplifier_t_step - | progress split_and - | apply conj - | match goal with - | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto - end - | break_innermost_match_step - | solve [ wf_t ] ]. - Qed. - - Lemma wf_eliminate_dead t e1 e2 - : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (eliminate_dead1 e1) (eliminate_dead2 e2). - Proof. intro Hwf; apply wf_eliminate_dead' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. - End with_var. - - Lemma Wf_EliminateDead {t} (e : @expr.Expr base_type ident t) - : expr.Wf e -> expr.Wf (EliminateDead e). - Proof. intros Hwf var1 var2; eapply wf_eliminate_dead, Hwf. Qed. - - Section interp. - Context {base_interp : base_type -> Type} - {interp_ident : forall t, ident t -> type.interp base_interp t} - {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. - - Lemma interp_eliminate_dead'_gen (live : PositiveSet.t) G t (e1 e2 : expr t) - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) - (Hwf : expr.wf G e1 e2) - p - : expr.interp interp_ident (snd (eliminate_dead' live e1 p)) == expr.interp interp_ident e2. - Proof. - revert p; induction Hwf; cbn [eliminate_dead']; cbv [Proper respectful] in *; - repeat first [ progress interp_safe_t - | simplifier_t_step - | break_innermost_match_step - | interp_unsafe_t_step ]. - Qed. - - Lemma interp_eliminate_dead live t (e1 e2 : expr t) - (Hwf : expr.wf nil e1 e2) - : expr.interp interp_ident (eliminate_dead live e1) == expr.interp interp_ident e2. - Proof. apply interp_eliminate_dead'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. - - Lemma Interp_EliminateDead {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) - : expr.Interp interp_ident (EliminateDead e) == expr.Interp interp_ident e. - Proof. apply interp_eliminate_dead, Hwf. Qed. - End interp. - End with_ident. - End DeadCodeElimination. - - Module Subst01. - Import MiscCompilerPasses.Compilers.Subst01. - - Local Ltac simplifier_t_step := - first [ progress cbn [fst snd] in * - | progress eta_expand ]. - - Section with_ident. - Context {base_type : Type}. - Local Notation type := (type.type base_type). - Context {ident : type -> Type}. - Local Notation expr := (@expr.expr base_type ident). - - Section with_var. - Context {var1 var2 : type -> Type} - (live : PositiveMap.t nat). - Local Notation expr1 := (@expr.expr base_type ident var1). - Local Notation expr2 := (@expr.expr base_type ident var2). - Local Notation subst01'1 := (@subst01' base_type ident var1 live). - Local Notation subst01'2 := (@subst01' base_type ident var2 live). - Local Notation subst011 := (@subst01 base_type ident var1 live). - Local Notation subst012 := (@subst01 base_type ident var2 live). - - Lemma wf_subst01' G1 G2 t e1 e2 p - (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) - : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (subst01'1 e1 p)) (snd (subst01'2 e2 p)) - /\ fst (subst01'1 e1 p) = fst (subst01'2 e2 p). - Proof. - intro Hwf; revert dependent G2; revert p; induction Hwf; - cbn [subst01']; - repeat first [ progress wf_safe_t - | simplifier_t_step - | progress split_and - | apply conj - | match goal with - | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto - end - | break_innermost_match_step - | solve [ wf_t ] ]. - Qed. - - Lemma wf_subst01 t e1 e2 - : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst011 e1) (subst012 e2). - Proof. intro Hwf; apply wf_subst01' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. - End with_var. - - Lemma Wf_Subst01 {t} (e : @expr.Expr base_type ident t) - : expr.Wf e -> expr.Wf (Subst01 e). - Proof. intros Hwf var1 var2; eapply wf_subst01, Hwf. Qed. - - Section interp. - Context {base_interp : base_type -> Type} - {interp_ident : forall t, ident t -> type.interp base_interp t} - {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. - - Lemma interp_subst01'_gen (live : PositiveMap.t nat) G t (e1 e2 : expr t) - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) - (Hwf : expr.wf G e1 e2) - p - : expr.interp interp_ident (snd (subst01' live e1 p)) == expr.interp interp_ident e2. - Proof. - revert p; induction Hwf; cbn [subst01']; cbv [Proper respectful] in *; - repeat first [ progress interp_safe_t - | simplifier_t_step - | break_innermost_match_step - | interp_unsafe_t_step ]. - Qed. - - Lemma interp_subst01 live t (e1 e2 : expr t) - (Hwf : expr.wf nil e1 e2) - : expr.interp interp_ident (subst01 live e1) == expr.interp interp_ident e2. - Proof. apply interp_subst01'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. - - Lemma Interp_Subst01 {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) - : expr.Interp interp_ident (Subst01 e) == expr.Interp interp_ident e. - Proof. apply interp_subst01, Hwf. Qed. - End interp. - End with_ident. - End Subst01. -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/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v new file mode 100644 index 000000000..5a806ef9f --- /dev/null +++ b/src/Experiments/NewPipeline/UnderLetsProofs.v @@ -0,0 +1,465 @@ +Require Import Coq.Lists.List. +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Experiments.NewPipeline.LanguageInversion. +Require Import Crypto.Experiments.NewPipeline.LanguageWf. +Require Import Crypto.Experiments.NewPipeline.UnderLets. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Option. +Import ListNotations. Local Open Scope list_scope. + +Import EqNotations. +Module Compilers. + Import Language.Compilers. + Import LanguageInversion.Compilers. + Import LanguageWf.Compilers. + Import UnderLets.Compilers. + Import ident.Notations. + Import expr.Notations. + Import invert_expr. + + Module SubstVarLike. + Section with_ident. + Context {base_type : Type}. + Local Notation type := (type.type base_type). + Context {ident : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + Section with_var. + Context {var1 var2 : type -> Type}. + Local Notation expr1 := (@expr.expr base_type ident var1). + Local Notation expr2 := (@expr.expr base_type ident var2). + Section with_var_like. + Context (is_var_like1 : forall t, @expr var1 t -> bool) + (is_var_like2 : forall t, @expr var2 t -> bool). + Local Notation subst_var_like1 := (@SubstVarLike.subst_var_like base_type ident var1 is_var_like1). + Local Notation subst_var_like2 := (@SubstVarLike.subst_var_like base_type ident var2 is_var_like2). + Definition is_var_like_wfT := forall G t e1 e2, expr.wf G (t:=t) e1 e2 -> is_var_like1 t e1 = is_var_like2 t e2. + Context (is_var_like_good : is_var_like_wfT). + + Lemma wf_subst_var_like G1 G2 t e1 e2 + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) + : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (subst_var_like1 e1) (subst_var_like2 e2). + Proof. + cbv [is_var_like_wfT] in *. + intro Hwf; revert dependent G2; induction Hwf; + cbn [SubstVarLike.subst_var_like]; + repeat first [ match goal with + | [ H : is_var_like1 _ ?x = _, H' : is_var_like2 _ ?y = _ |- _ ] + => assert (is_var_like1 _ x = is_var_like2 _ y) by eauto; congruence + end + | progress wf_safe_t + | progress break_innermost_match + | solve [ wf_t ] ]. + Qed. + End with_var_like. + + Section with_ident_like. + Context (ident_is_good : forall t, ident t -> bool). + + Lemma wfT_is_recursively_var_or_ident + : is_var_like_wfT (fun t => SubstVarLike.is_recursively_var_or_ident ident_is_good) + (fun t => SubstVarLike.is_recursively_var_or_ident ident_is_good). + Proof. + intros G t e1 e2 Hwf; induction Hwf; cbn [SubstVarLike.is_recursively_var_or_ident]; + congruence. + Qed. + End with_ident_like. + + Lemma wfT_is_var + : is_var_like_wfT (fun _ e => match invert_Var e with Some _ => true | None => false end) + (fun _ e => match invert_Var e with Some _ => true | None => false end). + Proof. intros G t e1 e2 Hwf; destruct Hwf; cbn [invert_Var]; reflexivity. Qed. + End with_var. + + Local Notation SubstVarLike := (@SubstVarLike.SubstVarLike base_type ident). + Local Notation SubstVar := (@SubstVarLike.SubstVar base_type ident). + Local Notation SubstVarOrIdent := (@SubstVarLike.SubstVarOrIdent base_type ident). + + Lemma Wf_SubstVarLike (is_var_like : forall var t, @expr var t -> bool) + (is_var_like_good : forall var1 var2, is_var_like_wfT (is_var_like var1) (is_var_like var2)) + {t} (e : expr.Expr t) + : expr.Wf e -> expr.Wf (SubstVarLike is_var_like e). + Proof. + intros Hwf var1 var2; eapply wf_subst_var_like; eauto with nocore; cbn [In]; tauto. + Qed. + + Lemma Wf_SubstVar {t} (e : expr.Expr t) + : expr.Wf e -> expr.Wf (SubstVar e). + Proof. + intros Hwf var1 var2; eapply wf_subst_var_like; eauto using wfT_is_var with nocore; cbn [In]; tauto. + Qed. + + Lemma Wf_SubstVarOrIdent (should_subst_ident : forall t, ident t -> bool) + {t} (e : expr.Expr t) + : expr.Wf e -> expr.Wf (SubstVarOrIdent should_subst_ident e). + Proof. + intros Hwf var1 var2; eapply wf_subst_var_like; eauto using wfT_is_recursively_var_or_ident with nocore; cbn [In]; tauto. + Qed. + + Section interp. + Context {base_interp : base_type -> Type} + {interp_ident : forall t, ident t -> type.interp base_interp t} + {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. + Section with_is_var_like. + Context (is_var_like : forall t, @expr (type.interp base_interp) t -> bool). + + Lemma interp_subst_var_like_gen G t (e1 e2 : expr t) + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) + (Hwf : expr.wf G e1 e2) + : expr.interp interp_ident (SubstVarLike.subst_var_like is_var_like e1) == expr.interp interp_ident e2. + Proof. + induction Hwf; cbn [SubstVarLike.subst_var_like]; cbv [Proper respectful] in *; + interp_safe_t; break_innermost_match; interp_safe_t. + Qed. + + Lemma interp_subst_var_like_gen_nil t (e1 e2 : expr t) + (Hwf : expr.wf nil e1 e2) + : expr.interp interp_ident (SubstVarLike.subst_var_like is_var_like e1) == expr.interp interp_ident e2. + Proof. apply interp_subst_var_like_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. + End with_is_var_like. + + Lemma Interp_SubstVarLike (is_var_like : forall var t, @expr var t -> bool) + {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (SubstVarLike is_var_like e) == expr.Interp interp_ident e. + Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. + + Lemma Interp_SubstVar {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (SubstVar e) == expr.Interp interp_ident e. + Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. + + Lemma Interp_SubstVarOrIdent (should_subst_ident : forall t, ident t -> bool) + {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (SubstVarOrIdent should_subst_ident e) == expr.Interp interp_ident e. + Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. + End interp. + End with_ident. + + Lemma Wf_SubstVarFstSndPairOpp {t} (e : expr.Expr t) + : expr.Wf e -> expr.Wf (SubstVarLike.SubstVarFstSndPairOpp e). + Proof. apply Wf_SubstVarOrIdent. Qed. + + Lemma Interp_SubstVarFstSndPairOpp {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : defaults.Interp (SubstVarLike.SubstVarFstSndPairOpp e) == defaults.Interp e. + 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. + Context {base_type : Type}. + Local Notation type := (type.type base_type). + Context {ident : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + Local Notation UnderLets := (@UnderLets base_type ident). + + Section with_var. + Context {var1 var2 : type -> Type}. + + Inductive wf {T1 T2} {P : list { t : type & var1 t * var2 t }%type -> T1 -> T2 -> Prop} + : list { t : type & var1 t * var2 t }%type -> @UnderLets var1 T1 -> @UnderLets var2 T2 -> Prop := + | Wf_Base G e1 e2 : P G e1 e2 -> wf G (Base e1) (Base e2) + | Wf_UnderLet G A x1 x2 f1 f2 + : expr.wf G x1 x2 + -> (forall v1 v2, wf (existT _ A (v1, v2) :: G) (f1 v1) (f2 v2)) + -> wf G (UnderLet x1 f1) (UnderLet x2 f2). + Global Arguments wf {T1 T2} P _ _ _. + + Lemma wf_to_expr {t} (x : @UnderLets var1 (@expr var1 t)) (y : @UnderLets var2 (@expr var2 t)) + G + : wf (fun G => expr.wf G) G x y -> expr.wf G (to_expr x) (to_expr y). + Proof. + intro Hwf; induction Hwf; cbn [to_expr]; [ assumption | constructor; auto ]. + Qed. + End with_var. + End with_ident. + + Section reify. + Local Notation type := (type.type base.type). + Local Notation expr := (@expr.expr base.type ident). + Local Notation UnderLets := (@UnderLets.UnderLets base.type ident). + + Section with_var. + Context {var1 var2 : type -> Type}. + Local Notation expr1 := (@expr.expr base.type ident var1). + Local Notation expr2 := (@expr.expr base.type ident var2). + Local Notation UnderLets1 := (@UnderLets.UnderLets base.type ident var1). + Local Notation UnderLets2 := (@UnderLets.UnderLets base.type ident var2). + + Local Ltac wf_reify_and_let_binds_base_cps_t Hk := + repeat first [ lazymatch goal with + | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e1 = Some _, H'' : reflect_list ?e2 = None |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence + | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence + | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H + end + | progress subst + | progress destruct_head' False + | progress expr.inversion_wf_constr + | progress expr.inversion_expr + | progress expr.invert_subst + | progress destruct_head'_sig + | progress destruct_head'_ex + | progress destruct_head'_and + | progress type.inversion_type + | progress base.type.inversion_type + | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind combine list_rect length] in * + | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in * + | rewrite base.try_make_transport_cps_correct in * + | progress type_beq_to_eq + | discriminate + | congruence + | apply Hk + | exists nil; reflexivity + | eexists (cons _ nil); reflexivity + | rewrite app_assoc; eexists; reflexivity + | progress wf_safe_t + | match goal with + | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H + end + | progress inversion_option + | progress break_innermost_match_hyps + | progress expr.inversion_wf_one_constr + | progress expr.invert_match_step + | match goal with |- wf _ _ _ _ => constructor end + | match goal with + | [ H : context[wf _ _ _ _] |- wf _ _ _ _ ] => apply H; eauto with nocore + end + | progress wf_unsafe_t_step + | match goal with + | [ H : context[match Compilers.reify_list ?ls with _ => _ end] |- _ ] + => is_var ls; destruct ls; rewrite ?expr.reify_list_cons, ?expr.reify_list_nil in H + | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H + | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ] + => pose proof (fun x y pf => H x y (or_introl pf)); + pose proof (fun x y pf => H x y (or_intror pf)); + clear H + end ]. + + Lemma wf_reify_and_let_binds_base_cps {t : base.type} {T1 T2} (e1 : expr1 (type.base t)) (e2 : expr2 (type.base t)) + (k1 : expr1 (type.base t) -> UnderLets1 T1) (k2 : expr2 (type.base t) -> UnderLets2 T2) + (P : _ -> _ -> _ -> Prop) G + (Hwf : expr.wf G e1 e2) + (Hk : forall G' e1 e2, (exists seg, G' = seg ++ G) -> expr.wf G' e1 e2 -> wf P G' (k1 e1) (k2 e2)) + : wf P G (reify_and_let_binds_base_cps e1 T1 k1) (reify_and_let_binds_base_cps e2 T2 k2). + Proof. + revert dependent G; induction t; cbn [reify_and_let_binds_base_cps]; intros; + try (cbv [SubstVarLike.is_var_fst_snd_pair_opp] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption); + break_innermost_match; wf_reify_and_let_binds_base_cps_t Hk. + all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. + all: revert dependent k1; revert dependent k2. + all: lazymatch goal with + | [ H : length ?l1 = length ?l2 |- _ ] + => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros + end; + wf_reify_and_let_binds_base_cps_t Hk. + Qed. + + Lemma wf_let_bind_return {t} (e1 : expr1 t) (e2 : expr2 t) + G + (Hwf : expr.wf G e1 e2) + : expr.wf G (let_bind_return e1) (let_bind_return e2). + Proof. + revert dependent G; induction t; intros; cbn [let_bind_return]; cbv [invert_Abs]; + wf_safe_t; + expr.invert_match; expr.inversion_wf; try solve [ wf_t ]. + { apply wf_to_expr. + pose (P := fun t => { e1e2 : expr1 t * expr2 t | expr.wf G (fst e1e2) (snd e1e2) }). + pose ((exist _ (e1, e2) Hwf) : P _) as pkg. + change e1 with (fst (proj1_sig pkg)). + change e2 with (snd (proj1_sig pkg)). + clearbody pkg; clear Hwf e1 e2. + type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ]. + cbn [fst snd proj1_sig proj2_sig] in *. + repeat match goal with + | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ] + => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity) + end. + assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity). + revert pf. + rewrite H'; clear H'. + induction Hwf; break_innermost_match; break_innermost_match_hyps; + repeat first [ progress intros + | progress type.inversion_type + | progress base.type.inversion_type + | progress wf_safe_t + | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal] in * + | match goal with + | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) + | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl) + | [ |- wf _ _ _ _ ] => constructor + end + | solve [ eauto ] + | apply wf_reify_and_let_binds_base_cps ]. } + Qed. + End with_var. + + Lemma Wf_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : expr.Wf (LetBindReturn e). + Proof. intros ??; apply wf_let_bind_return, Hwf. Qed. + + Local Ltac interp_to_expr_reify_and_let_binds_base_cps_t Hk := + repeat first [ progress subst + | progress destruct_head' False + | progress destruct_head'_and + | progress destruct_head' iff + | progress specialize_by_assumption + | progress expr.inversion_wf_constr + | progress expr.inversion_expr + | progress expr.invert_subst + | progress destruct_head'_sig + | progress destruct_head'_ex + | progress destruct_head'_and + | progress type.inversion_type + | progress base.type.inversion_type + | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind to_expr expr.interp ident.interp ident.gen_interp type.eqv length list_rect combine In] in * + | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in * + | rewrite base.try_make_transport_cps_correct in * + | progress type_beq_to_eq + | discriminate + | congruence + | apply Hk + | exists nil; reflexivity + | eexists (cons _ nil); reflexivity + | rewrite app_assoc; eexists; reflexivity + | rewrite expr.reify_list_cons + | rewrite expr.reify_list_nil + | progress interp_safe_t + | match goal with + | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H + | [ H : forall t v1 v2, In _ _ -> _ == _, H' : In _ _ |- _ ] => apply H in H' + end + | progress inversion_option + | progress break_innermost_match_hyps + | progress expr.inversion_wf_one_constr + | progress expr.invert_match_step + | match goal with + | [ |- ?R (expr.interp _ ?e1) (expr.interp _ ?e2) ] + => solve [ eapply (@expr.wf_interp_Proper _ _ e1 e2); eauto ] + | [ H : context[reflect_list (reify_list _)] |- _ ] => rewrite expr.reflect_reify_list in H + | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ] + => pose proof (fun x y pf => H x y (or_introl pf)); + pose proof (fun x y pf => H x y (or_intror pf)); + clear H + end + | progress interp_unsafe_t_step + | match goal with + | [ H : expr.wf _ (reify_list _) ?e |- _ ] + => is_var e; destruct (reflect_list e) eqn:?; expr.invert_subst; + [ rewrite expr.wf_reify_list in H | apply expr.wf_reflect_list in H ] + | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H + | [ H : context[expr.interp _ _ = _] |- expr.interp _ (to_expr _) = ?k2 _ ] + => erewrite H; clear H; + [ match goal with + | [ |- ?k (expr.interp ?ii ?e) = ?k' ?v ] + => has_evar e; + let p := fresh in + set (p := expr.interp ii e); + match v with + | context G[expr.interp ii ?e'] + => unify e e'; let v' := context G[p] in change (k p = k' v') + end; + clearbody p; reflexivity + end + | .. ] + end ]. + + Lemma interp_to_expr_reify_and_let_binds_base_cps {t : base.type} {t' : base.type} (e1 : expr (type.base t)) (e2 : expr (type.base t)) + G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) + (Hwf : expr.wf G e1 e2) + (k1 : expr (type.base t) -> UnderLets _ (expr (type.base t'))) + (k2 : base.interp t -> base.interp t') + (Hk : forall e1 v, defaults.interp e1 == v -> defaults.interp (to_expr (k1 e1)) == k2 v) + : defaults.interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (defaults.interp e2). + Proof. + revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros; + try (cbv [SubstVarLike.is_var_fst_snd_pair_opp] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption); + break_innermost_match; interp_to_expr_reify_and_let_binds_base_cps_t Hk. + all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. + all: revert dependent k1; revert dependent k2. + all: lazymatch goal with + | [ H : length ?l1 = length ?l2 |- _ ] + => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros + end; + interp_to_expr_reify_and_let_binds_base_cps_t Hk. + Qed. + + Lemma interp_let_bind_return {t} (e1 e2 : expr t) + G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) + (Hwf : expr.wf G e1 e2) + : defaults.interp (let_bind_return e1) == defaults.interp e2. + Proof. + revert dependent G; induction t; intros; cbn [let_bind_return type.eqv expr.interp] in *; cbv [invert_Abs respectful] in *; + repeat first [ progress wf_safe_t + | progress expr.invert_subst + | progress expr.invert_match + | progress expr.inversion_wf + | progress break_innermost_match_hyps + | progress destruct_head' False + | solve [ wf_t ] + | match goal with + | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] + => eapply (H e0 (e @ $v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ] + | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] + => cbn [expr.interp]; eapply H; [ | solve [ wf_t ] ]; solve [ wf_t ] + end ]; + []. + { pose (P := fun t => { e1e2 : expr t * expr t | expr.wf G (fst e1e2) (snd e1e2) }). + pose ((exist _ (e1, e2) Hwf) : P _) as pkg. + change e1 with (fst (proj1_sig pkg)). + change e2 with (snd (proj1_sig pkg)). + clearbody pkg; clear Hwf e1 e2. + type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ]. + cbn [fst snd proj1_sig proj2_sig] in *. + repeat match goal with + | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ] + => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity) + end. + assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity). + revert pf. + rewrite H'; clear H'. + induction Hwf; break_innermost_match; break_innermost_match_hyps; + repeat first [ progress intros + | progress type.inversion_type + | progress base.type.inversion_type + | progress wf_safe_t + | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal to_expr] in * + | match goal with + | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) + | [ H : forall x (pf : ?a = ?a), _ |- _ ] => specialize (fun x => H x eq_refl) + | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl) + | [ H : forall x y z (pf : ?a = ?a), _ |- _ ] => specialize (fun x y z => H x y z eq_refl) + | [ |- context[(expr_let x := _ in _)%expr] ] => progress cbn [expr.interp]; cbv [LetIn.Let_In] + | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ] + => eapply H; eauto with nocore + end + | solve [ eauto ] + | solve [ eapply expr.wf_interp_Proper; eauto ] ]. + all: eapply interp_to_expr_reify_and_let_binds_base_cps with (k1:=Base) (k2:=(fun x => x)); eauto; wf_safe_t. } + Qed. + + Lemma Interp_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : defaults.Interp (LetBindReturn e) == defaults.Interp e. + Proof. + apply interp_let_bind_return with (G:=nil); cbn [List.In]; eauto; tauto. + Qed. + End reify. + End UnderLets. + + Hint Resolve UnderLets.Wf_LetBindReturn : wf. + Hint Rewrite @UnderLets.Interp_LetBindReturn : interp. +End Compilers. diff --git a/src/Experiments/NewPipeline/UnderLetsWf.v b/src/Experiments/NewPipeline/UnderLetsWf.v deleted file mode 100644 index 7d0e1aa6b..000000000 --- a/src/Experiments/NewPipeline/UnderLetsWf.v +++ /dev/null @@ -1,459 +0,0 @@ -Require Import Coq.Lists.List. -Require Import Coq.Classes.Morphisms. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLets. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.SpecializeAllWays. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Option. -Import ListNotations. Local Open Scope list_scope. - -Import EqNotations. -Module Compilers. - Import Language.Compilers. - Import LanguageInversion.Compilers. - Import LanguageWf.Compilers. - Import UnderLets.Compilers. - Import ident.Notations. - Import expr.Notations. - Import invert_expr. - - Module SubstVarLike. - Section with_ident. - Context {base_type : Type}. - Local Notation type := (type.type base_type). - Context {ident : type -> Type}. - Local Notation expr := (@expr.expr base_type ident). - Section with_var. - Context {var1 var2 : type -> Type}. - Local Notation expr1 := (@expr.expr base_type ident var1). - Local Notation expr2 := (@expr.expr base_type ident var2). - Section with_var_like. - Context (is_var_like1 : forall t, @expr var1 t -> bool) - (is_var_like2 : forall t, @expr var2 t -> bool). - Local Notation subst_var_like1 := (@SubstVarLike.subst_var_like base_type ident var1 is_var_like1). - Local Notation subst_var_like2 := (@SubstVarLike.subst_var_like base_type ident var2 is_var_like2). - Definition is_var_like_wfT := forall G t e1 e2, expr.wf G (t:=t) e1 e2 -> is_var_like1 t e1 = is_var_like2 t e2. - Context (is_var_like_good : is_var_like_wfT). - - Lemma wf_subst_var_like G1 G2 t e1 e2 - (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) - : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (subst_var_like1 e1) (subst_var_like2 e2). - Proof. - cbv [is_var_like_wfT] in *. - intro Hwf; revert dependent G2; induction Hwf; - cbn [SubstVarLike.subst_var_like]; - repeat first [ match goal with - | [ H : is_var_like1 _ ?x = _, H' : is_var_like2 _ ?y = _ |- _ ] - => assert (is_var_like1 _ x = is_var_like2 _ y) by eauto; congruence - end - | progress wf_safe_t - | progress break_innermost_match - | solve [ wf_t ] ]. - Qed. - End with_var_like. - - Section with_ident_like. - Context (ident_is_good : forall t, ident t -> bool). - - Lemma wfT_is_recursively_var_or_ident - : is_var_like_wfT (fun t => SubstVarLike.is_recursively_var_or_ident ident_is_good) - (fun t => SubstVarLike.is_recursively_var_or_ident ident_is_good). - Proof. - intros G t e1 e2 Hwf; induction Hwf; cbn [SubstVarLike.is_recursively_var_or_ident]; - congruence. - Qed. - End with_ident_like. - - Lemma wfT_is_var - : is_var_like_wfT (fun _ e => match invert_Var e with Some _ => true | None => false end) - (fun _ e => match invert_Var e with Some _ => true | None => false end). - Proof. intros G t e1 e2 Hwf; destruct Hwf; cbn [invert_Var]; reflexivity. Qed. - End with_var. - - Local Notation SubstVarLike := (@SubstVarLike.SubstVarLike base_type ident). - Local Notation SubstVar := (@SubstVarLike.SubstVar base_type ident). - Local Notation SubstVarOrIdent := (@SubstVarLike.SubstVarOrIdent base_type ident). - - Lemma Wf_SubstVarLike (is_var_like : forall var t, @expr var t -> bool) - (is_var_like_good : forall var1 var2, is_var_like_wfT (is_var_like var1) (is_var_like var2)) - {t} (e : expr.Expr t) - : expr.Wf e -> expr.Wf (SubstVarLike is_var_like e). - Proof. - intros Hwf var1 var2; eapply wf_subst_var_like; eauto with nocore; cbn [In]; tauto. - Qed. - - Lemma Wf_SubstVar {t} (e : expr.Expr t) - : expr.Wf e -> expr.Wf (SubstVar e). - Proof. - intros Hwf var1 var2; eapply wf_subst_var_like; eauto using wfT_is_var with nocore; cbn [In]; tauto. - Qed. - - Lemma Wf_SubstVarOrIdent (should_subst_ident : forall t, ident t -> bool) - {t} (e : expr.Expr t) - : expr.Wf e -> expr.Wf (SubstVarOrIdent should_subst_ident e). - Proof. - intros Hwf var1 var2; eapply wf_subst_var_like; eauto using wfT_is_recursively_var_or_ident with nocore; cbn [In]; tauto. - Qed. - - Section interp. - Context {base_interp : base_type -> Type} - {interp_ident : forall t, ident t -> type.interp base_interp t} - {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. - Section with_is_var_like. - Context (is_var_like : forall t, @expr (type.interp base_interp) t -> bool). - - Lemma interp_subst_var_like_gen G t (e1 e2 : expr t) - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) - (Hwf : expr.wf G e1 e2) - : expr.interp interp_ident (SubstVarLike.subst_var_like is_var_like e1) == expr.interp interp_ident e2. - Proof. - induction Hwf; cbn [SubstVarLike.subst_var_like]; cbv [Proper respectful] in *; - interp_safe_t; break_innermost_match; interp_safe_t. - Qed. - - Lemma interp_subst_var_like_gen_nil t (e1 e2 : expr t) - (Hwf : expr.wf nil e1 e2) - : expr.interp interp_ident (SubstVarLike.subst_var_like is_var_like e1) == expr.interp interp_ident e2. - Proof. apply interp_subst_var_like_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. - End with_is_var_like. - - Lemma Interp_SubstVarLike (is_var_like : forall var t, @expr var t -> bool) - {t} (e : expr.Expr t) (Hwf : expr.Wf e) - : expr.Interp interp_ident (SubstVarLike is_var_like e) == expr.Interp interp_ident e. - Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. - - Lemma Interp_SubstVar {t} (e : expr.Expr t) (Hwf : expr.Wf e) - : expr.Interp interp_ident (SubstVar e) == expr.Interp interp_ident e. - Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. - - Lemma Interp_SubstVarOrIdent (should_subst_ident : forall t, ident t -> bool) - {t} (e : expr.Expr t) (Hwf : expr.Wf e) - : expr.Interp interp_ident (SubstVarOrIdent should_subst_ident e) == expr.Interp interp_ident e. - Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. - End interp. - End with_ident. - - Lemma Wf_SubstVarFstSndPairOpp {t} (e : expr.Expr t) - : expr.Wf e -> expr.Wf (SubstVarLike.SubstVarFstSndPairOpp e). - Proof. apply Wf_SubstVarOrIdent. Qed. - - Lemma Interp_SubstVarFstSndPairOpp {t} (e : expr.Expr t) (Hwf : expr.Wf e) - : defaults.Interp (SubstVarLike.SubstVarFstSndPairOpp e) == defaults.Interp e. - Proof. apply Interp_SubstVarOrIdent, Hwf. Qed. - End SubstVarLike. - - Module UnderLets. - Import UnderLets.Compilers.UnderLets. - Section with_ident. - Context {base_type : Type}. - Local Notation type := (type.type base_type). - Context {ident : type -> Type}. - Local Notation expr := (@expr.expr base_type ident). - Local Notation UnderLets := (@UnderLets base_type ident). - - Section with_var. - Context {var1 var2 : type -> Type}. - - Inductive wf {T1 T2} {P : list { t : type & var1 t * var2 t }%type -> T1 -> T2 -> Prop} - : list { t : type & var1 t * var2 t }%type -> @UnderLets var1 T1 -> @UnderLets var2 T2 -> Prop := - | Wf_Base G e1 e2 : P G e1 e2 -> wf G (Base e1) (Base e2) - | Wf_UnderLet G A x1 x2 f1 f2 - : expr.wf G x1 x2 - -> (forall v1 v2, wf (existT _ A (v1, v2) :: G) (f1 v1) (f2 v2)) - -> wf G (UnderLet x1 f1) (UnderLet x2 f2). - Global Arguments wf {T1 T2} P _ _ _. - - Lemma wf_to_expr {t} (x : @UnderLets var1 (@expr var1 t)) (y : @UnderLets var2 (@expr var2 t)) - G - : wf (fun G => expr.wf G) G x y -> expr.wf G (to_expr x) (to_expr y). - Proof. - intro Hwf; induction Hwf; cbn [to_expr]; [ assumption | constructor; auto ]. - Qed. - End with_var. - End with_ident. - - Section reify. - Local Notation type := (type.type base.type). - Local Notation expr := (@expr.expr base.type ident). - Local Notation UnderLets := (@UnderLets.UnderLets base.type ident). - - Section with_var. - Context {var1 var2 : type -> Type}. - Local Notation expr1 := (@expr.expr base.type ident var1). - Local Notation expr2 := (@expr.expr base.type ident var2). - Local Notation UnderLets1 := (@UnderLets.UnderLets base.type ident var1). - Local Notation UnderLets2 := (@UnderLets.UnderLets base.type ident var2). - - Local Ltac wf_reify_and_let_binds_base_cps_t Hk := - repeat first [ lazymatch goal with - | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e1 = Some _, H'' : reflect_list ?e2 = None |- _ ] - => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence - | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ] - => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence - | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H - end - | progress subst - | progress destruct_head' False - | progress expr.inversion_wf_constr - | progress expr.inversion_expr - | progress expr.invert_subst - | progress destruct_head'_sig - | progress destruct_head'_ex - | progress destruct_head'_and - | progress type.inversion_type - | progress base.type.inversion_type - | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind combine list_rect length] in * - | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in * - | rewrite base.try_make_transport_cps_correct in * - | progress type_beq_to_eq - | discriminate - | congruence - | apply Hk - | exists nil; reflexivity - | eexists (cons _ nil); reflexivity - | rewrite app_assoc; eexists; reflexivity - | progress wf_safe_t - | match goal with - | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H - end - | progress inversion_option - | progress break_innermost_match_hyps - | progress expr.inversion_wf_one_constr - | progress expr.invert_match_step - | match goal with |- wf _ _ _ _ => constructor end - | match goal with - | [ H : context[wf _ _ _ _] |- wf _ _ _ _ ] => apply H; eauto with nocore - end - | progress wf_unsafe_t_step - | match goal with - | [ H : context[match Compilers.reify_list ?ls with _ => _ end] |- _ ] - => is_var ls; destruct ls; rewrite ?expr.reify_list_cons, ?expr.reify_list_nil in H - | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H - | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ] - => pose proof (fun x y pf => H x y (or_introl pf)); - pose proof (fun x y pf => H x y (or_intror pf)); - clear H - end ]. - - Lemma wf_reify_and_let_binds_base_cps {t : base.type} {T1 T2} (e1 : expr1 (type.base t)) (e2 : expr2 (type.base t)) - (k1 : expr1 (type.base t) -> UnderLets1 T1) (k2 : expr2 (type.base t) -> UnderLets2 T2) - (P : _ -> _ -> _ -> Prop) G - (Hwf : expr.wf G e1 e2) - (Hk : forall G' e1 e2, (exists seg, G' = seg ++ G) -> expr.wf G' e1 e2 -> wf P G' (k1 e1) (k2 e2)) - : wf P G (reify_and_let_binds_base_cps e1 T1 k1) (reify_and_let_binds_base_cps e2 T2 k2). - Proof. - revert dependent G; induction t; cbn [reify_and_let_binds_base_cps]; intros; - try (cbv [SubstVarLike.is_var_fst_snd_pair_opp] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption); - break_innermost_match; wf_reify_and_let_binds_base_cps_t Hk. - all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. - all: revert dependent k1; revert dependent k2. - all: lazymatch goal with - | [ H : length ?l1 = length ?l2 |- _ ] - => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros - end; - wf_reify_and_let_binds_base_cps_t Hk. - Qed. - - Lemma wf_let_bind_return {t} (e1 : expr1 t) (e2 : expr2 t) - G - (Hwf : expr.wf G e1 e2) - : expr.wf G (let_bind_return e1) (let_bind_return e2). - Proof. - revert dependent G; induction t; intros; cbn [let_bind_return]; cbv [invert_Abs]; - wf_safe_t; - expr.invert_match; expr.inversion_wf; try solve [ wf_t ]. - { apply wf_to_expr. - pose (P := fun t => { e1e2 : expr1 t * expr2 t | expr.wf G (fst e1e2) (snd e1e2) }). - pose ((exist _ (e1, e2) Hwf) : P _) as pkg. - change e1 with (fst (proj1_sig pkg)). - change e2 with (snd (proj1_sig pkg)). - clearbody pkg; clear Hwf e1 e2. - type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ]. - cbn [fst snd proj1_sig proj2_sig] in *. - repeat match goal with - | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ] - => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity) - | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] - => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity) - | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] - => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity) - end. - assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity). - revert pf. - rewrite H'; clear H'. - induction Hwf; break_innermost_match; break_innermost_match_hyps; - repeat first [ progress intros - | progress type.inversion_type - | progress base.type.inversion_type - | progress wf_safe_t - | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal] in * - | match goal with - | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) - | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl) - | [ |- wf _ _ _ _ ] => constructor - end - | solve [ eauto ] - | apply wf_reify_and_let_binds_base_cps ]. } - Qed. - End with_var. - - Lemma Wf_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : expr.Wf (LetBindReturn e). - Proof. intros ??; apply wf_let_bind_return, Hwf. Qed. - - Local Ltac interp_to_expr_reify_and_let_binds_base_cps_t Hk := - repeat first [ progress subst - | progress destruct_head' False - | progress destruct_head'_and - | progress destruct_head' iff - | progress specialize_by_assumption - | progress expr.inversion_wf_constr - | progress expr.inversion_expr - | progress expr.invert_subst - | progress destruct_head'_sig - | progress destruct_head'_ex - | progress destruct_head'_and - | progress type.inversion_type - | progress base.type.inversion_type - | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind to_expr expr.interp ident.interp ident.gen_interp type.eqv length list_rect combine In] in * - | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in * - | rewrite base.try_make_transport_cps_correct in * - | progress type_beq_to_eq - | discriminate - | congruence - | apply Hk - | exists nil; reflexivity - | eexists (cons _ nil); reflexivity - | rewrite app_assoc; eexists; reflexivity - | rewrite expr.reify_list_cons - | rewrite expr.reify_list_nil - | progress interp_safe_t - | match goal with - | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H - | [ H : forall t v1 v2, In _ _ -> _ == _, H' : In _ _ |- _ ] => apply H in H' - end - | progress inversion_option - | progress break_innermost_match_hyps - | progress expr.inversion_wf_one_constr - | progress expr.invert_match_step - | match goal with - | [ |- ?R (expr.interp _ ?e1) (expr.interp _ ?e2) ] - => solve [ eapply (@expr.wf_interp_Proper _ _ e1 e2); eauto ] - | [ H : context[reflect_list (reify_list _)] |- _ ] => rewrite expr.reflect_reify_list in H - | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ] - => pose proof (fun x y pf => H x y (or_introl pf)); - pose proof (fun x y pf => H x y (or_intror pf)); - clear H - end - | progress interp_unsafe_t_step - | match goal with - | [ H : expr.wf _ (reify_list _) ?e |- _ ] - => is_var e; destruct (reflect_list e) eqn:?; expr.invert_subst; - [ rewrite expr.wf_reify_list in H | apply expr.wf_reflect_list in H ] - | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H - | [ H : context[expr.interp _ _ = _] |- expr.interp _ (to_expr _) = ?k2 _ ] - => erewrite H; clear H; - [ match goal with - | [ |- ?k (expr.interp ?ii ?e) = ?k' ?v ] - => has_evar e; - let p := fresh in - set (p := expr.interp ii e); - match v with - | context G[expr.interp ii ?e'] - => unify e e'; let v' := context G[p] in change (k p = k' v') - end; - clearbody p; reflexivity - end - | .. ] - end ]. - - Lemma interp_to_expr_reify_and_let_binds_base_cps {t : base.type} {t' : base.type} (e1 : expr (type.base t)) (e2 : expr (type.base t)) - G - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) - (Hwf : expr.wf G e1 e2) - (k1 : expr (type.base t) -> UnderLets _ (expr (type.base t'))) - (k2 : base.interp t -> base.interp t') - (Hk : forall e1 v, defaults.interp e1 == v -> defaults.interp (to_expr (k1 e1)) == k2 v) - : defaults.interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (defaults.interp e2). - Proof. - revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros; - try (cbv [SubstVarLike.is_var_fst_snd_pair_opp] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption); - break_innermost_match; interp_to_expr_reify_and_let_binds_base_cps_t Hk. - all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. - all: revert dependent k1; revert dependent k2. - all: lazymatch goal with - | [ H : length ?l1 = length ?l2 |- _ ] - => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros - end; - interp_to_expr_reify_and_let_binds_base_cps_t Hk. - Qed. - - Lemma interp_let_bind_return {t} (e1 e2 : expr t) - G - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) - (Hwf : expr.wf G e1 e2) - : defaults.interp (let_bind_return e1) == defaults.interp e2. - Proof. - revert dependent G; induction t; intros; cbn [let_bind_return type.eqv expr.interp] in *; cbv [invert_Abs respectful] in *; - repeat first [ progress wf_safe_t - | progress expr.invert_subst - | progress expr.invert_match - | progress expr.inversion_wf - | progress break_innermost_match_hyps - | progress destruct_head' False - | solve [ wf_t ] - | match goal with - | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] - => eapply (H e0 (e @ $v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ] - | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] - => cbn [expr.interp]; eapply H; [ | solve [ wf_t ] ]; solve [ wf_t ] - end ]; - []. - { pose (P := fun t => { e1e2 : expr t * expr t | expr.wf G (fst e1e2) (snd e1e2) }). - pose ((exist _ (e1, e2) Hwf) : P _) as pkg. - change e1 with (fst (proj1_sig pkg)). - change e2 with (snd (proj1_sig pkg)). - clearbody pkg; clear Hwf e1 e2. - type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ]. - cbn [fst snd proj1_sig proj2_sig] in *. - repeat match goal with - | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ] - => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity) - | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] - => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity) - | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] - => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity) - end. - assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity). - revert pf. - rewrite H'; clear H'. - induction Hwf; break_innermost_match; break_innermost_match_hyps; - repeat first [ progress intros - | progress type.inversion_type - | progress base.type.inversion_type - | progress wf_safe_t - | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal to_expr] in * - | match goal with - | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) - | [ H : forall x (pf : ?a = ?a), _ |- _ ] => specialize (fun x => H x eq_refl) - | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl) - | [ H : forall x y z (pf : ?a = ?a), _ |- _ ] => specialize (fun x y z => H x y z eq_refl) - | [ |- context[(expr_let x := _ in _)%expr] ] => progress cbn [expr.interp]; cbv [LetIn.Let_In] - | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ] - => eapply H; eauto with nocore - end - | solve [ eauto ] - | solve [ eapply expr.wf_interp_Proper; eauto ] ]. - all: eapply interp_to_expr_reify_and_let_binds_base_cps with (k1:=Base) (k2:=(fun x => x)); eauto; wf_safe_t. } - Qed. - - Lemma Interp_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : defaults.Interp (LetBindReturn e) == defaults.Interp e. - Proof. - apply interp_let_bind_return with (G:=nil); cbn [List.In]; eauto; tauto. - Qed. - End reify. - End UnderLets. -End Compilers. -- cgit v1.2.3