Skip to main content

⛄ Frozen_deposits_storage.v

Proofs

See code, Gitlab , OCaml

The function [init_value] is value.
The function [get] is value.
The function [find] is value.
The function [update_balance] is value.
The function [credit_only_call_from_token] is value.
The function [spend_only_call_from_token] is value.
The function [update_initial_amount] is value.
[allocated] after [init_value] returns [true]
[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.