def nonce_accepts

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

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

80def nonce_accepts(+bytes: List<&2, U32>,
81    +expected_size: {List.length(&2, U32, bytes) == 12n : Nat},
82    +expected_valid: {AES.bytes_valid(bytes) == True{} : Bool},
83    size: Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>,
84    valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
85    size_present: {Maybe.is_some(&0,
86        {List.length(&2, U32, bytes) == 12n : Nat}, size) == True{} : Bool},
87    valid_present: {Maybe.is_some(&0,
88        {AES.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool}) ->
89    {AES.nonce_from_proofs(bytes, size, valid) ==
90     Done{AES.Nonce{bytes, expected_size, expected_valid}} :
91        Result<&2, &2, AES.Error, AES.Nonce>}:
92    match size valid:
93        case None{} _:
94            Empty.absurd({AES.nonce_from_proofs(bytes, size, valid) ==
95                Done{AES.Nonce{bytes, expected_size, expected_valid}} :
96                Result<&2, &2, AES.Error, AES.Nonce>},
97                Logic.false_true(size_present))
98        case _ None{}:
99            Empty.absurd({AES.nonce_from_proofs(bytes, size, valid) ==
100                Done{AES.Nonce{bytes, expected_size, expected_valid}} :
101                Result<&2, &2, AES.Error, AES.Nonce>},
102                Logic.false_true(valid_present))
103        case Some{size_proof} Some{valid_proof}:
104            Equal.cong(AES.Nonce,
105                Result<&2, &2, AES.Error, AES.Nonce>, value => Done{value},
106                AES.Nonce{bytes, size_proof, valid_proof},
107                AES.Nonce{bytes, expected_size, expected_valid},
108                nonce_certificates(bytes, size_proof, valid_proof,
109                    expected_size, expected_valid))