CertificateChecker.v

(**
   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 Daisy.Commands.

(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
  if (typeCheck e defVars (typeMap defVars e)) then 
    if (validIntervalbounds e absenv P NatSet.empty)
    then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
    else false
  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 defVars:
  forall (E1 E2:env) (vR:R) (vF:R) fVars m,
    approxEnv E1 defVars absenv fVars NatSet.empty E2 ->
    (forall v, NatSet.mem v fVars = true ->
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
    NatSet.Subset (Expressions.usedVars e) fVars ->
    eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) vR M0 ->
    eval_exp E2 defVars (toRExp e) vF m ->
    CertificateChecker e absenv P defVars = 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.
  - hnf. intros a in_diff.
    rewrite NatSet.diff_spec in in_diff.
    apply fVars_subset.
    destruct in_diff; auto.
  - intros v v_in_empty.
    rewrite NatSet.mem_spec in v_in_empty.
    inversion v_in_empty.
Qed.

Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
  if (typeCheckCmd f defVars (typeMapCmd defVars f))
       then if (validIntervalboundsCmd f absenv P NatSet.empty)
            then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
            else false
  else false.

Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
  forall (E1 E2:env) outVars vR vF fVars m,
    approxEnv E1 defVars absenv fVars NatSet.empty E2 ->
    (forall v, NatSet.mem v fVars= true ->
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
    NatSet.Subset (Commands.freeVars f) fVars ->
    ssa f fVars outVars ->
    bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 ->
    bstep (toRCmd f) E2 defVars vF m ->
    CertificateCheckerCmd f absenv P defVars = 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.
  - 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 v_in_empty.
    rewrite NatSet.mem_spec in v_in_empty.
    inversion v_in_empty.
Qed.