Prove error bounds statement for RoundoffErrorValidator

coq/ErrorAnalysis.v

@@ -2,57 +2,39 @@ From Coq
      Require Import Reals.Reals QArith.Qreals.
 
 From Flover
-     Require Import ExpressionSemantics Environments RealRangeArith TypeValidator.
+     Require Import ExpressionSemanticsDeterministic Environments RealRangeArith TypeValidator.
 
-Definition eval_Real E1 Gamma (e:expr Q) nR :=
-  eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) nR REAL.
-
-Arguments eval_Real _ _ _ _/.
-
-Definition eval_Fin E2 Gamma (e:expr Q) nF m :=
-  eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m.
-
-Arguments eval_Fin _ _ _ _ _/.
-
-Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma fVars dVars :Prop :=
+Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
   (match e with
-  | Unop u e => validErrorBounds e E1 E2 A Gamma fVars dVars
-  | Downcast m e => validErrorBounds e E1 E2 A Gamma fVars dVars
+  | Unop u e => validErrorBounds e E1 E2 A Gamma DeltaMap
+  | Downcast m e => validErrorBounds e E1 E2 A Gamma DeltaMap
   | Binop b e1 e2 =>
-    validErrorBounds e1 E1 E2 A Gamma fVars dVars /\
-    validErrorBounds e2 E1 E2 A Gamma fVars dVars
+    validErrorBounds e1 E1 E2 A Gamma DeltaMap /\
+    validErrorBounds e2 E1 E2 A Gamma DeltaMap
   | Fma e1 e2 e3 =>
-    validErrorBounds e1 E1 E2 A Gamma fVars dVars /\
-    validErrorBounds e2 E1 E2 A Gamma fVars dVars /\
-    validErrorBounds e3 E1 E2 A Gamma fVars dVars
+    validErrorBounds e1 E1 E2 A Gamma DeltaMap /\
+    validErrorBounds e2 E1 E2 A Gamma DeltaMap /\
+    validErrorBounds e3 E1 E2 A Gamma DeltaMap
   | _ => True
    end)  /\
-  forall v__R iv err,
-    validTypes e Gamma ->
-    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
-    NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
-    eval_Real E1 Gamma e v__R ->
-    validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
+  forall v__R (iv: intv) (err: error),
+    eval_expr_det E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
     FloverMap.find e A = Some (iv, err) ->
     (exists v__FP m__FP,
-      eval_expr E2 (toRExpMap Gamma) (toRExp e) v__FP m__FP) /\
+      eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
     (forall v__FP m__FP,
-        eval_expr E2 (toRExpMap Gamma) (toRExp e) v__FP m__FP ->
+        eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
         (Rabs (v__R - v__FP) <= (Q2R err))%R).
 
-Lemma validErrorBounds_single e E1 E2 A Gamma fVars dVars:
-  validErrorBounds e E1 E2 A Gamma fVars dVars ->
+Lemma validErrorBounds_single e E1 E2 A Gamma DeltaMap:
+  validErrorBounds e E1 E2 A Gamma DeltaMap ->
   forall v__R iv err,
-    validTypes e Gamma ->
-    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
-    NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
-    eval_Real E1 Gamma e v__R ->
-    validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
+    eval_expr_det E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
     FloverMap.find e A = Some (iv, err) ->
     (exists v__FP m__FP,
-      eval_expr E2 (toRExpMap Gamma) (toRExp e) v__FP m__FP) /\
+      eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
     (forall v__FP m__FP,
-        eval_expr E2 (toRExpMap Gamma) (toRExp e) v__FP m__FP ->
+        eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
         (Rabs (v__R - v__FP) <= (Q2R err))%R).
 Proof.
   intros validError_e;

coq/ErrorValidationAA.v

@@ -4633,17 +4633,124 @@ Proof.
   - apply validErrorboundAA_sound_downcast; auto.
 Qed.
 
-Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap fVars dVars:
-  validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars ->
-  validErrorBounds e E1 E2 A Gamma fVars dVars.
+Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_map noise noise_map:
+  (forall e' : FloverMap.key,
+      FloverMap.In e' expr_map ->
+      (exists (v__FP' : R) (m__FP' : mType),
+          eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') /\
+      checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map noise expr_map) ->
+  contained_subexpr e expr_map ->
+  validErrorBounds e E1 E2 A Gamma DeltaMap.
 Proof.
-  induction e; intros Hvalidbounds.
+  induction e; intros Hchecked Hsubexpr.
+  - split; [trivial|].
+    intros * Heval__R Hcert.
+    specialize Hsubexpr as (_ & Hsubexpr).
+    specialize Hchecked as (Hex & Hall); eauto.
+    intuition.
+    specialize Hall as (? & ? & ?); eauto.
+    intuition.
+    eapply Rle_trans; eauto.
+    match goal with
+    | H: af_evals _ _ _ |- _ => apply to_interval_containment in H; rename H into Hiv
+    end.
+    match goal with
+    | H: toInterval _ = _ |- _ => rewrite H in Hiv
+    end.
+    cbn in Hiv.
+    now rewrite Rabs_Rle_condition.
   - split; [trivial|].
-    admit.
-  - admit.
-  - admit.
-  -
-Admitted.
+    intros * Heval__R Hcert.
+    specialize Hsubexpr as (_ & Hsubexpr).
+    specialize Hchecked as (Hex & Hall); eauto.
+    intuition.
+    specialize Hall as (? & ? & ?); eauto.
+    intuition.
+    eapply Rle_trans; eauto.
+    match goal with
+    | H: af_evals _ _ _ |- _ => apply to_interval_containment in H; rename H into Hiv
+    end.
+    match goal with
+    | H: toInterval _ = _ |- _ => rewrite H in Hiv
+    end.
+    cbn in Hiv.
+    now rewrite Rabs_Rle_condition.
+  - cbn.
+    specialize (IHe Hchecked).
+    specialize Hsubexpr as (Hsubexpr & Hin).
+    split; auto.
+    intros * Heval__R Hcert.
+    specialize Hchecked as (Hex & Hall); eauto.
+    intuition.
+    specialize Hall as (? & ? & ?); eauto.
+    intuition.
+    eapply Rle_trans; eauto.
+    match goal with
+    | H: af_evals _ _ _ |- _ => apply to_interval_containment in H; rename H into Hiv
+    end.
+    match goal with
+    | H: toInterval _ = _ |- _ => rewrite H in Hiv
+    end.
+    cbn in Hiv.
+    now rewrite Rabs_Rle_condition.
+  - cbn.
+    specialize (IHe1 Hchecked).
+    specialize (IHe2 Hchecked).
+    specialize Hsubexpr as ((Hsubexpr1 & Hsubexpr2) & Hin).
+    split; auto.
+    intros * Heval__R Hcert.
+    specialize Hchecked as (Hex & Hall); eauto.
+    intuition.
+    specialize Hall as (? & ? & ?); eauto.
+    intuition.
+    eapply Rle_trans; eauto.
+    match goal with
+    | H: af_evals _ _ _ |- _ => apply to_interval_containment in H; rename H into Hiv
+    end.
+    match goal with
+    | H: toInterval _ = _ |- _ => rewrite H in Hiv
+    end.
+    cbn in Hiv.
+    now rewrite Rabs_Rle_condition.
+  - cbn.
+    specialize (IHe1 Hchecked).
+    specialize (IHe2 Hchecked).
+    specialize (IHe3 Hchecked).
+    specialize Hsubexpr as ((Hsubexpr1 & Hsubexpr2 & Hsubexpr3) & Hin).
+    split; auto.
+    intros * Heval__R Hcert.
+    specialize Hchecked as (Hex & Hall); eauto.
+    intuition.
+    specialize Hall as (? & ? & ?); eauto.
+    intuition.
+    eapply Rle_trans; eauto.
+    match goal with
+    | H: af_evals _ _ _ |- _ => apply to_interval_containment in H; rename H into Hiv
+    end.
+    match goal with
+    | H: toInterval _ = _ |- _ => rewrite H in Hiv
+    end.
+    cbn in Hiv.
+    now rewrite Rabs_Rle_condition.
+  - cbn.
+    specialize (IHe Hchecked).
+    specialize Hsubexpr as (Hsubexpr & Hin).
+    split; auto.
+    intros * Heval__R Hcert.
+    specialize Hchecked as (Hex & Hall); eauto.
+    intuition.
+    specialize Hall as (? & ? & ?); eauto.
+    intuition.
+    eapply Rle_trans; eauto.
+    match goal with
+    | H: af_evals _ _ _ |- _ => apply to_interval_containment in H; rename H into Hiv
+    end.
+    match goal with
+    | H: toInterval _ = _ |- _ => rewrite H in Hiv
+    end.
+    cbn in Hiv.
+    now rewrite Rabs_Rle_condition.
+Qed.
 
 Lemma validErrorboundAACmd_sound c:
   forall E1 E2 A Gamma DeltaMap fVars dVars outVars

coq/RoundoffErrorValidator.v

@@ -2,7 +2,8 @@ From Coq
      Require Import Reals.Reals QArith.Qreals.
 
 From Flover
-     Require Export Infra.ExpressionAbbrevs ErrorValidation ErrorValidationAA RealRangeValidator
+     Require Export Infra.ExpressionAbbrevs ErrorAnalysis ErrorValidation
+     ErrorValidationAA ExpressionSemanticsDeterministic RealRangeValidator
      TypeValidator Environments.
 
 Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType)
@@ -17,22 +18,47 @@ Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType)
 
 Theorem RoundoffErrorValidator_sound:
   forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
