Model the purpose standing, the non-execution consequence, and the admission wall

dag/std/witness_purpose.dag

@@ -30,13 +30,73 @@ type WitnessResourceBound
 // instant/deadline and completion-receipt carriers; then TerminatingOneShot joins WitnessPurpose
 // and this frontier type deletes.
 
+// WHAT A BEHAVIORAL DISCRIMINATOR REQUIRES OF THE DECISION IT WATCHES, and the reason this is a
+// REFINEMENT of BehavioralDiscriminator rather than a sixth peer arm (operator ruling, 2026-09-02).
+// The bare arm said only "this witness discriminates behaviour", which is true of a discriminating
+// RED and of an accepted positive control equally -- so it could not order a population by which
+// rows carry a wall. DESIGN 4b(1) already names these as the two halves of executed evidence: a
+// discriminating RED refused on the real acceptance path, PLUS an accepted positive control. This
+// type is that pair, authored.
+//
+// WHY THE DISTINCTION IS A SAFETY FACT AND NOT A LABEL. A row requiring a refusal is GREEN in the
+// ordinary case, so when it does not execute -- preempted, skipped, undecided -- the wall it
+// carries is switched off with nothing red anywhere, and a later green over that absence is a
+// green over a refusal that did not run. A row requiring an acceptance, not executing, leaves a
+// question open and removes no wall. Same terminal state, different consequence, and until this
+// payload existed nothing in the tree could tell them apart. The class is
+// `gunbc.recurring_failure_mode` `non_execution_undifferentiated_by_what_it_silenced`.
+//
+// THE SUBJECT IS THE DECISION, NEVER THE WITNESS. Both arms name the decision the row watches --
+// the function or declaration that must refuse or must admit -- so the fact is joinable against
+// that decision rather than being an adjective on the test. A payload naming the test itself would
+// restate the identity the row already has and could not be checked against anything.
+//
+// AUTHORED, NOT INFERRED, which the module header already requires of purpose and which binds here
+// specifically: a lens could observe that a test body matches a refusal-shaped variant, and that
+// observation is NOT this fact. It would make the compiler's own reading of the body the authority
+// on what the body is for, so a body that stopped requiring the refusal would silently restate its
+// own purpose instead of going red.
+type DiscriminatedOutcome
+  = RefusalRequired { refuser: DeclarationRef }
+  | AcceptanceRequired { acceptor: DeclarationRef }
+
 type WitnessPurpose
-  = BehavioralDiscriminator
+  = BehavioralDiscriminator { discriminates: DiscriminatedOutcome }
   | BoundaryCrossing { modeled_boundary: DeclarationRef, chosen_input: ContentHash }
   | PopulationTotality { population: DeclarationRef }
   | ExternalFidelity { effect: DeclarationRef }
   | ResourceContract { bound: WitnessResourceBound }
 
+// ONE WITNESS'S DECLARED PURPOSE, as a binding that NAMES the witness rather than a field on it.
+// There is no per-`test fn` declaration slot in the language, so the fact has to be authored
+// beside the witness and point at it. THIS SLICE MAKES A WITNESS-LOCAL AUTHORED BINDING
+// REPRESENTABLE AND NOTHING MORE. `witness` is a `DeclarationRef` and points anywhere, so a central
+// module can author bindings to arbitrary witnesses just as readily as a witness's own module can:
+// the type does not construct same-module provenance, and no test here executes a locality rule.
+// So this row must NOT be cited as evidence that the population is independently defined rather
+// than selected -- that property is owed by the future consumer, which must decide provenance from
+// `v1.declaration_index` discovery (below) and refuse a central roster, and it is unbuilt. Claiming
+// it here would be 4b's richer-type-names-are-not-safety: cosmetic until construction AND
+// acceptance enforce the distinction, and it would let another row's trigger be retired by nothing.
+//
+// WHY THIS IS JOINABLE WITHOUT A NEW AUTHORITY, and the reason the binding is a `DeclarationRef`
+// rather than a string. `v1.declaration_index` already records, per module, every typed-literal
+// `DeclarationRef` citation paired with the top-level declaration whose subtree carries it
+// (`CitedSymbol.in_declaration`), and every authored type reference under the same key
+// (`authored_type_references`). So "does a purpose binding exist for this identity" is decidable
+// from the index that already runs, by asking whether some declaration in the module both
+// references this type and cites that witness. A string would not be a citation and would be
+// reachable from no index.
+//
+// THE BINDING IS NOT EVIDENCE THAT THE PURPOSE IS TRUE OF THE ROW. It is the authored claim about
+// what the row is for, and that claim's correspondence to the body stays outside the modeled
+// guarantee -- see the module header's authored-not-inferred rule. What the binding makes
+// possible is ranking a row that DID NOT RUN, which needs only the declaration.
+type WitnessPurposeBinding {
+  witness: DeclarationRef
+  purpose: WitnessPurpose
+}
+
 type TerminatingOneShotFrontier
   = TerminatingOneShotUnavailableDeadlineSubstrateAbsent
   | TerminatingOneShotUnavailableCompletionSubstrateAbsent

dag/test/claim/witness_purpose_taxonomy_witness_test.dag

