law fast_find2

lawful-bytes@0.1.1.0 · LAWS.bend:429

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

429law fast_find2:
430  for b: D.Bytes
431  for d: Nat
432  for from: U32
433  for to: U32
434  for c1: U32
435  for c2: U32
436  for h: {D.ok(b, d) == True{} : Bool}
437  for hft: {U32.is_le(from, to) == True{} : Bool}
438  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
439  for hc1: {U32.is_lt(c1, 256) == True{} : Bool}
440  for hc2: {U32.is_lt(c2, 256) == True{} : Bool}
441  {FA.find2(b, from, to, c1, c2) == B.find2(b, from, to, c1, c2) : D.Bytes & U32}