🎛️ Constants_parametric_previous_repr.v

Proofs

The validity predicate for [dal].

    Record t (x : dal) := {
      number_of_slots : Pervasives.Int16.Valid.t x.(number_of_slots);
      number_of_shards : Pervasives.Int16.Valid.t x.(number_of_shards);
      endorsement_lag : Pervasives.Int16.Valid.t x.(endorsement_lag);
      availability_threshold :
        Pervasives.Int16.Valid.t x.(availability_threshold);
      slot_size : Pervasives.Int31.Valid.t x.(slot_size);
      redundancy_factor : Pervasives.UInt8.Valid.t x.(redundancy_factor);
      page_size : Pervasives.UInt16.Valid.t x.(page_size);
    }.
  End Valid.
End dal.

Encoding [dal_encoding] is valid.

Lemma dal_encoding_is_valid
: Data_encoding.Valid.t dal.Valid.t dal_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve dal_encoding_is_valid : Data_encoding_db.

Module tx_rollup.

The validity predicate for [tx_rollup].

The validity predicate for [sc_rollup].

  Module Valid.
    Import Proto_alpha.Constants_parametric_previous_repr.sc_rollup.

    Record t (x : sc_rollup) : Prop := {
      origination_size : Pervasives.Int31.Valid.t x.(origination_size);
      challenge_window_in_blocks :
        Pervasives.Int31.Valid.t x.(challenge_window_in_blocks);
      max_number_of_messages_per_commitment_period :
        Pervasives.Int31.Valid.t
          x.(max_number_of_messages_per_commitment_period);
      stake_amount : Tez_repr.Valid.t x.(stake_amount);
      commitment_period_in_blocks :
        Pervasives.Int31.Valid.t x.(commitment_period_in_blocks);
      max_lookahead_in_blocks : Int32.Valid.t x.(max_lookahead_in_blocks);
      max_active_outbox_levels : Int32.Valid.t x.(max_active_outbox_levels);
      max_outbox_messages_per_level :
        Pervasives.Int31.Valid.t x.(max_outbox_messages_per_level);
      number_of_sections_in_dissection :
        Pervasives.UInt8.Valid.t x.(number_of_sections_in_dissection);
      timeout_period_in_blocks :
        Pervasives.Int31.Valid.t x.(timeout_period_in_blocks);
      max_number_of_stored_cemented_commitments :
        Pervasives.Int31.Valid.t x.(max_number_of_stored_cemented_commitments);
    }.
  End Valid.
End sc_rollup.

Module zk_rollup.
  Module Valid.
    Import Proto_alpha.Constants_parametric_previous_repr.zk_rollup.

Validity predicate for [zk_rollup]

    Record t (x : Constants_parametric_previous_repr.zk_rollup) : Prop := {
      origination_size : Pervasives.Int31.Valid.t x.(origination_size);
      min_pending_to_process :
        Pervasives.Int31.Valid.t x.(min_pending_to_process);
    }.
  End Valid.
End zk_rollup.

The validity predicate for [t].

