Lemma branch coverage

The check is lemma_branch_coverage. It is verify-stage. Severity of an uncovered branch is warning, not fail. The refresh command is proof verify-lemma --coverage ./.... The inspect file is .proof/lemma-coverage.json.

The hop reads persisted visit events. Each event names a production <file>:<line> plus the AST kind: if-then, if-else, switch, case, call, for, range. An empty covered_by list is the finding. This is formal coverage: which branches the SMT translator visited while lowering each lemma. It is not Go test coverage. It is not MC/DC.

The help file teaches the silent lemma first. One funclit proves the positive identity. The negative arm still returns -x. Nothing in the suite asked whether the translator reached that node.

// reqproof:lemma abs_positive_identity func(x int) bool {
//   return x >= 0 ==> Abs(x) == x
// }
func Abs(x int) int {
    if x < 0 {
        return -x
    }
    return x
}

# proof verify-lemma --coverage ./...
# .proof/lemma-coverage.json
# pkg/mathx/abs.go if-then "x < 0" covered_by: []

# proof audit --check lemma_branch_coverage
# [VERIFICATION] lemma_branch_coverage
# pkg/mathx/abs.go:5 if-then "x < 0" not reached
# silent lemma: last PROVE still on the other arm

Refresh the JSON before you decide. --coverage implies --no-cache, so every body is re-translated and the recorder sees every visit. Then pick one resolution, not a stack of them: write a Pattern A lemma whose body invokes the host, write a host-attached funclit whose guard selects the missing arm, or delete the branch if it is dead. There is no per-line waiver. A branch is either covered by a lemma or it is gone.

proof verify-lemma --coverage ./...
proof audit --check lemma_branch_coverage --verbose

The teaching graph is still one Abs whose last PROVE sat on the positive arm. Close it by adding a second funclit whose guard selects x < 0, by writing a Pattern A lemma whose body invokes the host, or by deleting a branch that should not exist. Do not delete .proof/lemma-coverage.json to make the warning disappear. With no coverage file the check skips, and the uncovered branches did not go anywhere. They just stopped being counted. Narrowing --coverage to a package you already covered is the same cheat: the number improves because the denominator shrank.

// reqproof:lemma abs_positive_identity func(x int) bool {
//   return x >= 0 ==> Abs(x) == x
// }
// reqproof:lemma abs_negative_negates func(x int) bool {
//   return x < 0 ==> Abs(x) == -x
// }
func Abs(x int) int {
    if x < 0 {
        return -x
    }
    return x
}

# proof verify-lemma --coverage ./...
# proof audit --check lemma_branch_coverage
# no empty covered_by on Abs. this hop is quiet

A lemma written only to touch a branch, asserting something trivially true, moves the node into the covered column without an SMT obligation that would contradict a counterexample hidden there. That is the anti-pattern this check is meant to measure, and it is not a pass. The summary can still warn at 100% lemma branch coverage when production-reach is low: the corpus proves things thoroughly about a small slice of the package. Covering every branch the existing lemmas already touch does nothing for that. Write lemmas that bind new production functions, then refresh. The solver hop stays on Z3/Kind2 on one function. The hash hop stays on lemma binding freshness. Jama still authors. Proof vs Jama.

Warning, not fail. Not blocking. No project loaded is a pass. No .proof/lemma-coverage.json is a skip, not a fail. A project with lemma annotations gets a skip reason that points at proof verify-lemma --coverage. A project with no lemmas at all is told coverage is not applicable until lemmas are authored. No recorded production branches is a silent pass. The hop looks at persisted visit events. It does not re-run Kind2. It does not re-run Z3. It does not write the JSON. It does not prove the Go. A visit is coverage of translation, never a claim that the branch is constrained: a trivial funclit will still count. Raising severity to error in proof.yaml is a strictness setting, not a remediation. There is no per-line waiver. --coverage is a separate, slower cadence because it implies --no-cache. Synthetic proof scaffolding is not recorded. Loop-bearing functions credit the recursive helper, which mirrors the original body. We have not scored this floor against a frozen Jama pack or a ReqIF export. The loss is named, not scored.

The solver hop stays on Z3/Kind2 on one function. The engagement stays on software correctness audit. Jama still authors.

What is lemma branch coverage? Same question. Same URL.

Is this Z3 or Kind2 on one function? No. That hop runs the solver. This hop asks whether any lemma translation reached the other arm. See Z3/Kind2 on one function.

Is this lemma binding freshness? No. That hop is a separate-file binding whose SHA-256 no longer matches the live function. This hop is an AST node with an empty covered_by. See lemma binding freshness.

Is this a trivial lemma? No. That hop is a candidate tautology: the assertion is the model body. This hop is whether any lemma translation reached the other arm. A trivial funclit still counts as a visit. See trivial lemma.

Is this formalization lemma verdict consistency? No. That hop is a SYS-REQ that still says valid while the lemma cache is timeout. This hop is a production branch the translator never visited. See formalization lemma verdict consistency.

Is this MC/DC for Go? No. That hop is independent condition pairs in tests. This hop is SMT translation visits. See MC/DC coverage for Go.

Does a tree with no lemmas pass? The check skips when the coverage file is missing. That is not a proof that the Go is correct. It is a proof that this hop had nothing to join.

Does a green hop prove the code matches the shall? No. The hop observes visit events. It does not prove the Go.

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