theory Arch_DR

lemma set_vm_root_for_flush_dwp[wp]:
  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_vm_root_for_flush word1 word2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" apply (simp add:set_vm_root_for_flush_def) apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+ apply (wpc) apply wp+ apply (rule hoare_conjI,rule hoare_drop_imp) apply (wp do_machine_op_wp|clarsimp simp:load_hw_asid_def)+ apply (wpc|wp)+ apply (rule_tac Q="\<lambda>rv s. transform s = cs" in hoare_strengthen_post) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_vm_root_for_flush word1 word2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do tcb <- gets cur_thread;
thread_root <- CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0));
not_is_pd <- case thread_root of ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> word1) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch word1 word2;
return True
od else return False
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tcb x not_is_pd xa. not_is_pd \<Longrightarrow> \<lbrace>?B26 tcb x True xa\<rbrace> case xa of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
store_hw_asid word2 new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid \<lbrace>\<lambda>hwasid ps. transform ps = cs\<rbrace>
 2. \<And>tcb x not_is_pd. not_is_pd \<Longrightarrow> \<lbrace>?Q5 tcb x (ds_id True)\<rbrace> load_hw_asid word2 \<lbrace>?B26 tcb x not_is_pd\<rbrace>
 3. \<And>tcb x not_is_pd. \<not> not_is_pd \<Longrightarrow> \<lbrace>?R5 tcb x not_is_pd\<rbrace> return False \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>tcb x. \<lbrace>?B3 tcb x\<rbrace> case x of ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> word1) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>not_is_pd s. (not_is_pd \<longrightarrow> ?Q5 tcb x not_is_pd s) \<and> (\<not> not_is_pd \<longrightarrow> ?R5 tcb x not_is_pd s)\<rbrace>
 5. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B3 tcb\<rbrace>
 6. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 7. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal (8 subgoals):
 1. \<And>tcb x not_is_pd xa. \<lbrakk>not_is_pd; xa = None\<rbrakk> \<Longrightarrow> \<lbrace>?R41 tcb x True xa\<rbrace> do new_hw_asid <- find_free_hw_asid;
store_hw_asid word2 new_hw_asid;
return new_hw_asid
od \<lbrace>\<lambda>hwasid ps. transform ps = cs\<rbrace>
 2. \<And>tcb x not_is_pd xa x2. \<lbrakk>not_is_pd; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. ?R40 tcb x True xa a x2\<rbrace> return x2 \<lbrace>\<lambda>hwasid ps. transform ps = cs\<rbrace>
 3. \<And>tcb x not_is_pd. not_is_pd \<Longrightarrow> \<lbrace>?Q5 tcb x (ds_id True)\<rbrace> load_hw_asid word2 \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R41 tcb x not_is_pd a b) \<and> (\<forall>xa. a = Some xa \<longrightarrow> ?R40 tcb x not_is_pd a b xa)\<rbrace>
 4. \<And>tcb x not_is_pd. \<not> not_is_pd \<Longrightarrow> \<lbrace>?R5 tcb x not_is_pd\<rbrace> return False \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>tcb x. \<lbrace>?B3 tcb x\<rbrace> case x of ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> word1) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>not_is_pd s. (not_is_pd \<longrightarrow> ?Q5 tcb x not_is_pd s) \<and> (\<not> not_is_pd \<longrightarrow> ?R5 tcb x not_is_pd s)\<rbrace>
 6. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B3 tcb\<rbrace>
 7. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 8. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal (6 subgoals):
 1. \<And>tcb x not_is_pd. not_is_pd \<Longrightarrow> \<lbrace>?Q5 tcb x (ds_id True)\<rbrace> load_hw_asid word2 \<lbrace>\<lambda>a b. (a = None \<longrightarrow> transform b = cs) \<and> (\<forall>x. a = Some x \<longrightarrow> transform b = cs)\<rbrace>
 2. \<And>tcb x not_is_pd. \<not> not_is_pd \<Longrightarrow> \<lbrace>?R5 tcb x not_is_pd\<rbrace> return False \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>tcb x. \<lbrace>?B3 tcb x\<rbrace> case x of ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> word1) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>not_is_pd s. (not_is_pd \<longrightarrow> ?Q5 tcb x not_is_pd s) \<and> (\<not> not_is_pd \<longrightarrow> ?R5 tcb x not_is_pd s)\<rbrace>
 4. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B3 tcb\<rbrace>
 5. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 6. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal (7 subgoals):
 1. \<And>tcb x not_is_pd. not_is_pd \<Longrightarrow> \<lbrace>?Q5 tcb x (ds_id True)\<rbrace> load_hw_asid word2 \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<And>tcb x not_is_pd. not_is_pd \<Longrightarrow> \<lbrace>?Q5 tcb x (ds_id True)\<rbrace> load_hw_asid word2 \<lbrace>\<lambda>r s. \<forall>x. r = Some x \<longrightarrow> transform s = cs\<rbrace>
 3. \<And>tcb x not_is_pd. \<not> not_is_pd \<Longrightarrow> \<lbrace>?R5 tcb x not_is_pd\<rbrace> return False \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>tcb x. \<lbrace>?B3 tcb x\<rbrace> case x of ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> word1) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>not_is_pd s. (not_is_pd \<longrightarrow> ?Q5 tcb x not_is_pd s) \<and> (\<not> not_is_pd \<longrightarrow> ?R5 tcb x not_is_pd s)\<rbrace>
 5. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B3 tcb\<rbrace>
 6. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 7. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>tcb x. \<lbrace>?B3 tcb x\<rbrace> case x of ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> word1) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>not_is_pd s. transform s = cs\<rbrace>
 2. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B3 tcb\<rbrace>
 3. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 4. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = cap.NullCap \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc xd. x = cap.UntypedCap xa xb xc xd \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = cap.EndpointCap xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = cap.NotificationCap xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = cap.ReplyCap xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = cap.CNodeCap xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> transform s = cs) \<and> (x = cap.DomainCap \<longrightarrow> transform s = cs) \<and> (x = IRQControlCap \<longrightarrow> transform s = cs) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> transform s = cs) \<and> (xa = ASIDControlCap \<longrightarrow> transform s = cs) \<and> (\<forall>x xb xc xd xe. xa = PageCap x xb xc xd xe \<longrightarrow> transform s = cs) \<and> (\<forall>x xb. xa = arch_cap.PageTableCap x xb \<longrightarrow> transform s = cs) \<and> (\<forall>x xb. xa = arch_cap.PageDirectoryCap x xb \<longrightarrow> (xb = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. xb = Some x \<longrightarrow> transform s = cs)))\<rbrace>
 2. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<And>tcb rv s. transform s = cs \<Longrightarrow> (rv = cap.NullCap \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb xc. rv = cap.UntypedCap x xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = cap.EndpointCap x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = cap.NotificationCap x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = cap.ReplyCap x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = cap.CNodeCap x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> transform s = cs) \<and> (rv = cap.DomainCap \<longrightarrow> transform s = cs) \<and> (rv = IRQControlCap \<longrightarrow> transform s = cs) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> transform s = cs) \<and> (x = ASIDControlCap \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb. x = arch_cap.PageTableCap xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb. x = arch_cap.PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. xb = Some x \<longrightarrow> transform s = cs)))
 3. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 4. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!