arm crefine+infoflow: minimal fixups for arch-split up to InvariantUp…

…dates_H Most of the changes were ported from X64 (which were adapted from AARCH64). Signed-off-by: Rafal Kolanski <[email protected]>
seL4 · Jan 8, 2025 · ea44902 · ea44902
1 parent aa2e36a
commit ea44902
Show file tree

Hide file tree

Showing 18 changed files with 162 additions and 135 deletions.
diff --git a/proof/crefine/ARM/ADT_C.thy b/proof/crefine/ARM/ADT_C.thy
@@ -102,7 +102,7 @@ lemma setTCBContext_C_corres:
   apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def
                         carch_state_relation_def cmachine_state_relation_def
                         typ_heap_simps' update_tcb_map_tos)
-  apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def
+  apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def tcb_cte_cases_neqs
                    cvariable_relation_upd_const ko_at_projectKO_opt cteSizeBits_def)
   apply (simp add: cep_relations_drop_fun_upd)
   apply (drule ko_at_projectKO_opt)
@@ -746,6 +746,7 @@ lemma map_to_ctes_tcb_ctes:
   "ctes_of s' = ctes_of s \<Longrightarrow>
    ko_at' tcb p s \<Longrightarrow> ko_at' tcb' p s' \<Longrightarrow>
    \<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb"
+  supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *)
   apply (clarsimp simp add: ran_tcb_cte_cases)
   apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKO_opt_tcb
                  split: kernel_object.splits)
@@ -1216,7 +1217,7 @@ lemma ksPSpace_eq_imp_typ_at'_eq:
 lemma ksPSpace_eq_imp_valid_cap'_eq:
   assumes ksPSpace: "ksPSpace s' = ksPSpace s"
   shows "valid_cap' c s' = valid_cap' c s"
-  by (auto simp: valid_cap'_def page_table_at'_def page_directory_at'_def
+  by (auto simp: valid_cap'_def valid_arch_cap'_def page_table_at'_def page_directory_at'_def
                  valid_untyped'_def
                  ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace]
                  ksPSpace_eq_imp_typ_at'_eq[OF ksPSpace]
@@ -1226,10 +1227,9 @@ lemma ksPSpace_eq_imp_valid_cap'_eq:
 lemma ksPSpace_eq_imp_valid_tcb'_eq:
   assumes ksPSpace: "ksPSpace s' = ksPSpace s"
   shows "valid_tcb' tcb s' = valid_tcb' tcb s"
-
   by (auto simp: ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace]
                  ksPSpace_eq_imp_valid_cap'_eq[OF ksPSpace]
-                 valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def
+                 valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def valid_arch_tcb'_def
           split: thread_state.splits option.splits)
 
 lemma ksPSpace_eq_imp_valid_arch_obj'_eq:

diff --git a/proof/crefine/ARM/ArchMove_C.thy b/proof/crefine/ARM/ArchMove_C.thy
@@ -32,6 +32,8 @@ lemma ps_clear_is_aligned_ksPSpace_None:
                     power_overflow)
   by assumption
 
+context begin interpretation Arch .
+
 lemma ps_clear_is_aligned_ctes_None:
   assumes "ps_clear p tcbBlockSizeBits s"
       and "is_aligned p tcbBlockSizeBits"
@@ -50,8 +52,6 @@ lemma Arch_switchToThread_obj_at_pre:
   apply (wp doMachineOp_obj_at setVMRoot_obj_at hoare_drop_imps|wpc)+
   done
 
-context begin interpretation Arch .
-
 lemma asid_pool_at'_ko:
   "asid_pool_at' p s \<Longrightarrow> \<exists>pool. ko_at' (ASIDPool pool) p s"
   apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs)
@@ -147,21 +147,23 @@ lemma valid_untyped':
   apply (frule pspace_distinctD'[OF _ pspace_distinct'])
   apply simp
   apply (frule aligned_ranges_subset_or_disjoint[OF al])
