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