theory CNode_AC

lemma empty_slot_integrity_transferable[wp_transferable]:
  "\<lbrace>integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag
                       and cdt_change_allowed' aag slot and K (c = NullCap)\<rbrace>
   empty_slot slot c
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply integrity_trans_start apply (rule hoare_pre) apply (simp add: empty_slot_def) apply (simp add: empty_slot_shuffle[simplified]) apply (simp add: set_cdt_def) apply (wp set_original_wp) apply (rename_tac cdtv x) apply (rule_tac Q = "\<lambda>_ s'. integrity aag X s s'\<and> cdtv = cdt s \<and>
                            is_original_cap s = is_original_cap s'"
                       in hoare_post_imp) apply (clarsimp simp add: integrity_def) apply (frule all_childrenD[OF cdt_change_allowed_all_children];fastforce) apply (wp empty_slot_extended_list_integ_lift) apply (rule hoare_pre) apply (rule_tac m = "cdt s" in empty_slot_list_integrity) apply simp apply wp+ apply (wp set_cap_integrity_deletion gets_wp get_cap_wp)+ by (fastforce intro: cdt_change_allowed_all_children)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and cdt_change_allowed' aag slot and K (c = NullCap)\<rbrace> empty_slot slot c \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> empty_slot slot c \<lbrace>\<lambda>_. integrity aag X s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> empty_slot slot c \<lbrace>\<lambda>_. integrity aag X s\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- set_cap NullCap slot;
