Expand description
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§
- Awaited
Observation Source - 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
internalfor an effect that leaves no boundary at all. - Call
Omission Evidence - A bounded check of one specified edit, never general value or site credit.
- Comparison
- Comparison
Input - Input provenance through const aliases/await, not evaluated value identity.
- Comparison
Operand - Source identities of both operands. Equal source text is not binding identity.
- Completion
Check - Completion
Diagnostic - Completion
Matcher - Completion
Sensitivity Evidence - Count
Sensitivity Evidence - Count
Sensitivity Variant - Decision
Facts - The sites each outcome of a decision controls, and the site sets its witness rules ask about.
- Default
Kept - Dependent
- Direct
Return Check - Direct
Return Sensitivity Evidence - Direct
Return Variant - Facts
- Missing
Exception Diagnostic - Mock
Count Call - Mock
Count Evidence - Mock
Count RowBinding - Source-reproduced registration inputs; not a value-protection proof.
- Mock
Count RowValue - Mock
History Selection - A bounded selection from a copied history, not a claim about the whole mock.
- Mock
Projection - Which part of a mock’s history a passing assertion reads. This is source evidence; relating a history element to a production site remains unresolved.
- Object
Valued - Observation
- Predicate strength applies to the projected value, not automatically to the arguments or count of each production call contributing to a mock history.
- Observation
Capture Source - Outcomes
- Payload
Check - Payload
Coercion - Payload
Projection - Payload
Sensitivity Evidence - Payload
Variant - Pragma
Check - Pragma
Hint - A source suggestion, deliberately separate from observations and join inputs.
- Pragma
Target - Primitive
Decision - Bounded direct-call, side-effect-free literal branches checked by the frontend.
- Primitive
Decision Check - Process
Exit Consumer - Process
Exit Event - Process
Exit Evidence - Checked resolver syntax, not a checked runtime/producer instance relation.
- Process
Exit Resolution - Reason
- Resolution
- Sink
Binding - A test-owned object the test passed into production, and the parameter it arrived through.
- Site
- Summary
- Test
Facts - Test
Witness Issue - Witness
Issue
Enums§
- Hint
Validation - Reason
Kind - 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.
- Sensitivity
Basis - Source
Primitive - Source literals, not sampled runtime values. Numeric text preserves -0.
- 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;
Presencesays a value arrived. - Witness
Issue Kind
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.