Files
sanderling/internal/verifier
pj 569e0c818e docs(verifier): document extractor advancement and refresh invariants
Extractor previous/current advance only on PushSnapshot, never per
thunk-call. refreshPredicateErrors depends on this for safe re-entry.
Also flags that re-invoked predicates run outside their LTL gate, so
they must be side-effect-free reads.
2026-04-26 22:19:32 +07:00
..