theory PageTableDuplicates

lemma finaliseSlot_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s
    \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_to' slot s) \<rbrace>
  finaliseSlot slot exposed
  \<lbrace>\<lambda>_ s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<rbrace>" unfolding finaliseSlot_def apply (rule validE_valid, rule hoare_pre,
    rule hoare_post_impErr, rule use_spec) apply (rule finaliseSlot_invs'[where p=slot and slot=slot and Pr="vs_valid_duplicates' o ksPSpace"]) apply (simp_all add: valid_duplicates_finalise_prop_stuff) apply (wp | simp add: o_def)+ apply (auto dest: cte_wp_at_valid_objs_valid_cap') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot exposed \<lbrace>\<lambda>_ s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot' slot exposed \<lbrace>\<lambda>_ s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?Q2\<rbrace> finaliseSlot' slot exposed \<lbrace>?Q5\<rbrace>, \<lbrace>?E5\<rbrace>
 2. \<And>rv s. ?Q5 rv s \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s
 3. \<And>e s. ?E5 e s \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s
 4. \<And>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. \<And>s cap final sl. \<lbrace>no_cte_prop (vs_valid_duplicates' \<circ> ksPSpace) and invs' and sch_act_simple and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> global.finaliseCap cap final False \<lbrace>\<lambda>rv. no_cte_prop (vs_valid_duplicates' \<circ> ksPSpace)\<rbrace>
 2. \<And>s. finalise_prop_stuff (vs_valid_duplicates' \<circ> ksPSpace)
 3. \<And>rv s. no_cte_prop (vs_valid_duplicates' \<circ> ksPSpace) s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P17 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P17 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)) \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s
 4. \<And>e s. no_cte_prop (vs_valid_duplicates' \<circ> ksPSpace) s \<and> invs' s \<and> sch_act_simple s \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s
 5. \<And>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> no_cte_prop (vs_valid_duplicates' \<circ> ksPSpace) s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P17 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P17 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) proof (prove)
goal (2 subgoals):
 1. \<And>cap final sl. \<lbrace>vs_valid_duplicates' \<circ> ksPSpace and invs' and sch_act_simple and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> global.finaliseCap cap final False \<lbrace>\<lambda>rv. vs_valid_duplicates' \<circ> ksPSpace\<rbrace>
 2. \<And>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s proof (prove)
goal (2 subgoals):
 1. \<And>cap sl s. vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s \<Longrightarrow> valid_objs' s \<and> pspace_aligned' s \<and> valid_cap' cap s
 2. \<And>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s proof (prove)
goal:
No subgoals!