🦏 Sc_rollup_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_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Store := Storage.Sc_rollup.
Module Commitment_hash := Sc_rollup_commitment_repr.Hash.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Store := Storage.Sc_rollup.
Module Commitment_hash := Sc_rollup_commitment_repr.Hash.
[address_from_nonce ctxt nonce] produces an address completely determined by
an operation hash and an origination counter, and accounts for gas spent.
Definition address_from_nonce
(ctxt : Raw_context.t) (nonce_value : Origination_nonce.t)
: M? (Raw_context.t × Sc_rollup_repr.Address.t) :=
let? ctxt :=
Raw_context.consume_gas ctxt Sc_rollup_costs.Constants.cost_serialize_nonce
in
match
Data_encoding.Binary.to_bytes_opt None Origination_nonce.encoding
nonce_value with
| None ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_address_generation" unit tt)
| Some nonce_bytes ⇒
let bytes_len := Bytes.length nonce_bytes in
Error_monad.Result_syntax.op_letplus
(Raw_context.consume_gas ctxt (Sc_rollup_costs.cost_hash_bytes bytes_len))
(fun ctxt ⇒
(ctxt, (Sc_rollup_repr.Address.hash_bytes None [ nonce_bytes ])))
end.
Definition originate
(ctxt : Raw_context.t) (kind_value : Sc_rollups.Kind.t)
(parameters_ty : Script_repr.lazy_expr)
(genesis_commitment : Sc_rollup_commitment_storage.Commitment.t)
: M?
(Sc_rollup_repr.Address.t × Z.t ×
Sc_rollup_commitment_storage.Commitment_hash.t × Raw_context.t) :=
let? '(ctxt, genesis_commitment_hash) :=
Sc_rollup_commitment_storage.hash_value ctxt genesis_commitment in
let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
let? '(ctxt, address) := address_from_nonce ctxt nonce_value in
let? '(ctxt, pvm_kind_size, _kind_existed) :=
Store.PVM_kind.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
ctxt address kind_value in
let origination_level := (Raw_context.current_level ctxt).(Level_repr.t.level)
in
let? '(ctxt, genesis_info_size, _info_existed) :=
Store.Genesis_info.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
ctxt address
{| Sc_rollup_commitment_repr.genesis_info.level := origination_level;
Sc_rollup_commitment_repr.genesis_info.commitment_hash :=
genesis_commitment_hash; |} in
let? '(ctxt, param_ty_size_diff, _added) :=
Store.Parameters_type.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
ctxt address parameters_ty in
let? '(ctxt, lcc_size_diff) :=
Store.Last_cemented_commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt address genesis_commitment_hash in
let? '(ctxt, commitment_size_diff, _was_bound) :=
Store.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, address) genesis_commitment_hash genesis_commitment in
let? '(ctxt, commitment_added_size_diff, _commitment_existed) :=
Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, address) genesis_commitment_hash origination_level in
let? '(ctxt, commitment_staker_count_size_diff, _commitment_staker_existed) :=
Store.Commitment_stake_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, address) genesis_commitment_hash Int32.zero in
let? '(ctxt, stakers_size_diff) :=
Store.Staker_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt address 0 in
let addresses_size := 2 ×i Sc_rollup_repr.Address.size_value in
let stored_kind_size := 2 in
let origination_size := Constants_storage.sc_rollup_origination_size ctxt in
let size_value :=
Z.of_int
((((((((((origination_size +i stored_kind_size) +i addresses_size) +i
lcc_size_diff) +i commitment_size_diff) +i commitment_added_size_diff) +i
commitment_staker_count_size_diff) +i stakers_size_diff) +i
param_ty_size_diff) +i pvm_kind_size) +i genesis_info_size) in
return? (address, size_value, genesis_commitment_hash, ctxt).
Definition kind_value
(ctxt : Raw_context.t) (address : Sc_rollup_repr.Address.t)
: M? (Raw_context.t × Sc_rollups.Kind.t) :=
let? '(ctxt, kind_opt) :=
Store.PVM_kind.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
ctxt address in
match kind_opt with
| Some k_value ⇒ return? (ctxt, k_value)
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
address)
end.
Definition list_unaccounted (ctxt : Raw_context.t)
: M? (list Sc_rollup_repr.Address.t) :=
Store.PVM_kind.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted)
ctxt.
Definition genesis_info
(ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
: M? (Raw_context.t × Sc_rollup_commitment_repr.genesis_info) :=
let? '(ctxt, genesis_info) :=
Store.Genesis_info.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
ctxt rollup in
match genesis_info with
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
rollup)
| Some genesis_info ⇒ return? (ctxt, genesis_info)
end.
Definition get_metadata
(ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
: M? (Raw_context.t × Sc_rollup_metadata_repr.t) :=
let? '(ctxt, genesis_info) := genesis_info ctxt rollup in
let metadata :=
{| Sc_rollup_metadata_repr.t.address := rollup;
Sc_rollup_metadata_repr.t.origination_level :=
genesis_info.(Sc_rollup_commitment_repr.genesis_info.level); |} in
return? (ctxt, metadata).
Definition parameters_type
(ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
: M? (option Script_repr.lazy_expr × Raw_context.t) :=
Error_monad.Lwt_result_syntax.op_letplus
(Store.Parameters_type.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
ctxt rollup)
(fun function_parameter ⇒
let '(ctxt, res) := function_parameter in
(res, ctxt)).
(ctxt : Raw_context.t) (nonce_value : Origination_nonce.t)
: M? (Raw_context.t × Sc_rollup_repr.Address.t) :=
let? ctxt :=
Raw_context.consume_gas ctxt Sc_rollup_costs.Constants.cost_serialize_nonce
in
match
Data_encoding.Binary.to_bytes_opt None Origination_nonce.encoding
nonce_value with
| None ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_address_generation" unit tt)
| Some nonce_bytes ⇒
let bytes_len := Bytes.length nonce_bytes in
Error_monad.Result_syntax.op_letplus
(Raw_context.consume_gas ctxt (Sc_rollup_costs.cost_hash_bytes bytes_len))
(fun ctxt ⇒
(ctxt, (Sc_rollup_repr.Address.hash_bytes None [ nonce_bytes ])))
end.
Definition originate
(ctxt : Raw_context.t) (kind_value : Sc_rollups.Kind.t)
(parameters_ty : Script_repr.lazy_expr)
(genesis_commitment : Sc_rollup_commitment_storage.Commitment.t)
: M?
(Sc_rollup_repr.Address.t × Z.t ×
Sc_rollup_commitment_storage.Commitment_hash.t × Raw_context.t) :=
let? '(ctxt, genesis_commitment_hash) :=
Sc_rollup_commitment_storage.hash_value ctxt genesis_commitment in
let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
let? '(ctxt, address) := address_from_nonce ctxt nonce_value in
let? '(ctxt, pvm_kind_size, _kind_existed) :=
Store.PVM_kind.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
ctxt address kind_value in
let origination_level := (Raw_context.current_level ctxt).(Level_repr.t.level)
in
let? '(ctxt, genesis_info_size, _info_existed) :=
Store.Genesis_info.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
ctxt address
{| Sc_rollup_commitment_repr.genesis_info.level := origination_level;
Sc_rollup_commitment_repr.genesis_info.commitment_hash :=
genesis_commitment_hash; |} in
let? '(ctxt, param_ty_size_diff, _added) :=
Store.Parameters_type.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
ctxt address parameters_ty in
let? '(ctxt, lcc_size_diff) :=
Store.Last_cemented_commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt address genesis_commitment_hash in
let? '(ctxt, commitment_size_diff, _was_bound) :=
Store.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, address) genesis_commitment_hash genesis_commitment in
let? '(ctxt, commitment_added_size_diff, _commitment_existed) :=
Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, address) genesis_commitment_hash origination_level in
let? '(ctxt, commitment_staker_count_size_diff, _commitment_staker_existed) :=
Store.Commitment_stake_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, address) genesis_commitment_hash Int32.zero in
let? '(ctxt, stakers_size_diff) :=
Store.Staker_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt address 0 in
let addresses_size := 2 ×i Sc_rollup_repr.Address.size_value in
let stored_kind_size := 2 in
let origination_size := Constants_storage.sc_rollup_origination_size ctxt in
let size_value :=
Z.of_int
((((((((((origination_size +i stored_kind_size) +i addresses_size) +i
lcc_size_diff) +i commitment_size_diff) +i commitment_added_size_diff) +i
commitment_staker_count_size_diff) +i stakers_size_diff) +i
param_ty_size_diff) +i pvm_kind_size) +i genesis_info_size) in
return? (address, size_value, genesis_commitment_hash, ctxt).
Definition kind_value
(ctxt : Raw_context.t) (address : Sc_rollup_repr.Address.t)
: M? (Raw_context.t × Sc_rollups.Kind.t) :=
let? '(ctxt, kind_opt) :=
Store.PVM_kind.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
ctxt address in
match kind_opt with
| Some k_value ⇒ return? (ctxt, k_value)
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
address)
end.
Definition list_unaccounted (ctxt : Raw_context.t)
: M? (list Sc_rollup_repr.Address.t) :=
Store.PVM_kind.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted)
ctxt.
Definition genesis_info
(ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
: M? (Raw_context.t × Sc_rollup_commitment_repr.genesis_info) :=
let? '(ctxt, genesis_info) :=
Store.Genesis_info.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
ctxt rollup in
match genesis_info with
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
rollup)
| Some genesis_info ⇒ return? (ctxt, genesis_info)
end.
Definition get_metadata
(ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
: M? (Raw_context.t × Sc_rollup_metadata_repr.t) :=
let? '(ctxt, genesis_info) := genesis_info ctxt rollup in
let metadata :=
{| Sc_rollup_metadata_repr.t.address := rollup;
Sc_rollup_metadata_repr.t.origination_level :=
genesis_info.(Sc_rollup_commitment_repr.genesis_info.level); |} in
return? (ctxt, metadata).
Definition parameters_type
(ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
: M? (option Script_repr.lazy_expr × Raw_context.t) :=
Error_monad.Lwt_result_syntax.op_letplus
(Store.Parameters_type.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
ctxt rollup)
(fun function_parameter ⇒
let '(ctxt, res) := function_parameter in
(res, ctxt)).