🦏 Sc_rollup_stake_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.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_result_syntax.tzfail
(Build_extensible "Sc_rollup_not_staked" unit tt)
| Some branch ⇒ return? (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_result_syntax.tzfail
(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).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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_result_syntax.tzfail
(Build_extensible "Sc_rollup_not_staked" unit tt)
| Some branch ⇒ return? (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_result_syntax.tzfail
(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_result_syntax.tzfail
(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_result_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.
(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_result_syntax.tzfail
(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_result_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.
(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.
[assert_commitment_is_not_past_curfew ctxt rollup inbox_level] will look in the
storage [Commitment_first_publication_level] for the level of the oldest commit for
[inbox_level] and if it is more than [sc_rollup_challenge_window_in_blocks]
ago it fails with [Sc_rollup_commitment_past_curfew]. Otherwise it adds the
respective storage (if it is not set) and returns the context.
Definition assert_commitment_is_not_past_curfew
(ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
(inbox_level : Raw_level_repr.t) : M? Raw_context.t :=
let refutation_deadline_blocks :=
Int32.of_int (Constants_storage.sc_rollup_challenge_window_in_blocks ctxt)
in
let current_level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
let? '(ctxt, oldest_commit) :=
Store.Commitment_first_publication_level.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(ctxt, rollup) inbox_level in
match oldest_commit with
| Some oldest_commit ⇒
if
(Raw_level_repr.diff_value current_level oldest_commit) >i32
refutation_deadline_blocks
then
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_commitment_past_curfew" unit tt)
else
return? ctxt
| None ⇒
let? '(ctxt, _diff, _existed) :=
Store.Commitment_first_publication_level.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, rollup) inbox_level current_level in
return? ctxt
end.
(ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
(inbox_level : Raw_level_repr.t) : M? Raw_context.t :=
let refutation_deadline_blocks :=
Int32.of_int (Constants_storage.sc_rollup_challenge_window_in_blocks ctxt)
in
let current_level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
let? '(ctxt, oldest_commit) :=
Store.Commitment_first_publication_level.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(ctxt, rollup) inbox_level in
match oldest_commit with
| Some oldest_commit ⇒
if
(Raw_level_repr.diff_value current_level oldest_commit) >i32
refutation_deadline_blocks
then
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_commitment_past_curfew" unit tt)
else
return? ctxt
| None ⇒
let? '(ctxt, _diff, _existed) :=
Store.Commitment_first_publication_level.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, rollup) inbox_level current_level in
return? ctxt
end.
Check invariants on [inbox_level], enforcing overallocation of storage,
regularity of block production and curfew.
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
assert_commitment_is_not_past_curfew ctxt rollup
commitment.(Sc_rollup_commitment_repr.V1.t.inbox_level).
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
| None ⇒ return? (None, ctxt)
| Some pred_hash ⇒ aux 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? '_ :=
Error_monad.fail_when
(Sc_rollup_repr.Number_of_ticks.op_eq
commitment.(Sc_rollup_commitment_repr.V1.t.number_of_ticks)
Sc_rollup_repr.Number_of_ticks.zero)
(Build_extensible "Sc_rollup_zero_tick_commitment" unit tt) in
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_on ⇒ return? (ctxt, nil, staked_on)
| None ⇒ deposit_stake ctxt rollup staker
end in
Error_monad.Lwt_result_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
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (lcc_size_diff =i 0) in
let? ctxt := deallocate_commitment_metadata ctxt rollup old_lcc in
let? '(ctxt, _freed_size) :=
Store.Commitment_first_publication_level.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing)
(ctxt, rollup)
new_lcc_commitment.(Sc_rollup_commitment_repr.V1.t.inbox_level) 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
| None ⇒ return? (ctxt, new_lcc_commitment)
| Some old_lcc ⇒
Error_monad.Lwt_result_syntax.op_letplus
(deallocate_commitment ctxt rollup old_lcc)
(fun ctxt ⇒ (ctxt, new_lcc_commitment))
end.
#[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_result_syntax.tzfail
(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_result_syntax.op_letplus (go staked_on ctxt)
(fun ctxt ⇒ (ctxt, balance_updates))
end.
(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
assert_commitment_is_not_past_curfew ctxt rollup
commitment.(Sc_rollup_commitment_repr.V1.t.inbox_level).
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
| None ⇒ return? (None, ctxt)
| Some pred_hash ⇒ aux 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? '_ :=
Error_monad.fail_when
(Sc_rollup_repr.Number_of_ticks.op_eq
commitment.(Sc_rollup_commitment_repr.V1.t.number_of_ticks)
Sc_rollup_repr.Number_of_ticks.zero)
(Build_extensible "Sc_rollup_zero_tick_commitment" unit tt) in
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_on ⇒ return? (ctxt, nil, staked_on)
| None ⇒ deposit_stake ctxt rollup staker
end in
Error_monad.Lwt_result_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
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (lcc_size_diff =i 0) in
let? ctxt := deallocate_commitment_metadata ctxt rollup old_lcc in
let? '(ctxt, _freed_size) :=
Store.Commitment_first_publication_level.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing)
(ctxt, rollup)
new_lcc_commitment.(Sc_rollup_commitment_repr.V1.t.inbox_level) 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
| None ⇒ return? (ctxt, new_lcc_commitment)
| Some old_lcc ⇒
Error_monad.Lwt_result_syntax.op_letplus
(deallocate_commitment ctxt rollup old_lcc)
(fun ctxt ⇒ (ctxt, new_lcc_commitment))
end.
#[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_result_syntax.tzfail
(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_result_syntax.op_letplus (go staked_on ctxt)
(fun ctxt ⇒ (ctxt, balance_updates))
end.