summaryrefslogtreecommitdiff
path: root/snapshots
diff options
context:
space:
mode:
Diffstat (limited to 'snapshots')
-rw-r--r--snapshots/hol4/sail/aarch64/aarch64_monoScript.sml36
-rw-r--r--snapshots/hol4/sail/cheri/cheriScript.sml36
-rw-r--r--snapshots/hol4/sail/cheri/mips_extrasScript.sml11
-rw-r--r--snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml60
-rw-r--r--snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml54
-rw-r--r--snapshots/hol4/sail/mips/mipsScript.sml36
-rw-r--r--snapshots/hol4/sail/mips/mips_extrasScript.sml11
-rw-r--r--snapshots/hol4/sail/riscv/riscvScript.sml45
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:03:20 +0000