Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion INVARIANTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,6 @@ materialization, messaging, DING, or presence must preserve them.
| **Atomic resource proposal publication** | Every changed resource publication is one host-owned compare-and-swap fenced by binding generation, state revision, and prior carrier digest. A persistent cross-process lock admits at most one proposal from the same prior. The content-derived proposal ID binds the accepted carrier digest and semantic outbox envelope; the durable intent becomes eligible only with the exact canonical carrier, then folds into one authoritative catch-up state. A pre-carrier crash exposes old state, a post-carrier crash catches up on restart, and retry after a lost acknowledgement returns the durable receipt without another transition. Ordinary reconciliation fails closed on out-of-band divergence after a committed intent; only an explicit generation-advance recovery may re-adopt the canonical carrier or its absence while invalidating the old intent and fence. | `src/resource_profile.rs::tests::atomic_publication_fences_races_and_survives_crash_restarts`; `src/resource_profile.rs::tests::generation_advance_explicitly_recovers_diverged_or_missing_carrier` |
| **Pass progress is independent of publication** | A reconcile pass completes whether or not resync publication is making progress. Publication runs on its own thread, so a pass's per-seat watch-set handshakes never wait for a catalog lock, a stream lock, or a refused publication. One publication is outstanding per subscription at a time, and a queued publication is dropped when its subscription is deactivated or removed by a refresh, so nothing is published to a seat the pass has already decided receives no events. | `src/run/tests.rs::reconcile_pass_completes_while_a_resync_publication_is_blocked`; `src/resync/tests.rs::a_flush_never_hands_off_a_subscription_whose_publication_is_outstanding`; `src/resync/tests.rs::deactivation_drops_only_that_recipients_queued_publication`; `src/resync/tests.rs::a_refresh_drops_a_queued_publication_for_a_subscription_it_removed` |
| **Terminal refusals are classified, not retried** | A refused resync publication is classified by what could admit it later. A recipient that is declared but not running parks its reservation: it is attempted once, captures and schedules nothing while parked, and re-arms with its exact reserved bytes when a refresh carries that recipient again. An ambiguous recipient, a foreign owning host, and an undeclared stream are permanently refused: the reservation is dropped and the carrier baseline advances so the same transition is not re-captured. Everything else, including an absent declaration, stays retryable. | `src/resync/tests.rs::a_not_running_recipient_parks_its_reservation_and_is_attempted_once`; `src/resync/tests.rs::a_parked_reservation_re_arms_and_replays_when_its_recipient_runs_again`; `src/resync/tests.rs::a_permanently_refused_reservation_is_dropped_and_not_recaptured`; `src/resync/tests.rs::refusals_are_classified_by_what_could_admit_them_later` |
| **Unbindable session sockets fail at admission** | Host-scoped validation rejects a pty task whose session socket path would exceed the portable 104-byte `sun_path` bound, because `pty` refuses that bind and the task can then never spawn. The bound is derived from the pty root resolved for the selected host rather than a fixed identity length, only that host's pty tasks are judged against it, and the diagnostic names the resolved path and the byte overage. A park whose cause is that same unbindable path does not advise `st2 unpark`, which would relaunch into the identical failure. | `tests/validate.rs::an_unbindable_session_socket_path_is_rejected_at_admission`; `tests/validate.rs::another_hosts_long_identity_is_not_judged_against_this_hosts_pty_root`; `tests/validate.rs::a_long_exec_task_id_is_not_a_socket_path_issue`; `src/run/tests.rs::session_socket_overage_is_derived_from_the_resolved_root`; `tests/run.rs::a_structurally_unrecoverable_park_does_not_advise_unpark` |
| **Unbindable session sockets fail at admission** | Host-scoped validation rejects a pty task whose session socket path would exceed the portable 104-byte `sun_path` bound, because `pty` refuses that bind and the task can then never spawn. The bound comes from the pty root resolved for the RUNTIME catalog the caller names, never from the tree under inspection: publication admits a candidate through a disposable projection nested in the catalog, and measuring that tree charges every identity for the projection's own depth and refuses declarations whose real socket is bindable. Only a deliberately context-free validation omits the guard. It is not a fixed identity length either, only that host's pty tasks are judged, and the diagnostic names the resolved path and the byte overage. A park whose cause is that same unbindable path does not advise `st2 unpark`, which would relaunch into the identical failure. | `tests/agent_publish.rs::publication_judges_the_socket_bound_against_the_runtime_catalog_not_the_projection`; `tests/agent_publish.rs::publication_still_refuses_an_unbindable_canonical_socket_path`; `tests/validate.rs::an_unbindable_session_socket_path_is_rejected_at_admission`; `tests/validate.rs::another_hosts_long_identity_is_not_judged_against_this_hosts_pty_root`; `tests/validate.rs::a_long_exec_task_id_is_not_a_socket_path_issue`; `src/run/tests.rs::session_socket_overage_is_derived_from_the_resolved_root`; `tests/run.rs::a_structurally_unrecoverable_park_does_not_advise_unpark` |
| **Marker-matched declaration authority** | Every st2 write path that rewrites a declaration carrying `meta { managed-by "nix" }` admits it only from a caller asserting exactly the marker that declaration carries: the lifecycle verb and the compare-and-swap `agent publish` both refuse a mismatched marker, an unmarked subject, an unresolvable multi-marker declaration, and an empty or padded assertion before any write, while presentation, address, stream, and Resource authoring refuse a Nix-owned declaration outright. Publication reads that authority from the incumbent, so creating a declaration and republishing byte-identical bytes stay open — neither replaces bytes another writer owns. A marker-matched edit rewrites nothing but the lifecycle line and is admitted through the same full-catalog gate as a compare-and-swap publication of the same bytes, so it cannot commit a declaration the catalog would reject. | `src/agent_author.rs::marker_matched_lifecycle_authority_is_exact_and_source_preserving`; `src/agent_author.rs::marker_matched_retirement_refuses_a_candidate_admission_would_reject`; `tests/agent_desired_state.rs::cli_managed_by_authority_retires_a_projected_seat_and_refuses_every_inexact_claim`; `tests/agent_publish.rs::publication_honours_the_incumbent_ownership_marker`; `tests/agent_publish.rs::publication_refuses_an_unresolvable_owner_and_repairs_unreadable_bytes` |
| **Proof references resolve** | Every qualified test named in this table exists in its named source file, so stale invariant claims fail the suite instead of silently surviving a refactor. | `tests/invariants.rs::qualified_proof_references_resolve` |
20 changes: 14 additions & 6 deletions docs/vrs/spec.md
Original file line number Diff line number Diff line change
Expand Up @@ -418,12 +418,20 @@ Host-scoped validation rejects a pty task whose session socket path would exceed
portable `sun_path` bound. `pty` binds `<PTY_ROOT>/<session-id>.sock` and refuses a
bind over the limit, so such a task can never spawn and fails identically on every
reconcile pass, which also makes the pass result useless as a health signal for that
host. The bound is derived from the pty root resolved for the selected host, never a
fixed maximum identity length: the usable identity length is what remains of the limit
after that root. The portable 104-byte bound applies so a declaration admitted on Linux
does not fail on Darwin, and the diagnostic states the resolved path and the byte
overage so the author can shorten the identity rather than discover the failure as a
spawn error later.
host. The bound is derived from the pty root resolved for the RUNTIME catalog — the
one the supervisor will bind sockets from — and never from the tree under inspection,
which is frequently a different tree: publication admits a candidate through a
disposable projection nested in the catalog, transactions validate captures and stages,
and a retained catalog is addressed through a file-descriptor path that canonicalizes
back to the real one. A caller that knows where sockets will be bound supplies that
root; only a deliberately context-free validation omits the guard. Measuring the
inspected tree instead charges every identity for the depth of whichever temporary tree
is being validated and refuses declarations whose real socket is bindable. The bound is
never a fixed maximum identity length either: the usable identity length is what
remains of the limit after the runtime root. The portable 104-byte bound applies so a
declaration admitted on Linux does not fail on Darwin, and the diagnostic states the
resolved path and the byte overage so the author can shorten the identity rather than
discover the failure as a spawn error later.

