forked from achlipala/frap
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ModelChecking_sol.v
82 lines (74 loc) · 2.37 KB
/
ModelChecking_sol.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
Theorem factorial_ok_2 :
invariantFor (factorial_sys 2) (fact_correct 2).
Proof.
simplify.
eapply invariant_weaken.
(* We begin like in last chapter, by strengthening to an inductive
* invariant. *)
apply multiStepClosure_ok.
(* The difference is that we will use multi-step closure to find the invariant
* automatically. Note that the invariant appears as an existential variable,
* whose name begins with a question mark. *)
simplify.
rewrite fact_init_is.
(* It's important to phrase the current candidate invariant explicitly as a
* finite set, before continuing. Otherwise, it won't be obvious how to take
* the one-step closure. *)
(* Compute which states are reachable after one step. *)
eapply MscStep.
apply oneStepClosure_split; simplify.
invert H; simplify.
apply singleton_in.
apply oneStepClosure_empty.
simplify.
(* Compute which states are reachable after two steps. *)
eapply MscStep.
apply oneStepClosure_split; simplify.
invert H; simplify.
apply singleton_in.
apply oneStepClosure_split; simplify.
invert H; simplify.
apply singleton_in.
apply oneStepClosure_empty.
simplify.
(* Compute which states are reachable after three steps. *)
eapply MscStep.
apply oneStepClosure_split; simplify.
invert H; simplify.
apply singleton_in.
apply oneStepClosure_split; simplify.
invert H; simplify.
apply singleton_in.
apply oneStepClosure_split; simplify.
invert H; simplify.
apply singleton_in.
apply oneStepClosure_empty.
simplify.
(* Now the candidate invariatn is closed under single steps. Let's prove
* it. *)
apply MscDone.
apply prove_oneStepClosure; simplify.
propositional.
propositional; invert H0; try equality.
invert H; equality.
invert H1; equality.
(* Finally, we prove that our new invariant implies the simpler, noninductive
* one that we started with. *)
simplify.
propositional; subst; simplify; propositional.
(* [subst]: remove all hypotheses like [x = e] for variables [x], simply
* replacing all uses of [x] by [e]. *)
Qed.
Theorem twoadd2_ok :
invariantFor (parallel twoadd_sys twoadd_sys) (twoadd_correct (private := _)).
Proof.
eapply invariant_weaken.
eapply invariant_simulates.
apply withInterference_abstracts.
apply withInterference_parallel.
apply twoadd_ok.
apply twoadd_ok.
unfold twoadd_correct.
invert 1.
assumption.
Qed.