AESKnownAnswerProof.envelope_equal: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend as AESKnownAnswerProof
Lines 33-59 of qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend&start_line=33&end_line=59

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 envelope_equal(+nonce: AES.Nonce, +ciphertext: List<&2, U32>,
    +tag: AES.Tag, +valid: {AES.bytes_valid(ciphertext) == True{} : Bool},
    +expected_ciphertext: List<&2, U32>, +expected_tag: AES.Tag,
    same_ciphertext: {ciphertext == expected_ciphertext : List<&2, U32>},
    same_tag: {tag == expected_tag : AES.Tag}) ->
    @+expected_valid: {AES.bytes_valid(expected_ciphertext) == True{} : Bool} ->
    {AES.Envelope{nonce, ciphertext, tag, valid} ==
     AES.Envelope{nonce, expected_ciphertext, expected_tag, expected_valid} :
        AES.Envelope}:
    %same_ciphertext :
        @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
        {AES.Envelope{nonce, ciphertext, tag, valid} ==
         AES.Envelope{nonce, _, expected_tag, expected_valid} : AES.Envelope}
    expected_valid =>
        Equal.trans(AES.Envelope,
            AES.Envelope{nonce, ciphertext, tag, valid},
            AES.Envelope{nonce, ciphertext, expected_tag, valid},
            AES.Envelope{nonce, ciphertext, expected_tag, expected_valid},
            Equal.cong(AES.Tag, AES.Envelope,
                value => AES.Envelope{nonce, ciphertext, value, valid},
                tag, expected_tag, same_tag),
            Equal.cong({AES.bytes_valid(ciphertext) == True{} : Bool},
                AES.Envelope,
                proof => AES.Envelope{nonce, ciphertext, expected_tag, proof},
                valid, expected_valid,
                Certificate.bool_unique(AES.bytes_valid(ciphertext), True{},
                    valid, expected_valid)))

Uses (10):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Envelope
  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=Tag
  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