🗳️ Voting_period_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.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.
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.