Skip to main content

🧑 Main.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
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.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_migration_for_j.

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_passes : Alpha_context.packed_operation list int :=
  Alpha_context.Operation.acceptable_passes.

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.

Records for the constructor parameters
Module ConstructorRecords_validation_mode.
  Module validation_mode.
    Module Application.
      Record record {block_header fitness payload_producer block_producer
        predecessor_round predecessor_level : Set} : Set := Build {
        block_header : block_header;
        fitness : fitness;
        payload_producer : payload_producer;
        block_producer : block_producer;
        predecessor_round : predecessor_round;
        predecessor_level : predecessor_level;
      }.
      Arguments record : clear implicits.
      Definition with_block_header
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level} block_header
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_round t_predecessor_level) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level block_header r.(fitness)
          r.(payload_producer) r.(block_producer) r.(predecessor_round)
          r.(predecessor_level).
      Definition with_fitness
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level} fitness
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_round t_predecessor_level) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level r.(block_header) fitness
          r.(payload_producer) r.(block_producer) r.(predecessor_round)
          r.(predecessor_level).
      Definition with_payload_producer
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level} payload_producer
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_round t_predecessor_level) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level r.(block_header) r.(fitness)
          payload_producer r.(block_producer) r.(predecessor_round)
          r.(predecessor_level).
      Definition with_block_producer
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level} block_producer
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_round t_predecessor_level) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level r.(block_header) r.(fitness)
          r.(payload_producer) block_producer r.(predecessor_round)
          r.(predecessor_level).
      Definition with_predecessor_round
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level} predecessor_round
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_round t_predecessor_level) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level r.(block_header) r.(fitness)
          r.(payload_producer) r.(block_producer) predecessor_round
          r.(predecessor_level).
      Definition with_predecessor_level
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level} predecessor_level
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_round t_predecessor_level) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_round t_predecessor_level r.(block_header) r.(fitness)
          r.(payload_producer) r.(block_producer) r.(predecessor_round)
          predecessor_level.
    End Application.
    Definition Application_skeleton := Application.record.

    Module Partial_application.
      Record record {block_header fitness payload_producer block_producer
        predecessor_level predecessor_round : Set} : Set := Build {
        block_header : block_header;
        fitness : fitness;
        payload_producer : payload_producer;
        block_producer : block_producer;
        predecessor_level : predecessor_level;
        predecessor_round : predecessor_round;
      }.
      Arguments record : clear implicits.
      Definition with_block_header
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} block_header
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_level t_predecessor_round) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round block_header r.(fitness)
          r.(payload_producer) r.(block_producer) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_fitness
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} fitness
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_level t_predecessor_round) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round r.(block_header) fitness
          r.(payload_producer) r.(block_producer) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_payload_producer
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} payload_producer
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_level t_predecessor_round) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round r.(block_header) r.(fitness)
          payload_producer r.(block_producer) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_block_producer
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} block_producer
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_level t_predecessor_round) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round r.(block_header) r.(fitness)
          r.(payload_producer) block_producer r.(predecessor_level)
          r.(predecessor_round).
      Definition with_predecessor_level
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} predecessor_level
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_level t_predecessor_round) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round r.(block_header) r.(fitness)
          r.(payload_producer) r.(block_producer) predecessor_level
          r.(predecessor_round).
      Definition with_predecessor_round
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} predecessor_round
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_level t_predecessor_round) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round r.(block_header) r.(fitness)
          r.(payload_producer) r.(block_producer) r.(predecessor_level)
          predecessor_round.
    End Partial_application.
    Definition Partial_application_skeleton := Partial_application.record.

    Module Partial_construction.
      Record record {predecessor predecessor_fitness predecessor_level
        predecessor_round : Set} : Set := Build {
        predecessor : predecessor;
        predecessor_fitness : predecessor_fitness;
        predecessor_level : predecessor_level;
        predecessor_round : predecessor_round;
      }.
      Arguments record : clear implicits.
      Definition with_predecessor
        {t_predecessor t_predecessor_fitness t_predecessor_level
          t_predecessor_round} predecessor
        (r :
          record t_predecessor t_predecessor_fitness t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_predecessor_fitness t_predecessor_level
          t_predecessor_round predecessor r.(predecessor_fitness)
          r.(predecessor_level) r.(predecessor_round).
      Definition with_predecessor_fitness
        {t_predecessor t_predecessor_fitness t_predecessor_level
          t_predecessor_round} predecessor_fitness
        (r :
          record t_predecessor t_predecessor_fitness t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_predecessor_fitness t_predecessor_level
          t_predecessor_round r.(predecessor) predecessor_fitness
          r.(predecessor_level) r.(predecessor_round).
      Definition with_predecessor_level
        {t_predecessor t_predecessor_fitness t_predecessor_level
          t_predecessor_round} predecessor_level
        (r :
          record t_predecessor t_predecessor_fitness t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_predecessor_fitness t_predecessor_level
          t_predecessor_round r.(predecessor) r.(predecessor_fitness)
          predecessor_level r.(predecessor_round).
      Definition with_predecessor_round
        {t_predecessor t_predecessor_fitness t_predecessor_level
          t_predecessor_round} predecessor_round
        (r :
          record t_predecessor t_predecessor_fitness t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_predecessor_fitness t_predecessor_level
          t_predecessor_round r.(predecessor) r.(predecessor_fitness)
          r.(predecessor_level) predecessor_round.
    End Partial_construction.
    Definition Partial_construction_skeleton := Partial_construction.record.

    Module Full_construction.
      Record record {predecessor payload_producer block_producer
        protocol_data_contents level round predecessor_level predecessor_round :
        Set} : Set := Build {
        predecessor : predecessor;
        payload_producer : payload_producer;
        block_producer : block_producer;
        protocol_data_contents : protocol_data_contents;
        level : level;
        round : round;
        predecessor_level : predecessor_level;
        predecessor_round : predecessor_round;
      }.
      Arguments record : clear implicits.
      Definition with_predecessor
        {t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round} predecessor
        (r :
          record t_predecessor t_payload_producer t_block_producer
            t_protocol_data_contents t_level t_round t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round predecessor r.(payload_producer)
          r.(block_producer) r.(protocol_data_contents) r.(level) r.(round)
          r.(predecessor_level) r.(predecessor_round).
      Definition with_payload_producer
        {t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round} payload_producer
        (r :
          record t_predecessor t_payload_producer t_block_producer
            t_protocol_data_contents t_level t_round t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round r.(predecessor) payload_producer
          r.(block_producer) r.(protocol_data_contents) r.(level) r.(round)
          r.(predecessor_level) r.(predecessor_round).
      Definition with_block_producer
        {t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round} block_producer
        (r :
          record t_predecessor t_payload_producer t_block_producer
            t_protocol_data_contents t_level t_round t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round r.(predecessor) r.(payload_producer)
          block_producer r.(protocol_data_contents) r.(level) r.(round)
          r.(predecessor_level) r.(predecessor_round).
      Definition with_protocol_data_contents
        {t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round} protocol_data_contents
        (r :
          record t_predecessor t_payload_producer t_block_producer
            t_protocol_data_contents t_level t_round t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round r.(predecessor) r.(payload_producer)
          r.(block_producer) protocol_data_contents r.(level) r.(round)
          r.(predecessor_level) r.(predecessor_round).
      Definition with_level
        {t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round} level
        (r :
          record t_predecessor t_payload_producer t_block_producer
            t_protocol_data_contents t_level t_round t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round r.(predecessor) r.(payload_producer)
          r.(block_producer) r.(protocol_data_contents) level r.(round)
          r.(predecessor_level) r.(predecessor_round).
      Definition with_round
        {t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round} round
        (r :
          record t_predecessor t_payload_producer t_block_producer
            t_protocol_data_contents t_level t_round t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round r.(predecessor) r.(payload_producer)
          r.(block_producer) r.(protocol_data_contents) r.(level) round
          r.(predecessor_level) r.(predecessor_round).
      Definition with_predecessor_level
        {t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round} predecessor_level
        (r :
          record t_predecessor t_payload_producer t_block_producer
            t_protocol_data_contents t_level t_round t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round r.(predecessor) r.(payload_producer)
          r.(block_producer) r.(protocol_data_contents) r.(level) r.(round)
          predecessor_level r.(predecessor_round).
      Definition with_predecessor_round
        {t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round} predecessor_round
        (r :
          record t_predecessor t_payload_producer t_block_producer
            t_protocol_data_contents t_level t_round t_predecessor_level
            t_predecessor_round) :=
        Build t_predecessor t_payload_producer t_block_producer
          t_protocol_data_contents t_level t_round t_predecessor_level
          t_predecessor_round r.(predecessor) r.(payload_producer)
          r.(block_producer) r.(protocol_data_contents) r.(level) r.(round)
          r.(predecessor_level) predecessor_round.
    End Full_construction.
    Definition Full_construction_skeleton := Full_construction.record.
  End validation_mode.
End ConstructorRecords_validation_mode.
Import ConstructorRecords_validation_mode.

Reserved Notation "'validation_mode.Application".
Reserved Notation "'validation_mode.Partial_application".
Reserved Notation "'validation_mode.Partial_construction".
Reserved Notation "'validation_mode.Full_construction".

Inductive validation_mode : Set :=
| Application : 'validation_mode.Application validation_mode
| Partial_application : 'validation_mode.Partial_application validation_mode
| Partial_construction :
  'validation_mode.Partial_construction validation_mode
| Full_construction : 'validation_mode.Full_construction validation_mode

where "'validation_mode.Application" :=
  (validation_mode.Application_skeleton Alpha_context.Block_header.t
    Alpha_context.Fitness.t Alpha_context.public_key_hash
    Alpha_context.public_key_hash Alpha_context.Round.t Alpha_context.Level.t)
and "'validation_mode.Partial_application" :=
  (validation_mode.Partial_application_skeleton Alpha_context.Block_header.t
    Alpha_context.Fitness.t Alpha_context.public_key_hash
    Alpha_context.public_key_hash Alpha_context.Level.t Alpha_context.Round.t)
and "'validation_mode.Partial_construction" :=
  (validation_mode.Partial_construction_skeleton Block_hash.t Fitness.t
    Alpha_context.Level.t Alpha_context.Round.t)
and "'validation_mode.Full_construction" :=
  (validation_mode.Full_construction_skeleton Block_hash.t
    Alpha_context.public_key_hash Alpha_context.public_key_hash
    Alpha_context.Block_header.contents Int32.t Alpha_context.Round.t
    Alpha_context.Level.t Alpha_context.Round.t).

Module validation_mode.
  Include ConstructorRecords_validation_mode.validation_mode.
  Definition Application := 'validation_mode.Application.
  Definition Partial_application := 'validation_mode.Partial_application.
  Definition Partial_construction := 'validation_mode.Partial_construction.
  Definition Full_construction := 'validation_mode.Full_construction.
End validation_mode.

Module validation_state.
  Record record : Set := Build {
    mode : validation_mode;
    chain_id : Chain_id.t;
    ctxt : Alpha_context.t;
    op_count : int;
    migration_balance_updates : Alpha_context.Receipt.balance_updates;
    liquidity_baking_toggle_ema : Alpha_context.Liquidity_baking.Toggle_EMA.t;
    implicit_operations_results :
      list Apply_results.packed_successful_manager_operation_result;
  }.
  Definition with_mode mode (r : record) :=
    Build mode r.(chain_id) r.(ctxt) r.(op_count) r.(migration_balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_chain_id chain_id (r : record) :=
    Build r.(mode) chain_id r.(ctxt) r.(op_count) r.(migration_balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_ctxt ctxt (r : record) :=
    Build r.(mode) r.(chain_id) ctxt r.(op_count) r.(migration_balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_op_count op_count (r : record) :=
    Build r.(mode) r.(chain_id) r.(ctxt) op_count r.(migration_balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_migration_balance_updates migration_balance_updates
    (r : record) :=
    Build r.(mode) r.(chain_id) r.(ctxt) r.(op_count) migration_balance_updates
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_liquidity_baking_toggle_ema liquidity_baking_toggle_ema
    (r : record) :=
    Build r.(mode) r.(chain_id) r.(ctxt) r.(op_count)
      r.(migration_balance_updates) liquidity_baking_toggle_ema
      r.(implicit_operations_results).
  Definition with_implicit_operations_results implicit_operations_results
    (r : record) :=
    Build r.(mode) r.(chain_id) r.(ctxt) r.(op_count)
      r.(migration_balance_updates) r.(liquidity_baking_toggle_ema)
      implicit_operations_results.
End validation_state.
Definition validation_state := validation_state.record.

Definition begin_partial_application
  (chain_id : Chain_id.t) (ctxt : Context.t) (predecessor_timestamp : Time.t)
  (predecessor_fitness : Fitness.t)
  (block_header : Alpha_context.Block_header.t) : M? validation_state :=
  let level :=
    block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.level)
    in
  let timestamp :=
    block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.timestamp)
    in
  let? fitness :=
    Alpha_context.Fitness.from_raw
      block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.fitness)
    in
  let? predecessor_round :=
    Alpha_context.Fitness.round_from_raw predecessor_fitness in
  let? '(ctxt, migration_balance_updates, migration_operation_results) :=
    Alpha_context.prepare ctxt level predecessor_timestamp timestamp in
  let? predecessor_level := Alpha_context.Raw_level.of_int32 (Int32.pred level)
    in
  let predecessor_level := Alpha_context.Level.from_raw ctxt predecessor_level
    in
  let?
    '(ctxt, payload_producer_pk, block_producer,
      liquidity_baking_operations_results, liquidity_baking_toggle_ema) :=
    Apply.begin_application ctxt chain_id block_header fitness
      predecessor_timestamp predecessor_level predecessor_round in
  let mode :=
    Partial_application
      {| validation_mode.Partial_application.block_header := block_header;
        validation_mode.Partial_application.fitness := fitness;
        validation_mode.Partial_application.payload_producer :=
          Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
            payload_producer_pk;
        validation_mode.Partial_application.block_producer := block_producer;
        validation_mode.Partial_application.predecessor_level :=
          predecessor_level;
        validation_mode.Partial_application.predecessor_round :=
          predecessor_round; |} in
  return?
    {| validation_state.mode := mode; validation_state.chain_id := chain_id;
      validation_state.ctxt := ctxt; validation_state.op_count := 0;
      validation_state.migration_balance_updates := migration_balance_updates;
      validation_state.liquidity_baking_toggle_ema :=
        liquidity_baking_toggle_ema;
      validation_state.implicit_operations_results :=
        Pervasives.op_at
          (Apply_results.pack_migration_operation_results
            migration_operation_results) liquidity_baking_operations_results; |}.

Definition begin_application
  (chain_id : Chain_id.t) (ctxt : Context.t) (predecessor_timestamp : Time.t)
  (predecessor_fitness : Alpha_context.Fitness.raw)
  (block_header : Alpha_context.Block_header.t) : M? validation_state :=
  let level :=
    block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.level)
    in
  let timestamp :=
    block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.timestamp)
    in
  let? fitness :=
    Alpha_context.Fitness.from_raw
      block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.fitness)
    in
  let? predecessor_round :=
    Alpha_context.Fitness.round_from_raw predecessor_fitness in
  let? predecessor_level := Alpha_context.Raw_level.of_int32 (Int32.pred level)
    in
  let? '(ctxt, migration_balance_updates, migration_operation_results) :=
    Alpha_context.prepare ctxt level predecessor_timestamp timestamp in
  let predecessor_level := Alpha_context.Level.from_raw ctxt predecessor_level
    in
  let?
    '(ctxt, payload_producer, block_producer,
      liquidity_baking_operations_results, liquidity_baking_toggle_ema) :=
    Apply.begin_application ctxt chain_id block_header fitness
      predecessor_timestamp predecessor_level predecessor_round in
  let mode :=
    Application
      {| validation_mode.Application.block_header := block_header;
        validation_mode.Application.fitness := fitness;
        validation_mode.Application.payload_producer :=
          Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
            payload_producer;
        validation_mode.Application.block_producer := block_producer;
        validation_mode.Application.predecessor_round := predecessor_round;
        validation_mode.Application.predecessor_level := predecessor_level; |}
    in
  return?
    {| validation_state.mode := mode; validation_state.chain_id := chain_id;
      validation_state.ctxt := ctxt; validation_state.op_count := 0;
      validation_state.migration_balance_updates := migration_balance_updates;
      validation_state.liquidity_baking_toggle_ema :=
        liquidity_baking_toggle_ema;
      validation_state.implicit_operations_results :=
        Pervasives.op_at
          (Apply_results.pack_migration_operation_results
            migration_operation_results) liquidity_baking_operations_results; |}.

Definition begin_construction
  (chain_id : Chain_id.t) (ctxt : Context.t) (predecessor_timestamp : Time.t)
  (predecessor_level : int32) (predecessor_fitness : Alpha_context.Fitness.raw)
  (predecessor : Block_hash.t) (timestamp : Time.t)
  (protocol_data : option block_header_data) (function_parameter : unit)
  : M? validation_state :=
  let '_ := function_parameter in
  let level := Int32.succ predecessor_level in
  let? '(ctxt, migration_balance_updates, migration_operation_results) :=
    Alpha_context.prepare ctxt level predecessor_timestamp timestamp in
  let? predecessor_level := Alpha_context.Raw_level.of_int32 predecessor_level
    in
  let predecessor_level := Alpha_context.Level.from_raw ctxt predecessor_level
    in
  let?
    '(mode, ctxt, liquidity_baking_operations_results,
      liquidity_baking_toggle_ema) :=
    match protocol_data with
    | None
      let? predecessor_round :=
        Alpha_context.Fitness.round_from_raw predecessor_fitness in
      let toggle_vote := Liquidity_baking_repr.LB_pass in
      let?
        '(ctxt, liquidity_baking_operations_results, liquidity_baking_toggle_ema) :=
        Apply.begin_partial_construction ctxt predecessor_level toggle_vote in
      let mode :=
        Partial_construction
          {| validation_mode.Partial_construction.predecessor := predecessor;
            validation_mode.Partial_construction.predecessor_fitness :=
              predecessor_fitness;
            validation_mode.Partial_construction.predecessor_level :=
              predecessor_level;
            validation_mode.Partial_construction.predecessor_round :=
              predecessor_round; |} in
      return?
        (mode, ctxt, liquidity_baking_operations_results,
          liquidity_baking_toggle_ema)
    | Some proto_header
      let? predecessor_round :=
        Alpha_context.Fitness.round_from_raw predecessor_fitness in
      let round_durations := Alpha_context.Constants.round_durations ctxt in
      let? round :=
        Alpha_context.Round.round_of_timestamp round_durations
          predecessor_timestamp predecessor_round timestamp in
      let? '{|
        Apply.full_construction.ctxt := ctxt;
          Apply.full_construction.protocol_data := protocol_data_contents;
          Apply.full_construction.payload_producer := payload_producer;
          Apply.full_construction.block_producer := block_producer;
          Apply.full_construction.round := round;
          Apply.full_construction.implicit_operations_results :=
            liquidity_baking_operations_results;
          Apply.full_construction.liquidity_baking_toggle_ema :=
            liquidity_baking_toggle_ema
          |} :=
        Apply.begin_full_construction ctxt predecessor_timestamp
          predecessor_level predecessor_round round
          proto_header.(Alpha_context.Block_header.protocol_data.contents) in
      let mode :=
        Full_construction
          {| validation_mode.Full_construction.predecessor := predecessor;
            validation_mode.Full_construction.payload_producer :=
              payload_producer;
            validation_mode.Full_construction.block_producer := block_producer;
            validation_mode.Full_construction.protocol_data_contents :=
              protocol_data_contents;
            validation_mode.Full_construction.level := level;
            validation_mode.Full_construction.round := round;
            validation_mode.Full_construction.predecessor_level :=
              predecessor_level;
            validation_mode.Full_construction.predecessor_round :=
              predecessor_round; |} in
      return?
        (mode, ctxt, liquidity_baking_operations_results,
          liquidity_baking_toggle_ema)
    end in
  return?
    {| validation_state.mode := mode; validation_state.chain_id := chain_id;
      validation_state.ctxt := ctxt; validation_state.op_count := 0;
      validation_state.migration_balance_updates := migration_balance_updates;
      validation_state.liquidity_baking_toggle_ema :=
        liquidity_baking_toggle_ema;
      validation_state.implicit_operations_results :=
        Pervasives.op_at
          (Apply_results.pack_migration_operation_results
            migration_operation_results) liquidity_baking_operations_results; |}.

Definition apply_operation_with_mode
  (mode : Apply.apply_mode) (ctxt : Alpha_context.context)
  (chain_id : Chain_id.t) (data : validation_state) (op_count : int)
  (operation : operation) (payload_producer : Alpha_context.public_key_hash)
  : M? (validation_state × operation_receipt) :=
  let '{|
    Alpha_context.packed_operation.shell := shell;
      Alpha_context.packed_operation.protocol_data :=
        Alpha_context.Operation_data protocol_data
      |} := operation in
  let operation :=
    {| Alpha_context.operation.shell := shell;
      Alpha_context.operation.protocol_data := protocol_data; |} in
  let? '(ctxt, result_value) :=
    Apply.apply_operation ctxt chain_id mode Script_ir_translator.Optimized
      payload_producer (Alpha_context.Operation.hash_value operation) operation
    in
  let op_count := op_count +i 1 in
  return?
    ((validation_state.with_op_count op_count
      (validation_state.with_ctxt ctxt data)),
      (Apply_results.Operation_metadata result_value)).

Definition apply_operation (function_parameter : validation_state)
  : Alpha_context.packed_operation M? (validation_state × operation_receipt) :=
  let
    '{|
      validation_state.mode := mode;
        validation_state.chain_id := chain_id;
        validation_state.ctxt := ctxt;
        validation_state.op_count := op_count
        |} as data := function_parameter in
  fun (operation : Alpha_context.packed_operation) ⇒
    match
      (mode,
        match mode with
        | Partial_application _
          Pervasives.not
            (List._exists (Compare.Int.equal 0)
              (Alpha_context.Operation.acceptable_passes operation))
        | _false
        end) with
    | (Partial_application _, true)
      let op_count := op_count +i 1 in
      return?
        ((validation_state.with_op_count op_count
          (validation_state.with_ctxt ctxt data)),
          Apply_results.No_operation_metadata)
    |
      (Partial_application {|
        validation_mode.Partial_application.block_header := {|
          Alpha_context.Block_header.t.shell := {|
            Block_header.shell_header.predecessor := predecessor
              |};
            Alpha_context.Block_header.t.protocol_data := {|
              Alpha_context.Block_header.protocol_data.contents := {|
                Alpha_context.Block_header.contents.payload_hash :=
                  payload_hash
                  |}
                |}
            |};
          validation_mode.Partial_application.fitness := fitness;
          validation_mode.Partial_application.payload_producer :=
            payload_producer;
          validation_mode.Partial_application.predecessor_level :=
            predecessor_level;
          validation_mode.Partial_application.predecessor_round :=
            predecessor_round
          |}, _)
      let locked_round := Alpha_context.Fitness.locked_round fitness in
      apply_operation_with_mode
        (Apply.Application
          {| Apply.apply_mode.Application.predecessor_block := predecessor;
            Apply.apply_mode.Application.payload_hash := payload_hash;
            Apply.apply_mode.Application.locked_round := locked_round;
            Apply.apply_mode.Application.predecessor_level := predecessor_level;
            Apply.apply_mode.Application.predecessor_round := predecessor_round;
            Apply.apply_mode.Application.round :=
              Alpha_context.Fitness.round fitness; |}) ctxt chain_id data
        op_count operation payload_producer
    |
      (Application {|
        validation_mode.Application.block_header := {|
          Alpha_context.Block_header.t.shell := {|
            Block_header.shell_header.predecessor := predecessor
              |};
            Alpha_context.Block_header.t.protocol_data := {|
              Alpha_context.Block_header.protocol_data.contents := {|
                Alpha_context.Block_header.contents.payload_hash :=
                  payload_hash
                  |}
                |}
            |};
          validation_mode.Application.fitness := fitness;
          validation_mode.Application.payload_producer := payload_producer;
          validation_mode.Application.predecessor_round := predecessor_round;
          validation_mode.Application.predecessor_level := predecessor_level
          |}, _)
      let locked_round := Alpha_context.Fitness.locked_round fitness in
      apply_operation_with_mode
        (Apply.Application
          {| Apply.apply_mode.Application.predecessor_block := predecessor;
            Apply.apply_mode.Application.payload_hash := payload_hash;
            Apply.apply_mode.Application.locked_round := locked_round;
            Apply.apply_mode.Application.predecessor_level := predecessor_level;
            Apply.apply_mode.Application.predecessor_round := predecessor_round;
            Apply.apply_mode.Application.round :=
              Alpha_context.Fitness.round fitness; |}) ctxt chain_id data
        op_count operation payload_producer
    |
      (Partial_construction {|
        validation_mode.Partial_construction.predecessor_fitness :=
          predecessor_fitness;
          validation_mode.Partial_construction.predecessor_level :=
            predecessor_level;
          validation_mode.Partial_construction.predecessor_round :=
            predecessor_round
          |}, _)
      let? grand_parent_round :=
        Alpha_context.Fitness.predecessor_round_from_raw predecessor_fitness in
      apply_operation_with_mode
        (Apply.Partial_construction
          {|
            Apply.apply_mode.Partial_construction.predecessor_level :=
              predecessor_level;
            Apply.apply_mode.Partial_construction.predecessor_round :=
              predecessor_round;
            Apply.apply_mode.Partial_construction.grand_parent_round :=
              grand_parent_round; |}) ctxt chain_id data op_count operation
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero)
    |
      (Full_construction {|
        validation_mode.Full_construction.predecessor := predecessor;
          validation_mode.Full_construction.payload_producer := payload_producer;
          validation_mode.Full_construction.protocol_data_contents := {|
            Alpha_context.Block_header.contents.payload_hash := payload_hash
              |};
          validation_mode.Full_construction.round := round;
          validation_mode.Full_construction.predecessor_level :=
            predecessor_level;
          validation_mode.Full_construction.predecessor_round :=
            predecessor_round
          |}, _)
      apply_operation_with_mode
        (Apply.Full_construction
          {|
            Apply.apply_mode.Full_construction.predecessor_block := predecessor;
            Apply.apply_mode.Full_construction.payload_hash := payload_hash;
            Apply.apply_mode.Full_construction.predecessor_level :=
              predecessor_level;
            Apply.apply_mode.Full_construction.predecessor_round :=
              predecessor_round;
            Apply.apply_mode.Full_construction.round := round; |}) ctxt chain_id
        data op_count operation payload_producer
    end.

Definition cache_nonce_from_block_header
  (shell : Block_header.shell_header)
  (contents : Alpha_context.Block_header.contents) : bytes :=
  let shell :=
    {| Block_header.shell_header.level := 0;
      Block_header.shell_header.proto_level := 0;
      Block_header.shell_header.predecessor :=
        shell.(Block_header.shell_header.predecessor);
      Block_header.shell_header.timestamp := Time.of_seconds 0;
      Block_header.shell_header.validation_passes := 0;
      Block_header.shell_header.operations_hash :=
        shell.(Block_header.shell_header.operations_hash);
      Block_header.shell_header.fitness := nil;
      Block_header.shell_header.context := Context_hash.zero; |} in
  let contents :=
    Alpha_context.Block_header.contents.with_proof_of_work_nonce
      (Bytes.make Constants_repr.proof_of_work_nonce_size "0" % char)
      (Alpha_context.Block_header.contents.with_payload_hash
        Block_payload_hash.zero contents) in
  let protocol_data :=
    {| Alpha_context.Block_header.protocol_data.contents := contents;
      Alpha_context.Block_header.protocol_data.signature := Signature.zero; |}
    in
  let x_value :=
    {| Alpha_context.Block_header.t.shell := shell;
      Alpha_context.Block_header.t.protocol_data := protocol_data; |} in
  Block_hash.to_bytes (Alpha_context.Block_header.hash_value x_value).

Definition finalize_block_application
  (ctxt : Alpha_context.context) (round : Alpha_context.Round.t)
  (cache_nonce : Bytes.t)
  (finalize_application_mode : Apply.finalize_application_mode)
  (protocol_data : Alpha_context.Block_header.contents)
  (payload_producer : Alpha_context.public_key_hash)
  (block_producer : Alpha_context.public_key_hash)
  (liquidity_baking_toggle_ema : Alpha_context.Liquidity_baking.Toggle_EMA.t)
  (implicit_operations_results :
    list Apply_results.packed_successful_manager_operation_result)
  (predecessor : Block_hash.t)
  (migration_balance_updates : Alpha_context.Receipt.balance_updates)
  (op_count : int)
  : M? (Updater.validation_result × Apply_results.block_metadata) :=
  let? '(ctxt, fitness, receipt) :=
    Apply.finalize_application ctxt finalize_application_mode protocol_data
      payload_producer block_producer liquidity_baking_toggle_ema
      implicit_operations_results round predecessor migration_balance_updates in
  let ctxt := Alpha_context.Cache.Admin.sync ctxt cache_nonce in
  let level := Alpha_context.Level.current ctxt in
  let raw_level :=
    Alpha_context.Raw_level.to_int32 level.(Alpha_context.Level.t.level) in
  let commit_message :=
    Format.asprintf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "lvl "
          (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            (CamlinternalFormatBasics.String_literal ", fit:"
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.String_literal ", round "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", "
                      (CamlinternalFormatBasics.Int
                        CamlinternalFormatBasics.Int_d
                        CamlinternalFormatBasics.No_padding
                        CamlinternalFormatBasics.No_precision
                        (CamlinternalFormatBasics.String_literal " ops"
                          CamlinternalFormatBasics.End_of_format)))))))))
        "lvl %ld, fit:%a, round %a, %d ops") raw_level Alpha_context.Fitness.pp
      fitness Alpha_context.Round.pp round op_count in
  let validation_result :=
    Alpha_context.finalize (Some commit_message) ctxt
      (Alpha_context.Fitness.to_raw fitness) in
  return? (validation_result, receipt).

