Merge branch 'errors_affine' into 'master'

Rework type for delta map and fix issue #13

Closes #13

See merge request AVA/FloVer!18

coq/CertificateChecker.v

@@ -30,8 +30,8 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
 **)
 Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
   forall (E1 E2:env) DeltaMap,
-    (forall (e' : expr R) (m' : mType),
-        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    (forall (v : R) (m' : mType),
+        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
     (forall v, NatSet.In v (Expressions.usedVars e) ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
@@ -81,10 +81,10 @@ Proof.
   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).
-  pose proof (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H1 eval_real R
+  pose proof (RoundoffErrorValidator_sound e H approxE1E2 H1 eval_real R
                                           valid_e map_e Hdvars) as Hsound.
   unfold validErrorBounds in Hsound.
-  eapply validErrorBounds_single in Hsound; eauto.
+  eapply validErrorBoundsRec_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.
@@ -106,8 +106,8 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
 Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
         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) ->
+    (forall (v : R) (m' : mType),
+        exists d : R, DeltaMap v  m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
     (forall v, NatSet.In v (freeVars f) ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
@@ -158,7 +158,7 @@ Proof.
   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.
+  eapply validErrorBoundsCmdRec_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.

coq/Commands.v

@@ -48,7 +48,7 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
   Define big step semantics for the Flover language, terminating on a "returned"
   result value
  **)
-Inductive bstep : cmd R -> env -> (expr R -> option mType) -> (expr R -> mType -> option R) ->
+Inductive bstep : cmd R -> env -> (expr R -> option mType) -> (R -> mType -> option R) ->
                   R -> mType -> Prop :=
   let_b m m' x e s E v res defVars DeltaMap:
     eval_expr E defVars DeltaMap e v m ->

coq/ErrorAnalysis.v

@@ -4,17 +4,17 @@ From Coq
 From Flover
      Require Import Commands ExpressionSemantics Environments RealRangeArith TypeValidator.
 
-Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
+Fixpoint validErrorBoundsRec (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
   (match e with
-  | Unop u e => validErrorBounds e E1 E2 A Gamma DeltaMap
-  | Downcast m e => validErrorBounds e E1 E2 A Gamma DeltaMap
+  | Unop u e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
+  | Downcast m e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
   | Binop b e1 e2 =>
-    validErrorBounds e1 E1 E2 A Gamma DeltaMap /\
-    validErrorBounds e2 E1 E2 A Gamma DeltaMap
+    validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
+    validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap
   | Fma e1 e2 e3 =>
-    validErrorBounds e1 E1 E2 A Gamma DeltaMap /\
-    validErrorBounds e2 E1 E2 A Gamma DeltaMap /\
-    validErrorBounds e3 E1 E2 A Gamma DeltaMap
+    validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
+    validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap /\
+    validErrorBoundsRec e3 E1 E2 A Gamma DeltaMap
   | _ => True
    end)  /\
   forall v__R (iv: intv) (err: error),
@@ -26,8 +26,14 @@ Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
         eval_expr 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 DeltaMap:
-  validErrorBounds e E1 E2 A Gamma DeltaMap ->
+Definition validErrorBounds e E1 E2 A Gamma: Prop :=
+  forall DeltaMap,
+    (forall (v : R) (m' : mType),
+        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    validErrorBoundsRec e E1 E2 A Gamma DeltaMap.
+
+Lemma validErrorBoundsRec_single e E1 E2 A Gamma DeltaMap:
+  validErrorBoundsRec e E1 E2 A Gamma DeltaMap ->
   forall v__R iv err,
     eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
     FloverMap.find e A = Some (iv, err) ->
@@ -39,13 +45,13 @@ Lemma validErrorBounds_single e E1 E2 A Gamma DeltaMap:
 Proof.
   intros validError_e;
     intros;  destruct e; cbn in *; split;
-      destruct validError_e as (? & ? & ?); eauto.
+      edestruct validError_e as (? & ? & ?); eauto.
 Qed.
 
-Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
+Fixpoint validErrorBoundsCmdRec (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
   match c with
   | Let m x e k =>
-    validErrorBounds e E1 E2 A Gamma DeltaMap /\
+    validErrorBoundsRec e E1 E2 A Gamma DeltaMap /\
     (exists iv_e err_e iv_x err_x,
        FloverMap.find e A = Some (iv_e, err_e) /\
        FloverMap.find (Var Q x) A = Some (iv_x, err_x) /\
@@ -53,8 +59,8 @@ Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
     (forall v__R v__FP,
         eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
         eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
-        validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
-  | Ret e => validErrorBounds e E1 E2 A Gamma DeltaMap
+        validErrorBoundsCmdRec k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
+  | Ret e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
   end  /\
   forall v__R (iv: intv) (err: error),
     bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
@@ -65,8 +71,14 @@ Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
         bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
         (Rabs (v__R - v__FP) <= (Q2R err))%R).
 
-Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap:
-  validErrorBoundsCmd c E1 E2 A Gamma DeltaMap ->
+Definition validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma: Prop :=
+  forall DeltaMap,
+    (forall (v : R) (m' : mType),
+        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    validErrorBoundsCmdRec c E1 E2 A Gamma DeltaMap.
+
+Lemma validErrorBoundsCmdRec_single c E1 E2 A Gamma DeltaMap:
+  validErrorBoundsCmdRec c E1 E2 A Gamma DeltaMap ->
   forall v__R (iv: intv) (err: error),
     bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
     FloverMap.find (getRetExp c) A = Some (iv, err) ->
@@ -78,5 +90,5 @@ Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap:
 Proof.
   intros validError_e;
     intros;  destruct c; cbn in *; split;
-      destruct validError_e as (? & ? & ?); eauto.
+      edestruct validError_e as (? & ? & ?); eauto.
 Qed.

coq/ErrorBounds.v

@@ -43,8 +43,8 @@ Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
             (updDefVars (Binop Plus (Var R 1) (Var R 2)) m
                         (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
-            (fun x _ => if R_orderedExps.eq_dec x (Binop Plus (Var R 1) (Var R 2))
-                     then DeltaMap (Binop Plus (toRExp e1) (toRExp e2)) m
+            (fun x _ => if Req_dec_sum x (evalBinop Plus e1F e2F)
+                     then DeltaMap (evalBinop Plus e1F e2F) m
                      else None)
             (Binop Plus (Var R 1) (Var R 2)) vF m ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
@@ -116,8 +116,8 @@ Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
             (updDefVars (Binop Sub (Var R 1) (Var R 2)) m
                         (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
-            (fun x _ => if R_orderedExps.eq_dec x (Binop Sub (Var R 1) (Var R 2))
-                     then DeltaMap (Binop Sub (toRExp e1) (toRExp e2)) m
+            (fun x _ => if Req_dec_sum x (evalBinop Sub e1F e2F)
+                     then DeltaMap (evalBinop Sub e1F e2F) m
                      else None)
             (Binop Sub (Var R 1) (Var R 2)) vF m ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
@@ -194,8 +194,8 @@ Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
             (updDefVars (Binop Mult (Var R 1) (Var R 2)) m
                         (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
-            (fun x _ => if R_orderedExps.eq_dec x (Binop Mult (Var R 1) (Var R 2))
-                     then DeltaMap (Binop Mult (toRExp e1) (toRExp e2)) m
+            (fun x _ => if Req_dec_sum x (evalBinop Mult e1F e2F)
+                     then DeltaMap (evalBinop Mult e1F e2F) m
                      else None)
             (Binop Mult (Var R 1) (Var R 2)) vF m ->
   (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
@@ -245,8 +245,8 @@ Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
             (updDefVars (Binop Div (Var R 1) (Var R 2)) m
                         (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
-            (fun x _ => if R_orderedExps.eq_dec x (Binop Div (Var R 1) (Var R 2))
-                     then DeltaMap (Binop Div (toRExp e1) (toRExp e2)) m
+            (fun x _ => if Req_dec_sum x (evalBinop Div e1F e2F)
+                     then DeltaMap (evalBinop Div e1F e2F) m
                      else None)
             (Binop Div (Var R 1) (Var R 2)) vF m ->
   (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
@@ -301,8 +301,8 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
             (updDefVars (Fma (Var R 1) (Var R 2) (Var R 3)) m
                         (updDefVars (Var R 3) m3
                                     (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))))
-            (fun x _ => if R_orderedExps.eq_dec x (Fma (Var R 1) (Var R 2) (Var R 3))
-                     then DeltaMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) m
+            (fun x _ => if Req_dec_sum x (evalFma e1F e2F e3F)
+                     then DeltaMap (evalFma e1F e2F e3F) m
                      else None)
             (Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
   (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + computeErrorR (e1F + e2F * e3F ) m)%R.
@@ -366,8 +366,8 @@ Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
   eval_expr (updEnv 1 nF1 emptyEnv)
             (updDefVars (Downcast mEps (Var R 1)) mEps
                         (updDefVars (Var R 1) m defVars))
-            (fun x _ => if R_orderedExps.eq_dec x (Downcast mEps (Var R 1))
-                     then DeltaMap (Downcast mEps e) mEps
+            (fun x _ => if Req_dec_sum x nF1
+                     then DeltaMap nF1 mEps
                      else None)
             (toRExp (Downcast mEps (Var Q 1))) nF mEps->
   (Rabs (nR - nF1) <= err)%R ->

coq/ErrorValidationAA.v

@@ -236,6 +236,11 @@ Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
   | Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
   end.
 
+(* Notation for the universal case of the soundness statement, to help reason
+   about memoization cases. This allows us to show several monotonicity lemmas
+   that simplify the soundness proofs. This definition is just an extract from
+   the full soundness statement, for elaboration on the used assumptions and the
+   goal, find that statement below *)
 Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap
            noise_map noise expr_map :=
   forall v__R v__FP m__FP (iv__A: intv) (err__A: error),
@@ -777,12 +782,17 @@ Proof.
       * apply flover_map_in_add.
 Qed.
 
+(* The soundness statements starts off with assumption that the checking
+   function succeeds and then also maintains several invariants. We require
+   these invariants because of the checker function dependency on the current
+   noise index and its memoization of the previosly computed polynomials. We
+   explain these invariants in-line below. *)
 Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars :=
   forall (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
     (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
     (iv__A : intv) (err__A : error),
-    (forall (e' : expr R) (m' : mType),
-        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    (forall (v : R) (m' : mType),
+        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
     approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
     eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
     validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
@@ -790,39 +800,74 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
     NatSet.Subset (usedVars e -- dVars) fVars ->
     validTypes e Gamma ->
     FloverMap.find e A = Some (iv__A, err__A) ->
+    (* Starting noise index is greater than 0 and the noise mapping doesn't
+       map it and anything above to a noise value *)
     (0 < noise1)%nat ->
     (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
+    (* If a var is a dVar, we know it's in expr_map and invoke the corresponding
+     preconditions (described below) *)
     dVars_contained dVars expr_map1 ->
+    (* Precondition:
+       Memoization for the existential case of the goal: if we checked the expression
+       already, we know that there is an execution and certificate results for it *)
     (forall e' : FloverMap.key,
         FloverMap.In e' expr_map1 ->
+        (* Assumption needed for Cmd_sound proof *)
         NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
         (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
         exists (v__FP' : R) (m__FP' : mType),
           eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
+    (* Precondition:
+       Memoization for the universal case of the goal -- note that
+       `checked_error_expressions` track only that case: if we checked
+       the expression already, then, if we provide the execution in
+       finite precision and the certificate results, we will know that
+       the execution's error is bounded *)
     (forall e' : FloverMap.key,
         FloverMap.In e' expr_map1 ->
         checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
+    (* THE EXESTENTIAL CASE OF THE GOAL *)
     ((exists (v__FP : R) (m__FP : mType),
          eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
+     (* Invariant of the existential case:
+        our given expr_map1 is updated only with the expressions for which
+        the existential part holds *)
      (forall e' : FloverMap.key,
          ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
          NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
          (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
          exists (v__FP' : R) (m__FP' : mType),
            eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP')) /\
+    (* UNIVERSAL CASE OF THE GOAL *)
     (forall (v__FP : R) (m__FP : mType),
         eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
+        (* For the given evaluation we can find a polynomial and an
+           error bound with a monotonic extension of noise_map1 to
+           noise_map2 *)
         exists (af : affine_form Q) (err__af : R) (noise_map2 : noise_mapping),
+          (* Invariant: the checker function only adds new polynomials
+             to the expr_map, never removes something from it *)
           contained_flover_map expr_map1 expr_map2 /\
+          (* Noise index invariants: the checker function returns new
+             noise that is not used in already produced polynomials *)
           (noise1 <= noise2)%nat /\
           fresh noise2 (afQ2R af) /\
+          (* Invariant: noise_map is incrementally updated *)
           contained_map noise_map1 noise_map2 /\
           (forall n0 : nat, (n0 >= noise2)%nat -> noise_map2 n0 = None) /\
           FloverMap.find (elt:=affine_form Q) e expr_map2 = Some af /\
+          (* To show that the error is bounded by the polynomial, we say that
+             the polynomial's range is bounded by err__af, which has a value
+             less or equal to the certificate error, and that the polynomial
+             captures any difference between real and finite-precision
+             evaluations *)
           (0 <= err__af)%R /\
           toInterval (afQ2R af) = ((- err__af)%R, err__af) /\
           (err__af <= Q2R err__A)%R /\
           af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\
+          (* Invariant of the universal case:
+             our given expr_map1 is updated only with the expressions for which
+             the universal part (the conclusion directly above) holds *)
           (forall e' : FloverMap.key,
               ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
               checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)).
@@ -1008,7 +1053,7 @@ Proof.
                eval_expr E2 (toRExpMap Gamma) DeltaMap
                              (toRExp (Expressions.Const m v)) v__FP m__FP).
     {
-      specialize (Hdeltamap (toRExp (Expressions.Const m v)) m)
+      specialize (Hdeltamap (Q2R v) m)
         as (delta' & Hdelta & Hdelta').
       exists (perturb (Q2R v) m delta'), m.
       eapply Const_dist' with (delta := delta'); auto.
@@ -1351,7 +1396,7 @@ Proof.
     assert (exists (v__FP : R) (m__FP : mType),
                eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Plus e1 e2)) v__FP m__FP) as H.
     {
-      specialize (Hdeltamap (toRExp (Binop Plus e1 e2)) m__e)
+      specialize (Hdeltamap (evalBinop Plus nF1 nF2) m__e)
         as (delta' & Hdelta & Hdelta').
       eexists; exists m__e.
       eapply Binop_dist' with (delta := delta'); eauto.
@@ -1615,7 +1660,7 @@ Proof.
     assert (exists (v__FP : R) (m__FP : mType),
                eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Sub e1 e2)) v__FP m__FP).
     {
-      specialize (Hdeltamap (toRExp (Binop Sub e1 e2)) m__e)
+      specialize (Hdeltamap (evalBinop Sub nF1 nF2) m__e)
         as (delta' & Hdelta & Hdelta').
       eexists; exists m__e.
       eapply Binop_dist' with (delta := delta'); eauto.
@@ -1867,7 +1912,7 @@ Proof.
     assert (exists (v__FP : R) (m__FP : mType),
                eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Mult e1 e2)) v__FP m__FP).
     {
-      specialize (Hdeltamap (toRExp (Binop Mult e1 e2)) m__e)
+      specialize (Hdeltamap (evalBinop Mult nF1 nF2) m__e)
         as (delta' & Hdelta & Hdelta').
       eexists; exists m__e.
       eapply Binop_dist' with (delta := delta'); eauto.
@@ -2180,7 +2225,7 @@ Proof.
     assert (exists (v__FP : R) (m__FP : mType),
                eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Div e1 e2)) v__FP m__FP).
     {
-      specialize (Hdeltamap (toRExp (Binop Div e1 e2)) m__e)
+      specialize (Hdeltamap (evalBinop Div nF1 nF2) m__e)
         as (delta' & Hdelta & Hdelta').
       eexists; exists m__e.
       eapply Binop_dist' with (delta := delta'); eauto.
@@ -2578,7 +2623,7 @@ Proof.
     assert (exists (v__FP : R) (m__FP : mType),
                eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Fma e1 e2 e3)) v__FP m__FP).
     {
-      specialize (Hdeltamap (toRExp (Fma e1 e2 e3)) m__e)
+      specialize (Hdeltamap (evalFma nF1 nF2 nF3) m__e)
         as (delta' & Hdelta & Hdelta').
       eexists; exists m__e.
       eapply Fma_dist' with (delta:= delta'); eauto.
@@ -2879,7 +2924,7 @@ Proof.
     assert (exists (v__FP : R) (m__FP : mType),
                eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Downcast m__e e)) v__FP m__FP).
     {
-      specialize (Hdeltamap (toRExp (Downcast m__e e)) m__e)
+      specialize (Hdeltamap nF m__e)
         as (delta' & Hdelta & Hdelta').
       exists (perturb nF m__e delta'), m__e.
       eapply Downcast_dist' with (delta := delta'); eauto.
@@ -3020,7 +3065,7 @@ Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_m
           eval_expr 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.
+  validErrorBoundsRec e E1 E2 A Gamma DeltaMap.
 Proof.
   induction e; intros Hchecked Hsubexpr.
   - split; [trivial|].
@@ -3058,6 +3103,7 @@ Proof.
   - cbn.
     specialize (IHe Hchecked).
     specialize Hsubexpr as (Hsubexpr & Hin).
+    unfold validErrorBounds in IHe.
     split; auto.
     intros * Heval__R Hcert.
     specialize Hchecked as (Hex & Hall); eauto.
@@ -3077,6 +3123,7 @@ Proof.
     specialize (IHe1 Hchecked).
     specialize (IHe2 Hchecked).
     specialize Hsubexpr as ((Hsubexpr1 & Hsubexpr2) & Hin).
+    unfold validErrorBounds in IHe1, IHe2.
     split; auto.
     intros * Heval__R Hcert.
     specialize Hchecked as (Hex & Hall); eauto.
@@ -3097,6 +3144,7 @@ Proof.
     specialize (IHe2 Hchecked).
     specialize (IHe3 Hchecked).
     specialize Hsubexpr as ((Hsubexpr1 & Hsubexpr2 & Hsubexpr3) & Hin).
+    unfold validErrorBounds in IHe1, IHe2, IHe3.
     split; auto.
     intros * Heval__R Hcert.
     specialize Hchecked as (Hex & Hall); eauto.
@@ -3115,6 +3163,7 @@ Proof.
   - cbn.
     specialize (IHe Hchecked).
     specialize Hsubexpr as (Hsubexpr & Hin).
+    unfold validErrorBounds in IHe.
     split; auto.
     intros * Heval__R Hcert.
     specialize Hchecked as (Hex & Hall); eauto.
@@ -3285,8 +3334,8 @@ Theorem validErrorboundAACmd_sound c:
   forall E1 E2 A Gamma DeltaMap fVars dVars outVars
     (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
     (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R),
-    (forall (e' : expr R) (m' : mType),
-        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    (forall (v : R) (m' : mType),
+        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
     approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
     bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
     validRangesCmd c A E1 (toRTMap (toRExpMap Gamma)) ->
@@ -3331,7 +3380,7 @@ Theorem validErrorboundAACmd_sound c:
           toInterval (afQ2R af) = ((- err__af)%R, err__af) /\
           (err__af <= Q2R err__A)%R /\
           af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\
-          validErrorBoundsCmd c E1 E2 A Gamma DeltaMap /\
+          validErrorBoundsCmdRec c E1 E2 A Gamma DeltaMap /\
           (forall e' : FloverMap.key,
               ~ FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
               FloverMap.In (elt:=affine_form Q) e' expr_map2 ->
@@ -3737,7 +3786,7 @@ Proof.
         replace m__FP0 with m__FP in * by eauto using bstep_Gamma_det.
         assert (v__FP0 = v__FP) by eauto using bstep_det.
         assert (v__R0 = v__R) by eauto using bstep_det.
-        cbn in Hcert.
+        cbn in Hcert'.
         assert (err = err__A) by congruence.
         subst.
         eapply Rle_trans; eauto.

coq/ExpressionSemantics.v

@@ -34,16 +34,16 @@ Open Scope R_scope.
 
 Inductive eval_expr (E:env)
           (Gamma: expr R -> option mType)
-          (DeltaMap: expr R -> mType -> option R)
+          (DeltaMap: R -> mType -> option R)
   :(expr R) -> R -> mType -> Prop :=
 | Var_load m x v:
     Gamma (Var R x) = Some m ->
     E x = Some v ->
     eval_expr E Gamma DeltaMap (Var R x) v m
-| Const_dist m n delta:
-    DeltaMap (Const m n) m = Some delta ->
+| Const_dist m c delta:
+    DeltaMap c m = Some delta ->
     Rabs delta <= mTypeToR m ->
-    eval_expr E Gamma DeltaMap (Const m n) (perturb n m delta) m
+    eval_expr E Gamma DeltaMap (Const m c) (perturb c m delta) m
 | Unop_neg m mN f1 v1:
     Gamma (Unop Neg f1) = Some mN ->
     isCompat m mN = true ->
@@ -51,7 +51,7 @@ Inductive eval_expr (E:env)
     eval_expr E Gamma DeltaMap (Unop Neg f1) (evalUnop Neg v1) mN
 | Unop_inv m mN f1 v1 delta:
     Gamma (Unop Inv f1) = Some mN ->
-    DeltaMap (Unop Inv f1) mN = Some delta ->
+    DeltaMap (evalUnop Inv v1) mN = Some delta ->
     isCompat m mN = true ->
     Rabs delta <= mTypeToR mN ->
     eval_expr E Gamma DeltaMap f1 v1 m ->
@@ -59,14 +59,14 @@ Inductive eval_expr (E:env)
     eval_expr E Gamma DeltaMap (Unop Inv f1) (perturb (evalUnop Inv v1) mN delta) mN
 | Downcast_dist m m1 f1 v1 delta:
     Gamma (Downcast m f1) = Some m ->
-    DeltaMap (Downcast m f1) m = Some delta ->
+    DeltaMap v1 m = Some delta ->
     isMorePrecise m1 m = true ->
     Rabs delta <= mTypeToR m ->
     eval_expr E Gamma DeltaMap f1 v1 m1 ->
     eval_expr E Gamma DeltaMap (Downcast m f1) (perturb v1 m delta) m
 | Binop_dist m1 m2 op f1 f2 v1 v2 delta m:
     Gamma (Binop op f1 f2) = Some m ->
-    DeltaMap (Binop op f1 f2) m = Some delta ->
+    DeltaMap (evalBinop op v1 v2) m = Some delta ->
     isJoin m1 m2 m = true ->
     Rabs delta <= mTypeToR m ->
     eval_expr E Gamma DeltaMap f1 v1 m1 ->
@@ -75,7 +75,7 @@ Inductive eval_expr (E:env)
     eval_expr E Gamma DeltaMap (Binop op f1 f2) (perturb (evalBinop op v1 v2) m delta) m
 | Fma_dist m1 m2 m3 m f1 f2 f3 v1 v2 v3 delta:
     Gamma (Fma f1 f2 f3) = Some m ->
-    DeltaMap (Fma f1 f2 f3) m = Some delta ->
+    DeltaMap (evalFma v1 v2 v3) m = Some delta ->
     isJoin3 m1 m2 m3 m = true ->
     Rabs delta <= mTypeToR m ->
     eval_expr E Gamma DeltaMap f1 v1 m1 ->
@@ -83,7 +83,7 @@ Inductive eval_expr (E:env)
     eval_expr E Gamma DeltaMap f3 v3 m3 ->
     eval_expr E Gamma DeltaMap (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m.
 
-Definition DeltaMapR: expr R -> mType -> option R := (fun x m => Some 0).
+Definition DeltaMapR: R -> mType -> option R := (fun x m => Some 0).
 
 Close Scope R_scope.
 
@@ -92,12 +92,12 @@ Hint Constructors eval_expr.
 (** *)
 (*   Show some simpler (more general) rule lemmata *)
 (* **)
-Lemma Const_dist' DeltaMap m n delta v m' E Gamma:
+Lemma Const_dist' DeltaMap m c delta v m' E Gamma:
   Rle (Rabs delta) (mTypeToR m') ->
-  DeltaMap (Const m n) m = Some delta ->
-  v = perturb n m delta ->
+  DeltaMap c m = Some delta ->
+  v = perturb c m delta ->
   m' = m ->
-  eval_expr E Gamma DeltaMap (Const m n) v m'.
+  eval_expr E Gamma DeltaMap (Const m c) v m'.
 Proof.
   intros; subst; auto.
 Qed.
@@ -120,7 +120,7 @@ Hint Resolve Unop_neg'.
 Lemma Unop_inv' DeltaMap m mN f1 v1 delta v m' E Gamma:
   Rle (Rabs delta) (mTypeToR m') ->
   eval_expr E Gamma DeltaMap f1 v1 m ->
-  DeltaMap (Unop Inv f1) m' = Some delta ->
+  DeltaMap (evalUnop Inv v1) m' = Some delta ->
   (~ v1 = 0)%R  ->
   v = perturb (evalUnop Inv v1) mN delta ->
   Gamma (Unop Inv f1) = Some mN ->
@@ -137,7 +137,7 @@ Lemma Downcast_dist' DeltaMap m m1 f1 v1 delta v m' E Gamma:
   isMorePrecise m1 m = true ->
   Rle (Rabs delta) (mTypeToR m') ->
   eval_expr E Gamma DeltaMap f1 v1 m1 ->
-  DeltaMap (Downcast m f1) m' = Some delta ->
+  DeltaMap v1 m' = Some delta ->
   v = (perturb v1 m delta) ->
   Gamma (Downcast m f1) = Some m ->
   m' = m ->
@@ -152,7 +152,7 @@ Lemma Binop_dist' DeltaMap m1 m2 op f1 f2 v1 v2 delta v m m' E Gamma:
   Rle (Rabs delta) (mTypeToR m') ->
   eval_expr E Gamma DeltaMap f1 v1 m1 ->
   eval_expr E Gamma DeltaMap f2 v2 m2 ->
-  DeltaMap (Binop op f1 f2) m' = Some delta ->
+  DeltaMap (evalBinop op v1 v2) m' = Some delta ->
   ((op = Div) -> (~ v2 = 0)%R) ->
   v = perturb (evalBinop op v1 v2) m' delta ->
   Gamma (Binop op f1 f2) = Some m ->
@@ -170,7 +170,7 @@ Lemma Fma_dist' DeltaMap m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma m:
   eval_expr E Gamma DeltaMap f1 v1 m1 ->
   eval_expr E Gamma DeltaMap f2 v2 m2 ->
   eval_expr E Gamma DeltaMap f3 v3 m3 ->
-  DeltaMap (Fma f1 f2 f3) m' = Some delta ->
+  DeltaMap (evalFma v1 v2 v3) m' = Some delta ->
   v = perturb (evalFma v1 v2 v3) m' delta ->
   Gamma (Fma f1 f2 f3) = Some m ->
   isJoin3 m1 m2 m3 m = true ->
@@ -293,15 +293,15 @@ variables in the Environment.
 Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 m Gamma DeltaMap delta:
   (b = Div -> ~(v2 = 0 )%R) ->
   (Rabs delta <= mTypeToR m)%R ->
-  DeltaMap (Binop b f1 f2) m = Some delta ->
+  DeltaMap (evalBinop b v1 v2) m = Some delta ->
   eval_expr E Gamma DeltaMap f1 v1 m1 ->
   eval_expr E Gamma DeltaMap f2 v2 m2 ->
   eval_expr E Gamma DeltaMap (Binop b f1 f2) (perturb (evalBinop b v1 v2) m delta) m ->
   eval_expr (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
             (updDefVars (Binop b (Var R 1) (Var R 2)) m
                         (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 Gamma)))
-            (fun x _ => if R_orderedExps.eq_dec x (Binop b (Var R 1) (Var R 2))
-                     then DeltaMap (Binop b f1 f2) m
+            (fun x _ => if Req_dec_sum x (evalBinop b v1 v2)
+                     then DeltaMap (evalBinop b v1 v2) m
                      else None)
             (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) m delta) m.
 Proof.
@@ -319,15 +319,15 @@ Proof.
   eapply Binop_dist' with (v1:=v1) (v2:=v2) (delta:=delta); try eauto.
   - eapply Var_load; eauto.
   - eapply Var_load; eauto.
-  - destruct R_orderedExps.eq_dec as [?|H]; auto.
-    exfalso; apply H; apply R_orderedExps.eq_refl.
+  - destruct Req_dec_sum as [?|H]; auto.
+    exfalso; now apply H.
   - <