A park notice whose cause is structurally unrecoverable says so instead of offering
`st2 unpark`, which would relaunch into the identical failure. The test is the same
Expand Down
9 changes: 8 additions & 1 deletion src/agent_author/declared_field.rs
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,14 @@ fn refuse_address_collision(
spec.address = requested.map(str::to_owned);
}
}
let report = crate::validate::validate_discovered(catalog_root, Some(this_host), &prospective);
// The prospective catalog is an in-memory edit of the live one, which is where sockets
// will be bound, so the live root is the runtime root.
let report = crate::validate::validate_discovered(
catalog_root,
Some(this_host),
crate::validate::RuntimeRoot::Catalog(catalog_root),
&prospective,
);
if !report
.issues
.iter()
Expand Down
25 changes: 19 additions & 6 deletions src/agent_publish.rs
Original file line number Diff line number Diff line change
Expand Up @@ -494,8 +494,12 @@ fn verify_published_spec(
observed_sha256 == expected_sha256 && observed == expected_bytes,
"published Agent Spec readback mismatch: expected sha256 {expected_sha256}, found {observed_sha256}"
);
crate::catalog_transaction::validate_full_catalog(catalog)
.context("published catalog fails locked core/catalog re-admission")?;
// The live catalog is validated in place, so it is its own runtime root.
crate::catalog_transaction::validate_full_catalog(
catalog,
crate::validate::RuntimeRoot::Catalog(catalog),
)
.context("published catalog fails locked core/catalog re-admission")?;
Ok(observed_sha256)
}

