theory ArchVSpace_AI

lemma set_vm_root_for_flush_asid_map [wp]:
  "\<lbrace>valid_asid_map and K (asid \<le> mask asid_bits)\<rbrace>
  set_vm_root_for_flush pd asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: set_vm_root_for_flush_def) apply (wp|wpc|simp)+ apply (rule hoare_strengthen_post [where
               Q="\<lambda>_. valid_asid_map and K (asid \<le> mask asid_bits)"]) apply wp apply simp apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and K (asid \<le> mask local.asid_bits)\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)\<rbrace> do tcb <- gets cur_thread;
thread_root <- get_cap (tcb, tcb_cnode_index (Suc 0));
not_is_pd <- case thread_root of ArchObjectCap (PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb xc xd. x = UntypedCap xa xb xc xd) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb xc. x = EndpointCap xa xb xc) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb xc. x = NotificationCap xa xb xc) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb xc. x = ReplyCap xa xb xc) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb xc. x = CNodeCap xa xb xc) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa. x = ThreadCap xa) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (x = DomainCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (x = IRQControlCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa. x = IRQHandlerCap xa) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb xc. x = Zombie xa xb xc) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (xa = ASIDControlCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xb xc xd xe. xa = PageCap x xb xc xd xe) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xb. xa = PageTableCap x xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (\<forall>x xb. xa = PageDirectoryCap x xb \<longrightarrow> (xb = None \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x. xb = Some x) \<longrightarrow> (x \<noteq> pd \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (x = pd \<longrightarrow> valid_asid_map s))))\<rbrace>
 2. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 3. \<And>s. (valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>_. valid_asid_map and K (asid \<le> mask local.asid_bits)\<rbrace>
 2. \<And>tcb rv s. (valid_asid_map and K (asid \<le> mask local.asid_bits)) s \<Longrightarrow> (rv = NullCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb xc. rv = UntypedCap x xa xb xc) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = EndpointCap x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = NotificationCap x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = ReplyCap x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = CNodeCap x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x. rv = ThreadCap x) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (rv = DomainCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (rv = IRQControlCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x. rv = IRQHandlerCap x) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = Zombie x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> ((\<exists>xa xb. x = ASIDPoolCap xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (x = ASIDControlCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb xc xd xe. x = PageCap xa xb xc xd xe) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb. x = PageTableCap xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x. xb = Some x) \<longrightarrow> (xa \<noteq> pd \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (xa = pd \<longrightarrow> valid_asid_map s))))
 3. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 4. \<And>s. (valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>tcb rv s. (valid_asid_map and K (asid \<le> mask local.asid_bits)) s \<Longrightarrow> (rv = NullCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb xc. rv = UntypedCap x xa xb xc) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = EndpointCap x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = NotificationCap x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = ReplyCap x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = CNodeCap x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x. rv = ThreadCap x) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (rv = DomainCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (rv = IRQControlCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x. rv = IRQHandlerCap x) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x xa xb. rv = Zombie x xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> ((\<exists>xa xb. x = ASIDPoolCap xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (x = ASIDControlCap \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb xc xd xe. x = PageCap xa xb xc xd xe) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>xa xb. x = PageTableCap xa xb) \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> ((\<exists>x. xb = Some x) \<longrightarrow> (xa \<noteq> pd \<longrightarrow> valid_asid_map s \<and> asid \<le> mask local.asid_bits) \<and> (xa = pd \<longrightarrow> valid_asid_map s))))
 2. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>\<lambda>tcb. valid_asid_map and K (asid \<le> mask local.asid_bits)\<rbrace>
 3. \<And>s. (valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>\<lambda>tcb. valid_asid_map and K (asid \<le> mask local.asid_bits)\<rbrace>
 2. \<And>s. (valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_asid_map and K (asid \<le> mask local.asid_bits)) s proof (prove)
goal:
No subgoals!