🧑‍⚖️ Amendment.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.

Returns the proposal submitted by the most delegates. Returns None in case of a tie, if proposal quorum is below required minimum or if there are no proposals.

Definition select_winning_proposal (ctxt : Alpha_context.context)
  : M ? (option Protocol_hash.t ) :=
  let ? proposals := Alpha_context.Vote.get_proposals ctxt in
  let merge {A : Set}
    (proposal : A) (vote : int64) (winners : option (list A × int64))
    : option (list A × int64) :=
    match winners with
    | None ⇒ Some ([ proposal ], vote)
    | (Some (winners, winners_vote)) as previous ⇒
      if vote =i64 winners_vote then
        Some ((cons proposal winners), winners_vote)
      else
        if vote >i64 winners_vote then
          Some ([ proposal ], vote)
        else
          previous
    end in
  match Protocol_hash.Map.(S.INDEXES_MAP.fold) merge proposals None with
  | Some (cons proposal [], vote) ⇒
    let ? max_vote := Alpha_context.Vote.get_total_voting_power_free ctxt in
    let min_proposal_quorum :=
      Z.of_int32 (Alpha_context.Constants.min_proposal_quorum ctxt) in
    let min_vote_to_pass :=
      Z.to_int64
        ((min_proposal_quorum ×Z (Z.of_int64 max_vote )) /Z (Z.of_int 10000)) in
    if vote ≥i64 min_vote_to_pass then
      Error_monad.return_some proposal
    else
      Error_monad.return_none
  | _ ⇒ Error_monad.return_none
  end.

A proposal is approved if it has supermajority and the participation reaches the current quorum. Supermajority means the yays are more 8/10 of casted votes. The participation is the ratio of all received votes, including passes, with respect to the number of possible votes. The participation EMA (exponential moving average) uses the last participation EMA and the current participation./ The expected quorum is calculated using the last participation EMA, capped by the min/max quorum protocol constants.

Definition approval_and_participation_ema
  (ballots : Alpha_context.Vote.ballots) (maximum_vote : int64)
  (participation_ema : int32) (expected_quorum : int32) : bool × int32 :=
  let casted_votes :=
    ballots.(Alpha_context.Vote.ballots.yay) +i64
    ballots.(Alpha_context.Vote.ballots.nay) in
  let all_votes := casted_votes +i64 ballots.(Alpha_context.Vote.ballots.pass)
    in
  let supermajority := (8 ×i64 casted_votes ) /i64 10 in
  let participation :=
    Z.to_int32
      (((Z.of_int64 all_votes ) ×Z (Z.of_int 10000)) /Z (Z.of_int64 maximum_vote ))
    in
  let approval :=
    (participation ≥i32 expected_quorum ) &&
    (ballots.(Alpha_context.Vote.ballots.yay) ≥i64 supermajority ) in
  let new_participation_ema :=
    ((8 ×i32 participation_ema ) +i32 (2 ×i32 participation )) /i32 10 in
  (approval, new_participation_ema).

Definition get_approval_and_update_participation_ema
  (ctxt : Alpha_context.context) : M ? (Alpha_context.context × bool) :=
  let ? ballots := Alpha_context.Vote.get_ballots ctxt in
  let ? maximum_vote := Alpha_context.Vote.get_total_voting_power_free ctxt in
  let ? participation_ema := Alpha_context.Vote.get_participation_ema ctxt in
  let ? expected_quorum := Alpha_context.Vote.get_current_quorum ctxt in
  let ? ctxt := Alpha_context.Vote.clear_ballots ctxt in
  let '(approval, new_participation_ema) :=
    approval_and_participation_ema ballots maximum_vote participation_ema
      expected_quorum in
  let ? ctxt :=
    Alpha_context.Vote.set_participation_ema ctxt new_participation_ema in
  return ? (ctxt, approval).

Implements the state machine of the amendment procedure. Note that [update_listings], that computes the vote weight of each delegate, is run at the end of each voting period. This state-machine prepare the voting_period for the next block.

Apply a [Proposals] operation from a registered dictator of a test chain. This forcibly updates the voting period, changing the current voting period kind and the current proposal if applicable. Of course, there must never be such a dictator on mainnet: see {!is_testnet_dictator}.