Skip to main content

🦏 Sc_rollup_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
      "Sc_rollup_max_number_of_available_messages_reached"
      "Maximum number of available messages reached"
      "Maximum number of available messages reached" None
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_max_number_of_available_messages_reached"
            then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_max_number_of_available_messages_reached"
          unit tt) in
  let description := "Already staked." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_already_staked" "Already staked" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_already_staked" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_already_staked" unit tt) in
  let description := "Attempted to cement a disputed commitment." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary "Sc_rollup_disputed"
      "Commitment disputed" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_disputed" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_disputed" unit tt) in
  let description := "Attempted to use a rollup that has not been originated."
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_does_not_exist" "Rollup does not exist" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (x_value : Sc_rollup_repr.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Rollup "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " does not exist"
                      CamlinternalFormatBasics.End_of_format)))
                "Rollup %a does not exist") Sc_rollup_repr.pp x_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_does_not_exist" then
            let x_value := cast Sc_rollup_repr.t payload in
            Some x_value
          else None
        end)
      (fun (x_value : Sc_rollup_repr.t) ⇒
        Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.t x_value) in
  let description := "No conflict." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_no_conflict" "No conflict" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_no_conflict" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_no_conflict" unit tt) in
  let description := "No stakers." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary "Sc_rollup_no_stakers"
      "No stakers" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_no_stakers" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_no_stakers" unit tt) in
  let description := "Unknown staker." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary "Sc_rollup_not_staked"
      "Unknown staker" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_not_staked" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_not_staked" unit tt) in
  let description :=
    "Attempted to withdraw while not staked on the last cemented commitment." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_not_staked_on_lcc" "Rollup not staked on LCC" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_not_staked_on_lcc" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_not_staked_on_lcc" unit tt) in
  let description := "Parent is not cemented." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_parent_not_lcc" "Parent not cemented" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_parent_not_lcc" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_parent_not_lcc" unit tt) in
  let description := "Can not remove a cemented commitment." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary "Sc_rollup_remove_lcc"
      "Can not remove cemented" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_remove_lcc" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_remove_lcc" unit tt) in
  let description := "Staker backtracked." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_staker_backtracked" "Staker backtracked" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_staker_backtracked" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_staker_backtracked" unit tt) in
  let description :=
    "Commitment is too far ahead of the last cemented commitment." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_too_far_ahead" "Commitment too far ahead" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_too_far_ahead" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_too_far_ahead" unit tt) in
  let description :=
    "Attempted to cement a commitment before its refutation deadline." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary "Sc_rollup_too_recent"
      "Commitment too recent" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_too_recent" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_too_recent" unit tt) in
  let description := "Unknown commitment." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_unknown_commitment" "Rollup does not exist" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (x_value : Sc_rollup_repr.Commitment_hash.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Commitment "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " does not exist"
                      CamlinternalFormatBasics.End_of_format)))
                "Commitment %a does not exist")
              Sc_rollup_repr.Commitment_hash.pp x_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "commitment"
          Sc_rollup_repr.Commitment_hash.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_unknown_commitment" then
            let x_value := cast Sc_rollup_repr.Commitment_hash.t payload in
            Some x_value
          else None
        end)
      (fun (x_value : Sc_rollup_repr.Commitment_hash.t) ⇒
        Build_extensible "Sc_rollup_unknown_commitment"
          Sc_rollup_repr.Commitment_hash.t x_value) in
  let description := "Attempted to commit to a bad inbox level." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Sc_rollup_bad_inbox_level" "Committed too soon" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_bad_inbox_level" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_bad_inbox_level" unit tt) in
  tt.

To be removed once [Lwt_tzresult_syntax] is in the environment.
Module Lwt_tzresult_syntax.
  Definition op_letstar {A B C : Set}
    : Pervasives.result A B (A Pervasives.result C B)
    Pervasives.result C B := Error_monad.op_gtgteqquestion.

  Definition _return {A B : Set} : A Pervasives.result A B :=
    Error_monad._return.
End Lwt_tzresult_syntax.

Module Store := Storage.Sc_rollup.