@@ -12,10 +12,14 @@ import std.witness_purpose {
   WitnessPurpose,
   WitnessResourceBound,
   BehavioralDiscriminator,
+  DiscriminatedOutcome,
+  RefusalRequired,
+  AcceptanceRequired,
   BoundaryCrossing,
   PopulationTotality,
   ExternalFidelity,
   ResourceContract,
+  WitnessPurposeBinding,
   EvalWallTimeBound,
   EvalThreadCpuBound,
   PeakMemoryBound,
@@ -24,7 +28,7 @@ import std.witness_purpose {
   TerminatingOneShotUnavailableCompletionSubstrateAbsent,
 }
 
-data witness_purpose_taxonomy_witness_note: String = "Slice C-a: stable WitnessPurpose vocabulary only — BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract. TerminatingOneShot is NOT a WitnessPurpose arm; TerminatingOneShotFrontier records honest deferral (deadline and completion substrates absent) until typed carriers land. No placement, envelope, or cadence logic — those are C-b/C-c slices."
+data witness_purpose_taxonomy_witness_note: String = "Slice C-a vocabulary, with BehavioralDiscriminator REFINED (operator ruling 2026-09-02) to carry a DiscriminatedOutcome — RefusalRequired or AcceptanceRequired — naming the watched decision, so a row that carries a wall is distinguishable from a positive control. Still five arms: BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract. TerminatingOneShot is NOT a WitnessPurpose arm; TerminatingOneShotFrontier records honest deferral (deadline and completion substrates absent) until typed carriers land. No placement, envelope, or cadence logic — those are C-b/C-c slices."
 
 fn fixture_subject_hash() -> ContentHash {
   Fnv1a64(
@@ -39,17 +43,85 @@ fn fixture_population_ref() -> DeclarationRef {
   )
 }
 
+fn fixture_refuser_ref() -> DeclarationRef {
+  decl_ref(
+    module_path: "test.claim.witness_purpose_taxonomy_witness",
+    decl_name: "fixture_population_ref",
+  )
+}
+
 test fn behavioral_discriminator_is_stable_purpose_arm() -> Bool {
-  let purpose = BehavioralDiscriminator
+  let purpose = BehavioralDiscriminator {
+    discriminates: RefusalRequired { refuser: fixture_refuser_ref() },
+  }
+  match purpose {
+    BehavioralDiscriminator { discriminates: _ } => true
+    BoundaryCrossing { modeled_boundary: _, chosen_input: _ } => false
+    PopulationTotality { population: _ } => false
+    ExternalFidelity { effect: _ } => false
+    ResourceContract { bound: _ } => false
+  }
+}
+
+// THE DISCRIMINATING CASE FOR THE REFINEMENT, and the one the bare arm could not express. Both
+// values are BehavioralDiscriminator over the SAME watched decision -- identical on every fact the
+// arm carried before this change -- and they differ only on what that decision is required to do.
+// A row requiring a refusal is green only if the decision REFUSES; a positive control is green
+// only if it ADMITS. If the payload is ever dropped, or both arms collapse to one, these two
+// become the same value again and this test goes red.
+//
+// WHY THIS IS NOT A TAUTOLOGY OVER A FRESH COPRODUCT: the assertion is that the two reach
+// DIFFERENT arms of a total match while agreeing on the watched decision, which is exactly the
+// join a consumer performs when it ranks a non-executed row. A test that only constructed one arm
+// would pass against a coproduct whose second arm was unreachable.
+// THE PREDICATE A CONSUMER PERFORMS, written once so the two assertions below cannot drift into
+// two different readings of the same coproduct. Total over both arms: a third outcome added to
+// DiscriminatedOutcome fails to compile here rather than falling to whichever answer is cheaper.
+fn purpose_requires_a_refusal(purpose: WitnessPurpose) -> Bool {
   match purpose {
-    BehavioralDiscriminator => true
+    BehavioralDiscriminator { discriminates: d } =>
+      match d {
+        RefusalRequired { refuser: _ } => true
+        AcceptanceRequired { acceptor: _ } => false
+      }
     BoundaryCrossing { modeled_boundary: _, chosen_input: _ } => false
     PopulationTotality { population: _ } => false
     ExternalFidelity { effect: _ } => false
     ResourceContract { bound: _ } => false
   }
 }
 
+// THE DISCRIMINATING CASE FOR THE REFINEMENT, and the one the bare arm could not express. Both
+// values are BehavioralDiscriminator over the SAME watched decision -- identical on every fact the
+// arm carried before this change -- and they differ only on what that decision is required to do.
+// If the payload is ever dropped, or the two outcome arms collapse to one, these two become the
+// same value and this test goes red.
+//
+// WHY IT IS NOT A TAUTOLOGY OVER A FRESH COPRODUCT: the assertion is that two values AGREEING on
+// the watched decision reach OPPOSITE answers from the predicate a ranking consumer runs, which is
+// the whole content of the refinement. A test constructing only one arm would pass against a
+// coproduct whose second arm was unreachable, and a test comparing two different decisions would
+// pass on the decision rather than on the requirement.
+test fn refusal_and_acceptance_requirements_do_not_report_alike() -> Bool {
+  let wall = BehavioralDiscriminator {
+    discriminates: RefusalRequired { refuser: fixture_refuser_ref() },
+  }
+  let control = BehavioralDiscriminator {
+    discriminates: AcceptanceRequired { acceptor: fixture_refuser_ref() },
+  }
+  purpose_requires_a_refusal(purpose: wall)
+    && !purpose_requires_a_refusal(purpose: control)
+}
+
+// A NON-DISCRIMINATOR PURPOSE CARRIES NO WALL BY THIS PREDICATE, so the ranking key cannot be read
+// as "every purpose that mentions a DeclarationRef". Without this arm the predicate could be
+// satisfied by any purpose at all and still look green above.
+test fn a_non_discriminator_purpose_requires_no_refusal() -> Bool {
+  !purpose_requires_a_refusal(
+    purpose: PopulationTotality { population: fixture_population_ref() },
+  )
+}
+
 test fn boundary_crossing_carries_modeled_boundary_and_chosen_input() -> Bool {
   let purpose = BoundaryCrossing {
     modeled_boundary: fixture_population_ref(),
@@ -133,9 +205,39 @@ test fn terminating_one_shot_unavailable_records_deadline_substrate_absent() ->
   }
 }
 
+// THE BINDING CARRIES THE WITNESS AND THE PURPOSE AS SEPARATE FACTS, which is what lets a ranking
+// consumer answer about a row that DID NOT RUN: the witness identity comes from the binding, not
+// from having executed anything.
+//
+// THE DISCRIMINATING PAIR IS TWO BINDINGS OVER THE SAME WITNESS differing ONLY in purpose. If the
+// binding ever dropped its purpose field, or carried the witness alone, these two would be the
+// same value and the consumer would rank a wall and a positive control identically -- which is
+// precisely the defect gunbc.recurring_failure_mode
+// non_execution_undifferentiated_by_what_it_silenced records. Holding the witness constant is what
+// makes the purpose the only variable.
+test fn two_bindings_on_one_witness_separate_on_purpose() -> Bool {
+  let wall = WitnessPurposeBinding {
+    witness: fixture_population_ref(),
+    purpose: BehavioralDiscriminator {
+      discriminates: RefusalRequired { refuser: fixture_refuser_ref() },
+    },
+  }
+  let control = WitnessPurposeBinding {
+    witness: fixture_population_ref(),
+    purpose: BehavioralDiscriminator {
+      discriminates: AcceptanceRequired { acceptor: fixture_refuser_ref() },
+    },
+  }
+  wall.witness == control.witness
+    && purpose_requires_a_refusal(purpose: wall.purpose)
+    && !purpose_requires_a_refusal(purpose: control.purpose)
+}
+
 test fn witness_purpose_has_five_stable_arms_only() -> Bool {
   let purposes = [
-    BehavioralDiscriminator,
+    BehavioralDiscriminator {
+      discriminates: RefusalRequired { refuser: fixture_refuser_ref() },
+    },
     BoundaryCrossing {
       modeled_boundary: fixture_population_ref(),
       chosen_input: fixture_subject_hash(),

src/v2/lens/inert_carrier.dag

@@ -50,7 +50,7 @@ data inert_carrier_roster: List<FrontierRow> = [
   inert_row(unit: "SharedBuildProvenance", reason: "modeled floor-preparation provenance carrier in v2.workflow.required_floor (#9046): it records whether a shared build was BUILT BY preparation or found already warm and, in that arm, WHICH site got there first -- the triggered_by/owned_by distinction the attribution repair exists to keep structural. It is declared ahead of its reader: the host mirror (v1_compiler.cli_run SharedBuildProvenance) is what the running floor renders today, so the corpus carries the model with only floor_preparation_shared_build_witness_test referencing it. Its reader is the .dag-side preparation report that supersedes that hand-written host mirror, which floor_preparation_host_mirror_dissolve_on in that same module already tracks"),
   inert_row(unit: "SystemdUnitStatus", reason: "modeled systemd extdeps carrier with no live consumer yet"),
   inert_row(unit: "TerminatingOneShotFrontier", reason: "modeled std.witness_purpose frontier coproduct from #7965 (Slice C-a): its variants name the two substrate absences that block a terminating one-shot classification, and only its own test file references it, so it is inert by the seed rule until the classifier consumes it"),
-  inert_row(unit: "WitnessPurpose", reason: "modeled std.witness_purpose taxonomy from #7965 (Slice C-a): the stable purpose coproduct a witness declares, landed ahead of the consumer that derives witness size from it, with no non-test reference yet")
+  inert_row(unit: "WitnessPurposeBinding", reason: "modeled std.witness_purpose binding (operator ruling 2026-09-02): one witness identity paired with its declared WitnessPurpose, authored beside the witness because the language carries no per-test-fn declaration slot. It is what a ranking consumer joins against for a row that did not run. Referenced only by test.claim.witness_purpose_taxonomy_witness until the floor consumer lands, and dissolves in the same diff that gives it a reader"),
 ]
 
 fn inert_carrier_rostered_names() -> List<String> {