Add missing HOL4 files (and disable overzealous cleaning)

10 files changed, 3989 insertions, 1 deletions

diff --git a/snapshots/hol4/sail/lib/hol/Holmakefile b/snapshots/hol4/sail/lib/hol/Holmakefile
index 45ed41ff..d7df9bcb 100644
--- a/snapshots/hol4/sail/lib/hol/Holmakefile
+++ b/snapshots/hol4/sail/lib/hol/Holmakefile
@@ -2,7 +2,7 @@ SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.
   sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \
   state_monadScript.sml stateScript.sml promptScript.sml prompt_monadScript.sml
 
-EXTRA_CLEANS = $(SCRIPTS)
+#EXTRA_CLEANS = $(SCRIPTS)
 
 THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
 
diff --git a/snapshots/hol4/sail/lib/hol/promptScript.sml b/snapshots/hol4/sail/lib/hol/promptScript.sml
new file mode 100644
index 00000000..95d6e752
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/promptScript.sml
@@ -0,0 +1,15 @@
+(*Generated by Lem from prompt.lem.*)
+open HolKernel Parse boolLib bossLib;
+open prompt_monadTheory state_monadTheory stateTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "prompt"
+
+(*open import Prompt_monad*)
+(*open import State_monad*)
+(*open import State*)
+val _ = export_theory()
+
diff --git a/snapshots/hol4/sail/lib/hol/prompt_monadScript.sml b/snapshots/hol4/sail/lib/hol/prompt_monadScript.sml
new file mode 100644
index 00000000..627620ff
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/prompt_monadScript.sml
@@ -0,0 +1,24 @@
+(*Generated by Lem from prompt_monad.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory sail_valuesTheory sail_instr_kindsTheory state_monadTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "prompt_monad"
+
+(*open import Pervasives_extra*)
+(*open import Sail_instr_kinds*)
+(*open import Sail_values*)
+(*open import State_monad*)
+
+(* Fake interface of the prompt monad by redirecting to the state monad, since
+   the former is not currently supported by HOL4 *)
+
+val _ = type_abbrev((* ( 'a_rv, 'b_a, 'c_e) *) "monad" , ``:('a_rv,'b_a,'c_e) state_monad$monadS``);
+val _ = type_abbrev((* ( 'a_rv, 'b_a, 'c_e, 'd_r) *) "monadR" , ``:('a_rv,'b_a,'c_e,'d_r) state_monad$monadRS``);
+val _ = Define `
+ ((barrier:'c -> 'a state_monad$sequential_state ->(((unit),'b)state_monad$result#'a state_monad$sequential_state)set) _=  (returnS () ))`;
+val _ = export_theory()
+
diff --git a/snapshots/hol4/sail/lib/hol/sail_instr_kindsScript.sml b/snapshots/hol4/sail/lib/hol/sail_instr_kindsScript.sml
new file mode 100644
index 00000000..cfe0ac60
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/sail_instr_kindsScript.sml
@@ -0,0 +1,473 @@
+(*Generated by Lem from ../../src/lem_interp/sail_instr_kinds.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "sail_instr_kinds"
+
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(*========================================================================*)
+
+(*open import Pervasives_extra*)
+
+
+val _ = Hol_datatype `
+(*  'a *) EnumerationType_class= <|
+  toNat_method : 'a -> num
+|>`;
+
+
+
+(*val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> Basic_classes.ordering*)
+val _ = Define `
+ ((enumeration_typeCompare:'a EnumerationType_class -> 'a -> 'a -> lem_basic_classes$ordering)dict_Sail_instr_kinds_EnumerationType_a e1 e2=   
+(genericCompare (<) (=) (
+  dict_Sail_instr_kinds_EnumerationType_a.toNat_method e1) (dict_Sail_instr_kinds_EnumerationType_a.toNat_method e2)))`;
+
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_var_dict:'a EnumerationType_class -> 'a lem_basic_classes$Ord_class)dict_Sail_instr_kinds_EnumerationType_a= (<|
+
+  compare_method := 
+  (enumeration_typeCompare dict_Sail_instr_kinds_EnumerationType_a);
+
+  isLess_method := (\  r1 r2. (enumeration_typeCompare 
+  dict_Sail_instr_kinds_EnumerationType_a r1 r2) = LT);
+
+  isLessEqual_method := (\ r1 r2. (enumeration_typeCompare 
+  dict_Sail_instr_kinds_EnumerationType_a r1 r2) <> GT);
+
+  isGreater_method := (\  r1 r2. (enumeration_typeCompare 
+  dict_Sail_instr_kinds_EnumerationType_a r1 r2) = GT);
+
+  isGreaterEqual_method := (\ r1 r2. (enumeration_typeCompare 
+  dict_Sail_instr_kinds_EnumerationType_a r1 r2) <> LT)|>))`;
+
+
+
+(* Data structures for building up instructions *)
+
+(* careful: changes in the read/write/barrier kinds have to be
+   reflected in deep_shallow_convert *)
+val _ = Hol_datatype `
+ read_kind =
+  (* common reads *)
+    Read_plain
+  (* Power reads *)
+  | Read_reserve
+  (* AArch64 reads *)
+  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
+  (* RISC-V reads *)
+  | Read_RISCV_acquire  | Read_RISCV_strong_acquire
+  | Read_RISCV_reserved | Read_RISCV_reserved_acquire
+  | Read_RISCV_reserved_strong_acquire
+  (* x86 reads *)
+  | Read_X86_locked`;
+ (* the read part of a lock'd instruction (rmw) *)
+
+val _ = Define `
+((instance_Show_Show_Sail_instr_kinds_read_kind_dict:(read_kind)lem_show$Show_class)= (<|
+
+  show_method := (\x .  
+  (case x of
+        Read_plain => "Read_plain"
+    | Read_reserve => "Read_reserve"
+    | Read_acquire => "Read_acquire"
+    | Read_exclusive => "Read_exclusive"
+    | Read_exclusive_acquire => "Read_exclusive_acquire"
+    | Read_stream => "Read_stream"
+    | Read_RISCV_acquire => "Read_RISCV_acquire"
+    | Read_RISCV_strong_acquire => "Read_RISCV_strong_acquire"
+    | Read_RISCV_reserved => "Read_RISCV_reserved"
+    | Read_RISCV_reserved_acquire => "Read_RISCV_reserved_acquire"
+    | Read_RISCV_reserved_strong_acquire => "Read_RISCV_reserved_strong_acquire"
+    | Read_X86_locked => "Read_X86_locked"
+  ))|>))`;
+
+
+val _ = Hol_datatype `
+ write_kind =
+  (* common writes *)
+    Write_plain
+  (* Power writes *)
+  | Write_conditional
+  (* AArch64 writes *)
+  | Write_release | Write_exclusive | Write_exclusive_release
+  (* RISC-V *)
+  | Write_RISCV_release     | Write_RISCV_strong_release
+  | Write_RISCV_conditional | Write_RISCV_conditional_release
+  | Write_RISCV_conditional_strong_release
+  (* x86 writes *)
+  | Write_X86_locked`;
+ (* the write part of a lock'd instruction (rmw) *)
+
+val _ = Define `
+((instance_Show_Show_Sail_instr_kinds_write_kind_dict:(write_kind)lem_show$Show_class)= (<|
+
+  show_method := (\x .  
+  (case x of
+        Write_plain => "Write_plain"
+    | Write_conditional => "Write_conditional"
+    | Write_release => "Write_release"
+    | Write_exclusive => "Write_exclusive"
+    | Write_exclusive_release => "Write_exclusive_release"
+    | Write_RISCV_release => "Write_RISCV_release"
+    | Write_RISCV_strong_release => "Write_RISCV_strong_release"
+    | Write_RISCV_conditional => "Write_RISCV_conditional"
+    | Write_RISCV_conditional_release => "Write_RISCV_conditional_release"
+    | Write_RISCV_conditional_strong_release => "Write_RISCV_conditional_strong_release"
+    | Write_X86_locked => "Write_X86_locked"
+  ))|>))`;
+
+
+val _ = Hol_datatype `
+ barrier_kind =
+  (* Power barriers *)
+  Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
+  (* AArch64 barriers *)
+  | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
+  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
+  | Barrier_TM_COMMIT
+  (* MIPS barriers *)
+  | Barrier_MIPS_SYNC
+  (* RISC-V barriers *)
+  | Barrier_RISCV_rw_rw
+  | Barrier_RISCV_r_rw
+  | Barrier_RISCV_r_r
+  | Barrier_RISCV_rw_w
+  | Barrier_RISCV_w_w
+  | Barrier_RISCV_i
+  (* X86 *)
+  | Barrier_x86_MFENCE`;
+
+
+
+val _ = Define `
+((instance_Show_Show_Sail_instr_kinds_barrier_kind_dict:(barrier_kind)lem_show$Show_class)= (<|
+
+  show_method := (\x .  
+  (case x of
+        Barrier_Sync => "Barrier_Sync"
+    | Barrier_LwSync => "Barrier_LwSync"
+    | Barrier_Eieio => "Barrier_Eieio"
+    | Barrier_Isync => "Barrier_Isync"
+    | Barrier_DMB => "Barrier_DMB"
+    | Barrier_DMB_ST => "Barrier_DMB_ST"
+    | Barrier_DMB_LD => "Barrier_DMB_LD"
+    | Barrier_DSB => "Barrier_DSB"
+    | Barrier_DSB_ST => "Barrier_DSB_ST"
+    | Barrier_DSB_LD => "Barrier_DSB_LD"
+    | Barrier_ISB => "Barrier_ISB"
+    | Barrier_TM_COMMIT => "Barrier_TM_COMMIT"
+    | Barrier_MIPS_SYNC => "Barrier_MIPS_SYNC"
+    | Barrier_RISCV_rw_rw => "Barrier_RISCV_rw_rw"
+    | Barrier_RISCV_r_rw => "Barrier_RISCV_r_rw"
+    | Barrier_RISCV_r_r => "Barrier_RISCV_r_r"
+    | Barrier_RISCV_rw_w => "Barrier_RISCV_rw_w"
+    | Barrier_RISCV_w_w => "Barrier_RISCV_w_w"
+    | Barrier_RISCV_i => "Barrier_RISCV_i"
+    | Barrier_x86_MFENCE => "Barrier_x86_MFENCE"
+  ))|>))`;
+
+
+val _ = Hol_datatype `
+ trans_kind =
+  (* AArch64 *)
+    Transaction_start | Transaction_commit | Transaction_abort`;
+
+
+val _ = Define `
+((instance_Show_Show_Sail_instr_kinds_trans_kind_dict:(trans_kind)lem_show$Show_class)= (<|
+
+  show_method := (\x .  
+  (case x of
+        Transaction_start => "Transaction_start"
+    | Transaction_commit => "Transaction_commit"
+    | Transaction_abort => "Transaction_abort"
+  ))|>))`;
+
+
+val _ = Hol_datatype `
+ instruction_kind =
+    IK_barrier   of barrier_kind
+  | IK_mem_read  of read_kind
+  | IK_mem_write of write_kind
+  | IK_mem_rmw   of (read_kind # write_kind)
+  | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
+  indirect/computed-branch (single nia of kind NIA_indirect_address)
+  and branch/jump (single nia of kind NIA_concrete_address) *)
+  | IK_trans     of trans_kind
+  | IK_simple`;
+
+
+
+val _ = Define `
+((instance_Show_Show_Sail_instr_kinds_instruction_kind_dict:(instruction_kind)lem_show$Show_class)= (<|
+
+  show_method := (\x .  
+  (case x of
+        IK_barrier barrier_kind => STRCAT "IK_barrier "
+                                     (((\x .  (case x of
+                                                    Barrier_Sync => "Barrier_Sync"
+                                                | Barrier_LwSync => "Barrier_LwSync"
+                                                | Barrier_Eieio => "Barrier_Eieio"
+                                                | Barrier_Isync => "Barrier_Isync"
+                                                | Barrier_DMB => "Barrier_DMB"
+                                                | Barrier_DMB_ST => "Barrier_DMB_ST"
+                                                | Barrier_DMB_LD => "Barrier_DMB_LD"
+                                                | Barrier_DSB => "Barrier_DSB"
+                                                | Barrier_DSB_ST => "Barrier_DSB_ST"
+                                                | Barrier_DSB_LD => "Barrier_DSB_LD"
+                                                | Barrier_ISB => "Barrier_ISB"
+                                                | Barrier_TM_COMMIT => 
+                                              "Barrier_TM_COMMIT"
+                                                | Barrier_MIPS_SYNC => 
+                                              "Barrier_MIPS_SYNC"
+                                                | Barrier_RISCV_rw_rw => 
+                                              "Barrier_RISCV_rw_rw"
+                                                | Barrier_RISCV_r_rw => 
+                                              "Barrier_RISCV_r_rw"
+                                                | Barrier_RISCV_r_r => 
+                                              "Barrier_RISCV_r_r"
+                                                | Barrier_RISCV_rw_w => 
+                                              "Barrier_RISCV_rw_w"
+                                                | Barrier_RISCV_w_w => 
+                                              "Barrier_RISCV_w_w"
+                                                | Barrier_RISCV_i => 
+                                              "Barrier_RISCV_i"
+                                                | Barrier_x86_MFENCE => 
+                                              "Barrier_x86_MFENCE"
+                                              )) barrier_kind))
+    | IK_mem_read read_kind => STRCAT "IK_mem_read "
+                                 (((\x .  (case x of
+                                                Read_plain => "Read_plain"
+                                            | Read_reserve => "Read_reserve"
+                                            | Read_acquire => "Read_acquire"
+                                            | Read_exclusive => "Read_exclusive"
+                                            | Read_exclusive_acquire => 
+                                          "Read_exclusive_acquire"
+                                            | Read_stream => "Read_stream"
+                                            | Read_RISCV_acquire => "Read_RISCV_acquire"
+                                            | Read_RISCV_strong_acquire => 
+                                          "Read_RISCV_strong_acquire"
+                                            | Read_RISCV_reserved => 
+                                          "Read_RISCV_reserved"
+                                            | Read_RISCV_reserved_acquire => 
+                                          "Read_RISCV_reserved_acquire"
+                                            | Read_RISCV_reserved_strong_acquire => 
+                                          "Read_RISCV_reserved_strong_acquire"
+                                            | Read_X86_locked => "Read_X86_locked"
+                                          )) read_kind))
+    | IK_mem_write write_kind => STRCAT "IK_mem_write "
+                                   (((\x .  (case x of
+                                                  Write_plain => "Write_plain"
+                                              | Write_conditional => 
+                                            "Write_conditional"
+                                              | Write_release => "Write_release"
+                                              | Write_exclusive => "Write_exclusive"
+                                              | Write_exclusive_release => 
+                                            "Write_exclusive_release"
+                                              | Write_RISCV_release => 
+                                            "Write_RISCV_release"
+                                              | Write_RISCV_strong_release => 
+                                            "Write_RISCV_strong_release"
+                                              | Write_RISCV_conditional => 
+                                            "Write_RISCV_conditional"
+                                              | Write_RISCV_conditional_release => 
+                                            "Write_RISCV_conditional_release"
+                                              | Write_RISCV_conditional_strong_release => 
+                                            "Write_RISCV_conditional_strong_release"
+                                              | Write_X86_locked => "Write_X86_locked"
+                                            )) write_kind))
+    | IK_mem_rmw (r, w) => STRCAT "IK_mem_rmw "
+                             (STRCAT
+                                (((\x .  (case x of
+                                               Read_plain => "Read_plain"
+                                           | Read_reserve => "Read_reserve"
+                                           | Read_acquire => "Read_acquire"
+                                           | Read_exclusive => "Read_exclusive"
+                                           | Read_exclusive_acquire => 
+                                         "Read_exclusive_acquire"
+                                           | Read_stream => "Read_stream"
+                                           | Read_RISCV_acquire => "Read_RISCV_acquire"
+                                           | Read_RISCV_strong_acquire => 
+                                         "Read_RISCV_strong_acquire"
+                                           | Read_RISCV_reserved => "Read_RISCV_reserved"
+                                           | Read_RISCV_reserved_acquire => 
+                                         "Read_RISCV_reserved_acquire"
+                                           | Read_RISCV_reserved_strong_acquire => 
+                                         "Read_RISCV_reserved_strong_acquire"
+                                           | Read_X86_locked => "Read_X86_locked"
+                                         )) r))
+                                (STRCAT " "
+                                   (((\x .  (case x of
+                                                  Write_plain => "Write_plain"
+                                              | Write_conditional => 
+                                            "Write_conditional"
+                                              | Write_release => "Write_release"
+                                              | Write_exclusive => "Write_exclusive"
+                                              | Write_exclusive_release => 
+                                            "Write_exclusive_release"
+                                              | Write_RISCV_release => 
+                                            "Write_RISCV_release"
+                                              | Write_RISCV_strong_release => 
+                                            "Write_RISCV_strong_release"
+                                              | Write_RISCV_conditional => 
+                                            "Write_RISCV_conditional"
+                                              | Write_RISCV_conditional_release => 
+                                            "Write_RISCV_conditional_release"
+                                              | Write_RISCV_conditional_strong_release => 
+                                            "Write_RISCV_conditional_strong_release"
+                                              | Write_X86_locked => "Write_X86_locked"
+                                            )) w))))
+    | IK_branch => "IK_branch"
+    | IK_trans trans_kind => STRCAT "IK_trans "
+                               (((\x .  (case x of
+                                              Transaction_start => "Transaction_start"
+                                          | Transaction_commit => "Transaction_commit"
+                                          | Transaction_abort => "Transaction_abort"
+                                        )) trans_kind))
+    | IK_simple => "IK_simple"
+  ))|>))`;
+
+
+
+val _ = Define `
+ ((read_is_exclusive:read_kind -> bool)= 
+  (\x .  (case x of
+               Read_plain => F
+           | Read_reserve => T
+           | Read_acquire => F
+           | Read_exclusive => T
+           | Read_exclusive_acquire => T
+           | Read_stream => F
+           | Read_RISCV_acquire => F
+           | Read_RISCV_strong_acquire => F
+           | Read_RISCV_reserved => T
+           | Read_RISCV_reserved_acquire => T
+           | Read_RISCV_reserved_strong_acquire => T
+           | Read_X86_locked => T
+         )))`;
+
+
+
+
+val _ = Define `
+((instance_Sail_instr_kinds_EnumerationType_Sail_instr_kinds_read_kind_dict:(read_kind)EnumerationType_class)= (<|
+
+  toNat_method := (\x .  
+  (case x of
+        Read_plain =>( 0 : num)
+    | Read_reserve =>( 1 : num)
+    | Read_acquire =>( 2 : num)
+    | Read_exclusive =>( 3 : num)
+    | Read_exclusive_acquire =>( 4 : num)
+    | Read_stream =>( 5 : num)
+    | Read_RISCV_acquire =>( 6 : num)
+    | Read_RISCV_strong_acquire =>( 7 : num)
+    | Read_RISCV_reserved =>( 8 : num)
+    | Read_RISCV_reserved_acquire =>( 9 : num)
+    | Read_RISCV_reserved_strong_acquire =>( 10 : num)
+    | Read_X86_locked =>( 11 : num)
+  ))|>))`;
+
+
+val _ = Define `
+((instance_Sail_instr_kinds_EnumerationType_Sail_instr_kinds_write_kind_dict:(write_kind)EnumerationType_class)= (<|
+
+  toNat_method := (\x .  
+  (case x of
+        Write_plain =>( 0 : num)
+    | Write_conditional =>( 1 : num)
+    | Write_release =>( 2 : num)
+    | Write_exclusive =>( 3 : num)
+    | Write_exclusive_release =>( 4 : num)
+    | Write_RISCV_release =>( 5 : num)
+    | Write_RISCV_strong_release =>( 6 : num)
+    | Write_RISCV_conditional =>( 7 : num)
+    | Write_RISCV_conditional_release =>( 8 : num)
+    | Write_RISCV_conditional_strong_release =>( 9 : num)
+    | Write_X86_locked =>( 10 : num)
+  ))|>))`;
+
+
+val _ = Define `
+((instance_Sail_instr_kinds_EnumerationType_Sail_instr_kinds_barrier_kind_dict:(barrier_kind)EnumerationType_class)= (<|
+
+  toNat_method := (\x .  
+  (case x of
+        Barrier_Sync =>( 0 : num)
+    | Barrier_LwSync =>( 1 : num)
+    | Barrier_Eieio =>( 2 : num)
+    | Barrier_Isync =>( 3 : num)
+    | Barrier_DMB =>( 4 : num)
+    | Barrier_DMB_ST =>( 5 : num)
+    | Barrier_DMB_LD =>( 6 : num)
+    | Barrier_DSB =>( 7 : num)
+    | Barrier_DSB_ST =>( 8 : num)
+    | Barrier_DSB_LD =>( 9 : num)
+    | Barrier_ISB =>( 10 : num)
+    | Barrier_TM_COMMIT =>( 11 : num)
+    | Barrier_MIPS_SYNC =>( 12 : num)
+    | Barrier_RISCV_rw_rw =>( 13 : num)
+    | Barrier_RISCV_r_rw =>( 14 : num)
+    | Barrier_RISCV_r_r =>( 15 : num)
+    | Barrier_RISCV_rw_w =>( 16 : num)
+    | Barrier_RISCV_w_w =>( 17 : num)
+    | Barrier_RISCV_i =>( 18 : num)
+    | Barrier_x86_MFENCE =>( 19 : num)
+  ))|>))`;
+
+val _ = export_theory()
+
diff --git a/snapshots/hol4/sail/lib/hol/sail_operatorsScript.sml b/snapshots/hol4/sail/lib/hol/sail_operatorsScript.sml
new file mode 100644
index 00000000..f1f0c8d4
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/sail_operatorsScript.sml
@@ -0,0 +1,367 @@
+(*Generated by Lem from ../../src/gen_lib/sail_operators.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "sail_operators"
+
+(*open import Pervasives_extra*)
+(*open import Machine_word*)
+(*open import Sail_values*)
+
+(*** Bit vector operations *)
+
+(*val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list Sail_values.bitU*)
+val _ = Define `
+ ((concat_bv:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'a -> 'b ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b l r=  (
+  dict_Sail_values_Bitvector_a.bits_of_method l ++ dict_Sail_values_Bitvector_b.bits_of_method r))`;
+
+
+(*val cons_bv : forall 'a. Bitvector 'a => Sail_values.bitU -> 'a -> list Sail_values.bitU*)
+val _ = Define `
+ ((cons_bv:'a sail_values$Bitvector_class -> sail_values$bitU -> 'a ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a b v=  (b :: 
+  dict_Sail_values_Bitvector_a.bits_of_method v))`;
+
+
+(*val cast_unit_bv : Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((cast_unit_bv:sail_values$bitU ->(sail_values$bitU)list) b=  ([b]))`;
+
+
+(*val bv_of_bit : Num.integer -> Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((bv_of_bit:int -> sail_values$bitU ->(sail_values$bitU)list) len b=  (extz_bits len [b]))`;
+
+
+val _ = Define `
+ ((most_significant:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU)dict_Sail_values_Bitvector_a v=  ((case  
+  dict_Sail_values_Bitvector_a.bits_of_method v of
+    b :: _ => b
+  | _ => B0 (* Treat empty bitvector as all zeros *)
+  )))`;
+
+
+val _ = Define `
+ ((get_max_representable_in:bool -> int -> int) sign (n : int) : int=  
+ (if (n =( 64 : int)) then (case sign of   T => max_64 | F => max_64u )
+  else if (n=( 32 : int)) then (case sign of   T => max_32 | F => max_32u )
+  else if (n=( 8 : int)) then max_8
+  else if (n=( 5 : int)) then max_5
+  else (case sign of   T => (( 2 : int))** ((Num (ABS (I n))) -( 1 : num))
+                       | F => (( 2 : int))** (Num (ABS (I n)))
+       )))`;
+
+
+val _ = Define `
+ ((get_min_representable_in:'a -> int -> int) _ (n : int) : int=  
+ (if n =( 64 : int) then min_64
+  else if n =( 32 : int) then min_32
+  else if n =( 8 : int) then min_8
+  else if n =( 5 : int) then min_5
+  else( 0 : int) - ((( 2 : int))** (Num (ABS (I n))))))`;
+
+
+(*val arith_op_bv_int : forall 'a 'b. Bitvector 'a =>
+  (Num.integer -> Num.integer -> Num.integer) -> bool -> 'a -> Num.integer -> 'a*)
+val _ = Define `
+ ((arith_op_bv_int:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> 'a -> int -> 'a)dict_Sail_values_Bitvector_a op sign l r=  
+ (let r' = (dict_Sail_values_Bitvector_a.of_int_method (dict_Sail_values_Bitvector_a.length_method l) r) in  dict_Sail_values_Bitvector_a.arith_op_bv_method op sign l r'))`;
+
+
+(*val arith_op_int_bv : forall 'a 'b. Bitvector 'a =>
+  (Num.integer -> Num.integer -> Num.integer) -> bool -> Num.integer -> 'a -> 'a*)
+val _ = Define `
+ ((arith_op_int_bv:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> int -> 'a -> 'a)dict_Sail_values_Bitvector_a op sign l r=  
+ (let l' = (dict_Sail_values_Bitvector_a.of_int_method (dict_Sail_values_Bitvector_a.length_method r) l) in  dict_Sail_values_Bitvector_a.arith_op_bv_method op sign l' r))`;
+
+
+val _ = Define `
+ ((arith_op_bv_bool:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a op sign l r=  (arith_op_bv_int 
+  dict_Sail_values_Bitvector_a op sign l (if r then( 1 : int) else( 0 : int))))`;
+
+val _ = Define `
+ ((arith_op_bv_bit:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a op sign l r=  (OPTION_MAP (arith_op_bv_bool 
+  dict_Sail_values_Bitvector_a op sign l) (bool_of_bitU r)))`;
+
+
+(* TODO (or just omit and define it per spec if needed)
+val arith_op_overflow_bv : forall 'a. Bitvector 'a =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU)
+let arith_op_overflow_bv op sign size l r =
+  let len = length l in
+  let act_size = len * size in
+  match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with
+    | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) ->
+       let n = op l_sign r_sign in
+       let n_unsign = op l_unsign r_unsign in
+       let correct_size = of_int act_size n in
+       let one_more_size_u = bits_of_int (act_size + 1) n_unsign in
+       let overflow =
+         if n <= get_max_representable_in sign len &&
+              n >= get_min_representable_in sign len
+         then B0 else B1 in
+       let c_out = most_significant one_more_size_u in
+       (correct_size,overflow,c_out)
+    | (_, _, _, _) ->
+       (repeat [BU] act_size, BU, BU)
+  end
+
+let add_overflow_bv = arith_op_overflow_bv integerAdd false 1
+let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1
+let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1
+let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1
+let mult_overflow_bv = arith_op_overflow_bv integerMult false 2
+let mults_overflow_bv = arith_op_overflow_bv integerMult true 2
+
+val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU)
+let arith_op_overflow_bv_bit op sign size l r_bit =
+  let act_size = length l * size in
+  match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with
+    | (Just l', Just l_u, false) ->
+       let (n, nu, changed) = match r_bit with
+         | B1 -> (op l' 1, op l_u 1, true)
+         | B0 -> (l', l_u, false)
+         | BU -> (* unreachable due to check above *)
+            failwith "arith_op_overflow_bv_bit applied to undefined bit"
+         end in
+       let correct_size = of_int act_size n in
+       let one_larger = bits_of_int (act_size + 1) nu in
+       let overflow =
+         if changed
+         then
+           if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
+           then B0 else B1
+         else B0 in
+       (correct_size, overflow, most_significant one_larger)
+    | (_, _, _) ->
+       (repeat [BU] act_size, BU, BU)
+  end
+
+let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1
+let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1
+let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1
+let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*)
+
+val _ = Hol_datatype `
+ shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot`;
+
+
+val _ = Define `
+ ((invert_shift:shift -> shift)= 
+  (\x .  (case x of
+               LL_shift => RR_shift
+           | RR_shift => LL_shift
+           | RR_shift_arith => LL_shift
+           | LL_rot => RR_rot
+           | RR_rot => LL_rot
+         )))`;
+
+
+(*val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((shift_op_bv:'a sail_values$Bitvector_class -> shift -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a op v n=  
+ (let v = (dict_Sail_values_Bitvector_a.bits_of_method v) in
+  if n =( 0 : int) then v else
+  let (op, n) = (if n >( 0 : int) then (op, n) else (invert_shift op, ~ n)) in
+  (case op of
+    LL_shift =>
+     subrange_list T v n (int_of_num (LENGTH v) -( 1 : int)) ++ repeat [B0] n
+  | RR_shift =>
+     repeat [B0] n ++ subrange_list T v(( 0 : int)) ((int_of_num (LENGTH v) - n) -( 1 : int))
+  | RR_shift_arith =>
+     repeat [most_significant 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) v] n ++ subrange_list T v(( 0 : int)) ((int_of_num (LENGTH v) - n) -( 1 : int))
+  | LL_rot =>
+     subrange_list T v n (int_of_num (LENGTH v) -( 1 : int)) ++ subrange_list T v(( 0 : int)) (n -( 1 : int))
+  | RR_rot =>
+     subrange_list F v(( 0 : int)) (n -( 1 : int)) ++ subrange_list F v n (int_of_num (LENGTH v) -( 1 : int))
+  )))`;
+
+
+val _ = Define `
+ ((shiftl_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a=  (shift_op_bv 
+  dict_Sail_values_Bitvector_a LL_shift))`;
+ (*"<<"*)
+val _ = Define `
+ ((shiftr_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a=  (shift_op_bv 
+  dict_Sail_values_Bitvector_a RR_shift))`;
+ (*">>"*)
+val _ = Define `
+ ((arith_shiftr_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a=  (shift_op_bv 
+  dict_Sail_values_Bitvector_a RR_shift_arith))`;
+
+val _ = Define `
+ ((rotl_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a=  (shift_op_bv 
+  dict_Sail_values_Bitvector_a LL_rot))`;
+ (*"<<<"*)
+val _ = Define `
+ ((rotr_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a=  (shift_op_bv 
+  dict_Sail_values_Bitvector_a LL_rot))`;
+ (*">>>"*)
+
+val _ = Define `
+ ((shiftl_mword:'a words$word -> int -> 'a words$word) w n=  (words$word_lsl w (nat_of_int n)))`;
+
+val _ = Define `
+ ((shiftr_mword:'a words$word -> int -> 'a words$word) w n=  (words$word_lsr w (nat_of_int n)))`;
+
+val _ = Define `
+ ((arith_shiftr_mword:'a words$word -> int -> 'a words$word) w n=  (words$word_asr w (nat_of_int n)))`;
+
+val _ = Define `
+ ((rotl_mword:'a words$word -> int -> 'a words$word) w n=  (words$word_rol w (nat_of_int n)))`;
+
+val _ = Define `
+ ((rotr_mword:'a words$word -> int -> 'a words$word) w n=  (words$word_ror w (nat_of_int n)))`;
+
+
+ val _ = Define `
+ ((arith_op_no0:(int -> int -> int) -> int -> int ->(int)option) (op : int -> int -> int) l r=  
+ (if r =( 0 : int)
+  then NONE
+  else SOME (op l r)))`;
+
+
+(*val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+  (Num.integer -> Num.integer -> Num.integer) -> bool -> Num.integer -> 'a -> 'a -> Maybe.maybe 'b*)
+val _ = Define `
+ ((arith_op_bv_no0:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class ->(int -> int -> int) -> bool -> int -> 'a -> 'a -> 'b option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b op sign size1 l r=  
+ (OPTION_BIND (int_of_bv 
+  dict_Sail_values_Bitvector_a sign l) (\ l' . 
+  OPTION_BIND (int_of_bv 
+  dict_Sail_values_Bitvector_a sign r) (\ r' . 
+  if r' =( 0 : int) then NONE else SOME (
+  dict_Sail_values_Bitvector_b.of_int_method (dict_Sail_values_Bitvector_a.length_method l * size1) (op l' r'))))))`;
+
+
+val _ = Define `
+ ((mod_bv:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> 'b -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b=  (arith_op_bv_no0 
+  dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_mod F(( 1 : int))))`;
+
+val _ = Define `
+ ((quot_bv:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> 'b -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b=  (arith_op_bv_no0 
+  dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_quot F(( 1 : int))))`;
+
+val _ = Define `
+ ((quots_bv:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> 'b -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b=  (arith_op_bv_no0 
+  dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_quot T(( 1 : int))))`;
+
+
+val _ = Define `
+ ((mod_mword:'a words$word -> 'a words$word -> 'a words$word)=  words$word_mod)`;
+
+val _ = Define `
+ ((quot_mword:'a words$word -> 'a words$word -> 'a words$word)=  words$word_div)`;
+
+val _ = Define `
+ ((quots_mword:'a words$word -> 'a words$word -> 'a words$word)=  words$word_quot)`;
+
+
+val _ = Define `
+ ((arith_op_bv_int_no0:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class ->(int -> int -> int) -> bool -> int -> 'a -> int -> 'b option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b op sign size1 l r=  
+ (arith_op_bv_no0 dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b op sign size1 l (dict_Sail_values_Bitvector_a.of_int_method (dict_Sail_values_Bitvector_a.length_method l) r)))`;
+
+
+val _ = Define `
+ ((quot_bv_int:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> int -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b=  (arith_op_bv_int_no0 
+  dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_quot F(( 1 : int))))`;
+
+val _ = Define `
+ ((mod_bv_int:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> 'b -> int -> 'a option)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b=  (arith_op_bv_int_no0 
+  dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a hardware_mod F(( 1 : int))))`;
+
+
+val _ = Define `
+ ((mod_mword_int:'a words$word -> int -> 'a words$word) l r=  (words$word_mod l (integer_word$i2w r)))`;
+
+val _ = Define `
+ ((quot_mword_int:'a words$word -> int -> 'a words$word) l r=  (words$word_div l (integer_word$i2w r)))`;
+
+val _ = Define `
+ ((quots_mword_int:'a words$word -> int -> 'a words$word) l r=  (words$word_quot l (integer_word$i2w r)))`;
+
+
+val _ = Define `
+ ((replicate_bits_bv:'a sail_values$Bitvector_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a v count1=  (repeat (
+  dict_Sail_values_Bitvector_a.bits_of_method v) count1))`;
+
+val _ = Define `
+ ((duplicate_bit_bv:'a sail_values$BitU_class -> 'a -> int ->(sail_values$bitU)list)dict_Sail_values_BitU_a bit len=  (replicate_bits_bv 
+  (instance_Sail_values_Bitvector_list_dict dict_Sail_values_BitU_a) [bit] len))`;
+
+
+(*val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
+val _ = Define `
+ ((eq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  (
+  dict_Sail_values_Bitvector_a.bits_of_method l = dict_Sail_values_Bitvector_a.bits_of_method r))`;
+
+
+(*val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
+val _ = Define `
+ ((neq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  (~ (eq_bv 
+  dict_Sail_values_Bitvector_a l r)))`;
+
+
+(*val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
+val _ = Define `
+ ((ult_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  (lexicographic_less (\  l r. (compare_bitU l r) = LT) (\ l r. (compare_bitU l r) <> GT) (REVERSE (
+  dict_Sail_values_Bitvector_a.bits_of_method l)) (REVERSE (dict_Sail_values_Bitvector_a.bits_of_method r))))`;
+
+val _ = Define `
+ ((ulteq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  ((eq_bv 
+  dict_Sail_values_Bitvector_a l r) \/ (ult_bv dict_Sail_values_Bitvector_a l r)))`;
+
+val _ = Define `
+ ((ugt_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  (~ (ulteq_bv 
+  dict_Sail_values_Bitvector_a l r)))`;
+
+val _ = Define `
+ ((ugteq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  ((eq_bv 
+  dict_Sail_values_Bitvector_a l r) \/ (ugt_bv dict_Sail_values_Bitvector_a l r)))`;
+
+
+(*val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
+val _ = Define `
+ ((slt_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  
+ ((case (most_significant 
+  dict_Sail_values_Bitvector_a l, most_significant dict_Sail_values_Bitvector_a r) of
+      (B0, B0) => ult_bv 
+  dict_Sail_values_Bitvector_a l r
+    | (B0, B1) => F
+    | (B1, B0) => T
+    | (B1, B1) =>
+       let l' = (add_one_bit_ignore_overflow (
+  dict_Sail_values_Bitvector_a.bits_of_method l)) in
+       let r' = (add_one_bit_ignore_overflow (
+  dict_Sail_values_Bitvector_a.bits_of_method r)) in
+       ugt_bv (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l' r'
+    | (BU, BU) => ult_bv 
+  dict_Sail_values_Bitvector_a l r
+    | (BU, _) => T
+    | (_, BU) => F
+  )))`;
+
+val _ = Define `
+ ((slteq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  ((eq_bv 
+  dict_Sail_values_Bitvector_a l r) \/ (slt_bv dict_Sail_values_Bitvector_a l r)))`;
+
+val _ = Define `
+ ((sgt_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  (~ (slteq_bv 
+  dict_Sail_values_Bitvector_a l r)))`;
+
+val _ = Define `
+ ((sgteq_bv:'a sail_values$Bitvector_class -> 'a -> 'a -> bool)dict_Sail_values_Bitvector_a l r=  ((eq_bv 
+  dict_Sail_values_Bitvector_a l r) \/ (sgt_bv dict_Sail_values_Bitvector_a l r)))`;
+
+
+(*val ucmp_mword : forall 'a. Size 'a => (Num.integer -> Num.integer -> bool) -> Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+
+(*val scmp_mword : forall 'a. Size 'a => (Num.integer -> Num.integer -> bool) -> Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+val _ = export_theory()
+
diff --git a/snapshots/hol4/sail/lib/hol/sail_operators_bitlistsScript.sml b/snapshots/hol4/sail/lib/hol/sail_operators_bitlistsScript.sml
new file mode 100644
index 00000000..5d2978bb
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/sail_operators_bitlistsScript.sml
@@ -0,0 +1,792 @@
+(*Generated by Lem from ../../src/gen_lib/sail_operators_bitlists.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory sail_operatorsTheory prompt_monadTheory promptTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "sail_operators_bitlists"
+
+(*open import Pervasives_extra*)
+(*open import Machine_word*)
+(*open import Sail_values*)
+(*open import Sail_operators*)
+(*open import Prompt_monad*)
+(*open import Prompt*)
+
+(* Specialisation of operators to bit lists *)
+
+(*val uint_maybe : list Sail_values.bitU -> Maybe.maybe Num.integer*)
+val _ = Define `
+ ((uint_maybe0:(sail_values$bitU)list ->(int)option) v=  (unsigned_of_bits (MAP (\ b. b) v)))`;
+
+val _ = Define `
+ ((uint_fail0:'a sail_values$Bitvector_class -> 'a -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set)dict_Sail_values_Bitvector_a v=  (state_monad$maybe_failS "uint" (
+  dict_Sail_values_Bitvector_a.unsigned_method v)))`;
+
+val _ = Define `
+ ((uint_oracle0:(sail_values$bitU)list -> 'a state_monad$sequential_state ->(((int),'b)state_monad$result#'a state_monad$sequential_state)set) v=  (state_monad$bindS  
+(state$bools_of_bits_oracleS v) (\ bs . 
+  state_monad$returnS (int_of_bools F bs))))`;
+
+val _ = Define `
+ ((uint:(sail_values$bitU)list -> int) v=  (maybe_failwith (uint_maybe0 v)))`;
+
+
+(*val sint_maybe : list Sail_values.bitU -> Maybe.maybe Num.integer*)
+val _ = Define `
+ ((sint_maybe0:(sail_values$bitU)list ->(int)option) v=  (signed_of_bits (MAP (\ b. b) v)))`;
+
+val _ = Define `
+ ((sint_fail0:'a sail_values$Bitvector_class -> 'a -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set)dict_Sail_values_Bitvector_a v=  (state_monad$maybe_failS "sint" (
+  dict_Sail_values_Bitvector_a.signed_method v)))`;
+
+val _ = Define `
+ ((sint_oracle0:(sail_values$bitU)list -> 'a state_monad$sequential_state ->(((int),'b)state_monad$result#'a state_monad$sequential_state)set) v=  (state_monad$bindS  
+(state$bools_of_bits_oracleS v) (\ bs . 
+  state_monad$returnS (int_of_bools T bs))))`;
+
+val _ = Define `
+ ((sint:(sail_values$bitU)list -> int) v=  (maybe_failwith (sint_maybe0 v)))`;
+
+
+(*val extz_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((extz_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)= 
+  (extz_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val exts_vec : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((exts_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)= 
+  (exts_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val zero_extend : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((zero_extend0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) bits len=  (extz_bits len bits))`;
+
+
+(*val sign_extend : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((sign_extend0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) bits len=  (exts_bits len bits))`;
+
+
+(*val vector_truncate : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((vector_truncate0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) bs len=  (extz_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) len bs))`;
+
+
+(*val vec_of_bits_maybe    : list Sail_values.bitU -> Maybe.maybe (list Sail_values.bitU)*)
+(*val vec_of_bits_fail     : forall 'rv 'e. list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+(*val vec_of_bits_oracle   : forall 'rv 'e. list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+(*val vec_of_bits_failwith : list Sail_values.bitU -> list Sail_values.bitU*)
+(*val vec_of_bits          : list Sail_values.bitU -> list Sail_values.bitU*)
+
+(*val access_vec_inc : list Sail_values.bitU -> Num.integer -> Sail_values.bitU*)
+val _ = Define `
+ ((access_vec_inc0:(sail_values$bitU)list -> int -> sail_values$bitU)= 
+  (access_bv_inc
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val access_vec_dec : list Sail_values.bitU -> Num.integer -> Sail_values.bitU*)
+val _ = Define `
+ ((access_vec_dec0:(sail_values$bitU)list -> int -> sail_values$bitU)= 
+  (access_bv_dec
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val update_vec_inc : list Sail_values.bitU -> Num.integer -> Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((update_vec_inc0:(sail_values$bitU)list -> int -> sail_values$bitU ->(sail_values$bitU)list)= 
+  (update_bv_inc
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((update_vec_inc_maybe0:(sail_values$bitU)list -> int -> sail_values$bitU ->((sail_values$bitU)list)option) v i b=  (SOME (update_vec_inc0 v i b)))`;
+
+val _ = Define `
+ ((update_vec_inc_fail0:(sail_values$bitU)list -> int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) v i b=  (state_monad$returnS (update_vec_inc0 v i b)))`;
+
+val _ = Define `
+ ((update_vec_inc_oracle0:(sail_values$bitU)list -> int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) v i b=  (state_monad$returnS (update_vec_inc0 v i b)))`;
+
+
+(*val update_vec_dec : list Sail_values.bitU -> Num.integer -> Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((update_vec_dec0:(sail_values$bitU)list -> int -> sail_values$bitU ->(sail_values$bitU)list)= 
+  (update_bv_dec
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((update_vec_dec_maybe0:(sail_values$bitU)list -> int -> sail_values$bitU ->((sail_values$bitU)list)option) v i b=  (SOME (update_vec_dec0 v i b)))`;
+
+val _ = Define `
+ ((update_vec_dec_fail0:(sail_values$bitU)list -> int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) v i b=  (state_monad$returnS (update_vec_dec0 v i b)))`;
+
+val _ = Define `
+ ((update_vec_dec_oracle0:(sail_values$bitU)list -> int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) v i b=  (state_monad$returnS (update_vec_dec0 v i b)))`;
+
+
+(*val subrange_vec_inc : list Sail_values.bitU -> Num.integer -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((subrange_vec_inc0:(sail_values$bitU)list -> int -> int ->(sail_values$bitU)list)= 
+  (subrange_bv_inc
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val subrange_vec_dec : list Sail_values.bitU -> Num.integer -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((subrange_vec_dec0:(sail_values$bitU)list -> int -> int ->(sail_values$bitU)list)= 
+  (subrange_bv_dec
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val update_subrange_vec_inc : list Sail_values.bitU -> Num.integer -> Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((update_subrange_vec_inc0:(sail_values$bitU)list -> int -> int ->(sail_values$bitU)list ->(sail_values$bitU)list)= 
+  (update_subrange_bv_inc
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val update_subrange_vec_dec : list Sail_values.bitU -> Num.integer -> Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((update_subrange_vec_dec0:(sail_values$bitU)list -> int -> int ->(sail_values$bitU)list ->(sail_values$bitU)list)= 
+  (update_subrange_bv_dec
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val concat_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((concat_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)= 
+  (concat_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val cons_vec : Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((cons_vec0:sail_values$bitU ->(sail_values$bitU)list ->(sail_values$bitU)list)= 
+  (cons_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((cons_vec_maybe0:sail_values$bitU ->(sail_values$bitU)list ->((sail_values$bitU)list)option) b v=  (SOME (cons_vec0 b v)))`;
+
+val _ = Define `
+ ((cons_vec_fail0:sail_values$bitU ->(sail_values$bitU)list -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b v=  (state_monad$returnS (cons_vec0 b v)))`;
+
+val _ = Define `
+ ((cons_vec_oracle0:sail_values$bitU ->(sail_values$bitU)list -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b v=  (state_monad$returnS (cons_vec0 b v)))`;
+
+
+(*val cast_unit_vec : Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((cast_unit_vec0:sail_values$bitU ->(sail_values$bitU)list)=  cast_unit_bv)`;
+
+val _ = Define `
+ ((cast_unit_vec_maybe0:sail_values$bitU ->((sail_values$bitU)list)option) b=  (SOME (cast_unit_vec0 b)))`;
+
+val _ = Define `
+ ((cast_unit_vec_fail0:sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b=  (state_monad$returnS (cast_unit_vec0 b)))`;
+
+val _ = Define `
+ ((cast_unit_vec_oracle0:sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b=  (state_monad$returnS (cast_unit_vec0 b)))`;
+
+
+(*val vec_of_bit : Num.integer -> Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((vec_of_bit0:int -> sail_values$bitU ->(sail_values$bitU)list)=  bv_of_bit)`;
+
+val _ = Define `
+ ((vec_of_bit_maybe0:int -> sail_values$bitU ->((sail_values$bitU)list)option) len b=  (SOME (vec_of_bit0 len b)))`;
+
+val _ = Define `
+ ((vec_of_bit_fail0:int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) len b=  (state_monad$returnS (vec_of_bit0 len b)))`;
+
+val _ = Define `
+ ((vec_of_bit_oracle0:int -> sail_values$bitU -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) len b=  (state_monad$returnS (vec_of_bit0 len b)))`;
+
+
+(*val msb : list Sail_values.bitU -> Sail_values.bitU*)
+val _ = Define `
+ ((msb0:(sail_values$bitU)list -> sail_values$bitU)= 
+  (most_significant
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val int_of_vec_maybe : bool -> list Sail_values.bitU -> Maybe.maybe Num.integer*)
+val _ = Define `
+ ((int_of_vec_maybe0:bool ->(sail_values$bitU)list ->(int)option)= 
+  (int_of_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((int_of_vec_fail0:bool ->(sail_values$bitU)list -> 'a state_monad$sequential_state ->(((int),'b)state_monad$result#'a state_monad$sequential_state)set) sign v=  (state_monad$maybe_failS "int_of_vec" (int_of_vec_maybe0 sign v)))`;
+
+val _ = Define `
+ ((int_of_vec_oracle:bool ->(sail_values$bitU)list -> 'a state_monad$sequential_state ->(((int),'b)state_monad$result#'a state_monad$sequential_state)set) sign v=  (state_monad$bindS (state$bools_of_bits_oracleS v) (\ v .  state_monad$returnS (int_of_bools sign v))))`;
+
+val _ = Define `
+ ((int_of_vec0:bool ->(sail_values$bitU)list -> int) sign v=  (maybe_failwith (int_of_vec_maybe0 sign v)))`;
+
+
+(*val string_of_vec : list Sail_values.bitU -> string*)
+val _ = Define `
+ ((string_of_vec0:(sail_values$bitU)list -> string)= 
+  (string_of_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val and_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val or_vec  : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val xor_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val not_vec : list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((and_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=  (binop_list and_bit))`;
+
+val _ = Define `
+ ((or_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=   (binop_list or_bit))`;
+
+val _ = Define `
+ ((xor_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=  (binop_list xor_bit))`;
+
+val _ = Define `
+ ((not_vec0:(sail_values$bitU)list ->(sail_values$bitU)list)=  (MAP not_bit))`;
+
+
+(*val arith_op_double_bl : forall 'a 'b. Bitvector 'a =>
+  (Num.integer -> Num.integer -> Num.integer) -> bool -> 'a -> 'a -> list Sail_values.bitU*)
+val _ = Define `
+ ((arith_op_double_bl:'a sail_values$Bitvector_class ->(int -> int -> int) -> bool -> 'a -> 'a ->(sail_values$bitU)list)dict_Sail_values_Bitvector_a op sign l r=  
+ (let len =(( 2 : int) * 
+  dict_Sail_values_Bitvector_a.length_method l) in
+  let l' = (if sign then exts_bv 
+  dict_Sail_values_Bitvector_a len l else extz_bv dict_Sail_values_Bitvector_a len l) in
+  let r' = (if sign then exts_bv 
+  dict_Sail_values_Bitvector_a len r else extz_bv dict_Sail_values_Bitvector_a len r) in
+  MAP (\ b. b) (arith_op_bits op sign (MAP (\ b. b) l') (MAP (\ b. b) r'))))`;
+
+
+(*val add_vec   : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val adds_vec  : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val sub_vec   : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val subs_vec  : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val mult_vec  : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val mults_vec : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((add_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=    (\ l r. MAP (\ b. b) (arith_op_bits (+) F (MAP (\ b. b) l) (MAP (\ b. b) r))))`;
+
+val _ = Define `
+ ((adds_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=   (\ l r. MAP (\ b. b) (arith_op_bits (+) T (MAP (\ b. b) l) (MAP (\ b. b) r))))`;
+
+val _ = Define `
+ ((sub_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=    (\ l r. MAP (\ b. b) (arith_op_bits (-) F (MAP (\ b. b) l) (MAP (\ b. b) r))))`;
+
+val _ = Define `
+ ((subs_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=   (\ l r. MAP (\ b. b) (arith_op_bits (-) T (MAP (\ b. b) l) (MAP (\ b. b) r))))`;
+
+val _ = Define `
+ ((mult_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=   (arith_op_double_bl 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) F))`;
+
+val _ = Define `
+ ((mults_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)=  (arith_op_double_bl 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) T))`;
+
+
+(*val add_vec_int       : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val adds_vec_int      : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val sub_vec_int       : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val subs_vec_int      : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val mult_vec_int      : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val mults_vec_int     : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((add_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)   l r=  (arith_op_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (+) F l r))`;
+
+val _ = Define `
+ ((adds_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)  l r=  (arith_op_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (+) T l r))`;
+
+val _ = Define `
+ ((sub_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)   l r=  (arith_op_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (-) F l r))`;
+
+val _ = Define `
+ ((subs_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)  l r=  (arith_op_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (-) T l r))`;
+
+val _ = Define `
+ ((mult_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)  l r=  (arith_op_double_bl 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) F l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`;
+
+val _ = Define `
+ ((mults_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list) l r=  (arith_op_double_bl 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) T l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`;
+
+
+(*val add_int_vec       : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val adds_int_vec      : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val sub_int_vec       : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val subs_int_vec      : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val mult_int_vec      : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val mults_int_vec     : Num.integer -> list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((add_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)   l r=  (arith_op_int_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (+) F l r))`;
+
+val _ = Define `
+ ((adds_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)  l r=  (arith_op_int_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (+) T l r))`;
+
+val _ = Define `
+ ((sub_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)   l r=  (arith_op_int_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (-) F l r))`;
+
+val _ = Define `
+ ((subs_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)  l r=  (arith_op_int_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (-) T l r))`;
+
+val _ = Define `
+ ((mult_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list)  l r=  (arith_op_double_bl 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) F (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`;
+
+val _ = Define `
+ ((mults_int_vec0:int ->(sail_values$bitU)list ->(sail_values$bitU)list) l r=  (arith_op_double_bl 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) ( * ) T (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`;
+
+
+(*val add_vec_bit      : list Sail_values.bitU -> Sail_values.bitU -> list Sail_values.bitU*)
+(*val adds_vec_bit     : list Sail_values.bitU -> Sail_values.bitU -> list Sail_values.bitU*)
+(*val sub_vec_bit      : list Sail_values.bitU -> Sail_values.bitU -> list Sail_values.bitU*)
+(*val subs_vec_bit     : list Sail_values.bitU -> Sail_values.bitU -> list Sail_values.bitU*)
+
+val _ = Define `
+ ((add_vec_bool0:'a sail_values$Bitvector_class -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a       l r=  (arith_op_bv_bool 
+  dict_Sail_values_Bitvector_a (+) F l r))`;
+
+val _ = Define `
+ ((add_vec_bit_maybe0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a  l r=  (arith_op_bv_bit 
+  dict_Sail_values_Bitvector_a (+) F l r))`;
+
+val _ = Define `
+ ((add_vec_bit_fail0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a   l r=  (state_monad$maybe_failS "add_vec_bit" (add_vec_bit_maybe0 
+  dict_Sail_values_Bitvector_a l r)))`;
+
+val _ = Define `
+ ((add_vec_bit_oracle0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r=  (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r .  state_monad$returnS (add_vec_bool0 
+  dict_Sail_values_Bitvector_a l r))))`;
+
+val _ = Define `
+ ((add_vec_bit0:(sail_values$bitU)list -> sail_values$bitU ->(sail_values$bitU)list)        l r=  (option_CASE (add_vec_bit_maybe0 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+
+val _ = Define `
+ ((adds_vec_bool0:'a sail_values$Bitvector_class -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a       l r=  (arith_op_bv_bool 
+  dict_Sail_values_Bitvector_a (+) T l r))`;
+
+val _ = Define `
+ ((adds_vec_bit_maybe0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a  l r=  (arith_op_bv_bit 
+  dict_Sail_values_Bitvector_a (+) T l r))`;
+
+val _ = Define `
+ ((adds_vec_bit_fail0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a   l r=  (state_monad$maybe_failS "adds_vec_bit" (adds_vec_bit_maybe0 
+  dict_Sail_values_Bitvector_a l r)))`;
+
+val _ = Define `
+ ((adds_vec_bit_oracle0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r=  (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r .  state_monad$returnS (adds_vec_bool0 
+  dict_Sail_values_Bitvector_a l r))))`;
+
+val _ = Define `
+ ((adds_vec_bit0:(sail_values$bitU)list -> sail_values$bitU ->(sail_values$bitU)list)        l r=  (option_CASE (adds_vec_bit_maybe0 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+
+val _ = Define `
+ ((sub_vec_bool0:'a sail_values$Bitvector_class -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a        l r=  (arith_op_bv_bool 
+  dict_Sail_values_Bitvector_a (-) F l r))`;
+
+val _ = Define `
+ ((sub_vec_bit_maybe0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a   l r=  (arith_op_bv_bit 
+  dict_Sail_values_Bitvector_a (-) F l r))`;
+
+val _ = Define `
+ ((sub_vec_bit_fail0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a    l r=  (state_monad$maybe_failS "sub_vec_bit" (sub_vec_bit_maybe0 
+  dict_Sail_values_Bitvector_a l r)))`;
+
+val _ = Define `
+ ((sub_vec_bit_oracle0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a  l r=  (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r .  state_monad$returnS (sub_vec_bool0 
+  dict_Sail_values_Bitvector_a l r))))`;
+
+val _ = Define `
+ ((sub_vec_bit0:(sail_values$bitU)list -> sail_values$bitU ->(sail_values$bitU)list)         l r=  (option_CASE (sub_vec_bit_maybe0 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+
+val _ = Define `
+ ((subs_vec_bool0:'a sail_values$Bitvector_class -> 'a -> bool -> 'a)dict_Sail_values_Bitvector_a       l r=  (arith_op_bv_bool 
+  dict_Sail_values_Bitvector_a (-) T l r))`;
+
+val _ = Define `
+ ((subs_vec_bit_maybe0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'a option)dict_Sail_values_Bitvector_a  l r=  (arith_op_bv_bit 
+  dict_Sail_values_Bitvector_a (-) T l r))`;
+
+val _ = Define `
+ ((subs_vec_bit_fail0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a   l r=  (state_monad$maybe_failS "sub_vec_bit" (subs_vec_bit_maybe0 
+  dict_Sail_values_Bitvector_a l r)))`;
+
+val _ = Define `
+ ((subs_vec_bit_oracle0:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU -> 'c state_monad$sequential_state ->(('a,'d)state_monad$result#'c state_monad$sequential_state)set)dict_Sail_values_Bitvector_a l r=  (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r .  state_monad$returnS (subs_vec_bool0 
+  dict_Sail_values_Bitvector_a l r))))`;
+
+val _ = Define `
+ ((subs_vec_bit0:(sail_values$bitU)list -> sail_values$bitU ->(sail_values$bitU)list)        l r=  (option_CASE (subs_vec_bit_maybe0 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+
+(*val add_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val add_overflow_vec_signed  : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_signed  : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val mult_overflow_vec        : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val mult_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU)
+let add_overflow_vec         = add_overflow_bv
+let add_overflow_vec_signed  = add_overflow_bv_signed
+let sub_overflow_vec         = sub_overflow_bv
+let sub_overflow_vec_signed  = sub_overflow_bv_signed
+let mult_overflow_vec        = mult_overflow_bv
+let mult_overflow_vec_signed = mult_overflow_bv_signed
+
+val add_overflow_vec_bit         : list bitU -> bitU -> (list bitU * bitU * bitU)
+val add_overflow_vec_bit_signed  : list bitU -> bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_bit         : list bitU -> bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_bit_signed  : list bitU -> bitU -> (list bitU * bitU * bitU)
+let add_overflow_vec_bit         = add_overflow_bv_bit
+let add_overflow_vec_bit_signed  = add_overflow_bv_bit_signed
+let sub_overflow_vec_bit         = sub_overflow_bv_bit
+let sub_overflow_vec_bit_signed  = sub_overflow_bv_bit_signed*)
+
+(*val shiftl       : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val shiftr       : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val arith_shiftr : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val rotl         : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val rotr         : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((shiftl0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= 
+  (shiftl_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((shiftr0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= 
+  (shiftr_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((arith_shiftr0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= 
+  (arith_shiftr_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((rotl0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= 
+  (rotl_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((rotr0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= 
+  (rotr_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val mod_vec        : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val mod_vec_maybe  : list Sail_values.bitU -> list Sail_values.bitU -> Maybe.maybe (list Sail_values.bitU)*)
+(*val mod_vec_fail   : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+(*val mod_vec_oracle : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+val _ = Define `
+ ((mod_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)        l r=  (option_CASE (mod_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+val _ = Define `
+ ((mod_vec_maybe0:(sail_values$bitU)list ->(sail_values$bitU)list ->((sail_values$bitU)list)option)  l r=  (mod_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`;
+
+val _ = Define `
+ ((mod_vec_fail0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "mod_vec" (mod_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`;
+
+val _ = Define `
+ ((mod_vec_oracle0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  (state$of_bits_oracleS 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (mod_vec0 l r)))`;
+
+
+(*val quot_vec        : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val quot_vec_maybe  : list Sail_values.bitU -> list Sail_values.bitU -> Maybe.maybe (list Sail_values.bitU)*)
+(*val quot_vec_fail   : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+(*val quot_vec_oracle : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+val _ = Define `
+ ((quot_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)        l r=  (option_CASE (quot_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+val _ = Define `
+ ((quot_vec_maybe0:(sail_values$bitU)list ->(sail_values$bitU)list ->((sail_values$bitU)list)option)  l r=  (quot_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`;
+
+val _ = Define `
+ ((quot_vec_fail0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "quot_vec" (quot_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`;
+
+val _ = Define `
+ ((quot_vec_oracle0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  (state$of_bits_oracleS 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (quot_vec0 l r)))`;
+
+
+(*val quots_vec        : list Sail_values.bitU -> list Sail_values.bitU -> list Sail_values.bitU*)
+(*val quots_vec_maybe  : list Sail_values.bitU -> list Sail_values.bitU -> Maybe.maybe (list Sail_values.bitU)*)
+(*val quots_vec_fail   : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+(*val quots_vec_oracle : forall 'rv 'e. list Sail_values.bitU -> list Sail_values.bitU -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+val _ = Define `
+ ((quots_vec0:(sail_values$bitU)list ->(sail_values$bitU)list ->(sail_values$bitU)list)        l r=  (option_CASE (quots_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+val _ = Define `
+ ((quots_vec_maybe0:(sail_values$bitU)list ->(sail_values$bitU)list ->((sail_values$bitU)list)option)  l r=  (quots_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`;
+
+val _ = Define `
+ ((quots_vec_fail0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "quots_vec" (quots_bv 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`;
+
+val _ = Define `
+ ((quots_vec_oracle0:(sail_values$bitU)list ->(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  (state$of_bits_oracleS 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (quots_vec0 l r)))`;
+
+
+(*val mod_vec_int        : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val mod_vec_int_maybe  : list Sail_values.bitU -> Num.integer -> Maybe.maybe (list Sail_values.bitU)*)
+(*val mod_vec_int_fail   : forall 'rv 'e. list Sail_values.bitU -> Num.integer -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+(*val mod_vec_int_oracle : forall 'rv 'e. list Sail_values.bitU -> Num.integer -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+val _ = Define `
+ ((mod_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)        l r=  (option_CASE (mod_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+val _ = Define `
+ ((mod_vec_int_maybe0:(sail_values$bitU)list -> int ->((sail_values$bitU)list)option)  l r=  (mod_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`;
+
+val _ = Define `
+ ((mod_vec_int_fail0:(sail_values$bitU)list -> int -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "mod_vec_int" (mod_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`;
+
+val _ = Define `
+ ((mod_vec_int_oracle0:(sail_values$bitU)list -> int -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  (state$of_bits_oracleS 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (mod_vec_int0 l r)))`;
+
+
+(*val quot_vec_int        : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+(*val quot_vec_int_maybe  : list Sail_values.bitU -> Num.integer -> Maybe.maybe (list Sail_values.bitU)*)
+(*val quot_vec_int_fail   : forall 'rv 'e. list Sail_values.bitU -> Num.integer -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+(*val quot_vec_int_oracle : forall 'rv 'e. list Sail_values.bitU -> Num.integer -> Prompt_monad.monad 'rv (list Sail_values.bitU) 'e*)
+val _ = Define `
+ ((quot_vec_int0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)        l r=  (option_CASE (quot_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r) (repeat [BU] (int_of_num (LENGTH l))) I))`;
+
+val _ = Define `
+ ((quot_vec_int_maybe0:(sail_values$bitU)list -> int ->((sail_values$bitU)list)option)  l r=  (quot_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r))`;
+
+val _ = Define `
+ ((quot_vec_int_fail0:(sail_values$bitU)list -> int -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "quot_vec_int" (quot_bv_int 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (instance_Sail_values_Bitvector_list_dict
+   instance_Sail_values_BitU_Sail_values_bitU_dict) l r)))`;
+
+val _ = Define `
+ ((quot_vec_int_oracle0:(sail_values$bitU)list -> int -> 'rv state_monad$sequential_state ->((((sail_values$bitU)list),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  (state$of_bits_oracleS 
+  (instance_Sail_values_Bitvector_list_dict
+     instance_Sail_values_BitU_Sail_values_bitU_dict) (quot_vec_int0 l r)))`;
+
+
+(*val replicate_bits : list Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((replicate_bits0:(sail_values$bitU)list -> int ->(sail_values$bitU)list)= 
+  (replicate_bits_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+
+(*val duplicate : Sail_values.bitU -> Num.integer -> list Sail_values.bitU*)
+val _ = Define `
+ ((duplicate0:sail_values$bitU -> int ->(sail_values$bitU)list)= 
+  (duplicate_bit_bv instance_Sail_values_BitU_Sail_values_bitU_dict))`;
+
+val _ = Define `
+ ((duplicate_maybe0:sail_values$bitU -> int ->((sail_values$bitU)list)option) b n=  (SOME (duplicate0 b n)))`;
+
+val _ = Define `
+ ((duplicate_fail0:sail_values$bitU -> int -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b n=  (state_monad$returnS (duplicate0 b n)))`;
+
+val _ = Define `
+ ((duplicate_oracle0:sail_values$bitU -> int -> 'a state_monad$sequential_state ->((((sail_values$bitU)list),'b)state_monad$result#'a state_monad$sequential_state)set) b n=  (state_monad$bindS  
+(state$bool_of_bitU_oracleS b) (\ b . 
+  state_monad$returnS (duplicate0 (bitU_of_bool b) n))))`;
+
+
+(*val reverse_endianness : list Sail_values.bitU -> list Sail_values.bitU*)
+val _ = Define `
+ ((reverse_endianness0:(sail_values$bitU)list ->(sail_values$bitU)list) v=  (reverse_endianness_list v))`;
+
+
+(*val eq_vec    : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val neq_vec   : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val ult_vec   : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val slt_vec   : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val ugt_vec   : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val sgt_vec   : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val ulteq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val slteq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val ugteq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+(*val sgteq_vec : list Sail_values.bitU -> list Sail_values.bitU -> bool*)
+val _ = Define `
+ ((eq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (eq_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((neq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (neq_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((ult_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (ult_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((slt_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (slt_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((ugt_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (ugt_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((sgt_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (sgt_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((ulteq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (ulteq_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((slteq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (slteq_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((ugteq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (ugteq_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = Define `
+ ((sgteq_vec:(sail_values$bitU)list ->(sail_values$bitU)list -> bool)= 
+  (sgteq_bv
+     (instance_Sail_values_Bitvector_list_dict
+        instance_Sail_values_BitU_Sail_values_bitU_dict)))`;
+
+val _ = export_theory()
+
diff --git a/snapshots/hol4/sail/lib/hol/sail_operators_mwordsScript.sml b/snapshots/hol4/sail/lib/hol/sail_operators_mwordsScript.sml
new file mode 100644
index 00000000..bd0a68ef
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/sail_operators_mwordsScript.sml
@@ -0,0 +1,612 @@
+(*Generated by Lem from ../../src/gen_lib/sail_operators_mwords.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory sail_operatorsTheory prompt_monadTheory promptTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "sail_operators_mwords"
+
+(*open import Pervasives_extra*)
+(*open import Machine_word*)
+(*open import Sail_values*)
+(*open import Sail_operators*)
+(*open import Prompt_monad*)
+(*open import Prompt*)
+val _ = Define `
+ ((uint_maybe:'a words$word ->(int)option) v=  (SOME (lem$w2ui v)))`;
+
+val _ = Define `
+ ((uint_fail:'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) v=  (state_monad$returnS (lem$w2ui v)))`;
+
+val _ = Define `
+ ((uint_oracle:'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) v=  (state_monad$returnS (lem$w2ui v)))`;
+
+val _ = Define `
+ ((sint_maybe:'a words$word ->(int)option) v=  (SOME (integer_word$w2i v)))`;
+
+val _ = Define `
+ ((sint_fail:'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) v=  (state_monad$returnS (integer_word$w2i v)))`;
+
+val _ = Define `
+ ((sint_oracle:'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) v=  (state_monad$returnS (integer_word$w2i v)))`;
+
+
+(*val vec_of_bits_maybe    : forall 'a. Size 'a => list Sail_values.bitU -> Maybe.maybe (Machine_word.mword 'a)*)
+(*val vec_of_bits_fail     : forall 'rv 'a 'e. Size 'a => list Sail_values.bitU -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+(*val vec_of_bits_oracle   : forall 'rv 'a 'e. Size 'a => list Sail_values.bitU -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+(*val vec_of_bits_failwith : forall 'a. Size 'a => list Sail_values.bitU -> Machine_word.mword 'a*)
+(*val vec_of_bits          : forall 'a. Size 'a => list Sail_values.bitU -> Machine_word.mword 'a*)
+val _ = Define `
+ ((vec_of_bits_maybe:(sail_values$bitU)list ->('a words$word)option) bits=  (OPTION_MAP bitstring$v2w (just_list (MAP bool_of_bitU bits))))`;
+
+val _ = Define `
+ ((vec_of_bits_fail:(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) bits=  (state$of_bits_failS 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict bits))`;
+
+val _ = Define `
+ ((vec_of_bits_oracle:(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) bits=  (state$of_bits_oracleS 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict bits))`;
+
+val _ = Define `
+ ((vec_of_bits_failwith:(sail_values$bitU)list -> 'a words$word) bits=  (of_bits_failwith 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict bits))`;
+
+val _ = Define `
+ ((vec_of_bits:(sail_values$bitU)list -> 'a words$word) bits=  (of_bits_failwith 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict bits))`;
+
+
+(*val access_vec_inc : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Sail_values.bitU*)
+val _ = Define `
+ ((access_vec_inc:'a words$word -> int -> sail_values$bitU)= 
+  (access_bv_inc instance_Sail_values_Bitvector_Machine_word_mword_dict))`;
+
+
+(*val access_vec_dec : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Sail_values.bitU*)
+val _ = Define `
+ ((access_vec_dec:'a words$word -> int -> sail_values$bitU)= 
+  (access_bv_dec instance_Sail_values_Bitvector_Machine_word_mword_dict))`;
+
+
+val _ = Define `
+ ((update_vec_dec_maybe:'a words$word -> int -> sail_values$bitU ->('a words$word)option) w i b=  (update_mword_dec w i b))`;
+
+val _ = Define `
+ ((update_vec_dec_fail:'a words$word -> int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) w i b=  (state_monad$bindS  
+(state$bool_of_bitU_fail b) (\ b . 
+  state_monad$returnS (update_mword_bool_dec w i b))))`;
+
+val _ = Define `
+ ((update_vec_dec_oracle:'a words$word -> int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) w i b=  (state_monad$bindS  
+(state$bool_of_bitU_oracleS b) (\ b . 
+  state_monad$returnS (update_mword_bool_dec w i b))))`;
+
+val _ = Define `
+ ((update_vec_dec:'a words$word -> int -> sail_values$bitU -> 'a words$word) w i b=  (maybe_failwith (update_vec_dec_maybe w i b)))`;
+
+
+val _ = Define `
+ ((update_vec_inc_maybe:'a words$word -> int -> sail_values$bitU ->('a words$word)option) w i b=  (update_mword_inc w i b))`;
+
+val _ = Define `
+ ((update_vec_inc_fail:'a words$word -> int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) w i b=  (state_monad$bindS  
+(state$bool_of_bitU_fail b) (\ b . 
+  state_monad$returnS (update_mword_bool_inc w i b))))`;
+
+val _ = Define `
+ ((update_vec_inc_oracle:'a words$word -> int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) w i b=  (state_monad$bindS  
+(state$bool_of_bitU_oracleS b) (\ b . 
+  state_monad$returnS (update_mword_bool_inc w i b))))`;
+
+val _ = Define `
+ ((update_vec_inc:'a words$word -> int -> sail_values$bitU -> 'a words$word) w i b=  (maybe_failwith (update_vec_inc_maybe w i b)))`;
+
+
+(*val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((subrange_vec_dec:'a words$word -> int -> int -> 'b words$word) w i j=  (words$word_extract (nat_of_int i) (nat_of_int j) w))`;
+
+
+(*val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((subrange_vec_inc:'a words$word -> int -> int -> 'b words$word) w i j=  (subrange_vec_dec w ((int_of_num (words$word_len w) -( 1 : int)) - i) ((int_of_num (words$word_len w) -( 1 : int)) - j)))`;
+
+
+(*val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*)
+val _ = Define `
+ ((update_subrange_vec_dec:'a words$word -> int -> int -> 'b words$word -> 'a words$word) w i j w'=  (words$bit_field_insert (nat_of_int i) (nat_of_int j) w' w))`;
+
+
+(*val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*)
+val _ = Define `
+ ((update_subrange_vec_inc:'a words$word -> int -> int -> 'b words$word -> 'a words$word) w i j w'=  (update_subrange_vec_dec w ((int_of_num (words$word_len w) -( 1 : int)) - i) ((int_of_num (words$word_len w) -( 1 : int)) - j) w'))`;
+
+
+(*val extz_vec : forall 'a 'b. Size 'a, Size 'b => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'b*)
+val _ = Define `
+ ((extz_vec:int -> 'a words$word -> 'b words$word) _ w=  (words$w2w w))`;
+
+
+(*val exts_vec : forall 'a 'b. Size 'a, Size 'b => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'b*)
+val _ = Define `
+ ((exts_vec:int -> 'a words$word -> 'b words$word) _ w=  (words$sw2sw w))`;
+
+
+(*val zero_extend : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((zero_extend:'a words$word -> int -> 'b words$word) w _=  (words$w2w w))`;
+
+
+(*val sign_extend : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((sign_extend:'a words$word -> int -> 'b words$word) w _=  (words$sw2sw w))`;
+
+
+(*val vector_truncate : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((vector_truncate:'a words$word -> int -> 'b words$word) w _=  (words$w2w w))`;
+
+
+(*val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => Machine_word.mword 'a -> Machine_word.mword 'b -> Machine_word.mword 'c*)
+val _ = Define `
+ ((concat_vec:'a words$word -> 'b words$word -> 'c words$word)=  words$word_concat)`;
+
+
+(*val cons_vec_bool : forall 'a 'b 'c. Size 'a, Size 'b => bool -> Machine_word.mword 'a -> Machine_word.mword 'b*)
+val _ = Define `
+ ((cons_vec_bool:bool -> 'a words$word -> 'b words$word) b w=  (bitstring$v2w (b :: bitstring$w2v w)))`;
+
+val _ = Define `
+ ((cons_vec_maybe:sail_values$bitU -> 'c words$word ->('b words$word)option) b w=  (OPTION_MAP (\ b .  cons_vec_bool b w) (bool_of_bitU b)))`;
+
+val _ = Define `
+ ((cons_vec_fail:sail_values$bitU -> 'c words$word -> 'd state_monad$sequential_state ->((('b words$word),'e)state_monad$result#'d state_monad$sequential_state)set) b w=  (state_monad$bindS (state$bool_of_bitU_fail b) (\ b .  state_monad$returnS (cons_vec_bool b w))))`;
+
+val _ = Define `
+ ((cons_vec_oracle:sail_values$bitU -> 'c words$word -> 'd state_monad$sequential_state ->((('b words$word),'e)state_monad$result#'d state_monad$sequential_state)set) b w=  (state_monad$bindS (state$bool_of_bitU_oracleS b) (\ b .  state_monad$returnS (cons_vec_bool b w))))`;
+
+val _ = Define `
+ ((cons_vec:sail_values$bitU -> 'a words$word -> 'b words$word) b w=  (maybe_failwith (cons_vec_maybe b w)))`;
+
+
+(*val vec_of_bool : forall 'a. Size 'a => Num.integer -> bool -> Machine_word.mword 'a*)
+val _ = Define `
+ ((vec_of_bool:int -> bool -> 'a words$word) _ b=  (bitstring$v2w [b]))`;
+
+val _ = Define `
+ ((vec_of_bit_maybe:int -> sail_values$bitU ->('a words$word)option) len b=  (OPTION_MAP (vec_of_bool len) (bool_of_bitU b)))`;
+
+val _ = Define `
+ ((vec_of_bit_fail:int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) len b=  (state_monad$bindS (state$bool_of_bitU_fail b) (\ b .  state_monad$returnS (vec_of_bool len b))))`;
+
+val _ = Define `
+ ((vec_of_bit_oracle:int -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) len b=  (state_monad$bindS (state$bool_of_bitU_oracleS b) (\ b .  state_monad$returnS (vec_of_bool len b))))`;
+
+val _ = Define `
+ ((vec_of_bit:int -> sail_values$bitU -> 'a words$word) len b=  (maybe_failwith (vec_of_bit_maybe len b)))`;
+
+
+(*val cast_bool_vec : bool -> Machine_word.mword Machine_word.ty1*)
+val _ = Define `
+ ((cast_bool_vec:bool ->(1)words$word) b=  (vec_of_bool(( 1 : int)) b))`;
+
+val _ = Define `
+ ((cast_unit_vec_maybe:sail_values$bitU ->('a words$word)option) b=  (vec_of_bit_maybe(( 1 : int)) b))`;
+
+val _ = Define `
+ ((cast_unit_vec_fail:sail_values$bitU -> 'a state_monad$sequential_state ->((((1)words$word),'b)state_monad$result#'a state_monad$sequential_state)set) b=  (state_monad$bindS (state$bool_of_bitU_fail b) (\ b .  state_monad$returnS (cast_bool_vec b))))`;
+
+val _ = Define `
+ ((cast_unit_vec_oracle:sail_values$bitU -> 'a state_monad$sequential_state ->((((1)words$word),'b)state_monad$result#'a state_monad$sequential_state)set) b=  (state_monad$bindS (state$bool_of_bitU_oracleS b) (\ b .  state_monad$returnS (cast_bool_vec b))))`;
+
+val _ = Define `
+ ((cast_unit_vec:sail_values$bitU -> 'a words$word) b=  (maybe_failwith (cast_unit_vec_maybe b)))`;
+
+
+(*val msb : forall 'a. Size 'a => Machine_word.mword 'a -> Sail_values.bitU*)
+val _ = Define `
+ ((msb:'a words$word -> sail_values$bitU)= 
+  (most_significant instance_Sail_values_Bitvector_Machine_word_mword_dict))`;
+
+
+(*val int_of_vec : forall 'a. Size 'a => bool -> Machine_word.mword 'a -> Num.integer*)
+val _ = Define `
+ ((int_of_vec:bool -> 'a words$word -> int) sign w=  
+ (if sign
+  then integer_word$w2i w
+  else lem$w2ui w))`;
+
+val _ = Define `
+ ((int_of_vec_maybe:bool -> 'a words$word ->(int)option) sign w=  (SOME (int_of_vec sign w)))`;
+
+val _ = Define `
+ ((int_of_vec_fail:bool -> 'a words$word -> 'b state_monad$sequential_state ->(((int),'c)state_monad$result#'b state_monad$sequential_state)set) sign w=  (state_monad$returnS (int_of_vec sign w)))`;
+
+
+(*val string_of_vec : forall 'a. Size 'a => Machine_word.mword 'a -> string*)
+val _ = Define `
+ ((string_of_vec:'a words$word -> string)= 
+  (string_of_bv instance_Sail_values_Bitvector_Machine_word_mword_dict))`;
+
+
+(*val and_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val or_vec  : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val xor_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val not_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a*)
+val _ = Define `
+ ((and_vec:'a words$word -> 'a words$word -> 'a words$word)=  words$word_and)`;
+
+val _ = Define `
+ ((or_vec:'a words$word -> 'a words$word -> 'a words$word)=   words$word_or)`;
+
+val _ = Define `
+ ((xor_vec:'a words$word -> 'a words$word -> 'a words$word)=  words$word_xor)`;
+
+val _ = Define `
+ ((not_vec:'a words$word -> 'a words$word)=  words$word_1comp)`;
+
+
+(*val add_vec   : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val adds_vec  : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val sub_vec   : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val subs_vec  : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val mult_vec  : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'b*)
+(*val mults_vec : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'b*)
+val _ = Define `
+ ((add_vec:'a words$word -> 'a words$word -> 'a words$word)   l r=  (integer_word$i2w ((int_of_mword F l) + (int_of_mword F r))))`;
+
+val _ = Define `
+ ((adds_vec:'a words$word -> 'a words$word -> 'a words$word)  l r=  (integer_word$i2w ((int_of_mword T l) + (int_of_mword T r))))`;
+
+val _ = Define `
+ ((sub_vec:'a words$word -> 'a words$word -> 'a words$word)   l r=  (integer_word$i2w ((int_of_mword F l) - (int_of_mword F r))))`;
+
+val _ = Define `
+ ((subs_vec:'a words$word -> 'a words$word -> 'a words$word)  l r=  (integer_word$i2w ((int_of_mword T l) - (int_of_mword T r))))`;
+
+val _ = Define `
+ ((mult_vec:'a words$word -> 'a words$word -> 'b words$word)  l r=  (integer_word$i2w ((int_of_mword F (words$w2w l :  'b words$word)) * (int_of_mword F (words$w2w r :  'b words$word)))))`;
+
+val _ = Define `
+ ((mults_vec:'a words$word -> 'a words$word -> 'b words$word) l r=  (integer_word$i2w ((int_of_mword T (words$sw2sw l :  'b words$word)) * (int_of_mword T (words$sw2sw r :  'b words$word)))))`;
+
+
+(*val add_vec_int   : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val adds_vec_int  : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val sub_vec_int   : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val subs_vec_int  : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*)
+(*val mults_vec_int : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((add_vec_int:'a words$word -> int -> 'a words$word)   l r=  (arith_op_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (+)   F l r))`;
+
+val _ = Define `
+ ((adds_vec_int:'a words$word -> int -> 'a words$word)  l r=  (arith_op_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (+)   T  l r))`;
+
+val _ = Define `
+ ((sub_vec_int:'a words$word -> int -> 'a words$word)   l r=  (arith_op_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (-) F l r))`;
+
+val _ = Define `
+ ((subs_vec_int:'a words$word -> int -> 'a words$word)  l r=  (arith_op_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (-) T  l r))`;
+
+val _ = Define `
+ ((mult_vec_int:'a words$word -> int -> 'b words$word)  l r=  (arith_op_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict ( * )  F (words$w2w l :  'b words$word) r))`;
+
+val _ = Define `
+ ((mults_vec_int:'a words$word -> int -> 'b words$word) l r=  (arith_op_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict ( * )  T  (words$sw2sw l :  'b words$word) r))`;
+
+
+(*val add_int_vec   : forall 'a. Size 'a => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val adds_int_vec  : forall 'a. Size 'a => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val sub_int_vec   : forall 'a. Size 'a => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val subs_int_vec  : forall 'a. Size 'a => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'b*)
+(*val mults_int_vec : forall 'a 'b. Size 'a, Size 'b => Num.integer -> Machine_word.mword 'a -> Machine_word.mword 'b*)
+val _ = Define `
+ ((add_int_vec:int -> 'a words$word -> 'a words$word)   l r=  (arith_op_int_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (+)   F l r))`;
+
+val _ = Define `
+ ((adds_int_vec:int -> 'a words$word -> 'a words$word)  l r=  (arith_op_int_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (+)   T  l r))`;
+
+val _ = Define `
+ ((sub_int_vec:int -> 'a words$word -> 'a words$word)   l r=  (arith_op_int_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (-) F l r))`;
+
+val _ = Define `
+ ((subs_int_vec:int -> 'a words$word -> 'a words$word)  l r=  (arith_op_int_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (-) T  l r))`;
+
+val _ = Define `
+ ((mult_int_vec:int -> 'a words$word -> 'b words$word)  l r=  (arith_op_int_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict ( * )  F l (words$w2w r :  'b words$word)))`;
+
+val _ = Define `
+ ((mults_int_vec:int -> 'a words$word -> 'b words$word) l r=  (arith_op_int_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict ( * )  T  l (words$sw2sw r :  'b words$word)))`;
+
+
+(*val add_vec_bool  : forall 'a. Size 'a => Machine_word.mword 'a -> bool -> Machine_word.mword 'a*)
+(*val adds_vec_bool : forall 'a. Size 'a => Machine_word.mword 'a -> bool -> Machine_word.mword 'a*)
+(*val sub_vec_bool  : forall 'a. Size 'a => Machine_word.mword 'a -> bool -> Machine_word.mword 'a*)
+(*val subs_vec_bool : forall 'a. Size 'a => Machine_word.mword 'a -> bool -> Machine_word.mword 'a*)
+
+val _ = Define `
+ ((add_vec_bool:'a words$word -> bool -> 'a words$word)        l r=  (arith_op_bv_bool 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (+) F l r))`;
+
+val _ = Define `
+ ((add_vec_bit_maybe:'a words$word -> sail_values$bitU ->('a words$word)option)   l r=  (OPTION_MAP (add_vec_bool l) (bool_of_bitU r)))`;
+
+val _ = Define `
+ ((add_vec_bit_fail:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set)    l r=  (state_monad$bindS (state$bool_of_bitU_fail r) (\ r .  state_monad$returnS (add_vec_bool l r))))`;
+
+val _ = Define `
+ ((add_vec_bit_oracle:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set)  l r=  (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r .  state_monad$returnS (add_vec_bool l r))))`;
+
+val _ = Define `
+ ((add_vec_bit:'a words$word -> sail_values$bitU -> 'a words$word)         l r=  (maybe_failwith (add_vec_bit_maybe  l r)))`;
+
+
+val _ = Define `
+ ((adds_vec_bool:'a words$word -> bool -> 'a words$word)       l r=  (arith_op_bv_bool 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (+) T  l r))`;
+
+val _ = Define `
+ ((adds_vec_bit_maybe:'a words$word -> sail_values$bitU ->('a words$word)option)  l r=  (OPTION_MAP (adds_vec_bool l) (bool_of_bitU r)))`;
+
+val _ = Define `
+ ((adds_vec_bit_fail:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set)   l r=  (state_monad$bindS (state$bool_of_bitU_fail r) (\ r .  state_monad$returnS (adds_vec_bool l r))))`;
+
+val _ = Define `
+ ((adds_vec_bit_oracle:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r=  (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r .  state_monad$returnS (adds_vec_bool l r))))`;
+
+val _ = Define `
+ ((adds_vec_bit:'a words$word -> sail_values$bitU -> 'a words$word)        l r=  (maybe_failwith (adds_vec_bit_maybe l r)))`;
+
+
+val _ = Define `
+ ((sub_vec_bool:'a words$word -> bool -> 'a words$word)        l r=  (arith_op_bv_bool 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (-) F l r))`;
+
+val _ = Define `
+ ((sub_vec_bit_maybe:'a words$word -> sail_values$bitU ->('a words$word)option)   l r=  (OPTION_MAP (sub_vec_bool l) (bool_of_bitU r)))`;
+
+val _ = Define `
+ ((sub_vec_bit_fail:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set)    l r=  (state_monad$bindS (state$bool_of_bitU_fail r) (\ r .  state_monad$returnS (sub_vec_bool l r))))`;
+
+val _ = Define `
+ ((sub_vec_bit_oracle:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set)  l r=  (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r .  state_monad$returnS (sub_vec_bool l r))))`;
+
+val _ = Define `
+ ((sub_vec_bit:'a words$word -> sail_values$bitU -> 'a words$word)         l r=  (maybe_failwith (sub_vec_bit_maybe  l r)))`;
+
+
+val _ = Define `
+ ((subs_vec_bool:'a words$word -> bool -> 'a words$word)       l r=  (arith_op_bv_bool 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict (-) T  l r))`;
+
+val _ = Define `
+ ((subs_vec_bit_maybe:'a words$word -> sail_values$bitU ->('a words$word)option)  l r=  (OPTION_MAP (subs_vec_bool l) (bool_of_bitU r)))`;
+
+val _ = Define `
+ ((subs_vec_bit_fail:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set)   l r=  (state_monad$bindS (state$bool_of_bitU_fail r) (\ r .  state_monad$returnS (subs_vec_bool l r))))`;
+
+val _ = Define `
+ ((subs_vec_bit_oracle:'a words$word -> sail_values$bitU -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) l r=  (state_monad$bindS (state$bool_of_bitU_oracleS r) (\ r .  state_monad$returnS (subs_vec_bool l r))))`;
+
+val _ = Define `
+ ((subs_vec_bit:'a words$word -> sail_values$bitU -> 'a words$word)        l r=  (maybe_failwith (subs_vec_bit_maybe  l r)))`;
+
+
+(* TODO
+val maybe_mword_of_bits_overflow : forall 'a. Size 'a => (list bitU * bitU * bitU) -> maybe (mword 'a * bitU * bitU)
+let maybe_mword_of_bits_overflow (bits, overflow, carry) =
+  Maybe.map (fun w -> (w, overflow, carry)) (of_bits bits)
+
+val add_overflow_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
+val adds_overflow_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
+val sub_overflow_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
+val subs_overflow_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
+val mult_overflow_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
+val mults_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
+let add_overflow_vec   l r = maybe_mword_of_bits_overflow (add_overflow_bv l r)
+let adds_overflow_vec  l r = maybe_mword_of_bits_overflow (adds_overflow_bv l r)
+let sub_overflow_vec   l r = maybe_mword_of_bits_overflow (sub_overflow_bv l r)
+let subs_overflow_vec  l r = maybe_mword_of_bits_overflow (subs_overflow_bv l r)
+let mult_overflow_vec  l r = maybe_mword_of_bits_overflow (mult_overflow_bv l r)
+let mults_overflow_vec l r = maybe_mword_of_bits_overflow (mults_overflow_bv l r)
+
+val add_overflow_vec_bit         : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val add_overflow_vec_bit_signed  : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_bit         : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_bit_signed  : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+let add_overflow_vec_bit         = add_overflow_bv_bit
+let add_overflow_vec_bit_signed  = add_overflow_bv_bit_signed
+let sub_overflow_vec_bit         = sub_overflow_bv_bit
+let sub_overflow_vec_bit_signed  = sub_overflow_bv_bit_signed*)
+
+(*val shiftl       : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val shiftr       : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val arith_shiftr : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val rotl         : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val rotr         : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+val _ = Define `
+ ((shiftl:'a words$word -> int -> 'a words$word)=        shiftl_mword)`;
+
+val _ = Define `
+ ((shiftr:'a words$word -> int -> 'a words$word)=        shiftr_mword)`;
+
+val _ = Define `
+ ((arith_shiftr:'a words$word -> int -> 'a words$word)=  arith_shiftr_mword)`;
+
+val _ = Define `
+ ((rotl:'a words$word -> int -> 'a words$word)=          rotl_mword)`;
+
+val _ = Define `
+ ((rotr:'a words$word -> int -> 'a words$word)=          rotr_mword)`;
+
+
+(*val mod_vec        : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val mod_vec_maybe  : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Maybe.maybe (Machine_word.mword 'a)*)
+(*val mod_vec_fail   : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+(*val mod_vec_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+val _ = Define `
+ ((mod_vec:'a words$word -> 'a words$word -> 'a words$word)        l r=  (mod_mword l r))`;
+
+val _ = Define `
+ ((mod_vec_maybe:'a words$word -> 'a words$word ->('a words$word)option)  l r=  (mod_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`;
+
+val _ = Define `
+ ((mod_vec_fail:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "mod_vec" (mod_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`;
+
+val _ = Define `
+ ((mod_vec_oracle:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  
+ ((case (mod_bv instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of
+      SOME w => state_monad$returnS w
+    | NONE => state$mword_oracleS () 
+  )))`;
+
+
+(*val quot_vec        : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val quot_vec_maybe  : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Maybe.maybe (Machine_word.mword 'a)*)
+(*val quot_vec_fail   : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+(*val quot_vec_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+val _ = Define `
+ ((quot_vec:'a words$word -> 'a words$word -> 'a words$word)        l r=  (quot_mword l r))`;
+
+val _ = Define `
+ ((quot_vec_maybe:'a words$word -> 'a words$word ->('a words$word)option)  l r=  (quot_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`;
+
+val _ = Define `
+ ((quot_vec_fail:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "quot_vec" (quot_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`;
+
+val _ = Define `
+ ((quot_vec_oracle:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  
+ ((case (quot_bv instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of
+      SOME w => state_monad$returnS w
+    | NONE => state$mword_oracleS () 
+  )))`;
+
+
+(*val quots_vec        : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Machine_word.mword 'a*)
+(*val quots_vec_maybe  : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Maybe.maybe (Machine_word.mword 'a)*)
+(*val quots_vec_fail   : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+(*val quots_vec_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+val _ = Define `
+ ((quots_vec:'a words$word -> 'a words$word -> 'a words$word)        l r=  (quots_mword l r))`;
+
+val _ = Define `
+ ((quots_vec_maybe:'a words$word -> 'a words$word ->('a words$word)option)  l r=  (quots_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`;
+
+val _ = Define `
+ ((quots_vec_fail:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "quots_vec" (quots_bv 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`;
+
+val _ = Define `
+ ((quots_vec_oracle:'a words$word -> 'a words$word -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  
+ ((case (quots_bv instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of
+      SOME w => state_monad$returnS w
+    | NONE => state$mword_oracleS () 
+  )))`;
+
+
+(*val mod_vec_int        : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val mod_vec_int_maybe  : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Maybe.maybe (Machine_word.mword 'a)*)
+(*val mod_vec_int_fail   : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Num.integer -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+(*val mod_vec_int_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Num.integer -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+val _ = Define `
+ ((mod_vec_int:'a words$word -> int -> 'a words$word)        l r=  (mod_mword_int l r))`;
+
+val _ = Define `
+ ((mod_vec_int_maybe:'a words$word -> int ->('a words$word)option)  l r=  (mod_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`;
+
+val _ = Define `
+ ((mod_vec_int_fail:'a words$word -> int -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "mod_vec_int" (mod_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`;
+
+val _ = Define `
+ ((mod_vec_int_oracle:'a words$word -> int -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  
+ ((case (mod_bv_int instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of
+      SOME w => state_monad$returnS w
+    | NONE => state$mword_oracleS () 
+  )))`;
+
+
+(*val quot_vec_int        : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'a*)
+(*val quot_vec_int_maybe  : forall 'a. Size 'a => Machine_word.mword 'a -> Num.integer -> Maybe.maybe (Machine_word.mword 'a)*)
+(*val quot_vec_int_fail   : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Num.integer -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+(*val quot_vec_int_oracle : forall 'rv 'a 'e. Size 'a => Machine_word.mword 'a -> Num.integer -> Prompt_monad.monad 'rv (Machine_word.mword 'a) 'e*)
+val _ = Define `
+ ((quot_vec_int:'a words$word -> int -> 'a words$word)        l r=  (quot_mword_int l r))`;
+
+val _ = Define `
+ ((quot_vec_int_maybe:'a words$word -> int ->('a words$word)option)  l r=  (quot_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r))`;
+
+val _ = Define `
+ ((quot_vec_int_fail:'a words$word -> int -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set)   l r=  (state_monad$maybe_failS "quot_vec_int" (quot_bv_int 
+  instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r)))`;
+
+val _ = Define `
+ ((quot_vec_int_oracle:'a words$word -> int -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) l r=  
+ ((case (quot_bv_int instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict l r) of
+      SOME w => state_monad$returnS w
+    | NONE => state$mword_oracleS () 
+  )))`;
+
+
+(*val replicate_bits : forall 'a 'b. Size 'a, Size 'b => Machine_word.mword 'a -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((replicate_bits:'a words$word -> int -> 'b words$word) v count1=  (bitstring$v2w (repeat (bitstring$w2v v) count1)))`;
+
+
+(*val duplicate_bool : forall 'a. Size 'a => bool -> Num.integer -> Machine_word.mword 'a*)
+val _ = Define `
+ ((duplicate_bool:bool -> int -> 'a words$word)   b n=  (bitstring$v2w (repeat [b] n)))`;
+
+val _ = Define `
+ ((duplicate_maybe:sail_values$bitU -> int ->('a words$word)option)  b n=  (OPTION_MAP (\ b .  duplicate_bool b n) (bool_of_bitU b)))`;
+
+val _ = Define `
+ ((duplicate_fail:sail_values$bitU -> int -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set)   b n=  (state_monad$bindS (state$bool_of_bitU_fail b) (\ b .  state_monad$returnS (duplicate_bool b n))))`;
+
+val _ = Define `
+ ((duplicate_oracle:sail_values$bitU -> int -> 'b state_monad$sequential_state ->((('a words$word),'c)state_monad$result#'b state_monad$sequential_state)set) b n=  (state_monad$bindS (state$bool_of_bitU_oracleS b) (\ b .  state_monad$returnS (duplicate_bool b n))))`;
+
+val _ = Define `
+ ((duplicate:sail_values$bitU -> int -> 'a words$word)        b n=  (maybe_failwith (duplicate_maybe b n)))`;
+
+
+(*val reverse_endianness : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a*)
+val _ = Define `
+ ((reverse_endianness:'a words$word -> 'a words$word) v=  (bitstring$v2w (reverse_endianness_list (bitstring$w2v v))))`;
+
+
+(*val eq_vec    : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val neq_vec   : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val ult_vec   : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val slt_vec   : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val ugt_vec   : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val sgt_vec   : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val ulteq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val slteq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val ugteq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+(*val sgteq_vec : forall 'a. Size 'a => Machine_word.mword 'a -> Machine_word.mword 'a -> bool*)
+val _ = export_theory()
+
diff --git a/snapshots/hol4/sail/lib/hol/sail_valuesScript.sml b/snapshots/hol4/sail/lib/hol/sail_valuesScript.sml
new file mode 100644
index 00000000..2d6c019a
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/sail_valuesScript.sml
@@ -0,0 +1,1238 @@
+(*Generated by Lem from ../../src/gen_lib/sail_values.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory lem_machine_wordTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "sail_values"
+
+(*open import Pervasives_extra*)
+(*open import Machine_word*)
+(*open import Sail_impl_base*)
+
+
+val _ = type_abbrev( "ii" , ``: int``);
+val _ = type_abbrev( "nn" , ``: num``);
+
+(*val nat_of_int : Num.integer -> nat*)
+val _ = Define `
+ ((nat_of_int:int -> num) i=  (if i <( 0 : int) then( 0 : num) else Num (ABS (I i))))`;
+
+
+(*val pow : Num.integer -> Num.integer -> Num.integer*)
+val _ = Define `
+ ((pow0:int -> int -> int) m n=  (m ** (nat_of_int n)))`;
+
+
+val _ = Define `
+ ((pow2:int -> int) n=  (pow0(( 2 : int)) n))`;
+
+
+(*val eq : forall 'a. Eq 'a => 'a -> 'a -> bool*)
+
+(*val neq : forall 'a. Eq 'a => 'a -> 'a -> bool*)
+
+(*let add_int l r = integerAdd l r
+let add_signed l r = integerAdd l r
+let sub_int l r = integerMinus l r
+let mult_int l r = integerMult l r
+let div_int l r = integerDiv l r
+let div_nat l r = natDiv l r
+let power_int_nat l r = integerPow l r
+let power_int_int l r = integerPow l (nat_of_int r)
+let negate_int i = integerNegate i
+let min_int l r = integerMin l r
+let max_int l r = integerMax l r
+
+let add_real l r = realAdd l r
+let sub_real l r = realMinus l r
+let mult_real l r = realMult l r
+let div_real l r = realDiv l r
+let negate_real r = realNegate r
+let abs_real r = realAbs r
+let power_real b e = realPowInteger b e*)
+
+(*val prerr_endline : string -> unit*)
+val _ = Define `
+ ((prerr_endline:string -> unit) _=  () )`;
+
+
+(*val print_int : string -> Num.integer -> unit*)
+val _ = Define `
+ ((print_int:string -> int -> unit) msg i=  (prerr_endline ( STRCAT msg (stringFromInteger i))))`;
+
+
+(*val putchar : Num.integer -> unit*)
+val _ = Define `
+ ((putchar:int -> unit) _=  () )`;
+
+
+(*val shr_int : ii -> ii -> ii*)
+ val shr_int_defn = Hol_defn "shr_int" `
+ ((shr_int:int -> int -> int) x s=  (if s >( 0 : int) then shr_int (x /( 2 : int)) (s -( 1 : int)) else x))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn shr_int_defn;
+
+(*val shl_int : Num.integer -> Num.integer -> Num.integer*)
+ val shl_int_defn = Hol_defn "shl_int" `
+ ((shl_int:int -> int -> int) i shift=  (if shift >( 0 : int) then( 2 : int) * shl_int i (shift -( 1 : int)) else i))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn shl_int_defn;
+val _ = Define `
+ ((take_list:int -> 'a list -> 'a list) n xs=  (TAKE (nat_of_int n) xs))`;
+
+val _ = Define `
+ ((drop_list:int -> 'a list -> 'a list) n xs=  (DROP (nat_of_int n) xs))`;
+
+
+(*val repeat : forall 'a. list 'a -> Num.integer -> list 'a*)
+ val repeat_defn = Hol_defn "repeat" `
+ ((repeat:'a list -> int -> 'a list) xs n=  
+ (if n <=( 0 : int) then []
+  else xs ++ repeat xs (n -( 1 : int))))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn repeat_defn;
+
+val _ = Define `
+ ((duplicate_to_list:'a -> int -> 'a list) bit length=  (repeat [bit] length))`;
+
+
+ val replace_defn = Hol_defn "replace" `
+ ((replace:'a list -> int -> 'a -> 'a list) bs (n : int) b'=  ((case bs of
+    [] => []
+  | b :: bs =>
+     if n =( 0 : int) then b' :: bs
+              else b :: replace bs (n -( 1 : int)) b'
+  )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn replace_defn;
+
+val _ = Define `
+ ((upper:'a -> 'a) n=  n)`;
+
+
+(* Modulus operation corresponding to quot below -- result
+   has sign of dividend. *)
+val _ = Define `
+ ((hardware_mod:int -> int -> int) (a: int) (b:int) : int=  
+ (let m = ((ABS a) % (ABS b)) in
+  if a <( 0 : int) then ~ m else m))`;
+
+
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
+val _ = Define `
+ ((hardware_quot:int -> int -> int) (a:int) (b:int) : int=  
+ (let q = ((ABS a) / (ABS b)) in
+  if ((a<( 0 : int)) <=> (b<( 0 : int))) then
+    q  (* same sign -- result positive *)
+  else
+    ~ q))`;
+ (* different sign -- result negative *)
+
+val _ = Define `
+ ((max_64u:int)=  (((( 2 : int))**(( 64 : num))) -( 1 : int)))`;
+
+val _ = Define `
+ ((max_64:int)=   (((( 2 : int))**(( 63 : num))) -( 1 : int)))`;
+
+val _ = Define `
+ ((min_64:int)=  (( 0 : int) - ((( 2 : int))**(( 63 : num)))))`;
+
+val _ = Define `
+ ((max_32u:int)=  ((( 4294967295 : int) : int)))`;
+
+val _ = Define `
+ ((max_32:int)=   ((( 2147483647 : int) : int)))`;
+
+val _ = Define `
+ ((min_32:int)=   ((( 0 : int) -( 2147483648 : int) : int)))`;
+
+val _ = Define `
+ ((max_8:int)=    ((( 127 : int) : int)))`;
+
+val _ = Define `
+ ((min_8:int)=    ((( 0 : int) -( 128 : int) : int)))`;
+
+val _ = Define `
+ ((max_5:int)=    ((( 31 : int) : int)))`;
+
+val _ = Define `
+ ((min_5:int)=    ((( 0 : int) -( 32 : int) : int)))`;
+
+
+(* just_list takes a list of maybes and returns Just xs if all elements have
+   a value, and Nothing if one of the elements is Nothing. *)
+(*val just_list : forall 'a. list (Maybe.maybe 'a) -> Maybe.maybe (list 'a)*)
+ val just_list_defn = Hol_defn "just_list" `
+ ((just_list:('a option)list ->('a list)option) l=  ((case l of
+    [] => SOME []
+  | (x :: xs) =>
+    (case (x, just_list xs) of
+        (SOME x, SOME xs) => SOME (x :: xs)
+      | (_, _) => NONE
+    )
+  )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn just_list_defn;
+
+(*val maybe_failwith : forall 'a. Maybe.maybe 'a -> 'a*)
+val _ = Define `
+ ((maybe_failwith:'a option -> 'a)= 
+  (\x .  (case x of   SOME a => a | NONE => failwith "maybe_failwith" )))`;
+
+
+(*** Bits *)
+val _ = Hol_datatype `
+ bitU = B0 | B1 | BU`;
+
+
+val _ = Define `
+ ((showBitU:bitU -> string)= 
+  (\x .  (case x of   B0 => "O" | B1 => "I" | BU => "U" )))`;
+
+
+val _ = Define `
+ ((bitU_char:bitU -> char)= 
+  (\x .  (case x of   B0 => #"0" | B1 => #"1" | BU => #"?" )))`;
+
+
+val _ = Define `
+((instance_Show_Show_Sail_values_bitU_dict:(bitU)lem_show$Show_class)= (<|
+
+  show_method := showBitU|>))`;
+
+
+(*val compare_bitU : bitU -> bitU -> Basic_classes.ordering*)
+val _ = Define `
+ ((compare_bitU:bitU -> bitU -> lem_basic_classes$ordering) l r=  ((case (l, r) of
+    (BU, BU) => EQ
+  | (B0, B0) => EQ
+  | (B1, B1) => EQ
+  | (BU, _)  => LT
+  | (_, BU)  => GT
+  | (B0, _)  => LT
+  | (_, _)   => GT
+)))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_Sail_values_bitU_dict:(bitU)lem_basic_classes$Ord_class)= (<|
+
+  compare_method := compare_bitU;
+
+  isLess_method := (\  l r. (compare_bitU l r) = LT);
+
+  isLessEqual_method := (\ l r. (compare_bitU l r) <> GT);
+
+  isGreater_method := (\  l r. (compare_bitU l r) = GT);
+
+  isGreaterEqual_method := (\ l r. (compare_bitU l r) <> LT)|>))`;
+
+
+val _ = Hol_datatype `
+(*  'a *) BitU_class= <|
+  to_bitU_method : 'a -> bitU;
+  of_bitU_method : bitU -> 'a
+|>`;
+
+
+val _ = Define `
+((instance_Sail_values_BitU_Sail_values_bitU_dict:(bitU)BitU_class)= (<|
+
+  to_bitU_method := (\ b. b);
+
+  of_bitU_method := (\ b. b)|>))`;
+
+
+val _ = Define `
+ ((bool_of_bitU:bitU ->(bool)option)= 
+  (\x .  (case x of   B0 => SOME F | B1 => SOME T | BU => NONE )))`;
+
+
+val _ = Define `
+ ((bitU_of_bool:bool -> bitU) b=  (if b then B1 else B0))`;
+
+
+(*instance (BitU bool)
+  let to_bitU = bitU_of_bool
+  let of_bitU = bool_of_bitU
+end*)
+
+val _ = Define `
+ ((cast_bit_bool:bitU ->(bool)option)=  bool_of_bitU)`;
+
+
+val _ = Define `
+ ((not_bit:bitU -> bitU)= 
+  (\x .  (case x of   B1 => B0 | B0 => B1 | BU => BU )))`;
+
+
+(*val is_one : Num.integer -> bitU*)
+val _ = Define `
+ ((is_one:int -> bitU) i=  
+ (if i =( 1 : int) then B1 else B0))`;
+
+
+(*val and_bit : bitU -> bitU -> bitU*)
+val _ = Define `
+ ((and_bit:bitU -> bitU -> bitU) x y=  
+ ((case (x, y) of
+      (B0, _) => B0
+    | (_, B0) => B0
+    | (B1, B1) => B1
+    | (_, _) => BU
+  )))`;
+
+
+(*val or_bit : bitU -> bitU -> bitU*)
+val _ = Define `
+ ((or_bit:bitU -> bitU -> bitU) x y=  
+ ((case (x, y) of
+      (B1, _) => B1
+    | (_, B1) => B1
+    | (B0, B0) => B0
+    | (_, _) => BU
+  )))`;
+
+
+(*val xor_bit : bitU -> bitU -> bitU*)
+val _ = Define `
+ ((xor_bit:bitU -> bitU -> bitU) x y=  
+((case (x, y) of
+      (B0, B0) => B0
+    | (B0, B1) => B1
+    | (B1, B0) => B1
+    | (B1, B1) => B0
+    | (_, _) => BU
+  )))`;
+
+
+(*val &. : bitU -> bitU -> bitU*)
+
+(*val |. : bitU -> bitU -> bitU*)
+
+(*val +. : bitU -> bitU -> bitU*)
+
+
+(*** Bool lists ***)
+
+(*val bools_of_nat_aux : Num.integer -> Num.natural -> list bool -> list bool*)
+ val bools_of_nat_aux_defn = Hol_defn "bools_of_nat_aux" `
+ ((bools_of_nat_aux:int -> num ->(bool)list ->(bool)list) len x acc=  
+ (if len <=( 0 : int) then acc
+  else bools_of_nat_aux (len -( 1 : int)) (x DIV( 2:num)) ((if (x MOD( 2:num)) =( 1:num) then T else F) :: acc)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn bools_of_nat_aux_defn;
+val _ = Define `
+ ((bools_of_nat:int -> num ->(bool)list) len n=  (bools_of_nat_aux len n []))`;
+ (*List.reverse (bools_of_nat_aux n)*)
+
+(*val nat_of_bools_aux : Num.natural -> list bool -> Num.natural*)
+ val nat_of_bools_aux_defn = Hol_defn "nat_of_bools_aux" `
+ ((nat_of_bools_aux:num ->(bool)list -> num) acc bs=  ((case bs of
+    [] => acc
+  | T :: bs => nat_of_bools_aux ((( 2:num) * acc) +( 1:num)) bs
+  | F :: bs => nat_of_bools_aux (( 2:num) * acc) bs
+)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn nat_of_bools_aux_defn;
+val _ = Define `
+ ((nat_of_bools:(bool)list -> num) bs=  (nat_of_bools_aux(( 0:num)) bs))`;
+
+
+(*val unsigned_of_bools : list bool -> Num.integer*)
+val _ = Define `
+ ((unsigned_of_bools:(bool)list -> int) bs=  (int_of_num (nat_of_bools bs)))`;
+
+
+(*val signed_of_bools : list bool -> Num.integer*)
+val _ = Define `
+ ((signed_of_bools:(bool)list -> int) bs=  
+ ((case bs of
+      T :: _  =>( 0 : int) - (( 1 : int) + (unsigned_of_bools (MAP (\ x. ~ x) bs)))
+    | F :: _ => unsigned_of_bools bs
+    | [] =>( 0 : int) (* Treat empty list as all zeros *)
+  )))`;
+
+
+(*val int_of_bools : bool -> list bool -> Num.integer*)
+val _ = Define `
+ ((int_of_bools:bool ->(bool)list -> int) sign bs=  (if sign then signed_of_bools bs else unsigned_of_bools bs))`;
+
+
+(*val pad_list : forall 'a. 'a -> list 'a -> Num.integer -> list 'a*)
+ val pad_list_defn = Hol_defn "pad_list" `
+ ((pad_list:'a -> 'a list -> int -> 'a list) x xs n=  
+ (if n <=( 0 : int) then xs else pad_list x (x :: xs) (n -( 1 : int))))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn pad_list_defn;
+
+val _ = Define `
+ ((ext_list:'a -> int -> 'a list -> 'a list) pad len xs=  
+ (let longer = (len - (int_of_num (LENGTH xs))) in
+  if longer <( 0 : int) then DROP (nat_of_int (ABS (longer))) xs
+  else pad_list pad xs longer))`;
+
+
+val _ = Define `
+ ((extz_bools:int ->(bool)list ->(bool)list) len bs=  (ext_list F len bs))`;
+
+val _ = Define `
+ ((exts_bools:int ->(bool)list ->(bool)list) len bs=  
+ ((case bs of
+      T :: _ => ext_list T len bs
+    | _ => ext_list F len bs
+  )))`;
+
+
+ val add_one_bool_ignore_overflow_aux_defn = Hol_defn "add_one_bool_ignore_overflow_aux" `
+ ((add_one_bool_ignore_overflow_aux:(bool)list ->(bool)list) bits=  ((case bits of
+    [] => []
+  | F :: bits => T :: bits
+  | T :: bits => F :: add_one_bool_ignore_overflow_aux bits
+)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn add_one_bool_ignore_overflow_aux_defn;
+
+val _ = Define `
+ ((add_one_bool_ignore_overflow:(bool)list ->(bool)list) bits=  
+ (REVERSE (add_one_bool_ignore_overflow_aux (REVERSE bits))))`;
+
+
+(*let bool_list_of_int n =
+  let bs_abs = false :: bools_of_nat (naturalFromInteger (abs n)) in
+  if n >= (0 : integer) then bs_abs
+  else add_one_bool_ignore_overflow (List.map not bs_abs)
+let bools_of_int len n = exts_bools len (bool_list_of_int n)*)
+val _ = Define `
+ ((bools_of_int:int -> int ->(bool)list) len n=  
+ (let bs_abs = (bools_of_nat len (Num (ABS (ABS n)))) in
+  if n >= (( 0 : int) : int) then bs_abs
+  else add_one_bool_ignore_overflow (MAP (\ x. ~ x) bs_abs)))`;
+
+
+(*** Bit lists ***)
+
+(*val has_undefined_bits : list bitU -> bool*)
+val _ = Define `
+ ((has_undefined_bits:(bitU)list -> bool) bs=  (EXISTS (\x .  
+  (case x of BU => T | _ => F )) bs))`;
+
+
+val _ = Define `
+ ((bits_of_nat:int -> num ->(bitU)list) len n=  (MAP bitU_of_bool (bools_of_nat len n)))`;
+
+
+val _ = Define `
+ ((nat_of_bits:(bitU)list ->(num)option) bits=  
+ ((case (just_list (MAP bool_of_bitU bits)) of
+      SOME bs => SOME (nat_of_bools bs)
+    | NONE => NONE
+  )))`;
+
+
+val _ = Define `
+ ((not_bits:(bitU)list ->(bitU)list)=  (MAP not_bit))`;
+
+
+(*val binop_list : forall 'a. ('a -> 'a -> 'a) -> list 'a -> list 'a -> list 'a*)
+val _ = Define `
+ ((binop_list:('a -> 'a -> 'a) -> 'a list -> 'a list -> 'a list) op xs ys=  
+ (FOLDR (\ (x, y) acc .  op x y :: acc) [] (list_combine xs ys)))`;
+
+
+val _ = Define `
+ ((unsigned_of_bits:(bitU)list ->(int)option) bits=  
+ ((case (just_list (MAP bool_of_bitU bits)) of
+      SOME bs => SOME (unsigned_of_bools bs)
+    | NONE => NONE
+  )))`;
+
+
+val _ = Define `
+ ((signed_of_bits:(bitU)list ->(int)option) bits=  
+ ((case (just_list (MAP bool_of_bitU bits)) of
+      SOME bs => SOME (signed_of_bools bs)
+    | NONE => NONE
+  )))`;
+
+
+(*val int_of_bits : bool -> list bitU -> Maybe.maybe Num.integer*)
+val _ = Define `
+ ((int_of_bits:bool ->(bitU)list ->(int)option) sign bs=  (if sign then signed_of_bits bs else unsigned_of_bits bs))`;
+
+
+val _ = Define `
+ ((extz_bits:int ->(bitU)list ->(bitU)list) len bits=  (ext_list B0 len bits))`;
+
+val _ = Define `
+ ((exts_bits:int ->(bitU)list ->(bitU)list) len bits=  
+ ((case bits of
+    BU :: _ => ext_list BU len bits
+  | B1 :: _ => ext_list B1 len bits
+  | _ => ext_list B0 len bits
+  )))`;
+
+
+ val add_one_bit_ignore_overflow_aux_defn = Hol_defn "add_one_bit_ignore_overflow_aux" `
+ ((add_one_bit_ignore_overflow_aux:(bitU)list ->(bitU)list) bits=  ((case bits of
+    [] => []
+  | B0 :: bits => B1 :: bits
+  | B1 :: bits => B0 :: add_one_bit_ignore_overflow_aux bits
+  | BU :: bits => BU :: MAP (\b .  
+  (case (b ) of ( _ ) => BU )) bits
+)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn add_one_bit_ignore_overflow_aux_defn;
+
+val _ = Define `
+ ((add_one_bit_ignore_overflow:(bitU)list ->(bitU)list) bits=  
+ (REVERSE (add_one_bit_ignore_overflow_aux (REVERSE bits))))`;
+
+
+(*let bit_list_of_int n = List.map bitU_of_bool (bool_list_of_int n)
+let bits_of_int len n = exts_bits len (bit_list_of_int n)*)
+val _ = Define `
+ ((bits_of_int:int -> int ->(bitU)list) len n=  (MAP bitU_of_bool (bools_of_int len n)))`;
+
+
+(*val arith_op_bits :
+  (Num.integer -> Num.integer -> Num.integer) -> bool -> list bitU -> list bitU -> list bitU*)
+val _ = Define `
+ ((arith_op_bits:(int -> int -> int) -> bool ->(bitU)list ->(bitU)list ->(bitU)list) op sign l r=  
+ ((case (int_of_bits sign l, int_of_bits sign r) of
+      (SOME li, SOME ri) => bits_of_int (int_of_num (LENGTH l)) (op li ri)
+    | (_, _) => repeat [BU] (int_of_num (LENGTH l))
+  )))`;
+
+
+val _ = Define `
+ ((char_of_nibble:bitU#bitU#bitU#bitU ->(char)option)= 
+  (\x .  (case x of
+               (B0, B0, B0, B0) => SOME #"0"
+           | (B0, B0, B0, B1) => SOME #"1"
+           | (B0, B0, B1, B0) => SOME #"2"
+           | (B0, B0, B1, B1) => SOME #"3"
+           | (B0, B1, B0, B0) => SOME #"4"
+           | (B0, B1, B0, B1) => SOME #"5"
+           | (B0, B1, B1, B0) => SOME #"6"
+           | (B0, B1, B1, B1) => SOME #"7"
+           | (B1, B0, B0, B0) => SOME #"8"
+           | (B1, B0, B0, B1) => SOME #"9"
+           | (B1, B0, B1, B0) => SOME #"A"
+           | (B1, B0, B1, B1) => SOME #"B"
+           | (B1, B1, B0, B0) => SOME #"C"
+           | (B1, B1, B0, B1) => SOME #"D"
+           | (B1, B1, B1, B0) => SOME #"E"
+           | (B1, B1, B1, B1) => SOME #"F"
+           | _ => NONE
+         )))`;
+
+
+ val hexstring_of_bits_defn = Hol_defn "hexstring_of_bits" `
+ ((hexstring_of_bits:(bitU)list ->((char)list)option) bs=  ((case bs of
+    b1 :: b2 :: b3 :: b4 :: bs =>
+     let n = (char_of_nibble (b1, b2, b3, b4)) in
+     let s = (hexstring_of_bits bs) in
+     (case (n, s) of
+       (SOME n, SOME s) => SOME (n :: s)
+     | _ => NONE
+     )
+  | _ => NONE
+  )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn hexstring_of_bits_defn;
+
+val _ = Define `
+ ((show_bitlist:(bitU)list -> string) bs=  
+ ((case hexstring_of_bits bs of
+    SOME s => IMPLODE (#"0" :: (#"x" :: s))
+  | NONE => IMPLODE (#"0" :: (#"b" :: MAP bitU_char bs))
+  )))`;
+
+
+(*val subrange_list_inc : forall 'a. list 'a -> Num.integer -> Num.integer -> list 'a*)
+val _ = Define `
+ ((subrange_list_inc:'a list -> int -> int -> 'a list) xs i j=  
+ (let (toJ,suffix0) = (TAKE (nat_of_int (j +( 1 : int))) xs, DROP (nat_of_int (j +( 1 : int))) xs) in
+  let (prefix0,fromItoJ) = (TAKE (nat_of_int i) toJ, DROP (nat_of_int i) toJ) in
+  fromItoJ))`;
+
+
+(*val subrange_list_dec : forall 'a. list 'a -> Num.integer -> Num.integer -> list 'a*)
+val _ = Define `
+ ((subrange_list_dec:'a list -> int -> int -> 'a list) xs i j=  
+ (let top = ((int_of_num (LENGTH xs)) -( 1 : int)) in
+  subrange_list_inc xs (top - i) (top - j)))`;
+
+
+(*val subrange_list : forall 'a. bool -> list 'a -> Num.integer -> Num.integer -> list 'a*)
+val _ = Define `
+ ((subrange_list:bool -> 'a list -> int -> int -> 'a list) is_inc xs i j=  (if is_inc then subrange_list_inc xs i j else subrange_list_dec xs i j))`;
+
+
+(*val update_subrange_list_inc : forall 'a. list 'a -> Num.integer -> Num.integer -> list 'a -> list 'a*)
+val _ = Define `
+ ((update_subrange_list_inc:'a list -> int -> int -> 'a list -> 'a list) xs i j xs'=  
+ (let (toJ,suffix) = (TAKE (nat_of_int (j +( 1 : int))) xs, DROP (nat_of_int (j +( 1 : int))) xs) in
+  let (prefix,fromItoJ0) = (TAKE (nat_of_int i) toJ, DROP (nat_of_int i) toJ) in  
+(prefix ++ xs') ++ suffix))`;
+
+
+(*val update_subrange_list_dec : forall 'a. list 'a -> Num.integer -> Num.integer -> list 'a -> list 'a*)
+val _ = Define `
+ ((update_subrange_list_dec:'a list -> int -> int -> 'a list -> 'a list) xs i j xs'=  
+ (let top = ((int_of_num (LENGTH xs)) -( 1 : int)) in
+  update_subrange_list_inc xs (top - i) (top - j) xs'))`;
+
+
+(*val update_subrange_list : forall 'a. bool -> list 'a -> Num.integer -> Num.integer -> list 'a -> list 'a*)
+val _ = Define `
+ ((update_subrange_list:bool -> 'a list -> int -> int -> 'a list -> 'a list) is_inc xs i j xs'=  
+ (if is_inc then update_subrange_list_inc xs i j xs' else update_subrange_list_dec xs i j xs'))`;
+
+
+(*val access_list_inc : forall 'a. list 'a -> Num.integer -> 'a*)
+val _ = Define `
+ ((access_list_inc:'a list -> int -> 'a) xs n=  (EL (nat_of_int n) xs))`;
+
+
+(*val access_list_dec : forall 'a. list 'a -> Num.integer -> 'a*)
+val _ = Define `
+ ((access_list_dec:'a list -> int -> 'a) xs n=  
+ (let top = ((int_of_num (LENGTH xs)) -( 1 : int)) in
+  access_list_inc xs (top - n)))`;
+
+
+(*val access_list : forall 'a. bool -> list 'a -> Num.integer -> 'a*)
+val _ = Define `
+ ((access_list:bool -> 'a list -> int -> 'a) is_inc xs n=  
+ (if is_inc then access_list_inc xs n else access_list_dec xs n))`;
+
+
+(*val update_list_inc : forall 'a. list 'a -> Num.integer -> 'a -> list 'a*)
+val _ = Define `
+ ((update_list_inc:'a list -> int -> 'a -> 'a list) xs n x=  (LUPDATE x (nat_of_int n) xs))`;
+
+
+(*val update_list_dec : forall 'a. list 'a -> Num.integer -> 'a -> list 'a*)
+val _ = Define `
+ ((update_list_dec:'a list -> int -> 'a -> 'a list) xs n x=  
+ (let top = ((int_of_num (LENGTH xs)) -( 1 : int)) in
+  update_list_inc xs (top - n) x))`;
+
+
+(*val update_list : forall 'a. bool -> list 'a -> Num.integer -> 'a -> list 'a*)
+val _ = Define `
+ ((update_list:bool -> 'a list -> int -> 'a -> 'a list) is_inc xs n x=  
+ (if is_inc then update_list_inc xs n x else update_list_dec xs n x))`;
+
+
+val _ = Define `
+ ((extract_only_bit:(bitU)list -> bitU)= 
+  (\x .  (case x of   [] => BU | [e] => e | _ => BU )))`;
+
+
+(*** Machine words *)
+
+(*val length_mword : forall 'a. Machine_word.mword 'a -> Num.integer*)
+
+(*val slice_mword_dec : forall 'a 'b. Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((slice_mword_dec:'a words$word -> int -> int -> 'b words$word) w i j=  (words$word_extract (nat_of_int j) (nat_of_int i) w))`;
+
+
+(*val slice_mword_inc : forall 'a 'b. Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((slice_mword_inc:'a words$word -> int -> int -> 'b words$word) w i j=  
+ (let top = ((int_of_num (words$word_len w)) -( 1 : int)) in
+  slice_mword_dec w (top - i) (top - j)))`;
+
+
+(*val slice_mword : forall 'a 'b. bool -> Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b*)
+val _ = Define `
+ ((slice_mword:bool -> 'a words$word -> int -> int -> 'b words$word) is_inc w i j=  (if is_inc then slice_mword_inc w i j else slice_mword_dec w i j))`;
+
+
+(*val update_slice_mword_dec : forall 'a 'b. Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*)
+val _ = Define `
+ ((update_slice_mword_dec:'a words$word -> int -> int -> 'b words$word -> 'a words$word) w i j w'=  (words$bit_field_insert (nat_of_int j) (nat_of_int i) w' w))`;
+
+
+(*val update_slice_mword_inc : forall 'a 'b. Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*)
+val _ = Define `
+ ((update_slice_mword_inc:'a words$word -> int -> int -> 'b words$word -> 'a words$word) w i j w'=  
+ (let top = ((int_of_num (words$word_len w)) -( 1 : int)) in
+  update_slice_mword_dec w (top - i) (top - j) w'))`;
+
+
+(*val update_slice_mword : forall 'a 'b. bool -> Machine_word.mword 'a -> Num.integer -> Num.integer -> Machine_word.mword 'b -> Machine_word.mword 'a*)
+val _ = Define `
+ ((update_slice_mword:bool -> 'a words$word -> int -> int -> 'b words$word -> 'a words$word) is_inc w i j w'=  
+ (if is_inc then update_slice_mword_inc w i j w' else update_slice_mword_dec w i j w'))`;
+
+
+(*val access_mword_dec : forall 'a. Machine_word.mword 'a -> Num.integer -> bitU*)
+val _ = Define `
+ ((access_mword_dec:'a words$word -> int -> bitU) w n=  (bitU_of_bool (words$word_bit (nat_of_int n) w)))`;
+
+
+(*val access_mword_inc : forall 'a. Machine_word.mword 'a -> Num.integer -> bitU*)
+val _ = Define `
+ ((access_mword_inc:'a words$word -> int -> bitU) w n=  
+ (let top = ((int_of_num (words$word_len w)) -( 1 : int)) in
+  access_mword_dec w (top - n)))`;
+
+
+(*val access_mword : forall 'a. bool -> Machine_word.mword 'a -> Num.integer -> bitU*)
+val _ = Define `
+ ((access_mword:bool -> 'a words$word -> int -> bitU) is_inc w n=  
+ (if is_inc then access_mword_inc w n else access_mword_dec w n))`;
+
+
+(*val update_mword_bool_dec : forall 'a. Machine_word.mword 'a -> Num.integer -> bool -> Machine_word.mword 'a*)
+val _ = Define `
+ ((update_mword_bool_dec:'a words$word -> int -> bool -> 'a words$word) w n b=  ($:+ (nat_of_int n) b w))`;
+
+val _ = Define `
+ ((update_mword_dec:'a words$word -> int -> bitU ->('a words$word)option) w n b=  (OPTION_MAP (update_mword_bool_dec w n) (bool_of_bitU b)))`;
+
+
+(*val update_mword_bool_inc : forall 'a. Machine_word.mword 'a -> Num.integer -> bool -> Machine_word.mword 'a*)
+val _ = Define `
+ ((update_mword_bool_inc:'a words$word -> int -> bool -> 'a words$word) w n b=  
+ (let top = ((int_of_num (words$word_len w)) -( 1 : int)) in
+  update_mword_bool_dec w (top - n) b))`;
+
+val _ = Define `
+ ((update_mword_inc:'a words$word -> int -> bitU ->('a words$word)option) w n b=  (OPTION_MAP (update_mword_bool_inc w n) (bool_of_bitU b)))`;
+
+
+(*val int_of_mword : forall 'a. bool -> Machine_word.mword 'a -> Num.integer*)
+val _ = Define `
+ ((int_of_mword:bool -> 'a words$word -> int) sign w=  
+ (if sign then integer_word$w2i w else lem$w2ui w))`;
+
+
+(* Translating between a type level number (itself 'n) and an integer *)
+
+val _ = Define `
+ ((size_itself_int:'a itself -> int) x=  (int_of_num (size_itself x)))`;
+
+
+(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
+   the actual integer is ignored. *)
+
+(*val make_the_value : forall 'n. Num.integer -> Machine_word.itself 'n*)
+val _ = Define `
+ ((make_the_value:int -> 'n itself) _=  the_value)`;
+
+
+(*** Bitvectors *)
+
+val _ = Hol_datatype `
+(*  'a *) Bitvector_class= <|
+  bits_of_method : 'a -> bitU list;
+  (* We allow of_bits to be partial, as not all bitvector representations
+     support undefined bits *)
+  of_bits_method : bitU list ->  'a option;
+  of_bools_method : bool list -> 'a;
+  length_method : 'a -> int;
+  (* of_int: the first parameter specifies the desired length of the bitvector *)
+  of_int_method : int -> int -> 'a;
+  (* Conversion to integers is undefined if any bit is undefined *)
+  unsigned_method : 'a ->  int option;
+  signed_method : 'a ->  int option;
+  (* Lifting of integer operations to bitvectors:  The boolean flag indicates
+     whether to treat the bitvectors as signed (true) or not (false). *)
+  arith_op_bv_method : (int -> int -> int) -> bool -> 'a -> 'a -> 'a
+|>`;
+
+
+(*val of_bits_failwith : forall 'a. Bitvector 'a => list bitU -> 'a*)
+val _ = Define `
+ ((of_bits_failwith:'a Bitvector_class ->(bitU)list -> 'a)dict_Sail_values_Bitvector_a bits=  (maybe_failwith (
+  dict_Sail_values_Bitvector_a.of_bits_method bits)))`;
+
+
+val _ = Define `
+ ((int_of_bv:'a Bitvector_class -> bool -> 'a ->(int)option)dict_Sail_values_Bitvector_a sign=  (if sign then  
+  dict_Sail_values_Bitvector_a.signed_method else  dict_Sail_values_Bitvector_a.unsigned_method))`;
+
+
+val _ = Define `
+((instance_Sail_values_Bitvector_list_dict:'a BitU_class ->('a list)Bitvector_class)dict_Sail_values_BitU_a= (<|
+
+  bits_of_method := (\ v. MAP  
+  dict_Sail_values_BitU_a.to_bitU_method v);
+
+  of_bits_method := (\ v. SOME (MAP  
+  dict_Sail_values_BitU_a.of_bitU_method v));
+
+  of_bools_method := (\ v. MAP  
+  dict_Sail_values_BitU_a.of_bitU_method (MAP bitU_of_bool v));
+
+  length_method := (\ xs. int_of_num (LENGTH xs));
+
+  of_int_method := (\ len n. MAP  
+  dict_Sail_values_BitU_a.of_bitU_method (bits_of_int len n));
+
+  unsigned_method := (\ v. unsigned_of_bits (MAP  
+  dict_Sail_values_BitU_a.to_bitU_method v));
+
+  signed_method := (\ v. signed_of_bits (MAP  
+  dict_Sail_values_BitU_a.to_bitU_method v));
+
+  arith_op_bv_method := (\ op sign l r. MAP  
+  dict_Sail_values_BitU_a.of_bitU_method (arith_op_bits op sign (MAP  
+  dict_Sail_values_BitU_a.to_bitU_method l) (MAP  dict_Sail_values_BitU_a.to_bitU_method r)))|>))`;
+
+
+val _ = Define `
+((instance_Sail_values_Bitvector_Machine_word_mword_dict:('a words$word)Bitvector_class)= (<|
+
+  bits_of_method := (\ v. MAP bitU_of_bool (bitstring$w2v v));
+
+  of_bits_method := (\ v. OPTION_MAP bitstring$v2w (just_list (MAP bool_of_bitU v)));
+
+  of_bools_method := (\ v. bitstring$v2w v);
+
+  length_method := (\ v. int_of_num (words$word_len v));
+
+  of_int_method := (\i n .  
+  (case (i ,n ) of ( _ , n ) => integer_word$i2w n ));
+
+  unsigned_method := (\ v. SOME (lem$w2ui v));
+
+  signed_method := (\ v. SOME (integer_word$w2i v));
+
+  arith_op_bv_method := (\ op sign l r. integer_word$i2w (op (int_of_mword sign l) (int_of_mword sign r)))|>))`;
+
+
+val _ = Define `
+ ((access_bv_inc:'a Bitvector_class -> 'a -> int -> bitU)dict_Sail_values_Bitvector_a v n=  (access_list T  (
+  dict_Sail_values_Bitvector_a.bits_of_method v) n))`;
+
+val _ = Define `
+ ((access_bv_dec:'a Bitvector_class -> 'a -> int -> bitU)dict_Sail_values_Bitvector_a v n=  (access_list F (
+  dict_Sail_values_Bitvector_a.bits_of_method v) n))`;
+
+
+val _ = Define `
+ ((update_bv_inc:'a Bitvector_class -> 'a -> int -> bitU ->(bitU)list)dict_Sail_values_Bitvector_a v n b=  (update_list T  (
+  dict_Sail_values_Bitvector_a.bits_of_method v) n b))`;
+
+val _ = Define `
+ ((update_bv_dec:'a Bitvector_class -> 'a -> int -> bitU ->(bitU)list)dict_Sail_values_Bitvector_a v n b=  (update_list F (
+  dict_Sail_values_Bitvector_a.bits_of_method v) n b))`;
+
+
+val _ = Define `
+ ((subrange_bv_inc:'a Bitvector_class -> 'a -> int -> int ->(bitU)list)dict_Sail_values_Bitvector_a v i j=  (subrange_list T  (
+  dict_Sail_values_Bitvector_a.bits_of_method v) i j))`;
+
+val _ = Define `
+ ((subrange_bv_dec:'a Bitvector_class -> 'a -> int -> int ->(bitU)list)dict_Sail_values_Bitvector_a v i j=  (subrange_list F (
+  dict_Sail_values_Bitvector_a.bits_of_method v) i j))`;
+
+
+val _ = Define `
+ ((update_subrange_bv_inc:'a Bitvector_class -> 'b Bitvector_class -> 'b -> int -> int -> 'a ->(bitU)list)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b v i j v'=  (update_subrange_list T  (
+  dict_Sail_values_Bitvector_b.bits_of_method v) i j (dict_Sail_values_Bitvector_a.bits_of_method v')))`;
+
+val _ = Define `
+ ((update_subrange_bv_dec:'a Bitvector_class -> 'b Bitvector_class -> 'b -> int -> int -> 'a ->(bitU)list)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b v i j v'=  (update_subrange_list F (
+  dict_Sail_values_Bitvector_b.bits_of_method v) i j (dict_Sail_values_Bitvector_a.bits_of_method v')))`;
+
+
+(*val extz_bv : forall 'a. Bitvector 'a => Num.integer -> 'a -> list bitU*)
+val _ = Define `
+ ((extz_bv:'a Bitvector_class -> int -> 'a ->(bitU)list)dict_Sail_values_Bitvector_a n v=  (extz_bits n (
+  dict_Sail_values_Bitvector_a.bits_of_method v)))`;
+
+
+(*val exts_bv : forall 'a. Bitvector 'a => Num.integer -> 'a -> list bitU*)
+val _ = Define `
+ ((exts_bv:'a Bitvector_class -> int -> 'a ->(bitU)list)dict_Sail_values_Bitvector_a n v=  (exts_bits n (
+  dict_Sail_values_Bitvector_a.bits_of_method v)))`;
+
+
+(*val string_of_bv : forall 'a. Bitvector 'a => 'a -> string*)
+val _ = Define `
+ ((string_of_bv:'a Bitvector_class -> 'a -> string)dict_Sail_values_Bitvector_a v=  (show_bitlist (
+  dict_Sail_values_Bitvector_a.bits_of_method v)))`;
+
+
+(*** Bytes and addresses *)
+
+val _ = type_abbrev( "memory_byte" , ``: bitU list``);
+
+(*val byte_chunks : forall 'a. list 'a -> Maybe.maybe (list (list 'a))*)
+ val byte_chunks_defn = Hol_defn "byte_chunks" `
+ ((byte_chunks:'a list ->(('a list)list)option) bs=  ((case bs of
+    [] => SOME []
+  | a::b::c::d::e::f::g::h::rest =>
+     OPTION_BIND (byte_chunks rest) (\ rest .  SOME ([a;b;c;d;e;f;g;h] :: rest))
+  | _ => NONE
+)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn byte_chunks_defn;
+
+(*val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> Maybe.maybe (list memory_byte)*)
+val _ = Define `
+ ((bytes_of_bits:'a Bitvector_class -> 'a ->((memory_byte)list)option)dict_Sail_values_Bitvector_a bs=  (byte_chunks (
+  dict_Sail_values_Bitvector_a.bits_of_method bs)))`;
+
+
+(*val bits_of_bytes : list memory_byte -> list bitU*)
+val _ = Define `
+ ((bits_of_bytes:((bitU)list)list ->(bitU)list) bs=  (FLAT (MAP (\ v. MAP (\ b. b) v) bs)))`;
+
+
+val _ = Define `
+ ((mem_bytes_of_bits:'a Bitvector_class -> 'a ->(((bitU)list)list)option)dict_Sail_values_Bitvector_a bs=  (OPTION_MAP REVERSE (bytes_of_bits 
+  dict_Sail_values_Bitvector_a bs)))`;
+
+val _ = Define `
+ ((bits_of_mem_bytes:((bitU)list)list ->(bitU)list) bs=  (bits_of_bytes (REVERSE bs)))`;
+
+
+(*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU
+let bitv_of_byte_lifteds v =
+  foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v
+
+val bitv_of_bytes : list Sail_impl_base.byte -> list bitU
+let bitv_of_bytes v =
+  foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v
+
+val byte_lifteds_of_bitv : list bitU -> list byte_lifted
+let byte_lifteds_of_bitv bits =
+  let bits = List.map bit_lifted_of_bitU bits in
+  byte_lifteds_of_bit_lifteds bits
+
+val bytes_of_bitv : list bitU -> list byte
+let bytes_of_bitv bits =
+  let bits = List.map bit_of_bitU bits in
+  bytes_of_bits bits
+
+val bit_lifteds_of_bitUs : list bitU -> list bit_lifted
+let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits
+
+val bit_lifteds_of_bitv : list bitU -> list bit_lifted
+let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs v
+
+
+val address_lifted_of_bitv : list bitU -> address_lifted
+let address_lifted_of_bitv v =
+  let byte_lifteds = byte_lifteds_of_bitv v in
+  let maybe_address_integer =
+    match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with
+    | Just bs -> Just (integer_of_byte_list bs)
+    | _ -> Nothing
+    end in
+  Address_lifted byte_lifteds maybe_address_integer
+
+val bitv_of_address_lifted : address_lifted -> list bitU
+let bitv_of_address_lifted (Address_lifted bs _) = bitv_of_byte_lifteds bs
+
+val address_of_bitv : list bitU -> address
+let address_of_bitv v =
+  let bytes = bytes_of_bitv v in
+  address_of_byte_list bytes*)
+
+ val reverse_endianness_list_defn = Hol_defn "reverse_endianness_list" `
+ ((reverse_endianness_list:'a list -> 'a list) bits=  
+ (if LENGTH bits <=( 8 : num) then bits else
+    reverse_endianness_list (drop_list(( 8 : int)) bits) ++ take_list(( 8 : int)) bits))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn reverse_endianness_list_defn;
+
+
+(*** Registers *)
+
+(*type register_field = string
+type register_field_index = string * (integer * integer) (* name, start and end *)
+
+type register =
+  | Register of string * (* name *)
+                integer * (* length *)
+                integer * (* start index *)
+                bool * (* is increasing *)
+                  list register_field_index
+  | UndefinedRegister of integer (* length *)
+  | RegisterPair of register * register*)
+
+val _ = Hol_datatype `
+(* ( 'a_regstate, 'b_regval, 'c_a) *) register_ref =
+  <| name : string;
+     (*is_inc : bool;*)
+     read_from :'a_regstate -> 'c_a;
+     write_to :'c_a -> 'a_regstate -> 'a_regstate;
+     of_regval :'b_regval -> 'c_a option;
+     regval_of :'c_a -> 'b_regval |>`;
+
+
+(* Register accessors: pair of functions for reading and writing register values *)
+val _ = type_abbrev((* ( 'regstate, 'regval) *) "register_accessors" , ``:
+  ((string -> 'regstate ->  'regval option) #
+   (string -> 'regval -> 'regstate ->  'regstate option))``);
+
+val _ = Hol_datatype `
+(* ( 'a_regtype, 'b_a) *) field_ref =
+  <| field_name : string;
+     field_start : int;
+     field_is_inc : bool;
+     get_field :'a_regtype -> 'b_a;
+     set_field :'a_regtype -> 'b_a -> 'a_regtype |>`;
+
+
+(*let name_of_reg = function
+  | Register name _ _ _ _ -> name
+  | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister"
+  | RegisterPair _ _ -> failwith "name_of_reg RegisterPair"
+end
+
+let size_of_reg = function
+  | Register _ size _ _ _ -> size
+  | UndefinedRegister size -> size
+  | RegisterPair _ _ -> failwith "size_of_reg RegisterPair"
+end
+
+let start_of_reg = function
+  | Register _ _ start _ _ -> start
+  | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister"
+  | RegisterPair _ _ -> failwith "start_of_reg RegisterPair"
+end
+
+let is_inc_of_reg = function
+  | Register _ _ _ is_inc _ -> is_inc
+  | UndefinedRegister _ -> failwith "is_inc_of_reg UndefinedRegister"
+  | RegisterPair _ _ -> failwith "in_inc_of_reg RegisterPair"
+end
+
+let dir_of_reg = function
+  | Register _ _ _ is_inc _ -> dir_of_bool is_inc
+  | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister"
+  | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair"
+end
+
+let size_of_reg_nat reg = natFromInteger (size_of_reg reg)
+let start_of_reg_nat reg = natFromInteger (start_of_reg reg)
+
+val register_field_indices_aux : register -> register_field -> maybe (integer * integer)
+let rec register_field_indices_aux register rfield =
+  match register with
+  | Register _ _ _ _ rfields -> List.lookup rfield rfields
+  | RegisterPair r1 r2 ->
+      let m_indices = register_field_indices_aux r1 rfield in
+      if isJust m_indices then m_indices else register_field_indices_aux r2 rfield
+  | UndefinedRegister _ -> Nothing
+  end
+
+val register_field_indices : register -> register_field -> integer * integer
+let register_field_indices register rfield =
+  match register_field_indices_aux register rfield with
+  | Just indices -> indices
+  | Nothing -> failwith "Invalid register/register-field combination"
+  end
+
+let register_field_indices_nat reg regfield=
+  let (i,j) = register_field_indices reg regfield in
+  (natFromInteger i,natFromInteger j)*)
+
+(*let rec external_reg_value reg_name v =
+  let (internal_start, external_start, direction) =
+    match reg_name with
+     | Reg _ start size dir ->
+        (start, (if dir = D_increasing then start else (start - (size +1))), dir)
+     | Reg_slice _ reg_start dir (slice_start, _) ->
+        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
+         slice_start, dir)
+     | Reg_field _ reg_start dir _ (slice_start, _) ->
+        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
+         slice_start, dir)
+     | Reg_f_slice _ reg_start dir _ _ (slice_start, _) ->
+        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
+         slice_start, dir)
+     end in
+  let bits = bit_lifteds_of_bitv v in
+  <| rv_bits           = bits;
+     rv_dir            = direction;
+     rv_start          = external_start;
+     rv_start_internal = internal_start |>
+
+val internal_reg_value : register_value -> list bitU
+let internal_reg_value v =
+  List.map bitU_of_bit_lifted v.rv_bits
+         (*(integerFromNat v.rv_start_internal)
+         (v.rv_dir = D_increasing)*)
+
+
+let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
+  match d with
+  (*This is the case the thread/concurrecny model expects, so no change needed*)
+  | D_increasing -> (i,j)
+  | D_decreasing -> let slice_i = start - i in
+                    let slice_j = (i - j) + slice_i in
+                    (slice_i,slice_j)
+  end *)
+
+(* TODO
+let external_reg_whole r =
+  Reg (r.name) (natFromInteger r.start) (natFromInteger r.size) (dir_of_bool r.is_inc)
+
+let external_reg_slice r (i,j) =
+  let start = natFromInteger r.start in
+  let dir = dir_of_bool r.is_inc in
+  Reg_slice (r.name) start dir (external_slice dir start (i,j))
+
+let external_reg_field_whole reg rfield =
+  let (m,n) = register_field_indices_nat reg rfield in
+  let start = start_of_reg_nat reg in
+  let dir = dir_of_reg reg in
+  Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n))
+
+let external_reg_field_slice reg rfield (i,j) =
+  let (m,n) = register_field_indices_nat reg rfield in
+  let start = start_of_reg_nat reg in
+  let dir = dir_of_reg reg in
+  Reg_f_slice (name_of_reg reg) start dir rfield
+              (external_slice dir start (m,n))
+              (external_slice dir start (i,j))*)
+
+(*val external_mem_value : list bitU -> memory_value
+let external_mem_value v =
+  byte_lifteds_of_bitv v $> List.reverse
+
+val internal_mem_value : memory_value -> list bitU
+let internal_mem_value bytes =
+  List.reverse bytes $> bitv_of_byte_lifteds*)
+
+
+(*val foreach : forall 'a 'vars.
+  (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars*)
+ val foreach_defn = Hol_defn "foreach" `
+ ((foreach:'a list -> 'vars ->('a -> 'vars -> 'vars) -> 'vars) l vars body=  
+ ((case l of
+      [] => vars
+    | (x :: xs) => foreach xs (body x vars) body
+  )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn foreach_defn;
+
+(*val index_list : Num.integer -> Num.integer -> Num.integer -> list Num.integer*)
+ val index_list_defn = Hol_defn "index_list" `
+ ((index_list:int -> int -> int ->(int)list) from to step=  
+ (if ((step >( 0 : int)) /\ (from <= to)) \/ ((step <( 0 : int)) /\ (to <= from)) then
+    from :: index_list (from + step) to step
+  else []))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn index_list_defn;
+
+(*val while : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars*)
+ val while_defn = Hol_defn "while" `
+ ((while:'vars ->('vars -> bool) ->('vars -> 'vars) -> 'vars) vars cond body=  
+ (if cond vars then while (body vars) cond body else vars))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn while_defn;
+
+(*val until : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars*)
+ val until_defn = Hol_defn "until" `
+ ((until:'vars ->('vars -> bool) ->('vars -> 'vars) -> 'vars) vars cond body=  
+ (let vars = (body vars) in
+  if cond vars then vars else until (body vars) cond body))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn until_defn;
+
+
+(* convert numbers unsafely to naturals *)
+
+val _ = Hol_datatype `
+(*  'a *) ToNatural_class= <| toNatural_method : 'a -> num |>`;
+
+(* eta-expanded for Isabelle output, otherwise it breaks *)
+val _ = Define `
+((instance_Sail_values_ToNatural_Num_integer_dict:(int)ToNatural_class)= (<|
+
+  toNatural_method := (\ n .  Num (ABS n))|>))`;
+
+val _ = Define `
+((instance_Sail_values_ToNatural_Num_int_dict:(int)ToNatural_class)= (<|
+
+  toNatural_method := (\ n .  ((Num (ABS n)):num))|>))`;
+
+val _ = Define `
+((instance_Sail_values_ToNatural_nat_dict:(num)ToNatural_class)= (<|
+
+  toNatural_method := (\ n .  ( n:num))|>))`;
+
+val _ = Define `
+((instance_Sail_values_ToNatural_Num_natural_dict:(num)ToNatural_class)= (<|
+
+  toNatural_method := (\ n .  n)|>))`;
+
+
+val _ = Define `
+ ((toNaturalFiveTup:'a ToNatural_class -> 'b ToNatural_class -> 'c ToNatural_class -> 'd ToNatural_class -> 'e ToNatural_class -> 'd#'c#'b#'a#'e -> num#num#num#num#num)dict_Sail_values_ToNatural_a dict_Sail_values_ToNatural_b dict_Sail_values_ToNatural_c dict_Sail_values_ToNatural_d dict_Sail_values_ToNatural_e (n1,n2,n3,n4,n5)= 
+  (dict_Sail_values_ToNatural_d.toNatural_method n1, dict_Sail_values_ToNatural_c.toNatural_method n2, dict_Sail_values_ToNatural_b.toNatural_method n3, dict_Sail_values_ToNatural_a.toNatural_method n4, dict_Sail_values_ToNatural_e.toNatural_method n5))`;
+
+
+(* Let the following types be generated by Sail per spec, using either bitlists
+   or machine words as bitvector representation *)
+(*type regfp =
+  | RFull of (string)
+  | RSlice of (string * integer * integer)
+  | RSliceBit of (string * integer)
+  | RField of (string * string)
+
+type niafp =
+  | NIAFP_successor
+  | NIAFP_concrete_address of vector bitU
+  | NIAFP_indirect_address
+
+(* only for MIPS *)
+type diafp =
+  | DIAFP_none
+  | DIAFP_concrete of vector bitU
+  | DIAFP_reg of regfp
+
+let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
+  | RFull name ->
+     let (start,length,direction,_) = reg_info name Nothing in
+     Reg name start length direction
+  | RSlice (name,i,j) ->
+     let i = natFromInteger i in
+     let j = natFromInteger j in
+     let (start,length,direction,_) = reg_info name Nothing in
+     let slice = external_slice direction start (i,j) in
+     Reg_slice name start direction slice
+  | RSliceBit (name,i) ->
+     let i = natFromInteger i in
+     let (start,length,direction,_) = reg_info name Nothing in
+     let slice = external_slice direction start (i,i) in
+     Reg_slice name start direction slice
+  | RField (name,field_name) ->
+     let (start,length,direction,span) = reg_info name (Just field_name) in
+     let slice = external_slice direction start span in
+     Reg_field name start direction field_name slice
+end
+
+let niafp_to_nia reginfo = function
+  | NIAFP_successor -> NIA_successor
+  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
+  | NIAFP_indirect_address -> NIA_indirect_address
+end
+
+let diafp_to_dia reginfo = function
+  | DIAFP_none -> DIA_none
+  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
+  | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
+end
+*)
+val _ = export_theory()
+
diff --git a/snapshots/hol4/sail/lib/hol/stateScript.sml b/snapshots/hol4/sail/lib/hol/stateScript.sml
new file mode 100644
index 00000000..0eb048a0
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/stateScript.sml
@@ -0,0 +1,119 @@
+(*Generated by Lem from ../../src/gen_lib/state.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory sail_valuesTheory state_monadTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "state"
+
+(*open import Pervasives_extra*)
+(*open import Sail_values*)
+(*open import State_monad*)
+(*open import {isabelle} `State_monad_lemmas`*)
+
+(*val iterS_aux : forall 'rv 'a 'e. Num.integer -> (Num.integer -> 'a -> State_monad.monadS 'rv unit 'e) -> list 'a -> State_monad.monadS 'rv unit 'e*)
+ val iterS_aux_defn = Hol_defn "iterS_aux" `
+ ((iterS_aux:int ->(int -> 'a -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'a list -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) i f xs=  ((case xs of
+    x :: xs => seqS (f i x) (iterS_aux (i +( 1 : int)) f xs)
+  | [] => returnS () 
+  )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn iterS_aux_defn;
+
+(*val iteriS : forall 'rv 'a 'e. (Num.integer -> 'a -> State_monad.monadS 'rv unit 'e) -> list 'a -> State_monad.monadS 'rv unit 'e*)
+val _ = Define `
+ ((iteriS:(int -> 'a ->('rv,(unit),'e)state_monad$monadS) -> 'a list -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) f xs=  (iterS_aux(( 0 : int)) f xs))`;
+
+
+(*val iterS : forall 'rv 'a 'e. ('a -> State_monad.monadS 'rv unit 'e) -> list 'a -> State_monad.monadS 'rv unit 'e*)
+val _ = Define `
+ ((iterS:('a -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'a list -> 'rv state_monad$sequential_state ->(((unit),'e)state_monad$result#'rv state_monad$sequential_state)set) f xs=  (iteriS (\i x .  
+  (case (i ,x ) of ( _ , x ) => f x )) xs))`;
+
+
+(*val foreachS : forall 'a 'rv 'vars 'e.
+  list 'a -> 'vars -> ('a -> 'vars -> State_monad.monadS 'rv 'vars 'e) -> State_monad.monadS 'rv 'vars 'e*)
+ val foreachS_defn = Hol_defn "foreachS" `
+ ((foreachS:'a list -> 'vars ->('a -> 'vars -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) xs vars body=  ((case xs of
+    [] => returnS vars
+  | x :: xs => bindS     
+(body x vars) (\ vars . 
+     foreachS xs vars body)
+)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn foreachS_defn;
+
+(*val bool_of_bitU_fail : forall 'rv 'e. Sail_values.bitU -> State_monad.monadS 'rv bool 'e*)
+val _ = Define `
+ ((bool_of_bitU_fail:sail_values$bitU -> 'rv state_monad$sequential_state ->(((bool),'e)state_monad$result#'rv state_monad$sequential_state)set)= 
+  (\x .  (case x of
+               B0 => returnS F
+           | B1 => returnS T
+           | BU => failS "bool_of_bitU"
+         )))`;
+
+
+(*val bool_of_bitU_oracleS : forall 'rv 'e. Sail_values.bitU -> State_monad.monadS 'rv bool 'e*)
+val _ = Define `
+ ((bool_of_bitU_oracleS:sail_values$bitU -> 'rv state_monad$sequential_state ->(((bool),'e)state_monad$result#'rv state_monad$sequential_state)set)= 
+  (\x .  (case x of
+               B0 => returnS F
+           | B1 => returnS T
+           | BU => undefined_boolS () 
+         )))`;
+
+
+(*val bools_of_bits_oracleS : forall 'rv 'e. list Sail_values.bitU -> State_monad.monadS 'rv (list bool) 'e*)
+val _ = Define `
+ ((bools_of_bits_oracleS:(sail_values$bitU)list -> 'rv state_monad$sequential_state ->((((bool)list),'e)state_monad$result#'rv state_monad$sequential_state)set) bits=  
+ (foreachS bits []
+    (\ b bools .  bindS      
+(bool_of_bitU_oracleS b) (\ b . 
+      returnS (bools ++ [b])))))`;
+
+
+(*val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list Sail_values.bitU -> State_monad.monadS 'rv 'a 'e*)
+val _ = Define `
+ ((of_bits_oracleS:'a sail_values$Bitvector_class ->(sail_values$bitU)list ->('rv,'a,'e)state_monad$monadS)dict_Sail_values_Bitvector_a bits=  (bindS  
+(bools_of_bits_oracleS bits) (\ bs . 
+  returnS (dict_Sail_values_Bitvector_a.of_bools_method bs))))`;
+
+
+(*val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list Sail_values.bitU -> State_monad.monadS 'rv 'a 'e*)
+val _ = Define `
+ ((of_bits_failS:'a sail_values$Bitvector_class ->(sail_values$bitU)list ->('rv,'a,'e)state_monad$monadS)dict_Sail_values_Bitvector_a bits=  (maybe_failS "of_bits" (
+  dict_Sail_values_Bitvector_a.of_bits_method bits)))`;
+
+
+(*val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> State_monad.monadS 'rv (Machine_word.mword 'a) 'e*)
+val _ = Define `
+ ((mword_oracleS:unit -> 'rv state_monad$sequential_state ->((('a words$word),'e)state_monad$result#'rv state_monad$sequential_state)set) () =  (bindS  
+(bools_of_bits_oracleS (repeat [BU] (int_of_num (dimindex (the_value : 'a itself))))) (\ bs . 
+  returnS (bitstring$v2w bs))))`;
+
+
+
+(*val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> State_monad.monadS 'rv bool 'e) ->
+                ('vars -> State_monad.monadS 'rv 'vars 'e) -> State_monad.monadS 'rv 'vars 'e*)
+ val whileS_defn = Hol_defn "whileS" `
+ ((whileS:'vars ->('vars -> 'rv state_monad$sequential_state ->(((bool),'e)state_monad$result#'rv state_monad$sequential_state)set) ->('vars -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) vars cond body s=  
+ (( bindS(cond vars) (\ cond_val s' . 
+  if cond_val then
+    ( bindS(body vars) (\ vars s'' .  whileS vars cond body s'')) s'
+  else returnS vars s')) s))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn whileS_defn;
+
+(*val untilS : forall 'rv 'vars 'e. 'vars -> ('vars -> State_monad.monadS 'rv bool 'e) ->
+                ('vars -> State_monad.monadS 'rv 'vars 'e) -> State_monad.monadS 'rv 'vars 'e*)
+ val untilS_defn = Hol_defn "untilS" `
+ ((untilS:'vars ->('vars -> 'rv state_monad$sequential_state ->(((bool),'e)state_monad$result#'rv state_monad$sequential_state)set) ->('vars -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) -> 'rv state_monad$sequential_state ->(('vars,'e)state_monad$result#'rv state_monad$sequential_state)set) vars cond body s=  
+ (( bindS(body vars) (\ vars s' . 
+  ( bindS(cond vars) (\ cond_val s'' . 
+  if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn untilS_defn;
+val _ = export_theory()
+
diff --git a/snapshots/hol4/sail/lib/hol/state_monadScript.sml b/snapshots/hol4/sail/lib/hol/state_monadScript.sml
new file mode 100644
index 00000000..cf4764c0
--- /dev/null
+++ b/snapshots/hol4/sail/lib/hol/state_monadScript.sml
@@ -0,0 +1,348 @@
+(*Generated by Lem from ../../src/gen_lib/state_monad.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory sail_valuesTheory sail_instr_kindsTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "state_monad"
+
+(*open import Pervasives_extra*)
+(*open import Sail_instr_kinds*)
+(*open import Sail_values*)
+
+(* 'a is result type *)
+
+val _ = type_abbrev( "memstate" , ``: (int, sail_values$memory_byte) fmap``);
+val _ = type_abbrev( "tagstate" , ``: (int, sail_values$bitU) fmap``);
+(* type regstate = map string (vector bitU) *)
+
+val _ = Hol_datatype `
+(*  'regs *) sequential_state =
+  <| regstate : 'regs;
+     memstate : memstate;
+     tagstate : tagstate;
+     write_ea :  (sail_instr_kinds$write_kind # int # int)option;
+     last_exclusive_operation_was_load : bool;
+     (* Random bool generator for use as an undefined bit oracle *)
+     next_bool : num -> (bool # num);
+     seed : num |>`;
+
+
+(*val init_state : forall 'regs. 'regs -> (nat -> (bool* nat)) -> nat -> sequential_state 'regs*)
+val _ = Define `
+ ((init_state:'regs ->(num -> bool#num) -> num -> 'regs sequential_state) regs o1 s=  
+ (<| regstate := regs;
+     memstate := FEMPTY;
+     tagstate := FEMPTY;
+     write_ea := NONE;
+     last_exclusive_operation_was_load := F;
+     next_bool := o1;
+     seed := s |>))`;
+
+
+val _ = Hol_datatype `
+ ex =
+    Failure of string
+  | Throw of 'e`;
+
+
+val _ = Hol_datatype `
+ result =
+    Value of 'a
+  | Ex of ( 'e ex)`;
+
+
+(* State, nondeterminism and exception monad with result value type 'a
+   and exception type 'e. *)
+val _ = type_abbrev((* ( 'a_regs, 'b_a, 'c_e) *) "monadS" , ``:'a_regs sequential_state -> (('b_a,'c_e)result #'a_regs sequential_state) set``);
+
+(*val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((returnS:'a -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) a s=  ({(Value a,s)}))`;
+
+
+(*val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e*)
+val _ = Define `
+ ((bindS:('regs sequential_state ->(('a,'e)result#'regs sequential_state)set) ->('a -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) m f (s : 'regs sequential_state)=  
+ (BIGUNION (IMAGE (\x .  
+  (case x of   (Value a, s') => f a s' | (Ex e, s') => {(Ex e, s')} )) (m s))))`;
+
+
+(*val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e*)
+val _ = Define `
+ ((seqS:('regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) ->('regs sequential_state ->(('b,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) m n=  (bindS m (\u .  
+  (case (u ) of ( (_ : unit) ) => n ))))`;
+
+
+(*val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((chooseS:'a set -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) xs s=  (IMAGE (\ x .  (Value x, s)) xs))`;
+
+
+(*val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((readS:('regs sequential_state -> 'a) -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) f=  (\ s .  returnS (f s) s))`;
+
+
+(*val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e*)
+val _ = Define `
+ ((updateS:('regs sequential_state -> 'regs sequential_state) -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) f=  (\ s .  returnS ()  (f s)))`;
+
+
+(*val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((failS:string -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) msg s=  ({(Ex (Failure msg), s)}))`;
+
+
+(*val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e*)
+val _ = Define `
+ ((undefined_boolS:unit -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) () =  (bindS  
+(readS (\ s .  s.next_bool (s.seed))) (\ (b, seed) .  seqS  
+(updateS (\ s .  ( s with<| seed := seed |>)))  
+(returnS b))))`;
+
+
+(*val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((exitS:unit -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) () =  (failS "exit"))`;
+
+
+(*val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((throwS:'e -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) e s=  ({(Ex (Throw e), s)}))`;
+
+
+(*val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) ->  monadS 'regs 'a 'e2*)
+val _ = Define `
+ ((try_catchS:('regs sequential_state ->(('a,'e1)result#'regs sequential_state)set) ->('e1 -> 'regs sequential_state ->(('a,'e2)result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,'e2)result#'regs sequential_state)set) m h s=  
+ (BIGUNION (IMAGE (\x .  
+  (case x of
+        (Value a, s') => returnS a s'
+    | (Ex (Throw e), s') => h e s'
+    | (Ex (Failure msg), s') => {(Ex (Failure msg), s')}
+  )) (m s))))`;
+
+
+(*val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e*)
+val _ = Define `
+ ((assert_expS:bool -> string -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) exp msg=  (if exp then returnS ()  else failS msg))`;
+
+
+(* For early return, we abuse exceptions by throwing and catching
+   the return value. The exception type is "either 'r 'e", where "Right e"
+   represents a proper exception and "Left r" an early return of value "r". *)
+val _ = type_abbrev((* ( 'a_regs, 'b_a, 'c_r, 'd_e) *) "monadRS" , ``:('a_regs,'b_a, (('c_r,'d_e)sum)) monadS``);
+
+(*val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e*)
+val _ = Define `
+ ((early_returnS:'r -> 'regs sequential_state ->(('a,(('r,'e)sum))result#'regs sequential_state)set) r=  (throwS (INL r)))`;
+
+
+(*val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((catch_early_returnS:('regs sequential_state ->(('a,(('a,'e)sum))result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) m=  
+ (try_catchS m
+    (\x .  (case x of   INL a => returnS a | INR e => throwS e ))))`;
+
+
+(* Lift to monad with early return by wrapping exceptions *)
+(*val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e*)
+val _ = Define `
+ ((liftRS:('regs sequential_state ->(('a,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,(('r,'e)sum))result#'regs sequential_state)set) m=  (try_catchS m (\ e .  throwS (INR e))))`;
+
+
+(* Catch exceptions in the presence of early returns *)
+(*val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) ->  monadRS 'regs 'a 'r 'e2*)
+val _ = Define `
+ ((try_catchRS:('regs sequential_state ->(('a,(('r,'e1)sum))result#'regs sequential_state)set) ->('e1 -> 'regs sequential_state ->(('a,(('r,'e2)sum))result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,(('r,'e2)sum))result#'regs sequential_state)set) m h=  
+ (try_catchS m
+    (\x .  (case x of   INL r => throwS (INL r) | INR e => h e ))))`;
+
+
+(*val maybe_failS : forall 'regs 'a 'e. string -> Maybe.maybe 'a -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((maybe_failS:string -> 'a option -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) msg= 
+  (\x .  (case x of   SOME a => returnS a | NONE => failS msg )))`;
+
+
+(*val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs Sail_values.bitU 'e*)
+val _ = Define `
+ ((read_tagS:'a sail_values$Bitvector_class -> 'a ->('regs,(sail_values$bitU),'e)monadS)dict_Sail_values_Bitvector_a addr=  (bindS  
+(maybe_failS "unsigned" (
+  dict_Sail_values_Bitvector_a.unsigned_method addr)) (\ addr . 
+  readS (\ s .  option_CASE (FLOOKUP s.tagstate addr) B0 I))))`;
+
+
+(* Read bytes from memory and return in little endian order *)
+(*val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => Sail_instr_kinds.read_kind -> 'a -> nat -> monadS 'regs (list Sail_values.memory_byte) 'e*)
+val _ = Define `
+ ((read_mem_bytesS:'a sail_values$Bitvector_class -> sail_instr_kinds$read_kind -> 'a -> num ->('regs,((sail_values$memory_byte)list),'e)monadS)dict_Sail_values_Bitvector_a read_kind addr sz=  (bindS  
+(maybe_failS "unsigned" (
+  dict_Sail_values_Bitvector_a.unsigned_method addr)) (\ addr . 
+  let sz = (int_of_num sz) in
+  let addrs = (index_list addr ((addr+sz)-( 1 : int))(( 1 : int))) in  
+  let read_byte = (\ s addr .  FLOOKUP s.memstate addr) in
+  bindS (readS (\ s .  just_list (MAP (read_byte s) addrs)))
+    (\x .  (case x of
+                 SOME mem_val => seqS
+                                   (updateS
+                                      (\ s . 
+                                       if read_is_exclusive read_kind then
+                                         ( s with<| last_exclusive_operation_was_load := T |>)
+                                       else s)) (returnS mem_val)
+             | NONE => failS "read_memS"
+           )))))`;
+
+
+(*val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => Sail_instr_kinds.read_kind -> 'a -> Num.integer -> monadS 'regs 'b 'e*)
+val _ = Define `
+ ((read_memS:'a sail_values$Bitvector_class -> 'b sail_values$Bitvector_class -> sail_instr_kinds$read_kind -> 'a -> int ->('regs,'b,'e)monadS)dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b rk a sz=  (bindS  
+(read_mem_bytesS dict_Sail_values_Bitvector_a rk a (nat_of_int sz)) (\ bytes . 
+  maybe_failS "bits_of_mem_bytes" (
+  dict_Sail_values_Bitvector_b.of_bits_method (bits_of_mem_bytes bytes)))))`;
+
+
+(*val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e*)
+val _ = Define `
+ ((excl_resultS:unit -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) () =  (bindS  
+(readS (\ s .  s.last_exclusive_operation_was_load)) (\ excl_load .  seqS  
+(updateS (\ s .  ( s with<| last_exclusive_operation_was_load := F |>)))  
+(chooseS (if excl_load then {F; T} else {F})))))`;
+
+
+(*val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => Sail_instr_kinds.write_kind -> 'a -> nat -> monadS 'regs unit 'e*)
+val _ = Define `
+ ((write_mem_eaS:'a sail_values$Bitvector_class -> sail_instr_kinds$write_kind -> 'a -> num ->('regs,(unit),'e)monadS)dict_Sail_values_Bitvector_a write_kind addr sz=  (bindS  
+(maybe_failS "unsigned" (
+  dict_Sail_values_Bitvector_a.unsigned_method addr)) (\ addr . 
+  let sz = (int_of_num sz) in
+  updateS (\ s .  ( s with<| write_ea := (SOME (write_kind, addr, sz)) |>)))))`;
+
+
+(* Write little-endian list of bytes to previously announced address *)
+(*val write_mem_bytesS : forall 'regs 'e. list Sail_values.memory_byte -> monadS 'regs bool 'e*)
+val _ = Define `
+ ((write_mem_bytesS:((sail_values$bitU)list)list -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) v=  (bindS  
+(readS (\ s .  s.write_ea)) (\x .  
+  (case x of
+        NONE => failS "write ea has not been announced yet"
+    | SOME (_, addr, sz) =>
+  let addrs = (index_list addr ((addr + sz) - ( 1 : int)) (( 1 : int))) in
+  (*let v = external_mem_value (bits_of v) in*)
+  let a_v = (lem_list$list_combine addrs v) in
+  let write_byte = (\mem p .  (case (mem ,p ) of
+                                  ( mem , (addr, v) ) => mem  |+ ( addr ,  
+                                                        v )
+                              )) in
+  seqS
+    (updateS
+       (\ s .  ( s with<| memstate := (FOLDL write_byte s.memstate a_v) |>)))
+    (returnS T)
+  ))))`;
+
+
+(*val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e*)
+val _ = Define `
+ ((write_mem_valS:'a sail_values$Bitvector_class -> 'a ->('regs,(bool),'e)monadS)dict_Sail_values_Bitvector_a v=  ((case mem_bytes_of_bits 
+  dict_Sail_values_Bitvector_a v of
+    SOME v => write_mem_bytesS v
+  | NONE => failS "write_mem_val"
+)))`;
+
+
+(*val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> Sail_values.bitU -> monadS 'regs bool 'e*)
+val _ = Define `
+ ((write_tagS:'a sail_values$Bitvector_class -> 'a -> sail_values$bitU ->('regs,(bool),'e)monadS)dict_Sail_values_Bitvector_a addr t=  (bindS   
+(maybe_failS "unsigned" (
+  dict_Sail_values_Bitvector_a.unsigned_method addr)) (\ addr .  seqS   
+(updateS (\ s .  ( s with<| tagstate := (s.tagstate |+ (addr, t)) |>)))   
+(returnS T))))`;
+
+
+(*val read_regS : forall 'regs 'rv 'a 'e. Sail_values.register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e*)
+val _ = Define `
+ ((read_regS:('regs,'rv,'a)sail_values$register_ref -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) reg=  (readS (\ s .  reg.read_from s.regstate)))`;
+
+
+(* TODO
+let read_reg_range reg i j state =
+  let v = slice (get_reg state (name_of_reg reg)) i j in
+  [(Value (vec_to_bvec v),state)]
+let read_reg_bit reg i state =
+  let v = access (get_reg state (name_of_reg reg)) i in
+  [(Value v,state)]
+let read_reg_field reg regfield =
+  let (i,j) = register_field_indices reg regfield in
+  read_reg_range reg i j
+let read_reg_bitfield reg regfield =
+  let (i,_) = register_field_indices reg regfield in
+  read_reg_bit reg i *)
+
+(*val read_regvalS : forall 'regs 'rv 'e.
+  Sail_values.register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e*)
+val _ = Define `
+ ((read_regvalS:(string -> 'regs -> 'rv option)#(string -> 'rv -> 'regs -> 'regs option) -> string -> 'regs sequential_state ->(('rv,'e)result#'regs sequential_state)set) (read, _) reg=  (bindS  
+(readS (\ s .  read reg s.regstate)) (\x .  
+  (case x of
+        SOME v => returnS v
+    | NONE => failS ( STRCAT "read_regvalS " reg)
+  ))))`;
+
+
+(*val write_regvalS : forall 'regs 'rv 'e.
+  Sail_values.register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e*)
+val _ = Define `
+ ((write_regvalS:(string -> 'regs -> 'rv option)#(string -> 'rv -> 'regs -> 'regs option) -> string -> 'rv -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) (_, write) reg v=  (bindS  
+(readS (\ s .  write reg v s.regstate)) (\x .  
+  (case x of
+        SOME rs' => updateS (\ s .  ( s with<| regstate := rs' |>))
+    | NONE => failS ( STRCAT "write_regvalS " reg)
+  ))))`;
+
+
+(*val write_regS : forall 'regs 'rv 'a 'e. Sail_values.register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e*)
+val _ = Define `
+ ((write_regS:('regs,'rv,'a)sail_values$register_ref -> 'a -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) reg v=  
+ (updateS (\ s .  ( s with<| regstate := (reg.write_to v s.regstate) |>))))`;
+
+
+(* TODO
+val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e
+let update_reg reg f v state =
+  let current_value = get_reg state reg in
+  let new_value = f current_value v in
+  [(Value (), set_reg state reg new_value)]
+
+let write_reg_field reg regfield = update_reg reg regfield.set_field
+
+val update_reg_range : forall 'regs 'rv 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'rv 'a -> integer -> integer -> 'a -> 'b -> 'a
+let update_reg_range reg i j reg_val new_val = set_bits (reg.is_inc) reg_val i j (bits_of new_val)
+let write_reg_range reg i j = update_reg reg (update_reg_range reg i j)
+
+let update_reg_pos reg i reg_val x = update_list reg.is_inc reg_val i x
+let write_reg_pos reg i = update_reg reg (update_reg_pos reg i)
+
+let update_reg_bit reg i reg_val bit = set_bit (reg.is_inc) reg_val i (to_bitU bit)
+let write_reg_bit reg i = update_reg reg (update_reg_bit reg i)
+
+let update_reg_field_range regfield i j reg_val new_val =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j)
+
+let update_reg_field_pos regfield i reg_val x =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = update_list regfield.field_is_inc current_field_value i x in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i)
+
+let update_reg_field_bit regfield i reg_val bit =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*)
+val _ = export_theory()
+