squash aspec: review feedback and other arches

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

spec/abstract/ARM/Init_A.thy

@@ -74,6 +74,9 @@ definition
     tcb_fault = None,
     tcb_bound_notification = None,
     tcb_mcpriority = minBound,
+    tcb_priority = 0,
+    tcb_time_slice = timeSlice,
+    tcb_domain = 0,
     tcb_arch = init_arch_tcb
   \<rparr>,
   init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), \<comment> \<open>same reason as why we kept the definition of @{term init_globals_frame}\<close>
@@ -95,6 +98,12 @@ definition
     is_original_cap = init_ioc,
     cur_thread = idle_thread_ptr,
     idle_thread = idle_thread_ptr,
+    scheduler_action = resume_cur_thread,
+    domain_list = [(0,15)],
+    domain_index = 0,
+    cur_domain = 0,
+    domain_time = 15,
+    ready_queues = const (const []),
     machine_state = init_machine_state,
     interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (ucast irq << cte_level_bits),
     interrupt_states = \<lambda>_. Structures_A.IRQInactive,

spec/abstract/ARM_HYP/Init_A.thy

@@ -76,6 +76,9 @@ definition
     tcb_fault = None,
     tcb_bound_notification = None,
     tcb_mcpriority = minBound,
+    tcb_priority = 0,
+    tcb_time_slice = timeSlice,
+    tcb_domain = 0,
     tcb_arch = init_arch_tcb
   \<rparr>,
   us_global_pd_ptr \<mapsto> us_global_pd)"
@@ -95,6 +98,12 @@ definition
     is_original_cap = init_ioc,
     cur_thread = idle_thread_ptr,
     idle_thread = idle_thread_ptr,
+    scheduler_action = resume_cur_thread,
+    domain_list = [(0,15)],
+    domain_index = 0,
+    cur_domain = 0,
+    domain_time = 15,
+    ready_queues = const (const []),
     machine_state = init_machine_state,
     interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (ucast irq << cte_level_bits),
     interrupt_states = \<lambda>_. Structures_A.IRQInactive,

spec/abstract/RISCV64/Init_A.thy

@@ -111,6 +111,9 @@ definition init_kheap :: kheap
          tcb_fault = None,
          tcb_bound_notification = None,
          tcb_mcpriority = minBound,
+         tcb_priority = 0,
+         tcb_time_slice = timeSlice,
+         tcb_domain = 0,
          tcb_arch = init_arch_tcb
          \<rparr>,
       riscv_global_pt_ptr \<mapsto> init_global_pt
@@ -134,6 +137,12 @@ definition init_A_st :: "'z::state_ext state"
     is_original_cap = init_ioc,
     cur_thread = idle_thread_ptr,
     idle_thread = idle_thread_ptr,
+    scheduler_action = resume_cur_thread,
+    domain_list = [(0,15)],
+    domain_index = 0,
+    cur_domain = 0,
+    domain_time = 15,
+    ready_queues = const (const []),
     machine_state = init_machine_state,
     interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (ucast irq << cte_level_bits),
     interrupt_states = \<lambda>_. IRQInactive,

spec/abstract/Structures_A.thy

@@ -520,8 +520,7 @@ datatype irq_state =
  | IRQTimer
  | IRQReserved
 
-text \<open>The current scheduler action,
-  which is part of the scheduling state.\<close>
+text \<open>The current scheduler action, which is part of the scheduling state.\<close>
 datatype scheduler_action =
     resume_cur_thread
   | switch_thread (sch_act_target : obj_ref)

spec/abstract/Tcb_A.thy

@@ -259,7 +259,7 @@ definition
      thread_set_domain tptr new_dom;
      ts \<leftarrow> get_thread_state tptr;
      when (runnable ts) $ tcb_sched_action tcb_sched_enqueue tptr;
-     when (tptr = cur) $ reschedule_required
+     when (tptr = cur) reschedule_required
    od"
 
 definition invoke_domain:: "obj_ref \<Rightarrow> domain \<Rightarrow> (data list,'z::state_ext) p_monad"

spec/abstract/X64/Init_A.thy

@@ -92,6 +92,9 @@ definition
          tcb_fault = None,
          tcb_bound_notification = None,
          tcb_mcpriority = minBound,
+         tcb_priority = 0,
+         tcb_time_slice = timeSlice,
+         tcb_domain = 0,
          tcb_arch = init_arch_tcb
          \<rparr>,
      init_global_pml4 \<mapsto> ArchObj (PageMapL4 global_pml4),
@@ -114,6 +117,12 @@ definition
     is_original_cap = init_ioc,
     cur_thread = idle_thread_ptr,
     idle_thread = idle_thread_ptr,
+    scheduler_action = resume_cur_thread,
+    domain_list = [(0,15)],
+    domain_index = 0,
+    cur_domain = 0,
+    domain_time = 15,
+    ready_queues = const (const []),
     machine_state = init_machine_state,
     interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (ucast irq << cte_level_bits),
     interrupt_states = \<lambda>_. Structures_A.IRQInactive,