Skip to main content

🎛️ Constants_parametric_previous_repr.v

Proofs

See code, Gitlab , OCaml

The validity predicate for [dal].
  Module Valid.
    Import Proto_alpha.Constants_parametric_previous_repr.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);
    }.
  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].
  Module Valid.
    Import Proto_alpha.Constants_parametric_previous_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_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_available_messages :
        Pervasives.Int31.Valid.t x.(max_available_messages);
      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);
    }.
  End Valid.
End sc_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);
    tokens_per_roll : Tez_repr.Valid.t x.(tokens_per_roll);
    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_sunset_level :
      Int32.Valid.t x.(liquidity_baking_sunset_level);
    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);
  }.
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.

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.