🎛️ Constants_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Definition mainnet_id : Chain_id.t :=
Chain_id.of_b58check_exn "NetXdQprcVkpaWU".
Definition fitness_version_number : string := String.String "002" "".
Definition proof_of_work_nonce_size : int := 8.
Definition nonce_length : int := 32.
Definition max_anon_ops_per_block : int := 132.
Definition max_proposals_per_delegate : int := 20.
Definition max_operation_data_length : int := 32 ×i 1024.
Definition max_micheline_node_count : int := 50000.
Definition max_micheline_bytes_limit : int := 50000.
Definition max_allowed_global_constant_depth : int := 10000.
Definition michelson_maximum_type_size : int := 2001.
Definition cache_layout_size : int := 3.
Definition sc_max_wrapped_proof_binary_size : int := 30000.
Definition sc_rollup_message_size_limit : int := 4096.
Definition fixed : Set := unit.
Definition fixed_encoding : Data_encoding.encoding unit :=
Data_encoding.conv
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
((proof_of_work_nonce_size, nonce_length, max_anon_ops_per_block,
max_operation_data_length, max_proposals_per_delegate,
max_micheline_node_count, max_micheline_bytes_limit,
max_allowed_global_constant_depth, cache_layout_size,
michelson_maximum_type_size),
(sc_max_wrapped_proof_binary_size, sc_rollup_message_size_limit)))
(fun (function_parameter :
(int × int × int × int × int × int × int × int × int × int) × (int × int))
⇒
let
'((_proof_of_work_nonce_size, _nonce_length, _max_anon_ops_per_block,
_max_operation_data_length, _max_proposals_per_delegate,
_max_micheline_node_count, _max_micheline_bytes_limit,
_max_allowed_global_constant_depth, _cache_layout_size,
_michelson_maximum_type_size),
(_sc_max_wrapped_proof_binary_size, _sc_rollup_message_size_limit)) :=
function_parameter in
tt) None
(Data_encoding.merge_objs
(Data_encoding.obj10
(Data_encoding.req None None "proof_of_work_nonce_size"
Data_encoding.uint8)
(Data_encoding.req None None "nonce_length" Data_encoding.uint8)
(Data_encoding.req None None "max_anon_ops_per_block"
Data_encoding.uint8)
(Data_encoding.req None None "max_operation_data_length"
Data_encoding.int31)
(Data_encoding.req None None "max_proposals_per_delegate"
Data_encoding.uint8)
(Data_encoding.req None None "max_micheline_node_count"
Data_encoding.int31)
(Data_encoding.req None None "max_micheline_bytes_limit"
Data_encoding.int31)
(Data_encoding.req None None "max_allowed_global_constants_depth"
Data_encoding.int31)
(Data_encoding.req None None "cache_layout_size" Data_encoding.uint8)
(Data_encoding.req None None "michelson_maximum_type_size"
Data_encoding.uint16))
(Data_encoding.obj2
(Data_encoding.req None None "sc_max_wrapped_proof_binary_size"
Data_encoding.int31)
(Data_encoding.req None None "sc_rollup_message_size_limit"
Data_encoding.int31))).
Definition fixed_value : unit := tt.
Module t.
Record record : Set := Build {
fixed : fixed;
parametric : Constants_parametric_repr.t;
}.
Definition with_fixed fixed (r : record) :=
Build fixed r.(parametric).
Definition with_parametric parametric (r : record) :=
Build r.(fixed) parametric.
End t.
Definition t := t.record.
Definition all_of_parametric (parametric_value : Constants_parametric_repr.t)
: t := {| t.fixed := fixed_value; t.parametric := parametric_value; |}.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{| t.fixed := fixed_value; t.parametric := parametric_value |} :=
function_parameter in
(fixed_value, parametric_value))
(fun (function_parameter : fixed × Constants_parametric_repr.t) ⇒
let '(fixed_value, parametric_value) := function_parameter in
{| t.fixed := fixed_value; t.parametric := parametric_value; |}) None
(Data_encoding.merge_objs fixed_encoding Constants_parametric_repr.encoding).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Definition mainnet_id : Chain_id.t :=
Chain_id.of_b58check_exn "NetXdQprcVkpaWU".
Definition fitness_version_number : string := String.String "002" "".
Definition proof_of_work_nonce_size : int := 8.
Definition nonce_length : int := 32.
Definition max_anon_ops_per_block : int := 132.
Definition max_proposals_per_delegate : int := 20.
Definition max_operation_data_length : int := 32 ×i 1024.
Definition max_micheline_node_count : int := 50000.
Definition max_micheline_bytes_limit : int := 50000.
Definition max_allowed_global_constant_depth : int := 10000.
Definition michelson_maximum_type_size : int := 2001.
Definition cache_layout_size : int := 3.
Definition sc_max_wrapped_proof_binary_size : int := 30000.
Definition sc_rollup_message_size_limit : int := 4096.
Definition fixed : Set := unit.
Definition fixed_encoding : Data_encoding.encoding unit :=
Data_encoding.conv
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
((proof_of_work_nonce_size, nonce_length, max_anon_ops_per_block,
max_operation_data_length, max_proposals_per_delegate,
max_micheline_node_count, max_micheline_bytes_limit,
max_allowed_global_constant_depth, cache_layout_size,
michelson_maximum_type_size),
(sc_max_wrapped_proof_binary_size, sc_rollup_message_size_limit)))
(fun (function_parameter :
(int × int × int × int × int × int × int × int × int × int) × (int × int))
⇒
let
'((_proof_of_work_nonce_size, _nonce_length, _max_anon_ops_per_block,
_max_operation_data_length, _max_proposals_per_delegate,
_max_micheline_node_count, _max_micheline_bytes_limit,
_max_allowed_global_constant_depth, _cache_layout_size,
_michelson_maximum_type_size),
(_sc_max_wrapped_proof_binary_size, _sc_rollup_message_size_limit)) :=
function_parameter in
tt) None
(Data_encoding.merge_objs
(Data_encoding.obj10
(Data_encoding.req None None "proof_of_work_nonce_size"
Data_encoding.uint8)
(Data_encoding.req None None "nonce_length" Data_encoding.uint8)
(Data_encoding.req None None "max_anon_ops_per_block"
Data_encoding.uint8)
(Data_encoding.req None None "max_operation_data_length"
Data_encoding.int31)
(Data_encoding.req None None "max_proposals_per_delegate"
Data_encoding.uint8)
(Data_encoding.req None None "max_micheline_node_count"
Data_encoding.int31)
(Data_encoding.req None None "max_micheline_bytes_limit"
Data_encoding.int31)
(Data_encoding.req None None "max_allowed_global_constants_depth"
Data_encoding.int31)
(Data_encoding.req None None "cache_layout_size" Data_encoding.uint8)
(Data_encoding.req None None "michelson_maximum_type_size"
Data_encoding.uint16))
(Data_encoding.obj2
(Data_encoding.req None None "sc_max_wrapped_proof_binary_size"
Data_encoding.int31)
(Data_encoding.req None None "sc_rollup_message_size_limit"
Data_encoding.int31))).
Definition fixed_value : unit := tt.
Module t.
Record record : Set := Build {
fixed : fixed;
parametric : Constants_parametric_repr.t;
}.
Definition with_fixed fixed (r : record) :=
Build fixed r.(parametric).
Definition with_parametric parametric (r : record) :=
Build r.(fixed) parametric.
End t.
Definition t := t.record.
Definition all_of_parametric (parametric_value : Constants_parametric_repr.t)
: t := {| t.fixed := fixed_value; t.parametric := parametric_value; |}.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{| t.fixed := fixed_value; t.parametric := parametric_value |} :=
function_parameter in
(fixed_value, parametric_value))
(fun (function_parameter : fixed × Constants_parametric_repr.t) ⇒
let '(fixed_value, parametric_value) := function_parameter in
{| t.fixed := fixed_value; t.parametric := parametric_value; |}) None
(Data_encoding.merge_objs fixed_encoding Constants_parametric_repr.encoding).
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"constants.invalid_protocol_constants" "Invalid protocol constants"
"The provided protocol constants are not coherent."
(Some
(fun (ppf : Format.formatter) ⇒
fun (reason_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid protocol constants: "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid protocol constants: %s") reason_value))
(Data_encoding.obj1
(Data_encoding.req None None "reason" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_protocol_constants" then
let reason_value := cast string payload in
Some reason_value
else None
end)
(fun (reason_value : string) ⇒
Build_extensible "Invalid_protocol_constants" string reason_value).
Definition check_constants (constants : Constants_parametric_repr.t)
: M? unit :=
let? '_ :=
Error_monad.error_unless
(Period_repr.op_gt
constants.(Constants_parametric_repr.t.minimal_block_delay)
Period_repr.zero)
(Build_extensible "Invalid_protocol_constants" string
"The minimal block delay must be greater than zero") in
let? '_ :=
Error_monad.error_unless
(Period_repr.op_gt
constants.(Constants_parametric_repr.t.delay_increment_per_round)
Period_repr.zero)
(Build_extensible "Invalid_protocol_constants" string
"The delay increment per round must be greater than zero") in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.consensus_committee_size) >i 0)
(Build_extensible "Invalid_protocol_constants" string
"The consensus committee size must be strictly greater than 0.") in
let? '_ :=
Error_monad.error_unless
((constants.(Constants_parametric_repr.t.consensus_threshold) ≥i 0) &&
(constants.(Constants_parametric_repr.t.consensus_threshold) ≤i
constants.(Constants_parametric_repr.t.consensus_committee_size)))
(Build_extensible "Invalid_protocol_constants" string
"The consensus threshold must be greater than or equal to 0 and less than or equal to the consensus commitee size.")
in
let? '_ :=
Error_monad.error_unless
(let '{|
Ratio_repr.t.numerator := numerator;
Ratio_repr.t.denominator := denominator
|} :=
constants.(Constants_parametric_repr.t.minimal_participation_ratio) in
(numerator ≥i 0) && (denominator >i 0))
(Build_extensible "Invalid_protocol_constants" string
"The minimal participation ratio must be a non-negative valid ratio.")
in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.minimal_participation_ratio).(Ratio_repr.t.numerator)
≤i
constants.(Constants_parametric_repr.t.minimal_participation_ratio).(Ratio_repr.t.denominator))
(Build_extensible "Invalid_protocol_constants" string
"The minimal participation ratio must be less than or equal to 100%.")
in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.max_slashing_period) >i 0)
(Build_extensible "Invalid_protocol_constants" string
"The unfreeze delay must be strictly greater than 0.") in
let? '_ :=
Error_monad.error_unless
((constants.(Constants_parametric_repr.t.frozen_deposits_percentage) >i 0)
&&
(constants.(Constants_parametric_repr.t.frozen_deposits_percentage) ≤i
100))
(Build_extensible "Invalid_protocol_constants" string
"The frozen percentage ratio must be strictly greater than 0 and less or equal than 100.")
in
let? '_ :=
Error_monad.error_unless
(Tez_repr.op_gteq
constants.(Constants_parametric_repr.t.double_baking_punishment)
Tez_repr.zero)
(Build_extensible "Invalid_protocol_constants" string
"The double baking punishment must be non-negative.") in
let? '_ :=
Error_monad.error_unless
(let '{|
Ratio_repr.t.numerator := numerator;
Ratio_repr.t.denominator := denominator
|} :=
constants.(Constants_parametric_repr.t.ratio_of_frozen_deposits_slashed_per_double_endorsement)
in
(numerator ≥i 0) && (denominator >i 0))
(Build_extensible "Invalid_protocol_constants" string
"The ratio of frozen deposits ratio slashed per double endorsement must be a non-negative valid ratio.")
in
let? '_ :=
Error_monad.error_unless
(let snapshot_frequence :=
constants.(Constants_parametric_repr.t.blocks_per_cycle) /i32
constants.(Constants_parametric_repr.t.blocks_per_stake_snapshot) in
(snapshot_frequence >i32 Int32.zero) &&
(snapshot_frequence <i32 (Int32.of_int (Pervasives.lsl 1 16))))
(Build_extensible "Invalid_protocol_constants" string
"The ratio blocks_per_cycle per blocks_per_stake_snapshot should be between 1 and 65535")
in
let? '_ :=
Error_monad.error_unless
((constants.(Constants_parametric_repr.t.nonce_revelation_threshold) >i32
Int32.zero) &&
(constants.(Constants_parametric_repr.t.nonce_revelation_threshold) <i32
constants.(Constants_parametric_repr.t.blocks_per_cycle)))
(Build_extensible "Invalid_protocol_constants" string
"The nonce revelation threshold must be strictly smaller than blocks_per_cycle and strictly positive.")
in
let? '_ :=
Error_monad.error_unless
(let threshold :=
Int64.of_int32
constants.(Constants_parametric_repr.t.nonce_revelation_threshold) in
let block :=
Period_repr.to_seconds
constants.(Constants_parametric_repr.t.minimal_block_delay) in
let ips :=
if
constants.(Constants_parametric_repr.t.blocks_per_commitment) >i32 32
then
Int64.of_int 200000
else
Int64.one in
let factor := Int64.of_int 5 in
let difficulty := (ips ×i64 factor) ×i64 (threshold ×i64 block) in
constants.(Constants_parametric_repr.t.vdf_difficulty) >i64 difficulty)
(Build_extensible "Invalid_protocol_constants" string
"The VDF difficulty must be strictly greater than the product of the nonce_revelation_threshold, the minimial_block_delay, a benchmark of modulo squaring in class groups and a security threshold.")
in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.origination_size)
≥i 0)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup origination size must be non-negative.") in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.challenge_window_in_blocks)
≥i 0)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup challenge window in blocks must be non-negative.")
in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.max_number_of_messages_per_commitment_period)
>i 0)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup max number of messages per commitment period must be strictly greater than 0.")
in
let? '_ :=
Error_monad.error_unless
(Tez_repr.op_gteq
constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.stake_amount)
Tez_repr.zero)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup max stake amount must be non-negative.") in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.commitment_period_in_blocks)
>i 0)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup commitment period in blocks must be strictly greater than 0.")
in
let? '_ :=
Error_monad.error_unless
(let sc_rollup_max_lookahead_in_blocks :=
constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.max_lookahead_in_blocks)
in
(sc_rollup_max_lookahead_in_blocks >i32
(Int32.of_int
constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.commitment_period_in_blocks)))
&&
(sc_rollup_max_lookahead_in_blocks >i32
(Int32.of_int
constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.challenge_window_in_blocks))))
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup max lookahead in blocks must be greater than [sc_rollup_commitment_period_in_blocks] and [sc_rollup_challenge_window_in_blocks].")
in
let? '_ :=
Error_monad.error_unless
((constants.(Constants_parametric_repr.t.dal).(Constants_parametric_repr.dal.number_of_slots)
>i 0) &&
(constants.(Constants_parametric_repr.t.dal).(Constants_parametric_repr.dal.number_of_slots)
≤i 256))
(Build_extensible "Invalid_protocol_constants" string
"The number of data availability slot must be between 1 and 256") in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.max_number_of_stored_cemented_commitments)
>i 0)
(Build_extensible "Invalid_protocol_constants" string
"The number of maximum stored cemented commitments must be strictly positive")
in
Result.return_unit.
Module Generated.
Module t.
Record record : Set := Build {
consensus_threshold : int;
baking_reward_fixed_portion : Tez_repr.t;
baking_reward_bonus_per_slot : Tez_repr.t;
endorsing_reward_per_slot : Tez_repr.t;
liquidity_baking_subsidy : Tez_repr.t;
}.
Definition with_consensus_threshold consensus_threshold (r : record) :=
Build consensus_threshold r.(baking_reward_fixed_portion)
r.(baking_reward_bonus_per_slot) r.(endorsing_reward_per_slot)
r.(liquidity_baking_subsidy).
Definition with_baking_reward_fixed_portion baking_reward_fixed_portion
(r : record) :=
Build r.(consensus_threshold) baking_reward_fixed_portion
r.(baking_reward_bonus_per_slot) r.(endorsing_reward_per_slot)
r.(liquidity_baking_subsidy).
Definition with_baking_reward_bonus_per_slot baking_reward_bonus_per_slot
(r : record) :=
Build r.(consensus_threshold) r.(baking_reward_fixed_portion)
baking_reward_bonus_per_slot r.(endorsing_reward_per_slot)
r.(liquidity_baking_subsidy).
Definition with_endorsing_reward_per_slot endorsing_reward_per_slot
(r : record) :=
Build r.(consensus_threshold) r.(baking_reward_fixed_portion)
r.(baking_reward_bonus_per_slot) endorsing_reward_per_slot
r.(liquidity_baking_subsidy).
Definition with_liquidity_baking_subsidy liquidity_baking_subsidy
(r : record) :=
Build r.(consensus_threshold) r.(baking_reward_fixed_portion)
r.(baking_reward_bonus_per_slot) r.(endorsing_reward_per_slot)
liquidity_baking_subsidy.
End t.
Definition t := t.record.
Definition generate
(consensus_committee_size : int) (blocks_per_minute : Ratio_repr.t) : t :=
let consensus_threshold := ((consensus_committee_size ×i 2) /i 3) +i 1 in
let rewards_per_minute := Tez_repr.mul_exn Tez_repr.one 80 in
let rewards_per_block :=
Tez_repr.div_exn
(Tez_repr.mul_exn rewards_per_minute
blocks_per_minute.(Ratio_repr.t.denominator))
blocks_per_minute.(Ratio_repr.t.numerator) in
let rewards_half := Tez_repr.div_exn rewards_per_block 2 in
let rewards_quarter := Tez_repr.div_exn rewards_per_block 4 in
let bonus_committee_size := consensus_committee_size -i consensus_threshold
in
{| t.consensus_threshold := consensus_threshold;
t.baking_reward_fixed_portion :=
if bonus_committee_size ≤i 0 then
rewards_half
else
rewards_quarter;
t.baking_reward_bonus_per_slot :=
if bonus_committee_size ≤i 0 then
Tez_repr.zero
else
Tez_repr.div_exn rewards_quarter bonus_committee_size;
t.endorsing_reward_per_slot :=
Tez_repr.div_exn rewards_half consensus_committee_size;
t.liquidity_baking_subsidy := Tez_repr.div_exn rewards_per_block 16; |}.
End Generated.
Definition cache_layout (p_value : Constants_parametric_repr.t) : list int :=
[
p_value.(Constants_parametric_repr.t.cache_script_size);
p_value.(Constants_parametric_repr.t.cache_stake_distribution_cycles);
p_value.(Constants_parametric_repr.t.cache_sampler_state_cycles)
].
Error_monad.register_error_kind Error_monad.Permanent
"constants.invalid_protocol_constants" "Invalid protocol constants"
"The provided protocol constants are not coherent."
(Some
(fun (ppf : Format.formatter) ⇒
fun (reason_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid protocol constants: "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid protocol constants: %s") reason_value))
(Data_encoding.obj1
(Data_encoding.req None None "reason" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_protocol_constants" then
let reason_value := cast string payload in
Some reason_value
else None
end)
(fun (reason_value : string) ⇒
Build_extensible "Invalid_protocol_constants" string reason_value).
Definition check_constants (constants : Constants_parametric_repr.t)
: M? unit :=
let? '_ :=
Error_monad.error_unless
(Period_repr.op_gt
constants.(Constants_parametric_repr.t.minimal_block_delay)
Period_repr.zero)
(Build_extensible "Invalid_protocol_constants" string
"The minimal block delay must be greater than zero") in
let? '_ :=
Error_monad.error_unless
(Period_repr.op_gt
constants.(Constants_parametric_repr.t.delay_increment_per_round)
Period_repr.zero)
(Build_extensible "Invalid_protocol_constants" string
"The delay increment per round must be greater than zero") in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.consensus_committee_size) >i 0)
(Build_extensible "Invalid_protocol_constants" string
"The consensus committee size must be strictly greater than 0.") in
let? '_ :=
Error_monad.error_unless
((constants.(Constants_parametric_repr.t.consensus_threshold) ≥i 0) &&
(constants.(Constants_parametric_repr.t.consensus_threshold) ≤i
constants.(Constants_parametric_repr.t.consensus_committee_size)))
(Build_extensible "Invalid_protocol_constants" string
"The consensus threshold must be greater than or equal to 0 and less than or equal to the consensus commitee size.")
in
let? '_ :=
Error_monad.error_unless
(let '{|
Ratio_repr.t.numerator := numerator;
Ratio_repr.t.denominator := denominator
|} :=
constants.(Constants_parametric_repr.t.minimal_participation_ratio) in
(numerator ≥i 0) && (denominator >i 0))
(Build_extensible "Invalid_protocol_constants" string
"The minimal participation ratio must be a non-negative valid ratio.")
in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.minimal_participation_ratio).(Ratio_repr.t.numerator)
≤i
constants.(Constants_parametric_repr.t.minimal_participation_ratio).(Ratio_repr.t.denominator))
(Build_extensible "Invalid_protocol_constants" string
"The minimal participation ratio must be less than or equal to 100%.")
in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.max_slashing_period) >i 0)
(Build_extensible "Invalid_protocol_constants" string
"The unfreeze delay must be strictly greater than 0.") in
let? '_ :=
Error_monad.error_unless
((constants.(Constants_parametric_repr.t.frozen_deposits_percentage) >i 0)
&&
(constants.(Constants_parametric_repr.t.frozen_deposits_percentage) ≤i
100))
(Build_extensible "Invalid_protocol_constants" string
"The frozen percentage ratio must be strictly greater than 0 and less or equal than 100.")
in
let? '_ :=
Error_monad.error_unless
(Tez_repr.op_gteq
constants.(Constants_parametric_repr.t.double_baking_punishment)
Tez_repr.zero)
(Build_extensible "Invalid_protocol_constants" string
"The double baking punishment must be non-negative.") in
let? '_ :=
Error_monad.error_unless
(let '{|
Ratio_repr.t.numerator := numerator;
Ratio_repr.t.denominator := denominator
|} :=
constants.(Constants_parametric_repr.t.ratio_of_frozen_deposits_slashed_per_double_endorsement)
in
(numerator ≥i 0) && (denominator >i 0))
(Build_extensible "Invalid_protocol_constants" string
"The ratio of frozen deposits ratio slashed per double endorsement must be a non-negative valid ratio.")
in
let? '_ :=
Error_monad.error_unless
(let snapshot_frequence :=
constants.(Constants_parametric_repr.t.blocks_per_cycle) /i32
constants.(Constants_parametric_repr.t.blocks_per_stake_snapshot) in
(snapshot_frequence >i32 Int32.zero) &&
(snapshot_frequence <i32 (Int32.of_int (Pervasives.lsl 1 16))))
(Build_extensible "Invalid_protocol_constants" string
"The ratio blocks_per_cycle per blocks_per_stake_snapshot should be between 1 and 65535")
in
let? '_ :=
Error_monad.error_unless
((constants.(Constants_parametric_repr.t.nonce_revelation_threshold) >i32
Int32.zero) &&
(constants.(Constants_parametric_repr.t.nonce_revelation_threshold) <i32
constants.(Constants_parametric_repr.t.blocks_per_cycle)))
(Build_extensible "Invalid_protocol_constants" string
"The nonce revelation threshold must be strictly smaller than blocks_per_cycle and strictly positive.")
in
let? '_ :=
Error_monad.error_unless
(let threshold :=
Int64.of_int32
constants.(Constants_parametric_repr.t.nonce_revelation_threshold) in
let block :=
Period_repr.to_seconds
constants.(Constants_parametric_repr.t.minimal_block_delay) in
let ips :=
if
constants.(Constants_parametric_repr.t.blocks_per_commitment) >i32 32
then
Int64.of_int 200000
else
Int64.one in
let factor := Int64.of_int 5 in
let difficulty := (ips ×i64 factor) ×i64 (threshold ×i64 block) in
constants.(Constants_parametric_repr.t.vdf_difficulty) >i64 difficulty)
(Build_extensible "Invalid_protocol_constants" string
"The VDF difficulty must be strictly greater than the product of the nonce_revelation_threshold, the minimial_block_delay, a benchmark of modulo squaring in class groups and a security threshold.")
in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.origination_size)
≥i 0)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup origination size must be non-negative.") in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.challenge_window_in_blocks)
≥i 0)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup challenge window in blocks must be non-negative.")
in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.max_number_of_messages_per_commitment_period)
>i 0)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup max number of messages per commitment period must be strictly greater than 0.")
in
let? '_ :=
Error_monad.error_unless
(Tez_repr.op_gteq
constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.stake_amount)
Tez_repr.zero)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup max stake amount must be non-negative.") in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.commitment_period_in_blocks)
>i 0)
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup commitment period in blocks must be strictly greater than 0.")
in
let? '_ :=
Error_monad.error_unless
(let sc_rollup_max_lookahead_in_blocks :=
constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.max_lookahead_in_blocks)
in
(sc_rollup_max_lookahead_in_blocks >i32
(Int32.of_int
constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.commitment_period_in_blocks)))
&&
(sc_rollup_max_lookahead_in_blocks >i32
(Int32.of_int
constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.challenge_window_in_blocks))))
(Build_extensible "Invalid_protocol_constants" string
"The smart contract rollup max lookahead in blocks must be greater than [sc_rollup_commitment_period_in_blocks] and [sc_rollup_challenge_window_in_blocks].")
in
let? '_ :=
Error_monad.error_unless
((constants.(Constants_parametric_repr.t.dal).(Constants_parametric_repr.dal.number_of_slots)
>i 0) &&
(constants.(Constants_parametric_repr.t.dal).(Constants_parametric_repr.dal.number_of_slots)
≤i 256))
(Build_extensible "Invalid_protocol_constants" string
"The number of data availability slot must be between 1 and 256") in
let? '_ :=
Error_monad.error_unless
(constants.(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.max_number_of_stored_cemented_commitments)
>i 0)
(Build_extensible "Invalid_protocol_constants" string
"The number of maximum stored cemented commitments must be strictly positive")
in
Result.return_unit.
Module Generated.
Module t.
Record record : Set := Build {
consensus_threshold : int;
baking_reward_fixed_portion : Tez_repr.t;
baking_reward_bonus_per_slot : Tez_repr.t;
endorsing_reward_per_slot : Tez_repr.t;
liquidity_baking_subsidy : Tez_repr.t;
}.
Definition with_consensus_threshold consensus_threshold (r : record) :=
Build consensus_threshold r.(baking_reward_fixed_portion)
r.(baking_reward_bonus_per_slot) r.(endorsing_reward_per_slot)
r.(liquidity_baking_subsidy).
Definition with_baking_reward_fixed_portion baking_reward_fixed_portion
(r : record) :=
Build r.(consensus_threshold) baking_reward_fixed_portion
r.(baking_reward_bonus_per_slot) r.(endorsing_reward_per_slot)
r.(liquidity_baking_subsidy).
Definition with_baking_reward_bonus_per_slot baking_reward_bonus_per_slot
(r : record) :=
Build r.(consensus_threshold) r.(baking_reward_fixed_portion)
baking_reward_bonus_per_slot r.(endorsing_reward_per_slot)
r.(liquidity_baking_subsidy).
Definition with_endorsing_reward_per_slot endorsing_reward_per_slot
(r : record) :=
Build r.(consensus_threshold) r.(baking_reward_fixed_portion)
r.(baking_reward_bonus_per_slot) endorsing_reward_per_slot
r.(liquidity_baking_subsidy).
Definition with_liquidity_baking_subsidy liquidity_baking_subsidy
(r : record) :=
Build r.(consensus_threshold) r.(baking_reward_fixed_portion)
r.(baking_reward_bonus_per_slot) r.(endorsing_reward_per_slot)
liquidity_baking_subsidy.
End t.
Definition t := t.record.
Definition generate
(consensus_committee_size : int) (blocks_per_minute : Ratio_repr.t) : t :=
let consensus_threshold := ((consensus_committee_size ×i 2) /i 3) +i 1 in
let rewards_per_minute := Tez_repr.mul_exn Tez_repr.one 80 in
let rewards_per_block :=
Tez_repr.div_exn
(Tez_repr.mul_exn rewards_per_minute
blocks_per_minute.(Ratio_repr.t.denominator))
blocks_per_minute.(Ratio_repr.t.numerator) in
let rewards_half := Tez_repr.div_exn rewards_per_block 2 in
let rewards_quarter := Tez_repr.div_exn rewards_per_block 4 in
let bonus_committee_size := consensus_committee_size -i consensus_threshold
in
{| t.consensus_threshold := consensus_threshold;
t.baking_reward_fixed_portion :=
if bonus_committee_size ≤i 0 then
rewards_half
else
rewards_quarter;
t.baking_reward_bonus_per_slot :=
if bonus_committee_size ≤i 0 then
Tez_repr.zero
else
Tez_repr.div_exn rewards_quarter bonus_committee_size;
t.endorsing_reward_per_slot :=
Tez_repr.div_exn rewards_half consensus_committee_size;
t.liquidity_baking_subsidy := Tez_repr.div_exn rewards_per_block 16; |}.
End Generated.
Definition cache_layout (p_value : Constants_parametric_repr.t) : list int :=
[
p_value.(Constants_parametric_repr.t.cache_script_size);
p_value.(Constants_parametric_repr.t.cache_stake_distribution_cycles);
p_value.(Constants_parametric_repr.t.cache_sampler_state_cycles)
].