From 9abd0511bdad74578e08ac30d93762c83647dbd8 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sun, 26 Apr 2026 15:44:01 +0700
Subject: [PATCH] fix(verifier): refresh predicate errors per step

EvaluateProperties short-circuits once an Always-property latches to
violated, so the underlying goja predicate stops being called and
formula.err keeps whatever it threw at step 1. The runner logs
PredicateError every step a property is violated, which made every
subsequent log line repeat the step-1 throw. That looks like the spec
runtime is seeing stale state, but it is just stale error reporting.

EvaluateProperties now invokes every registered predicate once per step
purely to refresh formula.err. Verdicts are unaffected. The thunk
itself stops latching so the new value wins on whichever path runs first.
---
 internal/verifier/bindings.go |  7 ++++---
 internal/verifier/worker.go   | 24 +++++++++++++++++++++---
 2 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/internal/verifier/bindings.go b/internal/verifier/bindings.go
index f8facbe..6d67b0e 100644
--- a/internal/verifier/bindings.go
+++ b/internal/verifier/bindings.go
@@ -14,9 +14,10 @@ type extractorState struct {
 
 type formulaState struct {
 	predicate goja.Callable
-	// err latches the first goja error returned by predicate. The thunk
-	// returns false on error so the LTL evaluator marks the property
-	// violated; PredicateError surfaces the underlying cause.
+	// err holds the goja error from this thunk's most recent invocation, or
+	// nil if the latest call succeeded. The thunk returns false on error so
+	// the LTL evaluator marks the property violated; PredicateError surfaces
+	// the underlying cause for the current step.
 	err error
 }
 
diff --git a/internal/verifier/worker.go b/internal/verifier/worker.go
index 24fd683..d7ae7e4 100644
--- a/internal/verifier/worker.go
+++ b/internal/verifier/worker.go
@@ -254,6 +254,7 @@ func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict {
 	for name, evaluator := range v.evaluators {
 		verdicts[name] = evaluator.ObserveAt(stepTime)
 	}
+	v.refreshPredicateErrors()
 	return verdicts
 }
 
@@ -302,15 +303,32 @@ func (v *Verifier) formulaThunk(index int) func() bool {
 		formula := v.formulas[index]
 		result, err := formula.predicate(goja.Undefined())
 		if err != nil {
-			if formula.err == nil {
-				formula.err = err
-			}
+			formula.err = err
 			return false
 		}
+		formula.err = nil
 		return result.ToBoolean()
 	}
 }
 
+// refreshPredicateErrors re-invokes every registered predicate so that
+// formula.err reflects the current step rather than a latched first-step
+// throw. EvaluateProperties short-circuits once a property has latched to
+// 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.
+func (v *Verifier) refreshPredicateErrors() {
+	for _, formula := range v.formulas {
+		result, err := formula.predicate(goja.Undefined())
+		if err != nil {
+			formula.err = err
+			continue
+		}
+		_ = result
+		formula.err = nil
+	}
+}
+
 // PredicateError returns the first goja error raised by any thunk in the
 // named property's formula tree, or nil if none fired. Callers typically
 // consult this after EvaluateProperties reports a violation to distinguish