From 569e0c818e7c8e098c9ba85d9e8b8fe2f77f340a Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 26 Apr 2026 22:19:32 +0700 Subject: [PATCH] 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. --- internal/verifier/worker.go | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/internal/verifier/worker.go b/internal/verifier/worker.go index d7ae7e4..3e2c319 100644 --- a/internal/verifier/worker.go +++ b/internal/verifier/worker.go @@ -216,6 +216,10 @@ func (v *Verifier) PushSnapshot(input SnapshotInput) error { if err := v.runtime.GlobalObject().Set("state", state); err != nil { return fmt.Errorf("set state: %w", err) } + // Extractor previous/current advance exactly once per PushSnapshot. + // Predicate thunks read these slots but never trigger advancement, so + // invoking a thunk multiple times between snapshots is value-stable. + // refreshPredicateErrors relies on this to safely re-call predicates. for index, extractor := range v.extractors { previous := extractor.handle.Get("current") _ = extractor.handle.Set("previous", previous) @@ -317,6 +321,12 @@ func (v *Verifier) formulaThunk(index int) func() bool { // violated, so without this refresh the runner's per-step "predicate error" // log freezes on whatever the predicate threw at step 1. The refreshed errors // have no effect on verdicts. +// +// Invariant: predicates may be re-invoked here outside the LTL gate that +// would normally skip them (e.g. an `implies` consequent whose antecedent is +// false). They must therefore be side-effect-free reads of extractor state; +// any spec that asserts internal preconditions inside a predicate could +// surface a spurious error in the inspect UI without affecting verdicts. func (v *Verifier) refreshPredicateErrors() { for _, formula := range v.formulas { result, err := formula.predicate(goja.Undefined())