🗳️ Vote_storage.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.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_costs.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Definition get_delegate_proposal_count
(ctxt : Raw_context.t) (proposer : Signature.public_key_hash) : M? int :=
Error_monad.op_gtpipeeqquestion
(Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.find) ctxt
proposer) (fun x_1 ⇒ Option.value_value x_1 0).
Definition set_delegate_proposal_count
(ctxt : Raw_context.t) (proposer : Signature.public_key_hash) (count : int)
: Raw_context.t :=
Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.add) ctxt
proposer count.
Definition has_proposed
(ctxt : Raw_context.t) (proposer : Signature.public_key_hash)
(proposal : Protocol_hash.t) : bool :=
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.mem) ctxt
(proposal, proposer).
Definition add_proposal
(ctxt : Raw_context.t) (proposer : Signature.public_key_hash)
(proposal : Protocol_hash.t) : Raw_context.t :=
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.add) ctxt
(proposal, proposer).
Definition get_proposals (ctxt : Raw_context.t)
: M? (Protocol_hash.Map.(S.INDEXES_MAP.t) int64) :=
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.fold) ctxt
(Variant.Build "Sorted" unit tt) Protocol_hash.Map.(S.INDEXES_MAP.empty)
(fun (function_parameter : Protocol_hash.t × Signature.public_key_hash) ⇒
let '(proposal, delegate) := function_parameter in
fun (acc_value : Protocol_hash.Map.(S.INDEXES_MAP.t) int64) ⇒
let? weight :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.get) ctxt
delegate in
let previous :=
match Protocol_hash.Map.(S.INDEXES_MAP.find) proposal acc_value with
| None ⇒ 0
| Some x_value ⇒ x_value
end in
return?
(Protocol_hash.Map.(S.INDEXES_MAP.add) proposal (weight +i64 previous)
acc_value)).
Definition clear_proposals (ctxt : Raw_context.t) : M? Raw_context.t :=
let? ctxt :=
Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.clear) ctxt
in
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.clear) ctxt.
Module ballots.
Record record : Set := Build {
yay : int64;
nay : int64;
pass : int64;
}.
Definition with_yay yay (r : record) :=
Build yay r.(nay) r.(pass).
Definition with_nay nay (r : record) :=
Build r.(yay) nay r.(pass).
Definition with_pass pass (r : record) :=
Build r.(yay) r.(nay) pass.
End ballots.
Definition ballots := ballots.record.
Definition ballots_zero : ballots :=
{| ballots.yay := 0; ballots.nay := 0; ballots.pass := 0; |}.
Definition ballots_encoding : Data_encoding.encoding ballots :=
Data_encoding.conv
(fun (function_parameter : ballots) ⇒
let '{| ballots.yay := yay; ballots.nay := nay; ballots.pass := pass |} :=
function_parameter in
(yay, nay, pass))
(fun (function_parameter : int64 × int64 × int64) ⇒
let '(yay, nay, pass) := function_parameter in
{| ballots.yay := yay; ballots.nay := nay; ballots.pass := pass; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "yay" Data_encoding.int64_value)
(Data_encoding.req None None "nay" Data_encoding.int64_value)
(Data_encoding.req None None "pass" Data_encoding.int64_value)).
Definition equal_ballots (b1 : ballots) (b2 : ballots) : bool :=
(Int64.equal b1.(ballots.yay) b2.(ballots.yay)) &&
((Int64.equal b1.(ballots.nay) b2.(ballots.nay)) &&
(Int64.equal b1.(ballots.pass) b2.(ballots.pass))).
Definition pp_ballots (ppf : Format.formatter) (b_value : ballots) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "{ yay = "
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal "; nay = "
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal "; pass = "
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " }"
CamlinternalFormatBasics.End_of_format)))))))
"{ yay = %Ld; nay = %Ld; pass = %Ld }") b_value.(ballots.yay)
b_value.(ballots.nay) b_value.(ballots.pass).
Definition has_recorded_ballot
: Raw_context.t → Signature.public_key_hash → bool :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.mem).
Definition record_ballot
: Raw_context.t → Signature.public_key_hash → Vote_repr.ballot →
M? Raw_context.t :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.init_value).
Definition get_ballots (ctxt : Raw_context.t) : M? ballots :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.fold) ctxt
(Variant.Build "Sorted" unit tt) ballots_zero
(fun (delegate : Signature.public_key_hash) ⇒
fun (ballot : Vote_repr.ballot) ⇒
fun (ballots : ballots) ⇒
let? weight :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.get) ctxt
delegate in
let count := Int64.add weight in
match ballot with
| Vote_repr.Yay ⇒
return? (ballots.with_yay (count ballots.(ballots.yay)) ballots)
| Vote_repr.Nay ⇒
return? (ballots.with_nay (count ballots.(ballots.nay)) ballots)
| Vote_repr.Pass ⇒
return? (ballots.with_pass (count ballots.(ballots.pass)) ballots)
end).
Definition get_ballot_list
: Raw_context.t → M? (list (Signature.public_key_hash × Vote_repr.ballot)) :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.bindings).
Definition clear_ballots : Raw_context.t → M? Raw_context.t :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.clear).
Definition listings_encoding
: Data_encoding.encoding (list (Signature.public_key_hash × int64)) :=
Data_encoding.list_value None
(Data_encoding.obj2
(Data_encoding.req None None "pkh"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "voting_power" Data_encoding.int64_value)).
Definition update_listings (ctxt : Raw_context.t) : M? Raw_context.t :=
let? ctxt :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.clear) ctxt in
let? '(ctxt, total) :=
Stake_storage.fold ctxt
(fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(delegate, stake) := function_parameter in
fun (function_parameter : Raw_context.t × int64) ⇒
let '(ctxt, total) := function_parameter in
let weight := Tez_repr.to_mutez stake in
let? ctxt :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.init_value)
ctxt delegate weight in
return? (ctxt, (total +i64 weight))) (Variant.Build "Sorted" unit tt)
(ctxt, 0) in
let ctxt :=
Storage.Vote.Voting_power_in_listings.(Storage_sigs.Single_data_storage.add)
ctxt total in
return? ctxt.
Module delegate_info.
Record record : Set := Build {
voting_power : option Int64.t;
current_ballot : option Vote_repr.ballot;
current_proposals : list Protocol_hash.t;
remaining_proposals : int;
}.
Definition with_voting_power voting_power (r : record) :=
Build voting_power r.(current_ballot) r.(current_proposals)
r.(remaining_proposals).
Definition with_current_ballot current_ballot (r : record) :=
Build r.(voting_power) current_ballot r.(current_proposals)
r.(remaining_proposals).
Definition with_current_proposals current_proposals (r : record) :=
Build r.(voting_power) r.(current_ballot) current_proposals
r.(remaining_proposals).
Definition with_remaining_proposals remaining_proposals (r : record) :=
Build r.(voting_power) r.(current_ballot) r.(current_proposals)
remaining_proposals.
End delegate_info.
Definition delegate_info := delegate_info.record.
Definition pp_delegate_info
(ppf : Format.formatter) (info_value : delegate_info) : unit :=
match info_value.(delegate_info.voting_power) with
| None ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Voting power: none"
CamlinternalFormatBasics.End_of_format) "Voting power: none")
| Some p_value ⇒
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Voting power: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)) "Voting power: %a")
Tez_repr.pp (Tez_repr.of_mutez_exn p_value) in
let '_ :=
match info_value.(delegate_info.current_ballot) with
| None ⇒ tt
| Some ballot ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Current ballot: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))
"@,Current ballot: %a") Vote_repr.pp_ballot ballot
end in
match info_value.(delegate_info.current_proposals) with
| [] ⇒
if info_value.(delegate_info.remaining_proposals) ≠i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Remaining proposals: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)))
"@,Remaining proposals: %d")
info_value.(delegate_info.remaining_proposals)
else
tt
| proposals ⇒
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "Current proposals:"
CamlinternalFormatBasics.End_of_format)))
"@,@[<v 2>Current proposals:") in
let '_ :=
List.iter
(fun (p_value : Protocol_hash.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "- "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))) "@,- %a")
Protocol_hash.pp p_value) proposals in
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format) "@]") in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Remaining proposals: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)))
"@,Remaining proposals: %d")
info_value.(delegate_info.remaining_proposals)
end
end.
Definition delegate_info_encoding : Data_encoding.encoding delegate_info :=
Data_encoding.conv
(fun (function_parameter : delegate_info) ⇒
let '{|
delegate_info.voting_power := voting_power;
delegate_info.current_ballot := current_ballot;
delegate_info.current_proposals := current_proposals;
delegate_info.remaining_proposals := remaining_proposals
|} := function_parameter in
(voting_power, current_ballot, current_proposals, remaining_proposals))
(fun (function_parameter :
option Int64.t × option Vote_repr.ballot × list Protocol_hash.t × int) ⇒
let
'(voting_power, current_ballot, current_proposals, remaining_proposals) :=
function_parameter in
{| delegate_info.voting_power := voting_power;
delegate_info.current_ballot := current_ballot;
delegate_info.current_proposals := current_proposals;
delegate_info.remaining_proposals := remaining_proposals; |}) None
(Data_encoding.obj4
(Data_encoding.opt None None "voting_power" Data_encoding.int64_value)
(Data_encoding.opt None None "current_ballot" Vote_repr.ballot_encoding)
(Data_encoding.dft None None "current_proposals"
(Data_encoding.list_value None Protocol_hash.encoding) nil)
(Data_encoding.dft None None "remaining_proposals" Data_encoding.int31 0)).
Definition in_listings : Raw_context.t → Signature.public_key_hash → bool :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.mem).
Definition get_listings
: Raw_context.t → M? (list (Signature.public_key_hash × int64)) :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.bindings).
Definition get_delegate_info
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? delegate_info :=
let? voting_power :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt delegate
in
match voting_power with
| None ⇒
return?
{| delegate_info.voting_power := voting_power;
delegate_info.current_ballot := None;
delegate_info.current_proposals := nil;
delegate_info.remaining_proposals := 0; |}
| Some _ ⇒
let? period := Voting_period_storage.get_current_kind ctxt in
let? current_ballot :=
match period with
| (Voting_period_repr.Exploration | Voting_period_repr.Promotion) ⇒
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.find) ctxt
delegate
|
(Voting_period_repr.Proposal | Voting_period_repr.Cooldown |
Voting_period_repr.Adoption) ⇒ return? None
end in
let? current_proposals :=
match period with
|
(Voting_period_repr.Exploration | Voting_period_repr.Promotion |
Voting_period_repr.Cooldown | Voting_period_repr.Adoption) ⇒
return? nil
| Voting_period_repr.Proposal ⇒
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.fold) ctxt
(Variant.Build "Undefined" unit tt) nil
(fun (function_parameter :
Protocol_hash.t × Signature.public_key_hash) ⇒
let '(h_value, d_value) := function_parameter in
fun (acc_value : list Protocol_hash.t) ⇒
if
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
d_value delegate
then
return? (cons h_value acc_value)
else
return? acc_value)
end in
let remaining_proposals :=
match period with
| Voting_period_repr.Proposal ⇒
Constants_repr.max_proposals_per_delegate -i
(List.length current_proposals)
| _ ⇒ 0
end in
return?
{| delegate_info.voting_power := voting_power;
delegate_info.current_ballot := current_ballot;
delegate_info.current_proposals := current_proposals;
delegate_info.remaining_proposals := remaining_proposals; |}
end.
Definition get_voting_power_free
(ctxt : Raw_context.t) (owner : Signature.public_key_hash) : M? int64 :=
Error_monad.op_gtpipeeqquestion
(Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt owner)
(fun x_1 ⇒ Option.value_value x_1 0).
Definition get_voting_power
(ctxt : Raw_context.t) (owner : Signature.public_key_hash)
: M? (Raw_context.t × int64) :=
let? ctxt := Raw_context.consume_gas ctxt (Storage_costs.read_access 4 8) in
let? function_parameter :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt owner in
match function_parameter with
| None ⇒ return? (ctxt, 0)
| Some power ⇒ return? (ctxt, power)
end.
Definition get_total_voting_power_free : Raw_context.t → M? int64 :=
Storage.Vote.Voting_power_in_listings.(Storage_sigs.Single_data_storage.get).
Definition get_total_voting_power (ctxt : Raw_context.t)
: M? (Raw_context.t × int64) :=
let? ctxt := Raw_context.consume_gas ctxt (Storage_costs.read_access 2 8) in
let? total_voting_power := get_total_voting_power_free ctxt in
return? (ctxt, total_voting_power).
Definition get_current_quorum (ctxt : Raw_context.t) : M? int32 :=
let? participation_ema :=
Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.get) ctxt
in
let quorum_min := Constants_storage.quorum_min ctxt in
let quorum_max := Constants_storage.quorum_max ctxt in
let quorum_diff := quorum_max -i32 quorum_min in
return? (quorum_min +i32 ((participation_ema ×i32 quorum_diff) /i32 10000)).
Definition get_participation_ema : Raw_context.t → M? int32 :=
Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.get).
Definition set_participation_ema : Raw_context.t → int32 → M? Raw_context.t :=
Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.update).
Definition current_proposal_exists : Raw_context.t → bool :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.mem).
Definition get_current_proposal : Raw_context.t → M? Protocol_hash.t :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.get).
Definition find_current_proposal
: Raw_context.t → M? (option Protocol_hash.t) :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.find).
Definition init_current_proposal
: Raw_context.t → Protocol_hash.t → M? Raw_context.t :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.init_value).
Definition clear_current_proposal : Raw_context.t → Raw_context.t :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.remove).
Definition init_value (ctxt : Raw_context.t) (start_position : Int32.t)
: M? Raw_context.t :=
let participation_ema := Constants_storage.quorum_max ctxt in
let? ctxt :=
Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.init_value)
ctxt participation_ema in
Voting_period_storage.init_first_period ctxt start_position.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_costs.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Definition get_delegate_proposal_count
(ctxt : Raw_context.t) (proposer : Signature.public_key_hash) : M? int :=
Error_monad.op_gtpipeeqquestion
(Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.find) ctxt
proposer) (fun x_1 ⇒ Option.value_value x_1 0).
Definition set_delegate_proposal_count
(ctxt : Raw_context.t) (proposer : Signature.public_key_hash) (count : int)
: Raw_context.t :=
Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.add) ctxt
proposer count.
Definition has_proposed
(ctxt : Raw_context.t) (proposer : Signature.public_key_hash)
(proposal : Protocol_hash.t) : bool :=
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.mem) ctxt
(proposal, proposer).
Definition add_proposal
(ctxt : Raw_context.t) (proposer : Signature.public_key_hash)
(proposal : Protocol_hash.t) : Raw_context.t :=
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.add) ctxt
(proposal, proposer).
Definition get_proposals (ctxt : Raw_context.t)
: M? (Protocol_hash.Map.(S.INDEXES_MAP.t) int64) :=
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.fold) ctxt
(Variant.Build "Sorted" unit tt) Protocol_hash.Map.(S.INDEXES_MAP.empty)
(fun (function_parameter : Protocol_hash.t × Signature.public_key_hash) ⇒
let '(proposal, delegate) := function_parameter in
fun (acc_value : Protocol_hash.Map.(S.INDEXES_MAP.t) int64) ⇒
let? weight :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.get) ctxt
delegate in
let previous :=
match Protocol_hash.Map.(S.INDEXES_MAP.find) proposal acc_value with
| None ⇒ 0
| Some x_value ⇒ x_value
end in
return?
(Protocol_hash.Map.(S.INDEXES_MAP.add) proposal (weight +i64 previous)
acc_value)).
Definition clear_proposals (ctxt : Raw_context.t) : M? Raw_context.t :=
let? ctxt :=
Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.clear) ctxt
in
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.clear) ctxt.
Module ballots.
Record record : Set := Build {
yay : int64;
nay : int64;
pass : int64;
}.
Definition with_yay yay (r : record) :=
Build yay r.(nay) r.(pass).
Definition with_nay nay (r : record) :=
Build r.(yay) nay r.(pass).
Definition with_pass pass (r : record) :=
Build r.(yay) r.(nay) pass.
End ballots.
Definition ballots := ballots.record.
Definition ballots_zero : ballots :=
{| ballots.yay := 0; ballots.nay := 0; ballots.pass := 0; |}.
Definition ballots_encoding : Data_encoding.encoding ballots :=
Data_encoding.conv
(fun (function_parameter : ballots) ⇒
let '{| ballots.yay := yay; ballots.nay := nay; ballots.pass := pass |} :=
function_parameter in
(yay, nay, pass))
(fun (function_parameter : int64 × int64 × int64) ⇒
let '(yay, nay, pass) := function_parameter in
{| ballots.yay := yay; ballots.nay := nay; ballots.pass := pass; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "yay" Data_encoding.int64_value)
(Data_encoding.req None None "nay" Data_encoding.int64_value)
(Data_encoding.req None None "pass" Data_encoding.int64_value)).
Definition equal_ballots (b1 : ballots) (b2 : ballots) : bool :=
(Int64.equal b1.(ballots.yay) b2.(ballots.yay)) &&
((Int64.equal b1.(ballots.nay) b2.(ballots.nay)) &&
(Int64.equal b1.(ballots.pass) b2.(ballots.pass))).
Definition pp_ballots (ppf : Format.formatter) (b_value : ballots) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "{ yay = "
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal "; nay = "
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal "; pass = "
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " }"
CamlinternalFormatBasics.End_of_format)))))))
"{ yay = %Ld; nay = %Ld; pass = %Ld }") b_value.(ballots.yay)
b_value.(ballots.nay) b_value.(ballots.pass).
Definition has_recorded_ballot
: Raw_context.t → Signature.public_key_hash → bool :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.mem).
Definition record_ballot
: Raw_context.t → Signature.public_key_hash → Vote_repr.ballot →
M? Raw_context.t :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.init_value).
Definition get_ballots (ctxt : Raw_context.t) : M? ballots :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.fold) ctxt
(Variant.Build "Sorted" unit tt) ballots_zero
(fun (delegate : Signature.public_key_hash) ⇒
fun (ballot : Vote_repr.ballot) ⇒
fun (ballots : ballots) ⇒
let? weight :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.get) ctxt
delegate in
let count := Int64.add weight in
match ballot with
| Vote_repr.Yay ⇒
return? (ballots.with_yay (count ballots.(ballots.yay)) ballots)
| Vote_repr.Nay ⇒
return? (ballots.with_nay (count ballots.(ballots.nay)) ballots)
| Vote_repr.Pass ⇒
return? (ballots.with_pass (count ballots.(ballots.pass)) ballots)
end).
Definition get_ballot_list
: Raw_context.t → M? (list (Signature.public_key_hash × Vote_repr.ballot)) :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.bindings).
Definition clear_ballots : Raw_context.t → M? Raw_context.t :=
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.clear).
Definition listings_encoding
: Data_encoding.encoding (list (Signature.public_key_hash × int64)) :=
Data_encoding.list_value None
(Data_encoding.obj2
(Data_encoding.req None None "pkh"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "voting_power" Data_encoding.int64_value)).
Definition update_listings (ctxt : Raw_context.t) : M? Raw_context.t :=
let? ctxt :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.clear) ctxt in
let? '(ctxt, total) :=
Stake_storage.fold ctxt
(fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(delegate, stake) := function_parameter in
fun (function_parameter : Raw_context.t × int64) ⇒
let '(ctxt, total) := function_parameter in
let weight := Tez_repr.to_mutez stake in
let? ctxt :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.init_value)
ctxt delegate weight in
return? (ctxt, (total +i64 weight))) (Variant.Build "Sorted" unit tt)
(ctxt, 0) in
let ctxt :=
Storage.Vote.Voting_power_in_listings.(Storage_sigs.Single_data_storage.add)
ctxt total in
return? ctxt.
Module delegate_info.
Record record : Set := Build {
voting_power : option Int64.t;
current_ballot : option Vote_repr.ballot;
current_proposals : list Protocol_hash.t;
remaining_proposals : int;
}.
Definition with_voting_power voting_power (r : record) :=
Build voting_power r.(current_ballot) r.(current_proposals)
r.(remaining_proposals).
Definition with_current_ballot current_ballot (r : record) :=
Build r.(voting_power) current_ballot r.(current_proposals)
r.(remaining_proposals).
Definition with_current_proposals current_proposals (r : record) :=
Build r.(voting_power) r.(current_ballot) current_proposals
r.(remaining_proposals).
Definition with_remaining_proposals remaining_proposals (r : record) :=
Build r.(voting_power) r.(current_ballot) r.(current_proposals)
remaining_proposals.
End delegate_info.
Definition delegate_info := delegate_info.record.
Definition pp_delegate_info
(ppf : Format.formatter) (info_value : delegate_info) : unit :=
match info_value.(delegate_info.voting_power) with
| None ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Voting power: none"
CamlinternalFormatBasics.End_of_format) "Voting power: none")
| Some p_value ⇒
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Voting power: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)) "Voting power: %a")
Tez_repr.pp (Tez_repr.of_mutez_exn p_value) in
let '_ :=
match info_value.(delegate_info.current_ballot) with
| None ⇒ tt
| Some ballot ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Current ballot: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))
"@,Current ballot: %a") Vote_repr.pp_ballot ballot
end in
match info_value.(delegate_info.current_proposals) with
| [] ⇒
if info_value.(delegate_info.remaining_proposals) ≠i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Remaining proposals: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)))
"@,Remaining proposals: %d")
info_value.(delegate_info.remaining_proposals)
else
tt
| proposals ⇒
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "Current proposals:"
CamlinternalFormatBasics.End_of_format)))
"@,@[<v 2>Current proposals:") in
let '_ :=
List.iter
(fun (p_value : Protocol_hash.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "- "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))) "@,- %a")
Protocol_hash.pp p_value) proposals in
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format) "@]") in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Remaining proposals: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)))
"@,Remaining proposals: %d")
info_value.(delegate_info.remaining_proposals)
end
end.
Definition delegate_info_encoding : Data_encoding.encoding delegate_info :=
Data_encoding.conv
(fun (function_parameter : delegate_info) ⇒
let '{|
delegate_info.voting_power := voting_power;
delegate_info.current_ballot := current_ballot;
delegate_info.current_proposals := current_proposals;
delegate_info.remaining_proposals := remaining_proposals
|} := function_parameter in
(voting_power, current_ballot, current_proposals, remaining_proposals))
(fun (function_parameter :
option Int64.t × option Vote_repr.ballot × list Protocol_hash.t × int) ⇒
let
'(voting_power, current_ballot, current_proposals, remaining_proposals) :=
function_parameter in
{| delegate_info.voting_power := voting_power;
delegate_info.current_ballot := current_ballot;
delegate_info.current_proposals := current_proposals;
delegate_info.remaining_proposals := remaining_proposals; |}) None
(Data_encoding.obj4
(Data_encoding.opt None None "voting_power" Data_encoding.int64_value)
(Data_encoding.opt None None "current_ballot" Vote_repr.ballot_encoding)
(Data_encoding.dft None None "current_proposals"
(Data_encoding.list_value None Protocol_hash.encoding) nil)
(Data_encoding.dft None None "remaining_proposals" Data_encoding.int31 0)).
Definition in_listings : Raw_context.t → Signature.public_key_hash → bool :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.mem).
Definition get_listings
: Raw_context.t → M? (list (Signature.public_key_hash × int64)) :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.bindings).
Definition get_delegate_info
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? delegate_info :=
let? voting_power :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt delegate
in
match voting_power with
| None ⇒
return?
{| delegate_info.voting_power := voting_power;
delegate_info.current_ballot := None;
delegate_info.current_proposals := nil;
delegate_info.remaining_proposals := 0; |}
| Some _ ⇒
let? period := Voting_period_storage.get_current_kind ctxt in
let? current_ballot :=
match period with
| (Voting_period_repr.Exploration | Voting_period_repr.Promotion) ⇒
Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.find) ctxt
delegate
|
(Voting_period_repr.Proposal | Voting_period_repr.Cooldown |
Voting_period_repr.Adoption) ⇒ return? None
end in
let? current_proposals :=
match period with
|
(Voting_period_repr.Exploration | Voting_period_repr.Promotion |
Voting_period_repr.Cooldown | Voting_period_repr.Adoption) ⇒
return? nil
| Voting_period_repr.Proposal ⇒
Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.fold) ctxt
(Variant.Build "Undefined" unit tt) nil
(fun (function_parameter :
Protocol_hash.t × Signature.public_key_hash) ⇒
let '(h_value, d_value) := function_parameter in
fun (acc_value : list Protocol_hash.t) ⇒
if
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
d_value delegate
then
return? (cons h_value acc_value)
else
return? acc_value)
end in
let remaining_proposals :=
match period with
| Voting_period_repr.Proposal ⇒
Constants_repr.max_proposals_per_delegate -i
(List.length current_proposals)
| _ ⇒ 0
end in
return?
{| delegate_info.voting_power := voting_power;
delegate_info.current_ballot := current_ballot;
delegate_info.current_proposals := current_proposals;
delegate_info.remaining_proposals := remaining_proposals; |}
end.
Definition get_voting_power_free
(ctxt : Raw_context.t) (owner : Signature.public_key_hash) : M? int64 :=
Error_monad.op_gtpipeeqquestion
(Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt owner)
(fun x_1 ⇒ Option.value_value x_1 0).
Definition get_voting_power
(ctxt : Raw_context.t) (owner : Signature.public_key_hash)
: M? (Raw_context.t × int64) :=
let? ctxt := Raw_context.consume_gas ctxt (Storage_costs.read_access 4 8) in
let? function_parameter :=
Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt owner in
match function_parameter with
| None ⇒ return? (ctxt, 0)
| Some power ⇒ return? (ctxt, power)
end.
Definition get_total_voting_power_free : Raw_context.t → M? int64 :=
Storage.Vote.Voting_power_in_listings.(Storage_sigs.Single_data_storage.get).
Definition get_total_voting_power (ctxt : Raw_context.t)
: M? (Raw_context.t × int64) :=
let? ctxt := Raw_context.consume_gas ctxt (Storage_costs.read_access 2 8) in
let? total_voting_power := get_total_voting_power_free ctxt in
return? (ctxt, total_voting_power).
Definition get_current_quorum (ctxt : Raw_context.t) : M? int32 :=
let? participation_ema :=
Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.get) ctxt
in
let quorum_min := Constants_storage.quorum_min ctxt in
let quorum_max := Constants_storage.quorum_max ctxt in
let quorum_diff := quorum_max -i32 quorum_min in
return? (quorum_min +i32 ((participation_ema ×i32 quorum_diff) /i32 10000)).
Definition get_participation_ema : Raw_context.t → M? int32 :=
Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.get).
Definition set_participation_ema : Raw_context.t → int32 → M? Raw_context.t :=
Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.update).
Definition current_proposal_exists : Raw_context.t → bool :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.mem).
Definition get_current_proposal : Raw_context.t → M? Protocol_hash.t :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.get).
Definition find_current_proposal
: Raw_context.t → M? (option Protocol_hash.t) :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.find).
Definition init_current_proposal
: Raw_context.t → Protocol_hash.t → M? Raw_context.t :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.init_value).
Definition clear_current_proposal : Raw_context.t → Raw_context.t :=
Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.remove).
Definition init_value (ctxt : Raw_context.t) (start_position : Int32.t)
: M? Raw_context.t :=
let participation_ema := Constants_storage.quorum_max ctxt in
let? ctxt :=
Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.init_value)
ctxt participation_ema in
Voting_period_storage.init_first_period ctxt start_position.