ErrorValidationAA.v 180 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(**
   This file contains the coq implementation of the error bound validator as
   well as its soundness proof. The function validErrorbound is the Error bound
   validator from the certificate checking process. Under the assumption that a
   valid range arithmetic result has been computed, it can validate error bounds
   encoded in the analysis result. The validator is used in the file
   CertificateChecker.v to build the complete checker.
 **)
From Coq
     Require Import QArith.QArith QArith.Qminmax QArith.Qabs QArith.Qreals
Nikita Zyuzin's avatar
Nikita Zyuzin committed
11
     micromega.Psatz Recdef Reals.Reals.
12 13 14

From Flover
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
15 16 17
     Infra.RealSimps Infra.Ltacs Commands Environments ErrorAnalysis ErrorValidationAAutil
     ExpressionSemantics IntervalValidation TypeValidator RealRangeValidator ErrorBounds
     ErrorValidation AffineForm AffineArithQ AffineArith.
18

19 20 21 22 23 24 25
(** Error bound validator **)
Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
         (typeMap:FloverMap.t mType) (* derived types for e *)
         (A:analysisResult) (* encoded result of Flover *)
         (dVars:NatSet.t) (* let-bound variables encountered previously *)
         (currNoise: nat) (* current maximal noise term *)
         (errMap:FloverMap.t (affine_form Q)) (* previously seen affine polys *)
26
  : option (FloverMap.t (affine_form Q) * nat) :=
27 28 29 30 31
  (* case analysis for the expression *)
  if FloverMap.mem e errMap then
    (* We have already checked a subexpression *)
    Some (errMap, currNoise)
  else
32 33 34 35
    olet m := FloverMap.find e typeMap in
    olet dRes := FloverMap.find e A in
    let (intv, err) := dRes in
    (* Error bounds are intervals symmetric at 0 --> the bound must be positive here *)
36 37 38
    if negb (Qleb 0 err) then
      None
    else match e with
39
    | Var _ x =>
40
      if NatSet.mem x dVars then
41
        Some (errMap, currNoise) (* defined variable for a previously checked expression *)
42
      else
43 44
        (* Build an affine polynomial *)
        let errNew := computeErrorQ (maxAbs intv) m in
45
        let af := mkErrorPolyQ errNew currNoise in
46 47 48 49
        if Qleb errNew err then
          Some (FloverMap.add e af errMap, (currNoise+1)%nat)
        else
          None
50
    | Expressions.Const m v =>
51
        let errNew := computeErrorQ (maxAbs intv) m in
52
        let af := mkErrorPolyQ errNew currNoise in
53 54 55 56
        if Qleb errNew err then
          Some (FloverMap.add (elt:=affine_form Q) e af errMap, (currNoise+1)%nat)
        else
          None
57
    | Unop Neg e1 =>
58
        olet res := validErrorboundAA e1 typeMap A dVars currNoise errMap in
59 60
        let (newErrorMap, maxNoise) := res in
        olet afPolye1 := FloverMap.find e1 newErrorMap in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
61
        let errPoly := AffineArithQ.negate_aff afPolye1 in
62 63 64
        match FloverMap.find e1 A with
        | Some (iv_e1, err1) =>
          if Qeq_bool err err1 then
Nikita Zyuzin's avatar
Nikita Zyuzin committed
65
            Some (FloverMap.add e errPoly newErrorMap, maxNoise)
66 67 68 69
          else
            None
        | None => None
        end
70
    | Unop Inv e1 => None
71 72
    | Binop b e1 e2 =>
        olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
73 74 75 76 77 78 79 80 81 82
        let (newErrorMap1, maxNoise1) := res1 in
        olet res2 := validErrorboundAA e2 typeMap A dVars maxNoise1 newErrorMap1 in
        let (newErrorMap2, maxNoise2) := res2 in
        (* Error polynomial for e1 *)
        olet afPolye1 := FloverMap.find e1 newErrorMap2 in
        (* Error polynomial for e2 *)
        olet afPolye2 := FloverMap.find e2 newErrorMap2 in
        (* Analysis results for e1, e2 *)
        match FloverMap.find e1 A, FloverMap.find e2 A with
        | Some (ive1, err1), Some (ive2, err2) =>
83 84 85 86 87 88
            let errIve1 := widenIntv ive1 err1 in
            let errIve2 := widenIntv ive2 err2 in
            match b with
            | Plus =>
                let actualRange := (addIntv errIve1 errIve2) in
                let errNew := computeErrorQ (maxAbs actualRange) m in
89 90
                let errPoly := AffineArithQ.plus_aff
                                (AffineArithQ.plus_aff afPolye1 afPolye2)
91
                                (mkErrorPolyQ errNew maxNoise2) in
92
                let errVal := maxAbs (toIntv errPoly) in
93 94 95 96
                if Qleb errVal err then
                  Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
                else
                  None
97 98 99
            | Sub =>
                let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in
                let errNew := computeErrorQ mAbs m in
100 101
                let errPoly := AffineArithQ.plus_aff
                                (AffineArithQ.subtract_aff afPolye1 afPolye2)
102
                                (mkErrorPolyQ errNew maxNoise2) in
103
                let errVal := maxAbs (toIntv errPoly) in
104 105 106 107
                if Qleb errVal err then
                  Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
                else
                  None
108 109 110
            | Mult =>
                let aaRangee1 := fromIntv ive1 maxNoise2 in
                let aaRangee2 := fromIntv ive2 (maxNoise2 + 1) in
111 112 113 114 115 116 117
                (* Differs from intervals and daisy -- subtraction does not change the range *)
                (* but matters for concrete evaluations *)
                let propError := AffineArithQ.subtract_aff
                                   (AffineArithQ.plus_aff
                                      (AffineArithQ.mult_aff aaRangee1 afPolye2 (maxNoise2 + 2))
                                      (AffineArithQ.mult_aff aaRangee2 afPolye1 (maxNoise2 + 3)))
                                   (AffineArithQ.mult_aff afPolye1 afPolye2 (maxNoise2 + 4)) in
118 119
                let mAbs := (maxAbs (multIntv errIve1 errIve2)) in
                let errNew := computeErrorQ mAbs m in
120
                let errPoly := AffineArithQ.plus_aff propError
121
                                        (mkErrorPolyQ errNew (maxNoise2 + 5)) in
122
                let errVal := maxAbs (toIntv errPoly) in
123 124 125 126
                if Qleb errVal err then
                  Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 6)%nat)
                else
                  None
127
            | Div =>
128 129 130
                if ((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
                    ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))) then
                  let aaRangee1 := fromIntv ive1 maxNoise2 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
131 132 133 134 135
                  let aaRangeInve2 := fromIntv (invertIntv ive2) (maxNoise2 + 1) in
                  let minAbsIve2 := minAbs errIve2 in
                  let errMultiplier := fromIntv (invertIntv (multIntv ive2 errIve2))
                                                (maxNoise2 + 2) in
                  let invErrAf2 := AffineArithQ.mult_aff afPolye2 errMultiplier (maxNoise2 + 3) in
136
                  let propError := AffineArithQ.plus_aff
