AESEnvelopeProof.aes_parse_decoded_masked_map: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
Lines 582-660 of qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&start_line=582&end_line=660

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

def aes_parse_decoded_masked_map(+nonce: List<&2, U32>, +tag: List<&2, U32>,
    +ciphertext: List<&2, U32>,
    nonce_size: {List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat},
    tag_size: {List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat},
    nonce_valid: {AES.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool},
    tag_valid: {AES.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool},
    ciphertext_valid: {AES.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool}) ->
    {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
        AES.parse_decoded(aes_hex_mask_bytes(nonce), aes_hex_mask_bytes(tag),
            aes_hex_mask_bytes(ciphertext),
            Some{nonce_size}, Some{tag_size}, Some{nonce_valid},
            Some{tag_valid}, Some{ciphertext_valid})) ==
     Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++ "." ++
        AES.hex_bytes(ciphertext)} : Result<&2, &2, AES.Error, String>}:
    +masked_nonce = aes_hex_mask_bytes(nonce)
    +masked_tag = aes_hex_mask_bytes(tag)
    +masked_ciphertext = aes_hex_mask_bytes(ciphertext)
    encoded_fixed = "v1." ++
        AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
        AES.hex_bytes(AES.fixed_bytes(16n, masked_tag)) ++ "." ++
        AES.hex_bytes(masked_ciphertext)
    encoded_masked = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
        AES.hex_bytes(masked_tag) ++ "." ++ AES.hex_bytes(masked_ciphertext)
    encoded_raw = "v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
        "." ++ AES.hex_bytes(ciphertext)
    cipher_equal = aes_hex_bytes_mask_idempotent(ciphertext)
    tag_equal = aes_hex_bytes_mask_idempotent(tag)
    nonce_equal = aes_hex_bytes_mask_idempotent(nonce)
    cipher_path = Equal.cong(String, String,
        last => ("v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
            AES.hex_bytes(masked_tag) ++ "." ++ last),
        AES.hex_bytes(masked_ciphertext), AES.hex_bytes(ciphertext), cipher_equal)
    tag_path = Equal.cong(String, String,
        value => ("v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++ value ++
            "." ++ AES.hex_bytes(ciphertext)),
        AES.hex_bytes(masked_tag), AES.hex_bytes(tag), tag_equal)
    nonce_path = Equal.cong(String, String,
        value => ("v1." ++ value ++ "." ++ AES.hex_bytes(tag) ++ "." ++
            AES.hex_bytes(ciphertext)),
        AES.hex_bytes(masked_nonce), AES.hex_bytes(nonce), nonce_equal)
    cipher_intermediate = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
        AES.hex_bytes(masked_tag) ++ "." ++ AES.hex_bytes(ciphertext)
    tag_intermediate = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
        AES.hex_bytes(tag) ++ "." ++ AES.hex_bytes(ciphertext)
    cipher_tag_path = Equal.trans(String, encoded_masked,
        cipher_intermediate, tag_intermediate, cipher_path, tag_path)
    encode_fields_equal = Equal.trans(String, encoded_masked,
        tag_intermediate, encoded_raw, cipher_tag_path, nonce_path)
    fixed_nonce_equal = Equal.cong(List<&2, U32>, String,
        xs => AES.hex_bytes(xs),
        AES.fixed_bytes(12n, masked_nonce), masked_nonce,
        aes_fixed_bytes_identity(12n, masked_nonce, nonce_size))
    fixed_tag_equal = Equal.cong(List<&2, U32>, String,
        xs => AES.hex_bytes(xs),
        AES.fixed_bytes(16n, masked_tag), masked_tag,
        aes_fixed_bytes_identity(16n, masked_tag, tag_size))
    fixed_tag_intermediate = "v1." ++
        AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
        AES.hex_bytes(masked_tag) ++ "." ++
        AES.hex_bytes(masked_ciphertext)
    fixed_tag_path = Equal.cong(String, String,
        value => "v1." ++
            AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
            value ++ "." ++ AES.hex_bytes(masked_ciphertext),
        AES.hex_bytes(AES.fixed_bytes(16n, masked_tag)),
        AES.hex_bytes(masked_tag), fixed_tag_equal)
    fixed_nonce_path = Equal.cong(String, String,
        value => "v1." ++ value ++ "." ++ AES.hex_bytes(masked_tag) ++
            "." ++ AES.hex_bytes(masked_ciphertext),
        AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)),
        AES.hex_bytes(masked_nonce), fixed_nonce_equal)
    fixed_to_masked = Equal.trans(String, encoded_fixed,
        fixed_tag_intermediate, encoded_masked,
        fixed_tag_path, fixed_nonce_path)
    fixed_to_raw = Equal.trans(String, encoded_fixed,
        encoded_masked, encoded_raw,
        fixed_to_masked, encode_fields_equal)
    Equal.cong(String, Result<&2, &2, AES.Error, String>,
        text => Done{text}, encoded_fixed, encoded_raw, fixed_to_raw)

Uses (22):
  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=Maybe
  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=Result.map
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  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=Error
  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=encode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=fixed_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=hex_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=parse_decoded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_fixed_bytes_identity
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_bytes_mask_idempotent
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_mask_bytes