Skip to main content

👥 Delegate_activation_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Delegate_activation_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.

(* @TODO *)
Axiom set_inactive_implies_is_inactive_eq_true : {ctxt} {pkh},
  let ctxt' := Delegate_activation_storage.set_inactive ctxt pkh in
      Delegate_activation_storage.is_inactive ctxt' pkh = return? true.

(* @TODO *)
(* set_active is not that simple, here is the comment from the code*)
(* We allow a number of cycles before a delegate is deactivated as follows:
   - if the delegate is active, we give it at least `1 + preserved_cycles`
     after the current cycle before to be deactivated.
   - if the delegate is new or inactive, we give it additionally
     `preserved_cycles` because the delegate needs this number of cycles to
     receive rights, so `1 + 2 * preserved_cycles` in total. *)

Axiom set_active_implies_is_inactive_eq_true : {ctxt} {pkh},
  match Delegate_activation_storage.set_active ctxt pkh with
  | Pervasives.Ok (ctxt', is_active)
    if is_active
    then Delegate_activation_storage.is_inactive ctxt' pkh = return? false
    else True
  | Pervasives.Error _True
  end.