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
|
val IsZero_slice : forall 'n, 'n >= 0.
(bits('n), int, int) -> bool effect {escape}
function IsZero_slice (xs, i, 'l) = {
assert(constraint('l >= 0));
IsZero(xs & slice_mask(i, l))
}
val IsOnes_slice : forall 'n, 'n >= 0.
(bits('n), int, int) -> bool effect {escape}
function IsOnes_slice (xs, i, 'l) = {
assert(constraint('l >= 0));
let m : bits('n) = slice_mask(i,l) in
(xs & m) == m
}
val ZeroExtend_slice_append : forall 'n 'm 'o, 'n >= 0 & 'm >= 0 & 'o >= 0.
(bits('n), int, int, bits('m)) -> bits('o) effect {escape}
function ZeroExtend_slice_append (xs, i, 'l, ys) = {
assert(constraint('l >= 0));
let xs = xs & slice_mask(i,l) in
let xs : bits('o) = extzv(xs >> i) << 'm in
let ys : bits('o) = extzv(ys) in
xs | ys
}
val IsZero_slice2 : forall 'n, 'n >= 0.
(bits('n), int, int) -> bool effect {escape}
function IsZero_slice2 (xs, i, 'l) = {
assert(constraint('l >= 0));
IsZero(xs & slice_mask(i, l))
}
|
