Commit 9c38c892 authored by Heiko Becker's avatar Heiko Becker

Start working on AA error validator, implement function first

parent b93f1500
(**
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
micromega.Psatz Reals.Reals.
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
RealRangeValidator ErrorBounds AffineForm AffineArith AffineArithQ.
(** 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 *)
:option (FloverMap.t (affine_form Q) * nat) :=
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 *)
if (negb (Qleb 0 err))
then None
else
(* We have already checked a subexpression *)
if (FloverMap.mem e errMap)
then Some (errMap, currNoise)
else
(* case analysis for the expression *)
match e with
| Var _ x =>
if (NatSet.mem x dVars)
then Some (errMap, currNoise) (* previously checked defined variable *)
else
(* Build an affine polynomial *)
let errNew := computeErrorQ (maxAbs intv) m in
let af := fromIntv (mkIntv (-errNew) errNew) currNoise in
if (Qleb errNew err)
then Some (FloverMap.add e af errMap, (currNoise+1)%nat)
else None
| Expressions.Const m v =>
let errNew := computeErrorQ (maxAbs intv) m in
let af := fromIntv (mkIntv (-errNew) errNew) currNoise in
if (Qleb errNew err)
then Some (FloverMap.add (elt:=affine_form Q) e af errMap, (currNoise+1)%nat)
else None
| Unop Neg e1 =>
olet res := validErrorboundAA e1 typeMap A dVars currNoise errMap in
let (newErrorMap, maxNoise) := res in
olet afPolye1 := FloverMap.find e1 newErrorMap in
match FloverMap.find e1 A with
| Some (iv_e1, err1) =>
if (Qeq_bool err err1)
then Some (FloverMap.add e afPolye1 newErrorMap, maxNoise)
else None
| None => None
end
| Unop Inv e1 => None
| Binop b e1 e2 =>
olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
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
| None, _ => None
| _, None => None
| Some (ive1, err1), Some (ive2, err2) =>
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
let errPoly := plus_aff
(plus_aff afPolye1 afPolye2)
(fromIntv (mkIntv (-errNew) errNew) maxNoise2) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
else None
| Sub =>
let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff
(subtract_aff afPolye1 afPolye2)
(fromIntv (mkIntv (-errNew) errNew) maxNoise2) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
else None
| Mult =>
let aaRangee1 := fromIntv ive1 maxNoise2 in
let aaRangee2 := fromIntv ive2 (maxNoise2 + 1) in
let propError := plus_aff
(plus_aff (mult_aff aaRangee1 afPolye2 (maxNoise2 + 2))
(mult_aff aaRangee2 afPolye1 (maxNoise2 + 3) ))
(mult_aff afPolye1 afPolye2 (maxNoise2 + 4)) in
let mAbs := (maxAbs (multIntv errIve1 errIve2)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff propError
(fromIntv (mkIntv (-errNew) errNew) (maxNoise2 + 5)) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 6)%nat)
else None
| Div =>
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
let invertede2 := invertIntv ive2 in
let aaRangeInve2 := fromIntv invertede2 (maxNoise2 + 1) in
let invertedErre2 := inverse_aff afPolye2 (maxNoise2 + 2) (* TODO invert *) in
let propError := plus_aff
(plus_aff (mult_aff aaRangee1 invertedErre2 (maxNoise2 + 3))
(mult_aff aaRangeInve2 afPolye1 (maxNoise2 + 4)))
(mult_aff afPolye1 invertedErre2 (maxNoise2 + 5)) in
let mAbs := (maxAbs (divideIntv errIve1 errIve2)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff propError
(fromIntv (mkIntv (-errNew) errNew) (maxNoise2 + 6)) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 7)%nat)
else None
else None
end
end
| Fma e1 e2 e3 =>
olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
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
| None, _, _ => None
| _, None, _ => None
| _, _, None => None
| 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
let aaRangee1 := fromIntv ive1 maxNoise2 in
let aaRangee2 := fromIntv ive2 (maxNoise2 + 1) in
let propError := plus_aff
(plus_aff
(plus_aff (mult_aff aaRangee1 afPolye2 (maxNoise2 + 2))
(mult_aff aaRangee2 afPolye1 (maxNoise2 + 3) ))
(mult_aff afPolye1 afPolye2 (maxNoise2 + 4)))
afPolye3 in
let mAbs := (maxAbs (addIntv (multIntv errIve1 errIve2) errIve3)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff propError
(fromIntv (mkIntv (-errNew) errNew) (maxNoise2 + 5)) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 6)%nat)
else None
end
| Downcast m e1 =>
olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
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
let errPoly := plus_aff afPolye1
(fromIntv (mkIntv (-newErr) newErr) maxNoise1) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap1, (maxNoise1 + 1)%nat)
else None
end.
(** Error bound command validator **)
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 *)
(currNoise: nat) (* current maximal noise term *)
(errMap:FloverMap.t (affine_form Q)) (* previously seen affine polys *)
:option (FloverMap.t (affine_form Q) * nat) :=
match f with
|Let m x e g =>
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 validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1
(FloverMap.add (Var Q x) afPolye errMap1)
else None
| _,_ => None
end
|Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
end.
......@@ -2,7 +2,7 @@ From Coq
Require Import Reals.Reals QArith.Qreals.
From Flover
Require Export Infra.ExpressionAbbrevs ErrorValidation.
Require Export Infra.ExpressionAbbrevs ErrorValidation RealRangeValidator.
Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
(* if *)
......@@ -19,7 +19,7 @@ forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
NatSet.Subset (usedVars e -- dVars) fVars ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
RoundoffErrorValidator e Gamma A dVars = true ->
IntervalValidation.validIntervalbounds e A P dVars = true ->
RangeValidator e A P dVars = true ->
IntervalValidation.dVars_range_valid dVars E1 A ->
IntervalValidation.fVars_P_sound fVars E1 P ->
IntervalValidation.vars_typed (fVars dVars) defVars ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment