aarch64 refine: proof update for det_ext refactor

Signed-off-by: Corey Lewis <[email protected]>

proof/refine/AARCH64/ADT_H.thy

@@ -281,6 +281,9 @@ definition
       tcb_fault = map_option FaultMap (tcbFault tcb),
       tcb_bound_notification = tcbBoundNotification tcb,
       tcb_mcpriority = tcbMCP tcb,
+      tcb_priority = tcbPriority tcb,
+      tcb_time_slice = tcbTimeSlice tcb,
+      tcb_domain = tcbDomain tcb,
       tcb_arch = ArchTcbMap (tcbArch tcb)\<rparr>"
 
 definition
@@ -831,53 +834,6 @@ proof -
     done
 qed
 
-definition
-  "EtcbMap tcb \<equiv>
-     \<lparr>tcb_priority = tcbPriority tcb,
-      time_slice = tcbTimeSlice tcb,
-      tcb_domain = tcbDomain tcb\<rparr>"
-
-definition absEkheap ::
-  "(machine_word \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> obj_ref \<Rightarrow> etcb option" where
-  "absEkheap h \<equiv> \<lambda>x.
-     case h x of
-       Some (KOTCB tcb) \<Rightarrow> Some (EtcbMap tcb)
-     | _ \<Rightarrow> None"
-
-lemma absEkheap_correct:
-  assumes pspace_relation: "pspace_relation (kheap s) (ksPSpace s')"
-  assumes ekheap_relation: "ekheap_relation (ekheap s) (ksPSpace s')"
-  assumes vetcbs: "valid_etcbs s"
-  shows "absEkheap (ksPSpace s') = ekheap s"
-  apply (rule ext)
-  apply (clarsimp simp: absEkheap_def split: option.splits Structures_H.kernel_object.splits)
-  apply (subgoal_tac "\<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) =
-                          (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb'))")
-   using vetcbs ekheap_relation
-   apply (clarsimp simp: valid_etcbs_def is_etcb_at_def dom_def ekheap_relation_def st_tcb_at_def obj_at_def)
-   apply (erule_tac x=x in allE)+
-   apply (rule conjI, force)
-   apply clarsimp
-   apply (rule conjI, clarsimp simp: EtcbMap_def etcb_relation_def)+
-   apply clarsimp
-  using pspace_relation
-  apply (clarsimp simp add: pspace_relation_def pspace_dom_def UNION_eq
-                              dom_def Collect_eq)
-  apply (rule iffI)
-   apply (erule_tac x=x in allE)+
-   apply (case_tac "ksPSpace s' x", clarsimp)
-    apply (erule_tac x=x in allE, clarsimp)
-   apply clarsimp
-   apply (case_tac a, simp_all add: tcb_relation_cut_def other_obj_relation_def)
-  apply (insert pspace_relation)
-  apply (clarsimp simp: obj_at'_def)
-  apply (erule(1) pspace_dom_relatedE)
-  apply (erule(1) obj_relation_cutsE)
-     apply (clarsimp simp: other_obj_relation_def
-                    split: Structures_A.kernel_object.split_asm  if_split_asm
-                           AARCH64_A.arch_kernel_obj.split_asm)+
-  done
-
 text \<open>The following function can be used to reverse cte_map.\<close>
 definition
   "cteMap cns \<equiv> \<lambda>p.
@@ -1645,30 +1601,19 @@ lemma absSchedulerAction_correct:
 definition
   "absExst s \<equiv>
      \<lparr>work_units_completed_internal = ksWorkUnitsCompleted s,
-      scheduler_action_internal = absSchedulerAction (ksSchedulerAction s),
-      ekheap_internal = absEkheap (ksPSpace s),
-      domain_list_internal = ksDomSchedule s,
-      domain_index_internal = ksDomScheduleIdx s,
-      cur_domain_internal = ksCurDomain s,
-      domain_time_internal = ksDomainTime s,
-      ready_queues_internal = (\<lambda>d p. heap_walk (tcbSchedNexts_of s) (tcbQueueHead (ksReadyQueues s (d, p))) []),
       cdt_list_internal = absCDTList (cteMap (gsCNodes s)) (ctes_of s)\<rparr>"
 
 lemma absExst_correct:
   assumes invs: "einvs s" and invs': "invs' s'"
   assumes rel: "(s, s') \<in> state_relation"
   shows "absExst s' = exst s"
   apply (rule det_ext.equality)
-           using rel invs invs'
-           apply (simp_all add: absExst_def absSchedulerAction_correct absEkheap_correct
-                                absCDTList_correct[THEN fun_cong] state_relation_def invs_def
-                                valid_state_def ready_queues_relation_def ready_queue_relation_def
-                                invs'_def valid_state'_def
-                                valid_pspace_def valid_sched_def valid_pspace'_def curry_def
-                                fun_eq_iff)
-   apply (fastforce simp: absEkheap_correct)
-  apply (fastforce simp: list_queue_relation_def Let_def dest: heap_ls_is_walk)
-  done
+      using rel invs invs'
+      apply (simp_all add: absExst_def absSchedulerAction_correct
+                           absCDTList_correct[THEN fun_cong] state_relation_def invs_def valid_state_def
+                           ready_queues_relation_def invs'_def valid_state'_def
+                           valid_pspace_def valid_sched_def valid_pspace'_def curry_def fun_eq_iff)
+      done
 
 
 definition
@@ -1677,6 +1622,12 @@ definition
     cdt = absCDT (cteMap (gsCNodes s)) (ctes_of s),
     is_original_cap = absIsOriginalCap (cteMap (gsCNodes s)) (ksPSpace s),
     cur_thread = ksCurThread s, idle_thread = ksIdleThread s,
+    scheduler_action = absSchedulerAction (ksSchedulerAction s),
+    domain_list = ksDomSchedule s,
+    domain_index = ksDomScheduleIdx s,
+    cur_domain = ksCurDomain s,
+    domain_time = ksDomainTime s,
+    ready_queues = (\<lambda>d p. heap_walk (tcbSchedNexts_of s) (tcbQueueHead (ksReadyQueues s (d, p))) []),
     machine_state = observable_memory (ksMachineState s) (user_mem' s),
     interrupt_irq_node = absInterruptIRQNode (ksInterruptState s),
     interrupt_states = absInterruptStates (ksInterruptState s),

proof/refine/AARCH64/ArchAcc_R.thy

@@ -455,11 +455,6 @@ lemma setObject_PT_corres:
     apply ((simp split: if_split_asm)+)[2]
    apply (simp add: other_obj_relation_def
                split: Structures_A.kernel_object.splits arch_kernel_obj.splits)
-  apply (rule conjI)
-   apply (clarsimp simp: ekheap_relation_def pspace_relation_def)
-   apply (drule_tac x=p in bspec, erule domI)
-   apply (simp add: other_obj_relation_def
-           split: Structures_A.kernel_object.splits)
   apply (extract_conjunct \<open>match conclusion in "ghost_relation _ _ _ _" \<Rightarrow> -\<close>)
    apply (clarsimp simp add: ghost_relation_def)
    apply (erule_tac x="p && ~~ mask (pt_bits (pt_type pt))" in allE)+

proof/refine/AARCH64/Arch_R.thy

@@ -96,24 +96,6 @@ lemma createObject_typ_at':
   apply (clarsimp simp: is_aligned_no_overflow_mask)
   done
 
-lemma retype_region2_ext_retype_region_ArchObject:
-  "retype_region ptr n us (ArchObject x)=
-  retype_region2 ptr n us (ArchObject x)"
-  apply (rule ext)
-  apply (simp add: retype_region_def retype_region2_def bind_assoc
-                   retype_region2_ext_def retype_region_ext_def default_ext_def)
-  apply (rule ext)
-  apply (intro monad_eq_split_tail ext)+
-     apply simp
-    apply simp
-   apply (simp add:gets_def get_def bind_def return_def simpler_modify_def )
-   apply (rule_tac x = xc in fun_cong)
-   apply (rule_tac f = do_extended_op in arg_cong)
-   apply (rule ext)
-   apply simp
-  apply simp
-  done
-
 lemma set_cap_device_and_range_aligned:
   "is_aligned ptr sz \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace>
     set_cap
@@ -165,7 +147,6 @@ lemma performASIDControlInvocation_corres:
             apply (clarsimp simp:is_cap_simps)
            apply (simp add: free_index_of_def)
           apply (rule corres_split)
-             apply (simp add: retype_region2_ext_retype_region_ArchObject )
              apply (rule corres_retype [where ty="Inl (KOArch (KOASIDPool F))" for F,
                                         unfolded APIType_map2_def makeObjectKO_def,
                                         THEN createObjects_corres',simplified,
@@ -315,9 +296,8 @@ lemma performASIDControlInvocation_corres:
    apply (rule conjI, rule pspace_no_overlap_subset,
          rule pspace_no_overlap_detype[OF caps_of_state_valid])
         apply (simp add:invs_psp_aligned invs_valid_objs is_aligned_neg_mask_eq)+
-   apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def
-                         st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def
-                         wrap_ext_det_ext_ext_def)
+   apply (clarsimp simp: detype_def clear_um_def valid_sched_def
+                         st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def)
   apply (simp add: detype_def clear_um_def)
   apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation])
     apply (simp add:invs_valid_objs)+