From 385166b49879f93824e7b4489ac8fa0fbb8b0804 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 6 Aug 2018 15:35:18 -0400 Subject: Finish relax interp proofs After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 17m50.60s | Total | 17m59.23s || -0m08.63s | -0.80% -------------------------------------------------------------------------------------------------------------------- 0m02.92s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m07.06s || -0m04.13s | -58.64% 5m55.40s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m56.43s || -0m01.03s | -0.28% 0m38.25s | Experiments/NewPipeline/AbstractInterpretationWf | 0m40.00s || -0m01.75s | -4.37% 0m23.76s | p384_32.c | 0m25.24s || -0m01.47s | -5.86% 4m32.74s | Experiments/NewPipeline/Toplevel1 | 4m31.77s || +0m00.97s | +0.35% 1m36.34s | Experiments/NewPipeline/Toplevel2 | 1m35.98s || +0m00.36s | +0.37% 0m38.76s | p521_32.c | 0m38.53s || +0m00.22s | +0.59% 0m37.08s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.15s || -0m00.07s | -0.18% 0m35.15s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m34.38s || +0m00.76s | +2.23% 0m32.29s | p521_64.c | 0m32.14s || +0m00.14s | +0.46% 0m20.50s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m20.86s || -0m00.35s | -1.72% 0m18.69s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m18.91s || -0m00.21s | -1.16% 0m13.51s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m13.95s || -0m00.43s | -3.15% 0m12.46s | Experiments/NewPipeline/CStringification | 0m12.60s || -0m00.13s | -1.11% 0m10.36s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.52s || -0m00.16s | -1.52% 0m08.55s | p384_64.c | 0m08.77s || -0m00.21s | -2.50% 0m08.52s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.83s || -0m00.31s | -3.51% 0m05.38s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.43s || -0m00.04s | -0.92% 0m05.34s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.42s || -0m00.08s | -1.47% 0m04.01s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m03.85s || +0m00.15s | +4.15% 0m03.88s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.08s || -0m00.20s | -4.90% 0m03.77s | secp256k1_32.c | 0m03.83s || -0m00.06s | -1.56% 0m03.76s | p256_32.c | 0m03.80s || -0m00.04s | -1.05% 0m03.18s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.25s || -0m00.06s | -2.15% 0m02.10s | p224_32.c | 0m02.14s || -0m00.04s | -1.86% 0m02.03s | curve25519_32.c | 0m02.06s || -0m00.03s | -1.45% 0m01.60s | p256_64.c | 0m01.67s || -0m00.06s | -4.19% 0m01.59s | p224_64.c | 0m01.58s || +0m00.01s | +0.63% 0m01.53s | secp256k1_64.c | 0m01.68s || -0m00.14s | -8.92% 0m01.42s | Experiments/NewPipeline/CLI | 0m01.38s || +0m00.04s | +2.89% 0m01.38s | curve25519_64.c | 0m01.39s || -0m00.01s | -0.71% 0m01.16s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.21s || -0m00.05s | -4.13% 0m01.16s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.25s || -0m00.09s | -7.20% 0m01.02s | Experiments/NewPipeline/CompilersTestCases | 0m01.03s || -0m00.01s | -0.97% 0m01.01s | Experiments/NewPipeline/AbstractInterpretation | 0m01.07s || -0m00.06s | -5.60% --- .../NewPipeline/AbstractInterpretation.v | 72 +++-- .../NewPipeline/AbstractInterpretationProofs.v | 341 +++++++++++++++------ .../NewPipeline/AbstractInterpretationWf.v | 17 - src/Experiments/NewPipeline/Toplevel1.v | 17 +- 4 files changed, 293 insertions(+), 154 deletions(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v index 9d07eb1c4..4d9673eb1 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretation.v +++ b/src/Experiments/NewPipeline/AbstractInterpretation.v @@ -987,24 +987,40 @@ Module Compilers. := @partial.ident.extract abstract_domain' abstract_interp_ident t (e _) bound. End specialized. End partial. - Import defaults. + Module Import CheckCasts. + Fixpoint get_casts {t} (e : expr t) : list { t : _ & ident t } + := match e with + | expr.Ident t idc => if partial.is_annotation _ idc then [existT _ t idc] else nil + | expr.Var t v => v + | expr.Abs s d f => @get_casts _ (f nil) + | expr.App s d f x => @get_casts _ f ++ @get_casts _ x + | expr.LetIn A B x f => @get_casts _ x ++ @get_casts _ (f nil) + end%list. + + Definition GetUnsupportedCasts {t} (e : Expr t) : list { t : _ & ident t } + := get_casts (e _). + End CheckCasts. + Module RelaxZRange. Module ident. Section relax. Context (relax_zrange : zrange -> option zrange). - Definition relax {t} (idc : ident t) : option (ident t) - := match idc in ident.ident t return option (ident t) with + Let always_relax_zrange : zrange -> zrange + := fun range => match relax_zrange range with + | Some r => r + | None => range + end. + + Definition relax {t} (idc : ident t) : ident t + := match idc in ident.ident t return ident t with | ident.Z_cast range - => (r <- relax_zrange range; - Some (ident.Z_cast r)) + => ident.Z_cast (always_relax_zrange range) | ident.Z_cast2 (r1, r2) - => (r1 <- relax_zrange r1; - r2 <- relax_zrange r2; - Some (ident.Z_cast2 (r1, r2))) - | _ => None + => ident.Z_cast2 (always_relax_zrange r1, always_relax_zrange r2) + | idc => idc end%option. End relax. End ident. @@ -1018,24 +1034,12 @@ Module Compilers. Fixpoint relax {t} (e : @expr var t) : @expr var t := match e with | expr.Var _ _ as e - | expr.Ident _ _ as e => e + | expr.Ident t idc + => expr.Ident (ident.relax relax_zrange idc) | expr.Abs s d f => expr.Abs (fun v => @relax d (f v)) | expr.LetIn tx tC ex eC => expr.LetIn (@relax tx ex) (fun v => @relax tC (eC v)) - | expr.App s d f x - => let f' := @relax _ f in - let x' := @relax _ x in - match s, d return expr (s -> d) -> expr s -> expr d with - | type.base base.type.Z, type.base base.type.Z - | type.base (base.type.Z * base.type.Z)%etype, type.base (base.type.Z * base.type.Z)%etype - => fun f x - => match option_map (ident.relax relax_zrange) - (invert_Ident f) with - | Some (Some idc) => expr.App (expr.Ident idc) x - | _ => expr.App f x - end - | _, _ => expr.App - end f' x' + | expr.App s d f x => expr.App (@relax _ f) (@relax _ x) end. End with_var. @@ -1055,24 +1059,30 @@ Module Compilers. := partial.EtaExpandWithListInfoFromBound (GeneralizeVar.GeneralizeVar (e _)) bound. Definition CheckPartialEvaluateWithBounds + {A} (relax_zrange : zrange -> option zrange) {t} (E : Expr t) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (b_out : ZRange.type.base.option.interp (type.final_codomain t)) - : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) + : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + A) := let b_computed := partial.Extract E b_in in if ZRange.type.base.option.is_tighter_than b_computed b_out then @inl (Expr t) _ (RelaxZRange.expr.Relax relax_zrange E) - else @inr _ (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) (b_computed, E). + else inr (@inl (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) _ (b_computed, E)). Definition CheckedPartialEvaluateWithBounds (relax_zrange : zrange -> option zrange) {t} (E : Expr t) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (b_out : ZRange.type.base.option.interp (type.final_codomain t)) - : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) - := let E := PartialEvaluateWithBounds E b_in in - dlet_nd e := GeneralizeVar.ToFlat E in - let E := GeneralizeVar.FromFlat e in - CheckPartialEvaluateWithBounds relax_zrange E b_in b_out. + : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + list { t : _ & ident t }) + := dlet_nd e := GeneralizeVar.ToFlat E in + let E := GeneralizeVar.FromFlat e in + match CheckCasts.GetUnsupportedCasts E with + | nil => (let E := PartialEvaluateWithBounds E b_in in + dlet_nd e := GeneralizeVar.ToFlat E in + let E := GeneralizeVar.FromFlat e in + CheckPartialEvaluateWithBounds relax_zrange E b_in b_out) + | unsupported_casts => inr (inr unsupported_casts) + end. End Compilers. diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v index b50064e9c..66ed19540 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v @@ -18,6 +18,7 @@ Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Experiments.NewPipeline.Language. Require Import Crypto.Experiments.NewPipeline.LanguageInversion. Require Import Crypto.Experiments.NewPipeline.LanguageWf. @@ -45,19 +46,147 @@ Module Compilers. Let type_base (x : base_type) : type := type.base x. Local Coercion type_base : base_type >-> type. Context {ident : type -> Type}. - Local Notation expr := (@expr base_type ident). Local Notation Expr := (@expr.Expr base_type ident). - Local Notation UnderLets := (@UnderLets base_type ident). - Context (abstract_domain' : base_type -> Type) + Context (abstract_domain' base_interp : base_type -> Type) + (abstraction_relation' : forall t, abstract_domain' t -> base_interp t -> Prop) (bottom' : forall A, abstract_domain' A) + (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v) (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t) - (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop) - {abstract_interp_ident_Proper : forall t, Proper (eq ==> abstract_domain'_R t) (abstract_interp_ident t)} - {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}. + (interp_ident : forall t, ident t -> type.interp base_interp t) + (interp_ident_Proper : forall t (idc : ident t), type.related_hetero abstraction_relation' (abstract_interp_ident t idc) (interp_ident t idc)). Local Notation abstract_domain := (@abstract_domain base_type abstract_domain'). + Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop + := type.related_hetero (@abstraction_relation'). Local Notation bottom := (@bottom base_type abstract_domain' (@bottom')). Local Notation bottom_for_each_lhs_of_arrow := (@bottom_for_each_lhs_of_arrow base_type abstract_domain' (@bottom')). - Local Notation abstract_domain_R := (@abstract_domain_R base_type abstract_domain' abstract_domain'_R). + Local Notation var := (type.interp base_interp). + Local Notation expr := (@expr base_type ident var). + Local Notation UnderLets := (@UnderLets base_type ident var). + Local Notation value := (@value base_type ident var abstract_domain'). + Local Notation value_with_lets := (@value_with_lets base_type ident var abstract_domain'). + Local Notation state_of_value := (@state_of_value base_type ident var abstract_domain'). + Context (annotate : forall (is_let_bound : bool) t, abstract_domain' t -> expr t -> UnderLets (expr t)). + (* + Local Notation reify1 := (@reify base_type ident var1 abstract_domain' annotate1 bottom'). + Local Notation reify2 := (@reify base_type ident var2 abstract_domain' annotate2 bottom'). + Local Notation reflect1 := (@reflect base_type ident var1 abstract_domain' annotate1 bottom'). + Local Notation reflect2 := (@reflect base_type ident var2 abstract_domain' annotate2 bottom'). + Local Notation interp1 := (@interp base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). + Local Notation interp2 := (@interp base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). + Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). + Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). + Local Notation eval'1 := (@eval' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). + Local Notation eval'2 := (@eval' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). + Local Notation eta_expand_with_bound'1 := (@eta_expand_with_bound' base_type ident var1 abstract_domain' annotate1 bottom'). + Local Notation eta_expand_with_bound'2 := (@eta_expand_with_bound' base_type ident var2 abstract_domain' annotate2 bottom'). +*) +(* + + Fixpoint value (t : type) + := (abstract_domain t + * match t return Type (* COQBUG(https://github.com/coq/coq/issues/7727) *) with + | type.base t + => @expr var t + | type.arrow s d + => value s -> UnderLets (value d) + end)%type. + + Definition value_with_lets (t : type) + := UnderLets (value t). + + + Fixpoint bottom {t} : abstract_domain t + := match t with + | type.base t => bottom' t + | type.arrow s d => fun _ => @bottom d + end. + + Fixpoint bottom_for_each_lhs_of_arrow {t} : type.for_each_lhs_of_arrow abstract_domain t + := match t return type.for_each_lhs_of_arrow abstract_domain t with + | type.base t => tt + | type.arrow s d => (bottom, @bottom_for_each_lhs_of_arrow d) + end. + + Definition state_of_value {t} : value t -> abstract_domain t + := match t return value t -> abstract_domain t with + | type.base t => fun '(st, v) => st + | type.arrow s d => fun '(st, v) => st + end. + + Fixpoint reify (is_let_bound : bool) {t} : value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t) + := match t return value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t) with + | type.base t + => fun '(st, v) 'tt + => annotate is_let_bound t st v + | type.arrow s d + => fun '(f_st, f_e) '(sv, dv) + => Base + (λ x , (UnderLets.to_expr + (fx <-- f_e (@reflect _ (expr.Var x) sv); + @reify false _ fx dv))) + end%core%expr + with reflect {t} : @expr var t -> abstract_domain t -> value t + := match t return @expr var t -> abstract_domain t -> value t with + | type.base t + => fun e st => (st, e) + | type.arrow s d + => fun e absf + => (absf, + (fun v + => let stv := state_of_value v in + (rv <-- (@reify false s v bottom_for_each_lhs_of_arrow); + Base (@reflect d (e @ rv) (absf stv))%expr))) + end%under_lets. + + (* N.B. Because the [App] case only looks at the second argument + of arrow-values, we are free to set the state of [Abs] + nodes to [bottom], because for any [Abs] nodes which are + actually applied (here and in places where we don't + rewrite), we just drop it. *) + Fixpoint interp {t} (e : @expr value_with_lets t) : value_with_lets t + := match e in expr.expr t return value_with_lets t with + | expr.Ident t idc => interp_ident _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*) + | expr.Var t v => v + | expr.Abs s d f => Base (bottom, fun x => @interp d (f (Base x))) + | expr.App s d f x + => (x' <-- @interp s x; + f' <-- @interp (s -> d)%etype f; + snd f' x') + | expr.LetIn (type.arrow _ _) B x f + => (x' <-- @interp _ x; + @interp _ (f (Base x'))) + | expr.LetIn (type.base A) B x f + => (x' <-- @interp _ x; + x'' <-- reify true (* this forces a let-binder here *) x' tt; + @interp _ (f (Base (reflect x'' (state_of_value x'))))) + end%under_lets. + + Definition eval_with_bound' {t} (e : @expr value_with_lets t) + (st : type.for_each_lhs_of_arrow abstract_domain t) + : expr t + := UnderLets.to_expr (e' <-- interp e; reify false e' st). + + Definition eval' {t} (e : @expr value_with_lets t) : expr t + := eval_with_bound' e bottom_for_each_lhs_of_arrow. + + Definition eta_expand_with_bound' {t} (e : @expr var t) + (st : type.for_each_lhs_of_arrow abstract_domain t) + : expr t + := UnderLets.to_expr (reify false (reflect e bottom) st). + + Section extract. + Context (ident_extract : forall t, ident t -> abstract_domain t). + + Definition extract' {t} (e : @expr abstract_domain t) : abstract_domain t + := expr.interp (@ident_extract) e. + + Definition extract_gen {t} (e : @expr abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t) + : abstract_domain' (type.final_codomain t) + := type.app_curried (extract' e) bound. + End extract. + End with_var. + + Section extract. Context (ident_extract : forall t, ident t -> abstract_domain t) @@ -82,8 +211,9 @@ Module Compilers. eapply extract'_Proper; eassumption. Qed. End extract. +*) End with_type. - +(* Module ident. Import defaults. Local Notation UnderLets := (@UnderLets base.type ident). @@ -118,7 +248,7 @@ Module Compilers. End extract. End with_type. End ident. - +*) Section specialized. Import defaults. Local Notation abstract_domain' := ZRange.type.base.option.interp (only parsing). @@ -201,58 +331,91 @@ Module Compilers. End partial. Import defaults. + Module Import CheckCasts. + Module ident. + Lemma interp_eqv_without_casts t idc + cast_outside_of_range1 cast_outside_of_range2 + (Hc : partial.is_annotation t idc = false) + : ident.gen_interp cast_outside_of_range1 idc + == ident.gen_interp cast_outside_of_range2 idc. + Proof. + generalize (@ident.gen_interp_Proper cast_outside_of_range1 t idc idc eq_refl); + destruct idc; try exact id; cbn in Hc; discriminate. + Qed. + End ident. + + Lemma interp_eqv_without_casts + cast_outside_of_range1 cast_outside_of_range2 + G {t} e1 e2 e3 + (HG : forall t v1 v2 v3, List.In (existT _ t (v1, v2, v3)) G -> v2 == v3) + (Hwf : expr.wf3 G e1 e2 e3) + (Hc : @CheckCasts.get_casts t e1 = nil) + : expr.interp (@ident.gen_interp cast_outside_of_range1) e2 + == expr.interp (@ident.gen_interp cast_outside_of_range2) e3. + Proof. + induction Hwf; + repeat first [ progress cbn [CheckCasts.get_casts] in * + | discriminate + | match goal with + | [ H : (_ ++ _)%list = nil |- _ ] => apply List.app_eq_nil in H + end + | progress destruct_head'_and + | progress break_innermost_match_hyps + | progress interp_safe_t + | solve [ eauto using ident.interp_eqv_without_casts ] ]. + Qed. + + Lemma Interp_WithoutUnsupportedCasts {t} (e : Expr t) + (Hc : CheckCasts.GetUnsupportedCasts e = nil) + (Hwf : expr.Wf3 e) + cast_outside_of_range1 cast_outside_of_range2 + : expr.Interp (@ident.gen_interp cast_outside_of_range1) e + == expr.Interp (@ident.gen_interp cast_outside_of_range2) e. + Proof. eapply interp_eqv_without_casts with (G:=nil); wf_safe_t. Qed. + End CheckCasts. + Module RelaxZRange. + Definition relaxed_cast_outside_of_range + (relax_zrange : zrange -> option zrange) + (cast_outside_of_range : zrange -> Z -> Z) + : zrange -> Z -> Z + := fun r v + => match relax_zrange r with + | Some r' => ident.cast cast_outside_of_range r' v + | None => cast_outside_of_range r v + end. + Module ident. Section relax. Context (relax_zrange : zrange -> option zrange) + (cast_outside_of_range : zrange -> Z -> Z) (Hrelax : forall r r' z, is_tighter_than_bool z r = true -> relax_zrange r = Some r' -> is_tighter_than_bool z r' = true). - Lemma interp_relax {t} (idc idc' : ident t) - (Hidc : @RelaxZRange.ident.relax relax_zrange t idc = Some idc') - v - (Hinterp : forall cast_outside_of_range, type.app_curried (ident.gen_interp cast_outside_of_range idc) v = type.app_curried (ident.interp idc) v) - : forall cast_outside_of_range, type.app_curried (ident.gen_interp cast_outside_of_range idc') v = type.app_curried (ident.interp idc) v. + Local Notation relaxed_cast_outside_of_range := (@relaxed_cast_outside_of_range relax_zrange cast_outside_of_range). + + Lemma interp_relax {t} (idc : ident t) + : ident.gen_interp cast_outside_of_range (@RelaxZRange.ident.relax relax_zrange t idc) + == ident.gen_interp relaxed_cast_outside_of_range idc. Proof. - intro cast_outside_of_range. - pose proof (Hinterp (fun _ => id)). - pose proof (fun myrange => Hinterp (fun _ => cast_outside_of_range myrange)). - destruct idc; cbv [RelaxZRange.ident.relax Option.bind] in *; inversion_option; break_innermost_match_hyps; inversion_option; subst; - repeat match goal with - | [ H : relax_zrange _ = Some _ |- _ ] => unique pose proof (fun zl zu pf => Hrelax _ _ (Build_zrange zl zu) pf H) - end; - repeat first [ reflexivity + pose proof (@ident.gen_interp_Proper cast_outside_of_range t idc idc eq_refl) as Hp. + destruct idc; cbn [type.related] in *; repeat (let x := fresh "x" in intro x; specialize (Hp x)); + repeat first [ assumption + | reflexivity | discriminate | congruence - | progress cbv [RelaxZRange.ident.relax Option.bind id ident.cast is_tighter_than_bool] in * - | progress cbn [fst snd] in * | progress subst - | progress inversion_option - | progress inversion_prod + | progress cbv [relaxed_cast_outside_of_range RelaxZRange.ident.relax Option.bind ident.cast respectful is_tighter_than_bool id] in * + | progress cbn [ident.gen_interp type.related type.interp base.interp upper lower] in * | progress destruct_head'_prod - | progress destruct_head'_and - | progress cbn in * - | progress Bool.split_andb - | progress intros + | progress specialize_by (exact eq_refl) + | break_match_step ltac:(fun x => let h := head x in constr_eq h relax_zrange) | match goal with - | [ H : forall x, (_, _) = (_, _) |- _ ] - => pose proof (fun x => f_equal (@fst _ _) (H x)); - pose proof (fun x => f_equal (@snd _ _) (H x)); - clear H - | [ H : context[andb _ _ = true] |- _ ] => rewrite Bool.andb_true_iff in H || setoid_rewrite Bool.andb_true_iff in H - | [ H : context[Z.leb _ _ = true] |- _ ] => rewrite Z.leb_le in H || setoid_rewrite Z.leb_le in H - | [ H : forall a b, and (Z.le ?x a) (Z.le b ?y) -> _ /\ _, H' : Z.le ?x _, H'' : Z.le _ ?y |- _ ] - => unique pose proof (proj1 (H _ _ (conj H' H''))); - unique pose proof (proj2 (H _ _ (conj H' H''))) + | [ H : relax_zrange ?r = Some ?r' |- context[Z.leb (lower ?r) ?v] ] + => pose proof (fun pf => Hrelax _ _ (Build_zrange v v) pf H); clear H end - | progress rewrite ?Bool.andb_false_iff in * - | progress destruct_head'_or - | progress break_innermost_match_hyps - | progress break_innermost_match - | progress Z.ltb_to_lt - | apply (f_equal2 (@pair _ _)) - | lia ]. + | break_innermost_match_step ]. Qed. End relax. End ident. @@ -262,63 +425,27 @@ Module Compilers. Context (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). - Lemma interp_relax {t} (e : expr t) - v - (Hinterp : forall cast_outside_of_range, type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) e) v - = type.app_curried (defaults.interp e) v) - : forall cast_outside_of_range, type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (RelaxZRange.expr.relax relax_zrange e)) v - = type.app_curried (defaults.interp e) v. + -> is_tighter_than_bool z r' = true) + (cast_outside_of_range : zrange -> Z -> Z). + + Local Notation relaxed_cast_outside_of_range := (@relaxed_cast_outside_of_range relax_zrange cast_outside_of_range). + + Lemma interp_relax G {t} (e1 e2 : expr t) + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) + (Hwf : expr.wf G e1 e2) + : expr.interp (@ident.gen_interp cast_outside_of_range) (RelaxZRange.expr.relax relax_zrange e1) + == expr.interp (@ident.gen_interp relaxed_cast_outside_of_range) e2. Proof. - intro cast_outside_of_range; rewrite <- (Hinterp cast_outside_of_range); pose proof (Hinterp cast_outside_of_range). - induction e; cbn -[RelaxZRange.ident.relax] in *; interp_safe_t; cbv [option_map] in *; + induction Hwf; cbn -[RelaxZRange.ident.relax] in *; interp_safe_t; cbv [option_map] in *; break_innermost_match; cbn -[RelaxZRange.ident.relax] in *; interp_safe_t; - eauto using tt. - all: repeat first [ reflexivity - | progress intros - | progress specialize_by_assumption - | progress cbn -[RelaxZRange.ident.relax] in * - | match goal with - | [ H : unit -> ?T |- _ ] => specialize (H tt) - | [ H : forall x : _ * _, _ |- _ ] => specialize (fun a b => H (a, b)) - | [ e : expr (type.base (base.type.type_base base.type.unit)) |- _ ] - => match goal with - | [ |- context[expr.interp ?ii e] ] => destruct (expr.interp ii e) - | [ H : context[expr.interp ?ii e] |- _ ] => destruct (expr.interp ii e) - end - end - | progress cbn [fst snd] in * - | match goal with - | [ H : _ |- _ ] => rewrite H - end ]. - all: specialize_all_ways. - all: repeat first [ reflexivity - | progress intros - | progress specialize_by_assumption - | progress cbn -[RelaxZRange.ident.relax] in * - | match goal with - | [ H : unit -> ?T |- _ ] => specialize (H tt) - | [ H : forall x : _ * _, _ |- _ ] => specialize (fun a b => H (a, b)) - | [ e : expr (type.base (base.type.type_base base.type.unit)) |- _ ] - => match goal with - | [ |- context[expr.interp ?ii e] ] => destruct (expr.interp ii e) - | [ H : context[expr.interp ?ii e] |- _ ] => destruct (expr.interp ii e) - end - end - | progress cbn [fst snd] in * - | match goal with - | [ H : _ |- _ ] => rewrite H - end ]. - Admitted. + eauto using tt, @ident.interp_relax. + Qed. Lemma Interp_Relax {t} (e : Expr t) - (Hwf : expr.Wf3 e) - v - (Hinterp : forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) e) v - = type.app_curried (defaults.Interp e) v) - : forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (RelaxZRange.expr.Relax relax_zrange e)) v - = type.app_curried (defaults.Interp e) v. - Proof. eapply @interp_relax; try assumption. Qed. + (Hwf : Wf e) + : expr.Interp (@ident.gen_interp cast_outside_of_range) (RelaxZRange.expr.Relax relax_zrange e) + == expr.Interp (@ident.gen_interp relaxed_cast_outside_of_range) e. + Proof. apply interp_relax with (G:=nil); wf_safe_t. Qed. End relax. End expr. End RelaxZRange. @@ -336,11 +463,12 @@ Module Compilers. (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 (expr.Interp (@ident.gen_interp cast_outside_of_range) (PartialEvaluateWithBounds E b_in)) arg1 - = type.app_curried (Interp E) arg2. + = type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) E) arg2. Proof. Admitted. Lemma Interp_PartialEvaluateWithBounds_bounded + cast_outside_of_range {t} (E : Expr t) (Hwf : Wf E) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) @@ -348,7 +476,7 @@ Module Compilers. (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 (partial.Extract (PartialEvaluateWithBounds E b_in) b_in) - (type.app_curried (expr.Interp (@ident.interp) (PartialEvaluateWithBounds E b_in)) arg1) + (type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (PartialEvaluateWithBounds E b_in)) arg1) = true. Proof. Admitted. @@ -362,6 +490,7 @@ Module Compilers. (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. + cbv [PartialEvaluateWithListInfoFromBounds]. Admitted. Theorem CheckedPartialEvaluateWithBounds_Correct @@ -385,6 +514,14 @@ Module Compilers. Proof. cbv [CheckedPartialEvaluateWithBounds CheckPartialEvaluateWithBounds Let_In] in *; break_innermost_match_hyps; inversion_sum; subst. + let H := lazymatch goal with H : _ = nil |- _ => H end in + pose proof (@Interp_WithoutUnsupportedCasts _ _ H ltac:(solve [ auto with wf ])) as H'; clear H; + assert (forall cast_outside_of_range1 cast_outside_of_range2, + expr.Interp (@ident.gen_interp cast_outside_of_range1) E == expr.Interp (@ident.gen_interp cast_outside_of_range2) E) + by (intros c1 c2; specialize (H' c1 c2); + rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat in H' by eauto with wf typeclass_instances; + assumption). + clear H'. split. { intros arg1 arg2 Harg12 Harg1. assert (arg1_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg1) @@ -398,6 +535,8 @@ Module Compilers. | rewrite RelaxZRange.expr.Interp_Relax; eauto | erewrite !Interp_PartialEvaluateWithBounds | solve [ eauto with wf ] + | apply type.app_curried_Proper + | apply expr.Wf_Interp_Proper_gen | progress intros ]. } { auto with wf. } Qed. diff --git a/src/Experiments/NewPipeline/AbstractInterpretationWf.v b/src/Experiments/NewPipeline/AbstractInterpretationWf.v index 69844c8ef..c0938e7d5 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationWf.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationWf.v @@ -777,23 +777,6 @@ Module Compilers. Proof using Type. clear -Hwf. induction Hwf; wf_safe_t. - cbn [RelaxZRange.expr.relax]; cbv [option_map] in *. - break_innermost_match; - repeat first [ progress wf_safe_t - | progress expr.invert_subst - | progress expr.inversion_wf_constr - | progress destruct_head' False - | progress inversion_option - | progress cbn [invert_Ident invert_Var invert_Abs invert_App invert_LetIn] in * - | match goal with - | [ H : context[RelaxZRange.expr.relax ?r ?x], H' : RelaxZRange.expr.relax ?r ?x = _ |- _ ] - => rewrite H' in H - | [ H : context[match RelaxZRange.expr.relax ?r ?x with _ => _ end] |- _ ] - => remember (RelaxZRange.expr.relax r x) in *; progress expr.invert_match - | [ H : ?x = Some ?a, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H' - end - | progress expr.inversion_wf_one_constr ]. Qed. End with_var2. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index e896e495f..626fb04f1 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -541,6 +541,7 @@ Module Pipeline. | Values_not_provably_distinctZ (descr : string) (lhs rhs : Z) | Values_not_provably_equalZ (descr : string) (lhs rhs : Z) | Values_not_provably_equal_listZ (descr : string) (lhs rhs : list Z) + | Unsupported_casts_in_input {t} (e : @Compilers.defaults.Expr t) (ls : list { t : _ & ident t }) | Stringification_failed {t} (e : @Compilers.defaults.Expr t) (err : string) | Invalid_argument (msg : string). @@ -647,6 +648,10 @@ Module Pipeline. | Values_not_provably_equalZ descr lhs rhs | Values_not_provably_equal_listZ descr lhs rhs => ["Values not provably equal (" ++ descr ++ ") : expected " ++ show true lhs ++ " = " ++ show true rhs] + | Unsupported_casts_in_input t e ls + => ["Unsupported casts in input syntax tree:"] + ++ show_lines false e + ++ ["Unsupported casts: " ++ @show_list _ (fun p v => show p (projT2 v)) false ls] | Stringification_failed t e err => ["Stringification failed on the syntax tree:"] ++ show_lines false e ++ [err] | Invalid_argument msg => ["Invalid argument:" ++ msg]%string @@ -699,11 +704,13 @@ Module Pipeline. end in dlet_nd e := ToFlat E in let E := FromFlat e in - let E := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in - match E with + let E' := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in + match E' with | inl E => Success E - | inr (b, E) + | inr (inl (b, E)) => Error (Computed_bounds_are_not_tight_enough b out_bounds E arg_bounds) + | inr (inr unsupported_casts) + => Error (Unsupported_casts_in_input E unsupported_casts) end. Definition BoundsPipelineToStrings @@ -807,7 +814,7 @@ Module Pipeline. cbv [BoundsPipeline Let_In bounds_goodT] in *; repeat match goal with | [ H : match ?x with _ => _ end = Success _ |- _ ] - => destruct x eqn:?; cbv beta iota in H; [ | destruct_head'_prod; congruence ]; + => destruct x eqn:?; cbv beta iota in H; [ | break_innermost_match_hyps; congruence ]; let H' := fresh in inversion H as [H']; clear H; rename H' into H end. @@ -820,7 +827,7 @@ Module Pipeline. [ destruct H' as [H01 Hwf'] | .. ] end; [ - | match goal with + | lazymatch goal with | [ |- Wf _ ] => idtac | _ => eassumption || reflexivity end.. ]. -- cgit v1.2.3