Skip to main content

🏗️ Apply_internal_results.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Records for the constructor parameters
Module ConstructorRecords_internal_operation_contents.
  Module internal_operation_contents.
    Module Transaction.
      Record record {amount parameters entrypoint destination : Set} : Set := Build {
        amount : amount;
        parameters : parameters;
        entrypoint : entrypoint;
        destination : destination;
      }.
      Arguments record : clear implicits.
      Definition with_amount {t_amount t_parameters t_entrypoint t_destination}
        amount (r : record t_amount t_parameters t_entrypoint t_destination) :=
        Build t_amount t_parameters t_entrypoint t_destination amount
          r.(parameters) r.(entrypoint) r.(destination).
      Definition with_parameters
        {t_amount t_parameters t_entrypoint t_destination} parameters
        (r : record t_amount t_parameters t_entrypoint t_destination) :=
        Build t_amount t_parameters t_entrypoint t_destination r.(amount)
          parameters r.(entrypoint) r.(destination).
      Definition with_entrypoint
        {t_amount t_parameters t_entrypoint t_destination} entrypoint
        (r : record t_amount t_parameters t_entrypoint t_destination) :=
        Build t_amount t_parameters t_entrypoint t_destination r.(amount)
          r.(parameters) entrypoint r.(destination).
      Definition with_destination
        {t_amount t_parameters t_entrypoint t_destination} destination
        (r : record t_amount t_parameters t_entrypoint t_destination) :=
        Build t_amount t_parameters t_entrypoint t_destination r.(amount)
          r.(parameters) r.(entrypoint) destination.
    End Transaction.
    Definition Transaction_skeleton := Transaction.record.

    Module Origination.
      Record record {delegate script credit : Set} : Set := Build {
        delegate : delegate;
        script : script;
        credit : credit;
      }.
      Arguments record : clear implicits.
      Definition with_delegate {t_delegate t_script t_credit} delegate
        (r : record t_delegate t_script t_credit) :=
        Build t_delegate t_script t_credit delegate r.(script) r.(credit).
      Definition with_script {t_delegate t_script t_credit} script
        (r : record t_delegate t_script t_credit) :=
        Build t_delegate t_script t_credit r.(delegate) script r.(credit).
      Definition with_credit {t_delegate t_script t_credit} credit
        (r : record t_delegate t_script t_credit) :=
        Build t_delegate t_script t_credit r.(delegate) r.(script) credit.
    End Origination.
    Definition Origination_skeleton := Origination.record.

    Module Event.
      Record record {ty tag payload : Set} : Set := Build {
        ty : ty;
        tag : tag;
        payload : payload;
      }.
      Arguments record : clear implicits.
      Definition with_ty {t_ty t_tag t_payload} ty
        (r : record t_ty t_tag t_payload) :=
        Build t_ty t_tag t_payload ty r.(tag) r.(payload).
      Definition with_tag {t_ty t_tag t_payload} tag
        (r : record t_ty t_tag t_payload) :=
        Build t_ty t_tag t_payload r.(ty) tag r.(payload).
      Definition with_payload {t_ty t_tag t_payload} payload
        (r : record t_ty t_tag t_payload) :=
        Build t_ty t_tag t_payload r.(ty) r.(tag) payload.
    End Event.
    Definition Event_skeleton := Event.record.
  End internal_operation_contents.
End ConstructorRecords_internal_operation_contents.
Import ConstructorRecords_internal_operation_contents.

Reserved Notation "'internal_operation_contents.Transaction".
Reserved Notation "'internal_operation_contents.Origination".
Reserved Notation "'internal_operation_contents.Event".

Inductive internal_operation_contents : Set :=
| Transaction :
  'internal_operation_contents.Transaction internal_operation_contents
| Origination :
  'internal_operation_contents.Origination internal_operation_contents
| Delegation : option Signature.public_key_hash internal_operation_contents
| Event : 'internal_operation_contents.Event internal_operation_contents

where "'internal_operation_contents.Transaction" :=
  (internal_operation_contents.Transaction_skeleton Alpha_context.Tez.tez
    Alpha_context.Script.lazy_expr Alpha_context.Entrypoint.t
    Alpha_context.Destination.t)
and "'internal_operation_contents.Origination" :=
  (internal_operation_contents.Origination_skeleton
    (option Signature.public_key_hash) Alpha_context.Script.t
    Alpha_context.Tez.tez)
and "'internal_operation_contents.Event" :=
  (internal_operation_contents.Event_skeleton Alpha_context.Script.expr
    Alpha_context.Entrypoint.t Alpha_context.Script.expr).

