From c025a217efc89ebc5d3092023aeab1c0c22d70df Mon Sep 17 00:00:00 2001 From: Joachim Bard Date: Fri, 14 Dec 2018 10:55:29 +0100 Subject: [PATCH] redefining type precond --- coq/CertificateChecker.v | 8 ++++---- coq/IEEE_connection.v | 8 ++++---- coq/Infra/Abbrevs.v | 6 ------ coq/Infra/ExpressionAbbrevs.v | 6 ++++++ coq/RealRangeArith.v | 6 ------ coq/RealRangeValidator.v | 14 ++++++++------ coq/SMTArith.v | 10 ++++++---- coq/SMTValidation.v | 16 ++++++++-------- 8 files changed, 36 insertions(+), 38 deletions(-) diff --git a/coq/CertificateChecker.v b/coq/CertificateChecker.v index a58cea1..cc9cafa 100644 --- a/coq/CertificateChecker.v +++ b/coq/CertificateChecker.v @@ -61,10 +61,10 @@ Proof. assert (dVars_range_valid NatSet.empty E1 absenv). { unfold dVars_range_valid. 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. { unfold affine_dVars_range_valid. - intros; set_tac. } + intros; set_tac. } *) assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)). { hnf; intros a in_empty. set_tac. } @@ -145,8 +145,8 @@ Proof. as freeVars_contained by set_tac. assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f. { eapply (RangeValidatorCmd_sound _ (fVars:=preVars P)); eauto; intuition. - unfold affine_dVars_range_valid; intros. - set_tac. } + (* unfold affine_dVars_range_valid; intros. + set_tac. *) } 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]. diff --git a/coq/IEEE_connection.v b/coq/IEEE_connection.v index dec6127..51423e0 100644 --- a/coq/IEEE_connection.v +++ b/coq/IEEE_connection.v @@ -1191,10 +1191,10 @@ Proof. assert (dVars_range_valid NatSet.empty E1 A). { unfold dVars_range_valid. 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. { unfold AffineValidation.affine_dVars_range_valid. - intros; set_tac. } + intros; set_tac. } *) assert (NatSet.Subset (usedVars (B2Qexpr e) -- NatSet.empty) (Expressions.usedVars (B2Qexpr e))). { hnf; intros a in_empty. set_tac. } @@ -1270,8 +1270,8 @@ Proof. - eapply (ssa_equal_set (inVars:=preVars P)); eauto. apply NatSetProps.empty_union_2. set_tac. - unfold RealRangeArith.dVars_range_valid. intros; set_tac. - - unfold AffineValidation.affine_dVars_range_valid; intros. - set_tac. + (* - unfold AffineValidation.affine_dVars_range_valid; intros. + set_tac. *) - eapply validSSA_checks_freeVars; eauto. } pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single. destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]]. diff --git a/coq/Infra/Abbrevs.v b/coq/Infra/Abbrevs.v index 4994b90..9a60030 100644 --- a/coq/Infra/Abbrevs.v +++ b/coq/Infra/Abbrevs.v @@ -35,12 +35,6 @@ Arguments mkIntv _ _/. Arguments ivlo _ /. 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 **) diff --git a/coq/Infra/ExpressionAbbrevs.v b/coq/Infra/ExpressionAbbrevs.v index ebffcdd..9206ed8 100644 --- a/coq/Infra/ExpressionAbbrevs.v +++ b/coq/Infra/ExpressionAbbrevs.v @@ -170,6 +170,12 @@ Module FloverMapFacts := OrdProperties (FloverMap). Definition analysisResult :Type := FloverMap.t (intv * error). 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 := forall (e: expr Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v. diff --git a/coq/RealRangeArith.v b/coq/RealRangeArith.v index 9ac4ad2..17e9f15 100644 --- a/coq/RealRangeArith.v +++ b/coq/RealRangeArith.v @@ -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) /\ (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 := match goal with | [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e diff --git a/coq/RealRangeValidator.v b/coq/RealRangeValidator.v index 6e38c8d..2b60923 100644 --- a/coq/RealRangeValidator.v +++ b/coq/RealRangeValidator.v @@ -8,8 +8,10 @@ From Flover From Coq Require Export QArith.QArith. From Flover - Require Export IntervalValidation AffineValidation SMTArith SMTValidation RealRangeArith + Require Export IntervalValidation SMTArith SMTValidation RealRangeArith 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 := if @@ -23,11 +25,11 @@ Definition RangeValidator e A P Qmap dVars := 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): RangeValidator e A P Qmap dVars = true -> 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 -> eval_precond E P -> unsat_queries E Qmap -> @@ -81,13 +83,13 @@ Definition RangeValidatorCmd e A P Qmap dVars:= end. *) -Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : FloverMap.t intv) - (Qmap: FloverMap.t (SMTLogic * SMTLogic)) dVars +Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) + (Qmap: usedQueries) dVars (E : env) Gamma fVars outVars: RangeValidatorCmd f A P Qmap dVars = true -> ssa f (NatSet.union fVars dVars) outVars -> 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 -> NatSet.Subset (preVars P) fVars -> NatSet.Subset (freeVars f -- dVars) fVars -> diff --git a/coq/SMTArith.v b/coq/SMTArith.v index cc21c0d..2694c26 100644 --- a/coq/SMTArith.v +++ b/coq/SMTArith.v @@ -42,6 +42,8 @@ Inductive SMTLogic := Definition FalseQ := NotQ TrueQ. +Definition usedQueries : Type := FloverMap.t (SMTLogic * SMTLogic). + Definition getPrecond q := match q with | AndQ p _ => Some p @@ -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. (* -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 -> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv). *) @@ -274,7 +276,7 @@ Proof. apply eqb_var in Heq. cbn in *. now subst. 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) -> 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 := | _ => s end. -Definition preVars (P: FloverMap.t intv) := +Definition preVars (P: precond) := List.fold_right addVar2Set NatSet.empty (FloverMap.elements P). Lemma preVars_sound P x iv : @@ -329,7 +331,7 @@ Definition addVarConstraint (el: expr Q * intv) q := | _ => q end. -Definition precond2SMT (P: FloverMap.t intv) := +Definition precond2SMT (P: precond) := List.fold_right addVarConstraint TrueQ (FloverMap.elements P). (* diff --git a/coq/SMTValidation.v b/coq/SMTValidation.v index bd33053..d4f7bdb 100644 --- a/coq/SMTValidation.v +++ b/coq/SMTValidation.v @@ -28,7 +28,7 @@ Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P := | _ => hi 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 | None => iv | 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 : (a <= x)%R -> (z <= b)%R -> (x <= y <= z)%R -> (a <= y <= b)%R. Proof. lra. Qed. -Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t intv) - (Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars: NatSet.t) : bool := +Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond) + (Q: usedQueries) (validVars: NatSet.t) : bool := match FloverMap.find e A with | None => false | Some (intv, _) => @@ -195,8 +195,8 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t end end. -Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: FloverMap.t intv) - (Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars:NatSet.t) : bool := +Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: precond) + (Q: usedQueries) (validVars:NatSet.t) : bool := match f with | Let m x e g => false (* @@ -214,8 +214,8 @@ Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: FloverMap.t validSMTIntervalbounds e A P Q validVars end. -Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverMap.t intv) - (Q: FloverMap.t (SMTLogic * SMTLogic)) fVars dVars (E: env) Gamma : +Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond) + (Q: usedQueries) fVars dVars (E: env) Gamma : unsat_queries E Q -> validSMTIntervalbounds f A P Q dVars = true -> dVars_range_valid dVars E A -> @@ -435,7 +435,7 @@ Proof. Qed. Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) - (Q: FloverMap.t (SMTLogic * SMTLogic)): + (Q: usedQueries): forall Gamma E fVars dVars outVars P, ssa f (NatSet.union fVars dVars) outVars -> dVars_range_valid dVars E A -> -- GitLab