Module Valid.
  Import Proto_alpha.Constants_parametric_previous_repr.t.

  Record t (x : Proto_alpha.Constants_parametric_previous_repr.t) : Prop := {
    preserved_cycles : Pervasives.UInt8.Valid.t x.(preserved_cycles);
    blocks_per_cycle : Int32.Valid.t x.(blocks_per_cycle);
    blocks_per_commitment : Int32.Valid.t x.(blocks_per_commitment);
    nonce_revelation_threshold : Int32.Valid.t x.(nonce_revelation_threshold);
    blocks_per_stake_snapshot : Int32.Valid.t x.(blocks_per_stake_snapshot);
    cycles_per_voting_period : Int32.Valid.t x.(cycles_per_voting_period);
    hard_gas_limit_per_operation :
      Gas_limit_repr.Arith.Integral.Valid.t x.(hard_gas_limit_per_operation);
    hard_gas_limit_per_block :
      Gas_limit_repr.Arith.Integral.Valid.t x.(hard_gas_limit_per_block);
    proof_of_work_threshold : Int64.Valid.t x.(proof_of_work_threshold);
    minimal_stake : Tez_repr.Valid.t x.(minimal_stake);
    vdf_difficulty : Int64.Valid.t x.(vdf_difficulty);
    seed_nonce_revelation_tip :
      Tez_repr.Valid.t x.(seed_nonce_revelation_tip);
    origination_size : Pervasives.Int31.Valid.t x.(origination_size);
    baking_reward_fixed_portion :
      Tez_repr.Valid.t x.(baking_reward_fixed_portion);
    baking_reward_bonus_per_slot :
      Tez_repr.Valid.t x.(baking_reward_bonus_per_slot);
    endorsing_reward_per_slot :
      Tez_repr.Valid.t x.(endorsing_reward_per_slot);
    cost_per_byte : Tez_repr.Valid.t x.(cost_per_byte);
    quorum_min : Int32.Valid.t x.(quorum_min);
    quorum_max : Int32.Valid.t x.(quorum_max);
    min_proposal_quorum : Int32.Valid.t x.(min_proposal_quorum);
    liquidity_baking_subsidy : Tez_repr.Valid.t x.(liquidity_baking_subsidy);
    liquidity_baking_toggle_ema_threshold :
      Int32.Valid.t x.(liquidity_baking_toggle_ema_threshold);
    max_operations_time_to_live :
      Pervasives.Int16.Valid.t x.(max_operations_time_to_live);
    minimal_block_delay : Period_repr.Valid.t x.(minimal_block_delay);
    delay_increment_per_round :
      Period_repr.Valid.t x.(delay_increment_per_round);
    minimal_participation_ratio :
      Ratio_repr.Valid.t x.(minimal_participation_ratio);
    consensus_committee_size :
      Pervasives.Int31.Valid.t x.(consensus_committee_size);
    consensus_threshold : Pervasives.Int31.Valid.t x.(consensus_threshold);
    max_slashing_period : Pervasives.Int31.Valid.t x.(max_slashing_period);
    frozen_deposits_percentage :
      Pervasives.Int31.Valid.t x.(frozen_deposits_percentage);
    double_baking_punishment : Tez_repr.Valid.t x.(double_baking_punishment);
    ratio_of_frozen_deposits_slashed_per_double_endorsement :
      Ratio_repr.Valid.t
        x.(ratio_of_frozen_deposits_slashed_per_double_endorsement);
    cache_script_size : Pervasives.Int31.Valid.t x.(cache_script_size);
    cache_stake_distribution_cycles :
      Pervasives.Int8.Valid.t x.(cache_stake_distribution_cycles);
    cache_sampler_state_cycles :
      Pervasives.Int8.Valid.t x.(cache_sampler_state_cycles);
    tx_rollup : tx_rollup.Valid.t x.(tx_rollup);
    dal : dal.Valid.t x.(dal);
    sc_rollup : sc_rollup.Valid.t x.(sc_rollup);
    zk_rollup : zk_rollup.Valid.t x.(zk_rollup);
  }.
End Valid.

Encoding [tx_rollup_encoding] is valid.

Lemma tx_rollup_encoding_is_valid
: Data_encoding.Valid.t tx_rollup.Valid.t tx_rollup_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve tx_rollup_encoding_is_valid : Data_encoding_db.

Encoding [sc_rollup_encoding] is valid.

Lemma sc_rollup_encoding_is_valid
: Data_encoding.Valid.t sc_rollup.Valid.t sc_rollup_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve sc_rollup_encoding_is_valid : Data_encoding_db.

Encoding [zk_rollup_encoding] is valid.

Lemma zk_rollup_encoding_is_valid
: Data_encoding.Valid.t zk_rollup.Valid.t zk_rollup_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve zk_rollup_encoding_is_valid : Data_encoding_db.

The encoding [encoding] is valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t
    Constants_parametric_previous_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros x H;
  intuition; try (destruct H; assumption);
  hauto l: on.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.