(** 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. **) Require Import Coq.Reals.Reals Coq.QArith.Qreals. Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs. Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing. Require Export Coq.QArith.QArith. Require Export Daisy.Infra.ExpressionAbbrevs. (** Certificate checking function **) Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) := if (validIntervalbounds e absenv P NatSet.empty) then (validErrorbound e (fun (e:exp Q) => typeExpression e) absenv NatSet.empty) else false. (** 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:exp Q) (absenv:analysisResult) P: forall (E1 E2:env) (vR:R) (vF:R) fVars m, approxEnv E1 absenv fVars NatSet.empty E2 -> (forall v, NatSet.mem v fVars = true -> exists vR, E1 v = Some (vR, M0) /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> NatSet.Subset (Expressions.usedVars e) fVars -> eval_exp E1 (toREval (toRExp e)) vR M0 -> eval_exp E2 (toRExp e) vF m -> CertificateChecker e absenv P = true -> (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R. (** The proofs is a simple composition of the soundness proofs for the range validator and the error bound validator. **) Proof. intros * approxE1E2 P_valid fVars_subset eval_real eval_float certificate_valid. unfold CertificateChecker in certificate_valid. rewrite <- andb_lazy_alt in certificate_valid. andb_to_prop certificate_valid. env_assert absenv e env_e. destruct env_e as [iv [err absenv_eq]]. destruct iv as [ivlo ivhi]. rewrite absenv_eq; simpl. eapply validErrorbound_sound; eauto. - admit. (*eapply validTypeMap; eauto. *) - hnf. intros a in_diff. rewrite NatSet.diff_spec in in_diff. apply fVars_subset. destruct in_diff; auto. - intros v m0 v_in_empty. rewrite NatSet.mem_spec in v_in_empty. inversion v_in_empty. Admitted. (* Qed. *) Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) := if (validIntervalboundsCmd f absenv P NatSet.empty) then (validErrorboundCmd f (fun e => typeExpression e) absenv NatSet.empty) else false. Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P: forall (E1 E2:env) outVars vR vF fVars m, approxEnv E1 absenv fVars NatSet.empty E2 -> (forall v, NatSet.mem v fVars= true -> exists vR, E1 v = Some (vR, M0) /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> NatSet.Subset (Commands.freeVars f) fVars -> ssaPrg f fVars outVars -> bstep (toREvalCmd (toRCmd f)) E1 vR M0 -> bstep (toRCmd f) E2 vF m -> CertificateCheckerCmd f absenv P = true -> (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R. (** The proofs is a simple composition of the soundness proofs for the range validator and the error bound validator. **) Proof. intros * approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float certificate_valid. unfold CertificateCheckerCmd in certificate_valid. rewrite <- andb_lazy_alt in certificate_valid. andb_to_prop certificate_valid. env_assert absenv (getRetExp f) env_f. destruct env_f as [iv [err absenv_eq]]. destruct iv as [ivlo ivhi]. rewrite absenv_eq; simpl. eapply (validErrorboundCmd_sound); eauto. - admit. (* eapply typeMapCmdValid; eauto.*) - instantiate (1 := outVars). eapply ssa_equal_set; try eauto. hnf. intros a; split; intros in_union. + rewrite NatSet.union_spec in in_union. destruct in_union as [in_fVars | in_empty]; try auto. inversion in_empty. + rewrite NatSet.union_spec; auto. - hnf; intros a in_diff. rewrite NatSet.diff_spec in in_diff. destruct in_diff. apply fVars_subset; auto. - intros v m1 v_in_empty. rewrite NatSet.mem_spec in v_in_empty. inversion v_in_empty. Admitted.