law zb_bidx

lawful-bytes@0.1.1.0 · proof_fast_word.bend:70

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

70# bidx finds the first zero byte.
71law zb_bidx:
72  for +v: U32
73  for +h: {Nat.is_lt(P0(v), 4n) == True{} : Bool}
74  {U32.to_nat(FA.bidx(FA.zb(v))) == P0(v) : Nat}