Autolink clean

The check is autolink_clean. It is implement-stage. Severity of a hygiene miss is warning, not fail. It asks autolink to scan real artifacts and refresh source-backed trace state. It does not rewrite authored requirement YAML. A helper error fails the hop. A non-empty Errors list warns, with a count; --verbose prints the rest after the first three.

A hit is a scan error the autolink channel already renders: an annotation that names a missing requirement, a malformed trace comment, a file type the scanner should not have opened, or a requirement-id-shaped token whose prefix the project never registered. The last one used to be silent. An operator who wrote // Implements: STK-REQ-001 in a tree that only registered SYS-REQ saw zero matches and zero warnings. The hop now surfaces that token on the same Errors channel.

// pkg/cache/ttl.go
// Implements: STK-REQ-001
func ttlExpired(deadline uint32, now uint32) bool {
    return now >= deadline
}
# proof audit --check autolink_clean
# [IMPLEMENTATION] autolink_clean -- 1 autolink errors
# [autolink] STK-REQ-001 at pkg/cache/ttl.go:2 has unrecognized prefix "STK-REQ"
# silent drop: the comment shipped. no configured prefix owns it

Zero errors is process health. A tree with no annotations also reports 0 autolink errors and passes. Completeness of Implements: / Verifies: stays on orphan code and orphan tests. Do not treat a green autolink stamp as a reviewed graph.

Fix the named file. Add the prefix to proof.yaml, or rename the id to a configured prefix. Then re-run. Do not mint a Jama note to carry the skip.

proof audit --check autolink_clean
proof trace autolink
proof trace autolink-code --dry-run
proof audit --scope baseline --verbose

The teaching graph is still one Implements line whose prefix the project never registered, and a board that called autolink done because the count was zero. Close it by adding the prefix, or by renaming the id. Do not treat a Jama note as this hop. Do not treat 0 autolink errors as a complete graph.

# proof.yaml
project:
  specs:
    - prefix: SYS-REQ
    - prefix: STK-REQ
# proof audit --check autolink_clean
# [IMPLEMENTATION] autolink_clean -- 0 autolink errors

The completeness hop stays on orphan code. The matrix hop stays on requirements traceability matrix. Jama still authors. Proof vs Jama.

Warning, not fail. Promote once the corpus is clean. Zero annotations is 0 autolink errors and a pass. The hop does not ask whether every function has an Implements line. It does not rewrite authored YAML. It does not write the annotation. Details cap at three unless --verbose. A missing Probe binary fails the helper instead of warning, and downstream documentation coverage then reads stale state. The hop does not prove the Go. Copied comments that already use a configured prefix still pass. We have not scored this floor against a frozen Jama pack or a ReqIF round-trip. The loss is named, not scored.

The completeness hop stays on orphan code. The engagement stays on software correctness audit. Jama still authors.

What is autolink clean? Same question. Same URL.

Is this a requirements traceability matrix? No. That hop rebuilds requirement, code, test. This hop asks whether the scan that would fill that table still ran without errors. See requirements traceability matrix.

Is this orphan code? No. That hop is a production function with no live Implements line. This hop is process health of autolink. Zero annotations still pass here. See orphan code.

Is this orphan tests? No. That hop is a Test* with no live Verifies line. See orphan tests.

Does 0 autolink errors mean every function is traced? No. It means the scan produced no errors. An empty tree also reports zero.

Does a green hop prove the Go? No. The hop observes scan errors. It does not prove the function is correct.

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