Skip to main content

🧑‍⚖️ Amendment.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.V7.
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
    | NoneSome ([ 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.
Definition start_new_voting_period (ctxt : Alpha_context.context)
  : M? Alpha_context.context :=
  let? kind_value := Alpha_context.Voting_period.get_current_kind ctxt in
  let? ctxt :=
    match kind_value with
    | Alpha_context.Voting_period.Proposal
      let? proposal := select_winning_proposal ctxt in
      let? ctxt := Alpha_context.Vote.clear_proposals ctxt in
      match proposal with
      | NoneAlpha_context.Voting_period.reset ctxt
      | Some proposal
        Error_monad.op_gtgteqquestion
          (Alpha_context.Vote.init_current_proposal ctxt proposal)
          Alpha_context.Voting_period.succ
      end
    | Alpha_context.Voting_period.Exploration
      let? '(ctxt, approved) := get_approval_and_update_participation_ema ctxt
        in
      if approved then
        Alpha_context.Voting_period.succ ctxt
      else
        let ctxt := Alpha_context.Vote.clear_current_proposal ctxt in
        Alpha_context.Voting_period.reset ctxt
    | Alpha_context.Voting_period.Cooldown
      Alpha_context.Voting_period.succ ctxt
    | Alpha_context.Voting_period.Promotion
      let? '(ctxt, approved) := get_approval_and_update_participation_ema ctxt
        in
      if approved then
        Alpha_context.Voting_period.succ ctxt
      else
        Error_monad.op_gtgteq (Alpha_context.Vote.clear_current_proposal ctxt)
          Alpha_context.Voting_period.reset
    | Alpha_context.Voting_period.Adoption
      let? proposal := Alpha_context.Vote.get_current_proposal ctxt in
      let ctxt := Alpha_context.activate ctxt proposal in
      Error_monad.op_gtgteq (Alpha_context.Vote.clear_current_proposal ctxt)
        Alpha_context.Voting_period.reset
    end in
  Alpha_context.Vote.update_listings ctxt.

Definition may_start_new_voting_period (ctxt : Alpha_context.context)
  : M? Alpha_context.context :=
  let? is_last := Alpha_context.Voting_period.is_last_block ctxt in
  if is_last then
    start_new_voting_period ctxt
  else
    return? ctxt.

Definition get_testnet_dictator
  (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
  : option Alpha_context.public_key_hash :=
  match
    ((Alpha_context.Constants.testnet_dictator ctxt),
      match Alpha_context.Constants.testnet_dictator ctxt with
      | Some pkhChain_id.op_ltgt chain_id Alpha_context.Constants.mainnet_id
      | _false
      end) with
  | (Some pkh, true)Some pkh
  | (_, _)None
  end.

Definition is_testnet_dictator
  (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
  (delegate : Signature.public_key_hash) : bool :=
  match get_testnet_dictator ctxt chain_id with
  | Some pkh
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) pkh delegate
  | _false
  end.

Helpers to apply [Proposals] operations from a registered dictator of a test chain. These operations let the dictator immediately change the current voting period's kind, and the current proposal if applicable. Of course, there must never be such a dictator on mainnet.
Forcibly update the voting period according to a voting dictator's Proposals operation.
{!check_proposals} should guarantee that this function cannot return an error.
  Definition record_proposals
    (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
    (proposals : list Alpha_context.Vote.proposal) : M? Alpha_context.context :=
    let? ctxt := Alpha_context.Vote.clear_ballots ctxt in
    let? ctxt := Alpha_context.Vote.clear_proposals ctxt in
    let ctxt := Alpha_context.Vote.clear_current_proposal ctxt in
    let ctxt := Alpha_context.record_dictator_proposal_seen ctxt in
    match proposals with
    | []
      Alpha_context.Voting_period.Testnet_dictator.overwrite_current_kind ctxt
        chain_id Voting_period_repr.Proposal
    | cons proposal []
      let? ctxt := Alpha_context.Vote.init_current_proposal ctxt proposal in
      Alpha_context.Voting_period.Testnet_dictator.overwrite_current_kind ctxt
        chain_id Voting_period_repr.Adoption
    | cons _ (cons _ _) ⇒
      Error_monad.Lwt_tzresult_syntax.fail
        (Build_extensible "Testnet_dictator_multiple_proposals" unit tt)
    end.
End Testnet_dictator.

Definition apply_proposals
  (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
  (contents : Alpha_context.contents)
  : M? (Alpha_context.context × Apply_results.contents_result_list) :=
  match contents with
  |
    Alpha_context.Proposals {|
      Alpha_context.contents.Proposals.source := source;
        Alpha_context.contents.Proposals.period := _;
        Alpha_context.contents.Proposals.proposals := proposals
        |} ⇒
    let? ctxt :=
      if is_testnet_dictator ctxt chain_id source then
        Testnet_dictator.record_proposals ctxt chain_id proposals
      else
        if Alpha_context.dictator_proposal_seen ctxt then
          return? ctxt
        else
          let? count :=
            Alpha_context.Vote.get_delegate_proposal_count ctxt source in
          let new_count := count +i (List.length proposals) in
          let ctxt :=
            Alpha_context.Vote.set_delegate_proposal_count ctxt source new_count
            in
          let ctxt :=
            List.fold_left_s
              (fun (ctxt : Alpha_context.context) ⇒
                fun (proposal : Alpha_context.Vote.proposal) ⇒
                  Alpha_context.Vote.add_proposal ctxt source proposal) ctxt
              proposals in
          return? ctxt in
    return? (ctxt, (Apply_results.Single_result Apply_results.Proposals_result))
  | _unreachable_gadt_branch
  end.

Definition apply_ballot
  (ctxt : Alpha_context.t) (contents : Alpha_context.contents)
  : M? (Alpha_context.t × Apply_results.contents_result_list) :=
  match contents with
  |
    Alpha_context.Ballot {|
      Alpha_context.contents.Ballot.source := source;
        Alpha_context.contents.Ballot.period := _;
        Alpha_context.contents.Ballot.proposal := _;
        Alpha_context.contents.Ballot.ballot := ballot
        |} ⇒
    let? ctxt :=
      if Alpha_context.dictator_proposal_seen ctxt then
        return? ctxt
      else
        Alpha_context.Vote.record_ballot ctxt source ballot in
    return? (ctxt, (Apply_results.Single_result Apply_results.Ballot_result))
  | _unreachable_gadt_branch
  end.