law p0_low

lawful-bytes@0.1.1.0 · proof_fast_word.bend:235

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

235# The first word of a search: the bytes below i's place are set to 0xFF, so
236# the first zero byte is the first c at or above that place.
237law p0_low:
238  for +w: U32
239  for +c: U32
240  for +i: U32
241  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
242  {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(FA.low(i)))) == Nat.add(U32.to_nat((i .&. 3 : U32)), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat((i .&. 3 : U32))), c)) : Nat}