AESConstructorProof.nonce_accepts: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend as AESConstructorProof
Lines 80-109 of qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend&start_line=80&end_line=109

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

def nonce_accepts(+bytes: List<&2, U32>,
    +expected_size: {List.length(&2, U32, bytes) == 12n : Nat},
    +expected_valid: {AES.bytes_valid(bytes) == True{} : Bool},
    size: Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>,
    valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
    size_present: {Maybe.is_some(&0,
        {List.length(&2, U32, bytes) == 12n : Nat}, size) == True{} : Bool},
    valid_present: {Maybe.is_some(&0,
        {AES.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool}) ->
    {AES.nonce_from_proofs(bytes, size, valid) ==
     Done{AES.Nonce{bytes, expected_size, expected_valid}} :
        Result<&2, &2, AES.Error, AES.Nonce>}:
    match size valid:
        case None{} _:
            Empty.absurd({AES.nonce_from_proofs(bytes, size, valid) ==
                Done{AES.Nonce{bytes, expected_size, expected_valid}} :
                Result<&2, &2, AES.Error, AES.Nonce>},
                Logic.false_true(size_present))
        case _ None{}:
            Empty.absurd({AES.nonce_from_proofs(bytes, size, valid) ==
                Done{AES.Nonce{bytes, expected_size, expected_valid}} :
                Result<&2, &2, AES.Error, AES.Nonce>},
                Logic.false_true(valid_present))
        case Some{size_proof} Some{valid_proof}:
            Equal.cong(AES.Nonce,
                Result<&2, &2, AES.Error, AES.Nonce>, value => Done{value},
                AES.Nonce{bytes, size_proof, valid_proof},
                AES.Nonce{bytes, expected_size, expected_valid},
                nonce_certificates(bytes, size_proof, valid_proof,
                    expected_size, expected_valid))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.is_some
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=nonce_from_proofs
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend&name=nonce_certificates
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend&name=false_true