Commit 773e05ea authored by Nikita Zyuzin's avatar Nikita Zyuzin

Prove the remains of validAffineBoundsCmd_sound

parent 35edd282
......@@ -2164,6 +2164,93 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
| Ret e => validAffineBounds e A P validVars exprsAf currentMaxNoise
end.
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma vR vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars dVars) outVars ->
NatSet.Subset (usedVars e) (fVars dVars) ->
~ (n fVars dVars) ->
eval_expr E Gamma e vR REAL ->
eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) e vR REAL.
Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto.
Qed.
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars dVars) outVars ->
NatSet.Subset (usedVars e) (fVars dVars) ->
~ (n fVars dVars) ->
validRanges e A E Gamma ->
validRanges e A (updEnv n vR' E) (updDefVars n REAL Gamma).
Proof.
intros Hssa Hsub Hnotin Hranges.
induction e.
- split; auto.
destruct Hranges as [_ [iv [err [vR Hranges]]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
- split; auto.
destruct Hranges as [_ [iv [err [vR Hranges]]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
- simpl in Hsub.
destruct Hranges as [Hunopranges Hranges].
specialize (IHe Hsub Hunopranges).
split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
rewrite usedVars_toREval_toRExp_compat; auto.
- simpl in Hsub.
assert (NatSet.Subset (usedVars e1) (fVars dVars)) as Hsub1 by set_tac.
assert (NatSet.Subset (usedVars e2) (fVars dVars)) as Hsub2 by (clear Hsub1; set_tac).
destruct Hranges as [[Hdiv [Hranges1 Hranges2]] Hranges].
specialize (IHe1 Hsub1 Hranges1).
specialize (IHe2 Hsub2 Hranges2).
simpl.
repeat split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
simpl.
repeat rewrite usedVars_toREval_toRExp_compat; auto.
- simpl in Hsub.
assert (NatSet.Subset (usedVars e1) (fVars dVars)) as Hsub1 by set_tac.
assert (NatSet.Subset (usedVars e2) (fVars dVars)) as Hsub2 by (clear Hsub1; set_tac).
assert (NatSet.Subset (usedVars e3) (fVars dVars)) as Hsub3 by (clear Hsub1 Hsub2; set_tac).
destruct Hranges as [[Hranges1 [Hranges2 Hranges3]] Hranges].
specialize (IHe1 Hsub1 Hranges1).
specialize (IHe2 Hsub2 Hranges2).
specialize (IHe3 Hsub3 Hranges3).
simpl.
repeat split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
simpl.
repeat rewrite usedVars_toREval_toRExp_compat; auto.
- simpl in Hsub.
destruct Hranges as [Hranges' Hranges].
specialize (IHe Hsub Hranges').
split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
rewrite usedVars_toREval_toRExp_compat; auto.
Qed.
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) ->
......@@ -2356,13 +2443,11 @@ Proof.
* rewrite <- H; rewrite <- H0; set_tac.
* eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto.
apply not_in_not_mem in H6.
rewrite usedVars_toREval_toRExp_compat.
intros ?; apply H6.
set_tac.
* admit.
eapply eval_expr_ssa_extension; try eassumption.
rewrite usedVars_toREval_toRExp_compat; auto.
* eapply validRanges_ssa_extension; eauto.
now apply not_in_not_mem in H6.
- destruct (FloverMap.find e' exprAfs') eqn: ?.
+ specialize (visitedNewexpr ltac:(eauto) ltac:(eauto)).
unfold checked_expressions in visitedNewexpr |-*.
......@@ -2376,13 +2461,11 @@ Proof.
* rewrite FloverMapFacts.P.F.add_neq_o; eauto.
* eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto.
apply not_in_not_mem in H6.
rewrite usedVars_toREval_toRExp_compat.
intros ?; apply H6.
set_tac.
* admit.
eapply eval_expr_ssa_extension; try eassumption.
rewrite usedVars_toREval_toRExp_compat; auto.
* eapply validRanges_ssa_extension; eauto.
now apply not_in_not_mem in H6.
+ destruct (FloverMapFacts.O.MO.eq_dec (Var Q n) e') as [Hvare' | Hvare'];
try (rewrite FloverMapFacts.P.F.add_neq_o in Hsome; eauto;
rewrite Heqo0 in Hsome; destruct Hsome as [? Hsome]; congruence).
......@@ -2439,8 +2522,25 @@ Proof.
+ econstructor; try eauto.
eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n REAL Gamma)) ; try eauto.
intros n1; erewrite Rmap_updVars_comm; eauto.
+ admit.
+ admit.
+ intros vR' ?.
assert (vR' = vR) by (eapply meps_0_deterministic; eauto); subst.
auto.
+ exists ihaiv, ihaerr, ihvR.
split; auto.
split.
* econstructor; try eauto.
eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n REAL Gamma)) ; try eauto.
intros n1; erewrite Rmap_updVars_comm; eauto.
* apply AffineArith.to_interval_containment in ihevals.
unfold isSupersetIntv in ihsup.
apply andb_prop in ihsup as [Hsupl Hsupr].
apply Qle_bool_iff in Hsupl.
apply Qle_bool_iff in Hsupr.
apply Qle_Rle in Hsupl.
apply Qle_Rle in Hsupr.
rewrite <- to_interval_to_intv in ihevals.
destruct ihevals as [Heval1 Heval2].
split; eauto using Rle_trans.
+ intros e' Hnone Hsome.
specialize (ihchecked e').
specialize (visitedNewexpr e').
......@@ -2449,6 +2549,20 @@ Proof.
af, vR, (xlo, xhi), aerr__n.
assert (Q_orderedExps.exprCompare e' (Var Q n) = Eq)
by (now rewrite Q_orderedExps.exprCompare_eq_sym).
assert (isSupersetIntv (toIntv af) (xlo, xhi) = true).
{
apply andb_prop in Heq.
destruct Heq as [eq_lo eq_hi].
apply Qeq_bool_iff in eq_lo.
apply Qeq_bool_iff in eq_hi.
unfold isSupersetIntv in Hsup |-*.
apply andb_true_intro.
apply andb_prop in Hsup.
destruct Hsup as [Hsup__l Hsup__r].
rewrite Qle_bool_iff in Hsup__l, Hsup__r.
simpl in Hsup__l, Hsup__r |-*.
split; rewrite Qle_bool_iff; lra.
}
do 2 (erewrite FloverMapFacts.P.F.find_o with (x := e'); eauto).
{
repeat split; auto.
......@@ -2456,17 +2570,6 @@ Proof.
rewrite <- H.
simpl.
set_tac.
- apply andb_prop in Heq.
destruct Heq as [eq_lo eq_hi].
apply Qeq_bool_iff in eq_lo.
apply Qeq_bool_iff in eq_hi.
unfold isSupersetIntv in Hsup |-*.
apply andb_true_intro.
apply andb_prop in Hsup.
destruct Hsup as [Hsup__l Hsup__r].
rewrite Qle_bool_iff in Hsup__l, Hsup__r.
simpl in Hsup__l, Hsup__r |-*.
split; rewrite Qle_bool_iff; lra.
- assert (af = eaf) by congruence; subst.
apply ihcontf.
rewrite FloverMapFacts.P.F.add_eq_o; eauto.
......@@ -2474,7 +2577,12 @@ Proof.
- apply fresh_monotonic with (n := noise'); try lia; auto.
- rewrite expr_compare_eq_eval_compat with (e2 := (Var Q n)); auto.
apply Var_load; unfold updDefVars, updEnv; simpl; now rewrite Nat.eqb_refl.
- admit.
- eapply validRanges_eq_compat; eauto.
split; auto.
apply validAffineBounds_validRanges.
exists map2, af, vR, (xlo, xhi), aerr__n.
intuition.
apply Var_load; unfold updDefVars, updEnv; simpl; now rewrite Nat.eqb_refl.
- eapply af_evals_map_extension with (map1 := map2); eauto.
}
* rewrite FloverMapFacts.P.F.add_neq_o in ihchecked; eauto.
......@@ -2493,7 +2601,20 @@ Proof.
destruct valid_bounds_cmd as [map2 [af [vR [aiv [aerr valid_bounds_cmd]]]]].
exists map2, af, vR, aiv, aerr.
intuition; eauto.
constructor.
eauto.
admit.
Admitted.
+ constructor.
eauto.
+ exists aiv, aerr, vR.
split; auto.
split.
* constructor; eauto.
* apply AffineArith.to_interval_containment in H9.
unfold isSupersetIntv in H2.
apply andb_prop in H2 as [Hsupl Hsupr].
apply Qle_bool_iff in Hsupl.
apply Qle_bool_iff in Hsupr.
apply Qle_Rle in Hsupl.
apply Qle_Rle in Hsupr.
rewrite <- to_interval_to_intv in H9.
destruct H9 as [Heval1 Heval2].
split; eauto using Rle_trans.
Qed.
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