aspec: message_info_to_data is mostly arch independent

Factored out msg_label_bits, which is the only architecture specific part.

proof/drefine/Intent_DR.thy

@@ -1598,10 +1598,10 @@ lemma store_word_corres_helper:
       apply (rule_tac sz = vmpage_size and y = thread in within_page_ipc_buf)
             apply (simp add:ipc_frame_wp_at_def obj_at_def ipc_buffer_wp_at_def)+
       apply (simp add:msg_max_length_def msg_align_bits buffer_cptr_index_def)
-      apply (case_tac "(get_tcb_message_info tcb)")
+      apply (case_tac "get_tcb_message_info tcb")
       apply (clarsimp simp add: get_tcb_message_info_def data_to_message_info_def)
       apply (erule order_less_le_trans)
-      apply simp
+      apply (simp add: mask_def)
       apply (rule iffD1[OF word_le_nat_alt[where b = "0x6::word32",simplified]])
       apply (rule less_less_trans)
        apply (rule  word_and_le1[where a = 3])
@@ -1734,7 +1734,7 @@ lemma dcorres_store_word_safe:
          apply (case_tac "get_tcb_message_info tcb")
          apply (clarsimp simp add: get_tcb_message_info_def data_to_message_info_def)
          apply (erule order_less_le_trans)
-         apply simp
+         apply (simp add: mask_def)
          apply (rule iffD1[OF word_le_nat_alt[where b = "0x6::word32",simplified]])
          apply (rule less_less_trans)
           apply (rule word_and_le1[where a = 3])

proof/drefine/Syscall_DR.thy

@@ -1053,7 +1053,7 @@ lemma reply_from_kernel_error:
      apply (rule exI)
      apply (rule conjI[rotated])
       apply (simp add:obj_at_def)
-     apply (simp add:get_tcb_message_info_def data_to_message_info_def word_neq_0_conv)
+     apply (simp add:get_tcb_message_info_def data_to_message_info_def word_neq_0_conv mask_def)
      apply (simp add:shiftr_over_or_dist le_mask_iff word_neq_0_conv)
      apply (subst shiftl_shiftr_id)
        apply (simp add:word_bits_def mask_def le_mask_iff[symmetric])+

proof/invariant-abstract/ARM/ArchIpc_AI.thy

@@ -118,10 +118,8 @@ lemma is_derived_cap_rights [simp, Ipc_AI_assms]:
 
 lemma data_to_message_info_valid [Ipc_AI_assms]:
   "valid_message_info (data_to_message_info w)"
-  apply (simp add: valid_message_info_def data_to_message_info_def)
-  apply (rule conjI)
-  apply (simp add: word_and_le1 msg_max_length_def msg_max_extra_caps_def Let_def not_less)+
-  done
+  by (simp add: valid_message_info_def data_to_message_info_def  word_and_le1 msg_max_length_def
+                msg_max_extra_caps_def Let_def not_less mask_def)
 
 lemma get_extra_cptrs_length[wp, Ipc_AI_assms]:
   "\<lbrace>\<lambda>s . valid_message_info mi\<rbrace>

proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy

@@ -120,10 +120,8 @@ lemma is_derived_cap_rights [simp, Ipc_AI_assms]:
 
 lemma data_to_message_info_valid [Ipc_AI_assms]:
   "valid_message_info (data_to_message_info w)"
-  apply (simp add: valid_message_info_def data_to_message_info_def)
-  apply (rule conjI)
-  apply (simp add: word_and_le1 msg_max_length_def msg_max_extra_caps_def Let_def not_less)+
-  done
+  by (simp add: valid_message_info_def data_to_message_info_def  word_and_le1 msg_max_length_def
+                msg_max_extra_caps_def Let_def not_less mask_def)
 
 lemma get_extra_cptrs_length[wp, Ipc_AI_assms]:
   "\<lbrace>\<lambda>s . valid_message_info mi\<rbrace>

proof/invariant-abstract/X64/ArchIpc_AI.thy

@@ -120,10 +120,8 @@ lemma is_derived_cap_rights [simp, Ipc_AI_assms]:
 
 lemma data_to_message_info_valid [Ipc_AI_assms]:
   "valid_message_info (data_to_message_info w)"
-  apply (simp add: valid_message_info_def data_to_message_info_def)
-  apply (rule conjI)
-  apply (simp add: word_and_le1 msg_max_length_def msg_max_extra_caps_def Let_def not_less)+
-  done
+  by (simp add: valid_message_info_def data_to_message_info_def  word_and_le1 msg_max_length_def
+                msg_max_extra_caps_def Let_def not_less mask_def)
 
 lemma get_extra_cptrs_length[wp, Ipc_AI_assms]:
   "\<lbrace>\<lambda>s . valid_message_info mi\<rbrace>

proof/refine/ARM/VSpace_R.thy

