law ej_xor

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:238

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

238law ej_xor:
239  for +w: U32
240  for +c: U32
241  for +j: Nat
242  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
243  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
244  {U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), j), 0) == U32.is_eq(W.byte(w, j), c) : Bool}