Module internal_operation_contents.
  Include ConstructorRecords_internal_operation_contents.internal_operation_contents.
  Definition Transaction := 'internal_operation_contents.Transaction.
  Definition Origination := 'internal_operation_contents.Origination.
  Definition Event := 'internal_operation_contents.Event.
End internal_operation_contents.

Inductive packed_internal_operation_contents : Set :=
| Internal_operation_contents :
  internal_operation_contents packed_internal_operation_contents.

Module internal_operation.
  Record record : Set := Build {
    source : Alpha_context.Contract.t;
    operation : internal_operation_contents;
    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_operation.
Definition internal_operation := internal_operation.record.

Inductive packed_internal_operation : Set :=
| Internal_operation : internal_operation packed_internal_operation.

Definition internal_operation_value
  (function_parameter : Script_typed_ir.internal_operation)
  : internal_operation :=
  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_to_implicit {|
        Script_typed_ir.internal_operation_contents.Transaction_to_implicit.destination
          := destination;
          Script_typed_ir.internal_operation_contents.Transaction_to_implicit.amount
            := amount
          |} ⇒
      Transaction
        {| internal_operation_contents.Transaction.amount := amount;
          internal_operation_contents.Transaction.parameters :=
            Alpha_context.Script.unit_parameter;
          internal_operation_contents.Transaction.entrypoint :=
            Alpha_context.Entrypoint.default;
          internal_operation_contents.Transaction.destination :=
            Alpha_context.Destination.Contract
              (Contract_repr.Implicit destination); |}
    |
      Script_typed_ir.Transaction_to_smart_contract {|
        Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.destination
          := destination;
          Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.amount
            := amount;
          Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.entrypoint
            := entrypoint;
          Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.unparsed_parameters
            := unparsed_parameters
          |} ⇒
      Transaction
        {| internal_operation_contents.Transaction.amount := amount;
          internal_operation_contents.Transaction.parameters :=
            Alpha_context.Script.lazy_expr_value unparsed_parameters;
          internal_operation_contents.Transaction.entrypoint := entrypoint;
          internal_operation_contents.Transaction.destination :=
            Alpha_context.Destination.Contract
              (Contract_repr.Originated destination); |}
    |
      Script_typed_ir.Transaction_to_tx_rollup {|
        Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.destination
          := destination;
          Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.unparsed_parameters
            := unparsed_parameters
          |} ⇒
      Transaction
        {|
          internal_operation_contents.Transaction.amount :=
            Alpha_context.Tez.zero;
          internal_operation_contents.Transaction.parameters :=
            Alpha_context.Script.lazy_expr_value unparsed_parameters;
          internal_operation_contents.Transaction.entrypoint :=
            Alpha_context.Entrypoint.deposit;
          internal_operation_contents.Transaction.destination :=
            Alpha_context.Destination.Tx_rollup destination; |}
    |
      Script_typed_ir.Transaction_to_sc_rollup {|
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.destination
          := destination;
          Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.entrypoint
            := entrypoint;
          Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.unparsed_parameters
            := unparsed_parameters
          |} ⇒
      Transaction
        {|
          internal_operation_contents.Transaction.amount :=
            Alpha_context.Tez.zero;
          internal_operation_contents.Transaction.parameters :=
            Alpha_context.Script.lazy_expr_value unparsed_parameters;
          internal_operation_contents.Transaction.entrypoint := entrypoint;
          internal_operation_contents.Transaction.destination :=
            Alpha_context.Destination.Sc_rollup destination; |}
    |
      Script_typed_ir.Event {|
        Script_typed_ir.internal_operation_contents.Event.ty := ty_value;
          Script_typed_ir.internal_operation_contents.Event.tag := tag;
          Script_typed_ir.internal_operation_contents.Event.unparsed_data :=
            unparsed_data
          |} ⇒
      Event
        {| internal_operation_contents.Event.ty := ty_value;
          internal_operation_contents.Event.tag := tag;
          internal_operation_contents.Event.payload := unparsed_data; |}
    |
      Script_typed_ir.Transaction_to_zk_rollup {|
        Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.destination
          := destination;
          Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.unparsed_parameters
            := unparsed_parameters
          |} ⇒
      Transaction
        {|
          internal_operation_contents.Transaction.amount :=
            Alpha_context.Tez.zero;
          internal_operation_contents.Transaction.parameters :=
            Alpha_context.Script.lazy_expr_value unparsed_parameters;
          internal_operation_contents.Transaction.entrypoint :=
            Alpha_context.Entrypoint.deposit;
          internal_operation_contents.Transaction.destination :=
            Alpha_context.Destination.Zk_rollup destination; |}
    |
      Script_typed_ir.Origination {|
        Script_typed_ir.internal_operation_contents.Origination.delegate := delegate;
          Script_typed_ir.internal_operation_contents.Origination.code := code;
          Script_typed_ir.internal_operation_contents.Origination.unparsed_storage
            := unparsed_storage;
          Script_typed_ir.internal_operation_contents.Origination.credit :=
            credit
          |} ⇒
      let script :=
        {|
          Alpha_context.Script.t.code :=
            Alpha_context.Script.lazy_expr_value code;
          Alpha_context.Script.t.storage :=
            Alpha_context.Script.lazy_expr_value unparsed_storage; |} in
      Origination
        {| internal_operation_contents.Origination.delegate := delegate;
          internal_operation_contents.Origination.script := script;
          internal_operation_contents.Origination.credit := credit; |}
    | Script_typed_ir.Delegation delegateDelegation delegate
    end in
  {| internal_operation.source := source;
    internal_operation.operation := operation;
    internal_operation.nonce := nonce_value; |}.

Definition packed_internal_operation_value
  (function_parameter : Script_typed_ir.packed_internal_operation)
  : packed_internal_operation :=
  let 'Script_typed_ir.Internal_operation op := function_parameter in
  Internal_operation (internal_operation_value op).

Definition packed_internal_operations
  : list Script_typed_ir.packed_internal_operation
  list packed_internal_operation := List.map packed_internal_operation_value.

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 ticket_receipt
        originated_contracts consumed_gas storage_size
        allocated_destination_contract : Set} : Set := Build {
        storage : storage;
        lazy_storage_diff : lazy_storage_diff;
        balance_updates : balance_updates;
        ticket_receipt : ticket_receipt;
        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_ticket_receipt
          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_ticket_receipt 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_ticket_receipt
          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.(ticket_receipt)
          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_ticket_receipt
          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_ticket_receipt 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_ticket_receipt
          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.(ticket_receipt)
          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_ticket_receipt
          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_ticket_receipt 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_ticket_receipt
          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.(ticket_receipt)
          r.(originated_contracts) r.(consumed_gas) r.(storage_size)
          r.(paid_storage_size_diff) r.(allocated_destination_contract).
      Definition with_ticket_receipt
        {t_storage t_lazy_storage_diff t_balance_updates t_ticket_receipt
          t_originated_contracts t_consumed_gas t_storage_size
          t_paid_storage_size_diff t_allocated_destination_contract}
        ticket_receipt
        (r :
          record t_storage t_lazy_storage_diff t_balance_updates
            t_ticket_receipt 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_ticket_receipt
          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) ticket_receipt
          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_ticket_receipt
          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_ticket_receipt 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_ticket_receipt
          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.(ticket_receipt)
          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_ticket_receipt
          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_ticket_receipt 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_ticket_receipt
          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.(ticket_receipt)
          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_ticket_receipt
          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_ticket_receipt 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_ticket_receipt
          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.(ticket_receipt)
          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_ticket_receipt
          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_ticket_receipt 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_ticket_receipt
          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.(ticket_receipt)
          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_ticket_receipt
          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_ticket_receipt 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_ticket_receipt
          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.(ticket_receipt)
          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.

    Module Transaction_to_sc_rollup_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 Transaction_to_sc_rollup_result.
    Definition Transaction_to_sc_rollup_result_skeleton :=
      Transaction_to_sc_rollup_result.record.

    Module Transaction_to_zk_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_zk_rollup_result.
    Definition Transaction_to_zk_rollup_result_skeleton :=
      Transaction_to_zk_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".
Reserved Notation
  "'successful_transaction_result.Transaction_to_sc_rollup_result".
Reserved Notation
  "'successful_transaction_result.Transaction_to_zk_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
| Transaction_to_sc_rollup_result :
  'successful_transaction_result.Transaction_to_sc_rollup_result
  successful_transaction_result
| Transaction_to_zk_rollup_result :
  'successful_transaction_result.Transaction_to_zk_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 Alpha_context.Ticket_receipt.t
    (list Contract_hash.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)
and "'successful_transaction_result.Transaction_to_sc_rollup_result" :=
  (successful_transaction_result.Transaction_to_sc_rollup_result_skeleton
    Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Inbox.t)
and "'successful_transaction_result.Transaction_to_zk_rollup_result" :=
  (successful_transaction_result.Transaction_to_zk_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.
  Definition Transaction_to_sc_rollup_result :=
    'successful_transaction_result.Transaction_to_sc_rollup_result.
  Definition Transaction_to_zk_rollup_result :=
    'successful_transaction_result.Transaction_to_zk_rollup_result.
End successful_transaction_result.

Module successful_origination_result.
  Record record : Set := Build {
    lazy_storage_diff : option Alpha_context.Lazy_storage.diffs;
    balance_updates : Alpha_context.Receipt.balance_updates;
    originated_contracts : list Contract_hash.t;
    consumed_gas : Alpha_context.Gas.Arith.fp;
    storage_size : Z.t;
    paid_storage_size_diff : Z.t;
  }.
  Definition with_lazy_storage_diff lazy_storage_diff (r : record) :=
    Build lazy_storage_diff r.(balance_updates) r.(originated_contracts)
      r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff).
  Definition with_balance_updates balance_updates (r : record) :=
    Build r.(lazy_storage_diff) balance_updates r.(originated_contracts)
      r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff).
  Definition with_originated_contracts originated_contracts (r : record) :=
    Build r.(lazy_storage_diff) r.(balance_updates) originated_contracts
      r.(consumed_gas) r.(storage_size) r.(paid_storage_size_diff).
  Definition with_consumed_gas consumed_gas (r : record) :=
    Build r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
      consumed_gas r.(storage_size) r.(paid_storage_size_diff).
  Definition with_storage_size storage_size (r : record) :=
    Build 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 (r : record) :=
    Build r.(lazy_storage_diff) r.(balance_updates) r.(originated_contracts)
      r.(consumed_gas) r.(storage_size) paid_storage_size_diff.
