defs.bend

lawful-bytes@0.1.1.0 · 107 lines · 16 definitions

1import Base
2import lawful-words@0.1.0.0/defs.bend as W
3import lawful-arrays@0.1.0.0/defs.bend as A
4
5# lawful-bytes definitions: the Bytes type and what it means. The operations
6# are in bytes.bend, the laws in LAWS.bend.
7
8# Bytes packed four to a word, little-endian, in a block of 2^d words: byte i
9# is byte i & 3 of word i >> 2. len is the number of bytes in use; the bytes
10# past len are unspecified.
11type Bytes is Type:
12  Bytes{len: U32, buf: Array<U32>}
13
14# The four bytes of each word, in order.
15def unpack(ws: List<&2, U32>) -> List<&2, U32>:
16  match ws:
17    case Nil{}:
18      Nil{}
19    case Con{+w, t}:
20      List.append(&2, U32, [W.byte(w, 0n), W.byte(w, 1n), W.byte(w, 2n), W.byte(w, 3n)], unpack(t))
21
22# What a Bytes holds: its first len bytes.
23def view(b: Bytes) -> List<&2, U32>:
24  Bytes{len, buf} = b
25  List.take(&2, U32, unpack(A.view(U32, buf)), U32.to_nat(len))
26
27# The number of bytes in use.
28def size(b: Bytes) -> Nat:
29  Bytes{len, buf} = b
30  U32.to_nat(len)
31
32# How many bytes fit: four per word.
33def cap(b: Bytes) -> Nat:
34  Bytes{len, buf} = b
35  Nat.mul(4n, List.length(&2, U32, A.view(U32, buf)))
36
37# b is well formed with a block of depth d: a perfect block of 2^d words,
38# d <= 29, and len within the block. A buffer holds at most 2^31 bytes (2 GiB),
39# so every index and length fits in a U32; the laws' hypotheses keep sums of
40# lengths in range too. Larger files are read in pieces.
41def ok(b: Bytes, +d: Nat) -> Bool:
42  Bytes{len, buf} = b
43  A.full(U32, buf, d) && (Nat.is_le(d, 29n) && Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))))
44
45# Every element is a byte (below 256).
46def all_bytes(xs: List<&2, U32>) -> Bool:
47  match xs:
48    case Nil{}:
49      True{}
50    case Con{x, t}:
51      U32.is_lt(x, 256) && all_bytes(t)
52
53# n elements from index i.
54def slice(xs: List<&2, U32>, +i: Nat, +n: Nat) -> List<&2, U32>:
55  List.take(&2, U32, List.drop(&2, U32, xs, i), n)
56
57# How many leading elements are not c.
58def run_len(xs: List<&2, U32>, +c: U32) -> Nat:
59  match xs:
60    case Nil{}:
61      0n
62    case Con{+x, t}:
63      Bool.pick(Nat, U32.is_eq(x, c), 0n, Nat.add(1n, run_len(t, c)))
64
65# How many leading elements are neither c1 nor c2.
66def run_len2(xs: List<&2, U32>, +c1: U32, +c2: U32) -> Nat:
67  match xs:
68    case Nil{}:
69      0n
70    case Con{+x, t}:
71      Bool.pick(Nat, U32.is_eq(x, c1) || U32.is_eq(x, c2), 0n, Nat.add(1n, run_len2(t, c1, c2)))
72
73# The first index j with from <= j < to where xs has c; to if there is none
74# (for from <= to <= length(xs), as the laws assume).
75def first(xs: List<&2, U32>, +from: Nat, +to: Nat, +c: U32) -> Nat:
76  Nat.add(from, run_len(slice(xs, from, Nat.sub(to, from)), c))
77
78# The same for either of two values (same assumptions).
79def first2(xs: List<&2, U32>, +from: Nat, +to: Nat, +c1: U32, +c2: U32) -> Nat:
80  Nat.add(from, run_len2(slice(xs, from, Nat.sub(to, from)), c1, c2))
81
82# Two lists are equal, element by element.
83def list_eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
84  match xs ys:
85    case Nil{} Nil{}:
86      True{}
87    case Con{x, xt} Con{y, yt}:
88      U32.is_eq(x, y) && list_eq(xt, yt)
89    case Nil{} Con{y, yt}:
90      False{}
91    case Con{x, xt} Nil{}:
92      False{}
93
94# xs has c at index k.
95def is_some(m: Maybe<&2, U32>, +c: U32) -> Bool:
96  match m:
97    case Some{x}:
98      U32.is_eq(x, c)
99    case None{}:
100      False{}
101
102def has(xs: List<&2, U32>, +k: Nat, +c: U32) -> Bool:
103  is_some(List.get(&2, U32, xs, k), c)
104
105# xs has c1 or c2 at index k.
106def has2(+xs: List<&2, U32>, +k: Nat, +c1: U32, +c2: U32) -> Bool:
107  is_some(List.get(&2, U32, xs, k), c1) || is_some(List.get(&2, U32, xs, k), c2)