(** This file contains the coq implementation of the certificate checker as well as its soundness proof. The checker is a composition of the range analysis validator and the error bound validator. Running this function on the encoded analysis result gives the desired theorem as shown in the soundness theorem. **) From Flover Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator Environments TypeValidator FPRangeValidator ExpressionAbbrevs Commands. Require Export ExpressionSemantics Flover.Commands Coq.QArith.QArith. (** Certificate checking function **) Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:FloverMap.t mType):= let tMap := (getValidMap defVars e (FloverMap.empty mType)) in match tMap with |Succes tMap => if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty then RoundoffErrorValidator e tMap absenv NatSet.empty else false | _ => 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. **) Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars: forall (E1 E2:env), (forall v, NatSet.In v (Expressions.usedVars e) -> exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> CertificateChecker e absenv P 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)) (toREval (toRExp e)) vR REAL /\ eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m /\ (forall vF m, eval_expr E2 (toRExpMap Gamma) (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 * P_valid certificate_valid. unfold CertificateChecker in certificate_valid. destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence. rename t into Gamma. assert (validTypes e Gamma). { eapply getValidMap_top_correct; eauto. intros. cbn in *; congruence. } rewrite <- andb_lazy_alt in certificate_valid. andb_to_prop certificate_valid. pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty. hnf in union_empty. assert (dVars_range_valid NatSet.empty E1 absenv). { unfold dVars_range_valid. intros; set_tac. } assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None)) as affine_dvars_valid. { unfold affine_dVars_range_valid. intros; set_tac. } assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)). { hnf; intros a in_empty. set_tac. } rename R0 into validFPRanges. assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as valid_e. { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (E:=E1)); 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]]]]]. destruct iv_e as [elo ehi]. exists Gamma; intros approxE1E2. rewrite <- eval_expr_REAL_det_nondet in eval_real. assert (forall (e' : expr Rdefinitions.R) (m' : mType), exists d, (fun e m => Some 0%R) e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) as Htmp by admit. assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac). pose proof (RoundoffErrorValidator_sound e _ Htmp H approxE1E2 H1 eval_real R valid_e map_e Hdvars) as Hsound. unfold validErrorBounds in Hsound. (* destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto. *) (* exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto. *) Admitted. Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars := match getValidMapCmd defVars f (FloverMap.empty mType) with | Succes Gamma => if (validSSA f (freeVars f)) then if (RangeValidatorCmd f absenv P NatSet.empty) && FPRangeValidatorCmd f absenv Gamma NatSet.empty then (RoundoffErrorValidatorCmd f Gamma absenv NatSet.empty) else false else false | _ => false end. Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars: forall (E1 E2:env), (forall v, NatSet.In v (freeVars f) -> exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> CertificateCheckerCmd f absenv P defVars = true -> exists Gamma, approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 -> exists iv err vR vF m, FloverMap.find (getRetExp f) absenv = Some (iv,err) /\ bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\ bstep (toRCmd f) E2 (toRExpMap Gamma) vF m /\ (forall vF m, bstep (toRCmd f) E2 (toRExpMap Gamma) 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 * P_valid certificate_valid. unfold CertificateCheckerCmd in certificate_valid. destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?; try congruence. rename t into Gamma. assert (validTypesCmd f Gamma). { eapply getValidMapCmd_correct; try eauto. intros; cbn in *; congruence. } 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 f (freeVars f ∪ NatSet.empty) outVars) as ssa_valid. { eapply ssa_equal_set; try eauto. apply NatSetProps.empty_union_2. apply NatSet.empty_spec. } rename R into validFPRanges. assert (dVars_range_valid NatSet.empty E1 absenv). { unfold dVars_range_valid. intros; set_tac. } assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f)) as freeVars_contained by set_tac. assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f. { eapply RangeValidatorCmd_sound; eauto. unfold RangeValidatorCmd. unfold affine_dVars_range_valid; intros. set_tac. } 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]. edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto; [admit|]. exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto. Admitted.