finishing covers checker (with proofs)

coq/CertificateChecker.v

@@ -6,7 +6,7 @@
 **)
 From Flover
      Require Import Infra.RealRationalProps Environments TypeValidator
-     ResultChecker SubdivsChecker2.
+     ResultChecker SubdivsChecker3.
 
 Require Export List ExpressionSemantics Coq.QArith.QArith Flover.SMTArith.
 Export ListNotations.

coq/SubdivsChecker3.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.
+Require Import Program.
+Require Import FunInd.
+
+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 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 v :
+  coverIntv iv intvs = true ->
+  (Q2R (ivlo iv) <= v <= Q2R (ivhi iv))%R ->
+  exists intv, In intv intvs /\ (Q2R (ivlo intv) <= v <= Q2R (ivhi intv))%R.
+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. canonize_hyps. cbn in *. lra.
+  - destruct (Rle_or_lt v (Q2R (ivhi intv0))) as [Hle|Hlt].
+    + andb_to_prop H.
+      canonize_hyps.
+      exists intv0. split; cbn; auto.
+      cbn in *. lra.
+    + andb_to_prop H.
+      destruct (IHintvs (ivhi intv0, ivhi iv)) as [intv [inl Hin1]]; eauto.
+      cbn in *. lra.
+Qed.
+
+Fixpoint getBucket x iv Ps :=
+  match Ps with
+  | nil => (nil, nil)
+  | P :: Ps' =>
+    match P with
+    | nil => (nil, Ps) (* fail *)
+    | (e, ivE) :: P' =>
+       match Q_orderedExps.compare e (Var Q x) with
+       | Eq =>
+         if isSupersetIntv iv ivE then
+           let (b, rest) := getBucket x iv Ps' in (P' :: b, rest)
+         else (nil, Ps)
+       | _ => (nil, Ps) (* fail *)
+       end
+    end
+  end.
+
+Lemma getBucket_length x iv Ps b rest :
+  getBucket x iv Ps = (b, rest) ->
+  length Ps = length (b ++ rest).
+Proof with try now injection 1; intros; subst.
+  induction Ps as [|P Ps] in b |- *; cbn...
+  destruct P as [|[e ivE] P]...
+  destruct (Q_orderedExps.compare e (Var Q x)) eqn:?...
+  destruct (isSupersetIntv iv ivE) eqn:?...
+  destruct (getBucket x iv Ps) eqn:?...
+  injection 1; intros; subst.
+  cbn. now rewrite <- IHPs.
+Qed.
+
+Lemma getBucket_sound x iv Ps b rest :
+  getBucket x iv Ps = (b, rest) ->
+  forall P, In P b ->
+       exists ivx, In ((Var Q x, ivx) :: P) Ps /\ isSupersetIntv iv ivx = true.
+Proof with try now injection 1; intros; subst.
+  induction Ps as [|P1 Ps] in b |- *; cbn...
+  destruct P1 as [|[e ivE] P1]...
+  cbn.
+  destruct (Q_orderedExps.compare e (Var Q x)) eqn:Heqc...
+  destruct (isSupersetIntv iv ivE) eqn:?...
+  destruct (getBucket x iv Ps) eqn:?...
+  injection 1; intros; subst.
+  destruct H2 as [-> | Hin].
+  - assert (e = Var Q x)
+      by (destruct e; try discriminate Heqc;
+        now rewrite (nat_compare_eq _ _ Heqc)).
+    exists ivE. subst. split; auto.
+  - edestruct IHPs as [ivx [inPs sub]]; eauto.
+Qed.
+
+Lemma getBucket_rest_sound x iv Ps b rest :
+  getBucket x iv Ps = (b, rest) ->
+  forall P, In P rest -> In P Ps.
+Proof with try now injection 1; intros; subst.
+  induction Ps as [|P Ps] in b |- *; cbn...
+  destruct P as [|[e ivE] P]...
+  destruct (Q_orderedExps.compare e (Var Q x)) eqn:?...
+  destruct (isSupersetIntv iv ivE) eqn:?...
+  destruct (getBucket x iv Ps) eqn:?...
+  injection 1; intros; subst.
+  right. eapply IHPs; eauto.
+Qed.
+(*
+Function checkDim cov x iv Ps {measure length Ps} :=
+  match Ps with
+  | nil => false
+  | P :: _ =>
+    match FloverMap.find (Var Q x) P with
+    | Some ivx =>
+      let (b, rest) := getBucket_aux x ivx Ps in
+      let covb := cov b in
+      covb && match rest with
+              | nil => isSupersetIntv iv ivx
+              | _ => checkDim cov x (snd ivx, snd iv) rest
+              end
+    | None => false
+    end
+  end.
+intros cov x iv Ps P Ps' HPs ivx Hfind b rest P' rest' Hrest.
+rewrite <- Hrest.
+rewrite <- HPs at 2.
+cbn.
+unfold addToBucket.
+rewrite Hfind.
+unfold isSupersetIntv, Qleb, Qle_bool.
+rewrite !Z.leb_refl.
+rewrite <- HPs.
+cbn.
+destruct (getBucket_aux x ivx Ps') eqn:Heq.
+apply getBucket_aux_sound in Heq.
+clear Hrest rest'.
+injection 1; intros; subst.
+cbn.
+rewrite Heq, app_length.
+apply le_lt_n_Sm, le_plus_r.
+Defined.
+*)
+
+Function checkDim cov x iv Ps {measure length Ps} :=
+  match Ps with
+  | nil => false
+  | P :: _ =>
+    match P with
+    | (e, ivx) :: _ =>
+      match Q_orderedExps.compare e (Var Q x) with
+      | Eq =>
+        let (b, rest) := getBucket x ivx Ps in
+        if isSupersetIntv iv ivx then cov b
+        else cov b && Qleb (fst ivx) (fst iv) && checkDim cov x (snd ivx, snd iv) rest
+      | _ => false
+      end
+    | _ => false
+    end
+  end.
+intros cov x iv Ps P rest [e ivE] b e' ivx H HP HPs Heq b' rest'.
+rewrite <- HPs at 2.
+cbn.
+rewrite Heq.
+unfold isSupersetIntv, Qleb, Qle_bool.
+rewrite !Z.leb_refl.
+rewrite <- HPs.
+destruct (getBucket x ivx rest) eqn:Hb.
+injection 1; intros; subst.
+cbn.
+rewrite (getBucket_length _ _ _ Hb); eauto.
+rewrite app_length.
+apply le_lt_n_Sm, le_plus_r.
+Defined.
+
+Fixpoint covers (P: list (expr Q * intv)) Ps :=
+  match P with
+  | nil => match Ps with nil::nil => true | _ => false end
+  | (Var _ x, iv) :: P =>
+    checkDim (covers P) x iv Ps
+  | _ :: P => false
+  end.
+
+Lemma checkDim_sound cov x iv Ps v E :
+  checkDim cov x iv Ps = true ->
+  E x = Some v ->
+  (Q2R (fst iv) <= v <= Q2R (snd iv))%R ->
+  exists P, In P Ps /\
+       (forall (x : nat) (iv : intv),
+           In (Var Q x, iv) P ->
+           exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R).
+Proof.
+  functional induction (checkDim cov x iv Ps); try discriminate 1.
+  - admit.
+  - cbn in *.
+Abort.
+  
+Lemma covers_sound P Ps E :
+  covers P Ps = true ->
+  (forall (x : nat) (iv : intv),
+      In (Var Q x, iv) P ->
+      exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R) ->
+  exists P', In P' Ps /\
+        (forall (x : nat) (iv : intv),
+            In (Var Q x, iv) P' ->
+            exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R).
+Proof.
+  induction P as [|[e iv] P] in Ps |- *.
+  - cbn. destruct Ps as [|[|? ?] [|? ?]] eqn:Heq; try discriminate 1.
+    intros _ _.
+    exists nil; split; try now constructor.
+    intros x iv H. exfalso. apply (in_nil H).
+  - destruct e; cbn; intros H; try discriminate H.
+    intros HPl.
+    assert (exists vR : R, E n = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R)
+      as [v [inE iniv]]
+        by (apply HPl; auto).
+    functional induction checkDim (covers P) n iv Ps; try discriminate H.
+    + destruct (IHP _ H) as [P' [inb HP']].
+      { intros. apply HPl. auto. }
+      destruct (getBucket_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
+      eexists; split; eauto.
+      intros x iv' [Heq | inP']; auto.
+      injection Heq. intros; subst.
+      cbn in *.
+      Flover_compute.
+      canonize_hyps.
+      cbn in *; subst.
+      exists v. split; [auto | lra].
+    + Flover_compute.
+      destruct (Rle_or_lt v (Q2R (snd ivx))) as [Hle|Hlt].
+      * destruct (IHP _ L0) as [P' [inb HP']].
+        { intros. apply HPl. auto. }
+        destruct (getBucket_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
+        eexists; split; eauto.
+        intros x iv' [Heq | inP']; auto.
+        injection Heq. intros; subst.
+        cbn in *.
+        Flover_compute.
+        canonize_hyps.
+        cbn in *; subst.
+        exists v. split; [auto | lra].
+      * assert (Q2R (snd ivx) <= v <= Q2R (snd iv))%R as Hv.
+        { unfold isSupersetIntv in *. cbn in *.
+          rewrite R0 in *. cbn in *.
+          canonize_hyps. split; lra. }
+        destruct IHb0 as [P' [inrest H]]; auto.
+        { intros x iv' [Heq | inP]; auto.
+          injection Heq; intros; subst.
+          cbn. exists v. split; auto. }
+        exists P'; split; auto.
+        eapply getBucket_rest_sound; eauto.
+Qed.
+
+(*
+Lemma in_subdivs_intv P Ps E :
+  covers P Ps = true ->
+  (forall (x : nat) (iv : intv),
+      In (Var Q x, iv) P ->
+      exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R) ->
+  exists P', In P' Ps /\
+        (forall (x : nat) (iv : intv),
+            In (Var Q x, iv) P' ->
+            exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R).
+Proof.
+  induction P as [|[e iv] P] in Ps |- *; intros chk H.
+  - destruct Ps as [|P' Ps]; cbn in chk; try discriminate chk.
+    exists P'; split; [now constructor |].
+    destruct P'; try discriminate chk. auto.
+  - cbn in chk.
+    destruct e; try discriminate chk.
+    destruct (mergeDim n  Ps) as [res| |] eqn:Hres; try discriminate chk.
+    apply andb_prop in chk as [rec curr].
+    destruct (H n iv) as [v [Hf Hc]]; try now constructor.
+    destruct (coverIntv_sound _ _ curr Hc) as [iv' [Hin Hc']].
+    apply in_map_iff in Hin as [[iv0 b] [Hiv0 Hin]].
+    cbn in *; subst.
+    eapply forallb_forall in rec; [| apply in_map_iff; eauto].
+    destruct (IHP _ rec) as [P' [inb valid_P']]; auto.
+    destruct (mergeDim_sound _ _ Hres _ _ _ Hin inb) as [iv0 [inPs Hsub]].
+    eexists; split; eauto.
+    intros x iv1 [Heq| inP'].
+    + inversion Heq; subst.
+      eexists; split; eauto.
+      Flover_compute.
+      canonize_hyps.
+      cbn in *. lra.
+    + auto.
+Qed.
+*)
+
+Definition checkPreconds (subdivs: list precond) (P: precond) :=
+  let Piv := FloverMap.elements (fst P) in
+  let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
+  covers Piv Ps && true. (* TODO check additional constraints *)
+
+Lemma checkPreconds_sound (subdivs: list (precond * analysisResult)) E P :
+  checkPreconds (map fst subdivs) P = true ->
+  eval_precond E P ->
+  exists PA, In PA subdivs /\ eval_precond E (fst PA).
+Proof.
+  intros H [Pintv Hadd].
+  andb_to_prop H.
+  eapply covers_sound in L; eauto.
+  destruct L as [Pl1 [Hin H]].
+  apply in_map_iff in Hin as [P1 [Heq1 Hin]].
+  apply in_map_iff in Hin as [PA1 [Heq2 Hin]].
+  exists PA1. split; auto.
+  split.
+  - rewrite Heq2.
+    now rewrite <- Heq1 in H.
+  - rewrite Heq2. admit. (* snd P == snd P1 should hold *)
+Admitted.
+
+(* 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) &&
+           checkPreconds (map fst (hd :: tl)) 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 chk.
+  apply andb_prop in chk as [chk valid_subdivs].
+  apply andb_prop in chk as [valid_ssa valid_cover].
+  apply (checkPreconds_sound (hd_subdivs :: tl_subdivs)) in P_valid as [[P' A] [in_subdivs P_valid]]; auto.
+  (* 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