🏗️ Apply_internal_results.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_operation_result.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_operation_result.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
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 delegate ⇒ Delegation 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.
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 delegate ⇒ Delegation 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 paid_storage_size_diff
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}
paid_storage_size_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)
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
paid_storage_size_diff : 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}
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
paid_storage_size_diff : 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}
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 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 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.
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 paid_storage_size_diff
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}
paid_storage_size_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)
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
paid_storage_size_diff : 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}
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
paid_storage_size_diff : 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}
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 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 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.
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"
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 ×
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_value ⇒ key_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
| None ⇒ None
| Some x_value ⇒ Some (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
| None ⇒ None
| Some o_value ⇒ Some (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.
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"
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 ×
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_value ⇒ key_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
| None ⇒ None
| Some x_value ⇒ Some (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
| None ⇒ None
| Some o_value ⇒ Some (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
| None ⇒ None
| 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
| None ⇒ None
| 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_value ⇒ x_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_'a1 ⇒ Internal_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))
| None ⇒ None
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
]).
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
| None ⇒ None
| 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
| None ⇒ None
| 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_value ⇒ x_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_'a1 ⇒ Internal_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))
| None ⇒ None
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
]).