Commit 231e24bf authored by Nikita Zyuzin's avatar Nikita Zyuzin

Progress with validationCmd soundness proof

parent 8ac618e5
......@@ -652,6 +652,18 @@ Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
(* 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 ->
FloverMap.find e expmap1 = None.
Proof.
intros cont Hfound1.
unfold contained_flover_map in cont.
destruct (FloverMap.find (elt:=affine_form Q) e expmap1) eqn: Heq; auto.
apply cont in Heq.
congruence.
Qed.
Definition checked_expressions (A: analysisResult) E Gamma e iexpmap inoise map1 :=
exists af vR aiv aerr,
FloverMap.find e A = Some (aiv, aerr) /\
......@@ -2083,7 +2095,25 @@ Proof.
(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.
{
intros e' Hsome.
specialize (visitedExpr e').
specialize (visitedNewexpr e').
destruct (FloverMap.find (elt:=affine_form Q) e' iexpmap) eqn: ?.
- specialize (visitedExpr ltac:(eauto)).
apply checked_expressions_contained with (expmap1 := iexpmap) (map1 := map1)
(noise1 := inoise); eauto.
+ pose proof contained_flover_map_extension as Hcont'.
eapply contained_flover_map_none in Hvar; try eassumption.
specialize (Hcont' _ iexpmap _ eaf Hvar).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
clear Hcont'.
now etransitivity; try eassumption.
+ destruct visitedExpr as [af' [vR' [aiv' [aerr' visitedExpr]]]].
exists af', vR', aiv', aerr'.
intuition.
admit.
- admit.
}
assert (contained_map map1 ihmap) as ?
by (etransitivity; eassumption).
......@@ -2094,17 +2124,13 @@ Proof.
assert (noise >= inoise)%nat by lia.
exists ihmap, ihaf, ihvR, ihaiv, ihaerr.
repeat split; try auto.
+ simpl.
econstructor; try eauto.
+ econstructor; try eauto.
eapply IntervalValidation.swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
intros n1; erewrite Rmap_updVars_comm; eauto.
+ intros e' Hnone Hsome.
unfold checked_expressions.
destruct (FloverMapFacts.O.MO.eq_dec e' (getRetExp c)).
* exists ihaf, ihvR, ihaiv, ihaerr.
specialize (ihchecked e').
intuition; try (erewrite FloverMapFacts.P.F.find_o; eauto).
admit.
* admit.
* admit.
- simpl.
eapply validAffineBounds_sound in valid_bounds_cmd; auto.
......
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