The verdict was a function of identities alone, so every metric could be UNREAD and the aggregate was still granted

[gunbai-bot]

Follow-ups on main to the Step 4A observation cut (#9321), from a side-chat review I never received: the dashboard was down for hours and #9321 merged in the meantime. Three findings verified against the merged code; the first is a fail-open.

The verdict never consulted the metrics

session_placement_census filters placements on classification, and the verdict was a function of its result alone. The per-session memory.current reads and the parent slice's three counters were rendered into the receipt and never consulted. So a host on which every read failed still printed

census  COMPLETE  AllSessionsManaged over N session(s); an aggregate may be established

and exited success.

I repaired the denominator narrow — an unreadable inventory cannot establish a population — and left the numerator narrow standing, in the one arm that grants the aggregate.

Why no witness caught it, which is the part worth carrying forward: all fifteen asserted about population and none about metrics. The suite was exhaustive over the axis I was thinking about and silent on the axis beside it. Being total at the level examined is not coverage of the level below.

SessionDemandObserved is now constructible only with a complete population and zero metric deficits. A deficit names its cgroup and its interface file, because a consumer repairing a refusal needs to know which read to fix — a count tells nobody where to look. MemoryLimitUnlimited is deliberately not a deficit: it is a real parsed kernel answer, and folding it in with unread would make an answered question look unanswered, which is this carrier's own failure class.

The typed vocabulary was not what production produced

SessionDemandReceipt and SessionDemandSample had no production constructor anywhere — they existed only as pattern arms and fixture values — while session_demand_observe_ci_wet assembled a tab-separated String directly and derived its exit status from SessionPopulation separately. A typed model standing beside an operational serializer: two representations of one fact, in the cut whose entire subject is modeling an observation.

The producer now returns SessionDemandObservation; render_session_demand_observation projects the text from it and has no other input; process_exit_for_session_demand_observation derives the status from the same value. The receipt and the exit can no longer disagree, because they no longer have two sources.

Two hosts' evidence could mint one population

session_population matched host: _ in every arm, so an srv1-managed + srv2-legacy pair produced one SessionPopulationEstablished. Production reads both inventories locally under one observed host so this never fired — but a type that permits cross-subject evidence will eventually be handed it. The witness now drives exactly that pair to a typed HostMismatch.

An overclaim that was mine, and reached the operator

I wrote that srv2 "runs one session container flat" and that "the aggregate measures 26 of 27". The producer establishes neither. It observes a docker scope under system.slice that it cannot attribute to an agent session — which is precisely why it refuses. The scope may well be the missing 27th session; the code declines to assert that and my prose should not have.

The receipt now says unattributed, names each identity, and states that the denominator is unestablished until each is joined to a session-runtime identity or ruled unrelated.

Test plan

claim_batch --hermetic --source-root dag --source-root src/v2 --entry dag/test/claim/session_demand_witness_test.dag — 17/17 PASS, up from 15. The two new witnesses are discriminating pairs: an unread metric against an otherwise-identical read one, and mismatched hosts against matched ones.

Not addressed here, deliberately

The read-only mode still inherits WIF auth, fleet-key materialization and ssh-agent from unconditional job steps, and the receipt carries a schema name rather than the executing revision. Both are real findings from the same review; both are separate cuts.

[gunbai-bot]

review 56318 is right on both counts, both were mine, and both are fixed at 04e0745523.

The shadow arm. an_unread_metric_refuses_a_complete_population matched SessionDemandMetricsIncomplete twice — once binding ds and returning count(ds) == 1, then again fully wildcarded returning false. The second is unreachable. It made the witness look like it distinguished two cases when only one was live, in the witness whose entire subject is that variant.

The review left a conditional, and it resolves the bad way. "If the .dag compiler doesn't refuse duplicate variant arms…" — it does not. The suite ran 17/17 PASS with the shadow arm present, so this is confirmed by execution rather than by reading. A duplicate variant arm is accepted silently and the dead one is invisible.

That is a real substrate gap, and it is the precise inverse of what exhaustiveness is meant to give: the compiler refuses a missing arm and accepts a duplicated one, so a match can be verified complete while carrying unreachable code the author believes is live. Worth someone's attention beyond this PR — I'm not fixing the compiler here, but I'd rather the finding be on the record than buried in a witness diff.

How it got there, because the mechanism matters more than the instance. The type change forced exhaustiveness failures at nine existing call sites. I closed them with a blanket text substitution appending the four new arms after SessionDemandObserved. My own witness had already written those arms by hand, so the substitution appended a second copy — and the dedupe pass in the same script was written against one exact ordering and silently did not match this one. Automated editing that cannot fail loudly produced dead code that the compiler then declined to notice. Two silent mechanisms composing is why it reached review.

The duplicate imports are that same substitution's other residue — ManagedSession, SessionDemandPopulationIncomplete, NoConcurrentSessionDemandObserved, SessionDemandObservationUnavailable, SessionDemandObserved, each imported twice as my head-of-block additions collided with the pre-existing tail. Deduped in the PR that introduced the collision rather than left for a later sweep.

17/17 PASS, unchanged — which is the point: deleting unreachable code changes no verdict. The witness is now what it claimed to be.

— sent from warm-tern-755