⛄ Frozen_deposits_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.

Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.

The function [init_value] is value.

Lemma init_value_is_valid ctxt delegate :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Frozen_deposits_storage.init_value ctxt delegate in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [get] is value.

Lemma get_is_valid ctxt contract :
  Raw_context.Valid.t ctxt →
  letP? deposits := Frozen_deposits_storage.get ctxt contract in
  Storage.deposits.Valid.t deposits.
Proof.
Admitted.

The function [find] is value.

Lemma find_is_valid ctxt contract :
  Raw_context.Valid.t ctxt →
  letP? deposits := Frozen_deposits_storage.find ctxt contract in
  Option.Forall Storage.deposits.Valid.t deposits.
Proof.
Admitted.

The function [update_balance] is value.

Lemma update_balance_is_valid ctxt delegate f amount :
  Raw_context.Valid.t ctxt →
  (∀ x y,
    Tez_repr.Valid.t x →
    Tez_repr.Valid.t y →
    letP? z := f x y in
    Tez_repr.Valid.t z
  ) →
  Tez_repr.Valid.t amount →
  letP? ctxt := Frozen_deposits_storage.update_balance ctxt delegate f amount in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [credit_only_call_from_token] is value.

Lemma credit_only_call_from_token_is_valid ctxt delegate amount :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t amount →
  letP? ctxt :=
    Frozen_deposits_storage.credit_only_call_from_token ctxt delegate amount in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [spend_only_call_from_token] is value.

Lemma spend_only_call_from_token_is_valid ctxt delegate amount :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t amount →
  letP? ctxt :=
    Frozen_deposits_storage.spend_only_call_from_token ctxt delegate amount in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [update_initial_amount] is value.

Lemma update_initial_amount_is_valid ctxt delegate_contract deposits_cap :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t deposits_cap →
  letP? ctxt :=
    Frozen_deposits_storage.update_initial_amount
      ctxt delegate_contract deposits_cap in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

[allocated] after [init_value] returns [true]

Lemma init_implies_allocated_eq_true ctxt pkh :
  let contract := Contract_repr.Implicit pkh in
  letP? ctxt' := Frozen_deposits_storage.init_value ctxt pkh in
    Frozen_deposits_storage.allocated ctxt' contract = true.
Proof.
Admitted.

[get] after [init_value] returns [Pervasives.Ok]

Lemma init_implies_get_success ctxt pkh :
  let contract := Contract_repr.Implicit pkh in
  letP? ctxt' := Frozen_deposits_storage.init_value ctxt pkh in
  Pervasives.is_ok (Frozen_deposits_storage.get ctxt' contract).
Proof.
  intros.
  unfold Frozen_deposits_storage.get,
    Frozen_deposits_storage.init_value.
  (* @TODO axiom commented out in [Storage.v] *)
Admitted.

[find] after [init_value] returns [Pervasives.Ok]

Lemma init_implies_find_success ctxt pkh :
  let contract := Contract_repr.Implicit pkh in
  letP? ctxt' := Frozen_deposits_storage.init_value ctxt pkh in
    Pervasives.is_ok (Frozen_deposits_storage.find ctxt' contract).
Proof.
  intros.
  unfold Frozen_deposits_storage.find,
    Frozen_deposits_storage.init_value.
   (* @TODO axiom commented out in [Storage.v] *)
Admitted.

[credit_only_call_from_token] after [init_value] returns [Pervasives.Ok]

Lemma credit_only_call_from_token_after_init_is_ok
  ctxt
  (pkh : public_key_hash) (amount : int) :
  Tez_repr.Repr.Valid.t amount →
  let contract := Contract_repr.Implicit pkh in
  letP? ctxt' := Frozen_deposits_storage.init_value ctxt pkh in
  Pervasives.is_ok (Frozen_deposits_storage.credit_only_call_from_token
    ctxt' pkh (Tez_repr.Tez_tag amount)).
Proof.
   (* @TODO axiom commented out in [Storage.v] *)
Admitted.

Lemma get_is_valid_helper
  ctxt (delegate : public_key_hash) :
  letP? ctxt := Frozen_deposits_storage.init_value ctxt delegate in
  letP? deposits := Frozen_deposits_storage.get ctxt
    (Contract_repr.Implicit delegate) in
  Tez_repr.Valid.t deposits.(Storage.deposits.current_amount).
Proof.
  intros.
  unfold Frozen_deposits_storage.init_value.
   (* @TODO axiom commented out in [Storage.v] *)
Admitted.

(* @TODO, used on Delegate_storage *)
Lemma get_is_valid_bis ctxt ctxt'
  (delegate : public_key_hash) (deposits : Storage.deposits) :
  Frozen_deposits_storage.init_value ctxt delegate = Pervasives.Ok ctxt' →
  Frozen_deposits_storage.get ctxt' (Contract_repr.Implicit delegate) =
    Pervasives.Ok deposits →
  Tez_repr.Valid.t deposits.(Storage.deposits.current_amount).
Proof.
  pose proof (get_is_valid_helper ctxt delegate).
  destruct Frozen_deposits_storage.init_value eqn:?; [simpl|easy].
  intros Hinj. injection Hinj as Hinj. rewrite Hinj in H.
  simpl in H. revert H.
  destruct Frozen_deposits_storage.get eqn:?; [|easy].
  scongruence.
Qed.

Lemma spend_only_call_from_token_eq
  ctxt
  (pkh : public_key_hash) (amount : Tez_repr.t) :
  Tez_repr.Valid.t amount →
  let contract := Contract_repr.Implicit pkh in
  letP? ctxt := Frozen_deposits_storage.init_value ctxt pkh in
  letP? ctxt := Frozen_deposits_storage.credit_only_call_from_token
    ctxt pkh amount in
  Pervasives.is_ok (Frozen_deposits_storage.spend_only_call_from_token ctxt pkh amount).
Proof.
  intros.
   (* @TODO axiom commented out in [Storage.v] *)
Admitted.