Skip to main content

💰 Fees_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "contract.cannot_pay_storage_fee" "Cannot pay storage fee"
      "The storage fee is higher than the contract balance"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Cannot pay storage storage fee"
                  CamlinternalFormatBasics.End_of_format)
                "Cannot pay storage storage fee"))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Cannot_pay_storage_fee" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Cannot_pay_storage_fee" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "storage_exhausted.operation" "Storage quota exceeded for the operation"
      "A script or one of its callee wrote more bytes than the operation said it would"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Operation_quota_exceeded" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Operation_quota_exceeded" unit tt) in
  Error_monad.register_error_kind Error_monad.Permanent "storage_limit_too_high"
    "Storage limit out of protocol hard bounds"
    "A transaction tried to exceed the hard limit on storage" None
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Storage_limit_too_high" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Storage_limit_too_high" unit tt).

Definition record_global_constant_storage_space {A : Set}
  (context_value : A) (size_value : Z.t) : A × Z.t :=
  let cost_of_key := Z.of_int 65 in
  let to_be_paid := size_value +Z cost_of_key in
  (context_value, to_be_paid).

Definition record_paid_storage_space
  (ctxt : Raw_context.t) (contract : Contract_repr.t)
  : M? (Raw_context.t × Z.t × Z.t) :=
  let? new_storage_size := Contract_storage.used_storage_space ctxt contract in
  let? '(to_be_paid, c_value) :=
    Contract_storage.set_paid_storage_space_and_return_fees_to_pay ctxt contract
      new_storage_size in
  return? (c_value, new_storage_size, to_be_paid).

Definition source_must_exist (c_value : Raw_context.t) (src : Token.source)
  : M? unit :=
  match src with
  | Token.Source_container (Token.Contract src) ⇒
    Contract_storage.must_exist c_value src
  | _Error_monad.return_unit
  end.

Definition burn_storage_fees
  (op_staroptstar : option Receipt_repr.update_origin)
  : Raw_context.t Z.t Token.source Z.t
  M? (Raw_context.t × Z.t × Receipt_repr.balance_updates) :=
  let origin :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | NoneReceipt_repr.Block_application
    end in
  fun (c_value : Raw_context.t) ⇒
    fun (storage_limit : Z.t) ⇒
      fun (payer : Token.source) ⇒
        fun (consumed : Z.t) ⇒
          let remaining := storage_limit -Z consumed in
          if remaining <Z Z.zero then
            Error_monad.fail
              (Build_extensible "Operation_quota_exceeded" unit tt)
          else
            let cost_per_byte := Constants_storage.cost_per_byte c_value in
            let? to_burn :=
              Tez_repr.op_starquestion cost_per_byte (Z.to_int64 consumed) in
            if Tez_repr.op_eq to_burn Tez_repr.zero then
              return? (c_value, remaining, nil)
            else
              Error_monad.trace_value
                (Build_extensible "Cannot_pay_storage_fee" unit tt)
                (let? '_ := source_must_exist c_value payer in
                let? '(ctxt, balance_updates) :=
                  Token.transfer (Some origin) c_value payer
                    (Token.Sink_infinite Token.Storage_fees) to_burn in
                return? (ctxt, remaining, balance_updates)).

Definition burn_origination_fees
  (op_staroptstar : option Receipt_repr.update_origin)
  : Raw_context.t Z.t Token.source
  M? (Raw_context.t × Z.t × Receipt_repr.balance_updates) :=
  let origin :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | NoneReceipt_repr.Block_application
    end in
  fun (c_value : Raw_context.t) ⇒
    fun (storage_limit : Z.t) ⇒
      fun (payer : Token.source) ⇒
        let origination_size := Constants_storage.origination_size c_value in
        burn_storage_fees (Some origin) c_value storage_limit payer
          (Z.of_int origination_size).

Definition burn_tx_rollup_origination_fees
  (op_staroptstar : option Receipt_repr.update_origin)
  : Raw_context.t Z.t Token.source
  M? (Raw_context.t × Z.t × Receipt_repr.balance_updates) :=
  let origin :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | NoneReceipt_repr.Block_application
    end in
  fun (c_value : Raw_context.t) ⇒
    fun (storage_limit : Z.t) ⇒
      fun (payer : Token.source) ⇒
        let tx_rollup_origination_size :=
          Constants_storage.tx_rollup_origination_size c_value in
        burn_storage_fees (Some origin) c_value storage_limit payer
          (Z.of_int tx_rollup_origination_size).

Definition burn_sc_rollup_origination_fees
  (op_staroptstar : option Receipt_repr.update_origin)
  : Raw_context.t Z.t Token.source Z.t
  M? (Raw_context.t × Z.t × Receipt_repr.balance_updates) :=
  let origin :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | NoneReceipt_repr.Block_application
    end in
  fun (c_value : Raw_context.t) ⇒
    fun (storage_limit : Z.t) ⇒
      fun (payer : Token.source) ⇒
        fun (consumed : Z.t) ⇒
          burn_storage_fees (Some origin) c_value storage_limit payer consumed.

Definition check_storage_limit (c_value : Raw_context.t) (storage_limit : Z.t)
  : M? unit :=
  if
    (storage_limit >Z
    (Raw_context.constants c_value).(Constants_repr.parametric.hard_storage_limit_per_operation))
    || (storage_limit <Z Z.zero)
  then
    Error_monad.error_value (Build_extensible "Storage_limit_too_high" unit tt)
  else
    Result.return_unit.