def from_ciphertext

qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:62

import Base
import qasim-bend-kit@0.1.0.2/LAWS.bend as L
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

62def from_ciphertext(+words: List<&2, U32>, +nonce: AES.Nonce,
63                    +aad: List<&2, U32>, +output: Core.GcmCiphertext) ->
64    {L.aes256gcm_nist_encrypt_observation(AES.encrypt_output_from_gcm(nonce,
65        Core.gcm_output_from_ciphertext(words, AES.raw_nonce_bytes(nonce), aad, output))) ==
66     parts(words, nonce, aad, ciphertext(output)) : List<&2, U32>}:
67    match nonce output:
68        case AES.Nonce{nonce_bytes, nonce_size, nonce_valid} Core.GcmCiphertext{bytes, valid}: {==}