💰 Fees_storage.v

Proofs

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.

Lemma record_global_constant_storage_space_is_valid ctxt size :
  Raw_context.Valid.t ctxt →
  let '(ctxt, _) :=
    Fees_storage.record_global_constant_storage_space ctxt size in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [record_paid_storage_space] is valid.

Lemma record_paid_storage_space_is_valid ctxt contract :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , _, _) := Fees_storage.record_paid_storage_space ctxt contract in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

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.

Lemma source_must_exist_is_valid ctxt src :
  Raw_context.Valid.t ctxt →
  letP ? _ := Fees_storage.source_must_exist ctxt src in
  True.
Proof.
Admitted.

The function [burn_storage_fees] is valid.

Lemma burn_storage_fees_is_valid origin ctxt storage_limit payer consumed :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , _, updates ) :=
    Fees_storage.burn_storage_fees origin ctxt storage_limit payer consumed in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

Module Contract_is_originated_and_has_a_spendable_amount.

@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; }.

End Contract_is_originated_and_has_a_spendable_amount.

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 : ∀
    ctxt
    (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.
Proof.
  intros.
  unfold Fees_storage.burn_storage_fees. simpl.
  replace (limit -Z consumed <? Z.zero) with false by lia.
  rewrite Z.to_int64_eq by lia.
Admitted.

The function [burn_storage_increase_fees] is valid.

Lemma burn_storage_increase_fees_is_valid origin ctxt payer amount_in_bytes :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , updates ) :=
    Fees_storage.burn_storage_increase_fees origin ctxt payer amount_in_bytes in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [burn_origination_fees] is valid.

Lemma burn_origination_fees_is_valid origin ctxt storage_limit payer :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , _, updates ) :=
    Fees_storage.burn_origination_fees origin ctxt storage_limit payer in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [burn_tx_rollup_origination_fees] is valid.

Lemma burn_tx_rollup_origination_fees_is_valid origin ctxt storage_limit payer :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , _, updates ) :=
    Fees_storage.burn_tx_rollup_origination_fees
      origin ctxt storage_limit payer in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [burn_sc_rollup_origination_fees] is valid.

Lemma burn_sc_rollup_origination_fees_is_valid
  origin ctxt storage_limit payer consumed :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , _, updates ) :=
    Fees_storage.burn_sc_rollup_origination_fees
      origin ctxt storage_limit payer consumed in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [burn_zk_rollup_origination_fees] is valid.

Lemma burn_zk_rollup_origination_fees_is_valid
  origin ctxt storage_limit payer consumed :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , _, updates ) :=
    Fees_storage.burn_zk_rollup_origination_fees
      origin ctxt storage_limit payer consumed in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [check_storage_limit] is valid.

Lemma check_storage_limit_is_valid ctxt storage_limit :
  Raw_context.Valid.t ctxt →
  letP ? _ := Fees_storage.check_storage_limit ctxt storage_limit in
  True.
Proof.
Admitted.