Commit b4da184d authored by Heiko Becker's avatar Heiko Becker

Provide a more general certificate checker theorem to ease IEEE connection proofs

parent 39a53d43
......@@ -23,12 +23,8 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
| _ => false
end.
(**
Soundness proof for the certificate checker.
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition and dissatisfies the queries.
**)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars:
Theorem Certificate_checking_is_sound_general (e:expr Q) (absenv:analysisResult)
P Qmap defVars:
forall (E1 E2:env) DeltaMap,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
......@@ -43,7 +39,11 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
(forall vF m,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(Rabs (vR - vF) <= Q2R err))%R /\
validTypes e Gamma /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma absenv.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -83,9 +83,45 @@ Proof.
pose proof (RoundoffErrorValidator_sound e H approxE1E2 H1 eval_real R
valid_e map_e Hdvars) as Hsound.
unfold validErrorBounds in Hsound.
pose proof Hsound as Hsound'.
eapply validErrorBoundsRec_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
eapply FPRangeValidator_sound; eauto. intros; set_tac.
Qed.
(**
Soundness proof for the certificate checker.
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition and dissatisfies the queries.
**)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars:
forall (E1 E2:env) DeltaMap,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P ->
unsat_queries Qmap ->
CertificateChecker e absenv P Qmap defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (usedVars e) NatSet.empty E2 ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
(forall vF m,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros * deltas_matched P_valid unsat_qs certificate_valid.
edestruct (Certificate_checking_is_sound_general)as [Gamma validCert]; eauto.
exists Gamma. intros approxEnvs.
specialize (validCert approxEnvs).
destruct validCert as (? & ? & ? & ? & ? & ? & ? & ? & ? & ?).
repeat eexists; eauto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: precond)
......
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