⛄ Frozen_deposits_storage.v
Proofs
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.