law fast_find

lawful-bytes@0.1.1.0 · LAWS.bend:414

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

414# The word-at-a-time find gives exactly the reference result (the same Bytes
415# and the same index). c must be a byte value: the search compares 8 bits per
416# byte.
417law fast_find:
418  for b: D.Bytes
419  for d: Nat
420  for from: U32
421  for to: U32
422  for c: U32
423  for h: {D.ok(b, d) == True{} : Bool}
424  for hft: {U32.is_le(from, to) == True{} : Bool}
425  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
426  for hc: {U32.is_lt(c, 256) == True{} : Bool}
427  {FA.find(b, from, to, c) == B.find(b, from, to, c) : D.Bytes & U32}