law same_view

lawful-bytes@0.1.1.0 · LAWS.bend:126

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

126# same compares two ranges of equal length, n bytes each.
127law same_view:
128  for a: D.Bytes
129  for b: D.Bytes
130  for d: Nat
131  for e: Nat
132  for i: U32
133  for j: U32
134  for n: U32
135  for ha: {D.ok(a, d) == True{} : Bool}
136  for hb: {D.ok(b, e) == True{} : Bool}
137  for hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(a)) == True{} : Bool}
138  for hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}
139  {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))) == D.list_eq(D.slice(D.view(a), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}