law find_view

lawful-bytes@0.1.1.0 · LAWS.bend:81

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

81# find answers the first index in from .. to-1 holding c, or to. c must be a
82# byte value: a word-at-a-time search compares 8 bits per byte.
83law find_view:
84  for b: D.Bytes
85  for d: Nat
86  for from: U32
87  for to: U32
88  for c: U32
89  for h: {D.ok(b, d) == True{} : Bool}
90  for hft: {U32.is_le(from, to) == True{} : Bool}
91  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
92  for hc: {U32.is_lt(c, 256) == True{} : Bool}
93  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find(b, from, to, c))) == D.first(D.view(b), U32.to_nat(from), U32.to_nat(to), c) : Nat}