Skip to main content

🗳️ Vote_storage.v

Translated OCaml

See proofs, 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.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_storage.

Definition recorded_proposal_count_for_delegate
  (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_1Option.value_value x_1 0).

Definition record_proposal
  (ctxt : Raw_context.t) (proposal : Protocol_hash.t)
  (proposer : Signature.public_key_hash) : M? Raw_context.t :=
  let? count := recorded_proposal_count_for_delegate ctxt proposer in
  let ctxt :=
    Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.add) ctxt
      proposer (count +i 1) in
  Error_monad.op_gtpipeeq
    (Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.add) ctxt
      (proposal, proposer)) Error_monad.ok.

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)
    (return? 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 : M? (Protocol_hash.Map.(S.INDEXES_MAP.t) int64)) ⇒
        let? weight :=
          Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.get) ctxt
            delegate in
        let? acc_value := acc_value in
        let previous :=
          match Protocol_hash.Map.(S.INDEXES_MAP.find) proposal acc_value with
          | None ⇒ 0
          | Some x_valuex_value
          end in
        return?
          (Protocol_hash.Map.(S.INDEXES_MAP.add) proposal (weight +i64 previous)
            acc_value)).

Definition clear_proposals (ctxt : Raw_context.t) : 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_encoding : Data_encoding.encoding ballots :=
  (let arg :=
    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; |}) in
  fun (eta : Data_encoding.encoding (int64 × int64 × int64)) ⇒ arg None eta)
    (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 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)
    (return? {| ballots.yay := 0; ballots.nay := 0; ballots.pass := 0; |})
    (fun (delegate : Signature.public_key_hash) ⇒
      fun (ballot : Vote_repr.ballot) ⇒
        fun (ballots : M? ballots) ⇒
          let? weight :=
            Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.get) ctxt
              delegate in
          let count := Int64.add weight in
          let? ballots := ballots 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 list (Signature.public_key_hash × Vote_repr.ballot) :=
  Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.bindings).

Definition clear_ballots : Raw_context.t 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.

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 list (Signature.public_key_hash × int64) :=
  Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.bindings).

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_1Option.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
  | Nonereturn? (ctxt, 0)
  | Some powerreturn? (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 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 M? Raw_context.t :=
  Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.remove_existing).

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.