1(*  Title:      HOL/TLA/Memory/MemoryImplementation.thy
2    Author:     Stephan Merz, University of Munich
3*)
4
5section \<open>RPC-Memory example: Memory implementation\<close>
6
7theory MemoryImplementation
8imports Memory RPC MemClerk
9begin
10
11datatype histState = histA | histB
12
13type_synonym histType = "(PrIds \<Rightarrow> histState) stfun"  (* the type of the history variable *)
14
15consts
16  (* the specification *)
17     (* channel (external) *)
18  memCh         :: "memChType"
19     (* internal variables *)
20  mm            :: "memType"
21
22  (* the state variables of the implementation *)
23     (* channels *)
24  (* same interface channel memCh *)
25  crCh          :: "rpcSndChType"
26  rmCh          :: "rpcRcvChType"
27     (* internal variables *)
28  (* identity refinement mapping for mm -- simply reused *)
29  rst           :: "rpcStType"
30  cst           :: "mClkStType"
31  ires          :: "resType"
32
33definition
34  (* auxiliary predicates *)
35  MVOKBARF      :: "Vals \<Rightarrow> bool"
36  where "MVOKBARF v \<longleftrightarrow> (v \<in> MemVal) \<or> (v = OK) \<or> (v = BadArg) \<or> (v = RPCFailure)"
37
38definition
39  MVOKBA        :: "Vals \<Rightarrow> bool"
40  where "MVOKBA v \<longleftrightarrow> (v \<in> MemVal) \<or> (v = OK) \<or> (v = BadArg)"
41
42definition
43  MVNROKBA      :: "Vals \<Rightarrow> bool"
44  where "MVNROKBA v \<longleftrightarrow> (v \<in> MemVal) \<or> (v = NotAResult) \<or> (v = OK) \<or> (v = BadArg)"
45
46definition
47  (* tuples of state functions changed by the various components *)
48  e             :: "PrIds => (bit * memOp) stfun"
49  where "e p = PRED (caller memCh!p)"
50
51definition
52  c             :: "PrIds \<Rightarrow> (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
53  where "c p = PRED (cst!p, rtrner memCh!p, caller crCh!p)"
54
55definition
56  r             :: "PrIds \<Rightarrow> (rpcState * (bit * Vals) * (bit * memOp)) stfun"
57  where "r p = PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
58
59definition
60  m             :: "PrIds \<Rightarrow> ((bit * Vals) * Vals) stfun"
61  where "m p = PRED (rtrner rmCh!p, ires!p)"
62
63definition
64  (* the environment action *)
65  ENext         :: "PrIds \<Rightarrow> action"
66  where "ENext p = ACT (\<exists>l. #l \<in> #MemLoc \<and> Call memCh p #(read l))"
67
68
69definition
70  (* specification of the history variable *)
71  HInit         :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
72  where "HInit rmhist p = PRED rmhist!p = #histA"
73
74definition
75  HNext         :: "histType \<Rightarrow> PrIds \<Rightarrow> action"
76  where "HNext rmhist p = ACT (rmhist!p)$ =
77                     (if (MemReturn rmCh ires p \<or> RPCFail crCh rmCh rst p)
78                      then #histB
79                      else if (MClkReply memCh crCh cst p)
80                           then #histA
81                           else $(rmhist!p))"
82
83definition
84  HistP         :: "histType \<Rightarrow> PrIds \<Rightarrow> temporal"
85  where "HistP rmhist p = (TEMP Init HInit rmhist p
86                           \<and> \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
87
88definition
89  Hist          :: "histType \<Rightarrow> temporal"
90  where "Hist rmhist = TEMP (\<forall>p. HistP rmhist p)"
91
92definition
93  (* the implementation *)
94  IPImp          :: "PrIds \<Rightarrow> temporal"
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)))"
100
101definition
102  ImpInit        :: "PrIds \<Rightarrow> stpred"
103  where "ImpInit p = PRED (  \<not>Calling memCh p
104                          \<and> MClkInit crCh cst p
105                          \<and> RPCInit rmCh rst p
106                          \<and> PInit ires p)"
107
108definition
109  ImpNext        :: "PrIds \<Rightarrow> action"
110  where "ImpNext p = (ACT  [ENext p]_(e p)
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))"
114
115definition
116  ImpLive        :: "PrIds \<Rightarrow> temporal"
117  where "ImpLive p = (TEMP  WF(MClkFwd memCh crCh cst p)_(c p)
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))"
122
123definition
124  Implementation :: "temporal"
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))"
129
130definition
131  (* the predicate S describes the states of the implementation.
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
136     invariant MemInv, proved in Memory.thy. *)
137  S :: "histType \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> mClkState \<Rightarrow> rpcState \<Rightarrow> histState \<Rightarrow> histState \<Rightarrow> PrIds \<Rightarrow> stpred"
138  where "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p = (PRED
139                Calling memCh p = #ecalling
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>)"
151
152definition
153  (* predicates S1 -- S6 define special instances of S *)
154  S1            :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
155  where "S1 rmhist p = S rmhist False False False clkA rpcA histA histA p"
156
157definition
158  S2            :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
159  where "S2 rmhist p = S rmhist True False False clkA rpcA histA histA p"
160
161definition
162  S3            :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
163  where "S3 rmhist p = S rmhist True True False clkB rpcA histA histB p"
164
165definition
166  S4            :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
167  where "S4 rmhist p = S rmhist True True True clkB rpcB histA histB p"
168
169definition
170  S5            :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
171  where "S5 rmhist p = S rmhist True True False clkB rpcB histB histB p"
172
173definition
174  S6            :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
175  where "S6 rmhist p = S rmhist True False False clkB rpcA histB histB p"
176
177definition
178  (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
179  ImpInv         :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
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))"
182
183definition
184  resbar        :: "histType \<Rightarrow> resType"        (* refinement mapping *)
185  where"resbar rmhist s p =
186                  (if (S1 rmhist p s | S2 rmhist p s)
187                   then ires s p
188                   else if S3 rmhist p s
189                   then if rmhist s p = histA
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 *)
200
201axiomatization where
202  (* the "base" variables: everything except resbar and hist (for any index) *)
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
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
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.
213
214    Steps are (roughly) numbered as in the hand proof.
215*)
216
217(* --------------------------- automatic prover --------------------------- *)
218
219declare 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!!
224   (but it can be a lot faster than the default setup)
225*)
226ML \<open>
227  val config_fast_solver = Attrib.setup_config_bool \<^binding>\<open>fast_solver\<close> (K false);
228  val fast_solver = mk_solver "fast_solver" (fn ctxt =>
229    if Config.get ctxt config_fast_solver
230    then assume_tac ctxt ORELSE' (eresolve_tac ctxt [notE])
231    else K no_tac);
232\<close>
233
234setup \<open>map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver)\<close>
235
236ML \<open>val temp_elim = make_elim oo temp_use\<close>
237
238
239
240(****************************** The history variable ******************************)
241
242section "History variable"
243
244lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) \<and> \<box>(\<forall>p. ImpNext p)
245         \<longrightarrow> (\<exists>\<exists>rmhist. Init(\<forall>p. HInit rmhist p)
246                          \<and> \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
247  apply clarsimp
248  apply (rule historyI)
249      apply assumption+
250  apply (rule MI_base)
251  apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm HInit_def}]) [] [] 1\<close>)
252   apply (erule fun_cong)
253  apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm HNext_def}])
254    [@{thm busy_squareI}] [] 1\<close>)
255  apply (erule fun_cong)
256  done
257
258lemma History: "\<turnstile> Implementation \<longrightarrow> (\<exists>\<exists>rmhist. Hist rmhist)"
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
271section "The safety part"
272
273(* ------------------------- Include lower-level lemmas ------------------------- *)
274
275(* RPCFailure notin MemVals U {OK,BadArg} *)
276
277lemma MVOKBAnotRF: "MVOKBA x \<Longrightarrow> x \<noteq> RPCFailure"
278  apply (unfold MVOKBA_def)
279  apply auto
280  done
281
282(* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *)
283
284lemma MVOKBARFnotNR: "MVOKBARF x \<Longrightarrow> x \<noteq> NotAResult"
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 ---
297lemma S1_excl: "\<turnstile> S1 rmhist p \<longrightarrow> S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p &
298    \<not>S4 rmhist p & \<not>S5 rmhist p & \<not>S6 rmhist p"
299  by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
300*)
301
302lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p \<and> \<not>S1 rmhist p"
303  by (auto simp: S_def S1_def S2_def)
304
305lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p"
306  by (auto simp: S_def S1_def S2_def S3_def)
307
308lemma 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"
309  by (auto simp: S_def S1_def S2_def S3_def S4_def)
310
311lemma 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"
313  by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
314
315lemma 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"
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
322lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p"
323  by (auto simp: ENext_def ACall_def)
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
334lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
335         \<longrightarrow> (S2 rmhist p)$"
336  by (force simp: ENext_def ACall_def c_def r_def m_def
337    caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
338
339lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
340  using [[fast_solver]]
341  by (auto elim!: squareE [temp_use] dest!: MClkidle [temp_use] simp: S_def S1_def)
342
343lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (r p)"
344  using [[fast_solver]]
345  by (auto elim!: squareE [temp_use] dest!: RPCidle [temp_use] simp: S_def S1_def)
346
347lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (m p)"
348  using [[fast_solver]]
349  by (auto elim!: squareE [temp_use] dest!: Memoryidle [temp_use] simp: S_def S1_def)
350
351lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S1 rmhist p)
352         \<longrightarrow> unchanged (rmhist!p)"
353  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm HNext_def}, @{thm S_def},
354    @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
355    @{thm AReturn_def}]) [] [temp_use \<^context> @{thm squareE}] 1\<close>)
356
357
358(* ------------------------------ State S2 ---------------------------------------- *)
359
360lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (e p)"
361  by (auto dest!: Envbusy [temp_use] simp: S_def S2_def)
362
363lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p"
364  by (auto simp: MClkNext_def MClkRetry_def MClkReply_def S_def S2_def)
365
366lemma S2Forward: "\<turnstile> $(S2 rmhist p) \<and> MClkFwd memCh crCh cst p
367         \<and> unchanged (e p, r p, m p, rmhist!p)
368         \<longrightarrow> (S3 rmhist p)$"
369  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm MClkFwd_def},
370    @{thm ACall_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
371    @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
372
373lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
374  by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
375
376lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (m p)"
377  by (auto simp: S_def S2_def dest!: Memoryidle [temp_use])
378
379lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S2 rmhist p)
380         \<longrightarrow> unchanged (rmhist!p)"
381  using [[fast_solver]]
382  by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
383    MClkReply_def AReturn_def S_def S2_def)
384
385(* ------------------------------ State S3 ---------------------------------------- *)
386
387lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (e p)"
388  by (auto dest!: Envbusy [temp_use] simp: S_def S3_def)
389
390lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (c p)"
391  by (auto dest!: MClkbusy [temp_use] simp: square_def S_def S3_def)
392
393lemma S3LegalRcvArg: "\<turnstile> S3 rmhist p \<longrightarrow> IsLegalRcvArg<arg<crCh!p>>"
394  by (auto simp: IsLegalRcvArg_def MClkRelayArg_def S_def S3_def)
395
396lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S3 rmhist p)
397         \<longrightarrow> RPCFwd crCh rmCh rst p \<or> RPCFail crCh rmCh rst p"
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
403lemma 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)"
406  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm RPCFwd_def},
407    @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
408    @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ACall_def}, @{thm e_def},
409    @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
410    @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1\<close>)
411
412lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S3 rmhist p) \<and> HNext rmhist p
413         \<and> unchanged (e p, c p, m p)
414         \<longrightarrow> (S6 rmhist p)$"
415  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm HNext_def},
416    @{thm RPCFail_def}, @{thm AReturn_def}, @{thm e_def}, @{thm c_def},
417    @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
418    @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
419
420lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
421  by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
422
423lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
424  by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
425    AReturn_def r_def rtrner_def S_def S3_def Calling_def)
426
427(* ------------------------------ State S4 ---------------------------------------- *)
428
429lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (e p)"
430  by (auto simp: S_def S4_def dest!: Envbusy [temp_use])
431
432lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (c p)"
433  by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
434
435lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (r p)"
436  using [[fast_solver]]
437  by (auto elim!: squareE [temp_use] dest!: RPCbusy [temp_use] simp: S_def S4_def)
438
439lemma 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)"
442  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm ReadInner_def},
443    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
444    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
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},
447    @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>)
448
449lemma 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)"
452  by (auto simp: Read_def dest!: S4ReadInner [temp_use])
453
454lemma 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)"
456  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm WriteInner_def},
457    @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
458    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
459    @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
460    @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1\<close>)
461
462lemma 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)"
465  by (auto simp: Write_def dest!: S4WriteInner [temp_use])
466
467lemma WriteS4: "\<turnstile> $ImpInv rmhist p \<and> Write rmCh mm ires p l \<longrightarrow> $S4 rmhist p"
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
471lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
472         \<and> HNext rmhist p
473         \<longrightarrow> (S5 rmhist p)$"
474  by (auto simp: HNext_def MemReturn_def AReturn_def e_def c_def r_def
475    rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
476
477lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
478  by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
479    AReturn_def m_def rtrner_def S_def S4_def Calling_def)
480
481(* ------------------------------ State S5 ---------------------------------------- *)
482
483lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (e p)"
484  by (auto simp: S_def S5_def dest!: Envbusy [temp_use])
485
486lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (c p)"
487  by (auto simp: S_def S5_def dest!: MClkbusy [temp_use])
488
489lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S5 rmhist p)
490         \<longrightarrow> RPCReply crCh rmCh rst p \<or> RPCFail crCh rmCh rst p"
491  by (auto simp: RPCNext_def RPCReject_def RPCFwd_def S_def S5_def)
492
493lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
494       \<longrightarrow> (S6 rmhist p)$"
495  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm RPCReply_def},
496    @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
497    @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
498    @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
499
500lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
501         \<longrightarrow> (S6 rmhist p)$"
502  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm RPCFail_def},
503    @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
504    @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
505    @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
506
507lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
508  by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
509
510lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> $(S5 rmhist p)
511         \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
512  using [[fast_solver]]
513  by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
514    MClkReply_def AReturn_def S_def S5_def)
515
516(* ------------------------------ State S6 ---------------------------------------- *)
517
518lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (e p)"
519  by (auto simp: S_def S6_def dest!: Envbusy [temp_use])
520
521lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S6 rmhist p)
522         \<longrightarrow> MClkRetry memCh crCh cst p \<or> MClkReply memCh crCh cst p"
523  by (auto simp: MClkNext_def MClkFwd_def S_def S6_def)
524
525lemma 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)"
528  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm HNext_def},
529    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm ACall_def}, @{thm AReturn_def},
530    @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
531    @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
532
533lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
534         \<and> unchanged (e p,r p,m p)
535         \<longrightarrow> (S1 rmhist p)$"
536  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm HNext_def},
537    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm AReturn_def}, @{thm MClkReply_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 S1_def}, @{thm Calling_def}]) [] [] 1\<close>)
540
541lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $S6 rmhist p \<longrightarrow> unchanged (r p)"
542  by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
543
544lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (m p)"
545  by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
546
547lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
548  by (auto simp: HNext_def MClkReply_def AReturn_def c_def rtrner_def S_def S6_def Calling_def)
549
550
551section "Correctness of predicate-action diagram"
552
553
554(* ========== Step 1.1 ================================================= *)
555(* The implementation's initial condition implies the state predicate S1 *)
556
557lemma Step1_1: "\<turnstile> ImpInit p \<and> HInit rmhist p \<longrightarrow> S1 rmhist p"
558  using [[fast_solver]]
559  by (auto elim!: squareE [temp_use] simp: MVNROKBA_def
560    MClkInit_def RPCInit_def PInit_def HInit_def ImpInit_def S_def S1_def)
561
562(* ========== Step 1.2 ================================================== *)
563(* Figure 16 is a predicate-action diagram for the implementation. *)
564
565lemma 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)"
568  apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm ImpNext_def}]) []
569      (map (temp_elim \<^context>)
570        [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1\<close>)
571   using [[fast_solver]]
572   apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
573  done
574
575lemma 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)"
579  apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm ImpNext_def}]) []
580    (map (temp_elim \<^context>)
581      [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1\<close>)
582   using [[fast_solver]]
583   apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
584  done
585
586lemma 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))"
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> []
593    (@{thm squareE} ::
594      map (temp_elim \<^context>) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1\<close>)
595   apply (auto dest!: S3Hist [temp_use])
596  done
597
598lemma 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))"
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}]) []
607    (@{thm squareE} ::
608      map (temp_elim \<^context>) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1\<close>)
609  apply (auto dest!: S4Hist [temp_use])
610  done
611
612lemma 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))"
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>)
619   using [[fast_solver]]
620   apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
621  done
622
623lemma 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))"
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>)
631     apply (auto dest: S6Hist [temp_use])
632  done
633
634(* --------------------------------------------------------------------------
635   Step 1.3: S1 implies the barred initial condition.
636*)
637
638section "Initialization (Step 1.3)"
639
640lemma Step1_3: "\<turnstile> S1 rmhist p \<longrightarrow> PInit (resbar rmhist) p"
641  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm resbar_def},
642    @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1\<close>)
643
644(* ----------------------------------------------------------------------
645   Step 1.4: Implementation's next-state relation simulates specification's
646             next-state relation (with appropriate substitutions)
647*)
648
649section "Step simulation (Step 1.4)"
650
651lemma Step1_4_1: "\<turnstile> ENext p \<and> $S1 rmhist p \<and> (S2 rmhist p)$ \<and> unchanged (c p, r p, m p)
652         \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
653  using [[fast_solver]]
654  by (auto elim!: squareE [temp_use] simp: c_def r_def m_def resbar_def)
655
656lemma 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)
658         \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
659  by (tactic \<open>action_simp_tac
660    (\<^context> addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
661    @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1\<close>)
662
663lemma 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)
665         \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
666  apply clarsimp
667  apply (drule S3_excl [temp_use] S4_excl [temp_use])+
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>)
670  done
671
672lemma 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)
674         \<longrightarrow> MemFail memCh (resbar rmhist) p"
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)
679   apply (auto simp: AReturn_def)
680  done
681
682lemma 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
684         \<longrightarrow> ReadInner memCh mm (resbar rmhist) p l"
685  apply clarsimp
686  apply (drule S4_excl [temp_use])+
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>)
689     apply (auto simp: resbar_def)
690       apply (tactic \<open>ALLGOALS (action_simp_tac
691                (\<^context> addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
692                  @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
693                [] [@{thm impE}, @{thm MemValNotAResultE}])\<close>)
694  done
695
696lemma 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))
698         \<longrightarrow> Read memCh mm (resbar rmhist) p"
699  by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
700
701lemma 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)
703         \<longrightarrow> WriteInner memCh mm (resbar rmhist) p l v"
704  apply clarsimp
705  apply (drule S4_excl [temp_use])+
706  apply (tactic \<open>action_simp_tac (\<^context> addsimps
707    [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
708    @{thm c_def}, @{thm m_def}]) [] [] 1\<close>)
709     apply (auto simp: resbar_def)
710    apply (tactic \<open>ALLGOALS (action_simp_tac (\<^context> addsimps
711      [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
712      @{thm S4_def}, @{thm WrRequest_def}]) [] [])\<close>)
713  done
714
715lemma 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)
717         \<longrightarrow> Write memCh mm (resbar rmhist) p l"
718  by (force simp: Write_def elim!: Step1_4_4b1 [temp_use])
719
720lemma 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)
722         \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
723  apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm e_def},
724    @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>)
725  apply (drule S4_excl [temp_use] S5_excl [temp_use])+
726  using [[fast_solver]]
727  apply (auto elim!: squareE [temp_use] simp: MemReturn_def AReturn_def)
728  done
729
730lemma 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)
732         \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
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)
736   apply (auto simp: RPCReply_def AReturn_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
737  done
738
739lemma 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)
741         \<longrightarrow> MemFail memCh (resbar rmhist) p"
742  apply clarsimp
743  apply (drule S6_excl [temp_use])
744  apply (auto simp: e_def c_def m_def RPCFail_def AReturn_def MemFail_def resbar_def)
745   apply (auto simp: S5_def S_def)
746  done
747
748lemma 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)
750         \<longrightarrow> MemReturn memCh (resbar rmhist) p"
751  apply clarsimp
752  apply (drule S6_excl [temp_use])+
753  apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm e_def},
754    @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
755    @{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\<close>)
756    apply simp_all (* simplify if-then-else *)
757    apply (tactic \<open>ALLGOALS (action_simp_tac (\<^context> addsimps
758      [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>)
759  done
760
761lemma 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)
763         \<longrightarrow> MemFail memCh (resbar rmhist) p"
764  apply clarsimp
765  apply (drule S3_excl [temp_use])+
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>)
768   apply (auto simp: S6_def S_def)
769  done
770
771lemma 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)"
773  by (auto simp: e_def c_def r_def m_def caller_def rtrner_def S_def Calling_def)
774
775lemma 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,
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
784lemma 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,
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*)
797ML \<open>
798fun split_idle_tac ctxt =
799  SELECT_GOAL
800   (TRY (resolve_tac ctxt @{thms actionI} 1) THEN
801    Induct_Tacs.case_tac ctxt "(s,t) \<Turnstile> unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN
802    rewrite_goals_tac ctxt @{thms action_rews} THEN
803    forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
804    asm_full_simp_tac ctxt 1);
805\<close>
806
807method_setup split_idle = \<open>
808  Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers)
809    >> (K (SIMPLE_METHOD' o split_idle_tac))
810\<close>
811
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. *)
819lemma 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)"
822  apply (split_idle simp: square_def)
823  apply force
824  done
825(* turn into (unsafe, looping!) introduction rule *)
826lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
827
828lemma S1safe: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
829         \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
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
836lemma S2safe: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
837         \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
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
844lemma S3safe: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
845         \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
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
852lemma 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))
854         \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
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
862lemma S5safe: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
863         \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
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
870lemma S6safe: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
871         \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
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
883section "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
892lemma 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)$"
894  apply split_idle
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
902lemma S1_RNextdisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
903         \<not>Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
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>)
906  apply force
907  done
908
909lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
910         \<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
911  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm angle_def}, @{thm MemReturn_def},
912    @{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
913
914lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
915         \<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
916  by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use]
917    elim!: STL4E [temp_use] DmdImplE [temp_use])
918
919lemma Return_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
920         \<longrightarrow> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
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
926lemma 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)$"
928  apply split_idle
929  apply (auto dest!: Step1_2_2 [temp_use])
930  done
931
932lemma 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)
934         \<longrightarrow> (S3 rmhist p)$"
935  by (auto simp: angle_def dest!: Step1_2_2 [temp_use])
936
937lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
938         \<longrightarrow> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
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
945lemma 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)
947         \<longrightarrow> (S2 rmhist p \<leadsto> S3 rmhist p)"
948  by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
949
950(* ------------------------------ State S3 ------------------------------ *)
951
952lemma 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)$"
954  apply split_idle
955  apply (auto dest!: Step1_2_3 [temp_use])
956  done
957
958lemma 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)$"
961  apply (auto simp: angle_def dest!: Step1_2_3 [temp_use])
962  done
963
964lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
965         \<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
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
972lemma 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)"
975  by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
976
977(* ------------- State S4 -------------------------------------------------- *)
978
979lemma 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)$"
982  apply split_idle
983  apply (auto dest!: Step1_2_4 [temp_use])
984  done
985
986(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
987
988lemma 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)$"
992  apply split_idle
993  apply (auto dest!: Step1_2_4 [temp_use])
994  done
995
996lemma 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)$"
1000  by (auto simp: angle_def
1001    dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
1002
1003lemma 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)
1005         \<longrightarrow> $Enabled (<RNext rmCh mm ires p>_(m p))"
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
1012lemma 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)"
1016  by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
1017
1018(* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
1019
1020lemma 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)$"
1023  apply (split_idle simp: m_def)
1024  apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
1025  done
1026
1027lemma 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)
1030         \<longrightarrow> (S5 rmhist p)$"
1031  by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
1032
1033lemma 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)
1036         \<longrightarrow> $Enabled (<MemReturn rmCh ires p>_(m p))"
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
1043lemma 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)"
1046  by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
1047
1048(* ------------------------------ State S5 ------------------------------ *)
1049
1050lemma 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)$"
1052  apply split_idle
1053  apply (auto dest!: Step1_2_5 [temp_use])
1054  done
1055
1056lemma 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)
1058         \<longrightarrow> (S6 rmhist p)$"
1059  by (auto simp: angle_def dest!: Step1_2_5 [temp_use])
1060
1061lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
1062         \<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
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
1069lemma 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)
1071         \<longrightarrow> (S5 rmhist p \<leadsto> S6 rmhist p)"
1072  by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
1073
1074(* ------------------------------ State S6 ------------------------------ *)
1075
1076lemma 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)$"
1078  apply split_idle
1079  apply (auto dest!: Step1_2_6 [temp_use])
1080  done
1081
1082lemma S6MClkReply_successors:
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)
1085         \<longrightarrow> (S1 rmhist p)$"
1086  by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use])
1087
1088lemma MClkReplyS6:
1089  "\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
1090  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm angle_def},
1091    @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ImpInv_def}, @{thm S_def},
1092    @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>)
1093
1094lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"
1095  apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
1096     apply (cut_tac MI_base)
1097     apply (blast dest: base_pair)
1098    apply (tactic \<open>ALLGOALS (action_simp_tac (\<^context>
1099      addsimps [@{thm S_def}, @{thm S6_def}]) [] [])\<close>)
1100  done
1101
1102lemma 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)
1104         \<longrightarrow> \<box>\<diamond>(S1 rmhist p)"
1105  apply clarsimp
1106  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
1107   apply (erule InfiniteEnsures)
1108    apply assumption
1109   apply (tactic \<open>action_simp_tac \<^context> []
1110     (map (temp_elim \<^context>) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1\<close>)
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
1118lemma S5S6LeadstoS6: "sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p
1119      \<Longrightarrow> sigma \<Turnstile> (S5 rmhist p \<or> S6 rmhist p) \<leadsto> S6 rmhist p"
1120  by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
1121
1122lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
1123         sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
1124      \<Longrightarrow> sigma \<Turnstile> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p
1125                    \<leadsto> S6 rmhist p"
1126  by (auto intro!: LatticeDisjunctionIntro [temp_use]
1127    S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
1128
1129lemma 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;
1132         sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
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
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
1147lemma 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;
1151         sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
1152      \<Longrightarrow> sigma \<Turnstile> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p"
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
1160lemma S2S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p;
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;
1165         sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
1166      \<Longrightarrow> sigma \<Turnstile> S2 rmhist p \<or> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p
1167                   \<leadsto> S6 rmhist p"
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
1176lemma NotS1LeadstoS6: "\<lbrakk> sigma \<Turnstile> \<box>ImpInv rmhist p;
1177         sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p;
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;
1182         sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
1183      \<Longrightarrow> sigma \<Turnstile> \<not>S1 rmhist p \<leadsto> S6 rmhist p"
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
1192lemma 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"
1195  apply (rule classical)
1196  apply (tactic \<open>asm_lr_simp_tac (\<^context> addsimps
1197    [temp_use \<^context> @{thm NotBox}, temp_rewrite \<^context> @{thm NotDmd}]) 1\<close>)
1198  apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
1199  done
1200
1201section "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*)
1207lemma Step1_5_1a: "\<turnstile> IPImp p \<longrightarrow> (\<forall>l. \<box>$MemInv mm l)"
1208  by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
1209
1210lemma 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)
1212         \<longrightarrow> \<box>ImpInv rmhist p"
1213  apply invariant
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 ***)
1221lemma Step1_5_2a: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<longrightarrow> Init(PInit (resbar rmhist) p)"
1222  by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3  [temp_use])
1223
1224(*** step simulation ***)
1225lemma 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))
1227         \<longrightarrow> \<box>[UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
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 ***)
1233lemma 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"
1238  apply clarsimp
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)")
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... *)
1254lemma 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
1257         \<longrightarrow> \<box>\<diamond>S1 rmhist p"
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 *)
1267lemma 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
1269         \<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
1270  by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
1271
1272lemma 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
1274         \<longrightarrow> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
1275  by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
1276
1277(* QED step of step 1 *)
1278lemma Step1: "\<turnstile> IPImp p \<and> HistP rmhist p \<longrightarrow> UPSpec memCh mm (resbar rmhist) p"
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 ------------------------------ *)
1284section "Step 2"
1285
1286lemma 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)"
1290  apply clarsimp
1291  apply (drule WriteS4 [action_use])
1292   apply assumption
1293  apply split_idle
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
1299lemma Step2_2: "\<turnstile>   (\<forall>p. ImpNext p)
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)
1303         \<longrightarrow> [\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
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
1310lemma Step2_lemma: "\<turnstile> \<box>(  (\<forall>p. ImpNext p)
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))
1314         \<longrightarrow> \<box>[\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
1315  by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
1316
1317lemma Step2: "\<turnstile> #l \<in> #MemLoc \<and> (\<forall>p. IPImp p \<and> HistP rmhist p)
1318         \<longrightarrow> MSpec memCh mm (resbar rmhist) l"
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 --------------------------------- *)
1328section "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*)
1337lemma Impl_IUSpec: "\<turnstile> Implementation \<and> Hist rmhist \<longrightarrow> IUSpec memCh mm (resbar rmhist)"
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. *)
1342lemma Implementation: "\<turnstile> Implementation \<longrightarrow> USpec memCh"
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
1348
1349end
1350