(**
   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),
    approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
    (forall v, NatSet.mem v (Expressions.usedVars e) = true ->
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
    (forall v, (v) mem (usedVars e) = true ->
          exists m : mType,
            defVars v = Some m) ->
    CertificateChecker e absenv P defVars = true ->
   exists vR vF m,
    eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
    eval_exp E2 defVars (toRExp e) vF m /\
    (forall vF m,
        eval_exp E2 defVars (toRExp e) vF m ->
        (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 types_defined 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.
  pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
  hnf in union_empty.
  assert (forall v1, (v1) mem (Expressions.usedVars e ∪ NatSet.empty) = true ->
                exists m0 : mType, defVars v1 = Some m0).
  { intros; eapply types_defined.
    rewrite NatSet.mem_spec in *.
    rewrite <- union_empty; eauto. }
  assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
  { hnf; intros a in_empty.
    set_tac. }
  assert (forall v, (v) mem (NatSet.empty) = true -> exists vR : R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
  { intros v v_in_empty.
    rewrite NatSet.mem_spec in v_in_empty.
    inversion v_in_empty. }
  edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto.
  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
  exists vR; exists vF; exists mF; split; auto.
Qed.

Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
  if (typeCheckCmd f defVars (typeMapCmd defVars f) && validSSA f (freeVars 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),
    approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
    (forall v, NatSet.mem v (freeVars f)= true ->
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
    (forall v, (v) mem (freeVars f) = true ->
          exists m : mType,
            defVars v = Some m) ->
    CertificateCheckerCmd f absenv P defVars = true ->
    exists vR vF m,
    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
    bstep (toRCmd f) E2 defVars vF m /\
    (forall vF m,
        bstep (toRCmd f) E2 defVars vF m ->
        (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 types_defined certificate_valid.
  unfold CertificateCheckerCmd in certificate_valid.
  repeat rewrite <- andb_lazy_alt in certificate_valid.
  andb_to_prop certificate_valid.
  apply validSSA_sound in R0.
  destruct R0 as [outVars ssa_f].
  env_assert absenv (getRetExp f) env_f.
  destruct env_f as [iv [err absenv_eq]].
  destruct iv as [ivlo ivhi].
  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. }
  assert (forall v, (v) mem (NatSet.empty) = true ->
               exists vR : R,
                 E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) as no_dVars_valid.
  { intros v v_in_empty.
    set_tac. inversion v_in_empty. }
  assert (forall v, (v) mem (freeVars f ∪ NatSet.empty) = true ->
               exists m : mType, defVars v = Some m) as types_valid.
  { intros v v_mem; apply types_defined.
    set_tac. rewrite NatSet.union_spec in v_mem.
    destruct v_mem; try auto.
    inversion H. }
  assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
    as freeVars_contained by set_tac.
  edestruct (validIntervalboundsCmd_sound) as [vR [eval_real bounded_real_f]] ; eauto.
  rewrite absenv_eq; simpl.
  edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
  exists vR; exists vF; exists mF; split; try auto.
  split; try auto.
  intros.
  eapply validErrorboundCmd_sound; eauto.
Qed.