theory ArchRetype_AI

lemma mapM_copy_global_invs_mappings_restricted:
  "\<lbrace>\<lambda>s. all_invs_but_equal_kernel_mappings_restricted (set pds) s
            \<and> (set pds \<inter> global_refs s = {})
            \<and> (\<forall>pd \<in> set pds. is_aligned pd pd_bits)\<rbrace>
     mapM_x copy_global_mappings pds
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (fold all_invs_but_equal_kernel_mappings_restricted_eq) apply (induct pds, simp_all only: mapM_x_Nil mapM_x_Cons K_bind_def) apply wpsimp apply (rule hoare_seq_ext, assumption, thin_tac "P" for P) apply (wpsimp wp: copy_global_invs_mappings_restricted) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set pds)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set pds \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set pds. is_aligned pd pd_bits)\<rbrace> mapM_x copy_global_mappings pds \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set pds)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set pds \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set pds. is_aligned pd pd_bits)\<rbrace> mapM_x copy_global_mappings pds \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- {})\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set [])\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set [] \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set []. is_aligned pd pd_bits)\<rbrace> return () \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- {})\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace>
 2. \<And>a pds. \<lbrace>\<lambda>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set pds)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set pds \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set pds. is_aligned pd pd_bits)\<rbrace> mapM_x copy_global_mappings pds \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- {})\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set (a # pds))\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set (a # pds) \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set (a # pds). is_aligned pd pd_bits)\<rbrace> do y <- copy_global_mappings a;
mapM_x copy_global_mappings pds
od \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- {})\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a pds. \<lbrace>\<lambda>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set pds)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set pds \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set pds. is_aligned pd pd_bits)\<rbrace> mapM_x copy_global_mappings pds \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- {})\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set (a # pds))\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set (a # pds) \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set (a # pds). is_aligned pd pd_bits)\<rbrace> do y <- copy_global_mappings a;
mapM_x copy_global_mappings pds
od \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- {})\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a pds. \<lbrace>\<lambda>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set (a # pds))\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set (a # pds) \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set (a # pds). is_aligned pd pd_bits)\<rbrace> copy_global_mappings a \<lbrace>\<lambda>x s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set pds)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) s \<and> set pds \<inter> global_refs s = {} \<and> (\<forall>pd\<in>set pds. is_aligned pd pd_bits)\<rbrace> proof (prove)
goal:
No subgoals!