Definition originate
  (ctxt : Raw_context.t) (kind_value : Sc_rollup_repr.Kind.t)
  (boot_sector : string)
  : M? (Sc_rollup_repr.Address.t × Z.t × Raw_context.t) :=
  let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
  let level := Raw_context.current_level ctxt in
  let? address := Sc_rollup_repr.Address.from_nonce nonce_value in
  let ctxt :=
    Storage.Sc_rollup.PVM_kind.(Storage_sigs.Indexed_data_storage.add) ctxt
      address kind_value in
  let ctxt :=
    Storage.Sc_rollup.Initial_level.(Storage_sigs.Indexed_data_storage.add) ctxt
      address (Level_storage.current ctxt).(Level_repr.t.level) in
  let ctxt :=
    Storage.Sc_rollup.Boot_sector.(Storage_sigs.Indexed_data_storage.add) ctxt
      address boot_sector in
  let inbox := Sc_rollup_inbox_repr.empty address level.(Level_repr.t.level) in
  let? '(ctxt, size_diff) :=
    Storage.Sc_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      ctxt address inbox in
  let? '(ctxt, lcc_size_diff) :=
    Store.Last_cemented_commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      ctxt address Sc_rollup_repr.Commitment_hash.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 boot_sector_size :=
    Data_encoding.Binary.length Data_encoding.string_value boot_sector 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 size_diff) +i lcc_size_diff) +i stakers_size_diff) in
  return? (address, size_value, ctxt).

Definition kind_value
  (ctxt : Raw_context.t) (address : Sc_rollup_repr.Address.t)
  : M? (option Sc_rollup_repr.Kind.t) :=
  Storage.Sc_rollup.PVM_kind.(Storage_sigs.Indexed_data_storage.find) ctxt
    address.

Definition last_cemented_commitment
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  : M? (Sc_rollup_repr.Commitment_hash.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Last_cemented_commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      ctxt rollup in
  match res with
  | None
    Error_monad.fail
      (Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
        rollup)
  | Some lccLwt_tzresult_syntax._return (lcc, ctxt)
  end.

Try to consume n messages.
Definition consume_n_messages
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t) (n_value : int)
  : M? Raw_context.t :=
  let? '(ctxt, inbox) :=
    Storage.Sc_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      ctxt rollup in
  let? function_parameter :=
    Sc_rollup_inbox_repr.consume_n_messages n_value inbox in
  match function_parameter with
  | NoneLwt_tzresult_syntax._return ctxt
  | Some inbox
    let? '(ctxt, size_value) :=
      Storage.Sc_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
        ctxt rollup inbox in
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit (size_value i 0) in
    Lwt_tzresult_syntax._return ctxt
  end.

