Commit c025a217 authored by Joachim Bard's avatar Joachim Bard

redefining type precond

parent 06425929
...@@ -61,10 +61,10 @@ Proof. ...@@ -61,10 +61,10 @@ Proof.
assert (dVars_range_valid NatSet.empty E1 absenv). assert (dVars_range_valid NatSet.empty E1 absenv).
{ unfold dVars_range_valid. { unfold dVars_range_valid.
intros; set_tac. } intros; set_tac. }
assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None)) (* assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
as affine_dvars_valid. as affine_dvars_valid.
{ unfold affine_dVars_range_valid. { unfold affine_dVars_range_valid.
intros; set_tac. } intros; set_tac. } *)
assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)). assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
{ hnf; intros a in_empty. { hnf; intros a in_empty.
set_tac. } set_tac. }
...@@ -145,8 +145,8 @@ Proof. ...@@ -145,8 +145,8 @@ Proof.
as freeVars_contained by set_tac. as freeVars_contained by set_tac.
assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f. assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
{ eapply (RangeValidatorCmd_sound _ (fVars:=preVars P)); eauto; intuition. { eapply (RangeValidatorCmd_sound _ (fVars:=preVars P)); eauto; intuition.
unfold affine_dVars_range_valid; intros. (* unfold affine_dVars_range_valid; intros.
set_tac. } 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 valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi]. destruct iv as [f_lo f_hi].
......
...@@ -1191,10 +1191,10 @@ Proof. ...@@ -1191,10 +1191,10 @@ Proof.
assert (dVars_range_valid NatSet.empty E1 A). assert (dVars_range_valid NatSet.empty E1 A).
{ unfold dVars_range_valid. { unfold dVars_range_valid.
intros; set_tac. } intros; set_tac. }
assert (AffineValidation.affine_dVars_range_valid NatSet.empty E1 A 1 (FloverMap.empty _) (fun _ => None)) (* assert (AffineValidation.affine_dVars_range_valid NatSet.empty E1 A 1 (FloverMap.empty _) (fun _ => None))
as affine_dvars_valid. as affine_dvars_valid.
{ unfold AffineValidation.affine_dVars_range_valid. { unfold AffineValidation.affine_dVars_range_valid.
intros; set_tac. } intros; set_tac. } *)
assert (NatSet.Subset (usedVars (B2Qexpr e) -- NatSet.empty) (Expressions.usedVars (B2Qexpr e))). assert (NatSet.Subset (usedVars (B2Qexpr e) -- NatSet.empty) (Expressions.usedVars (B2Qexpr e))).
{ hnf; intros a in_empty. { hnf; intros a in_empty.
set_tac. } set_tac. }
...@@ -1270,8 +1270,8 @@ Proof. ...@@ -1270,8 +1270,8 @@ Proof.
- eapply (ssa_equal_set (inVars:=preVars P)); eauto. - eapply (ssa_equal_set (inVars:=preVars P)); eauto.
apply NatSetProps.empty_union_2. set_tac. apply NatSetProps.empty_union_2. set_tac.
- unfold RealRangeArith.dVars_range_valid. intros; set_tac. - unfold RealRangeArith.dVars_range_valid. intros; set_tac.
- unfold AffineValidation.affine_dVars_range_valid; intros. (* - unfold AffineValidation.affine_dVars_range_valid; intros.
set_tac. set_tac. *)
- eapply validSSA_checks_freeVars; eauto. } - eapply validSSA_checks_freeVars; eauto. }
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 valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
......
...@@ -35,12 +35,6 @@ Arguments mkIntv _ _/. ...@@ -35,12 +35,6 @@ Arguments mkIntv _ _/.
Arguments ivlo _ /. Arguments ivlo _ /.
Arguments ivhi _ /. Arguments ivhi _ /.
(**
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
**)
Definition precond :Type := nat -> intv.
(** (**
Abbreviation for the type of a variable environment, which should be a partial function Abbreviation for the type of a variable environment, which should be a partial function
**) **)
......
...@@ -170,6 +170,12 @@ Module FloverMapFacts := OrdProperties (FloverMap). ...@@ -170,6 +170,12 @@ Module FloverMapFacts := OrdProperties (FloverMap).
Definition analysisResult :Type := FloverMap.t (intv * error). Definition analysisResult :Type := FloverMap.t (intv * error).
Definition expressionsAffine: Type := FloverMap.t (affine_form Q). Definition expressionsAffine: Type := FloverMap.t (affine_form Q).
(**
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
**)
Definition precond : Type := FloverMap.t intv.
Definition contained_flover_map V expmap1 expmap2 := Definition contained_flover_map V expmap1 expmap2 :=
forall (e: expr Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v. forall (e: expr Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v.
......
...@@ -13,12 +13,6 @@ Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop : ...@@ -13,12 +13,6 @@ Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :
FloverMap.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. (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
forall v,
NatSet.In v fVars ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
Ltac kill_trivial_exists := Ltac kill_trivial_exists :=
match goal with match goal with
| [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e | [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
......
...@@ -8,8 +8,10 @@ From Flover ...@@ -8,8 +8,10 @@ From Flover
From Coq Require Export QArith.QArith. From Coq Require Export QArith.QArith.
From Flover From Flover
Require Export IntervalValidation AffineValidation SMTArith SMTValidation RealRangeArith Require Export IntervalValidation SMTArith SMTValidation RealRangeArith
Infra.ExpressionAbbrevs Commands. Infra.ExpressionAbbrevs Commands.
(* TODO: add AffineValidation again to the export part after it is
adjusted to the new precond type *)
Definition RangeValidator e A P Qmap dVars := Definition RangeValidator e A P Qmap dVars :=
if if
...@@ -23,11 +25,11 @@ Definition RangeValidator e A P Qmap dVars := ...@@ -23,11 +25,11 @@ Definition RangeValidator e A P Qmap dVars :=
end. end.
*) *)
Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : FloverMap.t intv) Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond)
Qmap dVars (E : env) (Gamma : FloverMap.t mType): Qmap dVars (E : env) (Gamma : FloverMap.t mType):
RangeValidator e A P Qmap dVars = true -> RangeValidator e A P Qmap dVars = true ->
dVars_range_valid dVars E A -> dVars_range_valid dVars E A ->
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) -> (* affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) -> *)
validTypes e Gamma -> validTypes e Gamma ->
eval_precond E P -> eval_precond E P ->
unsat_queries E Qmap -> unsat_queries E Qmap ->
...@@ -81,13 +83,13 @@ Definition RangeValidatorCmd e A P Qmap dVars:= ...@@ -81,13 +83,13 @@ Definition RangeValidatorCmd e A P Qmap dVars:=
end. end.
*) *)
Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : FloverMap.t intv) Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond)
(Qmap: FloverMap.t (SMTLogic * SMTLogic)) dVars (Qmap: usedQueries) dVars
(E : env) Gamma fVars outVars: (E : env) Gamma fVars outVars:
RangeValidatorCmd f A P Qmap dVars = true -> RangeValidatorCmd f A P Qmap dVars = true ->
ssa f (NatSet.union fVars dVars) outVars -> ssa f (NatSet.union fVars dVars) outVars ->
dVars_range_valid dVars E A -> dVars_range_valid dVars E A ->
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) -> (* affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) -> *)
eval_precond E P -> eval_precond E P ->
NatSet.Subset (preVars P) fVars -> NatSet.Subset (preVars P) fVars ->
NatSet.Subset (freeVars f -- dVars) fVars -> NatSet.Subset (freeVars f -- dVars) fVars ->
......
...@@ -42,6 +42,8 @@ Inductive SMTLogic := ...@@ -42,6 +42,8 @@ Inductive SMTLogic :=
Definition FalseQ := NotQ TrueQ. Definition FalseQ := NotQ TrueQ.
Definition usedQueries : Type := FloverMap.t (SMTLogic * SMTLogic).
Definition getPrecond q := Definition getPrecond q :=
match q with match q with
| AndQ p _ => Some p | AndQ p _ => Some p
...@@ -252,7 +254,7 @@ Definition unsat_queries E qMap := ...@@ -252,7 +254,7 @@ Definition unsat_queries E qMap :=
forall e ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh. forall e ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh.
(* (*
Definition eval_precond E (P: FloverMap.t intv) := Definition eval_precond E (P: precond) :=
forall x iv, FloverMap.find (Var Q x) P = Some iv forall x iv, FloverMap.find (Var Q x) P = Some iv
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv). -> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*) *)
...@@ -274,7 +276,7 @@ Proof. ...@@ -274,7 +276,7 @@ Proof.
apply eqb_var in Heq. cbn in *. now subst. apply eqb_var in Heq. cbn in *. now subst.
Qed. Qed.
Definition eval_precond E (P: FloverMap.t intv) := Definition eval_precond E (P: precond) :=
forall x iv, List.In (Var Q x, iv) (FloverMap.elements P) -> forall x iv, List.In (Var Q x, iv) (FloverMap.elements P) ->
exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv). exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
...@@ -284,7 +286,7 @@ Definition addVar2Set (elt: (expr Q * intv)) s := ...@@ -284,7 +286,7 @@ Definition addVar2Set (elt: (expr Q * intv)) s :=
| _ => s | _ => s
end. end.
Definition preVars (P: FloverMap.t intv) := Definition preVars (P: precond) :=
List.fold_right addVar2Set NatSet.empty (FloverMap.elements P). List.fold_right addVar2Set NatSet.empty (FloverMap.elements P).
Lemma preVars_sound P x iv : Lemma preVars_sound P x iv :
...@@ -329,7 +331,7 @@ Definition addVarConstraint (el: expr Q * intv) q := ...@@ -329,7 +331,7 @@ Definition addVarConstraint (el: expr Q * intv) q :=
| _ => q | _ => q
end. end.
Definition precond2SMT (P: FloverMap.t intv) := Definition precond2SMT (P: precond) :=
List.fold_right addVarConstraint TrueQ (FloverMap.elements P). List.fold_right addVarConstraint TrueQ (FloverMap.elements P).
(* (*
......
...@@ -28,7 +28,7 @@ Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P := ...@@ -28,7 +28,7 @@ Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P :=
| _ => hi | _ => hi
end. end.
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: FloverMap.t (SMTLogic * SMTLogic)) P := Definition tightenBounds (e: expr Q) (iv: intv) (qMap: usedQueries) P :=
match FloverMap.find e qMap with match FloverMap.find e qMap with
| None => iv | None => iv
| Some (loQ, hiQ) => (tightenLowerBound e (fst iv) loQ P, tightenUpperBound e (snd iv) hiQ P) | Some (loQ, hiQ) => (tightenLowerBound e (fst iv) loQ P, tightenUpperBound e (snd iv) hiQ P)
...@@ -107,8 +107,8 @@ Lemma Rle_trans2 a b x y z : ...@@ -107,8 +107,8 @@ Lemma Rle_trans2 a b x y z :
(a <= x)%R -> (z <= b)%R -> (x <= y <= z)%R -> (a <= y <= b)%R. (a <= x)%R -> (z <= b)%R -> (x <= y <= z)%R -> (a <= y <= b)%R.
Proof. lra. Qed. Proof. lra. Qed.
Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t intv) Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
(Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars: NatSet.t) : bool := (Q: usedQueries) (validVars: NatSet.t) : bool :=
match FloverMap.find e A with match FloverMap.find e A with
| None => false | None => false
| Some (intv, _) => | Some (intv, _) =>
...@@ -195,8 +195,8 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t ...@@ -195,8 +195,8 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t
end end
end. end.
Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: FloverMap.t intv) Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: precond)
(Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars:NatSet.t) : bool := (Q: usedQueries) (validVars:NatSet.t) : bool :=
match f with match f with
| Let m x e g => false | Let m x e g => false
(* (*
...@@ -214,8 +214,8 @@ Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: FloverMap.t ...@@ -214,8 +214,8 @@ Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: FloverMap.t
validSMTIntervalbounds e A P Q validVars validSMTIntervalbounds e A P Q validVars
end. end.
Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverMap.t intv) Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond)
(Q: FloverMap.t (SMTLogic * SMTLogic)) fVars dVars (E: env) Gamma : (Q: usedQueries) fVars dVars (E: env) Gamma :
unsat_queries E Q -> unsat_queries E Q ->
validSMTIntervalbounds f A P Q dVars = true -> validSMTIntervalbounds f A P Q dVars = true ->
dVars_range_valid dVars E A -> dVars_range_valid dVars E A ->
...@@ -435,7 +435,7 @@ Proof. ...@@ -435,7 +435,7 @@ Proof.
Qed. Qed.
Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult)
(Q: FloverMap.t (SMTLogic * SMTLogic)): (Q: usedQueries):
forall Gamma E fVars dVars outVars P, forall Gamma E fVars dVars outVars P,
ssa f (NatSet.union fVars dVars) outVars -> ssa f (NatSet.union fVars dVars) outVars ->
dVars_range_valid dVars E A -> dVars_range_valid dVars E A ->
......
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