๐ย Updater.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Updater.
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 validation_state : Set} : Set := {
max_block_length : int;
max_operation_data_length : int;
validation_passes : list quota;
block_header_data := block_header_data;
block_header_data_encoding : Data_encoding.t block_header_data;
block_header := block_header;
block_header_metadata := block_header_metadata;
block_header_metadata_encoding : Data_encoding.t block_header_metadata;
operation_data := operation_data;
operation_receipt := operation_receipt;
operation := operation;
operation_data_encoding : Data_encoding.t operation_data;
operation_receipt_encoding : Data_encoding.t operation_receipt;
operation_data_and_receipt_encoding :
Data_encoding.t (operation_data ร operation_receipt);
acceptable_passes : operation โ list int;
relative_position_within_block : operation โ operation โ int;
validation_state := validation_state;
begin_partial_application :
Chain_id.t โ Context.t โ Time.t โ Fitness.t โ block_header โ
Error_monad.tzresult validation_state;
begin_application :
Chain_id.t โ Context.t โ Time.t โ Fitness.t โ block_header โ
Error_monad.tzresult validation_state;
begin_construction :
Chain_id.t โ Context.t โ Time.t โ Int32.t โ Fitness.t โ
Block_hash.t โ Time.t โ option block_header_data โ unit โ
Error_monad.tzresult validation_state;
apply_operation :
validation_state โ operation โ
Error_monad.tzresult (validation_state ร operation_receipt);
finalize_block :
validation_state โ option Block_header.shell_header โ
Error_monad.tzresult (validation_result ร block_header_metadata);
rpc_services : RPC_directory.t rpc_context;
init_value :
Chain_id.t โ Context.t โ Block_header.shell_header โ
Error_monad.tzresult validation_result;
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);
}.
End PROTOCOL.
Definition PROTOCOL := @PROTOCOL.signature.
Arguments PROTOCOL {_ _ _ _ _ _ _}.
Definition activate := Updater.activate.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Updater.
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 validation_state : Set} : Set := {
max_block_length : int;
max_operation_data_length : int;
validation_passes : list quota;
block_header_data := block_header_data;
block_header_data_encoding : Data_encoding.t block_header_data;
block_header := block_header;
block_header_metadata := block_header_metadata;
block_header_metadata_encoding : Data_encoding.t block_header_metadata;
operation_data := operation_data;
operation_receipt := operation_receipt;
operation := operation;
operation_data_encoding : Data_encoding.t operation_data;
operation_receipt_encoding : Data_encoding.t operation_receipt;
operation_data_and_receipt_encoding :
Data_encoding.t (operation_data ร operation_receipt);
acceptable_passes : operation โ list int;
relative_position_within_block : operation โ operation โ int;
validation_state := validation_state;
begin_partial_application :
Chain_id.t โ Context.t โ Time.t โ Fitness.t โ block_header โ
Error_monad.tzresult validation_state;
begin_application :
Chain_id.t โ Context.t โ Time.t โ Fitness.t โ block_header โ
Error_monad.tzresult validation_state;
begin_construction :
Chain_id.t โ Context.t โ Time.t โ Int32.t โ Fitness.t โ
Block_hash.t โ Time.t โ option block_header_data โ unit โ
Error_monad.tzresult validation_state;
apply_operation :
validation_state โ operation โ
Error_monad.tzresult (validation_state ร operation_receipt);
finalize_block :
validation_state โ option Block_header.shell_header โ
Error_monad.tzresult (validation_result ร block_header_metadata);
rpc_services : RPC_directory.t rpc_context;
init_value :
Chain_id.t โ Context.t โ Block_header.shell_header โ
Error_monad.tzresult validation_result;
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);
}.
End PROTOCOL.
Definition PROTOCOL := @PROTOCOL.signature.
Arguments PROTOCOL {_ _ _ _ _ _ _}.
Definition activate := Updater.activate.