def red_add

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

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

230def red_add(+n: Nat, +low: Word(n), +p: List<&2, Bool>, +q: List<&2, Bool>) -> {P.reduce(n, low, P.add(p, q)) == Word.xor(n, P.reduce(n, low, p), P.reduce(n, low, q)) : Word(n)}:
231  match p q:
232    case Nil{} _:
233      Equal.sym(Word(n), Word.xor(n, Word.zero(n), P.reduce(n, low, q)), P.reduce(n, low, q), xor_zero_l(n, P.reduce(n, low, q)))
234    case x <> xs Nil{}:
235      Equal.sym(Word(n), Word.xor(n, P.reduce(n, low, x <> xs), Word.zero(n)), P.reduce(n, low, x <> xs), xor_zero_r(n, P.reduce(n, low, x <> xs)))
236    case x <> xs y <> ys:
237      %Equal.sym(Word(n), P.reduce(n, low, P.add(xs, ys)), Word.xor(n, P.reduce(n, low, xs), P.reduce(n, low, ys)), red_add(n, low, xs, ys)) : {Word.xor(n, P.constant(n, Bool.xor(x, y)), P.times_x(n, low, _)) == Word.xor(n, P.reduce(n, low, x <> xs), P.reduce(n, low, y <> ys)) : Word(n)}
238      %Equal.sym(Word(n), P.times_x(n, low, Word.xor(n, P.reduce(n, low, xs), P.reduce(n, low, ys))), Word.xor(n, P.times_x(n, low, P.reduce(n, low, xs)), P.times_x(n, low, P.reduce(n, low, ys))), tx_xor(n, low, P.reduce(n, low, xs), P.reduce(n, low, ys))) : {Word.xor(n, P.constant(n, Bool.xor(x, y)), _) == Word.xor(n, P.reduce(n, low, x <> xs), P.reduce(n, low, y <> ys)) : Word(n)}
239      %Equal.sym(Word(n), P.constant(n, Bool.xor(x, y)), Word.xor(n, P.constant(n, x), P.constant(n, y)), constant_xor(n, x, y)) : {Word.xor(n, _, Word.xor(n, P.times_x(n, low, P.reduce(n, low, xs)), P.times_x(n, low, P.reduce(n, low, ys)))) == Word.xor(n, P.reduce(n, low, x <> xs), P.reduce(n, low, y <> ys)) : Word(n)}
240      xor_swap4(n, P.constant(n, x), P.constant(n, y), P.times_x(n, low, P.reduce(n, low, xs)), P.times_x(n, low, P.reduce(n, low, ys)))