🧑⚖️ Amendment.v
Translated 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.
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
| 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.
: 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).
(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
| None ⇒ Alpha_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.
: 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
| None ⇒ Alpha_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.
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.