🎛️ Constants_repr.v

Proofs

See code, Gitlab , 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.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.

Module Ratio.
  Module Valid.
    Import Constants_repr.ratio.

    Record t (ratio : Constants_repr.ratio) : Prop := {
      numerator :
        Pervasives.UInt16.Valid.t ratio.(Constants_repr.ratio.numerator);
      denominator :
        Pervasives.UInt16.Valid.t ratio.(Constants_repr.ratio.denominator) ∧
        ratio.(Constants_repr.ratio.denominator) > 0;
    }.
  End Valid.
End Ratio.

Lemma ratio_encoding_is_valid
  : Data_encoding.Valid.t Ratio.Valid.t Constants_repr.ratio_encoding.
  Data_encoding.Valid.data_encoding_auto.
  scrush.
Qed.
#[global] Hint Resolve ratio_encoding_is_valid : Data_encoding_db.

Lemma fixed_encoding_is_valid
  : Data_encoding.Valid.t (fun _ ⇒ True) Constants_repr.fixed_encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros []; now repeat constructor.
Qed.
#[global] Hint Resolve fixed_encoding_is_valid : Data_encoding_db.

Module Parametric.
  Module Valid.
    Import Constants_repr.parametric.

    Record t (c : Constants_repr.parametric) : Prop := {
      preserved_cycles :
        Pervasives.UInt8.Valid.t c.(preserved_cycles);
      blocks_per_cycle : Int32.Valid.t c.(blocks_per_cycle);
      blocks_per_commitment : Int32.Valid.t c.(blocks_per_commitment);
      blocks_per_stake_snapshot : Int32.Valid.t c.(blocks_per_stake_snapshot);
      cycles_per_voting_period : Int32.Valid.t c.(cycles_per_voting_period);
      hard_gas_limit_per_block :
        Gas_limit_repr.Is_rounded.t c.(hard_gas_limit_per_block) ∧
        Saturation_repr.Valid.t c.(hard_gas_limit_per_block);
      hard_gas_limit_per_operation :
        Gas_limit_repr.Is_rounded.t c.(hard_gas_limit_per_operation) ∧
        Saturation_repr.Valid.t
          c.(hard_gas_limit_per_operation);
      proof_of_work_threshold : Int64.Valid.t c.(proof_of_work_threshold);
      tokens_per_roll :
        Tez_repr.Valid.t c.(tokens_per_roll);
      seed_nonce_revelation_tip :
        Tez_repr.Valid.t c.(seed_nonce_revelation_tip);
      origination_size :
        Pervasives.Int31.Valid.t c.(origination_size);
      baking_reward_fixed_portion :
        Tez_repr.Valid.t c.(baking_reward_fixed_portion);
      baking_reward_bonus_per_slot :
        Tez_repr.Valid.t c.(baking_reward_bonus_per_slot);
      endorsing_reward_per_slot :
        Tez_repr.Valid.t c.(endorsing_reward_per_slot);
      cost_per_byte :
        Tez_repr.Valid.t c.(cost_per_byte);
      quorum_min : Int32.Valid.t c.(quorum_min);
      quorum_max : Int32.Valid.t c.(quorum_max);
      min_proposal_quorum : Int32.Valid.t c.(min_proposal_quorum);
      liquidity_baking_subsidy :
        Tez_repr.Valid.t c.(liquidity_baking_subsidy);
      liquidity_baking_sunset_level :
        Int32.Valid.t c.(liquidity_baking_sunset_level);
      liquidity_baking_toggle_ema_threshold :
        Int32.Valid.t c.(liquidity_baking_toggle_ema_threshold);
      max_operations_time_to_live :
        Pervasives.Int16.Valid.t c.(max_operations_time_to_live);
      minimal_block_delay :
        Period_repr.Valid.t c.(minimal_block_delay);
      delay_increment_per_round :
        Period_repr.Valid.t c.(delay_increment_per_round);
      minimal_participation_ratio :
        Ratio.Valid.t c.(minimal_participation_ratio);
      consensus_committee_size :
        Pervasives.Int31.Valid.t c.(consensus_committee_size);
      consensus_threshold :
        Pervasives.Int31.Valid.t c.(consensus_threshold);
      max_slashing_period :
        Pervasives.Int31.Valid.t c.(max_slashing_period);
      frozen_deposits_percentage :
        Pervasives.Int31.Valid.t c.(frozen_deposits_percentage);
      double_baking_punishment :
        Tez_repr.Valid.t c.(double_baking_punishment);
      ratio_of_frozen_deposits_slashed_per_double_endorsement :
        Ratio.Valid.t c.(ratio_of_frozen_deposits_slashed_per_double_endorsement);
      cache_script_size :
        Pervasives.Int31.Valid.t c.(cache_script_size);
      cache_stake_distribution_cycles :
        Pervasives.Int8.Valid.t c.(cache_stake_distribution_cycles);
      cache_sampler_state_cycles :
        Pervasives.Int8.Valid.t c.(cache_sampler_state_cycles);
      tx_rollup_origination_size :
        Pervasives.Int31.Valid.t c.(tx_rollup_origination_size);
      tx_rollup_hard_size_limit_per_inbox :
        Pervasives.Int31.Valid.t c.(tx_rollup_hard_size_limit_per_inbox);
      tx_rollup_hard_size_limit_per_message :
        Pervasives.Int31.Valid.t c.(tx_rollup_hard_size_limit_per_message);
      tx_rollup_max_withdrawals_per_batch :
        Pervasives.Int31.Valid.t c.(tx_rollup_max_withdrawals_per_batch);
      tx_rollup_commitment_bond :
        Tez_repr.Valid.t c.(tx_rollup_commitment_bond);
      tx_rollup_finality_period :
        Pervasives.Int31.Valid.t c.(tx_rollup_finality_period);
      tx_rollup_withdraw_period :
        Pervasives.Int31.Valid.t c.(tx_rollup_withdraw_period);
      tx_rollup_max_inboxes_count :
        Pervasives.Int31.Valid.t c.(tx_rollup_max_inboxes_count);
      tx_rollup_max_messages_per_inbox :
        Pervasives.Int31.Valid.t c.(tx_rollup_max_messages_per_inbox);
      tx_rollup_max_commitments_count :
        Pervasives.Int31.Valid.t c.(tx_rollup_max_commitments_count);
      tx_rollup_cost_per_byte_ema_factor :
        Pervasives.Int31.Valid.t c.(tx_rollup_cost_per_byte_ema_factor);
      tx_rollup_max_ticket_payload_size :
        Pervasives.Int31.Valid.t c.(tx_rollup_max_ticket_payload_size);
      tx_rollup_rejection_max_proof_size :
        Pervasives.Int31.Valid.t c.(tx_rollup_rejection_max_proof_size);
      tx_rollup_sunset_level :
        Int32.Valid.t c.(tx_rollup_sunset_level);
      sc_rollup_origination_size :
        Pervasives.Int31.Valid.t c.(sc_rollup_origination_size);
      sc_rollup_challenge_window_in_blocks :
        Pervasives.Int31.Valid.t c.(sc_rollup_challenge_window_in_blocks);
      sc_rollup_max_available_messages :
        Pervasives.Int31.Valid.t c.(sc_rollup_max_available_messages);
    }.
  End Valid.
