theory Finalise_R

lemma emptySlot_iflive'[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace>
     emptySlot sl opt
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: emptySlot_def case_Null_If if_live_then_nonz_cap'_def2
              del: comp_apply) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
             getCTE_wp opt_return_pres_lift
             clearUntypedFreeIndex_ctes_of
             clearUntypedFreeIndex_cteCaps_of
             hoare_vcg_ex_lift
             | wp (once) hoare_vcg_imp_lift
             | simp add: cte_wp_at_ctes_of del: comp_apply)+ apply (clarsimp simp: modify_map_same
    imp_conjR[symmetric]) apply (drule spec, drule(1) mp) apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def split: if_split_asm) apply (case_tac "p \<noteq> sl") apply blast apply (simp add: removeable'_def cteCaps_of_def) apply (erule disjE) apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def
                  dest!: capMaster_same_refs) apply fastforce apply clarsimp apply (drule(1) bspec) apply (clarsimp simp: ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>p zr. (map_option zobj_refs' \<circ> cteCaps_of s) p = Some zr \<and> ptr \<in> zr)) \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace> do y <- clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv s. \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>p zr. (map_option zobj_refs' \<circ> cteCaps_of s) p = Some zr \<and> ptr \<in> zr)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do y <- clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv s. \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>p zr. (map_option zobj_refs' \<circ> cteCaps_of s) p = Some zr \<and> ptr \<in> zr)\<rbrace>
 2. \<And>s. (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>p zr. (map_option zobj_refs' \<circ> cteCaps_of s) p = Some zr \<and> ptr \<in> zr)) \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>p zr. (map_option zobj_refs' \<circ> cteCaps_of s) p = Some zr \<and> ptr \<in> zr)) \<and> (\<exists>cte. ctes_of s sl = Some cte \<and> removeable' sl s (cteCap cte)) \<Longrightarrow> ctes_of s sl = None \<or> (\<forall>x. \<exists>xa. ctes_of s sl = Some xa \<and> (ko_wp_at' live' x s \<longrightarrow> cteCap xa = capability.NullCap \<or> (\<exists>xa xb. (map_option zobj_refs' \<circ> modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap)) xa = Some xb \<and> x \<in> xb))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>p zr. (\<exists>z. cteCaps_of s p = Some z \<and> zobj_refs' z = zr) \<and> ptr \<in> zr); removeable' sl s (cteCap cte); ctes_of s sl = Some cte; ko_wp_at' live' x s; \<forall>xa xb. (\<forall>z. modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) xa = Some z \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>removeable' sl s (cteCap cte); ctes_of s sl = Some cte; ko_wp_at' live' x s; \<forall>xa xb. (\<forall>z. modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) xa = Some z \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb; \<exists>p zr. (\<exists>z. cteCaps_of s p = Some z \<and> zobj_refs' z = zr) \<and> x \<in> zr\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. cteCaps_of s xa = Some z \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); removeable' sl s (cteCap cte); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCaps_of s p = Some z\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap proof (prove)
goal (2 subgoals):
 1. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. cteCaps_of s xa = Some z \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); removeable' sl s (cteCap cte); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCaps_of s p = Some z; p \<noteq> sl\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap
 2. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. cteCaps_of s xa = Some z \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); removeable' sl s (cteCap cte); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCaps_of s p = Some z; \<not> p \<noteq> sl\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. cteCaps_of s xa = Some z \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); removeable' sl s (cteCap cte); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCaps_of s p = Some z; \<not> p \<noteq> sl\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. (\<exists>za. ctes_of s xa = Some za \<and> cteCap za = z) \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); (\<exists>p. p \<noteq> sl \<and> cte_wp_at' (\<lambda>cte. capMasterCap (cteCap cte) = capMasterCap z) p s) \<or> (\<forall>p\<in>cte_refs' z (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' z. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs z. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCap cte = z; p = sl\<rbrakk> \<Longrightarrow> z = capability.NullCap proof (prove)
goal (2 subgoals):
 1. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. (\<exists>za. ctes_of s xa = Some za \<and> cteCap za = z) \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCap cte = z; p = sl; \<exists>p. p \<noteq> sl \<and> cte_wp_at' (\<lambda>cte. capMasterCap (cteCap cte) = capMasterCap z) p s\<rbrakk> \<Longrightarrow> z = capability.NullCap
 2. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. (\<exists>za. ctes_of s xa = Some za \<and> cteCap za = z) \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCap cte = z; p = sl; (\<forall>p\<in>cte_refs' z (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' z. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs z. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> z = capability.NullCap proof (prove)
goal (2 subgoals):
 1. \<And>s cte x pa ctea. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. (\<exists>za. ctes_of s xa = Some za \<and> cteCap za = z) \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' (cteCap cte); pa \<noteq> sl; ctes_of s pa = Some ctea; cte_refs' (cteCap ctea) = cte_refs' (cteCap cte); zobj_refs' (cteCap ctea) = zobj_refs' (cteCap cte)\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap
 2. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. (\<exists>za. ctes_of s xa = Some za \<and> cteCap za = z) \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCap cte = z; p = sl; (\<forall>p\<in>cte_refs' z (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' z. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs z. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> z = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s cte x p z. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. (\<exists>za. ctes_of s xa = Some za \<and> cteCap za = z) \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' z; cteCap cte = z; p = sl; (\<forall>p\<in>cte_refs' z (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' z. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs z. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> z = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. (\<exists>za. ctes_of s xa = Some za \<and> cteCap za = z) \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' (cteCap cte); \<forall>p\<in>cte_refs' (cteCap cte) (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s; \<forall>p\<in>zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p s; \<forall>t\<in>threadCapRefs (cteCap cte). \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>\<forall>xa. xa = sl \<or> (\<forall>xb. (\<forall>z. (\<exists>za. ctes_of s xa = Some za \<and> cteCap za = z) \<longrightarrow> zobj_refs' z \<noteq> xb) \<or> x \<notin> xb); ctes_of s sl = Some cte; ko_wp_at' live' x s; x \<in> zobj_refs' (cteCap cte); \<forall>p\<in>cte_refs' (cteCap cte) (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s; \<forall>t\<in>threadCapRefs (cteCap cte). \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); ko_wp_at' (Not \<circ> live') x s\<rbrakk> \<Longrightarrow> cteCap cte = capability.NullCap proof (prove)
goal:
No subgoals!