Skip to main content

🏗️ Apply_results.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Definition error_encoding : Data_encoding.encoding Error_monad._error :=
  (let arg :=
    fun x_1
      Data_encoding.def "error" x_1
        (Some
          "The full list of RPC errors would be too long to include.\nIt is available at RPC `/errors` (GET).\nErrors specific to protocol Alpha have an id that starts with `proto.alpha`.")
    in
  fun (eta : Data_encoding.encoding Error_monad._error) ⇒ arg None eta)
    (Data_encoding.splitted
      (Data_encoding.conv
        (fun (err : Error_monad._error) ⇒
          Data_encoding.Json.construct None Error_monad.error_encoding err)
        (fun (json_value : Data_encoding.json) ⇒
          Data_encoding.Json.destruct None Error_monad.error_encoding json_value)
        None Data_encoding.json_value) Error_monad.error_encoding).

Definition trace_encoding
  : Data_encoding.t (Error_monad.trace Error_monad._error) :=
  Error_monad.make_trace_encoding error_encoding.

Inductive internal_manager_operation : Set :=
| Transaction : Alpha_context.transaction internal_manager_operation
| Origination : Alpha_context.origination internal_manager_operation
| Delegation : option Signature.public_key_hash internal_manager_operation.

Inductive packed_internal_manager_operation : Set :=
| Manager : internal_manager_operation packed_internal_manager_operation.

Module internal_contents.
  Record record : Set := Build {
    source : Alpha_context.Contract.contract;
    operation : internal_manager_operation;
    nonce : int;
  }.
  Definition with_source source (r : record) :=
    Build source r.(operation) r.(nonce).
  Definition with_operation operation (r : record) :=
    Build r.(source) operation r.(nonce).
  Definition with_nonce nonce (r : record) :=
    Build r.(source) r.(operation) nonce.
End internal_contents.
Definition internal_contents := internal_contents.record.

Inductive packed_internal_contents : Set :=
| Internal_contents : internal_contents packed_internal_contents.

Definition manager_operation_of_internal_operation
  (operation : internal_manager_operation) : Alpha_context.manager_operation :=
  match operation with
  | Transaction transactionAlpha_context.Transaction transaction
  | Origination originationAlpha_context.Origination origination
  | Delegation delegateAlpha_context.Delegation delegate
  end.

Definition contents_of_internal_operation
  (function_parameter : Script_typed_ir.internal_operation)
  : internal_contents :=
  let '{|
    Script_typed_ir.internal_operation.source := source;
      Script_typed_ir.internal_operation.operation := operation;
      Script_typed_ir.internal_operation.nonce := nonce_value
      |} := function_parameter in
  let operation :=
    match operation with
    |
      Script_typed_ir.Transaction {|
        Script_typed_ir.manager_operation.Transaction.transaction := transaction
          |} ⇒ Transaction transaction
    |
      Script_typed_ir.Origination {|
        Script_typed_ir.manager_operation.Origination.origination := origination
          |} ⇒ Origination origination
    | Script_typed_ir.Delegation delegateDelegation delegate
    end in
  {| internal_contents.source := source;
    internal_contents.operation := operation;
    internal_contents.nonce := nonce_value; |}.

Definition contents_of_packed_internal_operation
  (function_parameter : Script_typed_ir.packed_internal_operation)
  : packed_internal_contents :=
  let 'Script_typed_ir.Internal_operation op := function_parameter in
  Internal_contents (contents_of_internal_operation op).

Definition contents_of_packed_internal_operations
  : list Script_typed_ir.packed_internal_operation
  list packed_internal_contents :=
  List.map contents_of_packed_internal_operation.

