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
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
|
module Bitwalker
use int.Int
use int.EuclideanDivision
use array.Array
use ref.Ref
(* use bv.BV32 *)
(* use bv.BV8 *)
(* use bv.BV64 *)
use mach.bv.BVCheck8 as BV8
use mach.bv.BVCheck32 as BV32
use mach.bv.BVCheck64 as BV64
use bv.BVConverter_32_64 as C32_64
use bv.BVConverter_8_32 as C8_32
(* file missing in repository
use mach.bv.BV
*)
function nth8_stream (stream : array BV8.t) (pos : int) : bool =
BV8.nth stream[div pos 8] (7 - mod pos 8)
lemma nth64:
forall value:BV64.t, i:int. 0 <= i < 64 ->
BV64.nth value i = BV64.nth_bv value (C32_64.toBig (BV32.of_int i))
lemma nth8:
forall value:BV8.t, i:int. 0 <= i < 8 ->
BV8.nth value i = BV8.nth_bv value (C8_32.toSmall (BV32.of_int i))
(* *)
let function maxvalue (len : BV32.t) : BV64.t =
BV64.lsl_bv (1:BV64.t) (C32_64.toBig len)
let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
requires { BV32.t'int len < 64}
ensures { BV64.eq_sub x BV64.zeros (BV32.t'int len) (64 - BV32.t'int len)
<-> BV64.t'int x < BV64.t'int (maxvalue len) }
=
assert { BV32.ult len (64:BV32.t) };
assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (64:BV64.t) (C32_64.toBig len))
<-> BV64.ult x (maxvalue len) }
(** return `value` with the bit of index `left` from the left set to `flag` *)
let poke_64bit_bv (value : BV64.t) (left : BV32.t) (flag : bool) : BV64.t
requires { BV32.t'int left < 64 }
ensures { forall i. 0 <= i < 64 /\ i <> 63 - BV32.t'int left ->
BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - BV32.t'int left) }
=
assert { BV32.ult left (64:BV32.t) };
begin
ensures { forall i:BV32.t. i <> BV32.sub (63:BV32.t) left ->
BV64.nth_bv result (C32_64.toBig i) =
BV64.nth_bv value (C32_64.toBig i) }
ensures { flag = BV64.nth_bv result
(C32_64.toBig (BV32.sub (63:BV32.t) left)) }
let mask =
BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.u_sub (63:BV32.t) left))
in
match flag with
| True -> BV64.bw_or value mask
| False -> BV64.bw_and value (BV64.bw_not mask)
end
end
(** return `value` with the bit of index `left` from the left set to `flag` *)
(* version where `left` is an int and not a bitvector, which
is closer to the result of the SPARK translation from signed
integers *)
let poke_64bit (value : BV64.t) (left : int) (flag : bool) : BV64.t
requires { 0 <= left < 64 }
ensures { forall i. 0 <= i < 64 /\ i <> 63 - left ->
BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - left) }
=
let ghost left_bv = BV64.of_int left in
assert { BV64.ult left_bv (64:BV64.t) };
assert { (BV64.sub (63:BV64.t) left_bv) = BV64.of_int (63 - left) };
begin
ensures { forall i:BV64.t. BV64.ule i (63:BV64.t) ->
i <> BV64.sub (63:BV64.t) left_bv ->
BV64.nth_bv result i = BV64.nth_bv value i }
ensures { flag = BV64.nth_bv result (BV64.sub (63:BV64.t) left_bv) }
let mask =
BV64.lsl_bv (1:BV64.t) (BV64.of_int (63 - left))
in
match flag with
| True -> BV64.bw_or value mask
| False -> BV64.bw_and value (BV64.bw_not mask)
end
end
(* return the bit of `byte` at position `left` starting from the
left *)
let peek_8bit_bv (byte : BV8.t) (left : BV32.t) : bool
requires { 0 <= BV32.t'int left < 8 }
ensures { result = BV8.nth byte (7 - BV32.t'int left) }
=
assert {BV32.ult left (8:BV32.t)};
begin
ensures {
result = BV8.nth_bv
byte (BV8.sub (7:BV8.t) (C8_32.toSmall left))}
let mask =
BV32.lsl_bv (1:BV32.t) (BV32.u_sub (7:BV32.t) left)
in
not (BV32.eq (BV32.bw_and (C8_32.toBig byte) mask) 0x0)
end
(* return the bit of the `left`/8 element of `addr` at position mod `left` 8 starting from the left *)
let peek_8bit_array (addr : array BV8.t) (left : BV32.t) : bool
requires { 8 * (length addr) < BV32.two_power_size }
requires { BV32.t'int left < 8 * length addr }
ensures { result = nth8_stream addr (BV32.t'int left) }
=
peek_8bit_bv (addr[ BV32.to_uint (BV32.u_div left (8:BV32.t)) ]) (BV32.u_rem left (8:BV32.t))
(* return a bitvector of 64 bits with its `len` bits of the right
set to the bits between `start` and `start+len` of `addr` *)
let peek (start : BV32.t) (len : BV32.t) (addr : array BV8.t) : BV64.t
requires { BV32.t'int len <= 64 }
requires { BV32.t'int start + BV32.t'int len < BV32.two_power_size }
requires { 8 * length addr < BV32.two_power_size }
ensures { BV32.t'int start + BV32.t'int len > (8 * length addr) ->
result = BV64.zeros }
ensures { BV32.t'int start + BV32.t'int len <= (8 * length addr) ->
(forall i:int. 0 <= i < BV32.t'int len ->
BV64.nth result i
= nth8_stream addr (BV32.t'int start + BV32.t'int len - i - 1))
/\
(forall i:int. BV32.t'int len <= i < 64 -> BV64.nth result i = False) }
=
if (BV32.to_uint (BV32.u_add start len) > ( 8 *length addr ))
then
0x0
else
let retval = ref 0x0 in
let i = ref 0x0 in
let lstart = BV32.u_sub (64:BV32.t) len in
while BV32.ult !i len do variant{ BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
invariant {forall j:int. BV32.t'int len - BV32.t'int !i <= j < BV32.t'int len ->
BV64.nth !retval j
= nth8_stream addr (BV32.t'int start + BV32.t'int len - j - 1)}
invariant {forall j:int. 0 <= j < BV32.t'int len - BV32.t'int !i ->
BV64.nth !retval j
= False}
invariant {forall j:int. BV32.t'int len <= j < 64 ->
BV64.nth !retval j
= False}
let flag = peek_8bit_array addr (BV32.u_add start !i) in
retval := poke_64bit_bv !retval (BV32.u_add lstart !i) flag;
i := BV32.u_add !i (1:BV32.t);
done;
!retval
let peek_64bit (value : BV64.t) (left : BV32.t) : bool
requires {BV32.t'int left < 64}
ensures {result = BV64.nth value (63 - BV32.t'int left)}
=
assert {BV32.ult left (64:BV32.t)};
begin
ensures {result = BV64.nth_bv value
(BV64.sub (63:BV64.t) (C32_64.toBig left))}
let mask = BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.u_sub (63:BV32.t) left)) in
not (BV64.eq (BV64.bw_and value mask) 0x0)
end
(*
static inline uint8_t PokeBit8(uint8_t byte, uint32_t left, int flag)
{
uint8_t mask = ((uint8_t) 1) << (7u - left);
return (flag == 0) ? (byte & ~mask) : (byte | mask);
}
*)
(* return `byte` with the bit at index `left` from the left set to `flag` *)
let poke_8bit (byte : BV8.t) (left : BV32.t) (flag : bool) : BV8.t
requires { BV32.t'int left < 8 }
ensures { forall i:int. 0 <= i < 8 -> i <> 7 - BV32.t'int left ->
BV8.nth result i = BV8.nth byte i }
ensures { BV8.nth result (7 - BV32.t'int left) = flag }
=
assert { BV32.ult left (8:BV32.t) };
begin
ensures { forall i:BV32.t. BV32.ult i (8:BV32.t) ->
i <> BV32.sub (7:BV32.t) left ->
BV8.nth_bv result (C8_32.toSmall i)
= BV8.nth_bv byte (C8_32.toSmall i) }
ensures { BV8.nth_bv result (BV8.sub (7:BV8.t) (C8_32.toSmall left))
= flag }
let mask = BV8.lsl_bv (1:BV8.t) (BV8.u_sub (7:BV8.t) (C8_32.toSmall left)) in
match flag with
| True -> BV8.bw_or byte mask
| False -> BV8.bw_and byte (BV8.bw_not mask)
end
end
let poke_8bit_array (addr : array BV8.t) (left : BV32.t) (flag : bool)
requires { 8 * (length addr) < BV32.two_power_size }
requires { BV32.t'int left < 8 * length addr }
writes { addr }
ensures { forall i:int. 0 <= i < 8 * length addr -> i <> BV32.t'int left ->
nth8_stream addr i = nth8_stream (old addr) i}
ensures { nth8_stream addr (BV32.t'int left) = flag }
=
let i = BV32.u_div left (8:BV32.t) in
let k = BV32.u_rem left (8:BV32.t) in
addr[BV32.to_uint i] <- poke_8bit addr[BV32.to_uint i] k flag
let poke (start : BV32.t) (len : BV32.t) (addr : array BV8.t) (value : BV64.t) : int
writes { addr }
requires{ BV32.t'int len < 64 } (* could be lower or equal if maxvalue and the condition to return -2 is corrected *)
requires{ BV32.t'int start + BV32.t'int len < BV32.two_power_size }
requires{ 8 * length addr < BV32.two_power_size }
ensures { -2 <= result <= 0 }
ensures { result = -1 <-> BV32.t'int start + BV32.t'int len > 8 * length addr }
ensures { result = -2 <-> BV64.t'int (maxvalue len) <= BV64.t'int value /\ BV32.t'int start + BV32.t'int len <= 8 * length addr }
ensures { result = 0 <-> BV64.t'int (maxvalue len) > BV64.t'int value /\ BV32.t'int start + BV32.t'int len <= 8 * length addr }
ensures { result = 0 ->
(forall i:int. 0 <= i < BV32.t'int start ->
nth8_stream (old addr) i
= nth8_stream addr i)
/\
(forall i:int. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
nth8_stream addr i
= BV64.nth value (BV32.t'int len - i - 1 + BV32.t'int start))
/\
(forall i:int. BV32.t'int start + BV32.t'int len <= i < 8 * length addr ->
nth8_stream addr i
= nth8_stream (old addr) i) }
=
if BV32.to_uint (BV32.u_add start len) > 8 * length addr
then
-1 (*error: invalid_bit_sequence*)
else
if BV64.uge value (maxvalue len) (* should be len <> 64 && _..._ *)
then
-2 (*error: value_too_big*)
else
let lstart = BV32.u_sub (64:BV32.t) len in
let i = ref 0x0 in
while BV32.ult !i len do variant { BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
invariant {forall j:int. 0 <= j < BV32.t'int start ->
nth8_stream (old addr) j
= nth8_stream addr j}
invariant {forall j:int. BV32.t'int start <= j < BV32.t'int start + BV32.t'int !i ->
nth8_stream addr j
= BV64.nth value (BV32.t'int len - j - 1 + BV32.t'int start) }
invariant {forall j:int. BV32.t'int start + BV32.t'int !i <= j < 8 * length addr ->
nth8_stream addr j
= nth8_stream (old addr) j }
let flag = peek_64bit value (BV32.u_add lstart !i) in
poke_8bit_array addr (BV32.u_add start !i) flag;
assert {nth8_stream addr (BV32.t'int start + BV32.t'int !i)
= BV64.nth value ((BV32.t'int len - BV32.t'int !i - 1))};
assert { forall k. BV32.t'int start <= k < BV32.t'int start + BV32.t'int !i ->
k <> BV32.t'int start + BV32.t'int !i &&
0 <= k < 8 * length addr &&
nth8_stream addr k
= BV64.nth value (BV32.t'int start + BV32.t'int len - k - 1)};
i := BV32.u_add !i (1:BV32.t);
done;
0
let peekthenpoke (start len : BV32.t) (addr : array BV8.t)
requires {8 * length addr < BV32.two_power_size}
requires {0 <= BV32.t'int len < 64}
requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
ensures {result = 0}
ensures {forall i. 0 <= i < 8 * length addr ->
nth8_stream addr i = nth8_stream (old addr) i}
=
let value = peek start len addr in
let res = poke start len addr value in
assert {res = 0};
assert {forall i. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
nth8_stream addr i
= nth8_stream (old addr) i};
res
let pokethenpeek (start len : BV32.t) (addr : array BV8.t) (value : BV64.t)
writes {addr}
requires {8 * length addr < BV32.two_power_size}
requires {0 <= BV32.t'int len < 64}
requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
requires {BV64.t'int value < BV64.t'int (maxvalue len)}
ensures {result = value}
=
assert { forall i:int. BV32.t'int len <= i < 64 ->
BV64.nth value i = False };
let poke_result = poke start len addr value in
assert { poke_result = 0 };
let peek_result = peek start len addr in
assert { BV64.(==) peek_result value };
peek_result
end
|
