preparing certificate checker for interval subdiv

coq/CertificateChecker.v

@@ -5,29 +5,24 @@
    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.
+     Require Import Infra.RealRationalProps Environments TypeValidator ResultChecker.
 
 Require Export ExpressionSemantics Coq.QArith.QArith Flover.SMTArith.
 
+(* TODO: add subdivs *)
 (** 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 =>
-   validSSA e (preVars P) &&
-            RangeValidator e absenv P Qmap NatSet.empty &&
-            FPRangeValidator e absenv tMap NatSet.empty &&
-            RoundoffErrorValidator e tMap absenv NatSet.empty
+  |Succes Gamma => ResultChecker e absenv P Qmap defVars Gamma
   | _ => 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.
+   the real valued execution respects the precondition.
 **)
 Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars:
   forall (E1 E2:env) DeltaMap,
@@ -45,142 +40,9 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap
         (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. }
-  andb_to_prop certificate_valid.
-  pose proof (NatSetProps.empty_union_2 (freeVars 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 (freeVars e -- NatSet.empty) (freeVars e)).
-  { hnf; intros a in_empty.
-    set_tac. }
-  rename R0 into validFPRanges.
-  pose proof (validSSA_checks_freeVars _ _ L) as sub.
-  destruct (validSSA_sound e (preVars P)) as [outVars ssa_e]; auto.
-  assert (validSSA e (freeVars e) = true) as ssa_valid
-      by (eapply validSSA_downward_closed; eauto using NatSetProps.subset_refl).
-  destruct (validSSA_sound e (freeVars e)) as [outVars2 ssa_e2]; eauto.
-  assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as valid_e.
-  { clear ssa_e2 outVars2 ssa_valid.
-    eapply (RangeValidator_sound (dVars:=NatSet.empty) (A:=absenv) (P:=P) (E:=E1) (fVars:=preVars P));
-      eauto using NatSetProps.subset_refl; set_tac.
-    eapply ssa_equal_set; eauto.
-    intros n. split; set_tac. intros [?|?]; auto. set_tac. }
-  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).
-*)
-  assert (ssa e (NatSet.union (freeVars e) (NatSet.empty)) outVars2).
-  { eapply ssa_equal_set; eauto. }
-  pose proof (RoundoffErrorValidator_sound _ deltas_matched H2 H approxE1E2 H1 eval_real R
-                                          valid_e map_e (* Hdvars *)) as Hsound.
-  unfold validErrorBounds in Hsound.
-  eapply validErrorBounds_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 (e' : expr R) (m' : mType),
-        exists d : R, DeltaMap e' 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 validErrorBoundsCmd_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.
+  eapply result_checking_is_sound; eauto.
 Qed.
-*)

coq/ResultChecker.v

+From Flover
+     Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
+     Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
+     Environments TypeValidator FPRangeValidator ExpressionAbbrevs.
+
+(** Result checking function **)
+Definition ResultChecker (e:expr Q) (absenv:analysisResult)
+           (P: precond) Qmap (defVars:FloverMap.t  mType) Gamma :=
+  validSSA e (preVars P) &&
+           RangeValidator e absenv P Qmap NatSet.empty &&
+           FPRangeValidator e absenv Gamma NatSet.empty &&
+           RoundoffErrorValidator e Gamma absenv NatSet.empty.
+
+(**
+   Soundness proof for the result checker.
+**)
+Theorem result_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap 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 ->
+    unsat_queries Qmap ->
+    getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
+    ResultChecker e absenv P Qmap 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.
+(**
+   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 valid_typeMap certificate_valid.
+  unfold ResultChecker in certificate_valid.
+  assert (validTypes e Gamma).
+  { eapply getValidMap_top_correct; eauto.
+    intros. cbn in *; congruence. }
+  andb_to_prop certificate_valid.
+  pose proof (NatSetProps.empty_union_2 (freeVars 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 (freeVars e -- NatSet.empty) (freeVars e)).
+  { hnf; intros a in_empty.
+    set_tac. }
+  rename R0 into validFPRanges.
+  pose proof (validSSA_checks_freeVars _ _ L) as sub.
+  destruct (validSSA_sound e (preVars P)) as [outVars ssa_e]; auto.
+  assert (validSSA e (freeVars e) = true) as ssa_valid
+      by (eapply validSSA_downward_closed; eauto using NatSetProps.subset_refl).
+  destruct (validSSA_sound e (freeVars e)) as [outVars2 ssa_e2]; eauto.
+  assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as valid_e.
+  { clear ssa_e2 outVars2 ssa_valid.
+    eapply (RangeValidator_sound (dVars:=NatSet.empty) (A:=absenv) (P:=P) (E:=E1) (fVars:=preVars P));
+      eauto using NatSetProps.subset_refl; set_tac.
+    eapply ssa_equal_set; eauto.
+    intros n. split; set_tac. intros [?|?]; auto. set_tac. }
+  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).
+*)
+  assert (ssa e (NatSet.union (freeVars e) (NatSet.empty)) outVars2).
+  { eapply ssa_equal_set; eauto. }
+  pose proof (RoundoffErrorValidator_sound _ deltas_matched H2 H approxE1E2 H1 eval_real R
+                                          valid_e map_e (* Hdvars *)) as Hsound.
+  unfold validErrorBounds in Hsound.
+  eapply validErrorBounds_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 (e' : expr R) (m' : mType),
+        exists d : R, DeltaMap e' 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 validErrorBoundsCmd_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.
+*)