Module asserted_coverage 

The language-neutral join of asserted coverage: sites, evidence and observations in, a verdict per site out.

Frontends contribute facts and never verdicts, so everything syntactic happens before this module: which boundaries a site’s effect or value reaches, which sites each outcome of a decision controls, what each assertion reads and how strongly. This module decides only what those facts imply, which is the one part of the metric that is the same in every language.

Evident and presence are candidate classifications under the frontend’s flow and observation rules, not formal proofs of arbitrary-change detection. Unresolved sites carry a reason: a gap a test can close, or an analysis limit the frontend could not follow. Limits remain visible and must not be silently removed from a reported accuracy denominator.

Structs

Boundary

A place a site’s effect or value arrives, and which an assertion may read: a function’s return or escape, a sink the test injected, a mocked module, an installed global, a process channel, rendered output, or internal for an effect that leaves no boundary at all.

DecisionFacts

The sites each outcome of a decision controls, and the site sets its witness rules ask about.

DefaultKept

Dependent

Facts

ObjectValued

Observation

What one assertion reads, as the frontend understood it.

Outcomes

PragmaCheck

PragmaHint

A source suggestion, deliberately separate from observations and join inputs.

PragmaTarget

Reason

Resolution

SinkBinding

A test-owned object the test passed into production, and the parameter it arrived through.

Site

Summary

TestFacts

TestWitnessIssue

WitnessIssue

Enums

HintValidation

ReasonKind

Why a site is not evident. A gap is closable by writing a test; a limit is something the frontend could not follow, and an agent that writes a test for one either wastes the effort or learns to satisfy the analyzer instead of the code.

Status

Strength

How strongly the modeled assertion checks what it reads. This classifies its predicate, not a formal proof of the complete source-to-assertion dependency; Presence says a value arrived.

WitnessIssueKind

Functions

check_pragma_hints

Check source hints against existing facts, without modifying the normal join. Indexes are shared across hints; only the selected test’s observations are copied. This bounded first pass supports effect boundaries/flow, not decision or internal derivation proofs. Unsupported paths remain unresolved, not contradicted.

join

Resolve every site. Effect sites first, since a decision’s outcomes are judged by the strength of the sites they control; then decisions; then internal effects derived through their dependents, which can promote a site and so are followed by a second decision pass, exactly as the prototype does.

summary

The metric: of the contractual sites, how many are evident.