theory Finalise_R

lemma emptySlot_mdb [wp]:
  "\<lbrace>valid_mdb'\<rbrace>
  emptySlot sl opt
  \<lbrace>\<lambda>_. valid_mdb'\<rbrace>" unfolding emptySlot_def apply (simp only: case_Null_If valid_mdb'_def) apply (wp updateCap_ctes_of_wp getCTE_wp'
            opt_return_pres_lift | simp add: cte_wp_at_ctes_of)+ apply (clarsimp) apply (case_tac cte) apply (rename_tac cap node) apply (simp) apply (subgoal_tac "mdb_empty (ctes_of s) sl cap node") prefer 2 apply (rule mdb_empty.intro) apply (rule mdb_ptr.intro) apply (rule vmdb.intro) apply (simp add: valid_mdb_ctes_def) apply (rule mdb_ptr_axioms.intro) apply (simp add: cte_wp_at_ctes_of) apply (rule conjI, clarsimp simp: valid_mdb_ctes_def) apply (erule mdb_empty.vmdb_n[unfolded const_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb'\<rbrace> emptySlot sl opt \<lbrace>\<lambda>_. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb'\<rbrace> do clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
mdbNode <- return (cteMDBNode newCTE);
prev <- return (mdbPrev mdbNode);
next <- return (mdbNext mdbNode);
case cteCap newCTE of capability.NullCap \<Rightarrow> return () | _ \<Rightarrow> do updateMDB prev (mdbNext_update (\<lambda>_. next));
updateMDB next (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged mdbNode) (mdbPrev_update (\<lambda>_. prev) mdb));
updateCap sl capability.NullCap;
updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>_. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb_ctes (ctes_of s)\<rbrace> do clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
mdbNode <- return (cteMDBNode newCTE);
prev <- return (mdbPrev mdbNode);
next <- return (mdbNext mdbNode);
if cteCap newCTE = capability.NullCap then return () else do updateMDB prev (mdbNext_update (\<lambda>_. next));
updateMDB next (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged mdbNode) (mdbPrev_update (\<lambda>_. prev) mdb));
updateCap sl capability.NullCap;
updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>_ s. valid_mdb_ctes (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_mdb_ctes (ctes_of s) \<Longrightarrow> \<forall>cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.NullCap \<longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode cte))))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode cte)) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some cte; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode cte))))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode cte)) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some cte; cteCap cte \<noteq> capability.NullCap; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode cte))))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode cte)) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some cte; cteCap cte \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode cte))))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode cte)) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode)))
 2. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> mdb_empty (ctes_of s) sl cap node proof (prove)
goal (2 subgoals):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> mdb_empty (ctes_of s) sl cap node
 2. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) sl cap node
 2. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> vmdb (ctes_of s)
 2. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> mdb_ptr_axioms (ctes_of s) sl cap node
 3. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of s)
 2. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> mdb_ptr_axioms (ctes_of s) sl cap node
 3. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> mdb_ptr_axioms (ctes_of s) sl cap node
 2. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node\<rbrakk> \<Longrightarrow> ctes_of s sl = Some (CTE cap node)
 2. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> no_0 (ctes_of s) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cap node. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s sl = Some (CTE cap node); cap \<noteq> capability.NullCap; cte = CTE cap node; mdb_empty (ctes_of s) sl cap node\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) (mdbPrev node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) (mdbNext node) (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged a \<or> mdbFirstBadged node) (mdbPrev_update (\<lambda>_. mdbPrev node) a)))) sl (cteCap_update (\<lambda>_. capability.NullCap))) sl (cteMDBNode_update (\<lambda>a. nullMDBNode))) proof (prove)
goal:
No subgoals!