Skip to main content

🦏 Sc_rollup_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
[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_valuereturn? (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_inforeturn? (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)).