Ghash.pack_ok: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend as Ghash
Lines 142-150 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend&start_line=142&end_line=150

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
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/aes.bend as S
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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend as B

# The hash subkey: the implementation packs E_K(0^128) into words.
def pack_ok(+st: T.State) -> {D.R(I.pack(st)) == G.block(S.bytes_of(st)) : Word(128n)}:
  match st:
    case T.S{T.W{a0, a1, a2, a3}, T.W{a4, a5, a6, a7}, T.W{a8, a9, a10, a11}, T.W{a12, a13, a14, a15}}:
      %Equal.sym(U32, I.word(T.W{a0, a1, a2, a3}), G.int32(a0, a1, a2, a3), B.word_ok(a0, a1, a2, a3)) : {D.R(I.B{_, I.word(T.W{a4, a5, a6, a7}), I.word(T.W{a8, a9, a10, a11}), I.word(T.W{a12, a13, a14, a15})}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}
      %Equal.sym(U32, I.word(T.W{a4, a5, a6, a7}), G.int32(a4, a5, a6, a7), B.word_ok(a4, a5, a6, a7)) : {D.R(I.B{G.int32(a0, a1, a2, a3), _, I.word(T.W{a8, a9, a10, a11}), I.word(T.W{a12, a13, a14, a15})}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}
      %Equal.sym(U32, I.word(T.W{a8, a9, a10, a11}), G.int32(a8, a9, a10, a11), B.word_ok(a8, a9, a10, a11)) : {D.R(I.B{G.int32(a0, a1, a2, a3), G.int32(a4, a5, a6, a7), _, I.word(T.W{a12, a13, a14, a15})}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}
      %Equal.sym(U32, I.word(T.W{a12, a13, a14, a15}), G.int32(a12, a13, a14, a15), B.word_ok(a12, a13, a14, a15)) : {D.R(I.B{G.int32(a0, a1, a2, a3), G.int32(a4, a5, a6, a7), G.int32(a8, a9, a10, a11), _}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}
      B.pack_int(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend&name=pack_int
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend&name=word_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend&name=R
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=bytes_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=int32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=Block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend&name=Quad
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend&name=State