🍃 Updater.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Block_hash.
Require TezosOfOCaml.Environment.Structs.V0.Block_header.
Require TezosOfOCaml.Environment.Structs.V0.Chain_id.
Require TezosOfOCaml.Environment.Structs.V0.Context.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.Fitness.
Require TezosOfOCaml.Environment.Structs.V0.Int32.
Require TezosOfOCaml.Environment.Structs.V0.Protocol_hash.
Require TezosOfOCaml.Environment.Structs.V0.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.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Block_hash.
Require TezosOfOCaml.Environment.Structs.V0.Block_header.
Require TezosOfOCaml.Environment.Structs.V0.Chain_id.
Require TezosOfOCaml.Environment.Structs.V0.Context.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.Fitness.
Require TezosOfOCaml.Environment.Structs.V0.Int32.
Require TezosOfOCaml.Environment.Structs.V0.Protocol_hash.
Require TezosOfOCaml.Environment.Structs.V0.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.