sys-init: repair proofs for 64-bit-clean spec

The new use of word_bits and "of_nat word_bits" in the spec breaks the
system initialiser proofs. Fix that breakage.

Does not include general 64-bit cleanup of the proofs.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Author: lsf37

sys-init/CreateIRQCaps_SI.thy

@@ -5,13 +5,13 @@
  *)
 
 theory CreateIRQCaps_SI
-imports
-  DSpecProofs.IRQ_DP
-  ObjectInitialised_SI
-  RootTask_SI
-  SysInit_SI
-  Mapped_Separating_Conjunction
-  Sep_Algebra.Sep_Fold_Cancel
+  imports
+    DSpecProofs.IRQ_DP
+    ObjectInitialised_SI
+    RootTask_SI
+    SysInitSpec.SysInit_SI
+    Mapped_Separating_Conjunction
+    Sep_Algebra.Sep_Fold_Cancel
 begin
 
 (*****************
@@ -151,7 +151,7 @@ lemma create_irq_cap_sep:
   apply (wp add: hoare_drop_imp sep_wp: seL4_IRQHandler_IRQControl_Get, simp)
   apply (rule conjI)
    apply sep_solve
-  apply (simp add: offset_slot_si_cnode_size' guard_equal_si_cspace_cap word_bits_def)
+  apply (simp add: offset_slot_si_cnode_size' guard_equal_si_cspace_cap)
   done
 
 lemma well_formed_spec_used_irqs_compute:

sys-init/CreateObjects_SI.thy

@@ -5,15 +5,15 @@
  *)
 
 theory CreateObjects_SI
-imports
-  StaticDerivations_SI
-  ObjectInitialised_SI
-  RootTask_SI
-  SysInit_SI
-  Sep_Algebra.Extended_Separation_Algebra
-  Sep_Algebra.Sep_Util
-  Sep_Algebra.Sep_Fold_Cancel
-  Mapped_Separating_Conjunction
+  imports
+    StaticDerivations_SI
+    ObjectInitialised_SI
+    RootTask_SI
+    SysInitSpec.SysInit_SI
+    Sep_Algebra.Extended_Separation_Algebra
+    Sep_Algebra.Sep_Util
+    Sep_Algebra.Sep_Fold_Cancel
+    Mapped_Separating_Conjunction
 begin
 
 lemma has_children_map_le:
@@ -65,7 +65,8 @@ lemma retype_untyped_wp_no_children:
                                                root_size=si_cnode_size and
                                                obj = new_object and
                                                obj_range=cover_ids and
-                                               tcb="obj_tcb root_tcb"]])
+                                               tcb="obj_tcb root_tcb",
+                            folded word_bits_num]])
                apply (fastforce)+
          apply (assumption
                 | simp add: unat_of_nat32
@@ -127,7 +128,8 @@ lemma retype_untyped_wp_has_children:
                                                dev = dev and
                                                obj = new_object and
                                                obj_range = cover_ids and
-                                               tcb = "obj_tcb root_tcb"]])
+                                               tcb = "obj_tcb root_tcb"],
+                            folded word_bits_num])
              apply (fastforce)+
          apply (simp add: unat_of_nat32 | rule offset_slot'[symmetric] guard_equal_si_cnode_cap)+
     apply (clarsimp)

sys-init/DuplicateCaps_SI.thy

@@ -5,11 +5,11 @@
  *)
 
 theory DuplicateCaps_SI
-imports
-  "DSpecProofs.CNode_DP"
-  ObjectInitialised_SI
-  RootTask_SI
-  SysInit_SI
+  imports
+    DSpecProofs.CNode_DP
+    ObjectInitialised_SI
+    RootTask_SI
+    SysInitSpec.SysInit_SI
 begin
 
 lemma sep_map_zip_fst:
