Bit masks in byte arrays

A mask is a ByteArray; bit j is bit j % 8 of byte j / 8. Three operations are primitives implemented in C (@[extern c inline]), each with a reference definition in Lean that the proofs use: Ratpoints.Mask.andShr, the AND with a row shifted to the right, in place when the mask is not shared; Ratpoints.Mask.andRows, the AND with a list of shifted rows, one after the other until nothing is left, whose reference is the loop of Ratpoints.Mask.andShr and whose C code, for at most 64 rows with shifts that are multiples of 8 and rows long enough for the mask, works through the mask in blocks of 128 bytes held in registers, every row ANDed into a block before the block is written back, and otherwise goes row by row, byte by byte; and Ratpoints.Mask.nextSet, the first set bit from a position on. The C code reads and writes words of 64 bits (16-byte vectors in Ratpoints.Mask.andRows) and bytes; it does not depend on the byte order. It assumes that size_t has 64 bits: a shift or a position that is not a scalar becomes SIZE_MAX, which lies beyond every array only then, and eight times the size of a mask must not wrap. On a platform with 32 bits, rows of more than 256 MiB with shifts from 2 ^ 31 on, and masks of 512 MiB or more, could give other results than the reference definitions.

The compiled program runs the C code, the proofs are about the reference definitions: that the two agree is not proved, it is what one has to trust beyond Lean's runtime.

def Ratpoints.Mask.byte (a : ByteArray) (i : Nat) : Nat

Byte i of a as a natural number, 0 past the end.

Equations

• Ratpoints.Mask.byte a i = if h : i < a.size then a[i].toNat else 0

def Ratpoints.Mask.bit (a : ByteArray) (j : Nat) : Bool

Bit j of the mask a.

Equations

• Ratpoints.Mask.bit a j = (Ratpoints.Mask.byte a (j / 8)).testBit (j % 8)

def Ratpoints.Mask.shrByte (row : ByteArray) (s i : Nat) : UInt8

Byte i of the mask row shifted to the right by s bits.

Equations

• Ratpoints.Mask.shrByte row s i = ((Ratpoints.Mask.byte row (s / 8 + i) + 256 * Ratpoints.Mask.byte row (s / 8 + i + 1)) >>> (s % 8)).toUInt8

def Ratpoints.Mask.andShrSpec (acc row : ByteArray) (s : Nat) : ByteArray

The reference definition of Ratpoints.Mask.andShr: byte i of the result is byte i of acc ANDed with byte i of row shifted to the right by s bits, and the result is the empty array when every byte is 0.

Equations

• One or more equations did not get rendered due to their size.

@[extern c inline "({ lean_object * rp_r = lean_sarray_ensure_exclusive(#1); size_t rp_n = lean_sarray_size(rp_r), rp_m = lean_sarray_size(#2); uint8_t * rp_a = lean_sarray_cptr(rp_r); uint8_t const * rp_b = lean_sarray_cptr(#2); size_t rp_s = lean_is_scalar(#3) ? lean_unbox(#3) : SIZE_MAX; size_t rp_q = rp_s >> 3; unsigned rp_k = (unsigned)(rp_s & 7); size_t rp_w = 0; uint64_t rp_or = 0; if (rp_q < rp_m) { rp_w = (rp_m - rp_q - (rp_k ? 1 : 0)) / 8; if (rp_w > rp_n / 8) rp_w = rp_n / 8; } uint8_t const * rp_c = rp_b + (rp_q < rp_m ? rp_q : 0); if (rp_k == 0) { for (size_t rp_i = 0; rp_i < rp_w; rp_i++) { uint64_t rp_x, rp_y; __builtin_memcpy(&rp_x, rp_a + 8 * rp_i, 8); __builtin_memcpy(&rp_y, rp_c + 8 * rp_i, 8); rp_x &= rp_y; rp_or |= rp_x; __builtin_memcpy(rp_a + 8 * rp_i, &rp_x, 8); } } else { for (size_t rp_i = 0; rp_i < rp_w; rp_i++) { uint64_t rp_x, rp_y; __builtin_memcpy(&rp_x, rp_a + 8 * rp_i, 8); __builtin_memcpy(&rp_y, rp_c + 8 * rp_i, 8); if (__BYTE_ORDER__ != __ORDER_LITTLE_ENDIAN__) rp_y = __builtin_bswap64(rp_y); rp_y = (rp_y >> rp_k) | ((uint64_t)rp_c[8 * rp_i + 8] << (64 - rp_k)); if (__BYTE_ORDER__ != __ORDER_LITTLE_ENDIAN__) rp_y = __builtin_bswap64(rp_y); rp_x &= rp_y; rp_or |= rp_x; __builtin_memcpy(rp_a + 8 * rp_i, &rp_x, 8); } } for (size_t rp_i = 8 * rp_w; rp_i < rp_n; rp_i++) { size_t rp_t = rp_q + rp_i; unsigned rp_v = rp_t < rp_m ? rp_b[rp_t] : 0; if (rp_t + 1 < rp_m) rp_v |= (unsigned)rp_b[rp_t + 1] << 8; rp_a[rp_i] &= (uint8_t)(rp_v >> rp_k); rp_or |= rp_a[rp_i]; } if (rp_or == 0) lean_sarray_set_size(rp_r, 0); rp_r; })"]

