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.Tzresult_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) (boot_sector : string)
  (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 level := Raw_context.current_level 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? '(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 :=
          level.(Level_repr.t.level);
        Sc_rollup_commitment_repr.genesis_info.commitment_hash :=
          genesis_commitment_hash; |} in
  let? '(ctxt, boot_sector_size, _sector_existed) :=
    Store.Boot_sector.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      ctxt address boot_sector 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 inbox_value :=
    Sc_rollup_inbox_repr.empty (Raw_context.recover ctxt) address
      level.(Level_repr.t.level) in
  let? '(ctxt, inbox_size_diff) :=
    Store.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      ctxt address inbox_value 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 level.(Level_repr.t.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 boot_sector_size) +i
      addresses_size) +i inbox_size_diff) +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_tzresult_syntax.fail
      (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_tzresult_syntax.fail
      (Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
        rollup)
  | Some genesis_inforeturn? (ctxt, genesis_info)
  end.

Definition get_boot_sector
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  : M? (Raw_context.t × string) :=
  let? '(ctxt, boot_sector) :=
    Storage.Sc_rollup.Boot_sector.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      ctxt rollup in
  match boot_sector with
  | None
    Error_monad.Lwt_tzresult_syntax.fail
      (Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
        rollup)
  | Some boot_sectorreturn? (ctxt, boot_sector)
  end.

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)).

Module Dal_slot.
  Definition slot_of_int_e (n_value : int) : M? Dal_slot_repr.Index.t :=
    match Dal_slot_repr.Index.of_int n_value with
    | None
      Error_monad.Tzresult_syntax.fail
        (Build_extensible "Dal_slot_index_above_hard_limit" unit tt)
    | Some slot_indexreturn? slot_index
    end.

  Definition fail_if_slot_index_invalid
    (ctxt : Raw_context.t) (slot_index : Dal_slot_repr.Index.t)
    : M? Dal_slot_repr.Index.t :=
    let? max_slot_index :=
      slot_of_int_e
        ((Raw_context.constants ctxt).(Constants_parametric_repr.t.dal).(Constants_parametric_repr.dal.number_of_slots)
        -i 1) in
    if
      ((Dal_slot_repr.Index.compare slot_index max_slot_index) >i 0) ||
      ((Dal_slot_repr.Index.compare slot_index Dal_slot_repr.Index.zero) <i 0)
    then
      Error_monad.Lwt_tzresult_syntax.fail
        (Build_extensible "Dal_subscribe_rollup_invalid_slot_index"
          Dal_errors_repr.Dal_subscribe_rollup_invalid_slot_index
          {|
            Dal_errors_repr.Dal_subscribe_rollup_invalid_slot_index.given :=
              slot_index;
            Dal_errors_repr.Dal_subscribe_rollup_invalid_slot_index.maximum :=
              max_slot_index; |})
    else
      return? slot_index.

  Definition all_indexes (ctxt : Raw_context.t)
    : M? (list Dal_slot_repr.Index.t) :=
    let max_slot_index :=
      (Raw_context.constants ctxt).(Constants_parametric_repr.t.dal).(Constants_parametric_repr.dal.number_of_slots)
      -i 1 in
    Error_monad.all_e
      (List.map slot_of_int_e (Misc.op_minusminusgt 0 max_slot_index)).

  Definition subscribed_slots_at_level
    (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
    (level : Raw_level_repr.raw_level) : M? Bitset.t :=
    let current_level := (Raw_context.current_level ctxt).(Level_repr.t.level)
      in
    if Raw_level_repr.op_gt level current_level then
      Error_monad.Lwt_tzresult_syntax.fail
        (Build_extensible "Dal_requested_subscriptions_at_future_level"
          (Raw_level_repr.t × Raw_level_repr.t) (current_level, level))
    else
      let? subscription_levels :=
        Store.Slot_subscriptions.(Storage_sigs.Indexed_data_storage.keys)
          (ctxt, rollup) in
      let relevant_subscription_levels :=
        List.filter
          (fun (subscription_level : Raw_level_repr.raw_level) ⇒
            Raw_level_repr.op_lteq subscription_level level) subscription_levels
        in
      let last_subscription_level_opt :=
        List.fold_left
          (fun (max_level : option Raw_level_repr.raw_level) ⇒
            fun (level : Raw_level_repr.raw_level) ⇒
              match max_level with
              | NoneSome level
              | Some max_level
                Some
                  (if Raw_level_repr.op_gt max_level level then
                    max_level
                  else
                    level)
              end) None relevant_subscription_levels in
      match last_subscription_level_opt with
      | Nonereturn? Bitset.empty
      | Some subscription_level
        Store.Slot_subscriptions.(Storage_sigs.Indexed_data_storage.get)
          (ctxt, rollup) subscription_level
      end.

  Definition subscribe
    (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
    (slot_index : Dal_slot_repr.Index.t)
    : M? (Dal_slot_repr.Index.t × Raw_level_repr.t × Raw_context.t) :=
    let? _slot_index := fail_if_slot_index_invalid ctxt slot_index in
    let? _initial_level := genesis_info ctxt rollup in
    let '{| Level_repr.t.level := level |} := Raw_context.current_level ctxt in
    let? subscribed_slots := subscribed_slots_at_level ctxt rollup level in
    let? slot_already_subscribed :=
      Bitset.mem subscribed_slots (Dal_slot_repr.Index.to_int slot_index) in
    if slot_already_subscribed then
      Error_monad.Lwt_tzresult_syntax.fail
        (Build_extensible "Dal_rollup_already_registered_to_slot"
          (Sc_rollup_repr.t × Dal_slot_repr.Index.t) (rollup, slot_index))
    else
      let? subscribed_slots :=
        Bitset.add subscribed_slots (Dal_slot_repr.Index.to_int slot_index) in
      let ctxt :=
        Store.Slot_subscriptions.(Storage_sigs.Indexed_data_storage.add)
          (ctxt, rollup) level subscribed_slots in
      return? (slot_index, level, ctxt).

  Definition subscribed_slot_indices
    (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
    (level : Raw_level_repr.raw_level) : M? (list Dal_slot_repr.Index.t) :=
    let all_indexes := all_indexes ctxt in
    let to_dal_slot_index_list (bitset : Bitset.t)
      : M? (list Dal_slot_repr.Index.t) :=
      let? all_indexes := all_indexes in
      Error_monad.Result_syntax.op_letplus
        (Error_monad.all_e
          (List.map
            (fun (i_value : Dal_slot_repr.Index.t) ⇒
              Error_monad.Result_syntax.op_letplus
                (Bitset.mem bitset (Dal_slot_repr.Index.to_int i_value))
                (fun is_index_present
                  if is_index_present then
                    [ i_value ]
                  else
                    nil)) all_indexes))
        (fun slot_indexesList.concat slot_indexes) in
    let? _initial_level := genesis_info ctxt rollup in
    let? subscribed_slots := subscribed_slots_at_level ctxt rollup level in
    let? result_value := to_dal_slot_index_list subscribed_slots in
    return? result_value.
End Dal_slot.