law shift_view

lawful-bytes@0.1.1.0 · LAWS.bend:257

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/bytes.bend as B

257# shift drops the first k bytes and moves the rest to the start (for reusing a
258# buffer when reading a stream in pieces).
259law shift_view:
260  for b: D.Bytes
261  for d: Nat
262  for k: U32
263  for h: {D.ok(b, d) == True{} : Bool}
264  for hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}
265  {D.view(B.shift(b, k)) == List.drop(&2, U32, D.view(b), U32.to_nat(k)) : List<&2, U32>}