🪤 Stake_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Stake_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.

(* @TODO *)
Axiom add_stake_eq : ∀ {ctxt} {delegate} {amount},
  Tez_repr.Valid.t (Tez_repr.Tez_tag amount) →
  match Stake_storage.add_stake
    ctxt delegate (Tez_repr.Tez_tag amount) with
  | Pervasives.Ok ctxt' ⇒
    let a1 :=
      Stake_storage.get_staking_balance ctxt delegate in
    let a2 :=
      Stake_storage.get_staking_balance ctxt' delegate in
    match a1, a2 with
    | Pervasives.Ok (Tez_repr.Tez_tag a1), Pervasives.Ok (Tez_repr.Tez_tag a2) ⇒ a2 = a1 +Z amount
    | _, _ ⇒ True
    end
  | Pervasives.Error _ ⇒ True
  end.

(* @TODO *)
Axiom remove_stake_eq : ∀ {ctxt} {delegate} {amount},
  Tez_repr.Valid.t (Tez_repr.Tez_tag amount) →
  match Stake_storage.remove_stake
    ctxt delegate (Tez_repr.Tez_tag amount) with
  | Pervasives.Ok ctxt' ⇒
    let a1 :=
      Stake_storage.get_staking_balance ctxt delegate in
    let a2 :=
      Stake_storage.get_staking_balance ctxt' delegate in
    match a1, a2 with
    | Pervasives.Ok (Tez_repr.Tez_tag a1), Pervasives.Ok (Tez_repr.Tez_tag a2) ⇒ a2 = a1 -Z amount
    | _, _ ⇒ True
    end
  | Pervasives.Error _ ⇒ True
  end.

(* @TODO *)
Axiom get_selected_distribuition_is_valid : ∀ {ctxt} {cycle},
  Cycle_repr.Valid.t cycle →
  match Stake_storage.get_selected_distribution ctxt cycle with
  | Pervasives.Ok l ⇒
    List.Forall Tez_repr.Valid.t (List.map snd l)
  | Pervasives.Error _ ⇒ True
  end.

(* @TODO *)
Axiom find_selected_distribuition_is_valid : ∀ {ctxt} {cycle},
  Cycle_repr.Valid.t cycle →
  match Stake_storage.find_selected_distribution ctxt cycle with
  | Pervasives.Ok (Some l) ⇒
    List.Forall Tez_repr.Valid.t (List.map snd l)
  | _ ⇒ True
  end.

Module Selected_distribution_for_cycle.
  (* @TODO *)
  Axiom init_get_eq : ∀ {ctxt} {cycle} {value},
  Cycle_repr.Valid.t cycle →
  match Stake_storage.Selected_distribution_for_cycle.init_value ctxt cycle value with
  | Pervasives.Ok ctxt' ⇒
    match Stake_storage.Selected_distribution_for_cycle.get ctxt' cycle with
    | Pervasives.Ok value' ⇒ value' = value
    | Pervasives.Error _ ⇒ True
    end
  | Pervasives.Error _ ⇒ True
  end.

  (* @TODO *)
  Axiom get_implies_remove_exists_is_ok : ∀ {ctxt} {cycle},
  Cycle_repr.Valid.t cycle →
  match Stake_storage.Selected_distribution_for_cycle.get ctxt cycle with
  | Pervasives.Ok _ ⇒
    let x := Stake_storage.Selected_distribution_for_cycle.remove_existing
      ctxt cycle in
    Result.is_ok x = true
  | Pervasives.Error _ ⇒ True
  end.
End Selected_distribution_for_cycle.

(* @TODO, used on Delegate_storage *)
Axiom get_staking_storage_is_valid :
  ∀ (ctxt : Proto_alpha.Raw_context.t) (delegate : public_key_hash)
    (balance : Tez_repr.t),
  Stake_storage.get_staking_balance ctxt delegate =
    Pervasives.Ok balance →
  Tez_repr.Valid.t balance.

[prepare_stake_distribution] is valid.

Lemma prepare_stake_distribution_is_valid
  (ctxt : Proto_alpha.Raw_context.t)
  : Raw_context.Valid.t ctxt →
    letP? ctxt := Stake_storage.prepare_stake_distribution ctxt in
    Raw_context.Valid.t ctxt.
Proof. Admitted.