feat(scheduler): lease-free Job domain model with verified state machine

Justfile

@@ -79,3 +79,17 @@ _ci: _rust-quality _change-risk
 
 ci:
     nix develop --accept-flake-config -c just _ci
+
+# Run Kani proof harnesses (bounded model checking). Slow; a separate gate, not part of _ci.
+_verify:
+    cargo kani --tests
+
+verify:
+    nix develop --accept-flake-config -c just _verify
+
+# One-time Kani setup. A no-op inside the Nix dev shell (KANI_HOME is pre-staged); only needed when running cargo kani outside Nix.
+_kani-setup:
+    cargo kani setup
+
+kani-setup:
+    nix develop --accept-flake-config -c just _kani-setup

crates/invariant-scheduler/Cargo.toml

@@ -3,4 +3,14 @@ name = "invariant-scheduler"
 version = "0.1.0"
 edition = "2024"
 
+# `kani` is an externally-set cfg (only active when `cargo kani` drives the
+# build). Register it so the `unexpected_cfgs` lint recognizes `#[cfg(kani)]`
+# on the proof harness instead of flagging it as a typo, while still checking
+# every other cfg name.
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+
+[dev-dependencies]
+proptest = "1.11"
+
 [dependencies]

crates/invariant-scheduler/src/domain/error.rs

@@ -1,12 +1,24 @@
 use std::fmt;
 
+/// An error returned by a fallible domain operation.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum DomainError {
+    /// A [`JobId`](crate::domain::JobId) was constructed from an empty string.
     EmptyJobId,
+    /// A [`TargetRef`](crate::domain::TargetRef) was constructed from an empty string.
     EmptyTargetRef,
+    /// Advancing a [`SchedulerTime`](crate::domain::SchedulerTime) overflowed
+    /// the representable range.
     TimeOverflow,
+    /// Incrementing an [`AttemptNumber`](crate::domain::AttemptNumber) overflowed
+    /// `u32::MAX`.
     AttemptOverflow,
+    /// A transition was attempted on a job already in a terminal status.
     JobTerminal,
+    /// A transition was attempted that is not legal from the job's current
+    /// non-terminal status.
+    IllegalTransition,
+    /// The ready queue could not accept another job because it is at capacity.
     QueueFull,
 }
 
@@ -18,6 +30,7 @@ impl fmt::Display for DomainError {
             Self::TimeOverflow => "scheduler time overflow",
             Self::AttemptOverflow => "attempt number overflow",
             Self::JobTerminal => "job is terminal",
+            Self::IllegalTransition => "illegal job state transition",
             Self::QueueFull => "ready queue is full",
         };
         f.write_str(message)
@@ -38,6 +51,10 @@ mod tests {
             (DomainError::TimeOverflow, "scheduler time overflow"),
             (DomainError::AttemptOverflow, "attempt number overflow"),
             (DomainError::JobTerminal, "job is terminal"),
+            (
+                DomainError::IllegalTransition,
+                "illegal job state transition",
+            ),
             (DomainError::QueueFull, "ready queue is full"),
         ];