Commit 6f1ffdcc authored by Heiko Becker's avatar Heiko Becker

Merge branch 'reworked_type_validator' into 'master'

Rework Coq type validator

See merge request AVA/FloVer!12
parents d78f37ce 4ccb040c
This diff is collapsed.
......@@ -7,51 +7,54 @@
From Flover
Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments Typing FPRangeValidator ExpressionAbbrevs Commands.
Environments TypeValidator FPRangeValidator ExpressionAbbrevs Commands.
Require Export Infra.ExpressionAbbrevs Flover.Commands Coq.QArith.QArith.
Require Export ExpressionSemantics Flover.Commands Coq.QArith.QArith.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
(P:precond) (defVars:nat -> option mType) (fBits:FloverMap.t N):=
let tMap := (typeMap defVars e (FloverMap.empty mType) fBits) in
if (typeCheck e defVars tMap fBits)
then
if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
then RoundoffErrorValidator e tMap absenv NatSet.empty
else false
else false.
(P:precond) (defVars:FloverMap.t mType):=
let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
match tMap with
|Succes tMap =>
if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
then RoundoffErrorValidator e tMap absenv NatSet.empty
else false
| _ => false
end.
(**
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.
**)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
defVars fBits:
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) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, NatSet.In v (usedVars e) ->
exists m : mType,
defVars v = Some m) ->
CertificateChecker e absenv P defVars fBits = true ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) vR REAL /\
eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m /\
(forall vF m,
eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
CertificateChecker e absenv P defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (usedVars e) NatSet.empty E2 ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) vR REAL /\
eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m /\
(forall vF m,
eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros * approxE1E2 P_valid types_defined certificate_valid.
intros * P_valid certificate_valid.
unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
rename t into Gamma.
assert (validTypes e Gamma).
{ eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. }
rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
......@@ -66,60 +69,68 @@ Proof.
assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
{ hnf; intros a in_empty.
set_tac. }
assert (vars_typed (usedVars e NatSet.empty) defVars).
{ unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
split; try auto. hnf; intros; set_tac. }
rename R into validFPRanges.
assert (validRanges e absenv E1 defVars (toRBMap fBits)) as valid_e.
{ eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1));
rename R0 into validFPRanges.
assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as valid_e.
{ eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (E:=E1));
auto. }
pose proof (validRanges_single _ _ _ _ _ valid_e) as valid_single;
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType) fBits) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; split; auto.
exists Gamma; intros approxE1E2.
edestruct (RoundoffErrorValidator_sound e H approxE1E2 H1 eval_real R
valid_e map_e)
as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
defVars fBits:=
let tMap := typeMapCmd defVars f (FloverMap.empty mType) fBits in
if (typeCheckCmd f defVars tMap fBits && validSSA f (freeVars f))
then
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv tMap NatSet.empty
then (RoundoffErrorValidatorCmd f tMap absenv NatSet.empty)
defVars :=
match getValidMapCmd defVars f (FloverMap.empty mType) with
| Succes Gamma =>
if (validSSA f (freeVars f))
then
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv Gamma NatSet.empty
then (RoundoffErrorValidatorCmd f Gamma absenv NatSet.empty)
else false
else false
else false.
| _ => false
end.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
defVars fBits:
defVars:
forall (E1 E2:env),
approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
(forall v, NatSet.In v (freeVars f) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, NatSet.In v (freeVars f) ->
exists m : mType,
defVars v = Some m) ->
CertificateCheckerCmd f absenv P defVars fBits = true ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\
bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m /\
CertificateCheckerCmd f absenv P defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
bstep (toRCmd f) E2 (toRExpMap Gamma) vF m /\
(forall vF m,
bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) vF m ->
(Rabs (vR - vF) <= Q2R (err))%R).
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros * approxE1E2 P_valid types_defined certificate_valid.
intros * P_valid certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?;
try congruence.
rename t into Gamma.
assert (validTypesCmd f Gamma).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
exists Gamma; intros approxE1E2.
repeat rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
apply validSSA_sound in R0.
destruct R0 as [outVars ssa_f].
apply validSSA_sound in L.
destruct L as [outVars ssa_f].
assert (ssa f (freeVars f NatSet.empty) outVars) as ssa_valid.
{ eapply ssa_equal_set; try eauto.
apply NatSetProps.empty_union_2.
......@@ -128,18 +139,16 @@ Proof.
assert (dVars_range_valid NatSet.empty E1 absenv).
{ unfold dVars_range_valid.
intros; set_tac. }
assert (vars_typed (freeVars f NatSet.empty) defVars).
{ unfold vars_typed. intros; apply types_defined. set_tac.
destruct H0; set_tac. }
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac.
assert (validRangesCmd f absenv E1 defVars (toRBMap fBits)) as valid_f.
assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
{ eapply RangeValidatorCmd_sound; eauto.
unfold RangeValidatorCmd.
unfold affine_dVars_range_valid; intros.
set_tac. }
pose proof (validRangesCmd_single _ _ _ _ _ valid_f) as valid_single.
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
Qed.
......@@ -2,7 +2,7 @@
Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Import Flover.Expressions.
Require Export Flover.ExpressionSemantics.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.
(**
......@@ -20,7 +20,6 @@ Fixpoint getRetExp (V:Type) (f:cmd V) :=
| Ret e => e
end.
Fixpoint toRCmd (f:cmd Q) :=
match f with
|Let m x e g => Let m x (toRExp e) (toRCmd g)
......@@ -49,14 +48,14 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> (nat -> option mType) -> (expr R -> option N) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars fBits:
eval_expr E defVars fBits e v m ->
bstep s (updEnv x v E) (updDefVars x m defVars) fBits res m' ->
bstep (Let m x e s) E defVars fBits res m'
|ret_b m e E v defVars fBits:
eval_expr E defVars fBits e v m ->
bstep (Ret e) E defVars fBits v m.
Inductive bstep : cmd R -> env -> (expr R -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_expr E defVars e v m ->
bstep s (updEnv x v E) defVars res m' -> (* (updDefVars (Var R x) m defVars) res m' -> *)
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
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 exprressions
......@@ -88,17 +87,45 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
end.
Lemma bstep_eq_env f:
forall E1 E2 Gamma fBits v m,
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
bstep f E1 Gamma fBits v m ->
bstep f E2 Gamma fBits v m.
bstep f E1 Gamma v m ->
bstep f E2 Gamma v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H8; eauto. eapply let_b; eauto.
- eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
+ auto.
- apply ret_b. eapply eval_eq_env; eauto.
Qed.
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
(forall n, Gamma1 n = Gamma2 n) ->
bstep f E Gamma1 vR m ->
bstep f E Gamma2 vR m.
Proof.
revert E Gamma1 Gamma2;
induction f; intros * Gamma_eq eval_f.
- inversion eval_f; subst.
econstructor; try eauto.
eapply swap_Gamma_eval_expr; eauto.
- inversion eval_f; subst.
econstructor; try eauto.
eapply swap_Gamma_eval_expr; eauto.
Qed.
Lemma bstep_Gamma_det f:
forall E1 E2 Gamma v1 v2 m1 m2,
bstep f E1 Gamma v1 m1 ->
bstep f E2 Gamma v2 m2 ->
m1 = m2.
Proof.
induction f; intros * eval_f1 eval_f2;
inversion eval_f1; subst;
inversion eval_f2; subst; try auto.
- eapply IHf; eauto.
- eapply Gamma_det; eauto.
Qed.
\ No newline at end of file
......@@ -16,29 +16,31 @@ It is necessary to have this relation, since two evaluations of the very same
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
Inductive approxEnv : env -> (expr R -> 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 ->
|approxRefl Gamma A:
approxEnv emptyEnv Gamma A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 Gamma A v1 v2 x fVars dVars m:
approxEnv E1 Gamma A fVars dVars E2 ->
Gamma (Var R x) = Some m ->
(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
(updDefVars (Var R x) m Gamma) 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 ->
|approxUpdBound E1 E2 Gamma A v1 v2 x fVars dVars m iv err:
approxEnv E1 Gamma A fVars dVars E2 ->
Gamma (Var R x) = Some m ->
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)
Gamma A fVars (NatSet.add x dVars)
(updEnv x v2 E2).
Section RelationProperties.
Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType)
Variable (x:nat) (v:R) (E1 E2:env) (Gamma:expr R -> option mType)
(A:analysisResult) (fVars dVars: NatSet.t).
Hypothesis approxEnvs: approxEnv E1 Gamma A fVars dVars E2.
......@@ -58,7 +60,7 @@ Section RelationProperties.
+ eapply IHa; eauto.
set_tac.
destruct x_valid; set_tac.
destruct H1 as [? | [? ?]]; subst; try auto.
destruct H2 as [? | [? ?]]; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
......@@ -66,7 +68,7 @@ Section RelationProperties.
+ eapply IHa; auto.
set_tac.
destruct x_valid; set_tac.
destruct H2 as [? | [ ? ?]]; subst; try auto.
destruct H3 as [? | [ ? ?]]; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
Qed.
......@@ -76,7 +78,7 @@ Section RelationProperties.
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x fVars ->
Gamma x = Some m ->
Gamma (Var R x) = Some m ->
(Rabs (v - v2) <= computeErrorR v m)%R.
Proof.
induction approxEnvs;
......@@ -87,30 +89,40 @@ Section RelationProperties.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
unfold updDefVars in x_typed.
rewrite Nat.eqb_refl in x_typed.
cbn in x_typed.
rewrite Nat.compare_refl in x_typed.
inversion x_typed; subst.
inversion E1_def; inversion E2_def; subst; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
apply IHa; auto.
unfold updDefVars in x_typed.
cbn in x_typed.
apply Nat.eqb_neq in x_neq.
destruct (x ?= x0)%nat eqn:?.
* apply Nat.compare_eq in Heqc; subst; congruence.
* apply IHa; auto.
* apply IHa; auto.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H1.
apply H2.
set_tac. }
unfold updEnv in *; rewrite x_x0_neq in *.
apply IHa; auto.
unfold updDefVars in x_typed;
rewrite x_x0_neq in x_typed; auto.
unfold updDefVars in x_typed.
cbn in x_typed.
apply Nat.eqb_neq in x_x0_neq.
destruct (x ?= x0)%nat eqn:?.
* apply Nat.compare_eq in Heqc; subst; congruence.
* apply IHa; auto.
* apply IHa; auto.
Qed.
Lemma approxEnv_dVar_bounded v2 m iv e:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x dVars ->
Gamma x = Some m ->
Gamma (Var R x) = Some m ->
FloverMap.find (Var Q x) A = Some (iv, e) ->
(Rabs (v - v2) <= Q2R e)%R.
Proof.
......@@ -120,22 +132,30 @@ Section RelationProperties.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H0; set_tac.
apply H1; set_tac.
}
unfold updEnv in *; rewrite x_x0_neq in *.
unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed.
apply IHa; auto.
unfold updDefVars in x_typed; cbn in x_typed.
apply Nat.eqb_neq in x_x0_neq.
destruct (x ?= x0)%nat eqn:?.
* apply Nat.compare_eq in Heqc; subst; congruence.
* apply IHa; auto.
* apply IHa; auto.
- set_tac.
destruct x_def as [x_x0 | [x_neq x_def]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
inversion E1_def; inversion E2_def; subst.
rewrite A_e in *; inversion H; auto.
rewrite A_e in *; inversion H0; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
apply IHa; auto.
unfold updDefVars in x_typed; cbn in x_typed.
apply Nat.eqb_neq in x_neq.
destruct (x ?= x0)%nat eqn:?.
* apply Nat.compare_eq in Heqc; subst; congruence.
* apply IHa; auto.
* apply IHa; auto.
Qed.
End RelationProperties.
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
......@@ -12,7 +12,7 @@ From Coq
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
Infra.RealSimps Infra.Ltacs Environments IntervalValidation TypeValidator
RealRangeValidator ErrorBounds AffineForm AffineArith AffineArithQ.
(** Error bound validator **)
......@@ -232,7 +232,6 @@ Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
(* (Rabs (vR - vF) <= (Q2R mAbs))%R. *)
(* Theorem validErrorboundAA_sound e: *)
(* forall E1 E2 P Gamma defVars nR A elo ehi tMap fVars dVars currNoise maxNoise initMap resMap M1, *)
(* (forall e vR, *)
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(** Ltac definitions **)
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals Coq.micromega.Psatz.
Require Import Flover.Infra.RealSimps Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
From Coq
Require Import Bool.Bool Reals.Reals QArith.QArith QArith.Qreals micromega.Psatz.
From Flover.Infra
Require Import RealSimps NatSet RationalSimps RealRationalProps Results.
Global Set Implicit Arguments.
......@@ -63,15 +65,29 @@ Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
| None => e
end.
Definition resultBind (X:Type) (r:result X) (f: X -> result X) :result X :=
match r with
| Succes res => f res
| _ => r
end.
Definition resultReturn (X:Type) (r:X) :=
Succes r.
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).
Notation "'rlet' x ':=' u 'in' t" := (resultBind u (fun x => t))
(only parsing, at level 0, t at level 200).
Notation "'ret' x" := (resultReturn x) (only parsing, at level 0 ).
Ltac optionD :=
match goal with
|H: context[resultBind ?v ?f] |- _ =>
destruct v eqn:?
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
destruct v eqn:?
end.
Lemma optionBind_eq (X Y: Type) v (f: X -> Y) (e: Y):
......@@ -90,9 +106,26 @@ 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 := rewrite <- andb_lazy_alt in *.
Ltac remove_conds_asm := rewrite <- andb_lazy_alt in * |- .
Ltac result_factorize_asm :=
match goal with
| [ H: ?t = ?u |- context [resultBind ?t _ ]]
=> rewrite H; cbn
| [ H1: ?t = ?u, H2: context [resultBind ?t _] |- _ ]
=> rewrite H1 in H2; cbn in H2
| [ H: context [resultBind ?t _ ] |- _ ]
=> destruct t eqn:?; cbn in H; try congruence
end.
Ltac remove_conds_asm := rewrite <- andb_lazy_alt, optionBind_cond in * |- .
Ltac result_factorize :=
result_factorize_asm ||
match goal with
| [ |- context [resultBind ?t _] ]
=> destruct t eqn:?; cbn; try congruence
end.
Ltac match_factorize_asm :=
match goal with
......@@ -128,6 +161,7 @@ Ltac match_simpl :=
try remove_conds;
try remove_matches;
repeat match_factorize;
repeat result_factorize;
try pair_factorize.
Ltac bool_factorize :=
......@@ -140,6 +174,7 @@ Ltac Flover_compute_asm :=
(try remove_conds_asm;
try remove_matches_asm;
repeat match_factorize_asm;
repeat result_factorize_asm;
try pair_factorize) ||
bool_factorize).
......@@ -148,6 +183,7 @@ Ltac Flover_compute :=
(try remove_conds;
try remove_matches;
repeat match_factorize;
repeat result_factorize;
try pair_factorize) ||
bool_factorize).
......
This diff is collapsed.
From Coq
Require Import Strings.Ascii Strings.String Lists.List.
Set Implicit Arguments.
Inductive result (rT:Type) : Type :=
| Succes: rT -> result rT
| Fail: string -> result rT
| FailDet: string -> rT -> result rT.
Definition injectResult (rT:Type) (r:result rT) :=
match r with
| Succes _ => true
| Fail _ _ => false
| FailDet _ _ => false
end.
Coercion injectResult : result >-> bool.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -178,10 +178,10 @@ Proof.
+ hnf; intros; split; auto.
Qed.
Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars fBits:
Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars:
ssa (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars ->
NatSet.In y inVars ->
eval_expr E defVars fBits (toREval (toRExp e)) v REAL ->
eval_expr E defVars (toREval (toRExp e)) v REAL ->
forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n.
Proof.
intros ssa_let y_free eval_e.
......@@ -210,12 +210,12 @@ Proof.
set_tac.
Qed.
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma fBits vR vR' m n c fVars dVars outVars:
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma vR vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars dVars) outVars ->
NatSet.Subset (usedVars e) (fVars dVars) ->
~ (n fVars dVars) ->
eval_expr E Gamma fBits e vR REAL ->
eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) fBits e vR REAL.
eval_expr E Gamma e vR REAL ->
eval_expr (updEnv n vR' E) Gamma e vR REAL.
Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_ignore_bind; [auto |].
......
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