Skip to main content

🎛️ Constants_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Tez_repr.

Definition preserved_cycles (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.preserved_cycles).

Definition blocks_per_cycle (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.blocks_per_cycle).

Definition blocks_per_commitment (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.blocks_per_commitment).

Definition nonce_revelation_threshold (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.nonce_revelation_threshold).

Definition blocks_per_stake_snapshot (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.blocks_per_stake_snapshot).

Definition cycles_per_voting_period (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.cycles_per_voting_period).

Definition hard_gas_limit_per_operation (c_value : Raw_context.t)
  : Gas_limit_repr.Arith.integral :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.hard_gas_limit_per_operation).

Definition hard_gas_limit_per_block (c_value : Raw_context.t)
  : Gas_limit_repr.Arith.integral :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.hard_gas_limit_per_block).

Definition cost_per_byte (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.cost_per_byte).

Definition hard_storage_limit_per_operation (c_value : Raw_context.t) : Z.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.hard_storage_limit_per_operation).

Definition proof_of_work_threshold (c_value : Raw_context.t) : int64 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.proof_of_work_threshold).

Definition minimal_stake (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.minimal_stake).

Definition vdf_difficulty (c_value : Raw_context.t) : int64 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.vdf_difficulty).

Definition seed_nonce_revelation_tip (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.seed_nonce_revelation_tip).

Definition origination_size (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.origination_size).

Definition baking_reward_fixed_portion (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.baking_reward_fixed_portion).

Definition baking_reward_bonus_per_slot (c_value : Raw_context.t)
  : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.baking_reward_bonus_per_slot).

Definition endorsing_reward_per_slot (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.endorsing_reward_per_slot).

Definition quorum_min (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.quorum_min).

Definition quorum_max (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.quorum_max).

Definition min_proposal_quorum (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.min_proposal_quorum).

Definition liquidity_baking_subsidy (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.liquidity_baking_subsidy).

Definition liquidity_baking_toggle_ema_threshold (c_value : Raw_context.t)
  : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.liquidity_baking_toggle_ema_threshold).

Definition parametric_value (c_value : Raw_context.t)
  : Constants_parametric_repr.t := Raw_context.constants c_value.

Definition tx_rollup (c_value : Raw_context.t)
  : Constants_parametric_repr.tx_rollup :=
  (Raw_context.constants c_value).(Constants_parametric_repr.t.tx_rollup).

Definition sc_rollup (c_value : Raw_context.t)
  : Constants_parametric_repr.sc_rollup :=
  (Raw_context.constants c_value).(Constants_parametric_repr.t.sc_rollup).

Definition minimal_block_delay (c_value : Raw_context.t) : Period_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.minimal_block_delay).

Definition delay_increment_per_round (c_value : Raw_context.t)
  : Period_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.delay_increment_per_round).

Definition consensus_committee_size (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.consensus_committee_size).

Definition consensus_threshold (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.consensus_threshold).

Definition minimal_participation_ratio (c_value : Raw_context.t)
  : Ratio_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.minimal_participation_ratio).

Definition max_slashing_period (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.max_slashing_period).

Definition frozen_deposits_percentage (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.frozen_deposits_percentage).

Definition double_baking_punishment (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.double_baking_punishment).

Definition tx_rollup_enable (c_value : Raw_context.t) : bool :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.enable).

Definition tx_rollup_sunset_level (c_value : Raw_context.t) : int32 :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.sunset_level).

Definition tx_rollup_origination_size (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.origination_size).

Definition tx_rollup_hard_size_limit_per_inbox (c_value : Raw_context.t)
  : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.hard_size_limit_per_inbox).

Definition tx_rollup_hard_size_limit_per_message (c_value : Raw_context.t)
  : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.hard_size_limit_per_message).

Definition tx_rollup_max_withdrawals_per_batch (c_value : Raw_context.t)
  : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.max_withdrawals_per_batch).

