def open128

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/laws.bend:24

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

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