law cut_ends

lawful-fields@0.1.1.0 · LAWS.bend:24

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-fields@0.1.1.0/defs.bend as F
import lawful-fields@0.1.1.0/fields.bend as C

24# The ends are exactly where split's pieces end, counted from from (so they
25# increase, and each next piece starts just after the previous end).
26law cut_ends:
27  for b: D.Bytes
28  for d: Nat
29  for from: U32
30  for to: U32
31  for sep: U32
32  for n: Nat
33  for h: {D.ok(b, d) == True{} : Bool}
34  for hft: {U32.is_le(from, to) == True{} : Bool}
35  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
36  for hs: {U32.is_lt(sep, 256) == True{} : Bool}
37  {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>}