(**
    Interval arithmetic checker and its soundness proof.
    The function validIntervalbounds checks wether the given analysis result is
    a valid range arithmetic for each sub term of the given expression e.
    The computation is done using our formalized interval arithmetic.
    The function is used in CertificateChecker.v to build the full checker.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing.
Require Export Flover.IntervalArithQ Flover.IntervalArith Flover.ssaPrgs.

Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
  match FloverMap.find e A with
  | None => false
  | Some (intv, _) =>
       match e with
       | Var _ v =>
         if NatSet.mem v validVars
         then true
         else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
       | Const _ n => isSupersetIntv (n,n) intv
       | Unop o f =>
         if validIntervalbounds f A P validVars
         then
           match FloverMap.find f A with
           | None => false
           | Some (iv, _) =>
          match o with
          | Neg =>
            let new_iv := negateIntv iv in
            isSupersetIntv new_iv intv
          | Inv =>
            if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
                ((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))))
            then
              let new_iv := invertIntv iv in
              isSupersetIntv new_iv intv
            else false
          end
        end
      else false
    | Binop op f1 f2 =>
      if ((validIntervalbounds f1 A P validVars) &&
          (validIntervalbounds f2 A P validVars))
      then
        match FloverMap.find f1 A, FloverMap.find f2 A with
        | Some (iv1, _), Some (iv2, _) =>
          match op with
          | Plus =>
            let new_iv := addIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Sub =>
            let new_iv := subtractIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Mult =>
            let new_iv := multIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Div =>
            if (((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
                ((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))))
            then
              let new_iv := divideIntv iv1 iv2 in
              isSupersetIntv new_iv intv
            else false
          end
        | _, _ => false
        end
      else false
    | Fma f1 f2 f3 =>
      if ((validIntervalbounds f1 A P validVars) &&
          (validIntervalbounds f2 A P validVars) &&
          (validIntervalbounds f3 A P validVars))
      then
        match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
        | Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
          let new_iv := addIntv iv1 (multIntv iv2 iv3) in
          isSupersetIntv new_iv intv
        | _, _, _ => false
        end
      else false
    | Downcast _ f1 =>
      if (validIntervalbounds f1 A P validVars)
      then
        match FloverMap.find f1 A with
        | None => false
        | Some (iv1, _) =>
        (* TODO: intv = iv1 might be a hard constraint... *)
        (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv)
        end
      else
        false
       end
  end.

Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
  match f with
  | Let m x e g =>
    match FloverMap.find e A, FloverMap.find (Var Q x) A with
    | Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) =>
      if (validIntervalbounds e A P validVars &&
                              Qeq_bool (e_lo) (x_lo) &&
                              Qeq_bool (e_hi) (x_hi))
      then validIntervalboundsCmd g A P (NatSet.add x validVars)
      else false
    | _, _ => false
    end
  |Ret e =>
   validIntervalbounds e A P validVars
  end.

Corollary Q2R_max4 a b c d:
  Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
  unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto.
Qed.

Corollary Q2R_min4 a b c d:
  Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
  unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
