def key_certificates

qasim-bend-kit@0.1.0.2 · proof/AES_ConstructorProof.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_CertificateProof.bend as Certificate

6def key_certificates(+bytes: List<&2, U32>,
7    +first_size: {List.length(&2, U32, bytes) == 32n : Nat},
8    +first_valid: {AES.bytes_valid(bytes) == True{} : Bool},
9    +second_size: {List.length(&2, U32, bytes) == 32n : Nat},
10    +second_valid: {AES.bytes_valid(bytes) == True{} : Bool}) ->
11    {AES.SecretKey{bytes, first_size, first_valid} ==
12     AES.SecretKey{bytes, second_size, second_valid} : AES.SecretKey}:
13    Equal.trans(AES.SecretKey,
14        AES.SecretKey{bytes, first_size, first_valid},
15        AES.SecretKey{bytes, second_size, first_valid},
16        AES.SecretKey{bytes, second_size, second_valid},
17        Equal.cong({List.length(&2, U32, bytes) == 32n : Nat}, AES.SecretKey,
18            proof => AES.SecretKey{bytes, proof, first_valid},
19            first_size, second_size,
20            Certificate.nat_unique(List.length(&2, U32, bytes), 32n,
21                first_size, second_size)),
22        Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.SecretKey,
23            proof => AES.SecretKey{bytes, second_size, proof},
24            first_valid, second_valid,
25            Certificate.bool_unique(AES.bytes_valid(bytes), True{},
26                first_valid, second_valid)))