💰 Fees_storage.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.
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 fee"
CamlinternalFormatBasics.End_of_format)
"Cannot pay 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
"contract.negative_storage_input" "Negative storage input"
"The storage amount asked for an operation is null or negative"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Null or negative storage input"
CamlinternalFormatBasics.End_of_format)
"Null or negative storage input"))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Negative_storage_input" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Negative_storage_input" 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_hash : Contract_hash.t)
: M? (Raw_context.t × Z.t × Z.t) :=
let contract := Contract_repr.Originated contract_hash in
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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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.tzfail
(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_storage_increase_fees
(op_staroptstar : option Receipt_repr.update_origin)
: Raw_context.t → Token.source → Z.t →
M? (Raw_context.t × Receipt_repr.balance_updates) :=
let origin :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_repr.Block_application
end in
fun (c_value : Raw_context.t) ⇒
fun (payer : Token.source) ⇒
fun (amount_in_bytes : Z.t) ⇒
if amount_in_bytes ≤Z Z.zero then
Error_monad.tzfail (Build_extensible "Negative_storage_input" 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 amount_in_bytes)
in
Error_monad.trace_value
(Build_extensible "Cannot_pay_storage_fee" unit tt)
(let? '_ := source_must_exist c_value payer in
Token.transfer (Some origin) c_value payer
(Token.Sink_infinite Token.Storage_fees) to_burn).
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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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 burn_zk_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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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_parametric_repr.t.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.
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 fee"
CamlinternalFormatBasics.End_of_format)
"Cannot pay 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
"contract.negative_storage_input" "Negative storage input"
"The storage amount asked for an operation is null or negative"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Null or negative storage input"
CamlinternalFormatBasics.End_of_format)
"Null or negative storage input"))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Negative_storage_input" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Negative_storage_input" 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_hash : Contract_hash.t)
: M? (Raw_context.t × Z.t × Z.t) :=
let contract := Contract_repr.Originated contract_hash in
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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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.tzfail
(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_storage_increase_fees
(op_staroptstar : option Receipt_repr.update_origin)
: Raw_context.t → Token.source → Z.t →
M? (Raw_context.t × Receipt_repr.balance_updates) :=
let origin :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_repr.Block_application
end in
fun (c_value : Raw_context.t) ⇒
fun (payer : Token.source) ⇒
fun (amount_in_bytes : Z.t) ⇒
if amount_in_bytes ≤Z Z.zero then
Error_monad.tzfail (Build_extensible "Negative_storage_input" 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 amount_in_bytes)
in
Error_monad.trace_value
(Build_extensible "Cannot_pay_storage_fee" unit tt)
(let? '_ := source_must_exist c_value payer in
Token.transfer (Some origin) c_value payer
(Token.Sink_infinite Token.Storage_fees) to_burn).
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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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 burn_zk_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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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_parametric_repr.t.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.