🖼️ Raw_context_aux.v

Simulations

Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Raw_context.

Simulation of the context, in-memory fields

Module config.
  Record t : Set := {
    remaining_operation_gas : Gas_limit_repr.Arith.fp;
    constants : Constants_parametric_repr.t;
    round_durations : Round_repr.Durations.t;
    cycle_eras : Level_repr.cycle_eras;
    level : Level_repr.t;
    predecessor_timestamp : Time.t;
    timestamp : Time.t;
    fees : Tez_repr.t;
    origination_nonce : option Origination_nonce.t;
    temporary_lazy_storage_ids : Lazy_storage_kind.Temp_ids.t;
    internal_nonce : int;
    internal_nonces_used : Raw_context.Int_set.(_Set.S.t);
    remaining_block_gas : Gas_limit_repr.Arith.fp;
    unlimited_operation_gas : bool;
    consensus : Raw_context.Raw_consensus.t;
    non_consensus_operations_rev : list Operation_hash.t;
    dictator_proposal_seen : bool;
    sampler_state :
      Cycle_repr.Map.(Map.S.t)
        (Seed_repr.seed × Sampler.t Raw_context.consensus_pk);
    stake_distribution_for_current_cycle :
      option
        (Signature.Public_key_hash
          .(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
          Tez_repr.t);
    tx_rollup_current_messages :
      Tx_rollup_repr.Map.(Map.S.t) Tx_rollup_inbox_repr.Merkle.tree;
    sc_rollup_current_messages :
      option Sc_rollup_inbox_merkelized_payload_hashes_repr.t;
    dal_slot_fee_market : Dal_slot_repr.Slot_market.t;
    dal_attestation_slot_accountability : Dal_attestation_repr.Accountability.t;
    dal_committee : Proto_alpha.Raw_context.dal_committee;
  }.
End config.
Definition config := config.t.

Simulation of the context, fields used in [Proto_alpha.Raw_context] that are not part of any storage at [Proto_alpha.Storage]

Module standalone.
  Record t : Set := {
    cycle_eras : Level_repr.cycle_eras;
    constants : Constants_parametric_repr.t;
    protocol_param : option Parameters_repr.t;
  }.
End standalone.
Definition standalone := standalone.t.