def tx_xor

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

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

202def tx_xor(+n: Nat, +low: Word(n), +a: Word(n), +b: Word(n)) -> {P.times_x(n, low, Word.xor(n, a, b)) == Word.xor(n, P.times_x(n, low, a), P.times_x(n, low, b)) : Word(n)}:
203  %Equal.sym(Bool, P.top(n, Word.xor(n, a, b)), Bool.xor(P.top(n, a), P.top(n, b)), top_xor(n, a, b)) : {Word.xor(n, P.wscale(n, _, low), Word.shl(n, Word.xor(n, a, b))) == Word.xor(n, P.times_x(n, low, a), P.times_x(n, low, b)) : Word(n)}
204  %Equal.sym(Word(n), P.wscale(n, Bool.xor(P.top(n, a), P.top(n, b)), low), Word.xor(n, P.wscale(n, P.top(n, a), low), P.wscale(n, P.top(n, b), low)), wscale_xor(n, P.top(n, a), P.top(n, b), low)) : {Word.xor(n, _, Word.shl(n, Word.xor(n, a, b))) == Word.xor(n, P.times_x(n, low, a), P.times_x(n, low, b)) : Word(n)}
205  %Equal.sym(Word(n), Word.shl(n, Word.xor(n, a, b)), Word.xor(n, Word.shl(n, a), Word.shl(n, b)), shl_xor(n, a, b)) : {Word.xor(n, Word.xor(n, P.wscale(n, P.top(n, a), low), P.wscale(n, P.top(n, b), low)), _) == Word.xor(n, P.times_x(n, low, a), P.times_x(n, low, b)) : Word(n)}
206  xor_swap4(n, P.wscale(n, P.top(n, a), low), P.wscale(n, P.top(n, b), low), Word.shl(n, a), Word.shl(n, b))