🧑 Main.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Alpha_services.
Require TezosOfOCaml.Proto_alpha.Apply.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Baking.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Dal_apply.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Mempool_validation.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Require TezosOfOCaml.Proto_alpha.Validate.
Require TezosOfOCaml.Proto_alpha.Validate_errors.
Definition block_header_data : Set := Alpha_context.Block_header.protocol_data.
Definition block_header : Set := Alpha_context.Block_header.t.
Definition block_header_data_encoding
: Data_encoding.encoding Alpha_context.Block_header.protocol_data :=
Alpha_context.Block_header.protocol_data_encoding.
Definition block_header_metadata : Set := Apply_results.block_metadata.
Definition block_header_metadata_encoding
: Data_encoding.encoding Apply_results.block_metadata :=
Apply_results.block_metadata_encoding.
Definition operation_data : Set := Alpha_context.packed_protocol_data.
Definition operation_data_encoding
: Data_encoding.t Alpha_context.Operation.packed_protocol_data :=
Alpha_context.Operation.protocol_data_encoding.
Definition operation_receipt : Set := Apply_results.packed_operation_metadata.
Definition operation_receipt_encoding
: Data_encoding.t Apply_results.packed_operation_metadata :=
Apply_results.operation_metadata_encoding.
Definition operation_data_and_receipt_encoding
: Data_encoding.t
(Alpha_context.Operation.packed_protocol_data ×
Apply_results.packed_operation_metadata) :=
Apply_results.operation_data_and_metadata_encoding.
Definition operation : Set := Alpha_context.packed_operation.
Definition acceptable_pass : Alpha_context.packed_operation → option int :=
Alpha_context.Operation.acceptable_pass.
Definition max_block_length : int :=
Alpha_context.Block_header.max_header_length.
Definition max_operation_data_length : int :=
Alpha_context.Constants.max_operation_data_length.
Definition validation_passes : list Updater.quota :=
[
{| Updater.quota.max_size := 2048 ×i 2048;
Updater.quota.max_op := Some 2048; |};
{| Updater.quota.max_size := 32 ×i 1024; Updater.quota.max_op := None; |};
{|
Updater.quota.max_size :=
Alpha_context.Constants.max_anon_ops_per_block ×i 1024;
Updater.quota.max_op :=
Some Alpha_context.Constants.max_anon_ops_per_block; |};
{| Updater.quota.max_size := 512 ×i 1024; Updater.quota.max_op := None; |}
].
Definition rpc_services : RPC_directory.directory Updater.rpc_context :=
let '_ := Alpha_services.register tt in
Services_registration.get_rpc_services tt.
Definition validation_state : Set := Validate.validation_state.
Definition application_state : Set := Apply.application_state.
Definition init_allowed_consensus_operations
(ctxt : Alpha_context.context) (endorsement_level : Alpha_context.Level.t)
(preendorsement_level : Alpha_context.Level.t) : M? Alpha_context.t :=
let? ctxt := Alpha_context.Delegate.prepare_stake_distribution ctxt in
let? '(ctxt, allowed_endorsements, allowed_preendorsements) :=
if Alpha_context.Level.op_eq endorsement_level preendorsement_level then
let? '(ctxt, slots) :=
Baking.endorsing_rights_by_first_slot ctxt endorsement_level in
let consensus_operations := slots in
return? (ctxt, consensus_operations, consensus_operations)
else
let? '(ctxt, endorsements) :=
Baking.endorsing_rights_by_first_slot ctxt endorsement_level in
let? '(ctxt, preendorsements) :=
Baking.endorsing_rights_by_first_slot ctxt preendorsement_level in
return? (ctxt, endorsements, preendorsements) in
let ctxt :=
Alpha_context.Consensus.initialize_consensus_operation ctxt
allowed_endorsements allowed_preendorsements in
return? ctxt.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Alpha_services.
Require TezosOfOCaml.Proto_alpha.Apply.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Baking.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Dal_apply.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Mempool_validation.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Require TezosOfOCaml.Proto_alpha.Validate.
Require TezosOfOCaml.Proto_alpha.Validate_errors.
Definition block_header_data : Set := Alpha_context.Block_header.protocol_data.
Definition block_header : Set := Alpha_context.Block_header.t.
Definition block_header_data_encoding
: Data_encoding.encoding Alpha_context.Block_header.protocol_data :=
Alpha_context.Block_header.protocol_data_encoding.
Definition block_header_metadata : Set := Apply_results.block_metadata.
Definition block_header_metadata_encoding
: Data_encoding.encoding Apply_results.block_metadata :=
Apply_results.block_metadata_encoding.
Definition operation_data : Set := Alpha_context.packed_protocol_data.
Definition operation_data_encoding
: Data_encoding.t Alpha_context.Operation.packed_protocol_data :=
Alpha_context.Operation.protocol_data_encoding.
Definition operation_receipt : Set := Apply_results.packed_operation_metadata.
Definition operation_receipt_encoding
: Data_encoding.t Apply_results.packed_operation_metadata :=
Apply_results.operation_metadata_encoding.
Definition operation_data_and_receipt_encoding
: Data_encoding.t
(Alpha_context.Operation.packed_protocol_data ×
Apply_results.packed_operation_metadata) :=
Apply_results.operation_data_and_metadata_encoding.
Definition operation : Set := Alpha_context.packed_operation.
Definition acceptable_pass : Alpha_context.packed_operation → option int :=
Alpha_context.Operation.acceptable_pass.
Definition max_block_length : int :=
Alpha_context.Block_header.max_header_length.
Definition max_operation_data_length : int :=
Alpha_context.Constants.max_operation_data_length.
Definition validation_passes : list Updater.quota :=
[
{| Updater.quota.max_size := 2048 ×i 2048;
Updater.quota.max_op := Some 2048; |};
{| Updater.quota.max_size := 32 ×i 1024; Updater.quota.max_op := None; |};
{|
Updater.quota.max_size :=
Alpha_context.Constants.max_anon_ops_per_block ×i 1024;
Updater.quota.max_op :=
Some Alpha_context.Constants.max_anon_ops_per_block; |};
{| Updater.quota.max_size := 512 ×i 1024; Updater.quota.max_op := None; |}
].
Definition rpc_services : RPC_directory.directory Updater.rpc_context :=
let '_ := Alpha_services.register tt in
Services_registration.get_rpc_services tt.
Definition validation_state : Set := Validate.validation_state.
Definition application_state : Set := Apply.application_state.
Definition init_allowed_consensus_operations
(ctxt : Alpha_context.context) (endorsement_level : Alpha_context.Level.t)
(preendorsement_level : Alpha_context.Level.t) : M? Alpha_context.t :=
let? ctxt := Alpha_context.Delegate.prepare_stake_distribution ctxt in
let? '(ctxt, allowed_endorsements, allowed_preendorsements) :=
if Alpha_context.Level.op_eq endorsement_level preendorsement_level then
let? '(ctxt, slots) :=
Baking.endorsing_rights_by_first_slot ctxt endorsement_level in
let consensus_operations := slots in
return? (ctxt, consensus_operations, consensus_operations)
else
let? '(ctxt, endorsements) :=
Baking.endorsing_rights_by_first_slot ctxt endorsement_level in
let? '(ctxt, preendorsements) :=
Baking.endorsing_rights_by_first_slot ctxt preendorsement_level in
return? (ctxt, endorsements, preendorsements) in
let ctxt :=
Alpha_context.Consensus.initialize_consensus_operation ctxt
allowed_endorsements allowed_preendorsements in
return? ctxt.
Circumstances and relevant information for [begin_validation] and
[begin_application] below. Records for the constructor parameters
Module ConstructorRecords_mode.
Module mode.
Module Construction.
Record record {predecessor_hash timestamp block_header_data : Set} : Set := Build {
predecessor_hash : predecessor_hash;
timestamp : timestamp;
block_header_data : block_header_data;
}.
Arguments record : clear implicits.
Definition with_predecessor_hash
{t_predecessor_hash t_timestamp t_block_header_data} predecessor_hash
(r : record t_predecessor_hash t_timestamp t_block_header_data) :=
Build t_predecessor_hash t_timestamp t_block_header_data
predecessor_hash r.(timestamp) r.(block_header_data).
Definition with_timestamp
{t_predecessor_hash t_timestamp t_block_header_data} timestamp
(r : record t_predecessor_hash t_timestamp t_block_header_data) :=
Build t_predecessor_hash t_timestamp t_block_header_data
r.(predecessor_hash) timestamp r.(block_header_data).
Definition with_block_header_data
{t_predecessor_hash t_timestamp t_block_header_data} block_header_data
(r : record t_predecessor_hash t_timestamp t_block_header_data) :=
Build t_predecessor_hash t_timestamp t_block_header_data
r.(predecessor_hash) r.(timestamp) block_header_data.
End Construction.
Definition Construction_skeleton := Construction.record.
Module Partial_construction.
Record record {predecessor_hash timestamp : Set} : Set := Build {
predecessor_hash : predecessor_hash;
timestamp : timestamp;
}.
Arguments record : clear implicits.
Definition with_predecessor_hash {t_predecessor_hash t_timestamp}
predecessor_hash (r : record t_predecessor_hash t_timestamp) :=
Build t_predecessor_hash t_timestamp predecessor_hash r.(timestamp).
Definition with_timestamp {t_predecessor_hash t_timestamp} timestamp
(r : record t_predecessor_hash t_timestamp) :=
Build t_predecessor_hash t_timestamp r.(predecessor_hash) timestamp.
End Partial_construction.
Definition Partial_construction_skeleton := Partial_construction.record.
End mode.
End ConstructorRecords_mode.
Import ConstructorRecords_mode.
Reserved Notation "'mode.Construction".
Reserved Notation "'mode.Partial_construction".
Inductive mode : Set :=
| Application : block_header → mode
| Partial_validation : block_header → mode
| Construction : 'mode.Construction → mode
| Partial_construction : 'mode.Partial_construction → mode
where "'mode.Construction" :=
(mode.Construction_skeleton Block_hash.t Time.t block_header_data)
and "'mode.Partial_construction" :=
(mode.Partial_construction_skeleton Block_hash.t Time.t).
Module mode.
Include ConstructorRecords_mode.mode.
Definition Construction := 'mode.Construction.
Definition Partial_construction := 'mode.Partial_construction.
End mode.
Definition prepare_ctxt
(ctxt : Context.t) (mode : mode) (predecessor : Block_header.shell_header)
: M?
(Alpha_context.t × Alpha_context.Receipt.balance_updates ×
list Alpha_context.Migration.origination_result ×
Alpha_context.Level.level × Alpha_context.Raw_level.raw_level) :=
let '(level, timestamp) :=
match mode with
| (Application block_header | Partial_validation block_header) ⇒
(block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.level),
block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.timestamp))
|
(Construction {| mode.Construction.timestamp := timestamp |} |
Partial_construction {|
mode.Partial_construction.timestamp := timestamp |}) ⇒
((Int32.succ predecessor.(Block_header.shell_header.level)), timestamp)
end in
let? '(ctxt, migration_balance_updates, migration_operation_results) :=
Alpha_context.prepare ctxt level
predecessor.(Block_header.shell_header.timestamp) timestamp in
let? predecessor_raw_level :=
Alpha_context.Raw_level.of_int32
predecessor.(Block_header.shell_header.level) in
let? predecessor_level :=
Alpha_context.Level.from_raw ctxt predecessor_raw_level in
let preendorsement_level :=
match mode with
| (Application _ | Partial_validation _ | Construction _) ⇒
Alpha_context.Level.current ctxt
| Partial_construction _ ⇒ predecessor_level
end in
let? ctxt :=
init_allowed_consensus_operations ctxt predecessor_level
preendorsement_level in
let? ctxt := Dal_apply.initialisation ctxt predecessor_level in
return?
(ctxt, migration_balance_updates, migration_operation_results,
predecessor_level, predecessor_raw_level).
Definition begin_validation
(ctxt : Context.t) (chain_id : Chain_id.t) (mode : mode)
(predecessor : Block_header.shell_header) : M? Validate.validation_state :=
let?
'(ctxt, _migration_balance_updates, _migration_operation_results,
predecessor_level, _predecessor_raw_level) :=
prepare_ctxt ctxt mode predecessor in
let predecessor_timestamp := predecessor.(Block_header.shell_header.timestamp)
in
let predecessor_fitness := predecessor.(Block_header.shell_header.fitness) in
match mode with
| Application block_header ⇒
let? fitness :=
Alpha_context.Fitness.from_raw
block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.fitness)
in
Validate.begin_application ctxt chain_id predecessor_level
predecessor_timestamp block_header fitness
| Partial_validation block_header ⇒
let? fitness :=
Alpha_context.Fitness.from_raw
block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.fitness)
in
Validate.begin_partial_validation ctxt chain_id predecessor_level
predecessor_timestamp block_header fitness
|
Construction {|
mode.Construction.predecessor_hash := predecessor_hash;
mode.Construction.timestamp := timestamp;
mode.Construction.block_header_data := block_header_data
|} ⇒
let? predecessor_round :=
Alpha_context.Fitness.round_from_raw predecessor_fitness in
let? round :=
Alpha_context.Round.round_of_timestamp
(Alpha_context.Constants.round_durations ctxt) predecessor_timestamp
predecessor_round timestamp in
Validate.begin_full_construction ctxt chain_id predecessor_level
predecessor_round predecessor_timestamp predecessor_hash round
block_header_data.(Alpha_context.Block_header.protocol_data.contents)
| Partial_construction _ ⇒
let? predecessor_round :=
Alpha_context.Fitness.round_from_raw predecessor_fitness in
let? grandparent_round :=
Alpha_context.Fitness.predecessor_round_from_raw predecessor_fitness in
return?
(Validate.begin_partial_construction ctxt chain_id predecessor_level
predecessor_round grandparent_round)
end.
Definition validate_operation
: option bool → Validate.validation_state → Operation_hash.t →
Alpha_context.packed_operation → M? Validate.validation_state :=
Validate.validate_operation.
Definition finalize_validation : Validate.validation_state → M? unit :=
Validate.finalize_block.
Module mode.
Module Construction.
Record record {predecessor_hash timestamp block_header_data : Set} : Set := Build {
predecessor_hash : predecessor_hash;
timestamp : timestamp;
block_header_data : block_header_data;
}.
Arguments record : clear implicits.
Definition with_predecessor_hash
{t_predecessor_hash t_timestamp t_block_header_data} predecessor_hash
(r : record t_predecessor_hash t_timestamp t_block_header_data) :=
Build t_predecessor_hash t_timestamp t_block_header_data
predecessor_hash r.(timestamp) r.(block_header_data).
Definition with_timestamp
{t_predecessor_hash t_timestamp t_block_header_data} timestamp
(r : record t_predecessor_hash t_timestamp t_block_header_data) :=
Build t_predecessor_hash t_timestamp t_block_header_data
r.(predecessor_hash) timestamp r.(block_header_data).
Definition with_block_header_data
{t_predecessor_hash t_timestamp t_block_header_data} block_header_data
(r : record t_predecessor_hash t_timestamp t_block_header_data) :=
Build t_predecessor_hash t_timestamp t_block_header_data
r.(predecessor_hash) r.(timestamp) block_header_data.
End Construction.
Definition Construction_skeleton := Construction.record.
Module Partial_construction.
Record record {predecessor_hash timestamp : Set} : Set := Build {
predecessor_hash : predecessor_hash;
timestamp : timestamp;
}.
Arguments record : clear implicits.
Definition with_predecessor_hash {t_predecessor_hash t_timestamp}
predecessor_hash (r : record t_predecessor_hash t_timestamp) :=
Build t_predecessor_hash t_timestamp predecessor_hash r.(timestamp).
Definition with_timestamp {t_predecessor_hash t_timestamp} timestamp
(r : record t_predecessor_hash t_timestamp) :=
Build t_predecessor_hash t_timestamp r.(predecessor_hash) timestamp.
End Partial_construction.
Definition Partial_construction_skeleton := Partial_construction.record.
End mode.
End ConstructorRecords_mode.
Import ConstructorRecords_mode.
Reserved Notation "'mode.Construction".
Reserved Notation "'mode.Partial_construction".
Inductive mode : Set :=
| Application : block_header → mode
| Partial_validation : block_header → mode
| Construction : 'mode.Construction → mode
| Partial_construction : 'mode.Partial_construction → mode
where "'mode.Construction" :=
(mode.Construction_skeleton Block_hash.t Time.t block_header_data)
and "'mode.Partial_construction" :=
(mode.Partial_construction_skeleton Block_hash.t Time.t).
Module mode.
Include ConstructorRecords_mode.mode.
Definition Construction := 'mode.Construction.
Definition Partial_construction := 'mode.Partial_construction.
End mode.
Definition prepare_ctxt
(ctxt : Context.t) (mode : mode) (predecessor : Block_header.shell_header)
: M?
(Alpha_context.t × Alpha_context.Receipt.balance_updates ×
list Alpha_context.Migration.origination_result ×
Alpha_context.Level.level × Alpha_context.Raw_level.raw_level) :=
let '(level, timestamp) :=
match mode with
| (Application block_header | Partial_validation block_header) ⇒
(block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.level),
block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.timestamp))
|
(Construction {| mode.Construction.timestamp := timestamp |} |
Partial_construction {|
mode.Partial_construction.timestamp := timestamp |}) ⇒
((Int32.succ predecessor.(Block_header.shell_header.level)), timestamp)
end in
let? '(ctxt, migration_balance_updates, migration_operation_results) :=
Alpha_context.prepare ctxt level
predecessor.(Block_header.shell_header.timestamp) timestamp in
let? predecessor_raw_level :=
Alpha_context.Raw_level.of_int32
predecessor.(Block_header.shell_header.level) in
let? predecessor_level :=
Alpha_context.Level.from_raw ctxt predecessor_raw_level in
let preendorsement_level :=
match mode with
| (Application _ | Partial_validation _ | Construction _) ⇒
Alpha_context.Level.current ctxt
| Partial_construction _ ⇒ predecessor_level
end in
let? ctxt :=
init_allowed_consensus_operations ctxt predecessor_level
preendorsement_level in
let? ctxt := Dal_apply.initialisation ctxt predecessor_level in
return?
(ctxt, migration_balance_updates, migration_operation_results,
predecessor_level, predecessor_raw_level).
Definition begin_validation
(ctxt : Context.t) (chain_id : Chain_id.t) (mode : mode)
(predecessor : Block_header.shell_header) : M? Validate.validation_state :=
let?
'(ctxt, _migration_balance_updates, _migration_operation_results,
predecessor_level, _predecessor_raw_level) :=
prepare_ctxt ctxt mode predecessor in
let predecessor_timestamp := predecessor.(Block_header.shell_header.timestamp)
in
let predecessor_fitness := predecessor.(Block_header.shell_header.fitness) in
match mode with
| Application block_header ⇒
let? fitness :=
Alpha_context.Fitness.from_raw
block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.fitness)
in
Validate.begin_application ctxt chain_id predecessor_level
predecessor_timestamp block_header fitness
| Partial_validation block_header ⇒
let? fitness :=
Alpha_context.Fitness.from_raw
block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.fitness)
in
Validate.begin_partial_validation ctxt chain_id predecessor_level
predecessor_timestamp block_header fitness
|
Construction {|
mode.Construction.predecessor_hash := predecessor_hash;
mode.Construction.timestamp := timestamp;
mode.Construction.block_header_data := block_header_data
|} ⇒
let? predecessor_round :=
Alpha_context.Fitness.round_from_raw predecessor_fitness in
let? round :=
Alpha_context.Round.round_of_timestamp
(Alpha_context.Constants.round_durations ctxt) predecessor_timestamp
predecessor_round timestamp in
Validate.begin_full_construction ctxt chain_id predecessor_level
predecessor_round predecessor_timestamp predecessor_hash round
block_header_data.(Alpha_context.Block_header.protocol_data.contents)
| Partial_construction _ ⇒
let? predecessor_round :=
Alpha_context.Fitness.round_from_raw predecessor_fitness in
let? grandparent_round :=
Alpha_context.Fitness.predecessor_round_from_raw predecessor_fitness in
return?
(Validate.begin_partial_construction ctxt chain_id predecessor_level
predecessor_round grandparent_round)
end.
Definition validate_operation
: option bool → Validate.validation_state → Operation_hash.t →
Alpha_context.packed_operation → M? Validate.validation_state :=
Validate.validate_operation.
Definition finalize_validation : Validate.validation_state → M? unit :=
Validate.finalize_block.
Init function; without side-effects in Coq
Definition init_module : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"main.begin_application.cannot_apply_in_partial_validation"
"cannot_apply_in_partial_validation"
"Cannot instantiate an application state using the 'Partial_validation' mode."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot instantiate an application state using the 'Partial_validation' mode."
CamlinternalFormatBasics.End_of_format)
"Cannot instantiate an application state using the 'Partial_validation' mode.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Cannot_apply_in_partial_validation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Cannot_apply_in_partial_validation" unit tt).
Definition begin_application
(ctxt : Context.t) (chain_id : Chain_id.t) (mode : mode)
(predecessor : Block_header.shell_header) : M? Apply.application_state :=
let?
'(ctxt, migration_balance_updates, migration_operation_results,
predecessor_level, predecessor_raw_level) :=
prepare_ctxt ctxt mode predecessor in
let predecessor_timestamp := predecessor.(Block_header.shell_header.timestamp)
in
let predecessor_fitness := predecessor.(Block_header.shell_header.fitness) in
match mode with
| Application block_header ⇒
Apply.begin_application ctxt chain_id migration_balance_updates
migration_operation_results predecessor_fitness block_header
| Partial_validation _ ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Cannot_apply_in_partial_validation" unit tt)
|
Construction {|
mode.Construction.predecessor_hash := predecessor_hash;
mode.Construction.timestamp := timestamp;
mode.Construction.block_header_data := block_header_data
|} ⇒
let? predecessor_round :=
Alpha_context.Fitness.round_from_raw predecessor_fitness in
Apply.begin_full_construction ctxt chain_id migration_balance_updates
migration_operation_results predecessor_timestamp predecessor_level
predecessor_round predecessor_hash timestamp
block_header_data.(Alpha_context.Block_header.protocol_data.contents)
|
Partial_construction {|
mode.Partial_construction.predecessor_hash := predecessor_hash |} ⇒
Apply.begin_partial_construction ctxt chain_id migration_balance_updates
migration_operation_results predecessor_raw_level predecessor_timestamp
predecessor_hash predecessor_fitness
end.
Definition apply_operation
: Apply.application_state → Operation_hash.t →
Alpha_context.packed_operation →
M? (Apply.application_state × Apply_results.packed_operation_metadata) :=
Apply.apply_operation.
Definition finalize_application
: Apply.application_state → option Alpha_context.Block_header.shell_header →
M? (Updater.validation_result × Apply_results.block_metadata) :=
Apply.finalize_block.
Definition compare_operations
(function_parameter : Operation_hash.t × Alpha_context.packed_operation)
: Operation_hash.t × Alpha_context.packed_operation → int :=
let '(oph1, op1) := function_parameter in
fun (function_parameter : Operation_hash.t × Alpha_context.packed_operation)
⇒
let '(oph2, op2) := function_parameter in
Alpha_context.Operation.compare (oph1, op1) (oph2, op2).
Definition init_value
(chain_id : Chain_id.t) (ctxt : Context.t)
(block_header : Block_header.shell_header) : M? Updater.validation_result :=
let level := block_header.(Block_header.shell_header.level) in
let timestamp := block_header.(Block_header.shell_header.timestamp) in
let predecessor := block_header.(Block_header.shell_header.predecessor) in
let typecheck (ctxt : Alpha_context.context) (script : Alpha_context.Script.t)
: M?
((Alpha_context.Script.t × option Alpha_context.Lazy_storage.diffs) ×
Alpha_context.context) :=
let allow_forged_in_storage := false in
let?
'(Script_ir_translator.Ex_script (Script_typed_ir.Script parsed_script),
ctxt) :=
Script_ir_translator.parse_script
(Script_ir_translator_config.make None None true tt) ctxt
allow_forged_in_storage script in
let? '(storage_value, lazy_storage_diff, ctxt) :=
Script_ir_translator.extract_lazy_storage_diff ctxt
Script_ir_unparser.Optimized false
Script_ir_translator.no_lazy_storage_id
Script_ir_translator.no_lazy_storage_id
parsed_script.(Script_typed_ir.script.Script.storage_type)
parsed_script.(Script_typed_ir.script.Script.storage) in
let? '(storage_value, ctxt) :=
Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
parsed_script.(Script_typed_ir.script.Script.storage_type) storage_value
in
let storage_value := Alpha_context.Script.lazy_expr_value storage_value in
return?
(((Alpha_context.Script.t.with_storage storage_value script),
lazy_storage_diff), ctxt) in
let? raw_level := Alpha_context.Raw_level.of_int32 level in
let init_fitness :=
Alpha_context.Fitness.create_without_locked_round raw_level
Alpha_context.Round.zero Alpha_context.Round.zero in
let? ctxt :=
Alpha_context.prepare_first_block chain_id ctxt typecheck level timestamp
predecessor in
let cache_nonce :=
Alpha_context.Cache.cache_nonce_from_block_header block_header
{|
Alpha_context.Block_header.contents.payload_hash :=
Block_payload_hash.zero;
Alpha_context.Block_header.contents.payload_round :=
Alpha_context.Round.zero;
Alpha_context.Block_header.contents.seed_nonce_hash := None;
Alpha_context.Block_header.contents.proof_of_work_nonce :=
Bytes.make Constants_repr.proof_of_work_nonce_size "0" % char;
Alpha_context.Block_header.contents.liquidity_baking_toggle_vote :=
Liquidity_baking_repr.LB_pass; |} in
let ctxt := Alpha_context.Cache.Admin.sync ctxt cache_nonce in
let? res :=
Alpha_context.finalize None ctxt (Alpha_context.Fitness.to_raw init_fitness)
in
return? res.
Definition value_of_key {A B C : Set} (function_parameter : A)
: Context.t → Time.t → int32 → B → C → Time.t →
M? (Context.cache_key → M? Context.cache_value) :=
let '_ := function_parameter in
fun (ctxt : Context.t) ⇒
fun (predecessor_timestamp : Time.t) ⇒
fun (pred_level : int32) ⇒
fun (function_parameter : B) ⇒
let '_ := function_parameter in
fun (function_parameter : C) ⇒
let '_ := function_parameter in
fun (timestamp : Time.t) ⇒
let level := Int32.succ pred_level in
let? '(ctxt, _, _) :=
Alpha_context.prepare ctxt level predecessor_timestamp timestamp
in
return? (Apply.value_of_key ctxt).
Module Mempool.
Definition t : Set := Mempool_validation.t.
Definition validation_info : Set := Mempool_validation.validation_info.
Definition keep_or_replace : Set := Mempool_validation.keep_or_replace.
Definition conflict_handler : Set := Mempool_validation.conflict_handler.
Definition operation_conflict : Set := Validate_errors.operation_conflict.
Definition add_result : Set := Mempool_validation.add_result.
Definition add_error : Set := Mempool_validation.add_error.
Definition merge_error : Set := Mempool_validation.merge_error.
Definition encoding : Data_encoding.t Mempool_validation.t :=
Mempool_validation.encoding.
Definition add_operation
: option bool → option Mempool_validation.conflict_handler →
Mempool_validation.validation_info → Mempool_validation.t →
Operation_hash.t × Alpha_context.packed_operation →
Pervasives.result (Mempool_validation.t × Mempool_validation.add_result)
Mempool_validation.add_error := Mempool_validation.add_operation.
Definition remove_operation
: Mempool_validation.t → Operation_hash.t → Mempool_validation.t :=
Mempool_validation.remove_operation.
Definition merge
: option Mempool_validation.conflict_handler → Mempool_validation.t →
Mempool_validation.t →
Pervasives.result Mempool_validation.t Mempool_validation.merge_error :=
Mempool_validation.merge.
Definition operations
: Mempool_validation.t →
Operation_hash.Map.(S.INDEXES_MAP.t) Alpha_context.packed_operation :=
Mempool_validation.operations.
Definition init_value
(ctxt : Context.t) (chain_id : Chain_id.t) (head_hash : Block_hash.t)
(head : Block_header.shell_header)
: M? (Mempool_validation.validation_info × Mempool_validation.t) :=
let?
'(ctxt, _migration_balance_updates, _migration_operation_results,
head_level, _head_raw_level) :=
prepare_ctxt ctxt
(Partial_construction
{| mode.Partial_construction.predecessor_hash := head_hash;
mode.Partial_construction.timestamp :=
head.(Block_header.shell_header.timestamp); |}) head in
let? fitness :=
Alpha_context.Fitness.from_raw head.(Block_header.shell_header.fitness) in
let predecessor_round := Alpha_context.Fitness.round fitness in
let grandparent_round := Alpha_context.Fitness.predecessor_round fitness in
return?
(Mempool_validation.init_value ctxt chain_id head_level predecessor_round
head_hash grandparent_round).
End Mempool.
Error_monad.register_error_kind Error_monad.Permanent
"main.begin_application.cannot_apply_in_partial_validation"
"cannot_apply_in_partial_validation"
"Cannot instantiate an application state using the 'Partial_validation' mode."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot instantiate an application state using the 'Partial_validation' mode."
CamlinternalFormatBasics.End_of_format)
"Cannot instantiate an application state using the 'Partial_validation' mode.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Cannot_apply_in_partial_validation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Cannot_apply_in_partial_validation" unit tt).
Definition begin_application
(ctxt : Context.t) (chain_id : Chain_id.t) (mode : mode)
(predecessor : Block_header.shell_header) : M? Apply.application_state :=
let?
'(ctxt, migration_balance_updates, migration_operation_results,
predecessor_level, predecessor_raw_level) :=
prepare_ctxt ctxt mode predecessor in
let predecessor_timestamp := predecessor.(Block_header.shell_header.timestamp)
in
let predecessor_fitness := predecessor.(Block_header.shell_header.fitness) in
match mode with
| Application block_header ⇒
Apply.begin_application ctxt chain_id migration_balance_updates
migration_operation_results predecessor_fitness block_header
| Partial_validation _ ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Cannot_apply_in_partial_validation" unit tt)
|
Construction {|
mode.Construction.predecessor_hash := predecessor_hash;
mode.Construction.timestamp := timestamp;
mode.Construction.block_header_data := block_header_data
|} ⇒
let? predecessor_round :=
Alpha_context.Fitness.round_from_raw predecessor_fitness in
Apply.begin_full_construction ctxt chain_id migration_balance_updates
migration_operation_results predecessor_timestamp predecessor_level
predecessor_round predecessor_hash timestamp
block_header_data.(Alpha_context.Block_header.protocol_data.contents)
|
Partial_construction {|
mode.Partial_construction.predecessor_hash := predecessor_hash |} ⇒
Apply.begin_partial_construction ctxt chain_id migration_balance_updates
migration_operation_results predecessor_raw_level predecessor_timestamp
predecessor_hash predecessor_fitness
end.
Definition apply_operation
: Apply.application_state → Operation_hash.t →
Alpha_context.packed_operation →
M? (Apply.application_state × Apply_results.packed_operation_metadata) :=
Apply.apply_operation.
Definition finalize_application
: Apply.application_state → option Alpha_context.Block_header.shell_header →
M? (Updater.validation_result × Apply_results.block_metadata) :=
Apply.finalize_block.
Definition compare_operations
(function_parameter : Operation_hash.t × Alpha_context.packed_operation)
: Operation_hash.t × Alpha_context.packed_operation → int :=
let '(oph1, op1) := function_parameter in
fun (function_parameter : Operation_hash.t × Alpha_context.packed_operation)
⇒
let '(oph2, op2) := function_parameter in
Alpha_context.Operation.compare (oph1, op1) (oph2, op2).
Definition init_value
(chain_id : Chain_id.t) (ctxt : Context.t)
(block_header : Block_header.shell_header) : M? Updater.validation_result :=
let level := block_header.(Block_header.shell_header.level) in
let timestamp := block_header.(Block_header.shell_header.timestamp) in
let predecessor := block_header.(Block_header.shell_header.predecessor) in
let typecheck (ctxt : Alpha_context.context) (script : Alpha_context.Script.t)
: M?
((Alpha_context.Script.t × option Alpha_context.Lazy_storage.diffs) ×
Alpha_context.context) :=
let allow_forged_in_storage := false in
let?
'(Script_ir_translator.Ex_script (Script_typed_ir.Script parsed_script),
ctxt) :=
Script_ir_translator.parse_script
(Script_ir_translator_config.make None None true tt) ctxt
allow_forged_in_storage script in
let? '(storage_value, lazy_storage_diff, ctxt) :=
Script_ir_translator.extract_lazy_storage_diff ctxt
Script_ir_unparser.Optimized false
Script_ir_translator.no_lazy_storage_id
Script_ir_translator.no_lazy_storage_id
parsed_script.(Script_typed_ir.script.Script.storage_type)
parsed_script.(Script_typed_ir.script.Script.storage) in
let? '(storage_value, ctxt) :=
Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
parsed_script.(Script_typed_ir.script.Script.storage_type) storage_value
in
let storage_value := Alpha_context.Script.lazy_expr_value storage_value in
return?
(((Alpha_context.Script.t.with_storage storage_value script),
lazy_storage_diff), ctxt) in
let? raw_level := Alpha_context.Raw_level.of_int32 level in
let init_fitness :=
Alpha_context.Fitness.create_without_locked_round raw_level
Alpha_context.Round.zero Alpha_context.Round.zero in
let? ctxt :=
Alpha_context.prepare_first_block chain_id ctxt typecheck level timestamp
predecessor in
let cache_nonce :=
Alpha_context.Cache.cache_nonce_from_block_header block_header
{|
Alpha_context.Block_header.contents.payload_hash :=
Block_payload_hash.zero;
Alpha_context.Block_header.contents.payload_round :=
Alpha_context.Round.zero;
Alpha_context.Block_header.contents.seed_nonce_hash := None;
Alpha_context.Block_header.contents.proof_of_work_nonce :=
Bytes.make Constants_repr.proof_of_work_nonce_size "0" % char;
Alpha_context.Block_header.contents.liquidity_baking_toggle_vote :=
Liquidity_baking_repr.LB_pass; |} in
let ctxt := Alpha_context.Cache.Admin.sync ctxt cache_nonce in
let? res :=
Alpha_context.finalize None ctxt (Alpha_context.Fitness.to_raw init_fitness)
in
return? res.
Definition value_of_key {A B C : Set} (function_parameter : A)
: Context.t → Time.t → int32 → B → C → Time.t →
M? (Context.cache_key → M? Context.cache_value) :=
let '_ := function_parameter in
fun (ctxt : Context.t) ⇒
fun (predecessor_timestamp : Time.t) ⇒
fun (pred_level : int32) ⇒
fun (function_parameter : B) ⇒
let '_ := function_parameter in
fun (function_parameter : C) ⇒
let '_ := function_parameter in
fun (timestamp : Time.t) ⇒
let level := Int32.succ pred_level in
let? '(ctxt, _, _) :=
Alpha_context.prepare ctxt level predecessor_timestamp timestamp
in
return? (Apply.value_of_key ctxt).
Module Mempool.
Definition t : Set := Mempool_validation.t.
Definition validation_info : Set := Mempool_validation.validation_info.
Definition keep_or_replace : Set := Mempool_validation.keep_or_replace.
Definition conflict_handler : Set := Mempool_validation.conflict_handler.
Definition operation_conflict : Set := Validate_errors.operation_conflict.
Definition add_result : Set := Mempool_validation.add_result.
Definition add_error : Set := Mempool_validation.add_error.
Definition merge_error : Set := Mempool_validation.merge_error.
Definition encoding : Data_encoding.t Mempool_validation.t :=
Mempool_validation.encoding.
Definition add_operation
: option bool → option Mempool_validation.conflict_handler →
Mempool_validation.validation_info → Mempool_validation.t →
Operation_hash.t × Alpha_context.packed_operation →
Pervasives.result (Mempool_validation.t × Mempool_validation.add_result)
Mempool_validation.add_error := Mempool_validation.add_operation.
Definition remove_operation
: Mempool_validation.t → Operation_hash.t → Mempool_validation.t :=
Mempool_validation.remove_operation.
Definition merge
: option Mempool_validation.conflict_handler → Mempool_validation.t →
Mempool_validation.t →
Pervasives.result Mempool_validation.t Mempool_validation.merge_error :=
Mempool_validation.merge.
Definition operations
: Mempool_validation.t →
Operation_hash.Map.(S.INDEXES_MAP.t) Alpha_context.packed_operation :=
Mempool_validation.operations.
Definition init_value
(ctxt : Context.t) (chain_id : Chain_id.t) (head_hash : Block_hash.t)
(head : Block_header.shell_header)
: M? (Mempool_validation.validation_info × Mempool_validation.t) :=
let?
'(ctxt, _migration_balance_updates, _migration_operation_results,
head_level, _head_raw_level) :=
prepare_ctxt ctxt
(Partial_construction
{| mode.Partial_construction.predecessor_hash := head_hash;
mode.Partial_construction.timestamp :=
head.(Block_header.shell_header.timestamp); |}) head in
let? fitness :=
Alpha_context.Fitness.from_raw head.(Block_header.shell_header.fitness) in
let predecessor_round := Alpha_context.Fitness.round fitness in
let grandparent_round := Alpha_context.Fitness.predecessor_round fitness in
return?
(Mempool_validation.init_value ctxt chain_id head_level predecessor_round
head_hash grandparent_round).
End Mempool.