Orphan code

The check is orphan_code_clean. It is implement-stage. Severity of a hygiene miss is warning, not fail. Under source_native (the default), every supported production function needs a // Implements: <REQ> annotation, or the triple form, pointing at a live requirement. Test symbols stay on orphan tests. This hop skips IsTest / IsTestFile rows.

A hit is a function with no requirement id, or an annotation that still names a retired or superseded id. Coverage checks (coverage_met, coverage_threshold, code_mcdc_coverage) run against the traced set. An unannotated function simply does not exist as far as those checks are concerned. The audit reports clean coverage of a corpus the team did not realise had shrunk.

// projectsActiveSpec returns the active spec set for the project.
func projectsActiveSpec(p *Project) []Spec {
    // ...
}
# proof lint --check orphan_code_clean
# [IMPLEMENTATION] orphan_code_clean -- pkg/repo/spec.go:projectsActiveSpec untraced
# silent shrink: the helper shipped. no shall owns it

Four legitimate resolutions, one per finding: write // Implements: to the requirement the function already satisfies; write the requirement first when nothing states that behavior; delete the code when it is dead; or exclude the subtree with lint.exclude when it is generated, vendored, or a fixture. Do not attach the nearest plausible id to make the count drop. That passes the audit while inflating a shall the function does not implement.

Inspect the untraced list before trusting a green summary. Then annotate, author, delete, or exclude. Do not mint a Jama note to carry the skip.

proof lint --check orphan_code_clean
proof lint --check orphan_code_clean pkg/repo/
proof trace autolink-code --dry-run
proof audit --scope baseline --verbose

The teaching graph is still one helper whose board called the refactor done and whose requirement was never named. Close it with an annotation, a new shall, a delete, or an exclude. Do not treat a Jama note as this hop. Do not treat a green coverage stamp as a reviewed tree.

// projectsActiveSpec returns the active spec set for the project.
//
// Implements: SYS-REQ-901
func projectsActiveSpec(p *Project) []Spec {
    // ...
}

The test hop stays on orphan tests. The percentage hop stays on coverage threshold. The matrix hop stays on requirements traceability matrix. Jama still authors. Proof vs Jama.

Warning, not fail. Promote once the corpus is clean. Under overlay_audit both orphan checks pass wholesale, because upstream-owned functions are not required to carry in-source comments. orphan_scope: traced warns for breadth when unannotated files are skipped; it does not pass. Test functions are not this hop. Details cap at five unless --verbose. The hop does not write the annotation. It does not write the requirement. It does not prove the Go. It does not find unreachable functions. A parser mistake can make plain data look like code. Extensionless scripts with a recognised shebang are scanned like their extensioned counterparts. We have not scored this floor against a frozen Jama pack or a go.dev deadcode run. The loss is named, not scored.

The test hop stays on orphan tests. The engagement stays on software correctness audit. Jama still authors.

What is orphan code? Same question. Same URL.

Is this dead code? No. Dead code is unreachable functions (CWE-561, go.dev deadcode). This hop is a live production function with no live requirement.

Is this orphan tests? No. That hop is a Test* with no live Verifies:. This hop is a production function with no live Implements:. See orphan tests.

Is this a coverage threshold? No. That hop is a percentage on the traced set. An orphan never enters that denominator. See coverage threshold.

Is this a requirements traceability matrix? No. That hop rebuilds requirement ↔ test ↔ code. This hop asks whether this production symbol is on the graph. See requirements traceability matrix.

Does overlay_audit fail this hop? No. Overlay projects pass wholesale. The overlay is expected to close trace through implemented_by links, not source comments.

Does a green hop prove the Go? No. The hop observes that production functions still have a live annotation. It does not prove the function is correct.

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