Definition inbox (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  : M? (Sc_rollup_inbox_repr.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Storage.Sc_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      ctxt rollup in
  match res with
  | None
    Error_monad.fail
      (Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
        rollup)
  | Some inboxLwt_tzresult_syntax._return (inbox, ctxt)
  end.

Definition assert_inbox_size_ok (ctxt : Raw_context.t) (next_size : Z.t)
  : M? unit :=
  let max_size := Constants_storage.sc_rollup_max_available_messages ctxt in
  Error_monad.fail_unless (next_size Z (Z.of_int max_size))
    (Build_extensible "Sc_rollup_max_number_of_available_messages_reached" unit
      tt).

Definition add_messages
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (messages : list string)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  let? '(inbox, ctxt) := inbox ctxt rollup in
  let next_size :=
    (Sc_rollup_inbox_repr.number_of_available_messages inbox) +Z
    (Z.of_int (List.length messages)) in
  let? '_ := assert_inbox_size_ok ctxt next_size in
  (fun (current_messages : Sc_rollup_inbox_repr.message) ⇒
    let '{| Level_repr.t.level := level |} := Raw_context.current_level ctxt in
    let? '(current_messages, inbox) :=
      Sc_rollup_inbox_repr.add_messages_no_history inbox level messages
        current_messages in
    (fun (ctxt : Raw_context.t) ⇒
      let? '(ctxt, size_value) :=
        Storage.Sc_rollup.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
          ctxt rollup inbox in
      return? (inbox, (Z.of_int size_value), ctxt))
      (Raw_context.Sc_rollup_in_memory_inbox.set_current_messages ctxt rollup
        current_messages))
    (Raw_context.Sc_rollup_in_memory_inbox.current_messages ctxt rollup).

Definition get_commitment_internal
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (commitment : Sc_rollup_repr.Commitment_hash.t)
  : M? (Sc_rollup_repr.Commitment.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) commitment in
  match res with
  | None
    Error_monad.fail
      (Build_extensible "Sc_rollup_unknown_commitment"
        Sc_rollup_repr.Commitment_hash.t commitment)
  | Some commitmentLwt_tzresult_syntax._return (commitment, ctxt)
  end.

Definition get_commitment
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (commitment : Sc_rollup_repr.Commitment_hash.t)
  : M? (Sc_rollup_repr.Commitment.t × Raw_context.t) :=
  let? '(_lcc, ctxt) := last_cemented_commitment ctxt rollup in
  get_commitment_internal ctxt rollup commitment.

Definition get_predecessor
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_repr.Commitment_hash.t)
  : M? (Sc_rollup_repr.Commitment_hash.t × Raw_context.t) :=
  let? '(commitment, ctxt) := get_commitment_internal ctxt rollup node_value in
  Lwt_tzresult_syntax._return
    (commitment.(Sc_rollup_repr.Commitment.t.predecessor), ctxt).

Definition find_staker
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash)
  : M? (Sc_rollup_repr.Commitment_hash.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match res with
  | NoneError_monad.fail (Build_extensible "Sc_rollup_not_staked" unit tt)
  | Some branchLwt_tzresult_syntax._return (branch, ctxt)
  end.

Definition modify_staker_count
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (f_value : int32 int32) : M? Raw_context.t :=
  let? '(ctxt, maybe_count) :=
    Store.Staker_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      ctxt rollup in
  let count := Option.value_value maybe_count 0 in
  let? '(ctxt, size_diff, _was_bound) :=
    Store.Staker_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      ctxt rollup (f_value count) in
  let '_ :=
    (* ❌ Assert instruction is not handled. *)
    assert unit (size_diff =i 0) in
  Lwt_tzresult_syntax._return ctxt.

Definition get_commitment_stake_count
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_repr.Commitment_hash.t)
  : M? (int32 × Raw_context.t) :=
  let? '(ctxt, maybe_staked_on_commitment) :=
    Store.Commitment_stake_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) node_value in
  Lwt_tzresult_syntax._return
    ((Option.value_value maybe_staked_on_commitment 0), ctxt).

[set_commitment_added ctxt rollup node current] sets the commitment addition time of [node] to [current] iff the commitment time was not previously set, and leaves it unchanged otherwise.
Definition set_commitment_added
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_repr.Commitment_hash.t) (new_value : Raw_level_repr.t)
  : M? (int × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) node_value in
  let new_value :=
    match res with
    | Nonenew_value
    | Some old_valueold_value
    end in
  let? '(ctxt, size_diff, _was_bound) :=
    Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      (ctxt, rollup) node_value new_value in
  Lwt_tzresult_syntax._return (size_diff, ctxt).

Definition deallocate
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_repr.Commitment_hash.t) : M? Raw_context.t :=
  if
    Sc_rollup_repr.Commitment_hash.op_eq node_value
      Sc_rollup_repr.Commitment_hash.zero
  then
    Lwt_tzresult_syntax._return ctxt
  else
    let? '(ctxt, _size_freed) :=
      Store.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing)
        (ctxt, rollup) node_value in
    let? '(ctxt, _size_freed) :=
      Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing)
        (ctxt, rollup) node_value in
    let? '(ctxt, _size_freed) :=
      Store.Commitment_stake_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing)
        (ctxt, rollup) node_value in
    Lwt_tzresult_syntax._return ctxt.