@@ -67,8 +67,8 @@ lemma seL4_CNode_Copy_sep_helper:
        (si_cnode_id, unat cap_ptr) \<mapsto>c default_cap (object_type obj) {kobj_id}
                                                      (object_size_bits obj) dev \<and>*
        (si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>* R\<guillemotright> s\<rbrace>
-    seL4_CNode_Copy seL4_CapInitThreadCNode free_cptr 32
-                    seL4_CapInitThreadCNode cap_ptr 32 UNIV
+    seL4_CNode_Copy seL4_CapInitThreadCNode free_cptr (of_nat word_bits)
+                    seL4_CapInitThreadCNode cap_ptr (of_nat word_bits) UNIV
   \<lbrace>\<lambda>rv.\<guillemotleft>si_tcb_id \<mapsto>f root_tcb \<and>*
        (si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
        (si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
@@ -90,7 +90,7 @@ lemma seL4_CNode_Copy_sep_helper:
    apply (rule conjI)
     apply sep_solve
    apply (clarsimp simp: guard_equal_si_cspace_cap
-                         guard_equal_si_cnode_cap word_bits_def)
+                         guard_equal_si_cnode_cap)
   apply (simp add: well_formed_update_cap_rights_idem derived_cap_default)
   apply sep_solve
   done

sys-init/InitCSpace_SI.thy

@@ -5,12 +5,12 @@
  *)
 
 theory InitCSpace_SI
-imports
-  "DSpecProofs.CNode_DP"
-  ObjectInitialised_SI
-  RootTask_SI
-  SysInit_SI
-  Mapped_Separating_Conjunction
+  imports
+    DSpecProofs.CNode_DP
+    ObjectInitialised_SI
+    RootTask_SI
+    SysInitSpec.SysInit_SI
+    Mapped_Separating_Conjunction
 begin
 
 (*********************
@@ -48,7 +48,7 @@ lemma irqhandler_cap_cap_irq [simp]:
 
 lemma InitThreadCNode_guard_equal[simp]:
   "guard_equal si_cspace_cap seL4_CapInitThreadCNode word_bits"
-  apply (clarsimp simp:seL4_CapInitThreadCNode_def word_bits_def)
+  apply (clarsimp simp:seL4_CapInitThreadCNode_def)
   apply (rule guard_equal_si_cspace_cap)
   apply (simp add:si_cnode_size_def)
   done
@@ -341,7 +341,7 @@ lemma mint_pre:
    src_root = seL4_CapInitThreadCNode;
    Some src_index = orig_caps (cap_object spec_cap);
    src_index < 2 ^ si_cnode_size;
-   src_depth = (32::word32);
+   src_depth = (of_nat word_bits::word32);
 
    rights = cap_rights spec_cap;
 
@@ -388,8 +388,8 @@ lemma mint_pre:
       R\<guillemotright> s \<and>
 
      \<comment> \<open>Cap slots match their cptrs.\<close>
-     one_lvl_lookup si_cspace_cap 32 si_cnode_size \<and>
-     one_lvl_lookup si_cspace_cap 32 si_cnode_size \<and>
+     one_lvl_lookup si_cspace_cap (of_nat word_bits) si_cnode_size \<and>
+     one_lvl_lookup si_cspace_cap (of_nat word_bits) si_cnode_size \<and>
      one_lvl_lookup si_cspace_cap (unat src_depth) si_cnode_size \<and>
      one_lvl_lookup dest_root_cap (unat dest_depth) dest_size \<and>
 
@@ -503,8 +503,8 @@ lemma move_pre_irq_handler:
       R\<guillemotright> s \<and>
 
      \<comment> \<open>Cap slots match their cptrs.\<close>
-     one_lvl_lookup si_cspace_cap 32 si_cnode_size \<and>
-     one_lvl_lookup si_cspace_cap 32 si_cnode_size \<and>
+     one_lvl_lookup si_cspace_cap word_bits si_cnode_size \<and>
+     one_lvl_lookup si_cspace_cap word_bits si_cnode_size \<and>
      one_lvl_lookup si_cspace_cap (unat src_depth) si_cnode_size \<and>
      one_lvl_lookup dest_root_cap (unat dest_depth) dest_size \<and>
 
@@ -804,7 +804,7 @@ lemma seL4_CNode_Mutate_object_slot_initialised_sep_helper:
      si_cap_at t dup_caps spec dev obj_id \<and>*
      object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> \<rbrace>
    seL4_CNode_Mutate dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                     seL4_CapInitThreadCNode src_index 32 data
+                     seL4_CapInitThreadCNode src_index (of_nat word_bits) data
    \<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
         si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
         si_cap_at t dup_caps spec dev obj_id \<and>*
@@ -815,11 +815,12 @@ lemma seL4_CNode_Mutate_object_slot_initialised_sep_helper:
                 and dest_root_cap = "default_cap CNodeType {dest_id} (object_size_bits spec_obj) False"
                 and root_size=si_cnode_size
                 and src_root=seL4_CapInitThreadCNode
-                and src_depth=32
+                and src_depth="of_nat word_bits"
                 and tcb=root_tcb
                 and src_cap = "default_cap type {client_object_id} (object_size_bits spec_cap_obj) dev"
                 in seL4_CNode_Mutate_sep[where
-                R = "(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>* si_asid \<and>* R"])
+                R = "(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>* si_asid \<and>* R",
+                folded word_bits_num])
     apply (assumption|simp add: ep_related_cap_default_cap
                  default_cap_has_type valid_src_cap_if_cnode
                  get_index_def)+
