Skip to main content

💰 Fees_storage.v

Proofs

See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.

(* The mli file says <size> in bytes, so I'm not sure if I have
 * to convert the `size` to `size in bytes` here *)

Module Global_storage_constant_space.
  Module Valid.
    Definition t (size : Z.t) (arg : Raw_context.t × Z.t) :=
      let '(_, cost) := arg in
      cost = size +Z 65.
  End Valid.
End Global_storage_constant_space.

Module Storage_limit.
  Module Valid.
    Definition t x ctxt :=
      0 x Constants_storage.hard_storage_limit_per_operation ctxt.
  End Valid.
End Storage_limit.

Lemma record_global_constant_storage_space_is_valid
  : {ctxt : Raw_context.t} {size : Z.t},
  Global_storage_constant_space.Valid.t size
    (Fees_storage.record_global_constant_storage_space ctxt size).
Proof.
  sfirstorder.
Qed.

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
  : {ctxt : Raw_context.t} {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.
  rewrite H, H0. simpl.
  replace (paid >=? _) with true by lia.
  easy.
Qed.

If [used] storage is greater then [paid], then [record_paid_storage_space_unpaid] updates the the storage with used and returns [used - paid]
Lemma record_paid_storage_space_unpaid_neq_0
  : {ctxt : Raw_context.t} {contract}
      (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' =
      Storage.Eq.Contracts.Paid_storage_space.apply
        ctxt
        (Storage_sigs.Indexed_data_storage.Change.Add contract used)
      to_be_paid = used - paid.
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.
  rewrite H, H0. simpl.
  replace (paid >=? _) with false by lia.
  destruct Storage.Contract.Paid_storage_space.(
     Storage_sigs.Indexed_data_storage.update) eqn:?; simpl; [|easy].
  split; [|lia].
  revert Heqt.
  rewrite (Storage.Eq.Contracts.Paid_storage_space.eq).(
    Storage_sigs.Indexed_data_storage.Eq.update).
  simpl. unfold Storage_sigs.Indexed_data_storage.Op.update.
  destruct (Storage_sigs.Indexed_data_storage.Op.mem _ _); [|easy].
  simpl. unfold Storage_sigs.Indexed_data_storage.Op.add.
  intros Hinj. injection Hinj as Hinj.
  rewrite <- Hinj; repeat f_equal; lia.
Qed.

[check_storage_limit] succeeds iff [limit] is between [0] and [hard_storage_limit_per_operation], inclusive.
Lemma check_storage_limit (ctxt : Raw_context.t) (limit : int) :
  Storage_limit.Valid.t limit ctxt
  let max :=
    (Raw_context.constants ctxt).(
      Constants_repr.parametric.hard_storage_limit_per_operation) in
  0 limit max
  Fees_storage.check_storage_limit ctxt limit = Pervasives.Ok tt.
Proof.
  intros.
  unfold Fees_storage.check_storage_limit.
  simpl.
  replace (limit >? _) with false by lia.
  replace (limit <? Z.zero) with false by lia.
  easy.
Qed.

Module Contract_is_implicit_and_has_a_spendable_amount.
  Record t (ctxt : Raw_context.t) (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_implicit : Contract_repr.is_implicit source = None;
    }.
End Contract_is_implicit_and_has_a_spendable_amount.

Given a [source] implict 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 :
    (ctxt : Raw_context.t)
    (limit consumed : Int64.t)
    (source : Contract_repr.t)
    (spendable_amount : Tez_repr.t),
  Int64.Valid.t consumed
  Int64.Valid.t limit
  limit consumed
  Contract_is_implicit_and_has_a_spendable_amount.t
    ctxt source spendable_amount
  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.
  unfold to_int64.
  rewrite Int64.normalize_identity; [|easy].
  destruct (Tez_repr.op_starquestion _ _) as [to_burn|?] eqn:?;
    [|easy].
  simpl.
  destruct (Tez_repr.op_eq _ _) eqn:?; [easy|]; simpl.
  unfold Contract_storage.must_exist.
  unfold Contract_storage._exists.
  destruct H2.
  rewrite is_implicit. unfold Contract_storage.allocated.
  rewrite has_spendable_amount. simpl.
  destruct (Token.transfer _ _ _ _ _) eqn:?; [|easy].
  simpl.
  destruct trace_value eqn:?; [|easy].
  simpl. destruct p0 as [[ctxt' limit'] updates].
  sauto.
Qed.