-    (nR : R) (err : error) (elo ehi : Q) (Gamma : FloverMap.t mType),
+    (nR : R) (err : error) (iv : intv) (Gamma : FloverMap.t mType) DeltaMap,
+    (forall (e' : expr R) (m' : mType),
+        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
     validTypes e Gamma ->
     approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
     NatSet.Subset (usedVars e -- dVars) fVars ->
-    eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) nR REAL ->
+    eval_expr_det E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) nR REAL ->
     RoundoffErrorValidator e Gamma A dVars = true ->
     validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
-    FloverMap.find (elt:=intv * error) e A = Some (elo, ehi, err) ->
-    (exists (nF : R) (m : mType),
-        eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m) /\
-    (forall (nF : R) (m : mType),
-        eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m ->
-        (Rabs (nR - nF) <= Q2R err)%R).
+    FloverMap.find e A = Some (iv, err) ->
+    dVars_contained dVars (FloverMap.empty (affine_form Q)) ->
+    validErrorBounds e E1 E2 A Gamma DeltaMap.
 Proof.
-  intros. cbn in *.
-  eapply validErrorbound_sound; eauto.
+  unfold RoundoffErrorValidator.
+  intros; cbn in *.
+  destruct (validErrorbound e Gamma A dVars) eqn: Hivvalid.
+  - admit.
+    (* eapply validErrorbound_sound; eauto. *)
+  - 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.
+    specialize (Hsubexpr e Gamma A dVars 1%nat noise (FloverMap.empty (affine_form Q)) expr_map).
+    specialize Hsubexpr as (Hsubexpr & Hcont & Hcheckedsubexpr); eauto;
+      [intros ? Hin; now rewrite FloverMapFacts.P.F.empty_in_iff in Hin|].
+    pose proof validErrorboundAA_sound as Hvalidbound.
+    specialize (Hvalidbound e E1 E2 A Gamma DeltaMap fVars dVars).
+    specialize Hvalidbound as (Hex & Hall); eauto.
+    + instantiate (1 := fun x => None); auto.
+    + intros ? Hin.
+      now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+    + intros ? Hin.
+      now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+    + specialize Hex as ((v__e & m__e & Hev) & Hexchecked).
+      specialize (Hall v__e m__e Hev) as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & Hall).
+      eapply validErrorbound_sound_validErrorBounds; eauto.
+      intros e' Hin.
+      specialize Hexchecked as (_ & Hex); eauto;
+        [now rewrite FloverMapFacts.P.F.empty_in_iff|].
+      split; eauto.
+      eapply Hall; eauto; now rewrite FloverMapFacts.P.F.empty_in_iff.
 Admitted.
 
 Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)