def step_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash.bend:17

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/gf.bend as GF
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend as B

17# One bit of Algorithm 1: Z += c*V, V = V*x.
18def step_ok(+c: Bool, +z: I.Block, +v: I.Block, +rest: List<&2, Bool>) -> {D.F(I.Acc{z, v}, c <> rest) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}:
19  %B.zstep_ok(c, z, v) : {GF.sa(128n, G.low(), rest, _, P.times_x(128n, G.low(), D.R(v))) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}
20  %B.mulx_ok(v) : {GF.sa(128n, G.low(), rest, D.R(I.add_masked(D.bit(c), z, v)), _) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}
21  {==}