Init function; without side-effects in Coq
Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "main.missing_shell_header"
    "Missing shell_header during finalisation of a block"
    "During finalisation of a block header in Application mode or Full construction mode, a shell header should be provided so that a cache nonce can be computed."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "No shell header provided during the finalisation of a block."
                CamlinternalFormatBasics.End_of_format)
              "No shell header provided during the finalisation of a block.")))
    Data_encoding.unit_value
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Missing_shell_header" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Missing_shell_header" unit tt).

Definition finalize_block (function_parameter : validation_state)
  : option Block_header.shell_header
  M? (Updater.validation_result × Apply_results.block_metadata) :=
  let '{|
    validation_state.mode := mode;
      validation_state.ctxt := ctxt;
      validation_state.op_count := op_count;
      validation_state.migration_balance_updates := migration_balance_updates;
      validation_state.liquidity_baking_toggle_ema :=
        liquidity_baking_toggle_ema;
      validation_state.implicit_operations_results :=
        implicit_operations_results
      |} := function_parameter in
  fun (shell_header : option Block_header.shell_header) ⇒
    match mode with
    |
      Partial_construction {|
        validation_mode.Partial_construction.predecessor_fitness :=
          predecessor_fitness
          |} ⇒
      let? voting_period_info :=
        Alpha_context.Voting_period.get_rpc_current_info ctxt in
      let level_info := Alpha_context.Level.current ctxt in
      let fitness := predecessor_fitness in
      let ctxt := Alpha_context.finalize None ctxt fitness in
      return?
        (ctxt,
          {|
            Apply_results.block_metadata.proposer :=
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero);
            Apply_results.block_metadata.baker :=
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero);
            Apply_results.block_metadata.level_info := level_info;
            Apply_results.block_metadata.voting_period_info :=
              voting_period_info;
            Apply_results.block_metadata.nonce_hash := None;
            Apply_results.block_metadata.consumed_gas :=
              Alpha_context.Gas.Arith.zero;
            Apply_results.block_metadata.deactivated := nil;
            Apply_results.block_metadata.balance_updates :=
              migration_balance_updates;
            Apply_results.block_metadata.liquidity_baking_toggle_ema :=
              liquidity_baking_toggle_ema;
            Apply_results.block_metadata.implicit_operations_results :=
              implicit_operations_results; |})
    |
      Partial_application {|
        validation_mode.Partial_application.fitness := fitness;
          validation_mode.Partial_application.block_producer := block_producer
          |} ⇒
      let level := Alpha_context.Level.current ctxt in
      let included_endorsements :=
        Alpha_context.Consensus.current_endorsement_power ctxt in
      let minimum := Alpha_context.Constants.consensus_threshold ctxt in
      let? endorsements_required :=
        Apply.are_endorsements_required ctxt level.(Alpha_context.Level.t.level)
        in
      let? '_ :=
        if endorsements_required then
          Apply.check_minimum_endorsements included_endorsements minimum
        else
          Result.return_unit in
      let? voting_period_info :=
        Alpha_context.Voting_period.get_rpc_current_info ctxt in
      let level_info := Alpha_context.Level.current ctxt in
      let ctxt :=
        Alpha_context.finalize None ctxt (Alpha_context.Fitness.to_raw fitness)
        in
      return?
        (ctxt,
          {|
            Apply_results.block_metadata.proposer :=
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero);
            Apply_results.block_metadata.baker := block_producer;
            Apply_results.block_metadata.level_info := level_info;
            Apply_results.block_metadata.voting_period_info :=
              voting_period_info;
            Apply_results.block_metadata.nonce_hash := None;
            Apply_results.block_metadata.consumed_gas :=
              Alpha_context.Gas.Arith.zero;
            Apply_results.block_metadata.deactivated := nil;
            Apply_results.block_metadata.balance_updates :=
              migration_balance_updates;
            Apply_results.block_metadata.liquidity_baking_toggle_ema :=
              liquidity_baking_toggle_ema;
            Apply_results.block_metadata.implicit_operations_results :=
              implicit_operations_results; |})
    |
      Application {|
        validation_mode.Application.block_header := {|
          Alpha_context.Block_header.t.shell := shell;
            Alpha_context.Block_header.t.protocol_data := {|
              Alpha_context.Block_header.protocol_data.contents := protocol_data
                |}
            |};
          validation_mode.Application.fitness := fitness;
          validation_mode.Application.payload_producer := payload_producer;
          validation_mode.Application.block_producer := block_producer
          |} ⇒
      let round := Alpha_context.Fitness.round fitness in
      let cache_nonce := cache_nonce_from_block_header shell protocol_data in
      finalize_block_application ctxt round cache_nonce
        (Apply.Finalize_application fitness) protocol_data payload_producer
        block_producer liquidity_baking_toggle_ema implicit_operations_results
        shell.(Block_header.shell_header.predecessor) migration_balance_updates
        op_count
    |
      Full_construction {|
        validation_mode.Full_construction.predecessor := predecessor;
          validation_mode.Full_construction.payload_producer := payload_producer;
          validation_mode.Full_construction.block_producer := block_producer;
          validation_mode.Full_construction.protocol_data_contents :=
            protocol_data_contents;
          validation_mode.Full_construction.level := level;
          validation_mode.Full_construction.round := round;
          validation_mode.Full_construction.predecessor_round :=
            predecessor_round
          |} ⇒
      let? shell_header :=
        Option.value_e shell_header
          (Error_monad.trace_of_error
            (Build_extensible "Missing_shell_header" unit tt)) in
      let cache_nonce :=
        cache_nonce_from_block_header shell_header protocol_data_contents in
      let? level := Alpha_context.Raw_level.of_int32 level in
      finalize_block_application ctxt round cache_nonce
        (Apply.Finalize_full_construction
          {|
            Apply.finalize_application_mode.Finalize_full_construction.level :=
              level;
            Apply.finalize_application_mode.Finalize_full_construction.predecessor_round
              := predecessor_round; |}) protocol_data_contents payload_producer
        block_producer liquidity_baking_toggle_ema implicit_operations_results
        predecessor migration_balance_updates op_count
    end.

