🖼️ Raw_context.v

Simulations

See code, See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Simulations.Storage_description.
Require TezosOfOCaml.Proto_alpha.Simulations.Storage_functors.
Require TezosOfOCaml.Proto_alpha.Simulations.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Simulations.Raw_context_generated.
Require TezosOfOCaml.Proto_alpha.Storage.

Include the generated context so we have the [t] type. The projections are included also

Include Raw_context_generated.

Definition to_remaining_gas_operation (r : t)
  : Gas_limit_repr.Arith.fp :=
  r.(config).(config.remaining_operation_gas).

A context without any value.

Parameter empty_context : Context.t.

Conversion back to the type [Context.t].

Definition to_context (x : standalone.t) : Context.t :=
  let ctxt := empty_context in
  (* version *)
  let ctxt :=
    Context.add ctxt Raw_context.version_key Raw_context.version_value in
  (* cycle_eras *)
  let ctxt :=
    let value :=
      Data_encoding.Binary.to_bytes_opt
        None Level_repr.cycle_eras_encoding x.(standalone.cycle_eras) in
    match value with
    | Some value ⇒ Context.add ctxt Raw_context.cycle_eras_key value
    | None ⇒ ctxt
    end in
  (* constants *)
  let ctxt :=
    let value :=
      Data_encoding.Binary.to_bytes_opt
        None Constants_parametric_repr.encoding x.(standalone.constants) in
    match value with
    | Some value ⇒ Context.add ctxt Raw_context.constants_key value
    | None ⇒ ctxt
    end in
  (* protocol_param: TODO *)
  ctxt.

Conversion back to the type [Raw_context.back].

Definition to_back (x : t) : Proto_alpha.Raw_context.back := {|
  Proto_alpha.Raw_context.back.context :=
    to_context x.(standalone);
  Proto_alpha.Raw_context.back.constants :=
    x.(config).(config.constants);
  Proto_alpha.Raw_context.back.round_durations :=
    x.(config).(config.round_durations);
  Proto_alpha.Raw_context.back.cycle_eras :=
    x.(config).(config.cycle_eras);
  Proto_alpha.Raw_context.back.level :=
    x.(config).(config.level);
  Proto_alpha.Raw_context.back.predecessor_timestamp :=
    x.(config).(config.predecessor_timestamp);
  Proto_alpha.Raw_context.back.timestamp :=
    x.(config).(config.timestamp);
  Proto_alpha.Raw_context.back.fees :=
    x.(config).(config.fees);
  Proto_alpha.Raw_context.back.origination_nonce :=
    x.(config).(config.origination_nonce);
  Proto_alpha.Raw_context.back.temporary_lazy_storage_ids :=
    x.(config).(config.temporary_lazy_storage_ids);
  Proto_alpha.Raw_context.back.internal_nonce :=
    x.(config).(config.internal_nonce);
  Proto_alpha.Raw_context.back.internal_nonces_used :=
    x.(config).(config.internal_nonces_used);
  Proto_alpha.Raw_context.back.remaining_block_gas :=
    x.(config).(config.remaining_block_gas);
  Proto_alpha.Raw_context.back.unlimited_operation_gas :=
    x.(config).(config.unlimited_operation_gas);
  Proto_alpha.Raw_context.back.consensus :=
    x.(config).(config.consensus);
  Proto_alpha.Raw_context.back.non_consensus_operations_rev :=
    x.(config).(config.non_consensus_operations_rev);
  Proto_alpha.Raw_context.back.dictator_proposal_seen :=
    x.(config).(config.dictator_proposal_seen);
  Proto_alpha.Raw_context.back.sampler_state :=
    x.(config).(config.sampler_state);
  Proto_alpha.Raw_context.back.stake_distribution_for_current_cycle :=
    x.(config).(config.stake_distribution_for_current_cycle);
  Proto_alpha.Raw_context.back.tx_rollup_current_messages :=
    x.(config).(config.tx_rollup_current_messages);
  Proto_alpha.Raw_context.back.sc_rollup_current_messages :=
    x.(config).(config.sc_rollup_current_messages);
  Proto_alpha.Raw_context.back.dal_slot_fee_market :=
    x.(config).(config.dal_slot_fee_market);
  Proto_alpha.Raw_context.back.dal_attestation_slot_accountability :=
    x.(config).(config.dal_attestation_slot_accountability);
  Proto_alpha.Raw_context.back.dal_committee :=
    x.(config).(config.dal_committee);
|}.

Conversion back to the type [Raw_context.t].

Definition to_t (x : t) : Proto_alpha.Raw_context.t :=
  {|
    Proto_alpha.Raw_context.t.remaining_operation_gas :=
      to_remaining_gas_operation x;
    Proto_alpha.Raw_context.t.back :=
      to_back x;
  |}.