Update HOL4 snapshot with Thomas' fixes

8 files changed, 127 insertions, 162 deletions

diff --git a/snapshots/hol4/sail/aarch64/aarch64_monoScript.sml b/snapshots/hol4/sail/aarch64/aarch64_monoScript.sml
index b454337e..3c70ce1c 100644
--- a/snapshots/hol4/sail/aarch64/aarch64_monoScript.sml
+++ b/snapshots/hol4/sail/aarch64/aarch64_monoScript.sml
@@ -170,14 +170,17 @@ val _ = Define `
 
 val _ = Define `
  ((is_zero_subrange:'n words$word -> int -> int -> bool) xs i j=
-    (((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) = ((extzv ((int_of_num (words$word_len xs))) (vec_of_bits [B0]  :  1 words$word)  :  'n words$word))))`;
+    (((and_vec xs
+         ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+        :  'n words$word)) = ((extzv ((int_of_num (words$word_len xs))) (vec_of_bits [B0]  :  1 words$word)  :  'n words$word))))`;
 
 
 (*val is_ones_subrange : forall 'n . Size 'n => mword 'n -> ii -> ii -> bool*)
 
 val _ = Define `
  ((is_ones_subrange:'n words$word -> int -> int -> bool) xs i j=
-    (let (m : 'n bits) = ((slice_mask ((int_of_num (words$word_len xs))) j ((j - i))  :  'n words$word)) in
+    (let (m : 'n bits) =
+     ((slice_mask ((int_of_num (words$word_len xs))) j ((((j - i)) + (( 1 : int):ii)))  :  'n words$word)) in
    (((and_vec xs m  :  'n words$word)) = m)))`;
 
 
@@ -209,12 +212,15 @@ val _ = Define `
  ((subrange_subrange_eq:'n words$word -> int -> int -> 'n words$word -> int -> int -> bool) xs i j ys i' j'=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    let ys =
      ((shiftr
-        ((and_vec ys ((slice_mask ((int_of_num (words$word_len xs))) j' ((i' - j'))  :  'n words$word))  :  'n words$word))
-        j'
+        ((and_vec ys
+            ((slice_mask ((int_of_num (words$word_len xs))) j' ((((i' - j')) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j'
        :  'n words$word)) in
    (xs = ys)))`;
 
@@ -225,16 +231,18 @@ val _ = Define `
  ((subrange_subrange_concat:int -> 'n words$word -> int -> int -> 'm words$word -> int -> int -> 's words$word) (s__tv : int) xs i j ys i' j'=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    let ys =
      ((shiftr
-        ((and_vec ys ((slice_mask ((int_of_num (words$word_len ys))) j' ((i' - j'))  :  'm words$word))  :  'm words$word))
-        j'
+        ((and_vec ys
+            ((slice_mask ((int_of_num (words$word_len ys))) j' ((((i' - j')) + (( 1 : int):ii)))  :  'm words$word))
+           :  'm words$word)) j'
        :  'm words$word)) in
    (or_vec
-      ((sub_vec_int ((shiftl ((extzv s__tv xs  :  's words$word)) i'  :  's words$word))
-          ((j' - (( 1 : int):ii)))
+      ((shiftl ((extzv s__tv xs  :  's words$word)) ((((i' - j')) + (( 1 : int):ii)))
          :  's words$word)) ((extzv s__tv ys  :  's words$word))
      :  's words$word)))`;
 
@@ -245,7 +253,9 @@ val _ = Define `
  ((place_subrange:int -> 'n words$word -> int -> int -> int -> 'm words$word) (m__tv : int) xs i j shift=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    (shiftl ((extzv m__tv xs  :  'm words$word)) shift  :  'm words$word)))`;
 
@@ -296,7 +306,9 @@ val _ = Define `
  ((unsigned_subrange:'n words$word -> int -> int -> int) xs i j=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) i
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) i
        :  'n words$word)) in
    lem$w2ui xs))`;
 
diff --git a/snapshots/hol4/sail/cheri/cheriScript.sml b/snapshots/hol4/sail/cheri/cheriScript.sml
index 5fa55723..01410ba7 100644
--- a/snapshots/hol4/sail/cheri/cheriScript.sml
+++ b/snapshots/hol4/sail/cheri/cheriScript.sml
@@ -2904,14 +2904,17 @@ val _ = Define `
 
 val _ = Define `
  ((is_zero_subrange:'n words$word -> int -> int -> bool) xs i j=
-    (((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) = ((extzv ((int_of_num (words$word_len xs))) (vec_of_bits [B0]  :  1 words$word)  :  'n words$word))))`;
+    (((and_vec xs
+         ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+        :  'n words$word)) = ((extzv ((int_of_num (words$word_len xs))) (vec_of_bits [B0]  :  1 words$word)  :  'n words$word))))`;
 
 
 (*val is_ones_subrange : forall 'n . Size 'n => mword 'n -> ii -> ii -> bool*)
 
 val _ = Define `
  ((is_ones_subrange:'n words$word -> int -> int -> bool) xs i j=
-    (let (m : 'n bits) = ((slice_mask ((int_of_num (words$word_len xs))) j ((j - i))  :  'n words$word)) in
+    (let (m : 'n bits) =
+     ((slice_mask ((int_of_num (words$word_len xs))) j ((((j - i)) + (( 1 : int):ii)))  :  'n words$word)) in
    (((and_vec xs m  :  'n words$word)) = m)))`;
 
 
@@ -2943,12 +2946,15 @@ val _ = Define `
  ((subrange_subrange_eq:'n words$word -> int -> int -> 'n words$word -> int -> int -> bool) xs i j ys i' j'=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    let ys =
      ((shiftr
-        ((and_vec ys ((slice_mask ((int_of_num (words$word_len xs))) j' ((i' - j'))  :  'n words$word))  :  'n words$word))
-        j'
+        ((and_vec ys
+            ((slice_mask ((int_of_num (words$word_len xs))) j' ((((i' - j')) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j'
        :  'n words$word)) in
    (xs = ys)))`;
 
@@ -2959,16 +2965,18 @@ val _ = Define `
  ((subrange_subrange_concat:int -> 'n words$word -> int -> int -> 'm words$word -> int -> int -> 's words$word) (s__tv : int) xs i j ys i' j'=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    let ys =
      ((shiftr
-        ((and_vec ys ((slice_mask ((int_of_num (words$word_len ys))) j' ((i' - j'))  :  'm words$word))  :  'm words$word))
-        j'
+        ((and_vec ys
+            ((slice_mask ((int_of_num (words$word_len ys))) j' ((((i' - j')) + (( 1 : int):ii)))  :  'm words$word))
+           :  'm words$word)) j'
        :  'm words$word)) in
    (or_vec
-      ((sub_vec_int ((shiftl ((extzv s__tv xs  :  's words$word)) i'  :  's words$word))
-          ((j' - (( 1 : int):ii)))
+      ((shiftl ((extzv s__tv xs  :  's words$word)) ((((i' - j')) + (( 1 : int):ii)))
          :  's words$word)) ((extzv s__tv ys  :  's words$word))
      :  's words$word)))`;
 
@@ -2979,7 +2987,9 @@ val _ = Define `
  ((place_subrange:int -> 'n words$word -> int -> int -> int -> 'm words$word) (m__tv : int) xs i j shift=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    (shiftl ((extzv m__tv xs  :  'm words$word)) shift  :  'm words$word)))`;
 
@@ -3030,7 +3040,9 @@ val _ = Define `
  ((unsigned_subrange:'n words$word -> int -> int -> int) xs i j=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) i
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) i
        :  'n words$word)) in
    lem$w2ui xs))`;
 
diff --git a/snapshots/hol4/sail/cheri/mips_extrasScript.sml b/snapshots/hol4/sail/cheri/mips_extrasScript.sml
index aef40b53..1af18e62 100644
--- a/snapshots/hol4/sail/cheri/mips_extrasScript.sml
+++ b/snapshots/hol4/sail/cheri/mips_extrasScript.sml
@@ -225,9 +225,18 @@ val _ = Define `
 
 
 val _ = Define `
- ((print_bits:'a Bitvector_class -> string -> 'a -> unit)dict_Sail2_values_Bitvector_a msg bs=  (prerr_endline ( STRCAT msg (string_of_bv 
+ ((print_bits:'a Bitvector_class -> string -> 'a -> unit)dict_Sail2_values_Bitvector_a msg bs=  (print_endline ( STRCAT msg (string_of_bv 
   dict_Sail2_values_Bitvector_a bs))))`;
 
+val _ = Define `
+ ((prerr_bits:'a Bitvector_class -> string -> 'a -> unit)dict_Sail2_values_Bitvector_a msg bs=  (prerr_endline ( STRCAT msg (string_of_bv 
+  dict_Sail2_values_Bitvector_a bs))))`;
+
+
+(*val prerr_string : string -> unit*)
+val _ = Define `
+ ((prerr_string:string -> unit) _=  () )`;
+
 
 (*val get_time_ns : unit -> integer*)
 val _ = Define `
diff --git a/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml b/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
index e6b4da4f..da349336 100644
--- a/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
+++ b/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
@@ -328,76 +328,40 @@ val _ = Define `
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T))`;
 
 
-(*val add_vec_int       : list bitU -> integer -> list bitU*)
-(*val adds_vec_int      : list bitU -> integer -> list bitU*)
-(*val sub_vec_int       : list bitU -> integer -> list bitU*)
-(*val subs_vec_int      : list bitU -> integer -> list bitU*)
-(*val mult_vec_int      : list bitU -> integer -> list bitU*)
-(*val mults_vec_int     : list bitU -> integer -> list bitU*)
+(*val add_vec_int      : list bitU -> integer -> list bitU*)
+(*val sub_vec_int      : list bitU -> integer -> list bitU*)
+(*val mult_vec_int     : list bitU -> integer -> list bitU*)
 val _ = Define `
- ((add_vec_int0:(bitU)list -> int ->(bitU)list)   l r=  (arith_op_bv_int 
-  (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) F l r))`;
-
-val _ = Define `
- ((adds_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_bv_int 
+ ((add_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_bv_int 
   (instance_Sail2_values_Bitvector_list_dict
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) T l r))`;
 
 val _ = Define `
- ((sub_vec_int0:(bitU)list -> int ->(bitU)list)   l r=  (arith_op_bv_int 
-  (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) F l r))`;
-
-val _ = Define `
- ((subs_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_bv_int 
+ ((sub_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_bv_int 
   (instance_Sail2_values_Bitvector_list_dict
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) T l r))`;
 
 val _ = Define `
- ((mult_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_double_bl 
-  (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) F l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`;
-
-val _ = Define `
- ((mults_vec_int0:(bitU)list -> int ->(bitU)list) l r=  (arith_op_double_bl 
+ ((mult_vec_int0:(bitU)list -> int ->(bitU)list) l r=  (arith_op_double_bl 
   (instance_Sail2_values_Bitvector_list_dict
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`;
 
 
-(*val add_int_vec       : integer -> list bitU -> list bitU*)
-(*val adds_int_vec      : integer -> list bitU -> list bitU*)
-(*val sub_int_vec       : integer -> list bitU -> list bitU*)
-(*val subs_int_vec      : integer -> list bitU -> list bitU*)
-(*val mult_int_vec      : integer -> list bitU -> list bitU*)
-(*val mults_int_vec     : integer -> list bitU -> list bitU*)
+(*val add_int_vec      : integer -> list bitU -> list bitU*)
+(*val sub_int_vec      : integer -> list bitU -> list bitU*)
+(*val mult_int_vec     : integer -> list bitU -> list bitU*)
 val _ = Define `
- ((add_int_vec0:int ->(bitU)list ->(bitU)list)   l r=  (arith_op_int_bv 
-  (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) F l r))`;
-
-val _ = Define `
- ((adds_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_int_bv 
+ ((add_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_int_bv 
   (instance_Sail2_values_Bitvector_list_dict
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) T l r))`;
 
 val _ = Define `
- ((sub_int_vec0:int ->(bitU)list ->(bitU)list)   l r=  (arith_op_int_bv 
-  (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) F l r))`;
-
-val _ = Define `
- ((subs_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_int_bv 
+ ((sub_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_int_bv 
   (instance_Sail2_values_Bitvector_list_dict
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) T l r))`;
 
 val _ = Define `
- ((mult_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_double_bl 
-  (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) F (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`;
-
-val _ = Define `
- ((mults_int_vec0:int ->(bitU)list ->(bitU)list) l r=  (arith_op_double_bl 
+ ((mult_int_vec0:int ->(bitU)list ->(bitU)list) l r=  (arith_op_double_bl 
   (instance_Sail2_values_Bitvector_list_dict
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`;
 
diff --git a/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml b/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
index 603daf57..9276cfef 100644
--- a/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
+++ b/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
@@ -278,65 +278,35 @@ 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 => mword 'a -> integer -> mword 'a*)
-(*val adds_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
-(*val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
-(*val subs_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
-(*val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
-(*val mults_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
+(*val add_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
+(*val sub_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
+(*val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
 val _ = Define `
- ((add_vec_int:'a words$word -> int -> 'a words$word)   l r=  (arith_op_bv_int 
-  instance_Sail2_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 
+ ((add_vec_int:'a words$word -> int -> 'a words$word)  l r=  (arith_op_bv_int 
   instance_Sail2_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_Sail2_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 
+ ((sub_vec_int:'a words$word -> int -> 'a words$word)  l r=  (arith_op_bv_int 
   instance_Sail2_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_Sail2_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 
+ ((mult_vec_int:'a words$word -> int -> 'b words$word) l r=  (arith_op_bv_int 
   instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  T  (words$sw2sw l :  'b words$word) r))`;
 
 
-(*val add_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
-(*val adds_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
-(*val sub_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
-(*val subs_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
-(*val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
-(*val mults_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
+(*val add_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
+(*val sub_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
+(*val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
 val _ = Define `
- ((add_int_vec:int -> 'a words$word -> 'a words$word)   l r=  (arith_op_int_bv 
-  instance_Sail2_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 
+ ((add_int_vec:int -> 'a words$word -> 'a words$word)  l r=  (arith_op_int_bv 
   instance_Sail2_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_Sail2_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 
+ ((sub_int_vec:int -> 'a words$word -> 'a words$word)  l r=  (arith_op_int_bv 
   instance_Sail2_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_Sail2_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 
+ ((mult_int_vec:int -> 'a words$word -> 'b words$word) l r=  (arith_op_int_bv 
   instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  T  l (words$sw2sw r :  'b words$word)))`;
 
 
diff --git a/snapshots/hol4/sail/mips/mipsScript.sml b/snapshots/hol4/sail/mips/mipsScript.sml
index 928a7276..2758a979 100644
--- a/snapshots/hol4/sail/mips/mipsScript.sml
+++ b/snapshots/hol4/sail/mips/mipsScript.sml
@@ -2728,14 +2728,17 @@ val _ = Define `
 
 val _ = Define `
  ((is_zero_subrange:'n words$word -> int -> int -> bool) xs i j=
-    (((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) = ((extzv ((int_of_num (words$word_len xs))) (vec_of_bits [B0]  :  1 words$word)  :  'n words$word))))`;
+    (((and_vec xs
+         ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+        :  'n words$word)) = ((extzv ((int_of_num (words$word_len xs))) (vec_of_bits [B0]  :  1 words$word)  :  'n words$word))))`;
 
 
 (*val is_ones_subrange : forall 'n . Size 'n => mword 'n -> ii -> ii -> bool*)
 
 val _ = Define `
  ((is_ones_subrange:'n words$word -> int -> int -> bool) xs i j=
-    (let (m : 'n bits) = ((slice_mask ((int_of_num (words$word_len xs))) j ((j - i))  :  'n words$word)) in
+    (let (m : 'n bits) =
+     ((slice_mask ((int_of_num (words$word_len xs))) j ((((j - i)) + (( 1 : int):ii)))  :  'n words$word)) in
    (((and_vec xs m  :  'n words$word)) = m)))`;
 
 
@@ -2767,12 +2770,15 @@ val _ = Define `
  ((subrange_subrange_eq:'n words$word -> int -> int -> 'n words$word -> int -> int -> bool) xs i j ys i' j'=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    let ys =
      ((shiftr
-        ((and_vec ys ((slice_mask ((int_of_num (words$word_len xs))) j' ((i' - j'))  :  'n words$word))  :  'n words$word))
-        j'
+        ((and_vec ys
+            ((slice_mask ((int_of_num (words$word_len xs))) j' ((((i' - j')) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j'
        :  'n words$word)) in
    (xs = ys)))`;
 
@@ -2783,16 +2789,18 @@ val _ = Define `
  ((subrange_subrange_concat:int -> 'n words$word -> int -> int -> 'm words$word -> int -> int -> 's words$word) (s__tv : int) xs i j ys i' j'=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    let ys =
      ((shiftr
-        ((and_vec ys ((slice_mask ((int_of_num (words$word_len ys))) j' ((i' - j'))  :  'm words$word))  :  'm words$word))
-        j'
+        ((and_vec ys
+            ((slice_mask ((int_of_num (words$word_len ys))) j' ((((i' - j')) + (( 1 : int):ii)))  :  'm words$word))
+           :  'm words$word)) j'
        :  'm words$word)) in
    (or_vec
-      ((sub_vec_int ((shiftl ((extzv s__tv xs  :  's words$word)) i'  :  's words$word))
-          ((j' - (( 1 : int):ii)))
+      ((shiftl ((extzv s__tv xs  :  's words$word)) ((((i' - j')) + (( 1 : int):ii)))
          :  's words$word)) ((extzv s__tv ys  :  's words$word))
      :  's words$word)))`;
 
@@ -2803,7 +2811,9 @@ val _ = Define `
  ((place_subrange:int -> 'n words$word -> int -> int -> int -> 'm words$word) (m__tv : int) xs i j shift=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) j
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) j
        :  'n words$word)) in
    (shiftl ((extzv m__tv xs  :  'm words$word)) shift  :  'm words$word)))`;
 
@@ -2854,7 +2864,9 @@ val _ = Define `
  ((unsigned_subrange:'n words$word -> int -> int -> int) xs i j=
     (let xs =
      ((shiftr
-        ((and_vec xs ((slice_mask ((int_of_num (words$word_len xs))) j ((i - j))  :  'n words$word))  :  'n words$word)) i
+        ((and_vec xs
+            ((slice_mask ((int_of_num (words$word_len xs))) j ((((i - j)) + (( 1 : int):ii)))  :  'n words$word))
+           :  'n words$word)) i
        :  'n words$word)) in
    lem$w2ui xs))`;
 
diff --git a/snapshots/hol4/sail/mips/mips_extrasScript.sml b/snapshots/hol4/sail/mips/mips_extrasScript.sml
index f89e7b2f..5cfb5b2d 100644
--- a/snapshots/hol4/sail/mips/mips_extrasScript.sml
+++ b/snapshots/hol4/sail/mips/mips_extrasScript.sml
@@ -225,9 +225,18 @@ val _ = Define `
 
 
 val _ = Define `
- ((print_bits:'a Bitvector_class -> string -> 'a -> unit)dict_Sail2_values_Bitvector_a msg bs=  (prerr_endline ( STRCAT msg (string_of_bv 
+ ((print_bits:'a Bitvector_class -> string -> 'a -> unit)dict_Sail2_values_Bitvector_a msg bs=  (print_endline ( STRCAT msg (string_of_bv 
   dict_Sail2_values_Bitvector_a bs))))`;
 
+val _ = Define `
+ ((prerr_bits:'a Bitvector_class -> string -> 'a -> unit)dict_Sail2_values_Bitvector_a msg bs=  (prerr_endline ( STRCAT msg (string_of_bv 
+  dict_Sail2_values_Bitvector_a bs))))`;
+
+
+(*val prerr_string : string -> unit*)
+val _ = Define `
+ ((prerr_string:string -> unit) _=  () )`;
+
 
 (*val get_time_ns : unit -> integer*)
 val _ = Define `
diff --git a/snapshots/hol4/sail/riscv/riscvScript.sml b/snapshots/hol4/sail/riscv/riscvScript.sml
index bd56ca74..e4eb3718 100644
--- a/snapshots/hol4/sail/riscv/riscvScript.sml
+++ b/snapshots/hol4/sail/riscv/riscvScript.sml
@@ -8887,25 +8887,16 @@ val _ = Define `
 
 val _ = Define `
  ((translationException:AccessType -> PTW_Error -> ExceptionType) (a : AccessType) (f : PTW_Error)=
-    (let (e : ExceptionType) =
-     ((case (a, f) of
-       (ReadWrite, PTW_Access) => E_SAMO_Access_Fault
-     | (ReadWrite, _) => E_SAMO_Page_Fault
-     | (Read, PTW_Access) => E_Load_Access_Fault
-     | (Read, _) => E_Load_Page_Fault
-     | (Write, PTW_Access) => E_SAMO_Access_Fault
-     | (Write, _) => E_SAMO_Page_Fault
-     | (Fetch, PTW_Access) => E_Fetch_Access_Fault
-     | (Fetch, _) => E_Fetch_Page_Fault
-     )) in
-   let (_ : unit) =
-     (print_endline
-       ((STRCAT "translationException("
-           ((STRCAT ((accessType_to_str a))
-               ((STRCAT ", "
-                   ((STRCAT ((ptw_error_to_str f))
-                       ((STRCAT ") -> " ((exceptionType_to_str e))))))))))))) in
-   e))`;
+    ((case (a, f) of
+     (ReadWrite, PTW_Access) => E_SAMO_Access_Fault
+   | (ReadWrite, _) => E_SAMO_Page_Fault
+   | (Read, PTW_Access) => E_Load_Access_Fault
+   | (Read, _) => E_Load_Page_Fault
+   | (Write, PTW_Access) => E_SAMO_Access_Fault
+   | (Write, _) => E_SAMO_Page_Fault
+   | (Fetch, PTW_Access) => E_Fetch_Access_Fault
+   | (Fetch, _) => E_Fetch_Page_Fault
+   )))`;
 
 
 val _ = Define `
@@ -9296,21 +9287,7 @@ val _ = Define `
    (phys_mem_read Data ((EXTZ (( 64 : int):ii) pte_addr  :  64 words$word)) (( 8 : int):ii) F F F
      : ( ( 64 words$word)MemoryOpResult) M) (\ (w__0 : ( 64 words$word) MemoryOpResult) . 
    (case w__0 of
-     MemException (_) =>
-      let (_ : unit) =
-        (print_endline
-          ((STRCAT "walk39(vaddr="
-              ((STRCAT ((string_of_bits vaddr))
-                  ((STRCAT " level="
-                      ((STRCAT ((stringFromInteger level))
-                          ((STRCAT " pt_base="
-                              ((STRCAT ((string_of_bits ptb))
-                                  ((STRCAT " pt_ofs="
-                                      ((STRCAT ((string_of_bits pt_ofs))
-                                          ((STRCAT " pte_addr="
-                                              ((STRCAT ((string_of_bits pte_addr))
-                                                  ": invalid pte address"))))))))))))))))))))) in
-      sail2_state_monad$returnS (PTW_Failure PTW_Access)
+     MemException (_) => sail2_state_monad$returnS (PTW_Failure PTW_Access)
    | MemValue (v) =>
       let pte = (Mk_SV39_PTE v) in
       let pbits = ((get_SV39_PTE_BITS pte  :  8 words$word)) in