Commit 724d0058 authored by Heiko Becker's avatar Heiko Becker

Add two new inference function inferErrorbound and inferIntervalbound.

The functions can be used to generate HOL4 level certificates without stepping
out of the logic and calling Daisy. As the functions are not verified their
returned certificate should still be send through the checker pipeline.
The sole benefit of the functions is that they can be used as in-logic
generators for checker input.
parent 9b99148c
(**
This file contains the HOL4 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.
**)
open simpLib realTheory realLib RealArith pred_setTheory;
open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
RealRangeArithTheory FloverTactics MachineTypeTheory
ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
TypeValidatorTheory IntervalValidationTheory EnvironmentsTheory
RealIntervalInferenceTheory
CommandsTheory ssaPrgsTheory FloverMapTheory;
open preamble;
val _ = new_theory "ErrorIntervalInference";
val inferErrorbound_def = Define `
inferErrorbound e (typeMap: typeMap) (I:ivMap) (akk:analysisResult) :analysisResult option=
(case (FloverMapTree_find e akk) of
| SOME _ => SOME akk
| NONE =>
do
iv_f <- FloverMapTree_find e I;
m <- FloverMapTree_find e typeMap;
(case e of
| Var v =>
SOME (FloverMapTree_insert e (iv_f, computeError (maxAbs iv_f) m) akk)
| Const _ n =>
SOME (FloverMapTree_insert e (iv_f, computeError (maxAbs iv_f) m) akk)
| Unop Neg e1 =>
do
recRes <- inferErrorbound e1 typeMap I akk;
(iv, err1) <- FloverMapTree_find e1 recRes;
SOME (FloverMapTree_insert e (iv_f, err1) recRes);
od
| Unop Inv e1 => NONE
| Binop op e1 e2 =>
do
recRes1 <- inferErrorbound e1 typeMap I akk;
recRes2 <- inferErrorbound e2 typeMap I recRes1;
(ive1, err1) <- FloverMapTree_find e1 recRes2;
(ive2, err2) <- FloverMapTree_find e2 recRes2;
let errIve1 = widenInterval ive1 err1 in
let errIve2 = widenInterval ive2 err2 in
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
if ((op = Div /\ noDivzero (IVhi errIve2) (IVlo errIve2) \/ op <> Div))
then
let eNew =
(case op of
| Plus =>
let mAbs = maxAbs (addInterval errIve1 errIve2) in
err1 + err2 + computeError mAbs m
| Sub =>
let mAbs = maxAbs (subtractInterval errIve1 errIve2) in
err1 + err2 + computeError mAbs m
| Mult =>
let mAbs = maxAbs (multInterval errIve1 errIve2);
eProp = upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2 in
eProp + computeError mAbs m
| Div =>
let upperBoundInvE2 = maxAbs (invertInterval ive2);
minAbsIve2 = minAbsFun (errIve2);
errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2;
mAbs = maxAbs (divideInterval errIve1 errIve2);
eProp = upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv in
eProp + computeError mAbs m)
in
SOME (FloverMapTree_insert e (iv_f, eNew) recRes2)
else NONE;
od
| Fma e1 e2 e3 =>
do
recRes1 <- inferErrorbound e1 typeMap I akk;
recRes2 <- inferErrorbound e2 typeMap I recRes1;
recRes3 <- inferErrorbound e3 typeMap I recRes2;
(ive1, err1) <- FloverMapTree_find e1 recRes3;
(ive2, err2) <- FloverMapTree_find e2 recRes3;
(ive3, err3) <- FloverMapTree_find e3 recRes3;
let errIve1 = widenInterval ive1 err1;
errIve2 = widenInterval ive2 err2;
errIve3 = widenInterval ive3 err3;
upperBoundE1 = maxAbs ive1;
upperBoundE2 = maxAbs ive2;
upperBoundE3 = maxAbs ive3;
errIntv_prod = multInterval errIve2 errIve3;
mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3);
mAbs = maxAbs (addInterval errIve1 errIntv_prod);
eNew = err1 + mult_error_bound + computeError mAbs m
in
SOME (FloverMapTree_insert e (iv_f, eNew) recRes3);
od
| Downcast m1 e1 =>
do
recRes <- inferErrorbound e1 typeMap I akk;
(ive1, err1) <- FloverMapTree_find e1 recRes;
let errIve1 = widenInterval ive1 err1;
mAbs = maxAbs errIve1;
eNew = err1 + computeError mAbs m1;
in
SOME (FloverMapTree_insert e (iv_f, eNew) recRes)
od)
od)`;
val inferErrorboundCmd_def = Define `
inferErrorboundCmd (f:real cmd) (typeMap: (real expr # mType) binTree)
(I:ivMap) (akk:analysisResult) =
case f of
| Let m x e g =>
do
recRes <- inferErrorbound e typeMap I akk;
(ive, erre) <- FloverMapTree_find e recRes;
inferErrorboundCmd g typeMap I (FloverMapTree_insert (Var x) (ive, erre) recRes);
od
| Ret e =>
inferErrorbound e typeMap I akk`;
val _ = export_theory();
(**
Interval arithmetic checker and its soundness proof.
The function validIntervalbounds checks wether the given analysis result is
a valid range arithmetic for each sub term of the given exprression e.
The computation is done using our formalized interval arithmetic.
The function is used in CertificateChecker.v to build the full checker.
**)
open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
sptreeLib;
open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics
ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
MachineTypeTheory FloverMapTheory TypeValidatorTheory RealRangeArithTheory
ExpressionSemanticsTheory;
open preamble;
val _ = new_theory "RealIntervalInference";
val _ = monadsyntax.enable_monadsyntax();
val _ = List.app monadsyntax.enable_monad ["option"];
val _ = type_abbrev ("ivMap", ``:(real # real) fMap``);
val inferIntervalbounds_def = Define `
inferIntervalbounds f (P:precond) (akk:ivMap) :ivMap option =
(case (FloverMapTree_find f akk) of
| SOME intv => SOME akk
| NONE =>
(case f of
| Var v =>
SOME (FloverMapTree_insert f (P v) akk)
| Const m n =>
SOME (FloverMapTree_insert f (n,n) akk)
| Unop op f1 =>
do
recRes <- inferIntervalbounds f1 P akk;
iv_f1 <- FloverMapTree_find f1 recRes;
case op of
| Neg =>
SOME (FloverMapTree_insert f (negateInterval iv_f1) recRes)
| _ => NONE
od
| Downcast m f1 =>
do
recRes <- inferIntervalbounds f1 P akk;
iv_f1 <- FloverMapTree_find f1 recRes;
SOME (FloverMapTree_insert f iv_f1 recRes);
od
| Binop op f1 f2 =>
do
recRes1 <- inferIntervalbounds f1 P akk;
recRes2 <- inferIntervalbounds f2 P recRes1;
iv_f1 <- FloverMapTree_find f1 recRes2;
iv_f2 <- FloverMapTree_find f2 recRes2;
if (op = Div /\ (IVlo iv_f2 <= 0 /\ 0 <= IVhi iv_f2))
then NONE
else
SOME
(let new_iv =
(case op of
| Plus => addInterval iv_f1 iv_f2
| Sub => subtractInterval iv_f1 iv_f2
| Mult => multInterval iv_f1 iv_f2
| Div => divideInterval iv_f1 iv_f2)
in FloverMapTree_insert f new_iv recRes2);
od
| Fma f1 f2 f3 =>
do
recRes1 <- inferIntervalbounds f1 P akk;
recRes2 <- inferIntervalbounds f2 P recRes1;
recRes3 <- inferIntervalbounds f3 P recRes2;
iv_f1 <- FloverMapTree_find f1 recRes3;
iv_f2 <- FloverMapTree_find f2 recRes3;
iv_f3 <- FloverMapTree_find f3 recRes3;
SOME (FloverMapTree_insert f (addInterval iv_f1 (multInterval iv_f2 iv_f3)) recRes3);
od))`;
val inferIntervalboundsCmd_def = Define `
inferIntervalboundsCmd (f:real cmd) (P:precond) (akk:ivMap) :ivMap option =
case f of
| Let m x e g =>
do
recRes <- inferIntervalbounds e P akk;
iv_x <- FloverMapTree_find e recRes;
inferIntervalboundsCmd g P (FloverMapTree_insert (Var x) iv_x recRes);
od
| Ret e => inferIntervalbounds e P akk`;
val _ = export_theory();
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