(** Definition of the computation of the absolute error. used to verify analsysis result in the final theorem of a certificate. **) Require Import Coq.Reals.Reals. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealConstruction Daisy.Infra.RealSimps. Require Import Daisy.IntervalArith Daisy.Expressions Daisy.Commands. Definition abs_env:Type := exp R -> interval -> err -> Prop. (** First define when given an interval and an error, when another error is sound overapproximation of the absolute error **) Definition isSoundErr (error:err) (iv:interval) (propagatedErr:err) := (error >= machineEpsilon * Rmax (Rabs (IVlo iv)) (Rabs (IVhi iv)))%R. Definition maxAbs (IV:interval) := Rmax (Rabs (IVlo IV)) (Rabs (IVhi IV)). Definition mult_err (e1:exp R) (val_e1:ann) (e2:exp R) (val_e2:ann) := (maxAbs (addInterval (addInterval (multInterval (getIntv val_e1) (getErr val_e2, getErr val_e2)) (multInterval (getIntv val_e2) (getErr val_e1, getErr val_e1))) (multInterval (multInterval (multInterval (getIntv val_e1) (getIntv val_e2)) (getErr val_e1, getErr val_e1)) (getErr val_e2, getErr val_e1)))). Definition isSoundErrBin (op:binop) (e1:exp R) (val_e1:ann) (e2:exp R) (val_e2:ann) (val:ann):= match op with Plus => isSupersetInterval (getIntv val) (addInterval (getIntv val_e1) (getIntv val_e2)) /\ isSoundErr (getErr val) (getIntv val) (getErr val_e1 + getErr val_e2)%R |Sub => isSupersetInterval (getIntv val) (subtractInterval (getIntv val_e1) (getIntv val_e2)) /\ isSoundErr (getErr val) (getIntv val) (getErr val_e1 - getErr val_e2)%R |Mult => isSupersetInterval (getIntv val) (multInterval (getIntv val_e1) (getIntv val_e2)) /\ isSoundErr (getErr val) (getIntv val) (mult_err e1 val_e1 e2 val_e2) |Div (** FIXME!! **) => (isSupersetInterval (getIntv val) (intv_div_err (getIntv val_e1) (getErr val_e1) (getIntv val_e2) (getErr val_e2)) /\ isSoundErr (getErr val) (getIntv val) (mult_err e1 val_e1 e2 (((/ IVlo (getIntv val_e2))%R, (/ IVhi (getIntv val_e2))%R), getErr val_e2))) end. Inductive AbsErrExp : exp R -> abs_env -> err -> Prop := AbsErrConst n iv e (env:abs_env): env (Const n) (iv) e -> isSoundErr e iv machineEpsilon -> AbsErrExp (Const n) env e |AbsErrVar v iv e (env:abs_env): env (Var R v) iv e -> isSoundErr e iv machineEpsilon -> AbsErrExp (Var R v) env e |AbsErrParam v iv e (env:abs_env): env (Param R v) iv e -> isSoundErr e iv machineEpsilon -> AbsErrExp (Param R v) env e |AbsErrBinop op e1 iv1 er1 e2 iv2 er2 iv eabs (env:abs_env): env e1 iv1 er1 -> env e2 iv2 er2 -> env (Binop op e1 e2) iv eabs -> AbsErrExp e1 env er1 -> AbsErrExp e2 env er2 -> isSoundErrBin op e1 (iv1,er1) e2 (iv2,er2) (iv,eabs) -> AbsErrExp (Binop op e1 e2) env eabs. Definition AbsErrBExp (c: bexp R) (err:intv*err) := True. Inductive AbsErrPrg : cmd R -> abs_env -> err -> Prop := AbsErrLet (x:nat) e s iv er (env:abs_env) err: env e iv er -> AbsErrExp e env er -> (env (Var R x) iv er) -> AbsErrPrg s env err -> AbsErrPrg (Let R x e s) env err |AbsErrIte c s t env err: (* AbsErrBExp c (env c) -> *) AbsErrPrg s env err -> AbsErrPrg t env err -> AbsErrPrg (Ite R c s t) env err |AbsErrRet e iv er (env:abs_env) : env e iv er -> AbsErrExp e env er -> AbsErrPrg (Ret R e) env er.