arm+riscv access: update proofs

proof/access-control/ARM/ArchDomainSepInv.thy

@@ -25,6 +25,21 @@ lemma arch_finalise_cap_rv[DomainSepInv_assms]:
   "\<lbrace>\<lambda>_. P (NullCap,NullCap)\<rbrace> arch_finalise_cap c x \<lbrace>\<lambda>rv _. P rv\<rbrace>"
   unfolding arch_finalise_cap_def by wpsimp
 
+crunch
+  invalidate_tlb_by_asid, handle_reserved_irq, handle_vm_fault,
+  handle_hypervisor_fault, handle_arch_fault_reply, arch_mask_irq_signal,
+  arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread
+  for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st"
+
+lemma arch_derive_cap_domain_sep_inv[DomainSepInv_assms, wp]:
+  "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. domain_sep_inv_cap irqs rv\<rbrace>,-"
+  unfolding arch_derive_cap_def
+  by wpsimp
+
+lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]:
+  "arch_post_modify_registers cur x31 \<lbrace>domain_sep_inv irqs st\<rbrace>"
+  unfolding arch_post_modify_registers_def by wpsimp
+
 end
 
 
@@ -38,12 +53,6 @@ qed
 
 context Arch begin global_naming ARM_A
 
-crunch
-  invalidate_tlb_by_asid, handle_reserved_irq, handle_vm_fault,
-  handle_hypervisor_fault, handle_arch_fault_reply, arch_mask_irq_signal,
-  arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread
-  for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st"
-
 lemma perform_page_invocation_domain_sep_inv:
   "\<lbrace>domain_sep_inv irqs st and valid_page_inv pgi\<rbrace>
    perform_page_invocation pgi
@@ -120,23 +129,14 @@ lemma arch_invoke_irq_control_domain_sep_inv[DomainSepInv_assms]:
    apply (wpsimp wp: do_machine_op_domain_sep_inv simp: arch_irq_control_inv_valid_def)+
   done
 
-lemma arch_derive_cap_domain_sep_inv[DomainSepInv_assms, wp]:
-  "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. domain_sep_inv_cap irqs rv\<rbrace>,-"
-  unfolding arch_derive_cap_def
-  by wpsimp
-
-lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]:
-  "arch_post_modify_registers cur x31 \<lbrace>domain_sep_inv irqs st\<rbrace>"
-  unfolding arch_post_modify_registers_def by wpsimp
-
 end
 
 
 global_interpretation DomainSepInv_2?: DomainSepInv_2
 proof goal_cases
   interpret Arch .
   case 1 show ?case
-    by (unfold_locales; fact DomainSepInv_assms)
+    by (unfold_locales; wpsimp wp: DomainSepInv_assms)
 qed
 
 end

proof/access-control/ARM/ArchInterrupt_AC.thy