Definition relative_position_within_block
  (op1 : Alpha_context.packed_operation) (op2 : Alpha_context.packed_operation)
  : int :=
  let 'Alpha_context.Operation_data op1 :=
    op1.(Alpha_context.packed_operation.protocol_data) in
  let 'Alpha_context.Operation_data op2 :=
    op2.(Alpha_context.packed_operation.protocol_data) in
  match
    (op1.(Alpha_context.protocol_data.contents),
      op2.(Alpha_context.protocol_data.contents)) with
  |
    (Alpha_context.Single (Alpha_context.Preendorsement _),
      Alpha_context.Single (Alpha_context.Preendorsement _)) ⇒ 0
  | (Alpha_context.Single (Alpha_context.Preendorsement _), _) ⇒ (-1)
  | (_, Alpha_context.Single (Alpha_context.Preendorsement _)) ⇒ 1
  |
    (Alpha_context.Single (Alpha_context.Endorsement _),
      Alpha_context.Single (Alpha_context.Endorsement _)) ⇒ 0
  | (Alpha_context.Single (Alpha_context.Endorsement _), _) ⇒ (-1)
  | (_, Alpha_context.Single (Alpha_context.Endorsement _)) ⇒ 1
  |
    (Alpha_context.Single (Alpha_context.Seed_nonce_revelation _),
      Alpha_context.Single (Alpha_context.Seed_nonce_revelation _)) ⇒ 0
  | (_, Alpha_context.Single (Alpha_context.Seed_nonce_revelation _)) ⇒ 1
  | (Alpha_context.Single (Alpha_context.Seed_nonce_revelation _), _) ⇒ (-1)
  |
    (Alpha_context.Single (Alpha_context.Double_preendorsement_evidence _),
      Alpha_context.Single (Alpha_context.Double_preendorsement_evidence _))
    0
  | (_, Alpha_context.Single (Alpha_context.Double_preendorsement_evidence _))
    ⇒ 1
  | (Alpha_context.Single (Alpha_context.Double_preendorsement_evidence _), _)
    ⇒ (-1)
  |
    (Alpha_context.Single (Alpha_context.Double_endorsement_evidence _),
      Alpha_context.Single (Alpha_context.Double_endorsement_evidence _)) ⇒ 0
  | (_, Alpha_context.Single (Alpha_context.Double_endorsement_evidence _)) ⇒ 1
  | (Alpha_context.Single (Alpha_context.Double_endorsement_evidence _), _)
    (-1)
  |
    (Alpha_context.Single (Alpha_context.Double_baking_evidence _),
      Alpha_context.Single (Alpha_context.Double_baking_evidence _)) ⇒ 0
  | (_, Alpha_context.Single (Alpha_context.Double_baking_evidence _)) ⇒ 1
  | (Alpha_context.Single (Alpha_context.Double_baking_evidence _), _) ⇒ (-1)
  |
    (Alpha_context.Single (Alpha_context.Activate_account _),
      Alpha_context.Single (Alpha_context.Activate_account _)) ⇒ 0
  | (_, Alpha_context.Single (Alpha_context.Activate_account _)) ⇒ 1
  | (Alpha_context.Single (Alpha_context.Activate_account _), _) ⇒ (-1)
  |
    (Alpha_context.Single (Alpha_context.Proposals _),
      Alpha_context.Single (Alpha_context.Proposals _)) ⇒ 0
  | (_, Alpha_context.Single (Alpha_context.Proposals _)) ⇒ 1
  | (Alpha_context.Single (Alpha_context.Proposals _), _) ⇒ (-1)
  |
    (Alpha_context.Single (Alpha_context.Ballot _),
      Alpha_context.Single (Alpha_context.Ballot _)) ⇒ 0
  | (_, Alpha_context.Single (Alpha_context.Ballot _)) ⇒ 1
  | (Alpha_context.Single (Alpha_context.Ballot _), _) ⇒ (-1)
  |
    (Alpha_context.Single (Alpha_context.Failing_noop _),
      Alpha_context.Single (Alpha_context.Failing_noop _)) ⇒ 0
  | (_, Alpha_context.Single (Alpha_context.Failing_noop _)) ⇒ 1
  | (Alpha_context.Single (Alpha_context.Failing_noop _), _) ⇒ (-1)
  |
    (Alpha_context.Single (Alpha_context.Manager_operation op1),
      Alpha_context.Single (Alpha_context.Manager_operation op2))
    Z.compare op1.(Alpha_context.contents.Manager_operation.counter)
      op2.(Alpha_context.contents.Manager_operation.counter)
  |
    (Alpha_context.Cons (Alpha_context.Manager_operation op1) _,
      Alpha_context.Single (Alpha_context.Manager_operation op2))
    Z.compare op1.(Alpha_context.contents.Manager_operation.counter)
      op2.(Alpha_context.contents.Manager_operation.counter)
  |
    (Alpha_context.Single (Alpha_context.Manager_operation op1),
      Alpha_context.Cons (Alpha_context.Manager_operation op2) _)
    Z.compare op1.(Alpha_context.contents.Manager_operation.counter)
      op2.(Alpha_context.contents.Manager_operation.counter)
  |
    (Alpha_context.Cons (Alpha_context.Manager_operation op1) _,
      Alpha_context.Cons (Alpha_context.Manager_operation op2) _)
    Z.compare op1.(Alpha_context.contents.Manager_operation.counter)
      op2.(Alpha_context.contents.Manager_operation.counter)
  | _unreachable_gadt_branch
  end.

