🎛️ 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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Period_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_repr.parametric.preserved_cycles).

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

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

Definition blocks_per_stake_snapshot (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.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_repr.parametric.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_repr.parametric.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_repr.parametric.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_repr.parametric.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_repr.parametric.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_repr.parametric.proof_of_work_threshold).

Definition tokens_per_roll (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tokens_per_roll).

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

Definition origination_size (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.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_repr.parametric.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_repr.parametric.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_repr.parametric.endorsing_reward_per_slot).

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

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

Definition min_proposal_quorum (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.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_repr.parametric.liquidity_baking_subsidy).

Definition liquidity_baking_sunset_level (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.liquidity_baking_sunset_level).

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

Definition parametric_value (c_value : Raw_context.t)
  : Constants_repr.parametric := Raw_context.constants c_value.

Definition minimal_block_delay (c_value : Raw_context.t) : Period_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.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_repr.parametric.delay_increment_per_round).

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

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

Definition minimal_participation_ratio (c_value : Raw_context.t)
  : Constants_repr.ratio :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.minimal_participation_ratio).

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

Definition frozen_deposits_percentage (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.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_repr.parametric.double_baking_punishment).

Definition tx_rollup_enable (c_value : Raw_context.t) : bool :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_enable).

Definition tx_rollup_sunset_level (c_value : Raw_context.t) : int32 :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_sunset_level).

Definition tx_rollup_origination_size (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_origination_size).

Definition tx_rollup_hard_size_limit_per_inbox (c_value : Raw_context.t)
  : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_hard_size_limit_per_inbox).

Definition tx_rollup_hard_size_limit_per_message (c_value : Raw_context.t)
  : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_hard_size_limit_per_message).

Definition tx_rollup_max_withdrawals_per_batch (c_value : Raw_context.t)
  : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_max_withdrawals_per_batch).

Definition tx_rollup_commitment_bond (c_value : Raw_context.t) : Tez_repr.t :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_commitment_bond).

Definition tx_rollup_finality_period (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_finality_period).

Definition tx_rollup_withdraw_period (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_withdraw_period).

Definition tx_rollup_max_inboxes_count (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_max_inboxes_count).

Definition tx_rollup_max_messages_per_inbox (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_max_messages_per_inbox).

Definition tx_rollup_max_commitments_count (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_max_commitments_count).

Definition tx_rollup_cost_per_byte_ema_factor (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_cost_per_byte_ema_factor).

Definition tx_rollup_max_ticket_payload_size (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_max_ticket_payload_size).

Definition tx_rollup_rejection_max_proof_size (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.tx_rollup_rejection_max_proof_size).

Definition ratio_of_frozen_deposits_slashed_per_double_endorsement
  (c_value : Raw_context.t) : Constants_repr.ratio :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.ratio_of_frozen_deposits_slashed_per_double_endorsement).

Definition sc_rollup_enable (c_value : Raw_context.t) : bool :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.sc_rollup_enable).

Definition sc_rollup_origination_size (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.sc_rollup_origination_size).

Definition sc_rollup_challenge_window_in_blocks (c_value : Raw_context.t)
  : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.sc_rollup_challenge_window_in_blocks).

Definition sc_rollup_max_available_messages (c_value : Raw_context.t) : int :=
  let constants := Raw_context.constants c_value in
  constants.(Constants_repr.parametric.sc_rollup_max_available_messages).