Expand description
How much an EvidenceRun shares across independently addressable
validation results.
compact answers a question about bytes: how much of a
serialized run collapses under hash-consing. This module answers a question
about work: how much of the derivation is reached from more than one
addressable result, and whether a judgment determines its own evidence. The
two are measured differently on purpose — this one never touches JSON, so
its counts are an independent check on the encoder’s.
Three definitions carry the measurement.
The address of a result. Interior results are addressed by
(constraint, node, polarity) — the shape memo’s (ShapeId, Term) key
(validate.rs) plus which way it came out. Every Witness and SatTrace
carries the first two; the enum itself carries the third. Constraint and
node, not shape and focus: focus is reserved for the top-level
selected node, and interior judgments are usually about some other node
reached from it.
The unit that is independently addressable. A run holds one record per
authored (statement, focus) pair, because a report must name the
statement its reader wrote. But two authored statements that normalize
together are one request: the engine evaluates it once, and materializing
it twice is duplication, not sharing. Sharing is therefore counted across
normalized requests — normalized_requests
— while the authored records are retained and counted separately, so
source traceability costs a number rather than hiding inside the sharing
one.
Payload divergence. A key is only an address if it determines what is
stored there. It may not: Witness::Atom carries reached_by and
produced_by, which describe how the node was reached rather than what was
decided about it, so one key can occur with several payloads.
divergent_keys measures how often that
happens, which is what decides whether evidence can be memoized on the
judgment the way conformance already is.
That gives a bracket rather than a single number:
payload_redundancy is what structure
sharing collapses losslessly today, and
key_redundancy is what a memo keyed like
the conformance memo could collapse if divergence were zero. The gap between
them is the evidence that depends on its derivation context.
Structs§
- Result
Sharing - Sharing and divergence over one run’s evidence.
Functions§
- result_
sharing - Measure sharing and divergence over a run’s evidence.