Definition modify_commitment_stake_count
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_repr.Commitment_hash.t) (f_value : int32 int32)
  : M? (int32 × int × Raw_context.t) :=
  let? '(count, ctxt) := get_commitment_stake_count ctxt rollup node_value in
  let new_count := f_value count in
  let? '(ctxt, size_diff, _was_bound) :=
    Store.Commitment_stake_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      (ctxt, rollup) node_value new_count in
  Lwt_tzresult_syntax._return (new_count, size_diff, ctxt).

Definition increase_commitment_stake_count
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_repr.Commitment_hash.t) : M? (int × Raw_context.t) :=
  let? '(_new_count, size_diff, ctxt) :=
    modify_commitment_stake_count ctxt rollup node_value Int32.succ in
  Lwt_tzresult_syntax._return (size_diff, ctxt).

Definition decrease_commitment_stake_count
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_repr.Commitment_hash.t) : M? Raw_context.t :=
  let? '(new_count, _size_diff, ctxt) :=
    modify_commitment_stake_count ctxt rollup node_value Int32.pred in
  if new_count i32 0 then
    deallocate ctxt rollup node_value
  else
    Lwt_tzresult_syntax._return ctxt.

Definition deposit_stake
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (staker : Signature.public_key_hash) : M? Raw_context.t :=
  let? '(lcc, ctxt) := last_cemented_commitment ctxt rollup in
  let? '(ctxt, res) :=
    Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match res with
  | None
    let? '(ctxt, _size) :=
      Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
        (ctxt, rollup) staker lcc in
    let? ctxt := modify_staker_count ctxt rollup Int32.succ in
    Lwt_tzresult_syntax._return ctxt
  | Some _
    Error_monad.fail (Build_extensible "Sc_rollup_already_staked" unit tt)
  end.

Definition withdraw_stake
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (staker : Signature.public_key_hash) : M? Raw_context.t :=
  let? '(lcc, ctxt) := last_cemented_commitment ctxt rollup in
  let? '(ctxt, res) :=
    Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match res with
  | NoneError_monad.fail (Build_extensible "Sc_rollup_not_staked" unit tt)
  | Some staked_on_commitment
    if Sc_rollup_repr.Commitment_hash.op_eq staked_on_commitment lcc then
      let? '(ctxt, _size_freed) :=
        Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing)
          (ctxt, rollup) staker in
      let? ctxt := modify_staker_count ctxt rollup Int32.pred in
      modify_staker_count ctxt rollup Int32.pred
    else
      Error_monad.fail (Build_extensible "Sc_rollup_not_staked_on_lcc" unit tt)
  end.

Definition sc_rollup_max_lookahead : int32 := 30000.

Definition sc_rollup_commitment_frequency : int := 20.

Definition sc_rollup_commitment_storage_size_in_bytes : int := 84.

Definition assert_commitment_not_too_far_ahead
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (lcc : Sc_rollup_repr.Commitment_hash.t)
  (commitment : Sc_rollup_repr.Commitment.t) : M? Raw_context.t :=
  let? '(ctxt, min_level) :=
    if
      Sc_rollup_repr.Commitment_hash.op_eq lcc
        Sc_rollup_repr.Commitment_hash.zero
    then
      let? level :=
        Store.Initial_level.(Storage_sigs.Indexed_data_storage.get) ctxt rollup
        in
      Lwt_tzresult_syntax._return (ctxt, level)
    else
      let? '(lcc, ctxt) := get_commitment_internal ctxt rollup lcc in
      Lwt_tzresult_syntax._return
        (ctxt, lcc.(Sc_rollup_repr.Commitment.t.inbox_level)) in
  let max_level := commitment.(Sc_rollup_repr.Commitment.t.inbox_level) in
  if
    sc_rollup_max_lookahead <i32 (Raw_level_repr.diff_value max_level min_level)
  then
    Error_monad.fail (Build_extensible "Sc_rollup_too_far_ahead" unit tt)
  else
    Lwt_tzresult_syntax._return ctxt.

Enfore that a commitment's inbox level increases by an exact fixed amount over its predecessor. This property is used in several places - not obeying it causes severe breakage.
Check invariants on [inbox_level], enforcing overallocation of storage and regularity of block prorudction.
The constants used by [assert_refine_conditions_met] must be chosen such that the maximum cost of storage allocated by each staker at most the size of their deposit.
Definition assert_refine_conditions_met
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (lcc : Sc_rollup_repr.Commitment_hash.t)
  (commitment : Sc_rollup_repr.Commitment.t) : M? Raw_context.t :=
  let? ctxt := assert_commitment_not_too_far_ahead ctxt rollup lcc commitment in
  assert_commitment_frequency ctxt rollup commitment.

#[bypass_check(guard)]
Definition refine_stake
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (staker : Signature.public_key_hash)
  (commitment : Sc_rollup_repr.Commitment.t)
  : M? (Sc_rollup_repr.Commitment_hash.t × Raw_context.t) :=
  let? '(lcc, ctxt) := last_cemented_commitment ctxt rollup in
  let? '(staked_on, ctxt) := find_staker ctxt rollup staker in
  let? ctxt := assert_refine_conditions_met ctxt rollup lcc commitment in
  let new_hash := Sc_rollup_repr.Commitment.hash_value commitment in
  let fix go
    (node_value : Sc_rollup_repr.Commitment_hash.t) (ctxt : Raw_context.t)
    {struct node_value}
    : M? (Sc_rollup_repr.Commitment_hash.t × Raw_context.t) :=
    if Sc_rollup_repr.Commitment_hash.op_eq node_value staked_on then
      let? '(ctxt, commitment_size_diff, _was_bound) :=
        Store.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
          (ctxt, rollup) new_hash commitment in
      let level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
      let? '(commitment_added_size_diff, ctxt) :=
        set_commitment_added ctxt rollup new_hash level in
      let? '(ctxt, staker_count_diff) :=
        Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
          (ctxt, rollup) staker new_hash in
      let? '(stake_count_size_diff, ctxt) :=
        increase_commitment_stake_count ctxt rollup new_hash in
      let size_diff :=
        ((commitment_size_diff +i commitment_added_size_diff) +i
        stake_count_size_diff) +i staker_count_diff in
      let '_ :=
        (* ❌ Assert instruction is not handled. *)
        assert unit
          ((size_diff =i 0) ||
          (size_diff =i sc_rollup_commitment_storage_size_in_bytes)) in
      Lwt_tzresult_syntax._return (new_hash, ctxt)
    else
      if Sc_rollup_repr.Commitment_hash.op_eq node_value lcc then
        Error_monad.fail
          (Build_extensible "Sc_rollup_staker_backtracked" unit tt)
      else
        let? '(pred, ctxt) := get_predecessor ctxt rollup node_value in
        let? '(_size, ctxt) :=
          increase_commitment_stake_count ctxt rollup node_value in
        go pred ctxt in
  go commitment.(Sc_rollup_repr.Commitment.t.predecessor) ctxt.