@@ -2106,10 +2106,9 @@ lemma message_info_to_data_eqv:
 
 lemma message_info_from_data_eqv:
   "message_info_map (data_to_message_info rv) = messageInfoFromWord rv"
-  apply (auto simp add: data_to_message_info_def messageInfoFromWord_def
-    msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def
-    shiftL_nat Let_def not_less msgMaxLength_def msgLabelBits_def)
-  done
+  by (auto simp: data_to_message_info_def messageInfoFromWord_def Let_def not_less
+                 msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def mask_def
+                 shiftL_nat msgMaxLength_def msgLabelBits_def)
 
 lemma set_mi_corres:
  "mi' = message_info_map mi \<Longrightarrow>

proof/refine/ARM_HYP/VSpace_R.thy

@@ -2740,10 +2740,9 @@ lemma message_info_to_data_eqv:
 
 lemma message_info_from_data_eqv:
   "message_info_map (data_to_message_info rv) = messageInfoFromWord rv"
-  apply (auto simp add: data_to_message_info_def messageInfoFromWord_def
-    msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def
-    shiftL_nat Let_def not_less msgMaxLength_def msgLabelBits_def)
-  done
+  by (auto simp: data_to_message_info_def messageInfoFromWord_def Let_def not_less
+                 msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def mask_def
+                 shiftL_nat msgMaxLength_def msgLabelBits_def)
 
 lemma set_mi_corres:
  "mi' = message_info_map mi \<Longrightarrow>

proof/refine/X64/VSpace_R.thy

@@ -1117,19 +1117,15 @@ lemma set_cap_valid_page_map_inv:
 lemma message_info_to_data_eqv:
   "wordFromMessageInfo (message_info_map mi) = message_info_to_data mi"
   apply (cases mi)
