Skip to main content

🦏 Sc_rollup_stake_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_errors.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.

Module Store := Storage.Sc_rollup.

Module Commitment_storage := Sc_rollup_commitment_storage.

Module Commitment := Sc_rollup_commitment_repr.

Module Commitment_hash := Commitment.Hash.

Definition find_staker_unsafe
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash)
  : M? (Sc_rollup_commitment_repr.Hash.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Stakers.(Storage_sigs.Indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match res with
  | None
    Error_monad.Lwt_tzresult_syntax.fail
      (Build_extensible "Sc_rollup_not_staked" unit tt)
  | Some branchreturn? (branch, ctxt)
  end.

Definition find_staker
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (staker : Signature.public_key_hash)
  : M? (Sc_rollup_commitment_repr.Hash.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Last_cemented_commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
      ctxt rollup in
  if Pervasives.not res then
    Error_monad.Lwt_tzresult_syntax.fail
      (Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
        rollup)
  else
    find_staker_unsafe ctxt rollup staker.

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
  if size_diff =i 0 then
    return? ctxt
  else
    Error_monad.error_value (Build_extensible "Asserted" unit tt).

Definition get_contract_and_stake
  (ctxt : Raw_context.t) (staker : Signature.public_key_hash)
  : Contract_repr.t × Tez_repr.t :=
  let staker_contract := Contract_repr.Implicit staker in
  let stake := Constants_storage.sc_rollup_stake_amount ctxt in
  (staker_contract, stake).

Warning: must be called only if [rollup] exists and [staker] is not to be found in {!Store.Stakers.}
Definition deposit_stake
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash)
  : M?
    (Raw_context.t × Receipt_repr.balance_updates ×
      Commitment_storage.Commitment_hash.t) :=
  let? '(lcc, ctxt) := Commitment_storage.last_cemented_commitment ctxt rollup
    in
  let '(staker_contract, stake) := get_contract_and_stake ctxt staker in
  let? '(ctxt, staker_balance) :=
    Token.balance ctxt (Token.Contract staker_contract) in
  let? '_ :=
    Error_monad.fail_when (Tez_repr.op_lt staker_balance stake)
      (Build_extensible "Sc_rollup_staker_funds_too_low"
        Sc_rollup_errors.Sc_rollup_staker_funds_too_low
        {| Sc_rollup_errors.Sc_rollup_staker_funds_too_low.staker := staker;
          Sc_rollup_errors.Sc_rollup_staker_funds_too_low.sc_rollup := rollup;
          Sc_rollup_errors.Sc_rollup_staker_funds_too_low.staker_balance :=
            staker_balance;
          Sc_rollup_errors.Sc_rollup_staker_funds_too_low.min_expected_balance
            := stake; |}) in
  let bond_id := Bond_id_repr.Sc_rollup_bond_id rollup in
  let? '(ctxt, balance_updates) :=
    Token.transfer None ctxt
      (Token.Source_container (Token.Contract staker_contract))
      (Token.Sink_container (Token.Frozen_bonds staker_contract bond_id)) stake
    in
  let? '(ctxt, _size) :=
    Store.Stakers.(Storage_sigs.Indexed_carbonated_data_storage.init_value)
      (ctxt, rollup) staker lcc in
  let? ctxt := modify_staker_count ctxt rollup Int32.succ in
  return? (ctxt, balance_updates, lcc).

Definition withdraw_stake
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash)
  : M? (Raw_context.t × Receipt_repr.balance_updates) :=
  let? '(lcc, ctxt) := Commitment_storage.last_cemented_commitment ctxt rollup
    in
  let? '(ctxt, res) :=
    Store.Stakers.(Storage_sigs.Indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match res with
  | None
    Error_monad.Lwt_tzresult_syntax.fail
      (Build_extensible "Sc_rollup_not_staked" unit tt)
  | Some staked_on_commitment
    let? '_ :=
      Error_monad.fail_unless (Commitment_hash.op_eq staked_on_commitment lcc)
        (Build_extensible "Sc_rollup_not_staked_on_lcc" unit tt) in
    let '(staker_contract, stake) := get_contract_and_stake ctxt staker in
    let bond_id := Bond_id_repr.Sc_rollup_bond_id rollup in
    let? '(ctxt, balance_updates) :=
      Token.transfer None ctxt
        (Token.Source_container (Token.Frozen_bonds staker_contract bond_id))
        (Token.Sink_container (Token.Contract staker_contract)) stake in
    let? '(ctxt, _size_freed) :=
      Store.Stakers.(Storage_sigs.Indexed_carbonated_data_storage.remove_existing)
        (ctxt, rollup) staker in
    Error_monad.Lwt_tzresult_syntax.op_letplus
      (modify_staker_count ctxt rollup Int32.pred)
      (fun ctxt(ctxt, balance_updates))
  end.

Definition assert_commitment_not_too_far_ahead
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (lcc : Commitment_storage.Commitment_hash.t) (commitment : Commitment.t)
  : M? Raw_context.t :=
  let? '(lcc, ctxt) := Commitment_storage.get_commitment_unsafe ctxt rollup lcc
    in
  let min_level := lcc.(Sc_rollup_commitment_repr.V1.t.inbox_level) in
  let max_level := commitment.(Sc_rollup_commitment_repr.V1.t.inbox_level) in
  let? '_ :=
    Error_monad.fail_when
      (let sc_rollup_max_lookahead :=
        Constants_storage.sc_rollup_max_lookahead_in_blocks ctxt in
      sc_rollup_max_lookahead <i32
      (Raw_level_repr.diff_value max_level min_level))
      (Build_extensible "Sc_rollup_too_far_ahead" unit tt) in
  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.
Definition assert_commitment_period
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t) (commitment : Commitment.t)
  : M? Raw_context.t :=
  let pred_hash := commitment.(Sc_rollup_commitment_repr.V1.t.predecessor) in
  let? '(pred, ctxt) :=
    Commitment_storage.get_commitment_unsafe ctxt rollup pred_hash in
  let pred_level := pred.(Sc_rollup_commitment_repr.V1.t.inbox_level) in
  let sc_rollup_commitment_period :=
    Constants_storage.sc_rollup_commitment_period_in_blocks ctxt in
  let? '_ :=
    let? res := Raw_level_repr.add pred_level sc_rollup_commitment_period in
    Error_monad.fail_unless
      (Raw_level_repr.op_eq
        commitment.(Sc_rollup_commitment_repr.V1.t.inbox_level) res)
      (Build_extensible "Sc_rollup_bad_inbox_level" unit tt) in
  return? ctxt.

Definition assert_same_hash_as_predecessor
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t) (commitment : Commitment.t)
  : M? Raw_context.t :=
  let? '(pred, ctxt) :=
    Commitment_storage.get_commitment_unsafe ctxt rollup
      commitment.(Sc_rollup_commitment_repr.V1.t.predecessor) in
  if
    Sc_rollup_repr.State_hash.equal
      pred.(Sc_rollup_commitment_repr.V1.t.compressed_state)
      commitment.(Sc_rollup_commitment_repr.V1.t.compressed_state)
  then
    return? ctxt
  else
    Error_monad.Lwt_tzresult_syntax.fail
      (Build_extensible "Sc_rollup_state_change_on_zero_tick_commitment" unit tt).

