feat(scheduler): lease-free Job domain model with verified state machine - #14
Merged
Conversation
- Add JobId and TargetRef: non-empty newtypes with fallible constructors (reject empty -> EmptyJobId / EmptyTargetRef). TargetRef stays opaque (no Ord); JobId keeps Ord as the identity type. - Harden Priority/Deadline/ReadyAt: const fn constructors and accessors, #[must_use] getters. - Re-export JobId/TargetRef from the domain module. - Unit tests for every invariant: empty rejection, value round-trips, priority MIN/MAX/DEFAULT and ordering direction, JobId ordering (13 tests).
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (1)
📝 WalkthroughSummary by CodeRabbit
WalkthroughAdds typed job domain types (ids, priority/deadline/readiness, attempt counting, status, Job with six transitions), exhaustive unit/property tests and a Kani proof for retry atomicity, Cargo test/tooling config, hermetic Kani provisioning in Nix, and Just recipes to run/setup Kani inside the dev shell. ChangesJob domain model and formal verification
Sequence Diagram(s)sequenceDiagram
participant Caller
participant Job
participant AttemptNumber
participant Verification
Caller->>Job: retry()
Job->>AttemptNumber: checked_next()
AttemptNumber-->>Job: Ok(next) or Err(AttemptOverflow)
alt increment succeeds
Job->>Job: set attempt to next
Job->>Job: set status = Queued
Job-->>Caller: Ok(())
else overflow
Job-->>Caller: Err(AttemptOverflow)
end
Caller->>Verification: run tests and Kani proof
Verification->>Job: assert retry atomicity
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@crates/invariant-scheduler/src/domain/priority.rs`:
- Around line 55-70: Remove ordering derives from ReadyAt to enforce the "not an
ordering/sort key" invariant: edit the ReadyAt definition to drop PartialOrd and
Ord from the #[derive(...)] list so it only implements Debug, Clone, Copy,
PartialEq, Eq, Hash; then search for any code comparing ReadyAt values and
replace those comparisons to compare ReadyAt.time() (SchedulerTime) instead.
Ensure ReadyAt::new and ReadyAt::time() remain unchanged.
In `@flake.nix`:
- Around line 144-149: The kaniBundleHash map currently contains x86_64-darwin =
null which will cause kaniBundleHash.${system} to evaluate to null and make
downstream fetchurl fail; update the kaniBundleHash handling in the flake to
either (A) provide the real prefetched sha256 for x86_64-darwin if that platform
should be supported, or (B) replace the null entry with an explicit runtime
error for that key (e.g., throw an informative error when system ==
"x86_64-darwin") so evaluation fails with a clear message; locate the
kaniBundleHash definition and adjust the x86_64-darwin branch or the code that
uses kaniBundleHash.${system} accordingly.
In `@Justfile`:
- Around line 90-95: The comment above the kani-setup recipe is misleading
because with KANI_HOME set by the Nix dev shell the cargo kani setup step is
skipped; update the Justfile to either (A) change the comment for
_kani-setup/kani-setup to state that setup is a no-op under the hermetic
NIX/KANI_HOME dev shell (mention KANI_HOME and Nix dev shell behavior), or (B)
remove the kani-setup wrapper entirely if you want to avoid a no-op target,
leaving _kani-setup only for non-Nix usage; ensure references to the target
names _kani-setup and kani-setup remain accurate in any docs or CI that call
them.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 61485cb8-ed85-4ee6-a779-2806387f9990
⛔ Files ignored due to path filters (1)
Cargo.lockis excluded by!**/*.lock
📒 Files selected for processing (7)
Justfilecrates/invariant-scheduler/Cargo.tomlcrates/invariant-scheduler/src/domain/error.rscrates/invariant-scheduler/src/domain/job.rscrates/invariant-scheduler/src/domain/mod.rscrates/invariant-scheduler/src/domain/priority.rsflake.nix
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
crates/invariant-scheduler/src/domain/mod.rs (1)
12-17:⚠️ Potential issue | 🟠 Major | ⚡ Quick winKeep
timepublic or treat this as a breaking API change.Making
timeprivate removes theinvariant_scheduler::domain::time::SchedulerTimepath. The re-export keeps the type available, but downstream code using the old module path will stop compiling.♻️ Minimal compatibility fix
-mod time; +pub mod time;🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@crates/invariant-scheduler/src/domain/mod.rs` around lines 12 - 17, The change made `mod time;` private which breaks the downstream path invariant_scheduler::domain::time::SchedulerTime; restore compatibility by making the module public (i.e., export the time module) so existing code can still reference domain::time::SchedulerTime while keeping the existing pub use time::SchedulerTime in place; update the declaration for the time module (related symbol: time and the re-export SchedulerTime) to be exported rather than private.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@crates/invariant-scheduler/src/domain/job.rs`:
- Around line 65-76: The docstring for AttemptNumber is misleading: it describes
"how many times" a job has been attempted while AttemptNumber is a zero-based
ordinal that starts at AttemptNumber::zero() and is incremented on retry(); this
causes off-by-one confusion for callers. Update the docs on the AttemptNumber
type and its accessors (e.g., AttemptNumber::zero(), any raw/count accessor, and
the retry() method) to state that it is a zero-based attempt index/ordinal
(first attempt = 0) or provide a proper count accessor (e.g., attempts_count()
that returns ordinal + 1) and ensure any documentation at the other occurrence
(the methods referenced around the second mention) is corrected to match the
chosen semantics.
---
Outside diff comments:
In `@crates/invariant-scheduler/src/domain/mod.rs`:
- Around line 12-17: The change made `mod time;` private which breaks the
downstream path invariant_scheduler::domain::time::SchedulerTime; restore
compatibility by making the module public (i.e., export the time module) so
existing code can still reference domain::time::SchedulerTime while keeping the
existing pub use time::SchedulerTime in place; update the declaration for the
time module (related symbol: time and the re-export SchedulerTime) to be
exported rather than private.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 3a544691-6fa6-43f8-be9d-07233218b226
📒 Files selected for processing (6)
crates/invariant-scheduler/src/domain/error.rscrates/invariant-scheduler/src/domain/job.rscrates/invariant-scheduler/src/domain/mod.rscrates/invariant-scheduler/src/domain/priority.rscrates/invariant-scheduler/src/domain/time.rscrates/invariant-scheduler/src/lib.rs
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
1 participant
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.
Slice 1 of the local scheduler: the lease-free
Jobaggregate and its value objects.Priority/Deadline/ReadyAt,JobId/TargetRef/AttemptNumber.Jobentity +JobStatussix-state machine with guarded transitions and atomic retry.just verify/just kani-setuprecipes.