End Parametric.

Lemma parametric_encoding_is_valid
  : Data_encoding.Valid.t
      Parametric.Valid.t Constants_repr.parametric_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros [] []; simpl in *;
    (repeat match goal with | |- context [_ ∧ _] ⇒ split end); try tauto.
  now step.
Qed.
#[global] Hint Resolve parametric_encoding_is_valid : Data_encoding_db.

Module Valid.
  Definition t (c : Constants_repr.t) : Prop :=
    Parametric.Valid.t c.(Constants_repr.t.parametric).
End Valid.

Lemma encoding_is_valid
  : Data_encoding.Valid.t Valid.t Constants_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Module Proto_previous.
  Module Valid.
    Import Constants_repr.Proto_previous.parametric.

    Record t (c : Constants_repr.Proto_previous.parametric) : Prop := {
      preserved_cycles :
        Pervasives.UInt8.Valid.t c.(preserved_cycles);
      blocks_per_cycle : Int32.Valid.t c.(blocks_per_cycle);
      blocks_per_commitment : Int32.Valid.t c.(blocks_per_commitment);
      blocks_per_voting_period : Int32.Valid.t c.(blocks_per_voting_period);
      minimal_block_delay :
        Period_repr.Valid.t c.(minimal_block_delay);
      proof_of_work_threshold : Int64.Valid.t c.(proof_of_work_threshold);
      tokens_per_roll :
        Tez_repr.Valid.t c.(tokens_per_roll);
      seed_nonce_revelation_tip :
        Tez_repr.Valid.t c.(seed_nonce_revelation_tip);
      origination_size :
        Pervasives.Int31.Valid.t c.(origination_size);
      cost_per_byte :
        Tez_repr.Valid.t c.(cost_per_byte);
      quorum_min : Int32.Valid.t c.(quorum_min);
      quorum_max : Int32.Valid.t c.(quorum_max);
      min_proposal_quorum : Int32.Valid.t c.(min_proposal_quorum);
      liquidity_baking_subsidy :
        Tez_repr.Valid.t c.(liquidity_baking_subsidy);
      liquidity_baking_sunset_level :
        Int32.Valid.t c.(liquidity_baking_sunset_level);
      liquidity_baking_toggle_ema_threshold :
        Int32.Valid.t c.(liquidity_baking_toggle_ema_threshold);
      hard_gas_limit_per_block :
        Gas_limit_repr.Is_rounded.t c.(hard_gas_limit_per_block) ∧
        Saturation_repr.Valid.t
          c.(hard_gas_limit_per_block);
      hard_gas_limit_per_operation :
        Gas_limit_repr.Is_rounded.t c.(hard_gas_limit_per_operation) ∧
        Saturation_repr.Valid.t
          c.(hard_gas_limit_per_operation);
      blocks_per_stake_snapshot :
        Int32.Valid.t c.(blocks_per_stake_snapshot);
      baking_reward_fixed_portion :
        Tez_repr.Valid.t c.(baking_reward_fixed_portion);
      baking_reward_bonus_per_slot :
        Tez_repr.Valid.t c.(baking_reward_bonus_per_slot);
      endorsing_reward_per_slot :
        Tez_repr.Valid.t c.(endorsing_reward_per_slot);
      max_operations_time_to_live :
        Pervasives.Int16.Valid.t c.(max_operations_time_to_live);
      delay_increment_per_round :
        Period_repr.Valid.t c.(delay_increment_per_round);
      consensus_committee_size :
        Pervasives.Int31.Valid.t c.(consensus_committee_size);
      consensus_threshold :
        Pervasives.Int31.Valid.t c.(consensus_threshold);
      minimal_participation_ratio :
        Ratio.Valid.t c.(minimal_participation_ratio);
      max_slashing_period :
        Pervasives.Int31.Valid.t c.(max_slashing_period);
      frozen_deposits_percentage :
        Pervasives.Int31.Valid.t c.(frozen_deposits_percentage);
      double_baking_punishment :
        Tez_repr.Valid.t c.(double_baking_punishment);
      ratio_of_frozen_deposits_slashed_per_double_endorsement :
        Ratio.Valid.t c.(ratio_of_frozen_deposits_slashed_per_double_endorsement);

 }.
  End Valid.

  Lemma delegate_selection_encoding_is_valid
    : Data_encoding.Valid.t (fun _ ⇒ True)
      Constants_repr.Proto_previous.delegate_selection_encoding.
    Data_encoding.Valid.data_encoding_auto;
    hfcrush.
  Qed.
  #[global] Hint Resolve delegate_selection_encoding_is_valid : Data_encoding_db.

  Lemma parametric_encoding_is_valid
    : Data_encoding.Valid.t Valid.t Constants_repr.Proto_previous.parametric_encoding.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve parametric_encoding_is_valid : Data_encoding_db.
End Proto_previous.