-  apply (simp add: wordFromMessageInfo_def
-    msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def
-    shiftL_nat)
+  apply (simp add: wordFromMessageInfo_def msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def shiftL_nat)
   done
 
 lemma message_info_from_data_eqv:
   "message_info_map (data_to_message_info rv) = messageInfoFromWord rv"
   using shiftr_mask_eq[where 'a=64 and n=12]
-  apply (auto simp add: data_to_message_info_def messageInfoFromWord_def
-                        msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def
-                        shiftL_nat Let_def not_less msgMaxLength_def msgLabelBits_def
-                        mask_def word_size)
-  done
+  by (auto simp: data_to_message_info_def messageInfoFromWord_def Let_def not_less
+                 msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def mask_def
+                 shiftL_nat msgMaxLength_def msgLabelBits_def)
 
 lemma set_mi_corres:
  "mi' = message_info_map mi \<Longrightarrow>

spec/abstract/ARM/ArchInvocation_A.thy

@@ -20,26 +20,6 @@ begin
 
 context Arch begin global_naming ARM_A
 
-text {* Message infos are encoded to or decoded from a data word. *}
-primrec
-  message_info_to_data :: "message_info \<Rightarrow> data"
-where
-  "message_info_to_data (MI len exc unw mlabel) =
-   (let
-        extra = exc << 7;
-        unwrapped = unw << 9;
-        label = mlabel << 12
-    in
-       label || extra || unwrapped || len)"
-
-text {* Hard-coded to avoid recursive imports? *}
-definition
-  data_to_message_info :: "data \<Rightarrow> message_info"
-where
-  "data_to_message_info w \<equiv>
-   MI (let v = w && ((1 << 7) - 1) in if v > 120 then 120 else v) ((w >> 7) && ((1 << 2) - 1))
-      ((w >> 9) && ((1 << 3) - 1)) ((w >> 12) && ((1 << 20) - 1))"
-
 text {* These datatypes encode the arguments to the various possible
 ARM-specific system calls. Selectors are defined for various fields
 for convenience elsewhere. *}

spec/abstract/ARM/Machine_A.thy

@@ -107,6 +107,10 @@ definition
   slot_bits :: nat where
   "slot_bits \<equiv> 4"
 
+definition
+  msg_label_bits :: nat where
+  [simp]: "msg_label_bits \<equiv> 20"
+
 type_synonym user_context = "register \<Rightarrow> data"
 
 definition

spec/abstract/ARM_HYP/ArchInvocation_A.thy

@@ -20,26 +20,6 @@ begin
 
 context Arch begin global_naming ARM_A
 
-text {* Message infos are encoded to or decoded from a data word. *}
-primrec
-  message_info_to_data :: "message_info \<Rightarrow> data"
-where
-  "message_info_to_data (MI len exc unw mlabel) =
-   (let
-        extra = exc << 7;
-        unwrapped = unw << 9;
-        label = mlabel << 12
-    in
-       label || extra || unwrapped || len)"
-
-text {* Hard-coded to avoid recursive imports? *}
-definition
-  data_to_message_info :: "data \<Rightarrow> message_info"
-where
-  "data_to_message_info w \<equiv>
-   MI (let v = w && ((1 << 7) - 1) in if v > 120 then 120 else v) ((w >> 7) && ((1 << 2) - 1))
-      ((w >> 9) && ((1 << 3) - 1)) ((w >> 12) && ((1 << 20) - 1))"
-
 text {* These datatypes encode the arguments to the various possible
 ARM-specific system calls. Selectors are defined for various fields
 for convenience elsewhere. *}

spec/abstract/ARM_HYP/Machine_A.thy

@@ -107,6 +107,10 @@ definition
   slot_bits :: nat where
   "slot_bits \<equiv> 4"
 
+definition
+  msg_label_bits :: nat where
+  [simp]: "msg_label_bits \<equiv> 20"
+
 type_synonym user_context = "register \<Rightarrow> data"
 
 definition

spec/abstract/Invocations_A.thy

@@ -25,10 +25,6 @@ requalify_types
   arch_irq_control_invocation
   arch_invocation
 
-requalify_consts
-  message_info_to_data
-  data_to_message_info
-
 end
 
 text {* These datatypes encode the arguments to the available system calls. *}

spec/abstract/Structures_A.thy

@@ -55,6 +55,7 @@ requalify_consts
   aa_type
   untyped_min_bits
   untyped_max_bits
+  msg_label_bits
 end
 
 text {*
@@ -264,28 +265,32 @@ transferred. The @{text mi_label} parameter is transferred directly from sender
 to receiver as part of the message.
 *}
 
-datatype message_info = MI length_type length_type data msg_label
+datatype message_info =
+  MI (mi_length: length_type)
+     (mi_extra_caps: length_type)
+     (mi_caps_unwrapped: data)
+     (mi_label: msg_label)
 
+text {* Message infos are encoded to or decoded from a data word. *}
 primrec
-  mi_label :: "message_info \<Rightarrow> msg_label"
+  message_info_to_data :: "message_info \<Rightarrow> data"
 where
-  "mi_label (MI len exc unw label) = label"
+  "message_info_to_data (MI len exc unw mlabel) =
+   (let
+        extra = exc << 7;
+        unwrapped = unw << 9;
+        label = mlabel << 12
+    in
+       label || extra || unwrapped || len)"
 
-primrec
-  mi_length :: "message_info \<Rightarrow> length_type"
+definition
+  data_to_message_info :: "data \<Rightarrow> message_info"
 where
-  "mi_length (MI len exc unw label) = len"
-
-primrec
-  mi_extra_caps :: "message_info \<Rightarrow> length_type"
-where
-  "mi_extra_caps (MI len exc unw label) = exc"
-
-primrec
-  mi_caps_unwrapped :: "message_info \<Rightarrow> data"
-where
- "mi_caps_unwrapped (MI len exc unw label) = unw"
-
+  "data_to_message_info w \<equiv>
+   MI (let v = w && mask 7 in if v > 120 then 120 else v)
+      ((w >> 7) && mask 2)
+      ((w >> 9) && mask 3)
+      ((w >> 12) && mask msg_label_bits)"
 
 section {* Kernel Objects *}
 

spec/abstract/X64/ArchInvocation_A.thy

@@ -20,28 +20,6 @@ begin
 
 context Arch begin global_naming X64_A
 
-text {* Message infos are encoded to or decoded from a data word. *}
-primrec
-  message_info_to_data :: "message_info \<Rightarrow> data"
-where
-  "message_info_to_data (MI len exc unw mlabel) =
-   (let
-        extra = exc << 7;
-        unwrapped = unw << 9;
-        label = mlabel << 12
-    in
-       label || extra || unwrapped || len)"
-
-text {* Hard-coded to avoid recursive imports? *}
-definition
-  data_to_message_info :: "data \<Rightarrow> message_info"
-where
-  "data_to_message_info w \<equiv>
-   MI (let v = w && ((1 << 7) - 1) in if v > 120 then 120 else v)
-      ((w >> 7) && ((1 << 2) - 1))
-      ((w >> 9) && ((1 << 3) - 1))
-      (w >> 12)"
-
 text {* These datatypes encode the arguments to the various possible
 x64-specific system calls. Selectors are defined for various fields
 for convenience elsewhere. *}

spec/abstract/X64/Machine_A.thy

@@ -110,6 +110,10 @@ definition
   slot_bits :: nat where
   "slot_bits \<equiv> 5"
 
+definition
+  msg_label_bits :: nat where
+  [simp]: "msg_label_bits \<equiv> 52"
+
 definition
   new_context :: "user_context" where
   "new_context \<equiv> UserContext FPUNullState ((\<lambda>r. 0)(CS := selCS3, SS := selDS3, FLAGS := 0x202))"