law append_view

lawful-bytes@0.1.1.0 · LAWS.bend:189

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

189# append adds n bytes of src, from s, at the end of dst.
190law append_view:
191  for dst: D.Bytes
192  for src: D.Bytes
193  for d: Nat
194  for e: Nat
195  for s: U32
196  for n: U32
197  for hd: {D.ok(dst, d) == True{} : Bool}
198  for he: {D.ok(src, e) == True{} : Bool}
199  for hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}
200  for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
201  {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>}