def tag_equal

qasim-bend-kit@0.1.0.2 · proof/AES_KnownAnswerProof.bend:7

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_CertificateProof.bend as Certificate

7def tag_equal(+bytes: List<&2, U32>,
8    +size: {List.length(&2, U32, bytes) == 16n : Nat},
9    +valid: {AES.bytes_valid(bytes) == True{} : Bool},
10    +expected: List<&2, U32>, same: {bytes == expected : List<&2, U32>}) ->
11    @+expected_size: {List.length(&2, U32, expected) == 16n : Nat} ->
12    @+expected_valid: {AES.bytes_valid(expected) == True{} : Bool} ->
13    {AES.Tag{bytes, size, valid} ==
14     AES.Tag{expected, expected_size, expected_valid} : AES.Tag}:
15    %same :
16        @+expected_size: {List.length(&2, U32, _) == 16n : Nat} ->
17        @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
18        {AES.Tag{bytes, size, valid} ==
19         AES.Tag{_, expected_size, expected_valid} : AES.Tag}
20    expected_size => expected_valid =>
21        Equal.trans(AES.Tag, AES.Tag{bytes, size, valid},
22            AES.Tag{bytes, expected_size, valid},
23            AES.Tag{bytes, expected_size, expected_valid},
24            Equal.cong({List.length(&2, U32, bytes) == 16n : Nat}, AES.Tag,
25                proof => AES.Tag{bytes, proof, valid}, size, expected_size,
26                Certificate.nat_unique(List.length(&2, U32, bytes), 16n,
27                    size, expected_size)),
28            Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Tag,
29                proof => AES.Tag{bytes, expected_size, proof}, valid,
30                expected_valid, Certificate.bool_unique(AES.bytes_valid(bytes),
31                    True{}, valid, expected_valid)))