def finish_auth
qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:208
import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as AESNistObservationProof
import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
208def finish_auth(+words: List<&2, U32>, +aad: List<&2, U32>, +envelope: AES.Envelope,
209 +tag: List<&2, U32>, +flag: Bool, +result: Result<&2, &2, AES.Error, List<&2, U32>>,
210 tag_matches: {envelope_tag_computed(words, aad, envelope) == tag : List<&2, U32>},
211 compare_matches: {auth_for_tag(envelope, tag) == flag : Bool},
212 branch_matches: {AES.decrypt_auth_result(words, envelope, flag) == result : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
213 {decrypt_expanded(words, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}:
214 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
215 decrypt_expanded(words, aad, envelope),
216 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))),
217 result, decrypt_auth_shape(words, aad, envelope),
218 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
219 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))),
220 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, tag)), result,
221 Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, actual_tag =>
222 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, actual_tag)),
223 envelope_tag_computed(words, aad, envelope), tag, tag_matches),
224 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
225 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, tag)),
226 AES.decrypt_auth_result(words, envelope, flag), result,
227 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, accepted => AES.decrypt_auth_result(words, envelope, accepted),
228 auth_for_tag(envelope, tag), flag, compare_matches), branch_matches)))