Nikita Zyuzin's avatar
Nikita Zyuzin committed
137 138 139 140
                                     (AffineArithQ.subtract_aff
                                        (AffineArithQ.mult_aff afPolye1 aaRangeInve2 (maxNoise2 + 4))
                                        (AffineArithQ.mult_aff aaRangee1 invErrAf2 (maxNoise2 + 5)))
                                     (AffineArithQ.mult_aff afPolye1 invErrAf2 (maxNoise2 + 6)) in
141 142
                  let mAbs := (maxAbs (divideIntv errIve1 errIve2)) in
                  let errNew := computeErrorQ mAbs m in
143
                  let errPoly := AffineArithQ.plus_aff propError
Nikita Zyuzin's avatar
Nikita Zyuzin committed
144
                                          (mkErrorPolyQ  errNew (maxNoise2 + 7)) in
145 146
                  let errVal := maxAbs (toIntv errPoly) in
                  if (Qleb errVal err) then
Nikita Zyuzin's avatar
Nikita Zyuzin committed
147
                    Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 8)%nat)
148 149 150 151
                  else
                    None
                else
                  None
152
            end
153 154
        | _, _ => None
        end
155 156
    | Fma e1 e2 e3 =>
        olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
        let (newErrorMap1, maxNoise1) := res1 in
        olet res2 := validErrorboundAA e2 typeMap A dVars maxNoise1 newErrorMap1 in
        let (newErrorMap2, maxNoise2) := res2 in
        olet res3 := validErrorboundAA e3 typeMap A dVars maxNoise2 newErrorMap2 in
        let (newErrorMap3, maxNoise3) := res3 in
        (* Error polynomial for e1 *)
        olet afPolye1 := FloverMap.find e1 newErrorMap3 in
        (* Error polynomial for e2 *)
        olet afPolye2 := FloverMap.find e2 newErrorMap3 in
        (* Error polynomial for e2 *)
        olet afPolye3 := FloverMap.find e3 newErrorMap3 in
        match FloverMap.find e1 A, FloverMap.find e2 A, FloverMap.find e3 A with
        | Some (ive1, err1), Some (ive2, err2), Some (ive3, err3) =>
          let errIve1 := widenIntv ive1 err1 in
          let errIve2 := widenIntv ive2 err2 in
          let errIve3 := widenIntv ive3 err3 in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
173 174
          let aaRangee2 := fromIntv ive2 maxNoise3 in
          let aaRangee3 := fromIntv ive3 (maxNoise3 + 1) in
175
          let propError := AffineArithQ.plus_aff
176
                             afPolye1
Nikita Zyuzin's avatar
Nikita Zyuzin committed
177 178 179 180 181 182
                             (AffineArithQ.subtract_aff
                                (AffineArithQ.plus_aff
                                   (AffineArithQ.mult_aff aaRangee2 afPolye3 (maxNoise3 + 2))
                                   (AffineArithQ.mult_aff aaRangee3 afPolye2 (maxNoise3 + 3)))
                                (AffineArithQ.mult_aff afPolye2 afPolye3 (maxNoise3 + 4))) in
          let mAbs := (maxAbs (addIntv errIve1 (multIntv errIve2 errIve3))) in
183
          let errNew := computeErrorQ mAbs m in
Nikita Zyuzin's avatar
Nikita Zyuzin committed
184
          let errPoly := AffineArithQ.plus_aff propError (mkErrorPolyQ errNew (maxNoise3 + 5)) in
185 186
          let errVal := maxAbs (toIntv errPoly) in
          if Qleb errVal err then
187
            Some (FloverMap.add e errPoly newErrorMap3, (maxNoise3 + 6)%nat)
188 189 190 191
          else
            None
        | _, _, _ => None
        end
192
    | Downcast m e1 =>
193
        olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
194 195 196 197 198 199 200 201
        let (newErrorMap1, maxNoise1) := res1 in
        (* Error polynomial for e1 *)
        olet afPolye1 := FloverMap.find e1 newErrorMap1 in
        olet aRes := FloverMap.find e1 A in
        let (ive1, err1) := aRes in
        let errIve1 := widenIntv ive1 err1 in
        let mAbs := maxAbs errIve1 in
        let newErr := computeErrorQ mAbs m in
202
        let errPoly := AffineArithQ.plus_aff afPolye1
203
                                (mkErrorPolyQ newErr maxNoise1) in
204 205 206 207 208
        let errVal := maxAbs (toIntv errPoly) in
        if Qleb errVal err then
          Some (FloverMap.add e errPoly newErrorMap1, (maxNoise1 + 1)%nat)
        else
          None
209
    end.
210 211

(** Error bound command validator **)
212 213 214 215
Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
         (typeMap: FloverMap.t mType) (* derived types for e *)
         (A: analysisResult) (* encoded result of Flover *)
         (dVars: NatSet.t) (* let-bound variables encountered previously *)
216
         (currNoise: nat) (* current maximal noise term *)
217
         (errMap: FloverMap.t (affine_form Q)) (* previously seen affine polys *)
218
  : option (FloverMap.t (affine_form Q) * nat) :=
219
  match f with
220
  | Let m x e g =>
221 222 223 224 225 226
    olet res1 := validErrorboundAA e typeMap A dVars currNoise errMap in
    let (errMap1, maxNoise1) := res1 in
    olet afPolye := FloverMap.find e errMap1 in
    match FloverMap.find e A, FloverMap.find (Var Q x) A with
    | Some (iv_e, err_e), Some (iv_x, err_x) =>
      if Qeq_bool err_e err_x then
Nikita Zyuzin's avatar
Nikita Zyuzin committed
227 228 229 230 231
        match FloverMap.find (Var Q x) errMap1 with
        | Some _ => None
        | None => validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1
                                      (FloverMap.add (Var Q x) afPolye errMap1)
        end
232 233 234 235
      else
          None
    | _,_ => None
    end
236
  | Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
237
  end.
Heiko Becker's avatar
Heiko Becker committed
238

239 240 241 242 243
(* 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 *)
244
Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap
245
           noise_map noise expr_map :=
246
  forall v__R v__FP m__FP (iv__A: intv) (err__A: error),
247 248
  eval_expr E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
  eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
249
  FloverMap.find e A = Some (iv__A, err__A) ->
250
  exists af err__af,
251
    fresh noise (afQ2R af) /\
252
    (forall n, (n >= noise)%nat -> noise_map n = None) /\
253 254 255 256
    FloverMap.find e expr_map = Some af /\
    (0 <= err__af)%R /\
    toInterval (afQ2R af) = (-err__af, err__af)%R /\
    (err__af <= Q2R err__A)%R /\
257
    af_evals (afQ2R af) (v__R - v__FP)%R noise_map.
258

259
Lemma checked_error_expressions_extension e E1 E2 A Gamma DeltaMap
260 261 262 263 264
      noise_map1 noise_map2 noise1 noise2 expr_map1 expr_map2:
  contained_map noise_map1 noise_map2 ->
  (noise1 <= noise2)%nat ->
  contained_flover_map expr_map1 expr_map2 ->
  (forall n, (n >= noise2)%nat -> noise_map2 n = None) ->
265 266
  checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1 ->
  checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2.
267 268 269 270 271 272 273 274 275
Proof.
  intros cont contf Hnoise Hvalidmap checked1.
  unfold checked_error_expressions in checked1 |-*.
  intros.
  specialize (checked1 v__R v__FP m__FP iv__A err__A) as (af & err__af & checked1); auto.
  exists af, err__af.
  intuition; eauto using fresh_monotonic, af_evals_map_extension.
Qed.

276
Lemma checked_error_expressions_flover_map_add_compat e e' af E1 E2 A Gamma DeltaMap
277 278
      noise_map noise expr_map:
  Q_orderedExps.exprCompare e' e <> Eq ->
279 280
  checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map noise expr_map ->
  checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map noise
281 282 283 284 285 286 287 288 289 290 291
                            (FloverMap.add e' af expr_map).
Proof.
  intros Hneq checked1.
  unfold checked_error_expressions in checked1 |-*.
  intros.
  specialize (checked1 v__R v__FP m__FP iv__A err__A) as (af' & err__af' & checked1); auto.
  exists af', err__af'.
  intuition.
  rewrite FloverMapFacts.P.F.add_neq_o; auto.
Qed.

292 293
Definition dVars_contained  dVars (expr_map: FloverMap.t (affine_form Q)): Prop :=
  forall v, NatSet.In v dVars -> FloverMap.In (Var Q v) expr_map.
294

295 296 297 298
Lemma dVars_contained_extension dVars expr_map1 expr_map2:
  contained_flover_map expr_map1 expr_map2 ->
  dVars_contained dVars expr_map1 ->
  dVars_contained dVars expr_map2.
299
Proof.
300 301
  intros H Hdvars.
  unfold dVars_contained in Hdvars |-*.
302 303
  intros v Hvin.
  specialize (Hdvars v Hvin).
304
  eapply flover_map_in_extension; eauto.
305 306
Qed.

307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419
Fixpoint contained_subexpr (e: expr Q) (expr_map: FloverMap.t (affine_form Q)): Prop :=
  match e with
  | Var _ x => True
  | Expressions.Const m v => True
  | Unop u e' => contained_subexpr e' expr_map
  | Binop b e1 e2 => contained_subexpr e1 expr_map /\ contained_subexpr e2 expr_map
  | Fma e1 e2 e3 => contained_subexpr e1 expr_map /\ contained_subexpr e2 expr_map /\
                   contained_subexpr e3 expr_map
  | Downcast m e' => contained_subexpr e' expr_map
  end /\ FloverMap.In e expr_map.

Lemma contained_subexpr_map_extension e expr_map1 expr_map2:
  contained_flover_map expr_map1 expr_map2 ->
  contained_subexpr e expr_map1 ->
  contained_subexpr e expr_map2.
Proof.
  intros Hcontf Hconte.
  induction e; cbn in *; intuition; eauto using flover_map_in_extension.
Qed.

Lemma contained_subexpr_add_compat e e' a expr_map:
  contained_subexpr e expr_map ->
  contained_subexpr e (FloverMap.add e' a expr_map).
Proof.
  intros Hcont.
  induction e; cbn in *; intuition; rewrite FloverMapFacts.P.F.add_in_iff; now right.
Qed.

Lemma contained_subexpr_eq_compat e e' expr_map:
  Q_orderedExps.exprCompare e e' = Eq ->
  contained_subexpr e expr_map ->
  contained_subexpr e' expr_map.
Proof.
  intros Hexpeq Hcont.
  functional induction (Q_orderedExps.exprCompare e e'); try congruence.
  - apply nat_compare_eq in Hexpeq.
    subst; auto.
  - cbn in Hcont |-*.
    split; auto.
    destruct Hcont as [_ Hcont].
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e3.
  - cbn in e3.
    apply Ndec.Pcompare_Peqb in e6.
    rewrite e6 in e3.
    rewrite andb_true_l in e3.
    apply Ndec.Ncompare_Neqb in Hexpeq.
    now rewrite Hexpeq in e3.
  - cbn in Hcont |-*.
    destruct Hcont as [Hsubcont Hcont].
    specialize (IHc Hexpeq Hsubcont).
    split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e5.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2) & Hcont).
    specialize (IHc e6 Hsubcont1).
    specialize (IHc0 Hexpeq Hsubcont2).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e6.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2) & Hcont).
    specialize (IHc e6 Hsubcont1).
    specialize (IHc0 Hexpeq Hsubcont2).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e6.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2) & Hcont).
    specialize (IHc e6 Hsubcont1).
    specialize (IHc0 Hexpeq Hsubcont2).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e6.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2) & Hcont).
    specialize (IHc e6 Hsubcont1).
    specialize (IHc0 Hexpeq Hsubcont2).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e6.
  - cbn in Hcont |-*.
    destruct Hcont as ((Hsubcont1 & Hsubcont2 & Hsubcont3) & Hcont).
    specialize (IHc e3 Hsubcont1).
    specialize (IHc0 e4 Hsubcont2).
    specialize (IHc1 Hexpeq Hsubcont3).
    repeat split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    rewrite e4.
    now rewrite e3.
  - cbn in Hcont |-*.
    destruct Hcont as [Hsubcont Hcont].
    specialize (IHc Hexpeq Hsubcont).
    split; auto.
    rewrite FloverMapFacts.P.F.In_iff in Hcont; eauto.
    cbn.
    now rewrite e5.
  - cbn in e5.
    apply Ndec.Pcompare_Peqb in e8.
    rewrite e8 in e5.
    rewrite andb_true_l in e5.
    apply Ndec.Ncompare_Neqb in Hexpeq.
    now rewrite Hexpeq in e5.
Qed.

