feat(ltl): formula AST and step evaluator for v0.1

Supports Always over Pure/Thunk leaves; eventually/next/bounds
deferred. Once a thunk returns false under an Always, the verdict
latches to violated so the runner can surface the offending step
without later observations masking it.

internal/ltl/evaluator.go

@@ -0,0 +1,60 @@
+package ltl
+
+import "fmt"
+
+type Verdict int
+
+const (
+	VerdictHolds Verdict = iota
+	VerdictViolated
+)
+
+func (v Verdict) String() string {
+	switch v {
+	case VerdictHolds:
+		return "holds"
+	case VerdictViolated:
+		return "violated"
+	default:
+		return fmt.Sprintf("verdict(%d)", int(v))
+	}
+}
+
+// Evaluator folds a formula across observed steps. v0.1 semantics:
+// Always(P) is satisfied if P held at every observed step; once P is false,
+// the verdict latches to Violated.
+type Evaluator struct {
+	formula  Formula
+	violated bool
+}
+
+func NewEvaluator(formula Formula) *Evaluator {
+	return &Evaluator{formula: formula}
+}
+
+// Observe evaluates the formula against the current state and returns the
+// running verdict. Once Violated, subsequent calls keep returning Violated
+// regardless of what later observations look like.
+func (e *Evaluator) Observe() Verdict {
+	if e.violated {
+		return VerdictViolated
+	}
+	if !holdsAtCurrentStep(e.formula) {
+		e.violated = true
+		return VerdictViolated
+	}
+	return VerdictHolds
+}
+
+func holdsAtCurrentStep(formula Formula) bool {
+	switch concrete := formula.(type) {
+	case AlwaysFormula:
+		return holdsAtCurrentStep(concrete.Inner)
+	case PureFormula:
+		return concrete.Value
+	case ThunkFormula:
+		return concrete.Func()
+	default:
+		panic(fmt.Sprintf("ltl: unsupported formula type %T", formula))
+	}
+}

internal/ltl/evaluator_test.go

@@ -0,0 +1,123 @@
+package ltl
+
+import (
+	"strings"
+	"testing"
+)
+
+func observe(formula Formula, count int) []Verdict {
+	evaluator := NewEvaluator(formula)
+	verdicts := make([]Verdict, 0, count)
+	for range count {
+		verdicts = append(verdicts, evaluator.Observe())
+	}
+	return verdicts
+}
+
+func TestPure_HoldsThenStays(t *testing.T) {
+	got := observe(Always(Pure(true)), 3)
+	for index, verdict := range got {
+		if verdict != VerdictHolds {
+			t.Errorf("step %d: got %v, want holds", index, verdict)
+		}
+	}
+}
+
+func TestPure_FalseImmediatelyViolates(t *testing.T) {
+	got := observe(Always(Pure(false)), 3)
+	for index, verdict := range got {
+		if verdict != VerdictViolated {
+			t.Errorf("step %d: got %v, want violated", index, verdict)
+		}
+	}
+}
+
+func TestThunk_TransitionFromHoldToViolate(t *testing.T) {
+	values := []bool{true, true, false, true, true}
+	step := 0
+	evaluator := NewEvaluator(Always(Thunk(func() bool {
+		current := values[step]
+		step++
+		return current
+	})))
+
+	wantSequence := []Verdict{
+		VerdictHolds,    // true
+		VerdictHolds,    // true
+		VerdictViolated, // false — latches
+		VerdictViolated, // true after violation — still violated
+		VerdictViolated, // true after violation — still violated
+	}
+	for index, want := range wantSequence {
+		got := evaluator.Observe()
+		if got != want {
+			t.Errorf("step %d: got %v, want %v", index, got, want)
+		}
+	}
+}
+
+func TestEvaluator_StickinessAfterViolation(t *testing.T) {
+	state := true
+	evaluator := NewEvaluator(Always(Thunk(func() bool { return state })))
+
+	if got := evaluator.Observe(); got != VerdictHolds {
+		t.Fatalf("step 1: got %v, want holds", got)
+	}
+	state = false
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Fatalf("step 2: got %v, want violated", got)
+	}
+	state = true
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Fatalf("step 3 (recovered state): violation should latch, got %v", got)
+	}
+}
+
+func TestEvaluator_TopLevelPureCountedAtEachStep(t *testing.T) {
+	got := observe(Pure(true), 2)
+	if got[0] != VerdictHolds || got[1] != VerdictHolds {
+		t.Errorf("bare Pure(true): %v", got)
+	}
+}
+
+func TestEvaluator_TopLevelThunkRespectsObservation(t *testing.T) {
+	state := true
+	evaluator := NewEvaluator(Thunk(func() bool { return state }))
+	if got := evaluator.Observe(); got != VerdictHolds {
+		t.Errorf("expected holds, got %v", got)
+	}
+	state = false
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Errorf("expected violated, got %v", got)
+	}
+}
+
+func TestVerdict_String(t *testing.T) {
+	if VerdictHolds.String() != "holds" {
+		t.Errorf("VerdictHolds.String() = %q", VerdictHolds.String())
+	}
+	if VerdictViolated.String() != "violated" {
+		t.Errorf("VerdictViolated.String() = %q", VerdictViolated.String())
+	}
+}
+
+func TestDescribe(t *testing.T) {
+	formula := Always(Pure(true))
+	if got := Describe(formula); !strings.Contains(got, "Always") || !strings.Contains(got, "Pure(true)") {
+		t.Errorf("Describe wrong: %q", got)
+	}
+	thunk := Always(Thunk(func() bool { return true }))
+	if got := Describe(thunk); !strings.Contains(got, "Thunk") {
+		t.Errorf("Describe(thunk) wrong: %q", got)
+	}
+}
+
+func TestObserve_PanicsOnUnknownFormulaType(t *testing.T) {
+	type unsupportedFormula struct{ Formula }
+	defer func() {
+		if recovered := recover(); recovered == nil {
+			t.Errorf("expected panic on unsupported formula type")
+		}
+	}()
+	holdsAtCurrentStep(unsupportedFormula{})
+}

internal/ltl/formula.go

@@ -0,0 +1,40 @@
+package ltl
+
+import "fmt"
+
+// Formula is the AST of a temporal logic property. v0.1 supports only Always
+// over Pure/Thunk leaves; eventually, next, and bounded operators are
+// deferred to v0.2+.
+type Formula interface {
+	isFormula()
+	describe() string
+}
+
+type AlwaysFormula struct {
+	Inner Formula
+}
+
+type PureFormula struct {
+	Value bool
+}
+
+type ThunkFormula struct {
+	Func func() bool
+}
+
+func Always(inner Formula) Formula { return AlwaysFormula{Inner: inner} }
+
+func Pure(value bool) Formula { return PureFormula{Value: value} }
+
+func Thunk(function func() bool) Formula { return ThunkFormula{Func: function} }
+
+func (AlwaysFormula) isFormula() {}
+func (PureFormula) isFormula()   {}
+func (ThunkFormula) isFormula()  {}
+
+func (a AlwaysFormula) describe() string { return "Always(" + a.Inner.describe() + ")" }
+func (p PureFormula) describe() string   { return fmt.Sprintf("Pure(%t)", p.Value) }
+func (ThunkFormula) describe() string    { return "Thunk(...)" }
+
+// Describe returns a debug-friendly representation of the formula.
+func Describe(formula Formula) string { return formula.describe() }