🗳️ Voting_period_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.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.

Definition blocks_per_voting_period (ctxt : Raw_context.t) : int32 :=
  (Constants_storage.cycles_per_voting_period ctxt) ×i32
  (Constants_storage.blocks_per_cycle ctxt).

Definition set_current
  : Raw_context.t → Voting_period_repr.voting_period → M? Raw_context.t :=
  Storage.Vote.Current_period.(Storage_sigs.Single_data_storage.update).

Definition get_current : Raw_context.t → M? Voting_period_repr.voting_period :=
  Storage.Vote.Current_period.(Storage_sigs.Single_data_storage.get).

Definition init_value
  : Raw_context.t → Voting_period_repr.voting_period → M? Raw_context.t :=
  Storage.Vote.Current_period.(Storage_sigs.Single_data_storage.init_value).

Definition init_first_period (ctxt : Raw_context.t) (start_position : Int32.t)
  : M? Raw_context.t :=
  let? ctxt := init_value ctxt (Voting_period_repr.root_value start_position) in
  Storage.Vote.Pred_period_kind.(Storage_sigs.Single_data_storage.init_value)
    ctxt Voting_period_repr.Proposal.

Definition common (ctxt : Raw_context.t)
  : M? (Raw_context.t × Voting_period_repr.voting_period × int32) :=
  let? current_period := get_current ctxt in
  let? ctxt :=
    Storage.Vote.Pred_period_kind.(Storage_sigs.Single_data_storage.update) ctxt
      current_period.(Voting_period_repr.voting_period.kind) in
  let start_position :=
    Int32.succ (Level_storage.current ctxt).(Level_repr.t.level_position) in
  return? (ctxt, current_period, start_position).

Definition reset (ctxt : Raw_context.t) : M? Raw_context.t :=
  let? '(ctxt, current_period, start_position) := common ctxt in
  set_current ctxt (Voting_period_repr.raw_reset current_period start_position).

Definition succ (ctxt : Raw_context.t) : M? Raw_context.t :=
  let? '(ctxt, current_period, start_position) := common ctxt in
  set_current ctxt (Voting_period_repr.raw_succ current_period start_position).

Definition get_current_kind (ctxt : Raw_context.t)
  : M? Voting_period_repr.kind :=
  let? '{| Voting_period_repr.voting_period.kind := kind_value |} :=
    get_current ctxt in
  return? kind_value.

Definition get_current_info (ctxt : Raw_context.t)
  : M? Voting_period_repr.info :=
  let? voting_period := get_current ctxt in
  let blocks_per_voting_period := blocks_per_voting_period ctxt in
  let level := Level_storage.current ctxt in
  let position := Voting_period_repr.position_since level voting_period in
  let remaining :=
    Voting_period_repr.remaining_blocks level voting_period
      blocks_per_voting_period in
  return?
    {| Voting_period_repr.info.voting_period := voting_period;
      Voting_period_repr.info.position := position;
      Voting_period_repr.info.remaining := remaining; |}.

Definition get_current_remaining (ctxt : Raw_context.t) : M? Int32.t :=
  let? voting_period := get_current ctxt in
  let blocks_per_voting_period := blocks_per_voting_period ctxt in
  return?
    (Voting_period_repr.remaining_blocks (Level_storage.current ctxt)
      voting_period blocks_per_voting_period).

Definition is_last_block (ctxt : Raw_context.t) : M? bool :=
  let? remaining := get_current_remaining ctxt in
  return? (remaining =i32 0).

Definition blocks_before_activation (ctxt : Raw_context.t)
  : M? (option Int32.t) :=
  let? function_parameter := get_current ctxt in
  match function_parameter with
  | {| Voting_period_repr.voting_period.kind := Voting_period_repr.Adoption |}
    ⇒
    Error_monad.op_gtgteqquestion (get_current_remaining ctxt)
      Error_monad.return_some
  | _ ⇒ Error_monad.return_none
  end.

Definition get_rpc_current_info (ctxt : Raw_context.t)
  : M? Voting_period_repr.info :=
  let?
    '{|
      Voting_period_repr.info.voting_period := voting_period;
        Voting_period_repr.info.position := position
        |} as voting_period_info := get_current_info ctxt in
  if position =i32 Int32.minus_one then
    let level := Level_storage.current ctxt in
    let blocks_per_voting_period := blocks_per_voting_period ctxt in
    let? pred_kind :=
      Storage.Vote.Pred_period_kind.(Storage_sigs.Single_data_storage.get) ctxt
      in
    let voting_period :=
      {|
        Voting_period_repr.voting_period.index :=
          Int32.pred voting_period.(Voting_period_repr.voting_period.index);
        Voting_period_repr.voting_period.kind := pred_kind;
        Voting_period_repr.voting_period.start_position :=
          voting_period.(Voting_period_repr.voting_period.start_position) -i32
          blocks_per_voting_period; |} in
    let position := Voting_period_repr.position_since level voting_period in
    let remaining :=
      Voting_period_repr.remaining_blocks level voting_period
        blocks_per_voting_period in
    return?
      {| Voting_period_repr.info.voting_period := voting_period;
        Voting_period_repr.info.position := position;
        Voting_period_repr.info.remaining := remaining; |}
  else
    return? voting_period_info.

Definition get_rpc_succ_info (ctxt : Raw_context.t)
  : M? Voting_period_repr.info :=
  let? level :=
    Level_storage.from_raw_with_offset ctxt 1
      (Level_storage.current ctxt).(Level_repr.t.level) in
  let? voting_period := get_current ctxt in
  let blocks_per_voting_period := blocks_per_voting_period ctxt in
  let position := Voting_period_repr.position_since level voting_period in
  let remaining :=
    Voting_period_repr.remaining_blocks level voting_period
      blocks_per_voting_period in
  return?
    {| Voting_period_repr.info.voting_period := voting_period;
      Voting_period_repr.info.position := position;
      Voting_period_repr.info.remaining := remaining; |}.

Module Testnet_dictator.
  Definition overwrite_current_kind
    (ctxt : Raw_context.t) (chain_id : Chain_id.t)
    (kind_value : Voting_period_repr.kind) : M? Raw_context.t :=
    let? '_ :=
      Error_monad.error_when (Chain_id.op_eq chain_id Constants_repr.mainnet_id)
        (Build_extensible "Forbidden_on_mainnet" unit tt) in
    let? current_period := get_current ctxt in
    let new_period :=
      Voting_period_repr.voting_period.with_kind kind_value current_period in
    set_current ctxt new_period.
End Testnet_dictator.