From c129d8447e9a4e18fc3f14da2892c9b8cf6cd48a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 14 Feb 2016 19:23:26 -0500 Subject: [PATCH] Some heftier ModelChecking examples --- Frap.v | 2 +- ModelChecking.v | 122 ++++++++++++++++++++++++++++++++++++++---------- Sets.v | 11 +++++ 3 files changed, 110 insertions(+), 25 deletions(-) diff --git a/Frap.v b/Frap.v index 26480e9..866a6fc 100644 --- a/Frap.v +++ b/Frap.v @@ -43,7 +43,7 @@ Ltac invert0 e := invert e; fail. Ltac invert1 e := invert0 e || (invert e; []). Ltac invert2 e := invert1 e || (invert e; [|]). -Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *); +Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *; repeat unifyTails); repeat (removeDups || doSubtract). Ltac propositional := intuition idtac. diff --git a/ModelChecking.v b/ModelChecking.v index 8e303f0..510acf4 100644 --- a/ModelChecking.v +++ b/ModelChecking.v @@ -146,13 +146,24 @@ Proof. constructor. Qed. -Theorem singleton_in : forall {A} (x : A), - {x} x. +Theorem singleton_in : forall {A} (x : A) rest, + ({x} \cup rest) x. Proof. + simplify. + left. simplify. equality. Qed. +Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A), + s2 x + -> (s1 \cup s2) x. +Proof. + simplify. + right. + assumption. +Qed. + Theorem factorial_ok_2 : invariantFor (factorial_sys 2) (fact_correct 2). Proof. @@ -213,13 +224,19 @@ Ltac model_check_done := | [ H : _ |- _ ] => invert H end; simplify; equality. +Ltac singletoner := + repeat match goal with + | _ => apply singleton_in + | [ |- (_ \cup _) _ ] => apply singleton_in_other + end. + Ltac model_check_step := eapply MscStep; [ repeat ((apply oneStepClosure_empty; simplify) || (apply oneStepClosure_split; [ simplify; repeat match goal with | [ H : _ |- _ ] => invert H - end; apply singleton_in | ])) + end; solve [ singletoner ] | ])) | simplify ]. Ltac model_check_steps1 := model_check_done || model_check_step. @@ -246,8 +263,8 @@ Proof. model_check. Qed. -Theorem factorial_ok_4 : - invariantFor (factorial_sys 4) (fact_correct 4). +Theorem factorial_ok_5 : + invariantFor (factorial_sys 5) (fact_correct 5). Proof. model_check. Qed. @@ -255,21 +272,6 @@ Qed. (** * Getting smarter about not exploring from the same state twice *) -(*Theorem oneStepClosure_new_done : forall state (sys : trsys state) (invariant : state -> Prop), - (forall st, sys.(Initial) st -> invariant st) - -> oneStepClosure_new sys invariant invariant - -> invariantFor sys invariant. -Proof. - unfold oneStepClosure_new. - propositional. - apply invariant_induction. - assumption. - simplify. - eapply H2. - eassumption. - assumption. -Qed.*) - Inductive multiStepClosure_smarter {state} (sys : trsys state) : (state -> Prop) -> (state -> Prop) -> (state -> Prop) -> Prop := | MscsDone : forall inv worklist, @@ -383,21 +385,23 @@ Ltac smodel_check_done := Ltac smodel_check_step := eapply MscsStep; [ - repeat ((apply oneStepClosure_new_empty; simplify) + repeat ((apply oneStepClosure_new_empty; solve [ simplify ]) || (apply oneStepClosure_new_split; [ simplify; repeat match goal with | [ H : _ |- _ ] => invert H - end; apply singleton_in | ])) + end; solve [ singletoner ] | ])) | simplify ]. Ltac smodel_check_steps1 := smodel_check_done || smodel_check_step. Ltac smodel_check_steps := repeat smodel_check_steps1. -Ltac smodel_check_find_invariant := +Ltac smodel_check_setup := simplify; eapply invariantFor_weaken; [ - apply multiStepClosure_smarter_ok; simplify; smodel_check_steps + apply multiStepClosure_smarter_ok; simplify | ]. +Ltac smodel_check_find_invariant := smodel_check_setup; [ smodel_check_steps | ]. + Ltac smodel_check := smodel_check_find_invariant; model_check_finish. Theorem factorial_ok_2_smarter_snazzy : @@ -417,3 +421,73 @@ Theorem factorial_ok_5_smarter_snazzy : Proof. smodel_check. Qed. + + +(** * Back to the multithreaded example from last time *) + +Theorem increment2_init_is : + parallel1 increment_init increment_init = { {| Shared := {| Global := 0; Locked := false |}; + Private := (Lock, Lock) |} }. +Proof. + simplify. + apply sets_equal; simplify. + propositional. + + invert H. + invert H2. + invert H4. + equality. + + rewrite <- H0. + constructor. + constructor. + constructor. +Qed. + +Hint Rewrite increment2_init_is. + +(*Theorem increment2_ok : + invariantFor increment2_sys increment2_right_answer. +Proof. + unfold increment2_right_answer. + smodel_check. +Qed.*) + +Definition increment3_sys := parallel increment_sys increment2_sys. + +Definition increment3_right_answer + (s : threaded_state inc_state (increment_program * (increment_program * increment_program))) := + s.(Private) = (Done, (Done, Done)) + -> s.(Shared).(Global) = 3. + +Theorem increment3_init_is : + parallel1 increment_init (parallel1 increment_init increment_init) + = { {| Shared := {| Global := 0; Locked := false |}; + Private := (Lock, (Lock, Lock)) |} }. +Proof. + simplify. + apply sets_equal; simplify. + propositional. + + invert H. + invert H2. + invert H4. + equality. + invert H. + + rewrite <- H0. + constructor. + constructor. + constructor. + constructor. +Qed. + +Hint Rewrite increment3_init_is. + +Theorem increment3_ok : + invariantFor increment3_sys increment3_right_answer. +Proof. + unfold increment3_right_answer. + smodel_check_find_invariant. + model_check_finish. +Qed. diff --git a/Sets.v b/Sets.v index c808620..c0b1fc9 100644 --- a/Sets.v +++ b/Sets.v @@ -238,3 +238,14 @@ Ltac doSubtract := || (apply DsKeep; [ simpl; intuition congruence | ]) || (apply DsDrop; [ simpl; intuition congruence | ])) end. + + +(** Undetermined set variables in fixed points should be turned into the empty set. *) +Ltac unifyTails := + match goal with + | [ |- context[_ \cup ?x] ] => is_evar x; + match type of x with + | set ?A => unify x (constant (@nil A)) + | ?A -> Prop => unify x (constant (@nil A)) + end + end.