Commit 530c94ef authored by Nikita Zyuzin's avatar Nikita Zyuzin

WIP Update

parent 25daf249
......@@ -484,21 +484,49 @@ Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m: mType, Gamma v = Some m.
Definition checked_expressions (A: analysisResult) E Gamma iexpmap inoise map1 :=
forall (e: exp Q),
(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 /\
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.
Fixpoint checked_expressions e iexpmap inoise map1 :=
match e with
| Var _ x =>
True
| Const x x0 =>
True
| Unop u e1 =>
checked_expressions e1 iexpmap inoise map1
| Binop b e1 e2 =>
checked_expressions e1 iexpmap inoise map1 /\ checked_expressions e2 iexpmap inoise map1
| Fma e1 e2 e3 =>
checked_expressions e1 iexpmap inoise map1 /\ checked_expressions e2 iexpmap inoise map1
/\ checked_expressions e3 iexpmap inoise map1
| Downcast m e1 =>
checked_expressions e1 iexpmap inoise map1
end /\
forall (A: analysisResult) E Gamma,
(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 /\
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.
(* Definition checked_expressions (A: analysisResult) E Gamma iexpmap inoise map1 := *)
(* forall (e: exp Q), *)
(* forall (A: analysisResult) E Gamma iexpmap inoise map1 *)
(* (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 /\ *)
(* 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 validAffineBounds_sound (e: exp Q) (A: analysisResult) (P: precond)
fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
checked_expressions A E Gamma iexpmap inoise map1 ->
checked_expressions e iexpmap inoise map1 ->
(inoise > 0)%nat ->
(forall n, (n >= inoise)%nat -> map1 n = None) ->
validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
......@@ -516,7 +544,8 @@ Lemma validAffineBounds_sound (e: exp Q) (A: analysisResult) (P: precond)
(forall n, (n >= noise)%nat -> map2 n = None) /\
(noise >= inoise)%nat /\
eval_exp E (toRMap Gamma) (toREval (toRExp e)) vR M0 /\
af_evals (afQ2R af) vR map2.
af_evals (afQ2R af) vR map2 /\
checked_expressions e exprAfs noise map2.
Proof.
revert noise exprAfs inoise iexpmap map1.
induction e;
......@@ -862,6 +891,7 @@ Proof.
destruct (IHe2 subnoise2 subexprAff2 subnoise1 subexprAff1 ihmap1) as [ihmap2 [af2' [vR2 [_ [_ [ihcont2 [ihcontf2 [_ [_ [Haf2 [subfresh2 [Hsubvalidmap2 [Hsubnoise2 [subeval2 subaff2]]]]]]]]]]]]]];
try auto; try lra; clear IHe2; eauto using fresh_n_gt_O.
{
unfold checked_expressions.
admit.
}
{
......
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