x64: machine: move word_size_bits definition to MachineTypes.

Furthermore, create generic library of word lemmas that require
the Arch context to prove, but can be proven with the same proof in
all architectures. These lemmas can then be used safely in generic
theory files. This library is in spec/machine/WordExports.thy

spec/abstract/X64/Arch_Structs_A.thy

@@ -148,11 +148,6 @@ datatype arch_kernel_obj =
  | IOContextTable "16 word \<Rightarrow> iocte"
  | IOPageTable "16 word \<Rightarrow> iopte" *)
 
-
-definition
-  word_size_bits :: nat where
-  "word_size_bits \<equiv> 3"
-
 definition table_size :: nat where
   "table_size = ptTranslationBits + word_size_bits"
 

spec/machine/ARM/MachineTypes.thy

@@ -21,6 +21,17 @@ begin
 
 context Arch begin global_naming ARM
 
+section "Machine Words"
+
+type_synonym machine_word = "word32"
+
+type_synonym machine_word_len = 32
+
+definition
+  word_size_bits :: "'a :: numeral"
+where
+  "word_size_bits \<equiv> 2"
+
 text {*
   An implementation of the machine's types, defining register set
   and some observable machine state.
@@ -48,8 +59,6 @@ datatype register =
   | FaultInstruction
   | CPSR
 
-type_synonym machine_word = "word32"
-
 consts'
 initContext :: "(register * machine_word) list"
 
@@ -58,8 +67,6 @@ sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_w
 
 (*<*)
 
-type_synonym machine_word_len = 32
-
 end
 
 context begin interpretation Arch .

spec/machine/MachineExports.thy

@@ -45,7 +45,19 @@ requalify_consts
   resetTimer
   maxIRQ
   minIRQ
+  word_size_bits
 
+(* HERE IS THE PLACE FOR GENERIC WORD LEMMAS FOR ALL ARCHITECTURES *)
+  
+lemma Suc_unat_mask_div_obfuscated: 
+  "Suc (unat (mask sz div (word_size::machine_word))) = 2 ^ (min sz word_bits - word_size_bits)"
+  unfolding word_size_bits_def
+  by (rule Suc_unat_mask_div)
+
+lemma word_size_size_bits_nat:
+  "2^word_size_bits = (word_size :: nat)"
+  by (simp add: word_size_bits_def word_size_def)
+  
 end
 
 end

spec/machine/X64/MachineTypes.thy

@@ -23,6 +23,18 @@ begin
 
 context Arch begin global_naming X64
 
+section "Machine Words"
+
+type_synonym machine_word = "word64"
+
+type_synonym machine_word_len = 64
+
+definition
+  word_size_bits :: "'a :: numeral"
+where
+  "word_size_bits \<equiv> 3"
+ 
+
 text {*
   An implementation of the machine's types, defining register set 
   and some observable machine state.
@@ -60,7 +72,6 @@ datatype register =
   | RSP
   | SS
 
-type_synonym machine_word = "word64"
 
 datatype gdtslot =
     GDT_NULL
@@ -88,7 +99,7 @@ sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_w
 
 (*<*)
 
-type_synonym machine_word_len = 64
+
 
 end