✒️ Contract_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Module Legacy_big_map_diff.
Lemma item_encoding_is_valid
: Data_encoding.Valid.t (fun _ ⇒ True) Contract_storage.Legacy_big_map_diff.item_encoding.
Data_encoding.Valid.data_encoding_auto.
intros []; simpl; try tauto.
destruct u, diff_value; tauto.
Qed.
#[global] Hint Resolve item_encoding_is_valid : Data_encoding_db.
Lemma encoding_is_valid
: Data_encoding.Valid.t (fun _ ⇒ True) Contract_storage.Legacy_big_map_diff.encoding.
Data_encoding.Valid.data_encoding_auto.
now intros; apply List.Forall_True.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Module Legacy_big_map_diff.
Lemma item_encoding_is_valid
: Data_encoding.Valid.t (fun _ ⇒ True) Contract_storage.Legacy_big_map_diff.item_encoding.
Data_encoding.Valid.data_encoding_auto.
intros []; simpl; try tauto.
destruct u, diff_value; tauto.
Qed.
#[global] Hint Resolve item_encoding_is_valid : Data_encoding_db.
Lemma encoding_is_valid
: Data_encoding.Valid.t (fun _ ⇒ True) Contract_storage.Legacy_big_map_diff.encoding.
Data_encoding.Valid.data_encoding_auto.
now intros; apply List.Forall_True.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
The function [to_lazy_storage_diff] is valid.
Lemma to_lazy_storage_diff_is_valid legacy_diffs :
letP? _ :=
Contract_storage.Legacy_big_map_diff.to_lazy_storage_diff legacy_diffs in
True.
Proof.
Admitted.
End Legacy_big_map_diff.
letP? _ :=
Contract_storage.Legacy_big_map_diff.to_lazy_storage_diff legacy_diffs in
True.
Proof.
Admitted.
End Legacy_big_map_diff.
The function [update_script_lazy_storage] is valid.
Lemma update_script_lazy_storage_is_valid ctxt param :
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.update_script_lazy_storage ctxt param in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.update_script_lazy_storage ctxt param in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
[Contract_storage.raw_originate] is valid Currently no precondition on the parameters except the first one
Lemma raw_originate_is_valid (ctxt : Proto_alpha.Raw_context.t)
(prepaid_bootstrap_storage : bool) (contract: Contract_hash.t)
(script : Script_repr.t × M× Lazy_storage_diff.diffs) :
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.raw_originate ctxt
prepaid_bootstrap_storage contract script
in Raw_context.Valid.t ctxt.
Proof.
Admitted.
(prepaid_bootstrap_storage : bool) (contract: Contract_hash.t)
(script : Script_repr.t × M× Lazy_storage_diff.diffs) :
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.raw_originate ctxt
prepaid_bootstrap_storage contract script
in Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [create_implicit] is valid.
Lemma create_implicit_is_valid ctxt manager balance :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t balance →
letP? ctxt := Contract_storage.create_implicit ctxt manager balance in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t balance →
letP? ctxt := Contract_storage.create_implicit ctxt manager balance in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [delete] is valid.
Lemma delete_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.delete ctxt contract in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.delete ctxt contract in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [must_exist] is valid.
Lemma must_exist_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.must_exist ctxt contract in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.must_exist ctxt contract in
True.
Proof.
Admitted.
The function [must_be_allocated] is valid.
Lemma must_be_allocated_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.must_be_allocated ctxt contract in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.must_be_allocated ctxt contract in
True.
Proof.
Admitted.
The function [list_value] is valid.
Lemma list_value_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.list_value ctxt in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.list_value ctxt in
True.
Proof.
Admitted.
The function [fresh_contract_from_current_nonce] is valid.
Lemma fresh_contract_from_current_nonce_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.fresh_contract_from_current_nonce ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.fresh_contract_from_current_nonce ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
[must_exists] after [_exists] returns [Pervasives.Ok unit]
Lemma exists_implies_must_exists_success (ctxt : Proto_alpha.Raw_context.t)
(hash : Contract_hash.t) :
let contract := Contract_repr.Originated hash in
Contract_storage._exists ctxt contract = true →
Contract_storage.must_exist ctxt contract = Pervasives.Ok tt.
Proof.
unfold Contract_storage.must_exist; simpl.
intros.
now rewrite H.
Qed.
(hash : Contract_hash.t) :
let contract := Contract_repr.Originated hash in
Contract_storage._exists ctxt contract = true →
Contract_storage.must_exist ctxt contract = Pervasives.Ok tt.
Proof.
unfold Contract_storage.must_exist; simpl.
intros.
now rewrite H.
Qed.
[must_be_allocated] after [allocated] returns [Pervasives.Ok unit]
Lemma allocated_implies_must_be_allocated_success
(ctxt : Proto_alpha.Raw_context.t) (contract : Contract_repr.t) :
Contract_storage.allocated ctxt contract = true →
Contract_storage.must_be_allocated ctxt contract = return? tt.
Proof.
intros.
unfold Contract_storage.must_be_allocated.
now rewrite H.
Qed.
(ctxt : Proto_alpha.Raw_context.t) (contract : Contract_repr.t) :
Contract_storage.allocated ctxt contract = true →
Contract_storage.must_be_allocated ctxt contract = return? tt.
Proof.
intros.
unfold Contract_storage.must_be_allocated.
now rewrite H.
Qed.
The function [originated_from_current_nonce] is valid.
Lemma originated_from_current_nonce_is_valid ctxt_since ctxt_until :
Raw_context.Valid.t ctxt_since →
Raw_context.Valid.t ctxt_until →
letP? _ :=
Contract_storage.originated_from_current_nonce ctxt_since ctxt_until in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt_since →
Raw_context.Valid.t ctxt_until →
letP? _ :=
Contract_storage.originated_from_current_nonce ctxt_since ctxt_until in
True.
Proof.
Admitted.
The function [check_counter_increment] is valid.
Lemma check_counter_increment_is_valid ctxt manager counter :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.check_counter_increment ctxt manager counter in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.check_counter_increment ctxt manager counter in
True.
Proof.
Admitted.
The function [increment_counter] is valid.
Lemma increment_counter_is_valid ctxt manager :
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.increment_counter ctxt manager in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.increment_counter ctxt manager in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_script_code] is valid.
Lemma get_script_code_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.get_script_code ctxt contract in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.get_script_code ctxt contract in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_script] is valid.
Lemma get_script_is_valid ctxt contract_hash :
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.get_script ctxt contract_hash in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.get_script ctxt contract_hash in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_storage] is valid.
Lemma get_storage_is_valid ctxt contract_hash :
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.get_storage ctxt contract_hash in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.get_storage ctxt contract_hash in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_counter] is valid.
Lemma get_counter_is_valid ctxt manager :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.get_counter ctxt manager in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.get_counter ctxt manager in
True.
Proof.
Admitted.
@TODO
Axiom from Storage.v was commented out.
[Storage.Eq.Contracts.Balance.eq]
[Storage.Contract.Spendable_balance.get] is valid when
the same storage was initialized with a valid balance
Lemma spendable_balance_get_is_valid
(ctxt : Proto_alpha.Raw_context.t) (delegate : public_key_hash)
(balance : Tez_repr.t) :
Tez_repr.Valid.t balance ->
letP? ctxt' := Storage.Contract.Spendable_balance.(
Storage_sigs.Indexed_data_storage.init_value)
ctxt (Contract_repr.Implicit delegate) balance in
letP? balance' := Storage.Contract.Spendable_balance.(
Storage_sigs.Indexed_data_storage.get)
ctxt' (Contract_repr.Implicit delegate) in
Tez_repr.Valid.t balance'.
Proof.
Admitted.
The function [get_balance] is valid.
Lemma get_balance_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? amount :=
Contract_storage.get_balance ctxt contract in
Tez_repr.Valid.t amount.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? amount :=
Contract_storage.get_balance ctxt contract in
Tez_repr.Valid.t amount.
Proof.
Admitted.
The function [get_balance_carbonated] is valid.
Lemma get_balance_carbonated_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? '(ctxt, balance) :=
Contract_storage.get_balance_carbonated ctxt contract in
Raw_context.Valid.t ctxt ∧
Tez_repr.Valid.t balance.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, balance) :=
Contract_storage.get_balance_carbonated ctxt contract in
Raw_context.Valid.t ctxt ∧
Tez_repr.Valid.t balance.
Proof.
Admitted.
The function [check_allocated_and_get_balance] is valid.
Lemma check_allocated_and_get_balance_is_valid ctxt pkh :
Raw_context.Valid.t ctxt →
letP? balance := Contract_storage.check_allocated_and_get_balance ctxt pkh in
Tez_repr.Valid.t balance.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? balance := Contract_storage.check_allocated_and_get_balance ctxt pkh in
Tez_repr.Valid.t balance.
Proof.
Admitted.
The function [update_script_storage] is valid.
Lemma update_script_storage_is_valid
ctxt contract storage_value lazy_storage_diff :
Raw_context.Valid.t ctxt →
letP? ctxt :=
Contract_storage.update_script_storage
ctxt contract storage_value lazy_storage_diff in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
ctxt contract storage_value lazy_storage_diff :
Raw_context.Valid.t ctxt →
letP? ctxt :=
Contract_storage.update_script_storage
ctxt contract storage_value lazy_storage_diff in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [spend_from_balance] is valid.
Lemma spend_from_balance_is_valid contract balance amount :
Tez_repr.Valid.t balance →
Tez_repr.Valid.t amount →
letP? result := Contract_storage.spend_from_balance contract balance amount in
Tez_repr.Valid.t result.
Proof.
Admitted.
Tez_repr.Valid.t balance →
Tez_repr.Valid.t amount →
letP? result := Contract_storage.spend_from_balance contract balance amount in
Tez_repr.Valid.t result.
Proof.
Admitted.
The function [check_emptiable] is valid.
Lemma check_emptiable_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.check_emptiable ctxt contract in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.check_emptiable ctxt contract in
True.
Proof.
Admitted.
The function [spend_only_call_from_token] is valid.
Lemma spend_only_call_from_token_is_valid ctxt contract amount :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.spend_only_call_from_token ctxt contract amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.spend_only_call_from_token ctxt contract amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [credit_only_call_from_token] is valid.
Lemma credit_only_call_from_token_is_valid ctxt contract amount :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.credit_only_call_from_token ctxt contract amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.credit_only_call_from_token ctxt contract amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [init_value] is valid.
Lemma init_value_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.init_value ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.init_value ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [used_storage_space] is valid.
Lemma used_storage_space_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.used_storage_space ctxt contract in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.used_storage_space ctxt contract in
True.
Proof.
Admitted.
The function [paid_storage_space] is valid.
Lemma paid_storage_space_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.paid_storage_space ctxt contract in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.paid_storage_space ctxt contract in
True.
Proof.
Admitted.
The function [set_paid_storage_space_and_return_fees_to_pay] is valid.
Lemma set_paid_storage_space_and_return_fees_to_pay_is_valid
ctxt contract new_storage_space :
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) :=
Contract_storage.set_paid_storage_space_and_return_fees_to_pay
ctxt contract new_storage_space in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
ctxt contract new_storage_space :
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) :=
Contract_storage.set_paid_storage_space_and_return_fees_to_pay
ctxt contract new_storage_space in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [increase_paid_storage] is valid.
Lemma increase_paid_storage_is_valid ctxt contract storage_incr :
Raw_context.Valid.t ctxt →
letP? ctxt :=
Contract_storage.increase_paid_storage ctxt contract storage_incr in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt :=
Contract_storage.increase_paid_storage ctxt contract storage_incr in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [update_balance] is valid.
Lemma update_balance_is_valid ctxt contract 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 := Contract_storage.update_balance ctxt contract 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 := Contract_storage.update_balance ctxt contract f amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [increase_balance_only_call_from_token] is valid.
Lemma increase_balance_only_call_from_token_is_valid ctxt contract amount :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.increase_balance_only_call_from_token
ctxt contract amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.increase_balance_only_call_from_token
ctxt contract amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [decrease_balance_only_call_from_token] is valid.
Lemma decrease_balance_only_call_from_token_is_valid ctxt contract amount :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.decrease_balance_only_call_from_token
ctxt contract amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.decrease_balance_only_call_from_token
ctxt contract amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_frozen_bonds] is valid.
Lemma get_frozen_bonds_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? amount := Contract_storage.get_frozen_bonds ctxt contract in
Tez_repr.Valid.t amount.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? amount := Contract_storage.get_frozen_bonds ctxt contract in
Tez_repr.Valid.t amount.
Proof.
Admitted.
The function [get_balance_and_frozen_bonds] is valid.
Lemma get_balance_and_frozen_bonds_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? amount := Contract_storage.get_balance_and_frozen_bonds ctxt contract in
Tez_repr.Valid.t amount.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? amount := Contract_storage.get_balance_and_frozen_bonds ctxt contract in
Tez_repr.Valid.t amount.
Proof.
Admitted.
The function [bond_allocated] is valid.
Lemma bond_allocated_is_valid ctxt contract bond_id :
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.bond_allocated ctxt contract bond_id in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, _) := Contract_storage.bond_allocated ctxt contract bond_id in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [find_bond] is valid.
Lemma find_bond_is_valid ctxt contract bond_id :
Raw_context.Valid.t ctxt →
letP? '(ctxt, amount) := Contract_storage.find_bond ctxt contract bond_id in
Raw_context.Valid.t ctxt ∧
Option.Forall Tez_repr.Valid.t amount.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, amount) := Contract_storage.find_bond ctxt contract bond_id in
Raw_context.Valid.t ctxt ∧
Option.Forall Tez_repr.Valid.t amount.
Proof.
Admitted.
The function [spend_bond_only_call_from_token] is valid.
Lemma spend_bond_only_call_from_token_is_valid ctxt contract bound_id amount :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.spend_bond_only_call_from_token
ctxt contract bound_id amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.spend_bond_only_call_from_token
ctxt contract bound_id amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [credit_bond_only_call_from_token] is valid.
Lemma credit_bond_only_call_from_token_is_valid ctxt contract bound_id amount :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.credit_bond_only_call_from_token
ctxt contract bound_id amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Contract_storage.credit_bond_only_call_from_token
ctxt contract bound_id amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [has_frozen_bonds] is valid.
Lemma has_frozen_bonds_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.has_frozen_bonds ctxt contract in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Contract_storage.has_frozen_bonds ctxt contract in
True.
Proof.
Admitted.
The function [should_keep_empty_implicit_contract] is valid.
Lemma should_keep_empty_implicit_contract_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? _ :=
Contract_storage.should_keep_empty_implicit_contract ctxt contract in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ :=
Contract_storage.should_keep_empty_implicit_contract ctxt contract in
True.
Proof.
Admitted.
The function [ensure_deallocated_if_empty] is valid.
Lemma ensure_deallocated_if_empty_is_valid ctxt contract :
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.ensure_deallocated_if_empty ctxt contract in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Contract_storage.ensure_deallocated_if_empty ctxt contract in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [simulate_spending] is valid.
Lemma simulate_spending_is_valid ctxt balance amount source :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t balance →
Tez_repr.Valid.t amount →
letP? '(amount, _) :=
Contract_storage.simulate_spending ctxt balance amount source in
Tez_repr.Valid.t amount.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t balance →
Tez_repr.Valid.t amount →
letP? '(amount, _) :=
Contract_storage.simulate_spending ctxt balance amount source in
Tez_repr.Valid.t amount.
Proof.
Admitted.