started to implement another cover checker

coq/SubdivsChecker2.v

+From Flover
+     Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
+     Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
+     Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
+     IntervalArithQ.
+(*
+From Flover
+     Require Import Infra.RealRationalProps Environments ExpressionSemantics
+     IntervalArithQ SMTArith RealRangeArith RealRangeValidator RoundoffErrorValidator
+     ssaPrgs TypeValidator ErrorAnalysis ResultChecker.
+*)
+
+Require Import List.
+
+Fixpoint resultLeq e (A1 A2: analysisResult) :=
+  match e with
+  | Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
+  | Binop _ e1 e2 | Let _ _ e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2
+  | Fma e1 e2 e3 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 && resultLeq e3 A1 A2
+  | _ => true
+  end &&
+      match FloverMap.find e A1, FloverMap.find e A2 with
+      | Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
+      | _, _ => false
+      end.
+
+Lemma resultLeq_sound e A1 A2 :
+  resultLeq e A1 A2 = true ->
+  exists iv1 err1 iv2 err2,
+    FloverMap.find e A1 = Some (iv1, err1) /\
+    FloverMap.find e A2 = Some (iv2, err2) /\
+    isSupersetIntv iv1 iv2 = true /\
+    err1 <= err2.
+Proof.
+  intros H.
+  assert (
+      match FloverMap.find e A1, FloverMap.find e A2 with
+      | Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
+      | _, _ => false
+      end = true).
+  { unfold resultLeq in H. destruct e;
+    apply andb_prop in H as [_ H]; auto. }
+  Flover_compute.
+  repeat eexists; auto.
+  - unfold isSupersetIntv. now rewrite L0.
+  - apply (reflect_iff _ _ (Z.leb_spec0 _ _)). auto.
+Qed.
+
+(* TODO: maybe put this somewhere else *)
+Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
+  NatSet.Empty dVars ->
+  approxEnv E1 Gamma A1 fVars dVars E2 ->
+  approxEnv E1 Gamma A2 fVars dVars E2.
+Proof.
+  intros He H.
+  induction H.
+  - constructor.
+  - econstructor; eauto.
+  - exfalso. eapply He. set_tac.
+Qed.
+
+Definition checkSubdivsStep e absenv defVars Gamma (b: bool) (PA: precond * analysisResult) :=
+  let (P, A) := PA in
+  b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) &&
+    resultLeq e A absenv.
+
+Definition checkSubdivs e absenv subdivs defVars Gamma :=
+  fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs true.
+
+Lemma checkSubdivs_false_fp e absenv subdivs defVars Gamma :
+  fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs false = false.
+Proof.
+  induction subdivs as [|[P A] subdivs]; auto.
+Qed.
+
+Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A :
+  checkSubdivs e absenv subdivs defVars Gamma = true ->
+  In (P, A) subdivs ->
+  RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true /\
+  resultLeq e A absenv = true.
+Proof.
+  intros H Hin.
+  induction subdivs; cbn in Hin; auto.
+  destruct Hin; subst; auto.
+  - cbn in *.
+    destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?;
+             try (rewrite checkSubdivs_false_fp in H; discriminate H).
+    split; auto.
+    destruct (resultLeq e A absenv) eqn: ?; auto.
+    rewrite checkSubdivs_false_fp in H; auto.
+  - apply IHsubdivs; auto. cbn in H.
+    unfold checkSubdivs.
+    destruct (checkSubdivsStep e absenv defVars Gamma true a) eqn:?; auto.
+    rewrite checkSubdivs_false_fp in H. discriminate H.
+Qed.
+
+(*
+Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) :=
+  match FloverMap.find e A1, FloverMap.find e A2 with
+  | Some (iv1, err1), Some (iv2, err2) =>
+    let acc1 := FloverMap.add e (unionIntv iv1 iv2, Qmax err1 err2) acc in
+    match e with
+    | Unop _ e1 | Downcast _ e1 => merge_subdivs_step e1 acc1 A1 A2
+    | Binop _ e1 e2 | Let _ _ e1 e2 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
+                                  merge_subdivs_step e2 acc2 A1 A2
+    | Fma e1 e2 e3 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
+                     let acc3 := merge_subdivs_step e2 acc2 A1 A2 in
+                     merge_subdivs_step e3 acc3 A1 A2
+    | _ => acc1
+    end
+  | _, _ => FloverMap.empty (intv * error)
+  end.
+
+(* TODO: it might be better to merge all results for one specific expression,
+   instead of merging 2 results for all expressions *)
+Definition merge_subdivs e hd tl : analysisResult :=
+  fold_left (merge_subdivs_step e (FloverMap.empty (intv * error))) tl hd.
+*)
+
+Definition joinIntv iv1 iv2 : result (option intv) :=
+  if isSupersetIntv iv2 iv1 then Succes (Some iv1) else
+    if Qeqb (ivhi iv1) (ivlo iv2) then Succes (Some (ivlo iv1, ivhi iv2)) else Fail _ "intervals don't align".
+
+Definition checkDimensionStep x (ivAcc: result (option intv)) P (* (ivNew: option intv) *) :=
+  let ivNew := FloverMap.find (Var Q x) P in
+  match ivAcc with
+  | Succes ivAcc => match ivNew with
+                 | Some ivNew => optionBind ivAcc (fun iv => joinIntv iv ivNew) (Succes (Some ivNew))
+                 | None => Fail _ "var not found in precond"
+                 end
+  | f => f
+  end.
+
+Definition checkDimension x iv Ps :=
+  match fold_left (checkDimensionStep x) Ps (Succes None) with
+  | Succes (Some ivU) => if isSupersetIntv iv ivU then Succes true else Fail _ "var not covered"
+  | Succes None => Fail _ "no subdivisions given"
+  | Fail _ msg | FailDet msg _ => Fail _ msg
+  end.
+
+Definition checkAllDimensionsStep Ps b (p: expr Q * intv) :=
+  match p with
+  | (Var _ x, iv) => resultBind b (fun _ => checkDimension x iv Ps) (* b && checkDimension x iv Ps *)
+  | _ => b
+  end.
+
+Definition checkAllDimensions P Ps :=
+  fold_left (checkAllDimensionsStep Ps) P (Succes false).
+
+Lemma checkAllDimensionsStep_fail_fp Ps P s :
+  fold_left (checkAllDimensionsStep Ps) P (Fail bool s) = Fail bool s.
+Proof.
+  induction P as [|p P]; auto.
+  destruct p as [e iv]. destruct e; auto.
+Qed.
+
+Lemma checkAllDimensionsStep_faildet_fp Ps P s b :
+  fold_left (checkAllDimensionsStep Ps) P (FailDet s b) = FailDet s b.
+Proof.
+  induction P as [|p P]; auto.
+  destruct p as [e iv]. destruct e; auto.
+Qed.
+
+Fixpoint coverIntv iv intvs :=
+  match intvs with
+  | nil => false
+  | intv :: nil => isSupersetIntv iv intv
+  | intv :: intvs =>
+    Qleb (ivlo intv) (ivlo iv) && coverIntv (ivhi intv, ivhi iv) intvs
+  end.
+
+Lemma coverIntv_sound iv intvs a :
+  coverIntv iv intvs = true ->
+  contained a iv ->
+  exists intv, In intv intvs /\ contained a intv.
+Proof.
+  induction intvs as [|intv0 intvs] in iv |- *; [intros H; discriminate H|].
+  destruct intvs as [|intv1 intvs]; cbn; intros H Hin.
+  - exists intv0. split; auto. andb_to_prop H. repeat canonize_Q_prop. unfold contained in *. lra.
+  - destruct (Qleb a (ivhi intv0)) eqn: Heq.
+    + andb_to_prop H.
+      repeat canonize_Q_prop.
+      exists intv0. split; cbn; auto.
+      unfold contained in *.
+      cbn in *. lra.
+    + andb_to_prop H.
+      destruct (IHintvs (ivhi intv0, ivhi iv)) as [intv [inl Hin1]].
+      * auto.
+      * assert (ivhi intv0 <= a) as H.
+        { apply Qnot_lt_le.
+          intros Hlt.
+          apply Qlt_le_weak in Hlt.
+          apply Qle_bool_iff in Hlt. unfold Qleb in Heq. rewrite Heq in Hlt.
+          discriminate Hlt. }
+        unfold contained in *. cbn in *. lra.
+      * exists intv. auto.
+Qed.
+
+Fixpoint mergeDim x Ps bs :=
+  match Ps with
+  | nil =>
+  | P :: Ps =>
+  end.
+
+Fixpoint covers P Ps :=
+  match P with
+  | nil => match Ps with nil :: nil => true | _ => false end
+  | (Var _ x, iv) :: P =>
+    let (intvs, buckets) := mergeDim x Ps in
+    forallb (covers P) buckets && coverIntv iv intvs
+  | _ :: P => covers P Ps
+  end.
+  
+Lemma in_subdivs_intv (Ps: list precondIntv) E (P: precondIntv) :
+  checkAllDimensions (FloverMap.elements P) Ps = Succes true ->
+  P_intv_sound E P ->
+  exists P', In P' Ps /\ P_intv_sound E P'.
+Proof.
+  intros chk H.
+  unfold P_intv_sound in H.
+  induction (FloverMap.elements P).
+  - cbn in chk. discriminate chk.
+  - cbn in chk.
+    destruct (checkAllDimensionsStep Ps (Succes false) a) eqn:Heq;
+      try (rewrite ?checkAllDimensionsStep_fail_fp, ?checkAllDimensionsStep_faildet_fp in chk;
+           discriminate chk).
+    destruct b.
+    + destruct a as [e iv].
+      destruct e; try discriminate Heq.
+      cbn in Heq.
+      admit. (* this might not work *)
+    + apply IHl; auto.
+      intros x iv inl. apply H. now right.
+Abort.
+  
+(* TODO: needs more assumptions, i.e. checker for precond *)
+Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P :
+  eval_precond E P ->
+  exists P' A, In (P', A) subdivs /\ eval_precond E P'.
+Admitted.
+
+(* TODO: check precond sound wrt. subdivs *)
+(* TODO: merge hd and tl again *)
+(** Interval subdivisions checking function **)
+Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
+           (P: precond) hd tl (defVars: FloverMap.t  mType) Gamma :=
+  validSSA e (preVars P) &&
+           checkSubdivs e absenv (hd :: tl) defVars Gamma.
+
+(**
+   Soundness proof for the interval subdivs checker.
+**)
+Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs tl_subdivs defVars Gamma:
+  forall (E1 E2: env) DeltaMap,
+    (forall (e': expr R) (m': mType),
+        exists d: R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    eval_precond E1 P ->
+    getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
+    SubdivsChecker e absenv P hd_subdivs tl_subdivs defVars Gamma = true ->
+    exists Gamma,
+      approxEnv E1 (toRExpMap Gamma) absenv (freeVars 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.
+Proof.
+  intros * deltas_matched P_valid valid_typeMap subdivs_valid.
+  andb_to_prop subdivs_valid.
+  rename L into valid_ssa.
+  rename R into valid_subdivs.
+  apply (in_subdivs (hd_subdivs :: tl_subdivs)) in P_valid as [P' [A [in_subdivs P_valid]]].
+  (* preVars P == preVars P' should hold *)
+  assert (validSSA e (preVars P') = true) as valid_ssa' by admit.
+  pose proof (checkSubdivs_sound  e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
+  assert (ResultChecker e A P' (FloverMap.empty(SMTLogic * SMTLogic))  defVars Gamma = true) as res_check
+    by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
+  exists Gamma; intros approxE1E2.
+  assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
+      by (eapply approxEnv_empty_dVars; eauto).
+  assert (validRanges e A E1 (toRTMap (toRExpMap Gamma))) as validRange.
+  { eapply result_checking_sound; eauto.
+    admit. (* unsat_queries of empty map *) }
+  assert (validErrorBounds e E1 E2 A Gamma DeltaMap) as Hsound.
+  { eapply result_checking_sound; eauto.
+    admit. (* unsat_queries of empty map *) }
+  eapply validRanges_single in validRange.
+  destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
+  eapply validErrorBounds_single in Hsound; eauto.
+  destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
+  destruct (resultLeq_sound _ _ _ A_leq) as [iv1 [err1 [iv2 [err2 H]]]].
+  destruct H as [F1 [F2 [sub err_leq]]].
+  exists iv2, err2, vR, vF, mF; repeat split; auto.
+  assert (err = err1) by congruence; subst.
+  apply Qle_Rle in err_leq.
+  intros vF0 m Heval.
+  specialize (err_bounded vF0 m Heval).
+  lra.
+Admitted.
\ No newline at end of file