Skip to main content

🎛️ Constants_parametric_repr.v

Proofs

See code, Gitlab , OCaml

The validity predicate for [dal].
  Module Valid.
    Import Proto_alpha.Constants_parametric_repr.dal.

    Record t (x : dal) := {
      number_of_slots :
        Pervasives.UInt8.Valid.positive 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);
      redundacy_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.
  intros [] []; split_conj; trivial; try apply H; cbn in *; lia.
Qed.
#[global] Hint Resolve dal_encoding_is_valid : Data_encoding_db.

Module tx_rollup.
The validity predicate for [tx_rollup].
  Module Valid.
    Import Proto_alpha.Constants_parametric_repr.tx_rollup.

    Record t (x : tx_rollup) : Prop := {
      origination_size : Pervasives.Int31.Valid.t x.(origination_size);
      hard_size_limit_per_inbox :
        Pervasives.Int31.Valid.t x.(hard_size_limit_per_inbox);
      hard_size_limit_per_message :
        Pervasives.Int31.Valid.t x.(hard_size_limit_per_message);
      commitment_bond : Tez_repr.Valid.t x.(tx_rollup.commitment_bond);
      finality_period : Pervasives.Int31.Valid.t x.(finality_period);
      withdraw_period : Pervasives.Int31.Valid.t x.(withdraw_period);
      max_inboxes_count :
        Pervasives.Int31.Valid.t x.(max_inboxes_count);
      max_messages_per_inbox :
        Pervasives.Int31.Valid.t x.(max_messages_per_inbox);
      max_commitments_count :
        Pervasives.Int31.Valid.t x.(max_commitments_count);
      cost_per_byte_ema_factor :
        Pervasives.Int31.Valid.t x.(cost_per_byte_ema_factor);
      max_ticket_payload_size :
        Pervasives.Int31.Valid.t x.(max_ticket_payload_size);
      max_withdrawals_per_batch :
        Pervasives.Int31.Valid.t x.(max_withdrawals_per_batch);
      rejection_max_proof_size :
        Pervasives.Int31.Valid.t x.(rejection_max_proof_size);
      sunset_level : Int32.Valid.t x.(sunset_level);
    }.
  End Valid.
End tx_rollup.

Module sc_rollup.
The validity predicate for [sc_rollup].
  Module Valid.
    Import Proto_alpha.Constants_parametric_repr.sc_rollup.

    Record t (x : sc_rollup) : Prop := {
      max_lookahead_in_blocks_gt_commitment_period_in_blocks :
        x.(max_lookahead_in_blocks) > x.(commitment_period_in_blocks);
      max_lookahead_in_blocks_gt_challenge_window_in_blocks :
        x.(max_lookahead_in_blocks) > x.(challenge_window_in_blocks);
      origination_size :
        Pervasives.Int31.Valid.non_negative x.(origination_size);
      challenge_window_in_blocks :
        Pervasives.Int31.Valid.non_negative
          x.(challenge_window_in_blocks);
      max_number_of_messages_per_commitment_period :
        Pervasives.Int31.Valid.positive
          x.(max_number_of_messages_per_commitment_period);
      stake_amount : Tez_repr.Valid.t x.(stake_amount);
      commitment_period_in_blocks :
        Pervasives.Int31.Valid.positive
          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.positive
          x.(max_number_of_stored_cemented_commitments);
    }.
  End Valid.
End sc_rollup.

The validity predicate for [zk_rollup]
Module zk_rollup.
  Module Valid.
    Import Proto_alpha.Constants_parametric_repr.zk_rollup.

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

The validity predicate for [t].
Module Valid.
  Import Proto_alpha.Constants_parametric_repr.t.

  Record t (x : Proto_alpha.Constants_parametric_repr.t) : Prop := {
    nonce_revelation_threshold_lt_blocks_per_cycle :
      x.(nonce_revelation_threshold) < x.(blocks_per_cycle);
    block_per_cycle_over_stake_snapshot :
      let y := x.(blocks_per_cycle) /i32
       x.(blocks_per_stake_snapshot) in
      Pervasives.UInt16.min < y < Pervasives.UInt16.max;
    vdf_difficulty_invariant :
      let y :=
        (if x.(blocks_per_commitment) >? 32 then 200000 else 1) in
        x.(vdf_difficulty) > y ×i64 5 ×i64
          (x.(nonce_revelation_threshold) ×i64
          Period_repr.to_seconds x.(minimal_block_delay));
    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.positive 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.non_zero x.(minimal_block_delay);
    delay_increment_per_round :
      Period_repr.Valid.non_zero x.(delay_increment_per_round);
    minimal_participation_ratio :
      Ratio_repr.Valid.t x.(minimal_participation_ratio)
      Ratio_repr.In_zero_one.t x.(minimal_participation_ratio);
    consensus_threshold_consensus_committee_size :
      x.(consensus_threshold) x.(consensus_committee_size);
    consensus_committee_size :
      Pervasives.Int31.Valid.positive x.(consensus_committee_size);
    consensus_threshold :
      Pervasives.Int31.Valid.non_negative x.(consensus_threshold);
    max_slashing_period :
      Pervasives.Int31.Valid.positive x.(max_slashing_period);
    frozen_deposits_percentage :
      0 < x.(frozen_deposits_percentage) 100;
    double_baking_punishment :
      Tez_repr.Valid.t x.(double_baking_punishment)
      x.(double_baking_punishment) Tez_repr.zero;
    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.
  intros [] []; split_conj; trivial; try apply H; cbn in *; lia.
Qed.
#[global] Hint Resolve sc_rollup_encoding_is_valid : Data_encoding_db.

The 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.

Encoding [encoding] is valid.
Lemma encoding_is_valid
  : Data_encoding.Valid.t Valid.t encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros [] []; simpl in *; repeat (split; trivial).
  all: try (try step; lia).
  all:
    repeat match goal with
    | H : _ _ |- _destruct H
    end;
    repeat match goal with
    | H : Ratio_repr.Valid.t _ |- _destruct H
    end;
    lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.