def cb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gcm.bend:22

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T

22# The counter block nonce || [c]_32.
23def cb(q0: T.Quad, q1: T.Quad, q2: T.Quad, +c: U32) -> List<&2, U32>:
24  match q0 q1 q2:
25    case T.W{a0, a1, a2, a3} T.W{a4, a5, a6, a7} T.W{a8, a9, a10, a11}:
26      [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, U32.and(255, U32.shrn(c, 24n)), U32.and(255, U32.shrn(c, 16n)), U32.and(255, U32.shrn(c, 8n)), U32.and(255, c)]