(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module extension.
  Module confidential_transfer.
    Module split_proof_generation.
      (*
      pub fn transfer_split_proof_data(
          current_available_balance: &ElGamalCiphertext,
          current_decryptable_available_balance: &AeCiphertext,
          transfer_amount: u64,
          source_elgamal_keypair: &ElGamalKeypair,
          aes_key: &AeKey,
          destination_elgamal_pubkey: &ElGamalPubkey,
          auditor_elgamal_pubkey: Option<&ElGamalPubkey>,
      ) -> Result<
          (
              CiphertextCommitmentEqualityProofData,
              BatchedGroupedCiphertext2HandlesValidityProofData,
              BatchedRangeProofU128Data,
              SourceDecryptHandles,
          ),
          TokenError,
      > {
          let default_auditor_pubkey = ElGamalPubkey::default();
          let auditor_elgamal_pubkey = auditor_elgamal_pubkey.unwrap_or(&default_auditor_pubkey);
      
          // Split the transfer amount into the low and high bit components.
          let (transfer_amount_lo, transfer_amount_hi) =
              verify_and_split_deposit_amount(transfer_amount)?;
      
          // Encrypt the `lo` and `hi` transfer amounts.
          let (transfer_amount_grouped_ciphertext_lo, transfer_amount_opening_lo) =
              TransferAmountCiphertext::new(
                  transfer_amount_lo,
                  source_elgamal_keypair.pubkey(),
                  destination_elgamal_pubkey,
                  auditor_elgamal_pubkey,
              );
      
          let (transfer_amount_grouped_ciphertext_hi, transfer_amount_opening_hi) =
              TransferAmountCiphertext::new(
                  transfer_amount_hi,
                  source_elgamal_keypair.pubkey(),
                  destination_elgamal_pubkey,
                  auditor_elgamal_pubkey,
              );
      
          // Decrypt the current available balance at the source
          let current_decrypted_available_balance = current_decryptable_available_balance
              .decrypt(aes_key)
              .ok_or(TokenError::AccountDecryption)?;
      
          // Compute the remaining balance at the source
          let new_decrypted_available_balance = current_decrypted_available_balance
              .checked_sub(transfer_amount)
              .ok_or(TokenError::InsufficientFunds)?;
      
          // Create a new Pedersen commitment for the remaining balance at the source
          let (new_available_balance_commitment, new_source_opening) =
              Pedersen::new(new_decrypted_available_balance);
      
          // Compute the remaining balance at the source as ElGamal ciphertexts
          let transfer_amount_source_ciphertext_lo =
              transfer_amount_source_ciphertext(&transfer_amount_grouped_ciphertext_lo.into());
          let transfer_amount_source_ciphertext_hi =
              transfer_amount_source_ciphertext(&transfer_amount_grouped_ciphertext_hi.into());
      
          let current_available_balance = ( *current_available_balance).into();
          let new_available_balance_ciphertext = subtract_with_lo_hi(
              &current_available_balance,
              &transfer_amount_source_ciphertext_lo,
              &transfer_amount_source_ciphertext_hi,
          )
          .ok_or(TokenError::CiphertextArithmeticFailed)?;
          let new_available_balance_ciphertext: ElGamalCiphertext = new_available_balance_ciphertext
              .try_into()
              .map_err(|_| TokenError::MalformedCiphertext)?;
      
          // generate equality proof data
          let equality_proof_data = CiphertextCommitmentEqualityProofData::new(
              source_elgamal_keypair,
              &new_available_balance_ciphertext,
              &new_available_balance_commitment,
              &new_source_opening,
              new_decrypted_available_balance,
          )
          .map_err(|_| TokenError::ProofGeneration)?;
      
          // create source decrypt handle
          let source_decrypt_handle_lo =
              DecryptHandle::new(source_elgamal_keypair.pubkey(), &transfer_amount_opening_lo);
          let source_decrypt_handle_hi =
              DecryptHandle::new(source_elgamal_keypair.pubkey(), &transfer_amount_opening_hi);
      
          let source_decrypt_handles = SourceDecryptHandles {
              lo: source_decrypt_handle_lo.into(),
              hi: source_decrypt_handle_hi.into(),
          };
      
          // encrypt the transfer amount under the destination and auditor ElGamal public
          // key
          let transfer_amount_destination_auditor_ciphertext_lo = GroupedElGamal::encrypt_with(
              [destination_elgamal_pubkey, auditor_elgamal_pubkey],
              transfer_amount_lo,
              &transfer_amount_opening_lo,
          );
          let transfer_amount_destination_auditor_ciphertext_hi = GroupedElGamal::encrypt_with(
              [destination_elgamal_pubkey, auditor_elgamal_pubkey],
              transfer_amount_hi,
              &transfer_amount_opening_hi,
          );
      
          // generate ciphertext validity data
          let ciphertext_validity_proof_data = BatchedGroupedCiphertext2HandlesValidityProofData::new(
              destination_elgamal_pubkey,
              auditor_elgamal_pubkey,
              &transfer_amount_destination_auditor_ciphertext_lo,
              &transfer_amount_destination_auditor_ciphertext_hi,
              transfer_amount_lo,
              transfer_amount_hi,
              &transfer_amount_opening_lo,
              &transfer_amount_opening_hi,
          )
          .map_err(|_| TokenError::ProofGeneration)?;
      
          // generate range proof data
          const REMAINING_BALANCE_BIT_LENGTH: usize = 64;
          const TRANSFER_AMOUNT_LO_BIT_LENGTH: usize = 16;
          const TRANSFER_AMOUNT_HI_BIT_LENGTH: usize = 32;
          const PADDING_BIT_LENGTH: usize = 16;
      
          let (padding_commitment, padding_opening) = Pedersen::new(0_u64);
      
          let range_proof_data = BatchedRangeProofU128Data::new(
              vec![
                  &new_available_balance_commitment,
                  transfer_amount_grouped_ciphertext_lo.get_commitment(),
                  transfer_amount_grouped_ciphertext_hi.get_commitment(),
                  &padding_commitment,
              ],
              vec![
                  new_decrypted_available_balance,
                  transfer_amount_lo,
                  transfer_amount_hi,
                  0,
              ],
              vec![
                  REMAINING_BALANCE_BIT_LENGTH,
                  TRANSFER_AMOUNT_LO_BIT_LENGTH,
                  TRANSFER_AMOUNT_HI_BIT_LENGTH,
                  PADDING_BIT_LENGTH,
              ],
              vec![
                  &new_source_opening,
                  &transfer_amount_opening_lo,
                  &transfer_amount_opening_hi,
                  &padding_opening,
              ],
          )
          .map_err(|_| TokenError::ProofGeneration)?;
      
          Ok((
              equality_proof_data,
              ciphertext_validity_proof_data,
              range_proof_data,
              source_decrypt_handles,
          ))
      }
      *)
      Definition transfer_split_proof_data (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [],
            [
              current_available_balance;
              current_decryptable_available_balance;
              transfer_amount;
              source_elgamal_keypair;
              aes_key;
              destination_elgamal_pubkey;
              auditor_elgamal_pubkey
            ] =>
          ltac:(M.monadic
            (let current_available_balance := M.alloc (| current_available_balance |) in
            let current_decryptable_available_balance :=
              M.alloc (| current_decryptable_available_balance |) in
            let transfer_amount := M.alloc (| transfer_amount |) in
            let source_elgamal_keypair := M.alloc (| source_elgamal_keypair |) in
            let aes_key := M.alloc (| aes_key |) in
            let destination_elgamal_pubkey := M.alloc (| destination_elgamal_pubkey |) in
            let auditor_elgamal_pubkey := M.alloc (| auditor_elgamal_pubkey |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let default_auditor_pubkey :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::default::Default",
                          Ty.path "solana_zk_token_sdk::encryption::elgamal::ElGamalPubkey",
                          [],
                          "default",
                          []
                        |),
                        []
                      |)
                    |) in
                  let auditor_elgamal_pubkey :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            [
                              Ty.apply
                                (Ty.path "&")
                                [ Ty.path "solana_zk_token_sdk::encryption::elgamal::ElGamalPubkey"
                                ]
                            ],
                          "unwrap_or",
                          []
                        |),
                        [ M.read (| auditor_elgamal_pubkey |); default_auditor_pubkey ]
                      |)
                    |) in
                  M.match_operator (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              [
                                Ty.tuple [ Ty.path "u64"; Ty.path "u64" ];
                                Ty.path "spl_token_2022::error::TokenError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_function (|
                                "spl_token_2022::extension::confidential_transfer::processor::verify_and_split_deposit_amount",
                                []
                              |),
                              [ M.read (| transfer_amount |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          [
                                            Ty.tuple
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                Ty.path
                                                  "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                              ];
                                            Ty.path "spl_token_2022::error::TokenError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "spl_token_2022::error::TokenError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let transfer_amount_lo := M.copy (| γ0_0 |) in
                          let transfer_amount_hi := M.copy (| γ0_1 |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path
                                    "solana_zk_token_sdk::instruction::transfer::encryption::TransferAmountCiphertext",
                                  "new",
                                  []
                                |),
                                [
                                  M.read (| transfer_amount_lo |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path
                                        "solana_zk_token_sdk::encryption::elgamal::ElGamalKeypair",
                                      "pubkey",
                                      []
                                    |),
                                    [ M.read (| source_elgamal_keypair |) ]
                                  |);
                                  M.read (| destination_elgamal_pubkey |);
                                  M.read (| auditor_elgamal_pubkey |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let transfer_amount_grouped_ciphertext_lo := M.copy (| γ0_0 |) in
                                  let transfer_amount_opening_lo := M.copy (| γ0_1 |) in
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path
                                            "solana_zk_token_sdk::instruction::transfer::encryption::TransferAmountCiphertext",
                                          "new",
                                          []
                                        |),
                                        [
                                          M.read (| transfer_amount_hi |);
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalKeypair",
                                              "pubkey",
                                              []
                                            |),
                                            [ M.read (| source_elgamal_keypair |) ]
                                          |);
                                          M.read (| destination_elgamal_pubkey |);
                                          M.read (| auditor_elgamal_pubkey |)
                                        ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                          let transfer_amount_grouped_ciphertext_hi :=
                                            M.copy (| γ0_0 |) in
                                          let transfer_amount_opening_hi := M.copy (| γ0_1 |) in
                                          let current_decrypted_available_balance :=
                                            M.copy (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        [
                                                          Ty.path "u64";
                                                          Ty.path
                                                            "spl_token_2022::error::TokenError"
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            [ Ty.path "u64" ],
                                                          "ok_or",
                                                          [
                                                            Ty.path
                                                              "spl_token_2022::error::TokenError"
                                                          ]
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext",
                                                              "decrypt",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                current_decryptable_available_balance
                                                              |);
                                                              M.read (| aes_key |)
                                                            ]
                                                          |);
                                                          Value.StructTuple
                                                            "spl_token_2022::error::TokenError::AccountDecryption"
                                                            []
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Break",
                                                          0
                                                        |) in
                                                      let residual := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::FromResidual",
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.path
                                                                            "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                          Ty.path
                                                                            "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                          Ty.path
                                                                            "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                          Ty.path
                                                                            "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                                        ];
                                                                      Ty.path
                                                                        "spl_token_2022::error::TokenError"
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::result::Result")
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible";
                                                                        Ty.path
                                                                          "spl_token_2022::error::TokenError"
                                                                      ]
                                                                  ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |)
                                            |) in
                                          let new_decrypted_available_balance :=
                                            M.copy (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        [
                                                          Ty.path "u64";
                                                          Ty.path
                                                            "spl_token_2022::error::TokenError"
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            [ Ty.path "u64" ],
                                                          "ok_or",
                                                          [
                                                            Ty.path
                                                              "spl_token_2022::error::TokenError"
                                                          ]
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "u64",
                                                              "checked_sub",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                current_decrypted_available_balance
                                                              |);
                                                              M.read (| transfer_amount |)
                                                            ]
                                                          |);
                                                          Value.StructTuple
                                                            "spl_token_2022::error::TokenError::InsufficientFunds"
                                                            []
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Break",
                                                          0
                                                        |) in
                                                      let residual := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::FromResidual",
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.path
                                                                            "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                          Ty.path
                                                                            "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                          Ty.path
                                                                            "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                          Ty.path
                                                                            "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                                        ];
                                                                      Ty.path
                                                                        "spl_token_2022::error::TokenError"
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::result::Result")
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible";
                                                                        Ty.path
                                                                          "spl_token_2022::error::TokenError"
                                                                      ]
                                                                  ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |)
                                            |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "solana_zk_token_sdk::encryption::pedersen::Pedersen",
                                                  "new",
                                                  [ Ty.path "u64" ]
                                                |),
                                                [ M.read (| new_decrypted_available_balance |) ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_tuple_field (| γ, 0 |) in
                                                  let γ0_1 :=
                                                    M.SubPointer.get_tuple_field (| γ, 1 |) in
                                                  let new_available_balance_commitment :=
                                                    M.copy (| γ0_0 |) in
                                                  let new_source_opening := M.copy (| γ0_1 |) in
                                                  let transfer_amount_source_ciphertext_lo :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::transfer_amount_source_ciphertext",
                                                          []
                                                        |),
                                                        [
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::convert::Into",
                                                                Ty.path
                                                                  "solana_zk_token_sdk::instruction::transfer::encryption::TransferAmountCiphertext",
                                                                [
                                                                  Ty.path
                                                                    "solana_zk_token_sdk::zk_token_elgamal::pod::instruction::TransferAmountCiphertext"
                                                                ],
                                                                "into",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  transfer_amount_grouped_ciphertext_lo
                                                                |)
                                                              ]
                                                            |)
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let transfer_amount_source_ciphertext_hi :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::transfer_amount_source_ciphertext",
                                                          []
                                                        |),
                                                        [
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::convert::Into",
                                                                Ty.path
                                                                  "solana_zk_token_sdk::instruction::transfer::encryption::TransferAmountCiphertext",
                                                                [
                                                                  Ty.path
                                                                    "solana_zk_token_sdk::zk_token_elgamal::pod::instruction::TransferAmountCiphertext"
                                                                ],
                                                                "into",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  transfer_amount_grouped_ciphertext_hi
                                                                |)
                                                              ]
                                                            |)
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let current_available_balance :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::convert::Into",
                                                          Ty.path
                                                            "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext",
                                                          [
                                                            Ty.path
                                                              "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext"
                                                          ],
                                                          "into",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.read (| current_available_balance |)
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let new_available_balance_ciphertext :=
                                                    M.copy (|
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::Try",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                [
                                                                  Ty.path
                                                                    "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext";
                                                                  Ty.path
                                                                    "spl_token_2022::error::TokenError"
                                                                ],
                                                              [],
                                                              "branch",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "core::option::Option")
                                                                    [
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext"
                                                                    ],
                                                                  "ok_or",
                                                                  [
                                                                    Ty.path
                                                                      "spl_token_2022::error::TokenError"
                                                                  ]
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "solana_zk_token_sdk::zk_token_elgamal::ops::subtract_with_lo_hi",
                                                                      []
                                                                    |),
                                                                    [
                                                                      current_available_balance;
                                                                      transfer_amount_source_ciphertext_lo;
                                                                      transfer_amount_source_ciphertext_hi
                                                                    ]
                                                                  |);
                                                                  Value.StructTuple
                                                                    "spl_token_2022::error::TokenError::CiphertextArithmeticFailed"
                                                                    []
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Break",
                                                                  0
                                                                |) in
                                                              let residual := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::try_trait::FromResidual",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            [
                                                                              Ty.tuple
                                                                                [
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                                  Ty.path
                                                                                    "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                                                ];
                                                                              Ty.path
                                                                                "spl_token_2022::error::TokenError"
                                                                            ],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              [
                                                                                Ty.path
                                                                                  "core::convert::Infallible";
                                                                                Ty.path
                                                                                  "spl_token_2022::error::TokenError"
                                                                              ]
                                                                          ],
                                                                          "from_residual",
                                                                          []
                                                                        |),
                                                                        [ M.read (| residual |) ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                                  0
                                                                |) in
                                                              let val := M.copy (| γ0_0 |) in
                                                              val))
                                                        ]
                                                      |)
                                                    |) in
                                                  let new_available_balance_ciphertext :=
                                                    M.copy (|
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::Try",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                [
                                                                  Ty.path
                                                                    "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                                                  Ty.path
                                                                    "spl_token_2022::error::TokenError"
                                                                ],
                                                              [],
                                                              "branch",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    [
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                                                    ],
                                                                  "map_err",
                                                                  [
                                                                    Ty.path
                                                                      "spl_token_2022::error::TokenError";
                                                                    Ty.function
                                                                      [
                                                                        Ty.tuple
                                                                          [
                                                                            Ty.path
                                                                              "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                                                          ]
                                                                      ]
                                                                      (Ty.path
                                                                        "spl_token_2022::error::TokenError")
                                                                  ]
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::convert::TryInto",
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                                                      [
                                                                        Ty.path
                                                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext"
                                                                      ],
                                                                      "try_into",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (|
                                                                        new_available_balance_ciphertext
                                                                      |)
                                                                    ]
                                                                  |);
                                                                  M.closure
                                                                    (fun γ =>
                                                                      ltac:(M.monadic
                                                                        match γ with
                                                                        | [ α0 ] =>
                                                                          M.match_operator (|
                                                                            M.alloc (| α0 |),
                                                                            [
                                                                              fun γ =>
                                                                                ltac:(M.monadic
                                                                                  (Value.StructTuple
                                                                                    "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                                                    []))
                                                                            ]
                                                                          |)
                                                                        | _ => M.impossible (||)
                                                                        end))
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Break",
                                                                  0
                                                                |) in
                                                              let residual := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::try_trait::FromResidual",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            [
                                                                              Ty.tuple
                                                                                [
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                                  Ty.path
                                                                                    "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                                                ];
                                                                              Ty.path
                                                                                "spl_token_2022::error::TokenError"
                                                                            ],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              [
                                                                                Ty.path
                                                                                  "core::convert::Infallible";
                                                                                Ty.path
                                                                                  "spl_token_2022::error::TokenError"
                                                                              ]
                                                                          ],
                                                                          "from_residual",
                                                                          []
                                                                        |),
                                                                        [ M.read (| residual |) ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                                  0
                                                                |) in
                                                              let val := M.copy (| γ0_0 |) in
                                                              val))
                                                        ]
                                                      |)
                                                    |) in
                                                  let equality_proof_data :=
                                                    M.copy (|
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::Try",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                [
                                                                  Ty.path
                                                                    "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                  Ty.path
                                                                    "spl_token_2022::error::TokenError"
                                                                ],
                                                              [],
                                                              "branch",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    [
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::errors::ProofGenerationError"
                                                                    ],
                                                                  "map_err",
                                                                  [
                                                                    Ty.path
                                                                      "spl_token_2022::error::TokenError";
                                                                    Ty.function
                                                                      [
                                                                        Ty.tuple
                                                                          [
                                                                            Ty.path
                                                                              "solana_zk_token_sdk::errors::ProofGenerationError"
                                                                          ]
                                                                      ]
                                                                      (Ty.path
                                                                        "spl_token_2022::error::TokenError")
                                                                  ]
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData",
                                                                      "new",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (|
                                                                        source_elgamal_keypair
                                                                      |);
                                                                      new_available_balance_ciphertext;
                                                                      new_available_balance_commitment;
                                                                      new_source_opening;
                                                                      M.read (|
                                                                        new_decrypted_available_balance
                                                                      |)
                                                                    ]
                                                                  |);
                                                                  M.closure
                                                                    (fun γ =>
                                                                      ltac:(M.monadic
                                                                        match γ with
                                                                        | [ α0 ] =>
                                                                          M.match_operator (|
                                                                            M.alloc (| α0 |),
                                                                            [
                                                                              fun γ =>
                                                                                ltac:(M.monadic
                                                                                  (Value.StructTuple
                                                                                    "spl_token_2022::error::TokenError::ProofGeneration"
                                                                                    []))
                                                                            ]
                                                                          |)
                                                                        | _ => M.impossible (||)
                                                                        end))
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Break",
                                                                  0
                                                                |) in
                                                              let residual := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::try_trait::FromResidual",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            [
                                                                              Ty.tuple
                                                                                [
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                                  Ty.path
                                                                                    "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                                                ];
                                                                              Ty.path
                                                                                "spl_token_2022::error::TokenError"
                                                                            ],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              [
                                                                                Ty.path
                                                                                  "core::convert::Infallible";
                                                                                Ty.path
                                                                                  "spl_token_2022::error::TokenError"
                                                                              ]
                                                                          ],
                                                                          "from_residual",
                                                                          []
                                                                        |),
                                                                        [ M.read (| residual |) ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                                  0
                                                                |) in
                                                              let val := M.copy (| γ0_0 |) in
                                                              val))
                                                        ]
                                                      |)
                                                    |) in
                                                  let source_decrypt_handle_lo :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "solana_zk_token_sdk::encryption::elgamal::DecryptHandle",
                                                          "new",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalKeypair",
                                                              "pubkey",
                                                              []
                                                            |),
                                                            [ M.read (| source_elgamal_keypair |) ]
                                                          |);
                                                          transfer_amount_opening_lo
                                                        ]
                                                      |)
                                                    |) in
                                                  let source_decrypt_handle_hi :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "solana_zk_token_sdk::encryption::elgamal::DecryptHandle",
                                                          "new",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalKeypair",
                                                              "pubkey",
                                                              []
                                                            |),
                                                            [ M.read (| source_elgamal_keypair |) ]
                                                          |);
                                                          transfer_amount_opening_hi
                                                        ]
                                                      |)
                                                    |) in
                                                  let source_decrypt_handles :=
                                                    M.alloc (|
                                                      Value.StructRecord
                                                        "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                        [
                                                          ("lo",
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::convert::Into",
                                                                Ty.path
                                                                  "solana_zk_token_sdk::encryption::elgamal::DecryptHandle",
                                                                [
                                                                  Ty.path
                                                                    "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::DecryptHandle"
                                                                ],
                                                                "into",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  source_decrypt_handle_lo
                                                                |)
                                                              ]
                                                            |));
                                                          ("hi",
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::convert::Into",
                                                                Ty.path
                                                                  "solana_zk_token_sdk::encryption::elgamal::DecryptHandle",
                                                                [
                                                                  Ty.path
                                                                    "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::DecryptHandle"
                                                                ],
                                                                "into",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  source_decrypt_handle_hi
                                                                |)
                                                              ]
                                                            |))
                                                        ]
                                                    |) in
                                                  let
                                                        transfer_amount_destination_auditor_ciphertext_lo :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "solana_zk_token_sdk::encryption::grouped_elgamal::GroupedElGamal",
                                                          "encrypt_with",
                                                          [ Ty.path "u64" ]
                                                        |),
                                                        [
                                                          Value.Array
                                                            [
                                                              M.read (|
                                                                destination_elgamal_pubkey
                                                              |);
                                                              M.read (| auditor_elgamal_pubkey |)
                                                            ];
                                                          M.read (| transfer_amount_lo |);
                                                          transfer_amount_opening_lo
                                                        ]
                                                      |)
                                                    |) in
                                                  let
                                                        transfer_amount_destination_auditor_ciphertext_hi :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "solana_zk_token_sdk::encryption::grouped_elgamal::GroupedElGamal",
                                                          "encrypt_with",
                                                          [ Ty.path "u64" ]
                                                        |),
                                                        [
                                                          Value.Array
                                                            [
                                                              M.read (|
                                                                destination_elgamal_pubkey
                                                              |);
                                                              M.read (| auditor_elgamal_pubkey |)
                                                            ];
                                                          M.read (| transfer_amount_hi |);
                                                          transfer_amount_opening_hi
                                                        ]
                                                      |)
                                                    |) in
                                                  let ciphertext_validity_proof_data :=
                                                    M.copy (|
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::Try",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                [
                                                                  Ty.path
                                                                    "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                  Ty.path
                                                                    "spl_token_2022::error::TokenError"
                                                                ],
                                                              [],
                                                              "branch",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    [
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::errors::ProofGenerationError"
                                                                    ],
                                                                  "map_err",
                                                                  [
                                                                    Ty.path
                                                                      "spl_token_2022::error::TokenError";
                                                                    Ty.function
                                                                      [
                                                                        Ty.tuple
                                                                          [
                                                                            Ty.path
                                                                              "solana_zk_token_sdk::errors::ProofGenerationError"
                                                                          ]
                                                                      ]
                                                                      (Ty.path
                                                                        "spl_token_2022::error::TokenError")
                                                                  ]
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData",
                                                                      "new",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (|
                                                                        destination_elgamal_pubkey
                                                                      |);
                                                                      M.read (|
                                                                        auditor_elgamal_pubkey
                                                                      |);
                                                                      transfer_amount_destination_auditor_ciphertext_lo;
                                                                      transfer_amount_destination_auditor_ciphertext_hi;
                                                                      M.read (|
                                                                        transfer_amount_lo
                                                                      |);
                                                                      M.read (|
                                                                        transfer_amount_hi
                                                                      |);
                                                                      transfer_amount_opening_lo;
                                                                      transfer_amount_opening_hi
                                                                    ]
                                                                  |);
                                                                  M.closure
                                                                    (fun γ =>
                                                                      ltac:(M.monadic
                                                                        match γ with
                                                                        | [ α0 ] =>
                                                                          M.match_operator (|
                                                                            M.alloc (| α0 |),
                                                                            [
                                                                              fun γ =>
                                                                                ltac:(M.monadic
                                                                                  (Value.StructTuple
                                                                                    "spl_token_2022::error::TokenError::ProofGeneration"
                                                                                    []))
                                                                            ]
                                                                          |)
                                                                        | _ => M.impossible (||)
                                                                        end))
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Break",
                                                                  0
                                                                |) in
                                                              let residual := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::try_trait::FromResidual",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            [
                                                                              Ty.tuple
                                                                                [
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                                  Ty.path
                                                                                    "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                                  Ty.path
                                                                                    "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                                                ];
                                                                              Ty.path
                                                                                "spl_token_2022::error::TokenError"
                                                                            ],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              [
                                                                                Ty.path
                                                                                  "core::convert::Infallible";
                                                                                Ty.path
                                                                                  "spl_token_2022::error::TokenError"
                                                                              ]
                                                                          ],
                                                                          "from_residual",
                                                                          []
                                                                        |),
                                                                        [ M.read (| residual |) ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                                  0
                                                                |) in
                                                              let val := M.copy (| γ0_0 |) in
                                                              val))
                                                        ]
                                                      |)
                                                    |) in
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "solana_zk_token_sdk::encryption::pedersen::Pedersen",
                                                          "new",
                                                          [ Ty.path "u64" ]
                                                        |),
                                                        [ Value.Integer 0 ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_tuple_field (|
                                                              γ,
                                                              0
                                                            |) in
                                                          let γ0_1 :=
                                                            M.SubPointer.get_tuple_field (|
                                                              γ,
                                                              1
                                                            |) in
                                                          let padding_commitment :=
                                                            M.copy (| γ0_0 |) in
                                                          let padding_opening :=
                                                            M.copy (| γ0_1 |) in
                                                          let range_proof_data :=
                                                            M.copy (|
                                                              M.match_operator (|
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::ops::try_trait::Try",
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::result::Result")
                                                                        [
                                                                          Ty.path
                                                                            "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                          Ty.path
                                                                            "spl_token_2022::error::TokenError"
                                                                        ],
                                                                      [],
                                                                      "branch",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            [
                                                                              Ty.path
                                                                                "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                              Ty.path
                                                                                "solana_zk_token_sdk::errors::ProofGenerationError"
                                                                            ],
                                                                          "map_err",
                                                                          [
                                                                            Ty.path
                                                                              "spl_token_2022::error::TokenError";
                                                                            Ty.function
                                                                              [
                                                                                Ty.tuple
                                                                                  [
                                                                                    Ty.path
                                                                                      "solana_zk_token_sdk::errors::ProofGenerationError"
                                                                                  ]
                                                                              ]
                                                                              (Ty.path
                                                                                "spl_token_2022::error::TokenError")
                                                                          ]
                                                                        |),
                                                                        [
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.path
                                                                                "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data",
                                                                              "new",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "slice")
                                                                                    [
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "&")
                                                                                        [
                                                                                          Ty.path
                                                                                            "solana_zk_token_sdk::encryption::pedersen::PedersenCommitment"
                                                                                        ]
                                                                                    ],
                                                                                  "into_vec",
                                                                                  [
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ]
                                                                                |),
                                                                                [
                                                                                  (* Unsize *)
                                                                                  M.pointer_coercion
                                                                                    (M.read (|
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "alloc::boxed::Box")
                                                                                            [
                                                                                              Ty.apply
                                                                                                (Ty.path
                                                                                                  "array")
                                                                                                [
                                                                                                  Ty.apply
                                                                                                    (Ty.path
                                                                                                      "&")
                                                                                                    [
                                                                                                      Ty.path
                                                                                                        "solana_zk_token_sdk::encryption::pedersen::PedersenCommitment"
                                                                                                    ]
                                                                                                ];
                                                                                              Ty.path
                                                                                                "alloc::alloc::Global"
                                                                                            ],
                                                                                          "new",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.alloc (|
                                                                                            Value.Array
                                                                                              [
                                                                                                new_available_balance_commitment;
                                                                                                M.call_closure (|
                                                                                                  M.get_associated_function (|
                                                                                                    Ty.path
                                                                                                      "solana_zk_token_sdk::instruction::transfer::encryption::TransferAmountCiphertext",
                                                                                                    "get_commitment",
                                                                                                    []
                                                                                                  |),
                                                                                                  [
                                                                                                    transfer_amount_grouped_ciphertext_lo
                                                                                                  ]
                                                                                                |);
                                                                                                M.call_closure (|
                                                                                                  M.get_associated_function (|
                                                                                                    Ty.path
                                                                                                      "solana_zk_token_sdk::instruction::transfer::encryption::TransferAmountCiphertext",
                                                                                                    "get_commitment",
                                                                                                    []
                                                                                                  |),
                                                                                                  [
                                                                                                    transfer_amount_grouped_ciphertext_hi
                                                                                                  ]
                                                                                                |);
                                                                                                padding_commitment
                                                                                              ]
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    |))
                                                                                ]
                                                                              |);
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "slice")
                                                                                    [ Ty.path "u64"
                                                                                    ],
                                                                                  "into_vec",
                                                                                  [
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ]
                                                                                |),
                                                                                [
                                                                                  (* Unsize *)
                                                                                  M.pointer_coercion
                                                                                    (M.read (|
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "alloc::boxed::Box")
                                                                                            [
                                                                                              Ty.apply
                                                                                                (Ty.path
                                                                                                  "array")
                                                                                                [
                                                                                                  Ty.path
                                                                                                    "u64"
                                                                                                ];
                                                                                              Ty.path
                                                                                                "alloc::alloc::Global"
                                                                                            ],
                                                                                          "new",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.alloc (|
                                                                                            Value.Array
                                                                                              [
                                                                                                M.read (|
                                                                                                  new_decrypted_available_balance
                                                                                                |);
                                                                                                M.read (|
                                                                                                  transfer_amount_lo
                                                                                                |);
                                                                                                M.read (|
                                                                                                  transfer_amount_hi
                                                                                                |);
                                                                                                Value.Integer
                                                                                                  0
                                                                                              ]
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    |))
                                                                                ]
                                                                              |);
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "slice")
                                                                                    [
                                                                                      Ty.path
                                                                                        "usize"
                                                                                    ],
                                                                                  "into_vec",
                                                                                  [
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ]
                                                                                |),
                                                                                [
                                                                                  (* Unsize *)
                                                                                  M.pointer_coercion
                                                                                    (M.read (|
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "alloc::boxed::Box")
                                                                                            [
                                                                                              Ty.apply
                                                                                                (Ty.path
                                                                                                  "array")
                                                                                                [
                                                                                                  Ty.path
                                                                                                    "usize"
                                                                                                ];
                                                                                              Ty.path
                                                                                                "alloc::alloc::Global"
                                                                                            ],
                                                                                          "new",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.alloc (|
                                                                                            Value.Array
                                                                                              [
                                                                                                M.read (|
                                                                                                  M.get_constant (|
                                                                                                    "spl_token_2022::extension::confidential_transfer::split_proof_generation::transfer_split_proof_data::REMAINING_BALANCE_BIT_LENGTH"
                                                                                                  |)
                                                                                                |);
                                                                                                M.read (|
                                                                                                  M.get_constant (|
                                                                                                    "spl_token_2022::extension::confidential_transfer::split_proof_generation::transfer_split_proof_data::TRANSFER_AMOUNT_LO_BIT_LENGTH"
                                                                                                  |)
                                                                                                |);
                                                                                                M.read (|
                                                                                                  M.get_constant (|
                                                                                                    "spl_token_2022::extension::confidential_transfer::split_proof_generation::transfer_split_proof_data::TRANSFER_AMOUNT_HI_BIT_LENGTH"
                                                                                                  |)
                                                                                                |);
                                                                                                M.read (|
                                                                                                  M.get_constant (|
                                                                                                    "spl_token_2022::extension::confidential_transfer::split_proof_generation::transfer_split_proof_data::PADDING_BIT_LENGTH"
                                                                                                  |)
                                                                                                |)
                                                                                              ]
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    |))
                                                                                ]
                                                                              |);
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "slice")
                                                                                    [
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "&")
                                                                                        [
                                                                                          Ty.path
                                                                                            "solana_zk_token_sdk::encryption::pedersen::PedersenOpening"
                                                                                        ]
                                                                                    ],
                                                                                  "into_vec",
                                                                                  [
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ]
                                                                                |),
                                                                                [
                                                                                  (* Unsize *)
                                                                                  M.pointer_coercion
                                                                                    (M.read (|
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "alloc::boxed::Box")
                                                                                            [
                                                                                              Ty.apply
                                                                                                (Ty.path
                                                                                                  "array")
                                                                                                [
                                                                                                  Ty.apply
                                                                                                    (Ty.path
                                                                                                      "&")
                                                                                                    [
                                                                                                      Ty.path
                                                                                                        "solana_zk_token_sdk::encryption::pedersen::PedersenOpening"
                                                                                                    ]
                                                                                                ];
                                                                                              Ty.path
                                                                                                "alloc::alloc::Global"
                                                                                            ],
                                                                                          "new",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.alloc (|
                                                                                            Value.Array
                                                                                              [
                                                                                                new_source_opening;
                                                                                                transfer_amount_opening_lo;
                                                                                                transfer_amount_opening_hi;
                                                                                                padding_opening
                                                                                              ]
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    |))
                                                                                ]
                                                                              |)
                                                                            ]
                                                                          |);
                                                                          M.closure
                                                                            (fun γ =>
                                                                              ltac:(M.monadic
                                                                                match γ with
                                                                                | [ α0 ] =>
                                                                                  M.match_operator (|
                                                                                    M.alloc (|
                                                                                      α0
                                                                                    |),
                                                                                    [
                                                                                      fun γ =>
                                                                                        ltac:(M.monadic
                                                                                          (Value.StructTuple
                                                                                            "spl_token_2022::error::TokenError::ProofGeneration"
                                                                                            []))
                                                                                    ]
                                                                                  |)
                                                                                | _ =>
                                                                                  M.impossible (||)
                                                                                end))
                                                                        ]
                                                                      |)
                                                                    ]
                                                                  |)
                                                                |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ0_0 :=
                                                                        M.SubPointer.get_struct_tuple_field (|
                                                                          γ,
                                                                          "core::ops::control_flow::ControlFlow::Break",
                                                                          0
                                                                        |) in
                                                                      let residual :=
                                                                        M.copy (| γ0_0 |) in
                                                                      M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.read (|
                                                                            M.return_ (|
                                                                              M.call_closure (|
                                                                                M.get_trait_method (|
                                                                                  "core::ops::try_trait::FromResidual",
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::result::Result")
                                                                                    [
                                                                                      Ty.tuple
                                                                                        [
                                                                                          Ty.path
                                                                                            "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                                                          Ty.path
                                                                                            "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                                                          Ty.path
                                                                                            "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                                                          Ty.path
                                                                                            "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                                                        ];
                                                                                      Ty.path
                                                                                        "spl_token_2022::error::TokenError"
                                                                                    ],
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "core::result::Result")
                                                                                      [
                                                                                        Ty.path
                                                                                          "core::convert::Infallible";
                                                                                        Ty.path
                                                                                          "spl_token_2022::error::TokenError"
                                                                                      ]
                                                                                  ],
                                                                                  "from_residual",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (|
                                                                                    residual
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ0_0 :=
                                                                        M.SubPointer.get_struct_tuple_field (|
                                                                          γ,
                                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                                          0
                                                                        |) in
                                                                      let val :=
                                                                        M.copy (| γ0_0 |) in
                                                                      val))
                                                                ]
                                                              |)
                                                            |) in
                                                          M.alloc (|
                                                            Value.StructTuple
                                                              "core::result::Result::Ok"
                                                              [
                                                                Value.Tuple
                                                                  [
                                                                    M.read (|
                                                                      equality_proof_data
                                                                    |);
                                                                    M.read (|
                                                                      ciphertext_validity_proof_data
                                                                    |);
                                                                    M.read (| range_proof_data |);
                                                                    M.read (|
                                                                      source_decrypt_handles
                                                                    |)
                                                                  ]
                                                              ]
                                                          |)))
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _ => M.impossible
        end.
      
      Module transfer_split_proof_data.
        Definition value_REMAINING_BALANCE_BIT_LENGTH : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer 64 |))).
        
        Definition value_TRANSFER_AMOUNT_LO_BIT_LENGTH : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer 16 |))).
        
        Definition value_TRANSFER_AMOUNT_HI_BIT_LENGTH : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer 32 |))).
        
        Definition value_PADDING_BIT_LENGTH : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer 16 |))).
      End transfer_split_proof_data.
    End split_proof_generation.
  End confidential_transfer.
End extension.
