def block_bytes
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as Gcmimport Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P
51def block_bytes(w: Word(128n)) -> List<&2, U32>:
52 bits_bytes(P.coefficients(128n, w))
Uses (5)
Used by (5)
- bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm:tag
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead:hb
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm:tag_ok
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead:bb16
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits:bb_ok