author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 62146 | 324bc1ffba12 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
41589 | 1 |
(* Title: HOL/TLA/Memory/MemoryImplementation.thy |
2 |
Author: Stephan Merz, University of Munich |
|
21624 | 3 |
*) |
3807 | 4 |
|
60592 | 5 |
section \<open>RPC-Memory example: Memory implementation\<close> |
3807 | 6 |
|
17309 | 7 |
theory MemoryImplementation |
8 |
imports Memory RPC MemClerk |
|
9 |
begin |
|
6255 | 10 |
|
58310 | 11 |
datatype histState = histA | histB |
3807 | 12 |
|
60588 | 13 |
type_synonym histType = "(PrIds \<Rightarrow> histState) stfun" (* the type of the history variable *) |
3807 | 14 |
|
15 |
consts |
|
16 |
(* the specification *) |
|
17 |
(* channel (external) *) |
|
18 |
memCh :: "memChType" |
|
19 |
(* internal variables *) |
|
6255 | 20 |
mm :: "memType" |
17309 | 21 |
|
3807 | 22 |
(* the state variables of the implementation *) |
23 |
(* channels *) |
|
24 |
(* same interface channel memCh *) |
|
25 |
crCh :: "rpcSndChType" |
|
26 |
rmCh :: "rpcRcvChType" |
|
27 |
(* internal variables *) |
|
6255 | 28 |
(* identity refinement mapping for mm -- simply reused *) |
3807 | 29 |
rst :: "rpcStType" |
30 |
cst :: "mClkStType" |
|
31 |
ires :: "resType" |
|
32 |
||
36866 | 33 |
definition |
6255 | 34 |
(* auxiliary predicates *) |
60588 | 35 |
MVOKBARF :: "Vals \<Rightarrow> bool" |
67613 | 36 |
where "MVOKBARF v \<longleftrightarrow> (v \<in> MemVal) \<or> (v = OK) \<or> (v = BadArg) \<or> (v = RPCFailure)" |
36866 | 37 |
|
38 |
definition |
|
60588 | 39 |
MVOKBA :: "Vals \<Rightarrow> bool" |
67613 | 40 |
where "MVOKBA v \<longleftrightarrow> (v \<in> MemVal) \<or> (v = OK) \<or> (v = BadArg)" |
36866 | 41 |
|
42 |
definition |
|
60588 | 43 |
MVNROKBA :: "Vals \<Rightarrow> bool" |
67613 | 44 |
where "MVNROKBA v \<longleftrightarrow> (v \<in> MemVal) \<or> (v = NotAResult) \<or> (v = OK) \<or> (v = BadArg)" |
6255 | 45 |
|
36866 | 46 |
definition |
6255 | 47 |
(* tuples of state functions changed by the various components *) |
48 |
e :: "PrIds => (bit * memOp) stfun" |
|
36866 | 49 |
where "e p = PRED (caller memCh!p)" |
50 |
||
51 |
definition |
|
60588 | 52 |
c :: "PrIds \<Rightarrow> (mClkState * (bit * Vals) * (bit * rpcOp)) stfun" |
36866 | 53 |
where "c p = PRED (cst!p, rtrner memCh!p, caller crCh!p)" |
54 |
||
55 |
definition |
|
60588 | 56 |
r :: "PrIds \<Rightarrow> (rpcState * (bit * Vals) * (bit * memOp)) stfun" |
36866 | 57 |
where "r p = PRED (rst!p, rtrner crCh!p, caller rmCh!p)" |
58 |
||
59 |
definition |
|
60588 | 60 |
m :: "PrIds \<Rightarrow> ((bit * Vals) * Vals) stfun" |
36866 | 61 |
where "m p = PRED (rtrner rmCh!p, ires!p)" |
6255 | 62 |
|
36866 | 63 |
definition |
3807 | 64 |
(* the environment action *) |
60588 | 65 |
ENext :: "PrIds \<Rightarrow> action" |
60591 | 66 |
where "ENext p = ACT (\<exists>l. #l \<in> #MemLoc \<and> Call memCh p #(read l))" |
6255 | 67 |
|
3807 | 68 |
|
36866 | 69 |
definition |
3807 | 70 |
(* specification of the history variable *) |
60588 | 71 |
HInit :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred" |
36866 | 72 |
where "HInit rmhist p = PRED rmhist!p = #histA" |
6255 | 73 |
|
36866 | 74 |
definition |
60588 | 75 |
HNext :: "histType \<Rightarrow> PrIds \<Rightarrow> action" |
36866 | 76 |
where "HNext rmhist p = ACT (rmhist!p)$ = |
60591 | 77 |
(if (MemReturn rmCh ires p \<or> RPCFail crCh rmCh rst p) |
6255 | 78 |
then #histB |
79 |
else if (MClkReply memCh crCh cst p) |
|
80 |
then #histA |
|
81 |
else $(rmhist!p))" |
|
82 |
||
36866 | 83 |
definition |
60588 | 84 |
HistP :: "histType \<Rightarrow> PrIds \<Rightarrow> temporal" |
36866 | 85 |
where "HistP rmhist p = (TEMP Init HInit rmhist p |
60591 | 86 |
\<and> \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))" |
6255 | 87 |
|
36866 | 88 |
definition |
60588 | 89 |
Hist :: "histType \<Rightarrow> temporal" |
60587 | 90 |
where "Hist rmhist = TEMP (\<forall>p. HistP rmhist p)" |
3807 | 91 |
|
36866 | 92 |
definition |
3807 | 93 |
(* the implementation *) |
60588 | 94 |
IPImp :: "PrIds \<Rightarrow> temporal" |
60591 | 95 |
where "IPImp p = (TEMP ( Init \<not>Calling memCh p \<and> \<box>[ENext p]_(e p) |
96 |
\<and> MClkIPSpec memCh crCh cst p |
|
97 |
\<and> RPCIPSpec crCh rmCh rst p |
|
98 |
\<and> RPSpec rmCh mm ires p |
|
99 |
\<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec rmCh mm ires l)))" |
|
6255 | 100 |
|
36866 | 101 |
definition |
60588 | 102 |
ImpInit :: "PrIds \<Rightarrow> stpred" |
60587 | 103 |
where "ImpInit p = PRED ( \<not>Calling memCh p |
60591 | 104 |
\<and> MClkInit crCh cst p |
105 |
\<and> RPCInit rmCh rst p |
|
106 |
\<and> PInit ires p)" |
|
6255 | 107 |
|
36866 | 108 |
definition |
60588 | 109 |
ImpNext :: "PrIds \<Rightarrow> action" |
36866 | 110 |
where "ImpNext p = (ACT [ENext p]_(e p) |
60591 | 111 |
\<and> [MClkNext memCh crCh cst p]_(c p) |
112 |
\<and> [RPCNext crCh rmCh rst p]_(r p) |
|
113 |
\<and> [RNext rmCh mm ires p]_(m p))" |
|
6255 | 114 |
|
36866 | 115 |
definition |
60588 | 116 |
ImpLive :: "PrIds \<Rightarrow> temporal" |
36866 | 117 |
where "ImpLive p = (TEMP WF(MClkFwd memCh crCh cst p)_(c p) |
60591 | 118 |
\<and> SF(MClkReply memCh crCh cst p)_(c p) |
119 |
\<and> WF(RPCNext crCh rmCh rst p)_(r p) |
|
120 |
\<and> WF(RNext rmCh mm ires p)_(m p) |
|
121 |
\<and> WF(MemReturn rmCh ires p)_(m p))" |
|
6255 | 122 |
|
36866 | 123 |
definition |
3807 | 124 |
Implementation :: "temporal" |
60591 | 125 |
where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) \<and> \<box>[ENext p]_(e p)) |
126 |
\<and> MClkISpec memCh crCh cst |
|
127 |
\<and> RPCISpec crCh rmCh rst |
|
128 |
\<and> IRSpec rmCh mm ires))" |
|
3807 | 129 |
|
36866 | 130 |
definition |
3807 | 131 |
(* the predicate S describes the states of the implementation. |
6255 | 132 |
slight simplification: two "histState" parameters instead of a |
133 |
(one- or two-element) set. |
|
134 |
NB: The second conjunct of the definition in the paper is taken care of by |
|
135 |
the type definitions. The last conjunct is asserted separately as the memory |
|
24180 | 136 |
invariant MemInv, proved in Memory.thy. *) |
60588 | 137 |
S :: "histType \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> mClkState \<Rightarrow> rpcState \<Rightarrow> histState \<Rightarrow> histState \<Rightarrow> PrIds \<Rightarrow> stpred" |
36866 | 138 |
where "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p = (PRED |
6255 | 139 |
Calling memCh p = #ecalling |
60591 | 140 |
\<and> Calling crCh p = #ccalling |
141 |
\<and> (#ccalling \<longrightarrow> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>) |
|
142 |
\<and> (\<not> #ccalling \<and> cst!p = #clkB \<longrightarrow> MVOKBARF<res<crCh!p>>) |
|
143 |
\<and> Calling rmCh p = #rcalling |
|
144 |
\<and> (#rcalling \<longrightarrow> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>) |
|
145 |
\<and> (\<not> #rcalling \<longrightarrow> ires!p = #NotAResult) |
|
146 |
\<and> (\<not> #rcalling \<and> rst!p = #rpcB \<longrightarrow> MVOKBA<res<rmCh!p>>) |
|
147 |
\<and> cst!p = #cs |
|
148 |
\<and> rst!p = #rs |
|
149 |
\<and> (rmhist!p = #hs1 \<or> rmhist!p = #hs2) |
|
150 |
\<and> MVNROKBA<ires!p>)" |
|
3807 | 151 |
|
36866 | 152 |
definition |
3807 | 153 |
(* predicates S1 -- S6 define special instances of S *) |
60588 | 154 |
S1 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred" |
36866 | 155 |
where "S1 rmhist p = S rmhist False False False clkA rpcA histA histA p" |
156 |
||
157 |
definition |
|
60588 | 158 |
S2 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred" |
36866 | 159 |
where "S2 rmhist p = S rmhist True False False clkA rpcA histA histA p" |
160 |
||
161 |
definition |
|
60588 | 162 |
S3 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred" |
36866 | 163 |
where "S3 rmhist p = S rmhist True True False clkB rpcA histA histB p" |
164 |
||
165 |
definition |
|
60588 | 166 |
S4 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred" |
36866 | 167 |
where "S4 rmhist p = S rmhist True True True clkB rpcB histA histB p" |
168 |
||
169 |
definition |
|
60588 | 170 |
S5 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred" |
36866 | 171 |
where "S5 rmhist p = S rmhist True True False clkB rpcB histB histB p" |
172 |
||
173 |
definition |
|
60588 | 174 |
S6 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred" |
36866 | 175 |
where "S6 rmhist p = S rmhist True False False clkB rpcA histB histB p" |
3807 | 176 |
|
36866 | 177 |
definition |
6255 | 178 |
(* The invariant asserts that the system is always in one of S1 - S6, for every p *) |
60588 | 179 |
ImpInv :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred" |
60591 | 180 |
where "ImpInv rmhist p = (PRED (S1 rmhist p \<or> S2 rmhist p \<or> S3 rmhist p |
181 |
\<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p))" |
|
6255 | 182 |
|
36866 | 183 |
definition |
60588 | 184 |
resbar :: "histType \<Rightarrow> resType" (* refinement mapping *) |
36866 | 185 |
where"resbar rmhist s p = |
6255 | 186 |
(if (S1 rmhist p s | S2 rmhist p s) |
187 |
then ires s p |
|
188 |
else if S3 rmhist p s |
|
17309 | 189 |
then if rmhist s p = histA |
6255 | 190 |
then ires s p else MemFailure |
191 |
else if S4 rmhist p s |
|
192 |
then if (rmhist s p = histB & ires s p = NotAResult) |
|
193 |
then MemFailure else ires s p |
|
194 |
else if S5 rmhist p s |
|
195 |
then res (rmCh s p) |
|
196 |
else if S6 rmhist p s |
|
197 |
then if res (crCh s p) = RPCFailure |
|
198 |
then MemFailure else res (crCh s p) |
|
199 |
else NotAResult)" (* dummy value *) |
|
3807 | 200 |
|
36866 | 201 |
axiomatization where |
3807 | 202 |
(* the "base" variables: everything except resbar and hist (for any index) *) |
17309 | 203 |
MI_base: "basevars (caller memCh!p, |
204 |
(rtrner memCh!p, caller crCh!p, cst!p), |
|
205 |
(rtrner crCh!p, caller rmCh!p, rst!p), |
|
206 |
(mm!l, rtrner rmCh!p, ires!p))" |
|
207 |
||
21624 | 208 |
(* |
209 |
The main theorem is theorem "Implementation" at the end of this file, |
|
210 |
which shows that the composition of a reliable memory, an RPC component, and |
|
24180 | 211 |
a memory clerk implements an unreliable memory. The files "MIsafe.thy" and |
212 |
"MIlive.thy" contain lower-level lemmas for the safety and liveness parts. |
|
21624 | 213 |
|
214 |
Steps are (roughly) numbered as in the hand proof. |
|
215 |
*) |
|
216 |
||
217 |
(* --------------------------- automatic prover --------------------------- *) |
|
218 |
||
219 |
declare if_weak_cong [cong del] |
|
220 |
||
221 |
(* A more aggressive variant that tries to solve subgoals by assumption |
|
222 |
or contradiction during the simplification. |
|
223 |
THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!! |
|
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
224 |
(but it can be a lot faster than the default setup) |
21624 | 225 |
*) |
60592 | 226 |
ML \<open> |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
227 |
val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false); |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45605
diff
changeset
|
228 |
val fast_solver = mk_solver "fast_solver" (fn ctxt => |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45605
diff
changeset
|
229 |
if Config.get ctxt config_fast_solver |
60754 | 230 |
then assume_tac ctxt ORELSE' (eresolve_tac ctxt [notE]) |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
231 |
else K no_tac); |
60592 | 232 |
\<close> |
21624 | 233 |
|
60592 | 234 |
setup \<open>map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver)\<close> |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
235 |
|
60592 | 236 |
ML \<open>val temp_elim = make_elim oo temp_use\<close> |
21624 | 237 |
|
238 |
||
239 |
||
240 |
(****************************** The history variable ******************************) |
|
241 |
||
242 |
section "History variable" |
|
243 |
||
60591 | 244 |
lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) \<and> \<box>(\<forall>p. ImpNext p) |
60588 | 245 |
\<longrightarrow> (\<exists>\<exists>rmhist. Init(\<forall>p. HInit rmhist p) |
60591 | 246 |
\<and> \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))" |
21624 | 247 |
apply clarsimp |
248 |
apply (rule historyI) |
|
249 |
apply assumption+ |
|
250 |
apply (rule MI_base) |
|
60592 | 251 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HInit_def}]) [] [] 1\<close>) |
21624 | 252 |
apply (erule fun_cong) |
60592 | 253 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}]) |
254 |
[@{thm busy_squareI}] [] 1\<close>) |
|
21624 | 255 |
apply (erule fun_cong) |
256 |
done |
|
257 |
||
60588 | 258 |
lemma History: "\<turnstile> Implementation \<longrightarrow> (\<exists>\<exists>rmhist. Hist rmhist)" |
21624 | 259 |
apply clarsimp |
260 |
apply (rule HistoryLemma [temp_use, THEN eex_mono]) |
|
261 |
prefer 3 |
|
262 |
apply (force simp: Hist_def HistP_def Init_def all_box [try_rewrite] |
|
263 |
split_box_conj [try_rewrite]) |
|
264 |
apply (auto simp: Implementation_def MClkISpec_def RPCISpec_def |
|
265 |
IRSpec_def MClkIPSpec_def RPCIPSpec_def RPSpec_def ImpInit_def |
|
266 |
Init_def ImpNext_def c_def r_def m_def all_box [temp_use] split_box_conj [temp_use]) |
|
267 |
done |
|
268 |
||
269 |
(******************************** The safety part *********************************) |
|
270 |
||
271 |
section "The safety part" |
|
272 |
||
273 |
(* ------------------------- Include lower-level lemmas ------------------------- *) |
|
274 |
||
275 |
(* RPCFailure notin MemVals U {OK,BadArg} *) |
|
276 |
||
60588 | 277 |
lemma MVOKBAnotRF: "MVOKBA x \<Longrightarrow> x \<noteq> RPCFailure" |
21624 | 278 |
apply (unfold MVOKBA_def) |
279 |
apply auto |
|
280 |
done |
|
281 |
||
282 |
(* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *) |
|
283 |
||
60588 | 284 |
lemma MVOKBARFnotNR: "MVOKBARF x \<Longrightarrow> x \<noteq> NotAResult" |
21624 | 285 |
apply (unfold MVOKBARF_def) |
286 |
apply auto |
|
287 |
done |
|
288 |
||
289 |
(* ================ Si's are mutually exclusive ================================ *) |
|
290 |
(* Si and Sj are mutually exclusive for i # j. This helps to simplify the big |
|
291 |
conditional in the definition of resbar when doing the step-simulation proof. |
|
292 |
We prove a weaker result, which suffices for our purposes: |
|
293 |
Si implies (not Sj), for j<i. |
|
294 |
*) |
|
295 |
||
296 |
(* --- not used --- |
|
60588 | 297 |
lemma S1_excl: "\<turnstile> S1 rmhist p \<longrightarrow> S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p & |
60587 | 298 |
\<not>S4 rmhist p & \<not>S5 rmhist p & \<not>S6 rmhist p" |
42772 | 299 |
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def) |
21624 | 300 |
*) |
301 |
||
60591 | 302 |
lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p \<and> \<not>S1 rmhist p" |
21624 | 303 |
by (auto simp: S_def S1_def S2_def) |
304 |
||
60591 | 305 |
lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p" |
21624 | 306 |
by (auto simp: S_def S1_def S2_def S3_def) |
307 |
||
60591 | 308 |
lemma S4_excl: "\<turnstile> S4 rmhist p \<longrightarrow> S4 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p \<and> \<not>S3 rmhist p" |
21624 | 309 |
by (auto simp: S_def S1_def S2_def S3_def S4_def) |
310 |
||
60591 | 311 |
lemma S5_excl: "\<turnstile> S5 rmhist p \<longrightarrow> S5 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p |
312 |
\<and> \<not>S3 rmhist p \<and> \<not>S4 rmhist p" |
|
21624 | 313 |
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def) |
314 |
||
60591 | 315 |
lemma S6_excl: "\<turnstile> S6 rmhist p \<longrightarrow> S6 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p |
316 |
\<and> \<not>S3 rmhist p \<and> \<not>S4 rmhist p \<and> \<not>S5 rmhist p" |
|
21624 | 317 |
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def) |
318 |
||
319 |
||
320 |
(* ==================== Lemmas about the environment ============================== *) |
|
321 |
||
60588 | 322 |
lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p" |
62146 | 323 |
by (auto simp: ENext_def ACall_def) |
21624 | 324 |
|
325 |
(* ==================== Lemmas about the implementation's states ==================== *) |
|
326 |
||
327 |
(* The following series of lemmas are used in establishing the implementation's |
|
328 |
next-state relation (Step 1.2 of the proof in the paper). For each state Si, we |
|
329 |
determine which component actions are possible and what state they result in. |
|
330 |
*) |
|
331 |
||
332 |
(* ------------------------------ State S1 ---------------------------------------- *) |
|
333 |
||
60591 | 334 |
lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p) |
60588 | 335 |
\<longrightarrow> (S2 rmhist p)$" |
62146 | 336 |
by (force simp: ENext_def ACall_def c_def r_def m_def |
21624 | 337 |
caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def) |
338 |
||
60591 | 339 |
lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)" |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
340 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
341 |
by (auto elim!: squareE [temp_use] dest!: MClkidle [temp_use] simp: S_def S1_def) |
21624 | 342 |
|
60591 | 343 |
lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (r p)" |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
344 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
345 |
by (auto elim!: squareE [temp_use] dest!: RPCidle [temp_use] simp: S_def S1_def) |
21624 | 346 |
|
60591 | 347 |
lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (m p)" |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
348 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
349 |
by (auto elim!: squareE [temp_use] dest!: Memoryidle [temp_use] simp: S_def S1_def) |
21624 | 350 |
|
60591 | 351 |
lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S1 rmhist p) |
60588 | 352 |
\<longrightarrow> unchanged (rmhist!p)" |
60592 | 353 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def}, |
39159 | 354 |
@{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def}, |
62146 | 355 |
@{thm AReturn_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>) |
21624 | 356 |
|
357 |
||
358 |
(* ------------------------------ State S2 ---------------------------------------- *) |
|
359 |
||
60591 | 360 |
lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (e p)" |
21624 | 361 |
by (auto dest!: Envbusy [temp_use] simp: S_def S2_def) |
362 |
||
60591 | 363 |
lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p" |
21624 | 364 |
by (auto simp: MClkNext_def MClkRetry_def MClkReply_def S_def S2_def) |
365 |
||
60591 | 366 |
lemma S2Forward: "\<turnstile> $(S2 rmhist p) \<and> MClkFwd memCh crCh cst p |
367 |
\<and> unchanged (e p, r p, m p, rmhist!p) |
|
60588 | 368 |
\<longrightarrow> (S3 rmhist p)$" |
60592 | 369 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def}, |
62146 | 370 |
@{thm ACall_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, |
60592 | 371 |
@{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>) |
21624 | 372 |
|
60591 | 373 |
lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)" |
21624 | 374 |
by (auto simp: S_def S2_def dest!: RPCidle [temp_use]) |
375 |
||
60591 | 376 |
lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (m p)" |
21624 | 377 |
by (auto simp: S_def S2_def dest!: Memoryidle [temp_use]) |
378 |
||
60591 | 379 |
lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S2 rmhist p) |
60588 | 380 |
\<longrightarrow> unchanged (rmhist!p)" |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
381 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
382 |
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def |
62146 | 383 |
MClkReply_def AReturn_def S_def S2_def) |
21624 | 384 |
|
385 |
(* ------------------------------ State S3 ---------------------------------------- *) |
|
386 |
||
60591 | 387 |
lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (e p)" |
21624 | 388 |
by (auto dest!: Envbusy [temp_use] simp: S_def S3_def) |
389 |
||
60591 | 390 |
lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (c p)" |
21624 | 391 |
by (auto dest!: MClkbusy [temp_use] simp: square_def S_def S3_def) |
392 |
||
60588 | 393 |
lemma S3LegalRcvArg: "\<turnstile> S3 rmhist p \<longrightarrow> IsLegalRcvArg<arg<crCh!p>>" |
21624 | 394 |
by (auto simp: IsLegalRcvArg_def MClkRelayArg_def S_def S3_def) |
395 |
||
60591 | 396 |
lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S3 rmhist p) |
397 |
\<longrightarrow> RPCFwd crCh rmCh rst p \<or> RPCFail crCh rmCh rst p" |
|
21624 | 398 |
apply clarsimp |
399 |
apply (frule S3LegalRcvArg [action_use]) |
|
400 |
apply (auto simp: RPCNext_def RPCReject_def RPCReply_def S_def S3_def) |
|
401 |
done |
|
402 |
||
60591 | 403 |
lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p \<and> HNext rmhist p \<and> $(S3 rmhist p) |
404 |
\<and> unchanged (e p, c p, m p) |
|
405 |
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)" |
|
60592 | 406 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFwd_def}, |
39159 | 407 |
@{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, |
62146 | 408 |
@{thm MClkReply_def}, @{thm AReturn_def}, @{thm ACall_def}, @{thm e_def}, |
39159 | 409 |
@{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def}, |
60592 | 410 |
@{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1\<close>) |
21624 | 411 |
|
60591 | 412 |
lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S3 rmhist p) \<and> HNext rmhist p |
413 |
\<and> unchanged (e p, c p, m p) |
|
60588 | 414 |
\<longrightarrow> (S6 rmhist p)$" |
60592 | 415 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, |
62146 | 416 |
@{thm RPCFail_def}, @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, |
39159 | 417 |
@{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def}, |
60592 | 418 |
@{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>) |
21624 | 419 |
|
60591 | 420 |
lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (m p)" |
21624 | 421 |
by (auto simp: S_def S3_def dest!: Memoryidle [temp_use]) |
422 |
||
60591 | 423 |
lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)" |
21624 | 424 |
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def |
62146 | 425 |
AReturn_def r_def rtrner_def S_def S3_def Calling_def) |
21624 | 426 |
|
427 |
(* ------------------------------ State S4 ---------------------------------------- *) |
|
428 |
||
60591 | 429 |
lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (e p)" |
21624 | 430 |
by (auto simp: S_def S4_def dest!: Envbusy [temp_use]) |
431 |
||
60591 | 432 |
lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (c p)" |
21624 | 433 |
by (auto simp: S_def S4_def dest!: MClkbusy [temp_use]) |
434 |
||
60591 | 435 |
lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (r p)" |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
436 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
437 |
by (auto elim!: squareE [temp_use] dest!: RPCbusy [temp_use] simp: S_def S4_def) |
21624 | 438 |
|
60591 | 439 |
lemma S4ReadInner: "\<turnstile> ReadInner rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p) |
440 |
\<and> HNext rmhist p \<and> $(MemInv mm l) |
|
441 |
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)" |
|
60592 | 442 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def}, |
39159 | 443 |
@{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def}, |
62146 | 444 |
@{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def}, |
39159 | 445 |
@{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, |
446 |
@{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, |
|
60592 | 447 |
@{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>) |
21624 | 448 |
|
60591 | 449 |
lemma S4Read: "\<turnstile> Read rmCh mm ires p \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p) |
450 |
\<and> HNext rmhist p \<and> (\<forall>l. $MemInv mm l) |
|
451 |
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)" |
|
21624 | 452 |
by (auto simp: Read_def dest!: S4ReadInner [temp_use]) |
453 |
||
60591 | 454 |
lemma S4WriteInner: "\<turnstile> WriteInner rmCh mm ires p l v \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p) \<and> HNext rmhist p |
455 |
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)" |
|
60592 | 456 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm WriteInner_def}, |
39159 | 457 |
@{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def}, |
62146 | 458 |
@{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def}, |
39159 | 459 |
@{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def}, |
60592 | 460 |
@{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1\<close>) |
21624 | 461 |
|
60591 | 462 |
lemma S4Write: "\<turnstile> Write rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p) |
463 |
\<and> (HNext rmhist p) |
|
464 |
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)" |
|
21624 | 465 |
by (auto simp: Write_def dest!: S4WriteInner [temp_use]) |
466 |
||
60591 | 467 |
lemma WriteS4: "\<turnstile> $ImpInv rmhist p \<and> Write rmCh mm ires p l \<longrightarrow> $S4 rmhist p" |
21624 | 468 |
by (auto simp: Write_def WriteInner_def ImpInv_def |
469 |
WrRequest_def S_def S1_def S2_def S3_def S4_def S5_def S6_def) |
|
470 |
||
60591 | 471 |
lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p) |
472 |
\<and> HNext rmhist p |
|
60588 | 473 |
\<longrightarrow> (S5 rmhist p)$" |
62146 | 474 |
by (auto simp: HNext_def MemReturn_def AReturn_def e_def c_def r_def |
21624 | 475 |
rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def) |
476 |
||
60591 | 477 |
lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)" |
21624 | 478 |
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def |
62146 | 479 |
AReturn_def m_def rtrner_def S_def S4_def Calling_def) |
21624 | 480 |
|
481 |
(* ------------------------------ State S5 ---------------------------------------- *) |
|
482 |
||
60591 | 483 |
lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (e p)" |
21624 | 484 |
by (auto simp: S_def S5_def dest!: Envbusy [temp_use]) |
485 |
||
60591 | 486 |
lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (c p)" |
21624 | 487 |
by (auto simp: S_def S5_def dest!: MClkbusy [temp_use]) |
488 |
||
60591 | 489 |
lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S5 rmhist p) |
490 |
\<longrightarrow> RPCReply crCh rmCh rst p \<or> RPCFail crCh rmCh rst p" |
|
21624 | 491 |
by (auto simp: RPCNext_def RPCReject_def RPCFwd_def S_def S5_def) |
492 |
||
60591 | 493 |
lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p) |
60588 | 494 |
\<longrightarrow> (S6 rmhist p)$" |
60592 | 495 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def}, |
62146 | 496 |
@{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def}, |
39159 | 497 |
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def}, |
60592 | 498 |
@{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>) |
21624 | 499 |
|
60591 | 500 |
lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p) |
60588 | 501 |
\<longrightarrow> (S6 rmhist p)$" |
60592 | 502 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def}, |
62146 | 503 |
@{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, |
39159 | 504 |
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, |
60592 | 505 |
@{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>) |
21624 | 506 |
|
60591 | 507 |
lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (m p)" |
21624 | 508 |
by (auto simp: S_def S5_def dest!: Memoryidle [temp_use]) |
509 |
||
60591 | 510 |
lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> $(S5 rmhist p) |
60588 | 511 |
\<longrightarrow> (rmhist!p)$ = $(rmhist!p)" |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
512 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
513 |
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def |
62146 | 514 |
MClkReply_def AReturn_def S_def S5_def) |
21624 | 515 |
|
516 |
(* ------------------------------ State S6 ---------------------------------------- *) |
|
517 |
||
60591 | 518 |
lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (e p)" |
21624 | 519 |
by (auto simp: S_def S6_def dest!: Envbusy [temp_use]) |
520 |
||
60591 | 521 |
lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S6 rmhist p) |
522 |
\<longrightarrow> MClkRetry memCh crCh cst p \<or> MClkReply memCh crCh cst p" |
|
21624 | 523 |
by (auto simp: MClkNext_def MClkFwd_def S_def S6_def) |
524 |
||
60591 | 525 |
lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p |
526 |
\<and> unchanged (e p,r p,m p) |
|
527 |
\<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)" |
|
60592 | 528 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, |
62146 | 529 |
@{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm ACall_def}, @{thm AReturn_def}, |
39159 | 530 |
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, |
60592 | 531 |
@{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>) |
21624 | 532 |
|
60591 | 533 |
lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p |
534 |
\<and> unchanged (e p,r p,m p) |
|
60588 | 535 |
\<longrightarrow> (S1 rmhist p)$" |
60592 | 536 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, |
62146 | 537 |
@{thm MemReturn_def}, @{thm RPCFail_def}, @{thm AReturn_def}, @{thm MClkReply_def}, |
39159 | 538 |
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, |
60592 | 539 |
@{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1\<close>) |
21624 | 540 |
|
60591 | 541 |
lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $S6 rmhist p \<longrightarrow> unchanged (r p)" |
21624 | 542 |
by (auto simp: S_def S6_def dest!: RPCidle [temp_use]) |
543 |
||
60591 | 544 |
lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (m p)" |
21624 | 545 |
by (auto simp: S_def S6_def dest!: Memoryidle [temp_use]) |
546 |
||
60591 | 547 |
lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)" |
62146 | 548 |
by (auto simp: HNext_def MClkReply_def AReturn_def c_def rtrner_def S_def S6_def Calling_def) |
21624 | 549 |
|
550 |
||
551 |
section "Correctness of predicate-action diagram" |
|
552 |
||
553 |
||
554 |
(* ========== Step 1.1 ================================================= *) |
|
555 |
(* The implementation's initial condition implies the state predicate S1 *) |
|
556 |
||
60591 | 557 |
lemma Step1_1: "\<turnstile> ImpInit p \<and> HInit rmhist p \<longrightarrow> S1 rmhist p" |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
558 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
559 |
by (auto elim!: squareE [temp_use] simp: MVNROKBA_def |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
560 |
MClkInit_def RPCInit_def PInit_def HInit_def ImpInit_def S_def S1_def) |
21624 | 561 |
|
562 |
(* ========== Step 1.2 ================================================== *) |
|
563 |
(* Figure 16 is a predicate-action diagram for the implementation. *) |
|
564 |
||
60591 | 565 |
lemma Step1_2_1: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p |
566 |
\<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S1 rmhist p |
|
567 |
\<longrightarrow> (S2 rmhist p)$ \<and> ENext p \<and> unchanged (c p, r p, m p)" |
|
60592 | 568 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
569 |
(map (temp_elim @{context}) |
60592 | 570 |
[@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1\<close>) |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
571 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
572 |
apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use]) |
21624 | 573 |
done |
574 |
||
60591 | 575 |
lemma Step1_2_2: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p |
576 |
\<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S2 rmhist p |
|
577 |
\<longrightarrow> (S3 rmhist p)$ \<and> MClkFwd memCh crCh cst p |
|
578 |
\<and> unchanged (e p, r p, m p, rmhist!p)" |
|
60592 | 579 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
580 |
(map (temp_elim @{context}) |
60592 | 581 |
[@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1\<close>) |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
582 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
583 |
apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use]) |
21624 | 584 |
done |
585 |
||
60591 | 586 |
lemma Step1_2_3: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p |
587 |
\<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S3 rmhist p |
|
588 |
\<longrightarrow> ((S4 rmhist p)$ \<and> RPCFwd crCh rmCh rst p \<and> unchanged (e p, c p, m p, rmhist!p)) |
|
589 |
\<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))" |
|
60592 | 590 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] |
591 |
(map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1\<close>) |
|
592 |
apply (tactic \<open>action_simp_tac @{context} [] |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
593 |
(@{thm squareE} :: |
60592 | 594 |
map (temp_elim @{context}) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1\<close>) |
21624 | 595 |
apply (auto dest!: S3Hist [temp_use]) |
596 |
done |
|
597 |
||
60591 | 598 |
lemma Step1_2_4: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p |
599 |
\<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) |
|
600 |
\<and> $S4 rmhist p \<and> (\<forall>l. $(MemInv mm l)) |
|
601 |
\<longrightarrow> ((S4 rmhist p)$ \<and> Read rmCh mm ires p \<and> unchanged (e p, c p, r p, rmhist!p)) |
|
602 |
\<or> ((S4 rmhist p)$ \<and> (\<exists>l. Write rmCh mm ires p l) \<and> unchanged (e p, c p, r p, rmhist!p)) |
|
603 |
\<or> ((S5 rmhist p)$ \<and> MemReturn rmCh ires p \<and> unchanged (e p, c p, r p))" |
|
60592 | 604 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] |
605 |
(map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1\<close>) |
|
606 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RNext_def}]) [] |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
607 |
(@{thm squareE} :: |
60592 | 608 |
map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1\<close>) |
21624 | 609 |
apply (auto dest!: S4Hist [temp_use]) |
610 |
done |
|
611 |
||
60591 | 612 |
lemma Step1_2_5: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p |
613 |
\<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S5 rmhist p |
|
614 |
\<longrightarrow> ((S6 rmhist p)$ \<and> RPCReply crCh rmCh rst p \<and> unchanged (e p, c p, m p)) |
|
615 |
\<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))" |
|
60592 | 616 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] |
617 |
(map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1\<close>) |
|
618 |
apply (tactic \<open>action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1\<close>) |
|
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
619 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
620 |
apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use]) |
21624 | 621 |
done |
622 |
||
60591 | 623 |
lemma Step1_2_6: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p |
624 |
\<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S6 rmhist p |
|
625 |
\<longrightarrow> ((S1 rmhist p)$ \<and> MClkReply memCh crCh cst p \<and> unchanged (e p, r p, m p)) |
|
626 |
\<or> ((S3 rmhist p)$ \<and> MClkRetry memCh crCh cst p \<and> unchanged (e p,r p,m p,rmhist!p))" |
|
60592 | 627 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] |
628 |
(map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1\<close>) |
|
629 |
apply (tactic \<open>action_simp_tac @{context} [] |
|
630 |
(@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1\<close>) |
|
21624 | 631 |
apply (auto dest: S6Hist [temp_use]) |
632 |
done |
|
633 |
||
634 |
(* -------------------------------------------------------------------------- |
|
635 |
Step 1.3: S1 implies the barred initial condition. |
|
636 |
*) |
|
637 |
||
638 |
section "Initialization (Step 1.3)" |
|
639 |
||
60588 | 640 |
lemma Step1_3: "\<turnstile> S1 rmhist p \<longrightarrow> PInit (resbar rmhist) p" |
60592 | 641 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm resbar_def}, |
642 |
@{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1\<close>) |
|
21624 | 643 |
|
644 |
(* ---------------------------------------------------------------------- |
|
645 |
Step 1.4: Implementation's next-state relation simulates specification's |
|
646 |
next-state relation (with appropriate substitutions) |
|
647 |
*) |
|
648 |
||
649 |
section "Step simulation (Step 1.4)" |
|
650 |
||
60591 | 651 |
lemma Step1_4_1: "\<turnstile> ENext p \<and> $S1 rmhist p \<and> (S2 rmhist p)$ \<and> unchanged (c p, r p, m p) |
60588 | 652 |
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)" |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
653 |
using [[fast_solver]] |
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
654 |
by (auto elim!: squareE [temp_use] simp: c_def r_def m_def resbar_def) |
21624 | 655 |
|
60591 | 656 |
lemma Step1_4_2: "\<turnstile> MClkFwd memCh crCh cst p \<and> $S2 rmhist p \<and> (S3 rmhist p)$ |
657 |
\<and> unchanged (e p, r p, m p, rmhist!p) |
|
60588 | 658 |
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)" |
60592 | 659 |
by (tactic \<open>action_simp_tac |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45605
diff
changeset
|
660 |
(@{context} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, |
60592 | 661 |
@{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1\<close>) |
21624 | 662 |
|
60591 | 663 |
lemma Step1_4_3a: "\<turnstile> RPCFwd crCh rmCh rst p \<and> $S3 rmhist p \<and> (S4 rmhist p)$ |
664 |
\<and> unchanged (e p, c p, m p, rmhist!p) |
|
60588 | 665 |
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)" |
21624 | 666 |
apply clarsimp |
667 |
apply (drule S3_excl [temp_use] S4_excl [temp_use])+ |
|
60592 | 668 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def}, |
669 |
@{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1\<close>) |
|
21624 | 670 |
done |
671 |
||
60591 | 672 |
lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S3 rmhist p \<and> (S6 rmhist p)$ |
673 |
\<and> unchanged (e p, c p, m p) |
|
60588 | 674 |
\<longrightarrow> MemFail memCh (resbar rmhist) p" |
21624 | 675 |
apply clarsimp |
676 |
apply (drule S6_excl [temp_use]) |
|
677 |
apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def) |
|
678 |
apply (force simp: S3_def S_def) |
|
62146 | 679 |
apply (auto simp: AReturn_def) |
21624 | 680 |
done |
681 |
||
60591 | 682 |
lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l |
683 |
\<and> unchanged (e p, c p, r p, rmhist!p) \<and> $MemInv mm l |
|
60588 | 684 |
\<longrightarrow> ReadInner memCh mm (resbar rmhist) p l" |
21624 | 685 |
apply clarsimp |
686 |
apply (drule S4_excl [temp_use])+ |
|
60592 | 687 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def}, |
688 |
@{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1\<close>) |
|
21624 | 689 |
apply (auto simp: resbar_def) |
60592 | 690 |
apply (tactic \<open>ALLGOALS (action_simp_tac |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45605
diff
changeset
|
691 |
(@{context} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, |
39159 | 692 |
@{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}]) |
60592 | 693 |
[] [@{thm impE}, @{thm MemValNotAResultE}])\<close>) |
21624 | 694 |
done |
695 |
||
60591 | 696 |
lemma Step1_4_4a: "\<turnstile> Read rmCh mm ires p \<and> $S4 rmhist p \<and> (S4 rmhist p)$ |
697 |
\<and> unchanged (e p, c p, r p, rmhist!p) \<and> (\<forall>l. $(MemInv mm l)) |
|
60588 | 698 |
\<longrightarrow> Read memCh mm (resbar rmhist) p" |
21624 | 699 |
by (force simp: Read_def elim!: Step1_4_4a1 [temp_use]) |
700 |
||
60591 | 701 |
lemma Step1_4_4b1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> WriteInner rmCh mm ires p l v |
702 |
\<and> unchanged (e p, c p, r p, rmhist!p) |
|
60588 | 703 |
\<longrightarrow> WriteInner memCh mm (resbar rmhist) p l v" |
21624 | 704 |
apply clarsimp |
705 |
apply (drule S4_excl [temp_use])+ |
|
60592 | 706 |
apply (tactic \<open>action_simp_tac (@{context} addsimps |
39159 | 707 |
[@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def}, |
60592 | 708 |
@{thm c_def}, @{thm m_def}]) [] [] 1\<close>) |
21624 | 709 |
apply (auto simp: resbar_def) |
60592 | 710 |
apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps |
39159 | 711 |
[@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def}, |
60592 | 712 |
@{thm S4_def}, @{thm WrRequest_def}]) [] [])\<close>) |
21624 | 713 |
done |
714 |
||
60591 | 715 |
lemma Step1_4_4b: "\<turnstile> Write rmCh mm ires p l \<and> $S4 rmhist p \<and> (S4 rmhist p)$ |
716 |
\<and> unchanged (e p, c p, r p, rmhist!p) |
|
60588 | 717 |
\<longrightarrow> Write memCh mm (resbar rmhist) p l" |
21624 | 718 |
by (force simp: Write_def elim!: Step1_4_4b1 [temp_use]) |
719 |
||
60591 | 720 |
lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> (S5 rmhist p)$ |
721 |
\<and> unchanged (e p, c p, r p) |
|
60588 | 722 |
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)" |
60592 | 723 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def}, |
724 |
@{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>) |
|
21624 | 725 |
apply (drule S4_excl [temp_use] S5_excl [temp_use])+ |
42771
b6037ae5027d
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
wenzelm
parents:
42770
diff
changeset
|
726 |
using [[fast_solver]] |
62146 | 727 |
apply (auto elim!: squareE [temp_use] simp: MemReturn_def AReturn_def) |
21624 | 728 |
done |
729 |
||
60591 | 730 |
lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$ |
731 |
\<and> unchanged (e p, c p, m p) |
|
60588 | 732 |
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)" |
21624 | 733 |
apply clarsimp |
734 |
apply (drule S5_excl [temp_use] S6_excl [temp_use])+ |
|
735 |
apply (auto simp: e_def c_def m_def resbar_def) |
|
62146 | 736 |
apply (auto simp: RPCReply_def AReturn_def S5_def S_def dest!: MVOKBAnotRF [temp_use]) |
21624 | 737 |
done |
738 |
||
60591 | 739 |
lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$ |
740 |
\<and> unchanged (e p, c p, m p) |
|
60588 | 741 |
\<longrightarrow> MemFail memCh (resbar rmhist) p" |
21624 | 742 |
apply clarsimp |
743 |
apply (drule S6_excl [temp_use]) |
|
62146 | 744 |
apply (auto simp: e_def c_def m_def RPCFail_def AReturn_def MemFail_def resbar_def) |
21624 | 745 |
apply (auto simp: S5_def S_def) |
746 |
done |
|
747 |
||
60591 | 748 |
lemma Step1_4_6a: "\<turnstile> MClkReply memCh crCh cst p \<and> $S6 rmhist p \<and> (S1 rmhist p)$ |
749 |
\<and> unchanged (e p, r p, m p) |
|
60588 | 750 |
\<longrightarrow> MemReturn memCh (resbar rmhist) p" |
21624 | 751 |
apply clarsimp |
752 |
apply (drule S6_excl [temp_use])+ |
|
60592 | 753 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def}, |
39159 | 754 |
@{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def}, |
62146 | 755 |
@{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\<close>) |
21624 | 756 |
apply simp_all (* simplify if-then-else *) |
60592 | 757 |
apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps |
758 |
[@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>) |
|
21624 | 759 |
done |
760 |
||
60591 | 761 |
lemma Step1_4_6b: "\<turnstile> MClkRetry memCh crCh cst p \<and> $S6 rmhist p \<and> (S3 rmhist p)$ |
762 |
\<and> unchanged (e p, r p, m p, rmhist!p) |
|
60588 | 763 |
\<longrightarrow> MemFail memCh (resbar rmhist) p" |
21624 | 764 |
apply clarsimp |
765 |
apply (drule S3_excl [temp_use])+ |
|
60592 | 766 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def}, @{thm r_def}, |
767 |
@{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1\<close>) |
|
21624 | 768 |
apply (auto simp: S6_def S_def) |
769 |
done |
|
770 |
||
60588 | 771 |
lemma S_lemma: "\<turnstile> unchanged (e p, c p, r p, m p, rmhist!p) |
772 |
\<longrightarrow> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)" |
|
21624 | 773 |
by (auto simp: e_def c_def r_def m_def caller_def rtrner_def S_def Calling_def) |
774 |
||
60588 | 775 |
lemma Step1_4_7H: "\<turnstile> unchanged (e p, c p, r p, m p, rmhist!p) |
776 |
\<longrightarrow> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p, |
|
21624 | 777 |
S4 rmhist p, S5 rmhist p, S6 rmhist p)" |
778 |
apply clarsimp |
|
779 |
apply (rule conjI) |
|
780 |
apply (force simp: c_def) |
|
781 |
apply (force simp: S1_def S2_def S3_def S4_def S5_def S6_def intro!: S_lemma [temp_use]) |
|
782 |
done |
|
783 |
||
60588 | 784 |
lemma Step1_4_7: "\<turnstile> unchanged (e p, c p, r p, m p, rmhist!p) |
785 |
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p, |
|
21624 | 786 |
S3 rmhist p, S4 rmhist p, S5 rmhist p, S6 rmhist p)" |
787 |
apply (rule actionI) |
|
788 |
apply (unfold action_rews) |
|
789 |
apply (rule impI) |
|
790 |
apply (frule Step1_4_7H [temp_use]) |
|
791 |
apply (auto simp: e_def c_def r_def m_def rtrner_def resbar_def) |
|
792 |
done |
|
793 |
||
794 |
(* Frequently needed abbreviation: distinguish between idling and non-idling |
|
795 |
steps of the implementation, and try to solve the idling case by simplification |
|
796 |
*) |
|
60592 | 797 |
ML \<open> |
42786 | 798 |
fun split_idle_tac ctxt = |
799 |
SELECT_GOAL |
|
60754 | 800 |
(TRY (resolve_tac ctxt @{thms actionI} 1) THEN |
60588 | 801 |
Induct_Tacs.case_tac ctxt "(s,t) \<Turnstile> unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
802 |
rewrite_goals_tac ctxt @{thms action_rews} THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
803 |
forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45605
diff
changeset
|
804 |
asm_full_simp_tac ctxt 1); |
60592 | 805 |
\<close> |
42786 | 806 |
|
60592 | 807 |
method_setup split_idle = \<open> |
42786 | 808 |
Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers) |
809 |
>> (K (SIMPLE_METHOD' o split_idle_tac)) |
|
60592 | 810 |
\<close> |
42786 | 811 |
|
21624 | 812 |
(* ---------------------------------------------------------------------- |
813 |
Combine steps 1.2 and 1.4 to prove that the implementation satisfies |
|
814 |
the specification's next-state relation. |
|
815 |
*) |
|
816 |
||
817 |
(* Steps that leave all variables unchanged are safe, so I may assume |
|
818 |
that some variable changes in the proof that a step is safe. *) |
|
60588 | 819 |
lemma unchanged_safe: "\<turnstile> (\<not>unchanged (e p, c p, r p, m p, rmhist!p) |
820 |
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) |
|
821 |
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
|
42786 | 822 |
apply (split_idle simp: square_def) |
21624 | 823 |
apply force |
824 |
done |
|
825 |
(* turn into (unsafe, looping!) introduction rule *) |
|
45605 | 826 |
lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]] |
21624 | 827 |
|
60591 | 828 |
lemma S1safe: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
60588 | 829 |
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 830 |
apply clarsimp |
831 |
apply (rule unchanged_safeI) |
|
832 |
apply (rule idle_squareI) |
|
833 |
apply (auto dest!: Step1_2_1 [temp_use] Step1_4_1 [temp_use]) |
|
834 |
done |
|
835 |
||
60591 | 836 |
lemma S2safe: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
60588 | 837 |
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 838 |
apply clarsimp |
839 |
apply (rule unchanged_safeI) |
|
840 |
apply (rule idle_squareI) |
|
841 |
apply (auto dest!: Step1_2_2 [temp_use] Step1_4_2 [temp_use]) |
|
842 |
done |
|
843 |
||
60591 | 844 |
lemma S3safe: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
60588 | 845 |
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 846 |
apply clarsimp |
847 |
apply (rule unchanged_safeI) |
|
848 |
apply (auto dest!: Step1_2_3 [temp_use]) |
|
849 |
apply (auto simp: square_def UNext_def dest!: Step1_4_3a [temp_use] Step1_4_3b [temp_use]) |
|
850 |
done |
|
851 |
||
60591 | 852 |
lemma S4safe: "\<turnstile> $S4 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
853 |
\<and> (\<forall>l. $(MemInv mm l)) |
|
60588 | 854 |
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 855 |
apply clarsimp |
856 |
apply (rule unchanged_safeI) |
|
857 |
apply (auto dest!: Step1_2_4 [temp_use]) |
|
858 |
apply (auto simp: square_def UNext_def RNext_def |
|
859 |
dest!: Step1_4_4a [temp_use] Step1_4_4b [temp_use] Step1_4_4c [temp_use]) |
|
860 |
done |
|
861 |
||
60591 | 862 |
lemma S5safe: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
60588 | 863 |
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 864 |
apply clarsimp |
865 |
apply (rule unchanged_safeI) |
|
866 |
apply (auto dest!: Step1_2_5 [temp_use]) |
|
867 |
apply (auto simp: square_def UNext_def dest!: Step1_4_5a [temp_use] Step1_4_5b [temp_use]) |
|
868 |
done |
|
869 |
||
60591 | 870 |
lemma S6safe: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
60588 | 871 |
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 872 |
apply clarsimp |
873 |
apply (rule unchanged_safeI) |
|
874 |
apply (auto dest!: Step1_2_6 [temp_use]) |
|
875 |
apply (auto simp: square_def UNext_def RNext_def |
|
876 |
dest!: Step1_4_6a [temp_use] Step1_4_6b [temp_use]) |
|
877 |
done |
|
878 |
||
879 |
(* ---------------------------------------------------------------------- |
|
880 |
Step 1.5: Temporal refinement proof, based on previous steps. |
|
881 |
*) |
|
882 |
||
883 |
section "The liveness part" |
|
884 |
||
885 |
(* Liveness assertions for the different implementation states, based on the |
|
886 |
fairness conditions. Prove subgoals of WF1 / SF1 rules as separate lemmas |
|
887 |
for readability. Reuse action proofs from safety part. |
|
888 |
*) |
|
889 |
||
890 |
(* ------------------------------ State S1 ------------------------------ *) |
|
891 |
||
60591 | 892 |
lemma S1_successors: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
893 |
\<longrightarrow> (S1 rmhist p)$ \<or> (S2 rmhist p)$" |
|
42786 | 894 |
apply split_idle |
21624 | 895 |
apply (auto dest!: Step1_2_1 [temp_use]) |
896 |
done |
|
897 |
||
898 |
(* Show that the implementation can satisfy the high-level fairness requirements |
|
899 |
by entering the state S1 infinitely often. |
|
900 |
*) |
|
901 |
||
60588 | 902 |
lemma S1_RNextdisabled: "\<turnstile> S1 rmhist p \<longrightarrow> |
60587 | 903 |
\<not>Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))" |
60592 | 904 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, |
905 |
@{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1\<close>) |
|
21624 | 906 |
apply force |
907 |
done |
|
908 |
||
60588 | 909 |
lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow> |
60587 | 910 |
\<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))" |
60592 | 911 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def}, |
62146 | 912 |
@{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>) |
21624 | 913 |
|
60588 | 914 |
lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p |
915 |
\<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" |
|
21624 | 916 |
by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use] |
917 |
elim!: STL4E [temp_use] DmdImplE [temp_use]) |
|
918 |
||
60588 | 919 |
lemma Return_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p |
920 |
\<longrightarrow> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" |
|
21624 | 921 |
by (auto simp: WF_alt [try_rewrite] |
922 |
intro!: S1_Returndisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use]) |
|
923 |
||
924 |
(* ------------------------------ State S2 ------------------------------ *) |
|
925 |
||
60591 | 926 |
lemma S2_successors: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
927 |
\<longrightarrow> (S2 rmhist p)$ \<or> (S3 rmhist p)$" |
|
42786 | 928 |
apply split_idle |
21624 | 929 |
apply (auto dest!: Step1_2_2 [temp_use]) |
930 |
done |
|
931 |
||
60591 | 932 |
lemma S2MClkFwd_successors: "\<turnstile> ($S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
933 |
\<and> <MClkFwd memCh crCh cst p>_(c p) |
|
60588 | 934 |
\<longrightarrow> (S3 rmhist p)$" |
21624 | 935 |
by (auto simp: angle_def dest!: Step1_2_2 [temp_use]) |
936 |
||
60591 | 937 |
lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
60588 | 938 |
\<longrightarrow> $Enabled (<MClkFwd memCh crCh cst p>_(c p))" |
21624 | 939 |
apply (auto simp: c_def intro!: MClkFwd_ch_enabled [temp_use] MClkFwd_enabled [temp_use]) |
940 |
apply (cut_tac MI_base) |
|
941 |
apply (blast dest: base_pair) |
|
942 |
apply (simp_all add: S_def S2_def) |
|
943 |
done |
|
944 |
||
60591 | 945 |
lemma S2_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
946 |
\<and> WF(MClkFwd memCh crCh cst p)_(c p) |
|
60588 | 947 |
\<longrightarrow> (S2 rmhist p \<leadsto> S3 rmhist p)" |
21624 | 948 |
by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+ |
949 |
||
950 |
(* ------------------------------ State S3 ------------------------------ *) |
|
951 |
||
60591 | 952 |
lemma S3_successors: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
953 |
\<longrightarrow> (S3 rmhist p)$ \<or> (S4 rmhist p \<or> S6 rmhist p)$" |
|
42786 | 954 |
apply split_idle |
21624 | 955 |
apply (auto dest!: Step1_2_3 [temp_use]) |
956 |
done |
|
957 |
||
60591 | 958 |
lemma S3RPC_successors: "\<turnstile> ($S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
959 |
\<and> <RPCNext crCh rmCh rst p>_(r p) |
|
960 |
\<longrightarrow> (S4 rmhist p \<or> S6 rmhist p)$" |
|
21624 | 961 |
apply (auto simp: angle_def dest!: Step1_2_3 [temp_use]) |
962 |
done |
|
963 |
||
60591 | 964 |
lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
60588 | 965 |
\<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))" |
21624 | 966 |
apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use]) |
967 |
apply (cut_tac MI_base) |
|
968 |
apply (blast dest: base_pair) |
|
969 |
apply (simp_all add: S_def S3_def) |
|
970 |
done |
|
971 |
||
60591 | 972 |
lemma S3_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
973 |
\<and> WF(RPCNext crCh rmCh rst p)_(r p) |
|
974 |
\<longrightarrow> (S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p)" |
|
21624 | 975 |
by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+ |
976 |
||
977 |
(* ------------- State S4 -------------------------------------------------- *) |
|
978 |
||
60591 | 979 |
lemma S4_successors: "\<turnstile> $S4 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
980 |
\<and> (\<forall>l. $MemInv mm l) |
|
981 |
\<longrightarrow> (S4 rmhist p)$ \<or> (S5 rmhist p)$" |
|
42786 | 982 |
apply split_idle |
21624 | 983 |
apply (auto dest!: Step1_2_4 [temp_use]) |
984 |
done |
|
985 |
||
986 |
(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *) |
|
987 |
||
60591 | 988 |
lemma S4a_successors: "\<turnstile> $(S4 rmhist p \<and> ires!p = #NotAResult) |
989 |
\<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> (\<forall>l. $MemInv mm l) |
|
990 |
\<longrightarrow> (S4 rmhist p \<and> ires!p = #NotAResult)$ |
|
991 |
\<or> ((S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)$" |
|
42786 | 992 |
apply split_idle |
21624 | 993 |
apply (auto dest!: Step1_2_4 [temp_use]) |
994 |
done |
|
995 |
||
60591 | 996 |
lemma S4aRNext_successors: "\<turnstile> ($(S4 rmhist p \<and> ires!p = #NotAResult) |
997 |
\<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> (\<forall>l. $MemInv mm l)) |
|
998 |
\<and> <RNext rmCh mm ires p>_(m p) |
|
999 |
\<longrightarrow> ((S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)$" |
|
21624 | 1000 |
by (auto simp: angle_def |
1001 |
dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use]) |
|
1002 |
||
60591 | 1003 |
lemma S4aRNext_enabled: "\<turnstile> $(S4 rmhist p \<and> ires!p = #NotAResult) |
1004 |
\<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l) |
|
60588 | 1005 |
\<longrightarrow> $Enabled (<RNext rmCh mm ires p>_(m p))" |
21624 | 1006 |
apply (auto simp: m_def intro!: RNext_enabled [temp_use]) |
1007 |
apply (cut_tac MI_base) |
|
1008 |
apply (blast dest: base_pair) |
|
1009 |
apply (simp add: S_def S4_def) |
|
1010 |
done |
|
1011 |
||
60591 | 1012 |
lemma S4a_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
1013 |
\<and> (\<forall>l. $MemInv mm l)) \<and> WF(RNext rmCh mm ires p)_(m p) |
|
1014 |
\<longrightarrow> (S4 rmhist p \<and> ires!p = #NotAResult |
|
1015 |
\<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)" |
|
21624 | 1016 |
by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+ |
1017 |
||
1018 |
(* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *) |
|
1019 |
||
60591 | 1020 |
lemma S4b_successors: "\<turnstile> $(S4 rmhist p \<and> ires!p \<noteq> #NotAResult) |
1021 |
\<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l) |
|
1022 |
\<longrightarrow> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult)$ \<or> (S5 rmhist p)$" |
|
42786 | 1023 |
apply (split_idle simp: m_def) |
21624 | 1024 |
apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use]) |
1025 |
done |
|
1026 |
||
60591 | 1027 |
lemma S4bReturn_successors: "\<turnstile> ($(S4 rmhist p \<and> ires!p \<noteq> #NotAResult) |
1028 |
\<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
|
1029 |
\<and> (\<forall>l. $MemInv mm l)) \<and> <MemReturn rmCh ires p>_(m p) |
|
60588 | 1030 |
\<longrightarrow> (S5 rmhist p)$" |
21624 | 1031 |
by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use]) |
1032 |
||
60591 | 1033 |
lemma S4bReturn_enabled: "\<turnstile> $(S4 rmhist p \<and> ires!p \<noteq> #NotAResult) |
1034 |
\<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
|
1035 |
\<and> (\<forall>l. $MemInv mm l) |
|
60588 | 1036 |
\<longrightarrow> $Enabled (<MemReturn rmCh ires p>_(m p))" |
21624 | 1037 |
apply (auto simp: m_def intro!: MemReturn_enabled [temp_use]) |
1038 |
apply (cut_tac MI_base) |
|
1039 |
apply (blast dest: base_pair) |
|
1040 |
apply (simp add: S_def S4_def) |
|
1041 |
done |
|
1042 |
||
60591 | 1043 |
lemma S4b_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l)) |
1044 |
\<and> WF(MemReturn rmCh ires p)_(m p) |
|
1045 |
\<longrightarrow> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)" |
|
21624 | 1046 |
by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+ |
1047 |
||
1048 |
(* ------------------------------ State S5 ------------------------------ *) |
|
1049 |
||
60591 | 1050 |
lemma S5_successors: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
1051 |
\<longrightarrow> (S5 rmhist p)$ \<or> (S6 rmhist p)$" |
|
42786 | 1052 |
apply split_idle |
21624 | 1053 |
apply (auto dest!: Step1_2_5 [temp_use]) |
1054 |
done |
|
1055 |
||
60591 | 1056 |
lemma S5RPC_successors: "\<turnstile> ($S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
1057 |
\<and> <RPCNext crCh rmCh rst p>_(r p) |
|
60588 | 1058 |
\<longrightarrow> (S6 rmhist p)$" |
21624 | 1059 |
by (auto simp: angle_def dest!: Step1_2_5 [temp_use]) |
1060 |
||
60591 | 1061 |
lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
60588 | 1062 |
\<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))" |
21624 | 1063 |
apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use]) |
1064 |
apply (cut_tac MI_base) |
|
1065 |
apply (blast dest: base_pair) |
|
1066 |
apply (simp_all add: S_def S5_def) |
|
1067 |
done |
|
1068 |
||
60591 | 1069 |
lemma S5_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
1070 |
\<and> WF(RPCNext crCh rmCh rst p)_(r p) |
|
60588 | 1071 |
\<longrightarrow> (S5 rmhist p \<leadsto> S6 rmhist p)" |
21624 | 1072 |
by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+ |
1073 |
||
1074 |
(* ------------------------------ State S6 ------------------------------ *) |
|
1075 |
||
60591 | 1076 |
lemma S6_successors: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
1077 |
\<longrightarrow> (S1 rmhist p)$ \<or> (S3 rmhist p)$ \<or> (S6 rmhist p)$" |
|
42786 | 1078 |
apply split_idle |
21624 | 1079 |
apply (auto dest!: Step1_2_6 [temp_use]) |
1080 |
done |
|
1081 |
||
1082 |
lemma S6MClkReply_successors: |
|
60591 | 1083 |
"\<turnstile> ($S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
1084 |
\<and> <MClkReply memCh crCh cst p>_(c p) |
|
60588 | 1085 |
\<longrightarrow> (S1 rmhist p)$" |
21624 | 1086 |
by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use]) |
1087 |
||
1088 |
lemma MClkReplyS6: |
|
60591 | 1089 |
"\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p" |
60592 | 1090 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, |
62146 | 1091 |
@{thm MClkReply_def}, @{thm AReturn_def}, @{thm ImpInv_def}, @{thm S_def}, |
60592 | 1092 |
@{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>) |
21624 | 1093 |
|
60588 | 1094 |
lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))" |
21624 | 1095 |
apply (auto simp: c_def intro!: MClkReply_enabled [temp_use]) |
1096 |
apply (cut_tac MI_base) |
|
1097 |
apply (blast dest: base_pair) |
|
60592 | 1098 |
apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} |
1099 |
addsimps [@{thm S_def}, @{thm S6_def}]) [] [])\<close>) |
|
21624 | 1100 |
done |
1101 |
||
60591 | 1102 |
lemma S6_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> $(ImpInv rmhist p)) |
1103 |
\<and> SF(MClkReply memCh crCh cst p)_(c p) \<and> \<box>\<diamond>(S6 rmhist p) |
|
60588 | 1104 |
\<longrightarrow> \<box>\<diamond>(S1 rmhist p)" |
21624 | 1105 |
apply clarsimp |
60588 | 1106 |
apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))") |
21624 | 1107 |
apply (erule InfiniteEnsures) |
1108 |
apply assumption |
|
60592 | 1109 |
apply (tactic \<open>action_simp_tac @{context} [] |
1110 |
(map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1\<close>) |
|
21624 | 1111 |
apply (auto simp: SF_def) |
1112 |
apply (erule contrapos_np) |
|
1113 |
apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use]) |
|
1114 |
done |
|
1115 |
||
1116 |
(* --------------- aggregate leadsto properties----------------------------- *) |
|
1117 |
||
60588 | 1118 |
lemma S5S6LeadstoS6: "sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p |
60591 | 1119 |
\<Longrightarrow> sigma \<Turnstile> (S5 rmhist p \<or> S6 rmhist p) \<leadsto> S6 rmhist p" |
21624 | 1120 |
by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) |
1121 |
||
60591 | 1122 |
lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p; |
60588 | 1123 |
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk> |
60591 | 1124 |
\<Longrightarrow> sigma \<Turnstile> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p |
60587 | 1125 |
\<leadsto> S6 rmhist p" |
21624 | 1126 |
by (auto intro!: LatticeDisjunctionIntro [temp_use] |
1127 |
S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use]) |
|
1128 |
||
60591 | 1129 |
lemma S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult |
1130 |
\<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p; |
|
1131 |
sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p; |
|
60588 | 1132 |
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk> |
60591 | 1133 |
\<Longrightarrow> sigma \<Turnstile> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p" |
1134 |
apply (subgoal_tac "sigma \<Turnstile> (S4 rmhist p \<and> ires!p = #NotAResult) \<or> |
|
1135 |
(S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p") |
|
1136 |
apply (erule_tac G = "PRED ((S4 rmhist p \<and> ires!p = #NotAResult) \<or> |
|
1137 |
(S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p)" in |
|
21624 | 1138 |
LatticeTransitivity [temp_use]) |
1139 |
apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use]) |
|
1140 |
apply (rule LatticeDisjunctionIntro [temp_use]) |
|
1141 |
apply (erule LatticeTransitivity [temp_use]) |
|
1142 |
apply (erule LatticeTriangle2 [temp_use]) |
|
1143 |
apply assumption |
|
1144 |
apply (auto intro!: S4bS5S6LeadstoS6 [temp_use]) |
|
1145 |
done |
|
1146 |
||
60591 | 1147 |
lemma S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p; |
1148 |
sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult |
|
1149 |
\<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p; |
|
1150 |
sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p; |
|
60588 | 1151 |
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk> |
60591 | 1152 |
\<Longrightarrow> sigma \<Turnstile> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p" |
21624 | 1153 |
apply (rule LatticeDisjunctionIntro [temp_use]) |
1154 |
apply (erule LatticeTriangle2 [temp_use]) |
|
1155 |
apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]]) |
|
1156 |
apply (auto intro!: S4S5S6LeadstoS6 [temp_use] necT [temp_use] |
|
1157 |
intro: ImplLeadsto_gen [temp_use] simp: Init_defs) |
|
1158 |
done |
|
1159 |
||
60588 | 1160 |
lemma S2S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p; |
60591 | 1161 |
sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p; |
1162 |
sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult |
|
1163 |
\<leadsto> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<or> S5 rmhist p; |
|
1164 |
sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p; |
|
60588 | 1165 |
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk> |
60591 | 1166 |
\<Longrightarrow> sigma \<Turnstile> S2 rmhist p \<or> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p |
60587 | 1167 |
\<leadsto> S6 rmhist p" |
21624 | 1168 |
apply (rule LatticeDisjunctionIntro [temp_use]) |
1169 |
apply (rule LatticeTransitivity [temp_use]) |
|
1170 |
prefer 2 apply assumption |
|
1171 |
apply (rule S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]]) |
|
1172 |
apply (auto intro!: S3S4S5S6LeadstoS6 [temp_use] necT [temp_use] |
|
1173 |
intro: ImplLeadsto_gen [temp_use] simp: Init_defs) |
|
1174 |
done |
|
1175 |
||
60588 | 1176 |
lemma NotS1LeadstoS6: "\<lbrakk> sigma \<Turnstile> \<box>ImpInv rmhist p; |
1177 |
sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p; |
|
60591 | 1178 |
sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p; |
1179 |
sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult |
|
1180 |
\<leadsto> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<or> S5 rmhist p; |
|
1181 |
sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p; |
|
60588 | 1182 |
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk> |
1183 |
\<Longrightarrow> sigma \<Turnstile> \<not>S1 rmhist p \<leadsto> S6 rmhist p" |
|
21624 | 1184 |
apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]]) |
1185 |
apply assumption+ |
|
1186 |
apply (erule INV_leadsto [temp_use]) |
|
1187 |
apply (rule ImplLeadsto_gen [temp_use]) |
|
1188 |
apply (rule necT [temp_use]) |
|
1189 |
apply (auto simp: ImpInv_def Init_defs intro!: necT [temp_use]) |
|
1190 |
done |
|
1191 |
||
60588 | 1192 |
lemma S1Infinite: "\<lbrakk> sigma \<Turnstile> \<not>S1 rmhist p \<leadsto> S6 rmhist p; |
1193 |
sigma \<Turnstile> \<box>\<diamond>S6 rmhist p \<longrightarrow> \<box>\<diamond>S1 rmhist p \<rbrakk> |
|
1194 |
\<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>S1 rmhist p" |
|
21624 | 1195 |
apply (rule classical) |
60592 | 1196 |
apply (tactic \<open>asm_lr_simp_tac (@{context} addsimps |
1197 |
[temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1\<close>) |
|
21624 | 1198 |
apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use]) |
1199 |
done |
|
1200 |
||
1201 |
section "Refinement proof (step 1.5)" |
|
1202 |
||
1203 |
(* Prove invariants of the implementation: |
|
1204 |
a. memory invariant |
|
1205 |
b. "implementation invariant": always in states S1,...,S6 |
|
1206 |
*) |
|
60588 | 1207 |
lemma Step1_5_1a: "\<turnstile> IPImp p \<longrightarrow> (\<forall>l. \<box>$MemInv mm l)" |
21624 | 1208 |
by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use]) |
1209 |
||
60591 | 1210 |
lemma Step1_5_1b: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<and> \<box>(ImpNext p) |
1211 |
\<and> \<box>[HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> \<box>(\<forall>l. $MemInv mm l) |
|
60588 | 1212 |
\<longrightarrow> \<box>ImpInv rmhist p" |
42770
3ebce8d71a05
eliminated obsolete MI_css -- use current context directly;
wenzelm
parents:
42018
diff
changeset
|
1213 |
apply invariant |
21624 | 1214 |
apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use] |
1215 |
dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use] |
|
1216 |
S3_successors [temp_use] S4_successors [temp_use] S5_successors [temp_use] |
|
1217 |
S6_successors [temp_use]) |
|
1218 |
done |
|
1219 |
||
1220 |
(*** Initialization ***) |
|
60591 | 1221 |
lemma Step1_5_2a: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<longrightarrow> Init(PInit (resbar rmhist) p)" |
21624 | 1222 |
by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3 [temp_use]) |
1223 |
||
1224 |
(*** step simulation ***) |
|
60591 | 1225 |
lemma Step1_5_2b: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p) |
1226 |
\<and> $ImpInv rmhist p \<and> (\<forall>l. $MemInv mm l)) |
|
60588 | 1227 |
\<longrightarrow> \<box>[UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 1228 |
by (auto simp: ImpInv_def elim!: STL4E [temp_use] |
1229 |
dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use] |
|
1230 |
S5safe [temp_use] S6safe [temp_use]) |
|
1231 |
||
1232 |
(*** Liveness ***) |
|
60591 | 1233 |
lemma GoodImpl: "\<turnstile> IPImp p \<and> HistP rmhist p |
1234 |
\<longrightarrow> Init(ImpInit p \<and> HInit rmhist p) |
|
1235 |
\<and> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)) |
|
1236 |
\<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) |
|
1237 |
\<and> ImpLive p" |
|
21624 | 1238 |
apply clarsimp |
60591 | 1239 |
apply (subgoal_tac "sigma \<Turnstile> Init (ImpInit p \<and> HInit rmhist p) \<and> \<box> (ImpNext p) \<and> |
1240 |
\<box>[HNext rmhist p]_ (c p, r p, m p, rmhist!p) \<and> \<box> (\<forall>l. $MemInv mm l)") |
|
21624 | 1241 |
apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite] |
1242 |
dest!: Step1_5_1b [temp_use]) |
|
1243 |
apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def |
|
1244 |
ImpLive_def c_def r_def m_def) |
|
1245 |
apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def |
|
1246 |
HistP_def Init_def ImpInit_def) |
|
1247 |
apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def |
|
1248 |
ImpNext_def c_def r_def m_def split_box_conj [temp_use]) |
|
1249 |
apply (force simp: HistP_def) |
|
1250 |
apply (force simp: allT [temp_use] dest!: Step1_5_1a [temp_use]) |
|
1251 |
done |
|
1252 |
||
1253 |
(* The implementation is infinitely often in state S1... *) |
|
60591 | 1254 |
lemma Step1_5_3a: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)) |
1255 |
\<and> \<box>(\<forall>l. $MemInv mm l) |
|
1256 |
\<and> \<box>($ImpInv rmhist p) \<and> ImpLive p |
|
60588 | 1257 |
\<longrightarrow> \<box>\<diamond>S1 rmhist p" |
21624 | 1258 |
apply (clarsimp simp: ImpLive_def) |
1259 |
apply (rule S1Infinite) |
|
1260 |
apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite] |
|
1261 |
intro!: NotS1LeadstoS6 [temp_use] S2_live [temp_use] S3_live [temp_use] |
|
1262 |
S4a_live [temp_use] S4b_live [temp_use] S5_live [temp_use]) |
|
1263 |
apply (auto simp: split_box_conj [temp_use] intro!: S6_live [temp_use]) |
|
1264 |
done |
|
1265 |
||
1266 |
(* ... and therefore satisfies the fairness requirements of the specification *) |
|
60591 | 1267 |
lemma Step1_5_3b: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)) |
1268 |
\<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p |
|
60588 | 1269 |
\<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 1270 |
by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use]) |
1271 |
||
60591 | 1272 |
lemma Step1_5_3c: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)) |
1273 |
\<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p |
|
60588 | 1274 |
\<longrightarrow> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" |
21624 | 1275 |
by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use]) |
1276 |
||
1277 |
(* QED step of step 1 *) |
|
60591 | 1278 |
lemma Step1: "\<turnstile> IPImp p \<and> HistP rmhist p \<longrightarrow> UPSpec memCh mm (resbar rmhist) p" |
21624 | 1279 |
by (auto simp: UPSpec_def split_box_conj [temp_use] |
1280 |
dest!: GoodImpl [temp_use] intro!: Step1_5_2a [temp_use] Step1_5_2b [temp_use] |
|
1281 |
Step1_5_3b [temp_use] Step1_5_3c [temp_use]) |
|
1282 |
||
1283 |
(* ------------------------------ Step 2 ------------------------------ *) |
|
1284 |
section "Step 2" |
|
1285 |
||
60591 | 1286 |
lemma Step2_2a: "\<turnstile> Write rmCh mm ires p l \<and> ImpNext p |
1287 |
\<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p) |
|
1288 |
\<and> $ImpInv rmhist p |
|
1289 |
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (e p, c p, r p, rmhist!p)" |
|
21624 | 1290 |
apply clarsimp |
1291 |
apply (drule WriteS4 [action_use]) |
|
1292 |
apply assumption |
|
42786 | 1293 |
apply split_idle |
21624 | 1294 |
apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use] |
1295 |
S4RPCUnch [temp_use]) |
|
1296 |
apply (auto simp: square_def dest: S4Write [temp_use]) |
|
1297 |
done |
|
1298 |
||
60588 | 1299 |
lemma Step2_2: "\<turnstile> (\<forall>p. ImpNext p) |
60591 | 1300 |
\<and> (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) |
1301 |
\<and> (\<forall>p. $ImpInv rmhist p) |
|
1302 |
\<and> [\<exists>q. Write rmCh mm ires q l]_(mm!l) |
|
60588 | 1303 |
\<longrightarrow> [\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)" |
21624 | 1304 |
apply (auto intro!: squareCI elim!: squareE) |
1305 |
apply (assumption | rule exI Step1_4_4b [action_use])+ |
|
1306 |
apply (force intro!: WriteS4 [temp_use]) |
|
1307 |
apply (auto dest!: Step2_2a [temp_use]) |
|
1308 |
done |
|
1309 |
||
60588 | 1310 |
lemma Step2_lemma: "\<turnstile> \<box>( (\<forall>p. ImpNext p) |
60591 | 1311 |
\<and> (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) |
1312 |
\<and> (\<forall>p. $ImpInv rmhist p) |
|
1313 |
\<and> [\<exists>q. Write rmCh mm ires q l]_(mm!l)) |
|
60588 | 1314 |
\<longrightarrow> \<box>[\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)" |
21624 | 1315 |
by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use]) |
1316 |
||
60591 | 1317 |
lemma Step2: "\<turnstile> #l \<in> #MemLoc \<and> (\<forall>p. IPImp p \<and> HistP rmhist p) |
60588 | 1318 |
\<longrightarrow> MSpec memCh mm (resbar rmhist) l" |
21624 | 1319 |
apply (auto simp: MSpec_def) |
1320 |
apply (force simp: IPImp_def MSpec_def) |
|
1321 |
apply (auto intro!: Step2_lemma [temp_use] simp: split_box_conj [temp_use] all_box [temp_use]) |
|
1322 |
prefer 4 |
|
1323 |
apply (force simp: IPImp_def MSpec_def) |
|
1324 |
apply (auto simp: split_box_conj [temp_use] elim!: allE dest!: GoodImpl [temp_use]) |
|
1325 |
done |
|
1326 |
||
1327 |
(* ----------------------------- Main theorem --------------------------------- *) |
|
1328 |
section "Memory implementation" |
|
1329 |
||
1330 |
(* The combination of a legal caller, the memory clerk, the RPC component, |
|
1331 |
and a reliable memory implement the unreliable memory. |
|
1332 |
*) |
|
1333 |
||
1334 |
(* Implementation of internal specification by combination of implementation |
|
1335 |
and history variable with explicit refinement mapping |
|
1336 |
*) |
|
60591 | 1337 |
lemma Impl_IUSpec: "\<turnstile> Implementation \<and> Hist rmhist \<longrightarrow> IUSpec memCh mm (resbar rmhist)" |
21624 | 1338 |
by (auto simp: IUSpec_def Implementation_def IPImp_def MClkISpec_def |
1339 |
RPCISpec_def IRSpec_def Hist_def intro!: Step1 [temp_use] Step2 [temp_use]) |
|
1340 |
||
1341 |
(* The main theorem: introduce hiding and eliminate history variable. *) |
|
60588 | 1342 |
lemma Implementation: "\<turnstile> Implementation \<longrightarrow> USpec memCh" |
21624 | 1343 |
apply clarsimp |
1344 |
apply (frule History [temp_use]) |
|
1345 |
apply (auto simp: USpec_def intro: eexI [temp_use] Impl_IUSpec [temp_use] |
|
1346 |
MI_base [temp_use] elim!: eexE) |
|
1347 |
done |
|
3807 | 1348 |
|
1349 |
end |