GhashDefs.steps: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as GhashDefs
Lines 25-31 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend&start_line=25&end_line=31

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as I

# The implementation's steps over a list of coefficients.
def steps(cs: List<&2, Bool>, acc: I.Acc) -> I.Acc:
  match cs:
    case Nil{}:
      acc
    case c <> r:
      steps(r, I.step(bit(c), acc))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend&name=bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=Acc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=step