def constant_xor

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gf.bend:222

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P

222def constant_xor(+n: Nat, +c: Bool, +d: Bool) -> {P.constant(n, Bool.xor(c, d)) == Word.xor(n, P.constant(n, c), P.constant(n, d)) : Word(n)}:
223  match n:
224    case 0n:
225      {==}
226    case 1n+p:
227      %Equal.sym(Word(p), Word.xor(p, Word.zero(p), Word.zero(p)), Word.zero(p), xor_zero_l(p, Word.zero(p))) : {WCon{Bool.xor(c, d), Word.zero(p)} == WCon{Bool.xor(c, d), _} : Word(1n+p)}
228      {==}