clearer structure for result checker soundness

coq/CertificateChecker.v

@@ -51,6 +51,6 @@ Proof.
   unfold CertificateChecker in certificate_valid.
   destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
   destruct subdivs.
-  - eapply result_checking_is_sound; eauto.
-  - eapply subdivs_checking_is_sound; eauto.
+  - eapply result_checking_sound_single; eauto.
+  - eapply subdivs_checking_sound; eauto.
 Qed.

coq/ResultChecker.v

@@ -3,45 +3,41 @@ From Flover
      Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
      Environments TypeValidator FPRangeValidator ExpressionAbbrevs.
 
+Definition RangeErrorChecker (e: expr Q) (absenv: analysisResult)
+           (P: precond) Qmap (defVars: FloverMap.t  mType) Gamma :=
+  RangeValidator e absenv P Qmap NatSet.empty &&
+                 FPRangeValidator e absenv Gamma NatSet.empty &&
+                 RoundoffErrorValidator e Gamma absenv NatSet.empty.
+
 (** 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.
+  validSSA e (preVars P) && RangeErrorChecker e absenv P Qmap defVars Gamma.
 
 (**
    Soundness proof for the result checker.
 **)
-Theorem result_checking_is_sound (e: expr Q) (absenv: analysisResult) P Qmap defVars Gamma:
+Theorem result_checking_sound (e: expr Q) (absenv: analysisResult) P Qmap defVars Gamma:
   forall (E1 E2: env) DeltaMap,
+    approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
     (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.
+    validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\ validErrorBounds e E1 E2 absenv Gamma DeltaMap.
 (**
    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.
+  intros * approxE1E2 deltas_matched P_valid unsat_qs valid_typeMap results_valid.
+  unfold ResultChecker in results_valid.
   assert (validTypes e Gamma).
   { eapply getValidMap_top_correct; eauto.
     intros. cbn in *; congruence. }
-  andb_to_prop certificate_valid.
+  andb_to_prop results_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).
@@ -56,7 +52,8 @@ Proof.
   assert (NatSet.Subset (freeVars e -- NatSet.empty) (freeVars e)).
   { hnf; intros a in_empty.
     set_tac. }
-  rename R0 into validFPRanges.
+  rename R into validFPRanges.
+  rename R0 into validRoundoffErr.
   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
@@ -71,19 +68,48 @@ Proof.
   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.
+  split; auto.
+  eapply RoundoffErrorValidator_sound; eauto.
+Qed.
+
+(**
+   Soundness proof for the result checker.
+**)
+Corollary result_checking_sound_single (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.
+Proof.
+  intros * deltas_matched P_valid unsat_qs valid_typeMap results_valid.
+  exists Gamma; intros approxE1E2.
+  assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as validRange
+      by (eapply result_checking_sound; eauto).
+  assert (validErrorBounds e E1 E2 absenv Gamma DeltaMap) as Hsound
+      by (eapply result_checking_sound; eauto).
+  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.
-  exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
+  exists iv, err, vR, vF, mF; repeat split; auto.
 Qed.
 
 (*