spec+proof+sysinit: refactor tcb_slots

This updates the TCB cap slots in the CapDL specification to match the
output of the CapDL-tool. It also provides a new definition to hide
these details and improve maintainability.

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

proof/dpolicy/Dpolicy.thy

@@ -473,7 +473,7 @@ lemma thread_bound_ntfns_transform:
   apply (rule_tac cap="infer_tcb_bound_notification (tcb_bound_notification a)" in csta_caps[where ptr="(oref, tcb_boundntfn_slot)"
                           and auth=auth and oref=oref' and s="transform s", simplified])
     apply (unfold tcb_boundntfn_slot_def)
-    apply (rule opt_cap_tcb[where sl=6, unfolded tcb_boundntfn_slot_def tcb_pending_op_slot_def tcb_slot_defs, simplified])
+    apply (rule opt_cap_tcb[where sl=tcb_boundntfn_slot, unfolded tcb_slot_defs, simplified])
       apply simp
      apply simp
     apply (rule notI, drule invs_valid_idle, simp add:valid_idle_def pred_tcb_def2)

proof/sep-capDL/Helpers_SD.thy

@@ -947,7 +947,7 @@ where
   | PageTable _ \<Rightarrow> [0..<2^pt_size]
   | AsidPool _ \<Rightarrow> [0..<2^asid_low_bits]
   | CNode cnode \<Rightarrow> [0..<2^(cdl_cnode_size_bits cnode)]
-  | Tcb _ \<Rightarrow> [0..<tcb_boundntfn_slot + 1]
+  | Tcb _ \<Rightarrow> tcb_slots_list
   | IRQNode _ \<Rightarrow> [0]
   | _ \<Rightarrow> []"
 

spec/capDL/Types_D.thy

@@ -283,14 +283,21 @@ definition
 (*
  * Each TCB contains a number of cap slots, each with a specific
  * purpose. These constants define the purpose of each slot.
+ *
+ * The specific list of slots is chosen to be consistent with the output
+ * of the CapDL-tool.
  *)
 definition "tcb_cspace_slot     = (0 :: cdl_cnode_index)"
 definition "tcb_vspace_slot     = (1 :: cdl_cnode_index)"
 definition "tcb_replycap_slot   = (2 :: cdl_cnode_index)"
 definition "tcb_caller_slot     = (3 :: cdl_cnode_index)"
 definition "tcb_ipcbuffer_slot  = (4 :: cdl_cnode_index)"
 definition "tcb_pending_op_slot = (5 :: cdl_cnode_index)"
-definition "tcb_boundntfn_slot  = (6 :: cdl_cnode_index)"
+definition "tcb_boundntfn_slot  = (8 :: cdl_cnode_index)"
+
+definition "tcb_slots_list \<equiv> [0..<tcb_pending_op_slot + 1] @ [tcb_boundntfn_slot]"
+abbreviation "tcb_slots \<equiv> set tcb_slots_list"
+lemmas tcb_slots_def = tcb_slots_list_def
 
 lemmas tcb_slot_defs =
   tcb_cspace_slot_def
@@ -300,6 +307,7 @@ lemmas tcb_slot_defs =
   tcb_ipcbuffer_slot_def
   tcb_pending_op_slot_def
   tcb_boundntfn_slot_def
+  tcb_slots_list_def
 
 (*
  * Getters and setters for various data types.
@@ -610,7 +618,7 @@ definition
   default_tcb :: "word8 \<Rightarrow> cdl_tcb"
 where
   "default_tcb current_domain = \<lparr>
-    cdl_tcb_caps = \<lambda>n. if n \<le> tcb_boundntfn_slot then Some NullCap else None,
+    cdl_tcb_caps = \<lambda>n. if n \<in> tcb_slots then Some NullCap else None,
     cdl_tcb_fault_endpoint = 0,
     cdl_tcb_intent = \<lparr>
       cdl_intent_op = None,

sys-init/InitTCB_SI.thy

@@ -36,12 +36,12 @@ lemma tcb_empty_decomp:
   apply (clarsimp simp: is_tcb_def object_default_state_def2)
   apply (case_tac obj, simp_all)
   apply (subst sep_map_o_decomp)
-  apply (subst sep_map_S_decomp_list [where slots = "[0 .e. tcb_boundntfn_slot]"])
-    apply (force simp: default_tcb_def object_slots_def)
-   apply clarsimp
+  apply (subst sep_map_S_decomp_list [where slots = tcb_slots_list])
+    apply (clarsimp simp: dom_object_slots_default_tcb)
+   apply (clarsimp simp: tcb_slot_defs)
   apply (clarsimp simp: sep_list_conj_def default_tcb_slots object_domain_def tcb_slot_defs)
   apply (subst sep_map_s_sep_map_c_eq,
-         simp add: default_tcb_def object_slots_def tcb_boundntfn_slot_def,
+         simp add: default_tcb_def object_slots_def tcb_slot_defs,
          clarsimp simp: sep_conj_ac)+
   done
 
@@ -69,11 +69,9 @@ lemma tcb_decomp':
   apply (clarsimp simp: is_tcb_def object_domain_def object_default_state_def2)
   apply (case_tac obj, simp_all)
   apply (subst sep_map_o_decomp)
-  apply (subst sep_map_S_decomp_list [where slots = "[0 .e. tcb_boundntfn_slot]"])
-    apply (drule (1) well_formed_object_slots, simp add: foo)
-    apply (force simp: object_default_state_def2 default_tcb_def object_slots_def
-                split: cdl_object.splits)
-   apply clarsimp
+  apply (subst sep_map_S_decomp_list [where slots = tcb_slots_list])
+    apply (clarsimp simp: dom_object_slots_default_tcb)
+   apply (clarsimp simp: tcb_slot_defs)
   apply (clarsimp simp: sep_list_conj_def default_tcb_slots tcb_slot_defs)
   apply (drule_tac obj'="Tcb (default_tcb minBound)" and p = k_obj_id in sep_map_E_eq [rotated],
          simp add: object_type_def)
@@ -107,11 +105,9 @@ lemma tcb_half_decomp':
   apply (clarsimp simp: is_tcb_def object_domain_def object_default_state_def2)
   apply (case_tac obj, simp_all)
   apply (subst sep_map_o_decomp)
-  apply (subst sep_map_S_decomp_list [where slots = "[0 .e. tcb_boundntfn_slot]"])
-    apply (drule (1) well_formed_object_slots, simp add: foo)
-    apply (force simp: object_default_state_def2 default_tcb_def object_slots_def
-                split: cdl_object.splits)
-   apply clarsimp
+  apply (subst sep_map_S_decomp_list [where slots = tcb_slots_list])
+    apply (clarsimp simp: dom_object_slots_default_tcb)
+   apply (clarsimp simp: tcb_slot_defs)
   apply (clarsimp simp: sep_list_conj_def default_tcb_slots tcb_slot_defs)
   apply (drule_tac obj'="Tcb (default_tcb minBound)" and p = k_obj_id in sep_map_E_eq [rotated],
          simp add: object_type_def)

sys-init/ObjectInitialised_SI.thy

@@ -629,6 +629,10 @@ lemma intent_reset_cnode:
   \<Longrightarrow> obj = obj'"
   by (clarsimp simp: intent_reset_def object_type_def split: cdl_object.splits)
 
+lemma zero_in_tcb_slots[simp]:
+  "0 \<in> tcb_slots"
+  by (simp add: tcb_slot_defs)
+
 lemma intent_reset_object_slots_NullCap:
   "\<lbrakk>intent_reset (object_default_state obj) = intent_reset obj';
    slot < 2 ^ object_size_bits obj; has_slots obj\<rbrakk>

sys-init/RootTask_SI.thy

@@ -629,13 +629,12 @@ lemma slots_tcb:
    slot = 3 \<or>
    slot = 4 \<or>
    slot = 5 \<or>
-   slot = 6"
+   slot = 8"
   apply (frule (1) well_formed_object_slots)
   apply (drule (1) well_formed_well_formed_tcb)
   apply (clarsimp simp: well_formed_tcb_def opt_cap_def slots_of_def)
   apply (drule (1) dom_eqD)
-  apply (clarsimp simp: object_default_state_def2 dom_object_slots_default_tcb
-                        tcb_pending_op_slot_def tcb_boundntfn_slot_def)
+  apply (clarsimp simp: object_default_state_def2 dom_object_slots_default_tcb tcb_slot_defs)
   done
 
 lemma object_at_dom_cdl_objects:

sys-init/WellFormed_SI.thy

@@ -403,7 +403,7 @@ lemma well_formed_finite [elim!]:
   apply (clarsimp simp: slots_of_def split: option.splits)
   apply (rename_tac obj)
   apply (drule_tac t="dom (object_slots obj)" in sym) (* Makes rewriting work. *)
-  apply (clarsimp simp: object_default_state_def2 object_slots_def
+  apply (clarsimp simp: object_default_state_def2 object_slots_def dom_expand
                         default_tcb_def tcb_pending_op_slot_def
                         empty_cnode_def empty_irq_node_def empty_cap_map_def
                  split: cdl_object.splits)
@@ -417,7 +417,7 @@ lemma well_formed_finite_object_slots:
 
 lemma well_formed_distinct_slots_of_list [elim!]:
   "well_formed spec \<Longrightarrow> distinct (slots_of_list spec obj_id)"
-  by (clarsimp simp: slots_of_list_def object_slots_list_def
+  by (clarsimp simp: slots_of_list_def object_slots_list_def tcb_slot_defs
                split: option.splits cdl_object.splits)
 
 lemma well_formed_object_size_bits:
@@ -578,8 +578,9 @@ lemma well_formed_cnode_object_size_bits_eq:
   apply (clarsimp simp: is_cnode_def  well_formed_cap_to_object_def)
   done
 
-lemma slots_of_set_helper: "\<lbrakk>{0..n :: nat} = dom f; f x \<noteq> None; m = n + 1\<rbrakk> \<Longrightarrow> x < m"
-  by (subgoal_tac "x \<le> n"; fastforce)
+lemma dom_cdl_tcb_caps_default_tcb:
+ "dom (cdl_tcb_caps (default_tcb domain)) = tcb_slots"
+  by (auto simp: object_slots_def default_tcb_def dom_expand tcb_slots_def)
 
 lemma slots_of_set [simp]:
   "well_formed spec \<Longrightarrow> set (slots_of_list spec obj_id) = dom (slots_of obj_id spec)"
@@ -590,9 +591,8 @@ lemma slots_of_set [simp]:
   apply (erule_tac x=obj in allE)
   apply (intro set_eqI iffI)
   by (fastforce simp: object_default_state_def2 object_slots_def object_slots_list_def
-                      default_tcb_def empty_cnode_def empty_irq_node_def empty_cap_map_def
-                      pt_size_def pd_size_def tcb_boundntfn_slot_def
-                elim: slots_of_set_helper
+                      dom_cdl_tcb_caps_default_tcb empty_cnode_def empty_irq_node_def empty_cap_map_def
+                      pt_size_def pd_size_def
                 split: cdl_object.splits)+
 
 lemma well_formed_well_formed_tcb:
@@ -890,8 +890,8 @@ lemma well_formed_cap_to_non_empty_pt:
   done
 
 lemma dom_object_slots_default_tcb:
- "dom (object_slots (Tcb (default_tcb domain))) = {0..tcb_boundntfn_slot}"
-  by (clarsimp simp: object_slots_def default_tcb_def)
+  "dom (object_slots (Tcb (default_tcb domain))) = tcb_slots"
+  by (clarsimp simp: object_slots_def dom_cdl_tcb_caps_default_tcb)
 
 lemma well_formed_tcb_has_fault:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some (Tcb tcb)\<rbrakk>
@@ -920,7 +920,7 @@ lemma well_formed_object_domain:
 
 lemma well_formed_tcb_object_slots:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some tcb; is_tcb tcb\<rbrakk>
-   \<Longrightarrow> dom (object_slots tcb) = {0..tcb_boundntfn_slot}"
+   \<Longrightarrow> dom (object_slots tcb) = tcb_slots"
   apply (frule (1) well_formed_object_slots)
   apply (clarsimp simp: object_default_state_def2 is_tcb_def split: cdl_object.splits)
   apply (rule dom_object_slots_default_tcb)
@@ -948,7 +948,7 @@ lemma well_formed_tcb_cspace_cap:
    apply (erule well_formed_cap_object [where obj_id=obj_id and slot=tcb_cspace_slot])
     apply (simp add: opt_cap_def slots_of_def)
    apply (clarsimp simp: cap_has_object_def cap_type_def split: cdl_cap.splits)
-  apply (auto simp: dom_def tcb_pending_op_slot_def tcb_cspace_slot_def)
+  apply (auto simp: dom_def tcb_slot_defs)
   done
 
 lemma cap_data_cap_guard_size_0:
@@ -980,13 +980,13 @@ lemma well_formed_tcb_cspace_cap_cap_data:
   done
 
 lemma well_formed_tcb_opt_cap:
-  "\<lbrakk>well_formed spec; tcb_at obj_id spec; slot \<in> {0..tcb_boundntfn_slot}\<rbrakk>
+  "\<lbrakk>well_formed spec; tcb_at obj_id spec; slot \<in> tcb_slots\<rbrakk>
    \<Longrightarrow> \<exists>cap. opt_cap (obj_id, slot) spec = Some cap"
   apply (clarsimp simp: object_at_def)
   apply (drule (1) well_formed_object_slots)
   apply (fastforce simp: object_default_state_def2 is_tcb_def
                          opt_cap_def slots_of_def object_slots_def
-                         default_tcb_def dom_def tcb_pending_op_slot_def
+                         default_tcb_def dom_def
                   split: cdl_object.splits if_split_asm)
   done