Obligation evidence complete

For every requirement that carries an obligation_checklist, the hop reads each class and the evidence types that class requires. Then it looks for an annotated test in the triple:

// SYS-REQ-<id>:<obligation_class>:<evidence_type>
func TestRejectsInvalid(t *testing.T) { /* ... */ }

The catalog declares the class list. error_handling wants negative. concurrent wants race. denial_of_service_resistant wants fuzz. On top of that list, the hop default-requires nominal at the implementable levels: the happy-path unit witness. You do not add nominal to every class YAML. The resolved set is the class list with nominal in front.

Bracket form does not count. // SYS-REQ-100 [negative] fills the legacy evidence class and leaves the obligation class empty. Bare // SYS-REQ-100 is a baseline test token only. Only the colon triple binds the kind to the class. Mixing a bracket into a class-scoped cell is the usual false-positive on this hop.

// SYS-REQ-100                              -> bare
// SYS-REQ-100 [negative]                   -> bracket, not this hop
// SYS-REQ-100:malformed_input:negative     -> triple

The token is spelled nominal, never positive. positive is the MC/DC witness. A // SYS-REQ-100:error_handling:positive triple credits nothing here. annotation_validity now asks whether you meant :nominal.

This hop is sibling to, not an extension of, obligation completeness (at least one SYS-REQ per class) and spec to obligations (compile the shall). A covering SYS-REQ can still fail here: the test never named the kind.

The teaching graph is still one class next to one missing kind. Read the finding. Then annotate a triple, decompose to a child, defer with a tracking ref, or suppress only when the class does not apply.

proof audit --check obligation_evidence_complete --verbose
proof test affected --requirement SYS-REQ-100 --run
proof help obligation-evidence
proof help obligation_evidence_complete

Covered is a triple. Deferred is required-but-untested, a counted warning, never a silent pass, and never promoted to error even under evidence_strict. Suppressed is not-applicable, silent, and reviewed by the suppression hops. A class cannot be both. Do not use --suppress-obligation to park a test you have not written. That fakes a green pass.

Lemma, race, and fuzz tokens also need run provenance: a fresh passing evidence-profile result whose command matches the lane. A matching comment is not enough. Fuzz stays opt-in via proof audit --fuzz. When the lane is not run, the cell stays uncovered. Under trace_policy.mode: overlay_audit, the file that holds the triple must already be a traces.verified_by target or carry // Verifies: for that requirement. Out of scope is not credited.

Close a finding by writing // <REQ>:<class>:<type> on a test that actually asserts the path, by moving the class to a child, by deferring with a reason and a tracking ref, or by suppressing with a reason of at least 32 characters when the class does not apply. The hop does not write the test. Jama still authors. Proof vs Jama.

Warning by default. Projects opt into error with audit.evidence_strict: true. Deferrals stay warnings even then. Zero warnings means genuinely done, including no parked debt. The hop does not write the test. It does not execute the lemma, the race detector, or the fuzzer unless you ran those lanes. A typed cell without provenance stays uncovered. Stakeholder requirements do not carry the nominal floor; that floor lives on SYS / SW / INT. Acceptance criteria are a different hop. We have not scored this floor against a frozen Jama pack, a Cornell-style legal memo, or an MC/DC independence suite. The loss is named, not scored.

The STK to SYS hop stays on obligation completeness. The compile hop stays on spec to obligations. The four-invariant hop stays on catalog completeness. The engagement stays on software correctness audit. Jama still authors.

What is obligation evidence complete? Same question. Same URL.

Is this obligation completeness? No. That hop is whether each listed class has a SYS-REQ. This hop is whether that SYS-REQ has the required triples. See obligation completeness.

Is this spec to obligations? No. That hop compiles a shall. See spec to obligations.

Does a bracket annotation count? No. // SYS-REQ-100 [negative] is legacy. Only the colon triple binds the class.

Does :positive count? No. That token is MC/DC. The positive floor here is :nominal.

Does a missing triple fail the merge? Not by default. The hop is warning until evidence_strict. A deferral stays a warning even then.

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