law p0_xor

lawful-bytes@0.1.1.0 · proof_fast_word.bend:111

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

111# Searching w for c is searching w xor rep(c) for a zero byte.
112law p0_xor:
113  for +w: U32
114  for +c: U32
115  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
116  {P0(U32.xor(w, FA.rep(c))) == D.run_len(C.L4(w), c) : Nat}