def nonce_equal

qasim-bend-kit@0.1.0.2 · proof/AES_ConstructorProof.bend:111

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

111def nonce_equal(+bytes: List<&2, U32>,
112    +size: {List.length(&2, U32, bytes) == 12n : Nat},
113    +valid: {AES.bytes_valid(bytes) == True{} : Bool},
114    +expected: List<&2, U32>, same: {bytes == expected : List<&2, U32>}) ->
115    @+expected_size: {List.length(&2, U32, expected) == 12n : Nat} ->
116    @+expected_valid: {AES.bytes_valid(expected) == True{} : Bool} ->
117    {AES.Nonce{bytes, size, valid} ==
118     AES.Nonce{expected, expected_size, expected_valid} : AES.Nonce}:
119    %same :
120        @+expected_size: {List.length(&2, U32, _) == 12n : Nat} ->
121        @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
122        {AES.Nonce{bytes, size, valid} ==
123         AES.Nonce{_, expected_size, expected_valid} : AES.Nonce}
124    expected_size => expected_valid =>
125        Equal.trans(AES.Nonce, AES.Nonce{bytes, size, valid},
126            AES.Nonce{bytes, expected_size, valid},
127            AES.Nonce{bytes, expected_size, expected_valid},
128            Equal.cong({List.length(&2, U32, bytes) == 12n : Nat}, AES.Nonce,
129                proof => AES.Nonce{bytes, proof, valid}, size, expected_size,
130                Certificate.nat_unique(List.length(&2, U32, bytes), 12n,
131                    size, expected_size)),
132            Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Nonce,
133                proof => AES.Nonce{bytes, expected_size, proof}, valid,
134                expected_valid, Certificate.bool_unique(AES.bytes_valid(bytes),
135                    True{}, valid, expected_valid)))