🍃 Updater.v

Environment

Gitlab

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.