def key_accepts

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

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_StringEqProof.bend as Logic

28def key_accepts(+bytes: List<&2, U32>,
29    +expected_size: {List.length(&2, U32, bytes) == 32n : Nat},
30    +expected_valid: {AES.bytes_valid(bytes) == True{} : Bool},
31    size: Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}>,
32    valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
33    size_present: {Maybe.is_some(&0,
34        {List.length(&2, U32, bytes) == 32n : Nat}, size) == True{} : Bool},
35    valid_present: {Maybe.is_some(&0,
36        {AES.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool}) ->
37    {AES.key_from_proofs(bytes, size, valid) ==
38     Done{AES.SecretKey{bytes, expected_size, expected_valid}} :
39        Result<&2, &2, AES.Error, AES.SecretKey>}:
40    match size valid:
41        case None{} _:
42            Empty.absurd({AES.key_from_proofs(bytes, size, valid) ==
43                Done{AES.SecretKey{bytes, expected_size, expected_valid}} :
44                Result<&2, &2, AES.Error, AES.SecretKey>},
45                Logic.false_true(size_present))
46        case _ None{}:
47            Empty.absurd({AES.key_from_proofs(bytes, size, valid) ==
48                Done{AES.SecretKey{bytes, expected_size, expected_valid}} :
49                Result<&2, &2, AES.Error, AES.SecretKey>},
50                Logic.false_true(valid_present))
51        case Some{size_proof} Some{valid_proof}:
52            Equal.cong(AES.SecretKey,
53                Result<&2, &2, AES.Error, AES.SecretKey>, value => Done{value},
54                AES.SecretKey{bytes, size_proof, valid_proof},
55                AES.SecretKey{bytes, expected_size, expected_valid},
56                key_certificates(bytes, size_proof, valid_proof,
57                    expected_size, expected_valid))