๐ย Updater.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V6.Updater.
Require TezosOfOCaml.Environment.Structs.V7.RPC_directory.
Module validation_result := Updater.validation_result.
Definition validation_result := Updater.validation_result.
Module quota := Updater.quota.
Definition quota := Updater.quota.
Module rpc_context := Updater.rpc_context.
Definition rpc_context := Updater.rpc_context.
Module PROTOCOL.
Record signature
{block_header_data block_header block_header_metadata operation_data
operation_receipt operation mode validation_state application_state
Mempool_t Mempool_validation_info Mempool_keep_or_replace
Mempool_operation_conflict Mempool_add_result Mempool_add_error
Mempool_merge_error : Set} : Set := {
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V6.Updater.
Require TezosOfOCaml.Environment.Structs.V7.RPC_directory.
Module validation_result := Updater.validation_result.
Definition validation_result := Updater.validation_result.
Module quota := Updater.quota.
Definition quota := Updater.quota.
Module rpc_context := Updater.rpc_context.
Definition rpc_context := Updater.rpc_context.
Module PROTOCOL.
Record signature
{block_header_data block_header block_header_metadata operation_data
operation_receipt operation mode validation_state application_state
Mempool_t Mempool_validation_info Mempool_keep_or_replace
Mempool_operation_conflict Mempool_add_result Mempool_add_error
Mempool_merge_error : Set} : Set := {
The maximum size of a block header in bytes.
The maximum size of an {!operation} in bytes. This value is bigger than the size
of the bytes required for {!operation_data}, because this value accounts
for the shell header.
Operations quota for each validation pass. The length of the
list denotes the number of validation passes.
The economic protocol-specific type of blocks.
Encoding for economic protocol-specific part of block headers.
A fully parsed block header.
Economic protocol-specific side information computed by the
protocol during the validation of a block. Should not include
information about the evaluation of operations which is handled
separately by {!operation_metadata}. To be used as an execution
trace by tools (client, indexer). Not necessary for
validation.
Encoding for economic protocol-specific block metadata.
The economic protocol-specific type of operations.
Economic protocol-specific side information computed by the
protocol during the validation of each operation, to be used
conjointly with {!block_header_metadata}.
A fully parsed operation.
Encoding for economoic protocol-specific operation data.
Encoding for eonomic protocol-specific operation receipts.
Encoding that mixes an operation data and its receipt.
[acceptable_pass op] gives the validation pass in which the
input operation [op] can appear. For instance, it results in
[Some 0] if [op] only belongs to the first pass. When [op] is
ill-formed, [acceptable_pass op] returns [None].
[compare_operations (oph1,op1) (oph2,op2)] defines a total
ordering relation on valid operations.
The following requirements must be satisfied: [oph1] is the
[Operation.hash.p1], [oph2] is [Operation.hash op2] and that
[op1] and [op2] are valid in the same context.
[compare_operations (oph1,op1) (oph2,op2) = 0] happens only if
[Operation_hash.compare oph1 oph2 = 0], meaning [op1 = op2] only
when [op1] and [op2] are structurally identical.
Two operations of different validation_passes are compared in the
reverse order of their [validation_pass]: the one with the
smaller [validation_pass] is compared as being the greater.
When belonging to the same validation_pass, two operations
comparison depends on their static parameters. An abstract weight
is computed for each operation based on its static parameters.
When two operations' weights are compared as equal,
[compare_operation (oph1,op1) (oph2,op2)] is
[Operation_hash.compare oph1 oph2].
[compare_operations] can be used as a [compare] component of an
{!Stdlib.Map.OrderedType}, or any such collection which relies on
a total comparison function.
The mode indicates the circumstances in which a block and/or
operations are validated or applied, and contains specific
information. It must be provided as an argument to
[begin_validation] and [begin_application].
A functional state that is transmitted throughout the validation
of a block (or during the lifetime of a mempool or RPC). It is
created by [begin_validation] below, updated by
[validate_operation], and required by [finalize_validation].
This state is immutable thus validator or baker implementations
are allowed to pause, replay or backtrack throughout validation
steps.
Similar to {!validation_state}, but for the application process.
[begin_validation predecessor_context chain_id mode
~predecessor] initializes the {!validation_state} for the
validation process of an existing or new block.
[predecessor_context] and [predecessor] are the resulting
context and shell header of the predecessor block. Exceptionally
in {!Partial_validation} mode, they may instead come from any
ancestor block that is more recent (i.e. has a greater level)
than the current head's "last_allowed_fork_level".
[mode] specifies the circumstances of validation and also
carries additional information: see {!mode}.
Note that for protocol versions <= K where [begin_validation]
does not exist yet, this calls the old [begin_application] by
necessity. However, in [Application] mode, this calls the old
[begin_application] in [Partial_validation] mode in order to run
more quickly. This preserves the behavior of [precheck] in
[lib_validation/block_validation.ml] for old protocols. It does
mean that the application of a validated block may fail in these
protocols.
begin_validation :
Context.t โ Chain_id.t โ mode โ Block_header.shell_header โ
Error_monad.tzresult validation_state;
Context.t โ Chain_id.t โ mode โ Block_header.shell_header โ
Error_monad.tzresult validation_state;
Validate an operation. If successful, return the updated
{!validation_state}.
[check_signature] indicates whether the signature should be
checked. It defaults to [true] because the signature needs to be
correct for the operation to be valid. This argument exists for
special cases where it is acceptable to bypass this check,
e.g. if we know that the operation has already been successfully
validated in another context.
validate_operation :
option bool โ validation_state โ Operation_hash.t โ operation โ
Error_monad.tzresult validation_state;
option bool โ validation_state โ Operation_hash.t โ operation โ
Error_monad.tzresult validation_state;
Run final and global checks on the block that must come after
the validation of all its operations to establish its
validity.
Initialize the {!application_state} for the application process
of an existing or new block. See {!begin_validation} for details
on the arguments.
In protocol versions > K, calling this function with the
{!Partial_validation} mode returns an error.
begin_application :
Context.t โ Chain_id.t โ mode โ Block_header.shell_header โ
Error_monad.tzresult application_state;
Context.t โ Chain_id.t โ mode โ Block_header.shell_header โ
Error_monad.tzresult application_state;
Apply an operation. If successful, return the updated
{!application_state} and the corresponding {!operation_receipt}.
This should be called for all operations in a block, after
{!begin_application} and before
{!finalize_application}. Moreover, the operation should have
already been validated by {!validate_operation}.
apply_operation :
application_state โ Operation_hash.t โ operation โ
Error_monad.tzresult (application_state ร operation_receipt);
application_state โ Operation_hash.t โ operation โ
Error_monad.tzresult (application_state ร operation_receipt);
Finalize the context resulting from the application of the
contents of the block.
If there is no protocol migration, i.e. if the block being
applied is not the last block of the current economic protocol,
then the resulting context can be used in the future as input for
the validation and application of its successor blocks.
In {!Construction} mode, the [Block_header.shell_header option]
argument must contain a value, which will be used to compute the
[cache_nonce]. In other modes, it can as well be [None] since it
will not be used.
finalize_application :
application_state โ option Block_header.shell_header โ
Error_monad.tzresult (validation_result ร block_header_metadata);
application_state โ option Block_header.shell_header โ
Error_monad.tzresult (validation_result ร block_header_metadata);
[rpc_services] provides the list of remote procedures exported
by this protocol implementation.
[init chain_id ctxt hd] initializes the context, or upgrades the
context after a protocol amendment. This function receives as
arguments the [chain_id] of the current chain and the context
[ctxt] resulting from the application of the block that triggered
the amendment, as well as its header [hd]. This function should
fail if the "protocol stitching", i.e., the transition from a
valid previous protocol to the one being activated, has not been
implemented.
init_value :
Chain_id.t โ Context.t โ Block_header.shell_header โ
Error_monad.tzresult validation_result;
Chain_id.t โ Context.t โ Block_header.shell_header โ
Error_monad.tzresult validation_result;
[value_of_key chain_id predecessor_context
predecessor_timestamp predecessor_level predecessor_fitness
predecessor timestamp] returns a function to build one value of
the cache from its key.
This function is used to restore all or part of the cache, for
instance when booting a validator to preheat the cache, or when a
reorganization happens. This function should never fail, returned
errors are fatal.
The generated function is passed to [Context.Cache.load_caches]
which will use it either immediately a cache-loading time or
on-demand, when a given cached value is accessed.
value_of_key :
Chain_id.t โ Context.t โ Time.t โ Int32.t โ Fitness.t โ
Block_hash.t โ Time.t โ
Error_monad.tzresult
(Context.cache_key โ Error_monad.tzresult Context.cache_value);
Chain_id.t โ Context.t โ Time.t โ Int32.t โ Fitness.t โ
Block_hash.t โ Time.t โ
Error_monad.tzresult
(Context.cache_key โ Error_monad.tzresult Context.cache_value);
Mempool type. This immutable functional state keeps track of
operations added to the mempool, and allows to detect conflicts
between them and a new candidate operation.
Validation info type required to validate and add operations to a
mempool.
Mempool_validation_info := Mempool_validation_info;
Mempool_keep_or_replace := Mempool_keep_or_replace;
Mempool_keep_or_replace := Mempool_keep_or_replace;
Type of the function that may be provided in order to resolve a
potential conflict when adding an operation to an existing mempool
or when merging two mempools. This handler may be defined as a
simple order relation over operations (e.g. prioritize the most
profitable operations) or an arbitrary one (e.g. prioritize
operations where the source is a specific manager).
Returning [`Keep] will leave the mempool unchanged and retain the
[existing_operation] while returning [`Replace] will remove
[existing_operation] and add [new_operation] instead.
Mempool_conflict_handler :=
Operation_hash.t ร operation โ Operation_hash.t ร operation โ
Mempool_keep_or_replace;
Mempool_operation_conflict := Mempool_operation_conflict;
Operation_hash.t ร operation โ Operation_hash.t ร operation โ
Mempool_keep_or_replace;
Mempool_operation_conflict := Mempool_operation_conflict;
Return type when adding an operation to the mempool
Error type returned when adding an operation to the mempool fails.
Error type returned when the merge of two mempools fails.
Initialize a static [validation_info] and [mempool], required
to validate and add operations, and an incremental and
serializable {!mempool}.
Mempool_init :
Context.t โ Chain_id.t โ Block_hash.t โ Block_header.shell_header โ
Error_monad.tzresult (Mempool_validation_info ร Mempool_t);
Context.t โ Chain_id.t โ Block_hash.t โ Block_header.shell_header โ
Error_monad.tzresult (Mempool_validation_info ร Mempool_t);
Mempool encoding
Adds an operation to a [mempool] if and only if it is valid and
does not conflict with previously added operation.
This function checks the validity of an operation and tries to
add it to the mempool.
If a validation error is triggered, the result will be a
[Validation_error]. If a conflict with a previous operation
exists, the result will be [Add_conflict] is then checked.
Important: no [Add_conflict] will be raised if a
[conflict_handler] is provided (see [add_result]).
If no error is raised the operation is potentially added to the
[mempool] depending on the [add_result] value.
Mempool_add_operation :
option bool โ option Mempool_conflict_handler โ
Mempool_validation_info โ Mempool_t โ Operation_hash.t ร operation โ
Pervasives.result (Mempool_t ร Mempool_add_result) Mempool_add_error;
option bool โ option Mempool_conflict_handler โ
Mempool_validation_info โ Mempool_t โ Operation_hash.t ร operation โ
Pervasives.result (Mempool_t ร Mempool_add_result) Mempool_add_error;
[remove_operation mempool oph] removes the operation [oph] from
the [mempool]. The [mempool] remains unchanged when [oph] is not
present in the [mempool]
[merge ?conflict_handler mempool mempool'] merges [mempool']
{b into} [mempool].
Mempools may only be merged if they are compatible: i.e. both have
been initialised with the same predecessor block. Otherwise, the
[Incompatible_mempool] error is returned.
Conflicts between operations from the two mempools can
occur. Similarly as [add_operation], a [Merge_conflict] error
may be raised when no [conflict_handler] is provided.
[existing_operation] in [conflict_handler ~existing_operation ~new_operation]
references operations present in [mempool] while
[new_operation] will reference operations present in
[mempool'].
Mempool_merge :
option Mempool_conflict_handler โ Mempool_t โ Mempool_t โ
Pervasives.result Mempool_t Mempool_merge_error;
option Mempool_conflict_handler โ Mempool_t โ Mempool_t โ
Pervasives.result Mempool_t Mempool_merge_error;
[operations mempool] returns the map of operations present in
[mempool].
Mempool_operations :
Mempool_t โ Operation_hash.Map.(S.INDEXES_MAP.t) operation;
}.
End PROTOCOL.
Definition PROTOCOL := @PROTOCOL.signature.
Arguments PROTOCOL {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.
Parameter activate : Context.t โ Protocol_hash.t โ Context.t.
Mempool_t โ Operation_hash.Map.(S.INDEXES_MAP.t) operation;
}.
End PROTOCOL.
Definition PROTOCOL := @PROTOCOL.signature.
Arguments PROTOCOL {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.
Parameter activate : Context.t โ Protocol_hash.t โ Context.t.