gate, verify: wire agent sessions into classification, rules, and models
commit
801d573gate, verify: wire agent sessions into classification, rules, and models
Namespace::AgentSession classifies refs/meta/agent-sessions/*; the gate binds it by genesis oid and keeps mutation owner-only (worker claim vocabulary is phase 2’s). ents-gate-rules gains session facts and a running-requires-parent-confirm denial rule with red tests; ents-verify gains a stateright lifecycle model whose properties are proven to have teeth against deliberately-broken variants.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Reviews
No reviews of this commit yet — record a verdict below.
Start a review
crates/kernel/ents-gate-rules/src/lib.rs
@@ -59,6 +59,20 @@
//! canonical infrastructure, which needs more trust than an ordinary
//! append).
//!
+//! A second rule grows the set again, for Phase 1b of
+//! `docs/agent-sessions-plan.adoc` (the agent-sessions plan)'s lifecycle
+//! invariants, restated over three new session-specific facts
+//! ([`session_running`], [`session_plan_hash`], [`session_confirm_hash`]):
+//!
+//! - [`running_violation`](GateRules::running_violation) — a commit whose
+//! agent-session meta status is `Running` must descend from a parent
+//! whose own tree recorded a confirm leaf binding that parent's
+//! plan-leaf hash; absent that parent, a session could reach `Running`
+//! without ever having been confirmed against the plan a worker is about
+//! to execute (`docs/agent-sessions-plan.adoc`'s Phase 1b: "a commit
+//! whose meta status is running requires a parent whose tree contains a
+//! confirm leaf binding that parent's plan-leaf hash").
+//!
//! Two invariants are deliberately *not* encoded here, the gap marked
//! rather than papered over:
//!
@@ -147,6 +161,20 @@
relation context(Oid, Oid);
/// Objects the repository already has, or that arrive in this pack.
relation object_exists(Oid);
+ /// A commit whose decoded agent-session meta status is `Running`
+ /// (`ents_forge::agent::Status::Running`,
+ /// `docs/agent-sessions-plan.adoc`'s Phase 1b) — the fact a real
+ /// extractor would derive from the commit's typed tree.
+ relation session_running(Oid);
+ /// (commit, plan-leaf content hash) — the agent session's plan-leaf
+ /// hash as recorded in this commit's own tree
+ /// (`AgentSession::plan_hash`), absent when the tree carries no plan
+ /// leaf.
+ relation session_plan_hash(Oid, Oid);
+ /// (commit, bound hash) — the plan-leaf hash this commit's own confirm
+ /// leaf binds (`AgentSession::confirm`), absent when the tree carries
+ /// no confirm leaf.
+ relation session_confirm_hash(Oid, Oid);
// ---- IDB: derived relations ----
@@ -183,6 +211,15 @@
relation admin_signed(Oid);
admin_signed(c.clone()) <-- signed_by(c, k), member(k, Role::Admin);
+ /// A `Running` commit whose immediate parent's own tree carries a
+ /// confirm leaf binding that same parent's plan-leaf hash — the parent
+ /// was `queued` the instant before the claim that produced this commit
+ /// (`docs/agent-sessions-plan.adoc`'s Phase 1b).
+ relation session_running_confirmed(Oid);
+ session_running_confirmed(c.clone()) <--
+ session_running(c), parent(c, p),
+ session_confirm_hash(p, h), session_plan_hash(p, h);
+
// ---- Denial rules: any row here rejects the transaction ----
/// Fast-forward-only: the new tip must descend from the old tip.
@@ -229,6 +266,14 @@
effect_admin_violation(r.clone(), c.clone()) <--
introduced(r, c), if r.starts_with("refs/meta/effects/"),
!admin_signed(c);
+
+ /// A commit whose agent-session meta status is `Running` must have a
+ /// parent whose own tree carries a confirm leaf binding that parent's
+ /// plan-leaf hash — otherwise the session reached `Running` without a
+ /// confirmed plan (`docs/agent-sessions-plan.adoc`'s Phase 1b).
+ relation running_violation(Ref, Oid);
+ running_violation(r.clone(), c.clone()) <--
+ introduced(r, c), session_running(c), !session_running_confirmed(c);
}
/// Facts for one proposed transaction. In the real system these would be
@@ -251,6 +296,12 @@
pub context: Vec<(Oid, Oid)>,
/// See [`GateRules::object_exists`].
pub object_exists: Vec<(Oid,)>,
+ /// See [`GateRules::session_running`].
+ pub session_running: Vec<(Oid,)>,
+ /// See [`GateRules::session_plan_hash`].
+ pub session_plan_hash: Vec<(Oid, Oid)>,
+ /// See [`GateRules::session_confirm_hash`].
+ pub session_confirm_hash: Vec<(Oid, Oid)>,
}
/// Run every denial rule to a fixpoint over `facts`. An empty result means
@@ -266,6 +317,9 @@
anchor: facts.anchor,
context: facts.context,
object_exists: facts.object_exists,
+ session_running: facts.session_running,
+ session_plan_hash: facts.session_plan_hash,
+ session_confirm_hash: facts.session_confirm_hash,
..GateRules::default()
};
rules.run();
@@ -296,6 +350,12 @@
"effect-admin: {r}: {c} not signed by an admin-registered member"
));
}
+ for (r, c) in &rules.running_violation {
+ out.push(format!(
+ "session-running: {r}: {c}'s session status is Running but no parent's confirm \
+ leaf binds that parent's plan-leaf hash"
+ ));
+ }
out.sort();
out
}
@@ -307,6 +367,7 @@
const ISSUE: &str = "refs/meta/issues/g";
const COMMENT: &str = "refs/meta/comments/g2";
const EFFECT: &str = "refs/meta/effects/ci";
+ const AGENT_SESSION: &str = "refs/meta/agent-sessions/g";
fn base() -> Facts {
Facts {
@@ -439,4 +500,65 @@
assert!(v.iter().any(|m| m.starts_with("effect-admin:")), "{v:?}");
assert!(!v.iter().any(|m| m.starts_with("signature:")), "{v:?}");
}
+
+ // ---- Agent-session lifecycle: `running_violation` ----
+ // (`docs/agent-sessions-plan.adoc`'s Phase 1b).
+
+ /// RED: `c1` claims the session (its status decodes as `Running`), but
+ /// its parent `g`'s tree carries no confirm leaf at all — `g` was never
+ /// queued, so the claim should never have been admitted.
+ #[test]
+ fn a_claim_whose_parent_was_never_confirmed_is_rejected() {
+ let mut f = base();
+ f.ref_update = vec![(AGENT_SESSION.into(), Some("g".into()), "c1".into())];
+ f.parent = vec![("c1".into(), "g".into())];
+ f.signed_by = vec![("c1".into(), "key:joey".into())];
+ f.session_running = vec![("c1".into(),)];
+ f.session_plan_hash = vec![("g".into(), "hash:plan-a".into())];
+ // No session_confirm_hash at all: `g` is awaiting confirmation, not
+ // queued.
+ let v = gate(f);
+ assert!(
+ v.iter()
+ .any(|m| m.starts_with("session-running:") && m.contains("c1")),
+ "{v:?}"
+ );
+ }
+
+ /// RED (the stale-confirm variant): `g`'s confirm leaf binds an older
+ /// plan hash than the one `g`'s own plan leaf now carries — a revision
+ /// that should have dropped the confirm, per
+ /// `ents_forge::agent::command::revise_plan`'s contract, evidently did
+ /// not. The claim built on top of it is still rejected.
+ #[test]
+ fn a_claim_whose_parent_confirm_binds_a_stale_plan_hash_is_rejected() {
+ let mut f = base();
+ f.ref_update = vec![(AGENT_SESSION.into(), Some("g".into()), "c1".into())];
+ f.parent = vec![("c1".into(), "g".into())];
+ f.signed_by = vec![("c1".into(), "key:joey".into())];
+ f.session_running = vec![("c1".into(),)];
+ f.session_plan_hash = vec![("g".into(), "hash:plan-b".into())];
+ f.session_confirm_hash = vec![("g".into(), "hash:plan-a".into())];
+ let v = gate(f);
+ assert!(
+ v.iter()
+ .any(|m| m.starts_with("session-running:") && m.contains("c1")),
+ "{v:?}"
+ );
+ }
+
+ /// GREEN: `c1` claims a session whose parent `g` was queued — `g`'s
+ /// confirm leaf binds exactly `g`'s own plan-leaf hash. The rule's
+ /// relation is empty; nothing else in the base fixture fires either.
+ #[test]
+ fn a_claim_whose_parent_was_confirmed_against_its_own_plan_passes() {
+ let mut f = base();
+ f.ref_update = vec![(AGENT_SESSION.into(), Some("g".into()), "c1".into())];
+ f.parent = vec![("c1".into(), "g".into())];
+ f.signed_by = vec![("c1".into(), "key:joey".into())];
+ f.session_running = vec![("c1".into(),)];
+ f.session_plan_hash = vec![("g".into(), "hash:plan-a".into())];
+ f.session_confirm_hash = vec![("g".into(), "hash:plan-a".into())];
+ assert!(gate(f).is_empty());
+ }
}
crates/kernel/ents-gate/src/verify.rs
@@ -611,7 +611,14 @@
Namespace::Effect | Namespace::Toolchain => {
bind_natural_key(objects, name, commit.tree, "name", &final_segment(name))
}
- Namespace::Comment | Namespace::Issue => bind_hash_identified(objects, name, new),
+ // An agent session is hash-identified exactly like a comment or an
+ // issue: the refname's final segment must be the genesis oid, and
+ // the all-roots walk must find no doppelgänger
+ // (`docs/agent-sessions-plan.adoc`'s Phase 1b, `meta-ref.
+ // identity-binding`).
+ Namespace::Comment | Namespace::Issue | Namespace::AgentSession => {
+ bind_hash_identified(objects, name, new)
+ }
Namespace::Review => {
let Some((target, member)) = namespace::parse_review_ref(name.as_ref()) else {
return Ok(binding_refusal(
@@ -802,7 +809,16 @@
};
let is_admin = signer.provenance == Provenance::AdminRegistered;
match namespace {
- Namespace::Comment | Namespace::Issue => {
+ // An agent session's mutation owner is exactly its genesis signer
+ // (∪ admins), the same rule a comment or issue advances under —
+ // Phase 1b keeps this owner-only rather than inventing a
+ // worker-may-advance-status carve-out: `ents-gate`'s vocabulary has
+ // no notion of "a claim, once made, authorizes a different signer"
+ // to express that safely, so a worker's status-advance commits stay
+ // Phase 2's concern (`docs/agent-sessions-plan.adoc` Phase 2's
+ // claim-via-CAS), landed by the session's own member or an admin
+ // acting on their behalf until that machinery exists.
+ Namespace::Comment | Namespace::Issue | Namespace::AgentSession => {
// Creation is provenance-keyed; only an advance is owner-keyed.
if old.is_none() {
return Ok(None);
crates/kernel/ents-gate/tests/gate.rs
@@ -87,6 +87,13 @@
name(&format!("refs/meta/issues/{genesis}"))
}
+/// The oid-keyed refname of an agent session whose genesis is `genesis` —
+/// hash-identified exactly like [`issue_ref`] (`docs/agent-sessions-plan.
+/// adoc`'s Phase 1b).
+fn agent_session_ref(genesis: ObjectId) -> FullName {
+ name(&format!("refs/meta/agent-sessions/{genesis}"))
+}
+
/// A signed empty-tree commit — a generic meta-mutation body. A
/// hash-identified entity binds by its genesis oid and the all-roots
/// walk, not by tree content, so an empty tree exercises the tip
@@ -525,6 +532,39 @@
);
}
+#[rstest]
+// @relation(gate.identity-binding, meta-ref.identity-binding, scope=function, role=Verifies)
+fn an_agent_session_binds_by_its_genesis_oid_like_other_hash_identified_entities() {
+ // Phase 1b: refs/meta/agent-sessions/* binds exactly like
+ // refs/meta/issues/* and refs/meta/comments/* — genesis oid plus the
+ // all-roots walk, no natural-key tree field involved.
+ let f = forge();
+ let genesis = commit(&f, vec![], Some(&f.admin), 300);
+ expect_pass(
+ &run(&f, &agent_session_ref(genesis), Some(genesis)),
+ AdmissionKind::TipInvariant,
+ );
+
+ let advance = commit(&f, vec![genesis], Some(&f.admin), 310);
+ let refname = agent_session_ref(genesis);
+ f.refs.set(refname.as_ref(), genesis);
+ expect_pass(
+ &run(&f, &refname, Some(advance)),
+ AdmissionKind::TipInvariant,
+ );
+
+ // A refname whose segment is not the tip's own genesis is refused, the
+ // same doppelgänger check `a_refname_not_naming_the_genesis_oid_is_refused`
+ // exercises for issues.
+ let wrong = agent_session_ref(
+ ObjectId::from_hex(b"00000000000000000000000000000000deadbeef").expect("hex"),
+ );
+ expect_fail(
+ &run(&f, &wrong, Some(genesis)),
+ Requirement::IdentityBinding,
+ );
+}
+
#[rstest]
// @relation(gate.identity-binding, model.review-pin, scope=function, role=Verifies)
fn a_pin_is_never_subjected_to_the_all_roots_walk() {
@@ -752,6 +792,49 @@
expect_fail(&verdict, Requirement::TipSigned);
}
+#[rstest]
+// @relation(gate.owner-mutation, scope=function, role=Verifies)
+fn an_admin_may_advance_another_members_agent_session() {
+ // Same owner-mutation rule as a comment's: the genesis signer or an
+ // admin-registered member may advance an agent session (Phase 1b keeps
+ // this owner-only — see `owner_mutation`'s doc on why a worker's
+ // status-advance is deliberately not modeled here yet).
+ let f = forge();
+ let second = Keypair::from_seed(OUTSIDER_SEED);
+ enroll_member(
+ &f.refs,
+ &f.objects,
+ "second",
+ &second,
+ Provenance::AdminRegistered,
+ 210,
+ );
+
+ let genesis = commit(&f, vec![], Some(&f.admin), 300);
+ let refname = agent_session_ref(genesis);
+ f.refs.set(refname.as_ref(), genesis);
+ let advance = commit(&f, vec![genesis], Some(&second), 310);
+ expect_pass(
+ &run(&f, &refname, Some(advance)),
+ AdmissionKind::TipInvariant,
+ );
+}
+
+#[rstest]
+// @relation(gate.owner-mutation, model.member-provenance, scope=function, role=Verifies)
+fn a_self_attested_non_owner_cannot_advance_an_agent_session() {
+ // Mirrors `a_self_attested_non_owner_cannot_advance_a_comment`: a
+ // self-attested member is not authorized for canonical refs at all
+ // (creation stays provenance-keyed, routed to the inbox), so it cannot
+ // advance someone else's agent session either.
+ let f = forge();
+ let genesis = commit(&f, vec![], Some(&f.admin), 300);
+ let refname = agent_session_ref(genesis);
+ f.refs.set(refname.as_ref(), genesis);
+ let advance = commit(&f, vec![genesis], Some(&f.guest), 310);
+ expect_fail(&run(&f, &refname, Some(advance)), Requirement::TipSigned);
+}
+
#[rstest]
// @relation(gate.owner-mutation, model.review, scope=function, role=Verifies)
fn the_wrong_member_cannot_advance_a_review() {
crates/kernel/ents-model/src/namespace.rs
@@ -69,13 +69,14 @@
/// extracts `id` from the proposed ref the same way `ents-forge`'s own
/// `genesis_id` does for a comment or issue.
///
-/// [`classify`] deliberately has no `agent-sessions` arm yet: an unrecognized
-/// segment falls through to [`Namespace::Unknown`], which is exactly what
-/// `model.extensibility` asks of a namespace no gate-level vocabulary
-/// interprets. Phase 1 of `docs/agent-sessions-plan.adoc` stops at this
-/// builder; classifying the namespace for `ents-gate`'s identity-binding and
-/// owner-mutation checks is Phase 1b's job, alongside the still-unwritten
-/// `meta-ref.adoc` namespace entry and `model.agent-session` section.
+/// [`classify`] routes this namespace to [`Namespace::AgentSession`]
+/// (`docs/agent-sessions-plan.adoc`'s Phase 1b), which `ents-gate`'s
+/// identity-binding and owner-mutation checks treat exactly like
+/// [`Namespace::Comment`] and [`Namespace::Issue`]: hash-identified by the
+/// genesis oid, mutable only by the genesis signer or an admin. The
+/// still-unwritten `meta-ref.adoc` namespace entry and `model.agent-session`
+/// section remain owner spec text (`docs/agent-sessions-plan.adoc`'s "Owner
+/// spec text needed").
pub fn agent_session_ref(id: &str) -> Result<FullName> {
build(format!("refs/meta/agent-sessions/{id}"))
}
@@ -382,6 +383,11 @@
Issue,
/// `refs/meta/comments/*`.
Comment,
+ /// `refs/meta/agent-sessions/*` — hash-identified by the session's own
+ /// genesis commit oid, the same shape as [`Namespace::Comment`] and
+ /// [`Namespace::Issue`] (`docs/agent-sessions-plan.adoc`'s Phase 1
+ /// [`agent_session_ref`], Phase 1b for this classification).
+ AgentSession,
/// `refs/meta/reviews/*`.
Review,
/// `refs/meta/pins/*` — retention pins (`model.review-pin`,
@@ -463,6 +469,7 @@
"member" => Some(Namespace::Member),
"issues" => Some(Namespace::Issue),
"comments" => Some(Namespace::Comment),
+ "agent-sessions" => Some(Namespace::AgentSession),
"reviews" => Some(Namespace::Review),
"pins" => Some(Namespace::Pin),
"effects" => Some(Namespace::Effect),
@@ -536,13 +543,7 @@
#[case::outside_meta("refs/heads/main", None)]
#[case::unrecognized("refs/meta/index/abc", Some(Namespace::Unknown))]
#[case::novel_namespace("refs/meta/widgets/7", Some(Namespace::Unknown))]
- // Phase 1b, not Phase 1, teaches `classify` this segment
- // (`agent_session_ref`'s own doc); until then it is forge state this
- // vocabulary does not yet interpret, per `model.extensibility`.
- #[case::agent_session_namespace_not_yet_classified(
- "refs/meta/agent-sessions/deadbeef",
- Some(Namespace::Unknown)
- )]
+ #[case::agent_session("refs/meta/agent-sessions/deadbeef", Some(Namespace::AgentSession))]
// @relation(meta-ref.namespace, meta-ref.granularity, scope=function, role=Verifies)
fn classify_matches_the_namespace_table(
#[case] refname: &str,
crates/verify/ents-verify/src/lib.rs
@@ -26,6 +26,10 @@
//! exception to "skeleton, not solution").
//! - [`effects`] — Phase 4 skeleton: trigger/dedup/results state shape.
//! - [`durability`] — Phase 5 skeleton: crash/durability ordering.
+//! - [`agent_session`] — `docs/agent-sessions-plan.adoc` Phase 1b: a
+//! fully-built (not skeleton) model of the agent-session lifecycle —
+//! `planning ⇄ ready → running → done | failed` plus the confirm-binding
+//! derived predicates Phase 1's `ents_forge::agent` module establishes.
//!
//! # The bounded universe
//!
@@ -37,6 +41,7 @@
//! this small is what makes exhaustive search (Phase 0.5) and bounded
//! model checking (Phases 3-5) tractable at all.
+pub mod agent_session;
pub mod durability;
pub mod effects;
pub mod receive;
crates/verify/ents-verify/src/agent_session.rs
@@ -1,0 +1,345 @@
+//! The agent-session lifecycle model (`docs/agent-sessions-plan.adoc`
+//! Phase 1b), a [`stateright`] model over the derived-predicate lifecycle
+//! Phase 1's `ents_forge::agent` module establishes: `planning ⇄ ready →
+//! running → done | failed`, confirm as a plan-hash binding rather than a
+//! boolean, and `queued`/`awaiting confirmation` read off the tip snapshot.
+//!
+//! Unlike [`crate::receive`], [`crate::effects`], and [`crate::durability`]
+//! (Phase 3–5 skeletons, deliberately `todo!()` — filling them in is the
+//! human exercise), this model is filled in completely: Phase 1b's own
+//! acceptance criteria ask for a working model of the lifecycle, mirroring
+//! [`crate::search`]'s fully-built exhaustive search rather than a stub.
+//!
+//! # The bounded universe
+//!
+//! Two plan generations ([`PlanGen::A`], [`PlanGen::B`]) are enough to
+//! exercise every transition the lifecycle names, including the one the
+//! entity's own doc calls out by name: drafting `B` after confirming `A`
+//! invalidates the existing confirm even though nothing about `B` reuses
+//! `A`'s hash for anything (`ents_forge::agent::command::revise_plan`'s
+//! "never compares the new text's hash against the old confirm's before
+//! dropping it"). A third generation would grow the reachable state count
+//! without adding a new transition shape, the same scope discipline
+//! `crate::search`'s module doc explains for its own bound.
+
+use stateright::{Model, Property};
+
+/// A plan's content-hash identity, standing in for `AgentSession::plan_hash`'s
+/// real git blob hash — two distinct values are enough to exercise every
+/// transition (see the module's bounded-universe note).
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum PlanGen {
+ /// The first plan drafted.
+ A,
+ /// A later revision.
+ B,
+}
+
+/// Both plan generations in the bounded universe, in a fixed enumeration
+/// order.
+pub const PLAN_GENS: [PlanGen; 2] = [PlanGen::A, PlanGen::B];
+
+/// The durable lifecycle phase (`ents_forge::agent::Status`), minus
+/// `Status::Failed`'s carried `FailureReason` detail — irrelevant to the
+/// invariants this model checks and would only inflate the state space.
+#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
+pub enum Status {
+ /// No confirmed plan exists yet.
+ #[default]
+ Planning,
+ /// A plan leaf exists; [`State::queued`] further distinguishes whether
+ /// it is bound by a current confirm.
+ Ready,
+ /// A worker has claimed the session — the point of no return.
+ Running,
+ /// The run completed and its result landed.
+ Done,
+ /// The run could not complete, or was refused.
+ Failed,
+}
+
+/// One session's modeled tip: durable status, the current plan generation
+/// (`None` before a plan is ever drafted), and the generation a confirm
+/// leaf binds (`None` when absent). Mirrors `AgentSession`'s three
+/// tip-relevant fields exactly — `thread` and the rest of `SessionMeta`
+/// play no part in the lifecycle invariants this model checks.
+#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
+pub struct State {
+ /// The session's durable lifecycle phase.
+ pub status: Status,
+ /// The current plan's generation, or `None` before one is drafted.
+ pub plan: Option<PlanGen>,
+ /// The generation the current confirm leaf binds, or `None` when
+ /// absent.
+ pub confirm: Option<PlanGen>,
+}
+
+impl State {
+ /// `AgentSession::queued`: `Ready`, and the confirm binds the current
+ /// plan's generation exactly — restated over this model's [`State`]
+ /// rather than a decoded tree.
+ #[must_use]
+ pub fn queued(&self) -> bool {
+ self.status == Status::Ready && self.confirm.is_some() && self.confirm == self.plan
+ }
+}
+
+/// Session-lifecycle actions (`docs/agent-sessions-plan.adoc` Phase 1b):
+/// draft or revise the plan, confirm it, un-queue (drop confirm, the
+/// plan's resolved-by-default item 1), claim (the worker's point of no
+/// return), and finish.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum Action {
+ /// `git ents agent plan`: draft or redraft the plan to the given
+ /// generation, unconditionally dropping any existing confirm
+ /// (`ents_forge::agent::command::revise_plan`) — offered even when the
+ /// plan already carries this generation, mirroring that command's own
+ /// "a plan revision that happens to land on byte-identical text is a
+ /// degenerate case not worth special-casing".
+ DraftPlan(PlanGen),
+ /// `git ents agent confirm`: bind the confirm leaf to the current
+ /// plan's generation.
+ Confirm,
+ /// Un-queue (resolved-by-default item 1 of `docs/agent-sessions-plan.
+ /// adoc`): drop the confirm leaf, returning the session to `Planning`
+ /// — legal only before claim.
+ UnQueue,
+ /// The worker's claim: legal only when `Ready` and [`State::queued`].
+ Claim,
+ /// The run reaches a terminal state.
+ Finish(Terminal),
+}
+
+/// The two terminal outcomes a run can finish in.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum Terminal {
+ /// The run completed and its result landed.
+ Done,
+ /// The run could not complete, or was refused.
+ Failed,
+}
+
+/// The Phase 1b lifecycle model.
+pub struct AgentSessionModel;
+
+impl Model for AgentSessionModel {
+ type State = State;
+ type Action = Action;
+
+ fn init_states(&self) -> Vec<Self::State> {
+ vec![State::default()]
+ }
+
+ fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) {
+ match state.status {
+ Status::Planning | Status::Ready => {
+ actions.extend(PLAN_GENS.iter().map(|g| Action::DraftPlan(*g)));
+ if state.status == Status::Ready && state.plan.is_some() {
+ actions.push(Action::Confirm);
+ }
+ if state.status == Status::Ready && state.confirm.is_some() {
+ actions.push(Action::UnQueue);
+ }
+ if state.queued() {
+ actions.push(Action::Claim);
+ }
+ }
+ Status::Running => {
+ actions.push(Action::Finish(Terminal::Done));
+ actions.push(Action::Finish(Terminal::Failed));
+ }
+ // Terminal states absorb: no action ever leaves them.
+ Status::Done | Status::Failed => {}
+ }
+ }
+
+ fn next_state(&self, last_state: &Self::State, action: Self::Action) -> Option<Self::State> {
+ let mut state = last_state.clone();
+ match action {
+ Action::DraftPlan(plan_gen)
+ if matches!(state.status, Status::Planning | Status::Ready) =>
+ {
+ state.plan = Some(plan_gen);
+ state.confirm = None;
+ state.status = Status::Ready;
+ }
+ Action::Confirm if state.status == Status::Ready && state.plan.is_some() => {
+ state.confirm = state.plan;
+ }
+ Action::UnQueue if state.status == Status::Ready && state.confirm.is_some() => {
+ state.confirm = None;
+ state.status = Status::Planning;
+ }
+ Action::Claim if state.queued() => {
+ state.status = Status::Running;
+ }
+ Action::Finish(terminal) if state.status == Status::Running => {
+ state.status = match terminal {
+ Terminal::Done => Status::Done,
+ Terminal::Failed => Status::Failed,
+ };
+ }
+ _ => return None,
+ }
+ Some(state)
+ }
+
+ fn properties(&self) -> Vec<Property<Self>> {
+ vec![
+ // "Running is unreachable without a confirm binding the
+ // then-current plan": since neither Claim nor Finish touch
+ // `plan`/`confirm`, and Claim's own guard is `queued()`, this
+ // holds throughout every state Running is ever observed in,
+ // not only at the instant of the claim.
+ Property::always("running_requires_confirmed_plan", |_, s: &State| {
+ s.status != Status::Running || (s.confirm.is_some() && s.confirm == s.plan)
+ }),
+ // "Plan revision invalidates prior confirm": no reachable
+ // state ever carries a confirm bound to a generation other
+ // than the current plan — `DraftPlan` drops it
+ // unconditionally, so a stale binding never survives a
+ // revision.
+ Property::always("confirm_never_binds_a_stale_plan", |_, s: &State| {
+ s.confirm.is_none() || s.confirm == s.plan
+ }),
+ // "Terminal states absorb": `Done` and `Failed` offer no
+ // action at all.
+ Property::always("terminal_states_absorb", |model, s: &State| {
+ if matches!(s.status, Status::Done | Status::Failed) {
+ let mut actions = Vec::new();
+ model.actions(s, &mut actions);
+ actions.is_empty()
+ } else {
+ true
+ }
+ }),
+ ]
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use stateright::Checker;
+
+ use super::*;
+
+ /// The lifecycle model, run to exhaustion, satisfies every property
+ /// this module states — the properties are believed sound, unlike
+ /// `crate::search`'s one deliberately-open ledger gap.
+ #[test]
+ fn lifecycle_satisfies_every_invariant() {
+ let checker = AgentSessionModel.checker().spawn_bfs().join();
+ checker.assert_no_discovery("running_requires_confirmed_plan");
+ checker.assert_no_discovery("confirm_never_binds_a_stale_plan");
+ checker.assert_no_discovery("terminal_states_absorb");
+ }
+
+ /// A deliberately broken variant of [`AgentSessionModel`]: `Claim` is
+ /// enabled whenever the session is merely `Ready`, without requiring
+ /// [`State::queued`]. Proves `running_requires_confirmed_plan` has
+ /// teeth — remove the real guard and the checker finds the witness.
+ struct ClaimWithoutConfirmGuard;
+
+ impl Model for ClaimWithoutConfirmGuard {
+ type State = State;
+ type Action = Action;
+
+ fn init_states(&self) -> Vec<Self::State> {
+ AgentSessionModel.init_states()
+ }
+
+ fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) {
+ AgentSessionModel.actions(state, actions);
+ if state.status == Status::Ready && !state.queued() {
+ actions.push(Action::Claim);
+ }
+ }
+
+ fn next_state(
+ &self,
+ last_state: &Self::State,
+ action: Self::Action,
+ ) -> Option<Self::State> {
+ if action == Action::Claim && last_state.status == Status::Ready {
+ let mut state = last_state.clone();
+ state.status = Status::Running;
+ return Some(state);
+ }
+ AgentSessionModel.next_state(last_state, action)
+ }
+
+ fn properties(&self) -> Vec<Property<Self>> {
+ vec![Property::always(
+ "running_requires_confirmed_plan",
+ |_, s: &State| {
+ s.status != Status::Running || (s.confirm.is_some() && s.confirm == s.plan)
+ },
+ )]
+ }
+ }
+
+ #[test]
+ fn the_claim_confirm_guard_is_load_bearing() {
+ let checker = ClaimWithoutConfirmGuard.checker().spawn_bfs().join();
+ let path = checker.assert_any_discovery("running_requires_confirmed_plan");
+ println!(
+ "running_requires_confirmed_plan witness (unguarded claim): {:?}",
+ path.into_actions()
+ );
+ }
+
+ /// A second deliberately broken variant: `DraftPlan` no longer drops
+ /// the existing confirm. Proves `confirm_never_binds_a_stale_plan` has
+ /// teeth — the real `DraftPlan` always drops confirm unconditionally
+ /// (`ents_forge::agent::command::revise_plan`'s own contract); remove
+ /// that and the checker finds a state where a confirm outlives the
+ /// plan hash it bound.
+ struct ReviseWithoutDroppingConfirm;
+
+ impl Model for ReviseWithoutDroppingConfirm {
+ type State = State;
+ type Action = Action;
+
+ fn init_states(&self) -> Vec<Self::State> {
+ AgentSessionModel.init_states()
+ }
+
+ fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) {
+ AgentSessionModel.actions(state, actions);
+ }
+
+ fn next_state(
+ &self,
+ last_state: &Self::State,
+ action: Self::Action,
+ ) -> Option<Self::State> {
+ if let Action::DraftPlan(plan_gen) = action
+ && matches!(last_state.status, Status::Planning | Status::Ready)
+ {
+ let mut state = last_state.clone();
+ state.plan = Some(plan_gen);
+ // Bug: the confirm leaf is left untouched.
+ state.status = Status::Ready;
+ return Some(state);
+ }
+ AgentSessionModel.next_state(last_state, action)
+ }
+
+ fn properties(&self) -> Vec<Property<Self>> {
+ vec![Property::always(
+ "confirm_never_binds_a_stale_plan",
+ |_, s: &State| s.confirm.is_none() || s.confirm == s.plan,
+ )]
+ }
+ }
+
+ #[test]
+ fn the_revise_drops_confirm_guard_is_load_bearing() {
+ let checker = ReviseWithoutDroppingConfirm.checker().spawn_bfs().join();
+ let path = checker.assert_any_discovery("confirm_never_binds_a_stale_plan");
+ println!(
+ "confirm_never_binds_a_stale_plan witness (revise without dropping confirm): {:?}",
+ path.into_actions()
+ );
+ }
+}