Commit 99aecf45 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Merge branch 'master' into affine_arithmetic_merge

Conflicts:
	coq/IEEE_connection.v
	coq/Infra/Abbrevs.v
	coq/Infra/ExpressionAbbrevs.v
	coq/Infra/Ltacs.v
	coq/Infra/RationalSimps.v
	coq/ssaPrgs.v
parents 29b21eb6 8414e5ff
......@@ -9,11 +9,7 @@ ckpt*
hol/run_hol.sh
coq/_CoqProject
coq/*.glob
coq/*.vo
coq/.*
coq/*.v.d
coq/*/*.v.d
coq/Makefile*
coq/*/*.glob
coq/*/.*
......@@ -26,21 +22,25 @@ coq/binary/CoqChecker*
coq/binary/coq_checker_*
coq/binary/*.cmx
coq/binary/*.o
**/*.glob
**/*.vo
**/*.v.d
**/*.v.d
hol4/*Theory*
hol4/*.ui
hol4/*.uo
hol4/.*
hol4/*/*Theory*
hol4/*/*.ui
hol4/*/*.uo
hol4/*/.*
hol4/*/heap
hol4/heap
hol4/output/*.sml
hol4/binary/cake_checker
hol4/binary/checker.S
hol4/output/certificate_*
**/*Theory*
**/heap
**/.HOLMK
rawdata/*
.ensime*
......
image: localhost:5000/flover
image: heikobecker/coq-polyml-ci
variables:
GIT_SUBMODULE_STRATEGY: normal
GIT_SUBMODULE_STRATEGY: none
stages:
- compile
- regression
# - regression
compile-coq:
stage: compile
only:
- master
script: ./scripts/ci-coq.sh
artifacts:
expire_in: 24h
paths:
- coq/
compile-hol:
stage: compile
only:
- master
script: ./scripts/ci-hol4.sh
artifacts:
expire_in: 24h
paths:
- hol4/binary/
regression-tests:
stage: regression
only:
- master
script: ./scripts/regressiontests.sh
\ No newline at end of file
# regression-tests:
# stage: regression
# script: ./scripts/regressiontests.sh
\ No newline at end of file
FROM debian:latest
ENV HOLCOMMIT 60830f02ff6b86e0fd69ce6679614d497089b2eb
WORKDIR /root
#Necessary packages for opam
......@@ -17,20 +15,18 @@ RUN opam init --comp=4.05.0 --auto-setup && \
# Install coq and dependencies
RUN opam repo add coq-released https://coq.inria.fr/opam/released && \
opam update && \
opam install coq.8.7.2 coq-flocq
opam update
#Install coq 8.7.2 in a switch
RUN opam switch -A 4.05.0 coq8.7.2
RUN opam install coq.8.7.2 coq-flocq.2.6.1
#Install coq 8.8 in a switch
RUN opam switch -A 4.05.0 coq8.8
RUN opam install coq.8.8.0 coq-flocq.2.6.1
# Install polyml from git
RUN git clone https://github.com/polyml/polyml.git polyml && \
cd polyml && \
git checkout v5.7 && \
./configure && make && make install
# Download HOL4 and compile
RUN git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4 && \
cd HOL4 && \
git checkout $HOLCOMMIT &&\
poly < tools/smart-configure.sml && \
./bin/build
ENV HOLDIR /root/HOL4
......@@ -6,18 +6,18 @@
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
Require Import Flover.RealRangeValidator Flover.ErrorValidation Flover.Environments Flover.Typing Flover.FPRangeValidator.
Require Import Flover.RealRangeValidator Flover.RoundoffErrorValidator Flover.Environments Flover.Typing Flover.FPRangeValidator.
Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
let tMap := (typeMap defVars e (FloverMap.empty mType)) in
if (typeCheck e defVars tMap)
then
if RangeValidator e absenv P && FPRangeValidator e absenv tMap NatSet.empty
then (validErrorbound e tMap absenv NatSet.empty)
then RoundoffErrorValidator e tMap absenv NatSet.empty
else false
else false.
......@@ -26,7 +26,7 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (def
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars:
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
forall (E1 E2:env),
approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
(forall v, NatSet.In v (Expressions.usedVars e) ->
......@@ -38,10 +38,10 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVar
CertificateChecker e absenv P defVars = true ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
eval_exp E2 defVars (toRExp e) vF m /\
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\
eval_expr E2 defVars (toRExp e) vF m /\
(forall vF m,
eval_exp E2 defVars (toRExp e) vF m ->
eval_expr E2 defVars (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
......@@ -67,7 +67,7 @@ Proof.
edestruct (RangeValidator_sound e absenv (P:=P) (Gamma:=defVars) (E:=E1))
as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
destruct iv_e as [elo ehi].
edestruct (validErrorbound_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; split; auto.
Qed.
......@@ -93,7 +93,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
CertificateCheckerCmd f absenv P defVars = true ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\
bstep (toRCmd f) E2 defVars vF m /\
(forall vF m,
bstep (toRCmd f) E2 defVars vF m ->
......
......@@ -11,8 +11,8 @@ Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.
Only assignments and return statement
**)
Inductive cmd (V:Type) :Type :=
Let: mType -> nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V.
Let: mType -> nat -> expr V -> cmd V -> cmd V
| Ret: expr V -> cmd V.
Fixpoint getRetExp (V:Type) (f:cmd V) :=
match f with
......@@ -29,7 +29,7 @@ Fixpoint toRCmd (f:cmd Q) :=
Fixpoint toREvalCmd (f:cmd R) :=
match f with
|Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
|Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
|Ret e => Ret (toREval e)
end.
......@@ -38,10 +38,10 @@ UNUSED!
Small Step semantics for Flover language
Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
let_s x e s E v eps:
eval_exp eps E e v ->
eval_expr eps E e v ->
sstep (Let x e s) E eps s (updEnv x v E)
|ret_s e E v eps:
eval_exp eps E e v ->
eval_expr eps E e v ->
sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
*)
......@@ -51,15 +51,15 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
**)
Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_exp E defVars e v m ->
eval_expr E defVars e v m ->
bstep s (updEnv x v E) (updDefVars x m defVars) res m' ->
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
eval_exp E defVars e v m ->
eval_expr E defVars e v m ->
bstep (Ret e) E defVars v m.
(**
The free variables of a command are all used variables of expressions
The free variables of a command are all used variables of exprressions
without the let bound variables
**)
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
......
(**
Environment library.
Defines the environment type for the Flover framework and a simulation relation between environments.
Defines the environment type for the Flover framework and a simulation relation
between environments.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Flover.Infra.ExpressionAbbrevs Flover.Infra.RationalSimps Flover.Commands.
From Coq
Require Import Reals.Reals micromega.Psatz QArith.Qreals.
From Flover
Require Import Infra.ExpressionAbbrevs Infra.RationalSimps Commands.
(**
Define an approximation relation between two environments.
We use this relation for the soundness proofs.
It is necessary to have this relation, since two evaluations of the very same
expression may yield different values for different machine epsilons
exprression may yield different values for different machine epsilons
(or environments that already only approximate each other)
**)
Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
-> NatSet.t -> env -> Prop :=
|approxRefl defVars A:
approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
approxEnv E1 defVars A fVars dVars E2 ->
(Rabs (v1 - v2) <= (Rabs v1) * Q2R (mTypeToQ m))%R ->
(Rabs (v1 - v2) <= computeErrorR v1 m)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
approxEnv (updEnv x v1 E1)
(updDefVars x m defVars) A (NatSet.add x fVars) dVars
(updEnv x v2 E2)
|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err:
approxEnv E1 defVars A fVars dVars E2 ->
FloverMap.find (Var Q x) A = Some (iv, err) ->
(Rabs (v1 - v2) <= Q2R err)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
approxEnv (updEnv x v1 E1)
(updDefVars x m defVars) A fVars (NatSet.add x dVars)
(updEnv x v2 E2).
Section RelationProperties.
......@@ -68,7 +77,7 @@ Section RelationProperties.
E2 x = Some v2 ->
NatSet.In x fVars ->
Gamma x = Some m ->
(Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R.
(Rabs (v - v2) <= computeErrorR v m)%R.
Proof.
induction approxEnvs;
intros E1_def E2_def x_free x_typed.
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
From Flover
Require Import Expressions Commands Environments ssaPrgs Typing
IntervalValidation ErrorValidation Infra.Ltacs Infra.RealRationalProps.
(* TODO: Flocq ops open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory *)
Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Flover.Infra.MachineType Flover.Typing Flover.Infra.RealSimps Flover.IntervalValidation Flover.ErrorValidation Flover.Commands Flover.Environments Flover.ssaPrgs Flover.Infra.Ltacs Flover.Infra.RealRationalProps.
Fixpoint FPRangeValidator (e:exp Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
match FloverMap.find e typeMap, FloverMap.find e A with
|Some m, Some (iv_e, err_e) =>
let iv_e_float := widenIntv iv_e err_e in
......@@ -67,14 +64,14 @@ Ltac prove_fprangeval m v L1 R:=
|H: _ = true |- _ => andb_to_prop H
end);
destruct (Req_dec v 0); try auto;
destruct (Rle_lt_dec (Rabs v) (Q2R (minValue m)))%R (* denormal case *);
destruct (Rle_lt_dec (Rabs v) (Q2R (minValue_pos m)))%R (* denormal case *);
try auto;
destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.
Theorem FPRangeValidator_sound:
forall (e:exp Q) E1 E2 Gamma v m A tMap P fVars dVars,
forall (e:expr Q) E1 E2 Gamma v m A tMap P fVars dVars,
approxEnv E1 Gamma A fVars dVars E2 ->
eval_exp E2 Gamma (toRExp e) v m ->
eval_expr E2 Gamma (toRExp e) v m ->
typeCheck e Gamma tMap = true ->
validIntervalbounds e A P dVars = true ->
validErrorbound e tMap A dVars = true ->
......@@ -199,7 +196,7 @@ Proof.
- rewrite NatSet.add_spec, NatSet.union_spec in in_set;
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
{ eapply (swap_Gamma_bstep (Gamma1 := updDefVars n M0 (toRMap Gamma))); eauto.
{ eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
eauto using Rmap_updVars_comm. }
{ set_tac; split.
- split; try auto.
......
This diff is collapsed.
(**
(*
This file contains some type abbreviations, to ease writing.
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.MachineType.
Global Set Implicit Arguments.
(**
We define Intervals twice.
First we define intervals of reals and fractions.
......@@ -62,18 +61,3 @@ Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
Definition updDefVars (x:nat) (m:mType) (defVars:nat -> option mType) (y:nat) :=
if (y =? x) then Some m else defVars y.
Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
match v with
| Some v => f v
| None => e
end.
Notation "'olet' x ':=' u 'in' t" := (optionBind u (fun x => t) None) (at level 0, t at level 200, only parsing).
Notation "'plet' x ':=' u 'in' t" := (optionBind u (fun x => t) False) (at level 0, t at level 200, only parsing).
Ltac optionD :=
match goal with
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
(**
Some abbreviations that require having defined expressions beforehand
Some abbreviations that require having defined exprressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
**)
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts.
Require Import Flover.AffineForm.
Require Export Flover.Infra.Abbrevs Flover.Expressions.
Require Export Flover.Infra.Abbrevs Flover.Expressions Flover.OrderedExpressions.
Module Q_orderedExps := ExpOrderedType (Q_as_OT).
Module Q_orderedExps := ExprOrderedType (Q_as_OT).
Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps).
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
......@@ -54,7 +54,7 @@ Proof.
Qed.
(**
We treat a function mapping an expression arguing on fractions as value type
We treat a function mapping an exprression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
(* Definition analysisResult :Type := exp Q -> intv * error. *)
(* Definition analysisResult :Type := expr Q -> intv * error. *)
......@@ -2,6 +2,8 @@
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals Coq.micromega.Psatz.
Require Import Flover.Infra.RealSimps Flover.Infra.Abbrevs Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Global Set Implicit Arguments.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
......@@ -17,6 +19,15 @@ Ltac andb_to_prop H :=
try andb_to_prop Left;
try andb_to_prop Right.
Ltac split_bool :=
match goal with
| [|- (_ && _) = true ] => apply Is_true_eq_true;
apply andb_prop_intro;
split;
apply Is_true_eq_left
| _ => fail "Cannot case split on non-boolean conjunction"
end.
Ltac canonize_Q_prop :=
match goal with
| [ H: Qle_bool ?a ?b = true |- _] => rewrite Qle_bool_iff in H
......@@ -46,6 +57,23 @@ Ltac Q2R_to_head_step :=
Ltac Q2R_to_head := repeat Q2R_to_head_step.
Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
match v with
| Some v => f v
| None => e
end.
Notation "'olet' x ':=' u 'in' t" := (optionBind u (fun x => t) None)
(only parsing, at level 0, t at level 200).
Notation "'plet' x ':=' u 'in' t" := (optionBind u (fun x => t) False)
(only parsing, at level 0, t at level 200).
Ltac optionD :=
match goal with
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
Lemma optionBind_eq (X Y: Type) v (f: X -> Y) (e: Y):
match v with |Some val => f val | None => e end = optionBind v f e.
Proof.
......@@ -60,8 +88,12 @@ Qed.
Ltac remove_matches := rewrite optionBind_eq in *.
Ltac remove_matches_asm := rewrite optionBind_eq in * |- .
Ltac remove_conds := rewrite <- andb_lazy_alt, optionBind_cond in *.
Ltac remove_conds_asm := rewrite <- andb_lazy_alt, optionBind_cond in * |- .
Ltac match_factorize_asm :=
match goal with
| [ H: ?t = ?u |- context [optionBind ?t _ _]]
......@@ -105,8 +137,8 @@ Ltac bool_factorize :=
Ltac Flover_compute_asm :=
repeat (
(try remove_conds;
try remove_matches;
(try remove_conds_asm;
try remove_matches_asm;
repeat match_factorize_asm;
try pair_factorize) ||
bool_factorize).
......@@ -156,3 +188,15 @@ Tactic Notation "unify asm" open_constr(pat) hyp(H):=
Ltac Qrewrite H :=
assert H as tmp by (try field; try lra); rewrite tmp; clear tmp.
Ltac destruct_ex H pat :=
match type of H with
| exists v, ?H' =>
let vFresh:=fresh v in
let fN := fresh "ex" in
destruct H as [vFresh fN];
destruct_ex fN pat
| _ => destruct H as pat
end.
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
This diff is collapsed.
(**
Some simplification properties of rationals, not proven in the Standard Library
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs.
Require Import Coq.micromega.Psatz.
**)
From Coq.QArith
Require Export QArith Qminmax Qabs Qround.
From Coq
Require Export micromega.Psatz.
Definition Qleb := Qle_bool.
Definition Qeqb := Qeq_bool.
(* Definition machineEpsilon := (1#(2^53)). *)
Definition maxAbs (iv:Q*Q) :=
Qmax (Qabs (fst iv)) (Qabs (snd iv)).
......@@ -69,18 +69,17 @@ Lemma Qeq_bool_sym a b:
Qeq_bool a b = Qeq_bool b a.
Proof.
unfold Qeq_bool.
case_eq (Zeq_bool (Qnum a * ' Qden b) (Qnum b * ' Qden a)); intros.
case_eq (Zeq_bool (Qnum a * (Zpos (Qden b))) (Qnum b * (Zpos (Qden a)))); intros.
- rewrite <- Zeq_is_eq_bool in H.
rewrite H; symmetry.
rewrite <- Zeq_is_eq_bool; auto.
- apply Zeq_bool_neq in H.
case_eq (Zeq_bool (Qnum b *' Qden a) (Qnum a * ' Qden b)); intros.
case_eq (Zeq_bool (Qnum b * Zpos (Qden a)) (Qnum a * Zpos (Qden b))); intros.
+ apply Zeq_is_eq_bool in H0.
rewrite H0 in H; auto.
+ auto.
Qed.
Lemma Qeq_bool_refl v:
(Qeq_bool v v = true).
Proof.
......@@ -245,3 +244,11 @@ Proof.
pose proof (Z.square_nonneg (Qnum x)).
lia.
Qed.
Lemma Qabs_0_impl_eq (d:Q):
Qabs d <= 0 -> d == 0.
Proof.
intros abs_leq_0.
rewrite Qabs_Qle_condition in abs_leq_0.
lra.
Qed.
(**
Some rewriting properties for translating between rationals and real numbers.
These are used in the soundness proofs since we want to have the final theorem on the real valued evaluation.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs
Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Flover.Infra.RationalSimps Flover.Infra.RealSimps.
**)
From Coq.QArith
Require Export Qreals.
From Flover.Infra
Require Export RationalSimps RealSimps.
Lemma Q2R0_is_0:
Q2R 0 = 0%R.
......
......@@ -2,7 +2,11 @@
Some simplification properties of real numbers, not proven in the Standard Library
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.Setoids.Setoid.
From Coq
Require Import Setoids.Setoid.
From Coq
Require Export Reals.Reals micromega.Psatz.
(** Define the maxAbs function on R and prove some minor properties of it.
TODO: Make use of IVLO and IVhi
......@@ -73,7 +77,7 @@ Qed.
Prove that using eps = 0 makes the evaluation deterministic
**)
Lemma Rabs_0_impl_eq (d:R):
Rle (Rabs d) R0 -> d = R0.
Rle (Rabs d) 0 -> d = 0%R.
Proof.
intros abs_leq_0.
pose proof (Rabs_pos d) as abs_geq_0.
......
This diff is collapsed.
This diff is collapsed.
......@@ -13,14 +13,14 @@ Definition RangeValidator e A P :=
| None => false
end.
Theorem RangeValidator_sound (f : exp Q) (A : analysisResult) (P : precond)
Theorem RangeValidator_sound (f : expr Q) (A : analysisResult) (P : precond)
(E : env) (Gamma : nat -> option mType) :
RangeValidator f A P = true ->
fVars_P_sound (usedVars f) E P ->
vars_typed (usedVars f) Gamma ->
exists (iv : intv) (err : error) (vR : R),
FloverMap.find (elt:=intv * error) f A = Some (iv, err) /\
eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
eval_expr E (toRMap Gamma) (toREval (toRExp f)) vR REAL /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
intros.
unfold RangeValidator in *.
......
From Coq
Require Import Reals.Reals QArith.Qreals.
From Flover
Require Export Infra.ExpressionAbbrevs ErrorValidation.
Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
(* if *)
validErrorbound e tMap A dVars.
(*then true *)
(* else validAffineErrorBounds e A tMap dVars *)
Theorem RoundoffErrorValidator_sound:
forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
(nR : R) (err : error) (P : precond) (elo ehi : Q) (Gamma : FloverMap.t mType)
(defVars : nat -> option mType),
Typing.typeCheck e defVars Gamma = true ->
Environments.approxEnv E1 defVars A fVars dVars E2 ->
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 ->
IntervalValidation.dVars_range_valid dVars E1 A ->
IntervalValidation.fVars_P_sound fVars E1 P ->
IntervalValidation.vars_typed (fVars dVars) defVars ->
FloverMap.find (elt:=intv * error) e A = Some (elo, ehi, err) ->
(exists (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m) /\
(forall (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m -> (Rabs (nR - nF) <= Q2R err)%R).
Proof.
intros.
cbn in *.
eapply validErrorbound_sound; eauto.
Qed.
......@@ -14,7 +14,7 @@ From Flover
Require Export Infra.ExpressionAbbrevs Infra.RealSimps Infra.NatSet
Infra.MachineType.
Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option mType :=
Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:expr V) : option mType :=
match e with
| Var _ v => Gamma v
| Const m n => Some m
......@@ -42,7 +42,7 @@ Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option
end
end.