Qed.

Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
  FloverMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) ->
  validIntervalbounds (Binop Div e1 e2) A P V = true ->
  (ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
  intros A_eq validBounds; cbn in *.
  Flover_compute; try congruence.
  apply le_neq_bool_to_lt_prop; auto.
Qed.

Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
  forall v, NatSet.In v dVars ->
       exists vR iv err,
         E v =  Some vR /\
         FloverMap.find (Var Q v) A = Some (iv, err) /\
         (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.

Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
  forall v,
    NatSet.In v fVars ->
    exists vR, E v = Some vR /\
          (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.

Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) :=
  forall v, NatSet.In v S ->
       exists m :mType, Gamma v = Some m.

Ltac kill_trivial_exists :=
  match goal with
  | [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
  | [ |- exists iv err, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
  end.

Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
        fVars dVars (E:env) Gamma:
    validIntervalbounds f A P dVars = true ->
    dVars_range_valid dVars E A ->
    NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
    fVars_P_sound fVars E P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
    exists iv err vR,
      FloverMap.find f A = Some (iv, err) /\
      eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
      (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
  induction f;
    intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
    cbn in *.
  - Flover_compute.
    destruct (NatSet.mem n dVars) eqn:?; simpl in *.
    + destruct (valid_definedVars n)
        as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
        try set_tac.
      rewrite map_n in *.
      inversion Heqo; subst.
      kill_trivial_exists.
      eexists; split; [auto| split; try eauto ].
      eapply Var_load; simpl; try auto.
      destruct (types_defined n) as [m type_m];
        set_tac.
      match_simpl; auto.
    + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]];
        set_tac; try auto.
      assert (NatSet.In n fVars) by set_tac.
      andb_to_prop valid_bounds.
      canonize_hyps; simpl in *.
      kill_trivial_exists.
      eexists; split; [auto | split].
      * econstructor; try eauto.
        destruct (types_defined n) as [m type_m];
          set_tac.
        match_simpl; auto.
      * lra.
  - Flover_compute; canonize_hyps; simpl in *.
    kill_trivial_exists.
    exists (perturb (Q2R v) 0).
    split; [auto| split].
    + econstructor; try eauto. apply Rabs_0_equiv.
    + unfold perturb; simpl; lra.
  - Flover_compute; simpl in *; try congruence.
    destruct IHf as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]];
      try auto.
    inversion iveq_f; subst.
    destruct u; try andb_to_prop R; simpl in *.
    + kill_trivial_exists.
      exists (evalUnop Neg vF); split;
        [auto | split ;
                            [econstructor; eauto | ]].
      canonize_hyps.
      rewrite Q2R_opp in *.
      simpl; lra.
    + rename L0 into nodiv0.
      apply le_neq_bool_to_lt_prop in nodiv0.
      kill_trivial_exists.
      exists (perturb (evalUnop Inv vF) 0); split;
        [destruct i; auto | split].
      * econstructor; eauto; try apply Rabs_0_equiv.
        (* Absence of division by zero *)
        hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
               rewrite Q2R0_is_0 in nodiv0; lra.
      * canonize_hyps.
        pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f))) (a :=vF)) as inv_valid.
         unfold invertInterval in inv_valid; simpl in *.
         rewrite delta_0_deterministic; [| rewrite Rbasic_fun.Rabs_R0; lra].
         destruct inv_valid; try auto.
         { destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
         { split; eapply Rle_trans.
           - apply L1.
           - rewrite Q2R_inv; try auto.
             destruct nodiv0; try lra.
             hnf; intros.
             assert (0 < Q2R (snd iv_f))%R.
             { eapply Rlt_le_trans.
               apply Qlt_Rlt in H1.
               rewrite <- Q2R0_is_0.
               apply H1. lra.
             }
             rewrite <- Q2R0_is_0 in H3.
             apply Rlt_Qlt in H3.
             lra.
           - apply H0.
           - rewrite <- Q2R_inv; try auto.
             hnf; intros.
             destruct nodiv0; try lra.
             assert (Q2R (fst iv_f) < 0)%R.
             { eapply Rle_lt_trans.
               Focus 2.
               rewrite <- Q2R0_is_0;
                 apply Qlt_Rlt in H2; apply H2.
               lra.
             }
             rewrite <- Q2R0_is_0 in H3.
             apply Rlt_Qlt in H3. lra. }
  - Flover_compute; try congruence.
    destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]];
      try auto; set_tac.
    destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]];
      try auto; set_tac.
    assert (M0 = join M0 M0) as M0_join by (cbv; auto);
      rewrite M0_join.
    kill_trivial_exists.
    exists (perturb (evalBinop b vF1 vF2) 0);
      split; [destruct i; auto | ].
    inversion env1; inversion env2; subst.
      destruct b; simpl in *.
    * split;
        [econstructor; try congruence; apply Rabs_0_equiv | ].
      pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                          (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_add.
      specialize (valid_add vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
      canonize_hyps; simpl in *.
      repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
      unfold perturb. lra.
    * split;
        [econstructor; try congruence; apply Rabs_0_equiv |].
      pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                             (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_sub.
      specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
      canonize_hyps; simpl in *.
      repeat rewrite <- Q2R_opp in *;
        repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
      unfold perturb; lra.
    * split;
        [ econstructor; try congruence; apply Rabs_0_equiv |].
      pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                                (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_mul.
      specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
      canonize_hyps; simpl in *.
      repeat rewrite <- Q2R_mult in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
      unfold perturb; lra.
    * andb_to_prop R.
      canonize_hyps.
      apply le_neq_bool_to_lt_prop in L.
      split;
        [ econstructor; try congruence; try apply Rabs_0_equiv | ].
      (* No division by zero proof *)
      { hnf; intros.
        destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. }
      { pose proof (interval_division_valid (a:=vF1) (b:=vF2)
                                            ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                            (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_div.
        simpl in *.
        destruct valid_div; try auto.
        - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
        - assert (~ (snd iv_f2) == 0).
          { hnf; intros. destruct L; try lra.
            assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
            lra. }
          assert (~ (fst iv_f2) == 0).
          { hnf; intros; destruct L; try lra.
            assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
            lra. }
          repeat (rewrite <- Q2R_inv in *; try auto).
          repeat rewrite <- Q2R_mult in *.
          rewrite <- Q2R_min4, <- Q2R_max4 in *.
          unfold perturb.
          lra.
      }
  - Flover_compute; try congruence.
    destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]; try auto; set_tac.
    destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]; try auto; set_tac.
    destruct IHf3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]]; try auto; set_tac.
    assert (M0 = join3 M0 M0 M0) as M0_join by (cbv; auto);
      rewrite M0_join.
    kill_trivial_exists.
    exists (perturb (evalFma vF1 vF2 vF3) 0); split; try auto.
    inversion env1; inversion env2; inversion env3; subst.
    split; [auto | ].
    * econstructor; try congruence; apply Rabs_0_equiv.
    * pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
      specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
      remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
      pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
      rewrite Heqiv_f23prod in valid_add, valid_mul.
      unfold multIntv in valid_add.
      canonize_hyps.
      simpl in *.
      repeat rewrite <- Q2R_mult in *;
        repeat rewrite <- Q2R_min4, <- Q2R_max4 in *;
        repeat rewrite <- Q2R_plus in *;
        repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
      specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
      unfold evalFma, evalBinop, perturb.
      lra.
  - match_simpl.
    andb_to_prop valid_bounds.
    match_simpl.
    destruct IHf as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]];
      try auto.
    inversion env_f; subst.
    kill_trivial_exists.
    exists (perturb vF 0).
    split; [destruct i; try auto |].
    split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |].
    unfold isSupersetIntv in *; andb_to_prop R.
    canonize_hyps; simpl in *.
    unfold perturb; lra.
