lawful-fields

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

Definitions (234, 1 to 100 shown):
  LAWS.cut_view (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=cut_view)
   # cut answers the end offsets of the first n pieces of from .. to-1, split at
   # sep: the pieces those ends delimit are the first n of F.split.
   law cut_view:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: U32
     for sep: U32
     for n: Nat
     for h: {D.ok(b, d) == True{} : Bool}
     for hft: {U32.is_le(from, to) == True{} : Bool}
     …
  LAWS.cut_ends (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=cut_ends)
   # The ends are exactly where split's pieces end, counted from from (so they
   # increase, and each next piece starts just after the previous end).
   law cut_ends:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: U32
     for sep: U32
     for n: Nat
     for h: {D.ok(b, d) == True{} : Bool}
     for hft: {U32.is_le(from, to) == True{} : Bool}
     …
  LAWS.cut_bounds (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=cut_bounds)
   # Every end lies in from .. to.
   law cut_bounds:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: U32
     for sep: U32
     for n: Nat
     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.cut_pair (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=cut_pair)
   law cut_pair:
     for b: D.Bytes
     for from: U32
     for to: U32
     for sep: U32
     for n: Nat
     {C.cut(b, from, to, sep, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n))) : D.Bytes & List<&2, U32>}
  LAWS.num_view (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=num_view)
   # num reads the decimal number in from .. to-1 when it is one and fits a U32.
   law num_view:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: 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}
     {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) == F.decb(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), Nat.pow(2n, 32n)) : Maybe<&2, Nat>}
  LAWS.num_pair (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=num_pair)
   law num_pair:
     for b: D.Bytes
     for from: U32
     for to: U32
     {C.num(b, from, to) == (b, Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) : D.Bytes & Maybe<&2, U32>}
  LAWS.split_length (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=split_length)
   # The number of pieces split gives is one more than the number of separators.
   law split_length:
     for xs: List<&2, U32>
     for sep: U32
     {List.length(&2, List<&2, U32>, F.split(xs, sep)) == Nat.add(F.count(xs, sep), 1n) : Nat}
  LAWS.split_join (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=split_join)
   # Joining the pieces with the separator gives xs back.
   law split_join:
     for xs: List<&2, U32>
     for sep: U32
     {F.join(F.split(xs, sep), sep) == xs : List<&2, U32>}
  LAWS.digits_view (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=digits_view)
   # digits says the bytes are one or more decimal digits, a number of any size
   # (num answers None both for non-numbers and for numbers of 2^32 or more).
   law digits_view:
     for b: D.Bytes
     for d: Nat
     for from: U32
     for to: 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}
     {Pair.snd(D.Bytes, Bool, C.digits(b, from, to)) == F.all_digits(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool}
  LAWS.digits_pair (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=digits_pair)
   law digits_pair:
     for b: D.Bytes
     for from: U32
     for to: U32
     {C.digits(b, from, to) == (b, Pair.snd(D.Bytes, Bool, C.digits(b, from, to))) : D.Bytes & Bool}
  LAWS.put_dec_view (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=put_dec_view)
   # put_dec writes n in decimal at the end (room for 10 more bytes needed).
   law put_dec_view:
     for b: D.Bytes
     for d: Nat
     for n: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}
     {D.view(C.put_dec(b, n)) == List.append(&2, U32, D.view(b), F.show(n)) : List<&2, U32>}
  LAWS.put_dec_ok (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=put_dec_ok)
   law put_dec_ok:
     for b: D.Bytes
     for d: Nat
     for n: U32
     for h: {D.ok(b, d) == True{} : Bool}
     for hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}
     {D.ok(C.put_dec(b, n), d) == True{} : Bool}
  LAWS.split_text (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=split_text)
   # Splitting bytes is splitting their text.
   law split_text:
     for xs: List<&2, U32>
     for sep: U32
     {String.split(F.text(xs), Chr{sep}) == F.texts(F.split(xs, sep)) : List<&2, String>}
  LAWS.join_text (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=join_text)
   # Joining bytes is joining their text.
   law join_text:
     for ps: List<&2, List<&2, U32>>
     for sep: U32
     {F.text(F.join(ps, sep)) == String.join(F.texts(ps), F.text([sep])) : String}
  LAWS.text_codes (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=text_codes)
   law text_codes:
     for s: String
     {F.text(F.codes(s)) == s : String}
  LAWS.join_at (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=join_at)
   # Joining a list of pieces splits at piece k: the first k+1 pieces, the
   # separator, the rest.
   law join_at:
     for ps: List<&2, List<&2, U32>>
     for sep: U32
     for k: Nat
     for h: {Nat.is_lt(Nat.add(k, 1n), List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
     {F.join(ps, sep) == List.append(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep), Con{sep, F.join(List.drop(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep)}) : List<&2, U32>}
  LAWS.ends_join (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=ends_join)
   # Piece k ends at the k-th end: the first k+1 pieces joined, from from.
   law ends_join:
     for ps: List<&2, List<&2, U32>>
     for sep: U32
     for from: Nat
     for k: Nat
     for h: {Nat.is_lt(k, List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
     {List.get(&2, Nat, F.ends(ps, from), k) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep)))} : Maybe<&2, Nat>}
  LAWS.pieces_length (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=pieces_length)
   law pieces_length:
     for es: List<&2, U32>
     for xs: List<&2, U32>
     for from: Nat
     {List.length(&2, List<&2, U32>, F.pieces(es, xs, from)) == List.length(&2, U32, es) : Nat}
  LAWS.decb_fits (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/LAWS.bend&name=decb_fits)
   # decb (with bound 2^32) is dec when the number fits.
   law decb_fits:
     for xs: List<&2, U32>
     for n: Nat
     for h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
     for hn: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
     {F.decb(xs, Nat.pow(2n, 32n)) == Some{n} : Maybe<&2, Nat>}
  PROOF.cut_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=cut_view.go)
   def cut_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, 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}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) ->
     {F.pieces(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n)), D.view(b), U32.to_nat(from)) == List.take(&2, List<&2, U32>, F.split(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), n) : List<&2, List<&2, U32>>}:
  PROOF.cut_ends.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=cut_ends.go)
   def cut_ends.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, 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}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) ->
     {F.nats(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n))) == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from)), n) : List<&2, Nat>}:
  PROOF.cut_bounds.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=cut_bounds.go)
   def cut_bounds.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, 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}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) ->
     {F.within(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n)), U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}:
  PROOF.cut_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=cut_pair.go)
   def cut_pair.go(-b: D.Bytes, +from: U32, +to: U32, +sep: U32, +n: Nat, m_b: BC.BMirror(b)) ->
     {C.cut(b, from, to, sep, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n))) : D.Bytes & List<&2, U32>}:
  PROOF.num_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=num_view.go)
   def num_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: 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}, m_b: BC.BMirror(b)) ->
     {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) == F.decb(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), Nat.pow(2n, 32n)) : Maybe<&2, Nat>}:
  PROOF.num_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=num_pair.go)
   def num_pair.go(-b: D.Bytes, +from: U32, +to: U32, m_b: BC.BMirror(b)) ->
     {C.num(b, from, to) == (b, Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) : D.Bytes & Maybe<&2, U32>}:
  PROOF.digits_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=digits_view.go)
   def digits_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: 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}, m_b: BC.BMirror(b)) ->
     {Pair.snd(D.Bytes, Bool, C.digits(b, from, to)) == F.all_digits(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool}:
  PROOF.digits_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=digits_pair.go)
   def digits_pair.go(-b: D.Bytes, +from: U32, +to: U32, m_b: BC.BMirror(b)) ->
     {C.digits(b, from, to) == (b, Pair.snd(D.Bytes, Bool, C.digits(b, from, to))) : D.Bytes & Bool}:
  PROOF.put_dec_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=put_dec_view.go)
   def put_dec_view.go(-b: D.Bytes, +d: Nat, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}, m_b: BC.BMirror(b)) ->
     {D.view(C.put_dec(b, n)) == List.append(&2, U32, D.view(b), F.show(n)) : List<&2, U32>}:
  PROOF.put_dec_ok.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/PROOF.bend&name=put_dec_ok.go)
   def put_dec_ok.go(-b: D.Bytes, +d: Nat, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}, m_b: BC.BMirror(b)) ->
     {D.ok(C.put_dec(b, n), d) == True{} : Bool}:
  Defs.split.push (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=split.push)
   def split.push(+c: U32, ps: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
  Defs.split.fin (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=split.fin)
   def split.fin(+c: U32, r: List<&2, List<&2, U32>>, cut: Bool) -> List<&2, List<&2, U32>>:
  Defs.split (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=split)
   # The pieces of xs between separators, as Base's String.split does for text:
   # always at least one piece, so [] gives [[]] and [sep] gives [[], []].
   def split(xs: List<&2, U32>, +sep: U32) -> List<&2, List<&2, U32>>:
  Defs.digit.if (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=digit.if)
   def digit.if(+x: U32, ok: Bool) -> Maybe<&2, Nat>:
  Defs.digit (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=digit)
   # The value of a decimal digit byte ('0' is 48).
   def digit(+x: U32) -> Maybe<&2, Nat>:
  Defs.dec.push (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=dec.push)
   def dec.push(acc: Maybe<&2, Nat>, d: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
  Defs.dec.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=dec.go)
   def dec.go(xs: List<&2, U32>, acc: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
  Defs.dec (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=dec)
   # A decimal number: one or more digits (leading zeros allowed), nothing else;
   # any size (framebender's Pos.read on text is the same function).
   def dec(xs: List<&2, U32>) -> Maybe<&2, Nat>:
  Defs.decb.if (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=decb.if)
   def decb.if(+n: Nat, fits: Bool) -> Maybe<&2, Nat>:
  Defs.decb.of (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=decb.of)
   def decb.of(m: Maybe<&2, Nat>, +bound: Nat) -> Maybe<&2, Nat>:
  Defs.decb (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=decb)
   # A decimal number below bound; None otherwise. The laws use bound = 2^32 (what
   # fits a U32), written Nat.pow(2n, 32n) in each law: the checker evaluates a
   # constant hidden in a definition, and 2^32 in unary is too deep.
   def decb(xs: List<&2, U32>, +bound: Nat) -> Maybe<&2, Nat>:
  Defs.nat_of (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=nat_of)
   # The number a Maybe<U32> stands for.
   def nat_of(m: Maybe<&2, U32>) -> Maybe<&2, Nat>:
  Defs.pieces (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=pieces)
   # The pieces of xs that end at each offset of es, the first starting at from
   # and each next one just after the previous end (where the separator was).
   def pieces(es: List<&2, U32>, +xs: List<&2, U32>, +from: Nat) -> List<&2, List<&2, U32>>:
  Defs.within (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=within)
   # Every offset in es lies in from .. to.
   def within(es: List<&2, U32>, +from: Nat, +to: Nat) -> Bool:
  Defs.count.if (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=count.if)
   def count.if(hit: Bool, +n: Nat) -> Nat:
  Defs.count (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=count)
   # How many times sep occurs in xs.
   def count(xs: List<&2, U32>, +sep: U32) -> Nat:
  Defs.join.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=join.go)
   def join.go(ps: List<&2, List<&2, U32>>, +sep: U32) -> List<&2, U32>:
  Defs.join (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=join)
   # The pieces joined with sep between them. join undoes split:
   # join(split(xs, sep), sep) == xs (the other way round fails when a piece holds
   # sep).
   def join(ps: List<&2, List<&2, U32>>, +sep: U32) -> List<&2, U32>:
  Defs.text (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=text)
   # Bytes as text and back: one Char per byte (Chr{b}), with no decoding (the
   # way framebender reads files). For text whose characters are all below 256.
   def text(xs: List<&2, U32>) -> String:
  Defs.texts (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=texts)
   def texts(ps: List<&2, List<&2, U32>>) -> List<&2, String>:
  Defs.codes (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=codes)
   def codes(s: String) -> List<&2, U32>:
  Defs.show (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=show)
   # The decimal digits of a number, as bytes (Base's Nat.show).
   def show(n: U32) -> List<&2, U32>:
  Defs.ends (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=ends)
   # The end offset of each piece, the first piece starting at from and each next
   # one just after the previous end.
   def ends(ps: List<&2, List<&2, U32>>, +from: Nat) -> List<&2, Nat>:
  Defs.nats (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=nats)
   # The numbers words stand for.
   def nats(es: List<&2, U32>) -> List<&2, Nat>:
  Defs.all_digits (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=all_digits)
   # xs is one or more digits (any value).
   def all_digits(xs: List<&2, U32>) -> Bool:
  Fields.cut.cons (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=cut.cons)
   def cut.cons(+e: U32, r: D.Bytes & List<&2, U32>) -> D.Bytes & List<&2, U32>:
  Fields.cut.next (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=cut.next)
   # The end of the piece starting at from, searched only when want is set (no
   # scan past the last field asked for; the answer is then unused).
   def cut.next(want: Bool, b: D.Bytes, +from: U32, +to: U32, +sep: U32) -> D.Bytes & U32:
  Fields.cut.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=cut.go)
   # n counts the pieces still wanted, this one included; more says the previous
   # piece ended at a separator; r holds this piece's end.
   def cut.go(+n: Nat, more: Bool, r: D.Bytes & U32, +to: U32, +sep: U32) -> D.Bytes & List<&2, U32>:
  Fields.cut (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=cut)
   # The end offsets of the first n pieces of bytes from .. to-1, split at sep:
   # each end is where a separator is, or to for the last piece.
   def cut(b: D.Bytes, +from: U32, +to: U32, +sep: U32, +n: Nat) -> D.Bytes & List<&2, U32>:
  Fields.num.fin (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=num.fin)
   def num.fin(+acc: U32, ok: Bool) -> Maybe<&2, U32>:
  Fields.num.out (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=num.out)
   def num.out(+acc: U32, ok: Bool, r: D.Bytes & U32) -> D.Bytes & Maybe<&2, U32>:
  Fields.num.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=num.go)
   # r holds byte j; acc is the value so far; ok says every byte was a digit and
   # nothing overflowed.
   def num.go(n: Nat, r: D.Bytes & U32, +j: U32, +acc: U32, ok: Bool) -> D.Bytes & Maybe<&2, U32>:
  Fields.num (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=num)
   # The decimal number in bytes from .. to-1, if it is one and below 2^32.
   def num(b: D.Bytes, +from: U32, +to: U32) -> D.Bytes & Maybe<&2, U32>:
  Fields.digits.out (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=digits.out)
   def digits.out(ok: Bool, r: D.Bytes & U32) -> D.Bytes & Bool:
  Fields.digits.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=digits.go)
   # r holds byte j; ok says every byte so far was a digit.
   def digits.go(n: Nat, r: D.Bytes & U32, +j: U32, ok: Bool) -> D.Bytes & Bool:
  Fields.digits (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=digits)
   # Bytes from .. to-1 are one or more decimal digits (a number of any size).
   def digits(b: D.Bytes, +from: U32, +to: U32) -> D.Bytes & Bool:
  Fields.put_dec.go (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=put_dec.go)
   def put_dec.go(xs: List<&2, U32>, b: D.Bytes) -> D.Bytes:
  Fields.put_dec.digits (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=put_dec.digits)
   # The decimal digits of n, most significant first, before acc; small says
   # n < 10 (the last digit). At most 10 steps for a U32.
   def put_dec.digits(k: Nat, small: Bool, +n: U32, acc: List<&2, U32>) -> List<&2, U32>:
  Fields.put_dec.list (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=put_dec.list)
   def put_dec.list(+n: U32) -> List<&2, U32>:
  Fields.put_dec (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=put_dec)
   # n written in decimal at the end of b (for room enough: at most 10 bytes).
   def put_dec(b: D.Bytes, +n: U32) -> D.Bytes:
  ProofCut.tz (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=tz)
   law tz:
     for -A: Data
     for +xs: List<&2, A>
     {List.take(&2, A, xs, 0n) == Nil{} : List<&2, A>}
  ProofCut.is_nil_t (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=is_nil_t)
   def is_nil_t(xs: List<&2, U32>) -> Type:
  ProofCut.nil_cons (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=nil_cons)
   law nil_cons:
     for -x: U32
     for -t: List<&2, U32>
     for e: {Nil{} == x <> t : List<&2, U32>}
     Empty
  ProofCut.le_antisym (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=le_antisym)
   law le_antisym:
     for +a: Nat
     for +b: Nat
     for +h1: {Nat.is_le(a, b) == True{} : Bool}
     for +h2: {Nat.is_le(b, a) == True{} : Bool}
     {a == b : Nat}
  ProofCut.sub_le_of (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sub_le_of)
   # T <= s + r gives T - s <= r.
   law sub_le_of:
     for +tt: Nat
     for +s: Nat
     for +r: Nat
     for +h: {Nat.is_le(tt, Nat.add(s, r)) == True{} : Bool}
     {Nat.is_le(Nat.sub(tt, s), r) == True{} : Bool}
  ProofCut.lt_sub_of (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=lt_sub_of)
   # s + r < T gives r < T - s.
   law lt_sub_of:
     for +s: Nat
     for +r: Nat
     for +tt: Nat
     for +h: {Nat.is_lt(Nat.add(s, r), tt) == True{} : Bool}
     {Nat.is_lt(r, Nat.sub(tt, s)) == True{} : Bool}
  ProofCut.sub_mono (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sub_mono)
   law sub_mono:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     for +h: {Nat.is_le(a, b) == True{} : Bool}
     {Nat.is_le(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}
  ProofCut.sub_sub (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sub_sub)
   law sub_sub:
     for +tt: Nat
     for +s: Nat
     for +k: Nat
     {Nat.sub(Nat.sub(tt, s), k) == Nat.sub(tt, Nat.add(s, k)) : Nat}
  ProofCut.drop_drop (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=drop_drop)
   law drop_drop:
     for +xs: List<&2, U32>
     for +a: Nat
     for +b: Nat
     {List.drop(&2, U32, List.drop(&2, U32, xs, a), b) == List.drop(&2, U32, xs, Nat.add(a, b)) : List<&2, U32>}
  ProofCut.drop_take (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=drop_take)
   law drop_take:
     for +zs: List<&2, U32>
     for +n: Nat
     for +k: Nat
     {List.drop(&2, U32, List.take(&2, U32, zs, n), k) == List.take(&2, U32, List.drop(&2, U32, zs, k), Nat.sub(n, k)) : List<&2, U32>}
  ProofCut.slice_drop (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=slice_drop)
   # A slice dropped by k is the slice from s + k.
   law slice_drop:
     for +xs: List<&2, U32>
     for +s: Nat
     for +tt: Nat
     for +k: Nat
     {List.drop(&2, U32, D.slice(xs, s, Nat.sub(tt, s)), k) == D.slice(xs, Nat.add(s, k), Nat.sub(tt, Nat.add(s, k))) : List<&2, U32>}
  ProofCut.nn (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=nn)
   def nn(ps: List<&2, List<&2, U32>>) -> Bool:
  ProofCut.nn_push (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=nn_push)
   law nn_push:
     for +c: U32
     for +ps: List<&2, List<&2, U32>>
     {nn(F.split.push(c, ps)) == True{} : Bool}
  ProofCut.nn_fin (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=nn_fin)
   law nn_fin:
     for +c: U32
     for +ps: List<&2, List<&2, U32>>
     for +b: Bool
     {nn(F.split.fin(c, ps, b)) == True{} : Bool}
  ProofCut.split_nn (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=split_nn)
   law split_nn:
     for +xs: List<&2, U32>
     for +sep: U32
     {nn(F.split(xs, sep)) == True{} : Bool}
  ProofCut.sp1c (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sp1c)
   law sp1c:
     for +x: U32
     for +t: List<&2, U32>
     for +sep: U32
     for +b: Bool
     for +hb: {U32.is_eq(x, sep) == b : Bool}
     for +h: {Nat.is_lt(D.run_len(x <> t, sep), List.length(&2, U32, x <> t)) == True{} : Bool}
     for ih: {Nat.is_lt(D.run_len(t, sep), List.length(&2, U32, t)) == True{} : Bool} -> {F.split(t, sep) == List.take(&2, U32, t, D.run_len(t, sep)) <> F.split(List.drop(&2, U32, t, Nat.add(D.run_len(t, sep), 1n)), sep) : List<&2, List<&2, U32>>}
     {F.split(x <> t, sep) == List.take(&2, U32, x <> t, D.run_len(x <> t, sep)) <> F.split(List.drop(&2, U32, x <> t, Nat.add(D.run_len(x <> t, sep), 1n)), sep) : List<&2, List<&2, U32>>}
  ProofCut.sp1 (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sp1)
   # With a separator in ys, the first piece ends at it.
   law sp1:
     for +ys: List<&2, U32>
     for +sep: U32
     for +h: {Nat.is_lt(D.run_len(ys, sep), List.length(&2, U32, ys)) == True{} : Bool}
     {F.split(ys, sep) == List.take(&2, U32, ys, D.run_len(ys, sep)) <> F.split(List.drop(&2, U32, ys, Nat.add(D.run_len(ys, sep), 1n)), sep) : List<&2, List<&2, U32>>}
  ProofCut.sp2c (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sp2c)
   law sp2c:
     for +x: U32
     for +t: List<&2, U32>
     for +sep: U32
     for +b: Bool
     for +hb: {U32.is_eq(x, sep) == b : Bool}
     for +h: {Nat.is_le(List.length(&2, U32, x <> t), D.run_len(x <> t, sep)) == True{} : Bool}
     for ih: {Nat.is_le(List.length(&2, U32, t), D.run_len(t, sep)) == True{} : Bool} -> {F.split(t, sep) == [t] : List<&2, List<&2, U32>>}
     {F.split(x <> t, sep) == [x <> t] : List<&2, List<&2, U32>>}
  ProofCut.sp2 (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sp2)
   # Without one, split gives ys itself.
   law sp2:
     for +ys: List<&2, U32>
     for +sep: U32
     for +h: {Nat.is_le(List.length(&2, U32, ys), D.run_len(ys, sep)) == True{} : Bool}
     {F.split(ys, sep) == [ys] : List<&2, List<&2, U32>>}
  ProofCut.PN (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=PN)
   # pieces and within read only the numbers of their offsets.
   def PN(ns: List<&2, Nat>, +xs: List<&2, U32>, +from: Nat) -> List<&2, List<&2, U32>>:
  ProofCut.WN (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=WN)
   def WN(ns: List<&2, Nat>, +from: Nat, +to: Nat) -> Bool:
  ProofCut.pn (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=pn)
   law pn:
     for +es: List<&2, U32>
     for +xs: List<&2, U32>
     for +from: Nat
     {F.pieces(es, xs, from) == PN(F.nats(es), xs, from) : List<&2, List<&2, U32>>}
  ProofCut.wn (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=wn)
   law wn:
     for +es: List<&2, U32>
     for +a: Nat
     for +b: Nat
     {F.within(es, a, b) == WN(F.nats(es), a, b) : Bool}
  ProofCut.pntake (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=pntake)
   law pntake:
     for +ns: List<&2, Nat>
     for +n: Nat
     for +xs: List<&2, U32>
     for +s: Nat
     {PN(List.take(&2, Nat, ns, n), xs, s) == List.take(&2, List<&2, U32>, PN(ns, xs, s), n) : List<&2, List<&2, U32>>}
  ProofCut.wtake (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=wtake)
   law wtake:
     for +ns: List<&2, Nat>
     for +n: Nat
     for +a: Nat
     for +b: Nat
     for +hw: {WN(ns, a, b) == True{} : Bool}
     {WN(List.take(&2, Nat, ns, n), a, b) == True{} : Bool}
  ProofCut.wk (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=wk)
   # A lower bound may be lowered.
   law wk:
     for +ns: List<&2, Nat>
     for +a: Nat
     for +a2: Nat
     for +b: Nat
     for +h: {Nat.is_le(a, a2) == True{} : Bool}
     for +hw: {WN(ns, a2, b) == True{} : Bool}
     {WN(ns, a, b) == True{} : Bool}
  ProofCut.pre_get (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=pre_get)
   law pre_get:
     for +xs: List<&2, U32>
     for +s: Nat
     for +x: U32
     for +t: List<&2, U32>
     for +hp: {List.take(&2, U32, List.drop(&2, U32, xs, s), 1n+List.length(&2, U32, t)) == x <> t : List<&2, U32>}
     {List.get(&2, U32, xs, s) == Some{x} : Maybe<&2, U32>}
  ProofCut.pre_tail (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=pre_tail)
   law pre_tail:
     for +xs: List<&2, U32>
     for +s: Nat
     for +x: U32
     for +t: List<&2, U32>
     for +hp: {List.take(&2, U32, List.drop(&2, U32, xs, s), 1n+List.length(&2, U32, t)) == x <> t : List<&2, U32>}
     {List.take(&2, U32, List.drop(&2, U32, xs, Nat.add(s, 1n)), List.length(&2, U32, t)) == t : List<&2, U32>}
  ProofCut.ends_push (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=ends_push)
   # Pushing a byte onto the first piece shifts every end by one.
   law ends_push:
     for +x: U32
     for +ps: List<&2, List<&2, U32>>
     for +s: Nat
     for +hnn: {nn(ps) == True{} : Bool}
     {F.ends(F.split.push(x, ps), s) == F.ends(ps, Nat.add(s, 1n)) : List<&2, Nat>}
  ProofCut.sa (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sa)
   law sa:
     for +s: Nat
     for +l: Nat
     {Nat.sub(Nat.add(Nat.add(s, 1n), l), s) == 1n+l : Nat}
  ProofCut.pb_push (https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=pb_push)
   law pb_push:
     for +x: U32
     for +ps: List<&2, List<&2, U32>>
     for +xs: List<&2, U32>
     for +s: Nat
     for +hnn: {nn(ps) == True{} : Bool}
     for +hg: {List.get(&2, U32, xs, s) == Some{x} : Maybe<&2, U32>}
     for +ih: {PN(F.ends(ps, Nat.add(s, 1n)), xs, Nat.add(s, 1n)) == ps : List<&2, List<&2, U32>>}
     {PN(F.ends(F.split.push(x, ps), s), xs, s) == F.split.push(x, ps) : List<&2, List<&2, U32>>}
More: https://jend.leeeet.dev/packages/lawful-fields.txt?definitions_offset=100