Commit f39146e5 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Continue cmd soundness proof

parent b884a957
...@@ -1038,12 +1038,26 @@ Proof. ...@@ -1038,12 +1038,26 @@ Proof.
destruct p as (exprAfs', noise'). destruct p as (exprAfs', noise').
pose proof validAffineBounds_sound as validab_sound. pose proof validAffineBounds_sound as validab_sound.
simpl in Hsubset. simpl in Hsubset.
specialize (validab_sound e A P fVars dVars E Gamma exprAfs' noise' iexpmap inoise map1 enough (NatSet.Subset (usedVars e -- dVars) fVars) as Hsubs.
checkedExprs Hnoise Hmapvalid Hvalidab dvars_valid). destruct (validab_sound e A P fVars dVars E Gamma exprAfs' noise' iexpmap inoise map1
edestruct IHc; clear IHc. checkedExprs Hnoise Hmapvalid Hvalidab dvars_valid Hsubs
Focus 4. fvars_valid vars_typed) as
exact valid_bounds_cmd. [map2 [af [vR [aiv [aerr [Hcont [Hares [Hsup [Hsubaf [Hfresh [Hvalidmap [Hnoise' [Heval evals]]]]]]]]]]]]]; clear validab_sound.
all: try eassumption. simpl.
assert (noise' > 0)%nat as H' by omega.
enough (forall n : nat, (n >= noise')%nat -> map1 n = None) as H''.
enough (ssa c (fVars (NatSet.add n dVars)) outVars) as H'''.
enough (affine_dVars_range_valid (NatSet.add n dVars) E A) as H4.
enough (NatSet.Subset (freeVars c -- NatSet.add n dVars) fVars) as H5.
enough (affine_fVars_P_sound fVars E P) as H6.
enough (affine_vars_typed (fVars NatSet.add n dVars) Gamma) as H7.
specialize (IHc (NatSet.add n dVars) exprAfs' noise' exprAfs noise
checkedExprs H' H'' valid_bounds_cmd H''' H4 H5 H6 H7).
destruct IHc as [ihmap [ihaf [ihvR [ihaiv [ihaerr [ihcont [ihares [ihsup [ihsubaf [ihfresh [ihvalidmap [ihnoise [ihbstep ihevals]]]]]]]]]]]]].
exists ihmap, ihaf, ihvR, ihaiv, ihaerr.
intuition.
econstructor; try exact Heval.
simpl.
- simpl. - simpl.
eapply validAffineBounds_sound in valid_bounds_cmd; auto. eapply validAffineBounds_sound in valid_bounds_cmd; auto.
destruct valid_bounds_cmd as [map2 [af [vR [aiv [aerr valid_bounds_cmd]]]]]. destruct valid_bounds_cmd as [map2 [af [vR [aiv [aerr valid_bounds_cmd]]]]].
......
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