theory CNodeInv_R

lemma cteMove_valid_pspace' [wp]:
  "\<lbrace>\<lambda>x. valid_pspace' x \<and>
            cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 x \<and>
            cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 x \<and>
            cte_wp_at' (\<lambda>c. cteCap c \<noteq> NullCap) word1 x \<and>
            x \<turnstile>' capability \<and>
            cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 x\<rbrace>
  cteMove capability word1 word2
  \<lbrace>\<lambda>y. valid_pspace'\<rbrace>" unfolding cteMove_def apply (simp add: pred_conj_def valid_pspace'_def valid_mdb'_def) apply (wp sch_act_wf_lift valid_queues_lift
    cur_tcb_lift updateCap_no_0  updateCap_ctes_of_wp getCTE_wp | simp)+ apply (clarsimp simp: invs'_def valid_state'_def)+ apply (clarsimp dest!: cte_at_cte_wp_atD) apply (rule_tac x = cte in exI) apply clarsimp apply (clarsimp dest!: cte_at_cte_wp_atD) apply (rule_tac x = ctea in exI) apply (clarsimp simp: isCap_simps) apply rule apply (clarsimp elim!: valid_mdb_ctesE) apply (case_tac ctea) apply (case_tac cte) apply (rule_tac old_dest_node = "cteMDBNode cte" and src_cap = "cteCap ctea" in
    mdb_move.cteMove_valid_mdb_helper) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of weak_derived'_def isCap_simps simp del: not_ex) apply unfold_locales apply (simp_all add: valid_mdb'_def cte_wp_at_ctes_of nullPointer_def weak_derived'_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. valid_pspace' x \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 x \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 x \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 x \<and> valid_cap' capability x \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 x\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>y. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. valid_pspace' x \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 x \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 x \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 x \<and> valid_cap' capability x \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 x\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>y. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. valid_objs' x \<and> pspace_aligned' x \<and> pspace_distinct' x \<and> no_0_obj' x \<and> valid_mdb_ctes (ctes_of x) \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 x \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 x \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 x \<and> valid_cap' capability x \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 x\<rbrace> do oldCTE <- getCTE word2;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
cte <- getCTE word1;
y <- updateCap word2 capability;
y <- updateCap word1 capability.NullCap;
y <- updateMDB word2 (const (cteMDBNode cte));
y <- updateMDB word1 (const nullMDBNode);
y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>y x. valid_objs' x \<and> pspace_aligned' x \<and> pspace_distinct' x \<and> no_0_obj' x \<and> valid_mdb_ctes (ctes_of x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s \<and> valid_cap' capability s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) word2 s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) word2 s \<and> (cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' (\<lambda>_. True) word1 s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) word1 s \<and> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' (\<lambda>_. True) word2 s\<rbrakk> \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) word2 s \<and> (cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' (\<lambda>_. True) word1 s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) word1 s \<and> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s\<rbrakk> \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) word2 s \<and> (cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' (\<lambda>_. True) word1 s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) word1 s \<and> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) cte) word2 s \<and> (cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' (\<lambda>_. True) word1 s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) word1 s \<and> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' (\<lambda>_. True) word1 s\<rbrakk> \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) word1 s \<and> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s\<rbrakk> \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) word1 s \<and> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) ctea) word1 s \<and> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode ctea))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode ctea)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode ctea))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode ctea)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s\<rbrakk> \<Longrightarrow> no_0 (ctes_of s)
 2. \<And>s cte ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode ctea))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode ctea)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode ctea))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode ctea)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x1 x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode ctea))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode ctea)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) word2 (cteCap_update (\<lambda>_. capability))) word1 (cteCap_update (\<lambda>_. capability.NullCap))) word2 (cteMDBNode_update (\<lambda>a. cteMDBNode ctea))) word1 (cteMDBNode_update (\<lambda>a. nullMDBNode))) (mdbPrev (cteMDBNode ctea)) (cteMDBNode_update (mdbNext_update (\<lambda>_. word2)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. word2)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_move (ctes_of s) word1 (cteCap ctea) (cteMDBNode ctea) word2 capability (cteMDBNode cte)
 2. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a; isUntypedCap capability\<rbrakk> \<Longrightarrow> capability = cteCap ctea proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a; isUntypedCap capability\<rbrakk> \<Longrightarrow> capability = cteCap ctea
 2. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_move (ctes_of s) word1 (cteCap ctea) (cteMDBNode ctea) word2 capability (cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_move (ctes_of s) word1 (cteCap ctea) (cteMDBNode ctea) word2 capability (cteMDBNode cte) proof (prove)
goal (8 subgoals):
 1. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of s)
 2. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> ctes_of s word1 = Some (CTE (cteCap ctea) (cteMDBNode ctea))
 3. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> ctes_of s word2 = Some (CTE capability.NullCap (cteMDBNode cte))
 4. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) = 0
 5. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0
 6. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> weak_derived' (cteCap ctea) capability
 7. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> cteCap ctea \<noteq> capability.NullCap
 8. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s; cte_wp_at' (\<lambda>c. (\<exists>d v0 v1 f. cteCap c = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = cteCap c) word1 s; cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s; valid_cap' capability s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s; cte_wp_at' ((=) cte) word2 s; cteCap cte = capability.NullCap; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; cte_wp_at' ((=) ctea) word1 s; ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> word1 \<noteq> word2 proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); capMasterCap x1 = capMasterCap capability \<and> capBadge x1 = capBadge capability \<and> capASID x1 = capASID capability \<and> cap_asid_base' x1 = cap_asid_base' capability \<and> cap_vptr' x1 = cap_vptr' capability \<and> (isReplyCap x1 \<longrightarrow> capTCBPtr x1 = capTCBPtr capability \<and> capReplyMaster x1 = capReplyMaster capability); (\<exists>d v0 v1 f. x1 = capability.UntypedCap d v0 v1 f) \<longrightarrow> capability = x1; x1 \<noteq> capability.NullCap; valid_cap' capability s; ctes_of s word2 = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; mdbPrev x2a = 0; mdbNext x2a = 0; ctes_of s word1 = Some (CTE x1 x2); ctea = CTE x1 x2; cte = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> word1 \<noteq> word2 proof (prove)
goal:
No subgoals!