Skip to main content

🧑‍⚖️ Amendment.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.

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_gtgteqquestion
          (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_gtgteqquestion
        (Alpha_context.Vote.clear_current_proposal ctxt)
        Alpha_context.Voting_period.reset
    end in
  Alpha_context.Vote.update_listings ctxt.

Init function; without side-effects in Coq
Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "invalid_proposal"
      "Invalid proposal"
      "Ballot provided for a proposal that is not the current one."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Invalid proposal"
                  CamlinternalFormatBasics.End_of_format) "Invalid proposal")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_proposal" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_proposal" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "unexpected_proposal"
      "Unexpected proposal" "Proposal recorded outside of a proposal period."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Unexpected proposal"
                  CamlinternalFormatBasics.End_of_format) "Unexpected proposal")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unexpected_proposal" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unexpected_proposal" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "unauthorized_proposal"
      "Unauthorized proposal"
      "The delegate provided for the proposal is not in the voting listings."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Unauthorized proposal"
                  CamlinternalFormatBasics.End_of_format)
                "Unauthorized proposal"))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unauthorized_proposal" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unauthorized_proposal" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "unexpected_ballot"
      "Unexpected ballot" "Ballot recorded outside of a voting period."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Unexpected ballot"
                  CamlinternalFormatBasics.End_of_format) "Unexpected ballot")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unexpected_ballot" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unexpected_ballot" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "unauthorized_ballot"
      "Unauthorized ballot"
      "The delegate provided for the ballot is not in the voting listings."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Unauthorized ballot"
                  CamlinternalFormatBasics.End_of_format) "Unauthorized ballot")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unauthorized_ballot" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unauthorized_ballot" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "duplicate_ballot"
      "Duplicate ballot" "The delegate has already submitted a ballot."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Duplicate ballot"
                  CamlinternalFormatBasics.End_of_format) "Duplicate ballot")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Duplicate_ballot" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Duplicate_ballot" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "too_many_proposals"
      "Too many proposals"
      "The delegate reached the maximum number of allowed proposals."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Too many proposals"
                  CamlinternalFormatBasics.End_of_format) "Too many proposals")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Too_many_proposals" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Too_many_proposals" unit tt) in
  Error_monad.register_error_kind Error_monad.Branch "empty_proposal"
    "Empty proposal" "Proposal lists cannot be empty."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Empty proposal"
                CamlinternalFormatBasics.End_of_format) "Empty proposal")))
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Empty_proposal" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Empty_proposal" unit tt).

Definition record_proposals
  (ctxt : Alpha_context.context) (delegate : Alpha_context.public_key_hash)
  (proposals : list Protocol_hash.t) : M? Alpha_context.context :=
  let? '_ :=
    match proposals with
    | []Error_monad.error_value (Build_extensible "Empty_proposal" unit tt)
    | cons _ _Result.return_unit
    end in
  let? function_parameter := Alpha_context.Voting_period.get_current_kind ctxt
    in
  match function_parameter with
  | Alpha_context.Voting_period.Proposal
    let in_listings := Alpha_context.Vote.in_listings ctxt delegate in
    if in_listings then
      let? count :=
        Alpha_context.Vote.recorded_proposal_count_for_delegate ctxt delegate in
      let '_ :=
        (* ❌ Assert instruction is not handled. *)
        assert unit
          (Alpha_context.Constants.max_proposals_per_delegate i count) in
      let? '_ :=
        Error_monad.error_when
          ((List.compare_length_with proposals
            (Alpha_context.Constants.max_proposals_per_delegate -i count)) >i 0)
          (Build_extensible "Too_many_proposals" unit tt) in
      List.fold_left_es
        (fun (ctxt : Alpha_context.context) ⇒
          fun (proposal : Protocol_hash.t) ⇒
            Alpha_context.Vote.record_proposal ctxt proposal delegate) ctxt
        proposals
    else
      Error_monad.fail (Build_extensible "Unauthorized_proposal" unit tt)
  |
    (Alpha_context.Voting_period.Exploration |
    Alpha_context.Voting_period.Cooldown | Alpha_context.Voting_period.Promotion
    | Alpha_context.Voting_period.Adoption) ⇒
    Error_monad.fail (Build_extensible "Unexpected_proposal" unit tt)
  end.

Definition record_ballot
  (ctxt : Alpha_context.context) (delegate : Alpha_context.public_key_hash)
  (proposal : Protocol_hash.t) (ballot : Alpha_context.Vote.ballot)
  : M? Alpha_context.context :=
  let? function_parameter := Alpha_context.Voting_period.get_current_kind ctxt
    in
  match function_parameter with
  |
    (Alpha_context.Voting_period.Exploration |
    Alpha_context.Voting_period.Promotion) ⇒
    let? current_proposal := Alpha_context.Vote.get_current_proposal ctxt in
    let? '_ :=
      Error_monad.error_unless (Protocol_hash.equal proposal current_proposal)
        (Build_extensible "Invalid_proposal" unit tt) in
    let has_ballot := Alpha_context.Vote.has_recorded_ballot ctxt delegate in
    let? '_ :=
      Error_monad.error_when has_ballot
        (Build_extensible "Duplicate_ballot" unit tt) in
    let in_listings := Alpha_context.Vote.in_listings ctxt delegate in
    if in_listings then
      Alpha_context.Vote.record_ballot ctxt delegate ballot
    else
      Error_monad.fail (Build_extensible "Unauthorized_ballot" unit tt)
  |
    (Alpha_context.Voting_period.Cooldown | Alpha_context.Voting_period.Proposal
    | Alpha_context.Voting_period.Adoption) ⇒
    Error_monad.fail (Build_extensible "Unexpected_ballot" unit tt)
  end.

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.