Check invariants on [inbox_level], enforcing overallocation of storage and regularity of block production.
The constants used by [assert_refine_conditions_met] must be chosen such that the maximum cost of storage allocated by each staker is at most the size of their deposit.
Definition assert_refine_conditions_met
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (lcc : Commitment_storage.Commitment_hash.t) (commitment : Commitment.t)
  : M? Raw_context.t :=
  let? ctxt := assert_commitment_not_too_far_ahead ctxt rollup lcc commitment in
  let? ctxt := assert_commitment_period ctxt rollup commitment in
  let? zero := Sc_rollup_repr.Number_of_ticks.zero in
  if
    Sc_rollup_repr.Number_of_ticks.equal
      commitment.(Sc_rollup_commitment_repr.V1.t.number_of_ticks) zero
  then
    assert_same_hash_as_predecessor ctxt rollup commitment
  else
    return? ctxt.

Definition get_commitment_stake_count
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_commitment_repr.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
  return? ((Option.value_value maybe_staked_on_commitment 0), ctxt).

Definition modify_commitment_stake_count
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_commitment_repr.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
  return? (new_count, size_diff, ctxt).

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

Definition deallocate_commitment_metadata
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Commitment_hash.t) : M? Raw_context.t :=
  if Commitment_hash.op_eq node_value Commitment_hash.zero then
    return? ctxt
  else
    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
    return? ctxt.

