adding ErrorValidationAA again

coq/CertificateChecker.v

@@ -78,14 +78,10 @@ Proof.
     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 (validErrorBounds e E1 E2 absenv Gamma DeltaMap) as Hsound.
-  { eapply (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H1 eval_real _
-                                         valid_e map_e).
-    Unshelve. unfold RoundoffErrorValidator. now rewrite L. }
-  (* TODO: pose proof (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H1 eval_real _
-                                          valid_e map_e (*Hdvars*)) as Hsound. *)
+  assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars
+      by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac).
+  pose proof (RoundoffErrorValidator_sound e _ deltas_matched 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.
@@ -165,11 +161,10 @@ Proof.
 
   pose proof RoundoffErrorValidatorCmd_sound as Hsound.
   eapply validErrorBoundsCmd_single in Hsound; eauto.
-  (* 2: unfold dVars_contained; intros; set_tac.*)
   - 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 RoundoffErrorValidatorCmd. now rewrite L0.
+  - unfold dVars_contained; intros; set_tac.
 Qed.

coq/RoundoffErrorValidator.v

@@ -3,19 +3,18 @@ From Coq
 
 From Flover
      Require Export Infra.ExpressionAbbrevs ErrorAnalysis ErrorValidation
-     (* *) ExpressionSemantics RealRangeValidator
+     ErrorValidationAA ExpressionSemantics RealRangeValidator
      TypeValidator Environments.
-(* TODO: add ErrorValidationAA again *)
 
 Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType)
            (A:analysisResult) (dVars:NatSet.t) :=
   if
   validErrorbound e tMap A dVars
   then true
-  else false (* match validErrorboundAA e tMap A dVars 1 (FloverMap.empty (affine_form Q)) with
+  else match validErrorboundAA e tMap A dVars 1 (FloverMap.empty (affine_form Q)) with
        | Some _ => true
        | None => false
-       end *).
+       end.
 
 Theorem RoundoffErrorValidator_sound:
   forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
@@ -29,15 +28,14 @@ Theorem RoundoffErrorValidator_sound:
     RoundoffErrorValidator e Gamma A dVars = true ->
     validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
     FloverMap.find e A = Some (iv, err) ->
-    (* dVars_contained dVars (FloverMap.empty (affine_form Q)) -> *)
+    dVars_contained dVars (FloverMap.empty (affine_form Q)) ->
     validErrorBounds e E1 E2 A Gamma DeltaMap.
 Proof.
   unfold RoundoffErrorValidator.
   intros; cbn in *.
   destruct (validErrorbound e Gamma A dVars) eqn: Hivvalid.
   - eapply validErrorbound_sound; eauto.
-  - discriminate.
-    (* destruct (validErrorboundAA e Gamma A dVars 1 (FloverMap.empty (affine_form Q))) eqn: Hafvalid;
+  - destruct (validErrorboundAA e Gamma A dVars 1 (FloverMap.empty (affine_form Q))) eqn: Hafvalid;
       [|congruence].
     destruct p as (expr_map, noise).
     pose proof validErrorboundAA_contained_subexpr as Hsubexpr.
@@ -60,7 +58,6 @@ Proof.
         [now rewrite FloverMapFacts.P.F.empty_in_iff|].
       split; eauto.
       eapply Hall; eauto; now rewrite FloverMapFacts.P.F.empty_in_iff.
-*)
 Qed.
 
 Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
@@ -68,10 +65,10 @@ Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
   if
   validErrorboundCmd f tMap A dVars
   then true
-  else false (*match validErrorboundAACmd f tMap A dVars 1 (FloverMap.empty (affine_form Q)) with
+  else match validErrorboundAACmd f tMap A dVars 1 (FloverMap.empty (affine_form Q)) with
        | Some _ => true
        | None => false
-       end*).
+       end.
 
 Theorem RoundoffErrorValidatorCmd_sound f:
   forall A E1 E2 outVars fVars dVars Gamma DeltaMap v__R,
@@ -81,7 +78,7 @@ Theorem RoundoffErrorValidatorCmd_sound f:
     ssa f (NatSet.union fVars dVars) outVars ->
     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
     bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
-    (* dVars_contained dVars (FloverMap.empty (affine_form Q)) -> *)
+    dVars_contained dVars (FloverMap.empty (affine_form Q)) ->
     RoundoffErrorValidatorCmd f Gamma A dVars = true ->
     validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
     validTypesCmd f Gamma ->
@@ -91,8 +88,7 @@ Proof.
   unfold RoundoffErrorValidatorCmd in *.
   destruct (validErrorboundCmd f Gamma A dVars) eqn: Hivvalid.
   - eapply validErrorboundCmd_sound; eauto.
-  - discriminate.
-    (*destruct (validErrorboundAACmd f Gamma A dVars 1 (FloverMap.empty (affine_form Q)))
+  - destruct (validErrorboundAACmd f Gamma A dVars 1 (FloverMap.empty (affine_form Q)))
              eqn: Hvalid; [|congruence].
     destruct p as (expr_map2, noise2).
     edestruct validErrorboundAACmd_sound; eauto.
@@ -110,5 +106,4 @@ Proof.
       specialize (H9 v__FP m__FP iv__A err__A Heval Hcert).
       edestruct H9 as (? & ? & ? & ?); eauto.
       intuition.
-*)
 Qed.