How to read the coverage report

The coverage report lists every judgment_fn! in the model and every inference rule inside it. The numbers come from the test suite: they are recorded while cargo test runs, so they say what the tests actually exercised, not what the model can in principle prove.

The index table

The report’s front page has one row per judgment and one row per rule inside it. The positive column says how many tests proved something with that rule. The negative column is a fraction: how many of the rule’s premises that can fail have been seen to fail, out of how many there are.

Positive and negative coverage

A judgment’s own page shows each rule as its source, one line per premise with the conclusion below the --- separator, and puts a number on each line:

• The green number on a rule’s conclusion is positive coverage: how many tests proved something using that rule. It says the rule can fire.
• The orange number on a premise is negative coverage: how many tests failed while trying to prove that premise. It says the premise is load-bearing, because some program was rejected by it.

A rule with positive coverage but no negative coverage on any premise is only tested in one direction: the tests show it accepting programs, but never show a premise doing the work of rejecting one.

The other cells

• ✗ means nothing was observed. For a conclusion, no test proved anything with the rule; for a premise, no test failed on it. This is a gap in the test suite, not necessarily a bug in the model.
• N/A marks a premise that cannot fail once the rule’s conclusion matches (a let without a ?), so there is nothing to cover negatively. On the index it marks a rule with no fallible premise at all.
• no applicable rule observed on a judgment means some test called the judgment and none of its rules matched at all.

Following a number

Clicking a number opens that cell’s page: the tests behind the number, each with its source and the proof tree it produced (successful trees for positive coverage, the failed tree pruned to the stacks involving the premise for negative coverage). The chart at the top of that page is the same rule, with the cell you came from highlighted, so you can move to a neighbouring cell without going back.

The by-test view is the same data organized the other way round: one page per test, listing the rules it proves and the premises it fails on. Every row links back, so “what else does this test cover” and “what else covers this premise” are both one click away.