@@ -832,7 +833,7 @@ lemma seL4_CNode_Mutate_object_slot_initialised_sep_helper:
           simp_all add: has_type_default_not_non ep_related_cap_default_cap)
       apply (thin_tac "\<guillemotleft>P \<and>* Q \<guillemotright>s" for P Q)
       apply sep_solve
-     apply ((clarsimp simp: si_cnode_cap_def word_bits_def si_cspace_cap_def
+     apply ((clarsimp simp: si_cnode_cap_def si_cspace_cap_def
                        dest!: guard_equal_si_cspace_cap |
                rule is_cnode_cap_si_cnode_cap)+)[2]
          (* it works because si_cnode_cap = si_cspace_cap *)
@@ -869,7 +870,7 @@ lemma seL4_CNode_Move_object_slot_initialised_cap_has_object_sep_helper:
      si_cap_at t dup_caps spec dev obj_id \<and>*
      object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> \<rbrace>
    seL4_CNode_Move dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                     seL4_CapInitThreadCNode src_index 32
+                     seL4_CapInitThreadCNode src_index (of_nat word_bits)
    \<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
         si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
         si_cap_at t dup_caps spec dev obj_id \<and>*
@@ -880,7 +881,7 @@ lemma seL4_CNode_Move_object_slot_initialised_cap_has_object_sep_helper:
               and dest_root_cap = "default_cap CNodeType {dest_id} (object_size_bits spec_obj) False"
               and root_size=si_cnode_size
               and src_root=seL4_CapInitThreadCNode
-              and src_depth=32
+              and src_depth="of_nat word_bits"
               and tcb=root_tcb
               and src_cap = "default_cap type {client_object_id} (object_size_bits spec_cap_obj) dev"
                in seL4_CNode_Move_sep[where
@@ -896,7 +897,7 @@ lemma seL4_CNode_Move_object_slot_initialised_cap_has_object_sep_helper:
      simp_all add:has_type_default_not_non ep_related_cap_default_cap)
       apply (thin_tac "\<guillemotleft>P \<and>* Q \<guillemotright>s" for P Q)
       apply sep_solve
-     apply ((clarsimp simp: si_cnode_cap_def word_bits_def si_cspace_cap_def
+     apply ((clarsimp simp: si_cnode_cap_def si_cspace_cap_def
                        dest!: guard_equal_si_cspace_cap |
                rule is_cnode_cap_si_cnode_cap)+)[2]
          (* it works because si_cnode_cap = si_cspace_cap *)
@@ -926,7 +927,7 @@ lemma seL4_CNode_Move_object_slot_initialised_irqhandler_cap_sep_helper:
      si_cap_at t dup_caps spec False obj_id \<and>*
      object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> \<rbrace>
    seL4_CNode_Move dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                     seL4_CapInitThreadCNode src_index 32
+                     seL4_CapInitThreadCNode src_index (of_nat word_bits)
    \<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
         si_null_irq_cap_at irq_caps spec (cap_irq spec_cap) \<and>*
         si_cap_at t dup_caps spec dev obj_id \<and>*
@@ -937,7 +938,7 @@ lemma seL4_CNode_Move_object_slot_initialised_irqhandler_cap_sep_helper:
               and dest_root_cap = "default_cap CNodeType {dest_id} (object_size_bits spec_obj) False"
               and root_size=si_cnode_size
               and src_root=seL4_CapInitThreadCNode
-              and src_depth=32
+              and src_depth="of_nat word_bits"
               and tcb=root_tcb
               and src_cap = " IrqHandlerCap (cap_irq spec_cap)"
                in seL4_CNode_Move_sep[where
@@ -952,9 +953,9 @@ lemma seL4_CNode_Move_object_slot_initialised_irqhandler_cap_sep_helper:
           simp_all add:has_type_default_not_non ep_related_cap_default_cap)
       apply (thin_tac "\<guillemotleft>P \<and>* Q \<guillemotright>s" for P Q)
       apply (sep_solve add: sep_any_imp)
-     apply ((clarsimp simp: si_cnode_cap_def word_bits_def si_cspace_cap_def
+     apply ((clarsimp simp: si_cnode_cap_def si_cspace_cap_def
                      dest!: guard_equal_si_cspace_cap |
-               rule is_cnode_cap_si_cnode_cap)+)[2]
+               rule is_cnode_cap_si_cnode_cap)+)[3]
          (* it works because si_cnode_cap = si_cspace_cap *)
   apply (drule_tac s=s and dest_root=dest_root and src_index=src_index and R=R
                 in move_post_irq_handler, (assumption|simp)+)
@@ -977,7 +978,7 @@ lemma seL4_CNode_Move_object_slot_initialised_cap_has_object_sep:
          si_cap_at t dup_caps spec dev obj_id \<and>*
          object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s\<rbrace>
      seL4_CNode_Move dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                     seL4_CapInitThreadCNode src_index 32
+                     seL4_CapInitThreadCNode src_index (of_nat word_bits)
    \<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
         si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
         si_cap_at t dup_caps spec dev obj_id \<and>*
@@ -1014,7 +1015,7 @@ lemma seL4_CNode_Move_object_slot_initialised_irqhandler_cap_sep:
          si_cap_at t dup_caps spec False obj_id \<and>*
          object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s\<rbrace>
      seL4_CNode_Move dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                     seL4_CapInitThreadCNode src_index 32
+                     seL4_CapInitThreadCNode src_index (of_nat word_bits)
    \<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
         si_null_irq_cap_at irq_caps spec (cap_irq spec_cap) \<and>*
         si_cap_at t dup_caps spec False obj_id \<and>*
@@ -1043,7 +1044,7 @@ lemma seL4_CNode_Move_object_slot_initialised_irqhandler_cap_sep_new:
         Some dest_root = dup_caps obj_id \<and>
         Some src_index = irq_caps (cap_irq spec_cap))\<rbrace>
      seL4_CNode_Move dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                     seL4_CapInitThreadCNode src_index 32
+                     seL4_CapInitThreadCNode src_index (of_nat word_bits)
    \<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
         si_null_irq_cap_at irq_caps spec (cap_irq spec_cap) \<and>*
         si_cap_at t dup_caps spec False obj_id \<and>*
@@ -1075,7 +1076,7 @@ lemma seL4_CNode_Mutate_object_slot_initialised_sep:
          si_cap_at t dup_caps spec dev obj_id \<and>*
          object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s \<rbrace>
       seL4_CNode_Mutate dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                     seL4_CapInitThreadCNode src_index 32 data
+                     seL4_CapInitThreadCNode src_index (of_nat word_bits) data
    \<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
         si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
         si_cap_at t dup_caps spec dev obj_id \<and>*
@@ -1387,7 +1388,7 @@ lemma seL4_CNode_Mint_object_slot_initialised_sep_helper:
      si_cap_at t dup_caps spec dev obj_id \<and>*
      object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> \<rbrace>
    seL4_CNode_Mint dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                   seL4_CapInitThreadCNode src_index 32 rights data
+                   seL4_CapInitThreadCNode src_index (of_nat word_bits) rights data
    \<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
         si_cap_at t orig_caps spec dev (cap_object spec_cap) \<and>*
         si_cap_at t dup_caps spec dev obj_id \<and>*
@@ -1399,7 +1400,7 @@ lemma seL4_CNode_Mint_object_slot_initialised_sep_helper:
               and dest_root_cap = "default_cap CNodeType {dest_id} (object_size_bits spec_obj) False"
               and root_size=si_cnode_size
               and src_root=seL4_CapInitThreadCNode
-              and src_depth=32
+              and src_depth="of_nat word_bits"
               and tcb=root_tcb
               and src_cap = "default_cap type {client_object_id} (object_size_bits spec_cap_obj) dev"
                in seL4_CNode_Mint_sep,
@@ -1452,7 +1453,7 @@ lemma seL4_CNode_Mint_object_slot_initialised_sep:
          si_cap_at t dup_caps spec dev obj_id \<and>*
          object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s \<rbrace>
      seL4_CNode_Mint dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
-                     seL4_CapInitThreadCNode src_index 32 rights data
+                     seL4_CapInitThreadCNode src_index (of_nat word_bits) rights data
    \<lbrace>\<lambda>_ s. \<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
            si_cap_at t orig_caps spec dev (cap_object spec_cap) \<and>*
            si_cap_at t dup_caps spec dev obj_id \<and>*

sys-init/InitIRQ_SI.thy

@@ -5,11 +5,11 @@
  *)
 
 theory InitIRQ_SI
-imports
-  "DSpecProofs.IRQ_DP"
-  ObjectInitialised_SI
-  RootTask_SI
-  SysInit_SI
+  imports
+    DSpecProofs.IRQ_DP
+    ObjectInitialised_SI
+    RootTask_SI
+    SysInitSpec.SysInit_SI
 begin
 
 lemma seL4_IRQHandler_SetEndpoint_irq_initialised_helper_sep:

sys-init/InitTCB_SI.thy

@@ -5,12 +5,11 @@
  *)
 
 theory InitTCB_SI
-imports
-  "DSpecProofs.KHeap_DP"
-  "DSpecProofs.TCB_DP"
-  ObjectInitialised_SI
-  RootTask_SI
-  SysInit_SI
+  imports
+    DSpecProofs.TCB_DP
+    ObjectInitialised_SI
+    RootTask_SI
+    SysInitSpec.SysInit_SI
 begin
 
 lemma cap_has_type_cap_has_object [simp]: