Skip to main content

✒️ Contract_storage.v

Proofs

See code, Gitlab , OCaml

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.

The function [to_lazy_storage_diff] is valid.
The function [update_script_lazy_storage] is valid.
[Contract_storage.raw_originate] is valid Currently no precondition on the parameters except the first one
The function [create_implicit] is valid.
The function [delete] is valid.
The function [must_exist] is valid.
The function [must_be_allocated] is valid.
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.

The function [fresh_contract_from_current_nonce] is valid.
[must_exists] after [_exists] returns [Pervasives.Ok unit]
[must_be_allocated] after [allocated] returns [Pervasives.Ok unit]
The function [originated_from_current_nonce] is valid.
The function [check_counter_increment] is valid.
The function [increment_counter] is valid.
The function [get_script_code] is valid.
The function [get_script] is valid.
The function [get_storage] is valid.
The function [get_counter] is valid.
@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.
The function [get_balance_carbonated] is valid.
The function [check_allocated_and_get_balance] is valid.
The function [update_script_storage] is valid.
The function [spend_from_balance] is valid.
The function [check_emptiable] is valid.
The function [spend_only_call_from_token] is valid.
The function [credit_only_call_from_token] is valid.
The function [init_value] is valid.
The function [used_storage_space] is valid.
The function [paid_storage_space] is valid.
The function [set_paid_storage_space_and_return_fees_to_pay] is valid.
The function [increase_paid_storage] is valid.
The function [update_balance] is valid.
The function [increase_balance_only_call_from_token] is valid.
The function [decrease_balance_only_call_from_token] is valid.
The function [get_frozen_bonds] is valid.
The function [get_balance_and_frozen_bonds] is valid.
The function [bond_allocated] is valid.
The function [find_bond] is valid.
The function [spend_bond_only_call_from_token] is valid.
The function [credit_bond_only_call_from_token] is valid.
The function [has_frozen_bonds] is valid.
The function [should_keep_empty_implicit_contract] is valid.
The function [ensure_deallocated_if_empty] is valid.
The function [simulate_spending] is valid.