Commit defb76de authored by Joachim Bard's avatar Joachim Bard

proving IEEE connection

parent 56829d57
......@@ -1156,17 +1156,14 @@ Proof.
- eapply getValidMap_preserving with (akk:=akk); eauto.
Qed.
Theorem IEEE_connection_expr e A P E1 E2 defVars:
Theorem IEEE_connection_expr e A P qMap E1 E2 defVars:
is64BitEval (B2Qexpr e) ->
is64BitEnv defVars ->
noDowncast (B2Qexpr e) ->
eval_expr_valid e E2 ->
(forall v,
NatSet.In v (usedVars (B2Qexpr e)) ->
exists vR,
(E1 v = Some vR) /\
Q2R (fst (P v)) <= vR <= Q2R(snd (P v)))%R ->
CertificateChecker (B2Qexpr e) A P defVars = true ->
unsat_queries E1 qMap ->
eval_precond E1 P ->
CertificateChecker (B2Qexpr e) A P qMap defVars = true ->
exists Gamma, (* m, currently = M64 *)
approxEnv E1 Gamma A (usedVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
exists iv err vR vF,
......@@ -1176,7 +1173,7 @@ Theorem IEEE_connection_expr e A P E1 E2 defVars:
eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\
(Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R.
Proof.
intros * is64eval is64bitenv no_cast eval_valid P_valid certificate_valid.
intros * is64eval is64bitenv no_cast eval_valid unsat_qs P_valid certificate_valid.
unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars (B2Qexpr e) (FloverMap.empty mType)) eqn:?; try congruence.
assert (is64BitEnv t).
......@@ -1203,7 +1200,7 @@ Proof.
set_tac. }
rename R0 into validFPRanges.
assert (validRanges (B2Qexpr e) A E1 (toRTMap (toRExpMap Gamma))) as valid_e.
{ eapply (RealRangeValidator.RangeValidator_sound (B2Qexpr e) (dVars:=NatSet.empty) (A:=A) (P:=P));
{ eapply (RealRangeValidator.RangeValidator_sound (B2Qexpr e) (dVars:=NatSet.empty) (A:=A) (P:=P) (Qmap:=qMap));
auto. }
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
......@@ -1223,16 +1220,15 @@ Proof.
repeat eexists; eauto.
Qed.
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P qMap
defVars E1 E2:
is64BitBstep (B2Qcmd f) ->
is64BitEnv defVars ->
noDowncastFun (B2Qcmd f) ->
bstep_valid f E2 ->
(forall v, NatSet.mem v (freeVars (B2Qcmd f))= true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
CertificateCheckerCmd (B2Qcmd f) A P defVars = true ->
unsat_queries E1 qMap ->
eval_precond E1 P ->
CertificateCheckerCmd (B2Qcmd f) A P qMap defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
exists iv err vR vF m,
......@@ -1244,7 +1240,7 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) vF m ->
(Rabs (vR - vF) <= Q2R err)%R).
Proof.
intros * is64bitBstep is64BitEnv_def noDowncast bstep_valid P_valid certificate_valid.
intros * is64bitBstep is64BitEnv_def noDowncast bstep_valid unsat_qs P_valid certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars (B2Qcmd f) (FloverMap.empty mType)) eqn:?;
try congruence.
......@@ -1259,22 +1255,24 @@ Proof.
exists Gamma; intros approxE1E2.
repeat rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
apply validSSA_sound in L.
destruct L as [outVars ssa_f].
assert (ssa (B2Qcmd f) (freeVars (B2Qcmd f) NatSet.empty) outVars) as ssa_valid.
{ eapply ssa_equal_set; try eauto.
apply NatSetProps.empty_union_2.
apply NatSet.empty_spec. }
assert (validSSA (B2Qcmd f) (freeVars (B2Qcmd f) NatSet.empty) = true) as ssa_valid_small.
{ eapply validSSA_downward_closed; eauto; set_tac.
eapply validSSA_checks_freeVars; eauto. intuition. set_tac. }
apply validSSA_sound in ssa_valid_small as [outVars_small ssa_small].
rename L into ssa_valid.
pose proof (validSSA_sound _ _ ssa_valid) as [outVars ssa_f].
rename R into validFPRanges.
assert (NatSet.Subset (freeVars (B2Qcmd f) -- NatSet.empty) (freeVars (B2Qcmd f)))
as freeVars_contained by set_tac.
assert (validRangesCmd (B2Qcmd f) A E1 (toRTMap (toRExpMap Gamma))) as valid_f.
{ eapply RealRangeValidator.RangeValidatorCmd_sound; eauto.
{ eapply (RealRangeValidator.RangeValidatorCmd_sound _ (fVars:=preVars P));
eauto; set_tac.
- eapply (ssa_equal_set (inVars:=preVars P)); eauto.
apply NatSetProps.empty_union_2. set_tac.
- unfold RealRangeArith.dVars_range_valid. intros; set_tac.
- unfold AffineValidation.affine_dVars_range_valid; intros.
set_tac.
- unfold RealRangeArith.fVars_P_sound. intros; eapply P_valid.
rewrite NatSet.mem_spec; auto. }
- eapply validSSA_checks_freeVars; eauto. }
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
......
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