def red_mul

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

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

313def red_mul(+n: Nat, +low: Word(n), +a: List<&2, Bool>, +b: List<&2, Bool>) -> {P.reduce(n, low, P.mul(a, b)) == sm(n, low, a, P.reduce(n, low, b)) : Word(n)}:
314  match a:
315    case Nil{}:
316      {==}
317    case c <> q:
318      %tx_sm(n, low, q, P.reduce(n, low, b)) : {P.reduce(n, low, P.add(P.scale(c, b), False{} <> P.mul(q, b))) == Word.xor(n, P.wscale(n, c, P.reduce(n, low, b)), _) : Word(n)}
319      %red_mul(n, low, q, b) : {P.reduce(n, low, P.add(P.scale(c, b), False{} <> P.mul(q, b))) == Word.xor(n, P.wscale(n, c, P.reduce(n, low, b)), P.times_x(n, low, _)) : Word(n)}
320      %red_shift(n, low, P.mul(q, b)) : {P.reduce(n, low, P.add(P.scale(c, b), False{} <> P.mul(q, b))) == Word.xor(n, P.wscale(n, c, P.reduce(n, low, b)), _) : Word(n)}
321      %red_scale(n, low, c, b) : {P.reduce(n, low, P.add(P.scale(c, b), False{} <> P.mul(q, b))) == Word.xor(n, _, P.reduce(n, low, False{} <> P.mul(q, b))) : Word(n)}
322      red_add(n, low, P.scale(c, b), False{} <> P.mul(q, b))