Obligation witness grounded

The check is obligation_witness_grounded. It is language-neutral at the mapping layer. Coverage profiles come from pkg/coverlink. Symbol spans come from probe symbols. The intersection is shared. The only per-language piece is a producer that emits a profile. Go is wired. A language with no producer, or an environment that cannot build the suspect, is an advisory coverage-unavailable row, never a silent pass.

Walk every coverage-trackable obligation witness. Out-of-process kinds (integration, fuzz, differential) are exempt: they never run under in-process coverage and they are credited by their own carrier check. Everyone else is a candidate. A static pre-filter asks whether the witness function names a symbol in implemented_by. A hit is grounded and coverage is skipped. Zero references is a SUSPECT, not a verdict: a same-file helper that reaches the impl is a legitimate suspect. Each suspect then runs ALONE under coverage. Collective coverage is masked by a real test sitting next to a theater one. Overlaps an impl-symbol span: CLEARED. Overlaps none: CONFIRMED theater. Severity of the hop itself is warning, not error.

proof audit --check obligation_witness_grounded
# SW-REQ-040 implemented_by: KeepAliveBound
# test still has // SW-REQ-040:lifecycle:nominal
# body: started := true; configured := started; if !configured { t.Fatal(...) }
# no call into KeepAliveBound
# static: zero impl-symbol refs -> SUSPECT
# coverage of that test alone: empty profile
# warn: SW-REQ-040:lifecycle:nominal TestLifecycle
#       executed none of KeepAliveBound (vacuous-theater)
# silent theater: the triple exists. the impl did not run

obligation_evidence_complete only asks whether the required evidence kinds exist as triples. This hop asks whether a coverage-trackable triple still executed the impl. A mapped profile result stays on obligation_profile_evidence_complete. A covering SYS-REQ stays on obligation_completeness. A listed class with no accept stays on obligation_baseline. A listed class with no signal stays on obligation_enforcement_backed.

A confirmed finding says only that this witness executed none of its requirement's implementation. Three cheap hints: vacuous-theater (empty profile), mislinked-impl (ran other product code), uncovered-impl (the triple is a promise no test keeps). Confirm the root cause before picking a fix. Make the witness real, retag a genuine out-of-process carrier, delete the triple so the gap is honest, or correct the trace link. A helper that calls the impl is fine. Coverage sees through the indirection.

// Verifies: SW-REQ-040
// SW-REQ-040:lifecycle:nominal
func TestLifecycle(t *testing.T) {
    if got := KeepAliveBound(true, 30); !got {
        t.Fatalf("expected bound materialized, got %v", got)
    }
}

The teaching graph is still one lifecycle class whose colon triple is present and whose test never calls KeepAliveBound. Write a real witness. Do not treat a Jama note as this hop. Do not treat a colon triple as an executed line.

proof audit --check obligation_witness_grounded --verbose
proof workflow check --stage implement --verbose

The presence hop stays on obligation evidence complete. The silent-triple hop stays on obligation profile evidence complete. The silent-no-op hop stays on obligation enforcement backed. The covering-child hop stays on obligation completeness. The silent-omission hop stays on obligation baseline. The silent-drop hop stays on obligation decomposition complete. The silent-pointer hop stays on obligation delegation resolves. The silent-placeholder hop stays on obligation suppression rationale. The silent unsigned skip stays on obligation suppression reviewer. Jama still authors. Proof vs Jama.

The hop does not write a test. It does not run the product for you beyond the isolated suspect coverage pass. No coverage-trackable witnesses is a silent pass. Severity of the hop is warning, not fail. Promote to error in project.checks.obligation_witness_grounded once the corpus is clean. Integration, fuzz, and differential witnesses are exempt. A helper-indirection test is a suspect until coverage clears it. coverage-unavailable is advisory, never a confirmed finding and never a silent pass. The issue-type hint is advisory. --skip-level L0 skips the hop. Opt-out is skip, never pass. The hop does not prove the Go. We have not scored this floor against a frozen Jama pack. The loss is named, not scored.

The child-file hop stays on requirements decomposition. The engagement stays on software correctness audit. Jama still authors.

What is obligation witness grounded? Same question. Same URL.

Is this obligation evidence complete? No. That hop is whether required evidence kinds exist as colon triples. This hop is whether a coverage-trackable triple still executed the impl. See obligation evidence complete.

Is this obligation profile evidence complete? No. That hop is whether a mapped profile still has a passing result file. A theater test with a race result still passes there. See obligation profile evidence complete.

Is this obligation enforcement backed? No. That hop is whether a listed class has a signal or any evidence. This hop is execution. See obligation enforcement backed.

Is this obligation completeness? No. That hop is whether each listed class has a covering SYS-REQ. See obligation completeness.

Is this obligation baseline? No. That hop is whether a tag-matched class was listed, suppressed, or delegated. See obligation baseline.

Is this acceptance witness quality? No. That hop is whether an acceptance tag still names one function. This hop is obligation triples. See acceptance witness quality.

Does a helper that calls the impl fail? No. Zero direct symbol refs make it a suspect. Coverage of that test alone still clears it if KeepAliveBound ran.

Does an integration test fail because coverage is empty? No. Out-of-process evidence types are exempt. Tag them as integration, fuzz, or differential.

Does a green hop prove the Go? No. The hop observes execution of listed impl symbols. It does not prove the function is correct.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.