Definition publish_commitment
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash)
  (commitment : Sc_rollup_repr.Commitment.t)
  : M? (Sc_rollup_repr.Commitment_hash.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match res with
  | None
    let? ctxt := deposit_stake ctxt rollup staker in
    refine_stake ctxt rollup staker commitment
  | Some _refine_stake ctxt rollup staker commitment
  end.

Definition cement_commitment
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (new_lcc : Sc_rollup_repr.Commitment_hash.t) : M? Raw_context.t :=
  let refutation_deadline_blocks :=
    Constants_storage.sc_rollup_challenge_window_in_blocks ctxt in
  let? '(old_lcc, ctxt) := last_cemented_commitment ctxt rollup in
  let? '(ctxt, total_staker_count) :=
    Store.Staker_count.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      ctxt rollup in
  if total_staker_count i32 0 then
    Error_monad.fail (Build_extensible "Sc_rollup_no_stakers" unit tt)
  else
    let? '(new_lcc_commitment, ctxt) :=
      get_commitment_internal ctxt rollup new_lcc in
    let? '(ctxt, new_lcc_added) :=
      Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
        (ctxt, rollup) new_lcc in
    if
      Sc_rollup_repr.Commitment_hash.op_ltgt
        new_lcc_commitment.(Sc_rollup_repr.Commitment.t.predecessor) old_lcc
    then
      Error_monad.fail (Build_extensible "Sc_rollup_parent_not_lcc" unit tt)
    else
      let? '(new_lcc_stake_count, ctxt) :=
        get_commitment_stake_count ctxt rollup new_lcc in
      if total_staker_count i32 new_lcc_stake_count then
        Error_monad.fail (Build_extensible "Sc_rollup_disputed" unit tt)
      else
        if
          let level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
          Raw_level_repr.op_lt level
            (Raw_level_repr.add new_lcc_added refutation_deadline_blocks)
        then
          Error_monad.fail (Build_extensible "Sc_rollup_too_recent" unit tt)
        else
          let? '(ctxt, lcc_size_diff) :=
            Store.Last_cemented_commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
              ctxt rollup new_lcc in
          let '_ :=
            (* ❌ Assert instruction is not handled. *)
            assert unit (lcc_size_diff =i 0) in
          let? ctxt := deallocate ctxt rollup old_lcc in
          consume_n_messages ctxt rollup
            (Int32.to_int
              (Sc_rollup_repr.Number_of_messages.(Bounded.Int32.S.to_int32)
                new_lcc_commitment.(Sc_rollup_repr.Commitment.t.number_of_messages))).

Definition conflict_point : Set :=
  Sc_rollup_repr.Commitment_hash.t × Sc_rollup_repr.Commitment_hash.t.

[goto_inbox_level ctxt rollup inbox_level commit] Follows the predecessors of [commit] until it arrives at the exact [inbox_level]. The result is the commit hash at the given inbox level.
#[bypass_check(guard)]
Definition goto_inbox_level
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (inbox_level : Raw_level_repr.raw_level)
  (commit : Sc_rollup_repr.Commitment_hash.t)
  : M? (Sc_rollup_repr.Commitment_hash.t × Raw_context.t) :=
  let fix go (ctxt : Raw_context.t) (commit : Sc_rollup_repr.Commitment_hash.t)
    {struct commit} : M? (Sc_rollup_repr.Commitment_hash.t × Raw_context.t) :=
    let? '(info_value, ctxt) := get_commitment_internal ctxt rollup commit in
    if
      Raw_level_repr.op_lteq
        info_value.(Sc_rollup_repr.Commitment.t.inbox_level) inbox_level
    then
      let '_ :=
        (* ❌ Assert instruction is not handled. *)
        assert unit
          (Raw_level_repr.op_eq
            info_value.(Sc_rollup_repr.Commitment.t.inbox_level) inbox_level) in
      Lwt_tzresult_syntax._return (commit, ctxt)
    else
      go ctxt info_value.(Sc_rollup_repr.Commitment.t.predecessor) in
  go ctxt commit.

#[bypass_check(guard)]
Definition get_conflict_point
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (staker1 : Signature.public_key_hash) (staker2 : Signature.public_key_hash)
  : M?
    ((Sc_rollup_repr.Commitment_hash.t × Sc_rollup_repr.Commitment_hash.t) ×
      Raw_context.t) :=
  let? '(lcc, ctxt) := last_cemented_commitment ctxt rollup in
  let? '(commit1, ctxt) := find_staker ctxt rollup staker1 in
  let? '(commit2, ctxt) := find_staker ctxt rollup staker2 in
  let? '_ :=
    Error_monad.fail_when
      ((Sc_rollup_repr.Commitment_hash.op_eq commit1
        Sc_rollup_repr.Commitment_hash.zero) ||
      ((Sc_rollup_repr.Commitment_hash.op_eq commit2
        Sc_rollup_repr.Commitment_hash.zero) ||
      ((Sc_rollup_repr.Commitment_hash.op_eq commit1 lcc) ||
      (Sc_rollup_repr.Commitment_hash.op_eq commit2 lcc))))
      (Build_extensible "Sc_rollup_no_conflict" unit tt) in
  let? '(commit1_info, ctxt) := get_commitment_internal ctxt rollup commit1 in
  let? '(commit2_info, ctxt) := get_commitment_internal ctxt rollup commit2 in
  let target_inbox_level :=
    Raw_level_repr.min commit1_info.(Sc_rollup_repr.Commitment.t.inbox_level)
      commit2_info.(Sc_rollup_repr.Commitment.t.inbox_level) in
  let? '(commit1, ctxt) :=
    goto_inbox_level ctxt rollup target_inbox_level commit1 in
  let? '(commit2, ctxt) :=
    goto_inbox_level ctxt rollup target_inbox_level commit2 in
  let fix traverse_in_parallel
    (ctxt : Raw_context.t) (commit1 : Sc_rollup_repr.Commitment_hash.t)
    (commit2 : Sc_rollup_repr.Commitment_hash.t) {struct commit1}
    : M?
      ((Sc_rollup_repr.Commitment_hash.t × Sc_rollup_repr.Commitment_hash.t) ×
        Raw_context.t) :=
    if Sc_rollup_repr.Commitment_hash.op_eq commit1 commit2 then
      Error_monad.fail (Build_extensible "Sc_rollup_no_conflict" unit tt)
    else
      let? '(commit1_info, ctxt) := get_commitment_internal ctxt rollup commit1
        in
      let? '(commit2_info, ctxt) := get_commitment_internal ctxt rollup commit2
        in
      let '_ :=
        (* ❌ Assert instruction is not handled. *)
        assert unit
          (Raw_level_repr.op_eq
            commit1_info.(Sc_rollup_repr.Commitment.t.inbox_level)
            commit2_info.(Sc_rollup_repr.Commitment.t.inbox_level)) in
      if
        Sc_rollup_repr.Commitment_hash.op_eq
          commit1_info.(Sc_rollup_repr.Commitment.t.predecessor)
          commit2_info.(Sc_rollup_repr.Commitment.t.predecessor)
      then
        Lwt_tzresult_syntax._return ((commit1, commit2), ctxt)
      else
        traverse_in_parallel ctxt
          commit1_info.(Sc_rollup_repr.Commitment.t.predecessor)
          commit2_info.(Sc_rollup_repr.Commitment.t.predecessor) in
  traverse_in_parallel ctxt commit1 commit2.

#[bypass_check(guard)]
Definition remove_staker
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (staker : Signature.public_key_hash) : M? Raw_context.t :=
  let? '(lcc, ctxt) := last_cemented_commitment ctxt rollup in
  let? '(ctxt, res) :=
    Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match res with
  | NoneError_monad.fail (Build_extensible "Sc_rollup_not_staked" unit tt)
  | Some staked_on
    if Sc_rollup_repr.Commitment_hash.op_eq staked_on lcc then
      Error_monad.fail (Build_extensible "Sc_rollup_remove_lcc" unit tt)
    else
      let? '(ctxt, _size_diff) :=
        Store.Stakers.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing)
          (ctxt, rollup) staker in
      let? ctxt := modify_staker_count ctxt rollup Int32.pred in
      let fix go
        (node_value : Sc_rollup_repr.Commitment_hash.t) (ctxt : Raw_context.t)
        {struct node_value} : M? Raw_context.t :=
        if Sc_rollup_repr.Commitment_hash.op_eq node_value lcc then
          Lwt_tzresult_syntax._return ctxt
        else
          let? '(pred, ctxt) := get_predecessor ctxt rollup node_value in
          let? ctxt := decrease_commitment_stake_count ctxt rollup node_value in
          go pred ctxt in
      go staked_on ctxt
  end.

Definition list_value {A : Set} (ctxt : Raw_context.t)
  : Pervasives.result (list Sc_rollup_repr.Address.t) A :=
  Error_monad.op_gtpipeeq
    (Storage.Sc_rollup.PVM_kind.(Storage_sigs.Indexed_data_storage.keys) ctxt)
    Result._return.

Definition initial_level
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  : M? Raw_level_repr.t :=
  let? level :=
    Storage.Sc_rollup.Initial_level.(Storage_sigs.Indexed_data_storage.find)
      ctxt rollup in
  match level with
  | None
    Error_monad.fail
      (Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
        rollup)
  | Some levelLwt_tzresult_syntax._return level
  end.