From 237ce6975a6251593633cbc7c677854fa2ea530e Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 6 Jun 2026 12:46:06 +0530
Subject: [PATCH] test(verifier): cover LTL combinator verdict transitions and
 within unit panic

---
 internal/verifier/combinator_test.go | 118 +++++++++++++++++++++++++++
 1 file changed, 118 insertions(+)
 create mode 100644 internal/verifier/combinator_test.go

diff --git a/internal/verifier/combinator_test.go b/internal/verifier/combinator_test.go
new file mode 100644
index 0000000..ad20501
--- /dev/null
+++ b/internal/verifier/combinator_test.go
@@ -0,0 +1,118 @@
+package verifier
+
+import (
+	"encoding/json"
+	"strings"
+	"testing"
+
+	"github.com/priyanshujain/sanderling/internal/ltl"
+)
+
+// TestCombinators_VerdictTransitions loads real specs through the goja runtime
+// using the chainable LTL combinators (implies/or/and/not + now + within steps)
+// and drives them across snapshots. Bug class: a user spec built from these
+// combinators silently mis-evaluates (wrong verdict at the wrong step).
+func TestCombinators_VerdictTransitions(t *testing.T) {
+	const heads = `
+globalThis.p = __sanderling__.extract(state => state.snapshots["p"] ?? false, "p");
+globalThis.q = __sanderling__.extract(state => state.snapshots["q"] ?? false, "q");
+`
+	type step struct {
+		p, q string
+		want ltl.Verdict
+	}
+	cases := []struct {
+		name  string
+		body  string
+		steps []step
+	}{
+		{
+			name: "implies",
+			body: `globalThis.properties = { r: __sanderling__.always(__sanderling__.now(()=>p.current).implies(__sanderling__.now(()=>q.current))) };`,
+			steps: []step{
+				{"false", "false", ltl.VerdictHolds}, // antecedent false -> vacuously holds
+				{"true", "true", ltl.VerdictHolds},
+				{"true", "false", ltl.VerdictViolated},  // p true, q false
+				{"false", "false", ltl.VerdictViolated}, // sticky
+			},
+		},
+		{
+			name: "or",
+			body: `globalThis.properties = { r: __sanderling__.always(__sanderling__.now(()=>p.current).or(__sanderling__.now(()=>q.current))) };`,
+			steps: []step{
+				{"true", "false", ltl.VerdictHolds},
+				{"false", "true", ltl.VerdictHolds},
+				{"false", "false", ltl.VerdictViolated},
+			},
+		},
+		{
+			name: "and",
+			body: `globalThis.properties = { r: __sanderling__.always(__sanderling__.now(()=>p.current).and(__sanderling__.now(()=>q.current))) };`,
+			steps: []step{
+				{"true", "true", ltl.VerdictHolds},
+				{"true", "false", ltl.VerdictViolated}, // one conjunct false
+			},
+		},
+		{
+			name: "not",
+			body: `globalThis.properties = { r: __sanderling__.always(__sanderling__.now(()=>p.current).not()) };`,
+			steps: []step{
+				{"false", "false", ltl.VerdictHolds},
+				{"true", "false", ltl.VerdictViolated},
+			},
+		},
+		{
+			name: "within_steps_deadline",
+			body: `globalThis.properties = { r: __sanderling__.always(__sanderling__.eventually(()=>p.current).within(2,'steps')) };`,
+			steps: []step{
+				{"false", "false", ltl.VerdictPending},  // obligation open
+				{"false", "false", ltl.VerdictViolated}, // deadline blown, never fired
+			},
+		},
+		{
+			name: "within_steps_satisfied",
+			body: `globalThis.properties = { r: __sanderling__.always(__sanderling__.eventually(()=>p.current).within(2,'steps')) };`,
+			steps: []step{
+				{"false", "false", ltl.VerdictPending},
+				{"true", "false", ltl.VerdictHolds}, // fired before deadline
+			},
+		},
+	}
+
+	for _, testCase := range cases {
+		t.Run(testCase.name, func(t *testing.T) {
+			verifier := newVerifier(t)
+			mustLoad(t, verifier, heads+testCase.body)
+			for i, s := range testCase.steps {
+				if err := verifier.PushSnapshot(SnapshotInput{
+					Snapshots: Snapshots{"p": json.RawMessage(s.p), "q": json.RawMessage(s.q)},
+					StepIndex: i + 1,
+				}); err != nil {
+					t.Fatal(err)
+				}
+				if got := verifier.EvaluateProperties()["r"]; got != s.want {
+					t.Errorf("step %d (p=%s q=%s): got %v, want %v", i+1, s.p, s.q, got, s.want)
+				}
+			}
+		})
+	}
+}
+
+// TestWithin_InvalidUnitPanics verifies an unrecognized within() unit surfaces
+// as a spec load error rather than silently constructing an unbounded
+// eventually. Bug class: a typo'd unit ('ms'/'s') would otherwise build a
+// formula that never enforces its deadline.
+func TestWithin_InvalidUnitPanics(t *testing.T) {
+	for _, unit := range []string{"ms", "s", "minutes", ""} {
+		verifier := newVerifier(t)
+		src := `globalThis.properties = { r: __sanderling__.always(__sanderling__.eventually(()=>true).within(2,'` + unit + `')) };`
+		err := verifier.Load(src)
+		if err == nil {
+			t.Errorf("unit %q: expected load error, got nil", unit)
+			continue
+		}
+		if !strings.Contains(err.Error(), "within unit must be") {
+			t.Errorf("unit %q: error = %v, want within-unit diagnostic", unit, err)
+		}
+	}
+}