👥 Delegate_activation_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

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

Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [is_inactive] is valid.

Lemma is_inactive_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? _ := Delegate_activation_storage.is_inactive ctxt delegate in
  True.
Proof.
Admitted.

The function [last_cycle_before_deactivation] is valid.

Lemma last_cycle_before_deactivation_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? cycle :=
    Delegate_activation_storage.last_cycle_before_deactivation ctxt delegate in
  Cycle_repr.Valid.t cycle.
Proof.
Admitted.

The function [set_inactive] is valid.

Lemma set_inactive_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  let ctxt :=
    Delegate_activation_storage.set_inactive ctxt delegate in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

(* @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.

The function [set_active] is valid.

Lemma set_active_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(ctxt, _) :=
    Delegate_activation_storage.set_active ctxt delegate in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

(* @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.