diff --git a/dag/gunbc/session_lease.dag b/dag/gunbc/session_lease.dag index 9821e7846da..2f97a23503a 100644 --- a/dag/gunbc/session_lease.dag +++ b/dag/gunbc/session_lease.dag @@ -42,10 +42,15 @@ type ProcessPortObservation | PortInaccessible | PortObservationRefused { reason: NonEmptyStr } +// A PLAN IS WHAT `Apply` EXECUTES, SO A REFUSAL IS NOT ONE. Refusing because a foreign +// process owns the port is a DECISION, and decision_for_process_port_verdict already +// answers it on the `Refuse` arm with the reason attached. Carrying a refusal here as +// well gave one fact two representations, and made `Apply { plan: RefuseForeignOwner }` +// -- execute the refusal -- a state every consumer had to answer for and no producer +// could reach. type ProcessLeasePlan = Start | DrainMatchingStaleThenStart - | RefuseForeignOwner fn classify_process_port( scope: ProcessPortScope, diff --git a/dag/test/claim/process_lease_plan_is_not_a_refusal_witness_test.dag b/dag/test/claim/process_lease_plan_is_not_a_refusal_witness_test.dag new file mode 100644 index 00000000000..dae6bb576c8 --- /dev/null +++ b/dag/test/claim/process_lease_plan_is_not_a_refusal_witness_test.dag @@ -0,0 +1,71 @@ +module test.claim.process_lease_plan_is_not_a_refusal_witness + +import gunbc.compile_diagnostic_census { + CensusObserved, + CensusNotRunnable, + census_blocking_rows, + census_rows_of_class, + census_total_count, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A PLAN IS WHAT `Apply` EXECUTES, SO A REFUSAL IS NOT ONE. gunbc.session_lease used to carry +// RefuseForeignOwner as a third ProcessLeasePlan, which made `Apply { plan: RefuseForeignOwner }` +// -- execute the refusal -- a writable state that every consumer of the decision had to answer +// for and that no producer could ever reach. decision_for_process_port_verdict already answers a +// foreign owner on the `Refuse` arm, with the reason attached, so the plan was a second +// representation of one fact rather than a fourth outcome. +// +// These two fixtures are what keeps that wall observed. Both import the real module, so +// re-adding the variant makes the negative go quiet and this file fail. The pair discriminates: +// they differ only in WHICH plan is written into the same `Apply`, so a green negative cannot be +// explained by `Apply` being unusable. + +data refusal_as_a_plan_source: String = "module process_lease_plan_negative\nimport gunbc.session_lease { ProcessLeasePlan }\nimport std.upsert_decision { UpsertDecision, Apply }\nfn f() -> UpsertDecision {\n Apply { plan: RefuseForeignOwner }\n}\n" + +data start_as_a_plan_source: String = "module process_lease_plan_positive\nimport gunbc.session_lease { ProcessLeasePlan, Start }\nimport std.upsert_decision { UpsertDecision, Apply }\nfn f() -> UpsertDecision {\n Apply { plan: Start }\n}\n" + +// THE COUNT IS SCOPED TO A CLASS AND A SUBJECT, WHICH IS WHAT THIS INSTRUMENT CAN SAY. +// compile_dag_diagnostic_census reports the rows of the WHOLE compilation the fixture is handed +// to, its imported closure included -- its own carrier note says so -- so a total count is a +// claim about the corpus rather than about the fixture. Measured here: the two sources carry 3 +// and 2 rows and differ at exactly one key. Scoping to it is what makes the remaining row +// attributable to the plan these two fixtures differ by. +data target_class: String = "InternalError" + +data target_subject: String = "variable:RefuseForeignOwner" + +// Absent, not zero, on the NotRunnable arm: a census that could not run is not a census that +// saw nothing, and collapsing them would be the fail-open the census module deleted from its +// own API. +fn census_rows(source: String) -> List? { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => Present { value: rows } + CensusNotRunnable { cause: _ } => Absent + } +} + +fn target_key_count_of(source: String) -> Int { + match census_rows(source: source) { + Present { value: rows } => + census_total_count( + rows: rows + |> filter(r => + (r.diagnostic_class as String) == target_class + && r.subject_name == target_subject + && r.blocking + ) + ) + Absent => -1 + } +} + +test fn w_a_refusal_cannot_be_written_as_a_lease_plan() -> Bool { + target_key_count_of(source: refusal_as_a_plan_source) == 1 +} + +test fn w_a_real_plan_on_the_same_arm_is_admitted() -> Bool { + target_key_count_of(source: start_as_a_plan_source) == 0 +} diff --git a/docs/plans/dispatch-maintain-cc.md b/docs/plans/dispatch-maintain-cc.md index 7e08382f61f..f5d09e6b191 100644 --- a/docs/plans/dispatch-maintain-cc.md +++ b/docs/plans/dispatch-maintain-cc.md @@ -23,7 +23,8 @@ actuator adds only runtime dedup + execution). serving lane … becomes live when a realization handler binds a handler_name dispatch"). No POST route or request-body handler exists anywhere in the corpus. - **Double-spawn gate**: `dag/gunbc/session_lease.dag` — observation→verdict→plan - (`Start` / `DrainMatchingStaleThenStart` / `RefuseForeignOwner`) over `std.upsert_decision`. + (`Start` / `DrainMatchingStaleThenStart`) over `std.upsert_decision`, with a foreign owner + refused on the decision rather than planned. Reuse the same shape keyed on tmux session name per node_id (a session lease, not a port lease; same discipline: observation carries facts, classifier decides). - **Lifecycle binding** (`dag/gunbc/code_change_workflow.dag`): phase 2, explicitly out of MVP.