🎛️ Constants_repr.v

Translated OCaml

See proofs, Gitlab , 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).

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)
  ].