Definition deallocate
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Commitment_hash.t) : M? Raw_context.t :=
  let? ctxt := deallocate_commitment_metadata ctxt rollup node_value in
  deallocate_commitment ctxt rollup node_value.

#[bypass_check(guard)]
Definition find_commitment_to_deallocate
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (commitment_hash : Commitment_storage.Commitment_hash.t)
  (num_commitments_to_keep : int)
  : M? (option Commitment_storage.Commitment_hash.t × Raw_context.t) :=
  let fix aux
    (ctxt : Raw_context.t)
    (commitment_hash : Commitment_storage.Commitment_hash.t) (n_value : int)
    {struct n_value}
    : M? (option Commitment_storage.Commitment_hash.t × Raw_context.t) :=
    if n_value =i 0 then
      return? ((Some commitment_hash), ctxt)
    else
      let? '(pred_hash, ctxt) :=
        Commitment_storage.get_predecessor_opt_unsafe ctxt rollup
          commitment_hash in
      match pred_hash with
      | Nonereturn? (None, ctxt)
      | Some pred_hashaux ctxt pred_hash (n_value -i 1)
      end in
  aux ctxt commitment_hash num_commitments_to_keep.

Definition decrease_commitment_stake_count
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_commitment_repr.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
    return? ctxt.

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

Definition commitment_storage_size_in_bytes : int := 85.

#[bypass_check(guard)]
Definition refine_stake
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash) (staked_on : Commitment_hash.t)
  (commitment : Commitment.t)
  : M?
    (Sc_rollup_commitment_storage.Commitment_hash.t × Raw_level_repr.t ×
      Raw_context.t) :=
  let? '(lcc, ctxt) := Commitment_storage.last_cemented_commitment ctxt rollup
    in
  let? ctxt := assert_refine_conditions_met ctxt rollup lcc commitment in
  let? '(ctxt, new_hash) :=
    Sc_rollup_commitment_storage.hash_value ctxt commitment in
  let fix go (node_value : Commitment_hash.t) (ctxt : Raw_context.t)
    {struct node_value}
    : M?
      (Sc_rollup_commitment_storage.Commitment_hash.t × Raw_level_repr.t ×
        Raw_context.t) :=
    if 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, commitment_added_level, ctxt) :=
        Commitment_storage.set_commitment_added ctxt rollup new_hash level in
      let? '(ctxt, staker_count_diff) :=
        Store.Stakers.(Storage_sigs.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 expected_size_diff := commitment_storage_size_in_bytes in
      if (size_diff =i 0) || (size_diff =i expected_size_diff) then
        return? (new_hash, commitment_added_level, ctxt)
      else
        Error_monad.error_value (Build_extensible "Asserted" unit tt)
    else
      let? '_ :=
        Error_monad.fail_when (Commitment_hash.op_eq node_value lcc)
          (Build_extensible "Sc_rollup_staker_backtracked" unit tt) in
      let? '(pred, ctxt) :=
        Commitment_storage.get_predecessor_unsafe 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_commitment_repr.V1.t.predecessor) ctxt.

