Commit 29b21eb6 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Try progressing on cmd validation soundness

parent a91b364b
......@@ -498,160 +498,6 @@ Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m: mType, Gamma v = Some m.
(* Fixpoint contained_subexpressions (V: Type) e (expmap: FloverMap.t V) := *)
(* match e with *)
(* | Var _ x => *)
(* True *)
(* | Const x x0 => *)
(* True *)
(* | Unop u e1 => *)
(* contained_subexpressions e1 expmap *)
(* | Binop b e1 e2 => *)
(* contained_subexpressions e1 expmap /\ contained_subexpressions e2 expmap *)
(* | Fma e1 e2 e3 => *)
(* contained_subexpressions e1 expmap /\ contained_subexpressions e2 expmap /\ *)
(* contained_subexpressions e3 expmap *)
(* | Downcast m e1 => *)
(* contained_subexpressions e1 expmap *)
(* end /\ exists af, FloverMap.find e expmap = Some af. *)
(* Fixpoint checked_expressions (A: analysisResult) E Gamma e iexpmap inoise map1 := *)
(* match e with *)
(* | Var _ x => *)
(* True *)
(* | Const x x0 => *)
(* True *)
(* | Unop u e1 => *)
(* checked_expressions A E Gamma e1 iexpmap inoise map1 *)
(* | Binop b e1 e2 => *)
(* checked_expressions A E Gamma e1 iexpmap inoise map1 /\ *)
(* checked_expressions A E Gamma e2 iexpmap inoise map1 *)
(* | Fma e1 e2 e3 => *)
(* checked_expressions A E Gamma e1 iexpmap inoise map1 /\ *)
(* checked_expressions A E Gamma e2 iexpmap inoise map1 /\ *)
(* checked_expressions A E Gamma e3 iexpmap inoise map1 *)
(* | Downcast m e1 => *)
(* checked_expressions A E Gamma e1 iexpmap inoise map1 *)
(* end /\ *)
(* ((exists (af: affine_form Q), FloverMap.find e iexpmap = Some af) -> *)
(* exists af vR aiv aerr, *)
(* FloverMap.find e A = Some (aiv, aerr) /\ *)
(* isSupersetIntv (toIntv af) aiv = true /\ *)
(* FloverMap.find e iexpmap = Some af /\ *)
(* contained_subexpressions e iexpmap /\ *)
(* fresh inoise af /\ *)
(* (forall n, (n >= inoise)%nat -> map1 n = None) /\ *)
(* eval_exp E (toRMap Gamma) (toREval (toRExp e)) vR M0 /\ *)
(* af_evals (afQ2R af) vR map1). *)
(* Lemma contained_subexpressions_map_extension (V: Type) e (expmap1: FloverMap.t V) expmap2: *)
(* contained_flover_map expmap1 expmap2 -> *)
(* contained_subexpressions e expmap1 -> *)
(* contained_subexpressions e expmap2. *)
(* Proof. *)
(* induction e; intros contf cont1. *)
(* - unfold contained_flover_map in contf. *)
(* unfold contained_subexpressions in *. *)
(* destruct cont1 as [_ [af cont1]]. *)
(* split; auto. *)
(* exists af. *)
(* now apply contf. *)
(* - unfold contained_flover_map in contf. *)
(* unfold contained_subexpressions in *. *)
(* destruct cont1 as [_ [af cont1]]. *)
(* split; auto. *)
(* exists af. *)
(* now apply contf. *)
(* - destruct cont1 as [contsub1 [af cont1]]. *)
(* specialize (IHe contf contsub1). *)
(* simpl; split; auto. *)
(* exists af. *)
(* now apply contf. *)
(* - destruct cont1 as [[contsub1 contsub2] [af cont1]]. *)
(* specialize (IHe1 contf contsub1). *)
(* specialize (IHe2 contf contsub2). *)
(* simpl; split; auto. *)
(* exists af. *)
(* now apply contf. *)
(* - destruct cont1 as [[contsub1 [contsub2 contsub3]] [af cont1]]. *)
(* specialize (IHe1 contf contsub1). *)
(* specialize (IHe2 contf contsub2). *)
(* specialize (IHe3 contf contsub3). *)
(* simpl; split; auto. *)
(* exists af. *)
(* now apply contf. *)
(* - destruct cont1 as [contsub1 [af cont1]]. *)
(* specialize (IHe contf contsub1). *)
(* simpl; split; auto. *)
(* exists af. *)
(* now apply contf. *)
(* Qed. *)
(* Lemma checked_expressions_contained A E Gamma e expmap1 expmap2 map1 map2 noise1 noise2: *)
(* contained_map map1 map2 -> *)
(* contained_flover_map expmap1 expmap2 -> *)
(* (noise2 >= noise1)%nat -> *)
(* contained_subexpressions e expmap1 -> *)
(* (forall n : nat, (n >= noise2)%nat -> map2 n = None) -> *)
(* checked_expressions A E Gamma e expmap1 noise1 map1 -> *)
(* checked_expressions A E Gamma e expmap2 noise2 map2. *)
(* Proof. *)
(* induction e; intros contm contf Hnoise Hfind Hmap2 checked1. *)
(* - simpl in Hfind |-*. *)
(* destruct Hfind as [_ Hfind]. *)
(* split; auto. *)
(* destruct checked1 as [_ [af [vR [aiv [aerr checked1]]]]]; eauto. *)
(* intros _. *)
(* exists af, vR, aiv, aerr. *)
(* intuition; eauto using fresh_monotonic, af_evals_map_extension. *)
(* - simpl in Hfind |-*. *)
(* destruct Hfind as [_ Hfind]. *)
(* split; auto. *)
(* destruct checked1 as [_ [af [vR [aiv [aerr checked1]]]]]; eauto. *)
(* intros _. *)
(* exists af, vR, aiv, aerr. *)
(* intuition; eauto using fresh_monotonic, af_evals_map_extension. *)
(* - simpl in Hfind |-*. *)
(* destruct Hfind as [found1 Hfind]. *)
(* destruct checked1 as [checked_sub1 checked1]. *)
(* specialize (IHe contm contf Hnoise found1 Hmap2 checked_sub1). *)
(* specialize (checked1 Hfind). *)
(* split; try assumption. *)
(* destruct checked1 as [af [vR [aiv [aerr checked1]]]]. *)
(* exists af, vR, aiv, aerr. *)
(* intuition; eauto using fresh_monotonic, af_evals_map_extension, contained_subexpressions_map_extension. *)
(* - simpl in Hfind |-*. *)
(* destruct Hfind as [[found1 found2] Hfind]. *)
(* destruct checked1 as [[checked_sub1 checked_sub2] checked1]. *)
(* specialize (IHe1 contm contf Hnoise found1 Hmap2 checked_sub1). *)
(* specialize (IHe2 contm contf Hnoise found2 Hmap2 checked_sub2). *)
(* specialize (checked1 Hfind). *)
(* repeat split; try assumption. *)
(* destruct checked1 as [af [vR [aiv [aerr checked1]]]]. *)
(* exists af, vR, aiv, aerr. *)
(* intuition; eauto using fresh_monotonic, af_evals_map_extension, contained_subexpressions_map_extension. *)
(* - simpl in Hfind |-*. *)
(* destruct Hfind as [[found1 [found2 found3]] Hfind]. *)
(* destruct checked1 as [[checked_sub1 [checked_sub2 checked_sub3]] checked1]. *)
(* specialize (IHe1 contm contf Hnoise found1 Hmap2 checked_sub1). *)
(* specialize (IHe2 contm contf Hnoise found2 Hmap2 checked_sub2). *)
(* specialize (IHe3 contm contf Hnoise found3 Hmap2 checked_sub3). *)
(* specialize (checked1 Hfind). *)
(* repeat split; try assumption. *)
(* destruct checked1 as [af [vR [aiv [aerr checked1]]]]. *)
(* exists af, vR, aiv, aerr. *)
(* intuition; eauto using fresh_monotonic, af_evals_map_extension, contained_subexpressions_map_extension. *)
(* - simpl in Hfind |-*. *)
(* destruct Hfind as [found1 Hfind]. *)
(* destruct checked1 as [checked_sub1 checked1]. *)
(* specialize (IHe contm contf Hnoise found1 Hmap2 checked_sub1). *)
(* specialize (checked1 Hfind). *)
(* split; try assumption. *)
(* destruct checked1 as [af [vR [aiv [aerr checked1]]]]. *)
(* exists af, vR, aiv, aerr. *)
(* intuition; eauto using fresh_monotonic, af_evals_map_extension, contained_subexpressions_map_extension. *)
(* Qed. *)
Lemma contained_flover_map_none (e: exp Q) (expmap1: FloverMap.t (affine_form Q)) expmap2:
contained_flover_map expmap1 expmap2 ->
FloverMap.find e expmap2 = None ->
......@@ -740,10 +586,18 @@ Proof.
{
inversion validBounds; subst; clear validBounds.
specialize (visitedExpr (Var Q n)).
destruct visitedExpr as [af [vR [aiv [aerr visitedExpr]]]].
- eexists; eauto.
- exists map1, af, vR, aiv, aerr.
intuition.
assert (NatSet.Subset (usedVars (Var Q n)) (fVars dVars)).
{
set_tac. set_tac. subst.
hnf in varsDisjoint.
specialize (varsDisjoint a0).
destruct (NatSet.mem a0 dVars) eqn:?.
+ right. now apply NatSet.mem_spec.
+ left. apply varsDisjoint. set_tac.
}
destruct visitedExpr as [af [vR [aiv [aerr visitedExpr]]]]; eauto.
exists map1, af, vR, aiv, aerr.
intuition.
}
destruct (FloverMap.find (elt:=intv * error) (Var Q n) A) as [p | p] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
......@@ -942,8 +796,7 @@ Proof.
- rewrite FloverMapFacts.P.F.add_neq_o in Hsome; auto.
congruence.
}
- clear varsTyped varsDisjoint dVarsValid fVarsSound fVars.
pose proof visitedExpr as visitedExpr'.
- pose proof visitedExpr as visitedExpr'.
unfold checked_expressions in visitedExpr.
destruct (FloverMap.find (elt:=affine_form Q) (Const m v) iexpmap) eqn: Hvisited.
{
......@@ -1458,7 +1311,7 @@ Proof.
destruct Qeq_bool.
- rewrite orb_true_l.
apply AffineArithQ.mult_aff_aux_preserves_fresh.
{
{
apply fresh_monotonic with (n := subnoise2);
try lia; try apply afQ2R_fresh; auto.
}
......@@ -1467,7 +1320,7 @@ Proof.
- destruct Qeq_bool.
+ rewrite orb_true_r.
apply AffineArithQ.mult_aff_aux_preserves_fresh.
{
{
apply fresh_monotonic with (n := subnoise2);
try lia; try apply afQ2R_fresh; auto.
}
......@@ -1476,7 +1329,7 @@ Proof.
+ simpl.
apply fresh_noise; try lia.
apply AffineArithQ.mult_aff_aux_preserves_fresh.
{
{
apply fresh_monotonic with (n := subnoise2);
try lia; try apply afQ2R_fresh; auto.
}
......@@ -1595,7 +1448,7 @@ Proof.
destruct (visitedExpr (Fma e1 e2 e3)) as [af [vR [aiv [aerr visitedExpr']]]].
- eexists; eauto.
- exists map1, af, vR, aiv, aerr.
intuition.
intuition.
}
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Fma e1 e2 e3) A) as [p | _] eqn: Hares; simpl in validBounds; try congruence.
......@@ -1667,9 +1520,9 @@ Proof.
assert (fresh subnoise3 (afQ2R af2)) as fresh2 by now apply afQ2R_fresh;
eauto using fresh_monotonic.
assert (fresh subnoise3 (afQ2R af3)) as fresh3 by now apply afQ2R_fresh.
assert (af_evals (afQ2R af1) vR1 ihmap3) as subaff1' by eauto using af_evals_map_extension.
assert (af_evals (afQ2R af2) vR2 ihmap3) as subaff2' by eauto using af_evals_map_extension.
assert (af_evals (afQ2R af3) vR3 ihmap3) as subaff3' by eauto using af_evals_map_extension.
assert (af_evals (afQ2R af1) vR1 ihmap3) as subaff1' by eauto using af_evals_map_extension.
assert (af_evals (afQ2R af2) vR2 ihmap3) as subaff2' by eauto using af_evals_map_extension.
assert (af_evals (afQ2R af3) vR3 ihmap3) as subaff3' by eauto using af_evals_map_extension.
specialize (multsound (afQ2R af2) (afQ2R af3) vR2 vR3 ihmap3 subnoise3 fresh2 fresh3 subaff2' subaff3') as [qMult multsound].
assert (contained_map map1 (updMap ihmap3 subnoise3 qMult)).
{
......@@ -1696,7 +1549,7 @@ Proof.
{
rewrite <- afQ2R_fresh in fresh1.
apply AffineArithQ.plus_aff_preserves_fresh.
{
{
apply fresh_monotonic with (n := subnoise3); try lia; auto.
}
unfold AffineArithQ.mult_aff.
......@@ -1829,7 +1682,7 @@ Proof.
destruct (visitedExpr (Downcast m e)) as [af [vR [aiv [aerr visitedExpr']]]].
- eexists; eauto.
- exists map1, af, vR, aiv, aerr.
intuition.
intuition.
}
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Downcast m e) A) as [p | p] eqn: Hares; simpl in validBounds; try congruence.
......@@ -1925,6 +1778,7 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
(forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
NatSet.Subset (usedVars e) (NatSet.union fVars dVars) /\
checked_expressions A E Gamma e iexpmap inoise map1) ->
(inoise > 0)%nat ->
(forall n, (n >= inoise)%nat -> map1 n = None) ->
......@@ -1974,6 +1828,10 @@ Proof.
set_tac. }
edestruct validab_sound as
[map2 [af [vR [aiv [aerr [Hcont [Hcontf [Hares [Hsup [Hsubaf [Hfresh [Hvalidmap [Hnoise' [Heval [evals visitedNewexpr]]]]]]]]]]]]]]]; eauto; clear validab_sound.
{
intros e' Hsome.
specialize (visitedExpr e' Hsome); intuition.
}
rewrite Hares in Hares__e.
inversion Hares__e; subst; clear Hares__e.
simpl.
......@@ -2096,10 +1954,11 @@ Proof.
as [ihmap [ihaf [ihvR [ihaiv [ihaerr [ihcont [ihcontf [ihares [ihsup [ihsubaf [ihfresh [ihvalidmap [ihnoise [ihbstep [ihevals ihchecked]]]]]]]]]]]]]]]; eauto; clear IHc.
{
intros e' Hsome.
specialize (visitedExpr e').
specialize (visitedNewexpr e').
destruct (FloverMap.find e' iexpmap) eqn: ?.
- specialize (visitedExpr ltac:(eauto)).
- specialize (visitedExpr e' ltac:(eauto)).
destruct visitedExpr as [Hsubset' visitedExpr].
split; try (rewrite <- H; rewrite <- Hsubset'; set_tac).
apply checked_expressions_contained with (expmap1 := iexpmap) (map1 := map1)
(noise1 := inoise); eauto.
+ pose proof contained_flover_map_extension as Hcont'.
......@@ -2112,7 +1971,16 @@ Proof.
+ destruct visitedExpr as [af' [vR' [aiv' [aerr' visitedExpr]]]].
exists af', vR', aiv', aerr'.
intuition.
admit.
eapply swap_Gamma_eval_exp.
eapply Rmap_updVars_comm.
eapply eval_exp_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto.
clear - Hsubset' H6.
apply not_in_not_mem in H6.
intros ?; apply H6.
assert (usedVars (toREval (toRExp e')) = usedVars e') by admit.
rewrite H0 in H.
set_tac.
- destruct (FloverMap.find e' exprAfs') eqn: ?.
+ specialize (visitedNewexpr ltac:(eauto) ltac:(eauto)).
unfold checked_expressions in visitedNewexpr |-*.
......@@ -2120,11 +1988,25 @@ Proof.
destruct (FloverMapFacts.O.MO.eq_dec (Var Q n) e');
try (erewrite FloverMapFacts.P.F.find_o in Heqo0;
try eapply Q_orderedExps.expCompare_eq_sym; eauto; congruence).
split; [admit | ].
exists af', vR', aiv', aerr'.
intuition.
* rewrite FloverMapFacts.P.F.add_neq_o; eauto.
* admit.
+ admit.
+ assert (e' = (Var Q n)) by admit.
subst; hnf.
destruct Hsome as [? Hsome].
erewrite FloverMapFacts.P.F.add_eq_o in Hsome.
assert (eaf = af) by congruence.
inversion Hsome; subst.
repeat eexists; eauto.
all: admit.
(* { *)
(* simpl. eapply Var_load; simpl; cbn; eauto. *)
(* - admit. *)
(* - unfold updEnv. *)
(* now rewrite Nat.eqb_refl. *)
(* } *)
}
assert (contained_map map1 ihmap) as ?
by (etransitivity; eassumption).
......
......@@ -1161,6 +1161,34 @@ Proof.
rewrite <- (H n); auto.
Qed.
Lemma eval_exp_ignore_bind e:
forall x v m Gamma E,
eval_exp E Gamma e v m ->
~ NatSet.In x (usedVars e) ->
forall m_new v_new,
eval_exp (updEnv x v_new E) (updDefVars x m_new Gamma) e v m.
Proof.
induction e; intros * eval_e no_usedVar *; cbn in *;
inversion eval_e; subst; try eauto.
- assert (n <> x).
{ hnf. intros. subst. apply no_usedVar; set_tac. }
rewrite <- Nat.eqb_neq in H.
eapply Var_load.
+ unfold updDefVars.
rewrite H; auto.
+ unfold updEnv.
rewrite H; auto.
- eapply Binop_dist'; eauto;
[ eapply IHe1 | eapply IHe2];
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
- eapply Fma_dist'; eauto;
[eapply IHe1 | eapply IHe2 | eapply IHe3];
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
Qed.
(*
(**
Analogous lemma for unary expressions.
......
......@@ -201,7 +201,15 @@ Proof.
case_eq (n =? y); auto.
Qed.
(*
Lemma ssa_inv_let V (e:exp V) m x g inVars outVars:
ssa (Let m x e g) inVars outVars ->
~ NatSet.In x inVars /\ ~ NatSet.In x (usedVars e).
Proof.
intros ssa_let.
inversion ssa_let; subst.
set_tac.
Qed.
(*
Lemma shadowing_free_rewriting_exp e v E1 E2 defVars:
(forall n, E1 n = E2 n)->
eval_exp E1 defVars (toREval e) v M0 <->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment