Skip to main content

🪤 Stake_storage.v

Proofs

See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_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 : 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.