def mul_sa

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

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

429# The product of two residues, reduced, is Algorithm 1 from Z = 0.
430def mul_sa(+n: Nat, +low: Word(n), +a: Word(n), +b: Word(n)) -> {P.reduce(n, low, P.mul(P.coefficients(n, a), P.coefficients(n, b))) == sa(n, low, P.coefficients(n, a), Word.zero(n), b) : Word(n)}:
431  %Equal.sym(Word(n), sa(n, low, P.coefficients(n, a), Word.zero(n), b), Word.xor(n, Word.zero(n), sm(n, low, P.coefficients(n, a), b)), sa_sm(n, low, P.coefficients(n, a), Word.zero(n), b)) : {P.reduce(n, low, P.mul(P.coefficients(n, a), P.coefficients(n, b))) == _ : Word(n)}
432  %Equal.sym(Word(n), Word.xor(n, Word.zero(n), sm(n, low, P.coefficients(n, a), b)), sm(n, low, P.coefficients(n, a), b), xor_zero_l(n, sm(n, low, P.coefficients(n, a), b))) : {P.reduce(n, low, P.mul(P.coefficients(n, a), P.coefficients(n, b))) == _ : Word(n)}
433  %red_coefficients(n, low, b) : {P.reduce(n, low, P.mul(P.coefficients(n, a), P.coefficients(n, b))) == sm(n, low, P.coefficients(n, a), _) : Word(n)}
434  red_mul(n, low, P.coefficients(n, a), P.coefficients(n, b))