From b07d971a08157e2cb7461d341654d336a1416fc3 Mon Sep 17 00:00:00 2001
From: Joel Beeren <joel.beeren@nicta.com.au>
Date: Fri, 25 Nov 2016 11:37:50 +1100
Subject: [PATCH] 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 |  5 -----
 spec/machine/ARM/MachineTypes.thy    | 15 +++++++++++----
 spec/machine/MachineExports.thy      | 12 ++++++++++++
 spec/machine/X64/MachineTypes.thy    | 15 +++++++++++++--
 4 files changed, 36 insertions(+), 11 deletions(-)

diff --git a/spec/abstract/X64/Arch_Structs_A.thy b/spec/abstract/X64/Arch_Structs_A.thy
index 3a9dc30f4..eb77221e0 100644
--- a/spec/abstract/X64/Arch_Structs_A.thy
+++ b/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"
 
diff --git a/spec/machine/ARM/MachineTypes.thy b/spec/machine/ARM/MachineTypes.thy
index 3acfe33fe..4ad1137b8 100644
--- a/spec/machine/ARM/MachineTypes.thy
+++ b/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 .
diff --git a/spec/machine/MachineExports.thy b/spec/machine/MachineExports.thy
index 06ac65b59..a298a9f16 100644
--- a/spec/machine/MachineExports.thy
+++ b/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
diff --git a/spec/machine/X64/MachineTypes.thy b/spec/machine/X64/MachineTypes.thy
index cf38ce13e..df8bc788e 100644
--- a/spec/machine/X64/MachineTypes.thy
+++ b/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