1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
open import Pervasives_extra
open import Machine_word
open import Sail_impl_base
open import Sail_values
open import Sail_operators
(* Specialisation of operators to machine words *)
val access_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU
let access_vec_inc = access_bv_inc
val access_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU
let access_vec_dec = access_bv_dec
val update_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a
let update_vec_inc = update_bv_inc
val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a
let update_vec_dec = update_bv_dec
val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
let subrange_vec_inc = subrange_bv_inc
val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
let subrange_vec_dec = subrange_bv_dec
val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
let update_subrange_vec_inc = update_subrange_bv_inc
val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
let update_subrange_vec_dec = update_subrange_bv_dec
val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let extz_vec = extz_bv
val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let exts_vec = exts_bv
val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
let concat_vec = concat_bv
val cons_vec : forall 'a 'b 'c. Size 'a, Size 'b => bitU -> mword 'a -> mword 'b
let cons_vec = cons_bv
val bool_of_vec : mword ty1 -> bitU
let bool_of_vec = bool_of_bv
val cast_unit_vec : bitU -> mword ty1
let cast_unit_vec = cast_unit_bv
val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a
let vec_of_bit = bv_of_bit
val msb : forall 'a. Size 'a => mword 'a -> bitU
let msb = most_significant
val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer
let int_of_vec = int_of_bv
val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val or_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a
let and_vec = and_bv
let or_vec = or_bv
let xor_vec = xor_bv
let not_vec = not_bv
val add_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val addS_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val sub_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val mult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
val multS_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
let add_vec = add_bv
let addS_vec = addS_bv
let sub_vec = sub_bv
let mult_vec = mult_bv
let multS_vec = multS_bv
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 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
let add_vec_int = add_bv_int
let addS_vec_int = addS_bv_int
let sub_vec_int = sub_bv_int
let mult_vec_int = mult_bv_int
let multS_vec_int = multS_bv_int
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 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
let add_int_vec = add_int_bv
let addS_int_vec = addS_int_bv
let sub_int_vec = sub_int_bv
let mult_int_vec = mult_int_bv
let multS_int_vec = multS_int_bv
val add_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
val addS_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
val sub_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
let add_vec_bit = add_bv_bit
let addS_vec_bit = addS_bv_bit
let sub_vec_bit = sub_bv_bit
val add_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val add_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val sub_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val sub_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val mult_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
val mult_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * 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 : 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 => mword 'a -> integer -> mword 'a
val shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
let shiftl = shiftl_bv
let shiftr = shiftr_bv
let arith_shiftr = arith_shiftr_bv
let rotl = rotl_bv
let rotr = rotr_bv
val mod_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val quot_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val quot_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
let mod_vec = mod_bv
let quot_vec = quot_bv
let quot_vec_signed = quot_bv_signed
val mod_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val quot_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
let mod_vec_int = mod_bv_int
let quot_vec_int = quot_bv_int
val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let replicate_bits = replicate_bits_bv
val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a
let duplicate = duplicate_bit_bv
val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val slt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ugt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val sgt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
let eq_vec = eq_bv
let neq_vec = neq_bv
let ult_vec = ult_bv
let slt_vec = slt_bv
let ugt_vec = ugt_bv
let sgt_vec = sgt_bv
let ulteq_vec = ulteq_bv
let slteq_vec = slteq_bv
let ugteq_vec = ugteq_bv
let sgteq_vec = sgteq_bv
|