Definition publish_commitment
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash) (commitment : Commitment.t)
  : M?
    (Sc_rollup_commitment_storage.Commitment_hash.t × Raw_level_repr.t ×
      Raw_context.t × Receipt_repr.balance_updates) :=
  let? '(ctxt, staked_on_opt) :=
    Store.Stakers.(Storage_sigs.Indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  let? '(ctxt, balance_updates, staked_on) :=
    match staked_on_opt with
    | Some staked_onreturn? (ctxt, nil, staked_on)
    | Nonedeposit_stake ctxt rollup staker
    end in
  Error_monad.Lwt_tzresult_syntax.op_letplus
    (refine_stake ctxt rollup staker staked_on commitment)
    (fun function_parameter
      let '(commitment_hash, ctxt, level) := function_parameter in
      (commitment_hash, ctxt, level, balance_updates)).

Definition cement_commitment
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (new_lcc : Commitment_storage.Commitment_hash.t)
  : M? (Raw_context.t × Commitment_storage.Commitment.t) :=
  let refutation_deadline_blocks :=
    Constants_storage.sc_rollup_challenge_window_in_blocks ctxt in
  let? '(old_lcc, ctxt) :=
    Commitment_storage.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
  let? '_ :=
    Error_monad.fail_when (total_staker_count i32 0)
      (Build_extensible "Sc_rollup_no_stakers" unit tt) in
  let? '(new_lcc_commitment, ctxt) :=
    Commitment_storage.get_commitment_unsafe ctxt rollup new_lcc in
  let? '_ :=
    Error_monad.fail_when
      (Commitment_hash.op_ltgt
        new_lcc_commitment.(Sc_rollup_commitment_repr.V1.t.predecessor) old_lcc)
      (Build_extensible "Sc_rollup_parent_not_lcc" unit tt) in
  let? '(new_lcc_stake_count, ctxt) :=
    get_commitment_stake_count ctxt rollup new_lcc in
  let? '_ :=
    Error_monad.fail_when (total_staker_count i32 new_lcc_stake_count)
      (Build_extensible "Sc_rollup_disputed" unit tt) in
  let? '(ctxt, new_lcc_added) :=
    Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      (ctxt, rollup) new_lcc in
  let? '_ :=
    let current_level := (Raw_context.current_level ctxt).(Level_repr.t.level)
      in
    let? min_level :=
      Raw_level_repr.add new_lcc_added refutation_deadline_blocks in
    Error_monad.fail_when (Raw_level_repr.op_lt current_level min_level)
      (Build_extensible "Sc_rollup_commitment_too_recent"
        Sc_rollup_errors.Sc_rollup_commitment_too_recent
        {|
          Sc_rollup_errors.Sc_rollup_commitment_too_recent.current_level :=
            current_level;
          Sc_rollup_errors.Sc_rollup_commitment_too_recent.min_level :=
            min_level; |}) in
  let? '(ctxt, lcc_size_diff) :=
    Store.Last_cemented_commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
      ctxt rollup new_lcc in
  if lcc_size_diff =i 0 then
    let? ctxt := deallocate_commitment_metadata ctxt rollup old_lcc in
    let num_commitments_to_keep :=
      (Raw_context.constants ctxt).(Constants_parametric_repr.t.sc_rollup).(Constants_parametric_repr.sc_rollup.max_number_of_stored_cemented_commitments)
      -i 1 in
    let? '(commitment_to_deallocate, ctxt) :=
      find_commitment_to_deallocate ctxt rollup old_lcc num_commitments_to_keep
      in
    match commitment_to_deallocate with
    | Nonereturn? (ctxt, new_lcc_commitment)
    | Some old_lcc
      Error_monad.Lwt_tzresult_syntax.op_letplus
        (deallocate_commitment ctxt rollup old_lcc)
        (fun ctxt(ctxt, new_lcc_commitment))
    end
  else
    Error_monad.error_value (Build_extensible "Asserted" unit tt).

#[bypass_check(guard)]
Definition remove_staker
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash)
  : M? (Raw_context.t × Receipt_repr.balance_updates) :=
  let? '(lcc, ctxt) := Commitment_storage.last_cemented_commitment ctxt rollup
    in
  let? '(ctxt, res) :=
    Store.Stakers.(Storage_sigs.Indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match res with
  | None
    Error_monad.Lwt_tzresult_syntax.fail
      (Build_extensible "Sc_rollup_not_staked" unit tt)
  | Some staked_on
    let? '_ :=
      Error_monad.fail_when (Commitment_hash.op_eq staked_on lcc)
        (Build_extensible "Sc_rollup_remove_lcc" unit tt) in
    let '(staker_contract, stake) := get_contract_and_stake ctxt staker in
    let bond_id := Bond_id_repr.Sc_rollup_bond_id rollup in
    let? '(ctxt, balance_updates) :=
      Token.transfer None ctxt
        (Token.Source_container (Token.Frozen_bonds staker_contract bond_id))
        (Token.Sink_infinite Token.Sc_rollup_refutation_punishments) stake in
    let? '(ctxt, _size_diff) :=
      Store.Stakers.(Storage_sigs.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 : Commitment_hash.t) (ctxt : Raw_context.t)
      {struct node_value} : M? Raw_context.t :=
      if Commitment_hash.op_eq node_value lcc then
        return? ctxt
      else
        let? '(pred, ctxt) :=
          Commitment_storage.get_predecessor_unsafe ctxt rollup node_value in
        let? ctxt := decrease_commitment_stake_count ctxt rollup node_value in
        go pred ctxt in
    Error_monad.Lwt_tzresult_syntax.op_letplus (go staked_on ctxt)
      (fun ctxt(ctxt, balance_updates))
  end.