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