🎛️ Constants_parametric_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Dal.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Period_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.State_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Module dal.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Dal.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Period_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.State_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Module dal.
The validity predicate for [dal].
Module Valid.
Import Proto_alpha.Constants_parametric_repr.dal.
Record t (x : dal) := {
number_of_slots : 1 ≤ x.(number_of_slots) ≤ 256;
attestation_lag : Pervasives.Int16.Valid.t x.(attestation_lag);
availability_threshold :
Pervasives.Int16.Valid.t x.(availability_threshold);
cryptobox_parameters : Dal.parameters.Valid.t x.(cryptobox_parameters);
}.
End Valid.
End dal.
Import Proto_alpha.Constants_parametric_repr.dal.
Record t (x : dal) := {
number_of_slots : 1 ≤ x.(number_of_slots) ≤ 256;
attestation_lag : Pervasives.Int16.Valid.t x.(attestation_lag);
availability_threshold :
Pervasives.Int16.Valid.t x.(availability_threshold);
cryptobox_parameters : Dal.parameters.Valid.t x.(cryptobox_parameters);
}.
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 [] []; simpl in *; intuition.
Qed.
#[global] Hint Resolve dal_encoding_is_valid : Data_encoding_db.
Module tx_rollup.
: Data_encoding.Valid.t dal.Valid.t dal_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; simpl in *; intuition.
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.
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.
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.
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);
hard_storage_limit_per_operation :
Int32.Valid.positive x.(hard_storage_limit_per_operation);
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.
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);
hard_storage_limit_per_operation :
Int32.Valid.positive x.(hard_storage_limit_per_operation);
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.
: 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.
: 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.
: 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.
: 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.