+  apply (simp only: add_mask_fold)
   apply (fold obj_range'_def)
   apply (rule iffI)
    apply auto[1]
   apply (rule conjI)
    apply (rule ccontr, simp)
    apply (simp add: Set.psubset_eq)
    apply (erule conjE)
-   apply (case_tac "obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}", simp)
+   apply (case_tac "obj_range' ptr' ko \<inter> mask_range ptr bits \<noteq> {}", simp)
    apply (cut_tac is_aligned_no_overflow[OF al])
-   apply (auto simp add: obj_range'_def)[1]
+   apply (auto simp add: obj_range'_def add_mask_fold)[1]
   apply (clarsimp simp add: usableUntypedRange.simps Int_commute)
-  apply (case_tac "obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}", simp+)
+  apply (case_tac "obj_range' ptr' ko \<inter> mask_range ptr bits \<noteq> {}", simp)
   apply (cut_tac is_aligned_no_overflow[OF al])
   apply (clarsimp simp add: obj_range'_def)
   apply (frule is_aligned_no_overflow)
+  apply (simp add: mask_def add_diff_eq)
   by (metis al intvl_range_conv' le_m1_iff_lt less_is_non_zero_p1
                nat_le_linear power_overflow sub_wrap add_0
                add_0_right word_add_increasing word_less_1 word_less_sub_1)

diff --git a/proof/crefine/ARM/Arch_C.thy b/proof/crefine/ARM/Arch_C.thy
@@ -487,7 +487,7 @@ shows
      apply (frule(1) ctes_of_valid_cap'[OF _ invs_valid_objs'])
      apply (clarsimp simp:valid_cap'_def asid_low_bits_def invs_urz)
      apply (strengthen descendants_range_in_subseteq'[mk_strg I E] refl)
-     apply simp
+     apply (simp add: word_size_bits_def)
      apply (intro conjI)
         apply (simp add:is_aligned_def)
       apply (rule descendants_range_caps_no_overlapI'[where d=isdev and cref = parent])

diff --git a/proof/crefine/ARM/Detype_C.thy b/proof/crefine/ARM/Detype_C.thy
@@ -307,13 +307,14 @@ proof -
       using vu unfolding valid_cap'_def valid_untyped'_def
       apply clarsimp
       apply (drule_tac x = x in spec)
-      apply (clarsimp simp:ko_wp_at'_def)
+      apply (clarsimp simp:ko_wp_at'_def add_mask_fold)
       done
 
     with koat have "\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1}"
       apply -
       apply (erule obj_atE')+
-      apply (simp add: ko_wp_at'_def projectKOs obj_range'_def not_less objBits_def project_inject)
+      apply (simp add: ko_wp_at'_def projectKOs obj_range'_def not_less objBits_def project_inject
+                       add_mask_fold)
       done
 
     thus ?thesis using subset1
@@ -481,7 +482,7 @@ proof -
      apply simp
     apply clarsimp
     apply (drule_tac y = n in aligned_add_aligned [where m = 4])
-     apply (simp add: tcb_cte_cases_def is_aligned_def split: if_split_asm)
+     apply (simp add: tcb_cte_cases_def cteSizeBits_def is_aligned_def split: if_split_asm)
     apply (simp add: word_bits_conv)
     apply simp
     done
@@ -1536,7 +1537,7 @@ proof -
   hence "cpspace_relation ?ks' (underlying_memory (ksMachineState s)) ?th_s"
     unfolding cpspace_relation_def
     using cendpoint_relation_restrict [OF D.valid_untyped invs rl]
-      cnotification_relation_restrict [OF D.valid_untyped invs rl]
+      cnotification_relation_restrict [OF D.valid_untyped invs rl] b2
     apply -
     apply (elim conjE)
     apply ((subst lift_t_typ_region_bytes,
@@ -1564,8 +1565,8 @@ proof -
       apply (clarsimp simp: restrict_map_Some_iff image_iff
                             map_comp_restrict_map_Some_iff)
      apply (simp add: cmap_relation_restrict_both_proj)
-    apply (rule cmap_array; simp add: pdeBits_def)
-   apply (rule cmap_array; simp add: pteBits_def)
+    apply (rule cmap_array; simp add: pdeBits_def word_size_bits_def)
+   apply (rule cmap_array; simp add: pteBits_def word_size_bits_def)
    done
   moreover
   from sr have
@@ -1686,7 +1687,7 @@ proof -
     apply (frule pspace_distinctD'[OF _ pspace_distinct'])
     apply (clarsimp simp add: valid_cap'_def valid_untyped'_def2 capAligned_def)
     apply (drule_tac x=x in spec)
-    apply (simp add: obj_range'_def objBitsKO_def)
+    apply (simp add: obj_range'_def objBitsKO_def mask_def add_diff_eq)
     apply (simp only: not_le)
     apply (cut_tac is_aligned_no_overflow[OF al])
     apply (case_tac "ptr \<le> x + 2 ^ pageBits - 1",
@@ -1725,7 +1726,7 @@ proof -
        [where 'a=32, folded word_bits_def, simplified, OF _ _ al _ wb])
        apply assumption+
     apply (rule iffI[rotated], simp)
-    apply (simp add: objBits_simps projectKOs)
+    apply (simp add: objBits_simps projectKOs mask_def add_diff_eq)
     apply (rule FalseE)
     apply (case_tac "ptr \<le> x", simp)
      apply clarsimp
@@ -1739,7 +1740,7 @@ proof -
     apply (frule pspace_distinctD'[OF _ pspace_distinct'])
     apply (clarsimp simp add: valid_cap'_def valid_untyped'_def2 capAligned_def)
     apply (drule_tac x=x in spec)
-    apply (simp add: obj_range'_def objBitsKO_def)
+    apply (simp add: obj_range'_def objBitsKO_def mask_def add_diff_eq)
     apply (simp only: not_le)
     apply (cut_tac is_aligned_no_overflow[OF al])
     apply (case_tac "ptr \<le> x + 2 ^ pageBits - 1",
@@ -1765,9 +1766,9 @@ proof -
         \<Longrightarrow> {p ..+ 2 ^ objBitsT TCBT} \<inter> {ptr..+2 ^ bits} = {}"
       apply (clarsimp simp: valid_cap'_def)
       apply (drule(1) map_to_ko_atI')
-      apply (clarsimp simp: obj_at'_def valid_untyped'_def2)
+      apply (clarsimp simp: obj_at'_def valid_untyped'_def2 mask_2pm1 add_diff_eq)
       apply (elim allE, drule(1) mp)
-      apply (clarsimp simp only: obj_range'_def upto_intvl_eq[symmetric] al)
+      apply (clarsimp simp only: obj_range'_def upto_intvl_eq[symmetric] al add_mask_fold[symmetric])
       apply (subgoal_tac "objBitsKO ko = objBitsT TCBT")
        apply (subgoal_tac "p \<in> {p ..+ 2 ^ objBitsT TCBT}")
         apply simp

diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy
@@ -1710,7 +1710,7 @@ proof -
     apply (clarsimp simp:tcbs_of_def cte_at'_obj_at'
       split:if_splits)
     apply (drule_tac x = "0x10 * tcbVTableSlot" in bspec)
-     apply (simp add:tcb_cte_cases_def tcbVTableSlot_def)
+     apply (simp add:tcb_cte_cases_def cteSizeBits_def tcbVTableSlot_def)
     apply simp
     done
 
@@ -1720,7 +1720,7 @@ proof -
     apply (clarsimp simp:tcbs_of_def cte_at'_obj_at'
       split:if_splits)
     apply (drule_tac x = "0x10 * tcbCallerSlot" in bspec)
-     apply (simp add:tcb_cte_cases_def tcbCallerSlot_def)
+     apply (simp add:tcb_cte_cases_def cteSizeBits_def tcbCallerSlot_def)
     apply simp
     done
 
@@ -2260,7 +2260,7 @@ proof -
                                  threadSet_st_tcb_at_state threadSet_cte_wp_at'
                                  threadSet_cur
                                | simp add: cur_tcb'_def[symmetric])+
-                     apply (simp add: valid_tcb'_def tcb_cte_cases_def
+                     apply (simp add: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def
                                       valid_tcb_state'_def)
                      apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift
                                set_ep_valid_objs'
@@ -2468,7 +2468,7 @@ lemma threadSet_tcbState_valid_objs:
      threadSet (tcbState_update (\<lambda>_. st)) t
    \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
   apply (wp threadSet_valid_objs')
-  apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
+  apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs)
   done
 
 lemmas array_assertion_abs_tcb_ctes_add
@@ -2520,7 +2520,7 @@ lemma fastpath_reply_recv_ccorres:
     apply (clarsimp simp:tcbs_of_def cte_at'_obj_at'
       split:if_splits)
     apply (drule_tac x = "0x10 * tcbVTableSlot" in bspec)
-     apply (simp add:tcb_cte_cases_def tcbVTableSlot_def)
+     apply (simp add:tcb_cte_cases_def cteSizeBits_def tcbVTableSlot_def)
     apply simp
     done
 
@@ -2530,7 +2530,7 @@ lemma fastpath_reply_recv_ccorres:
     apply (clarsimp simp:tcbs_of_def cte_at'_obj_at'
       split:if_splits)
     apply (drule_tac x = "0x10 * tcbCallerSlot" in bspec)
-     apply (simp add:tcb_cte_cases_def tcbCallerSlot_def)
+     apply (simp add:tcb_cte_cases_def cteSizeBits_def tcbCallerSlot_def)
     apply simp
     done
 

diff --git a/proof/crefine/ARM/Fastpath_Equiv.thy b/proof/crefine/ARM/Fastpath_Equiv.thy
@@ -305,7 +305,7 @@ lemma threadSet_tcbState_valid_objs:
      threadSet (tcbState_update (\<lambda>_. st)) t
    \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
   apply (wp threadSet_valid_objs')
-  apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
+  apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs)
   done
 
 lemma possibleSwitchTo_rewrite:
@@ -1760,7 +1760,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
               in cte_wp_at_valid_objs_valid_cap', clarsimp+)
   apply (clarsimp simp: valid_cap_simps')
   apply (subst tcb_at_cte_at_offset,
-         assumption, simp add: tcb_cte_cases_def cte_level_bits_def tcbSlots)
+         assumption, simp add: tcb_cte_cases_def cteSizeBits_def cte_level_bits_def tcbSlots)
   apply (clarsimp simp: inj_case_bool cte_wp_at_ctes_of
                         length_msgRegisters
                         order_less_imp_le

diff --git a/proof/crefine/ARM/Finalise_C.thy b/proof/crefine/ARM/Finalise_C.thy
@@ -798,7 +798,7 @@ lemma doUnbindNotification_ccorres:
       apply simp
       apply (erule(1) rf_sr_tcb_update_no_queue2)
               apply (simp add: typ_heap_simps')+
-       apply (simp add: tcb_cte_cases_def)
+       apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
       apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def)
      apply (simp add: invs'_def valid_state'_def)
      apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+
@@ -848,7 +848,7 @@ lemma doUnbindNotification_ccorres':
       apply simp
       apply (erule(1) rf_sr_tcb_update_no_queue2)
               apply (simp add: typ_heap_simps')+
-       apply (simp add: tcb_cte_cases_def)
+       apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
       apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def)
      apply (simp add: invs'_def valid_state'_def)
      apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+

diff --git a/proof/crefine/ARM/Ipc_C.thy b/proof/crefine/ARM/Ipc_C.thy
@@ -4333,7 +4333,7 @@ lemma sendIPC_block_ccorres_helper:
                               rf_sr_tcb_update_twice)
         apply (erule(1) rf_sr_tcb_update_no_queue_gen,
           (simp add: typ_heap_simps')+)[1]
-         apply (simp add: tcb_cte_cases_def)
+         apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
         apply (simp add: ctcb_relation_def cthread_state_relation_def
                          ThreadState_defs mask_def)
        apply ceqv
@@ -4343,7 +4343,7 @@ lemma sendIPC_block_ccorres_helper:
                threadSet_valid_objs')
     apply (clarsimp simp: guard_is_UNIV_def)
    apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def
-                         tcb_cte_cases_def)
+                         tcb_cte_cases_def tcb_cte_cases_neqs)
   apply clarsimp
   done
 
@@ -4890,7 +4890,7 @@ lemma receiveIPC_block_ccorres_helper:
         apply (frule h_t_valid_c_guard)
         apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice cap_get_tag_isCap)
         apply (erule(1) rf_sr_tcb_update_no_queue_gen, (simp add: typ_heap_simps)+)
-         apply (simp add: tcb_cte_cases_def)
+         apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
         apply (simp add: ctcb_relation_def cthread_state_relation_def ccap_relation_ep_helpers
                          ThreadState_defs mask_def cap_get_tag_isCap)
        apply ceqv
@@ -4900,7 +4900,7 @@ lemma receiveIPC_block_ccorres_helper:
                threadSet_weak_sch_act_wf_runnable')
     apply (clarsimp simp: guard_is_UNIV_def)
    apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def
-                         tcb_cte_cases_def)
+                         tcb_cte_cases_def tcb_cte_cases_neqs)
   apply clarsimp
   done
 
@@ -5893,7 +5893,7 @@ lemma receiveSignal_block_ccorres_helper:
         apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice)
         apply (erule(1) rf_sr_tcb_update_no_queue_gen,
           (simp add: typ_heap_simps')+)
-         apply (simp add: tcb_cte_cases_def)
+         apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
         apply (simp add: ctcb_relation_def cthread_state_relation_def
                          ThreadState_defs mask_def)
        apply ceqv
@@ -5902,7 +5902,7 @@ lemma receiveSignal_block_ccorres_helper:
      apply (wp hoare_vcg_all_lift threadSet_valid_objs'
                threadSet_weak_sch_act_wf_runnable')
     apply (clarsimp simp: guard_is_UNIV_def)
-   apply (auto simp: weak_sch_act_wf_def valid_tcb'_def tcb_cte_cases_def
+   apply (auto simp: weak_sch_act_wf_def valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs
                      valid_tcb_state'_def)
   done
 

diff --git a/proof/crefine/ARM/IsolatedThreadAction.thy b/proof/crefine/ARM/IsolatedThreadAction.thy
@@ -141,11 +141,11 @@ lemma getObject_return:
 
 lemmas getObject_return_tcb
     = getObject_return[OF meta_eq_to_obj_eq, OF loadObject_tcb,
-                       unfolded objBits_simps', simplified]
+                       unfolded gen_objBits_simps, simplified]
 
 lemmas setObject_modify_tcb
     = setObject_modify[OF _ meta_eq_to_obj_eq, OF _ updateObject_tcb,
-                       unfolded objBits_simps', simplified]
+                       unfolded gen_objBits_simps, simplified]
 
 lemma partial_overwrite_fun_upd:
   "inj idx \<Longrightarrow>

diff --git a/proof/crefine/ARM/Recycle_C.thy b/proof/crefine/ARM/Recycle_C.thy
@@ -341,10 +341,10 @@ lemma heap_to_user_data_in_user_mem'[simp]:
    apply (subst is_aligned_add_helper[THEN conjunct2,where n1 = 2])
      apply (erule aligned_add_aligned)
       apply (simp add: is_aligned_mult_triv2[where n = 2,simplified])
-     apply  (clarsimp simp: objBits_simps ARM.pageBits_def)
+     apply  (clarsimp simp: ARM.objBits_simps ARM.pageBits_def)
     apply simp
    apply (rule is_aligned_add_helper[THEN conjunct2])
-    apply (simp add: ARM.pageBits_def objBits_simps)
+    apply (simp add: ARM.pageBits_def ARM.objBits_simps)
    apply (rule word_less_power_trans2[where k = 2,simplified])
      apply (rule less_le_trans[OF ucast_less])
       apply simp+

diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy
@@ -640,7 +640,7 @@ lemma threadSet_all_invs_triv':
         apply (simp add: tcb_relation_def arch_tcb_context_set_def
                          atcbContextSet_def arch_tcb_relation_def)
        apply (simp add: tcb_cap_cases_def)
-      apply (simp add: tcb_cte_cases_def)
+      apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
      apply (simp add: exst_same_def)
     apply (wp thread_set_invs_trivial thread_set_ct_running thread_set_not_state_valid_sched
               threadSet_invs_trivial threadSet_ct_running' hoare_weak_lift_imp