def Ratpoints.Mask.andShr (acc : ByteArray) (row : ByteArray) (s : Nat) : ByteArray

The mask acc ANDed with the mask row shifted to the right by s bits: bit j < 8 n of the result (n the size of acc) is bit j of acc and bit j + s of row; the result is the empty array when no bit is set. The C code works in place when acc is not shared.

Equations

• Ratpoints.Mask.andShr acc row s = Ratpoints.Mask.andShrSpec acc row s

@[irreducible]

def Ratpoints.Mask.andRowsFrom (rs : Array ByteArray) (sh : Array Nat) (o : Nat) (acc : ByteArray) (i : Nat) : ByteArray

The reference definition of Ratpoints.Mask.andRows: acc ANDed with the rows rs[i] shifted to the right by sh[i] + o bits (Ratpoints.Mask.andShr), from position i on, one after the other until nothing is left.

Equations

• One or more equations did not get rendered due to their size.

@[extern c inline "({ typedef uint64_t rp_v2 __attribute__((vector_size(16))); lean_object * rp_r = #1; size_t rp_f = lean_array_size(#2); if (rp_f > 0) { rp_r = lean_sarray_ensure_exclusive(rp_r); size_t rp_n = lean_sarray_size(rp_r), rp_nw = rp_n / 8, rp_ns = lean_array_size(#3); uint8_t * rp_a = lean_sarray_cptr(rp_r); size_t rp_o = lean_is_scalar(#4) ? lean_unbox(#4) : SIZE_MAX; /* the fast path: at most 64 rows, every shift a multiple of 8, every row long enough */ uint8_t const * rp_p[64]; int rp_fast = rp_f <= 64; for (size_t rp_j = 0; rp_fast && rp_j < rp_f; rp_j++) { lean_object * rp_row = lean_array_get_core(#2, rp_j); lean_object * rp_so = rp_j < rp_ns ? lean_array_get_core(#3, rp_j) : lean_box(0); size_t rp_m = lean_sarray_size(rp_row); size_t rp_s = lean_is_scalar(rp_so) && rp_o != SIZE_MAX ? lean_unbox(rp_so) + rp_o : SIZE_MAX; size_t rp_q = rp_s >> 3; if ((rp_s & 7) != 0 || rp_q > rp_m || rp_m - rp_q < rp_n) rp_fast = 0; else rp_p[rp_j] = lean_sarray_cptr(rp_row) + rp_q; } uint64_t rp_any = 0; if (rp_fast) { size_t rp_w = 0; /* blocks of 16 words in eight vector registers; a block is left once it is zero, which is tested after every fourth row */ for (; rp_w + 16 <= rp_nw; rp_w += 16) { uint8_t * rp_b = rp_a + 8 * rp_w; rp_v2 rp_x0, rp_x1, rp_x2, rp_x3, rp_x4, rp_x5, rp_x6, rp_x7; __builtin_memcpy(&rp_x0, rp_b, 16); __builtin_memcpy(&rp_x1, rp_b + 16, 16); __builtin_memcpy(&rp_x2, rp_b + 32, 16); __builtin_memcpy(&rp_x3, rp_b + 48, 16); __builtin_memcpy(&rp_x4, rp_b + 64, 16); __builtin_memcpy(&rp_x5, rp_b + 80, 16); __builtin_memcpy(&rp_x6, rp_b + 96, 16); __builtin_memcpy(&rp_x7, rp_b + 112, 16); for (size_t rp_j = 0; rp_j < rp_f; rp_j++) { uint8_t const * rp_c = rp_p[rp_j] + 8 * rp_w; rp_v2 rp_y; __builtin_memcpy(&rp_y, rp_c, 16); rp_x0 &= rp_y; __builtin_memcpy(&rp_y, rp_c + 16, 16); rp_x1 &= rp_y; __builtin_memcpy(&rp_y, rp_c + 32, 16); rp_x2 &= rp_y; __builtin_memcpy(&rp_y, rp_c + 48, 16); rp_x3 &= rp_y; __builtin_memcpy(&rp_y, rp_c + 64, 16); rp_x4 &= rp_y; __builtin_memcpy(&rp_y, rp_c + 80, 16); rp_x5 &= rp_y; __builtin_memcpy(&rp_y, rp_c + 96, 16); rp_x6 &= rp_y; __builtin_memcpy(&rp_y, rp_c + 112, 16); rp_x7 &= rp_y; if ((rp_j & 3) == 3) { rp_v2 rp_t = rp_x0 | rp_x1 | rp_x2 | rp_x3 | rp_x4 | rp_x5 | rp_x6 | rp_x7; if ((rp_t[0] | rp_t[1]) == 0) break; } } __builtin_memcpy(rp_b, &rp_x0, 16); __builtin_memcpy(rp_b + 16, &rp_x1, 16); __builtin_memcpy(rp_b + 32, &rp_x2, 16); __builtin_memcpy(rp_b + 48, &rp_x3, 16); __builtin_memcpy(rp_b + 64, &rp_x4, 16); __builtin_memcpy(rp_b + 80, &rp_x5, 16); __builtin_memcpy(rp_b + 96, &rp_x6, 16); __builtin_memcpy(rp_b + 112, &rp_x7, 16); rp_v2 rp_t = rp_x0 | rp_x1 | rp_x2 | rp_x3 | rp_x4 | rp_x5 | rp_x6 | rp_x7; rp_any |= rp_t[0] | rp_t[1]; } /* the remaining words one at a time, then the remaining bytes */ for (; rp_w < rp_nw; rp_w++) { uint64_t rp_v; __builtin_memcpy(&rp_v, rp_a + 8 * rp_w, 8); for (size_t rp_j = 0; rp_v && rp_j < rp_f; rp_j++) { uint64_t rp_y; __builtin_memcpy(&rp_y, rp_p[rp_j] + 8 * rp_w, 8); rp_v &= rp_y; } __builtin_memcpy(rp_a + 8 * rp_w, &rp_v, 8); rp_any |= rp_v; } for (size_t rp_i = 8 * rp_nw; rp_i < rp_n; rp_i++) { for (size_t rp_j = 0; rp_j < rp_f; rp_j++) rp_a[rp_i] &= rp_p[rp_j][rp_i]; rp_any |= rp_a[rp_i]; } } else { /* otherwise row by row, byte by byte, as Ratpoints.Mask.andShr */ for (size_t rp_j = 0; rp_j < rp_f; rp_j++) { lean_object * rp_row = lean_array_get_core(#2, rp_j); lean_object * rp_so = rp_j < rp_ns ? lean_array_get_core(#3, rp_j) : lean_box(0); size_t rp_m = lean_sarray_size(rp_row); uint8_t const * rp_c = lean_sarray_cptr(rp_row); size_t rp_s = lean_is_scalar(rp_so) && rp_o != SIZE_MAX ? lean_unbox(rp_so) + rp_o : SIZE_MAX; size_t rp_q = rp_s >> 3; unsigned rp_k = (unsigned)(rp_s & 7); rp_any = 0; for (size_t rp_i = 0; rp_i < rp_n; rp_i++) { size_t rp_t = rp_q + rp_i; unsigned rp_v = rp_t < rp_m ? rp_c[rp_t] : 0; if (rp_t + 1 < rp_m) rp_v |= (unsigned)rp_c[rp_t + 1] << 8; rp_a[rp_i] &= (uint8_t)(rp_v >> rp_k); rp_any |= rp_a[rp_i]; } if (rp_any == 0) break; } } if (rp_any == 0) lean_sarray_set_size(rp_r, 0); } rp_r; })"]

