🐆 Tx_rollup_l2_apply.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.Indexable.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_batch.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context_sig.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Module Counter_mismatch.
Record record : Set := Build {
account : Tx_rollup_l2_address.t;
expected : int64;
provided : int64;
}.
Definition with_account account (r : record) :=
Build account r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(account) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(account) r.(expected) provided.
End Counter_mismatch.
Definition Counter_mismatch := Counter_mismatch.record.
Module Maximum_withdraws_per_message_exceeded.
Record record : Set := Build {
current : int;
maximum : int;
}.
Definition with_current current (r : record) :=
Build current r.(maximum).
Definition with_maximum maximum (r : record) :=
Build r.(current) maximum.
End Maximum_withdraws_per_message_exceeded.
Definition Maximum_withdraws_per_message_exceeded :=
Maximum_withdraws_per_message_exceeded.record.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_batch.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context_sig.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Module Counter_mismatch.
Record record : Set := Build {
account : Tx_rollup_l2_address.t;
expected : int64;
provided : int64;
}.
Definition with_account account (r : record) :=
Build account r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(account) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(account) r.(expected) provided.
End Counter_mismatch.
Definition Counter_mismatch := Counter_mismatch.record.
Module Maximum_withdraws_per_message_exceeded.
Record record : Set := Build {
current : int;
maximum : int;
}.
Definition with_current current (r : record) :=
Build current r.(maximum).
Definition with_maximum maximum (r : record) :=
Build r.(current) maximum.
End Maximum_withdraws_per_message_exceeded.
Definition Maximum_withdraws_per_message_exceeded :=
Maximum_withdraws_per_message_exceeded.record.
Init function; without side-effects in Coq
Definition init_module : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"tx_rollup_operation_counter_mismatch" "Operation counter mismatch"
"A transaction rollup operation has been submitted with an incorrect counter"
None
(Data_encoding.obj3
(Data_encoding.req None None "account" Tx_rollup_l2_address.encoding)
(Data_encoding.req None None "expected" Data_encoding.int64_value)
(Data_encoding.req None None "provided" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Counter_mismatch" then
let '{|
Counter_mismatch.account := account;
Counter_mismatch.expected := expected;
Counter_mismatch.provided := provided
|} := cast Counter_mismatch payload in
Some (account, expected, provided)
else None
end)
(fun (function_parameter : Tx_rollup_l2_address.t × int64 × int64) ⇒
let '(account, expected, provided) := function_parameter in
Build_extensible "Counter_mismatch" Counter_mismatch
{| Counter_mismatch.account := account;
Counter_mismatch.expected := expected;
Counter_mismatch.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_incorrect_aggregated_signature"
"Incorrect aggregated signature" "The aggregated signature is incorrect"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Incorrect_aggregated_signature" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Incorrect_aggregated_signature" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"tx_rollup_unknown_metadata" "Unknown metadata"
"A public key index was provided but the account information for this index is not present in the context."
None
(Data_encoding.obj1
(Data_encoding.req None None "idx" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unallocated_metadata" then
let i_value := cast int32 payload in
Some i_value
else None
end)
(fun (i_value : int32) ⇒
Build_extensible "Unallocated_metadata" int32 i_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_invalid_transaction" "Invalid transaction"
"The signer signed multiple operations in the same transaction. He must gather all the contents in a single operation"
None
(Data_encoding.obj1
(Data_encoding.req None None "pk"
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Multiple_operations_for_signer" then
let idx := cast Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) payload in
Some idx
else None
end)
(fun (idx : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) ⇒
Build_extensible "Multiple_operations_for_signer"
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) idx) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_invalid_transaction_encoding" "Invalid transaction encoding"
"The transaction could not be decoded from bytes" None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_transaction_encoding" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_transaction_encoding" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_invalid_batch_encoding" "Invalid batch encoding"
"The batch could not be decoded from bytes" None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_batch_encoding" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_batch_encoding" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_unexpectedly_indexed_ticket"
"Unexpected indexed ticket in deposit or transfer"
"Tickets in layer2-to-layer1 transfers must be referenced by value." None
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpectedly_indexed_ticket" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpectedly_indexed_ticket" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"tx_rollup_missing_ticket"
"Attempted to withdraw from a ticket missing in the rollup"
"A withdrawal must reference a ticket that already exists in the rollup."
None
(Data_encoding.obj1
(Data_encoding.req None None "ticket_hash"
Alpha_context.Ticket_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Missing_ticket" then
let ticket_hash := cast Alpha_context.Ticket_hash.t payload in
Some ticket_hash
else None
end)
(fun (ticket_hash : Alpha_context.Ticket_hash.t) ⇒
Build_extensible "Missing_ticket" Alpha_context.Ticket_hash.t
ticket_hash) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"tx_rollup_unknown_address"
"Attempted to sign a transfer with an unknown address"
"The address must exist in the context when signing a transfer with it."
None
(Data_encoding.obj1
(Data_encoding.req None None "address" Tx_rollup_l2_address.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unknown_address" then
let addr := cast Tx_rollup_l2_address.t payload in
Some addr
else None
end)
(fun (addr : Tx_rollup_l2_address.t) ⇒
Build_extensible "Unknown_address" Tx_rollup_l2_address.t addr) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"tx_rollup_invalid_self_transfer" "Attempted to transfer ticket to self"
"The index for the destination is the same as the sender" None
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_self_transfer" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_self_transfer" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_invalid_zero_transfer" "Attempted to transfer zero ticket"
"A transfer's amount must be greater than zero." None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_zero_transfer" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_zero_transfer" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_maximum_withdraws_per_message_exceeded"
"Maximum tx-rollup withdraws per message exceeded"
"The maximum number of withdraws allowed per tx-rollup message exceeded"
None
(Data_encoding.obj2
(Data_encoding.req None None "current" Data_encoding.int31)
(Data_encoding.req None None "limit" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Maximum_withdraws_per_message_exceeded" then
let '{|
Maximum_withdraws_per_message_exceeded.current := current;
Maximum_withdraws_per_message_exceeded.maximum := maximum
|} := cast Maximum_withdraws_per_message_exceeded payload in
Some (current, maximum)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(current, maximum) := function_parameter in
Build_extensible "Maximum_withdraws_per_message_exceeded"
Maximum_withdraws_per_message_exceeded
{| Maximum_withdraws_per_message_exceeded.current := current;
Maximum_withdraws_per_message_exceeded.maximum := maximum; |}).
Module indexes.
Record record : Set := Build {
address_indexes :
list (Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index);
ticket_indexes :
list
(Alpha_context.Ticket_hash.t ×
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index));
}.
Definition with_address_indexes address_indexes (r : record) :=
Build address_indexes r.(ticket_indexes).
Definition with_ticket_indexes ticket_indexes (r : record) :=
Build r.(address_indexes) ticket_indexes.
End indexes.
Definition indexes := indexes.record.
Definition encoding_indexes : Data_encoding.t indexes :=
Data_encoding.conv
(fun (function_parameter : indexes) ⇒
let '{|
indexes.address_indexes := address_indexes;
indexes.ticket_indexes := ticket_indexes
|} := function_parameter in
(address_indexes, ticket_indexes))
(fun (function_parameter :
list (Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index) ×
list
(Alpha_context.Ticket_hash.t ×
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index)))
⇒
let '(address_indexes, ticket_indexes) := function_parameter in
{| indexes.address_indexes := address_indexes;
indexes.ticket_indexes := ticket_indexes; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "address_indexes"
(Data_encoding.list_value None
(Data_encoding.tup2 Tx_rollup_l2_address.encoding
Tx_rollup_l2_address.Indexable.index_encoding)))
(Data_encoding.req None None "ticket_indexes"
(Data_encoding.list_value None
(Data_encoding.tup2 Alpha_context.Ticket_hash.encoding
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index_encoding))))).
Module Message_result.
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"tx_rollup_operation_counter_mismatch" "Operation counter mismatch"
"A transaction rollup operation has been submitted with an incorrect counter"
None
(Data_encoding.obj3
(Data_encoding.req None None "account" Tx_rollup_l2_address.encoding)
(Data_encoding.req None None "expected" Data_encoding.int64_value)
(Data_encoding.req None None "provided" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Counter_mismatch" then
let '{|
Counter_mismatch.account := account;
Counter_mismatch.expected := expected;
Counter_mismatch.provided := provided
|} := cast Counter_mismatch payload in
Some (account, expected, provided)
else None
end)
(fun (function_parameter : Tx_rollup_l2_address.t × int64 × int64) ⇒
let '(account, expected, provided) := function_parameter in
Build_extensible "Counter_mismatch" Counter_mismatch
{| Counter_mismatch.account := account;
Counter_mismatch.expected := expected;
Counter_mismatch.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_incorrect_aggregated_signature"
"Incorrect aggregated signature" "The aggregated signature is incorrect"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Incorrect_aggregated_signature" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Incorrect_aggregated_signature" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"tx_rollup_unknown_metadata" "Unknown metadata"
"A public key index was provided but the account information for this index is not present in the context."
None
(Data_encoding.obj1
(Data_encoding.req None None "idx" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unallocated_metadata" then
let i_value := cast int32 payload in
Some i_value
else None
end)
(fun (i_value : int32) ⇒
Build_extensible "Unallocated_metadata" int32 i_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_invalid_transaction" "Invalid transaction"
"The signer signed multiple operations in the same transaction. He must gather all the contents in a single operation"
None
(Data_encoding.obj1
(Data_encoding.req None None "pk"
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Multiple_operations_for_signer" then
let idx := cast Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) payload in
Some idx
else None
end)
(fun (idx : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) ⇒
Build_extensible "Multiple_operations_for_signer"
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) idx) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_invalid_transaction_encoding" "Invalid transaction encoding"
"The transaction could not be decoded from bytes" None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_transaction_encoding" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_transaction_encoding" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_invalid_batch_encoding" "Invalid batch encoding"
"The batch could not be decoded from bytes" None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_batch_encoding" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_batch_encoding" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_unexpectedly_indexed_ticket"
"Unexpected indexed ticket in deposit or transfer"
"Tickets in layer2-to-layer1 transfers must be referenced by value." None
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpectedly_indexed_ticket" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpectedly_indexed_ticket" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"tx_rollup_missing_ticket"
"Attempted to withdraw from a ticket missing in the rollup"
"A withdrawal must reference a ticket that already exists in the rollup."
None
(Data_encoding.obj1
(Data_encoding.req None None "ticket_hash"
Alpha_context.Ticket_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Missing_ticket" then
let ticket_hash := cast Alpha_context.Ticket_hash.t payload in
Some ticket_hash
else None
end)
(fun (ticket_hash : Alpha_context.Ticket_hash.t) ⇒
Build_extensible "Missing_ticket" Alpha_context.Ticket_hash.t
ticket_hash) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"tx_rollup_unknown_address"
"Attempted to sign a transfer with an unknown address"
"The address must exist in the context when signing a transfer with it."
None
(Data_encoding.obj1
(Data_encoding.req None None "address" Tx_rollup_l2_address.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unknown_address" then
let addr := cast Tx_rollup_l2_address.t payload in
Some addr
else None
end)
(fun (addr : Tx_rollup_l2_address.t) ⇒
Build_extensible "Unknown_address" Tx_rollup_l2_address.t addr) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"tx_rollup_invalid_self_transfer" "Attempted to transfer ticket to self"
"The index for the destination is the same as the sender" None
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_self_transfer" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_self_transfer" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_invalid_zero_transfer" "Attempted to transfer zero ticket"
"A transfer's amount must be greater than zero." None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_zero_transfer" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_zero_transfer" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent
"tx_rollup_maximum_withdraws_per_message_exceeded"
"Maximum tx-rollup withdraws per message exceeded"
"The maximum number of withdraws allowed per tx-rollup message exceeded"
None
(Data_encoding.obj2
(Data_encoding.req None None "current" Data_encoding.int31)
(Data_encoding.req None None "limit" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Maximum_withdraws_per_message_exceeded" then
let '{|
Maximum_withdraws_per_message_exceeded.current := current;
Maximum_withdraws_per_message_exceeded.maximum := maximum
|} := cast Maximum_withdraws_per_message_exceeded payload in
Some (current, maximum)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(current, maximum) := function_parameter in
Build_extensible "Maximum_withdraws_per_message_exceeded"
Maximum_withdraws_per_message_exceeded
{| Maximum_withdraws_per_message_exceeded.current := current;
Maximum_withdraws_per_message_exceeded.maximum := maximum; |}).
Module indexes.
Record record : Set := Build {
address_indexes :
list (Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index);
ticket_indexes :
list
(Alpha_context.Ticket_hash.t ×
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index));
}.
Definition with_address_indexes address_indexes (r : record) :=
Build address_indexes r.(ticket_indexes).
Definition with_ticket_indexes ticket_indexes (r : record) :=
Build r.(address_indexes) ticket_indexes.
End indexes.
Definition indexes := indexes.record.
Definition encoding_indexes : Data_encoding.t indexes :=
Data_encoding.conv
(fun (function_parameter : indexes) ⇒
let '{|
indexes.address_indexes := address_indexes;
indexes.ticket_indexes := ticket_indexes
|} := function_parameter in
(address_indexes, ticket_indexes))
(fun (function_parameter :
list (Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index) ×
list
(Alpha_context.Ticket_hash.t ×
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index)))
⇒
let '(address_indexes, ticket_indexes) := function_parameter in
{| indexes.address_indexes := address_indexes;
indexes.ticket_indexes := ticket_indexes; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "address_indexes"
(Data_encoding.list_value None
(Data_encoding.tup2 Tx_rollup_l2_address.encoding
Tx_rollup_l2_address.Indexable.index_encoding)))
(Data_encoding.req None None "ticket_indexes"
(Data_encoding.list_value None
(Data_encoding.tup2 Alpha_context.Ticket_hash.encoding
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index_encoding))))).
Module Message_result.
Records for the constructor parameters
Module ConstructorRecords_transaction_result.
Module transaction_result.
Module Transaction_failure.
Record record {index reason : Set} : Set := Build {
index : index;
reason : reason;
}.
Arguments record : clear implicits.
Definition with_index {t_index t_reason} index
(r : record t_index t_reason) :=
Build t_index t_reason index r.(reason).
Definition with_reason {t_index t_reason} reason
(r : record t_index t_reason) :=
Build t_index t_reason r.(index) reason.
End Transaction_failure.
Definition Transaction_failure_skeleton := Transaction_failure.record.
End transaction_result.
End ConstructorRecords_transaction_result.
Import ConstructorRecords_transaction_result.
Reserved Notation "'transaction_result.Transaction_failure".
Inductive transaction_result : Set :=
| Transaction_success : transaction_result
| Transaction_failure :
'transaction_result.Transaction_failure → transaction_result
where "'transaction_result.Transaction_failure" :=
(transaction_result.Transaction_failure_skeleton int Error_monad._error).
Module transaction_result.
Include ConstructorRecords_transaction_result.transaction_result.
Definition Transaction_failure := 'transaction_result.Transaction_failure.
End transaction_result.
Inductive deposit_result : Set :=
| Deposit_success : indexes → deposit_result
| Deposit_failure : Error_monad._error → deposit_result.
Definition encoding_transaction_result
: Data_encoding.encoding transaction_result :=
Data_encoding.union None
[
let kind_value := "transaction_success" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
(Data_encoding.constant kind_value)
(fun (function_parameter : transaction_result) ⇒
match function_parameter with
| Transaction_success ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Transaction_success);
let kind_value := "transaction_failure" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None kind_value
(Data_encoding.obj2
(Data_encoding.req None None "transaction_index"
Data_encoding.int31)
(Data_encoding.req None None "reason"
Error_monad.error_encoding))))
(fun (function_parameter : transaction_result) ⇒
match function_parameter with
|
Transaction_failure {|
transaction_result.Transaction_failure.index := index_value;
transaction_result.Transaction_failure.reason
:=
reason_value
|} ⇒ Some (index_value, reason_value)
| _ ⇒ None
end)
(fun (function_parameter : int × Error_monad._error) ⇒
let '(index_value, reason_value) := function_parameter in
Transaction_failure
{|
transaction_result.Transaction_failure.index :=
index_value;
transaction_result.Transaction_failure.reason :=
reason_value; |})
].
Definition encoding_deposit_result : Data_encoding.encoding deposit_result :=
Data_encoding.union None
[
let kind_value := "deposit_success" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None kind_value encoding_indexes))
(fun (function_parameter : deposit_result) ⇒
match function_parameter with
| Deposit_success indexes_value ⇒ Some indexes_value
| _ ⇒ None
end)
(fun (indexes_value : indexes) ⇒ Deposit_success indexes_value);
let kind_value := "deposit_failure" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None kind_value
(Data_encoding.obj1
(Data_encoding.req None None "reason"
Error_monad.error_encoding))))
(fun (function_parameter : deposit_result) ⇒
match function_parameter with
| Deposit_failure reason_value ⇒ Some reason_value
| _ ⇒ None
end)
(fun (reason_value : Error_monad._error) ⇒
Deposit_failure reason_value)
].
Module Batch_V1.
Module transaction_result.
Module Transaction_failure.
Record record {index reason : Set} : Set := Build {
index : index;
reason : reason;
}.
Arguments record : clear implicits.
Definition with_index {t_index t_reason} index
(r : record t_index t_reason) :=
Build t_index t_reason index r.(reason).
Definition with_reason {t_index t_reason} reason
(r : record t_index t_reason) :=
Build t_index t_reason r.(index) reason.
End Transaction_failure.
Definition Transaction_failure_skeleton := Transaction_failure.record.
End transaction_result.
End ConstructorRecords_transaction_result.
Import ConstructorRecords_transaction_result.
Reserved Notation "'transaction_result.Transaction_failure".
Inductive transaction_result : Set :=
| Transaction_success : transaction_result
| Transaction_failure :
'transaction_result.Transaction_failure → transaction_result
where "'transaction_result.Transaction_failure" :=
(transaction_result.Transaction_failure_skeleton int Error_monad._error).
Module transaction_result.
Include ConstructorRecords_transaction_result.transaction_result.
Definition Transaction_failure := 'transaction_result.Transaction_failure.
End transaction_result.
Inductive deposit_result : Set :=
| Deposit_success : indexes → deposit_result
| Deposit_failure : Error_monad._error → deposit_result.
Definition encoding_transaction_result
: Data_encoding.encoding transaction_result :=
Data_encoding.union None
[
let kind_value := "transaction_success" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
(Data_encoding.constant kind_value)
(fun (function_parameter : transaction_result) ⇒
match function_parameter with
| Transaction_success ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Transaction_success);
let kind_value := "transaction_failure" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None kind_value
(Data_encoding.obj2
(Data_encoding.req None None "transaction_index"
Data_encoding.int31)
(Data_encoding.req None None "reason"
Error_monad.error_encoding))))
(fun (function_parameter : transaction_result) ⇒
match function_parameter with
|
Transaction_failure {|
transaction_result.Transaction_failure.index := index_value;
transaction_result.Transaction_failure.reason
:=
reason_value
|} ⇒ Some (index_value, reason_value)
| _ ⇒ None
end)
(fun (function_parameter : int × Error_monad._error) ⇒
let '(index_value, reason_value) := function_parameter in
Transaction_failure
{|
transaction_result.Transaction_failure.index :=
index_value;
transaction_result.Transaction_failure.reason :=
reason_value; |})
].
Definition encoding_deposit_result : Data_encoding.encoding deposit_result :=
Data_encoding.union None
[
let kind_value := "deposit_success" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None kind_value encoding_indexes))
(fun (function_parameter : deposit_result) ⇒
match function_parameter with
| Deposit_success indexes_value ⇒ Some indexes_value
| _ ⇒ None
end)
(fun (indexes_value : indexes) ⇒ Deposit_success indexes_value);
let kind_value := "deposit_failure" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None kind_value
(Data_encoding.obj1
(Data_encoding.req None None "reason"
Error_monad.error_encoding))))
(fun (function_parameter : deposit_result) ⇒
match function_parameter with
| Deposit_failure reason_value ⇒ Some reason_value
| _ ⇒ None
end)
(fun (reason_value : Error_monad._error) ⇒
Deposit_failure reason_value)
].
Module Batch_V1.
Records for the constructor parameters
Module ConstructorRecords_t.
Module t.
Module Batch_result.
Record record {results indexes : Set} : Set := Build {
results : results;
indexes : indexes;
}.
Arguments record : clear implicits.
Definition with_results {t_results t_indexes} results
(r : record t_results t_indexes) :=
Build t_results t_indexes results r.(indexes).
Definition with_indexes {t_results t_indexes} indexes
(r : record t_results t_indexes) :=
Build t_results t_indexes r.(results) indexes.
End Batch_result.
Definition Batch_result_skeleton := Batch_result.record.
End t.
End ConstructorRecords_t.
Import ConstructorRecords_t.
Reserved Notation "'t.Batch_result".
Inductive t : Set :=
| Batch_result : 't.Batch_result → t
where "'t.Batch_result" :=
(t.Batch_result_skeleton
(list (Tx_rollup_l2_batch.V1.transaction × transaction_result)) indexes).
Module t.
Include ConstructorRecords_t.t.
Definition Batch_result := 't.Batch_result.
End t.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let
'Batch_result {|
t.Batch_result.results := results;
t.Batch_result.indexes := indexes_value
|} := function_parameter in
(results, indexes_value))
(fun (function_parameter :
list (Tx_rollup_l2_batch.V1.transaction × transaction_result) ×
indexes) ⇒
let '(results, indexes_value) := function_parameter in
Batch_result
{| t.Batch_result.results := results;
t.Batch_result.indexes := indexes_value; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "results"
(Data_encoding.list_value None
(Data_encoding.tup2
(Data_encoding.Compact.make
(Some (Variant.Build "Uint8" unit tt))
Tx_rollup_l2_batch.V1.compact_transaction_signer_index)
encoding_transaction_result)))
(Data_encoding.req None None "allocated_indexes" encoding_indexes)).
(* Batch_V1 *)
Definition module :=
{|
Storage_sigs.VALUE.encoding := encoding
|}.
End Batch_V1.
Definition Batch_V1 := Batch_V1.module.
Inductive message_result : Set :=
| Deposit_result : deposit_result → message_result
| Batch_V1_result : Batch_V1.(Storage_sigs.VALUE.t) → message_result.
Definition message_result_encoding : Data_encoding.encoding message_result :=
Data_encoding.union None
[
let kind_value := "deposit_result" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None kind_value
encoding_deposit_result))
(fun (function_parameter : message_result) ⇒
match function_parameter with
| Deposit_result result_value ⇒ Some result_value
| _ ⇒ None
end)
(fun (result_value : deposit_result) ⇒
Deposit_result result_value);
let kind_value := "batch_v1_result" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None kind_value
Batch_V1.(Storage_sigs.VALUE.encoding)))
(fun (function_parameter : message_result) ⇒
match function_parameter with
| Batch_V1_result result_value ⇒ Some result_value
| _ ⇒ None
end)
(fun (result_value : Batch_V1.(Storage_sigs.VALUE.t)) ⇒
Batch_V1_result result_value)
].
Definition t : Set :=
message_result × list Alpha_context.Tx_rollup_withdraw.t.
Definition encoding
: Data_encoding.encoding
(message_result × list Alpha_context.Tx_rollup_withdraw.t) :=
Data_encoding.tup2 message_result_encoding
(Data_encoding.list_value None Alpha_context.Tx_rollup_withdraw.encoding).
End Message_result.
Module parameters.
Record record : Set := Build {
tx_rollup_max_withdrawals_per_batch : int;
}.
Definition with_tx_rollup_max_withdrawals_per_batch
tx_rollup_max_withdrawals_per_batch (r : record) :=
Build tx_rollup_max_withdrawals_per_batch.
End parameters.
Definition parameters := parameters.record.
Module BATCH_V1.
Record signature {ctxt_type : Set} {m : Set → Set} : Set := {
ctxt_type := ctxt_type;
m := m;
apply_batch :
ctxt_type → parameters → Tx_rollup_l2_batch.V1.t →
m
(ctxt_type × Message_result.Batch_V1.(Storage_sigs.VALUE.t) ×
list Alpha_context.Tx_rollup_withdraw.t);
check_signature :
ctxt_type → Tx_rollup_l2_batch.V1.t →
m (ctxt_type × indexes × Tx_rollup_l2_batch.V1.t);
}.
End BATCH_V1.
Definition BATCH_V1 := @BATCH_V1.signature.
Arguments BATCH_V1 {_ _}.
Module S.
Record signature {ctxt_type : Set} {m : Set → Set} : Set := {
ctxt_type := ctxt_type;
m := m;
Batch_V1 : BATCH_V1 (ctxt_type := ctxt_type) (m := fun (a : Set) ⇒ m a);
Module t.
Module Batch_result.
Record record {results indexes : Set} : Set := Build {
results : results;
indexes : indexes;
}.
Arguments record : clear implicits.
Definition with_results {t_results t_indexes} results
(r : record t_results t_indexes) :=
Build t_results t_indexes results r.(indexes).
Definition with_indexes {t_results t_indexes} indexes
(r : record t_results t_indexes) :=
Build t_results t_indexes r.(results) indexes.
End Batch_result.
Definition Batch_result_skeleton := Batch_result.record.
End t.
End ConstructorRecords_t.
Import ConstructorRecords_t.
Reserved Notation "'t.Batch_result".
Inductive t : Set :=
| Batch_result : 't.Batch_result → t
where "'t.Batch_result" :=
(t.Batch_result_skeleton
(list (Tx_rollup_l2_batch.V1.transaction × transaction_result)) indexes).
Module t.
Include ConstructorRecords_t.t.
Definition Batch_result := 't.Batch_result.
End t.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let
'Batch_result {|
t.Batch_result.results := results;
t.Batch_result.indexes := indexes_value
|} := function_parameter in
(results, indexes_value))
(fun (function_parameter :
list (Tx_rollup_l2_batch.V1.transaction × transaction_result) ×
indexes) ⇒
let '(results, indexes_value) := function_parameter in
Batch_result
{| t.Batch_result.results := results;
t.Batch_result.indexes := indexes_value; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "results"
(Data_encoding.list_value None
(Data_encoding.tup2
(Data_encoding.Compact.make
(Some (Variant.Build "Uint8" unit tt))
Tx_rollup_l2_batch.V1.compact_transaction_signer_index)
encoding_transaction_result)))
(Data_encoding.req None None "allocated_indexes" encoding_indexes)).
(* Batch_V1 *)
Definition module :=
{|
Storage_sigs.VALUE.encoding := encoding
|}.
End Batch_V1.
Definition Batch_V1 := Batch_V1.module.
Inductive message_result : Set :=
| Deposit_result : deposit_result → message_result
| Batch_V1_result : Batch_V1.(Storage_sigs.VALUE.t) → message_result.
Definition message_result_encoding : Data_encoding.encoding message_result :=
Data_encoding.union None
[
let kind_value := "deposit_result" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None kind_value
encoding_deposit_result))
(fun (function_parameter : message_result) ⇒
match function_parameter with
| Deposit_result result_value ⇒ Some result_value
| _ ⇒ None
end)
(fun (result_value : deposit_result) ⇒
Deposit_result result_value);
let kind_value := "batch_v1_result" in
Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None kind_value
Batch_V1.(Storage_sigs.VALUE.encoding)))
(fun (function_parameter : message_result) ⇒
match function_parameter with
| Batch_V1_result result_value ⇒ Some result_value
| _ ⇒ None
end)
(fun (result_value : Batch_V1.(Storage_sigs.VALUE.t)) ⇒
Batch_V1_result result_value)
].
Definition t : Set :=
message_result × list Alpha_context.Tx_rollup_withdraw.t.
Definition encoding
: Data_encoding.encoding
(message_result × list Alpha_context.Tx_rollup_withdraw.t) :=
Data_encoding.tup2 message_result_encoding
(Data_encoding.list_value None Alpha_context.Tx_rollup_withdraw.encoding).
End Message_result.
Module parameters.
Record record : Set := Build {
tx_rollup_max_withdrawals_per_batch : int;
}.
Definition with_tx_rollup_max_withdrawals_per_batch
tx_rollup_max_withdrawals_per_batch (r : record) :=
Build tx_rollup_max_withdrawals_per_batch.
End parameters.
Definition parameters := parameters.record.
Module BATCH_V1.
Record signature {ctxt_type : Set} {m : Set → Set} : Set := {
ctxt_type := ctxt_type;
m := m;
apply_batch :
ctxt_type → parameters → Tx_rollup_l2_batch.V1.t →
m
(ctxt_type × Message_result.Batch_V1.(Storage_sigs.VALUE.t) ×
list Alpha_context.Tx_rollup_withdraw.t);
check_signature :
ctxt_type → Tx_rollup_l2_batch.V1.t →
m (ctxt_type × indexes × Tx_rollup_l2_batch.V1.t);
}.
End BATCH_V1.
Definition BATCH_V1 := @BATCH_V1.signature.
Arguments BATCH_V1 {_ _}.
Module S.
Record signature {ctxt_type : Set} {m : Set → Set} : Set := {
ctxt_type := ctxt_type;
m := m;
Batch_V1 : BATCH_V1 (ctxt_type := ctxt_type) (m := fun (a : Set) ⇒ m a);
[apply_deposit ctxt deposit] credits a quantity of tickets to a layer2
address in [ctxt].
This function can fail if the [deposit.amount] is not strictly-positive.
If the [deposit] causes an error, then a withdrawal returning
the funds to the deposit's sender is returned.
apply_deposit :
ctxt_type → Alpha_context.Tx_rollup_message.deposit →
m
(ctxt_type × Message_result.deposit_result ×
option Alpha_context.Tx_rollup_withdraw.t);
ctxt_type → Alpha_context.Tx_rollup_message.deposit →
m
(ctxt_type × Message_result.deposit_result ×
option Alpha_context.Tx_rollup_withdraw.t);
[apply_message ctxt parameters message] interprets the [message] in the
[ctxt].
That is,
{ul {li Deposit tickets if the message is a deposit. }
{li Decodes the batch and interprets it for the
correct batch version. }}
The function can fail with {!Invalid_batch_encoding} if it's not able
to decode the batch.
The function can also return errors from subsequent functions,
see {!apply_deposit} and batch interpretations for various versions.
The list of withdrawals in the message result followed the ordering
of the contents in the message.
apply_message :
ctxt_type → parameters → Alpha_context.Tx_rollup_message.t →
m (ctxt_type × Message_result.t);
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Module Make.
Class FArgs {Context_t : Set} {Context_m : Set → Set} := {
Context :
Tx_rollup_l2_context_sig.CONTEXT (t := Context_t) (m := Context_m);
}.
Arguments Build_FArgs {_ _}.
Definition ctxt_type `{FArgs} : Set :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.t).
Definition index_value `{FArgs} {A B C : Set}
(get_or_associate_index :
A → B →
Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(A × Tx_rollup_l2_context_sig.created_existed × Indexable.index B))
(add_index : C → B × Indexable.index B → C) (ctxt : A) (indexes_value : C)
(indexable : Indexable.t B)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m) (A × C × Indexable.index B) :=
match Indexable.destruct indexable with
| Either.Right v_value ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
(get_or_associate_index ctxt v_value)
(fun function_parameter ⇒
let '(ctxt, created, idx) := function_parameter in
match created with
| Tx_rollup_l2_context_sig.Existed ⇒ (ctxt, indexes_value, idx)
| Tx_rollup_l2_context_sig.Created ⇒
(ctxt, (add_index indexes_value (v_value, idx)), idx)
end)
| Either.Left i_value ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, i_value)
end.
Definition address_index `{FArgs}
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(indexes_value : indexes) (indexable : Indexable.t Tx_rollup_l2_address.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes ×
Indexable.index Tx_rollup_l2_address.t) :=
let get_or_associate_index :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
in
let add_index
(indexes_value : indexes)
(x_value : Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index)
: indexes :=
indexes.with_address_indexes
(cons x_value indexes_value.(indexes.address_indexes)) indexes_value in
index_value get_or_associate_index add_index ctxt indexes_value indexable.
Definition ticket_index `{FArgs}
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(indexes_value : indexes)
(indexable : Indexable.t Alpha_context.Ticket_hash.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes ×
Indexable.index Alpha_context.Ticket_hash.t) :=
let get_or_associate_index :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
in
let add_index
(indexes_value : indexes)
(x_value :
Alpha_context.Ticket_hash.t ×
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index))
: indexes :=
indexes.with_ticket_indexes
(cons x_value indexes_value.(indexes.ticket_indexes)) indexes_value in
index_value get_or_associate_index add_index ctxt indexes_value indexable.
Definition address_of_signer_index `{FArgs}
(idx : Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
: Tx_rollup_l2_address.Indexable.index :=
Indexable.index_exn (Indexable.to_int32 idx).
Definition signer_of_address_index `{FArgs}
(idx : Tx_rollup_l2_address.Indexable.index)
: Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index) :=
Indexable.index_exn (Indexable.to_int32 idx).
Definition empty_indexes `{FArgs} : indexes :=
{| indexes.address_indexes := nil; indexes.ticket_indexes := nil; |}.
Definition assert_non_zero_quantity `{FArgs} (qty : Tx_rollup_l2_qty.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m) unit :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_when)
(Tx_rollup_l2_qty.op_eq qty Tx_rollup_l2_qty.zero)
(Build_extensible "Invalid_zero_transfer" unit tt).
ctxt_type → parameters → Alpha_context.Tx_rollup_message.t →
m (ctxt_type × Message_result.t);
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Module Make.
Class FArgs {Context_t : Set} {Context_m : Set → Set} := {
Context :
Tx_rollup_l2_context_sig.CONTEXT (t := Context_t) (m := Context_m);
}.
Arguments Build_FArgs {_ _}.
Definition ctxt_type `{FArgs} : Set :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.t).
Definition index_value `{FArgs} {A B C : Set}
(get_or_associate_index :
A → B →
Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(A × Tx_rollup_l2_context_sig.created_existed × Indexable.index B))
(add_index : C → B × Indexable.index B → C) (ctxt : A) (indexes_value : C)
(indexable : Indexable.t B)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m) (A × C × Indexable.index B) :=
match Indexable.destruct indexable with
| Either.Right v_value ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
(get_or_associate_index ctxt v_value)
(fun function_parameter ⇒
let '(ctxt, created, idx) := function_parameter in
match created with
| Tx_rollup_l2_context_sig.Existed ⇒ (ctxt, indexes_value, idx)
| Tx_rollup_l2_context_sig.Created ⇒
(ctxt, (add_index indexes_value (v_value, idx)), idx)
end)
| Either.Left i_value ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, i_value)
end.
Definition address_index `{FArgs}
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(indexes_value : indexes) (indexable : Indexable.t Tx_rollup_l2_address.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes ×
Indexable.index Tx_rollup_l2_address.t) :=
let get_or_associate_index :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
in
let add_index
(indexes_value : indexes)
(x_value : Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index)
: indexes :=
indexes.with_address_indexes
(cons x_value indexes_value.(indexes.address_indexes)) indexes_value in
index_value get_or_associate_index add_index ctxt indexes_value indexable.
Definition ticket_index `{FArgs}
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(indexes_value : indexes)
(indexable : Indexable.t Alpha_context.Ticket_hash.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes ×
Indexable.index Alpha_context.Ticket_hash.t) :=
let get_or_associate_index :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
in
let add_index
(indexes_value : indexes)
(x_value :
Alpha_context.Ticket_hash.t ×
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index))
: indexes :=
indexes.with_ticket_indexes
(cons x_value indexes_value.(indexes.ticket_indexes)) indexes_value in
index_value get_or_associate_index add_index ctxt indexes_value indexable.
Definition address_of_signer_index `{FArgs}
(idx : Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
: Tx_rollup_l2_address.Indexable.index :=
Indexable.index_exn (Indexable.to_int32 idx).
Definition signer_of_address_index `{FArgs}
(idx : Tx_rollup_l2_address.Indexable.index)
: Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index) :=
Indexable.index_exn (Indexable.to_int32 idx).
Definition empty_indexes `{FArgs} : indexes :=
{| indexes.address_indexes := nil; indexes.ticket_indexes := nil; |}.
Definition assert_non_zero_quantity `{FArgs} (qty : Tx_rollup_l2_qty.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m) unit :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_when)
(Tx_rollup_l2_qty.op_eq qty Tx_rollup_l2_qty.zero)
(Build_extensible "Invalid_zero_transfer" unit tt).
[get_metadata ctxt idx] returns the metadata associated to [idx] in
[ctxt]. It must have an associated metadata in the context, otherwise,
something went wrong in {!check_signature}.
Definition get_metadata `{FArgs}
(ctxt : ctxt_type) (idx : Tx_rollup_l2_context_sig.address_index)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Tx_rollup_l2_context_sig.metadata :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.get)
ctxt idx)
(fun metadata ⇒
match metadata with
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Unallocated_metadata" int32
(Indexable.to_int32 idx))
| Some metadata ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
metadata
end).
(ctxt : ctxt_type) (idx : Tx_rollup_l2_context_sig.address_index)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Tx_rollup_l2_context_sig.metadata :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.get)
ctxt idx)
(fun metadata ⇒
match metadata with
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Unallocated_metadata" int32
(Indexable.to_int32 idx))
| Some metadata ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
metadata
end).
[get_metadata_signer] gets the metadata for a signer using {!get_metadata}.
It transforms a signer index to an address one.
Definition get_metadata_signer `{FArgs}
(ctxt : ctxt_type)
(signer_idx :
Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Tx_rollup_l2_context_sig.metadata :=
get_metadata ctxt (address_of_signer_index signer_idx).
(ctxt : ctxt_type)
(signer_idx :
Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Tx_rollup_l2_context_sig.metadata :=
get_metadata ctxt (address_of_signer_index signer_idx).
[transfers ctxt source_idx destination_idx tidx amount] transfers [amount]
from [source_idx] to [destination_idx] of [tidx].
Definition transfer `{FArgs}
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(source_idx : Indexable.index Tx_rollup_l2_address.address)
(destination_idx : Indexable.index Tx_rollup_l2_address.address)
(tidx : Tx_rollup_l2_context_sig.ticket_index) (amount : Tx_rollup_l2_qty.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
((Indexable.compare_indexes source_idx destination_idx) ≠i 0)
(Build_extensible "Invalid_self_transfer" unit tt))
(fun function_parameter ⇒
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(assert_non_zero_quantity amount)
(fun function_parameter ⇒
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.spend)
ctxt tidx source_idx amount)
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.credit)
ctxt tidx destination_idx amount))).
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(source_idx : Indexable.index Tx_rollup_l2_address.address)
(destination_idx : Indexable.index Tx_rollup_l2_address.address)
(tidx : Tx_rollup_l2_context_sig.ticket_index) (amount : Tx_rollup_l2_qty.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
((Indexable.compare_indexes source_idx destination_idx) ≠i 0)
(Build_extensible "Invalid_self_transfer" unit tt))
(fun function_parameter ⇒
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(assert_non_zero_quantity amount)
(fun function_parameter ⇒
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.spend)
ctxt tidx source_idx amount)
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.credit)
ctxt tidx destination_idx amount))).
[deposit ctxt aidx tidx amount] credits [amount] of [tidx] to [aidx].
They are deposited from the layer1 and created in the layer2 context, but,
we only handle the creation part (i.e. in the layer2) in this module.
Definition deposit `{FArgs}
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(aidx : Tx_rollup_l2_context_sig.address_index)
(tidx : Tx_rollup_l2_context_sig.ticket_index) (amount : Tx_rollup_l2_qty.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.credit)
ctxt tidx aidx amount.
Module Batch_V1.
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(aidx : Tx_rollup_l2_context_sig.address_index)
(tidx : Tx_rollup_l2_context_sig.ticket_index) (amount : Tx_rollup_l2_qty.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.credit)
ctxt tidx aidx amount.
Module Batch_V1.
[operation_with_signer_index ctxt indexes op] takes an operation
and performs multiple get/sets on the context to return an operation
where the signer is replaced by its index.
It performs on the [ctxt]:
{ul {li If the signer is an index, we read the public key from the
[ctxt].}
{li If the signer is a public key, we associate a new index to
it in the [ctxt]. The public key is also added to the metadata
if not already present.}}
{b Note:} If the context already contains all the required information,
we only read from it.
Definition operation_with_signer_index `{FArgs}
(ctxt : ctxt_type) (indexes_value : indexes)
(op : Tx_rollup_l2_batch.V1.operation)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × Tx_rollup_l2_batch.V1.operation ×
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
match Indexable.destruct op.(Tx_rollup_l2_batch.V1.operation.signer)
with
| Either.Left signer_index ⇒
let address_index := address_of_signer_index signer_index in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(get_metadata ctxt address_index)
(fun metadata ⇒
let pk := metadata.(Tx_rollup_l2_context_sig.metadata.public_key)
in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, pk, address_index))
| Either.Right (Tx_rollup_l2_batch.Bls_pk signer_pk) ⇒
let addr :=
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) signer_pk in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
ctxt addr)
(fun function_parameter ⇒
let '(ctxt, created, idx) := function_parameter in
match created with
| Tx_rollup_l2_context_sig.Existed ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.get)
ctxt idx)
(fun metadata ⇒
match metadata with
| Some _ ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
ctxt
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.init_with_public_key)
ctxt idx signer_pk
end))
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, signer_pk, idx))
| Tx_rollup_l2_context_sig.Created ⇒
let indexes_value :=
indexes.with_address_indexes
(cons (addr, idx) indexes_value.(indexes.address_indexes))
indexes_value in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.init_with_public_key)
ctxt idx signer_pk)
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, signer_pk, idx))
end)
| Either.Right (Tx_rollup_l2_batch.L2_addr signer_addr) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get)
ctxt signer_addr)
(fun idx ⇒
match idx with
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Unknown_address" Tx_rollup_l2_address.t
signer_addr)
| Some idx ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(get_metadata ctxt idx)
(fun metadata ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value,
metadata.(Tx_rollup_l2_context_sig.metadata.public_key),
idx))
end)
end
(fun function_parameter ⇒
let '(ctxt, indexes_value, pk, idx) := function_parameter in
let op :=
Tx_rollup_l2_batch.V1.operation.with_signer
(signer_of_address_index idx) op in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, op, pk)).
(ctxt : ctxt_type) (indexes_value : indexes)
(op : Tx_rollup_l2_batch.V1.operation)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × Tx_rollup_l2_batch.V1.operation ×
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
match Indexable.destruct op.(Tx_rollup_l2_batch.V1.operation.signer)
with
| Either.Left signer_index ⇒
let address_index := address_of_signer_index signer_index in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(get_metadata ctxt address_index)
(fun metadata ⇒
let pk := metadata.(Tx_rollup_l2_context_sig.metadata.public_key)
in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, pk, address_index))
| Either.Right (Tx_rollup_l2_batch.Bls_pk signer_pk) ⇒
let addr :=
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) signer_pk in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
ctxt addr)
(fun function_parameter ⇒
let '(ctxt, created, idx) := function_parameter in
match created with
| Tx_rollup_l2_context_sig.Existed ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.get)
ctxt idx)
(fun metadata ⇒
match metadata with
| Some _ ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
ctxt
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.init_with_public_key)
ctxt idx signer_pk
end))
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, signer_pk, idx))
| Tx_rollup_l2_context_sig.Created ⇒
let indexes_value :=
indexes.with_address_indexes
(cons (addr, idx) indexes_value.(indexes.address_indexes))
indexes_value in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.init_with_public_key)
ctxt idx signer_pk)
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, signer_pk, idx))
end)
| Either.Right (Tx_rollup_l2_batch.L2_addr signer_addr) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get)
ctxt signer_addr)
(fun idx ⇒
match idx with
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Unknown_address" Tx_rollup_l2_address.t
signer_addr)
| Some idx ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(get_metadata ctxt idx)
(fun metadata ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value,
metadata.(Tx_rollup_l2_context_sig.metadata.public_key),
idx))
end)
end
(fun function_parameter ⇒
let '(ctxt, indexes_value, pk, idx) := function_parameter in
let op :=
Tx_rollup_l2_batch.V1.operation.with_signer
(signer_of_address_index idx) op in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, op, pk)).
[check_transaction ctxt indexes transmitted transaction] performs an
*active* check of an operation.
We consider this as an *active* check because the function is likely to
write in the [ctxt], since it replaces the signer's public key
(if provided) by its index in {!operation_with_signer_index}.
Outside of the active preprocessing, we check that a signer signs
at most one operation in the [transaction].
It also associates the signer to the bytes representation of a
transaction in [transmitted], which is used to check the aggregated
signature.
Definition check_transaction `{FArgs}
(ctxt : ctxt_type) (indexes_value : indexes)
(transmitted : list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes))
(transaction : Tx_rollup_l2_batch.V1.transaction)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes ×
list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
list Tx_rollup_l2_batch.V1.operation) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
match
Data_encoding.Binary.to_bytes_opt None
(Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
Tx_rollup_l2_batch.V1.compact_transaction) transaction with
| Some buf ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
buf
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Invalid_transaction_encoding" unit tt)
end
(fun buf ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (function_parameter :
ctxt_type × indexes ×
list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
list Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) ×
list Tx_rollup_l2_batch.V1.operation) ⇒
let '(ctxt, indexes_value, transmitted, signers, ops) :=
function_parameter in
fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(operation_with_signer_index ctxt indexes_value op)
(fun function_parameter ⇒
let '(ctxt, indexes_value, op, pk) := function_parameter
in
if
List.mem Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.equal)
pk signers
then
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Multiple_operations_for_signer"
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) pk)
else
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, (cons (pk, buf) transmitted),
(cons pk signers), (cons op ops))))
(ctxt, indexes_value, transmitted, nil, nil) transaction)
(fun function_parameter ⇒
let '(ctxt, indexes_value, transmitted, _, rev_ops) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, transmitted, (List.rev rev_ops)))).
Definition check_signature `{FArgs}
(ctxt : ctxt_type) (function_parameter : Tx_rollup_l2_batch.V1.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × Tx_rollup_l2_batch.V1.t) :=
let
'{|
Tx_rollup_l2_batch.V1.t.contents := transactions;
Tx_rollup_l2_batch.V1.t.aggregated_signature := aggregated_signature
|} as batch := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (function_parameter :
ctxt_type × indexes ×
list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
list Tx_rollup_l2_batch.V1.transaction) ⇒
let '(ctxt, indexes_value, transmitted, new_transactions) :=
function_parameter in
fun (transaction : Tx_rollup_l2_batch.V1.transaction) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(check_transaction ctxt indexes_value transmitted transaction)
(fun function_parameter ⇒
let '(ctxt, indexes_value, transmitted, transaction) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, transmitted,
(cons transaction new_transactions))))
(ctxt, empty_indexes, nil, nil) transactions)
(fun function_parameter ⇒
let '(ctxt, indexes_value, transmitted, rev_new_transactions) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.bls_verify) transmitted
aggregated_signature)
(fun b_value ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
b_value
(Build_extensible "Incorrect_aggregated_signature" unit tt))
(fun function_parameter ⇒
let '_ := function_parameter in
let batch :=
Tx_rollup_l2_batch.V1.t.with_contents
(List.rev rev_new_transactions) batch in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, batch)))).
(ctxt : ctxt_type) (indexes_value : indexes)
(transmitted : list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes))
(transaction : Tx_rollup_l2_batch.V1.transaction)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes ×
list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
list Tx_rollup_l2_batch.V1.operation) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
match
Data_encoding.Binary.to_bytes_opt None
(Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
Tx_rollup_l2_batch.V1.compact_transaction) transaction with
| Some buf ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
buf
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Invalid_transaction_encoding" unit tt)
end
(fun buf ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (function_parameter :
ctxt_type × indexes ×
list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
list Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) ×
list Tx_rollup_l2_batch.V1.operation) ⇒
let '(ctxt, indexes_value, transmitted, signers, ops) :=
function_parameter in
fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(operation_with_signer_index ctxt indexes_value op)
(fun function_parameter ⇒
let '(ctxt, indexes_value, op, pk) := function_parameter
in
if
List.mem Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.equal)
pk signers
then
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Multiple_operations_for_signer"
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) pk)
else
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, (cons (pk, buf) transmitted),
(cons pk signers), (cons op ops))))
(ctxt, indexes_value, transmitted, nil, nil) transaction)
(fun function_parameter ⇒
let '(ctxt, indexes_value, transmitted, _, rev_ops) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, transmitted, (List.rev rev_ops)))).
Definition check_signature `{FArgs}
(ctxt : ctxt_type) (function_parameter : Tx_rollup_l2_batch.V1.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × Tx_rollup_l2_batch.V1.t) :=
let
'{|
Tx_rollup_l2_batch.V1.t.contents := transactions;
Tx_rollup_l2_batch.V1.t.aggregated_signature := aggregated_signature
|} as batch := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (function_parameter :
ctxt_type × indexes ×
list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
list Tx_rollup_l2_batch.V1.transaction) ⇒
let '(ctxt, indexes_value, transmitted, new_transactions) :=
function_parameter in
fun (transaction : Tx_rollup_l2_batch.V1.transaction) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(check_transaction ctxt indexes_value transmitted transaction)
(fun function_parameter ⇒
let '(ctxt, indexes_value, transmitted, transaction) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, transmitted,
(cons transaction new_transactions))))
(ctxt, empty_indexes, nil, nil) transactions)
(fun function_parameter ⇒
let '(ctxt, indexes_value, transmitted, rev_new_transactions) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.bls_verify) transmitted
aggregated_signature)
(fun b_value ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
b_value
(Build_extensible "Incorrect_aggregated_signature" unit tt))
(fun function_parameter ⇒
let '_ := function_parameter in
let batch :=
Tx_rollup_l2_batch.V1.t.with_contents
(List.rev rev_new_transactions) batch in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, batch)))).
[apply_operation_content ctxt source content] performs the transfer
on the [ctxt]. The validity of the transfer is checked in
the context itself, e.g. for an invalid balance.
It returns the potential created indexes:
{ul {li The destination address index.}
{li The ticket exchanged index.}}
Definition apply_operation_content `{FArgs}
(ctxt : ctxt_type) (indexes_value : indexes)
(source_idx :
Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
(op_content : Tx_rollup_l2_batch.V1.operation_content)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × option Alpha_context.Tx_rollup_withdraw.t) :=
match op_content with
|
Tx_rollup_l2_batch.V1.Withdraw {|
Tx_rollup_l2_batch.V1.operation_content.Withdraw.destination := claimer;
Tx_rollup_l2_batch.V1.operation_content.Withdraw.ticket_hash :=
ticket_hash;
Tx_rollup_l2_batch.V1.operation_content.Withdraw.qty := amount
|} ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_index).(Tx_rollup_l2_context_sig.INDEX.get)
ctxt ticket_hash)
(fun tidx_opt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstarquestion)
(Option.value_e tidx_opt
(Build_extensible "Missing_ticket" Alpha_context.Ticket_hash.t
ticket_hash))
(fun tidx ⇒
let source_idx := address_of_signer_index source_idx in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(assert_non_zero_quantity amount)
(fun function_parameter ⇒
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.spend)
ctxt tidx source_idx amount)
(fun ctxt ⇒
let withdrawal :=
{|
Alpha_context.Tx_rollup_withdraw.order.claimer :=
claimer;
Alpha_context.Tx_rollup_withdraw.order.ticket_hash
:= ticket_hash;
Alpha_context.Tx_rollup_withdraw.order.amount :=
amount; |} in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, (Some withdrawal))))))
|
Tx_rollup_l2_batch.V1.Transfer {|
Tx_rollup_l2_batch.V1.operation_content.Transfer.destination := destination;
Tx_rollup_l2_batch.V1.operation_content.Transfer.ticket_hash :=
ticket_hash;
Tx_rollup_l2_batch.V1.operation_content.Transfer.qty := qty
|} ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(address_index ctxt indexes_value destination)
(fun function_parameter ⇒
let '(ctxt, indexes_value, dest_idx) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(ticket_index ctxt indexes_value ticket_hash)
(fun function_parameter ⇒
let '(ctxt, indexes_value, tidx) := function_parameter in
let source_idx := address_of_signer_index source_idx in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(transfer ctxt source_idx dest_idx tidx qty)
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, None))))
end.
(ctxt : ctxt_type) (indexes_value : indexes)
(source_idx :
Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
(op_content : Tx_rollup_l2_batch.V1.operation_content)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × option Alpha_context.Tx_rollup_withdraw.t) :=
match op_content with
|
Tx_rollup_l2_batch.V1.Withdraw {|
Tx_rollup_l2_batch.V1.operation_content.Withdraw.destination := claimer;
Tx_rollup_l2_batch.V1.operation_content.Withdraw.ticket_hash :=
ticket_hash;
Tx_rollup_l2_batch.V1.operation_content.Withdraw.qty := amount
|} ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_index).(Tx_rollup_l2_context_sig.INDEX.get)
ctxt ticket_hash)
(fun tidx_opt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstarquestion)
(Option.value_e tidx_opt
(Build_extensible "Missing_ticket" Alpha_context.Ticket_hash.t
ticket_hash))
(fun tidx ⇒
let source_idx := address_of_signer_index source_idx in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(assert_non_zero_quantity amount)
(fun function_parameter ⇒
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.spend)
ctxt tidx source_idx amount)
(fun ctxt ⇒
let withdrawal :=
{|
Alpha_context.Tx_rollup_withdraw.order.claimer :=
claimer;
Alpha_context.Tx_rollup_withdraw.order.ticket_hash
:= ticket_hash;
Alpha_context.Tx_rollup_withdraw.order.amount :=
amount; |} in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, (Some withdrawal))))))
|
Tx_rollup_l2_batch.V1.Transfer {|
Tx_rollup_l2_batch.V1.operation_content.Transfer.destination := destination;
Tx_rollup_l2_batch.V1.operation_content.Transfer.ticket_hash :=
ticket_hash;
Tx_rollup_l2_batch.V1.operation_content.Transfer.qty := qty
|} ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(address_index ctxt indexes_value destination)
(fun function_parameter ⇒
let '(ctxt, indexes_value, dest_idx) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(ticket_index ctxt indexes_value ticket_hash)
(fun function_parameter ⇒
let '(ctxt, indexes_value, tidx) := function_parameter in
let source_idx := address_of_signer_index source_idx in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(transfer ctxt source_idx dest_idx tidx qty)
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, None))))
end.
[check_counter ctxt signer counter] asserts that the provided [counter] is the
successor of the one associated to the [signer] in the [ctxt].
Definition check_counter `{FArgs}
(ctxt : ctxt_type)
(signer : Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.t))
(counter : int64) : Context.(Tx_rollup_l2_context_sig.CONTEXT.m) unit :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(get_metadata_signer ctxt signer)
(fun metadata ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
(counter =i64
(Int64.succ metadata.(Tx_rollup_l2_context_sig.metadata.counter)))
(Build_extensible "Counter_mismatch" Counter_mismatch
{|
Counter_mismatch.account :=
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
metadata.(Tx_rollup_l2_context_sig.metadata.public_key);
Counter_mismatch.expected :=
Int64.succ
metadata.(Tx_rollup_l2_context_sig.metadata.counter);
Counter_mismatch.provided := counter; |})).
(ctxt : ctxt_type)
(signer : Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.t))
(counter : int64) : Context.(Tx_rollup_l2_context_sig.CONTEXT.m) unit :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(get_metadata_signer ctxt signer)
(fun metadata ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
(counter =i64
(Int64.succ metadata.(Tx_rollup_l2_context_sig.metadata.counter)))
(Build_extensible "Counter_mismatch" Counter_mismatch
{|
Counter_mismatch.account :=
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
metadata.(Tx_rollup_l2_context_sig.metadata.public_key);
Counter_mismatch.expected :=
Int64.succ
metadata.(Tx_rollup_l2_context_sig.metadata.counter);
Counter_mismatch.provided := counter; |})).
[apply_operation ctxt indexes op] checks the counter validity for the [op.signer] with
{!check_counter}, and then calls {!apply_operation_content} for each content in [op].
Definition apply_operation `{FArgs}
(ctxt : ctxt_type) (indexes_value : indexes)
(function_parameter : Tx_rollup_l2_batch.V1.operation)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t) :=
let '{|
Tx_rollup_l2_batch.V1.operation.signer := signer;
Tx_rollup_l2_batch.V1.operation.counter := counter;
Tx_rollup_l2_batch.V1.operation.contents := contents
|} := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(check_counter ctxt signer counter)
(fun function_parameter ⇒
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (function_parameter :
ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
⇒
let '(ctxt, indexes_value, withdrawals) := function_parameter in
fun (content : Tx_rollup_l2_batch.V1.operation_content) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(apply_operation_content ctxt indexes_value signer content)
(fun function_parameter ⇒
let '(ctxt, indexes_value, withdrawal_opt) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value,
(Pervasives.op_at (Option.to_list withdrawal_opt)
withdrawals)))) (ctxt, indexes_value, nil) contents)
(fun function_parameter ⇒
let '(ctxt, indexes_value, rev_withdrawals) := function_parameter
in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, (List.rev rev_withdrawals)))).
(ctxt : ctxt_type) (indexes_value : indexes)
(function_parameter : Tx_rollup_l2_batch.V1.operation)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t) :=
let '{|
Tx_rollup_l2_batch.V1.operation.signer := signer;
Tx_rollup_l2_batch.V1.operation.counter := counter;
Tx_rollup_l2_batch.V1.operation.contents := contents
|} := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(check_counter ctxt signer counter)
(fun function_parameter ⇒
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (function_parameter :
ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
⇒
let '(ctxt, indexes_value, withdrawals) := function_parameter in
fun (content : Tx_rollup_l2_batch.V1.operation_content) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(apply_operation_content ctxt indexes_value signer content)
(fun function_parameter ⇒
let '(ctxt, indexes_value, withdrawal_opt) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value,
(Pervasives.op_at (Option.to_list withdrawal_opt)
withdrawals)))) (ctxt, indexes_value, nil) contents)
(fun function_parameter ⇒
let '(ctxt, indexes_value, rev_withdrawals) := function_parameter
in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, (List.rev rev_withdrawals)))).
[apply_transaction ctxt indexes transaction] applies each operation in
the [transaction]. It returns a {!transaction_result}, i.e. either
every operation in the [transaction] succedeed and the [ctxt] is
modified, or the [transaction] is a failure and the context
is left untouched.
Definition apply_transaction `{FArgs}
(initial_ctxt : ctxt_type) (initial_indexes : indexes)
(transaction : Tx_rollup_l2_batch.V1.transaction)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × Message_result.transaction_result ×
list Alpha_context.Tx_rollup_withdraw.t) :=
let fix fold
(params : ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
(index_value : int) (ops : list Tx_rollup_l2_batch.V1.operation)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × Message_result.transaction_result ×
list Alpha_context.Tx_rollup_withdraw.t) :=
let '(ctxt, prev_indexes, withdrawals) := params in
match ops with
| [] ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, prev_indexes, Message_result.Transaction_success, withdrawals)
| cons op rst ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.catch)
(apply_operation ctxt prev_indexes op)
(fun (function_parameter :
ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
⇒
let '(ctxt, indexes_value, op_withdrawals) := function_parameter
in
fold
(ctxt, indexes_value,
(Pervasives.op_at withdrawals op_withdrawals))
(index_value +i 1) rst)
(fun (reason_value : Error_monad._error) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(initial_ctxt, initial_indexes,
(Message_result.Transaction_failure
{|
Message_result.transaction_result.Transaction_failure.index
:= index_value;
Message_result.transaction_result.Transaction_failure.reason
:= reason_value; |}), nil)))
(fun function_parameter ⇒
let '(ctxt, indexes_value, status, withdrawals) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, status, withdrawals))
end in
fold (initial_ctxt, initial_indexes, nil) 0 transaction.
(initial_ctxt : ctxt_type) (initial_indexes : indexes)
(transaction : Tx_rollup_l2_batch.V1.transaction)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × Message_result.transaction_result ×
list Alpha_context.Tx_rollup_withdraw.t) :=
let fix fold
(params : ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
(index_value : int) (ops : list Tx_rollup_l2_batch.V1.operation)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × indexes × Message_result.transaction_result ×
list Alpha_context.Tx_rollup_withdraw.t) :=
let '(ctxt, prev_indexes, withdrawals) := params in
match ops with
| [] ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, prev_indexes, Message_result.Transaction_success, withdrawals)
| cons op rst ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.catch)
(apply_operation ctxt prev_indexes op)
(fun (function_parameter :
ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
⇒
let '(ctxt, indexes_value, op_withdrawals) := function_parameter
in
fold
(ctxt, indexes_value,
(Pervasives.op_at withdrawals op_withdrawals))
(index_value +i 1) rst)
(fun (reason_value : Error_monad._error) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(initial_ctxt, initial_indexes,
(Message_result.Transaction_failure
{|
Message_result.transaction_result.Transaction_failure.index
:= index_value;
Message_result.transaction_result.Transaction_failure.reason
:= reason_value; |}), nil)))
(fun function_parameter ⇒
let '(ctxt, indexes_value, status, withdrawals) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value, status, withdrawals))
end in
fold (initial_ctxt, initial_indexes, nil) 0 transaction.
[update_counters ctxt status transaction] updates the counters for
the signers of operations in [transaction]. If the [transaction]
failed because of a [Counter_mismatch] the counters are left
untouched.
Definition update_counters `{FArgs}
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(status : Message_result.transaction_result)
(transaction : list Tx_rollup_l2_batch.V1.operation)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
match status with
|
Message_result.Transaction_failure {|
Message_result.transaction_result.Transaction_failure.reason := err
|} ⇒
match err with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Counter_mismatch" then
let '_ := cast Counter_mismatch payload in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
ctxt
else
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t)) ⇒
fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.incr_counter)
ctxt
(address_of_signer_index
op.(Tx_rollup_l2_batch.V1.operation.signer))) ctxt
transaction
end
| Message_result.Transaction_success ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t)) ⇒
fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.incr_counter)
ctxt
(address_of_signer_index
op.(Tx_rollup_l2_batch.V1.operation.signer))) ctxt transaction
end.
Definition apply_batch `{FArgs}
(ctxt : ctxt_type) (parameters : parameters)
(batch : Tx_rollup_l2_batch.V1.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × Message_result.Batch_V1.(Storage_sigs.VALUE.t) ×
list Alpha_context.Tx_rollup_withdraw.t) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(check_signature ctxt batch)
(fun function_parameter ⇒
let '(ctxt, indexes_value, batch) := function_parameter in
let '{| Tx_rollup_l2_batch.V1.t.contents := contents |} := batch in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (function_parameter :
ctxt_type × indexes ×
list
(Tx_rollup_l2_batch.V1.transaction ×
Message_result.transaction_result) ×
list Alpha_context.Tx_rollup_withdraw.t) ⇒
let '(prev_ctxt, prev_indexes, results, withdrawals) :=
function_parameter in
fun (transaction : Tx_rollup_l2_batch.V1.transaction) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(apply_transaction prev_ctxt prev_indexes transaction)
(fun function_parameter ⇒
let
'(new_ctxt, new_indexes, status, transaction_withdrawals) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(update_counters new_ctxt status transaction)
(fun new_ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(new_ctxt, new_indexes,
(cons (transaction, status) results),
(Pervasives.op_at withdrawals
transaction_withdrawals)))))
(ctxt, indexes_value, nil, nil) contents)
(fun function_parameter ⇒
let '(ctxt, indexes_value, rev_results, withdrawals) :=
function_parameter in
let limit :=
parameters.(parameters.tx_rollup_max_withdrawals_per_batch) in
if Compare.List_length_with.op_gt withdrawals limit then
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Maximum_withdraws_per_message_exceeded"
Maximum_withdraws_per_message_exceeded
{|
Maximum_withdraws_per_message_exceeded.current :=
List.length withdrawals;
Maximum_withdraws_per_message_exceeded.maximum := limit;
|})
else
let results := List.rev rev_results in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt,
(Message_result.Batch_V1.Batch_result
{|
Message_result.Batch_V1.t.Batch_result.results :=
results;
Message_result.Batch_V1.t.Batch_result.indexes :=
indexes_value; |}), withdrawals))).
(* Batch_V1 *)
Definition module `{FArgs} :=
{|
BATCH_V1.apply_batch := apply_batch;
BATCH_V1.check_signature := check_signature
|}.
End Batch_V1.
Definition Batch_V1 `{FArgs}
: BATCH_V1 (ctxt_type := ctxt_type)
(m := fun (a : Set) ⇒ Context.(Tx_rollup_l2_context_sig.CONTEXT.m) a) :=
Batch_V1.module.
Definition apply_deposit `{FArgs}
(initial_ctxt : ctxt_type)
(function_parameter : Alpha_context.Tx_rollup_message.deposit)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × Message_result.deposit_result ×
option Alpha_context.Tx_rollup_withdraw.t) :=
let '{|
Tx_rollup_message_repr.deposit.sender := sender;
Tx_rollup_message_repr.deposit.destination := destination;
Tx_rollup_message_repr.deposit.ticket_hash := ticket_hash;
Tx_rollup_message_repr.deposit.amount := amount
|} := function_parameter in
let apply_deposit (function_parameter : unit)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes) :=
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(address_index initial_ctxt empty_indexes destination)
(fun function_parameter ⇒
let '(ctxt, indexes_value, aidx) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(ticket_index ctxt indexes_value (Indexable.value_value ticket_hash))
(fun function_parameter ⇒
let '(ctxt, indexes_value, tidx) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(deposit ctxt aidx tidx amount)
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value)))) in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.catch)
(apply_deposit tt)
(fun (function_parameter : ctxt_type × indexes) ⇒
let '(ctxt, indexes_value) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, (Message_result.Deposit_success indexes_value), None))
(fun (reason_value : Error_monad._error) ⇒
let withdrawal :=
{| Alpha_context.Tx_rollup_withdraw.order.claimer := sender;
Alpha_context.Tx_rollup_withdraw.order.ticket_hash := ticket_hash;
Alpha_context.Tx_rollup_withdraw.order.amount := amount; |} in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(initial_ctxt, (Message_result.Deposit_failure reason_value),
(Some withdrawal))).
Definition apply_message `{FArgs}
(ctxt : ctxt_type) (parameters : parameters)
(msg : Alpha_context.Tx_rollup_message.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × Message_result.t) :=
match msg with
| Alpha_context.Tx_rollup_message.Deposit deposit ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(apply_deposit ctxt deposit)
(fun function_parameter ⇒
let '(ctxt, result_value, withdrawl_opt) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt,
((Message_result.Deposit_result result_value),
(Option.to_list withdrawl_opt))))
| Alpha_context.Tx_rollup_message.Batch str ⇒
let batch :=
Data_encoding.Binary.of_string_opt Tx_rollup_l2_batch.encoding str in
match batch with
| Some (Tx_rollup_l2_batch.V1 batch) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Batch_V1.(BATCH_V1.apply_batch) ctxt parameters batch)
(fun function_parameter ⇒
let '(ctxt, result_value, withdrawals) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt,
((Message_result.Batch_V1_result result_value), withdrawals)))
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Invalid_batch_encoding" unit tt)
end
end.
(* Make *)
Definition functor `{FArgs} :=
{|
S.Batch_V1 := Batch_V1;
S.apply_deposit := apply_deposit;
S.apply_message := apply_message
|}.
End Make.
Definition Make {Context_t : Set} {Context_m : Set → Set}
(Context : Tx_rollup_l2_context_sig.CONTEXT (t := Context_t) (m := Context_m))
: S (ctxt_type := Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(m := fun (a : Set) ⇒ Context.(Tx_rollup_l2_context_sig.CONTEXT.m) a) :=
let '_ := Make.Build_FArgs Context in
Make.functor.
(ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(status : Message_result.transaction_result)
(transaction : list Tx_rollup_l2_batch.V1.operation)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
match status with
|
Message_result.Transaction_failure {|
Message_result.transaction_result.Transaction_failure.reason := err
|} ⇒
match err with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Counter_mismatch" then
let '_ := cast Counter_mismatch payload in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
ctxt
else
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t)) ⇒
fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.incr_counter)
ctxt
(address_of_signer_index
op.(Tx_rollup_l2_batch.V1.operation.signer))) ctxt
transaction
end
| Message_result.Transaction_success ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t)) ⇒
fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.incr_counter)
ctxt
(address_of_signer_index
op.(Tx_rollup_l2_batch.V1.operation.signer))) ctxt transaction
end.
Definition apply_batch `{FArgs}
(ctxt : ctxt_type) (parameters : parameters)
(batch : Tx_rollup_l2_batch.V1.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × Message_result.Batch_V1.(Storage_sigs.VALUE.t) ×
list Alpha_context.Tx_rollup_withdraw.t) :=
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(check_signature ctxt batch)
(fun function_parameter ⇒
let '(ctxt, indexes_value, batch) := function_parameter in
let '{| Tx_rollup_l2_batch.V1.t.contents := contents |} := batch in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
(fun (function_parameter :
ctxt_type × indexes ×
list
(Tx_rollup_l2_batch.V1.transaction ×
Message_result.transaction_result) ×
list Alpha_context.Tx_rollup_withdraw.t) ⇒
let '(prev_ctxt, prev_indexes, results, withdrawals) :=
function_parameter in
fun (transaction : Tx_rollup_l2_batch.V1.transaction) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(apply_transaction prev_ctxt prev_indexes transaction)
(fun function_parameter ⇒
let
'(new_ctxt, new_indexes, status, transaction_withdrawals) :=
function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(update_counters new_ctxt status transaction)
(fun new_ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(new_ctxt, new_indexes,
(cons (transaction, status) results),
(Pervasives.op_at withdrawals
transaction_withdrawals)))))
(ctxt, indexes_value, nil, nil) contents)
(fun function_parameter ⇒
let '(ctxt, indexes_value, rev_results, withdrawals) :=
function_parameter in
let limit :=
parameters.(parameters.tx_rollup_max_withdrawals_per_batch) in
if Compare.List_length_with.op_gt withdrawals limit then
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Maximum_withdraws_per_message_exceeded"
Maximum_withdraws_per_message_exceeded
{|
Maximum_withdraws_per_message_exceeded.current :=
List.length withdrawals;
Maximum_withdraws_per_message_exceeded.maximum := limit;
|})
else
let results := List.rev rev_results in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt,
(Message_result.Batch_V1.Batch_result
{|
Message_result.Batch_V1.t.Batch_result.results :=
results;
Message_result.Batch_V1.t.Batch_result.indexes :=
indexes_value; |}), withdrawals))).
(* Batch_V1 *)
Definition module `{FArgs} :=
{|
BATCH_V1.apply_batch := apply_batch;
BATCH_V1.check_signature := check_signature
|}.
End Batch_V1.
Definition Batch_V1 `{FArgs}
: BATCH_V1 (ctxt_type := ctxt_type)
(m := fun (a : Set) ⇒ Context.(Tx_rollup_l2_context_sig.CONTEXT.m) a) :=
Batch_V1.module.
Definition apply_deposit `{FArgs}
(initial_ctxt : ctxt_type)
(function_parameter : Alpha_context.Tx_rollup_message.deposit)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × Message_result.deposit_result ×
option Alpha_context.Tx_rollup_withdraw.t) :=
let '{|
Tx_rollup_message_repr.deposit.sender := sender;
Tx_rollup_message_repr.deposit.destination := destination;
Tx_rollup_message_repr.deposit.ticket_hash := ticket_hash;
Tx_rollup_message_repr.deposit.amount := amount
|} := function_parameter in
let apply_deposit (function_parameter : unit)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes) :=
let '_ := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(address_index initial_ctxt empty_indexes destination)
(fun function_parameter ⇒
let '(ctxt, indexes_value, aidx) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(ticket_index ctxt indexes_value (Indexable.value_value ticket_hash))
(fun function_parameter ⇒
let '(ctxt, indexes_value, tidx) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(deposit ctxt aidx tidx amount)
(fun ctxt ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, indexes_value)))) in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.catch)
(apply_deposit tt)
(fun (function_parameter : ctxt_type × indexes) ⇒
let '(ctxt, indexes_value) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt, (Message_result.Deposit_success indexes_value), None))
(fun (reason_value : Error_monad._error) ⇒
let withdrawal :=
{| Alpha_context.Tx_rollup_withdraw.order.claimer := sender;
Alpha_context.Tx_rollup_withdraw.order.ticket_hash := ticket_hash;
Alpha_context.Tx_rollup_withdraw.order.amount := amount; |} in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(initial_ctxt, (Message_result.Deposit_failure reason_value),
(Some withdrawal))).
Definition apply_message `{FArgs}
(ctxt : ctxt_type) (parameters : parameters)
(msg : Alpha_context.Tx_rollup_message.t)
: Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
(ctxt_type × Message_result.t) :=
match msg with
| Alpha_context.Tx_rollup_message.Deposit deposit ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(apply_deposit ctxt deposit)
(fun function_parameter ⇒
let '(ctxt, result_value, withdrawl_opt) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt,
((Message_result.Deposit_result result_value),
(Option.to_list withdrawl_opt))))
| Alpha_context.Tx_rollup_message.Batch str ⇒
let batch :=
Data_encoding.Binary.of_string_opt Tx_rollup_l2_batch.encoding str in
match batch with
| Some (Tx_rollup_l2_batch.V1 batch) ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
(Batch_V1.(BATCH_V1.apply_batch) ctxt parameters batch)
(fun function_parameter ⇒
let '(ctxt, result_value, withdrawals) := function_parameter in
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
(ctxt,
((Message_result.Batch_V1_result result_value), withdrawals)))
| None ⇒
Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
(Build_extensible "Invalid_batch_encoding" unit tt)
end
end.
(* Make *)
Definition functor `{FArgs} :=
{|
S.Batch_V1 := Batch_V1;
S.apply_deposit := apply_deposit;
S.apply_message := apply_message
|}.
End Make.
Definition Make {Context_t : Set} {Context_m : Set → Set}
(Context : Tx_rollup_l2_context_sig.CONTEXT (t := Context_t) (m := Context_m))
: S (ctxt_type := Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
(m := fun (a : Set) ⇒ Context.(Tx_rollup_l2_context_sig.CONTEXT.m) a) :=
let '_ := Make.Build_FArgs Context in
Make.functor.