Module types 

Data types for the path-refinement layer.

These structures are produced by the backward visitor and consumed by the forward visitor, engine, and diagnostic formatting. ContractFact is the only variant never produced by the backward visitor itself — it is injected by the engine before the forward visit.

Structs

ProofGoal

A proof goal for one (checkpoint, path) item: the set of relevant items plus the path context needed to verify the target property.

Enums

RelevantItem

One relevant item kept from the backward slice.