def Ratpoints.Mask.andRows (acc : ByteArray) (rs : Array ByteArray) (sh : Array Nat) (o : Nat) : ByteArray

The mask acc ANDed with the rows rs[i] shifted to the right by sh[i] + o bits, all of them: bit j < 8 n of the result (n the size of acc) is bit j of acc and bit j + sh[i] + o of every rs[i], and the result is the empty array when no bit is left (when there is a row). The C code works in place when acc is not shared.

Equations

• Ratpoints.Mask.andRows acc rs sh o = Ratpoints.Mask.andRowsFrom rs sh o acc 0

def Ratpoints.Mask.nextSetSpec (a : ByteArray) (j : Nat) : Nat

The reference definition of Ratpoints.Mask.nextSet: the first k from j to 8 n - 1 with bit k of a set (n the size of a), or 8 n.

Equations

• Ratpoints.Mask.nextSetSpec a j = (List.find? (Ratpoints.Mask.bit a) (List.range' j (8 * a.size - j))).getD (8 * a.size)

@[extern c inline "({ size_t rp_n = lean_sarray_size(#1); uint8_t const * rp_a = lean_sarray_cptr(#1); size_t rp_j = lean_is_scalar(#2) ? lean_unbox(#2) : SIZE_MAX; size_t rp_res = 8 * rp_n; if (rp_j < 8 * rp_n) { size_t rp_i = rp_j >> 3; unsigned rp_c = (unsigned)rp_a[rp_i] >> (rp_j & 7); if (rp_c) rp_res = rp_j + (size_t)__builtin_ctz(rp_c); else { rp_i++; for (;;) { uint64_t rp_w; if (rp_i + 8 > rp_n) break; __builtin_memcpy(&rp_w, rp_a + rp_i, 8); if (rp_w) break; rp_i += 8; } while (rp_i < rp_n && rp_a[rp_i] == 0) rp_i++; if (rp_i < rp_n) rp_res = 8 * rp_i + (size_t)__builtin_ctz(rp_a[rp_i]); } } lean_usize_to_nat(rp_res); })"]

def Ratpoints.Mask.nextSet (a : ByteArray) (j : Nat) : Nat

The first set bit of the mask a at or after j, or 8 n (n the size of a) when there is none.

Equations

• Ratpoints.Mask.nextSet a j = Ratpoints.Mask.nextSetSpec a j

def Ratpoints.Mask.isZero (a : ByteArray) : Bool

Whether no bit of the mask a is set.

Equations

• Ratpoints.Mask.isZero a = (a.size == 0 || Ratpoints.Mask.nextSet a 0 == 8 * a.size)

def Ratpoints.Mask.ones (len : Nat) : ByteArray

The mask of len bits, all set, in whole 64-bit words.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Mask.setBitsFrom (a : ByteArray) : Nat → Nat → List Nat

The set bits of the mask a from j on, in ascending order (with fuel at least the number of them).

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Mask.setBitsFrom a 0 x✝ = []

def Ratpoints.Mask.setBits (a : ByteArray) : List Nat

The set bits of the mask a, in ascending order.

Equations

• Ratpoints.Mask.setBits a = Ratpoints.Mask.setBitsFrom a (8 * a.size) 0