Definition tx_rollup_commitment_bond (c_value : Raw_context.t) : Tez_repr.t :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.commitment_bond).

Definition tx_rollup_finality_period (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.finality_period).

Definition tx_rollup_withdraw_period (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.withdraw_period).

Definition tx_rollup_max_inboxes_count (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.max_inboxes_count).

Definition tx_rollup_max_messages_per_inbox (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.max_messages_per_inbox).

Definition tx_rollup_max_commitments_count (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.max_commitments_count).

Definition tx_rollup_cost_per_byte_ema_factor (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.cost_per_byte_ema_factor).

Definition tx_rollup_max_ticket_payload_size (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.max_ticket_payload_size).

Definition tx_rollup_rejection_max_proof_size (c_value : Raw_context.t) : int :=
  let tx_rollup := Raw_context.tx_rollup c_value in
  tx_rollup.(Constants_parametric_repr.tx_rollup.rejection_max_proof_size).

Definition ratio_of_frozen_deposits_slashed_per_double_endorsement
  (c_value : Raw_context.t) : Ratio_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.ratio_of_frozen_deposits_slashed_per_double_endorsement).

Definition testnet_dictator (c_value : Raw_context.t)
  : option Signature.public_key_hash :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.testnet_dictator).

Definition sc_rollup_enable (c_value : Raw_context.t) : bool :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.enable).

Definition sc_rollup_origination_size (c_value : Raw_context.t) : int :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.origination_size).

Definition sc_rollup_challenge_window_in_blocks (c_value : Raw_context.t)
  : int :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.challenge_window_in_blocks).

Definition sc_rollup_max_number_of_messages_per_commitment_period
  (c_value : Raw_context.t) : int :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.max_number_of_messages_per_commitment_period).

Definition sc_rollup_stake_amount (c_value : Raw_context.t) : Tez_repr.t :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.stake_amount).

Definition sc_rollup_commitment_period_in_blocks (c_value : Raw_context.t)
  : int :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.commitment_period_in_blocks).

Definition sc_rollup_max_lookahead_in_blocks (c_value : Raw_context.t)
  : int32 :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.max_lookahead_in_blocks).

Definition sc_rollup_max_active_outbox_levels (c_value : Raw_context.t)
  : int32 :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.max_active_outbox_levels).

Definition sc_rollup_max_outbox_messages_per_level (c_value : Raw_context.t)
  : int :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.max_outbox_messages_per_level).

Definition sc_rollup_number_of_sections_in_dissection (c_value : Raw_context.t)
  : int :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.number_of_sections_in_dissection).

Definition sc_rollup_timeout_period_in_blocks (c_value : Raw_context.t) : int :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.timeout_period_in_blocks).

Definition max_number_of_stored_cemented_commitments (c_value : Raw_context.t)
  : int :=
  let sc_rollup := Raw_context.sc_rollup c_value in
  sc_rollup.(Constants_parametric_repr.sc_rollup.max_number_of_stored_cemented_commitments).

Definition dal_number_of_slots (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.dal).(Constants_parametric_repr.dal.number_of_slots).

Definition dal_enable (c_value : Raw_context.t) : bool :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_parametric_repr.t.dal).(Constants_parametric_repr.dal.feature_enable).

Definition zk_rollup_enable (c_value : Raw_context.t) : bool :=
  let zk_rollup := Raw_context.zk_rollup c_value in
  zk_rollup.(Constants_parametric_repr.zk_rollup.enable).

Definition zk_rollup_min_pending_to_process (c_value : Raw_context.t) : int :=
  let zk_rollup := Raw_context.zk_rollup c_value in
  zk_rollup.(Constants_parametric_repr.zk_rollup.min_pending_to_process).

Definition zk_rollup_origination_size (c_value : Raw_context.t) : int :=
  let zk_rollup := Raw_context.zk_rollup c_value in
  zk_rollup.(Constants_parametric_repr.zk_rollup.origination_size).