Skip to main content

Module sharing

Module sharing 

Source
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§

ResultSharing
Sharing and divergence over one run’s evidence.

Functions§

result_sharing
Measure sharing and divergence over a run’s evidence.