Api.open128: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/api.bend as Api
Lines 23-29 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/api.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/api.bend&start_line=23&end_line=29

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aesgcm.bend as GCM

# Decrypt what an encryption returned (None stays None).
def open128(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
  match m:
    case None{}:
      None{}
    case Some{ct}:
      GCM.aes128_gcm_decrypt(key, nonce, aad, ct)

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aesgcm.bend&name=aes128_gcm_decrypt