Ghash.ghash_all_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 128-140 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=128&end_line=140

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/gcm.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D

# GHASH_H(A || 0^v || C || 0^u || [len(A)]_64 || [len(C)]_64).
def ghash_all_ok(+h: I.Block, +aad: List<&2, U32>, +c: List<&2, U32>) -> {G.ghash(D.R(h), List.append(&2, U32, G.pad(aad), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c)))), Word.zero(128n)) == D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))) : Word(128n)}:
  Equal.trans(Word(128n),
    G.ghash(D.R(h), List.append(&2, U32, G.pad(aad), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c)))), D.R(I.zero())),
    G.ghash(D.R(h), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), D.R(I.ghash(h, aad, I.zero()))),
    D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))),
    ghash_ok(h, aad, List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), I.zero()),
    Equal.trans(Word(128n),
      G.ghash(D.R(h), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), D.R(I.ghash(h, aad, I.zero()))),
      G.ghash(D.R(h), List.append(&2, U32, G.len64(aad), G.len64(c)), D.R(I.ghash(h, c, I.ghash(h, aad, I.zero())))),
      D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))),
      ghash_ok(h, c, List.append(&2, U32, G.len64(aad), G.len64(c)), I.ghash(h, aad, I.zero())),
      ghash_ok(h, I.lengths(aad, c), Nil{}, I.ghash(h, c, I.ghash(h, aad, I.zero())))))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend&name=ghash_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/gcm.bend&name=ghash
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=len64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=pad
  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=ghash
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=lengths
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=zero