Skip to main content

💰 Fees_storage.v


See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Fees_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.

The function [record_global_constant_storage_space] is valid.
The function [record_paid_storage_space] is valid.
Given that [paid] space is greather than [used] space then [record_paid_storage_space_unpaid] returns 0 (nothing is left to be paid) and does not update the context Lemma record_paid_storage_space_unpaid_eq_0 : forall {ctxt contract} (absolute_key : Raw_context.key) (used paid : Storage.Encoding.Z.(Storage_sigs.VALUE.t)), Storage.Contract.Used_storage_space.( Storage_sigs.Indexed_data_storage.find) ctxt contract = Pervasives.Ok (Some used) -> Storage.Contract.Paid_storage_space.( Storage_sigs.Indexed_data_storage.get) ctxt contract = Pervasives.Ok paid -> paid >= used -> let ticket_table_size_diff := 0 in letP? '(ctxt', _, to_be_paid) := Fees_storage.record_paid_storage_space ctxt contract in ctxt' = ctxt /\ to_be_paid = 0. Proof. intros. unfold Fees_storage.record_paid_storage_space. unfold Contract_storage.used_storage_space. unfold op_gtpipeeqquestion. simpl. unfold Contract_storage.set_paid_storage_space_and_return_fees_to_pay. Admitted.
The function [source_must_exist] is valid.
The function [burn_storage_fees] is valid.
@TODO types changed in new version. Record t ctxt (source : Contract_repr.t) (spendable_amount : Tez_repr.t) : Prop := { has_spendable_amount : Storage.Contract.Spendable_balance.( Storage_sigs.Indexed_data_storage.find) ctxt source = Pervasives.Ok (Some spendable_amount); is_originated : match source with | Contract_repr.Originated _ => True | _ => False end; }.
Given a [source] originated contract, a valid [consumed], repesenting the consumed storage space, a valid [limit], repsenting the maximum consumable space, a [Raw_context.t] containing the [spendable_amount] for [source], on success, [burn_storage_fees] return a value [burnt], such that [burnt = limit - consumed]
Lemma burn_storage_fees_is_valid_eq :
    (limit consumed : Int64.t)
    (source : Contract_repr.t)
    (spendable_amount : Tez_repr.t),
  Int64.Valid.t consumed
  Int64.Valid.t limit
  limit consumed
  letP? '(_, burnt, _) := Fees_storage.burn_storage_fees
    None ctxt limit
    (Token.Source_container (Token.Contract source)) consumed in
  burnt = limit - consumed.
  unfold Fees_storage.burn_storage_fees. simpl.
  replace (limit -Z consumed <? with false by lia.
  rewrite Z.to_int64_eq by lia.

The function [burn_storage_increase_fees] is valid.
The function [burn_origination_fees] is valid.
The function [burn_tx_rollup_origination_fees] is valid.
The function [burn_sc_rollup_origination_fees] is valid.
The function [burn_zk_rollup_origination_fees] is valid.
The function [check_storage_limit] is valid.