law e_lo

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:272

import Base
import lawful-words@0.1.0.0/defs.bend as W
import lawful-bytes@0.1.1.0/fast.bend as FA

272# A byte below the start: set to 0xFF, never zero.
273law e_lo:
274  for +w: U32
275  for +c: U32
276  for +m: U32
277  for +j: Nat
278  for +hm: {W.byte(m, j) == 255 : U32}
279  {U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), m), j), 0) == False{} : Bool}