From 6f347e3fc4a07009adc5a34c5a427396e1b074fc Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Fri, 8 Nov 2024 15:54:45 +1100
Subject: [PATCH] squash aspec: review feedback and other arches

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 spec/abstract/ARM/Init_A.thy     | 9 +++++++++
 spec/abstract/ARM_HYP/Init_A.thy | 9 +++++++++
 spec/abstract/RISCV64/Init_A.thy | 9 +++++++++
 spec/abstract/Structures_A.thy   | 3 +--
 spec/abstract/Tcb_A.thy          | 2 +-
 spec/abstract/X64/Init_A.thy     | 9 +++++++++
 6 files changed, 38 insertions(+), 3 deletions(-)

diff --git a/spec/abstract/ARM/Init_A.thy b/spec/abstract/ARM/Init_A.thy
index 2872ed1276..aec20c6802 100644
--- a/spec/abstract/ARM/Init_A.thy
+++ b/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,
diff --git a/spec/abstract/ARM_HYP/Init_A.thy b/spec/abstract/ARM_HYP/Init_A.thy
index e87c2dd6cd..6e43b278a0 100644
--- a/spec/abstract/ARM_HYP/Init_A.thy
+++ b/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,
diff --git a/spec/abstract/RISCV64/Init_A.thy b/spec/abstract/RISCV64/Init_A.thy
index 42bb63a180..f8f527d8cd 100644
--- a/spec/abstract/RISCV64/Init_A.thy
+++ b/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,
diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy
index 1c9c17d636..32088edd49 100644
--- a/spec/abstract/Structures_A.thy
+++ b/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)
diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy
index 51aa1bddd6..95b47cbb09 100644
--- a/spec/abstract/Tcb_A.thy
+++ b/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"
diff --git a/spec/abstract/X64/Init_A.thy b/spec/abstract/X64/Init_A.thy
index c0dd40f3a4..38fddc30aa 100644
--- a/spec/abstract/X64/Init_A.thy
+++ b/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,