AESConstructorProof.nonce_equal: 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 111-135 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=111&end_line=135

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

def nonce_equal(+bytes: List<&2, U32>,
    +size: {List.length(&2, U32, bytes) == 12n : Nat},
    +valid: {AES.bytes_valid(bytes) == True{} : Bool},
    +expected: List<&2, U32>, same: {bytes == expected : List<&2, U32>}) ->
    @+expected_size: {List.length(&2, U32, expected) == 12n : Nat} ->
    @+expected_valid: {AES.bytes_valid(expected) == True{} : Bool} ->
    {AES.Nonce{bytes, size, valid} ==
     AES.Nonce{expected, expected_size, expected_valid} : AES.Nonce}:
    %same :
        @+expected_size: {List.length(&2, U32, _) == 12n : Nat} ->
        @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
        {AES.Nonce{bytes, size, valid} ==
         AES.Nonce{_, expected_size, expected_valid} : AES.Nonce}
    expected_size => expected_valid =>
        Equal.trans(AES.Nonce, AES.Nonce{bytes, size, valid},
            AES.Nonce{bytes, expected_size, valid},
            AES.Nonce{bytes, expected_size, expected_valid},
            Equal.cong({List.length(&2, U32, bytes) == 12n : Nat}, AES.Nonce,
                proof => AES.Nonce{bytes, proof, valid}, size, expected_size,
                Certificate.nat_unique(List.length(&2, U32, bytes), 12n,
                    size, expected_size)),
            Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Nonce,
                proof => AES.Nonce{bytes, expected_size, proof}, valid,
                expected_valid, Certificate.bool_unique(AES.bytes_valid(bytes),
                    True{}, valid, expected_valid)))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Nat
  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=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/proof/AES_CertificateProof.bend&name=bool_unique
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_unique