Qed.

Lemma Rmap_updVars_comm Gamma n m:
  forall x,
    updDefVars n M0 (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
Proof.
  unfold updDefVars, toRMap; simpl.
  intros x; destruct (x =? n); try auto.
Qed.

Lemma swap_Gamma_eval_exp e E vR m Gamma1 Gamma2:
  (forall n, Gamma1 n = Gamma2 n) ->
  eval_exp E Gamma1 e vR m ->
  eval_exp E Gamma2 e vR m.
Proof.
  revert E vR Gamma1 Gamma2 m;
    induction e; intros * Gamma_eq eval_e;
      inversion eval_e; subst; simpl in *;
        try eauto.
  apply Var_load; try auto.
  rewrite <- Gamma_eq; auto.
Qed.

Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
  (forall n, Gamma1 n = Gamma2 n) ->
  bstep f E Gamma1 vR m ->
  bstep f E Gamma2 vR m.
Proof.
  revert E Gamma1 Gamma2;
  induction f; intros * Gamma_eq eval_f.
  - inversion eval_f; subst.
    econstructor; try eauto.
    +  eapply swap_Gamma_eval_exp; eauto.
    + apply (IHf _ (updDefVars n m0 Gamma1) _); try eauto.
      intros n1.
      unfold updDefVars.
      case (n1 =? n); auto.
  - inversion eval_f; subst.
    econstructor; try eauto.
    eapply swap_Gamma_eval_exp; eauto.
Qed.

Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
  forall Gamma E fVars dVars outVars P,
    ssa f (NatSet.union fVars dVars) outVars ->
    dVars_range_valid dVars E A ->
    fVars_P_sound fVars E P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
    validIntervalboundsCmd f A P dVars = true ->
    exists iv_e err_e vR,
      FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
      bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\
      (Q2R (fst iv_e) <=  vR <= Q2R (snd iv_e))%R.
Proof.
  induction f;
    intros *  ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f;
    cbn in *.
  - Flover_compute.
    inversion ssa_f; subst.
    canonize_hyps.
    pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e.
    destruct validIV_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]];
      try auto.
    { set_tac. repeat split; auto.
      hnf; intros; subst.
      set_tac. }
    rewrite find_v in *; inversion Heqo; subst.
    specialize (IHf (updDefVars n M0 Gamma) (updEnv n v E) fVars (NatSet.add n dVars)).
    assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
    + hnf. intros a; split; intros in_set; set_tac.
      * destruct in_set as [ ? | [? ?]]; try auto; set_tac.
        destruct H0; auto.
      * destruct in_set as [? | ?]; try auto; set_tac.
        destruct H as [? | [? ?]]; auto.
    + edestruct IHf as [iv_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]];
        try eauto.
       eapply ssa_equal_set. symmetry in H. apply H. apply H7.
      * intros v0 mem_v0.
        unfold updEnv.
        case_eq (v0 =? n); intros v0_eq.
        { rename R1 into eq_lo;
            rename R0 into eq_hi.
          rewrite Nat.eqb_eq in v0_eq; subst.
          exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra. }
        { apply dVars_sound.
          set_tac.
          destruct mem_v0 as [? | [? ?]]; try auto.
          rewrite Nat.eqb_neq in v0_eq.
          congruence. }
      * intros v0 mem_fVars.
        unfold updEnv.
        case_eq (v0 =? n); intros case_v0; auto.
        rewrite Nat.eqb_eq in case_v0; subst.
        assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac.
        exfalso; set_tac. apply H6; set_tac; auto.
      * intros x x_contained.
        set_tac.
        destruct x_contained as [x_free | x_def].
        { destruct (types_valid x) as [m_x Gamma_x]; try set_tac.
          exists m_x.
          unfold updDefVars. case_eq (x =? n); intros eq_case; try auto.
          rewrite Nat.eqb_eq in eq_case.
          subst.
          exfalso; apply H6; set_tac. }
        { set_tac.
          destruct x_def as [x_n | x_def]; subst.
          - exists M0; unfold updDefVars; rewrite Nat.eqb_refl; auto.
          - destruct x_def. destruct (types_valid x) as [m_x Gamma_x].
            + rewrite NatSet.union_spec; auto.
            + exists m_x.
              unfold updDefVars; case_eq (x =? n); intros eq_case; try auto.
              rewrite Nat.eqb_eq in eq_case; subst.
              congruence. }
      * clear L R1 R0 R IHf.
        hnf. intros a a_freeVar.
        rewrite NatSet.diff_spec in a_freeVar.
        destruct a_freeVar as [a_freeVar a_no_dVar].
        apply usedVars_subset.
        simpl.
        rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
        repeat split; try auto.
        { hnf; intros; subst.
          apply a_no_dVar.
          rewrite NatSet.add_spec; auto. }
        { hnf; intros a_dVar.
          apply a_no_dVar.
          rewrite NatSet.add_spec; auto. }
      * simpl. exists iv_f, err_f, vR; repeat split; try auto; try lra.
        econstructor; try eauto.
        eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
        intros n1; erewrite Rmap_updVars_comm; eauto.
  - unfold validIntervalboundsCmd in valid_bounds_f.
    pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
    destruct valid_iv_e as [?[?[? [? [? ?]]]]]; try auto.
    simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
Qed.