🏗️ Apply.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Amendment.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Baking.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_cache.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_interpreter.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size_costs.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Ticket_accounting.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_parameters.
Inductive denunciation_kind : Set :=
| Preendorsement : denunciation_kind
| Endorsement : denunciation_kind
| Block : denunciation_kind.
Definition denunciation_kind_encoding
: Data_encoding.encoding denunciation_kind :=
Data_encoding.string_enum
[
("preendorsement", Preendorsement);
("endorsement", Endorsement);
("block", Block)
].
Definition pp_denunciation_kind
(fmt : Format.formatter) (function_parameter : denunciation_kind) : unit :=
match function_parameter with
| Preendorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "preendorsement"
CamlinternalFormatBasics.End_of_format) "preendorsement")
| Endorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "endorsement"
CamlinternalFormatBasics.End_of_format) "endorsement")
| Block ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "baking"
CamlinternalFormatBasics.End_of_format) "baking")
end.
Module Not_enough_endorsements.
Record record : Set := Build {
required : int;
provided : int;
}.
Definition with_required required (r : record) :=
Build required r.(provided).
Definition with_provided provided (r : record) :=
Build r.(required) provided.
End Not_enough_endorsements.
Definition Not_enough_endorsements := Not_enough_endorsements.record.
Module Invalid_double_baking_evidence.
Record record : Set := Build {
hash1 : Block_hash.t;
level1 : Alpha_context.Raw_level.t;
round1 : Alpha_context.Round.t;
hash2 : Block_hash.t;
level2 : Alpha_context.Raw_level.t;
round2 : Alpha_context.Round.t;
}.
Definition with_hash1 hash1 (r : record) :=
Build hash1 r.(level1) r.(round1) r.(hash2) r.(level2) r.(round2).
Definition with_level1 level1 (r : record) :=
Build r.(hash1) level1 r.(round1) r.(hash2) r.(level2) r.(round2).
Definition with_round1 round1 (r : record) :=
Build r.(hash1) r.(level1) round1 r.(hash2) r.(level2) r.(round2).
Definition with_hash2 hash2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) hash2 r.(level2) r.(round2).
Definition with_level2 level2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) r.(hash2) level2 r.(round2).
Definition with_round2 round2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) r.(hash2) r.(level2) round2.
End Invalid_double_baking_evidence.
Definition Invalid_double_baking_evidence :=
Invalid_double_baking_evidence.record.
Module Wrong_level_for_consensus_operation.
Record record : Set := Build {
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_level_for_consensus_operation.
Definition Wrong_level_for_consensus_operation :=
Wrong_level_for_consensus_operation.record.
Module Wrong_round_for_consensus_operation.
Record record : Set := Build {
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_round_for_consensus_operation.
Definition Wrong_round_for_consensus_operation :=
Wrong_round_for_consensus_operation.record.
Module Preendorsement_round_too_high.
Record record : Set := Build {
block_round : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_block_round block_round (r : record) :=
Build block_round r.(provided).
Definition with_provided provided (r : record) :=
Build r.(block_round) provided.
End Preendorsement_round_too_high.
Definition Preendorsement_round_too_high :=
Preendorsement_round_too_high.record.
Module Wrong_payload_hash_for_consensus_operation.
Record record : Set := Build {
expected : Block_payload_hash.t;
provided : Block_payload_hash.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_payload_hash_for_consensus_operation.
Definition Wrong_payload_hash_for_consensus_operation :=
Wrong_payload_hash_for_consensus_operation.record.
Module Consensus_operation_for_future_level.
Record record : Set := Build {
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_for_future_level.
Definition Consensus_operation_for_future_level :=
Consensus_operation_for_future_level.record.
Module Consensus_operation_for_future_round.
Record record : Set := Build {
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_for_future_round.
Definition Consensus_operation_for_future_round :=
Consensus_operation_for_future_round.record.
Module Consensus_operation_for_old_level.
Record record : Set := Build {
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_for_old_level.
Definition Consensus_operation_for_old_level :=
Consensus_operation_for_old_level.record.
Module Consensus_operation_for_old_round.
Record record : Set := Build {
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_for_old_round.
Definition Consensus_operation_for_old_round :=
Consensus_operation_for_old_round.record.
Module Consensus_operation_on_competing_proposal.
Record record : Set := Build {
expected : Block_payload_hash.t;
provided : Block_payload_hash.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_on_competing_proposal.
Definition Consensus_operation_on_competing_proposal :=
Consensus_operation_on_competing_proposal.record.
Module Set_deposits_limit_too_high.
Record record : Set := Build {
limit : Alpha_context.Tez.t;
max_limit : Alpha_context.Tez.t;
}.
Definition with_limit limit (r : record) :=
Build limit r.(max_limit).
Definition with_max_limit max_limit (r : record) :=
Build r.(limit) max_limit.
End Set_deposits_limit_too_high.
Definition Set_deposits_limit_too_high := Set_deposits_limit_too_high.record.
Module Wrong_voting_period.
Record record : Set := Build {
expected : int32;
provided : int32;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_voting_period.
Definition Wrong_voting_period := Wrong_voting_period.record.
Module Inconsistent_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
delegate1 : Signature.public_key_hash;
delegate2 : Signature.public_key_hash;
}.
Definition with_kind kind (r : record) :=
Build kind r.(delegate1) r.(delegate2).
Definition with_delegate1 delegate1 (r : record) :=
Build r.(kind) delegate1 r.(delegate2).
Definition with_delegate2 delegate2 (r : record) :=
Build r.(kind) r.(delegate1) delegate2.
End Inconsistent_denunciation.
Definition Inconsistent_denunciation := Inconsistent_denunciation.record.
Module Too_early_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
level : Alpha_context.Raw_level.t;
current : Alpha_context.Raw_level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(level) r.(current).
Definition with_level level (r : record) :=
Build r.(kind) level r.(current).
Definition with_current current (r : record) :=
Build r.(kind) r.(level) current.
End Too_early_denunciation.
Definition Too_early_denunciation := Too_early_denunciation.record.
Module Outdated_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
level : Alpha_context.Raw_level.t;
last_cycle : Alpha_context.Cycle.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(level) r.(last_cycle).
Definition with_level level (r : record) :=
Build r.(kind) level r.(last_cycle).
Definition with_last_cycle last_cycle (r : record) :=
Build r.(kind) r.(level) last_cycle.
End Outdated_denunciation.
Definition Outdated_denunciation := Outdated_denunciation.record.
Module Invalid_activation.
Record record : Set := Build {
pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t);
}.
Definition with_pkh pkh (r : record) :=
Build pkh.
End Invalid_activation.
Definition Invalid_activation := Invalid_activation.record.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Amendment.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Baking.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_cache.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_interpreter.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size_costs.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Ticket_accounting.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_parameters.
Inductive denunciation_kind : Set :=
| Preendorsement : denunciation_kind
| Endorsement : denunciation_kind
| Block : denunciation_kind.
Definition denunciation_kind_encoding
: Data_encoding.encoding denunciation_kind :=
Data_encoding.string_enum
[
("preendorsement", Preendorsement);
("endorsement", Endorsement);
("block", Block)
].
Definition pp_denunciation_kind
(fmt : Format.formatter) (function_parameter : denunciation_kind) : unit :=
match function_parameter with
| Preendorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "preendorsement"
CamlinternalFormatBasics.End_of_format) "preendorsement")
| Endorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "endorsement"
CamlinternalFormatBasics.End_of_format) "endorsement")
| Block ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "baking"
CamlinternalFormatBasics.End_of_format) "baking")
end.
Module Not_enough_endorsements.
Record record : Set := Build {
required : int;
provided : int;
}.
Definition with_required required (r : record) :=
Build required r.(provided).
Definition with_provided provided (r : record) :=
Build r.(required) provided.
End Not_enough_endorsements.
Definition Not_enough_endorsements := Not_enough_endorsements.record.
Module Invalid_double_baking_evidence.
Record record : Set := Build {
hash1 : Block_hash.t;
level1 : Alpha_context.Raw_level.t;
round1 : Alpha_context.Round.t;
hash2 : Block_hash.t;
level2 : Alpha_context.Raw_level.t;
round2 : Alpha_context.Round.t;
}.
Definition with_hash1 hash1 (r : record) :=
Build hash1 r.(level1) r.(round1) r.(hash2) r.(level2) r.(round2).
Definition with_level1 level1 (r : record) :=
Build r.(hash1) level1 r.(round1) r.(hash2) r.(level2) r.(round2).
Definition with_round1 round1 (r : record) :=
Build r.(hash1) r.(level1) round1 r.(hash2) r.(level2) r.(round2).
Definition with_hash2 hash2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) hash2 r.(level2) r.(round2).
Definition with_level2 level2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) r.(hash2) level2 r.(round2).
Definition with_round2 round2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) r.(hash2) r.(level2) round2.
End Invalid_double_baking_evidence.
Definition Invalid_double_baking_evidence :=
Invalid_double_baking_evidence.record.
Module Wrong_level_for_consensus_operation.
Record record : Set := Build {
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_level_for_consensus_operation.
Definition Wrong_level_for_consensus_operation :=
Wrong_level_for_consensus_operation.record.
Module Wrong_round_for_consensus_operation.
Record record : Set := Build {
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_round_for_consensus_operation.
Definition Wrong_round_for_consensus_operation :=
Wrong_round_for_consensus_operation.record.
Module Preendorsement_round_too_high.
Record record : Set := Build {
block_round : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_block_round block_round (r : record) :=
Build block_round r.(provided).
Definition with_provided provided (r : record) :=
Build r.(block_round) provided.
End Preendorsement_round_too_high.
Definition Preendorsement_round_too_high :=
Preendorsement_round_too_high.record.
Module Wrong_payload_hash_for_consensus_operation.
Record record : Set := Build {
expected : Block_payload_hash.t;
provided : Block_payload_hash.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_payload_hash_for_consensus_operation.
Definition Wrong_payload_hash_for_consensus_operation :=
Wrong_payload_hash_for_consensus_operation.record.
Module Consensus_operation_for_future_level.
Record record : Set := Build {
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_for_future_level.
Definition Consensus_operation_for_future_level :=
Consensus_operation_for_future_level.record.
Module Consensus_operation_for_future_round.
Record record : Set := Build {
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_for_future_round.
Definition Consensus_operation_for_future_round :=
Consensus_operation_for_future_round.record.
Module Consensus_operation_for_old_level.
Record record : Set := Build {
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_for_old_level.
Definition Consensus_operation_for_old_level :=
Consensus_operation_for_old_level.record.
Module Consensus_operation_for_old_round.
Record record : Set := Build {
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_for_old_round.
Definition Consensus_operation_for_old_round :=
Consensus_operation_for_old_round.record.
Module Consensus_operation_on_competing_proposal.
Record record : Set := Build {
expected : Block_payload_hash.t;
provided : Block_payload_hash.t;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Consensus_operation_on_competing_proposal.
Definition Consensus_operation_on_competing_proposal :=
Consensus_operation_on_competing_proposal.record.
Module Set_deposits_limit_too_high.
Record record : Set := Build {
limit : Alpha_context.Tez.t;
max_limit : Alpha_context.Tez.t;
}.
Definition with_limit limit (r : record) :=
Build limit r.(max_limit).
Definition with_max_limit max_limit (r : record) :=
Build r.(limit) max_limit.
End Set_deposits_limit_too_high.
Definition Set_deposits_limit_too_high := Set_deposits_limit_too_high.record.
Module Wrong_voting_period.
Record record : Set := Build {
expected : int32;
provided : int32;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_voting_period.
Definition Wrong_voting_period := Wrong_voting_period.record.
Module Inconsistent_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
delegate1 : Signature.public_key_hash;
delegate2 : Signature.public_key_hash;
}.
Definition with_kind kind (r : record) :=
Build kind r.(delegate1) r.(delegate2).
Definition with_delegate1 delegate1 (r : record) :=
Build r.(kind) delegate1 r.(delegate2).
Definition with_delegate2 delegate2 (r : record) :=
Build r.(kind) r.(delegate1) delegate2.
End Inconsistent_denunciation.
Definition Inconsistent_denunciation := Inconsistent_denunciation.record.
Module Too_early_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
level : Alpha_context.Raw_level.t;
current : Alpha_context.Raw_level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(level) r.(current).
Definition with_level level (r : record) :=
Build r.(kind) level r.(current).
Definition with_current current (r : record) :=
Build r.(kind) r.(level) current.
End Too_early_denunciation.
Definition Too_early_denunciation := Too_early_denunciation.record.
Module Outdated_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
level : Alpha_context.Raw_level.t;
last_cycle : Alpha_context.Cycle.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(level) r.(last_cycle).
Definition with_level level (r : record) :=
Build r.(kind) level r.(last_cycle).
Definition with_last_cycle last_cycle (r : record) :=
Build r.(kind) r.(level) last_cycle.
End Outdated_denunciation.
Definition Outdated_denunciation := Outdated_denunciation.record.
Module Invalid_activation.
Record record : Set := Build {
pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t);
}.
Definition with_pkh pkh (r : record) :=
Build pkh.
End Invalid_activation.
Definition Invalid_activation := Invalid_activation.record.
Init function; without side-effects in Coq
Definition init_module1 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operations.wrong_slot" "Wrong slot" "wrong slot"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "wrong slot"
CamlinternalFormatBasics.End_of_format) "wrong slot")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_slot_used_for_consensus_operation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Wrong_slot_used_for_consensus_operation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.not_enough_endorsements" "Not enough endorsements"
"The block being validated does not include the required minimum number of endorsements."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int × int) ⇒
let '(required, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong number of endorsements ("
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal "), at least "
(CamlinternalFormatBasics.Int
CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " are expected"
CamlinternalFormatBasics.End_of_format)))))
"Wrong number of endorsements (%i), at least %i are expected")
provided required))
(Data_encoding.obj2
(Data_encoding.req None None "required" Data_encoding.int31)
(Data_encoding.req None None "provided" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Not_enough_endorsements" then
let '{|
Not_enough_endorsements.required := required;
Not_enough_endorsements.provided := provided
|} := cast Not_enough_endorsements payload in
Some (required, provided)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(required, provided) := function_parameter in
Build_extensible "Not_enough_endorsements" Not_enough_endorsements
{| Not_enough_endorsements.required := required;
Not_enough_endorsements.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.wrong_consensus_operation_branch"
"Wrong consensus operation branch"
"Trying to include an endorsement or preendorsement which points to the wrong block.\n It should be the predecessor for preendorsements and the grandfather for endorsements."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Block_hash.t × Block_hash.t) ⇒
let '(e_value, p_value) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Wrong branch "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", expected "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"Wrong branch %a, expected %a") Block_hash.pp p_value
Block_hash.pp e_value))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Block_hash.encoding)
(Data_encoding.req None None "provided" Block_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_consensus_operation_branch" then
let '(e_value, p_value) :=
cast (Block_hash.t × Block_hash.t) payload in
Some (e_value, p_value)
else None
end)
(fun (function_parameter : Block_hash.t × Block_hash.t) ⇒
let '(e_value, p_value) := function_parameter in
Build_extensible "Wrong_consensus_operation_branch"
(Block_hash.t × Block_hash.t) (e_value, p_value)) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.invalid_double_baking_evidence" "Invalid double baking evidence"
"A double-baking evidence is inconsistent (two distinct level)"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Block_hash.t × Alpha_context.Raw_level.raw_level ×
Alpha_context.Round.t × Block_hash.t ×
Alpha_context.Raw_level.raw_level × Alpha_context.Round.t) ⇒
let '(hash1, level1, round1, hash2, level2, round2) :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid double-baking evidence (hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", levels/rounds: ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
") and ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal
"," % char
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
"))"
CamlinternalFormatBasics.End_of_format)))))))))))))
"Invalid double-baking evidence (hash: %a and %a, levels/rounds: (%ld,%ld) and (%ld,%ld))")
Block_hash.pp hash1 Block_hash.pp hash2
(Alpha_context.Raw_level.to_int32 level1)
(Alpha_context.Round.to_int32 round1)
(Alpha_context.Raw_level.to_int32 level2)
(Alpha_context.Round.to_int32 round2)))
(Data_encoding.obj6
(Data_encoding.req None None "hash1" Block_hash.encoding)
(Data_encoding.req None None "level1" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "round1" Alpha_context.Round.encoding)
(Data_encoding.req None None "hash2" Block_hash.encoding)
(Data_encoding.req None None "level2" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "round2" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_double_baking_evidence" then
let '{|
Invalid_double_baking_evidence.hash1 := hash1;
Invalid_double_baking_evidence.level1 := level1;
Invalid_double_baking_evidence.round1 := round1;
Invalid_double_baking_evidence.hash2 := hash2;
Invalid_double_baking_evidence.level2 := level2;
Invalid_double_baking_evidence.round2 := round2
|} := cast Invalid_double_baking_evidence payload in
Some (hash1, level1, round1, hash2, level2, round2)
else None
end)
(fun (function_parameter :
Block_hash.t × Alpha_context.Raw_level.raw_level × Alpha_context.Round.t
× Block_hash.t × Alpha_context.Raw_level.raw_level ×
Alpha_context.Round.t) ⇒
let '(hash1, level1, round1, hash2, level2, round2) :=
function_parameter in
Build_extensible "Invalid_double_baking_evidence"
Invalid_double_baking_evidence
{| Invalid_double_baking_evidence.hash1 := hash1;
Invalid_double_baking_evidence.level1 := level1;
Invalid_double_baking_evidence.round1 := round1;
Invalid_double_baking_evidence.hash2 := hash2;
Invalid_double_baking_evidence.level2 := level2;
Invalid_double_baking_evidence.round2 := round2; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"wrong_level_for_consensus_operation"
"Wrong level for consensus operation"
"Wrong level for consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong level for consensus operation (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Wrong level for consensus operation (expected: %a, provided: %a).")
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_level_for_consensus_operation" then
let '{|
Wrong_level_for_consensus_operation.expected := expected;
Wrong_level_for_consensus_operation.provided := provided
|} := cast Wrong_level_for_consensus_operation payload in
Some (expected, provided)
else None
end)
(fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_level_for_consensus_operation"
Wrong_level_for_consensus_operation
{| Wrong_level_for_consensus_operation.expected := expected;
Wrong_level_for_consensus_operation.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"wrong_round_for_consensus_operation"
"Wrong round for consensus operation"
"Wrong round for consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong round for consensus operation (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Wrong round for consensus operation (expected: %a, provided: %a).")
Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_round_for_consensus_operation" then
let '{|
Wrong_round_for_consensus_operation.expected := expected;
Wrong_round_for_consensus_operation.provided := provided
|} := cast Wrong_round_for_consensus_operation payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_round_for_consensus_operation"
Wrong_round_for_consensus_operation
{| Wrong_round_for_consensus_operation.expected := expected;
Wrong_round_for_consensus_operation.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"preendorsement_round_too_high" "Preendorsement round too high"
"Preendorsement round too high."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(block_round, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Preendorsement round too high (block_round: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Preendorsement round too high (block_round: %a, provided: %a).")
Alpha_context.Round.pp block_round Alpha_context.Round.pp provided))
(Data_encoding.obj2
(Data_encoding.req None None "block_round" Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Preendorsement_round_too_high" then
let '{|
Preendorsement_round_too_high.block_round := block_round;
Preendorsement_round_too_high.provided := provided
|} := cast Preendorsement_round_too_high payload in
Some (block_round, provided)
else None
end)
(fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
⇒
let '(block_round, provided) := function_parameter in
Build_extensible "Preendorsement_round_too_high"
Preendorsement_round_too_high
{| Preendorsement_round_too_high.block_round := block_round;
Preendorsement_round_too_high.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"wrong_payload_hash_for_consensus_operation"
"Wrong payload hash for consensus operation"
"Wrong payload hash for consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t)
⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong payload hash for consensus operation (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Wrong payload hash for consensus operation (expected: %a, provided: %a).")
Block_payload_hash.pp_short expected Block_payload_hash.pp_short
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Block_payload_hash.encoding)
(Data_encoding.req None None "provided" Block_payload_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_payload_hash_for_consensus_operation" then
let '{|
Wrong_payload_hash_for_consensus_operation.expected := expected;
Wrong_payload_hash_for_consensus_operation.provided := provided
|} := cast Wrong_payload_hash_for_consensus_operation payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_payload_hash_for_consensus_operation"
Wrong_payload_hash_for_consensus_operation
{| Wrong_payload_hash_for_consensus_operation.expected := expected;
Wrong_payload_hash_for_consensus_operation.provided := provided; |})
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"unexpected_endorsement_in_block" "Unexpected endorsement in block"
"Unexpected endorsement in block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unexpected endorsement in block."
CamlinternalFormatBasics.End_of_format)
"Unexpected endorsement in block."))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_endorsement_in_block" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_endorsement_in_block" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"unexpected_preendorsement_in_block" "Unexpected preendorsement in block"
"Unexpected preendorsement in block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unexpected preendorsement in block."
CamlinternalFormatBasics.End_of_format)
"Unexpected preendorsement in block."))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_preendorsement_in_block" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_preendorsement_in_block" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"consensus_operation_for_future_level"
"Consensus operation for future level"
"Consensus operation for future level."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation for future level\n (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation for future level\n (expected: %a, provided: %a).")
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_future_level" then
let '{|
Consensus_operation_for_future_level.expected := expected;
Consensus_operation_for_future_level.provided := provided
|} := cast Consensus_operation_for_future_level payload in
Some (expected, provided)
else None
end)
(fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_future_level"
Consensus_operation_for_future_level
{| Consensus_operation_for_future_level.expected := expected;
Consensus_operation_for_future_level.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"consensus_operation_for_future_round"
"Consensus operation for future round"
"Consensus operation for future round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation for future round (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation for future round (expected: %a, provided: %a).")
Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected_max" Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_future_round" then
let '{|
Consensus_operation_for_future_round.expected := expected;
Consensus_operation_for_future_round.provided := provided
|} := cast Consensus_operation_for_future_round payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_future_round"
Consensus_operation_for_future_round
{| Consensus_operation_for_future_round.expected := expected;
Consensus_operation_for_future_round.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Outdated
"consensus_operation_for_old_level" "Consensus operation for old level"
"Consensus operation for old level."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation for old level (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation for old level (expected: %a, provided: %a).")
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_old_level" then
let '{|
Consensus_operation_for_old_level.expected := expected;
Consensus_operation_for_old_level.provided := provided
|} := cast Consensus_operation_for_old_level payload in
Some (expected, provided)
else None
end)
(fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_old_level"
Consensus_operation_for_old_level
{| Consensus_operation_for_old_level.expected := expected;
Consensus_operation_for_old_level.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"consensus_operation_for_old_round" "Consensus operation for old round"
"Consensus operation for old round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation for old round (expected_min: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation for old round (expected_min: %a, provided: %a).")
Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected_min" Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_old_round" then
let '{|
Consensus_operation_for_old_round.expected := expected;
Consensus_operation_for_old_round.provided := provided
|} := cast Consensus_operation_for_old_round payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_old_round"
Consensus_operation_for_old_round
{| Consensus_operation_for_old_round.expected := expected;
Consensus_operation_for_old_round.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"consensus_operation_on_competing_proposal"
"Consensus operation on competing proposal"
"Consensus operation on competing proposal."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t)
⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation on competing proposal (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation on competing proposal (expected: %a, provided: %a).")
Block_payload_hash.pp_short expected Block_payload_hash.pp_short
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Block_payload_hash.encoding)
(Data_encoding.req None None "provided" Block_payload_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_on_competing_proposal" then
let '{|
Consensus_operation_on_competing_proposal.expected := expected;
Consensus_operation_on_competing_proposal.provided := provided
|} := cast Consensus_operation_on_competing_proposal payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_on_competing_proposal"
Consensus_operation_on_competing_proposal
{| Consensus_operation_on_competing_proposal.expected := expected;
Consensus_operation_on_competing_proposal.provided := provided; |})
in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.set_deposits_limit_on_unregistered_delegate"
"Set deposits limit on an unregistered delegate"
"Cannot set deposits limit on an unregistered delegate."
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot set a deposits limit on the unregistered delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Cannot set a deposits limit on the unregistered delegate %a.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) c_value))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Set_deposits_limit_on_unregistered_delegate" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Set_deposits_limit_on_unregistered_delegate"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.set_deposits_limit_too_high"
"Set deposits limit to a too high value"
"Cannot set deposits limit such that the active stake overflows."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Alpha_context.Tez.t × Alpha_context.Tez.t)
⇒
let '(limit, max_limit) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot set deposits limit to "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" as it is higher the allowed maximum "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Cannot set deposits limit to %a as it is higher the allowed maximum %a.")
Alpha_context.Tez.pp limit Alpha_context.Tez.pp max_limit))
(Data_encoding.obj2
(Data_encoding.req None None "limit" Alpha_context.Tez.encoding)
(Data_encoding.req None None "max_limit" Alpha_context.Tez.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Set_deposits_limit_too_high" then
let '{|
Set_deposits_limit_too_high.limit := limit;
Set_deposits_limit_too_high.max_limit := max_limit
|} := cast Set_deposits_limit_too_high payload in
Some (limit, max_limit)
else None
end)
(fun (function_parameter : Alpha_context.Tez.t × Alpha_context.Tez.t) ⇒
let '(limit, max_limit) := function_parameter in
Build_extensible "Set_deposits_limit_too_high"
Set_deposits_limit_too_high
{| Set_deposits_limit_too_high.limit := limit;
Set_deposits_limit_too_high.max_limit := max_limit; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"contract.empty_transaction" "Empty transaction"
"Forbidden to credit 0\234\156\169 to a contract without code."
(Some
(fun (ppf : Format.formatter) ⇒
fun (contract : Alpha_context.Contract.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Transactions of 0\234\156\169 towards a contract without code are forbidden ("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))
"Transactions of 0\234\156\169 towards a contract without code are forbidden (%a).")
Alpha_context.Contract.pp contract))
(Data_encoding.obj1
(Data_encoding.req None None "contract" Alpha_context.Contract.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Empty_transaction" then
let c_value := cast Alpha_context.Contract.t payload in
Some c_value
else None
end)
(fun (c_value : Alpha_context.Contract.t) ⇒
Build_extensible "Empty_transaction" Alpha_context.Contract.t c_value)
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.tx_rollup_is_disabled" "Tx rollup is disabled"
"Cannot originate a tx rollup as it is disabled."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal"
CamlinternalFormatBasics.End_of_format)
"Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_feature_disabled" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.tx_rollup_invalid_transaction_amount"
"Transaction amount to a transaction rollup must be zero"
"Because transaction rollups are outside of the delegation mechanism of Tezos, they cannot own Tez, and therefore transactions targeting a transaction rollup must have its amount field set to zero."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Transaction amount to a transaction rollup must be zero."
CamlinternalFormatBasics.End_of_format)
"Transaction amount to a transaction rollup must be zero.")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_invalid_transaction_amount" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_invalid_transaction_amount" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.cannot_transfer_ticket_to_implicit"
"Cannot transfer ticket to implicit account"
"Cannot transfer ticket to implicit account" None Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Cannot_transfer_ticket_to_implicit" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Cannot_transfer_ticket_to_implicit" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.tx_rollup_non_internal_transaction"
"Non-internal transaction to a transaction rollup"
"Non-internal transactions to a tx rollup are forbidden."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Transaction to a transaction rollup must be internal."
CamlinternalFormatBasics.End_of_format)
"Transaction to a transaction rollup must be internal.")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_non_internal_transaction" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_non_internal_transaction" unit tt) in
let description :=
"Smart contract rollups will be enabled in a future proposal." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.sc_rollup_disabled" "Smart contract rollups are disabled"
description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_feature_disabled" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.inconsistent_counters" "Inconsistent counters in operation"
"Inconsistent counters in operation. Counters of an operation must be successive."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Inconsistent counters in operation. Counters of an operation must be successive."
CamlinternalFormatBasics.End_of_format)
"Inconsistent counters in operation. Counters of an operation must be successive.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_counters" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_counters" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.wrong_voting_period" "Wrong voting period"
"Trying to include a proposal or ballot meant for another voting period"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int32 × int32) ⇒
let '(e_value, p_value) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Wrong voting period "
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", current is "
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))))
"Wrong voting period %ld, current is %ld") p_value e_value))
(Data_encoding.obj2
(Data_encoding.req None None "current_index" Data_encoding.int32_value)
(Data_encoding.req None None "provided_index" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_voting_period" then
let '{|
Wrong_voting_period.expected := expected;
Wrong_voting_period.provided := provided
|} := cast Wrong_voting_period payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : int32 × int32) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_voting_period" Wrong_voting_period
{| Wrong_voting_period.expected := expected;
Wrong_voting_period.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"internal_operation_replay" "Internal operation replay"
"An internal operation was emitted twice by a script"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Apply_results.packed_internal_contents) ⇒
let
'Apply_results.Internal_contents {|
Apply_results.internal_contents.nonce := nonce_value |} :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Internal operation "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" was emitted twice by a script"
CamlinternalFormatBasics.End_of_format)))
"Internal operation %d was emitted twice by a script")
nonce_value)) Apply_results.internal_contents_encoding
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Internal_operation_replay" then
let op := cast Apply_results.packed_internal_contents payload in
Some op
else None
end)
(fun (op : Apply_results.packed_internal_contents) ⇒
Build_extensible "Internal_operation_replay"
Apply_results.packed_internal_contents op) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.invalid_denunciation" "Invalid denunciation"
"A denunciation is malformed"
(Some
(fun (ppf : Format.formatter) ⇒
fun (kind_value : denunciation_kind) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Malformed double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " evidence"
CamlinternalFormatBasics.End_of_format)))
"Malformed double-%a evidence") pp_denunciation_kind kind_value))
(Data_encoding.obj1
(Data_encoding.req None None "kind" denunciation_kind_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_denunciation" then
let kind_value := cast denunciation_kind payload in
Some kind_value
else None
end)
(fun (kind_value : denunciation_kind) ⇒
Build_extensible "Invalid_denunciation" denunciation_kind kind_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.inconsistent_denunciation" "Inconsistent denunciation"
"A denunciation operation is inconsistent (two distinct delegates)"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(kind_value, delegate1, delegate2) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Inconsistent double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" evidence (distinct delegate: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"Inconsistent double-%a evidence (distinct delegate: %a and %a)")
pp_denunciation_kind kind_value
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
delegate1
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
delegate2))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "delegate1"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "delegate2"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_denunciation" then
let '{|
Inconsistent_denunciation.kind := kind_value;
Inconsistent_denunciation.delegate1 := delegate1;
Inconsistent_denunciation.delegate2 := delegate2
|} := cast Inconsistent_denunciation payload in
Some (kind_value, delegate1, delegate2)
else None
end)
(fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(kind_value, delegate1, delegate2) := function_parameter in
Build_extensible "Inconsistent_denunciation" Inconsistent_denunciation
{| Inconsistent_denunciation.kind := kind_value;
Inconsistent_denunciation.delegate1 := delegate1;
Inconsistent_denunciation.delegate2 := delegate2; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"block.unrequired_denunciation" "Unrequired denunciation"
"A denunciation is unrequired"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"A valid denunciation cannot be applied: the associated delegate has already been denounced for this level."
CamlinternalFormatBasics.End_of_format)
"A valid denunciation cannot be applied: the associated delegate has already been denounced for this level.")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unrequired_denunciation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unrequired_denunciation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"block.too_early_denunciation" "Too early denunciation"
"A denunciation is too far in the future"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, level, current) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" denunciation is too far in the future (current level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", given level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"A double-%a denunciation is too far in the future (current level: %a, given level: %a)")
pp_denunciation_kind kind_value Alpha_context.Raw_level.pp current
Alpha_context.Raw_level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "current" Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_early_denunciation" then
let '{|
Too_early_denunciation.kind := kind_value;
Too_early_denunciation.level := level;
Too_early_denunciation.current := current
|} := cast Too_early_denunciation payload in
Some (kind_value, level, current)
else None
end)
(fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, level, current) := function_parameter in
Build_extensible "Too_early_denunciation" Too_early_denunciation
{| Too_early_denunciation.kind := kind_value;
Too_early_denunciation.level := level;
Too_early_denunciation.current := current; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.outdated_denunciation" "Outdated denunciation"
"A denunciation is outdated."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Cycle.t) ⇒
let '(kind_value, level, last_cycle) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is outdated (last acceptable cycle: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", given level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"A double-%a is outdated (last acceptable cycle: %a, given level: %a)")
pp_denunciation_kind kind_value Alpha_context.Cycle.pp last_cycle
Alpha_context.Raw_level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "last" Alpha_context.Cycle.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Outdated_denunciation" then
let '{|
Outdated_denunciation.kind := kind_value;
Outdated_denunciation.level := level;
Outdated_denunciation.last_cycle := last_cycle
|} := cast Outdated_denunciation payload in
Some (kind_value, level, last_cycle)
else None
end)
(fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t × Alpha_context.Cycle.t)
⇒
let '(kind_value, level, last_cycle) := function_parameter in
Build_extensible "Outdated_denunciation" Outdated_denunciation
{| Outdated_denunciation.kind := kind_value;
Outdated_denunciation.level := level;
Outdated_denunciation.last_cycle := last_cycle; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.invalid_activation" "Invalid activation"
"The given key and secret do not correspond to any existing preallocated contract"
(Some
(fun (ppf : Format.formatter) ⇒
fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid activation. The public key "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" does not match any commitment."
CamlinternalFormatBasics.End_of_format)))
"Invalid activation. The public key %a does not match any commitment.")
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh))
(Data_encoding.obj1
(Data_encoding.req None None "pkh"
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_activation" then
let '{| Invalid_activation.pkh := pkh |} :=
cast Invalid_activation payload in
Some pkh
else None
end)
(fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) ⇒
Build_extensible "Invalid_activation" Invalid_activation
{| Invalid_activation.pkh := pkh; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.multiple_revelation"
"Multiple revelations were included in a manager operation"
"A manager operation should not contain more than one revelation"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Multiple revelations were included in a manager operation"
CamlinternalFormatBasics.End_of_format)
"Multiple revelations were included in a manager operation")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Multiple_revelation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Multiple_revelation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"gas_exhausted.init_deserialize"
"Not enough gas for initial deserialization of script expressions"
"Gas limit was not high enough to deserialize the transaction parameters or origination script code or initial storage, making the operation impossible to parse within the provided gas bounds."
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Gas_quota_exceeded_init_deserialize" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.inconsistent_sources" "Inconsistent sources in operation pack"
"The operation pack includes operations from different sources."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string ppf
"The operation pack includes operations from different sources."))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_sources" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_sources" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.failing_noop"
"Failing_noop operations are not executed by the protocol"
"The failing_noop operation is an operation that is not and never will be executed by the protocol."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The failing_noop operation cannot be executed by the protocol"
CamlinternalFormatBasics.End_of_format)
"The failing_noop operation cannot be executed by the protocol")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failing_noop_error" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Failing_noop_error" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent
"delegate.zero_frozen_deposits" "Zero frozen deposits"
"The delegate has zero frozen deposits."
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has zero frozen deposits; it is not allowed to bake/preendorse/endorse."
CamlinternalFormatBasics.End_of_format)))
"Delegate %a has zero frozen deposits; it is not allowed to bake/preendorse/endorse.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zero_frozen_deposits" then
let delegate := cast Signature.public_key_hash payload in
Some delegate
else None
end)
(fun (delegate : Signature.public_key_hash) ⇒
Build_extensible "Zero_frozen_deposits" Signature.public_key_hash delegate).
Definition assert_tx_rollup_feature_enabled (ctxt : Alpha_context.context)
: M? unit :=
let level := (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level)
in
let? sunset :=
Alpha_context.Raw_level.of_int32
(Alpha_context.Constants.tx_rollup_sunset_level ctxt) in
let? '_ :=
Error_monad.fail_when (Alpha_context.Raw_level.op_lteq sunset level)
(Build_extensible "Tx_rollup_feature_disabled" unit tt) in
Error_monad.fail_unless (Alpha_context.Constants.tx_rollup_enable ctxt)
(Build_extensible "Tx_rollup_feature_disabled" unit tt).
Definition assert_sc_rollup_feature_enabled (ctxt : Alpha_context.context)
: M? unit :=
Error_monad.fail_unless (Alpha_context.Constants.sc_rollup_enable ctxt)
(Build_extensible "Sc_rollup_feature_disabled" unit tt).
Definition update_script_storage_and_ticket_balances
(ctxt : Alpha_context.context) (self : Alpha_context.Contract.contract)
(storage_value : Alpha_context.Script.expr)
(lazy_storage_diff : option Alpha_context.Lazy_storage.diffs)
(ticket_diffs : Ticket_token_map.t Z.t)
(operations : list Script_typed_ir.packed_internal_operation)
: M? (Z.t × Alpha_context.t) :=
let? ctxt :=
Alpha_context.Contract.update_script_storage ctxt self storage_value
lazy_storage_diff in
Ticket_accounting.update_ticket_balances ctxt self ticket_diffs operations.
Definition apply_delegation {A : Set}
(ctxt : Alpha_context.context) (source : Alpha_context.Contract.t)
(delegate : option Alpha_context.public_key_hash)
(before_operation : Alpha_context.context)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list A) :=
let? ctxt := Alpha_context.Delegate.set ctxt source delegate in
return?
(ctxt,
(Apply_results.Delegation_result
{|
Apply_results.successful_manager_operation_result.Delegation_result.consumed_gas
:= Alpha_context.Gas.consumed before_operation ctxt; |}), nil).
Inductive execution_arg : Set :=
| Typed_arg : ∀ {a : Set},
Alpha_context.Script.location → Script_typed_ir.ty → a → execution_arg
| Untyped_arg : Alpha_context.Script.expr → execution_arg.
Definition apply_transaction_to_implicit
(ctxt : Alpha_context.context) (contract : Alpha_context.Contract.t)
(parameter : execution_arg) (entrypoint : Alpha_context.Entrypoint.t)
(before_operation : Alpha_context.context)
(balance_updates : Alpha_context.Receipt.balance_updates)
(allocated_destination_contract : bool)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result) :=
let is_unit :=
match parameter with
| Typed_arg _ Script_typed_ir.Unit_t _ ⇒ true
| Typed_arg _ _ _ ⇒ false
| Untyped_arg parameter ⇒
match Micheline.root_value parameter with
| Micheline.Prim _ Michelson_v1_primitives.D_Unit [] _ ⇒ true
| _ ⇒ false
end
end in
let? ctxt :=
let? '_ :=
if Alpha_context.Entrypoint.is_default entrypoint then
Result.return_unit
else
Error_monad.error_value
(Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
entrypoint) in
if is_unit then
return? ctxt
else
Error_monad.error_value
(Build_extensible "Bad_contract_parameter" Alpha_context.Contract.t
contract) in
let result_value :=
Apply_results.Transaction_result
(Apply_results.Transaction_to_contract_result
{|
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
:= None;
Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:= None;
Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:= balance_updates;
Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:= nil;
Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:= Alpha_context.Gas.consumed before_operation ctxt;
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:= Z.zero;
Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:= Z.zero;
Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:= allocated_destination_contract; |}) in
return? (ctxt, result_value).
Definition apply_transaction_to_smart_contract
(ctxt : Alpha_context.context) (source : Alpha_context.Contract.t)
(contract : Alpha_context.Contract.contract) (amount : Alpha_context.Tez.t)
(entrypoint : Alpha_context.Entrypoint.t)
(before_operation : Alpha_context.context)
(payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
(mode : Script_ir_translator.unparsing_mode) (internal : bool)
(script_ir : Script_ir_translator.ex_script) (script : Alpha_context.Script.t)
(parameter : execution_arg) (cache_key : Script_cache.identifier)
(balance_updates : Alpha_context.Receipt.balance_updates)
(allocated_destination_contract : bool)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list Script_typed_ir.packed_internal_operation) :=
let? balance := Alpha_context.Contract.get_balance ctxt contract in
let now := Alpha_context.Script_timestamp.now ctxt in
let level :=
Alpha_context.Script_int.abs
(Alpha_context.Script_int.of_int32
(Alpha_context.Raw_level.to_int32
(Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level))) in
let step_constants :=
{| Script_typed_ir.step_constants.source := source;
Script_typed_ir.step_constants.payer :=
Alpha_context.Contract.implicit_contract payer;
Script_typed_ir.step_constants.self := contract;
Script_typed_ir.step_constants.amount := amount;
Script_typed_ir.step_constants.balance := balance;
Script_typed_ir.step_constants.chain_id := chain_id;
Script_typed_ir.step_constants.now := now;
Script_typed_ir.step_constants.level := level; |} in
let execute :=
match parameter with
| Untyped_arg parameter ⇒
fun x_1 x_2 x_3 x_4 x_5 x_6 x_7 ⇒
Script_interpreter.execute x_1 x_2 x_3 x_4 x_5 x_6 x_7 parameter
| Typed_arg location parameter_ty parameter ⇒
fun x_1 x_2 x_3 x_4 x_5 x_6 x_7 ⇒
Script_interpreter.execute_with_typed_parameter x_1 x_2 x_3 x_4 x_5 x_6
x_7 parameter_ty location parameter
end in
let cached_script := Some script_ir in
let?
'({|
Script_interpreter.execution_result.script := updated_cached_script;
Script_interpreter.execution_result.code_size := updated_size;
Script_interpreter.execution_result.storage := storage_value;
Script_interpreter.execution_result.lazy_storage_diff :=
lazy_storage_diff;
Script_interpreter.execution_result.operations := operations;
Script_interpreter.execution_result.ticket_diffs := ticket_diffs
|}, ctxt) :=
execute None ctxt cached_script mode step_constants script entrypoint
internal in
let? '(ticket_table_size_diff, ctxt) :=
update_script_storage_and_ticket_balances ctxt contract storage_value
lazy_storage_diff ticket_diffs operations in
let? '(ticket_paid_storage_diff, ctxt) :=
Alpha_context.Ticket_balance.adjust_storage_space ctxt
ticket_table_size_diff in
let? '(ctxt, new_size, contract_paid_storage_size_diff) :=
Alpha_context.Fees.record_paid_storage_space ctxt contract in
let? originated_contracts :=
Alpha_context.Contract.originated_from_current_nonce before_operation ctxt
in
let? ctxt :=
Script_cache.update ctxt cache_key
((Alpha_context.Script.t.with_storage
(Alpha_context.Script.lazy_expr_value storage_value) script),
updated_cached_script) updated_size in
let result_value :=
Apply_results.Transaction_result
(Apply_results.Transaction_to_contract_result
{|
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
:= Some storage_value;
Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:= lazy_storage_diff;
Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:= balance_updates;
Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:= originated_contracts;
Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:= Alpha_context.Gas.consumed before_operation ctxt;
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:= new_size;
Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:= contract_paid_storage_size_diff +Z ticket_paid_storage_diff;
Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:= allocated_destination_contract; |}) in
return? (ctxt, result_value, operations).
Definition apply_transaction
(ctxt : Alpha_context.context) (parameter : execution_arg)
(source : Alpha_context.Contract.t)
(contract : Alpha_context.Contract.contract) (amount : Alpha_context.Tez.t)
(entrypoint : Alpha_context.Entrypoint.t)
(before_operation : Alpha_context.context)
(payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
(mode : Script_ir_translator.unparsing_mode) (internal : bool)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list Script_typed_ir.packed_internal_operation) :=
let? allocated_destination_contract :=
match Alpha_context.Contract.is_implicit contract with
| None ⇒
let? '_ :=
if Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero then
Alpha_context.Contract.must_exist ctxt contract
else
Error_monad.return_unit in
Error_monad.return_false
| Some _ ⇒
let? '_ :=
Error_monad.error_when
(Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
(Build_extensible "Empty_transaction" Alpha_context.Contract.contract
contract) in
Error_monad.op_gtpipeeqquestion
(Alpha_context.Contract.allocated ctxt contract) Pervasives.not
end in
let? '(ctxt, balance_updates) :=
Alpha_context.Token.transfer None ctxt
(Alpha_context.Token.Source_container
(Alpha_context.Token.Contract source))
(Alpha_context.Token.Sink_container
(Alpha_context.Token.Contract contract)) amount in
let? '(ctxt, cache_key, script) := Script_cache.find ctxt contract in
match script with
| None ⇒
let? '(ctxt, result_value) :=
apply_transaction_to_implicit ctxt contract parameter entrypoint
before_operation balance_updates allocated_destination_contract in
return? (ctxt, result_value, nil)
| Some (script, script_ir) ⇒
apply_transaction_to_smart_contract ctxt source contract amount entrypoint
before_operation payer chain_id mode internal script_ir script parameter
cache_key balance_updates allocated_destination_contract
end.
Definition ex_ticket_size
(ctxt : Alpha_context.context) (function_parameter : Ticket_scanner.ex_ticket)
: M? (Alpha_context.context × int) :=
let 'Ticket_scanner.Ex_ticket ty ticket := function_parameter in
let? ty := Script_typed_ir.ticket_t Micheline.dummy_location ty in
let? '(ty', ctxt) :=
Script_ir_translator.unparse_ty Micheline.dummy_location ctxt ty in
let '(ty_nodes, ty_size) := Script_typed_ir_size.node_size ty' in
let ty_size := Saturation_repr.to_int ty_size in
let ty_size_cost := Script_typed_ir_size_costs.nodes_cost ty_nodes in
let? ctxt := Alpha_context.Gas.consume ctxt ty_size_cost in
let '(val_nodes, val_size) := Script_typed_ir_size.value_size ty ticket in
let val_size := Saturation_repr.to_int val_size in
let val_size_cost := Script_typed_ir_size_costs.nodes_cost val_nodes in
let? ctxt := Alpha_context.Gas.consume ctxt val_size_cost in
return? (ctxt, (ty_size +i val_size)).
Definition apply_transaction_to_tx_rollup {A B : Set}
(ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
(parameters : A) (amount : Alpha_context.Tez.t)
(entrypoint : Alpha_context.Entrypoint.t)
(payer : Alpha_context.public_key_hash)
(dst_rollup : Alpha_context.Tx_rollup.t) (since : Alpha_context.context)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list B) :=
let? '_ := assert_tx_rollup_feature_enabled ctxt in
let? '_ :=
Error_monad.fail_unless
(Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
(Build_extensible "Tx_rollup_invalid_transaction_amount" unit tt) in
if
Alpha_context.Entrypoint.op_eq entrypoint
Alpha_context.Tx_rollup.deposit_entrypoint
then
let? '{|
Tx_rollup_parameters.deposit_parameters.ex_ticket := ex_ticket;
Tx_rollup_parameters.deposit_parameters.l2_destination := l2_destination
|} :=
Tx_rollup_parameters.get_deposit_parameters parameters_ty parameters in
let? '(ctxt, ticket_size) := ex_ticket_size ctxt ex_ticket in
let limit := Alpha_context.Constants.tx_rollup_max_ticket_payload_size ctxt
in
let? '_ :=
Error_monad.fail_when (ticket_size >i limit)
(Build_extensible "Ticket_payload_size_limit_exceeded"
Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded
{|
Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded.payload_size
:= ticket_size;
Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded.limit :=
limit; |}) in
let '(ex_token, ticket_amount) :=
Ticket_token.token_and_amount_of_ex_ticket ex_ticket in
let? '(ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Tx_rollup dst_rollup) ex_token in
let? ticket_amount :=
Option.value_e
(Option.bind (Alpha_context.Script_int.to_int64 ticket_amount)
Tx_rollup_l2_qty.of_int64)
(Error_monad.trace_of_error
(Build_extensible "Tx_rollup_invalid_transaction_amount" unit tt)) in
let '(deposit, message_size) :=
Alpha_context.Tx_rollup_message.make_deposit payer l2_destination
ticket_hash ticket_amount in
let? '(ctxt, state_value) :=
Alpha_context.Tx_rollup_state.get ctxt dst_rollup in
let? cost :=
Alpha_context.Tx_rollup_state.burn_cost None state_value message_size in
let? '(ctxt, balance_updates) :=
Alpha_context.Token.transfer None ctxt
(Alpha_context.Token.Source_container
(Alpha_context.Token.Contract
(Alpha_context.Contract.implicit_contract payer)))
(Alpha_context.Token.Sink_infinite Alpha_context.Token.Burned) cost in
let? '(ctxt, state_value, paid_storage_size_diff) :=
Alpha_context.Tx_rollup_inbox.append_message ctxt dst_rollup state_value
deposit in
let? ctxt :=
Alpha_context.Tx_rollup_state.update ctxt dst_rollup state_value in
let result_value :=
Apply_results.Transaction_result
(Apply_results.Transaction_to_tx_rollup_result
{|
Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
:= ticket_hash;
Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
:= balance_updates;
Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
:= Alpha_context.Gas.consumed since ctxt;
Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
:= paid_storage_size_diff; |}) in
return? (ctxt, result_value, nil)
else
Error_monad.fail
(Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
entrypoint).
Definition apply_origination {A B : Set}
(ctxt : Alpha_context.context) (storage_type : Script_typed_ir.ty)
(storage_value : A)
(unparsed_code : Micheline.canonical Alpha_context.Script.prim)
(contract : Alpha_context.Contract.t)
(delegate : option Signature.public_key_hash)
(source : Alpha_context.Contract.t) (credit : Alpha_context.Tez.t)
(before_operation : Alpha_context.context)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list B) :=
let? '(to_duplicate, ctxt) :=
Script_ir_translator.collect_lazy_storage ctxt storage_type storage_value in
let to_update := Script_ir_translator.no_lazy_storage_id in
let? '(storage_value, lazy_storage_diff, ctxt) :=
Script_ir_translator.extract_lazy_storage_diff ctxt
Script_ir_translator.Optimized false to_duplicate to_update storage_type
storage_value in
let? '(storage_value, ctxt) :=
Script_ir_translator.unparse_data ctxt Script_ir_translator.Optimized
storage_type storage_value in
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Alpha_context.Script.strip_locations_cost storage_value) in
let storage_value :=
Alpha_context.Script.lazy_expr_value
(Micheline.strip_locations storage_value) in
let? '(code, ctxt) :=
Script_ir_translator.unparse_code ctxt Script_ir_translator.Optimized
(Micheline.root_value unparsed_code) in
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Alpha_context.Script.strip_locations_cost code) in
let code :=
Alpha_context.Script.lazy_expr_value (Micheline.strip_locations code) in
let script :=
{| Alpha_context.Script.t.code := code;
Alpha_context.Script.t.storage := storage_value; |} in
let? ctxt :=
Alpha_context.Contract.raw_originate ctxt false contract
(script, lazy_storage_diff) in
let? ctxt :=
match delegate with
| None ⇒ return? ctxt
| Some delegate ⇒ Alpha_context.Delegate.init_value ctxt contract delegate
end in
let? '(ctxt, balance_updates) :=
Alpha_context.Token.transfer None ctxt
(Alpha_context.Token.Source_container
(Alpha_context.Token.Contract source))
(Alpha_context.Token.Sink_container
(Alpha_context.Token.Contract contract)) credit in
let? '(ctxt, size_value, paid_storage_size_diff) :=
Alpha_context.Fees.record_paid_storage_space ctxt contract in
let result_value :=
Apply_results.Origination_result
{|
Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff
:= lazy_storage_diff;
Apply_results.successful_manager_operation_result.Origination_result.balance_updates
:= balance_updates;
Apply_results.successful_manager_operation_result.Origination_result.originated_contracts
:= [ contract ];
Apply_results.successful_manager_operation_result.Origination_result.consumed_gas
:= Alpha_context.Gas.consumed before_operation ctxt;
Apply_results.successful_manager_operation_result.Origination_result.storage_size
:= size_value;
Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff
:= paid_storage_size_diff; |} in
return? (ctxt, result_value, nil).
Definition prepare_apply_manager_operation_content
(ctxt : Alpha_context.context) (source : Alpha_context.Contract.contract)
(gas_consumed_in_precheck : option Alpha_context.Gas.cost)
: M?
(Alpha_context.context × Alpha_context.context ×
Alpha_context.Script.consume_deserialization_gas) :=
let before_operation := ctxt in
let? '_ := Alpha_context.Contract.must_exist ctxt source in
let? ctxt :=
Alpha_context.Gas.consume ctxt Michelson_v1_gas.Cost_of.manager_operation in
let? ctxt :=
match gas_consumed_in_precheck with
| None ⇒ Pervasives.Ok ctxt
| Some gas ⇒ Alpha_context.Gas.consume ctxt gas
end in
let consume_deserialization_gas := Alpha_context.Script.When_needed in
return? (ctxt, before_operation, consume_deserialization_gas).
Definition apply_internal_manager_operation_content
(ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
(payer : Alpha_context.public_key_hash) (source : Alpha_context.Contract.t)
(chain_id : Chain_id.t)
(gas_consumed_in_precheck : option Alpha_context.Gas.cost)
(operation : Script_typed_ir.manager_operation)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list Script_typed_ir.packed_internal_operation) :=
let? '(ctxt, before_operation, consume_deserialization_gas) :=
prepare_apply_manager_operation_content ctxt source gas_consumed_in_precheck
in
match operation with
|
Script_typed_ir.Transaction {|
Script_typed_ir.manager_operation.Transaction.transaction := {|
Alpha_context.transaction.amount := amount;
Alpha_context.transaction.parameters := _;
Alpha_context.transaction.entrypoint := entrypoint;
Alpha_context.transaction.destination :=
Alpha_context.Destination.Contract contract
|};
Script_typed_ir.manager_operation.Transaction.location := location;
Script_typed_ir.manager_operation.Transaction.parameters_ty :=
parameters_ty;
Script_typed_ir.manager_operation.Transaction.parameters :=
typed_parameters
|} ⇒
let? '(ctxt, manager_result, operations) :=
apply_transaction ctxt (Typed_arg location parameters_ty typed_parameters)
source contract amount entrypoint before_operation payer chain_id mode
true in
return? (ctxt, manager_result, operations)
|
Script_typed_ir.Transaction {|
Script_typed_ir.manager_operation.Transaction.transaction := {|
Alpha_context.transaction.amount := amount;
Alpha_context.transaction.parameters := _;
Alpha_context.transaction.entrypoint := entrypoint;
Alpha_context.transaction.destination :=
Alpha_context.Destination.Tx_rollup dst
|};
Script_typed_ir.manager_operation.Transaction.location := _;
Script_typed_ir.manager_operation.Transaction.parameters_ty :=
parameters_ty;
Script_typed_ir.manager_operation.Transaction.parameters := parameters
|} ⇒
apply_transaction_to_tx_rollup ctxt parameters_ty parameters amount
entrypoint payer dst before_operation
|
Script_typed_ir.Origination {|
Script_typed_ir.manager_operation.Origination.origination := {|
Alpha_context.origination.delegate := delegate;
Alpha_context.origination.script := script;
Alpha_context.origination.credit := credit
|};
Script_typed_ir.manager_operation.Origination.preorigination := contract;
Script_typed_ir.manager_operation.Origination.storage_type :=
storage_type;
Script_typed_ir.manager_operation.Origination.storage := storage_value
|} ⇒
let? '(unparsed_code, ctxt) :=
Alpha_context.Script.force_decode_in_context consume_deserialization_gas
ctxt script.(Alpha_context.Script.t.code) in
apply_origination ctxt storage_type storage_value unparsed_code contract
delegate source credit before_operation
| Script_typed_ir.Delegation delegate ⇒
apply_delegation ctxt source delegate before_operation
end.
Axiom apply_external_manager_operation_content :
Alpha_context.context → Script_ir_translator.unparsing_mode →
Alpha_context.public_key_hash → Chain_id.t →
option Alpha_context.Gas.cost → Alpha_context.manager_operation →
M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list Script_typed_ir.packed_internal_operation).
Inductive success_or_failure : Set :=
| Success : Alpha_context.context → success_or_failure
| Failure : success_or_failure.
#[bypass_check(guard)]
Definition apply_internal_manager_operations
(ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
(payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
(ops : list Script_typed_ir.packed_internal_operation)
: success_or_failure ×
list Apply_results.packed_internal_manager_operation_result :=
let fix apply
(ctxt : Alpha_context.context)
(applied : list Apply_results.packed_internal_manager_operation_result)
(worklist : list Script_typed_ir.packed_internal_operation) {struct ctxt}
: success_or_failure ×
list Apply_results.packed_internal_manager_operation_result :=
match worklist with
| [] ⇒ ((Success ctxt), (List.rev applied))
|
cons
(Script_typed_ir.Internal_operation
({|
Script_typed_ir.internal_operation.source := source;
Script_typed_ir.internal_operation.operation := operation;
Script_typed_ir.internal_operation.nonce := nonce_value
|} as op)) rest ⇒
let op_res := Apply_results.contents_of_internal_operation op in
let function_parameter :=
if Alpha_context.internal_nonce_already_recorded ctxt nonce_value then
Error_monad.fail
(Build_extensible "Internal_operation_replay"
Apply_results.packed_internal_contents
(Apply_results.Internal_contents op_res))
else
let ctxt := Alpha_context.record_internal_nonce ctxt nonce_value in
apply_internal_manager_operation_content ctxt mode payer source
chain_id None operation in
match function_parameter with
| Pervasives.Error errors ⇒
let result_value :=
Apply_results.pack_internal_manager_operation_result op
(Apply_results.Failed
(Script_typed_ir.manager_kind
op.(Script_typed_ir.internal_operation.operation)) errors) in
let skipped :=
List.rev_map
(fun (function_parameter :
Script_typed_ir.packed_internal_operation) ⇒
let 'Script_typed_ir.Internal_operation op := function_parameter
in
Apply_results.pack_internal_manager_operation_result op
(Apply_results.Skipped
(Script_typed_ir.manager_kind
op.(Script_typed_ir.internal_operation.operation)))) rest in
(Failure,
(List.rev (Pervasives.op_at skipped (cons result_value applied))))
| Pervasives.Ok (ctxt, result_value, emitted) ⇒
apply ctxt
(cons
(Apply_results.pack_internal_manager_operation_result op
(Apply_results.Applied result_value)) applied)
(Pervasives.op_at emitted rest)
end
end in
apply ctxt nil ops.
Definition precheck_manager_contents
(ctxt : Alpha_context.context) (op : Alpha_context.contents)
(only_batch : bool)
: M? (Alpha_context.context × Apply_results.precheck_result) :=
match op with
|
Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.source := source;
Alpha_context.contents.Manager_operation.fee := fee;
Alpha_context.contents.Manager_operation.counter := counter;
Alpha_context.contents.Manager_operation.operation := operation;
Alpha_context.contents.Manager_operation.gas_limit := gas_limit;
Alpha_context.contents.Manager_operation.storage_limit := storage_limit
|} ⇒
let? ctxt :=
(if only_batch then
Error_monad.record_trace (Build_extensible "Gas_limit_too_high" unit tt)
else
fun (errs : M? Alpha_context.context) ⇒ errs)
(Alpha_context.Gas.consume_limit_in_block ctxt gas_limit) in
let ctxt := Alpha_context.Gas.set_limit ctxt gas_limit in
let ctxt_before := ctxt in
let? '_ := Alpha_context.Fees.check_storage_limit ctxt storage_limit in
let source_contract := Alpha_context.Contract.implicit_contract source in
let? '_ := Alpha_context.Contract.must_be_allocated ctxt source_contract in
let? '_ :=
Alpha_context.Contract.check_counter_increment ctxt source counter in
let consume_deserialization_gas := Alpha_context.Script.Always in
let? ctxt :=
match operation with
| Alpha_context.Reveal pk ⇒
Alpha_context.Contract.reveal_manager_key ctxt source pk
|
Alpha_context.Transaction {|
Alpha_context.transaction.parameters := parameters;
Alpha_context.transaction.destination := destination
|} ⇒
let? '_ :=
Error_monad.fail_when
match destination with
| Alpha_context.Destination.Tx_rollup _ ⇒ true
| _ ⇒ false
end (Build_extensible "Tx_rollup_non_internal_transaction" unit tt)
in
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(let? '(_arg, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt parameters in
return? ctxt)
|
Alpha_context.Origination {|
Alpha_context.origination.script := script |} ⇒
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(let? '(_code, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt
script.(Alpha_context.Script.t.code) in
let? '(_storage, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt
script.(Alpha_context.Script.t.storage) in
return? ctxt)
|
Alpha_context.Register_global_constant {|
Alpha_context.manager_operation.Register_global_constant.value := value_value
|} ⇒
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(let? '(_value, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt value_value in
return? ctxt)
| (Alpha_context.Delegation _ | Alpha_context.Set_deposits_limit _) ⇒
return? ctxt
| Alpha_context.Tx_rollup_origination ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
return? ctxt
|
Alpha_context.Tx_rollup_submit_batch {|
Alpha_context.manager_operation.Tx_rollup_submit_batch.content := content
|} ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
let size_limit :=
Alpha_context.Constants.tx_rollup_hard_size_limit_per_message ctxt in
let '(_message, message_size) :=
Alpha_context.Tx_rollup_message.make_batch content in
let? cost := Tx_rollup_gas.hash_cost message_size in
let? ctxt := Alpha_context.Gas.consume ctxt cost in
let? '_ :=
Error_monad.fail_unless (message_size ≤i size_limit)
(Build_extensible "Message_size_exceeds_limit" unit tt) in
return? ctxt
|
(Alpha_context.Tx_rollup_commit _ |
Alpha_context.Tx_rollup_return_bond _ |
Alpha_context.Tx_rollup_finalize_commitment _ |
Alpha_context.Tx_rollup_remove_commitment _) ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
return? ctxt
|
Alpha_context.Transfer_ticket {|
Alpha_context.manager_operation.Transfer_ticket.contents := contents;
Alpha_context.manager_operation.Transfer_ticket.ty := ty
|} ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(let? '(_contents, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt contents in
let? '(_ty, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt ty in
return? ctxt)
|
Alpha_context.Tx_rollup_dispatch_tickets {|
Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.message_result_path
:= message_result_path;
Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.tickets_info
:= tickets_info
|} ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
let '{|
Alpha_context.Constants.parametric.tx_rollup_max_messages_per_inbox :=
tx_rollup_max_messages_per_inbox;
Alpha_context.Constants.parametric.tx_rollup_max_withdrawals_per_batch
:= tx_rollup_max_withdrawals_per_batch
|} := Alpha_context.Constants.parametric_value ctxt in
let? '_ :=
Alpha_context.Tx_rollup_errors.check_path_depth
Alpha_context.Tx_rollup_errors.Commitment
(Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
message_result_path) tx_rollup_max_messages_per_inbox in
let? '_ :=
Error_monad.error_when (Compare.List_length_with.op_eq tickets_info 0)
(Build_extensible "No_withdrawals_to_dispatch" unit tt) in
let? '_ :=
Error_monad.error_when
(Compare.List_length_with.op_gt tickets_info
tx_rollup_max_withdrawals_per_batch)
(Build_extensible "Too_many_withdrawals" unit tt) in
let? ctxt :=
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(List.fold_left_e
(fun (ctxt : Alpha_context.context) ⇒
fun (function_parameter : Alpha_context.Tx_rollup_reveal.t) ⇒
let '{|
Alpha_context.Tx_rollup_reveal.t.contents := contents;
Alpha_context.Tx_rollup_reveal.t.ty := ty
|} := function_parameter in
let? '(_contents, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt contents in
let? '(_ty, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt ty in
return? ctxt) ctxt tickets_info) in
return? ctxt
|
Alpha_context.Tx_rollup_rejection {|
Alpha_context.manager_operation.Tx_rollup_rejection.message_path :=
message_path;
Alpha_context.manager_operation.Tx_rollup_rejection.message_result_path
:= message_result_path;
Alpha_context.manager_operation.Tx_rollup_rejection.previous_message_result_path
:= previous_message_result_path
|} ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
let '{|
Alpha_context.Constants.parametric.tx_rollup_max_messages_per_inbox :=
tx_rollup_max_messages_per_inbox
|} := Alpha_context.Constants.parametric_value ctxt in
let? '_ :=
Alpha_context.Tx_rollup_errors.check_path_depth
Alpha_context.Tx_rollup_errors.Inbox
(Alpha_context.Tx_rollup_inbox.Merkle.path_depth message_path)
tx_rollup_max_messages_per_inbox in
let? '_ :=
Alpha_context.Tx_rollup_errors.check_path_depth
Alpha_context.Tx_rollup_errors.Commitment
(Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
message_result_path) tx_rollup_max_messages_per_inbox in
let? '_ :=
Alpha_context.Tx_rollup_errors.check_path_depth
Alpha_context.Tx_rollup_errors.Commitment
(Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
previous_message_result_path) tx_rollup_max_messages_per_inbox in
return? ctxt
|
(Alpha_context.Sc_rollup_originate _ |
Alpha_context.Sc_rollup_add_messages _ |
Alpha_context.Sc_rollup_cement _ | Alpha_context.Sc_rollup_publish _) ⇒
let? '_ := assert_sc_rollup_feature_enabled ctxt in
return? ctxt
end in
let? ctxt := Alpha_context.Contract.increment_counter ctxt source in
let? '(ctxt, balance_updates) :=
Alpha_context.Token.transfer None ctxt
(Alpha_context.Token.Source_container
(Alpha_context.Token.Contract source_contract))
(Alpha_context.Token.Sink_container Alpha_context.Token.Block_fees) fee
in
let consumed_gas := Alpha_context.Gas.consumed ctxt_before ctxt in
return?
(ctxt,
{| Apply_results.precheck_result.consumed_gas := consumed_gas;
Apply_results.precheck_result.balance_updates := balance_updates; |})
| _ ⇒ unreachable_gadt_branch
end.
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operations.wrong_slot" "Wrong slot" "wrong slot"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "wrong slot"
CamlinternalFormatBasics.End_of_format) "wrong slot")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_slot_used_for_consensus_operation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Wrong_slot_used_for_consensus_operation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.not_enough_endorsements" "Not enough endorsements"
"The block being validated does not include the required minimum number of endorsements."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int × int) ⇒
let '(required, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong number of endorsements ("
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal "), at least "
(CamlinternalFormatBasics.Int
CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " are expected"
CamlinternalFormatBasics.End_of_format)))))
"Wrong number of endorsements (%i), at least %i are expected")
provided required))
(Data_encoding.obj2
(Data_encoding.req None None "required" Data_encoding.int31)
(Data_encoding.req None None "provided" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Not_enough_endorsements" then
let '{|
Not_enough_endorsements.required := required;
Not_enough_endorsements.provided := provided
|} := cast Not_enough_endorsements payload in
Some (required, provided)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(required, provided) := function_parameter in
Build_extensible "Not_enough_endorsements" Not_enough_endorsements
{| Not_enough_endorsements.required := required;
Not_enough_endorsements.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.wrong_consensus_operation_branch"
"Wrong consensus operation branch"
"Trying to include an endorsement or preendorsement which points to the wrong block.\n It should be the predecessor for preendorsements and the grandfather for endorsements."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Block_hash.t × Block_hash.t) ⇒
let '(e_value, p_value) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Wrong branch "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", expected "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"Wrong branch %a, expected %a") Block_hash.pp p_value
Block_hash.pp e_value))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Block_hash.encoding)
(Data_encoding.req None None "provided" Block_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_consensus_operation_branch" then
let '(e_value, p_value) :=
cast (Block_hash.t × Block_hash.t) payload in
Some (e_value, p_value)
else None
end)
(fun (function_parameter : Block_hash.t × Block_hash.t) ⇒
let '(e_value, p_value) := function_parameter in
Build_extensible "Wrong_consensus_operation_branch"
(Block_hash.t × Block_hash.t) (e_value, p_value)) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.invalid_double_baking_evidence" "Invalid double baking evidence"
"A double-baking evidence is inconsistent (two distinct level)"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Block_hash.t × Alpha_context.Raw_level.raw_level ×
Alpha_context.Round.t × Block_hash.t ×
Alpha_context.Raw_level.raw_level × Alpha_context.Round.t) ⇒
let '(hash1, level1, round1, hash2, level2, round2) :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid double-baking evidence (hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", levels/rounds: ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
") and ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal
"," % char
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
"))"
CamlinternalFormatBasics.End_of_format)))))))))))))
"Invalid double-baking evidence (hash: %a and %a, levels/rounds: (%ld,%ld) and (%ld,%ld))")
Block_hash.pp hash1 Block_hash.pp hash2
(Alpha_context.Raw_level.to_int32 level1)
(Alpha_context.Round.to_int32 round1)
(Alpha_context.Raw_level.to_int32 level2)
(Alpha_context.Round.to_int32 round2)))
(Data_encoding.obj6
(Data_encoding.req None None "hash1" Block_hash.encoding)
(Data_encoding.req None None "level1" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "round1" Alpha_context.Round.encoding)
(Data_encoding.req None None "hash2" Block_hash.encoding)
(Data_encoding.req None None "level2" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "round2" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_double_baking_evidence" then
let '{|
Invalid_double_baking_evidence.hash1 := hash1;
Invalid_double_baking_evidence.level1 := level1;
Invalid_double_baking_evidence.round1 := round1;
Invalid_double_baking_evidence.hash2 := hash2;
Invalid_double_baking_evidence.level2 := level2;
Invalid_double_baking_evidence.round2 := round2
|} := cast Invalid_double_baking_evidence payload in
Some (hash1, level1, round1, hash2, level2, round2)
else None
end)
(fun (function_parameter :
Block_hash.t × Alpha_context.Raw_level.raw_level × Alpha_context.Round.t
× Block_hash.t × Alpha_context.Raw_level.raw_level ×
Alpha_context.Round.t) ⇒
let '(hash1, level1, round1, hash2, level2, round2) :=
function_parameter in
Build_extensible "Invalid_double_baking_evidence"
Invalid_double_baking_evidence
{| Invalid_double_baking_evidence.hash1 := hash1;
Invalid_double_baking_evidence.level1 := level1;
Invalid_double_baking_evidence.round1 := round1;
Invalid_double_baking_evidence.hash2 := hash2;
Invalid_double_baking_evidence.level2 := level2;
Invalid_double_baking_evidence.round2 := round2; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"wrong_level_for_consensus_operation"
"Wrong level for consensus operation"
"Wrong level for consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong level for consensus operation (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Wrong level for consensus operation (expected: %a, provided: %a).")
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_level_for_consensus_operation" then
let '{|
Wrong_level_for_consensus_operation.expected := expected;
Wrong_level_for_consensus_operation.provided := provided
|} := cast Wrong_level_for_consensus_operation payload in
Some (expected, provided)
else None
end)
(fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_level_for_consensus_operation"
Wrong_level_for_consensus_operation
{| Wrong_level_for_consensus_operation.expected := expected;
Wrong_level_for_consensus_operation.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"wrong_round_for_consensus_operation"
"Wrong round for consensus operation"
"Wrong round for consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong round for consensus operation (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Wrong round for consensus operation (expected: %a, provided: %a).")
Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_round_for_consensus_operation" then
let '{|
Wrong_round_for_consensus_operation.expected := expected;
Wrong_round_for_consensus_operation.provided := provided
|} := cast Wrong_round_for_consensus_operation payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_round_for_consensus_operation"
Wrong_round_for_consensus_operation
{| Wrong_round_for_consensus_operation.expected := expected;
Wrong_round_for_consensus_operation.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"preendorsement_round_too_high" "Preendorsement round too high"
"Preendorsement round too high."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(block_round, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Preendorsement round too high (block_round: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Preendorsement round too high (block_round: %a, provided: %a).")
Alpha_context.Round.pp block_round Alpha_context.Round.pp provided))
(Data_encoding.obj2
(Data_encoding.req None None "block_round" Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Preendorsement_round_too_high" then
let '{|
Preendorsement_round_too_high.block_round := block_round;
Preendorsement_round_too_high.provided := provided
|} := cast Preendorsement_round_too_high payload in
Some (block_round, provided)
else None
end)
(fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
⇒
let '(block_round, provided) := function_parameter in
Build_extensible "Preendorsement_round_too_high"
Preendorsement_round_too_high
{| Preendorsement_round_too_high.block_round := block_round;
Preendorsement_round_too_high.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"wrong_payload_hash_for_consensus_operation"
"Wrong payload hash for consensus operation"
"Wrong payload hash for consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t)
⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong payload hash for consensus operation (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Wrong payload hash for consensus operation (expected: %a, provided: %a).")
Block_payload_hash.pp_short expected Block_payload_hash.pp_short
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Block_payload_hash.encoding)
(Data_encoding.req None None "provided" Block_payload_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_payload_hash_for_consensus_operation" then
let '{|
Wrong_payload_hash_for_consensus_operation.expected := expected;
Wrong_payload_hash_for_consensus_operation.provided := provided
|} := cast Wrong_payload_hash_for_consensus_operation payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_payload_hash_for_consensus_operation"
Wrong_payload_hash_for_consensus_operation
{| Wrong_payload_hash_for_consensus_operation.expected := expected;
Wrong_payload_hash_for_consensus_operation.provided := provided; |})
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"unexpected_endorsement_in_block" "Unexpected endorsement in block"
"Unexpected endorsement in block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unexpected endorsement in block."
CamlinternalFormatBasics.End_of_format)
"Unexpected endorsement in block."))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_endorsement_in_block" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_endorsement_in_block" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"unexpected_preendorsement_in_block" "Unexpected preendorsement in block"
"Unexpected preendorsement in block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unexpected preendorsement in block."
CamlinternalFormatBasics.End_of_format)
"Unexpected preendorsement in block."))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_preendorsement_in_block" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_preendorsement_in_block" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"consensus_operation_for_future_level"
"Consensus operation for future level"
"Consensus operation for future level."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation for future level\n (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation for future level\n (expected: %a, provided: %a).")
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_future_level" then
let '{|
Consensus_operation_for_future_level.expected := expected;
Consensus_operation_for_future_level.provided := provided
|} := cast Consensus_operation_for_future_level payload in
Some (expected, provided)
else None
end)
(fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_future_level"
Consensus_operation_for_future_level
{| Consensus_operation_for_future_level.expected := expected;
Consensus_operation_for_future_level.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"consensus_operation_for_future_round"
"Consensus operation for future round"
"Consensus operation for future round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation for future round (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation for future round (expected: %a, provided: %a).")
Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected_max" Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_future_round" then
let '{|
Consensus_operation_for_future_round.expected := expected;
Consensus_operation_for_future_round.provided := provided
|} := cast Consensus_operation_for_future_round payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_future_round"
Consensus_operation_for_future_round
{| Consensus_operation_for_future_round.expected := expected;
Consensus_operation_for_future_round.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Outdated
"consensus_operation_for_old_level" "Consensus operation for old level"
"Consensus operation for old level."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation for old level (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation for old level (expected: %a, provided: %a).")
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_old_level" then
let '{|
Consensus_operation_for_old_level.expected := expected;
Consensus_operation_for_old_level.provided := provided
|} := cast Consensus_operation_for_old_level payload in
Some (expected, provided)
else None
end)
(fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_old_level"
Consensus_operation_for_old_level
{| Consensus_operation_for_old_level.expected := expected;
Consensus_operation_for_old_level.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"consensus_operation_for_old_round" "Consensus operation for old round"
"Consensus operation for old round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation for old round (expected_min: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation for old round (expected_min: %a, provided: %a).")
Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected_min" Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_old_round" then
let '{|
Consensus_operation_for_old_round.expected := expected;
Consensus_operation_for_old_round.provided := provided
|} := cast Consensus_operation_for_old_round payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_old_round"
Consensus_operation_for_old_round
{| Consensus_operation_for_old_round.expected := expected;
Consensus_operation_for_old_round.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"consensus_operation_on_competing_proposal"
"Consensus operation on competing proposal"
"Consensus operation on competing proposal."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t)
⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Consensus operation on competing proposal (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Consensus operation on competing proposal (expected: %a, provided: %a).")
Block_payload_hash.pp_short expected Block_payload_hash.pp_short
provided))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Block_payload_hash.encoding)
(Data_encoding.req None None "provided" Block_payload_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_on_competing_proposal" then
let '{|
Consensus_operation_on_competing_proposal.expected := expected;
Consensus_operation_on_competing_proposal.provided := provided
|} := cast Consensus_operation_on_competing_proposal payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Consensus_operation_on_competing_proposal"
Consensus_operation_on_competing_proposal
{| Consensus_operation_on_competing_proposal.expected := expected;
Consensus_operation_on_competing_proposal.provided := provided; |})
in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.set_deposits_limit_on_unregistered_delegate"
"Set deposits limit on an unregistered delegate"
"Cannot set deposits limit on an unregistered delegate."
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot set a deposits limit on the unregistered delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Cannot set a deposits limit on the unregistered delegate %a.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) c_value))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Set_deposits_limit_on_unregistered_delegate" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Set_deposits_limit_on_unregistered_delegate"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.set_deposits_limit_too_high"
"Set deposits limit to a too high value"
"Cannot set deposits limit such that the active stake overflows."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Alpha_context.Tez.t × Alpha_context.Tez.t)
⇒
let '(limit, max_limit) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot set deposits limit to "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" as it is higher the allowed maximum "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Cannot set deposits limit to %a as it is higher the allowed maximum %a.")
Alpha_context.Tez.pp limit Alpha_context.Tez.pp max_limit))
(Data_encoding.obj2
(Data_encoding.req None None "limit" Alpha_context.Tez.encoding)
(Data_encoding.req None None "max_limit" Alpha_context.Tez.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Set_deposits_limit_too_high" then
let '{|
Set_deposits_limit_too_high.limit := limit;
Set_deposits_limit_too_high.max_limit := max_limit
|} := cast Set_deposits_limit_too_high payload in
Some (limit, max_limit)
else None
end)
(fun (function_parameter : Alpha_context.Tez.t × Alpha_context.Tez.t) ⇒
let '(limit, max_limit) := function_parameter in
Build_extensible "Set_deposits_limit_too_high"
Set_deposits_limit_too_high
{| Set_deposits_limit_too_high.limit := limit;
Set_deposits_limit_too_high.max_limit := max_limit; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"contract.empty_transaction" "Empty transaction"
"Forbidden to credit 0\234\156\169 to a contract without code."
(Some
(fun (ppf : Format.formatter) ⇒
fun (contract : Alpha_context.Contract.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Transactions of 0\234\156\169 towards a contract without code are forbidden ("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))
"Transactions of 0\234\156\169 towards a contract without code are forbidden (%a).")
Alpha_context.Contract.pp contract))
(Data_encoding.obj1
(Data_encoding.req None None "contract" Alpha_context.Contract.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Empty_transaction" then
let c_value := cast Alpha_context.Contract.t payload in
Some c_value
else None
end)
(fun (c_value : Alpha_context.Contract.t) ⇒
Build_extensible "Empty_transaction" Alpha_context.Contract.t c_value)
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.tx_rollup_is_disabled" "Tx rollup is disabled"
"Cannot originate a tx rollup as it is disabled."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal"
CamlinternalFormatBasics.End_of_format)
"Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_feature_disabled" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.tx_rollup_invalid_transaction_amount"
"Transaction amount to a transaction rollup must be zero"
"Because transaction rollups are outside of the delegation mechanism of Tezos, they cannot own Tez, and therefore transactions targeting a transaction rollup must have its amount field set to zero."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Transaction amount to a transaction rollup must be zero."
CamlinternalFormatBasics.End_of_format)
"Transaction amount to a transaction rollup must be zero.")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_invalid_transaction_amount" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_invalid_transaction_amount" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.cannot_transfer_ticket_to_implicit"
"Cannot transfer ticket to implicit account"
"Cannot transfer ticket to implicit account" None Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Cannot_transfer_ticket_to_implicit" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Cannot_transfer_ticket_to_implicit" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.tx_rollup_non_internal_transaction"
"Non-internal transaction to a transaction rollup"
"Non-internal transactions to a tx rollup are forbidden."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Transaction to a transaction rollup must be internal."
CamlinternalFormatBasics.End_of_format)
"Transaction to a transaction rollup must be internal.")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_non_internal_transaction" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_non_internal_transaction" unit tt) in
let description :=
"Smart contract rollups will be enabled in a future proposal." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.sc_rollup_disabled" "Smart contract rollups are disabled"
description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_feature_disabled" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.inconsistent_counters" "Inconsistent counters in operation"
"Inconsistent counters in operation. Counters of an operation must be successive."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Inconsistent counters in operation. Counters of an operation must be successive."
CamlinternalFormatBasics.End_of_format)
"Inconsistent counters in operation. Counters of an operation must be successive.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_counters" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_counters" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.wrong_voting_period" "Wrong voting period"
"Trying to include a proposal or ballot meant for another voting period"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int32 × int32) ⇒
let '(e_value, p_value) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Wrong voting period "
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", current is "
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))))
"Wrong voting period %ld, current is %ld") p_value e_value))
(Data_encoding.obj2
(Data_encoding.req None None "current_index" Data_encoding.int32_value)
(Data_encoding.req None None "provided_index" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_voting_period" then
let '{|
Wrong_voting_period.expected := expected;
Wrong_voting_period.provided := provided
|} := cast Wrong_voting_period payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : int32 × int32) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_voting_period" Wrong_voting_period
{| Wrong_voting_period.expected := expected;
Wrong_voting_period.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"internal_operation_replay" "Internal operation replay"
"An internal operation was emitted twice by a script"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Apply_results.packed_internal_contents) ⇒
let
'Apply_results.Internal_contents {|
Apply_results.internal_contents.nonce := nonce_value |} :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Internal operation "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" was emitted twice by a script"
CamlinternalFormatBasics.End_of_format)))
"Internal operation %d was emitted twice by a script")
nonce_value)) Apply_results.internal_contents_encoding
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Internal_operation_replay" then
let op := cast Apply_results.packed_internal_contents payload in
Some op
else None
end)
(fun (op : Apply_results.packed_internal_contents) ⇒
Build_extensible "Internal_operation_replay"
Apply_results.packed_internal_contents op) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.invalid_denunciation" "Invalid denunciation"
"A denunciation is malformed"
(Some
(fun (ppf : Format.formatter) ⇒
fun (kind_value : denunciation_kind) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Malformed double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " evidence"
CamlinternalFormatBasics.End_of_format)))
"Malformed double-%a evidence") pp_denunciation_kind kind_value))
(Data_encoding.obj1
(Data_encoding.req None None "kind" denunciation_kind_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_denunciation" then
let kind_value := cast denunciation_kind payload in
Some kind_value
else None
end)
(fun (kind_value : denunciation_kind) ⇒
Build_extensible "Invalid_denunciation" denunciation_kind kind_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.inconsistent_denunciation" "Inconsistent denunciation"
"A denunciation operation is inconsistent (two distinct delegates)"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(kind_value, delegate1, delegate2) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Inconsistent double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" evidence (distinct delegate: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"Inconsistent double-%a evidence (distinct delegate: %a and %a)")
pp_denunciation_kind kind_value
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
delegate1
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
delegate2))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "delegate1"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "delegate2"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_denunciation" then
let '{|
Inconsistent_denunciation.kind := kind_value;
Inconsistent_denunciation.delegate1 := delegate1;
Inconsistent_denunciation.delegate2 := delegate2
|} := cast Inconsistent_denunciation payload in
Some (kind_value, delegate1, delegate2)
else None
end)
(fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(kind_value, delegate1, delegate2) := function_parameter in
Build_extensible "Inconsistent_denunciation" Inconsistent_denunciation
{| Inconsistent_denunciation.kind := kind_value;
Inconsistent_denunciation.delegate1 := delegate1;
Inconsistent_denunciation.delegate2 := delegate2; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"block.unrequired_denunciation" "Unrequired denunciation"
"A denunciation is unrequired"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"A valid denunciation cannot be applied: the associated delegate has already been denounced for this level."
CamlinternalFormatBasics.End_of_format)
"A valid denunciation cannot be applied: the associated delegate has already been denounced for this level.")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unrequired_denunciation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unrequired_denunciation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"block.too_early_denunciation" "Too early denunciation"
"A denunciation is too far in the future"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, level, current) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" denunciation is too far in the future (current level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", given level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"A double-%a denunciation is too far in the future (current level: %a, given level: %a)")
pp_denunciation_kind kind_value Alpha_context.Raw_level.pp current
Alpha_context.Raw_level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "current" Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_early_denunciation" then
let '{|
Too_early_denunciation.kind := kind_value;
Too_early_denunciation.level := level;
Too_early_denunciation.current := current
|} := cast Too_early_denunciation payload in
Some (kind_value, level, current)
else None
end)
(fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, level, current) := function_parameter in
Build_extensible "Too_early_denunciation" Too_early_denunciation
{| Too_early_denunciation.kind := kind_value;
Too_early_denunciation.level := level;
Too_early_denunciation.current := current; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.outdated_denunciation" "Outdated denunciation"
"A denunciation is outdated."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Cycle.t) ⇒
let '(kind_value, level, last_cycle) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is outdated (last acceptable cycle: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", given level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"A double-%a is outdated (last acceptable cycle: %a, given level: %a)")
pp_denunciation_kind kind_value Alpha_context.Cycle.pp last_cycle
Alpha_context.Raw_level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "last" Alpha_context.Cycle.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Outdated_denunciation" then
let '{|
Outdated_denunciation.kind := kind_value;
Outdated_denunciation.level := level;
Outdated_denunciation.last_cycle := last_cycle
|} := cast Outdated_denunciation payload in
Some (kind_value, level, last_cycle)
else None
end)
(fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t × Alpha_context.Cycle.t)
⇒
let '(kind_value, level, last_cycle) := function_parameter in
Build_extensible "Outdated_denunciation" Outdated_denunciation
{| Outdated_denunciation.kind := kind_value;
Outdated_denunciation.level := level;
Outdated_denunciation.last_cycle := last_cycle; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.invalid_activation" "Invalid activation"
"The given key and secret do not correspond to any existing preallocated contract"
(Some
(fun (ppf : Format.formatter) ⇒
fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid activation. The public key "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" does not match any commitment."
CamlinternalFormatBasics.End_of_format)))
"Invalid activation. The public key %a does not match any commitment.")
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh))
(Data_encoding.obj1
(Data_encoding.req None None "pkh"
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_activation" then
let '{| Invalid_activation.pkh := pkh |} :=
cast Invalid_activation payload in
Some pkh
else None
end)
(fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) ⇒
Build_extensible "Invalid_activation" Invalid_activation
{| Invalid_activation.pkh := pkh; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"block.multiple_revelation"
"Multiple revelations were included in a manager operation"
"A manager operation should not contain more than one revelation"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Multiple revelations were included in a manager operation"
CamlinternalFormatBasics.End_of_format)
"Multiple revelations were included in a manager operation")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Multiple_revelation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Multiple_revelation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"gas_exhausted.init_deserialize"
"Not enough gas for initial deserialization of script expressions"
"Gas limit was not high enough to deserialize the transaction parameters or origination script code or initial storage, making the operation impossible to parse within the provided gas bounds."
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Gas_quota_exceeded_init_deserialize" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.inconsistent_sources" "Inconsistent sources in operation pack"
"The operation pack includes operations from different sources."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string ppf
"The operation pack includes operations from different sources."))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_sources" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_sources" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.failing_noop"
"Failing_noop operations are not executed by the protocol"
"The failing_noop operation is an operation that is not and never will be executed by the protocol."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The failing_noop operation cannot be executed by the protocol"
CamlinternalFormatBasics.End_of_format)
"The failing_noop operation cannot be executed by the protocol")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failing_noop_error" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Failing_noop_error" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent
"delegate.zero_frozen_deposits" "Zero frozen deposits"
"The delegate has zero frozen deposits."
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has zero frozen deposits; it is not allowed to bake/preendorse/endorse."
CamlinternalFormatBasics.End_of_format)))
"Delegate %a has zero frozen deposits; it is not allowed to bake/preendorse/endorse.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zero_frozen_deposits" then
let delegate := cast Signature.public_key_hash payload in
Some delegate
else None
end)
(fun (delegate : Signature.public_key_hash) ⇒
Build_extensible "Zero_frozen_deposits" Signature.public_key_hash delegate).
Definition assert_tx_rollup_feature_enabled (ctxt : Alpha_context.context)
: M? unit :=
let level := (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level)
in
let? sunset :=
Alpha_context.Raw_level.of_int32
(Alpha_context.Constants.tx_rollup_sunset_level ctxt) in
let? '_ :=
Error_monad.fail_when (Alpha_context.Raw_level.op_lteq sunset level)
(Build_extensible "Tx_rollup_feature_disabled" unit tt) in
Error_monad.fail_unless (Alpha_context.Constants.tx_rollup_enable ctxt)
(Build_extensible "Tx_rollup_feature_disabled" unit tt).
Definition assert_sc_rollup_feature_enabled (ctxt : Alpha_context.context)
: M? unit :=
Error_monad.fail_unless (Alpha_context.Constants.sc_rollup_enable ctxt)
(Build_extensible "Sc_rollup_feature_disabled" unit tt).
Definition update_script_storage_and_ticket_balances
(ctxt : Alpha_context.context) (self : Alpha_context.Contract.contract)
(storage_value : Alpha_context.Script.expr)
(lazy_storage_diff : option Alpha_context.Lazy_storage.diffs)
(ticket_diffs : Ticket_token_map.t Z.t)
(operations : list Script_typed_ir.packed_internal_operation)
: M? (Z.t × Alpha_context.t) :=
let? ctxt :=
Alpha_context.Contract.update_script_storage ctxt self storage_value
lazy_storage_diff in
Ticket_accounting.update_ticket_balances ctxt self ticket_diffs operations.
Definition apply_delegation {A : Set}
(ctxt : Alpha_context.context) (source : Alpha_context.Contract.t)
(delegate : option Alpha_context.public_key_hash)
(before_operation : Alpha_context.context)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list A) :=
let? ctxt := Alpha_context.Delegate.set ctxt source delegate in
return?
(ctxt,
(Apply_results.Delegation_result
{|
Apply_results.successful_manager_operation_result.Delegation_result.consumed_gas
:= Alpha_context.Gas.consumed before_operation ctxt; |}), nil).
Inductive execution_arg : Set :=
| Typed_arg : ∀ {a : Set},
Alpha_context.Script.location → Script_typed_ir.ty → a → execution_arg
| Untyped_arg : Alpha_context.Script.expr → execution_arg.
Definition apply_transaction_to_implicit
(ctxt : Alpha_context.context) (contract : Alpha_context.Contract.t)
(parameter : execution_arg) (entrypoint : Alpha_context.Entrypoint.t)
(before_operation : Alpha_context.context)
(balance_updates : Alpha_context.Receipt.balance_updates)
(allocated_destination_contract : bool)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result) :=
let is_unit :=
match parameter with
| Typed_arg _ Script_typed_ir.Unit_t _ ⇒ true
| Typed_arg _ _ _ ⇒ false
| Untyped_arg parameter ⇒
match Micheline.root_value parameter with
| Micheline.Prim _ Michelson_v1_primitives.D_Unit [] _ ⇒ true
| _ ⇒ false
end
end in
let? ctxt :=
let? '_ :=
if Alpha_context.Entrypoint.is_default entrypoint then
Result.return_unit
else
Error_monad.error_value
(Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
entrypoint) in
if is_unit then
return? ctxt
else
Error_monad.error_value
(Build_extensible "Bad_contract_parameter" Alpha_context.Contract.t
contract) in
let result_value :=
Apply_results.Transaction_result
(Apply_results.Transaction_to_contract_result
{|
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
:= None;
Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:= None;
Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:= balance_updates;
Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:= nil;
Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:= Alpha_context.Gas.consumed before_operation ctxt;
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:= Z.zero;
Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:= Z.zero;
Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:= allocated_destination_contract; |}) in
return? (ctxt, result_value).
Definition apply_transaction_to_smart_contract
(ctxt : Alpha_context.context) (source : Alpha_context.Contract.t)
(contract : Alpha_context.Contract.contract) (amount : Alpha_context.Tez.t)
(entrypoint : Alpha_context.Entrypoint.t)
(before_operation : Alpha_context.context)
(payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
(mode : Script_ir_translator.unparsing_mode) (internal : bool)
(script_ir : Script_ir_translator.ex_script) (script : Alpha_context.Script.t)
(parameter : execution_arg) (cache_key : Script_cache.identifier)
(balance_updates : Alpha_context.Receipt.balance_updates)
(allocated_destination_contract : bool)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list Script_typed_ir.packed_internal_operation) :=
let? balance := Alpha_context.Contract.get_balance ctxt contract in
let now := Alpha_context.Script_timestamp.now ctxt in
let level :=
Alpha_context.Script_int.abs
(Alpha_context.Script_int.of_int32
(Alpha_context.Raw_level.to_int32
(Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level))) in
let step_constants :=
{| Script_typed_ir.step_constants.source := source;
Script_typed_ir.step_constants.payer :=
Alpha_context.Contract.implicit_contract payer;
Script_typed_ir.step_constants.self := contract;
Script_typed_ir.step_constants.amount := amount;
Script_typed_ir.step_constants.balance := balance;
Script_typed_ir.step_constants.chain_id := chain_id;
Script_typed_ir.step_constants.now := now;
Script_typed_ir.step_constants.level := level; |} in
let execute :=
match parameter with
| Untyped_arg parameter ⇒
fun x_1 x_2 x_3 x_4 x_5 x_6 x_7 ⇒
Script_interpreter.execute x_1 x_2 x_3 x_4 x_5 x_6 x_7 parameter
| Typed_arg location parameter_ty parameter ⇒
fun x_1 x_2 x_3 x_4 x_5 x_6 x_7 ⇒
Script_interpreter.execute_with_typed_parameter x_1 x_2 x_3 x_4 x_5 x_6
x_7 parameter_ty location parameter
end in
let cached_script := Some script_ir in
let?
'({|
Script_interpreter.execution_result.script := updated_cached_script;
Script_interpreter.execution_result.code_size := updated_size;
Script_interpreter.execution_result.storage := storage_value;
Script_interpreter.execution_result.lazy_storage_diff :=
lazy_storage_diff;
Script_interpreter.execution_result.operations := operations;
Script_interpreter.execution_result.ticket_diffs := ticket_diffs
|}, ctxt) :=
execute None ctxt cached_script mode step_constants script entrypoint
internal in
let? '(ticket_table_size_diff, ctxt) :=
update_script_storage_and_ticket_balances ctxt contract storage_value
lazy_storage_diff ticket_diffs operations in
let? '(ticket_paid_storage_diff, ctxt) :=
Alpha_context.Ticket_balance.adjust_storage_space ctxt
ticket_table_size_diff in
let? '(ctxt, new_size, contract_paid_storage_size_diff) :=
Alpha_context.Fees.record_paid_storage_space ctxt contract in
let? originated_contracts :=
Alpha_context.Contract.originated_from_current_nonce before_operation ctxt
in
let? ctxt :=
Script_cache.update ctxt cache_key
((Alpha_context.Script.t.with_storage
(Alpha_context.Script.lazy_expr_value storage_value) script),
updated_cached_script) updated_size in
let result_value :=
Apply_results.Transaction_result
(Apply_results.Transaction_to_contract_result
{|
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
:= Some storage_value;
Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:= lazy_storage_diff;
Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:= balance_updates;
Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:= originated_contracts;
Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:= Alpha_context.Gas.consumed before_operation ctxt;
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:= new_size;
Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:= contract_paid_storage_size_diff +Z ticket_paid_storage_diff;
Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:= allocated_destination_contract; |}) in
return? (ctxt, result_value, operations).
Definition apply_transaction
(ctxt : Alpha_context.context) (parameter : execution_arg)
(source : Alpha_context.Contract.t)
(contract : Alpha_context.Contract.contract) (amount : Alpha_context.Tez.t)
(entrypoint : Alpha_context.Entrypoint.t)
(before_operation : Alpha_context.context)
(payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
(mode : Script_ir_translator.unparsing_mode) (internal : bool)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list Script_typed_ir.packed_internal_operation) :=
let? allocated_destination_contract :=
match Alpha_context.Contract.is_implicit contract with
| None ⇒
let? '_ :=
if Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero then
Alpha_context.Contract.must_exist ctxt contract
else
Error_monad.return_unit in
Error_monad.return_false
| Some _ ⇒
let? '_ :=
Error_monad.error_when
(Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
(Build_extensible "Empty_transaction" Alpha_context.Contract.contract
contract) in
Error_monad.op_gtpipeeqquestion
(Alpha_context.Contract.allocated ctxt contract) Pervasives.not
end in
let? '(ctxt, balance_updates) :=
Alpha_context.Token.transfer None ctxt
(Alpha_context.Token.Source_container
(Alpha_context.Token.Contract source))
(Alpha_context.Token.Sink_container
(Alpha_context.Token.Contract contract)) amount in
let? '(ctxt, cache_key, script) := Script_cache.find ctxt contract in
match script with
| None ⇒
let? '(ctxt, result_value) :=
apply_transaction_to_implicit ctxt contract parameter entrypoint
before_operation balance_updates allocated_destination_contract in
return? (ctxt, result_value, nil)
| Some (script, script_ir) ⇒
apply_transaction_to_smart_contract ctxt source contract amount entrypoint
before_operation payer chain_id mode internal script_ir script parameter
cache_key balance_updates allocated_destination_contract
end.
Definition ex_ticket_size
(ctxt : Alpha_context.context) (function_parameter : Ticket_scanner.ex_ticket)
: M? (Alpha_context.context × int) :=
let 'Ticket_scanner.Ex_ticket ty ticket := function_parameter in
let? ty := Script_typed_ir.ticket_t Micheline.dummy_location ty in
let? '(ty', ctxt) :=
Script_ir_translator.unparse_ty Micheline.dummy_location ctxt ty in
let '(ty_nodes, ty_size) := Script_typed_ir_size.node_size ty' in
let ty_size := Saturation_repr.to_int ty_size in
let ty_size_cost := Script_typed_ir_size_costs.nodes_cost ty_nodes in
let? ctxt := Alpha_context.Gas.consume ctxt ty_size_cost in
let '(val_nodes, val_size) := Script_typed_ir_size.value_size ty ticket in
let val_size := Saturation_repr.to_int val_size in
let val_size_cost := Script_typed_ir_size_costs.nodes_cost val_nodes in
let? ctxt := Alpha_context.Gas.consume ctxt val_size_cost in
return? (ctxt, (ty_size +i val_size)).
Definition apply_transaction_to_tx_rollup {A B : Set}
(ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
(parameters : A) (amount : Alpha_context.Tez.t)
(entrypoint : Alpha_context.Entrypoint.t)
(payer : Alpha_context.public_key_hash)
(dst_rollup : Alpha_context.Tx_rollup.t) (since : Alpha_context.context)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list B) :=
let? '_ := assert_tx_rollup_feature_enabled ctxt in
let? '_ :=
Error_monad.fail_unless
(Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
(Build_extensible "Tx_rollup_invalid_transaction_amount" unit tt) in
if
Alpha_context.Entrypoint.op_eq entrypoint
Alpha_context.Tx_rollup.deposit_entrypoint
then
let? '{|
Tx_rollup_parameters.deposit_parameters.ex_ticket := ex_ticket;
Tx_rollup_parameters.deposit_parameters.l2_destination := l2_destination
|} :=
Tx_rollup_parameters.get_deposit_parameters parameters_ty parameters in
let? '(ctxt, ticket_size) := ex_ticket_size ctxt ex_ticket in
let limit := Alpha_context.Constants.tx_rollup_max_ticket_payload_size ctxt
in
let? '_ :=
Error_monad.fail_when (ticket_size >i limit)
(Build_extensible "Ticket_payload_size_limit_exceeded"
Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded
{|
Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded.payload_size
:= ticket_size;
Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded.limit :=
limit; |}) in
let '(ex_token, ticket_amount) :=
Ticket_token.token_and_amount_of_ex_ticket ex_ticket in
let? '(ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Tx_rollup dst_rollup) ex_token in
let? ticket_amount :=
Option.value_e
(Option.bind (Alpha_context.Script_int.to_int64 ticket_amount)
Tx_rollup_l2_qty.of_int64)
(Error_monad.trace_of_error
(Build_extensible "Tx_rollup_invalid_transaction_amount" unit tt)) in
let '(deposit, message_size) :=
Alpha_context.Tx_rollup_message.make_deposit payer l2_destination
ticket_hash ticket_amount in
let? '(ctxt, state_value) :=
Alpha_context.Tx_rollup_state.get ctxt dst_rollup in
let? cost :=
Alpha_context.Tx_rollup_state.burn_cost None state_value message_size in
let? '(ctxt, balance_updates) :=
Alpha_context.Token.transfer None ctxt
(Alpha_context.Token.Source_container
(Alpha_context.Token.Contract
(Alpha_context.Contract.implicit_contract payer)))
(Alpha_context.Token.Sink_infinite Alpha_context.Token.Burned) cost in
let? '(ctxt, state_value, paid_storage_size_diff) :=
Alpha_context.Tx_rollup_inbox.append_message ctxt dst_rollup state_value
deposit in
let? ctxt :=
Alpha_context.Tx_rollup_state.update ctxt dst_rollup state_value in
let result_value :=
Apply_results.Transaction_result
(Apply_results.Transaction_to_tx_rollup_result
{|
Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
:= ticket_hash;
Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
:= balance_updates;
Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
:= Alpha_context.Gas.consumed since ctxt;
Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
:= paid_storage_size_diff; |}) in
return? (ctxt, result_value, nil)
else
Error_monad.fail
(Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
entrypoint).
Definition apply_origination {A B : Set}
(ctxt : Alpha_context.context) (storage_type : Script_typed_ir.ty)
(storage_value : A)
(unparsed_code : Micheline.canonical Alpha_context.Script.prim)
(contract : Alpha_context.Contract.t)
(delegate : option Signature.public_key_hash)
(source : Alpha_context.Contract.t) (credit : Alpha_context.Tez.t)
(before_operation : Alpha_context.context)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list B) :=
let? '(to_duplicate, ctxt) :=
Script_ir_translator.collect_lazy_storage ctxt storage_type storage_value in
let to_update := Script_ir_translator.no_lazy_storage_id in
let? '(storage_value, lazy_storage_diff, ctxt) :=
Script_ir_translator.extract_lazy_storage_diff ctxt
Script_ir_translator.Optimized false to_duplicate to_update storage_type
storage_value in
let? '(storage_value, ctxt) :=
Script_ir_translator.unparse_data ctxt Script_ir_translator.Optimized
storage_type storage_value in
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Alpha_context.Script.strip_locations_cost storage_value) in
let storage_value :=
Alpha_context.Script.lazy_expr_value
(Micheline.strip_locations storage_value) in
let? '(code, ctxt) :=
Script_ir_translator.unparse_code ctxt Script_ir_translator.Optimized
(Micheline.root_value unparsed_code) in
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Alpha_context.Script.strip_locations_cost code) in
let code :=
Alpha_context.Script.lazy_expr_value (Micheline.strip_locations code) in
let script :=
{| Alpha_context.Script.t.code := code;
Alpha_context.Script.t.storage := storage_value; |} in
let? ctxt :=
Alpha_context.Contract.raw_originate ctxt false contract
(script, lazy_storage_diff) in
let? ctxt :=
match delegate with
| None ⇒ return? ctxt
| Some delegate ⇒ Alpha_context.Delegate.init_value ctxt contract delegate
end in
let? '(ctxt, balance_updates) :=
Alpha_context.Token.transfer None ctxt
(Alpha_context.Token.Source_container
(Alpha_context.Token.Contract source))
(Alpha_context.Token.Sink_container
(Alpha_context.Token.Contract contract)) credit in
let? '(ctxt, size_value, paid_storage_size_diff) :=
Alpha_context.Fees.record_paid_storage_space ctxt contract in
let result_value :=
Apply_results.Origination_result
{|
Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff
:= lazy_storage_diff;
Apply_results.successful_manager_operation_result.Origination_result.balance_updates
:= balance_updates;
Apply_results.successful_manager_operation_result.Origination_result.originated_contracts
:= [ contract ];
Apply_results.successful_manager_operation_result.Origination_result.consumed_gas
:= Alpha_context.Gas.consumed before_operation ctxt;
Apply_results.successful_manager_operation_result.Origination_result.storage_size
:= size_value;
Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff
:= paid_storage_size_diff; |} in
return? (ctxt, result_value, nil).
Definition prepare_apply_manager_operation_content
(ctxt : Alpha_context.context) (source : Alpha_context.Contract.contract)
(gas_consumed_in_precheck : option Alpha_context.Gas.cost)
: M?
(Alpha_context.context × Alpha_context.context ×
Alpha_context.Script.consume_deserialization_gas) :=
let before_operation := ctxt in
let? '_ := Alpha_context.Contract.must_exist ctxt source in
let? ctxt :=
Alpha_context.Gas.consume ctxt Michelson_v1_gas.Cost_of.manager_operation in
let? ctxt :=
match gas_consumed_in_precheck with
| None ⇒ Pervasives.Ok ctxt
| Some gas ⇒ Alpha_context.Gas.consume ctxt gas
end in
let consume_deserialization_gas := Alpha_context.Script.When_needed in
return? (ctxt, before_operation, consume_deserialization_gas).
Definition apply_internal_manager_operation_content
(ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
(payer : Alpha_context.public_key_hash) (source : Alpha_context.Contract.t)
(chain_id : Chain_id.t)
(gas_consumed_in_precheck : option Alpha_context.Gas.cost)
(operation : Script_typed_ir.manager_operation)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list Script_typed_ir.packed_internal_operation) :=
let? '(ctxt, before_operation, consume_deserialization_gas) :=
prepare_apply_manager_operation_content ctxt source gas_consumed_in_precheck
in
match operation with
|
Script_typed_ir.Transaction {|
Script_typed_ir.manager_operation.Transaction.transaction := {|
Alpha_context.transaction.amount := amount;
Alpha_context.transaction.parameters := _;
Alpha_context.transaction.entrypoint := entrypoint;
Alpha_context.transaction.destination :=
Alpha_context.Destination.Contract contract
|};
Script_typed_ir.manager_operation.Transaction.location := location;
Script_typed_ir.manager_operation.Transaction.parameters_ty :=
parameters_ty;
Script_typed_ir.manager_operation.Transaction.parameters :=
typed_parameters
|} ⇒
let? '(ctxt, manager_result, operations) :=
apply_transaction ctxt (Typed_arg location parameters_ty typed_parameters)
source contract amount entrypoint before_operation payer chain_id mode
true in
return? (ctxt, manager_result, operations)
|
Script_typed_ir.Transaction {|
Script_typed_ir.manager_operation.Transaction.transaction := {|
Alpha_context.transaction.amount := amount;
Alpha_context.transaction.parameters := _;
Alpha_context.transaction.entrypoint := entrypoint;
Alpha_context.transaction.destination :=
Alpha_context.Destination.Tx_rollup dst
|};
Script_typed_ir.manager_operation.Transaction.location := _;
Script_typed_ir.manager_operation.Transaction.parameters_ty :=
parameters_ty;
Script_typed_ir.manager_operation.Transaction.parameters := parameters
|} ⇒
apply_transaction_to_tx_rollup ctxt parameters_ty parameters amount
entrypoint payer dst before_operation
|
Script_typed_ir.Origination {|
Script_typed_ir.manager_operation.Origination.origination := {|
Alpha_context.origination.delegate := delegate;
Alpha_context.origination.script := script;
Alpha_context.origination.credit := credit
|};
Script_typed_ir.manager_operation.Origination.preorigination := contract;
Script_typed_ir.manager_operation.Origination.storage_type :=
storage_type;
Script_typed_ir.manager_operation.Origination.storage := storage_value
|} ⇒
let? '(unparsed_code, ctxt) :=
Alpha_context.Script.force_decode_in_context consume_deserialization_gas
ctxt script.(Alpha_context.Script.t.code) in
apply_origination ctxt storage_type storage_value unparsed_code contract
delegate source credit before_operation
| Script_typed_ir.Delegation delegate ⇒
apply_delegation ctxt source delegate before_operation
end.
Axiom apply_external_manager_operation_content :
Alpha_context.context → Script_ir_translator.unparsing_mode →
Alpha_context.public_key_hash → Chain_id.t →
option Alpha_context.Gas.cost → Alpha_context.manager_operation →
M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list Script_typed_ir.packed_internal_operation).
Inductive success_or_failure : Set :=
| Success : Alpha_context.context → success_or_failure
| Failure : success_or_failure.
#[bypass_check(guard)]
Definition apply_internal_manager_operations
(ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
(payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
(ops : list Script_typed_ir.packed_internal_operation)
: success_or_failure ×
list Apply_results.packed_internal_manager_operation_result :=
let fix apply
(ctxt : Alpha_context.context)
(applied : list Apply_results.packed_internal_manager_operation_result)
(worklist : list Script_typed_ir.packed_internal_operation) {struct ctxt}
: success_or_failure ×
list Apply_results.packed_internal_manager_operation_result :=
match worklist with
| [] ⇒ ((Success ctxt), (List.rev applied))
|
cons
(Script_typed_ir.Internal_operation
({|
Script_typed_ir.internal_operation.source := source;
Script_typed_ir.internal_operation.operation := operation;
Script_typed_ir.internal_operation.nonce := nonce_value
|} as op)) rest ⇒
let op_res := Apply_results.contents_of_internal_operation op in
let function_parameter :=
if Alpha_context.internal_nonce_already_recorded ctxt nonce_value then
Error_monad.fail
(Build_extensible "Internal_operation_replay"
Apply_results.packed_internal_contents
(Apply_results.Internal_contents op_res))
else
let ctxt := Alpha_context.record_internal_nonce ctxt nonce_value in
apply_internal_manager_operation_content ctxt mode payer source
chain_id None operation in
match function_parameter with
| Pervasives.Error errors ⇒
let result_value :=
Apply_results.pack_internal_manager_operation_result op
(Apply_results.Failed
(Script_typed_ir.manager_kind
op.(Script_typed_ir.internal_operation.operation)) errors) in
let skipped :=
List.rev_map
(fun (function_parameter :
Script_typed_ir.packed_internal_operation) ⇒
let 'Script_typed_ir.Internal_operation op := function_parameter
in
Apply_results.pack_internal_manager_operation_result op
(Apply_results.Skipped
(Script_typed_ir.manager_kind
op.(Script_typed_ir.internal_operation.operation)))) rest in
(Failure,
(List.rev (Pervasives.op_at skipped (cons result_value applied))))
| Pervasives.Ok (ctxt, result_value, emitted) ⇒
apply ctxt
(cons
(Apply_results.pack_internal_manager_operation_result op
(Apply_results.Applied result_value)) applied)
(Pervasives.op_at emitted rest)
end
end in
apply ctxt nil ops.
Definition precheck_manager_contents
(ctxt : Alpha_context.context) (op : Alpha_context.contents)
(only_batch : bool)
: M? (Alpha_context.context × Apply_results.precheck_result) :=
match op with
|
Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.source := source;
Alpha_context.contents.Manager_operation.fee := fee;
Alpha_context.contents.Manager_operation.counter := counter;
Alpha_context.contents.Manager_operation.operation := operation;
Alpha_context.contents.Manager_operation.gas_limit := gas_limit;
Alpha_context.contents.Manager_operation.storage_limit := storage_limit
|} ⇒
let? ctxt :=
(if only_batch then
Error_monad.record_trace (Build_extensible "Gas_limit_too_high" unit tt)
else
fun (errs : M? Alpha_context.context) ⇒ errs)
(Alpha_context.Gas.consume_limit_in_block ctxt gas_limit) in
let ctxt := Alpha_context.Gas.set_limit ctxt gas_limit in
let ctxt_before := ctxt in
let? '_ := Alpha_context.Fees.check_storage_limit ctxt storage_limit in
let source_contract := Alpha_context.Contract.implicit_contract source in
let? '_ := Alpha_context.Contract.must_be_allocated ctxt source_contract in
let? '_ :=
Alpha_context.Contract.check_counter_increment ctxt source counter in
let consume_deserialization_gas := Alpha_context.Script.Always in
let? ctxt :=
match operation with
| Alpha_context.Reveal pk ⇒
Alpha_context.Contract.reveal_manager_key ctxt source pk
|
Alpha_context.Transaction {|
Alpha_context.transaction.parameters := parameters;
Alpha_context.transaction.destination := destination
|} ⇒
let? '_ :=
Error_monad.fail_when
match destination with
| Alpha_context.Destination.Tx_rollup _ ⇒ true
| _ ⇒ false
end (Build_extensible "Tx_rollup_non_internal_transaction" unit tt)
in
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(let? '(_arg, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt parameters in
return? ctxt)
|
Alpha_context.Origination {|
Alpha_context.origination.script := script |} ⇒
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(let? '(_code, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt
script.(Alpha_context.Script.t.code) in
let? '(_storage, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt
script.(Alpha_context.Script.t.storage) in
return? ctxt)
|
Alpha_context.Register_global_constant {|
Alpha_context.manager_operation.Register_global_constant.value := value_value
|} ⇒
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(let? '(_value, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt value_value in
return? ctxt)
| (Alpha_context.Delegation _ | Alpha_context.Set_deposits_limit _) ⇒
return? ctxt
| Alpha_context.Tx_rollup_origination ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
return? ctxt
|
Alpha_context.Tx_rollup_submit_batch {|
Alpha_context.manager_operation.Tx_rollup_submit_batch.content := content
|} ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
let size_limit :=
Alpha_context.Constants.tx_rollup_hard_size_limit_per_message ctxt in
let '(_message, message_size) :=
Alpha_context.Tx_rollup_message.make_batch content in
let? cost := Tx_rollup_gas.hash_cost message_size in
let? ctxt := Alpha_context.Gas.consume ctxt cost in
let? '_ :=
Error_monad.fail_unless (message_size ≤i size_limit)
(Build_extensible "Message_size_exceeds_limit" unit tt) in
return? ctxt
|
(Alpha_context.Tx_rollup_commit _ |
Alpha_context.Tx_rollup_return_bond _ |
Alpha_context.Tx_rollup_finalize_commitment _ |
Alpha_context.Tx_rollup_remove_commitment _) ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
return? ctxt
|
Alpha_context.Transfer_ticket {|
Alpha_context.manager_operation.Transfer_ticket.contents := contents;
Alpha_context.manager_operation.Transfer_ticket.ty := ty
|} ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(let? '(_contents, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt contents in
let? '(_ty, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt ty in
return? ctxt)
|
Alpha_context.Tx_rollup_dispatch_tickets {|
Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.message_result_path
:= message_result_path;
Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.tickets_info
:= tickets_info
|} ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
let '{|
Alpha_context.Constants.parametric.tx_rollup_max_messages_per_inbox :=
tx_rollup_max_messages_per_inbox;
Alpha_context.Constants.parametric.tx_rollup_max_withdrawals_per_batch
:= tx_rollup_max_withdrawals_per_batch
|} := Alpha_context.Constants.parametric_value ctxt in
let? '_ :=
Alpha_context.Tx_rollup_errors.check_path_depth
Alpha_context.Tx_rollup_errors.Commitment
(Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
message_result_path) tx_rollup_max_messages_per_inbox in
let? '_ :=
Error_monad.error_when (Compare.List_length_with.op_eq tickets_info 0)
(Build_extensible "No_withdrawals_to_dispatch" unit tt) in
let? '_ :=
Error_monad.error_when
(Compare.List_length_with.op_gt tickets_info
tx_rollup_max_withdrawals_per_batch)
(Build_extensible "Too_many_withdrawals" unit tt) in
let? ctxt :=
Error_monad.record_trace
(Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
(List.fold_left_e
(fun (ctxt : Alpha_context.context) ⇒
fun (function_parameter : Alpha_context.Tx_rollup_reveal.t) ⇒
let '{|
Alpha_context.Tx_rollup_reveal.t.contents := contents;
Alpha_context.Tx_rollup_reveal.t.ty := ty
|} := function_parameter in
let? '(_contents, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt contents in
let? '(_ty, ctxt) :=
Alpha_context.Script.force_decode_in_context
consume_deserialization_gas ctxt ty in
return? ctxt) ctxt tickets_info) in
return? ctxt
|
Alpha_context.Tx_rollup_rejection {|
Alpha_context.manager_operation.Tx_rollup_rejection.message_path :=
message_path;
Alpha_context.manager_operation.Tx_rollup_rejection.message_result_path
:= message_result_path;
Alpha_context.manager_operation.Tx_rollup_rejection.previous_message_result_path
:= previous_message_result_path
|} ⇒
let? '_ := assert_tx_rollup_feature_enabled ctxt in
let '{|
Alpha_context.Constants.parametric.tx_rollup_max_messages_per_inbox :=
tx_rollup_max_messages_per_inbox
|} := Alpha_context.Constants.parametric_value ctxt in
let? '_ :=
Alpha_context.Tx_rollup_errors.check_path_depth
Alpha_context.Tx_rollup_errors.Inbox
(Alpha_context.Tx_rollup_inbox.Merkle.path_depth message_path)
tx_rollup_max_messages_per_inbox in
let? '_ :=
Alpha_context.Tx_rollup_errors.check_path_depth
Alpha_context.Tx_rollup_errors.Commitment
(Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
message_result_path) tx_rollup_max_messages_per_inbox in
let? '_ :=
Alpha_context.Tx_rollup_errors.check_path_depth
Alpha_context.Tx_rollup_errors.Commitment
(Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
previous_message_result_path) tx_rollup_max_messages_per_inbox in
return? ctxt
|
(Alpha_context.Sc_rollup_originate _ |
Alpha_context.Sc_rollup_add_messages _ |
Alpha_context.Sc_rollup_cement _ | Alpha_context.Sc_rollup_publish _) ⇒
let? '_ := assert_sc_rollup_feature_enabled ctxt in
return? ctxt
end in
let? ctxt := Alpha_context.Contract.increment_counter ctxt source in
let? '(ctxt, balance_updates) :=
Alpha_context.Token.transfer None ctxt
(Alpha_context.Token.Source_container
(Alpha_context.Token.Contract source_contract))
(Alpha_context.Token.Sink_container Alpha_context.Token.Block_fees) fee
in
let consumed_gas := Alpha_context.Gas.consumed ctxt_before ctxt in
return?
(ctxt,
{| Apply_results.precheck_result.consumed_gas := consumed_gas;
Apply_results.precheck_result.balance_updates := balance_updates; |})
| _ ⇒ unreachable_gadt_branch
end.
[burn_storage_fees ctxt smopr storage_limit payer] burns the storage fees
associated to an operation result [smopr].
Returns an updated context, an updated storage limit with the space consumed
by the operation subtracted, and [smopr] with the relevant balance updates
included.
Definition burn_storage_fees
(ctxt : Alpha_context.context)
(smopr : Apply_results.successful_manager_operation_result)
(storage_limit : Z.t) (payer : Alpha_context.public_key_hash)
: M?
(Alpha_context.context × Z.t ×
Apply_results.successful_manager_operation_result) :=
let payer :=
Alpha_context.Token.Source_container
(Alpha_context.Token.Contract
(Alpha_context.Contract.implicit_contract payer)) in
match smopr with
|
Apply_results.Transaction_result
(Apply_results.Transaction_to_contract_result payload) ⇒
let consumed :=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let? '(ctxt, storage_limit, origination_bus) :=
if
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract)
then
Alpha_context.Fees.burn_origination_fees None ctxt storage_limit payer
else
return? (ctxt, storage_limit, nil) in
let balance_updates :=
Pervasives.op_at storage_bus
(Pervasives.op_at
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates)
origination_bus) in
return?
(ctxt, storage_limit,
(Apply_results.Transaction_result
(Apply_results.Transaction_to_contract_result
{|
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.storage);
Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff);
Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:= balance_updates;
Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts);
Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas);
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size);
Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff);
Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract);
|})))
|
Apply_results.Transaction_result
(Apply_results.Transaction_to_tx_rollup_result payload) ⇒
let consumed :=
payload.(Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at storage_bus
payload.(Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Transaction_result
(Apply_results.Transaction_to_tx_rollup_result
(Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.with_balance_updates
balance_updates payload))))
| Apply_results.Origination_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let? '(ctxt, storage_limit, origination_bus) :=
Alpha_context.Fees.burn_origination_fees None ctxt storage_limit payer in
let balance_updates :=
Pervasives.op_at storage_bus
(Pervasives.op_at origination_bus
payload.(Apply_results.successful_manager_operation_result.Origination_result.balance_updates))
in
return?
(ctxt, storage_limit,
(Apply_results.Origination_result
{|
Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff);
Apply_results.successful_manager_operation_result.Origination_result.balance_updates
:= balance_updates;
Apply_results.successful_manager_operation_result.Origination_result.originated_contracts
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.originated_contracts);
Apply_results.successful_manager_operation_result.Origination_result.consumed_gas
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.consumed_gas);
Apply_results.successful_manager_operation_result.Origination_result.storage_size
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.storage_size);
Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff);
|}))
| (Apply_results.Reveal_result _ | Apply_results.Delegation_result _) ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Register_global_constant_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at storage_bus
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Register_global_constant_result
{|
Apply_results.successful_manager_operation_result.Register_global_constant_result.balance_updates
:= balance_updates;
Apply_results.successful_manager_operation_result.Register_global_constant_result.consumed_gas
:=
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.consumed_gas);
Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant
:=
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant);
Apply_results.successful_manager_operation_result.Register_global_constant_result.global_address
:=
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.global_address);
|}))
| Apply_results.Set_deposits_limit_result _ ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Tx_rollup_origination_result payload ⇒
let? '(ctxt, storage_limit, origination_bus) :=
Alpha_context.Fees.burn_tx_rollup_origination_fees None ctxt storage_limit
payer in
let balance_updates :=
Pervasives.op_at origination_bus
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Tx_rollup_origination_result
(Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.with_balance_updates
balance_updates payload)))
|
(Apply_results.Tx_rollup_return_bond_result _ |
Apply_results.Tx_rollup_remove_commitment_result _ |
Apply_results.Tx_rollup_rejection_result _ |
Apply_results.Tx_rollup_finalize_commitment_result _ |
Apply_results.Tx_rollup_commit_result _) ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Transfer_ticket_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at
payload.(Apply_results.successful_manager_operation_result.Transfer_ticket_result.balance_updates)
storage_bus in
return?
(ctxt, storage_limit,
(Apply_results.Transfer_ticket_result
(Apply_results.successful_manager_operation_result.Transfer_ticket_result.with_balance_updates
balance_updates payload)))
| Apply_results.Tx_rollup_submit_batch_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at storage_bus
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Tx_rollup_submit_batch_result
(Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.with_balance_updates
balance_updates payload)))
| Apply_results.Tx_rollup_dispatch_tickets_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at storage_bus
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Tx_rollup_dispatch_tickets_result
(Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.with_balance_updates
balance_updates payload)))
| Apply_results.Sc_rollup_originate_result payload ⇒
let? '(ctxt, storage_limit, balance_updates) :=
Alpha_context.Fees.burn_sc_rollup_origination_fees None ctxt storage_limit
payer
payload.(Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.size)
in
let result_value :=
Apply_results.Sc_rollup_originate_result
(Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.with_balance_updates
balance_updates payload) in
return? (ctxt, storage_limit, result_value)
| Apply_results.Sc_rollup_add_messages_result _ ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Sc_rollup_cement_result _ ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Sc_rollup_publish_result _ ⇒
return? (ctxt, storage_limit, smopr)
end.
Definition apply_manager_contents
(ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
(chain_id : Chain_id.t)
(gas_consumed_in_precheck : option Alpha_context.Gas.cost)
(op : Alpha_context.contents)
: success_or_failure × Apply_results.manager_operation_result ×
list Apply_results.packed_internal_manager_operation_result :=
match op with
|
Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.source := source;
Alpha_context.contents.Manager_operation.operation := operation;
Alpha_context.contents.Manager_operation.gas_limit := gas_limit;
Alpha_context.contents.Manager_operation.storage_limit := storage_limit
|} ⇒
let ctxt := Alpha_context.Gas.set_limit ctxt gas_limit in
let function_parameter :=
apply_external_manager_operation_content ctxt mode source chain_id
gas_consumed_in_precheck operation in
match function_parameter with
| Pervasives.Ok (ctxt, operation_results, internal_operations) ⇒
let function_parameter :=
apply_internal_manager_operations ctxt mode source chain_id
internal_operations in
match function_parameter with
| (Success ctxt, internal_operations_results) ⇒
let function_parameter :=
burn_storage_fees ctxt operation_results storage_limit source in
match function_parameter with
| Pervasives.Ok (ctxt, storage_limit, operation_results) ⇒
let function_parameter :=
List.fold_left_es
(fun (function_parameter :
Alpha_context.context × Z.t ×
list Apply_results.packed_internal_manager_operation_result)
⇒
let '(ctxt, storage_limit, res) := function_parameter in
fun (imopr :
Apply_results.packed_internal_manager_operation_result) ⇒
let
'Apply_results.Internal_manager_operation_result op mopr :=
imopr in
match mopr with
| Apply_results.Applied smopr ⇒
let? '(ctxt, storage_limit, smopr) :=
burn_storage_fees ctxt smopr storage_limit source in
let imopr :=
Apply_results.Internal_manager_operation_result op
(Apply_results.Applied smopr) in
return? (ctxt, storage_limit, (cons imopr res))
| _ ⇒ return? (ctxt, storage_limit, (cons imopr res))
end) (ctxt, storage_limit, nil) internal_operations_results in
match function_parameter with
| Pervasives.Ok (ctxt, _, internal_operations_results) ⇒
((Success ctxt), (Apply_results.Applied operation_results),
(List.rev internal_operations_results))
| Pervasives.Error errors ⇒
(Failure,
(Apply_results.Backtracked operation_results (Some errors)),
internal_operations_results)
end
| Pervasives.Error errors ⇒
(Failure, (Apply_results.Backtracked operation_results (Some errors)),
internal_operations_results)
end
| (Failure, internal_operations_results) ⇒
(Failure, (Apply_results.Applied operation_results),
internal_operations_results)
end
| Pervasives.Error errors ⇒
(Failure,
(Apply_results.Failed (Alpha_context.manager_kind operation) errors),
nil)
end
| _ ⇒ unreachable_gadt_branch
end.
Definition skipped_operation_result
(operation : Alpha_context.manager_operation)
: Apply_results.manager_operation_result :=
match operation with
| Alpha_context.Reveal _ ⇒
Apply_results.Applied
(Apply_results.Reveal_result
{|
Apply_results.successful_manager_operation_result.Reveal_result.consumed_gas
:= Alpha_context.Gas.Arith.zero; |})
| _ ⇒ Apply_results.Skipped (Alpha_context.manager_kind operation)
end.
Axiom mark_skipped :
Signature.public_key_hash → Alpha_context.Level.t →
Apply_results.prechecked_contents_list → Apply_results.contents_result_list.
(ctxt : Alpha_context.context)
(smopr : Apply_results.successful_manager_operation_result)
(storage_limit : Z.t) (payer : Alpha_context.public_key_hash)
: M?
(Alpha_context.context × Z.t ×
Apply_results.successful_manager_operation_result) :=
let payer :=
Alpha_context.Token.Source_container
(Alpha_context.Token.Contract
(Alpha_context.Contract.implicit_contract payer)) in
match smopr with
|
Apply_results.Transaction_result
(Apply_results.Transaction_to_contract_result payload) ⇒
let consumed :=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let? '(ctxt, storage_limit, origination_bus) :=
if
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract)
then
Alpha_context.Fees.burn_origination_fees None ctxt storage_limit payer
else
return? (ctxt, storage_limit, nil) in
let balance_updates :=
Pervasives.op_at storage_bus
(Pervasives.op_at
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates)
origination_bus) in
return?
(ctxt, storage_limit,
(Apply_results.Transaction_result
(Apply_results.Transaction_to_contract_result
{|
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.storage);
Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff);
Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:= balance_updates;
Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts);
Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas);
Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size);
Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff);
Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:=
payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract);
|})))
|
Apply_results.Transaction_result
(Apply_results.Transaction_to_tx_rollup_result payload) ⇒
let consumed :=
payload.(Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at storage_bus
payload.(Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Transaction_result
(Apply_results.Transaction_to_tx_rollup_result
(Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.with_balance_updates
balance_updates payload))))
| Apply_results.Origination_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let? '(ctxt, storage_limit, origination_bus) :=
Alpha_context.Fees.burn_origination_fees None ctxt storage_limit payer in
let balance_updates :=
Pervasives.op_at storage_bus
(Pervasives.op_at origination_bus
payload.(Apply_results.successful_manager_operation_result.Origination_result.balance_updates))
in
return?
(ctxt, storage_limit,
(Apply_results.Origination_result
{|
Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff);
Apply_results.successful_manager_operation_result.Origination_result.balance_updates
:= balance_updates;
Apply_results.successful_manager_operation_result.Origination_result.originated_contracts
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.originated_contracts);
Apply_results.successful_manager_operation_result.Origination_result.consumed_gas
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.consumed_gas);
Apply_results.successful_manager_operation_result.Origination_result.storage_size
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.storage_size);
Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff
:=
payload.(Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff);
|}))
| (Apply_results.Reveal_result _ | Apply_results.Delegation_result _) ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Register_global_constant_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at storage_bus
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Register_global_constant_result
{|
Apply_results.successful_manager_operation_result.Register_global_constant_result.balance_updates
:= balance_updates;
Apply_results.successful_manager_operation_result.Register_global_constant_result.consumed_gas
:=
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.consumed_gas);
Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant
:=
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant);
Apply_results.successful_manager_operation_result.Register_global_constant_result.global_address
:=
payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.global_address);
|}))
| Apply_results.Set_deposits_limit_result _ ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Tx_rollup_origination_result payload ⇒
let? '(ctxt, storage_limit, origination_bus) :=
Alpha_context.Fees.burn_tx_rollup_origination_fees None ctxt storage_limit
payer in
let balance_updates :=
Pervasives.op_at origination_bus
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Tx_rollup_origination_result
(Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.with_balance_updates
balance_updates payload)))
|
(Apply_results.Tx_rollup_return_bond_result _ |
Apply_results.Tx_rollup_remove_commitment_result _ |
Apply_results.Tx_rollup_rejection_result _ |
Apply_results.Tx_rollup_finalize_commitment_result _ |
Apply_results.Tx_rollup_commit_result _) ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Transfer_ticket_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at
payload.(Apply_results.successful_manager_operation_result.Transfer_ticket_result.balance_updates)
storage_bus in
return?
(ctxt, storage_limit,
(Apply_results.Transfer_ticket_result
(Apply_results.successful_manager_operation_result.Transfer_ticket_result.with_balance_updates
balance_updates payload)))
| Apply_results.Tx_rollup_submit_batch_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at storage_bus
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Tx_rollup_submit_batch_result
(Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.with_balance_updates
balance_updates payload)))
| Apply_results.Tx_rollup_dispatch_tickets_result payload ⇒
let consumed :=
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff)
in
let? '(ctxt, storage_limit, storage_bus) :=
Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
consumed in
let balance_updates :=
Pervasives.op_at storage_bus
payload.(Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates)
in
return?
(ctxt, storage_limit,
(Apply_results.Tx_rollup_dispatch_tickets_result
(Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.with_balance_updates
balance_updates payload)))
| Apply_results.Sc_rollup_originate_result payload ⇒
let? '(ctxt, storage_limit, balance_updates) :=
Alpha_context.Fees.burn_sc_rollup_origination_fees None ctxt storage_limit
payer
payload.(Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.size)
in
let result_value :=
Apply_results.Sc_rollup_originate_result
(Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.with_balance_updates
balance_updates payload) in
return? (ctxt, storage_limit, result_value)
| Apply_results.Sc_rollup_add_messages_result _ ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Sc_rollup_cement_result _ ⇒
return? (ctxt, storage_limit, smopr)
| Apply_results.Sc_rollup_publish_result _ ⇒
return? (ctxt, storage_limit, smopr)
end.
Definition apply_manager_contents
(ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
(chain_id : Chain_id.t)
(gas_consumed_in_precheck : option Alpha_context.Gas.cost)
(op : Alpha_context.contents)
: success_or_failure × Apply_results.manager_operation_result ×
list Apply_results.packed_internal_manager_operation_result :=
match op with
|
Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.source := source;
Alpha_context.contents.Manager_operation.operation := operation;
Alpha_context.contents.Manager_operation.gas_limit := gas_limit;
Alpha_context.contents.Manager_operation.storage_limit := storage_limit
|} ⇒
let ctxt := Alpha_context.Gas.set_limit ctxt gas_limit in
let function_parameter :=
apply_external_manager_operation_content ctxt mode source chain_id
gas_consumed_in_precheck operation in
match function_parameter with
| Pervasives.Ok (ctxt, operation_results, internal_operations) ⇒
let function_parameter :=
apply_internal_manager_operations ctxt mode source chain_id
internal_operations in
match function_parameter with
| (Success ctxt, internal_operations_results) ⇒
let function_parameter :=
burn_storage_fees ctxt operation_results storage_limit source in
match function_parameter with
| Pervasives.Ok (ctxt, storage_limit, operation_results) ⇒
let function_parameter :=
List.fold_left_es
(fun (function_parameter :
Alpha_context.context × Z.t ×
list Apply_results.packed_internal_manager_operation_result)
⇒
let '(ctxt, storage_limit, res) := function_parameter in
fun (imopr :
Apply_results.packed_internal_manager_operation_result) ⇒
let
'Apply_results.Internal_manager_operation_result op mopr :=
imopr in
match mopr with
| Apply_results.Applied smopr ⇒
let? '(ctxt, storage_limit, smopr) :=
burn_storage_fees ctxt smopr storage_limit source in
let imopr :=
Apply_results.Internal_manager_operation_result op
(Apply_results.Applied smopr) in
return? (ctxt, storage_limit, (cons imopr res))
| _ ⇒ return? (ctxt, storage_limit, (cons imopr res))
end) (ctxt, storage_limit, nil) internal_operations_results in
match function_parameter with
| Pervasives.Ok (ctxt, _, internal_operations_results) ⇒
((Success ctxt), (Apply_results.Applied operation_results),
(List.rev internal_operations_results))
| Pervasives.Error errors ⇒
(Failure,
(Apply_results.Backtracked operation_results (Some errors)),
internal_operations_results)
end
| Pervasives.Error errors ⇒
(Failure, (Apply_results.Backtracked operation_results (Some errors)),
internal_operations_results)
end
| (Failure, internal_operations_results) ⇒
(Failure, (Apply_results.Applied operation_results),
internal_operations_results)
end
| Pervasives.Error errors ⇒
(Failure,
(Apply_results.Failed (Alpha_context.manager_kind operation) errors),
nil)
end
| _ ⇒ unreachable_gadt_branch
end.
Definition skipped_operation_result
(operation : Alpha_context.manager_operation)
: Apply_results.manager_operation_result :=
match operation with
| Alpha_context.Reveal _ ⇒
Apply_results.Applied
(Apply_results.Reveal_result
{|
Apply_results.successful_manager_operation_result.Reveal_result.consumed_gas
:= Alpha_context.Gas.Arith.zero; |})
| _ ⇒ Apply_results.Skipped (Alpha_context.manager_kind operation)
end.
Axiom mark_skipped :
Signature.public_key_hash → Alpha_context.Level.t →
Apply_results.prechecked_contents_list → Apply_results.contents_result_list.
Check that counters are consistent, i.e. that they are successive within a
batch. Fail with a {b permanent} error otherwise.
TODO: https://gitlab.com/tezos/tezos/-/issues/2301
Remove when format of operation is changed to save space.
Definition check_counters_consistency
(contents_list : Alpha_context.contents_list) : M? unit :=
let check_counter (previous_counter : option Z.t) (counter : Z.t) : M? unit :=
match previous_counter with
| None ⇒ Error_monad.return_unit
| Some previous_counter ⇒
let expected := Z.succ previous_counter in
if expected =Z counter then
Error_monad.return_unit
else
Error_monad.fail (Build_extensible "Inconsistent_counters" unit tt)
end in
let fix check_counters_rec
(previous_counter : option Alpha_context.counter)
(contents_list : Alpha_context.contents_list) : M? unit :=
match contents_list with
|
Alpha_context.Single
(Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.counter := counter |}) ⇒
check_counter previous_counter counter
|
Alpha_context.Cons
(Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.counter := counter |})
rest ⇒
let? '_ := check_counter previous_counter counter in
check_counters_rec (Some counter) rest
| _ ⇒ unreachable_gadt_branch
end in
check_counters_rec None contents_list.
(contents_list : Alpha_context.contents_list) : M? unit :=
let check_counter (previous_counter : option Z.t) (counter : Z.t) : M? unit :=
match previous_counter with
| None ⇒ Error_monad.return_unit
| Some previous_counter ⇒
let expected := Z.succ previous_counter in
if expected =Z counter then
Error_monad.return_unit
else
Error_monad.fail (Build_extensible "Inconsistent_counters" unit tt)
end in
let fix check_counters_rec
(previous_counter : option Alpha_context.counter)
(contents_list : Alpha_context.contents_list) : M? unit :=
match contents_list with
|
Alpha_context.Single
(Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.counter := counter |}) ⇒
check_counter previous_counter counter
|
Alpha_context.Cons
(Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.counter := counter |})
rest ⇒
let? '_ := check_counter previous_counter counter in
check_counters_rec (Some counter) rest
| _ ⇒ unreachable_gadt_branch
end in
check_counters_rec None contents_list.
Returns an updated context, and a list of prechecked contents containing
balance updates for fees related to each manager operation in
[contents_list].
Definition precheck_manager_contents_list
(ctxt : Alpha_context.context) (contents_list : Alpha_context.contents_list)
(mempool_mode : bool)
: M? (Alpha_context.context × Apply_results.prechecked_contents_list) :=
let fix rec_precheck_manager_contents_list
(ctxt : Alpha_context.context) (contents_list : Alpha_context.contents_list)
: M? (Alpha_context.context × Apply_results.prechecked_contents_list) :=
match contents_list with
| Alpha_context.Single contents ⇒
let? '(ctxt, result_value) :=
precheck_manager_contents ctxt contents mempool_mode in
return?
(ctxt,
(Apply_results.PrecheckedSingle
{| Apply_results.prechecked_contents.contents := contents;
Apply_results.prechecked_contents.result := result_value; |}))
| Alpha_context.Cons contents rest ⇒
let? '(ctxt, result_value) :=
precheck_manager_contents ctxt contents mempool_mode in
let? '(ctxt, results_rest) := rec_precheck_manager_contents_list ctxt rest
in
return?
(ctxt,
(Apply_results.PrecheckedCons
{| Apply_results.prechecked_contents.contents := contents;
Apply_results.prechecked_contents.result := result_value; |}
results_rest))
end in
let ctxt :=
if mempool_mode then
Alpha_context.Gas.reset_block_gas ctxt
else
ctxt in
let? '_ := check_counters_consistency contents_list in
rec_precheck_manager_contents_list ctxt contents_list.
Definition find_manager_public_key
(ctxt : Alpha_context.context) (op : Alpha_context.contents_list)
: M? Signature.public_key :=
let check_same_manager {A : Set}
(function_parameter : Signature.public_key_hash × option A)
: option (Signature.public_key_hash × option A) →
M? (Signature.public_key_hash × option A) :=
let '(source, source_key) := function_parameter in
fun (manager : option (Signature.public_key_hash × option A)) ⇒
match manager with
| None ⇒ return? (source, source_key)
| Some (manager, manager_key) ⇒
if
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) source
manager
then
return? (source, (Option.either manager_key source_key))
else
Error_monad.error_value
(Build_extensible "Inconsistent_sources" unit tt)
end in
let fix find_source
(contents_list : Alpha_context.contents_list)
(manager : option (Signature.public_key_hash × option Signature.public_key))
: M? (Signature.public_key_hash × option Signature.public_key) :=
let source (function_parameter : Alpha_context.contents)
: Signature.public_key_hash × option Signature.public_key :=
match function_parameter with
|
Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.source := source;
Alpha_context.contents.Manager_operation.operation :=
Alpha_context.Reveal key_value
|} ⇒ (source, (Some key_value))
|
Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.source := source |} ⇒
(source, None)
| _ ⇒ unreachable_gadt_branch
end in
match contents_list with
| Alpha_context.Single op ⇒ check_same_manager (source op) manager
| Alpha_context.Cons op rest ⇒
let? manager := check_same_manager (source op) manager in
find_source rest (Some manager)
end in
let? '(source, source_key) := find_source op None in
match source_key with
| Some key_value ⇒ return? key_value
| None ⇒ Alpha_context.Contract.get_manager_key None ctxt source
end.
Definition check_manager_signature
(ctxt : Alpha_context.context) (chain_id : Chain_id.t)
(op : Alpha_context.contents_list) (raw_operation : Alpha_context.operation)
: M? unit :=
let? public_key := find_manager_public_key ctxt op in
Alpha_context.Operation.check_signature public_key chain_id raw_operation.
Axiom apply_manager_contents_list_rec :
Alpha_context.context → Script_ir_translator.unparsing_mode →
Alpha_context.public_key_hash → Chain_id.t →
Apply_results.prechecked_contents_list →
success_or_failure × Apply_results.contents_result_list.
Axiom mark_backtracked :
Apply_results.contents_result_list → Apply_results.contents_result_list.
(ctxt : Alpha_context.context) (contents_list : Alpha_context.contents_list)
(mempool_mode : bool)
: M? (Alpha_context.context × Apply_results.prechecked_contents_list) :=
let fix rec_precheck_manager_contents_list
(ctxt : Alpha_context.context) (contents_list : Alpha_context.contents_list)
: M? (Alpha_context.context × Apply_results.prechecked_contents_list) :=
match contents_list with
| Alpha_context.Single contents ⇒
let? '(ctxt, result_value) :=
precheck_manager_contents ctxt contents mempool_mode in
return?
(ctxt,
(Apply_results.PrecheckedSingle
{| Apply_results.prechecked_contents.contents := contents;
Apply_results.prechecked_contents.result := result_value; |}))
| Alpha_context.Cons contents rest ⇒
let? '(ctxt, result_value) :=
precheck_manager_contents ctxt contents mempool_mode in
let? '(ctxt, results_rest) := rec_precheck_manager_contents_list ctxt rest
in
return?
(ctxt,
(Apply_results.PrecheckedCons
{| Apply_results.prechecked_contents.contents := contents;
Apply_results.prechecked_contents.result := result_value; |}
results_rest))
end in
let ctxt :=
if mempool_mode then
Alpha_context.Gas.reset_block_gas ctxt
else
ctxt in
let? '_ := check_counters_consistency contents_list in
rec_precheck_manager_contents_list ctxt contents_list.
Definition find_manager_public_key
(ctxt : Alpha_context.context) (op : Alpha_context.contents_list)
: M? Signature.public_key :=
let check_same_manager {A : Set}
(function_parameter : Signature.public_key_hash × option A)
: option (Signature.public_key_hash × option A) →
M? (Signature.public_key_hash × option A) :=
let '(source, source_key) := function_parameter in
fun (manager : option (Signature.public_key_hash × option A)) ⇒
match manager with
| None ⇒ return? (source, source_key)
| Some (manager, manager_key) ⇒
if
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) source
manager
then
return? (source, (Option.either manager_key source_key))
else
Error_monad.error_value
(Build_extensible "Inconsistent_sources" unit tt)
end in
let fix find_source
(contents_list : Alpha_context.contents_list)
(manager : option (Signature.public_key_hash × option Signature.public_key))
: M? (Signature.public_key_hash × option Signature.public_key) :=
let source (function_parameter : Alpha_context.contents)
: Signature.public_key_hash × option Signature.public_key :=
match function_parameter with
|
Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.source := source;
Alpha_context.contents.Manager_operation.operation :=
Alpha_context.Reveal key_value
|} ⇒ (source, (Some key_value))
|
Alpha_context.Manager_operation {|
Alpha_context.contents.Manager_operation.source := source |} ⇒
(source, None)
| _ ⇒ unreachable_gadt_branch
end in
match contents_list with
| Alpha_context.Single op ⇒ check_same_manager (source op) manager
| Alpha_context.Cons op rest ⇒
let? manager := check_same_manager (source op) manager in
find_source rest (Some manager)
end in
let? '(source, source_key) := find_source op None in
match source_key with
| Some key_value ⇒ return? key_value
| None ⇒ Alpha_context.Contract.get_manager_key None ctxt source
end.
Definition check_manager_signature
(ctxt : Alpha_context.context) (chain_id : Chain_id.t)
(op : Alpha_context.contents_list) (raw_operation : Alpha_context.operation)
: M? unit :=
let? public_key := find_manager_public_key ctxt op in
Alpha_context.Operation.check_signature public_key chain_id raw_operation.
Axiom apply_manager_contents_list_rec :
Alpha_context.context → Script_ir_translator.unparsing_mode →
Alpha_context.public_key_hash → Chain_id.t →
Apply_results.prechecked_contents_list →
success_or_failure × Apply_results.contents_result_list.
Axiom mark_backtracked :
Apply_results.contents_result_list → Apply_results.contents_result_list.
Records for the constructor parameters
Module ConstructorRecords_apply_mode.
Module apply_mode.
Module Application.
Record record {predecessor_block payload_hash locked_round
predecessor_level predecessor_round round : Set} : Set := Build {
predecessor_block : predecessor_block;
payload_hash : payload_hash;
locked_round : locked_round;
predecessor_level : predecessor_level;
predecessor_round : predecessor_round;
round : round;
}.
Arguments record : clear implicits.
Definition with_predecessor_block
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} predecessor_block
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round predecessor_block
r.(payload_hash) r.(locked_round) r.(predecessor_level)
r.(predecessor_round) r.(round).
Definition with_payload_hash
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} payload_hash
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
payload_hash r.(locked_round) r.(predecessor_level)
r.(predecessor_round) r.(round).
Definition with_locked_round
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} locked_round
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
r.(payload_hash) locked_round r.(predecessor_level)
r.(predecessor_round) r.(round).
Definition with_predecessor_level
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} predecessor_level
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
r.(payload_hash) r.(locked_round) predecessor_level
r.(predecessor_round) r.(round).
Definition with_predecessor_round
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} predecessor_round
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
r.(payload_hash) r.(locked_round) r.(predecessor_level)
predecessor_round r.(round).
Definition with_round
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} round
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
r.(payload_hash) r.(locked_round) r.(predecessor_level)
r.(predecessor_round) round.
End Application.
Definition Application_skeleton := Application.record.
Module Full_construction.
Record record {predecessor_block payload_hash predecessor_level
predecessor_round round : Set} : Set := Build {
predecessor_block : predecessor_block;
payload_hash : payload_hash;
predecessor_level : predecessor_level;
predecessor_round : predecessor_round;
round : round;
}.
Arguments record : clear implicits.
Definition with_predecessor_block
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} predecessor_block
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round predecessor_block r.(payload_hash)
r.(predecessor_level) r.(predecessor_round) r.(round).
Definition with_payload_hash
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} payload_hash
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round r.(predecessor_block) payload_hash
r.(predecessor_level) r.(predecessor_round) r.(round).
Definition with_predecessor_level
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} predecessor_level
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
predecessor_level r.(predecessor_round) r.(round).
Definition with_predecessor_round
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} predecessor_round
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
r.(predecessor_level) predecessor_round r.(round).
Definition with_round
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} round
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
r.(predecessor_level) r.(predecessor_round) round.
End Full_construction.
Definition Full_construction_skeleton := Full_construction.record.
Module Partial_construction.
Record record {predecessor_level predecessor_round grand_parent_round :
Set} : Set := Build {
predecessor_level : predecessor_level;
predecessor_round : predecessor_round;
grand_parent_round : grand_parent_round;
}.
Arguments record : clear implicits.
Definition with_predecessor_level
{t_predecessor_level t_predecessor_round t_grand_parent_round}
predecessor_level
(r :
record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
Build t_predecessor_level t_predecessor_round t_grand_parent_round
predecessor_level r.(predecessor_round) r.(grand_parent_round).
Definition with_predecessor_round
{t_predecessor_level t_predecessor_round t_grand_parent_round}
predecessor_round
(r :
record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
Build t_predecessor_level t_predecessor_round t_grand_parent_round
r.(predecessor_level) predecessor_round r.(grand_parent_round).
Definition with_grand_parent_round
{t_predecessor_level t_predecessor_round t_grand_parent_round}
grand_parent_round
(r :
record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
Build t_predecessor_level t_predecessor_round t_grand_parent_round
r.(predecessor_level) r.(predecessor_round) grand_parent_round.
End Partial_construction.
Definition Partial_construction_skeleton := Partial_construction.record.
End apply_mode.
End ConstructorRecords_apply_mode.
Import ConstructorRecords_apply_mode.
Reserved Notation "'apply_mode.Application".
Reserved Notation "'apply_mode.Full_construction".
Reserved Notation "'apply_mode.Partial_construction".
Inductive apply_mode : Set :=
| Application : 'apply_mode.Application → apply_mode
| Full_construction : 'apply_mode.Full_construction → apply_mode
| Partial_construction : 'apply_mode.Partial_construction → apply_mode
where "'apply_mode.Application" :=
(apply_mode.Application_skeleton Block_hash.t Block_payload_hash.t
(option Alpha_context.Round.t) Alpha_context.Level.t Alpha_context.Round.t
Alpha_context.Round.t)
and "'apply_mode.Full_construction" :=
(apply_mode.Full_construction_skeleton Block_hash.t Block_payload_hash.t
Alpha_context.Level.t Alpha_context.Round.t Alpha_context.Round.t)
and "'apply_mode.Partial_construction" :=
(apply_mode.Partial_construction_skeleton Alpha_context.Level.t
Alpha_context.Round.t Alpha_context.Round.t).
Module apply_mode.
Include ConstructorRecords_apply_mode.apply_mode.
Definition Application := 'apply_mode.Application.
Definition Full_construction := 'apply_mode.Full_construction.
Definition Partial_construction := 'apply_mode.Partial_construction.
End apply_mode.
Definition get_predecessor_level (function_parameter : apply_mode)
: Alpha_context.Level.t :=
match function_parameter with
|
(Application {|
apply_mode.Application.predecessor_level := predecessor_level |} |
Full_construction {|
apply_mode.Full_construction.predecessor_level := predecessor_level |}
|
Partial_construction {|
apply_mode.Partial_construction.predecessor_level := predecessor_level
|}) ⇒ predecessor_level
end.
Definition record_operation
(ctxt : Alpha_context.context) (operation : Alpha_context.operation)
: Alpha_context.context :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement _) ⇒ ctxt
| Alpha_context.Single (Alpha_context.Endorsement _) ⇒ ctxt
|
(Alpha_context.Single
(Alpha_context.Failing_noop _ | Alpha_context.Proposals _ |
Module apply_mode.
Module Application.
Record record {predecessor_block payload_hash locked_round
predecessor_level predecessor_round round : Set} : Set := Build {
predecessor_block : predecessor_block;
payload_hash : payload_hash;
locked_round : locked_round;
predecessor_level : predecessor_level;
predecessor_round : predecessor_round;
round : round;
}.
Arguments record : clear implicits.
Definition with_predecessor_block
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} predecessor_block
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round predecessor_block
r.(payload_hash) r.(locked_round) r.(predecessor_level)
r.(predecessor_round) r.(round).
Definition with_payload_hash
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} payload_hash
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
payload_hash r.(locked_round) r.(predecessor_level)
r.(predecessor_round) r.(round).
Definition with_locked_round
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} locked_round
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
r.(payload_hash) locked_round r.(predecessor_level)
r.(predecessor_round) r.(round).
Definition with_predecessor_level
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} predecessor_level
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
r.(payload_hash) r.(locked_round) predecessor_level
r.(predecessor_round) r.(round).
Definition with_predecessor_round
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} predecessor_round
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
r.(payload_hash) r.(locked_round) r.(predecessor_level)
predecessor_round r.(round).
Definition with_round
{t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
t_predecessor_round t_round} round
(r :
record t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_locked_round
t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
r.(payload_hash) r.(locked_round) r.(predecessor_level)
r.(predecessor_round) round.
End Application.
Definition Application_skeleton := Application.record.
Module Full_construction.
Record record {predecessor_block payload_hash predecessor_level
predecessor_round round : Set} : Set := Build {
predecessor_block : predecessor_block;
payload_hash : payload_hash;
predecessor_level : predecessor_level;
predecessor_round : predecessor_round;
round : round;
}.
Arguments record : clear implicits.
Definition with_predecessor_block
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} predecessor_block
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round predecessor_block r.(payload_hash)
r.(predecessor_level) r.(predecessor_round) r.(round).
Definition with_payload_hash
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} payload_hash
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round r.(predecessor_block) payload_hash
r.(predecessor_level) r.(predecessor_round) r.(round).
Definition with_predecessor_level
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} predecessor_level
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
predecessor_level r.(predecessor_round) r.(round).
Definition with_predecessor_round
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} predecessor_round
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
r.(predecessor_level) predecessor_round r.(round).
Definition with_round
{t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round} round
(r :
record t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round) :=
Build t_predecessor_block t_payload_hash t_predecessor_level
t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
r.(predecessor_level) r.(predecessor_round) round.
End Full_construction.
Definition Full_construction_skeleton := Full_construction.record.
Module Partial_construction.
Record record {predecessor_level predecessor_round grand_parent_round :
Set} : Set := Build {
predecessor_level : predecessor_level;
predecessor_round : predecessor_round;
grand_parent_round : grand_parent_round;
}.
Arguments record : clear implicits.
Definition with_predecessor_level
{t_predecessor_level t_predecessor_round t_grand_parent_round}
predecessor_level
(r :
record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
Build t_predecessor_level t_predecessor_round t_grand_parent_round
predecessor_level r.(predecessor_round) r.(grand_parent_round).
Definition with_predecessor_round
{t_predecessor_level t_predecessor_round t_grand_parent_round}
predecessor_round
(r :
record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
Build t_predecessor_level t_predecessor_round t_grand_parent_round
r.(predecessor_level) predecessor_round r.(grand_parent_round).
Definition with_grand_parent_round
{t_predecessor_level t_predecessor_round t_grand_parent_round}
grand_parent_round
(r :
record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
Build t_predecessor_level t_predecessor_round t_grand_parent_round
r.(predecessor_level) r.(predecessor_round) grand_parent_round.
End Partial_construction.
Definition Partial_construction_skeleton := Partial_construction.record.
End apply_mode.
End ConstructorRecords_apply_mode.
Import ConstructorRecords_apply_mode.
Reserved Notation "'apply_mode.Application".
Reserved Notation "'apply_mode.Full_construction".
Reserved Notation "'apply_mode.Partial_construction".
Inductive apply_mode : Set :=
| Application : 'apply_mode.Application → apply_mode
| Full_construction : 'apply_mode.Full_construction → apply_mode
| Partial_construction : 'apply_mode.Partial_construction → apply_mode
where "'apply_mode.Application" :=
(apply_mode.Application_skeleton Block_hash.t Block_payload_hash.t
(option Alpha_context.Round.t) Alpha_context.Level.t Alpha_context.Round.t
Alpha_context.Round.t)
and "'apply_mode.Full_construction" :=
(apply_mode.Full_construction_skeleton Block_hash.t Block_payload_hash.t
Alpha_context.Level.t Alpha_context.Round.t Alpha_context.Round.t)
and "'apply_mode.Partial_construction" :=
(apply_mode.Partial_construction_skeleton Alpha_context.Level.t
Alpha_context.Round.t Alpha_context.Round.t).
Module apply_mode.
Include ConstructorRecords_apply_mode.apply_mode.
Definition Application := 'apply_mode.Application.
Definition Full_construction := 'apply_mode.Full_construction.
Definition Partial_construction := 'apply_mode.Partial_construction.
End apply_mode.
Definition get_predecessor_level (function_parameter : apply_mode)
: Alpha_context.Level.t :=
match function_parameter with
|
(Application {|
apply_mode.Application.predecessor_level := predecessor_level |} |
Full_construction {|
apply_mode.Full_construction.predecessor_level := predecessor_level |}
|
Partial_construction {|
apply_mode.Partial_construction.predecessor_level := predecessor_level
|}) ⇒ predecessor_level
end.
Definition record_operation
(ctxt : Alpha_context.context) (operation : Alpha_context.operation)
: Alpha_context.context :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement _) ⇒ ctxt
| Alpha_context.Single (Alpha_context.Endorsement _) ⇒ ctxt
|
(Alpha_context.Single
(Alpha_context.Failing_noop _ | Alpha_context.Proposals _ |