def nonce_certificates

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

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

58def nonce_certificates(+bytes: List<&2, U32>,
59    +first_size: {List.length(&2, U32, bytes) == 12n : Nat},
60    +first_valid: {AES.bytes_valid(bytes) == True{} : Bool},
61    +second_size: {List.length(&2, U32, bytes) == 12n : Nat},
62    +second_valid: {AES.bytes_valid(bytes) == True{} : Bool}) ->
63    {AES.Nonce{bytes, first_size, first_valid} ==
64     AES.Nonce{bytes, second_size, second_valid} : AES.Nonce}:
65    Equal.trans(AES.Nonce,
66        AES.Nonce{bytes, first_size, first_valid},
67        AES.Nonce{bytes, second_size, first_valid},
68        AES.Nonce{bytes, second_size, second_valid},
69        Equal.cong({List.length(&2, U32, bytes) == 12n : Nat}, AES.Nonce,
70            proof => AES.Nonce{bytes, proof, first_valid},
71            first_size, second_size,
72            Certificate.nat_unique(List.length(&2, U32, bytes), 12n,
73                first_size, second_size)),
74        Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Nonce,
75            proof => AES.Nonce{bytes, second_size, proof},
76            first_valid, second_valid,
77            Certificate.bool_unique(AES.bytes_valid(bytes), True{},
78                first_valid, second_valid)))