End successful_origination_result.
Definition successful_origination_result :=
  successful_origination_result.record.

Result of applying an internal operation. Records for the constructor parameters
Module ConstructorRecords_successful_internal_operation_result.
  Module successful_internal_operation_result.
    Module IDelegation_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 IDelegation_result.
    Definition IDelegation_result_skeleton := IDelegation_result.record.

    Module IEvent_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 IEvent_result.
    Definition IEvent_result_skeleton := IEvent_result.record.
  End successful_internal_operation_result.
End ConstructorRecords_successful_internal_operation_result.
Import ConstructorRecords_successful_internal_operation_result.

Reserved Notation "'successful_internal_operation_result.IDelegation_result".
Reserved Notation "'successful_internal_operation_result.IEvent_result".

Inductive successful_internal_operation_result : Set :=
| ITransaction_result :
  successful_transaction_result successful_internal_operation_result
| IOrigination_result :
  successful_origination_result successful_internal_operation_result
| IDelegation_result :
  'successful_internal_operation_result.IDelegation_result
  successful_internal_operation_result
| IEvent_result :
  'successful_internal_operation_result.IEvent_result
  successful_internal_operation_result

where "'successful_internal_operation_result.IDelegation_result" :=
  (successful_internal_operation_result.IDelegation_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_internal_operation_result.IEvent_result" :=
  (successful_internal_operation_result.IEvent_result_skeleton
    Alpha_context.Gas.Arith.fp).

Module successful_internal_operation_result.
  Include ConstructorRecords_successful_internal_operation_result.successful_internal_operation_result.
  Definition IDelegation_result :=
    'successful_internal_operation_result.IDelegation_result.
  Definition IEvent_result :=
    'successful_internal_operation_result.IEvent_result.
End successful_internal_operation_result.

Inductive packed_successful_internal_operation_result : Set :=
| Successful_internal_operation_result :
  successful_internal_operation_result
  packed_successful_internal_operation_result.

Definition internal_operation_result : Set :=
  Apply_operation_result.operation_result Alpha_context.Kind.manager
    successful_internal_operation_result.

Inductive packed_internal_operation_result : Set :=
| Internal_operation_result :
  internal_operation internal_operation_result
  packed_internal_operation_result.

Definition pack_internal_operation_result
  (internal_op : Script_typed_ir.internal_operation)
  (manager_op : internal_operation_result) : packed_internal_operation_result :=
  let internal_op := internal_operation_value internal_op in
  Internal_operation_result internal_op manager_op.

Definition iselect : Set :=
  packed_internal_operation_result
  option (internal_operation × internal_operation_result).

Module Internal_operation.
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_operation_contents option internal_operation_contents)
      (internal_operation_contents t_a) (t_a internal_operation_contents)).

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

  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 "ticket_receipt"
              Alpha_context.Ticket_receipt.encoding nil)
            (Data_encoding.dft None None "originated_contracts"
              (Data_encoding.list_value None
                Alpha_context.Contract.originated_encoding) nil)
            (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.ticket_receipt
                    :=
                    ticket_receipt;
                  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, ticket_receipt,
                  originated_contracts, 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 ×
              Alpha_context.Ticket_receipt.t × list Contract_hash.t
              × Alpha_context.Gas.Arith.fp × Z.t × Z.t × bool ×
              option Alpha_context.Lazy_storage.diffs) ⇒
            let
              '(storage_value, balance_updates, ticket_receipt,
                originated_contracts, consumed_gas,
                storage_size, paid_storage_size_diff,
                allocated_destination_contract,
                lazy_storage_diff) := function_parameter 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.ticket_receipt
                  := ticket_receipt;
                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; |});
        Data_encoding.case_value "To_tx_rollup" None (Data_encoding.Tag 1)
          (Data_encoding.obj4
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil)
            (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, consumed_gas, ticket_hash,
                  paid_storage_size_diff)
            | _None
            end)
          (fun (function_parameter :
            Alpha_context.Receipt.balance_updates ×
              Alpha_context.Gas.Arith.fp ×
              Alpha_context.Ticket_hash.t × Z.t) ⇒
            let
              '(balance_updates, consumed_gas, ticket_hash,
                paid_storage_size_diff) := function_parameter 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_gas;
                successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
                  := paid_storage_size_diff; |});
        Data_encoding.case_value "To_sc_rollup" None (Data_encoding.Tag 2)
          (Data_encoding.obj2
            (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))
          (fun (function_parameter : successful_transaction_result) ⇒
            match function_parameter with
            |
              Transaction_to_sc_rollup_result {|
                successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
                  := consumed_gas;
                  successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
                    :=
                    inbox_after
                  |} ⇒ Some (consumed_gas, inbox_after)
            | _None
            end)
          (fun (function_parameter :
            Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Inbox.t)
            ⇒
            let '(consumed_gas, inbox_after) := function_parameter in
            Transaction_to_sc_rollup_result
              {|
                successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
                  := consumed_gas;
                successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
                  := inbox_after; |})
      ].

  Definition transaction_case : case :=
    MCase
      {| case.MCase.tag := 1; 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_operation_result) ⇒
            match function_parameter with
            |
              Internal_operation_result
                ({| internal_operation.operation := Transaction _ |} as op) res
              ⇒ Some (op, res)
            | _None
            end;
        case.MCase.select :=
          fun (function_parameter : packed_internal_operation_contents) ⇒
            match function_parameter with
            | Internal_operation_contents ((Transaction _) as op) ⇒ Some op
            | _None
            end;
        case.MCase.proj :=
          fun (function_parameter : internal_operation_contents) ⇒
            match function_parameter with
            |
              Transaction {|
                internal_operation_contents.Transaction.amount := amount;
                  internal_operation_contents.Transaction.parameters :=
                    parameters;
                  internal_operation_contents.Transaction.entrypoint :=
                    entrypoint;
                  internal_operation_contents.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
              {| internal_operation_contents.Transaction.amount := amount;
                internal_operation_contents.Transaction.parameters :=
                  parameters;
                internal_operation_contents.Transaction.entrypoint :=
                  entrypoint;
                internal_operation_contents.Transaction.destination :=
                  destination; |}; |}.

  Definition origination_case : case :=
    MCase
      {| case.MCase.tag := 2; 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_operation_result) ⇒
            match function_parameter with
            |
              Internal_operation_result
                ({| internal_operation.operation := Origination _ |} as op) res
              ⇒ Some (op, res)
            | _None
            end;
        case.MCase.select :=
          fun (function_parameter : packed_internal_operation_contents) ⇒
            match function_parameter with
            | Internal_operation_contents ((Origination _) as op) ⇒ Some op
            | _None
            end;
        case.MCase.proj :=
          fun (function_parameter : internal_operation_contents) ⇒
            match function_parameter with
            |
              Origination {|
                internal_operation_contents.Origination.delegate := delegate;
                  internal_operation_contents.Origination.script := script;
                  internal_operation_contents.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
              {| internal_operation_contents.Origination.delegate := delegate;
                internal_operation_contents.Origination.script := script;
                internal_operation_contents.Origination.credit := credit; |}; |}.

  Definition delegation_case : case :=
    MCase
      {| case.MCase.tag := 3; 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_operation_result) ⇒
            match function_parameter with
            |
              Internal_operation_result
                ({| internal_operation.operation := Delegation _ |} as op) res
              ⇒ Some (op, res)
            | _None
            end;
        case.MCase.select :=
          fun (function_parameter : packed_internal_operation_contents) ⇒
            match function_parameter with
            | Internal_operation_contents ((Delegation _) as op) ⇒ Some op
            | _None
            end;
        case.MCase.proj :=
          fun (function_parameter : internal_operation_contents) ⇒
            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 event_case : case :=
    MCase
      {| case.MCase.tag := 4; case.MCase.name := "event";
        case.MCase.encoding :=
          Data_encoding.obj3
            (Data_encoding.req None None "type"
              Alpha_context.Script.expr_encoding)
            (Data_encoding.opt None None "tag"
              Alpha_context.Entrypoint.smart_encoding)
            (Data_encoding.opt None None "payload"
              Alpha_context.Script.expr_encoding);
        case.MCase.iselect :=
          fun (function_parameter : packed_internal_operation_result) ⇒
            match function_parameter with
            |
              Internal_operation_result
                ({| internal_operation.operation := Event _ |} as op) res
              Some (op, res)
            | _None
            end;
        case.MCase.select :=
          fun (function_parameter : packed_internal_operation_contents) ⇒
            match function_parameter with
            | Internal_operation_contents ((Event _) as op) ⇒ Some op
            | _None
            end;
        case.MCase.proj :=
          fun (function_parameter : internal_operation_contents) ⇒
            match function_parameter with
            |
              Event {|
                internal_operation_contents.Event.ty := ty_value;
                  internal_operation_contents.Event.tag := tag;
                  internal_operation_contents.Event.payload := payload
                  |} ⇒
              let tag :=
                if Alpha_context.Entrypoint.is_default tag then
                  None
                else
                  Some tag in
              let payload :=
                if Script_repr.is_unit payload then
                  None
                else
                  Some payload in
              (ty_value, tag, payload)
            | _unreachable_gadt_branch
            end;
        case.MCase.inj :=
          fun (function_parameter :
            Alpha_context.Script.expr × option Alpha_context.Entrypoint.t ×
              option Alpha_context.Script.expr) ⇒
            let '(ty_value, tag, payload) := function_parameter in
            let tag := Option.value_value tag Alpha_context.Entrypoint.default
              in
            let payload := Option.value_value payload Script_repr.unit_value in
            Event
              {| internal_operation_contents.Event.ty := ty_value;
                internal_operation_contents.Event.tag := tag;
                internal_operation_contents.Event.payload := payload; |}; |}.

  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_operation_contents :=
    let make (mcase : case)
      : Data_encoding.case packed_internal_operation_contents :=
      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
            |} := mcase in
      let 'existT _ __MCase_'a [inj, proj, select, encoding, name, tag] :=
        cast_exists (Es := Set)
          (fun __MCase_'a
            [__MCase_'a internal_operation_contents **
              internal_operation_contents __MCase_'a **
              packed_internal_operation_contents
              option internal_operation_contents ** 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_operation_contents) ⇒
          match select o_value with
          | NoneNone
          | Some o_valueSome (proj o_value)
          end)
        (fun (x_value : __MCase_'a) ⇒ Internal_operation_contents (inj x_value))
      in
    Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
      [
        make transaction_case;
        make origination_case;
        make delegation_case;
        make event_case
      ].
End Internal_operation.

Definition internal_operation_encoding
  : Data_encoding.t packed_internal_operation :=
  Data_encoding.def "apply_internal_results.alpha.operation_result" None None
    (Data_encoding.conv
      (fun (function_parameter : packed_internal_operation) ⇒
        let
          'Internal_operation {|
            internal_operation.source := source;
              internal_operation.operation := operation;
              internal_operation.nonce := nonce_value
              |} := function_parameter in
        ((source, nonce_value), (Internal_operation_contents operation)))
      (fun (function_parameter :
        (Alpha_context.Contract.t × int) × packed_internal_operation_contents)
        ⇒
        let '((source, nonce_value), Internal_operation_contents operation) :=
          function_parameter in
        Internal_operation
          {| internal_operation.source := source;
            internal_operation.operation := operation;
            internal_operation.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_operation.encoding)).

Module Internal_operation_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 Internal_operation.case
      (Data_encoding.t t_a) Alpha_context.Kind.manager
      (packed_successful_internal_operation_result
      option successful_internal_operation_result)
      (successful_internal_operation_result t_a)
      (t_a successful_internal_operation_result)
      (Data_encoding.t internal_operation_result)).

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

  Arguments MCase {_ _}.

  Definition make {A B : Set}
    (op_case : Internal_operation.case) (encoding : Data_encoding.encoding A)
    (kind_value : Alpha_context.Kind.manager)
    (select :
      packed_successful_internal_operation_result
      option successful_internal_operation_result)
    (proj : successful_internal_operation_result A)
    (inj : A successful_internal_operation_result) : case B :=
    let
      'Internal_operation.MCase {| Internal_operation.case.MCase.name := name |} :=
      op_case in
    let t_value :=
      Data_encoding.def
        (Format.asprintf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal
              "operation.alpha.internal_operation_result."
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.End_of_format))
            "operation.alpha.internal_operation_result.%s") name) None None
        (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 :
                Apply_operation_result.operation_result
                  Alpha_context.Kind.manager
                  successful_internal_operation_result)
                ⇒
                match o_value with
                |
                  (Apply_operation_result.Skipped _ |
                  Apply_operation_result.Failed _ _ |
                  Apply_operation_result.Backtracked _ _)
                  ⇒ None
                | Apply_operation_result.Applied o_value
                  match
                    select
                      (Successful_internal_operation_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
                Apply_operation_result.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"
                  Apply_operation_result.trace_encoding))
              (fun (function_parameter :
                Apply_operation_result.operation_result
                  Alpha_context.Kind.manager
                  successful_internal_operation_result)
                ⇒
                match function_parameter with
                | Apply_operation_result.Failed _ errs
                  Some (tt, errs)
                | _None
                end)
              (fun (function_parameter :
                unit × Error_monad.trace Error_monad._error) ⇒
                let '(_, errs) := function_parameter in
                Apply_operation_result.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 :
                Apply_operation_result.operation_result
                  Alpha_context.Kind.manager
                  successful_internal_operation_result)
                ⇒
                match function_parameter with
                | Apply_operation_result.Skipped _Some tt
                | _None
                end)
              (fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                Apply_operation_result.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"
                    Apply_operation_result.trace_encoding))
                encoding)
              (fun (o_value :
                Apply_operation_result.operation_result
                  Alpha_context.Kind.manager
                  successful_internal_operation_result)
                ⇒
                match o_value with
                |
                  (Apply_operation_result.Skipped _ |
                  Apply_operation_result.Failed _ _ |
                  Apply_operation_result.Applied _) ⇒
                  None
                |
                  Apply_operation_result.Backtracked
                    o_value errs
                  match
                    select
                      (Successful_internal_operation_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
                Apply_operation_result.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 transaction_case : case Alpha_context.Kind.transaction :=
    make Internal_operation.transaction_case
      Internal_operation.transaction_contract_variant_cases
      Alpha_context.Kind.Transaction_manager_kind
      (fun (function_parameter : packed_successful_internal_operation_result) ⇒
        match function_parameter with
        | Successful_internal_operation_result ((ITransaction_result _) as op)
          ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_internal_operation_result) ⇒
        match function_parameter with
        | ITransaction_result x_valuex_value
        | _unreachable_gadt_branch
        end)
      (fun (x_value : successful_transaction_result) ⇒
        ITransaction_result x_value).

  Definition origination_case : case Alpha_context.Kind.origination :=
    make Internal_operation.origination_case
      (Data_encoding.obj6
        (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.originated_encoding) nil)
        (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_internal_operation_result) ⇒
        match function_parameter with
        | Successful_internal_operation_result ((IOrigination_result _) as op)
          ⇒ Some op
        | _None
        end)
      (fun (function_parameter : successful_internal_operation_result) ⇒
        match function_parameter with
        |
          IOrigination_result {|
            successful_origination_result.lazy_storage_diff := lazy_storage_diff;
              successful_origination_result.balance_updates := balance_updates;
              successful_origination_result.originated_contracts :=
                originated_contracts;
              successful_origination_result.consumed_gas := consumed_gas;
              successful_origination_result.storage_size := storage_size;
              successful_origination_result.paid_storage_size_diff :=
                paid_storage_size_diff
              |} ⇒
          (balance_updates, originated_contracts, consumed_gas, storage_size,
            paid_storage_size_diff, lazy_storage_diff)
        | _unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × list Contract_hash.t ×
          Alpha_context.Gas.Arith.fp × Z.t × Z.t ×
          option Alpha_context.Lazy_storage.diffs) ⇒
        let
          '(balance_updates, originated_contracts, consumed_gas, storage_size,
            paid_storage_size_diff, lazy_storage_diff) := function_parameter in
        IOrigination_result
          {|
            successful_origination_result.lazy_storage_diff :=
              lazy_storage_diff;
            successful_origination_result.balance_updates := balance_updates;
            successful_origination_result.originated_contracts :=
              originated_contracts;
            successful_origination_result.consumed_gas := consumed_gas;
            successful_origination_result.storage_size := storage_size;
            successful_origination_result.paid_storage_size_diff :=
              paid_storage_size_diff; |}).

  Definition delegation_case : case Alpha_context.Kind.delegation :=
    make Internal_operation.delegation_case
      (Data_encoding.obj1
        (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_internal_operation_result) ⇒
        match function_parameter with
        | Successful_internal_operation_result ((IDelegation_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_internal_operation_result) ⇒
        match function_parameter with
        |
          IDelegation_result {|
            successful_internal_operation_result.IDelegation_result.consumed_gas :=
              consumed_gas
              |} ⇒ consumed_gas
        | _unreachable_gadt_branch
        end)
      (fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
        IDelegation_result
          {|
            successful_internal_operation_result.IDelegation_result.consumed_gas
              := consumed_gas; |}).

  Definition event_case : case Alpha_context.Kind.event :=
    make Internal_operation.event_case
      (Data_encoding.obj1
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Event_manager_kind
      (fun (function_parameter : packed_successful_internal_operation_result) ⇒
        match function_parameter with
        | Successful_internal_operation_result ((IEvent_result _) as op) ⇒
          Some op
        | _None
        end)
      (fun (function_parameter : successful_internal_operation_result) ⇒
        match function_parameter with
        |
          IEvent_result {|
            successful_internal_operation_result.IEvent_result.consumed_gas :=
              consumed_gas
              |} ⇒ consumed_gas
        | _unreachable_gadt_branch
        end)
      (fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
        IEvent_result
          {|
            successful_internal_operation_result.IEvent_result.consumed_gas :=
              consumed_gas; |}).
End Internal_operation_result.

Definition internal_operation_result_encoding
  : Data_encoding.t packed_internal_operation_result :=
  let make {kind : Set}
    (function_parameter : Internal_operation_result.case kind)
    : Internal_operation.case
    Data_encoding.case packed_internal_operation_result :=
    let 'Internal_operation_result.MCase res_case := function_parameter in
    fun (ires_mcase : Internal_operation.case) ⇒
      let 'Internal_operation.MCase ires_case := ires_mcase in
      let 'existT _ __MCase_'a1 ires_case :=
        cast_exists (Es := Set)
          (fun __MCase_'a1Internal_operation.case.MCase __MCase_'a1)
          ires_case in
      let 'Internal_operation.MCase op_case :=
        res_case.(Internal_operation_result.case.MCase.op_case) in
      Data_encoding.case_value op_case.(Internal_operation.case.MCase.name) None
        (Data_encoding.Tag op_case.(Internal_operation.case.MCase.tag))
        (Data_encoding.merge_objs
          (Data_encoding.obj3
            (Data_encoding.req None None "kind"
              (Data_encoding.constant
                op_case.(Internal_operation.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_operation.case.MCase.encoding)
            (Data_encoding.obj1
              (Data_encoding.req None None "result"
                res_case.(Internal_operation_result.case.MCase.t)))))
        (fun (op : packed_internal_operation_result) ⇒
          match ires_case.(Internal_operation.case.MCase.iselect) op with
          | Some (op, res)
            Some
              ((tt, op.(internal_operation.source),
                op.(internal_operation.nonce)),
                ((ires_case.(Internal_operation.case.MCase.proj)
                  op.(internal_operation.operation)), res))
          | NoneNone
          end)
        (fun (function_parameter :
          (unit × Alpha_context.Contract.t × int) ×
            (__MCase_'a1 × internal_operation_result)) ⇒
          let '((_, source, nonce_value), (op, res)) := function_parameter in
          let op :=
            {| internal_operation.source := source;
              internal_operation.operation :=
                ires_case.(Internal_operation.case.MCase.inj) op;
              internal_operation.nonce := nonce_value; |} in
          Internal_operation_result op res) in
  Data_encoding.def "apply_internal_results.alpha.operation_result" None None
    (Data_encoding.union None
      [
        make Internal_operation_result.transaction_case
          Internal_operation.transaction_case;
        make Internal_operation_result.origination_case
          Internal_operation.origination_case;
        make Internal_operation_result.delegation_case
          Internal_operation.delegation_case;
        make Internal_operation_result.event_case Internal_operation.event_case
      ]).