Records for the constructor parameters
Module ConstructorRecords_successful_transaction_result.
  Module successful_transaction_result.
    Module Transaction_to_contract_result.
      Record record {storage lazy_storage_diff balance_updates
        originated_contracts consumed_gas storage_size
        allocated_destination_contract : Set} : Set := Build {
        storage : storage;
        lazy_storage_diff : lazy_storage_diff;
        balance_updates : balance_updates;
        originated_contracts : originated_contracts;
        consumed_gas : consumed_gas;
        storage_size : storage_size;
        paid_storage_size_diff : paid_storage_size_diff;
        allocated_destination_contract : allocated_destination_contract;
      }.
      Arguments record : clear implicits.
      Definition with_storage
        {t_storage t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          t_allocated_destination_contract} storage
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_originated_contracts t_consumed_gas t_storage_size
            t_paid_storage_size_diff t_allocated_destination_contract) :=
        Build t_storage t_lazy_storage_diff t_balance_updates
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract storage
          r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
          r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff)
          r.(allocated_destination_contract).
      Definition with_lazy_storage_diff
        {t_storage t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          t_allocated_destination_contract} lazy_storage_diff
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_originated_contracts t_consumed_gas t_storage_size
            t_paid_storage_size_diff t_allocated_destination_contract) :=
        Build t_storage t_lazy_storage_diff t_balance_updates
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract r.(storage)
          lazy_storage_diff r.(balance_updates) r.(originated_contracts)
          r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff)
          r.(allocated_destination_contract).
      Definition with_balance_updates
        {t_storage t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          t_allocated_destination_contract} balance_updates
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_originated_contracts t_consumed_gas t_storage_size
            t_paid_storage_size_diff t_allocated_destination_contract) :=
        Build t_storage t_lazy_storage_diff t_balance_updates
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract r.(storage)
          r.(lazy_storage_diff) balance_updates r.(originated_contracts)
          r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff)
          r.(allocated_destination_contract).
      Definition with_originated_contracts
        {t_storage t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          t_allocated_destination_contract} originated_contracts
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_originated_contracts t_consumed_gas t_storage_size
            t_paid_storage_size_diff t_allocated_destination_contract) :=
        Build t_storage t_lazy_storage_diff t_balance_updates
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract r.(storage)
          r.(lazy_storage_diff) r.(balance_updates) originated_contracts
          r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff)
          r.(allocated_destination_contract).
      Definition with_consumed_gas
        {t_storage t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          t_allocated_destination_contract} consumed_gas
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_originated_contracts t_consumed_gas t_storage_size
            t_paid_storage_size_diff t_allocated_destination_contract) :=
        Build t_storage t_lazy_storage_diff t_balance_updates
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract r.(storage)
          r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
          consumed_gas r.(storage_size) r.(paid_storage_size_diff)
          r.(allocated_destination_contract).
      Definition with_storage_size
        {t_storage t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          t_allocated_destination_contract} storage_size
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_originated_contracts t_consumed_gas t_storage_size
            t_paid_storage_size_diff t_allocated_destination_contract) :=
        Build t_storage t_lazy_storage_diff t_balance_updates
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract r.(storage)
          r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
          r.(consumed_gas) storage_size r.(paid_storage_size_diff)
          r.(allocated_destination_contract).
      Definition with_paid_storage_size_diff
        {t_storage t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          t_allocated_destination_contract}
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_originated_contracts t_consumed_gas t_storage_size
            t_paid_storage_size_diff t_allocated_destination_contract) :=
        Build t_storage t_lazy_storage_diff t_balance_updates
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract r.(storage)
          r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
          r.(consumed_gas) r.(storage_size) paid_storage_size_diff
          r.(allocated_destination_contract).
      Definition with_allocated_destination_contract
        {t_storage t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          t_allocated_destination_contract} allocated_destination_contract
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_originated_contracts t_consumed_gas t_storage_size
            t_paid_storage_size_diff t_allocated_destination_contract) :=
        Build t_storage t_lazy_storage_diff t_balance_updates
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract r.(storage)
          r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
          r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff)
          allocated_destination_contract.
    End Transaction_to_contract_result.
    Definition Transaction_to_contract_result_skeleton :=
      Transaction_to_contract_result.record.

    Module Transaction_to_tx_rollup_result.
      Record record {ticket_hash balance_updates consumed_gas
         : Set} : Set := Build {
        ticket_hash : ticket_hash;
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_ticket_hash
        {t_ticket_hash t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        ticket_hash
        (r :
          record t_ticket_hash t_balance_updates t_consumed_gas
            t_paid_storage_size_diff) :=
        Build t_ticket_hash t_balance_updates t_consumed_gas
          t_paid_storage_size_diff ticket_hash r.(balance_updates)
          r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_balance_updates
        {t_ticket_hash t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r :
          record t_ticket_hash t_balance_updates t_consumed_gas
            t_paid_storage_size_diff) :=
        Build t_ticket_hash t_balance_updates t_consumed_gas
          t_paid_storage_size_diff r.(ticket_hash) balance_updates
          r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_ticket_hash t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        consumed_gas
        (r :
          record t_ticket_hash t_balance_updates t_consumed_gas
            t_paid_storage_size_diff) :=
        Build t_ticket_hash t_balance_updates t_consumed_gas
          t_paid_storage_size_diff r.(ticket_hash) r.(balance_updates)
          consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_ticket_hash t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        
        (r :
          record t_ticket_hash t_balance_updates t_consumed_gas
            t_paid_storage_size_diff) :=
        Build t_ticket_hash t_balance_updates t_consumed_gas
          t_paid_storage_size_diff r.(ticket_hash) r.(balance_updates)
          r.(consumed_gas) paid_storage_size_diff.
    End Transaction_to_tx_rollup_result.
    Definition Transaction_to_tx_rollup_result_skeleton :=
      Transaction_to_tx_rollup_result.record.
  End successful_transaction_result.
End ConstructorRecords_successful_transaction_result.
Import ConstructorRecords_successful_transaction_result.

Reserved Notation
  "'successful_transaction_result.Transaction_to_contract_result".
Reserved Notation
  "'successful_transaction_result.Transaction_to_tx_rollup_result".

Inductive successful_transaction_result : Set :=
| Transaction_to_contract_result :
  'successful_transaction_result.Transaction_to_contract_result
  successful_transaction_result
| Transaction_to_tx_rollup_result :
  'successful_transaction_result.Transaction_to_tx_rollup_result
  successful_transaction_result

where "'successful_transaction_result.Transaction_to_contract_result" :=
  (successful_transaction_result.Transaction_to_contract_result_skeleton
    (option Alpha_context.Script.expr) (option Alpha_context.Lazy_storage.diffs)
    Alpha_context.Receipt.balance_updates (list Alpha_context.Contract.t)
    Alpha_context.Gas.Arith.fp Z.t Z.t bool)
and "'successful_transaction_result.Transaction_to_tx_rollup_result" :=
  (successful_transaction_result.Transaction_to_tx_rollup_result_skeleton
    Alpha_context.Ticket_hash.t Alpha_context.Receipt.balance_updates
    Alpha_context.Gas.Arith.fp Z.t).

Module successful_transaction_result.
  Include ConstructorRecords_successful_transaction_result.successful_transaction_result.
  Definition Transaction_to_contract_result :=
    'successful_transaction_result.Transaction_to_contract_result.
  Definition Transaction_to_tx_rollup_result :=
    'successful_transaction_result.Transaction_to_tx_rollup_result.
End successful_transaction_result.

Records for the constructor parameters
Module ConstructorRecords_successful_manager_operation_result.
  Module successful_manager_operation_result.
    Module Reveal_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Reveal_result.
    Definition Reveal_result_skeleton := Reveal_result.record.

    Module Origination_result.
      Record record {lazy_storage_diff balance_updates originated_contracts
        consumed_gas storage_size : Set} : Set := Build {
        lazy_storage_diff : lazy_storage_diff;
        balance_updates : balance_updates;
        originated_contracts : originated_contracts;
        consumed_gas : consumed_gas;
        storage_size : storage_size;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_lazy_storage_diff
        {t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff}
        lazy_storage_diff
        (r :
          record t_lazy_storage_diff t_balance_updates t_originated_contracts
            t_consumed_gas t_storage_size t_paid_storage_size_diff) :=
        Build t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          lazy_storage_diff r.(balance_updates) r.(originated_contracts)
          r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff).
      Definition with_balance_updates
        {t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff}
        balance_updates
        (r :
          record t_lazy_storage_diff t_balance_updates t_originated_contracts
            t_consumed_gas t_storage_size t_paid_storage_size_diff) :=
        Build t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          r.(lazy_storage_diff) balance_updates r.(originated_contracts)
          r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff).
      Definition with_originated_contracts
        {t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff}
        originated_contracts
        (r :
          record t_lazy_storage_diff t_balance_updates t_originated_contracts
            t_consumed_gas t_storage_size t_paid_storage_size_diff) :=
        Build t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          r.(lazy_storage_diff) r.(balance_updates) originated_contracts
          r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff} consumed_gas
        (r :
          record t_lazy_storage_diff t_balance_updates t_originated_contracts
            t_consumed_gas t_storage_size t_paid_storage_size_diff) :=
        Build t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
          consumed_gas r.(storage_size) r.(paid_storage_size_diff).
      Definition with_storage_size
        {t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff} storage_size
        (r :
          record t_lazy_storage_diff t_balance_updates t_originated_contracts
            t_consumed_gas t_storage_size t_paid_storage_size_diff) :=
        Build t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
          r.(consumed_gas) storage_size r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff}
        
        (r :
          record t_lazy_storage_diff t_balance_updates t_originated_contracts
            t_consumed_gas t_storage_size t_paid_storage_size_diff) :=
        Build t_lazy_storage_diff t_balance_updates t_originated_contracts
          t_consumed_gas t_storage_size t_paid_storage_size_diff
          r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
          r.(consumed_gas) r.(storage_size) paid_storage_size_diff.
    End Origination_result.
    Definition Origination_result_skeleton := Origination_result.record.

    Module Delegation_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Delegation_result.
    Definition Delegation_result_skeleton := Delegation_result.record.

    Module Register_global_constant_result.
      Record record {balance_updates consumed_gas size_of_constant
        global_address : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        size_of_constant : size_of_constant;
        global_address : global_address;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
        balance_updates
        (r :
          record t_balance_updates t_consumed_gas t_size_of_constant
            t_global_address) :=
        Build t_balance_updates t_consumed_gas t_size_of_constant
          t_global_address balance_updates r.(consumed_gas) r.(size_of_constant)
          r.(global_address).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
        consumed_gas
        (r :
          record t_balance_updates t_consumed_gas t_size_of_constant
            t_global_address) :=
        Build t_balance_updates t_consumed_gas t_size_of_constant
          t_global_address r.(balance_updates) consumed_gas r.(size_of_constant)
          r.(global_address).
      Definition with_size_of_constant
        {t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
        size_of_constant
        (r :
          record t_balance_updates t_consumed_gas t_size_of_constant
            t_global_address) :=
        Build t_balance_updates t_consumed_gas t_size_of_constant
          t_global_address r.(balance_updates) r.(consumed_gas) size_of_constant
          r.(global_address).
      Definition with_global_address
        {t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
        global_address
        (r :
          record t_balance_updates t_consumed_gas t_size_of_constant
            t_global_address) :=
        Build t_balance_updates t_consumed_gas t_size_of_constant
          t_global_address r.(balance_updates) r.(consumed_gas)
          r.(size_of_constant) global_address.
    End Register_global_constant_result.
    Definition Register_global_constant_result_skeleton :=
      Register_global_constant_result.record.

    Module Set_deposits_limit_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Set_deposits_limit_result.
    Definition Set_deposits_limit_result_skeleton :=
      Set_deposits_limit_result.record.

    Module Tx_rollup_origination_result.
      Record record {balance_updates consumed_gas originated_tx_rollup : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        originated_tx_rollup : originated_tx_rollup;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_originated_tx_rollup}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
        Build t_balance_updates t_consumed_gas t_originated_tx_rollup
          balance_updates r.(consumed_gas) r.(originated_tx_rollup).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_originated_tx_rollup} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
        Build t_balance_updates t_consumed_gas t_originated_tx_rollup
          r.(balance_updates) consumed_gas r.(originated_tx_rollup).
      Definition with_originated_tx_rollup
        {t_balance_updates t_consumed_gas t_originated_tx_rollup}
        originated_tx_rollup
        (r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
        Build t_balance_updates t_consumed_gas t_originated_tx_rollup
          r.(balance_updates) r.(consumed_gas) originated_tx_rollup.
    End Tx_rollup_origination_result.
    Definition Tx_rollup_origination_result_skeleton :=
      Tx_rollup_origination_result.record.

    Module Tx_rollup_submit_batch_result.
      Record record {balance_updates consumed_gas : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Tx_rollup_submit_batch_result.
    Definition Tx_rollup_submit_batch_result_skeleton :=
      Tx_rollup_submit_batch_result.record.

    Module Tx_rollup_commit_result.
      Record record {balance_updates consumed_gas : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas}
        balance_updates (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas}
        consumed_gas (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
    End Tx_rollup_commit_result.
    Definition Tx_rollup_commit_result_skeleton :=
      Tx_rollup_commit_result.record.

    Module Tx_rollup_return_bond_result.
      Record record {balance_updates consumed_gas : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas}
        balance_updates (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas}
        consumed_gas (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
    End Tx_rollup_return_bond_result.
    Definition Tx_rollup_return_bond_result_skeleton :=
      Tx_rollup_return_bond_result.record.

    Module Tx_rollup_finalize_commitment_result.
      Record record {balance_updates consumed_gas level : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        level : level;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas t_level}
        balance_updates (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level balance_updates
          r.(consumed_gas) r.(level).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas t_level}
        consumed_gas (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
          consumed_gas r.(level).
      Definition with_level {t_balance_updates t_consumed_gas t_level} level
        (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
          r.(consumed_gas) level.
    End Tx_rollup_finalize_commitment_result.
    Definition Tx_rollup_finalize_commitment_result_skeleton :=
      Tx_rollup_finalize_commitment_result.record.

    Module Tx_rollup_remove_commitment_result.
      Record record {balance_updates consumed_gas level : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        level : level;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas t_level}
        balance_updates (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level balance_updates
          r.(consumed_gas) r.(level).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas t_level}
        consumed_gas (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
          consumed_gas r.(level).
      Definition with_level {t_balance_updates t_consumed_gas t_level} level
        (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
          r.(consumed_gas) level.
    End Tx_rollup_remove_commitment_result.
    Definition Tx_rollup_remove_commitment_result_skeleton :=
      Tx_rollup_remove_commitment_result.record.

    Module Tx_rollup_rejection_result.
      Record record {balance_updates consumed_gas : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas}
        balance_updates (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas}
        consumed_gas (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
    End Tx_rollup_rejection_result.
    Definition Tx_rollup_rejection_result_skeleton :=
      Tx_rollup_rejection_result.record.

    Module Tx_rollup_dispatch_tickets_result.
      Record record {balance_updates consumed_gas : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Tx_rollup_dispatch_tickets_result.
    Definition Tx_rollup_dispatch_tickets_result_skeleton :=
      Tx_rollup_dispatch_tickets_result.record.

    Module Transfer_ticket_result.
      Record record {balance_updates consumed_gas : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Transfer_ticket_result.
    Definition Transfer_ticket_result_skeleton := Transfer_ticket_result.record.

    Module Sc_rollup_originate_result.
      Record record {balance_updates address consumed_gas size : Set} : Set := Build {
        balance_updates : balance_updates;
        address : address;
        consumed_gas : consumed_gas;
        size : size;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_address t_consumed_gas t_size} balance_updates
        (r : record t_balance_updates t_address t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_consumed_gas t_size balance_updates
          r.(address) r.(consumed_gas) r.(size).
      Definition with_address
        {t_balance_updates t_address t_consumed_gas t_size} address
        (r : record t_balance_updates t_address t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_consumed_gas t_size
          r.(balance_updates) address r.(consumed_gas) r.(size).
      Definition with_consumed_gas
        {t_balance_updates t_address t_consumed_gas t_size} consumed_gas
        (r : record t_balance_updates t_address t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_consumed_gas t_size
          r.(balance_updates) r.(address) consumed_gas r.(size).
      Definition with_size {t_balance_updates t_address t_consumed_gas t_size}
        size (r : record t_balance_updates t_address t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_consumed_gas t_size
          r.(balance_updates) r.(address) r.(consumed_gas) size.
    End Sc_rollup_originate_result.
    Definition Sc_rollup_originate_result_skeleton :=
      Sc_rollup_originate_result.record.

    Module Sc_rollup_add_messages_result.
      Record record {consumed_gas inbox_after : Set} : Set := Build {
        consumed_gas : consumed_gas;
        inbox_after : inbox_after;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas t_inbox_after} consumed_gas
        (r : record t_consumed_gas t_inbox_after) :=
        Build t_consumed_gas t_inbox_after consumed_gas r.(inbox_after).
      Definition with_inbox_after {t_consumed_gas t_inbox_after} inbox_after
        (r : record t_consumed_gas t_inbox_after) :=
        Build t_consumed_gas t_inbox_after r.(consumed_gas) inbox_after.
    End Sc_rollup_add_messages_result.
    Definition Sc_rollup_add_messages_result_skeleton :=
      Sc_rollup_add_messages_result.record.

    Module Sc_rollup_cement_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Sc_rollup_cement_result.
    Definition Sc_rollup_cement_result_skeleton :=
      Sc_rollup_cement_result.record.

    Module Sc_rollup_publish_result.
      Record record {consumed_gas staked_hash : Set} : Set := Build {
        consumed_gas : consumed_gas;
        staked_hash : staked_hash;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas t_staked_hash} consumed_gas
        (r : record t_consumed_gas t_staked_hash) :=
        Build t_consumed_gas t_staked_hash consumed_gas r.(staked_hash).
      Definition with_staked_hash {t_consumed_gas t_staked_hash} staked_hash
        (r : record t_consumed_gas t_staked_hash) :=
        Build t_consumed_gas t_staked_hash r.(consumed_gas) staked_hash.
    End Sc_rollup_publish_result.
    Definition Sc_rollup_publish_result_skeleton :=
      Sc_rollup_publish_result.record.
  End successful_manager_operation_result.
End ConstructorRecords_successful_manager_operation_result.
Import ConstructorRecords_successful_manager_operation_result.

Reserved Notation "'successful_manager_operation_result.Reveal_result".
Reserved Notation "'successful_manager_operation_result.Origination_result".
Reserved Notation "'successful_manager_operation_result.Delegation_result".
Reserved Notation
  "'successful_manager_operation_result.Register_global_constant_result".
Reserved Notation
  "'successful_manager_operation_result.Set_deposits_limit_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_origination_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_submit_batch_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_commit_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_return_bond_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_finalize_commitment_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_remove_commitment_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_rejection_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result".
Reserved Notation "'successful_manager_operation_result.Transfer_ticket_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_originate_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_add_messages_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_cement_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_publish_result".

Inductive successful_manager_operation_result : Set :=
| Reveal_result :
  'successful_manager_operation_result.Reveal_result
  successful_manager_operation_result
| Transaction_result :
  successful_transaction_result successful_manager_operation_result
| Origination_result :
  'successful_manager_operation_result.Origination_result
  successful_manager_operation_result
| Delegation_result :
  'successful_manager_operation_result.Delegation_result
  successful_manager_operation_result
| Register_global_constant_result :
  'successful_manager_operation_result.Register_global_constant_result
  successful_manager_operation_result
| Set_deposits_limit_result :
  'successful_manager_operation_result.Set_deposits_limit_result
  successful_manager_operation_result
| Tx_rollup_origination_result :
  'successful_manager_operation_result.Tx_rollup_origination_result
  successful_manager_operation_result
| Tx_rollup_submit_batch_result :
  'successful_manager_operation_result.Tx_rollup_submit_batch_result
  successful_manager_operation_result
| Tx_rollup_commit_result :
  'successful_manager_operation_result.Tx_rollup_commit_result
  successful_manager_operation_result
| Tx_rollup_return_bond_result :
  'successful_manager_operation_result.Tx_rollup_return_bond_result
  successful_manager_operation_result
| Tx_rollup_finalize_commitment_result :
  'successful_manager_operation_result.Tx_rollup_finalize_commitment_result
  successful_manager_operation_result
| Tx_rollup_remove_commitment_result :
  'successful_manager_operation_result.Tx_rollup_remove_commitment_result
  successful_manager_operation_result
| Tx_rollup_rejection_result :
  'successful_manager_operation_result.Tx_rollup_rejection_result
  successful_manager_operation_result
| Tx_rollup_dispatch_tickets_result :
  'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result
  successful_manager_operation_result
| Transfer_ticket_result :
  'successful_manager_operation_result.Transfer_ticket_result
  successful_manager_operation_result
| Sc_rollup_originate_result :
  'successful_manager_operation_result.Sc_rollup_originate_result
  successful_manager_operation_result
| Sc_rollup_add_messages_result :
  'successful_manager_operation_result.Sc_rollup_add_messages_result
  successful_manager_operation_result
| Sc_rollup_cement_result :
  'successful_manager_operation_result.Sc_rollup_cement_result
  successful_manager_operation_result
| Sc_rollup_publish_result :
  'successful_manager_operation_result.Sc_rollup_publish_result
  successful_manager_operation_result

where "'successful_manager_operation_result.Reveal_result" :=
  (successful_manager_operation_result.Reveal_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Origination_result" :=
  (successful_manager_operation_result.Origination_result_skeleton
    (option Alpha_context.Lazy_storage.diffs)
    Alpha_context.Receipt.balance_updates (list Alpha_context.Contract.t)
    Alpha_context.Gas.Arith.fp Z.t Z.t)
and "'successful_manager_operation_result.Delegation_result" :=
  (successful_manager_operation_result.Delegation_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Register_global_constant_result" :=
  (successful_manager_operation_result.Register_global_constant_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t
    Script_expr_hash.t)
and "'successful_manager_operation_result.Set_deposits_limit_result" :=
  (successful_manager_operation_result.Set_deposits_limit_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_origination_result" :=
  (successful_manager_operation_result.Tx_rollup_origination_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
    Alpha_context.Tx_rollup.t)
and "'successful_manager_operation_result.Tx_rollup_submit_batch_result" :=
  (successful_manager_operation_result.Tx_rollup_submit_batch_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Tx_rollup_commit_result" :=
  (successful_manager_operation_result.Tx_rollup_commit_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_return_bond_result" :=
  (successful_manager_operation_result.Tx_rollup_return_bond_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_finalize_commitment_result"
  :=
  (successful_manager_operation_result.Tx_rollup_finalize_commitment_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
    Alpha_context.Tx_rollup_level.t)
and "'successful_manager_operation_result.Tx_rollup_remove_commitment_result" :=
  (successful_manager_operation_result.Tx_rollup_remove_commitment_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
    Alpha_context.Tx_rollup_level.t)
and "'successful_manager_operation_result.Tx_rollup_rejection_result" :=
  (successful_manager_operation_result.Tx_rollup_rejection_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result" :=
  (successful_manager_operation_result.Tx_rollup_dispatch_tickets_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Transfer_ticket_result" :=
  (successful_manager_operation_result.Transfer_ticket_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Sc_rollup_originate_result" :=
  (successful_manager_operation_result.Sc_rollup_originate_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Sc_rollup.Address.t
    Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Sc_rollup_add_messages_result" :=
  (successful_manager_operation_result.Sc_rollup_add_messages_result_skeleton
    Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Inbox.t)
and "'successful_manager_operation_result.Sc_rollup_cement_result" :=
  (successful_manager_operation_result.Sc_rollup_cement_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Sc_rollup_publish_result" :=
  (successful_manager_operation_result.Sc_rollup_publish_result_skeleton
    Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Commitment_hash.t).

Module successful_manager_operation_result.
  Include ConstructorRecords_successful_manager_operation_result.successful_manager_operation_result.
  Definition Reveal_result :=
    'successful_manager_operation_result.Reveal_result.
  Definition Origination_result :=
    'successful_manager_operation_result.Origination_result.
  Definition Delegation_result :=
    'successful_manager_operation_result.Delegation_result.
  Definition Register_global_constant_result :=
    'successful_manager_operation_result.Register_global_constant_result.
  Definition Set_deposits_limit_result :=
    'successful_manager_operation_result.Set_deposits_limit_result.
  Definition Tx_rollup_origination_result :=
    'successful_manager_operation_result.Tx_rollup_origination_result.
  Definition Tx_rollup_submit_batch_result :=
    'successful_manager_operation_result.Tx_rollup_submit_batch_result.
  Definition Tx_rollup_commit_result :=
    'successful_manager_operation_result.Tx_rollup_commit_result.
  Definition Tx_rollup_return_bond_result :=
    'successful_manager_operation_result.Tx_rollup_return_bond_result.
  Definition Tx_rollup_finalize_commitment_result :=
    'successful_manager_operation_result.Tx_rollup_finalize_commitment_result.
  Definition Tx_rollup_remove_commitment_result :=
    'successful_manager_operation_result.Tx_rollup_remove_commitment_result.
  Definition Tx_rollup_rejection_result :=
    'successful_manager_operation_result.Tx_rollup_rejection_result.
  Definition Tx_rollup_dispatch_tickets_result :=
    'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.
  Definition Transfer_ticket_result :=
    'successful_manager_operation_result.Transfer_ticket_result.
  Definition Sc_rollup_originate_result :=
    'successful_manager_operation_result.Sc_rollup_originate_result.
  Definition Sc_rollup_add_messages_result :=
    'successful_manager_operation_result.Sc_rollup_add_messages_result.
  Definition Sc_rollup_cement_result :=
    'successful_manager_operation_result.Sc_rollup_cement_result.
  Definition Sc_rollup_publish_result :=
    'successful_manager_operation_result.Sc_rollup_publish_result.
End successful_manager_operation_result.

Definition migration_origination_result_to_successful_manager_operation_result
  (function_parameter : Alpha_context.Migration.origination_result)
  : successful_manager_operation_result :=
  let '{|
    Alpha_context.Migration.origination_result.balance_updates := balance_updates;
      Alpha_context.Migration.origination_result.originated_contracts :=
        originated_contracts;
      Alpha_context.Migration.origination_result.storage_size := storage_size;
      Alpha_context.Migration.origination_result.paid_storage_size_diff :=
        paid_storage_size_diff
      |} := function_parameter in
  Origination_result
    {|
      successful_manager_operation_result.Origination_result.lazy_storage_diff
        := None;
      successful_manager_operation_result.Origination_result.balance_updates :=
        balance_updates;
      successful_manager_operation_result.Origination_result.originated_contracts
        := originated_contracts;
      successful_manager_operation_result.Origination_result.consumed_gas :=
        Alpha_context.Gas.Arith.zero;
      successful_manager_operation_result.Origination_result.storage_size :=
        storage_size;
      successful_manager_operation_result.Origination_result.paid_storage_size_diff
        := paid_storage_size_diff; |}.

Inductive packed_successful_manager_operation_result : Set :=
| Successful_manager_result :
  successful_manager_operation_result
  packed_successful_manager_operation_result.

Definition pack_migration_operation_results
  (results : list Alpha_context.Migration.origination_result)
  : list packed_successful_manager_operation_result :=
  List.map
    (fun (el : Alpha_context.Migration.origination_result) ⇒
      Successful_manager_result
        (migration_origination_result_to_successful_manager_operation_result el))
    results.

Inductive manager_operation_result : Set :=
| Applied : successful_manager_operation_result manager_operation_result
| Backtracked :
  successful_manager_operation_result
  option (Error_monad.trace Error_monad._error) manager_operation_result
| Failed :
  Alpha_context.Kind.manager Error_monad.trace Error_monad._error
  manager_operation_result
| Skipped : Alpha_context.Kind.manager manager_operation_result.

Inductive packed_internal_manager_operation_result : Set :=
| Internal_manager_operation_result :
  internal_contents manager_operation_result
  packed_internal_manager_operation_result.

Definition pack_internal_manager_operation_result
  (internal_op : Script_typed_ir.internal_operation)
  (manager_op : manager_operation_result)
  : packed_internal_manager_operation_result :=
  let internal_op := contents_of_internal_operation internal_op in
  Internal_manager_operation_result internal_op manager_op.

Module Manager_result.
Records for the constructor parameters
  Module ConstructorRecords_case.
    Module case.
      Module MCase.
        Record record {op_case encoding kind select proj inj t : Set} : Set := Build {
          op_case : op_case;
          encoding : encoding;
          kind : kind;
          select : select;
          proj : proj;
          inj : inj;
          t : t;
        }.
        Arguments record : clear implicits.
        Definition with_op_case
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} op_case
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t op_case
            r.(encoding) r.(kind) r.(select) r.(proj) r.(inj) r.(t).
        Definition with_encoding
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} encoding
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) encoding r.(kind) r.(select) r.(proj) r.(inj) r.(t).
        Definition with_kind
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} kind
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) kind r.(select) r.(proj) r.(inj) r.(t).
        Definition with_select
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} select
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) r.(kind) select r.(proj) r.(inj) r.(t).
        Definition with_proj
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} proj
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) r.(kind) r.(select) proj r.(inj) r.(t).
        Definition with_inj
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} inj
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) r.(kind) r.(select) r.(proj) inj r.(t).
        Definition with_t
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} t
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) r.(kind) r.(select) r.(proj) r.(inj) t.
      End MCase.
      Definition MCase_skeleton := MCase.record.
    End case.
  End ConstructorRecords_case.
  Import ConstructorRecords_case.

  Reserved Notation "'case.MCase".

  Inductive case (kind : Set) : Set :=
  | MCase : {a : Set}, 'case.MCase a case kind
  
  where "'case.MCase" :=
    (fun (t_a : Set) ⇒ case.MCase_skeleton
      Alpha_context.Operation.Encoding.Manager_operations.case
      (Data_encoding.t t_a) Alpha_context.Kind.manager
      (packed_successful_manager_operation_result
      option successful_manager_operation_result)
      (successful_manager_operation_result t_a)
      (t_a successful_manager_operation_result)
      (Data_encoding.t manager_operation_result)).

  Module case.
    Include ConstructorRecords_case.case.
    Definition MCase := 'case.MCase.
  End case.

  Arguments MCase {_ _}.

  Definition make {A B : Set}
    (op_case : Alpha_context.Operation.Encoding.Manager_operations.case)
    (encoding : Data_encoding.encoding A)
    (kind_value : Alpha_context.Kind.manager)
    (select :
      packed_successful_manager_operation_result
      option successful_manager_operation_result)
    (proj : successful_manager_operation_result A)
    (inj : A successful_manager_operation_result) : case B :=
    let
      'Alpha_context.Operation.Encoding.Manager_operations.MCase {|
        Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name := name
          |} := op_case in
    let t_value :=
      (let arg :=
        Data_encoding.def
          (Format.asprintf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "operation.alpha.operation_result."
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format))
              "operation.alpha.operation_result.%s") name) in
      fun (eta : Data_encoding.encoding manager_operation_result) ⇒
        arg None None eta)
        (Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
          [
            Data_encoding.case_value "Applied" None (Data_encoding.Tag 0)
              (Data_encoding.merge_objs
                (Data_encoding.obj1
                  (Data_encoding.req None None "status"
                    (Data_encoding.constant
                      "applied")))
                encoding)
              (fun (o_value : manager_operation_result) ⇒
                match o_value with
                | (Skipped _ | Failed _ _ | Backtracked _ _) ⇒
                  None
                | Applied o_value
                  match
                    select
                      (Successful_manager_result
                        o_value)
                    with
                  | NoneNone
                  | Some o_value
                    Some (tt, (proj o_value))
                  end
                end)
              (fun (function_parameter : unit × A) ⇒
                let '(_, x_value) := function_parameter in
                Applied (inj x_value));
            Data_encoding.case_value "Failed" None (Data_encoding.Tag 1)
              (Data_encoding.obj2
                (Data_encoding.req None None "status"
                  (Data_encoding.constant "failed"))
                (Data_encoding.req None None "errors"
                  trace_encoding))
              (fun (function_parameter : manager_operation_result) ⇒
                match function_parameter with
                | Failed _ errsSome (tt, errs)
                | _None
                end)
              (fun (function_parameter :
                unit × Error_monad.trace Error_monad._error) ⇒
                let '(_, errs) := function_parameter in
                Failed kind_value errs);
            Data_encoding.case_value "Skipped" None (Data_encoding.Tag 2)
              (Data_encoding.obj1
                (Data_encoding.req None None "status"
                  (Data_encoding.constant "skipped")))
              (fun (function_parameter : manager_operation_result) ⇒
                match function_parameter with
                | Skipped _Some tt
                | _None
                end)
              (fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                Skipped kind_value);
            Data_encoding.case_value "Backtracked" None (Data_encoding.Tag 3)
              (Data_encoding.merge_objs
                (Data_encoding.obj2
                  (Data_encoding.req None None "status"
                    (Data_encoding.constant
                      "backtracked"))
                  (Data_encoding.opt None None "errors"
                    trace_encoding)) encoding)
              (fun (o_value : manager_operation_result) ⇒
                match o_value with
                | (Skipped _ | Failed _ _ | Applied _) ⇒ None
                | Backtracked o_value errs
                  match
                    select
                      (Successful_manager_result
                        o_value)
                    with
                  | NoneNone
                  | Some o_value
                    Some
                      ((tt, errs),
                        (proj
                          o_value))
                  end
                end)
              (fun (function_parameter :
                (unit ×
                  option
                    (Error_monad.trace
                      Error_monad._error))
                  × A) ⇒
                let '((_, errs), x_value) := function_parameter
                  in
                Backtracked (inj x_value) errs)
          ]) in
    MCase
      {| case.MCase.op_case := op_case; case.MCase.encoding := encoding;
        case.MCase.kind := kind_value; case.MCase.select := select;
        case.MCase.proj := proj; case.MCase.inj := inj; case.MCase.t := t_value;
        |}.

  Definition reveal_case : case Alpha_context.Kind.reveal :=
    make Alpha_context.Operation.Encoding.Manager_operations.reveal_case
      (Data_encoding.obj2
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Reveal_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Reveal_result _) as op) ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Reveal_result {|
            successful_manager_operation_result.Reveal_result.consumed_gas := consumed_gas
              |} ⇒ ((Alpha_context.Gas.Arith.ceil consumed_gas), consumed_gas)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.integral × Alpha_context.Gas.Arith.fp) ⇒
        let '(consumed_gas, consumed_milligas) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Reveal_result
          {|
            successful_manager_operation_result.Reveal_result.consumed_gas :=
              consumed_milligas; |}).

  Definition transaction_contract_variant_cases
    : Data_encoding.encoding successful_transaction_result :=
    Data_encoding.union None
      [
        Data_encoding.case_value "To_contract" None (Data_encoding.Tag 0)
          (Data_encoding.obj9
            (Data_encoding.opt None None "storage"
              Alpha_context.Script.expr_encoding)
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil)
            (Data_encoding.dft None None "originated_contracts"
              (Data_encoding.list_value None
                Alpha_context.Contract.encoding) nil)
            (Data_encoding.dft None None "consumed_gas"
              Alpha_context.Gas.Arith.n_integral_encoding
              Alpha_context.Gas.Arith.zero)
            (Data_encoding.dft None None "consumed_milligas"
              Alpha_context.Gas.Arith.n_fp_encoding
              Alpha_context.Gas.Arith.zero)
            (Data_encoding.dft None None "storage_size"
              Data_encoding.z_value Z.zero)
            (Data_encoding.dft None None "paid_storage_size_diff"
              Data_encoding.z_value Z.zero)
            (Data_encoding.dft None None
              "allocated_destination_contract"
              Data_encoding.bool_value false)
            (Data_encoding.opt None None "lazy_storage_diff"
              Alpha_context.Lazy_storage.encoding))
          (fun (function_parameter : successful_transaction_result) ⇒
            match function_parameter with
            |
              Transaction_to_contract_result {|
                successful_transaction_result.Transaction_to_contract_result.storage :=
                  storage_value;
                  successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
                    :=
                    lazy_storage_diff;
                  successful_transaction_result.Transaction_to_contract_result.balance_updates
                    :=
                    balance_updates;
                  successful_transaction_result.Transaction_to_contract_result.originated_contracts
                    :=
                    originated_contracts;
                  successful_transaction_result.Transaction_to_contract_result.consumed_gas
                    :=
                    consumed_gas;
                  successful_transaction_result.Transaction_to_contract_result.storage_size
                    :=
                    storage_size;
                  successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
                    :=
                    paid_storage_size_diff;
                  successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
                    :=
                    allocated_destination_contract
                  |} ⇒
              Some
                (storage_value, balance_updates,
                  originated_contracts,
                  (Alpha_context.Gas.Arith.ceil consumed_gas),
                  consumed_gas, storage_size,
                  paid_storage_size_diff,
                  allocated_destination_contract,
                  lazy_storage_diff)
            | _None
            end)
          (fun (function_parameter :
            option Alpha_context.Script.expr ×
              Alpha_context.Receipt.balance_updates ×
              list Alpha_context.Contract.t ×
              Alpha_context.Gas.Arith.integral ×
              Alpha_context.Gas.Arith.fp × Z.t × Z.t × bool ×
              option Alpha_context.Lazy_storage.diffs) ⇒
            let
              '(storage_value, balance_updates,
                originated_contracts, consumed_gas,
                consumed_milligas, storage_size,
                paid_storage_size_diff,
                allocated_destination_contract,
                lazy_storage_diff) := function_parameter in
            let '_ :=
              (* ❌ Assert instruction is not handled. *)
              assert unit
                (Alpha_context.Gas.Arith.equal
                  (Alpha_context.Gas.Arith.ceil
                    consumed_milligas) consumed_gas) in
            Transaction_to_contract_result
              {|
                successful_transaction_result.Transaction_to_contract_result.storage
                  := storage_value;
                successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
                  := lazy_storage_diff;
                successful_transaction_result.Transaction_to_contract_result.balance_updates
                  := balance_updates;
                successful_transaction_result.Transaction_to_contract_result.originated_contracts
                  := originated_contracts;
                successful_transaction_result.Transaction_to_contract_result.consumed_gas
                  := consumed_milligas;
                successful_transaction_result.Transaction_to_contract_result.storage_size
                  := storage_size;
                successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
                  := paid_storage_size_diff;
                successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
                  := allocated_destination_contract; |});
        Data_encoding.case_value "To_tx_rollup" None (Data_encoding.Tag 1)
          (Data_encoding.obj5
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil)
            (Data_encoding.dft None None "consumed_gas"
              Alpha_context.Gas.Arith.n_integral_encoding
              Alpha_context.Gas.Arith.zero)
            (Data_encoding.dft None None "consumed_milligas"
              Alpha_context.Gas.Arith.n_fp_encoding
              Alpha_context.Gas.Arith.zero)
            (Data_encoding.req None None "ticket_hash"
              Alpha_context.Ticket_hash.encoding)
            (Data_encoding.req None None "paid_storage_size_diff"
              Data_encoding.n_value))
          (fun (function_parameter : successful_transaction_result) ⇒
            match function_parameter with
            |
              Transaction_to_tx_rollup_result {|
                successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
                  := ticket_hash;
                  successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
                    :=
                    balance_updates;
                  successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
                    :=
                    consumed_gas;
                  successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
                    :=
                    paid_storage_size_diff
                  |} ⇒
              Some
                (balance_updates,
                  (Alpha_context.Gas.Arith.ceil consumed_gas),
                  consumed_gas, ticket_hash,
                  paid_storage_size_diff)
            | _None
            end)
          (fun (function_parameter :
            Alpha_context.Receipt.balance_updates ×
              Alpha_context.Gas.Arith.integral ×
              Alpha_context.Gas.Arith.fp ×
              Alpha_context.Ticket_hash.t × Z.t) ⇒
            let
              '(balance_updates, consumed_gas, consumed_milligas,
                ticket_hash, paid_storage_size_diff) :=
              function_parameter in
            let '_ :=
              (* ❌ Assert instruction is not handled. *)
              assert unit
                (Alpha_context.Gas.Arith.equal
                  (Alpha_context.Gas.Arith.ceil
                    consumed_milligas) consumed_gas) in
            Transaction_to_tx_rollup_result
              {|
                successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
                  := ticket_hash;
                successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
                  := balance_updates;
                successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
                  := consumed_milligas;
                successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
                  := paid_storage_size_diff; |})
      ].

  Definition transaction_case : case Alpha_context.Kind.transaction :=
    make Alpha_context.Operation.Encoding.Manager_operations.transaction_case
      transaction_contract_variant_cases
      Alpha_context.Kind.Transaction_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Transaction_result _) as op) ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        | Transaction_result x_valuex_value
        | _unreachable_gadt_branch
        end)
      (fun (x_value : successful_transaction_result) ⇒
        Transaction_result x_value).

  Definition origination_case : case Alpha_context.Kind.origination :=
    make Alpha_context.Operation.Encoding.Manager_operations.origination_case
      (Data_encoding.obj7
        (Data_encoding.dft None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding nil)
        (Data_encoding.dft None None "originated_contracts"
          (Data_encoding.list_value None Alpha_context.Contract.encoding) nil)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "storage_size" Data_encoding.z_value Z.zero)
        (Data_encoding.dft None None "paid_storage_size_diff"
          Data_encoding.z_value Z.zero)
        (Data_encoding.opt None None "lazy_storage_diff"
          Alpha_context.Lazy_storage.encoding))
      Alpha_context.Kind.Origination_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Origination_result _) as op) ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Origination_result {|
            successful_manager_operation_result.Origination_result.lazy_storage_diff :=
              lazy_storage_diff;
              successful_manager_operation_result.Origination_result.balance_updates
                := balance_updates;
              successful_manager_operation_result.Origination_result.originated_contracts
                := originated_contracts;
              successful_manager_operation_result.Origination_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Origination_result.storage_size
                := storage_size;
              successful_manager_operation_result.Origination_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒
          (balance_updates, originated_contracts,
            (Alpha_context.Gas.Arith.ceil consumed_gas), consumed_gas,
            storage_size, paid_storage_size_diff, lazy_storage_diff)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × list Alpha_context.Contract.t ×
          Alpha_context.Gas.Arith.integral × Alpha_context.Gas.Arith.fp × Z.t ×
          Z.t × option Alpha_context.Lazy_storage.diffs) ⇒
        let
          '(balance_updates, originated_contracts, consumed_gas,
            consumed_milligas, storage_size, paid_storage_size_diff,
            lazy_storage_diff) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Origination_result
          {|
            successful_manager_operation_result.Origination_result.lazy_storage_diff
              := lazy_storage_diff;
            successful_manager_operation_result.Origination_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Origination_result.originated_contracts
              := originated_contracts;
            successful_manager_operation_result.Origination_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Origination_result.storage_size
              := storage_size;
            successful_manager_operation_result.Origination_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition register_global_constant_case
    : case Alpha_context.Kind.register_global_constant :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.register_global_constant_case
      (Data_encoding.obj5
        (Data_encoding.dft None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding nil)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "storage_size" Data_encoding.z_value Z.zero)
        (Data_encoding.req None None "global_address" Script_expr_hash.encoding))
      Alpha_context.Kind.Register_global_constant_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Register_global_constant_result _) as op)
          ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Register_global_constant_result {|
            successful_manager_operation_result.Register_global_constant_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Register_global_constant_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Register_global_constant_result.size_of_constant
                := size_of_constant;
              successful_manager_operation_result.Register_global_constant_result.global_address
                := global_address
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas, size_of_constant, global_address)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp × Z.t × Script_expr_hash.t) ⇒
        let
          '(balance_updates, consumed_gas, consumed_milligas, size_of_constant,
            global_address) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Register_global_constant_result
          {|
            successful_manager_operation_result.Register_global_constant_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Register_global_constant_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Register_global_constant_result.size_of_constant
              := size_of_constant;
            successful_manager_operation_result.Register_global_constant_result.global_address
              := global_address; |}).

  Definition delegation_case : case Alpha_context.Kind.delegation :=
    make Alpha_context.Operation.Encoding.Manager_operations.delegation_case
      (Data_encoding.obj2
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Delegation_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Delegation_result _) as op) ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Delegation_result {|
            successful_manager_operation_result.Delegation_result.consumed_gas :=
              consumed_gas
              |} ⇒ ((Alpha_context.Gas.Arith.ceil consumed_gas), consumed_gas)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.integral × Alpha_context.Gas.Arith.fp) ⇒
        let '(consumed_gas, consumed_milligas) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Delegation_result
          {|
            successful_manager_operation_result.Delegation_result.consumed_gas
              := consumed_milligas; |}).

  Definition set_deposits_limit_case
    : case Alpha_context.Kind.set_deposits_limit :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.set_deposits_limit_case
      (Data_encoding.obj2
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Set_deposits_limit_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Set_deposits_limit_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Set_deposits_limit_result {|
            successful_manager_operation_result.Set_deposits_limit_result.consumed_gas :=
              consumed_gas
              |} ⇒ ((Alpha_context.Gas.Arith.ceil consumed_gas), consumed_gas)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.integral × Alpha_context.Gas.Arith.fp) ⇒
        let '(consumed_gas, consumed_milligas) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Set_deposits_limit_result
          {|
            successful_manager_operation_result.Set_deposits_limit_result.consumed_gas
              := consumed_milligas; |}).

  Definition tx_rollup_origination_case
    : case Alpha_context.Kind.tx_rollup_origination :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_origination_case
      (Data_encoding.obj4
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "originated_rollup"
          Alpha_context.Tx_rollup.encoding))
      Alpha_context.Kind.Tx_rollup_origination_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_origination_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_origination_result {|
            successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
                := originated_tx_rollup
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas, originated_tx_rollup)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp × Alpha_context.Tx_rollup.tx_rollup) ⇒
        let
          '(balance_updates, consumed_gas, consumed_milligas,
            originated_tx_rollup) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Tx_rollup_origination_result
          {|
            successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
              := originated_tx_rollup; |}).

  Definition tx_rollup_submit_batch_case
    : case Alpha_context.Kind.tx_rollup_submit_batch :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_submit_batch_case
      (Data_encoding.obj4
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "paid_storage_size_diff"
          Data_encoding.n_value))
      Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_submit_batch_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_submit_batch_result {|
            successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas, paid_storage_size_diff)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp × Z.t) ⇒
        let
          '(balance_updates, consumed_gas, consumed_milligas,
            paid_storage_size_diff) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Tx_rollup_submit_batch_result
          {|
            successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition tx_rollup_commit_case : case Alpha_context.Kind.tx_rollup_commit :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_commit_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Tx_rollup_commit_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_commit_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_commit_result {|
            successful_manager_operation_result.Tx_rollup_commit_result.balance_updates :=
              balance_updates;
              successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
                := consumed_gas
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp) ⇒
        let '(balance_updates, consumed_gas, consumed_milligas) :=
          function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Tx_rollup_commit_result
          {|
            successful_manager_operation_result.Tx_rollup_commit_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
              := consumed_milligas; |}).

  Definition tx_rollup_return_bond_case
    : case Alpha_context.Kind.tx_rollup_return_bond :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_return_bond_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Tx_rollup_return_bond_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_return_bond_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_return_bond_result {|
            successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
                := consumed_gas
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp) ⇒
        let '(balance_updates, consumed_gas, consumed_milligas) :=
          function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Tx_rollup_return_bond_result
          {|
            successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
              := consumed_milligas; |}).

  Definition tx_rollup_finalize_commitment_case
    : case Alpha_context.Kind.tx_rollup_finalize_commitment :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_finalize_commitment_case
      (Data_encoding.obj4
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "level"
          Alpha_context.Tx_rollup_level.encoding))
      Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Successful_manager_result
            ((Tx_rollup_finalize_commitment_result _) as op) ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_finalize_commitment_result {|
            successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
                := level
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas, level)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp × Alpha_context.Tx_rollup_level.t) ⇒
        let '(balance_updates, consumed_gas, consumed_milligas, level) :=
          function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Tx_rollup_finalize_commitment_result
          {|
            successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
              := level; |}).

  Definition tx_rollup_remove_commitment_case
    : case Alpha_context.Kind.tx_rollup_remove_commitment :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_remove_commitment_case
      (Data_encoding.obj4
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "level"
          Alpha_context.Tx_rollup_level.encoding))
      Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Successful_manager_result
            ((Tx_rollup_remove_commitment_result _) as op) ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_remove_commitment_result {|
            successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
                := level
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas, level)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp × Alpha_context.Tx_rollup_level.t) ⇒
        let '(balance_updates, consumed_gas, consumed_milligas, level) :=
          function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Tx_rollup_remove_commitment_result
          {|
            successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
              := level; |}).

  Definition tx_rollup_rejection_case
    : case Alpha_context.Kind.tx_rollup_rejection :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_rejection_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Tx_rollup_rejection_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_rejection_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_rejection_result {|
            successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
                := consumed_gas
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp) ⇒
        let '(balance_updates, consumed_gas, consumed_milligas) :=
          function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Tx_rollup_rejection_result
          {|
            successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
              := consumed_milligas; |}).

  Definition tx_rollup_dispatch_tickets_case
    : case Alpha_context.Kind.tx_rollup_dispatch_tickets :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_dispatch_tickets_case
      (Data_encoding.obj4
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "paid_storage_size_diff"
          Data_encoding.z_value Z.zero))
      Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Successful_manager_result
            ((Tx_rollup_dispatch_tickets_result _) as op) ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_dispatch_tickets_result {|
            successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas, paid_storage_size_diff)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp × Z.t) ⇒
        let
          '(balance_updates, consumed_gas, consumed_milligas,
            paid_storage_size_diff) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Tx_rollup_dispatch_tickets_result
          {|
            successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition transfer_ticket_case : case Alpha_context.Kind.transfer_ticket :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.transfer_ticket_case
      (Data_encoding.obj4
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "paid_storage_size_diff"
          Data_encoding.z_value Z.zero))
      Alpha_context.Kind.Transfer_ticket_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Transfer_ticket_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Transfer_ticket_result {|
            successful_manager_operation_result.Transfer_ticket_result.balance_updates :=
              balance_updates;
              successful_manager_operation_result.Transfer_ticket_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒
          (balance_updates, (Alpha_context.Gas.Arith.ceil consumed_gas),
            consumed_gas, paid_storage_size_diff)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.integral
          × Alpha_context.Gas.Arith.fp × Z.t) ⇒
        let
          '(balance_updates, consumed_gas, consumed_milligas,
            paid_storage_size_diff) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Transfer_ticket_result
          {|
            successful_manager_operation_result.Transfer_ticket_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Transfer_ticket_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition sc_rollup_originate_case
    : case Alpha_context.Kind.sc_rollup_originate :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_originate_case
      (Data_encoding.obj5
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.req None None "address"
          Alpha_context.Sc_rollup.Address.encoding)
        (Data_encoding.dft None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding
          Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "size" Data_encoding.z_value))
      Alpha_context.Kind.Sc_rollup_originate_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_originate_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_originate_result {|
            successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Sc_rollup_originate_result.address
                := address;
              successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Sc_rollup_originate_result.size
                := size_value
              |} ⇒
          (balance_updates, address,
            (Alpha_context.Gas.Arith.ceil consumed_gas), consumed_gas,
            size_value)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates ×
          Alpha_context.Sc_rollup.Address.t × Alpha_context.Gas.Arith.integral ×
          Alpha_context.Gas.Arith.fp × Z.t) ⇒
        let
          '(balance_updates, address, consumed_gas, consumed_milligas,
            size_value) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Sc_rollup_originate_result
          {|
            successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Sc_rollup_originate_result.address
              := address;
            successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Sc_rollup_originate_result.size
              := size_value; |}).

  Definition sc_rollup_add_messages_case
    : case Alpha_context.Kind.sc_rollup_add_messages :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_add_messages_case
      (Data_encoding.obj3
        (Data_encoding.req None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "inbox_after"
          Alpha_context.Sc_rollup.Inbox.encoding))
      Alpha_context.Kind.Sc_rollup_add_messages_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_add_messages_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_add_messages_result {|
            successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
              := consumed_gas;
              successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
                := inbox_after
              |} ⇒
          ((Alpha_context.Gas.Arith.ceil consumed_gas), consumed_gas,
            inbox_after)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.integral × Alpha_context.Gas.Arith.fp ×
          Alpha_context.Sc_rollup.Inbox.t) ⇒
        let '(consumed_gas, consumed_milligas, inbox_after) :=
          function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Sc_rollup_add_messages_result
          {|
            successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
              := inbox_after; |}).

  Definition sc_rollup_cement_case : case Alpha_context.Kind.sc_rollup_cement :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_cement_case
      (Data_encoding.obj2
        (Data_encoding.req None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Sc_rollup_cement_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_cement_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_cement_result {|
            successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas :=
              consumed_gas
              |} ⇒ ((Alpha_context.Gas.Arith.ceil consumed_gas), consumed_gas)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.integral × Alpha_context.Gas.Arith.fp) ⇒
        let '(consumed_gas, consumed_milligas) := function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Sc_rollup_cement_result
          {|
            successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas
              := consumed_milligas; |}).

  Definition sc_rollup_publish_case
    : case Alpha_context.Kind.sc_rollup_publish :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_publish_case
      (Data_encoding.obj3
        (Data_encoding.req None None "consumed_gas"
          Alpha_context.Gas.Arith.n_integral_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "staked_hash"
          Alpha_context.Sc_rollup.Commitment_hash.encoding))
      Alpha_context.Kind.Sc_rollup_publish_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_publish_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_publish_result {|
            successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas :=
              consumed_gas;
              successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
                := staked_hash
              |} ⇒
          ((Alpha_context.Gas.Arith.ceil consumed_gas), consumed_gas,
            staked_hash)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.integral × Alpha_context.Gas.Arith.fp ×
          Alpha_context.Sc_rollup.Commitment_hash.t) ⇒
        let '(consumed_gas, consumed_milligas, staked_hash) :=
          function_parameter in
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit
            (Alpha_context.Gas.Arith.equal
              (Alpha_context.Gas.Arith.ceil consumed_milligas) consumed_gas) in
        Sc_rollup_publish_result
          {|
            successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas
              := consumed_milligas;
            successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
              := staked_hash; |}).