420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489
Lemma validErrorboundAA_contained_subexpr e Gamma A dVars noise1 noise2 expr_map1 expr_map2:
  (forall e', FloverMap.In e' expr_map1 ->
         contained_subexpr e' expr_map1) ->
  (forall n, NatSet.In n dVars -> FloverMap.In (Var Q n) expr_map1) ->
  validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
  contained_subexpr e expr_map2 /\
  contained_flover_map expr_map1 expr_map2 /\
  (forall e', ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
   contained_subexpr e' expr_map2).
Proof.
  revert noise1 noise2 expr_map1 expr_map2.
  induction e; intros * Hchecked Hdvars Hvalidbounds; cbn in Hvalidbounds.
  - destruct (FloverMap.mem (Var Q n) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    Flover_compute.
    destruct negb; [congruence|].
    destruct NatSet.mem eqn:Hmemvar.
    + inversion Hvalidbounds; subst; clear Hvalidbounds.
      intuition.
    + destruct Qleb; [|congruence].
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      repeat split.
      * cbn.
        intuition.
        apply flover_map_in_add.
      * apply contained_flover_map_extension.
        now rewrite <- mem_false_find_none.
      * intros e' Hnin1 Hin.
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition.
        apply flover_map_in_add.
  - destruct (FloverMap.mem (Expressions.Const m v) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    Flover_compute.
    destruct negb; [congruence|].
    destruct Qleb; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    repeat split.
    + cbn.
      intuition.
      apply flover_map_in_add.
    + apply contained_flover_map_extension.
      now rewrite <- mem_false_find_none.
    + intros e' Hnin1 Hin.
      apply flover_map_el_eq_extension in Hin; auto.
      specialize Hin as [Heq Hexpreq].
      eapply contained_subexpr_eq_compat; eauto.
      cbn.
      intuition.
      apply flover_map_in_add.
  - destruct (FloverMap.mem (Unop u e) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct p.
490
    destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527
    destruct u; [|congruence].
    destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
      as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
      simpl in Hvalidbounds; try congruence.
    destruct (FloverMap.find e subexpr_map) as [subaf|] eqn: Hsubaf;
      simpl in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e A) as [(subiv, suberr)|] eqn: Hsuba;
      simpl in Hvalidbounds; [|congruence].
    destruct (Qeq_bool e0 suberr) eqn: Heq__err; simpl in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    specialize IHe as (IHsubexpr & IHcont & IHechecked); eauto.
    split; [|split].
    + cbn.
      intuition; [|apply flover_map_in_add].
      now eapply contained_subexpr_add_compat.
    + etransitivity; try apply contained_flover_map_add_compat; eauto.
      apply contained_flover_map_extension.
      now rewrite <- mem_false_find_none.
    + intros e' Hnin1 Hin.
      destruct (flover_map_in_dec e' subexpr_map) as [Hsubin|Hsubnin];
        [apply contained_subexpr_add_compat; auto|].
      apply flover_map_el_eq_extension in Hin; auto.
      specialize Hin as [Heq Hexpreq].
      eapply contained_subexpr_eq_compat; eauto.
      cbn.
      intuition.
      * apply contained_subexpr_add_compat; auto.
      * apply flover_map_in_add.
  - destruct (FloverMap.mem (Binop b e1 e2) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct p as (? & err__A).
528
    destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659
    destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
      as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
      cbn in Hvalidbounds; try congruence.
    destruct (validErrorboundAA e2 Gamma A dVars subnoise1 subexpr_map1)
      as [(subexpr_map2, subnoise2)|] eqn: Hvalidsubexpr2;
      cbn in Hvalidbounds; try congruence.
    destruct (FloverMap.find e1 subexpr_map2) as [subaf1|] eqn: Hsubaf1;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e2 subexpr_map2) as [subaf2|] eqn: Hsubaf2;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e1 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A1 & err__A1).
    destruct (FloverMap.find e2 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A2 & err__A2).
    clear H0err.
    specialize IHe1 as (IHsubexpr1 & IHcont1 & IHchecked1); eauto.
    specialize (IHe2 subnoise1 subnoise2 subexpr_map1 subexpr_map2)
      as (IHsubexpr2 & IHcont2 & IHechecked2); eauto.
    {
      intros e' Hin.
      destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
      - eapply contained_subexpr_map_extension with (expr_map1 := expr_map1); eauto.
      - now apply IHchecked1.
    }
    {
      intros * ?.
      eapply flover_map_in_extension; try apply Hdvars; eauto.
    }
    rewrite mem_false_find_none in Hmem.
    destruct b.
    4: destruct (Qleb (snd iv__A2 + err__A2) 0 && negb (Qeq_bool (snd iv__A2 + err__A2) 0)
              || Qleb 0 (fst iv__A2 - err__A2) && negb (Qeq_bool (fst iv__A2 - err__A2) 0)); [|congruence].
    all: destruct Qleb; cbn in Hvalidbounds; [|congruence].
    all: inversion Hvalidbounds; subst; clear Hvalidbounds.
    + split; [|split].
      * cbn.
        intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
        apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
      * epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
        etransitivity; [exact G|].
        apply contained_flover_map_add_compat.
        etransitivity; [|exact IHcont2].
        assumption.
      * intros e' Hnin1 Hin.
        destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
          [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto|].
        destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
          [apply contained_subexpr_add_compat; auto|].
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
        apply contained_subexpr_add_compat.
        eapply contained_subexpr_map_extension; eauto.
    + split; [|split].
      * cbn.
        intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
        apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
      * epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
        etransitivity; [exact G|].
        apply contained_flover_map_add_compat.
        etransitivity; [|exact IHcont2].
        assumption.
      * intros e' Hnin1 Hin.
        destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
          [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto|].
        destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
          [apply contained_subexpr_add_compat; auto|].
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
        apply contained_subexpr_add_compat.
        eapply contained_subexpr_map_extension; eauto.
    + split; [|split].
      * cbn.
        intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
        apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
      * epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
        etransitivity; [exact G|].
        apply contained_flover_map_add_compat.
        etransitivity; [|exact IHcont2].
        assumption.
      * intros e' Hnin1 Hin.
        destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
          [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto|].
        destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
          [apply contained_subexpr_add_compat; auto|].
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
        apply contained_subexpr_add_compat.
        eapply contained_subexpr_map_extension; eauto.
    + split; [|split].
      * cbn.
        intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
        apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
      * epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
        etransitivity; [exact G|].
        apply contained_flover_map_add_compat.
        etransitivity; [|exact IHcont2].
        assumption.
      * intros e' Hnin1 Hin.
        destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
          [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto|].
        destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
          [apply contained_subexpr_add_compat; auto|].
        apply flover_map_el_eq_extension in Hin; auto.
        specialize Hin as [Heq Hexpreq].
        eapply contained_subexpr_eq_compat; eauto.
        cbn.
        intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
        apply contained_subexpr_add_compat.
        eapply contained_subexpr_map_extension; eauto.
  - destruct (FloverMap.mem (Fma e1 e2 e3) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct p as (? & err__A).
660
    destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753
    destruct (validErrorboundAA e1 Gamma A dVars noise1 expr_map1)
      as [(subexpr_map1, subnoise1)|] eqn: Hvalidsubexpr1;
      cbn in Hvalidbounds; try congruence.
    destruct (validErrorboundAA e2 Gamma A dVars subnoise1 subexpr_map1)
      as [(subexpr_map2, subnoise2)|] eqn: Hvalidsubexpr2;
      cbn in Hvalidbounds; try congruence.
    destruct (validErrorboundAA e3 Gamma A dVars subnoise2 subexpr_map2)
      as [(subexpr_map3, subnoise3)|] eqn: Hvalidsubexpr3;
      cbn in Hvalidbounds; try congruence.
    destruct (FloverMap.find e1 subexpr_map3) as [subaf1|] eqn: Hsubaf1;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e2 subexpr_map3) as [subaf2|] eqn: Hsubaf2;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e3 subexpr_map3) as [subaf3|] eqn: Hsubaf3;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e1 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A1 & err__A1).
    destruct (FloverMap.find e2 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A2 & err__A2).
    destruct (FloverMap.find e3 A); cbn in Hvalidbounds; [|congruence].
    destruct p as (iv__A3 & err__A3).
    clear H0err.
    specialize IHe1 as (IHsubexpr1 & IHcont1 & IHchecked1); eauto.
    specialize (IHe2 subnoise1 subnoise2 subexpr_map1 subexpr_map2)
      as (IHsubexpr2 & IHcont2 & IHchecked2); eauto.
    {
      intros e' Hin.
      destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
      - eapply contained_subexpr_map_extension with (expr_map1 := expr_map1); eauto.
      - now apply IHchecked1.
    }
    {
      intros * ?.
      eapply flover_map_in_extension; try apply Hdvars; eauto.
    }
    specialize (IHe3 subnoise2 subnoise3 subexpr_map2 subexpr_map3)
      as (IHsubexpr3 & IHcont3 & IHechecked3); eauto.
    {
      intros e' Hin.
      destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
      - eapply contained_subexpr_map_extension with (expr_map1 := expr_map1); eauto.
        etransitivity; eauto.
      - destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1].
        + apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
        + now apply IHchecked2.
    }
    {
      intros * ?.
      eapply flover_map_in_extension; try apply Hdvars; eauto.
      etransitivity; eauto.
    }
    rewrite mem_false_find_none in Hmem.
    destruct Qleb; cbn in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    split; [|split].
    + cbn.
      intuition; eauto using flover_map_in_add, contained_subexpr_add_compat.
      * apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map1); auto.
        etransitivity; eauto.
      * apply contained_subexpr_add_compat.
        apply contained_subexpr_map_extension with (expr_map1 := subexpr_map2); auto.
    + epose proof (contained_flover_map_extension _ _ _ Hmem) as G.
      etransitivity; [exact G|].
      apply contained_flover_map_add_compat.
      etransitivity; [|exact IHcont3].
      etransitivity; [|exact IHcont2].
      assumption.
    + intros e' Hnin1 Hin.
      destruct (flover_map_in_dec e' subexpr_map1) as [Hsubin1|Hsubnin1];
        [apply contained_subexpr_add_compat; eapply contained_subexpr_map_extension; eauto;
         eapply contained_subexpr_map_extension; eauto|].
      destruct (flover_map_in_dec e' subexpr_map2) as [Hsubin2|Hsubnin2];
        [apply contained_subexpr_add_compat; auto; eapply contained_subexpr_map_extension; eauto|].
      destruct (flover_map_in_dec e' subexpr_map3) as [Hsubin3|Hsubnin3];
        [apply contained_subexpr_add_compat; auto|].
      apply flover_map_el_eq_extension in Hin; auto.
      specialize Hin as [Heq Hexpreq].
      eapply contained_subexpr_eq_compat; eauto.
      cbn.
      intuition; eauto using contained_subexpr_add_compat, flover_map_in_add.
      all: apply contained_subexpr_add_compat.
      all: eapply contained_subexpr_map_extension; eauto.
      eapply contained_subexpr_map_extension; eauto.
  - destruct (FloverMap.mem (Downcast m e) expr_map1) eqn:Hmem.
    {
      inversion Hvalidbounds; subst; clear Hvalidbounds.
      apply FloverMap.mem_2 in Hmem.
      intuition.
    }
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct FloverMap.find; cbn in Hvalidbounds; [|congruence].
    destruct p.
754
    destruct (negb (Qleb 0 e0)) eqn: H0err; [congruence|].
755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784
    destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
      as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
      cbn in Hvalidbounds; try congruence.
    destruct (FloverMap.find e subexpr_map) as [subaf|] eqn: Hsubaf;
      cbn in Hvalidbounds; [|congruence].
    destruct (FloverMap.find e A) as [(subiv, suberr)|] eqn: Hsuba;
      cbn in Hvalidbounds; [|congruence].
    clear H0err.
    destruct Qleb; cbn in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    specialize IHe as (IHsubexpr & IHcont & IHechecked); eauto.
    split; [|split].
    + cbn.
      intuition; [|apply flover_map_in_add].
      now eapply contained_subexpr_add_compat.
    + etransitivity; try apply contained_flover_map_add_compat; eauto.
      apply contained_flover_map_extension.
      now rewrite <- mem_false_find_none.
    + intros e' Hnin1 Hin.
      destruct (flover_map_in_dec e' subexpr_map) as [Hsubin|Hsubnin];
        [apply contained_subexpr_add_compat; auto|].
      apply flover_map_el_eq_extension in Hin; auto.
      specialize Hin as [Heq Hexpreq].
      eapply contained_subexpr_eq_compat; eauto.
      cbn.
      intuition.
      * apply contained_subexpr_add_compat; auto.
      * apply flover_map_in_add.
Qed.

785 786 787 788 789
(* 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. *)
790 791
Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars :=
  forall (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
792
    (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
793
    (iv__A : intv) (err__A : error),
794 795
    (forall (v : R) (m' : mType),
        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
796
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
797
    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
798 799 800
    validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
    validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
    NatSet.Subset (usedVars e -- dVars) fVars ->
801
    validTypes e Gamma ->
802
    FloverMap.find e A = Some (iv__A, err__A) ->
803 804
    (* Starting noise index is greater than 0 and the noise mapping doesn't
       map it and anything above to a noise value *)
805 806
    (0 < noise1)%nat ->
    (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
807 808
    (* If a var is a dVar, we know it's in expr_map and invoke the corresponding
     preconditions (described below) *)
809
    dVars_contained dVars expr_map1 ->
810 811 812
    (* 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 *)
813
    (forall e' : FloverMap.key,
814
        FloverMap.In e' expr_map1 ->
815
        (* Assumption needed for Cmd_sound proof *)
816
        NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
817
        (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
818
        exists (v__FP' : R) (m__FP' : mType),
819
          eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
820 821 822 823 824 825
    (* 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 *)
826
    (forall e' : FloverMap.key,
827
        FloverMap.In e' expr_map1 ->
828
        checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
829
    (* THE EXESTENTIAL CASE OF THE GOAL *)
830
    ((exists (v__FP : R) (m__FP : mType),
831
         eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
832 833 834
     (* Invariant of the existential case:
        our given expr_map1 is updated only with the expressions for which
        the existential part holds *)
835
     (forall e' : FloverMap.key,
836 837
         ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
         NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
838
         (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
839
         exists (v__FP' : R) (m__FP' : mType),
840
           eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP')) /\
841
    (* UNIVERSAL CASE OF THE GOAL *)
842
    (forall (v__FP : R) (m__FP : mType),
843
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
844 845 846
        (* For the given evaluation we can find a polynomial and an
           error bound with a monotonic extension of noise_map1 to
           noise_map2 *)
847
        exists (af : affine_form Q) (err__af : R) (noise_map2 : noise_mapping),
848 849
          (* Invariant: the checker function only adds new polynomials
             to the expr_map, never removes something from it *)
850
          contained_flover_map expr_map1 expr_map2 /\
851 852
          (* Noise index invariants: the checker function returns new
             noise that is not used in already produced polynomials *)
853 854
          (noise1 <= noise2)%nat /\
          fresh noise2 (afQ2R af) /\
855
          (* Invariant: noise_map is incrementally updated *)
856 857 858
          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 /\
859 860 861 862 863
          (* 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 *)
864 865 866 867
          (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 /\
868 869 870
          (* 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 *)
871
          (forall e' : FloverMap.key,
872
              ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
873
              checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)).
874 875 876 877 878

Lemma validErrorboundAA_sound_var n E1 E2 A Gamma DeltaMap fVars dVars:
  validErrorboundAA_sound_statement (Var Q n) E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
  unfold validErrorboundAA_sound_statement.
879
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
880 881
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
                     Hcheckedex Hcheckedall;
882
  inversion Heval__R; subst.
883 884 885 886 887 888 889
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (Var Q n) expr_map1) eqn: Hmem; cbn in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
890
    specialize (Hcheckedex _ Hmem) as (Hvars & Hcert' & Hcheckedex).
891
    repeat split.
892
    1-4: congruence.
893 894 895 896 897
    intros v__FP m__FP Heval__FP.
    unfold checked_error_expressions in Hcheckedall.
    specialize (Hcheckedall v__R v__FP m__FP iv__A err__A) as (af & err__af & Hcheckedall); auto.
    exists af, err__af, noise_map1.
    intuition.
898 899 900 901 902 903 904 905 906 907 908
  }
  destruct (Htypecheck) as (m & Hetype & _ & Hvalidexec).
  rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
  pose proof Hrange as Hrange'.
  destruct Hrange as [_ [tmpiv [tmperr [tmpvR [Hres__A' [Heval1' Hcontained]]]]]].
  rewrite Hcert in Hres__A'.
  replace tmpiv with iv__A in * by congruence.
  replace tmperr with err__A in * by congruence; clear Hres__A' tmperr tmpiv.
  eapply meps_0_deterministic in Heval1'; try exact Heval__R.
  replace tmpvR with v__R in * by congruence; clear Heval1' tmpvR.
909
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
910 911 912 913
  cbn in Htypecheck.
  destruct (NatSet.mem n dVars) eqn: Hmem__n; cbn in Hvalidbounds.
  - inversion Hvalidbounds; subst; clear Hvalidbounds.
    apply NatSetProps.FM.mem_2 in Hmem__n.
914 915 916
    specialize (Hdvars n Hmem__n).
    rewrite <- FloverMapFacts.P.F.not_mem_in_iff in Hmem.
    congruence.
917 918
  - destruct (Qleb (computeErrorQ (maxAbs iv__A) m) err__A) eqn: Herrle; cbn in Hvalidbounds; [|congruence].
    inversion Hvalidbounds; subst; clear Hvalidbounds.
919
    rewrite mem_false_find_none in Hmem.
920 921 922 923
    apply not_in_not_mem in Hmem__n.
    assert (n  fVars) as Hmem__n' by (set_tac; set_tac).
    assert (exists v, E2 n = Some v) as [v__fp Hv__fp]
        by (eapply approxEnv_gives_value; eauto; set_tac).
924 925
    split.
    + assert (exists (v__FP : R) (m__FP : mType),
926
                 eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Var Q n)) v__FP m__FP).
927
      {
928 929 930
        exists v__fp, m.
        constructor; auto.
        eapply toRExpMap_some with (e:=Var Q n); eauto.
931
      }
932 933 934
      split; auto.
      intros e' Hnin Hin.
      destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq].
935 936
      split; [|split; [|now rewrite Hexpeq]].
      1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq;
937
        try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
938 939
      1: now apply subset_diff_to_subset_union.
      erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
940
    + intros v__FP m__FP Heval__FP.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
941
      rewrite Qle_bool_iff in Herrle.
942 943
      apply Qle_Rle in Herrle.
      inversion Heval__FP; subst.
944 945 946 947 948 949
      eapply toRExpMap_some with (e:=Var Q n) in Hetype; eauto.
      cbn in Hetype.
      replace m with m__FP in * by congruence; clear H2.
      replace v__fp with v__FP in * by congruence; clear H3.
      assert (exists q, af_evals (afQ2R (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1))
                            (v__R - v__FP)%R (updMap noise_map1 noise1 q)) as [q Hevals].
950 951 952 953
      {
        rewrite afQ2R_mkErrorPolyQ.
        rewrite computeErrorQ_computeErrorR.
        apply af_evals_mkErrorPolyR_updMap; auto using computeErrorR_pos.
954 955
        pose proof (approxEnv_fVar_bounded Henv H1 Hv__fp Hmem__n' Hetype) as H.
        eapply Rle_trans; try exact H.
956 957 958 959 960 961 962 963 964
        rewrite <- maxAbs_impl_RmaxAbs_iv.
        destruct iv__A as [liv__A hiv__A].
        apply computeErrorR_up.
        apply contained_leq_maxAbs.
        now cbn.
      }
      exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
      (Q2R (computeErrorQ (maxAbs iv__A) m__FP)), (updMap noise_map1 noise1 q).
      rewrite computeErrorQ_computeErrorR in Herrle |-*.
965
      {
966
        repeat split; try auto.
967
        - now apply contained_flover_map_extension.
968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992
        - lia.
        - rewrite afQ2R_mkErrorPolyQ.
          apply mkErrorPolyR_fresh_compat; lia.
        - apply contained_map_extension; auto.
        - intros n' Hn'.
          unfold updMap.
          destruct (n' =? noise1) eqn: Hneq.
          + apply beq_nat_true in Hneq.
            lia.
          + apply Hnoise_map1.
            lia.
        - rewrite FloverMapFacts.P.F.add_eq_o; try auto.
          apply Q_orderedExps.exprCompare_refl.
        - apply computeErrorR_pos.
        - rewrite afQ2R_mkErrorPolyQ.
          rewrite computeErrorQ_computeErrorR.
          rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
        - intros e' Hnin Hin.
          unfold checked_error_expressions.
          pose proof (flover_map_el_eq_extension Hnin Hin) as [Hexeq Hreq].
          rewrite Hreq.
          intros.
          exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
          (Q2R (computeErrorQ (maxAbs iv__A) m__FP)).
          rewrite computeErrorQ_computeErrorR.
993
          {
994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013
            repeat split; try auto.
            - rewrite afQ2R_mkErrorPolyQ.
              apply mkErrorPolyR_fresh_compat; lia.
            - intros n' Hn'.
              unfold updMap.
              destruct (n' =? noise1) eqn: Hneq.
              + apply beq_nat_true in Hneq.
                lia.
              + apply Hnoise_map1.
                lia.
            - rewrite FloverMapFacts.P.F.add_eq_o; auto.
            - apply computeErrorR_pos.
            - rewrite afQ2R_mkErrorPolyQ.
              rewrite computeErrorQ_computeErrorR.
              rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
            - erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
              now match goal with
                  | [H1: FloverMap.find e' A = Some (iv__A0, err__A0),
                         H2: FloverMap.find e' A = Some (iv__A, err__A) |- _] => rewrite H1 in H2; inversion H2
                  end.
1014 1015 1016
            - erewrite meps_0_deterministic with (v1 := v__R0) (v2 := v__R); eauto.
              erewrite eval_expr_functional with (v1 := v__FP0) (v2 := v__FP); eauto.
              erewrite Gamma_det; eauto.
1017
          }
1018
      }
1019 1020 1021 1022 1023 1024
Qed.

Lemma validErrorboundAA_sound_const v m E1 E2 A Gamma DeltaMap fVars dVars:
  validErrorboundAA_sound_statement (Expressions.Const m v) E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
  unfold validErrorboundAA_sound_statement.
1025
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
1026 1027 1028 1029 1030 1031 1032 1033 1034
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
                     Hcheckedex Hcheckedall;
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (Expressions.Const m v) expr_map1) eqn: Hmem; cbn in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
    inversion Hvalidbounds; subst; clear Hvalidbounds.
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
1035
    specialize (Hcheckedex _ Hmem) as (Hvars & Hcert' & Hcheckedex).
1036
    repeat split.
1037
    1-4: congruence.
1038 1039 1040 1041 1042
    intros v__FP m__FP Heval__FP.
    unfold checked_error_expressions in Hcheckedall.
    specialize (Hcheckedall v__R v__FP m__FP iv__A err__A) as (af & err__af & Hcheckedall); auto.
    exists af, err__af, noise_map1.
    intuition.
1043
  }
1044 1045 1046
  destruct (Htypecheck) as (m__e & Hetype & _ & Hvalidexec).
  rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; cbn in Hvalidbounds.
1047
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
1048 1049 1050
  destruct (Qleb (computeErrorQ (maxAbs iv__A) m) err__A) eqn: Herrle; cbn in Hvalidbounds; [|congruence].
  inversion Hvalidbounds; subst; clear Hvalidbounds.
  rewrite mem_false_find_none in Hmem.
1051 1052
  split.
  - assert (exists (v__FP : R) (m__FP : mType),
1053
               eval_expr E2 (toRExpMap Gamma) DeltaMap
1054 1055
                             (toRExp (Expressions.Const m v)) v__FP m__FP).
    {
1056
      specialize (Hdeltamap (Q2R v) m)
1057 1058
        as (delta' & Hdelta & Hdelta').
      exists (perturb (Q2R v) m delta'), m.
1059
      eapply Const_dist' with (delta := delta'); auto.
1060 1061 1062 1063
    }
    split; auto.
    intros e' Hnin Hin.
    destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq].
1064 1065
    split; [|split; [|now rewrite Hexpeq]].
    1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq;
1066
      try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1067 1068
    1: now apply subset_diff_to_subset_union.
    erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
1069
  - rewrite Qle_bool_iff in Herrle.
1070
    apply Qle_Rle in Herrle.
1071
    intros * Heval__FP.
1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093
    inversion Heval__R; subst.
    inversion Heval__FP; subst.
    cbn in Htypecheck.
    cbn in Hrange.
    destruct Hrange as (_ & tmpiv & tmperr & tmpvR & Hres__A' & Heval1' & Hcontained).
    rewrite Hcert in Hres__A'.
    replace tmpiv with iv__A in * by congruence.
    replace tmperr with err__A in * by congruence; clear Hres__A' tmperr tmpiv.
    pose proof Heval__R as Heval__R'.
    eapply meps_0_deterministic in Heval__R'; try exact Heval1'.
    cbn in Heval__R'.
    replace tmpvR with (Q2R v) in * by congruence; clear Heval1' Heval__R' tmpvR.
    cbn in Heval__R, Heval__FP.
    assert (exists q, af_evals (afQ2R (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1)) (Q2R v - perturb (Q2R v) m__FP delta0)%R (updMap noise_map1 noise1 q)) as [q Hevals].
    {
      rewrite afQ2R_mkErrorPolyQ.
      rewrite computeErrorQ_computeErrorR.
      apply af_evals_mkErrorPolyR_updMap; auto using computeErrorR_pos.
      rewrite <- maxAbs_impl_RmaxAbs_iv.
      destruct iv__A as [liv__A hiv__A].
      cbn in Hcontained |-*.
      pose proof (@const_abs_err_bounded (Q2R v) (Q2R v) (perturb (Q2R v) m__FP delta0)
1094
                                         E1 E2 m__FP _ _ Heval__R Heval__FP) as H'.
1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113
      apply (Rle_trans _ _ _ H').
      apply computeErrorR_up.
      apply contained_leq_maxAbs.
      now cbn.
    }
    assert (forall n : nat, (n >= noise1 + 1)%nat -> updMap noise_map1 noise1 q n = None).
    {
      intros n' Hn'.
      unfold updMap.
      destruct (n' =? noise1) eqn: Hneq.
      * apply beq_nat_true in Hneq.
        lia.
      * apply Hnoise_map1.
        lia.
    }
    exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
    (Q2R (computeErrorQ (maxAbs iv__A) m__FP)), (updMap noise_map1 noise1 q).
    rewrite computeErrorQ_computeErrorR in Herrle |-*.
    repeat split; auto.
1114
    + now apply contained_flover_map_extension.
1115 1116 1117 1118 1119 1120
    + lia.
    + rewrite afQ2R_mkErrorPolyQ.
      apply mkErrorPolyR_fresh_compat; lia.
    + apply contained_map_extension; auto.
    + rewrite FloverMapFacts.P.F.add_eq_o; try auto.
      apply Q_orderedExps.exprCompare_refl.
1121
    + apply computeErrorR_pos.
1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133
    + rewrite afQ2R_mkErrorPolyQ.
      rewrite computeErrorQ_computeErrorR.
      rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
    + intros e' Hnin Hin.
      unfold checked_error_expressions.
      pose proof (flover_map_el_eq_extension Hnin Hin) as [Hexeq Hreq].
      rewrite Hreq.
      intros.
      exists (mkErrorPolyQ (computeErrorQ (maxAbs iv__A) m__FP) noise1),
      (Q2R (computeErrorQ (maxAbs iv__A) m__FP)).
      rewrite computeErrorQ_computeErrorR.
      repeat split; try auto.
1134 1135
      * rewrite afQ2R_mkErrorPolyQ.
        apply mkErrorPolyR_fresh_compat; lia.
1136 1137
      * rewrite FloverMapFacts.P.F.add_eq_o; auto.
      * apply computeErrorR_pos.
1138 1139 1140
      * rewrite afQ2R_mkErrorPolyQ.
        rewrite computeErrorQ_computeErrorR.
        rewrite toInterval_mkErrorPolyR; auto using computeErrorR_pos.
1141 1142 1143 1144 1145
      * erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
        now match goal with
            | [H1: FloverMap.find e' A = Some (iv__A0, err__A0),
                   H2: FloverMap.find e' A = Some (iv__A, err__A) |- _] => rewrite H1 in H2; inversion H2
            end.
1146
      * erewrite meps_0_deterministic
1147
          with (v1 := v__R) (v2 := (perturb (Q2R v) REAL delta)); eauto.
1148
        erewrite eval_expr_functional
1149
          with (v1 := v__FP) (v2 := (perturb (Q2R v) m__FP delta0)); eauto.
1150
        erewrite Gamma_det; eauto.
1151 1152 1153 1154 1155 1156 1157 1158
Qed.

Lemma validErrorboundAA_sound_unop u e E1 E2 A Gamma DeltaMap fVars dVars:
  validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars ->
  validErrorboundAA_sound_statement (Unop u e) E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
  intros IHe.
  unfold validErrorboundAA_sound_statement in IHe |-*.
1159
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
1160
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
1161
                     Hcheckedex Hcheckedall.
1162 1163 1164 1165 1166
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (elt:=affine_form Q) (Unop u e) expr_map1) eqn: Hmem;
    simpl in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
1167
    inversion Hvalidbounds; subst; clear Hvalidbounds.
1168 1169
    apply FloverMap.mem_2 in Hmem.
    specialize (Hcheckedall _ Hmem).
1170
    specialize (Hcheckedex _ Hmem) as (Hvars & ? & Hcheckedex).
1171
    repeat split.
1172
    1-4: congruence.
1173 1174 1175 1176 1177
    intros v__FP m__FP Heval__FP.
    unfold checked_error_expressions in Hcheckedall.
    specialize (Hcheckedall v__R v__FP m__FP iv__A err__A) as (af & err__af & Hcheckedall); auto.
    exists af, err__af, noise_map1.
    intuition.
1178 1179 1180 1181
  }
  destruct Htypecheck as (m__e & Hetype & (Htypecheck__e & ?) & Hvalidexec).
  rewrite Hetype in Hvalidbounds; simpl in Hvalidbounds.
  rewrite Hcert in Hvalidbounds; simpl in Hvalidbounds.
1182
  destruct (negb (Qleb 0 err__A)) eqn: H0err; [congruence|].
1183 1184 1185 1186 1187 1188 1189 1190 1191 1192
  destruct u; [|congruence].
  destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1)
    as [(subexpr_map, subnoise)|] eqn: Hvalidsubexpr;
    simpl in Hvalidbounds; try congruence.
  destruct (FloverMap.find e subexpr_map) as [subaf|] eqn: Hsubaf;
    simpl in Hvalidbounds; [|congruence].
  destruct (FloverMap.find e A) as [(subiv, suberr)|] eqn: Hsuba;
    simpl in Hvalidbounds; [|congruence].
  destruct (Qeq_bool err__A suberr) eqn: Heq__err; simpl in Hvalidbounds; [|congruence].
  inversion Hvalidbounds; subst; clear Hvalidbounds.
1193
  inversion Heval__R; subst.
1194 1195 1196
  unfold isCompat in H2.
  destruct m; cbn in H2; try congruence; clear H2.
  pose proof H3 as H3det.
1197
  specialize (IHe expr_map1 subexpr_map noise_map1 noise1 noise2 v1 subiv suberr).
1198
  specialize IHe as (IHevex & IHevall); eauto;
1199 1200 1201 1202
    [destruct Hrange; auto|].
  split.
  - destruct IHevex as ((nF & m & IHeval) & IHcheckedex).
    assert (exists (v__FP : R) (m__FP : mType),
1203
               eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Unop Neg e)) v__FP m__FP).
1204 1205
    {
      exists (evalUnop Neg nF); exists m__e.
1206
      eapply Unop_neg'; eauto.
1207 1208 1209
      { eapply toRExpMap_some with (e:=Unop Neg e); eauto. }
      { destruct H as [? [? ?]].
        assert (x = m).
1210
        { eapply validTypes_exec; eauto. }
1211 1212 1213 1214 1215
        subst; auto. }
    }
    split; auto.
    intros e' Hnin Hin.
    destruct (flover_map_in_dec e' subexpr_map) as [Hin1|Hnin1].
1216
    + edestruct IHcheckedex as (? & ? & ?); eauto.
1217
    + destruct (flover_map_el_eq_extension Hnin1 Hin) as [Heq Hexpeq]; auto.
1218 1219
      split; [|split; [|now rewrite Hexpeq]].
      1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq;
1220
        try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1221 1222
      1: now apply subset_diff_to_subset_union.
      erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
1223 1224 1225 1226
  - intros v__FP m__FP Heval__FPdet.
    inversion Heval__FPdet; subst.
    pose proof H5 as H5det.
    specialize (IHevall v0 m)
1227
      as (ihaf & iherr__af & ihnoise_map & IHcontf & IHnoise & IHfresh & IHcontn & IHnoise_map &
1228 1229 1230 1231 1232 1233 1234
          IHsub__A & IHerrpos & IHiv__err & IHerr & IHevals & IHchecked); auto.
    replace subaf with ihaf by congruence.
    apply Qeq_bool_eq in Heq__err.
    apply Qeq_eqR in Heq__err.
    rename v0 into nF.
    exists (AffineArithQ.negate_aff ihaf), iherr__af, ihnoise_map.
    repeat split; auto.
1235 1236 1237 1238 1239
    + pose proof contained_flover_map_extension as H'.
      rewrite mem_false_find_none in Hmem.
      specialize (H' _ expr_map1 _ (AffineArithQ.negate_aff ihaf) Hmem).
      etransitivity; try eassumption.
      now apply contained_flover_map_add_compat.
1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256
    + rewrite afQ2R_negate_aff.
      unfold negate_aff.
      now apply mult_aff_const_fresh_compat.
    + rewrite FloverMapFacts.P.F.add_eq_o; try auto.
      apply Q_orderedExps.exprCompare_refl.
    + rewrite afQ2R_negate_aff.
      rewrite toInterval_negate_aff.
      rewrite IHiv__err.
      cbn.
      f_equal; lra.
    + now rewrite Heq__err.
    + rewrite Rsub_eq_Ropp_Rplus in IHevals.
      cbn.
      field_rewrite (- v1 - - nF = - (v1 - nF))%R.
      rewrite afQ2R_negate_aff.
      now apply negate_aff_sound.
    + intros e' Hnin Hin.
1257
      {
1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279
        destruct (FloverMapFacts.O.MO.eq_dec (Unop Neg e) e') as [Heqexp|Heqexp].
        - unfold checked_error_expressions.
          pose proof (expr_compare_eq_eval_compat _ _ Heqexp) as Hreq.
          rewrite <- Hreq.
          intros.
          exists (AffineArithQ.negate_aff ihaf), iherr__af.
          repeat split; try auto.
          + rewrite afQ2R_negate_aff.
            unfold negate_aff.
            now apply mult_aff_const_fresh_compat.
          + rewrite FloverMapFacts.P.F.add_eq_o; try auto.
          + rewrite afQ2R_negate_aff.
            rewrite toInterval_negate_aff.
            rewrite IHiv__err.
            cbn.
            f_equal; lra.
          + erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
            match goal with
            | [H1: FloverMap.find e' A = Some (iv__A0, err__A0),
                   H2: FloverMap.find e' A = Some (iv__A, err__A) |- _] => rewrite H1 in H2; inversion H2
            end.
            now rewrite Heq__err.
1280
          + erewrite meps_0_deterministic
1281
              with (v1 := v__R) (v2 := (evalUnop Neg v1)); eauto.
1282
            erewrite eval_expr_functional
1283
              with (v1 := v__FP) (v2 := (evalUnop Neg nF)); eauto;
1284
              [|erewrite Gamma_det; eauto].
1285 1286 1287 1288 1289 1290 1291 1292 1293
            rewrite Rsub_eq_Ropp_Rplus in IHevals.
            cbn.
            field_rewrite (- v1 - - nF = - (v1 - nF))%R.
            rewrite afQ2R_negate_aff.
            now apply negate_aff_sound.
        - destruct (FloverMapFacts.P.F.In_dec subexpr_map e') as [Hsubin|Hsubnin].
          + apply checked_error_expressions_flover_map_add_compat; auto.
          + pose proof (flover_map_el_eq_extension Hsubnin Hin) as [Hexeq Hreq].
            congruence.
1294
      }
1295 1296
Qed.

1297
Lemma validErrorboundAA_sound_plus e1 e2 E1 E2 A Gamma DeltaMap fVars dVars:
1298 1299
  validErrorboundAA_sound_statement e1 E1 E2 A Gamma DeltaMap fVars dVars ->
  validErrorboundAA_sound_statement e2 E1 E2 A Gamma DeltaMap fVars dVars ->
1300
  validErrorboundAA_sound_statement (Binop Plus e1 e2) E1 E2 A Gamma DeltaMap fVars dVars.
1301 1302 1303
Proof.
  intros IHe1 IHe2.
  unfold validErrorboundAA_sound_statement in IHe1, IHe2 |-*.
1304
  intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds
1305 1306
                     Hsubset Htypecheck Hcert Hnoise1 Hnoise_map1 Hdvars
                     Hcheckedex Hcheckedall;
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1307 1308 1309 1310
  cbn in Hvalidbounds.
  destruct (FloverMap.mem (Binop Plus e1 e2) expr_map1) eqn: Hmem; cbn in Hvalidbounds.
  {
    symmetry in Hvalidbounds.
Nikita Zyuzin's avatar