Commit 1a95eddd authored by Heiko Becker's avatar Heiko Becker

Renaming in Coq dev, move attic files to separate folder

parent 9113b954
......@@ -14,7 +14,7 @@ coq/*.vo
coq/.*
coq/*.v.d
coq/*/*.v.d
coq/Makefile
coq/Makefile*
coq/*/*.glob
coq/*/.*
coq/*/*.vo
......
......@@ -3,8 +3,8 @@
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.
Require Import Flover.Infra.Abbrevs Flover.Infra.RealConstruction Flover.Infra.RealSimps.
Require Import Flover.IntervalArith Flover.Expressions Flover.Commands.
Definition abs_env:Type := exp R -> interval -> err -> Prop.
......
(**
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
**)
Require Import Coq.Reals.Reals.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions.
Require Import Flover.Infra.Abbrevs Flover.Expressions.
(**
Next define what a program is.
Currently no loops, only conditionals and assignments
......@@ -15,7 +15,7 @@ Let: nat -> exp V -> cmd V -> cmd V
| Nop: cmd V.
(**
Small Step semantics for Daisy language, parametric by evaluation function.
Small Step semantics for Flover language, parametric by evaluation function.
**)
Inductive sstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
let_s x e s env v eps:
......@@ -31,7 +31,7 @@ Inductive sstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
eval_exp eps env e v ->
sstep (Ret R e) env eps (Nop R) (updEnv 0 v env).
(**
Analogously define Big Step semantics for the Daisy language,
Analogously define Big Step semantics for the Flover language,
parametric by the evaluation function
**)
Inductive bstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
......
(**
Formalization of the base expression language for the daisy framework
Formalization of the base expression language for the flover framework
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Interval.Interval_tactic.
Require Import Daisy.Infra.RealConstruction Daisy.Infra.RealSimps Daisy.Infra.Abbrevs.
Require Import Flover.Infra.RealConstruction Flover.Infra.RealSimps Flover.Infra.Abbrevs.
Set Implicit Arguments.
Module Type Expression.
......
......@@ -2,7 +2,7 @@
Precondition agreement checker and its soundness proof
**)
Require Import Coq.Reals.Reals Coq.Lists.List Coq.QArith.QArith.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RationalSimps Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ.
Require Import Flover.Infra.Abbrevs Flover.Expressions Flover.Infra.RationalSimps Flover.Infra.ExpressionAbbrevs Flover.IntervalArithQ.
Import Lists.List.ListNotations.
......
Require Import Daisy.CertificateChecker.
Require Import Flover.CertificateChecker.
(*
TODO: update according to:
[ Info ]
......
Require Import Daisy.CertificateChecker.
Require Import Flover.CertificateChecker.
(*
[ Info ]
......
Require Import Coq.Reals.Reals.
Require Import Daisy.Infra.abbrevs Daisy.daisy_lang Daisy.abs_err Daisy.exps.
Require Import Flover.Infra.abbrevs Flover.flover_lang Flover.abs_err Flover.exps.
(**
Notes:
......
Require Import Coq.Reals.Reals.
Require Import Interval.Interval_tactic.
Require Import Daisy.Infra.abbrevs.
Require Import Flover.Infra.abbrevs.
Definition min4 (a:R) (b:R) (c:R) (d:R) := Rmin a (Rmin b (Rmin c d)).
Definition max4 (a:R) (b:R) (c:R) (d:R) := Rmax a (Rmax b (Rmax c d)).
......
......@@ -2,7 +2,7 @@
Toy Example to understand what certificate we will need for a given program
**)
Require Import Coq.Reals.Reals.
Require Import Daisy.daisy_lang Daisy.exps Daisy.abs_err.
Require Import Flover.flover_lang Flover.exps Flover.abs_err.
Definition prg :cmd R :=
Ret R (Binop Mult (Const (3%R)) (Var R 1)).
......
......@@ -2,7 +2,7 @@ open preamble
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
open MachineTypeTheory ExpressionsTheory RealSimpsTheory DaisyTactics CertificateCheckerTheory
open MachineTypeTheory ExpressionsTheory RealSimpsTheory FloverTactics CertificateCheckerTheory
open FPRangeValidatorTheory IntervalValidationTheory TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
......
......@@ -5,15 +5,15 @@
as shown in the soundness theorem.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing Daisy.FPRangeValidator.
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
Require Import Flover.IntervalValidation Flover.ErrorValidation Flover.Environments Flover.Typing Flover.FPRangeValidator.
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
let tMap := (typeMap defVars e (DaisyMap.empty mType)) in
let tMap := (typeMap defVars e (FloverMap.empty mType)) in
if (typeCheck e defVars tMap)
then
if (validIntervalbounds e absenv P NatSet.empty) && FPRangeValidator e absenv tMap NatSet.empty
......@@ -37,7 +37,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVar
defVars v = Some m) ->
CertificateChecker e absenv P defVars = true ->
exists iv err vR vF m,
DaisyMap.find e absenv = Some (iv, err) /\
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 /\
(forall vF m,
......@@ -67,12 +67,12 @@ Proof.
edestruct (validIntervalbounds_sound e (A:=absenv) (P:=P) (fVars:=usedVars e) (dVars:=NatSet.empty) (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 (DaisyMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
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.
exists (elo, ehi), err_e, vR, vF, mF; split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
let tMap := typeMapCmd defVars f (DaisyMap.empty mType) in
let tMap := typeMapCmd defVars f (FloverMap.empty mType) in
if (typeCheckCmd f defVars tMap && validSSA f (freeVars f))
then
if (validIntervalboundsCmd f absenv P NatSet.empty) &&
......@@ -92,7 +92,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
defVars v = Some m) ->
CertificateCheckerCmd f absenv P defVars = true ->
exists iv err vR vF m,
DaisyMap.find (getRetExp f) absenv = Some (iv,err) /\
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
bstep (toRCmd f) E2 defVars vF m /\
(forall vF m,
......
Require Import Daisy.CertificateChecker Daisy.daisyParser.
Require Import Flover.CertificateChecker Flover.floverParser.
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
Extraction Language Ocaml.
......
(**
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Import Daisy.Expressions.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
Require Import Flover.Expressions.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.
(**
Next define what a program is.
......@@ -35,7 +35,7 @@ Fixpoint toREvalCmd (f:cmd R) :=
(*
UNUSED!
Small Step semantics for Daisy language
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 ->
......@@ -46,7 +46,7 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
*)
(**
Define big step semantics for the Daisy language, terminating on a "returned"
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
......
(**
Environment library.
Defines the environment type for the Daisy 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 Daisy.Infra.ExpressionAbbrevs Daisy.Infra.RationalSimps Daisy.Commands.
Require Import Flover.Infra.ExpressionAbbrevs Flover.Infra.RationalSimps Flover.Commands.
(**
Define an approximation relation between two environments.
......@@ -22,7 +22,7 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
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 ->
DaisyMap.find (Var Q x) A = Some (iv, err) ->
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).
......@@ -102,7 +102,7 @@ Section RelationProperties.
E2 x = Some v2 ->
NatSet.In x dVars ->
Gamma x = Some m ->
DaisyMap.find (Var Q x) A = Some (iv, e) ->
FloverMap.find (Var Q x) A = Some (iv, e) ->
(Rabs (v - v2) <= Q2R e)%R.
Proof.
induction approxEnvs;
......
......@@ -4,8 +4,8 @@ This shortens soundness proofs later.
Bounds are explained in section 5, Deriving Computable Error Bounds
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealSimps Flover.Infra.RealRationalProps.
Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
......
This diff is collapsed.
(**
Formalization of the base expression language for the daisy framework
Formalization of the base expression language for the flover framework
**)
From Coq
Require Import Reals.Reals micromega.Psatz QArith.QArith QArith.Qreals
Structures.Orders.
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps
Daisy.Infra.Ltacs.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet
Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
Require Import Flover.Infra.RealRationalProps Flover.Infra.RationalSimps
Flover.Infra.Ltacs.
Require Export Flover.Infra.Abbrevs Flover.Infra.RealSimps Flover.Infra.NatSet
Flover.IntervalArithQ Flover.IntervalArith Flover.Infra.MachineType.
(**
Expressions will use binary operators.
......@@ -180,7 +180,7 @@ Proof.
destruct f; intros g eq1 eq2;
destruct g; cbn in *;
try rewrite Nat.eqb_eq in *;
Daisy_compute; try congruence; type_conv; subst; try auto.
Flover_compute; try congruence; type_conv; subst; try auto.
- rewrite mTypeEq_refl; simpl.
rewrite Qeq_bool_iff in *; lra.
- rewrite unopEq_compat_eq in *; subst.
......
......@@ -3,10 +3,10 @@
Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.MachineType Daisy.Typing Daisy.Infra.RealSimps Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Commands Daisy.Environments Daisy.ssaPrgs Daisy.Infra.Ltacs Daisy.Infra.RealRationalProps.
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 :=
match DaisyMap.find e typeMap, DaisyMap.find e A with
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
let recRes :=
......@@ -84,13 +84,13 @@ Theorem FPRangeValidator_sound:
fVars_P_sound fVars E1 P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
(forall v, NatSet.In v dVars ->
exists vF m, E2 v = Some vF /\ DaisyMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
exists vF m, E2 v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
validFloatValue v m.
Proof.
intros *.
unfold FPRangeValidator.
intros.
assert (DaisyMap.find e tMap = Some m)
assert (FloverMap.find e tMap = Some m)
as type_e
by (eapply typingSoundnessExp; eauto).
unfold validFloatValue.
......@@ -116,20 +116,20 @@ Proof.
inversion H0; subst.
rewrite env_eq in H14; inversion H14; subst.
rewrite map_eq in type_e; inversion type_e; subst; auto.
+ Daisy_compute.
+ Flover_compute.
prove_fprangeval m v L1 R.
- Daisy_compute.
- Flover_compute.
prove_fprangeval m v L1 R.
- Daisy_compute; try congruence.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m0 v L1 R.
- Daisy_compute; try congruence.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval (join m0 m1) v L1 R.
- Daisy_compute; try congruence.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval (join3 m0 m1 m2) v L1 R.
- Daisy_compute; try congruence.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
Qed.
......@@ -149,7 +149,7 @@ Lemma FPRangeValidatorCmd_sound (f:cmd Q):
fVars_P_sound fVars E1 P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
(forall v, NatSet.In v dVars ->
exists vF m, E2 v = Some vF /\ DaisyMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
exists vF m, E2 v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
validFloatValue v m.
Proof.
induction f; intros;
......@@ -159,10 +159,10 @@ Proof.
repeat match goal with
| H : _ = true |- _ => andb_to_prop H
end.
- assert (DaisyMap.find e tMap = Some m)
- assert (FloverMap.find e tMap = Some m)
by(eapply typingSoundnessExp; eauto).
match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *).
Daisy_compute.
Flover_compute.
edestruct (validIntervalbounds_sound e L1 (Gamma := Gamma)(P:= P) (A:=A)
(fVars:=fVars) (dVars:=dVars)
(E:=E1))
......
This diff is collapsed.
......@@ -2,7 +2,7 @@
This file contains some type abbreviations, to ease writing.
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.MachineType.
Require Import Flover.Infra.MachineType.
Global Set Implicit Arguments.
(**
......
......@@ -3,16 +3,16 @@
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 Export Daisy.Infra.Abbrevs Daisy.Expressions.
Require Export Flover.Infra.Abbrevs Flover.Expressions.
Module Q_orderedExps := ExpOrderedType (Q_as_OT).
Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps).
Module DaisyMap := FMapAVL.Make(legacy_OrderedQExps).
Module DaisyMapFacts := OrdProperties (DaisyMap).
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
Definition analysisResult :Type := DaisyMap.t (intv * error).
Definition analysisResult :Type := FloverMap.t (intv * error).
(**
We treat a function mapping an expression arguing on fractions as value type
......
(** Ltac definitions **)
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Require Import Flover.Infra.RealSimps Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
......@@ -109,7 +109,7 @@ Ltac bool_factorize :=
| [H: _ = true |- _] => andb_to_prop H
end.
Ltac Daisy_compute_asm :=
Ltac Flover_compute_asm :=
repeat (
(try remove_conds;
try remove_matches;
......@@ -117,7 +117,7 @@ Ltac Daisy_compute_asm :=
try pair_factorize) ||
bool_factorize).
Ltac Daisy_compute :=
Ltac Flover_compute :=
repeat (
(try remove_conds;
try remove_matches;
......@@ -143,8 +143,8 @@ Ltac Daisy_compute :=
(* Ltac match_destr t:= *)
(* match goal with *)
(* | H: context [optionLift (DaisyMap.find ?k ?M) _ _] |- _ => *)
(* destruct (DaisyMap.find (elt:=intv * error) k M); idtac H *)
(* | H: context [optionLift (FloverMap.find ?k ?M) _ _] |- _ => *)
(* destruct (FloverMap.find (elt:=intv * error) k M); idtac H *)
(* end. *)
Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
......
......@@ -7,7 +7,7 @@
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs
Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.RealRationalProps.
Require Import Flover.Infra.RealRationalProps.
(**
Define machine precision as datatype
**)
......@@ -23,7 +23,7 @@ Definition mTypeToQ (e:mType) :Q :=
| M32 => (Qpower (2#1) (Zneg 24))
| M64 => (Qpower (2#1) (Zneg 53))
(*
(* the epsilons below match what is used internally in daisy,
(* the epsilons below match what is used internally in flover,
although these value do not match the IEEE standard *)
| M128 => (Qpower (2#1) (Zneg 105))
| M256 => (Qpower (2#1) (Zneg 211)) *)
......
......@@ -4,7 +4,7 @@ These are used in the soundness proofs since we want to have the final theorem o
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs
Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.RationalSimps Daisy.Infra.RealSimps.
Require Import Flover.Infra.RationalSimps Flover.Infra.RealSimps.
Lemma Q2R0_is_0:
Q2R 0 = 0%R.
......
......@@ -3,7 +3,7 @@
Used in soundness proofs for error bound validator.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps.
Require Import Flover.Infra.Abbrevs Flover.Infra.RealSimps.
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
......@@ -54,7 +54,7 @@ Qed.
(**
Now comes the old part with the computational definitions.
Where possible within time, they are shown sound with respect to the definitions from before, where not, we leave this as proof obligation for daisy.
Where possible within time, they are shown sound with respect to the definitions from before, where not, we leave this as proof obligation for flover.
**)
(**
......
......@@ -4,7 +4,7 @@
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.micromega.Psatz.
Require Import Coq.ZArith.ZArith.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps.
(**
Define validity of an intv, requiring that the lower bound is less than or equal to the upper bound.
......@@ -97,7 +97,7 @@ Qed.
(**
Now comes the old part with the computational definitions.
Where possible within time, they are shown sound with respect to the definitions from before, where not, we leave this as proof obligation for daisy.
Where possible within time, they are shown sound with respect to the definitions from before, where not, we leave this as proof obligation for flover.
**)
(**
......
......@@ -6,12 +6,12 @@
The function is used in CertificateChecker.v to build the full checker.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps Daisy.Typing.
Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing.
Require Export Flover.IntervalArithQ Flover.IntervalArith Flover.ssaPrgs.
Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
match DaisyMap.find e A with
match FloverMap.find e A with
| None => false
| Some (intv, _) =>
match e with
......@@ -23,7 +23,7 @@ Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars
| Unop o f =>
if validIntervalbounds f A P validVars
then
match DaisyMap.find f A with
match FloverMap.find f A with
| None => false
| Some (iv, _) =>
match o with
......@@ -44,7 +44,7 @@ Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars
if ((validIntervalbounds f1 A P validVars) &&
(validIntervalbounds f2 A P validVars))
then
match DaisyMap.find f1 A, DaisyMap.find f2 A with
match FloverMap.find f1 A, FloverMap.find f2 A with
| Some (iv1, _), Some (iv2, _) =>
match op with
| Plus =>
......@@ -72,7 +72,7 @@ Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars
(validIntervalbounds f2 A P validVars) &&
(validIntervalbounds f3 A P validVars))
then
match DaisyMap.find f1 A, DaisyMap.find f2 A, DaisyMap.find f3 A with
match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
| Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
let new_iv := addIntv iv1 (multIntv iv2 iv3) in
isSupersetIntv new_iv intv
......@@ -82,7 +82,7 @@ Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars
| Downcast _ f1 =>
if (validIntervalbounds f1 A P validVars)
then
match DaisyMap.find f1 A with
match FloverMap.find f1 A with
| None => false
| Some (iv1, _) =>
(* TODO: intv = iv1 might be a hard constraint... *)
......@@ -96,7 +96,7 @@ Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars
Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
match f with
| Let m x e g =>
match DaisyMap.find e A, DaisyMap.find (Var Q x) A with
match FloverMap.find e A, FloverMap.find (Var Q x) A with
| Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) =>
if (validIntervalbounds e A P validVars &&
Qeq_bool (e_lo) (x_lo) &&
......@@ -122,12 +122,12 @@ Proof.
Qed.
Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
DaisyMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) ->
FloverMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) ->
validIntervalbounds (Binop Div e1 e2) A P V = true ->
(ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
intros A_eq validBounds; cbn in *.
Daisy_compute; try congruence.
Flover_compute; try congruence.
apply le_neq_bool_to_lt_prop; auto.
Qed.
......@@ -135,7 +135,7 @@ Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :
forall v, NatSet.In v dVars ->
exists vR iv err,
E v = Some vR /\
DaisyMap.find (Var Q v) A = Some (iv, err) /\
FloverMap.find (Var Q v) A = Some (iv, err) /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
......@@ -162,14 +162,14 @@ Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
fVars_P_sound fVars E P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
exists iv err vR,
DaisyMap.find f A = Some (iv, err) /\
FloverMap.find f A = Some (iv, err) /\
eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
induction f;
intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
cbn in *.
- Daisy_compute.
- Flover_compute.
destruct (NatSet.mem n dVars) eqn:?; simpl in *.
+ destruct (valid_definedVars n)
as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
......@@ -194,13 +194,13 @@ Proof.
set_tac.
match_simpl; auto.
* lra.
- Daisy_compute; canonize_hyps; simpl in *.
- Flover_compute; canonize_hyps; simpl in *.
kill_trivial_exists.
exists (perturb (Q2R v) 0).
split; [auto| split].
+ econstructor; try eauto. apply Rabs_0_equiv.
+ unfold perturb; simpl; lra.
- Daisy_compute; simpl in *; try congruence.
- Flover_compute; simpl in *; try congruence.
destruct IHf as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]];
try auto.
inversion iveq_f; subst.
......@@ -254,7 +254,7 @@ Proof.
}
rewrite <- Q2R0_is_0 in H3.
apply Rlt_Qlt in H3. lra. }
- Daisy_compute; try congruence.
- Flover_compute; try congruence.
destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]];
try auto; set_tac.
destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]];
......@@ -332,7 +332,7 @@ Proof.
unfold perturb.
lra.
}
- Daisy_compute; try congruence.
- Flover_compute; try congruence.
destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]; try auto; set_tac.
destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]; try auto; set_tac.
destruct IHf3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]]; try auto; set_tac.
......@@ -422,14 +422,14 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f A P dVars = true ->
exists iv_e err_e vR,
DaisyMap.find (getRetExp f) A = Some (iv_e, err_e) /\
FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\
(Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R.
Proof.
induction f;
intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f;
cbn in *.
- Daisy_compute.
- Flover_compute.
inversion ssa_f; subst.
canonize_hyps.
pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e.
......
<
......@@ -7,10 +7,10 @@
From Coq
Require Import Reals.Reals micromega.Psatz QArith.QArith QArith.Qreals
MSets.MSets.
From Daisy
From Flover
Require Import Infra.RationalSimps Infra.RealRationalProps Infra.Ltacs
Commands ssaPrgs.