post_cap_deletion NullCap
od
od \<lbrace>\<lambda>_. integrity aag X s\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cap NullCap slot;
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
post_cap_deletion NullCap
od
od \<lbrace>\<lambda>_. integrity aag X s\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cap NullCap slot;
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- do s <- get;
put (s\<lparr>cdt := (\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)\<rparr>)
od;
post_cap_deletion NullCap
od
od \<lbrace>\<lambda>_. integrity aag X s\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s cap slot_p cdt x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 s cap slot_p cdt x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>y sa. (integrity aag X s and K (cleanup_info_wf NullCap aag)) (sa\<lparr>is_original_cap := (is_original_cap sa)(slot := False), cdt := (\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)\<rparr>)\<rbrace>
 2. \<And>s cap slot_p cdt. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdt\<rbrace> set_cap NullCap slot \<lbrace>?B15 s cap slot_p cdt\<rbrace>
 3. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 4. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 5. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 6. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>y sa. (integrity aag X s and K (cleanup_info_wf NullCap aag)) (sa\<lparr>is_original_cap := (is_original_cap sa)(slot := False), cdt := (\<lambda>p. if cdtv p = Some slot then cdtv slot else cdtv p)(slot := None)\<rparr>)\<rbrace>
 2. \<And>s cap slot_p cdt. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdt\<rbrace> set_cap NullCap slot \<lbrace>?B15 s cap slot_p cdt\<rbrace>
 3. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 4. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 5. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 6. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s cap slot_p cdtv x rv sa. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap; integrity aag X s sa \<and> cdtv = cdt s \<and> is_original_cap s = is_original_cap sa\<rbrakk> \<Longrightarrow> (integrity aag X s and K (cleanup_info_wf NullCap aag)) (sa\<lparr>is_original_cap := (is_original_cap sa)(slot := False), cdt := (\<lambda>p. if cdtv p = Some slot then cdtv slot else cdtv p)(slot := None)\<rparr>)
 2. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_ s'. integrity aag X s s' \<and> cdtv = cdt s \<and> is_original_cap s = is_original_cap s'\<rbrace>
 3. \<And>s cap slot_p cdt. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdt\<rbrace> set_cap NullCap slot \<lbrace>?B15 s cap slot_p cdt\<rbrace>
 4. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 5. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 6. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 7. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s cap sa a b. \<lbrakk>cap \<noteq> NullCap; valid_list s; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s sa; valid_objs s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x); valid_mdb s; \<forall>a b. cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (cdt s (a, b), is_original_cap sa (a, b)) (cdt sa (a, b), is_original_cap sa (a, b)); pas_refined aag s; \<forall>a b. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (cdt_list s (a, b)) (cdt_list sa (a, b)); cdt_change_allowed' aag slot s; c = NullCap; \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues sa d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a s sa; is_original_cap s = is_original_cap sa; cdt s (a, b) = Some slot; (a, b) \<noteq> slot\<rbrakk> \<Longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap sa (a, b)) (cdt s slot, is_original_cap sa (a, b))
 2. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_ s'. integrity aag X s s' \<and> cdtv = cdt s \<and> is_original_cap s = is_original_cap s'\<rbrace>
 3. \<And>s cap slot_p cdt. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdt\<rbrace> set_cap NullCap slot \<lbrace>?B15 s cap slot_p cdt\<rbrace>
 4. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 5. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 6. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 7. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_ s'. integrity aag X s s' \<and> cdtv = cdt s \<and> is_original_cap s = is_original_cap s'\<rbrace>
 2. \<And>s cap slot_p cdt. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdt\<rbrace> set_cap NullCap slot \<lbrace>?B15 s cap slot_p cdt\<rbrace>
 3. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 4. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 5. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 6. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (9 subgoals):
 1. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) s and ?Q82 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) s\<rbrace>
 2. \<And>s cap slot_p cdtv x P. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>
 3. \<And>s cap slot_p cdtv x P. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>
 4. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'81 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv sa. cdtv = cdt s \<and> is_original_cap s = is_original_cap sa\<rbrace>
 5. \<And>s cap slot_p cdt. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdt\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>x sa. (integrity aag X s and ?Q82 s cap slot_p cdt x) sa \<and> ?P'81 s cap slot_p cdt x sa\<rbrace>
 6. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 7. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 8. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 9. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (10 subgoals):
 1. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q84 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) s\<rbrace>
 2. \<And>s cap slot_p cdtv x sa. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap; (list_integ (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) s and ?Q82 s cap slot_p cdtv x) sa\<rbrakk> \<Longrightarrow> ?Q84 s cap slot_p cdtv x sa
 3. \<And>s cap slot_p cdtv x P. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>
 4. \<And>s cap slot_p cdtv x P. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>
 5. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'81 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv sa. cdtv = cdt s \<and> is_original_cap s = is_original_cap sa\<rbrace>
 6. \<And>s cap slot_p cdt. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdt\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>x sa. (integrity aag X s and ?Q82 s cap slot_p cdt x) sa \<and> ?P'81 s cap slot_p cdt x sa\<rbrace>
 7. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 8. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 9. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 10. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (9 subgoals):
 1. \<And>s cap slot_p cdtv x sa. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap; (list_integ (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) s and ?Q82 s cap slot_p cdtv x) sa\<rbrakk> \<Longrightarrow> (list_integ (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) s and (\<lambda>sa. valid_list_2 (cdt_list sa) (cdt s)) and K (cdt_change_allowed' aag slot s) and K (all_children (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt s))) sa
 2. \<And>s cap slot_p cdtv x P. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>
 3. \<And>s cap slot_p cdtv x P. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>
 4. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'81 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv sa. cdtv = cdt s \<and> is_original_cap s = is_original_cap sa\<rbrace>
 5. \<And>s cap slot_p cdt. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdt\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>x sa. (integrity aag X s and ?Q82 s cap slot_p cdt x) sa \<and> ?P'81 s cap slot_p cdt x sa\<rbrace>
 6. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 7. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 8. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 9. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (8 subgoals):
 1. \<And>s cap slot_p cdtv x P. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>
 2. \<And>s cap slot_p cdtv x P. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>
 3. \<And>s cap slot_p cdtv x. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'81 s cap slot_p cdtv x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv sa. cdtv = cdt s \<and> is_original_cap s = is_original_cap sa\<rbrace>
 4. \<And>s cap slot_p cdta. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdta\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>x sa. (integrity aag X s and (\<lambda>a. valid_list_2 (cdt_list a) (cdt s) \<and> all_children (\<lambda>a. cdt_change_allowed' aag a s) (cdt s))) sa \<and> ?P'81 s cap slot_p cdta x sa\<rbrace>
 5. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 6. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 7. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 8. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s cap slot_p cdta. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s cap slot_p cdta\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>x sa. integrity aag X s sa \<and> (valid_list_2 (cdt_list sa) (cdt s) \<and> all_children (\<lambda>a. cdt_change_allowed' aag a s) (cdt s)) \<and> cdta = cdt s \<and> is_original_cap s = is_original_cap sa\<rbrace>
 2. \<And>s cap slot_p. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s cap slot_p\<rbrace> gets cdt \<lbrace>?B14 s cap slot_p\<rbrace>
 3. \<And>s cap. \<lbrakk>valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R11 s cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B13 s cap\<rbrace>
 4. \<And>s. valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s \<and> c = NullCap \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> get_cap slot \<lbrace>\<lambda>cap sa. (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R11 s cap sa)\<rbrace>
 5. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and (cdt_change_allowed' aag slot and K (c = NullCap)))))) s; s = sa\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot sa \<longrightarrow> (cap = NullCap \<longrightarrow> integrity aag X s sa) \<and> (cap \<noteq> NullCap \<longrightarrow> (integrity aag X s and valid_mdb and valid_objs and pas_refined aag and cdt_change_allowed' aag slot) sa \<and> (valid_list_2 (cdt_list sa) (cdt s) \<and> all_children (\<lambda>a. cdt_change_allowed' aag a s) (cdt s)) \<and> cdt sa = cdt s \<and> is_original_cap s = is_original_cap sa)