Expand Down Expand Up @@ -576,8 +580,13 @@ fn read_regular_optional(path: &Path) -> Result<Option<Vec<u8>>> {

fn validate_overlay(catalog: &Path, control: &Path, candidate: &Candidate) -> Result<()> {
let shadow = build_overlay(catalog, control, candidate)?;
crate::catalog_transaction::validate_full_catalog(shadow.path())
.context("candidate fails full-catalog validation")
// The shadow is a disposable projection nested under the catalog; sockets will be bound from
// the real catalog, so that is the runtime root the candidate must satisfy.
crate::catalog_transaction::validate_full_catalog(
shadow.path(),
crate::validate::RuntimeRoot::Catalog(catalog),
)
.context("candidate fails full-catalog validation")
}

fn build_overlay(
Expand Down Expand Up @@ -653,8 +662,12 @@ pub(crate) fn admit_declaration_rewrite(
.with_context(|| format!("create validation overlay {}", parent.display()))?;
}
fs::write(&target, bytes).context("write candidate into validation shadow")?;
crate::catalog_transaction::validate_full_catalog(shadow.path())
.context("candidate fails full-catalog validation")
// Another disposable projection: judge the candidate against the catalog that will run.
crate::catalog_transaction::validate_full_catalog(
shadow.path(),
crate::validate::RuntimeRoot::Catalog(&catalog),
)
.context("candidate fails full-catalog validation")
}

fn copy_filtered_catalog(
Expand Down
8 changes: 7 additions & 1 deletion src/catalog_graph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,13 @@ pub fn snapshot(root: &Path, this_host: &str) -> Result<CatalogGraph> {
let _lock = crate::CatalogLock::shared(&root)
.context("acquire shared catalog-authoring lock for catalog graph")?;
let found = crate::discover_strict(&root);
let report = crate::validate::validate_discovered(&root, Some(this_host), &found);
// The graph reads the live catalog in place, so the tree under inspection is the runtime root.
let report = crate::validate::validate_discovered(
&root,
Some(this_host),
crate::validate::RuntimeRoot::Catalog(&root),
&found,
);

let mut runtime_by_path: BTreeMap<PathBuf, Vec<crate::agents::AgentRow>> = BTreeMap::new();
for row in crate::agents::roster_from_discovered(&found, &root, this_host) {
Expand Down
27 changes: 18 additions & 9 deletions src/catalog_transaction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -398,7 +398,8 @@ pub fn diff(request: DiffRequest) -> Result<DiffResult> {
let before = project(&retained_catalog, ProjectionSource::Current, &catalog)?;
validate_projection_link_counts(&retained_catalog, &before, "live catalog")?;
validate_live_workspace_facts(&catalog, &before.workspace_dirs)?;
validate_full_catalog(&retained_catalog).context("validate live catalog for diff")?;
validate_full_catalog(&retained_catalog, crate::validate::RuntimeRoot::Catalog(&catalog))
.context("validate live catalog for diff")?;
anyhow::ensure!(
before.root_sha256 == request.expect_sha256,
"catalog diff precondition failed: expected root sha256 {}, found {}",
Expand All @@ -409,7 +410,8 @@ pub fn diff(request: DiffRequest) -> Result<DiffResult> {
let captured = tempfile::tempdir().context("create prepared diff capture root")?;
capture_prepared_catalog(&prepared, captured.path())?;
let after = project(captured.path(), ProjectionSource::Prepared, &catalog)?;
validate_full_catalog(captured.path()).context("validate prepared catalog for diff")?;
validate_full_catalog(captured.path(), crate::validate::RuntimeRoot::Catalog(&catalog))
.context("validate prepared catalog for diff")?;

let before_specs = canonical_semantic_specs(&retained_catalog)?;
let after_specs = canonical_semantic_specs(captured.path())?;
Expand Down Expand Up @@ -1297,7 +1299,7 @@ pub fn bootstrap(request: BootstrapRequest) -> Result<BootstrapResult> {

let admission = tempfile::tempdir().context("create prepared-catalog admission root")?;
materialize_projection(&desired, admission.path())?;
validate_full_catalog(admission.path())?;
validate_full_catalog(admission.path(), crate::validate::RuntimeRoot::Catalog(&catalog))?;
let desired_config = crate::catalog::load(admission.path())?;
validate_external_pty_root(
&catalog,
Expand Down Expand Up @@ -1337,7 +1339,7 @@ pub fn bootstrap(request: BootstrapRequest) -> Result<BootstrapResult> {
desired.root_sha256,
staged.root_sha256
);
validate_full_catalog(&stage)?;
validate_full_catalog(&stage, crate::validate::RuntimeRoot::Catalog(&catalog))?;
let lock = initialize_bootstrap_control(&stage)?;
sync_tree_dirs(&stage)?;
Ok(lock)
Expand Down Expand Up @@ -1405,7 +1407,7 @@ fn inspect_existing_bootstrap(
&catalog,
&desired.workspace_dirs,
)?;
validate_full_catalog(&retained_catalog)?;
validate_full_catalog(&retained_catalog, crate::validate::RuntimeRoot::Catalog(&catalog))?;
anyhow::ensure!(
current.root_sha256 == desired.root_sha256,
"catalog bootstrap target already exists with root sha256 {}, expected {}",
Expand Down Expand Up @@ -1616,7 +1618,7 @@ pub fn apply(request: ApplyRequest) -> Result<ApplyResult> {
// are mirrored as empty directories; their live content is never copied or hashed.
let admission = tempfile::tempdir().context("create prepared-catalog admission root")?;
materialize_projection(&desired, admission.path())?;
validate_full_catalog(admission.path())?;
validate_full_catalog(admission.path(), crate::validate::RuntimeRoot::Catalog(&catalog))?;
let desired_config = crate::catalog::load(admission.path())?;
validate_external_pty_root(
&catalog,
Expand Down Expand Up @@ -1728,7 +1730,8 @@ pub fn apply(request: ApplyRequest) -> Result<ApplyResult> {
staged.root_sha256,
verified.root_sha256
);
validate_full_catalog(&catalog).context("validate applied live catalog")?;
validate_full_catalog(&catalog, crate::validate::RuntimeRoot::Catalog(&catalog))
.context("validate applied live catalog")?;
sync_dir(&catalog)?;
generation.commit()?;
test_checkpoint("before-clear");
Expand All @@ -1755,7 +1758,13 @@ pub fn apply(request: ApplyRequest) -> Result<ApplyResult> {
}

/// Full structural and host-scoped validation for a complete prospective catalog.
pub(crate) fn validate_full_catalog(root: &Path) -> Result<()> {
///
/// `runtime` names the catalog whose resolved pty root bounds session sockets. It is a separate
/// argument because `root` is frequently NOT that catalog: admission validates a projection, diff
/// validates a capture, bootstrap validates a stage, and a retained live catalog is addressed
/// through a file-descriptor path. Reading the bound off `root` charged declarations for the depth
/// of whichever temporary tree happened to be under inspection.
pub(crate) fn validate_full_catalog(root: &Path, runtime: crate::validate::RuntimeRoot<'_>) -> Result<()> {
let found = crate::discover(root);
let mut hosts = BTreeSet::new();
for spec in &found.specs {
Expand All @@ -1775,7 +1784,7 @@ pub(crate) fn validate_full_catalog(root: &Path) -> Result<()> {
.map(format_issue),
);
for host in hosts {
let report = crate::validate::validate_for_host(root, &host);
let report = crate::validate::validate_for_host_at(root, &host, runtime);
errors.extend(
report
.issues
Expand Down
Loading
Loading