arm-hyp crefine: minimal fixups for arch-split up to InvariantUpdates_H

Most of the changes were ported from ARM (which were adapted from
AARCH64).

Signed-off-by: Rafal Kolanski <[email protected]>

proof/crefine/ARM_HYP/ADT_C.thy

@@ -111,7 +111,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)
   apply (simp add: cep_relations_drop_fun_upd)
   apply (drule ko_at_projectKO_opt)
@@ -780,6 +780,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)
@@ -1366,7 +1367,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]

proof/crefine/ARM_HYP/ArchMove_C.thy

@@ -28,6 +28,8 @@ lemma vaddr_segment_nonsense6:
   apply (rule shiftr_less_t2n'[where m=11 and n=21 and 'a=machine_word_len, simplified])
   done
 
+context begin interpretation Arch .
+
 (* Short-hand for  unfolding cumbersome machine constants *)
 (* FIXME MOVE these should be in refine, and the _eq forms should NOT be declared [simp]! *)
 (* FIXME YUCK where did you come from *)
@@ -119,8 +121,6 @@ lemma addToBitmap_sets_L1Bitmap_same_dom:
   apply wpsimp
   by (metis nth_0 prioToL1Index_bit_set word_or_zero)
 
-context begin interpretation Arch .
-
 lemma setCTE_asidpool':
   "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>"
   apply (clarsimp simp: setCTE_def)
@@ -463,7 +463,7 @@ lemma fromEnum_maxBound_vppievent_irq_def:
 (* FIXME move *)
 lemma ps_clear_entire_slotI:
   "({p..p + 2 ^ n - 1}) \<inter> dom (ksPSpace s) = {} \<Longrightarrow> ps_clear p n s"
-  by (fastforce simp: ps_clear_def)
+  by (fastforce simp: ps_clear_def mask_def add_diff_eq)
 
 lemma ps_clear_ksPSpace_upd_same[simp]:
   "ps_clear p n (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> v)\<rparr>) = ps_clear p n s"
@@ -531,21 +531,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)

proof/crefine/ARM_HYP/Detype_C.thy

@@ -396,13 +396,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
@@ -570,7 +571,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
@@ -1645,7 +1646,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
     using  cmap_array[simplified table_bits_defs]
     apply -
     apply (elim conjE)
@@ -1793,7 +1794,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",
@@ -1846,7 +1847,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",
@@ -1872,9 +1873,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

proof/crefine/ARM_HYP/Fastpath_C.thy

@@ -1756,7 +1756,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
 
@@ -1766,7 +1766,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
 
@@ -2303,7 +2303,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'
@@ -2512,7 +2512,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
@@ -2564,7 +2564,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
 
@@ -2574,7 +2574,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
 

proof/crefine/ARM_HYP/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:
@@ -1766,7 +1766,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

proof/crefine/ARM_HYP/Finalise_C.thy

@@ -832,7 +832,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)+
@@ -882,7 +882,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)+
@@ -1896,7 +1896,7 @@ lemma archThreadSet_tcbVCPU_Basic_ccorres:
                                  update_tcb_map_to_tcb
                                  cmachine_state_relation_def
                                  update_tcb_map_tos)?)
-      apply (subst map_to_ctes_upd_tcb_no_ctes; simp add: tcb_cte_cases_def)
+      apply (subst map_to_ctes_upd_tcb_no_ctes; simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
      apply (erule cmap_relation_updI, erule ko_at_projectKO_opt, simp+)
       apply (clarsimp simp: ctcb_relation_def carch_tcb_relation_def ccontext_relation_def atcbContextGet_def)
      apply clarsimp

proof/crefine/ARM_HYP/Ipc_C.thy

@@ -4860,7 +4860,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
@@ -4870,7 +4870,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
 
@@ -5416,7 +5416,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
@@ -5426,7 +5426,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
 
@@ -6421,7 +6421,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
@@ -6430,7 +6430,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
 

proof/crefine/ARM_HYP/IsolatedThreadAction.thy

@@ -139,11 +139,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 tcbBlockSizeBits_def, simplified]
 
 lemmas setObject_modify_tcb
     = setObject_modify[OF _ meta_eq_to_obj_eq, OF _ updateObject_tcb,
-                       unfolded objBits_simps', simplified]
+                       unfolded gen_objBits_simps tcbBlockSizeBits_def, simplified]
 
 lemma partial_overwrite_fun_upd:
   "inj idx \<Longrightarrow>

proof/crefine/ARM_HYP/Recycle_C.thy

@@ -555,10 +555,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_HYP.pageBits_def)
+     apply  (clarsimp simp: ARM_HYP.objBits_simps ARM_HYP.pageBits_def)
     apply simp
    apply (rule is_aligned_add_helper[THEN conjunct2])
-    apply (simp add: ARM_HYP.pageBits_def objBits_simps)
+    apply (simp add: ARM_HYP.pageBits_def ARM_HYP.objBits_simps)
    apply (rule word_less_power_trans2[where k = 2,simplified])
      apply (rule less_le_trans[OF ucast_less])
       apply simp+

proof/crefine/ARM_HYP/Refine_C.thy

@@ -662,7 +662,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 fastforce
         apply fastforce
        apply fastforce