Skip to content

Commit 9e77bf7

Browse files
fix: point resource-observation invariant at its real proofs (#483)
`tests/invariants.rs::qualified_proof_references_resolve` was RED on main: the **Resource observation is state-first, atomic, and fenced** row still named four tests that #411 replaced when it rewrote `tests/resource_profile_supervisor_e2e.rs` onto the WASIp2 providers. The guarantee is unchanged; only the proof references move to the tests that actually carry it today: - `demand_observation_settlement_matrix_is_atomic_and_preserves_facts`, `demand_observation_coalesces_and_fences_watermarks` and `demand_observation_survives_restart_disconnect_and_denies_missing_capability` collapsed into `production_demand_jobs_coalesce_queue_disconnect_and_fence_generation`; - `observable_publication_reaches_builtin_resync_with_filter_catch_up_and_scope_isolation` became `production_component_preserves_resync_filter_catch_up_and_scope_isolation`; - the backpressure and stable-snapshot halves of the row gain `durable_admission_retains_the_256_request_boundary_without_a_runtime` and `supervisor_spawns_vista_capability_and_preserves_stable_snapshot`, which already existed but were not cited. No row is dropped and no guarantee is weakened. agent-identity: dev3.direct.omp.43sz6ujq agent-persona: generalist agent-supervisor: unavailable agent-tool: OMP agent-tool-version: 18.1.7 agent-runtime: OMP 18.1.7 tooling-profile: dotfiles@39a19af
1 parent 1322692 commit 9e77bf7

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

INVARIANTS.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ materialization, messaging, DING, or presence must preserve them.
3737
| **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` |
3838
| **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` |
3939
| **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` |
40-
| **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` |
40+
| **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::production_demand_jobs_coalesce_queue_disconnect_and_fence_generation`; `tests/resource_profile_supervisor_e2e.rs::durable_admission_retains_the_256_request_boundary_without_a_runtime`; `tests/resource_profile_supervisor_e2e.rs::production_component_preserves_resync_filter_catch_up_and_scope_isolation`; `tests/resource_profile_supervisor_e2e.rs::supervisor_spawns_vista_capability_and_preserves_stable_snapshot`; `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` |
4141
| **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` |
4242
| **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.rs::reconcile_pass_completes_while_a_resync_publication_is_blocked`; `src/resync.rs::a_flush_never_hands_off_a_subscription_whose_publication_is_outstanding`; `src/resync.rs::deactivation_drops_only_that_recipients_queued_publication`; `src/resync.rs::a_refresh_drops_a_queued_publication_for_a_subscription_it_removed` |
4343
| **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.rs::a_not_running_recipient_parks_its_reservation_and_is_attempted_once`; `src/resync.rs::a_parked_reservation_re_arms_and_replays_when_its_recipient_runs_again`; `src/resync.rs::a_permanently_refused_reservation_is_dropped_and_not_recaptured`; `src/resync.rs::refusals_are_classified_by_what_could_admit_them_later` |

0 commit comments

Comments
 (0)