arm+arm-hyp+aarch64 proofs: proof update for deferred cache flush

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

proof/access-control/ARM/ArchRetype_AC.thy

@@ -209,25 +209,21 @@ lemma copy_global_invs_mappings_restricted':
 lemma init_arch_objects_pas_refined[Retype_AC_assms]:
   "\<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall> x\<in>set refs. x \<notin> global_refs s)
                     and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api tp obj_sz))\<rbrace>
-   init_arch_objects tp ptr bits obj_sz refs
+   init_arch_objects tp dev ptr bits obj_sz refs
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
+  supply if_split[split del]
   apply (rule hoare_gen_asm)
-  apply (cases tp)
-       apply (simp_all add: init_arch_objects_def)
-       apply (wp | simp)+
-  apply (rename_tac aobject_type)
-  apply (case_tac aobject_type, simp_all)
-        apply ((simp | wp)+)[5]
-   apply wp
-    apply (rule_tac Q'="\<lambda>rv. pas_refined aag and
+  apply (cases tp;
+         (wpsimp simp: init_arch_objects_def
+                 wp: mapM_x_wp'[where f="\<lambda>r. do_machine_op (m r)" for m]))
+   apply (rule_tac Q'="\<lambda>rv. pas_refined aag and
                             all_invs_but_equal_kernel_mappings_restricted (set refs) and
                             (\<lambda>s. \<forall>x \<in> set refs. x \<notin> global_refs s)" in hoare_strengthen_post)
-     apply (wp mapM_x_wp[OF _ subset_refl])
-     apply ((wp copy_global_mappings_pas_refined copy_global_invs_mappings_restricted'
-                copy_global_mappings_global_refs_inv copy_global_invs_mappings_restricted'
-             | fastforce simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def)+)[2]
-   apply (wp dmo_invs hoare_vcg_const_Ball_lift valid_irq_node_typ
-         | fastforce simp: post_retype_invs_def)+
+    apply (wp mapM_x_wp[OF _ subset_refl])
+    apply ((wp copy_global_mappings_pas_refined copy_global_invs_mappings_restricted'
+               copy_global_mappings_global_refs_inv copy_global_invs_mappings_restricted'
+            | fastforce simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def)+)[2]
+  apply (fastforce simp: post_retype_invs_def split: if_split)
   done
 
 lemma region_in_kernel_window_preserved:
@@ -287,7 +283,7 @@ crunch delete_objects
   (ignore: do_machine_op freeMemory)
 
 lemma init_arch_objects_pas_cur_domain[Retype_AC_assms, wp]:
-  "init_arch_objects tp ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
+  "init_arch_objects tp dev ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
   by wp
 
 lemma retype_region_pas_cur_domain[Retype_AC_assms, wp]:
@@ -366,13 +362,12 @@ lemma dmo_clearMemory_respects'[Retype_AC_assms]:
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   unfolding do_machine_op_def clearMemory_def
   apply (simp add: split_def cleanCacheRange_PoU_def)
-  apply wp
-  apply clarsimp
+  apply wpsimp
   apply (erule use_valid)
-   apply wp
-    apply (simp add: cleanCacheRange_RAM_def cleanCacheRange_PoC_def cacheRangeOp_def cleanL2Range_def
-                     cleanByVA_def split_def dsb_def)
-    apply (wp mol_respects mapM_x_wp' storeWord_respects)+
+   apply (wp mapM_x_wp')
+   apply (simp add: cleanCacheRange_RAM_def cleanCacheRange_PoC_def cacheRangeOp_def cleanL2Range_def
+                    cleanByVA_def split_def dsb_def)
+   apply (wp mol_respects mapM_x_wp' storeWord_respects)+
    apply (simp add: word_size_bits_def)
    apply (clarsimp simp: word_size_def word_bits_def upto_enum_step_shift_red[where us=2, simplified])
    apply (erule bspec)
@@ -396,14 +391,20 @@ lemma dmo_cleanCacheRange_PoU_respects [wp]:
   "do_machine_op (cleanCacheRange_PoU vstart vend pstart) \<lbrace>integrity aag X st\<rbrace>"
   by (wpsimp wp: dmo_cacheRangeOp_lift simp: cleanCacheRange_PoU_def cleanByVA_PoU_def)
 
+lemma dmo_cleanCacheRange_RAM_respects [wp]:
+  "do_machine_op (cleanCacheRange_RAM vstart vend pstart) \<lbrace>integrity aag X st\<rbrace>"
+  by (wpsimp wp: dmo_cacheRangeOp_lift
+             simp: dmo_bind_valid cleanCacheRange_RAM_def cleanCacheRange_PoC_def
+                   cleanL2Range_def dsb_def cleanByVA_def)
+
 lemma dmo_mapM_x_cleanCacheRange_PoU_integrity:
   "do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU (f x) (g x) (h x)) refs) \<lbrace>integrity aag X st\<rbrace>"
   by (wp dmo_mapM_x_wp_inv)
 
 lemma init_arch_objects_integrity[Retype_AC_assms]:
   "\<lbrace>integrity aag X st and K (\<forall>x\<in>set refs. is_subject aag x)
                        and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace>
-   init_arch_objects new_type ptr num_objects obj_sz refs
+   init_arch_objects new_type dev ptr num_objects obj_sz refs
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (rule hoare_gen_asm)+
   apply (cases new_type; simp add: init_arch_objects_def split del: if_split)

proof/access-control/DomainSepInv.thy

@@ -315,7 +315,7 @@ locale DomainSepInv_1 =
   and arch_post_cap_deletion_domain_sep_inv[wp]:
     "arch_post_cap_deletion acap \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
   and init_arch_objects_domain_sep_inv[wp]:
-    "init_arch_objects typ ptr n sz refs \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
+    "init_arch_objects typ dev ptr n sz refs \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
   and prepare_thread_delete_domain_sep_inv[wp]:
     "prepare_thread_delete t \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
   and arch_finalise_cap_rv:

proof/access-control/Retype_AC.thy

@@ -184,15 +184,15 @@ locale Retype_AC_1 =
     "\<And>tp. is_aligned p (obj_bits_api (ArchObject tp) n)
            \<Longrightarrow> aobj_ref' (arch_default_cap tp p n dev) \<subseteq> ptr_range p (obj_bits_api (ArchObject tp) n)"
   and init_arch_objects_pas_refined:
-    "\<And>tp. \<lbrace>pas_refined aag and post_retype_invs tp refs
+    "\<And>tp dev. \<lbrace>pas_refined aag and post_retype_invs tp refs
                             and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)
                             and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api tp obj_sz))\<rbrace>
-           init_arch_objects tp ptr bits obj_sz refs
-           \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
+               init_arch_objects tp dev ptr bits obj_sz refs
+               \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
   and dmo_freeMemory_invs:
     "do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>s :: det_ext state. invs s\<rbrace>"
   and init_arch_objects_pas_cur_domain[wp]:
-    "\<And>tp. init_arch_objects tp ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
+    "\<And>tp dev. init_arch_objects tp dev ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
   and retype_region_pas_cur_domain[wp]:
     "\<And>tp. retype_region ptr n us tp dev \<lbrace>pas_cur_domain aag\<rbrace>"
   and reset_untyped_cap_pas_cur_domain[wp]:
@@ -222,7 +222,7 @@ locale Retype_AC_1 =
   and init_arch_objects_integrity:
     "\<lbrace>integrity aag X st and K (\<forall>x\<in>set refs. is_subject aag x)
                          and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace>
-     init_arch_objects new_type ptr num_objects obj_sz refs
+     init_arch_objects new_type dev ptr num_objects obj_sz refs
      \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   and integrity_asids_detype:
     "\<forall>r \<in> R. pasObjectAbs aag r \<in> subjects

proof/access-control/Syscall_AC.thy

@@ -504,7 +504,7 @@ locale Syscall_AC_1 =
   and handle_reserved_irq_arch_state[wp]:
     "\<And>P. handle_reserved_irq irq \<lbrace>\<lambda>s :: det_ext state. P (arch_state s)\<rbrace>"
   and init_arch_objects_arch_state[wp]:
-    "\<And>P. init_arch_objects new_type ptr n sz refs \<lbrace>\<lambda>s :: det_ext state. P (arch_state s)\<rbrace>"
+    "\<And>P. init_arch_objects new_type dev ptr n sz refs \<lbrace>\<lambda>s :: det_ext state. P (arch_state s)\<rbrace>"
   and getActiveIRQ_inv:
     "\<And>P. \<forall>f s. P s \<longrightarrow> P (irq_state_update f s)
           \<Longrightarrow> \<lbrace>P\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv. P\<rbrace>"

proof/crefine/AARCH64/Invoke_C.thy

@@ -1649,43 +1649,34 @@ lemma clearMemory_untyped_ccorres:
   apply (cinit' lift: bits_' ptr___ptr_to_unsigned_long_')
    apply (rule_tac P="ptr \<noteq> 0 \<and> sz < word_bits" in ccorres_gen_asm)
    apply (simp add: clearMemory_def)
-   apply (simp add: doMachineOp_bind storeWord_empty_fail)
-   apply (rule ccorres_split_nothrow_novcg_dc)
-      apply (rule_tac P="?P" and P'="{s. region_actually_is_bytes ptr (2 ^ sz) s}" in ccorres_from_vcg)
-      apply (rule allI, rule conseqPre, vcg)
-      apply clarsimp
-      apply (rule conjI; clarsimp)
-       apply (simp add: word_less_nat_alt unat_of_nat word_bits_def)
-      apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def
-                            is_aligned_no_wrap'[OF _ word64_power_less_1]
-                            unat_of_nat_eq word_bits_def)
-      apply (simp add: is_aligned_weaken is_aligned_triv[THEN is_aligned_weaken])
-      apply (clarsimp simp: ghost_assertion_size_logic[unfolded o_def] region_actually_is_bytes_dom_s)
-      apply (clarsimp simp: field_simps word_size_def mapM_x_storeWord_step
-                            word_bits_def cte_wp_at_ctes_of)
-      apply (frule ctes_of_valid', clarify+)
-      apply (simp add: doMachineOp_def split_def exec_gets)
-      apply (simp add: select_f_def simpler_modify_def bind_def valid_cap_simps' capAligned_def)
-      apply (subst pspace_no_overlap_underlying_zero_update; simp?)
-       apply (case_tac sz, simp_all)[1]
-       apply (case_tac nat, simp_all)[1]
-       apply (case_tac nata, simp_all)[1]
-      apply (clarsimp dest!: region_actually_is_bytes)
-      apply (drule(1) rf_sr_rep0)
-      apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
-                            carch_state_relation_def cmachine_state_relation_def)
-     apply csymbr
-     apply (ctac add: cleanCacheRange_RAM_ccorres)
-    apply wp
-   apply (simp add: guard_is_UNIV_def unat_of_nat
-                    word_bits_def capAligned_def word_of_nat_less)
+   apply (rule_tac P="?P" and P'="{s. region_actually_is_bytes ptr (2 ^ sz) s}" in ccorres_from_vcg)
+   apply (rule allI, rule conseqPre, vcg)
+   apply clarsimp
+   apply (rule conjI; clarsimp)
+    apply (simp add: word_less_nat_alt unat_of_nat word_bits_def)
+   apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def
+                         is_aligned_no_wrap'[OF _ word64_power_less_1]
+                         unat_of_nat_eq word_bits_def)
+   apply (simp add: is_aligned_weaken is_aligned_triv[THEN is_aligned_weaken])
+   apply (clarsimp simp: ghost_assertion_size_logic[unfolded o_def] region_actually_is_bytes_dom_s)
+   apply (clarsimp simp: field_simps word_size_def mapM_x_storeWord_step
+                         word_bits_def cte_wp_at_ctes_of)
+   apply (frule ctes_of_valid', clarify+)
+   apply (simp add: doMachineOp_def split_def exec_gets)
+   apply (simp add: select_f_def simpler_modify_def bind_def valid_cap_simps' capAligned_def)
+   apply (subst pspace_no_overlap_underlying_zero_update; simp?)
+    apply (case_tac sz, simp_all)[1]
+    apply (case_tac nat, simp_all)[1]
+    apply (case_tac nata, simp_all)[1]
+   apply (clarsimp dest!: region_actually_is_bytes)
+   apply (drule(1) rf_sr_rep0)
+   apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
+                         carch_state_relation_def cmachine_state_relation_def)
   apply (clarsimp simp: cte_wp_at_ctes_of)
   apply (frule ctes_of_valid'; clarify?)
   apply (clarsimp simp: isCap_simps valid_cap_simps' capAligned_def
                         word_of_nat_less Kernel_Config.resetChunkBits_def
                         word_bits_def unat_2p_sub_1)
-  apply (strengthen is_aligned_no_wrap'[where sz=sz] is_aligned_addrFromPPtr_n)+
-  apply (simp add: addrFromPPtr_mask_cacheLineSize pptrBaseOffset_alignment_def)
   apply (cases "ptr = 0"; simp)
   apply (drule subsetD, rule intvl_self, simp)
   apply simp

proof/crefine/AARCH64/Machine_C.thy

@@ -199,6 +199,13 @@ assumes cleanCacheRange_RAM_preserves_kernel_bytes:
           \<and> (\<forall>x. snd (hrs_htd (t_hrs_' (globals s)) x) 0 \<noteq> None
                  \<longrightarrow> hrs_mem (t_hrs_' (globals t)) x = hrs_mem (t_hrs_' (globals s)) x)}"
 
+assumes cleanCacheRange_PoU_preserves_kernel_bytes:
+  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanCacheRange_PoU_'proc
+       {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
+           \<and> (\<forall>x. snd (hrs_htd (t_hrs_' (globals s)) x) 0 \<noteq> None
+                  \<longrightarrow> hrs_mem (t_hrs_' (globals t)) x = hrs_mem (t_hrs_' (globals s)) x)}"
+
+
 (* Hypervisor-related machine ops *)
 
 (* ARM Hypervisor hardware register getters and setters *)

proof/crefine/AARCH64/Recycle_C.thy

@@ -252,8 +252,6 @@ lemma range_cover_nca_neg: "\<And>x p (off :: 9 word).
   apply (simp add: pageBits_def objBits_simps)
   done
 
-lemmas unat_of_nat32' = unat_of_nat_eq[where 'a=32]
-
 lemma clearMemory_PageCap_ccorres:
   "ccorres dc xfdc (invs' and valid_cap' (ArchObjectCap (FrameCap ptr undefined sz False None))
            and (\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s)
@@ -268,30 +266,27 @@ lemma clearMemory_PageCap_ccorres:
   apply (cinit' lift: bits_' ptr___ptr_to_unsigned_long_')
    apply (rule_tac P="capAligned (ArchObjectCap (FrameCap ptr undefined sz False None))"
                 in ccorres_gen_asm)
-   apply (rule ccorres_Guard_Seq)
+   apply (rule ccorres_Guard)
    apply (simp add: clearMemory_def)
-   apply (simp add: doMachineOp_bind)
-   apply (rule ccorres_split_nothrow_novcg_dc)
-      apply (rule_tac P="?P" in ccorres_from_vcg[where P'=UNIV])
-      apply (rule allI, rule conseqPre, vcg)
-      apply (clarsimp simp: valid_cap'_def capAligned_def
-                            is_aligned_no_wrap'[OF _ word64_power_less_1])
-      apply (prop_tac "ptr \<noteq> 0")
-       subgoal
-         apply (simp add: frame_at'_def)
-         apply (drule_tac x=0 in spec)
-         apply (clarsimp simp: pageBitsForSize_def bit_simps split: vmpage_size.splits)
-         done
-      apply simp
-      apply (prop_tac "3 \<le> pageBitsForSize sz")
-       apply (simp add: pageBitsForSize_def bit_simps split: vmpage_size.split)
-      apply (rule conjI)
-       apply (erule is_aligned_weaken)
-       apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits)
-      apply (rule conjI)
-       apply (rule is_aligned_power2)
-       apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits)
-      apply (clarsimp simp: ghost_assertion_size_logic[unfolded o_def])
+   apply (rule_tac P="?P" in ccorres_from_vcg[where P'=UNIV])
+   apply (rule allI, rule conseqPre, vcg)
+   apply (clarsimp simp: valid_cap'_def capAligned_def
+                         is_aligned_no_wrap'[OF _ word64_power_less_1])
+   apply (prop_tac "ptr \<noteq> 0")
+  subgoal
+    apply (simp add: frame_at'_def)
+    apply (drule_tac x=0 in spec)
+    apply (clarsimp simp: pageBitsForSize_def bit_simps split: vmpage_size.splits)
+    done
+   apply simp
+   apply (prop_tac "3 \<le> pageBitsForSize sz")
+    apply (simp add: pageBitsForSize_def bit_simps split: vmpage_size.split)
+   apply (rule conjI)
+    apply (erule is_aligned_weaken)
+    apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits)
+   apply (rule conjI)
+    apply (rule is_aligned_power2)
+    apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits)
    apply (clarsimp simp: ghost_assertion_size_logic[unfolded o_def] frame_at'_def)
    apply (simp add: flex_user_data_at_rf_sr_dom_s bit_simps)
    apply (clarsimp simp: field_simps word_size_def mapM_x_storeWord_step)
@@ -308,7 +303,7 @@ lemma clearMemory_PageCap_ccorres:
     apply (erule allfEI[where f=of_nat])
     apply (clarsimp simp: bit_simps)
     apply (subst(asm) of_nat_power, assumption)
-    apply simp
+     apply simp
      apply (insert pageBitsForSize_64 [of sz])[1]
      apply (erule order_le_less_trans [rotated])
      apply simp
@@ -376,25 +371,8 @@ lemma clearMemory_PageCap_ccorres:
     apply (simp add: bit_simps)
     apply (simp add: of_nat_power[where 'a=64, folded word_bits_def])
     apply (simp add: pageBits_def ko_at_projectKO_opt[OF user_data_at_ko])
-   (* FIXME AARCH64 indentation *)
    apply (rule inj_Ptr)
-     apply csymbr
-     apply (ctac add: cleanCacheRange_RAM_ccorres)
-    apply wp
-   apply (simp add: guard_is_UNIV_def unat_of_nat
-                    word_bits_def capAligned_def word_of_nat_less)
-  apply (clarsimp simp: word_bits_def valid_cap'_def
-                        capAligned_def word_of_nat_less)
-  apply (frule is_aligned_addrFromPPtr_n, simp add: pageBitsForSize_def split: vmpage_size.splits)
-  apply (simp add: bit_simps pptrBaseOffset_alignment_def)+
-  apply (simp add: is_aligned_no_overflow')
-  apply (rule conjI)
-  subgoal
-    apply (prop_tac "cacheLineSize \<le> pageBitsForSize sz")
-     apply (simp add: pageBitsForSize_def bit_simps cacheLineSize_def split: vmpage_size.splits)
-    apply (simp add: is_aligned_mask[THEN iffD1] is_aligned_weaken)
-    done
-  apply (simp add: pageBitsForSize_def bit_simps split: vmpage_size.splits)
+  apply (clarsimp simp: word_bits_def valid_cap'_def capAligned_def word_of_nat_less)
   done
 
 declare replicate_numeral [simp]