👥 Delegate_activation_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_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Definition is_inactive
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash) : M? bool :=
let inactive :=
Storage.Contract.Inactive_delegate.(Storage_sigs.Data_set_storage.mem) ctxt
(Contract_repr.Implicit delegate) in
if inactive then
return? inactive
else
let? function_parameter :=
Storage.Contract.Delegate_last_cycle_before_deactivation.(Storage_sigs.Indexed_data_storage.find)
ctxt (Contract_repr.Implicit delegate) in
match function_parameter with
| Some last_active_cycle ⇒
let '{| Level_repr.t.cycle := current_cycle |} :=
Raw_context.current_level ctxt in
return? (Cycle_repr.op_lt last_active_cycle current_cycle)
| None ⇒ return? false
end.
Definition last_cycle_before_deactivation
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? Cycle_repr.t :=
let contract := Contract_repr.Implicit delegate in
Storage.Contract.Delegate_last_cycle_before_deactivation.(Storage_sigs.Indexed_data_storage.get)
ctxt contract.
Definition set_inactive
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: Raw_context.t :=
Storage.Contract.Inactive_delegate.(Storage_sigs.Data_set_storage.add) ctxt
(Contract_repr.Implicit delegate).
Definition set_active
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (Raw_context.t × bool) :=
let? inactive := is_inactive ctxt delegate in
let current_cycle := (Raw_context.current_level ctxt).(Level_repr.t.cycle) in
let preserved_cycles := Constants_storage.preserved_cycles ctxt in
let delegate_contract := Contract_repr.Implicit delegate in
let? current_last_active_cycle :=
Storage.Contract.Delegate_last_cycle_before_deactivation.(Storage_sigs.Indexed_data_storage.find)
ctxt delegate_contract in
let last_active_cycle :=
match current_last_active_cycle with
| None ⇒ Cycle_repr.add current_cycle (1 +i (2 ×i preserved_cycles))
| Some current_last_active_cycle ⇒
let delay :=
if inactive then
1 +i (2 ×i preserved_cycles)
else
1 +i preserved_cycles in
let? updated := Cycle_repr.add current_cycle delay in
return? (Cycle_repr.max current_last_active_cycle updated)
end in
let? last_active_cycle := last_active_cycle in
let ctxt :=
Storage.Contract.Delegate_last_cycle_before_deactivation.(Storage_sigs.Indexed_data_storage.add)
ctxt delegate_contract last_active_cycle in
if Pervasives.not inactive then
return? (ctxt, inactive)
else
let ctxt :=
Storage.Contract.Inactive_delegate.(Storage_sigs.Data_set_storage.remove)
ctxt delegate_contract in
return? (ctxt, inactive).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Definition is_inactive
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash) : M? bool :=
let inactive :=
Storage.Contract.Inactive_delegate.(Storage_sigs.Data_set_storage.mem) ctxt
(Contract_repr.Implicit delegate) in
if inactive then
return? inactive
else
let? function_parameter :=
Storage.Contract.Delegate_last_cycle_before_deactivation.(Storage_sigs.Indexed_data_storage.find)
ctxt (Contract_repr.Implicit delegate) in
match function_parameter with
| Some last_active_cycle ⇒
let '{| Level_repr.t.cycle := current_cycle |} :=
Raw_context.current_level ctxt in
return? (Cycle_repr.op_lt last_active_cycle current_cycle)
| None ⇒ return? false
end.
Definition last_cycle_before_deactivation
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? Cycle_repr.t :=
let contract := Contract_repr.Implicit delegate in
Storage.Contract.Delegate_last_cycle_before_deactivation.(Storage_sigs.Indexed_data_storage.get)
ctxt contract.
Definition set_inactive
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: Raw_context.t :=
Storage.Contract.Inactive_delegate.(Storage_sigs.Data_set_storage.add) ctxt
(Contract_repr.Implicit delegate).
Definition set_active
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (Raw_context.t × bool) :=
let? inactive := is_inactive ctxt delegate in
let current_cycle := (Raw_context.current_level ctxt).(Level_repr.t.cycle) in
let preserved_cycles := Constants_storage.preserved_cycles ctxt in
let delegate_contract := Contract_repr.Implicit delegate in
let? current_last_active_cycle :=
Storage.Contract.Delegate_last_cycle_before_deactivation.(Storage_sigs.Indexed_data_storage.find)
ctxt delegate_contract in
let last_active_cycle :=
match current_last_active_cycle with
| None ⇒ Cycle_repr.add current_cycle (1 +i (2 ×i preserved_cycles))
| Some current_last_active_cycle ⇒
let delay :=
if inactive then
1 +i (2 ×i preserved_cycles)
else
1 +i preserved_cycles in
let? updated := Cycle_repr.add current_cycle delay in
return? (Cycle_repr.max current_last_active_cycle updated)
end in
let? last_active_cycle := last_active_cycle in
let ctxt :=
Storage.Contract.Delegate_last_cycle_before_deactivation.(Storage_sigs.Indexed_data_storage.add)
ctxt delegate_contract last_active_cycle in
if Pervasives.not inactive then
return? (ctxt, inactive)
else
let ctxt :=
Storage.Contract.Inactive_delegate.(Storage_sigs.Data_set_storage.remove)
ctxt delegate_contract in
return? (ctxt, inactive).