Definition init_value
  (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 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 None ctxt true allow_forged_in_storage
        script in
    let? '(storage_value, lazy_storage_diff, ctxt) :=
      Script_ir_translator.extract_lazy_storage_diff ctxt
        Script_ir_translator.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_translator.Optimized
        parsed_script.(Script_typed_ir.script.Script.storage_type) storage_value
      in
    let storage_value :=
      Alpha_context.Script.lazy_expr_value
        (Micheline.strip_locations 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 ctxt typecheck level timestamp
    in
  let? ctxt := Ticket_balance_migration_for_j.init_value ctxt in
  let cache_nonce :=
    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
  return?
    (Alpha_context.finalize None ctxt
      (Alpha_context.Fitness.to_raw init_fitness)).

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).

Definition check_manager_signature (function_parameter : validation_state)
  : Alpha_context.contents_list Alpha_context.operation M? unit :=
  let '{|
    validation_state.chain_id := chain_id; validation_state.ctxt := ctxt |} :=
    function_parameter in
  fun (op : Alpha_context.contents_list) ⇒
    fun (raw_op : Alpha_context.operation) ⇒
      Apply.check_manager_signature ctxt chain_id op raw_op.

Definition precheck_manager (function_parameter : validation_state)
  : Alpha_context.contents_list M? unit :=
  let '{| validation_state.ctxt := ctxt |} := function_parameter in
  fun (op : Alpha_context.contents_list) ⇒
    let? function_parameter := Apply.precheck_manager_contents_list ctxt op true
      in
    return?
      (let '_ := function_parameter in
      tt).