def shl_xor

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

import Base

147def shl_xor(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.shl(n, Word.xor(n, a, b)) == Word.xor(n, Word.shl(n, a), Word.shl(n, b)) : Word(n)}:
148  match n a b:
149    case 0n WNil{} WNil{}:
150      {==}
151    case 1n+p WCon{x, s} WCon{y, t}:
152      %put_xor(p, x, y, s, t) : {WCon{False{}, Word.shl.put(p, Bool.xor(x, y), Word.xor(p, s, t))} == WCon{False{}, _} : Word(1n+p)}
153      {==}