chore: assert that an ingress induction debit implies a paused execution - #11273
Draft
mraszyk wants to merge 1 commit into
Draft
chore: assert that an ingress induction debit implies a paused execution#11273mraszyk wants to merge 1 commit into
mraszyk wants to merge 1 commit into
Conversation
The guarantee that a pending `ingress_induction_cycles_debit` is always applied rests on an invariant that was documented nowhere and asserted nowhere: the debit only ever becomes positive while the canister has a paused execution or paused install code, because that is the only case in which `charge_ingress_induction_cost()` postpones the charge. That invariant is what makes the debit bounded in time: a canister with a pending debit is not `is_cold()`, so it stays in the hot pool and `abort_all_paused_executions()` is bound to apply the debit at the latest in the checkpoint round at the end of the current checkpoint interval, whether or not the paused execution completes on its own. Check the invariant in `SystemState::check_invariants()`, spell out the precondition on `add_postponed_charge_to_ingress_induction_cycles_debit()` and note in `must_be_in_schedule()` why it needs no condition for the debit. Also move `has_paused_execution_or_install_code()` to `SystemState`, which owns both the debit and the task queue, and delegate to it from `CanisterState`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
There was a problem hiding this comment.
Pull request overview
Adds an invariant linking pending ingress induction debits to paused executions.
Changes:
- Moves the paused-execution helper to
SystemState. - Adds invariant validation and documentation.
- Adds a regression test.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
canister_state/tests.rs |
Tests the new invariant. |
canister_state/system_state.rs |
Adds helper, precondition, and invariant check. |
canister_state.rs |
Delegates helper and documents scheduling behavior. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Comment on lines
+2319
to
+2326
| // A pending ingress induction cycles debit is only ever accumulated while the | ||
| // canister has a paused execution (see | ||
| // `add_postponed_charge_to_ingress_induction_cycles_debit()`) and is applied | ||
| // when that execution finishes or is aborted. This is what guarantees that the | ||
| // debit is always applied: `CanisterState::is_cold()` keeps a canister with a | ||
| // pending debit in the hot pool, so `abort_all_paused_executions()` is bound to | ||
| // apply the debit at the latest in the checkpoint round at the end of the | ||
| // current checkpoint interval. |
Comment on lines
+864
to
+865
| // A pending debit without a paused execution breaks the invariant: nothing would | ||
| // be bound to apply the debit. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The guarantee that a pending
ingress_induction_cycles_debitis always applied rests on an invariant that was documented nowhere and asserted nowhere: the debit only ever becomes positive while the canister has a paused execution or paused install code, because that is the only case in whichcharge_ingress_induction_cost()postpones the charge.That invariant is what makes the debit bounded in time: a canister with a pending debit is not
is_cold(), so it stays in the hot pool andabort_all_paused_executions()is bound to apply the debit at the latest in the checkpoint round at the end of the current checkpoint interval, whether or not the paused execution completes on its own.Check the invariant in
SystemState::check_invariants(), spell out the precondition onadd_postponed_charge_to_ingress_induction_cycles_debit()and note inmust_be_in_schedule()why it needs no condition for the debit. Also movehas_paused_execution_or_install_code()toSystemState, which owns both the debit and the task queue, and delegate to it fromCanisterState.