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