Commit 8804c37e authored by Nikita Zyuzin's avatar Nikita Zyuzin

Admit affineCmd proofs; prove RealRangeValidator proofs

parent 635bc329
......@@ -2186,6 +2186,7 @@ Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
(forall n, (n >= noise)%nat -> map2 n = None) /\
(noise >= inoise)%nat /\
bstep (toREvalCmd (toRCmd c)) E (toRMap Gamma) vR REAL /\
validRangesCmd c A E Gamma /\
af_evals (afQ2R af) vR map2 /\
(forall e, FloverMap.find e iexpmap = None ->
(exists af, FloverMap.find e exprAfs = Some af) ->
......@@ -2215,10 +2216,9 @@ Proof.
hnf; intros; subst.
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.
[map2 [af [vR [aiv [aerr [Hcont [Hcontf [Hares [Hsup [Hsubaf [Hfresh [Hvalidmap [Hnoise' [Heval [Hranges [evals visitedNewexpr]]]]]]]]]]]]]]]]; eauto; clear validab_sound.
rewrite Hares in Hares__e.
inversion Hares__e; subst; clear Hares__e.
simpl.
assert (noise' > 0)%nat as H' by omega.
assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))) as H.
{
......@@ -2335,7 +2335,7 @@ Proof.
edestruct IHc with (E := updEnv n vR E) (Gamma := updDefVars n REAL Gamma)
(dVars := NatSet.add n dVars)
(iexpmap := FloverMap.add (Var Q n) eaf exprAfs')
as [ihmap [ihaf [ihvR [ihaiv [ihaerr [ihcont [ihcontf [ihares [ihsup [ihsubaf [ihfresh [ihvalidmap [ihnoise [ihbstep [ihevals ihchecked]]]]]]]]]]]]]]]; eauto; clear IHc.
as [ihmap [ihaf [ihvR [ihaiv [ihaerr [ihcont [ihcontf [ihares [ihsup [ihsubaf [ihfresh [ihvalidmap [ihnoise [ihbstep [ihranges [ihevals ihchecked]]]]]]]]]]]]]]]]; eauto; clear IHc.
{
intros e' Hsome.
specialize (visitedNewexpr e').
......@@ -2362,6 +2362,7 @@ Proof.
rewrite usedVars_toREval_toRExp_compat.
intros ?; apply H6.
set_tac.
* admit.
- destruct (FloverMap.find e' exprAfs') eqn: ?.
+ specialize (visitedNewexpr ltac:(eauto) ltac:(eauto)).
unfold checked_expressions in visitedNewexpr |-*.
......@@ -2381,6 +2382,7 @@ Proof.
rewrite usedVars_toREval_toRExp_compat.
intros ?; apply H6.
set_tac.
* admit.
+ 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).
......@@ -2407,6 +2409,23 @@ Proof.
apply Q_orderedExps.exprCompare_refl.
* rewrite expr_compare_eq_eval_compat with (e2 := (Var Q n)); auto.
apply Var_load; unfold updDefVars, updEnv; simpl; now rewrite Nat.eqb_refl.
* eapply validRanges_eq_compat; eauto.
split; auto.
apply validAffineBounds_validRanges.
exists map2, af, vR, (xlo, xhi), aerr__n.
repeat split; auto.
-- 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.
-- apply Var_load; unfold updDefVars, updEnv; simpl; now rewrite Nat.eqb_refl.
}
assert (contained_map map1 ihmap) as ?
by (etransitivity; eassumption).
......@@ -2420,6 +2439,8 @@ 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 e' Hnone Hsome.
specialize (ihchecked e').
specialize (visitedNewexpr e').
......@@ -2453,6 +2474,7 @@ 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 af_evals_map_extension with (map1 := map2); eauto.
}
* rewrite FloverMapFacts.P.F.add_neq_o in ihchecked; eauto.
......@@ -2473,4 +2495,5 @@ Proof.
intuition; eauto.
constructor.
eauto.
Qed.
admit.
Admitted.
......@@ -27,48 +27,33 @@ Proof.
destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
- eapply validIntervalbounds_sound; eauto.
unfold dVars_range_valid; intros; set_tac.
- (* FIXME
@Nikita: Start here
pose (iexpmap := (FloverMap.empty (affine_form Q))).
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in H, H1.
destruct (validAffineBounds f A P dVars iexpmap inoise) eqn: Hafcheck;
destruct (validAffineBounds e A P dVars iexpmap inoise) eqn: Hafcheck;
try congruence.
clear H.
destruct p as [exprAfs noise].
pose proof (validAffineBounds_sound) as sound_affine.
assert ((forall e : FloverMap.key,
(exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e iexpmap = Some af) ->
checked_expressions A E Gamma (usedVars f) dVars e iexpmap inoise imap)) as Hchecked
by (intros e Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
assert ((forall e' : FloverMap.key,
(exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
checked_expressions A E Gamma (usedVars e) dVars e' iexpmap inoise imap)) as Hchecked
by (intros e' Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
rewrite FloverMapFacts.P.F.empty_o in Hein;
congruence).
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
assert (NatSet.Subset (usedVars f -- dVars) (usedVars f)) as Hsubset by set_tac.
assert (affine_fVars_P_sound (usedVars f) E P) as HfVars by exact H2.
assert (affine_vars_typed (usedVars f dVars) Gamma) as Hvarstyped
assert (NatSet.Subset (usedVars e -- dVars) (usedVars e)) as Hsubset by set_tac.
assert (affine_fVars_P_sound (usedVars e) E P) as HfVars by exact H2.
assert (affine_vars_typed (usedVars e dVars) Gamma) as Hvarstyped
by exact H3.
specialize (sound_affine f A P (usedVars f) dVars E Gamma
specialize (sound_affine e A P (usedVars e) dVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars Hvarstyped)
as [map2 [af [vR [aiv [aerr sound_affine]]]]].
destruct sound_affine as [_ [_ [Haiv [Hsup [_ [_ [_ [_ [Hee [Heval _]]]]]]]]]].
exists aiv, aerr, vR.
split; try split; try auto.
apply AffineArith.to_interval_containment in Heval.
unfold isSupersetIntv in Hsup.
apply andb_prop in Hsup 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 Heval.
simpl in Heval.
destruct Heval as [Heval1 Heval2].
split; eauto using Rle_trans. *)
Admitted.
intuition.
Qed.
Definition RangeValidatorCmd e A P dVars:=
if
......@@ -94,5 +79,28 @@ Proof.
unfold RangeValidatorCmd in ranges_valid.
destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
- eapply validIntervalboundsCmd_sound; eauto.
- (* FIXME *)
Admitted.
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in ranges_valid, H1.
destruct (validAffineBoundsCmd f A P dVars iexpmap inoise) eqn: Hafcheck;
try congruence.
destruct p as [exprAfs noise].
pose proof (validAffineBoundsCmd_sound) as sound_affine.
assert ((forall e' : FloverMap.key,
(exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
checked_expressions A E Gamma fVars dVars e' iexpmap inoise imap)) as Hchecked
by (intros e' Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
rewrite FloverMapFacts.P.F.empty_o in Hein;
congruence).
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
assert (affine_fVars_P_sound fVars E P) as HfVars by exact H2.
assert (affine_vars_typed (fVars dVars) Gamma) as Hvarstyped
by exact H3.
specialize (sound_affine f A P fVars dVars outVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H H1 H4 HfVars Hvarstyped)
as [map2 [af [vR [aiv [aerr sound_affine]]]]].
intuition.
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