🎛️ Constants_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
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.

Lemma hard_has_limit_per_operation_is_valid
  : ∀ {ctxt : Raw_context.t},
  Raw_context.Valid.t ctxt →
  Saturation_repr.Valid.t
    ctxt.(Raw_context.t.back)
      .(Raw_context.back.constants)
        .(Constants_repr.parametric.hard_gas_limit_per_operation).
Proof.
  dtauto.
Qed.

Lemma hard_gas_limit_per_block_is_valid
  (ctxt : Raw_context.t) :
  Raw_context.Valid.t ctxt →
  Saturation_repr.Valid.t
    ctxt.(Raw_context.t.back)
      .(Raw_context.back.constants)
        .(Constants_repr.parametric.hard_gas_limit_per_block).
Proof.
  dtauto.
Qed.

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

Lemma tokens_per_roll_is_valid
  (ctxt : Raw_context.t) :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.tokens_per_roll ctxt).
Proof.
  dtauto.
Qed.

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

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

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

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

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

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

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

Lemma liquidity_baking_subsidy_is_valid
  : ∀ {ctxt : Raw_context.t},
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t
    (Constants_storage.liquidity_baking_subsidy ctxt).
Proof.
  dtauto.
Qed.

Lemma parametric_is_valid
  : ∀ {ctxt : Raw_context.t},
  Raw_context.Valid.t ctxt →
  Constants_repr.Parametric.Valid.t
    (Constants_storage.parametric_value ctxt).
Proof.
  dtauto.
Qed.

(* @TODO *)
Lemma minimal_participation_ratio_is_valid
  (ctxt : Raw_context.t) :
  Raw_context.Valid.t ctxt →
  Constants_repr.Ratio.Valid.t
    (Constants_storage.minimal_participation_ratio ctxt).
Proof.
  dtauto.
Qed.

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

Lemma ratio_of_frozen_deposits_slashed_per_double_endorsement_is_valid
  (ctxt : Raw_context.t) :
  Raw_context.Valid.t ctxt →
  Constants_repr.Ratio.Valid.t
    (Constants_storage.ratio_of_frozen_deposits_slashed_per_double_endorsement ctxt).
Proof.
  dtauto.
Qed.

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

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