def mulx_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash_bits.bend:90

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D

90# V * x: the shift toward x^127 with the reduction by R.
91def mulx_ok(+v: I.Block) -> {D.R(I.mulx(v)) == P.times_x(128n, G.low(), D.R(v)) : Word(128n)}:
92  match v:
93    case I.B{U32{WCon{x0, xt}}, U32{WCon{y0, yt}}, U32{WCon{z0, zt}}, U32{WCon{u0, ut}}}:
94      mulx_w(x0, y0, z0, u0, xt, yt, zt, ut)