law allz_mask

lawful-words@0.1.0.0 · proof_zb.bend:609

import Base

609# A byte masked with 255.
610law allz_mask:
611  for +n: Nat
612  for +x: Word(8n)
613  for +r: Word(n)
614  {allz(Nat.add(8n, n), Word.and(Nat.add(8n, n), app8(n, x, r), app8(n, ones8(), Word.zero(n))))
615    == Bool.and(allz(8n, x), allz(n, Word.and(n, r, Word.zero(n)))) : Bool}