(**
   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 Flover.SMTArith.

(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
           (P: precond) Qmap (defVars:FloverMap.t  mType):=
  let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
  match tMap with
  |Succes tMap =>
   if RangeValidator e absenv P Qmap 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 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.
  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));
      eauto. }
  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.
  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 H approxE1E2 H1 eval_real R
                                           valid_e map_e Hdvars) as Hsound.
  unfold validErrorBounds in 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.
Qed.

Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: precond)
           (Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars :=
  match getValidMapCmd defVars f (FloverMap.empty mType) with
  | Succes Gamma =>
    if (validSSA f (preVars P))
    then
      if (RangeValidatorCmd f absenv P Qmap 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 Qmap
        defVars DeltaMap:
  forall (E1 E2:env),
    (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 ->
    CertificateCheckerCmd f absenv P Qmap 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)) DeltaMapR vR REAL /\
    bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m /\
    (forall vF m,
        bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap 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.
  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.
  pose proof (validSSA_checks_freeVars _ _ L) as sub.
  assert (validSSA f (freeVars f) = true) as ssa_valid
    by (eapply validSSA_downward_closed; eauto; set_tac).
  apply validSSA_sound in ssa_valid as [outVars_small ssa_f_small].
  apply validSSA_sound in L.
  destruct L as [outVars ssa_f].
  assert (ssa f (preVars P ∪ NatSet.empty) outVars) as ssa_valid.
  { eapply ssa_equal_set; 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 _ (fVars:=preVars P)); eauto; intuition.
    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].

  pose proof RoundoffErrorValidatorCmd_sound as Hsound.
  eapply validErrorBoundsCmdRec_single in Hsound; eauto.
  - specialize Hsound as ((vF & mF & eval_float) & ?).
    exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
  - eapply ssa_equal_set. 2: exact ssa_f_small.
    apply NatSetProps.empty_union_2.
    apply NatSet.empty_spec.
  - unfold dVars_contained; intros; set_tac.
Qed.