Skip to main content

🍃 Updater.v

Environment

Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Block_hash.
Require Proto_alpha.Environment.Block_header.
Require Proto_alpha.Environment.Chain_id.
Require Proto_alpha.Environment.Context.
Require Proto_alpha.Environment.Error_monad.
Require Proto_alpha.Environment.Fitness.
Require Proto_alpha.Environment.Int32.
Require Proto_alpha.Environment.Protocol_hash.
Require Proto_alpha.Environment.RPC_directory.

Module validation_result.
  Record record : Set := Build {
    context : Context.t;
    fitness : Fitness.t;
    message : option string;
    max_operations_ttl : int;
    last_allowed_fork_level : Int32.t }.
  Definition with_context context (r : record) :=
    Build context r.(fitness) r.(message) r.(max_operations_ttl)
      r.(last_allowed_fork_level).
  Definition with_fitness fitness (r : record) :=
    Build r.(context) fitness r.(message) r.(max_operations_ttl)
      r.(last_allowed_fork_level).
  Definition with_message message (r : record) :=
    Build r.(context) r.(fitness) message r.(max_operations_ttl)
      r.(last_allowed_fork_level).
  Definition with_max_operations_ttl max_operations_ttl (r : record) :=
    Build r.(context) r.(fitness) r.(message) max_operations_ttl
      r.(last_allowed_fork_level).
  Definition with_last_allowed_fork_level last_allowed_fork_level
    (r : record) :=
    Build r.(context) r.(fitness) r.(message) r.(max_operations_ttl)
      last_allowed_fork_level.
End validation_result.
Definition validation_result := validation_result.record.

Module quota.
  Record record : Set := Build {
    max_size : int;
    max_op : option int }.
  Definition with_max_size max_size (r : record) :=
    Build max_size r.(max_op).
  Definition with_max_op max_op (r : record) :=
    Build r.(max_size) max_op.
End quota.
Definition quota := quota.record.

Module rpc_context.
  Record record : Set := Build {
    block_hash : Block_hash.t;
    block_header : Block_header.shell_header;
    context : Context.t }.
  Definition with_block_hash block_hash (r : record) :=
    Build block_hash r.(block_header) r.(context).
  Definition with_block_header block_header (r : record) :=
    Build r.(block_hash) block_header r.(context).
  Definition with_context context (r : record) :=
    Build r.(block_hash) r.(block_header) context.
End rpc_context.
Definition rpc_context := rpc_context.record.

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 :
      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 {_ _ _ _ _ _ _}.

Parameter activate : Context.t Protocol_hash.t Context.t.