🎛️ Constants_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Constants_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

Most of the functions in [Context_storage] module are projections the [ctxt.back.constants] field. This tactic works by destructing the context simulation up to the [constants] field and then applying it

#[local] Ltac ctxt_trivial :=
  match goal with
  | |- Raw_context.Valid.t ?ctxt → _ ⇒
      intros H_ctxt;
      Raw_context.Valid.destruct_rewrite H_ctxt
  end;
  destruct_by_type (Raw_context.Valid.simulation _);
  destruct_by_type (Raw_context.config.Valid.simulation _);
  apply_by_type (Constants_parametric_repr.Valid.t _).

The function [preserved_cycles] is valid

Lemma preserved_cycles_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.UInt8.Valid.t (Constants_storage.preserved_cycles ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [blocks_per_cycles] is valid

Lemma blocks_per_cycles_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t (Constants_storage.blocks_per_cycle ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [blocks_per_commitment] is valid

Lemma blocks_per_commitment_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t (Constants_storage.blocks_per_commitment ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [nonce_revelation_threshold] is valid

Lemma nonce_revelation_threshold_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.positive
    (Constants_storage.nonce_revelation_threshold ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [blocks_per_stake_snapshot] is valid

Lemma blocks_per_stake_snapshot_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t (Constants_storage.blocks_per_stake_snapshot ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [cycles_per_voting_period] is valid

Lemma cycles_per_voting_period_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t (Constants_storage.cycles_per_voting_period ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [hard_gas_limit_per_operation] is valid

Lemma hard_gas_limit_per_operation_is_valid ctxt :
  Raw_context.Valid.simulation ctxt →
  Saturation_repr.Valid.t
    ctxt.(Raw_context.config)
      .(Raw_context_aux.config.constants)
        .(Constants_parametric_repr.t.hard_gas_limit_per_operation).
Proof.
  intros [].
  destruct config, constants.
  unfold Gas_limit_repr.Arith.Integral.Valid.t in ×.
  lia.
Qed.

The function [hard_storage_limit_per_operation] is valid

Lemma hard_storage_limit_per_operation_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.positive
    (Constants_storage.hard_storage_limit_per_operation ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [proof_of_work_threshold] is valid

Lemma proof_of_work_threshold_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int64.Valid.t (Constants_storage.proof_of_work_threshold ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [minimal_stake] is valid

Lemma minimal_stake_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t (Constants_storage.minimal_stake ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [vdf_difficulty] is valid

Lemma vdf_difficulty_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int64.Valid.t (Constants_storage.vdf_difficulty ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [origination_size] is valid

Lemma origination_size_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t (Constants_storage.origination_size ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [hard_gas_limit_per_block] is valid

Lemma hard_gas_limit_per_block_is_valid ctxt :
  Raw_context.Valid.simulation ctxt →
  Saturation_repr.Valid.t
    ctxt.(Raw_context.config)
      .(Raw_context_aux.config.constants)
        .(Constants_parametric_repr.t.hard_gas_limit_per_block).
Proof.
  intros [].
  destruct config, constants.
  unfold Gas_limit_repr.Arith.Integral.Valid.t in ×.
  lia.
Qed.

The function [cost_per_byte] is valid

Lemma cost_per_byte_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.cost_per_byte ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [seed_nonce_revelation_tip] is valid

Lemma seed_nonce_revelation_tip_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.seed_nonce_revelation_tip ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [baking_reward_fixed_portion] is valid

Lemma baking_reward_fixed_portion_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.baking_reward_fixed_portion ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [baking_reward_bonus_per_slot] is valid

Lemma baking_reward_bonus_per_slot_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.baking_reward_bonus_per_slot ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [endorsing_reward_per_slot] is valid

Lemma endorsing_reward_per_slot_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.endorsing_reward_per_slot ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [min_proposal_quorum] is valid

Lemma min_proposal_quorum_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t (
      Constants_storage.min_proposal_quorum ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [quorum_min] is valid

Lemma quorum_min_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t (
      Constants_storage.quorum_min ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [quorum_max] is valid

Lemma quorum_max_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t (
      Constants_storage.quorum_max ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [liquidity_baking_subsidy] is valid

Lemma liquidity_baking_subsidy_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.liquidity_baking_subsidy ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [liquidity_baking_toggle_ema_threshold] is valid

Lemma liquidity_baking_toggle_ema_threshold_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t
    (Constants_storage.liquidity_baking_toggle_ema_threshold ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [parametric] is valid

Lemma parametric_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Constants_parametric_repr.Valid.t
    (Constants_storage.parametric_value ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup] is valid

Lemma tx_rollup_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Constants_parametric_repr.tx_rollup.Valid.t
    (Constants_storage.tx_rollup ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup] is valid

Lemma sc_rollup_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Constants_parametric_repr.sc_rollup.Valid.t
    (Constants_storage.sc_rollup ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [consensus_committee_size] is valid

Lemma consensus_committee_size_is_valid
  (ctxt : Proto_alpha.Raw_context.t)
  : Raw_context.Valid.t ctxt →
    Pervasives.Int31.Valid.positive
      (Constants_storage.consensus_committee_size ctxt).
Proof.
  ctxt_trivial.
Qed.

[concensus_threshold] is valid

Lemma consensus_threshold_is_valid (ctxt : Proto_alpha.Raw_context.t)
  : Raw_context.Valid.t ctxt →
    Pervasives.Int31.Valid.non_negative
      (Constants_storage.consensus_threshold ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [minimal_participation_ratio] is valid

Lemma minimal_participation_ratio_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Ratio_repr.Valid.t
    (Constants_storage.minimal_participation_ratio ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [max_slashing_period] is valid

Lemma max_slashing_period_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.positive
    (Constants_storage.max_slashing_period ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [frozen_deposits_percentage] is valid

Lemma frozen_deposits_percentage_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  (0 < Constants_storage.frozen_deposits_percentage ctxt ≤ 100).
Proof.
  ctxt_trivial.
Qed.

The function [double_baking_punishment] is valid

Lemma double_baking_punishment_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.double_baking_punishment ctxt).
Proof.
  ctxt_trivial.
Qed.

(* The function [tx_rollup_enable] returns bool, bools are always
   valid, so no need for [tx_rollup_enable_is_valid *)

The function [tx_rollup_sunset_level] is valid

Lemma tx_rollup_sunset_level_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t (Constants_storage.tx_rollup_sunset_level ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_origination_size] is valid

Lemma tx_rollup_origination_size_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_origination_size ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_hard_size_limit_per_inbox] is valid

Lemma tx_rollup_hard_size_limit_per_inbox_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_hard_size_limit_per_inbox ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_hard_size_limit_per_message] is valid

Lemma tx_rollup_hard_size_limit_per_message_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_hard_size_limit_per_message ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_max_withdrawals_per_batch] is valid

Lemma tx_rollup_max_withdrawals_per_batch_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_max_withdrawals_per_batch ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_commitment_bond] is valid.

Lemma tx_rollup_commitment_bond_is_valid c_value :
  Raw_context.Valid.t c_value →
  Tez_repr.Valid.t
    (Constants_storage.tx_rollup_commitment_bond c_value).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_finality_period] is valid

Lemma tx_rollup_finality_period_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_finality_period ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_withdraw_period_is_valid] is valid

Lemma tx_rollup_withdraw_period_is_valid_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_withdraw_period ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_max_inboxes_count] is valid

Lemma tx_rollup_max_inboxes_count_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_max_inboxes_count ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_max_messages_per_inbox] is valid

Lemma tx_rollup_max_messages_per_inbox_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_max_messages_per_inbox ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_max_commitments_count] is valid

Lemma tx_rollup_max_commitments_count_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_max_commitments_count ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_cost_per_byte_ema_factor] is valid

Lemma tx_rollup_cost_per_byte_ema_factor_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_cost_per_byte_ema_factor ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_max_ticket_payload_size] is valid

Lemma tx_rollup_max_ticket_payload_size_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_max_ticket_payload_size ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [tx_rollup_rejection_max_proof_size] is valid

Lemma tx_rollup_rejection_max_proof_size_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.tx_rollup_rejection_max_proof_size ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [ratio_of_frozen_deposits_slashed_per_double_endorsement] is valid

Lemma ratio_of_frozen_deposits_slashed_per_double_endorsement_is_valid
  ctxt :
  Raw_context.Valid.t ctxt →
  Ratio_repr.Valid.t
    (Constants_storage
      .ratio_of_frozen_deposits_slashed_per_double_endorsement ctxt).
Proof.
  ctxt_trivial.
Qed.

(* The function [testnet_dictator] returns [option Signature.public_key_hash],
    there is no validity predicate for hashes, so no
    [testnet_dictator_is_valid] lemma *)

(* The function [sc_rollup_enable] returns a bool, bools are always
   valid, so no [sc_rollup_enable_is_valid] lemma *)

The function [sc_rollup_origination_size] is valid

Lemma sc_rollup_origination_size_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.non_negative
    (Constants_storage.sc_rollup_origination_size ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_challenge_window_in_blocks] is valid

Lemma sc_rollup_challenge_window_in_blocks_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.non_negative
    (Constants_storage.sc_rollup_challenge_window_in_blocks ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_max_number_of_messages_per_commitment_period] is valid

Lemma sc_rollup_max_number_of_messages_per_commitment_period_is_valid
  ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.positive
    (Constants_storage
       .sc_rollup_max_number_of_messages_per_commitment_period ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_stake_amount] is valid

Lemma sc_rollup_stake_amount_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.sc_rollup_stake_amount ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_commitment_period_in_blocks] is valid

Lemma sc_rollup_commitment_period_in_blocks_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.positive
    (Constants_storage.sc_rollup_commitment_period_in_blocks ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_max_lookahead_in_blocks] is valid

Lemma sc_rollup_max_lookahead_in_blocks_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t
    (Constants_storage.sc_rollup_max_lookahead_in_blocks ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_max_active_outbox_levels] is valid

Lemma sc_rollup_max_active_outbox_levels_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Int32.Valid.t
    (Constants_storage.sc_rollup_max_active_outbox_levels ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_max_outbox_messages_per_level] is valid

Lemma sc_rollup_max_outbox_messages_per_level_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.sc_rollup_max_outbox_messages_per_level ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_number_of_sections_in_dissection] is valid

Lemma sc_rollup_number_of_sections_in_dissection_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.UInt8.Valid.t
    (Constants_storage.sc_rollup_number_of_sections_in_dissection
       ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [sc_rollup_timeout_period_in_blocks] is valid

Lemma sc_rollup_timeout_period_in_blocks_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.sc_rollup_timeout_period_in_blocks ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [max_number_of_stored_cemented_commitments] is valid

Lemma max_number_of_stored_cemented_commitments_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.positive
    (Constants_storage.max_number_of_stored_cemented_commitments ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [dal_number_of_slots] is valid

Lemma dal_number_of_slots_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.UInt8.Valid.positive
    (Constants_storage.dal_number_of_slots ctxt).
Proof.
Admitted.

(* The function [dal_enable] returns bool, which is always valid, so
   no need for a [dal_enable_is_valid] lemma *)

(* The function [zk_rollup_enable] returns bool, which is always
   valid, so no need for a [zk_rollup_enable_is_valid] lemma *)

The function [zk_rollup_min_pending_to_process] is valid

Lemma zk_rollup_min_pending_to_process_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.zk_rollup_min_pending_to_process ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [zk_rollup_origination_size] is valid

Lemma zk_rollup_origination_size_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Pervasives.Int31.Valid.t
    (Constants_storage.zk_rollup_origination_size ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [minimal_block_delay] is valid

Lemma minimal_block_delay_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Period_repr.Valid.non_zero
    (Constants_storage.minimal_block_delay ctxt).
Proof.
  ctxt_trivial.
Qed.

The function [delay_increment_per_round] is valid

Lemma delay_increment_per_round_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  Period_repr.Valid.non_zero
    (Constants_storage.delay_increment_per_round ctxt).
Proof.
  ctxt_trivial.
Qed.