def rejects_comparison

qasim-bend-kit@0.1.0.2 · proof/AES_TagRejectProof.bend:6

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/proof/AES_TagCompareProof.bend as Compare

6def rejects_comparison(+words: List<&2, U32>,
7    +envelope: AES.Envelope, +supplied: List<&2, U32>,
8    +expected: List<&2, U32>,
9    changed: {supplied != expected : List<&2, U32>}) ->
10    {AES.decrypt_auth_result(words, envelope,
11        AES.bytes_equal_full_scan(supplied, expected)) ==
12     Fail{AES.AuthenticationFailed{}} :
13        Result<&2, &2, AES.Error, List<&2, U32>>}:
14    Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>,
15        authenticated => AES.decrypt_auth_result(words, envelope,
16            authenticated),
17        AES.bytes_equal_full_scan(supplied, expected), False{},
18        Compare.unequal_is_false(supplied, expected, changed))