👥 Delegate_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.

Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Operation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.

Module Contract.

[init] is valid, i.e., outputs a valid context.

  Lemma init_value_is_valid ctxt
    (contract : Contract_repr.t) (delegate : public_key_hash):
    Raw_context.Valid.t ctxt →
    letP? ' ctxt := Delegate_storage.Contract.init_value ctxt contract delegate
    in Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [set_self_delegate] is valid.

  Lemma set_self_delegate_is_valid ctxt delegate :
    Raw_context.Valid.t ctxt →
    letP? ctxt :=
      Delegate_storage.Contract.set_self_delegate ctxt delegate in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [set_delegate] is valid.

  Lemma set_delegate_is_valid ctxt contract delegate :
    Raw_context.Valid.t ctxt →
    letP? ctxt :=
      Delegate_storage.Contract.set_delegate ctxt contract delegate in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [set] is valid.

  Lemma set_is_valid ctxt contract delegate :
    Raw_context.Valid.t ctxt →
    letP? ctxt := Delegate_storage.Contract.set ctxt contract delegate in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.
End Contract.

The function [fold] is valid.

Lemma fold_is_valid {A : Set} (P : A → Prop) ctxt order acc f
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_acc : P acc)
  (H_f : ∀ key acc,
    P acc →
    letP? acc := f key acc in
    P acc
  ) :
  letP? acc := Delegate_storage.fold ctxt order acc f in
  P acc.
Proof.
Admitted.

The function [list_value] is valid.

Lemma list_value_is_valid ctxt
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? _ := Delegate_storage.list_value ctxt in
  True.
Proof.
Admitted.

The function [frozen_deposits_limit] is valid.

Lemma frozen_deposits_limit_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? limit := Delegate_storage.frozen_deposits_limit ctxt delegate in
  Option.Forall Tez_repr.Valid.t limit.
Proof.
Admitted.

[set_frozen_deposits_limit] is valid

Lemma set_frozen_deposits_limit_is_valid ctxt delegate limit :
  Raw_context.Valid.t ctxt →
  Option.Forall Tez_repr.Valid.t limit →
  let ctxt := Delegate_storage.set_frozen_deposits_limit ctxt delegate limit in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

[set_frozen_deposits_limit] followed by [frozen_deposits_limit] is an identity

Lemma set_frozen_deposits_limit_frozen_deposits_limit_eq
  (absolute_key : Context.key)
  (ctxt : Proto_alpha.Raw_context.t)
  (delegate : _)
  (amount : Tez_repr.t) :
  Delegate_storage.frozen_deposits_limit
    (Delegate_storage.set_frozen_deposits_limit
       ctxt delegate (Some amount)) delegate =
    Pervasives.Ok (Some amount).
Proof.
  unfold Delegate_storage.set_frozen_deposits_limit.
  (* @TODO Axiom was commented out in Storate.v *)
Admitted.

The function [frozen_deposits] is valid.

Lemma frozen_deposits_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt):
  letP? deposits := Delegate_storage.frozen_deposits ctxt delegate in
  Storage.deposits.Valid.t deposits.
Proof.
Admitted.

The function [spendable_balance] is valid.

Lemma spendable_balance_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? balance := Delegate_storage.spendable_balance ctxt delegate in
  Tez_repr.Valid.t balance.
Proof.
Admitted.

The function [staking_balance] is valid.

Lemma staking_balance_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? balance := Delegate_storage.staking_balance ctxt delegate in
  Tez_repr.Valid.t balance.
Proof.
Admitted.

The function [full_balance] is valid.

Lemma full_balance_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? full_balance := Delegate_storage.full_balance ctxt delegate in
  Tez_repr.Valid.t full_balance.
Proof.
Admitted.

The function [delegated_balance] is valid.

Lemma delegated_balance_is_valid ctxt delegate
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? balance := Delegate_storage.delegated_balance ctxt delegate in
  Tez_repr.Valid.t balance.
Proof.
Admitted.

The function [drain] is valid.

Lemma drain_is_valid ctxt delegate destination
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(ctxt, _, fees, updates) :=
    Delegate_storage.drain ctxt delegate destination in
  Raw_context.Valid.t ctxt ∧
  Tez_repr.Valid.t fees ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.