Commit 139e47af authored by Heiko Becker's avatar Heiko Becker
Browse files

Finish HOL4 port

parent a2c542f0
(**
This file contains the HOL4 implementation of the certificate checker as well as its soundness proof.
The checker is a composition of the range analysis validator and the error bound validator.
Running this function on the encoded analysis result gives the desired theorem
as shown in the soundness theorem.
**)
open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory ErrorValidationTheory
val _ = new_theory "CertificateChecker";
(** Certificate checking function **)
val CertificateChecker_def = Define
`CertificateChecker (e:real exp) (absenv:analysisResult) (P:precond) =
((validIntervalbounds e absenv P) /\ (validErrorbound e absenv))`;
(**
Soundness proof for the certificate checker.
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
**)
val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
``!(e:real exp) (absenv:analysisResult) P (cenv:env) (vR:real) (vF:real).
eval_exp 0 cenv P e vR /\
eval_exp machineEpsilon cenv P e vF /\
CertificateChecker e absenv P ==>
abs (vR - vF) <= (SND (absenv e))``,
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
simp [CertificateChecker_def] \\
rpt strip_tac \\
Cases_on `absenv e` \\
rename1 `absenv e = (iv, err)` \\
Cases_on `iv` \\
rename1 `absenv e = ((elo, ehi), err)` \\
match_mp_tac validErrorbound_sound \\
qexistsl_tac [`e`, `cenv`, `absenv`, `P`, `elo`, `ehi`] \\
fs[]);
val _ = export_theory();
(**
This file contains the coq implementation of the error bound validator as well
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
......
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