def payload_parameters

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

import Base
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

156def payload_parameters(+words: List<&2, U32>, +envelope: AES.Envelope,
157    +nonce: List<&2, U32>, +bytes: List<&2, U32>, +plaintext: List<&2, U32>,
158    nonce_matches: {AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) == nonce : List<&2, U32>},
159    ciphertext_matches: {AES.ciphertext(envelope) == bytes : List<&2, U32>},
160    computed: {Core.gcm_decrypt_expanded(words, nonce, bytes) == plaintext : List<&2, U32>}) ->
161    {AES.decrypt_auth_result(words, envelope, True{}) == Done{plaintext} : Result<&2, &2, AES.Error, List<&2, U32>>}:
162    Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>, AES.decrypt_auth_result(words, envelope, True{}),
163        Done{Core.gcm_decrypt_expanded(words, AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), AES.ciphertext(envelope))},
164        Done{plaintext}, payload_shape(words, envelope),
165        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
166            Done{Core.gcm_decrypt_expanded(words, AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), AES.ciphertext(envelope))},
167            Done{Core.gcm_decrypt_expanded(words, nonce, AES.ciphertext(envelope))}, Done{plaintext},
168            Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, value => Done{Core.gcm_decrypt_expanded(words, value, AES.ciphertext(envelope))},
169                AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), nonce, nonce_matches),
170            Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>, Done{Core.gcm_decrypt_expanded(words, nonce, AES.ciphertext(envelope))},
171                Done{Core.gcm_decrypt_expanded(words, nonce, bytes)}, Done{plaintext},
172                Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, value => Done{Core.gcm_decrypt_expanded(words, nonce, value)},
173                    AES.ciphertext(envelope), bytes, ciphertext_matches),
174                Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, value => Done{value},
175                    Core.gcm_decrypt_expanded(words, nonce, bytes), plaintext, computed))))