Skip to main content

🧑 Main.v

Translated OCaml

Gitlab , 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.

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.

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.