End Manager_result.

Definition iselect : Set :=
  packed_internal_manager_operation_result
  option (internal_contents × manager_operation_result).

Module Internal_result.
Records for the constructor parameters
  Module ConstructorRecords_case.
    Module case.
      Module MCase.
        Record record {tag name encoding iselect select proj inj : Set} : Set := Build {
          tag : tag;
          name : name;
          encoding : encoding;
          iselect : iselect;
          select : select;
          proj : proj;
          inj : inj;
        }.
        Arguments record : clear implicits.
        Definition with_tag
          {t_tag t_name t_encoding t_iselect t_select t_proj t_inj} tag
          (r : record t_tag t_name t_encoding t_iselect t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_iselect t_select t_proj t_inj tag
            r.(name) r.(encoding) r.(iselect) r.(select) r.(proj) r.(inj).
        Definition with_name
          {t_tag t_name t_encoding t_iselect t_select t_proj t_inj} name
          (r : record t_tag t_name t_encoding t_iselect t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_iselect t_select t_proj t_inj r.(tag)
            name r.(encoding) r.(iselect) r.(select) r.(proj) r.(inj).
        Definition with_encoding
          {t_tag t_name t_encoding t_iselect t_select t_proj t_inj} encoding
          (r : record t_tag t_name t_encoding t_iselect t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_iselect t_select t_proj t_inj r.(tag)
            r.(name) encoding r.(iselect) r.(select) r.(proj) r.(inj).
        Definition with_iselect
          {t_tag t_name t_encoding t_iselect t_select t_proj t_inj} iselect
          (r : record t_tag t_name t_encoding t_iselect t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_iselect t_select t_proj t_inj r.(tag)
            r.(name) r.(encoding) iselect r.(select) r.(proj) r.(inj).
        Definition with_select
          {t_tag t_name t_encoding t_iselect t_select t_proj t_inj} select
          (r : record t_tag t_name t_encoding t_iselect t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_iselect t_select t_proj t_inj r.(tag)
            r.(name) r.(encoding) r.(iselect) select r.(proj) r.(inj).
        Definition with_proj
          {t_tag t_name t_encoding t_iselect t_select t_proj t_inj} proj
          (r : record t_tag t_name t_encoding t_iselect t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_iselect t_select t_proj t_inj r.(tag)
            r.(name) r.(encoding) r.(iselect) r.(select) proj r.(inj).
        Definition with_inj
          {t_tag t_name t_encoding t_iselect t_select t_proj t_inj} inj
          (r : record t_tag t_name t_encoding t_iselect t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_iselect t_select t_proj t_inj r.(tag)
            r.(name) r.(encoding) r.(iselect) r.(select) r.(proj) inj.
      End MCase.
      Definition MCase_skeleton := MCase.record.
    End case.
  End ConstructorRecords_case.
  Import ConstructorRecords_case.

  Reserved Notation "'case.MCase".

  Inductive case : Set :=
  | MCase : {a : Set}, 'case.MCase a case
  
  where "'case.MCase" :=
    (fun (t_a : Set) ⇒ case.MCase_skeleton int string (Data_encoding.t t_a)
      iselect
      (packed_internal_manager_operation option internal_manager_operation)
      (internal_manager_operation t_a) (t_a internal_manager_operation)).

  Module case.
    Include ConstructorRecords_case.case.
    Definition MCase := 'case.MCase.
  End case.

  Definition transaction_case : case :=
    MCase
      {|
        case.MCase.tag :=
          Alpha_context.Operation.Encoding.Manager_operations.transaction_tag;
        case.MCase.name := "transaction";
        case.MCase.encoding :=
          Data_encoding.obj3
            (Data_encoding.req None None "amount" Alpha_context.Tez.encoding)
            (Data_encoding.req None None "destination"
              Alpha_context.Destination.encoding)
            (Data_encoding.opt None None "parameters"
              (Data_encoding.obj2
                (Data_encoding.req None None "entrypoint"
                  Alpha_context.Entrypoint.smart_encoding)
                (Data_encoding.req None None "value"
                  Alpha_context.Script.lazy_expr_encoding)));
        case.MCase.iselect :=
          fun (function_parameter : packed_internal_manager_operation_result) ⇒
            match function_parameter with
            |
              Internal_manager_operation_result
                ({| internal_contents.operation := Transaction _ |} as op) res
              ⇒ Some (op, res)
            | _None
            end;
        case.MCase.select :=
          fun (function_parameter : packed_internal_manager_operation) ⇒
            match function_parameter with
            | Manager ((Transaction _) as op) ⇒ Some op
            | _None
            end;
        case.MCase.proj :=
          fun (function_parameter : internal_manager_operation) ⇒
            match function_parameter with
            |
              Transaction {|
                Alpha_context.transaction.amount := amount;
                  Alpha_context.transaction.parameters := parameters;
                  Alpha_context.transaction.entrypoint := entrypoint;
                  Alpha_context.transaction.destination := destination
                  |} ⇒
              let parameters :=
                if
                  (Script_repr.is_unit_parameter parameters) &&
                  (Alpha_context.Entrypoint.is_default entrypoint)
                then
                  None
                else
                  Some (entrypoint, parameters) in
              (amount, destination, parameters)
            | _unreachable_gadt_branch
            end;
        case.MCase.inj :=
          fun (function_parameter :
            Alpha_context.Tez.t × Alpha_context.Destination.t ×
              option
                (Alpha_context.Entrypoint.t × Alpha_context.Script.lazy_expr))
            ⇒
            let '(amount, destination, parameters) := function_parameter in
            let '(entrypoint, parameters) :=
              match parameters with
              | None
                (Alpha_context.Entrypoint.default,
                  Alpha_context.Script.unit_parameter)
              | Some (entrypoint, value_value)(entrypoint, value_value)
              end in
            Transaction
              {| Alpha_context.transaction.amount := amount;
                Alpha_context.transaction.parameters := parameters;
                Alpha_context.transaction.entrypoint := entrypoint;
                Alpha_context.transaction.destination := destination; |}; |}.

  Definition origination_case : case :=
    MCase
      {|
        case.MCase.tag :=
          Alpha_context.Operation.Encoding.Manager_operations.origination_tag;
        case.MCase.name := "origination";
        case.MCase.encoding :=
          Data_encoding.obj3
            (Data_encoding.req None None "balance" Alpha_context.Tez.encoding)
            (Data_encoding.opt None None "delegate"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "script" Alpha_context.Script.encoding);
        case.MCase.iselect :=
          fun (function_parameter : packed_internal_manager_operation_result) ⇒
            match function_parameter with
            |
              Internal_manager_operation_result
                ({| internal_contents.operation := Origination _ |} as op) res
              ⇒ Some (op, res)
            | _None
            end;
        case.MCase.select :=
          fun (function_parameter : packed_internal_manager_operation) ⇒
            match function_parameter with
            | Manager ((Origination _) as op) ⇒ Some op
            | _None
            end;
        case.MCase.proj :=
          fun (function_parameter : internal_manager_operation) ⇒
            match function_parameter with
            |
              Origination {|
                Alpha_context.origination.delegate := delegate;
                  Alpha_context.origination.script := script;
                  Alpha_context.origination.credit := credit
                  |} ⇒ (credit, delegate, script)
            | _unreachable_gadt_branch
            end;
        case.MCase.inj :=
          fun (function_parameter :
            Alpha_context.Tez.t × option Signature.public_key_hash ×
              Alpha_context.Script.t) ⇒
            let '(credit, delegate, script) := function_parameter in
            Origination
              {| Alpha_context.origination.delegate := delegate;
                Alpha_context.origination.script := script;
                Alpha_context.origination.credit := credit; |}; |}.

  Definition delegation_case : case :=
    MCase
      {|
        case.MCase.tag :=
          Alpha_context.Operation.Encoding.Manager_operations.delegation_tag;
        case.MCase.name := "delegation";
        case.MCase.encoding :=
          Data_encoding.obj1
            (Data_encoding.opt None None "delegate"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding));
        case.MCase.iselect :=
          fun (function_parameter : packed_internal_manager_operation_result) ⇒
            match function_parameter with
            |
              Internal_manager_operation_result
                ({| internal_contents.operation := Delegation _ |} as op) res
              Some (op, res)
            | _None
            end;
        case.MCase.select :=
          fun (function_parameter : packed_internal_manager_operation) ⇒
            match function_parameter with
            | Manager ((Delegation _) as op) ⇒ Some op
            | _None
            end;
        case.MCase.proj :=
          fun (function_parameter : internal_manager_operation) ⇒
            match function_parameter with
            | Delegation key_valuekey_value
            | _unreachable_gadt_branch
            end;
        case.MCase.inj :=
          fun (key_value : option Signature.public_key_hash) ⇒
            Delegation key_value; |}.

  Definition case_value {A B : Set}
    (tag : Data_encoding.case_tag) (name : string)
    (args : Data_encoding.encoding A) (proj : B option A) (inj : A B)
    : Data_encoding.case B :=
    Data_encoding.case_value (String.capitalize_ascii name) None tag
      (Data_encoding.merge_objs
        (Data_encoding.obj1
          (Data_encoding.req None None "kind" (Data_encoding.constant name)))
        args)
      (fun (x_value : B) ⇒
        match proj x_value with
        | NoneNone
        | Some x_valueSome (tt, x_value)
        end)
      (fun (function_parameter : unit × A) ⇒
        let '(_, x_value) := function_parameter in
        inj x_value).

  Definition encoding
    : Data_encoding.encoding packed_internal_manager_operation :=
    let make (m_case : case)
      : Data_encoding.case packed_internal_manager_operation :=
      let
        'MCase {|
          case.MCase.tag := tag;
            case.MCase.name := name;
            case.MCase.encoding := encoding;
            case.MCase.iselect := _;
            case.MCase.select := select;
            case.MCase.proj := proj;
            case.MCase.inj := inj
            |} := m_case in
      let 'existT _ __MCase_'a [inj, proj, select, encoding, name, tag] :=
        existT (A := Set)
          (fun __MCase_'a
            [__MCase_'a internal_manager_operation **
              internal_manager_operation __MCase_'a **
              packed_internal_manager_operation
              option internal_manager_operation ** Data_encoding.t __MCase_'a **
              string ** int]) _ [inj, proj, select, encoding, name, tag] in
      case_value (Data_encoding.Tag tag) name encoding
        (fun (o_value : packed_internal_manager_operation) ⇒
          match select o_value with
          | NoneNone
          | Some o_valueSome (proj o_value)
          end) (fun (x_value : __MCase_'a) ⇒ Manager (inj x_value)) in
    Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
      [ make transaction_case; make origination_case; make delegation_case ].
End Internal_result.

Definition internal_contents_encoding
  : Data_encoding.t packed_internal_contents :=
  (let arg := Data_encoding.def "apply_results.alpha.internal_operation_result"
    in
  fun (eta : Data_encoding.encoding packed_internal_contents) ⇒
    arg None None eta)
    (Data_encoding.conv
      (fun (function_parameter : packed_internal_contents) ⇒
        let
          'Internal_contents {|
            internal_contents.source := source;
              internal_contents.operation := operation;
              internal_contents.nonce := nonce_value
              |} := function_parameter in
        ((source, nonce_value), (Manager operation)))
      (fun (function_parameter :
        (Alpha_context.Contract.contract × int) ×
          packed_internal_manager_operation) ⇒
        let '((source, nonce_value), Manager operation) := function_parameter in
        Internal_contents
          {| internal_contents.source := source;
            internal_contents.operation := operation;
            internal_contents.nonce := nonce_value; |}) None
      (Data_encoding.merge_objs
        (Data_encoding.obj2
          (Data_encoding.req None None "source" Alpha_context.Contract.encoding)
          (Data_encoding.req None None "nonce" Data_encoding.uint16))
        Internal_result.encoding)).

Definition internal_manager_operation_result_encoding
  : Data_encoding.t packed_internal_manager_operation_result :=
  let make {kind : Set} (function_parameter : Manager_result.case kind)
    : Internal_result.case
    Data_encoding.case packed_internal_manager_operation_result :=
    let 'Manager_result.MCase res_case := function_parameter in
    fun (ires_case : Internal_result.case) ⇒
      let 'Alpha_context.Operation.Encoding.Manager_operations.MCase op_case :=
        res_case.(Manager_result.case.MCase.op_case) in
      let 'Internal_result.MCase ires_case := ires_case in
      let 'existT _ __MCase_'a2 ires_case :=
        existT (A := Set)
          (fun __MCase_'a2Internal_result.case.MCase __MCase_'a2) _
          ires_case in
      Data_encoding.case_value
        op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name)
        None
        (Data_encoding.Tag
          op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.tag))
        (Data_encoding.merge_objs
          (Data_encoding.obj3
            (Data_encoding.req None None "kind"
              (Data_encoding.constant
                op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name)))
            (Data_encoding.req None None "source"
              Alpha_context.Contract.encoding)
            (Data_encoding.req None None "nonce" Data_encoding.uint16))
          (Data_encoding.merge_objs
            ires_case.(Internal_result.case.MCase.encoding)
            (Data_encoding.obj1
              (Data_encoding.req None None "result"
                res_case.(Manager_result.case.MCase.t)))))
        (fun (op : packed_internal_manager_operation_result) ⇒
          match ires_case.(Internal_result.case.MCase.iselect) op with
          | Some (op, res)
            Some
              ((tt, op.(internal_contents.source), op.(internal_contents.nonce)),
                ((ires_case.(Internal_result.case.MCase.proj)
                  op.(internal_contents.operation)), res))
          | NoneNone
          end)
        (fun (function_parameter :
          (unit × Alpha_context.Contract.t × int) ×
            (__MCase_'a2 × manager_operation_result)) ⇒
          let '((_, source, nonce_value), (op, res)) := function_parameter in
          let op :=
            {| internal_contents.source := source;
              internal_contents.operation :=
                ires_case.(Internal_result.case.MCase.inj) op;
              internal_contents.nonce := nonce_value; |} in
          Internal_manager_operation_result op res) in
  (let arg := Data_encoding.def "apply_results.alpha.operation_result" in
  fun (eta : Data_encoding.encoding packed_internal_manager_operation_result) ⇒
    arg None None eta)
    (Data_encoding.union None
      [
        make Manager_result.transaction_case Internal_result.transaction_case;
        make Manager_result.origination_case Internal_result.origination_case;
        make Manager_result.delegation_case Internal_result.delegation_case
      ]).

Definition successful_manager_operation_result_encoding
  : Data_encoding.t packed_successful_manager_operation_result :=
  let make {kind : Set} (mcase : Manager_result.case kind)
    : Data_encoding.case packed_successful_manager_operation_result :=
    let 'Manager_result.MCase res_case := mcase in
    let 'existT _ __MCase_'a res_case :=
      existT (A := Set) (fun __MCase_'aManager_result.case.MCase __MCase_'a)
        _ res_case in
    let 'Alpha_context.Operation.Encoding.Manager_operations.MCase op_case :=
      res_case.(Manager_result.case.MCase.op_case) in
    Data_encoding.case_value
      op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name)
      None
      (Data_encoding.Tag
        op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.tag))
      (Data_encoding.merge_objs
        (Data_encoding.obj1
          (Data_encoding.req None None "kind"
            (Data_encoding.constant
              op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name))))
        res_case.(Manager_result.case.MCase.encoding))
      (fun (res : packed_successful_manager_operation_result) ⇒
        match res_case.(Manager_result.case.MCase.select) res with
        | Some resSome (tt, (res_case.(Manager_result.case.MCase.proj) res))
        | NoneNone
        end)
      (fun (function_parameter : unit × __MCase_'a) ⇒
        let '(_, res) := function_parameter in
        Successful_manager_result (res_case.(Manager_result.case.MCase.inj) res))
    in
  (let arg :=
    Data_encoding.def "operation.alpha.successful_manager_operation_result" in
  fun (eta : Data_encoding.encoding packed_successful_manager_operation_result)
    ⇒ arg None None eta)
    (Data_encoding.union None
      [
        make Manager_result.reveal_case;
        make Manager_result.transaction_case;
        make Manager_result.origination_case;
        make Manager_result.delegation_case;
        make Manager_result.set_deposits_limit_case;
        make Manager_result.sc_rollup_originate_case
      ]).

Records for the constructor parameters
Module ConstructorRecords_contents_result.
  Module contents_result.
    Module Preendorsement_result.
      Record record {balance_updates delegate preendorsement_power : Set} : Set := Build {
        balance_updates : balance_updates;
        delegate : delegate;
        preendorsement_power : preendorsement_power;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_delegate t_preendorsement_power} balance_updates
        (r : record t_balance_updates t_delegate t_preendorsement_power) :=
        Build t_balance_updates t_delegate t_preendorsement_power
          balance_updates r.(delegate) r.(preendorsement_power).
      Definition with_delegate
        {t_balance_updates t_delegate t_preendorsement_power} delegate
        (r : record t_balance_updates t_delegate t_preendorsement_power) :=
        Build t_balance_updates t_delegate t_preendorsement_power
          r.(balance_updates) delegate r.(preendorsement_power).
      Definition with_preendorsement_power
        {t_balance_updates t_delegate t_preendorsement_power}
        preendorsement_power
        (r : record t_balance_updates t_delegate t_preendorsement_power) :=
        Build t_balance_updates t_delegate t_preendorsement_power
          r.(balance_updates) r.(delegate) preendorsement_power.
    End Preendorsement_result.
    Definition Preendorsement_result_skeleton := Preendorsement_result.record.

    Module Endorsement_result.
      Record record {balance_updates delegate endorsement_power : Set} : Set := Build {
        balance_updates : balance_updates;
        delegate : delegate;
        endorsement_power : endorsement_power;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_delegate t_endorsement_power} balance_updates
        (r : record t_balance_updates t_delegate t_endorsement_power) :=
        Build t_balance_updates t_delegate t_endorsement_power balance_updates
          r.(delegate) r.(endorsement_power).
      Definition with_delegate
        {t_balance_updates t_delegate t_endorsement_power} delegate
        (r : record t_balance_updates t_delegate t_endorsement_power) :=
        Build t_balance_updates t_delegate t_endorsement_power
          r.(balance_updates) delegate r.(endorsement_power).
      Definition with_endorsement_power
        {t_balance_updates t_delegate t_endorsement_power} endorsement_power
        (r : record t_balance_updates t_delegate t_endorsement_power) :=
        Build t_balance_updates t_delegate t_endorsement_power
          r.(balance_updates) r.(delegate) endorsement_power.
    End Endorsement_result.
    Definition