law fast_append_view

lawful-bytes@0.1.1.0 · LAWS.bend:460

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

460# The word-at-a-time append writes whole words, so up to 3 bytes past the new
461# length differ from the reference's: its laws are append's, on the view.
462law fast_append_view:
463  for dst: D.Bytes
464  for src: D.Bytes
465  for d: Nat
466  for e: Nat
467  for s: U32
468  for n: U32
469  for hd: {D.ok(dst, d) == True{} : Bool}
470  for he: {D.ok(src, e) == True{} : Bool}
471  for hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}
472  for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
473  {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>}