Skip to content
Merged
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
1 change: 1 addition & 0 deletions INVARIANTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,4 +34,5 @@ materialization, messaging, DING, or presence must preserve them.
| **Parked tasks are visible and individually recoverable** | A parked task is reported alongside an unmodified runtime observation as a complete known fault; only an unbelievable marker fails closed. Park markers and unpark requests share the exact canonical catalog-folder plus host ownership scope, and the projected recovery argv carries both axes, so same-host supervisors cannot see, delete, consume, or advertise recovery into each other's channels even for the same task ID. A projected park whose supervisor generation is gone is positively not parked. An explicit per-task unpark clears that task's park and spent budget so it is launchable again and stays recovered past `interval`, releases no other parked task, restarts no healthy peer, and restores the agent's derived DING. | `src/flapping.rs::unpark_restores_a_launchable_task_not_just_a_cleared_flag`; `src/flapping.rs::unpark_is_per_task_and_reports_whether_it_changed_anything`; `src/park.rs::same_host_supervisors_isolate_markers_and_requests_by_catalog`; `src/park.rs::a_marker_from_a_dead_supervisor_reads_as_not_parked`; `src/park.rs::published_parks_are_readable_and_clear_when_the_task_recovers`; `src/park.rs::an_unbelievable_marker_is_indeterminate_not_absent`; `src/park.rs::a_request_is_consumed_exactly_once`; `src/task_inventory.rs::a_parked_task_reports_its_fault_alongside_a_truthful_runtime_state`; `src/task_inventory.rs::an_unbelievable_park_marker_makes_the_envelope_incomplete`; `tests/task_inventory_cli.rs::projected_recovery_targets_its_exact_catalog_and_host_despite_ambient_defaults`; `tests/run.rs::an_operator_recovers_one_parked_task_without_disturbing_a_healthy_peer`; `tests/run.rs::an_unpark_request_for_a_task_that_is_not_parked_says_so` |
| **Tracked workspaces fail closed** | Materialization simulates content operations before writing and refuses a real change to any Git-tracked target. Byte-identical tracked, untracked, and non-Git targets retain useful behavior. | `tests/materialize.rs::every_content_directive_refuses_to_change_a_tracked_target_before_any_write`; `tests/materialize.rs::byte_identical_tracked_target_is_allowed_without_modification`; `tests/materialize.rs::untracked_and_non_git_targets_remain_materializable` |
| **Native flat root** | Without an authored override, catalog tasks, eval messaging, shell helpers, and DING all use the catalog itself as `ST_ROOT`; no nested bus directory is synthesized. | `src/eval_run.rs::bus_root_expands_st_root_else_defaults`; `tests/eval_run_e2e.rs::st2_eval_runs_a_benign_folder_to_a_pass_verdict`; `tests/pty.rs` |
| **Resource observation is state-first, atomic, and fenced** | ABI-3 periodic publication and demanded `Published` results reuse one bounded `Publication` payload and one host acceptance, digest, relevance, typed-fact, and catch-up core; the host never trusts a runtime digest or observation timestamp. Demand reaches only a resident runtime that explicitly declares `capability "demand"`. Every `Observe` carries a positive watermark and the exact owner, binding, and registration, and exactly one matching `Unchanged`, `Failed`, or `Published` atomic result closes it. One outstanding dispatch plus one latest trailing watermark coalesces bursts without losing in-flight arrivals. Backpressure retains queued demand, replacement fences stale output, restart and provider failure settle honestly, and client disconnect or wait expiry never cancels accepted work. | `tests/resource_profile_supervisor_e2e.rs::demand_observation_settlement_matrix_is_atomic_and_preserves_facts`; `tests/resource_profile_supervisor_e2e.rs::demand_observation_coalesces_and_fences_watermarks`; `tests/resource_profile_supervisor_e2e.rs::demand_observation_survives_restart_disconnect_and_denies_missing_capability`; `tests/resource_profile_supervisor_e2e.rs::observable_publication_reaches_builtin_resync_with_filter_catch_up_and_scope_isolation`; `tests/agent_resource.rs::refresh_cli_reports_exact_receipts_and_wait_expiry_keeps_the_request`; `src/resource_observe.rs::tests::receipt_evidence_shape_matches_atomic_results` |
| **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` |
Loading
Loading