theory ArchSyscall_IF

lemma sts_authorised_for_globals_inv[Syscall_IF_assms]:
  "set_thread_state d f \<lbrace>authorised_for_globals_inv oper\<rbrace>" unfolding authorised_for_globals_inv_def authorised_for_globals_arch_inv_def
            authorised_for_globals_page_table_inv_def authorised_for_globals_page_inv_def apply (case_tac oper) apply (wp | simp)+ apply (rename_tac arch_invocation) apply (case_tac arch_invocation) apply simp apply (rename_tac page_table_invocation) apply (case_tac page_table_invocation) apply wpsimp+ apply (rename_tac page_invocation) apply (case_tac page_invocation) apply (simp | wp hoare_vcg_ex_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>authorised_for_globals_inv oper\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. authorised_for_globals_inv oper\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 2. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 3. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 4. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 5. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 6. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 7. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 8. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 9. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace>
 10. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>\<lambda>s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case oper of InvokeArchObject ai \<Rightarrow> (case ai of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True) s | _ \<Rightarrow> True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>case x10 of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case x10 of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>arch_invocation. oper = InvokeArchObject arch_invocation \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>arch_invocation x1. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePageTable x1\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 2. \<And>arch_invocation x2. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePageDirectory x2\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 3. \<And>arch_invocation x3. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePage x3\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 4. \<And>arch_invocation x4. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 5. \<And>arch_invocation x5. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>arch_invocation x1. \<lbrakk>oper = InvokeArchObject (InvokePageTable x1); arch_invocation = InvokePageTable x1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case x1 of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case x1 of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True\<rbrace>
 2. \<And>arch_invocation x2. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePageDirectory x2\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 3. \<And>arch_invocation x3. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePage x3\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 4. \<And>arch_invocation x4. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 5. \<And>arch_invocation x5. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>arch_invocation page_table_invocation. \<lbrakk>oper = InvokeArchObject (InvokePageTable page_table_invocation); arch_invocation = InvokePageTable page_table_invocation\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case page_table_invocation of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case page_table_invocation of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True\<rbrace>
 2. \<And>arch_invocation x2. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePageDirectory x2\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 3. \<And>arch_invocation x3. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePage x3\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 4. \<And>arch_invocation x4. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 5. \<And>arch_invocation x5. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>arch_invocation page_table_invocation x11 x12 x13 x14. \<lbrakk>oper = InvokeArchObject (InvokePageTable page_table_invocation); arch_invocation = InvokePageTable page_table_invocation; page_table_invocation = PageTableMap x11 x12 x13 x14\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case page_table_invocation of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case page_table_invocation of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True\<rbrace>
 2. \<And>arch_invocation page_table_invocation x21 x22. \<lbrakk>oper = InvokeArchObject (InvokePageTable page_table_invocation); arch_invocation = InvokePageTable page_table_invocation; page_table_invocation = PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case page_table_invocation of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case page_table_invocation of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True\<rbrace>
 3. \<And>arch_invocation x2. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePageDirectory x2\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 4. \<And>arch_invocation x3. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokePage x3\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 5. \<And>arch_invocation x4. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 6. \<And>arch_invocation x5. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x3. oper = InvokeArchObject (InvokePage x3) \<Longrightarrow> \<lbrace>\<lambda>s. case x3 of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case x3 of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace>
 2. \<And>arch_invocation x4. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 3. \<And>arch_invocation x5. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>page_invocation. oper = InvokeArchObject (InvokePage page_invocation) \<Longrightarrow> \<lbrace>\<lambda>s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace>
 2. \<And>arch_invocation x4. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 3. \<And>arch_invocation x5. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>page_invocation x11 x12 x13 x14. \<lbrakk>oper = InvokeArchObject (InvokePage page_invocation); page_invocation = PageMap x11 x12 x13 x14\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace>
 2. \<And>page_invocation x21 x22. \<lbrakk>oper = InvokeArchObject (InvokePage page_invocation); page_invocation = PageUnmap x21 x22\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace>
 3. \<And>page_invocation x31 x32 x33 x34 x35 x36. \<lbrakk>oper = InvokeArchObject (InvokePage page_invocation); page_invocation = PageFlush x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace>
 4. \<And>page_invocation x4. \<lbrakk>oper = InvokeArchObject (InvokePage page_invocation); page_invocation = PageGetAddr x4\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_ s. case page_invocation of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True\<rbrace>
 5. \<And>arch_invocation x4. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace>
 6. \<And>arch_invocation x5. \<lbrakk>oper = InvokeArchObject arch_invocation; arch_invocation = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> \<lbrace>case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> set_thread_state d f \<lbrace>\<lambda>_. case arch_invocation of InvokePageTable oper \<Rightarrow> \<lambda>s. case oper of PageTableMap cap ptr pde p \<Rightarrow> p && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) | PageTableUnmap capa prod \<Rightarrow> True | InvokePage oper \<Rightarrow> \<lambda>s. case oper of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True | _ \<Rightarrow> \<lambda>_. True\<rbrace> proof (prove)
goal:
No subgoals!