@@ -21,8 +21,7 @@ definition arch_authorised_irq_ctl_inv ::
        (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag"
 
 lemma arch_invoke_irq_control_pas_refined[Interrupt_AC_assms]:
-  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
-                    and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv
+  "\<lbrace>pas_refined aag and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv
                     and K (arch_authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace>
    arch_invoke_irq_control irq_ctl_inv
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
@@ -75,7 +74,7 @@ global_interpretation Interrupt_AC_1?: Interrupt_AC_1 "arch_authorised_irq_ctl_i
 proof goal_cases
   interpret Arch .
   case 1 show ?case
-    by (unfold_locales; (fact Interrupt_AC_assms)?)
+    by (unfold_locales; fact Interrupt_AC_assms)
 qed
 
 

proof/access-control/ARM/ArchSyscall_AC.thy

@@ -179,7 +179,7 @@ global_interpretation Syscall_AC_1?: Syscall_AC_1
 proof goal_cases
   interpret Arch .
   case 1 show ?case
-    by (unfold_locales; (fact Syscall_AC_assms)?)
+    by (unfold_locales; wpsimp wp: Syscall_AC_assms)
 qed
 
 end

proof/access-control/RISCV64/ArchArch_AC.thy

@@ -19,20 +19,13 @@ context Arch begin global_naming RISCV64
 named_theorems Arch_AC_assms
 
 lemma set_mrs_state_vrefs[Arch_AC_assms, wp]:
-  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
-   set_mrs thread buf msgs
-   \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace>"
+  "set_mrs thread buf msgs \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace>"
   apply (simp add: set_mrs_def split_def set_object_def get_object_def split del: if_split)
   apply (wpsimp wp: gets_the_wp get_wp put_wp mapM_x_wp'
               simp: zipWithM_x_mapM_x split_def store_word_offs_def
          split_del: if_split)
-  apply (subst state_vrefs_eqI)
-        prefer 7
-        apply assumption
-       apply (clarsimp simp: opt_map_def)
-      apply (fastforce simp: opt_map_def aobj_of_def)
-     apply clarsimp
-    apply (auto simp: valid_arch_state_def)
+  apply (subst (asm) state_vrefs_tcb_upd[symmetric])
+   apply (auto simp: fun_upd_def get_tcb_def tcb_at_def)
   done
 
 lemma mul_add_word_size_lt_msg_align_bits_ofnat[Arch_AC_assms]:
@@ -503,11 +496,9 @@ lemma perform_pt_inv_unmap_pas_refined:
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
   unfolding perform_pt_inv_unmap_def
   apply (wpsimp wp: set_cap_pas_refined get_cap_wp)
-       apply (strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)
        apply wps
        apply (rule hoare_vcg_all_lift[OF hoare_vcg_imp_lift'[OF mapM_x_wp_inv]], wpsimp wp: mapM_x_wp_inv)
        apply (rule hoare_vcg_conj_lift[OF hoare_strengthen_post[OF mapM_x_swp_store_InvalidPTE_pas_refined]], assumption)
-       apply (rule hoare_vcg_conj_lift[OF hoare_strengthen_post[OF mapM_x_swp_store_pte_invs_unmap]], assumption)
        apply (wpsimp wp: pt_lookup_from_level_wrp store_pte_invs_unmap store_pte_pas_refined
                          mapM_x_wp_inv unmap_page_table_pas_refined
                          hoare_vcg_imp_lift' hoare_vcg_ball_lift hoare_vcg_all_lift)+

proof/access-control/RISCV64/ArchCNode_AC.thy

@@ -56,29 +56,28 @@ lemma sata_update2[CNode_AC_assms]:
                  simp: cap_links_asid_slot_def label_owns_asid_slot_def
                 split: if_split_asm)
 
+lemma vs_lookup_table_eqI':
+    "\<lbrakk> asid_table s' (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid);
+       \<forall>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr
+                  \<longrightarrow> bot_level \<le> max_pt_level
+                  \<longrightarrow> vspace_for_pool pool_ptr asid (asid_pools_of s') =
+                      vspace_for_pool pool_ptr asid (asid_pools_of s);
+       bot_level < max_pt_level \<longrightarrow> pts_of s' = pts_of s \<rbrakk>
+   \<Longrightarrow> vs_lookup_table bot_level asid vref s' = vs_lookup_table bot_level asid vref s"
+  by (auto simp: obind_def vs_lookup_table_def asid_pool_level_eq[symmetric]
+                 pool_for_asid_def vspace_for_pool_def
+          split: option.splits)
+
 lemma state_vrefs_eqI:
-  "\<lbrakk> \<forall>bot_level asid vref level p.
-       bot_level < level \<and> vs_lookup_table level asid vref s = Some (level, p)
-       \<longrightarrow> (if level \<le> max_pt_level
-            then pts_of s' p = pts_of s p
-            else asid_pools_of s' p = asid_pools_of s p);
-     aobjs_of s' = aobjs_of s; asid_table s' = asid_table s;
-     pspace_aligned s; valid_vspace_objs s; valid_asid_table s \<rbrakk>
-     \<Longrightarrow> state_vrefs (s' :: 'a :: state_ext state) = state_vrefs (s :: 'a :: state_ext state)"
-  apply (rule ext)
-  apply safe
-   apply (subst (asm) state_vrefs_def, clarsimp)
-   apply (fastforce intro: state_vrefsD elim: subst[OF vs_lookup_table_eqI,rotated -1])
-  apply (subst (asm) state_vrefs_def, clarsimp)
-  apply (rule state_vrefsD)
-     apply (subst vs_lookup_table_eqI; fastforce)
-    apply fastforce+
-  done
+  assumes "asid_table s' = asid_table s"
+  and "aobjs_of s' = aobjs_of s"
+  shows "state_vrefs s' = state_vrefs s"
+  apply (prop_tac "\<forall>level asid vref. vs_lookup_table level asid vref s = vs_lookup_table level asid vref s'")
+   apply (intro allI vs_lookup_table_eqI')
+  using assms by (auto simp: vspace_for_pool_def state_vrefs_def)
 
 lemma set_cap_state_vrefs[CNode_AC_assms, wp]:
-  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
-   set_cap cap slot
-   \<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
+  "set_cap cap slot \<lbrace>\<lambda>s :: det_ext state. P (state_vrefs s)\<rbrace>"
   apply (simp add: set_cap_def set_object_def)
   apply (wpsimp wp: get_object_wp)
   apply safe
@@ -100,14 +99,12 @@ crunch prepare_thread_delete, arch_finalise_cap
   (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)
 
 lemma state_vrefs_tcb_upd[CNode_AC_assms]:
-  "\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at t s \<rbrakk>
-     \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
+  "tcb_at t s \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
   apply (rule state_vrefs_eqI)
   by (fastforce simp: opt_map_def obj_at_def is_obj_defs valid_arch_state_def)+
 
 lemma state_vrefs_simple_type_upd[CNode_AC_assms]:
-  "\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s;
-     ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val) \<rbrakk>
+  "\<lbrakk> ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val) \<rbrakk>
      \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>) = state_vrefs s"
   apply (case_tac ko; case_tac "f val"; clarsimp)
   by (fastforce intro!: state_vrefs_eqI simp: opt_map_def obj_at_def is_obj_defs valid_arch_state_def)+

proof/access-control/RISCV64/ArchDomainSepInv.thy

@@ -25,28 +25,39 @@ lemma arch_finalise_cap_rv[DomainSepInv_assms]:
   "\<lbrace>\<lambda>_. P (NullCap,NullCap)\<rbrace> arch_finalise_cap c x \<lbrace>\<lambda>rv _. P rv\<rbrace>"
   unfolding arch_finalise_cap_def by wpsimp
 
+crunch
+  handle_reserved_irq, handle_vm_fault, perform_pg_inv_map, perform_pg_inv_unmap,
+  perform_pg_inv_get_addr, perform_pt_inv_map, perform_pt_inv_unmap,
+  handle_hypervisor_fault, handle_arch_fault_reply, arch_mask_irq_signal,
+  arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread,
+  store_asid_pool_entry, copy_global_mappings
+  for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st"
+  (wp: crunch_wps)
+
+lemma arch_derive_cap_domain_sep_inv[DomainSepInv_assms, wp]:
+  "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. domain_sep_inv_cap irqs rv\<rbrace>,-"
+  unfolding arch_derive_cap_def
+  by wpsimp
+
+lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]:
+  "arch_post_modify_registers cur t \<lbrace>domain_sep_inv irqs st\<rbrace>"
+  unfolding arch_post_modify_registers_def by wpsimp
+
+declare init_arch_objects_inv[DomainSepInv_assms]
+
 end
 
 
 global_interpretation DomainSepInv_1?: DomainSepInv_1
 proof goal_cases
   interpret Arch .
   case 1 show ?case
-    by (unfold_locales; (fact DomainSepInv_assms | wp init_arch_objects_inv))
+    by (unfold_locales; fact DomainSepInv_assms)
 qed
 
 
 context Arch begin global_naming RISCV64
 
-crunch
-  handle_reserved_irq, handle_vm_fault, perform_pg_inv_map, perform_pg_inv_unmap,
-  perform_pg_inv_get_addr, perform_pt_inv_map, perform_pt_inv_unmap,
-  handle_hypervisor_fault, handle_arch_fault_reply, arch_mask_irq_signal,
-  arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread,
-  store_asid_pool_entry, copy_global_mappings
-  for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st"
-  (wp: crunch_wps)
-
 lemma perform_page_invocation_domain_sep_inv:
   "\<lbrace>domain_sep_inv irqs st and valid_page_inv pgi\<rbrace>
    perform_page_invocation pgi
@@ -112,23 +123,14 @@ lemma arch_invoke_irq_control_domain_sep_inv[DomainSepInv_assms]:
    apply (wpsimp wp: do_machine_op_domain_sep_inv simp: arch_irq_control_inv_valid_def)+
   done
 
-lemma arch_derive_cap_domain_sep_inv[DomainSepInv_assms, wp]:
-  "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. domain_sep_inv_cap irqs rv\<rbrace>,-"
-  unfolding arch_derive_cap_def
-  by wpsimp
-
-lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]:
-  "arch_post_modify_registers cur t \<lbrace>domain_sep_inv irqs st\<rbrace>"
-  unfolding arch_post_modify_registers_def by wpsimp
-
 end
 
 
 global_interpretation DomainSepInv_2?: DomainSepInv_2
 proof goal_cases
   interpret Arch .
   case 1 show ?case
-    by (unfold_locales; fact DomainSepInv_assms)
+    by (unfold_locales; wpsimp wp: DomainSepInv_assms)
 qed
 
 end

proof/access-control/RISCV64/ArchFinalise_AC.thy

@@ -111,9 +111,7 @@ crunch prepare_thread_delete
   for respects[Finalise_AC_assms, wp]: "integrity aag X st"
 
 lemma sbn_st_vrefs[Finalise_AC_assms]:
-  "\<lbrace>(\<lambda>s. P (state_vrefs s)) and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
-   set_bound_notification t st
-   \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace>"
+  "set_bound_notification t st \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace>"
   apply (simp add: set_bound_notification_def)
   apply (wpsimp wp: set_object_wp dxo_wp_weak)
   apply (subst state_vrefs_tcb_upd)
@@ -216,7 +214,7 @@ lemma delete_asid_respects:
   apply (clarsimp simp: pas_refined_refl obj_at_def asid_pool_integrity_def)
   done
 
-lemma arch_finalise_cap_respects[wp]:
+lemma arch_finalise_cap_respects[Finalise_AC_assms, wp]:
   "\<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (ArchObjectCap cap)
                        and K (pas_cap_cur_auth aag (ArchObjectCap cap))\<rbrace>
    arch_finalise_cap cap final
@@ -229,10 +227,11 @@ lemma arch_finalise_cap_respects[wp]:
              intro: pas_refined_Control_into_is_subject_asid)
   done
 
-crunch arch_post_cap_deletion
-  for pspace_aligned[Finalise_AC_assms, wp]: "\<lambda>s :: det_ext state. pspace_aligned s"
-  and valid_vspace_objs[Finalise_AC_assms, wp]: "\<lambda>s :: det_ext state. valid_vspace_objs s"
-  and valid_arch_state[Finalise_AC_assms, wp]: "\<lambda>s :: det_ext state. valid_arch_state s"
+declare prepare_thread_delete_st_tcb_at_halted[Finalise_AC_assms]
+declare finalise_cap_valid_list[Finalise_AC_assms]
+declare arch_finalise_cap_pas_refined[Finalise_AC_assms]
+declare prepare_thread_delete_pas_refined[Finalise_AC_assms]
+declare finalise_cap_replaceable[Finalise_AC_assms]
 
 end
 
@@ -241,7 +240,7 @@ global_interpretation Finalise_AC_1?: Finalise_AC_1
 proof goal_cases
   interpret Arch .
   case 1 show ?case
-    by (unfold_locales; (fact Finalise_AC_assms | wp finalise_cap_replaceable))
+    by (unfold_locales; wpsimp wp: Finalise_AC_assms)
 qed
 
 

proof/access-control/RISCV64/ArchInterrupt_AC.thy

@@ -21,8 +21,7 @@ definition arch_authorised_irq_ctl_inv ::
        (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag"
 
 lemma arch_invoke_irq_control_pas_refined[Interrupt_AC_assms]:
-  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
-                    and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv
+  "\<lbrace>pas_refined aag and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv
                     and K (arch_authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace>
    arch_invoke_irq_control irq_ctl_inv
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"

proof/access-control/RISCV64/ArchIpc_AC.thy

@@ -188,11 +188,6 @@ lemma auth_ipc_buffers_machine_state_update[Ipc_AC_assms, simp]:
   "auth_ipc_buffers (machine_state_update f s) = auth_ipc_buffers s"
   by (clarsimp simp: auth_ipc_buffers_def get_tcb_def)
 
-crunch handle_arch_fault_reply
-  for pspace_aligned[Ipc_AC_assms, wp]: "\<lambda>s :: det_ext state. pspace_aligned s"
-  and valid_vspace_objs[Ipc_AC_assms, wp]: "\<lambda>s :: det_ext state. valid_vspace_objs s"
-  and valid_arch_state[Ipc_AC_assms, wp]: "\<lambda>s :: det_ext state. valid_arch_state s"
-
 lemma cap_insert_ext_integrity_asids_in_ipc[Ipc_AC_assms, wp]:
   "cap_insert_ext src_parent src_slot dest_slot src_p dest_p
    \<lbrace>\<lambda>s. integrity_asids aag subjects x asid st

proof/access-control/RISCV64/ArchSyscall_AC.thy

@@ -160,6 +160,7 @@ crunch
 \<comment> \<open>These aren't proved in the previous crunch, and hence need to be declared\<close>
 declare handle_arch_fault_reply_cur_thread[Syscall_AC_assms]
 declare handle_arch_fault_reply_it[Syscall_AC_assms]
+declare init_arch_objects_inv[Syscall_AC_assms]
 
 end
 
@@ -168,7 +169,7 @@ global_interpretation Syscall_AC_1?: Syscall_AC_1
 proof goal_cases
   interpret Arch .
   case 1 show ?case
-    by (unfold_locales; (fact Syscall_AC_assms | wp init_arch_objects_inv))
+    by (unfold_locales; wpsimp wp: Syscall_AC_assms)
 qed
 
 end