lawful-bytes

Releases (2):
  0.1.1.0  0x96f8731d7df2e01c9a22fc0773dfab33  indexed  https://jend.leeeet.dev/files.txt?path=lawful-bytes@0.1.1.0
  0.1.0.0  0xc018b2b7a70e32edf065f462beb7dcfd  unindexed  https://jend.leeeet.dev/files.txt?path=lawful-bytes@0.1.0.0

Definitions (578, 1 to 100 shown):
  LAWS.view_size (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=view_size)
   law view_size:
     for b: D.Bytes
     for d: Nat
     for h: {D.ok(b, d) == True{} : Bool}
     {List.length(&2, U32, D.view(b)) == D.size(b) : Nat}
  LAWS.view_bytes (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=view_bytes)
   law view_bytes:
     for b: D.Bytes
     {D.all_bytes(D.view(b)) == True{} : Bool}
  LAWS.cap_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=cap_ok)
   law cap_ok:
     for b: D.Bytes
     for d: Nat
     for h: {D.ok(b, d) == True{} : Bool}
     {D.cap(b) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}
  LAWS.empty_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=empty_view)
   law empty_view:
     for d: Nat
     {D.view(B.empty(d)) == Nil{} : List<&2, U32>}
  LAWS.empty_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=empty_ok)
   law empty_ok:
     for d: Nat
     for hd: {Nat.is_le(d, 29n) == True{} : Bool}
     {D.ok(B.empty(d), d) == True{} : Bool}
  LAWS.grow_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=grow_view)
   # grow keeps the bytes in a larger block.
   law grow_view:
     for b: D.Bytes
     for d: Nat
     for e: Nat
     for h: {D.ok(b, d) == True{} : Bool}
     for he: {Nat.is_le(d, e) == True{} : Bool}
     for he29: {Nat.is_le(e, 29n) == True{} : Bool}
     {D.view(B.grow(b, e)) == D.view(b) : List<&2, U32>}
  LAWS.grow_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=grow_ok)
   law grow_ok:
     for b: D.Bytes
     for d: Nat
     for e: Nat
     for h: {D.ok(b, d) == True{} : Bool}
     for he: {Nat.is_le(d, e) == True{} : Bool}
     for he29: {Nat.is_le(e, 29n) == True{} : Bool}
     {D.ok(B.grow(b, e), e) == True{} : Bool}
  LAWS.at_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=at_view)
   law at_view:
     for b: D.Bytes
     for d: Nat
     for i: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}
     {Some{Pair.snd(D.Bytes, U32, B.at(b, i))} == List.get(&2, U32, D.view(b), U32.to_nat(i)) : Maybe<&2, U32>}
  LAWS.at_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=at_pair)
   # The result as a literal pair: the same Bytes and the value (for rewriting).
   law at_pair:
     for b: D.Bytes
     for i: U32
     {B.at(b, i) == (b, Pair.snd(D.Bytes, U32, B.at(b, i))) : D.Bytes & U32}
  LAWS.find_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=find_view)
   # find answers the first index in from .. to-1 holding c, or to. c must be a
   # byte value: a word-at-a-time search compares 8 bits per byte.
   law find_view:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: U32
     for c: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hft: {U32.is_le(from, to) == True{} : Bool}
     for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
     …
  LAWS.find_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=find_pair)
   # The result as a literal pair: the same Bytes and the value (for rewriting).
   law find_pair:
     for b: D.Bytes
     for from: U32
     for to: U32
     for c: U32
     {B.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, B.find(b, from, to, c))) : D.Bytes & U32}
  LAWS.find2_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=find2_view)
   law find2_view:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: U32
     for c1: U32
     for c2: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hft: {U32.is_le(from, to) == True{} : Bool}
     for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
     for hc1: {U32.is_lt(c1, 256) == True{} : Bool}
     …
  LAWS.find2_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=find2_pair)
   # The result as a literal pair: the same Bytes and the value (for rewriting).
   law find2_pair:
     for b: D.Bytes
     for from: U32
     for to: U32
     for c1: U32
     for c2: U32
     {B.find2(b, from, to, c1, c2) == (b, Pair.snd(D.Bytes, U32, B.find2(b, from, to, c1, c2))) : D.Bytes & U32}
  LAWS.same_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=same_view)
   # same compares two ranges of equal length, n bytes each.
   law same_view:
     for a: D.Bytes
     for b: D.Bytes
     for d: Nat
     for e: Nat
     for i: U32
     for j: U32
     for n: U32
     for ha: {D.ok(a, d) == True{} : Bool}
     for hb: {D.ok(b, e) == True{} : Bool}
     …
  LAWS.same_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=same_pair)
   # same hands both buffers back (as a literal tuple, for rewriting).
   law same_pair:
     for a: D.Bytes
     for b: D.Bytes
     for i: U32
     for j: U32
     for n: U32
     {B.same(a, i, b, j, n) == (a, (b, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))))) : D.Bytes & (D.Bytes & Bool)}
  LAWS.set_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=set_view)
   law set_view:
     for b: D.Bytes
     for d: Nat
     for i: U32
     for v: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}
     for hv: {U32.is_lt(v, 256) == True{} : Bool}
     {D.view(B.set(b, i, v)) == List.set(&2, U32, D.view(b), U32.to_nat(i), v) : List<&2, U32>}
  LAWS.set_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=set_ok)
   law set_ok:
     for b: D.Bytes
     for d: Nat
     for i: U32
     for v: U32
     for h: {D.ok(b, d) == True{} : Bool}
     {D.ok(B.set(b, i, v), d) == True{} : Bool}
  LAWS.push_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=push_view)
   law push_view:
     for b: D.Bytes
     for d: Nat
     for v: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}
     for hv: {U32.is_lt(v, 256) == True{} : Bool}
     {D.view(B.push(b, v)) == List.append(&2, U32, D.view(b), [v]) : List<&2, U32>}
  LAWS.push_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=push_ok)
   law push_ok:
     for b: D.Bytes
     for d: Nat
     for v: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}
     {D.ok(B.push(b, v), d) == True{} : Bool}
  LAWS.append_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=append_view)
   # append adds n bytes of src, from s, at the end of dst.
   law append_view:
     for dst: D.Bytes
     for src: D.Bytes
     for d: Nat
     for e: Nat
     for s: U32
     for n: U32
     for hd: {D.ok(dst, d) == True{} : Bool}
     for he: {D.ok(src, e) == True{} : Bool}
     for hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}
     …
  LAWS.append_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=append_ok)
   law append_ok:
     for dst: D.Bytes
     for src: D.Bytes
     for d: Nat
     for s: U32
     for n: U32
     for hd: {D.ok(dst, d) == True{} : Bool}
     for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
     {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), d) == True{} : Bool}
  LAWS.append_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=append_pair)
   # append hands src back (as a literal pair, for rewriting).
   law append_pair:
     for dst: D.Bytes
     for src: D.Bytes
     for s: U32
     for n: U32
     {B.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}
  LAWS.len_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=len_view)
   law len_view:
     for b: D.Bytes
     {U32.to_nat(Pair.snd(D.Bytes, U32, B.len(b))) == D.size(b) : Nat}
  LAWS.len_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=len_pair)
   law len_pair:
     for b: D.Bytes
     {B.len(b) == (b, Pair.snd(D.Bytes, U32, B.len(b))) : D.Bytes & U32}
  LAWS.capacity_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=capacity_view)
   law capacity_view:
     for b: D.Bytes
     for d: Nat
     for h: {D.ok(b, d) == True{} : Bool}
     {U32.to_nat(Pair.snd(D.Bytes, U32, B.capacity(b))) == D.cap(b) : Nat}
  LAWS.capacity_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=capacity_pair)
   law capacity_pair:
     for b: D.Bytes
     {B.capacity(b) == (b, Pair.snd(D.Bytes, U32, B.capacity(b))) : D.Bytes & U32}
  LAWS.truncate_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=truncate_view)
   law truncate_view:
     for b: D.Bytes
     for n: U32
     for h: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}
     {D.view(B.truncate(b, n)) == List.take(&2, U32, D.view(b), U32.to_nat(n)) : List<&2, U32>}
  LAWS.truncate_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=truncate_ok)
   law truncate_ok:
     for b: D.Bytes
     for d: Nat
     for n: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hn: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}
     {D.ok(B.truncate(b, n), d) == True{} : Bool}
  LAWS.shift_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=shift_view)
   # shift drops the first k bytes and moves the rest to the start (for reusing a
   # buffer when reading a stream in pieces).
   law shift_view:
     for b: D.Bytes
     for d: Nat
     for k: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}
     {D.view(B.shift(b, k)) == List.drop(&2, U32, D.view(b), U32.to_nat(k)) : List<&2, U32>}
  LAWS.shift_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=shift_ok)
   law shift_ok:
     for b: D.Bytes
     for d: Nat
     for k: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}
     {D.ok(B.shift(b, k), d) == True{} : Bool}
  LAWS.of_list_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=of_list_view)
   law of_list_view:
     for d: Nat
     for xs: List<&2, U32>
     for hd: {Nat.is_le(d, 29n) == True{} : Bool}
     for hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
     for hb: {D.all_bytes(xs) == True{} : Bool}
     {D.view(B.of_list(d, xs)) == xs : List<&2, U32>}
  LAWS.of_list_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=of_list_ok)
   law of_list_ok:
     for d: Nat
     for xs: List<&2, U32>
     for hd: {Nat.is_le(d, 29n) == True{} : Bool}
     for hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
     {D.ok(B.of_list(d, xs), d) == True{} : Bool}
  LAWS.to_list_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=to_list_view)
   law to_list_view:
     for b: D.Bytes
     for d: Nat
     for s: U32
     for n: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(b)) == True{} : Bool}
     {Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n)) == D.slice(D.view(b), U32.to_nat(s), U32.to_nat(n)) : List<&2, U32>}
  LAWS.to_list_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=to_list_pair)
   law to_list_pair:
     for b: D.Bytes
     for s: U32
     for n: U32
     {B.to_list(b, s, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n))) : D.Bytes & List<&2, U32>}
  LAWS.same1_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=same1_view)
   law same1_view:
     for b: D.Bytes
     for d: Nat
     for i: U32
     for j: U32
     for n: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(b)) == True{} : Bool}
     for hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}
     {Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n)) == D.list_eq(D.slice(D.view(b), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}
  LAWS.same1_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=same1_pair)
   law same1_pair:
     for b: D.Bytes
     for i: U32
     for j: U32
     for n: U32
     {B.same1(b, i, j, n) == (b, Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n))) : D.Bytes & Bool}
  LAWS.first_range (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=first_range)
   law first_range:
     for xs: List<&2, U32>
     for from: Nat
     for to: Nat
     for c: U32
     for hft: {Nat.is_le(from, to) == True{} : Bool}
     for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
     {(Nat.is_le(from, D.first(xs, from, to, c)) && Nat.is_le(D.first(xs, from, to, c), to)) == True{} : Bool}
  LAWS.first_hit (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=first_hit)
   # Below to, the answer holds c.
   law first_hit:
     for xs: List<&2, U32>
     for from: Nat
     for to: Nat
     for c: U32
     for hft: {Nat.is_le(from, to) == True{} : Bool}
     for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
     for hlt: {Nat.is_lt(D.first(xs, from, to, c), to) == True{} : Bool}
     {D.has(xs, D.first(xs, from, to, c), c) == True{} : Bool}
  LAWS.first_miss (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=first_miss)
   # No index from from up to the answer holds c.
   law first_miss:
     for xs: List<&2, U32>
     for from: Nat
     for to: Nat
     for c: U32
     for k: Nat
     for hk1: {Nat.is_le(from, k) == True{} : Bool}
     for hk2: {Nat.is_lt(k, D.first(xs, from, to, c)) == True{} : Bool}
     {D.has(xs, k, c) == False{} : Bool}
  LAWS.first2_range (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=first2_range)
   law first2_range:
     for xs: List<&2, U32>
     for from: Nat
     for to: Nat
     for c1: U32
     for c2: U32
     for hft: {Nat.is_le(from, to) == True{} : Bool}
     for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
     {(Nat.is_le(from, D.first2(xs, from, to, c1, c2)) && Nat.is_le(D.first2(xs, from, to, c1, c2), to)) == True{} : Bool}
  LAWS.first2_hit (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=first2_hit)
   law first2_hit:
     for xs: List<&2, U32>
     for from: Nat
     for to: Nat
     for c1: U32
     for c2: U32
     for hft: {Nat.is_le(from, to) == True{} : Bool}
     for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
     for hlt: {Nat.is_lt(D.first2(xs, from, to, c1, c2), to) == True{} : Bool}
     {D.has2(xs, D.first2(xs, from, to, c1, c2), c1, c2) == True{} : Bool}
  LAWS.first2_miss (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=first2_miss)
   law first2_miss:
     for xs: List<&2, U32>
     for from: Nat
     for to: Nat
     for c1: U32
     for c2: U32
     for k: Nat
     for hk1: {Nat.is_le(from, k) == True{} : Bool}
     for hk2: {Nat.is_lt(k, D.first2(xs, from, to, c1, c2)) == True{} : Bool}
     {D.has2(xs, k, c1, c2) == False{} : Bool}
  LAWS.list_eq_true (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=list_eq_true)
   # A passed list_eq test gives equal lists.
   law list_eq_true:
     for xs: List<&2, U32>
     for ys: List<&2, U32>
     for h: {D.list_eq(xs, ys) == True{} : Bool}
     {xs == ys : List<&2, U32>}
  LAWS.list_eq_refl (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=list_eq_refl)
   # Equal lists pass list_eq.
   law list_eq_refl:
     for xs: List<&2, U32>
     {D.list_eq(xs, xs) == True{} : Bool}
  LAWS.fast_find (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=fast_find)
   # The word-at-a-time find gives exactly the reference result (the same Bytes
   # and the same index). c must be a byte value: the search compares 8 bits per
   # byte.
   law fast_find:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: U32
     for c: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hft: {U32.is_le(from, to) == True{} : Bool}
     …
  LAWS.fast_find2 (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=fast_find2)
   law fast_find2:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: U32
     for c1: U32
     for c2: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hft: {U32.is_le(from, to) == True{} : Bool}
     for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
     for hc1: {U32.is_lt(c1, 256) == True{} : Bool}
     …
  LAWS.fast_find_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=fast_find_pair)
   # The fast searches hand back the same Bytes, for any arguments (as find_pair
   # and find2_pair say of the reference).
   law fast_find_pair:
     for b: D.Bytes
     for from: U32
     for to: U32
     for c: U32
     {FA.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, FA.find(b, from, to, c))) : D.Bytes & U32}
  LAWS.fast_find2_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=fast_find2_pair)
   law fast_find2_pair:
     for b: D.Bytes
     for from: U32
     for to: U32
     for c1: U32
     for c2: U32
     {FA.find2(b, from, to, c1, c2) == (b, Pair.snd(D.Bytes, U32, FA.find2(b, from, to, c1, c2))) : D.Bytes & U32}
  LAWS.fast_append_view (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=fast_append_view)
   # The word-at-a-time append writes whole words, so up to 3 bytes past the new
   # length differ from the reference's: its laws are append's, on the view.
   law fast_append_view:
     for dst: D.Bytes
     for src: D.Bytes
     for d: Nat
     for e: Nat
     for s: U32
     for n: U32
     for hd: {D.ok(dst, d) == True{} : Bool}
     for he: {D.ok(src, e) == True{} : Bool}
     …
  LAWS.fast_append_ok (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=fast_append_ok)
   law fast_append_ok:
     for dst: D.Bytes
     for src: D.Bytes
     for d: Nat
     for s: U32
     for n: U32
     for hd: {D.ok(dst, d) == True{} : Bool}
     for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
     {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), d) == True{} : Bool}
  LAWS.fast_append_pair (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/LAWS.bend&name=fast_append_pair)
   law fast_append_pair:
     for dst: D.Bytes
     for src: D.Bytes
     for s: U32
     for n: U32
     {FA.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}
  PROOF.at_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=at_view.go)
   def at_view.go(-b: D.Bytes, +d: Nat, +i: U32, h: {D.ok(b, d) == True{} : Bool},
     hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}, m: C.BMirror(b)) ->
     {Some{Pair.snd(D.Bytes, U32, B.at(b, i))} == List.get(&2, U32, D.view(b), U32.to_nat(i)) : Maybe<&2, U32>}:
  PROOF.view_size.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=view_size.go)
   def view_size.go(-b: D.Bytes, +d: Nat, h: {D.ok(b, d) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {List.length(&2, U32, D.view(b)) == D.size(b) : Nat}:
  PROOF.view_bytes.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=view_bytes.go)
   def view_bytes.go(-b: D.Bytes, m_b: C.BMirror(b)) ->
     {D.all_bytes(D.view(b)) == True{} : Bool}:
  PROOF.cap_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=cap_ok.go)
   def cap_ok.go(-b: D.Bytes, +d: Nat, h: {D.ok(b, d) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.cap(b) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}:
  PROOF.grow_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=grow_view.go)
   def grow_view.go(-b: D.Bytes, +d: Nat, +e: Nat, h: {D.ok(b, d) == True{} : Bool}, he: {Nat.is_le(d, e) == True{} : Bool}, he29: {Nat.is_le(e, 29n) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.view(B.grow(b, e)) == D.view(b) : List<&2, U32>}:
  PROOF.grow_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=grow_ok.go)
   def grow_ok.go(-b: D.Bytes, +d: Nat, +e: Nat, h: {D.ok(b, d) == True{} : Bool}, he: {Nat.is_le(d, e) == True{} : Bool}, he29: {Nat.is_le(e, 29n) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.ok(B.grow(b, e), e) == True{} : Bool}:
  PROOF.at_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=at_pair.go)
   def at_pair.go(-b: D.Bytes, +i: U32, m_b: C.BMirror(b)) ->
     {B.at(b, i) == (b, Pair.snd(D.Bytes, U32, B.at(b, i))) : D.Bytes & U32}:
  PROOF.find_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=find_view.go)
   def find_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +c: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hc: {U32.is_lt(c, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {U32.to_nat(Pair.snd(D.Bytes, U32, B.find(b, from, to, c))) == D.first(D.view(b), U32.to_nat(from), U32.to_nat(to), c) : Nat}:
  PROOF.find_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=find_pair.go)
   def find_pair.go(-b: D.Bytes, +from: U32, +to: U32, +c: U32, m_b: C.BMirror(b)) ->
     {B.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, B.find(b, from, to, c))) : D.Bytes & U32}:
  PROOF.find2_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=find2_view.go)
   def find2_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +c1: U32, +c2: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hc1: {U32.is_lt(c1, 256) == True{} : Bool}, hc2: {U32.is_lt(c2, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2(b, from, to, c1, c2))) == D.first2(D.view(b), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}:
  PROOF.find2_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=find2_pair.go)
   def find2_pair.go(-b: D.Bytes, +from: U32, +to: U32, +c1: U32, +c2: U32, m_b: C.BMirror(b)) ->
     {B.find2(b, from, to, c1, c2) == (b, Pair.snd(D.Bytes, U32, B.find2(b, from, to, c1, c2))) : D.Bytes & U32}:
  PROOF.same_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=same_view.go)
   def same_view.go(-a: D.Bytes, -b: D.Bytes, +d: Nat, +e: Nat, +i: U32, +j: U32, +n: U32, ha: {D.ok(a, d) == True{} : Bool}, hb: {D.ok(b, e) == True{} : Bool}, hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(a)) == True{} : Bool}, hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}, m_a: C.BMirror(a), m_b: C.BMirror(b)) ->
     {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))) == D.list_eq(D.slice(D.view(a), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}:
  PROOF.same_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=same_pair.go)
   def same_pair.go(-a: D.Bytes, -b: D.Bytes, +i: U32, +j: U32, +n: U32, m_a: C.BMirror(a), m_b: C.BMirror(b)) ->
     {B.same(a, i, b, j, n) == (a, (b, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))))) : D.Bytes & (D.Bytes & Bool)}:
  PROOF.set_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=set_view.go)
   def set_view.go(-b: D.Bytes, +d: Nat, +i: U32, +v: U32, h: {D.ok(b, d) == True{} : Bool}, hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}, hv: {U32.is_lt(v, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.view(B.set(b, i, v)) == List.set(&2, U32, D.view(b), U32.to_nat(i), v) : List<&2, U32>}:
  PROOF.set_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=set_ok.go)
   def set_ok.go(-b: D.Bytes, +d: Nat, +i: U32, +v: U32, h: {D.ok(b, d) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.ok(B.set(b, i, v), d) == True{} : Bool}:
  PROOF.push_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=push_view.go)
   def push_view.go(-b: D.Bytes, +d: Nat, +v: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}, hv: {U32.is_lt(v, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.view(B.push(b, v)) == List.append(&2, U32, D.view(b), [v]) : List<&2, U32>}:
  PROOF.push_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=push_ok.go)
   def push_ok.go(-b: D.Bytes, +d: Nat, +v: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.ok(B.push(b, v), d) == True{} : Bool}:
  PROOF.append_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=append_view.go)
   def append_view.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +e: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, he: {D.ok(src, e) == True{} : Bool}, hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
     {D.view(Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n))) == List.append(&2, U32, D.view(dst), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}:
  PROOF.append_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=append_ok.go)
   def append_ok.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
     {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), d) == True{} : Bool}:
  PROOF.append_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=append_pair.go)
   def append_pair.go(-dst: D.Bytes, -src: D.Bytes, +s: U32, +n: U32, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
     {B.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}:
  PROOF.len_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=len_view.go)
   def len_view.go(-b: D.Bytes, m_b: C.BMirror(b)) ->
     {U32.to_nat(Pair.snd(D.Bytes, U32, B.len(b))) == D.size(b) : Nat}:
  PROOF.len_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=len_pair.go)
   def len_pair.go(-b: D.Bytes, m_b: C.BMirror(b)) ->
     {B.len(b) == (b, Pair.snd(D.Bytes, U32, B.len(b))) : D.Bytes & U32}:
  PROOF.capacity_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=capacity_view.go)
   def capacity_view.go(-b: D.Bytes, +d: Nat, h: {D.ok(b, d) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {U32.to_nat(Pair.snd(D.Bytes, U32, B.capacity(b))) == D.cap(b) : Nat}:
  PROOF.capacity_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=capacity_pair.go)
   def capacity_pair.go(-b: D.Bytes, m_b: C.BMirror(b)) ->
     {B.capacity(b) == (b, Pair.snd(D.Bytes, U32, B.capacity(b))) : D.Bytes & U32}:
  PROOF.truncate_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=truncate_view.go)
   def truncate_view.go(-b: D.Bytes, +n: U32, h: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.view(B.truncate(b, n)) == List.take(&2, U32, D.view(b), U32.to_nat(n)) : List<&2, U32>}:
  PROOF.truncate_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=truncate_ok.go)
   def truncate_ok.go(-b: D.Bytes, +d: Nat, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hn: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.ok(B.truncate(b, n), d) == True{} : Bool}:
  PROOF.shift_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=shift_view.go)
   def shift_view.go(-b: D.Bytes, +d: Nat, +k: U32, h: {D.ok(b, d) == True{} : Bool}, hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.view(B.shift(b, k)) == List.drop(&2, U32, D.view(b), U32.to_nat(k)) : List<&2, U32>}:
  PROOF.shift_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=shift_ok.go)
   def shift_ok.go(-b: D.Bytes, +d: Nat, +k: U32, h: {D.ok(b, d) == True{} : Bool}, hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {D.ok(B.shift(b, k), d) == True{} : Bool}:
  PROOF.to_list_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=to_list_view.go)
   def to_list_view.go(-b: D.Bytes, +d: Nat, +s: U32, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n)) == D.slice(D.view(b), U32.to_nat(s), U32.to_nat(n)) : List<&2, U32>}:
  PROOF.to_list_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=to_list_pair.go)
   def to_list_pair.go(-b: D.Bytes, +s: U32, +n: U32, m_b: C.BMirror(b)) ->
     {B.to_list(b, s, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n))) : D.Bytes & List<&2, U32>}:
  PROOF.same1_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=same1_view.go)
   def same1_view.go(-b: D.Bytes, +d: Nat, +i: U32, +j: U32, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(b)) == True{} : Bool}, hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n)) == D.list_eq(D.slice(D.view(b), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}:
  PROOF.same1_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=same1_pair.go)
   def same1_pair.go(-b: D.Bytes, +i: U32, +j: U32, +n: U32, m_b: C.BMirror(b)) ->
     {B.same1(b, i, j, n) == (b, Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n))) : D.Bytes & Bool}:
  PROOF.fast_find.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=fast_find.go)
   def fast_find.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +c: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hc: {U32.is_lt(c, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {FA.find(b, from, to, c) == B.find(b, from, to, c) : D.Bytes & U32}:
  PROOF.fast_find2.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=fast_find2.go)
   def fast_find2.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +c1: U32, +c2: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hc1: {U32.is_lt(c1, 256) == True{} : Bool}, hc2: {U32.is_lt(c2, 256) == True{} : Bool}, m_b: C.BMirror(b)) ->
     {FA.find2(b, from, to, c1, c2) == B.find2(b, from, to, c1, c2) : D.Bytes & U32}:
  PROOF.fast_find_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=fast_find_pair.go)
   def fast_find_pair.go(-b: D.Bytes, +from: U32, +to: U32, +c: U32, m_b: C.BMirror(b)) ->
     {FA.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, FA.find(b, from, to, c))) : D.Bytes & U32}:
  PROOF.fast_find2_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=fast_find2_pair.go)
   def fast_find2_pair.go(-b: D.Bytes, +from: U32, +to: U32, +c1: U32, +c2: U32, m_b: C.BMirror(b)) ->
     {FA.find2(b, from, to, c1, c2) == (b, Pair.snd(D.Bytes, U32, FA.find2(b, from, to, c1, c2))) : D.Bytes & U32}:
  PROOF.fast_append_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=fast_append_view.go)
   def fast_append_view.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +e: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, he: {D.ok(src, e) == True{} : Bool}, hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
     {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n))) == List.append(&2, U32, D.view(dst), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}:
  PROOF.fast_append_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=fast_append_ok.go)
   def fast_append_ok.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
     {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), d) == True{} : Bool}:
  PROOF.fast_append_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&name=fast_append_pair.go)
   def fast_append_pair.go(-dst: D.Bytes, -src: D.Bytes, +s: U32, +n: U32, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
     {FA.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}:
  Bytes.empty (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=empty)
   # An empty Bytes with room for 4 * 2^d bytes.
   def empty(+d: Nat) -> D.Bytes:
  Bytes.at.fin (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=at.fin)
   def at.fin(+len: U32, +i: U32, r: Array<U32> & U32) -> D.Bytes & U32:
  Bytes.at (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=at)
   # Byte i (for i < len).
   def at(b: D.Bytes, +i: U32) -> D.Bytes & U32:
  Bytes.set.fin (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=set.fin)
   def set.fin(+len: U32, +i: U32, +v: U32, r: Array<U32> & U32) -> D.Bytes:
  Bytes.set (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=set)
   # Byte i set to v (for i < len and v < 256).
   def set(b: D.Bytes, +i: U32, +v: U32) -> D.Bytes:
  Bytes.push.fin (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=push.fin)
   def push.fin(+len: U32, +v: U32, r: Array<U32> & U32) -> D.Bytes:
  Bytes.push (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=push)
   # v added at the end (for len < cap and v < 256).
   def push(b: D.Bytes, +v: U32) -> D.Bytes:
  Bytes.append.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=append.go)
   # n more bytes of src, from s; r holds src's byte s.
   def append.go(n: Nat, dst: D.Bytes, r: D.Bytes & U32, +s: U32) -> D.Bytes & D.Bytes:
  Bytes.append (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=append)
   # dst with bytes s .. s+n-1 of src added at the end; src handed back.
   def append(dst: D.Bytes, src: D.Bytes, +s: U32, +n: U32) -> D.Bytes & D.Bytes:
  Bytes.grow.go (https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/bytes.bend&name=grow.go)
   # Word i onwards copied into dst; r holds word i of the old block.
   def grow.go(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +i: U32) -> Array<U32>:
More: https://jend.leeeet.dev/packages/lawful-bytes.txt?definitions_offset=100