Skip to main content

👥 Delegate_activation_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.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_contract 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_contract 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)
    | Nonereturn? 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_contract 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_contract 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_contract 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
    | NoneCycle_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
      Cycle_repr.max current_last_active_cycle updated
    end 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).