feat: LTL operators, sampling, and default generators (#17)

* feat(ltl): add Now/Next/Eventually/Implies/Or/And/Not formulas

Replace the fold-with-latch evaluator with a residual-formula reducer.
Each Observe() instantiates a fresh obligation from the root (stripping
an outer Always), reduces each pending obligation against current state,
latches Violated on first failure, and surfaces Pending verdicts for
deferred obligations. Existing Always/Pure/Thunk tests continue to pass.

* feat(ltl): support relative duration for eventually().within()

* feat(proto): add Swipe, PressKey, RecentLogs RPCs

* feat(verifier,runner): formula handles, new action kinds, rich state

- verifier: add formula-spec registry; bindNow/bindNext/bindEventually with
  chainable .implies/.or/.and/.not and .within(n,unit) on eventually; bindFrom
  for uniform sampling. bindAlways keeps accepting plain predicates.
- verifier: store lastTree, lastAction, step time, logs, exceptions on the
  Verifier; SnapshotInput replaces the (snapshots, tree) pair. stateObject now
  produces state.lastAction/time/logs/exceptions matching the TS State type.
- verifier: make taps/swipes/waitOnce/pressKey built-in generators actually
  fire; taps picks a clickable, enabled element from the last hierarchy.
- agent: add exceptions field to Message wire format.
- driver: add Swipe/PressKey/RecentLogs to Driver interface; wire maestro
  client and mock driver. LogEntry exposed for runner consumption.
- runner: apply Swipe/PressKey/Wait actions; collect logcat and exceptions;
  pass lastAction and step time into PushSnapshot.

* feat(spec-api): LTL operators, new actions, richer State

- ltl.ts exports now/next/eventually; always overload accepts a Formula
- types.ts: Formula gains implies/or/and/not; EventuallyFormula adds .within;
  State gains lastAction/time/logs/exceptions; Swipe/PressKey/Wait action types
- actions.ts: Swipe/PressKey/Wait/from constructors; waitOnce + pressKey
  default generators
- tests exercise the chaining, sampling, and new actions through a recorded
  fake runtime

* feat(sidecar): add swipe, pressKey, recentLogs RPC handlers

* feat(sdk-android): capture uncaught exceptions

Install a default uncaught handler on Uatu.start, chained with any
existing handler so Android's crash reporter still runs. Expose
Uatu.reportError for callers to forward caught throwables. A bounded
circular buffer (default 50) drains into each STATE message's new
exceptions field. Protocol.kt serializes/deserializes the field,
matching the Go wire format added to internal/agent/protocol.go.

* feat(spec-api): add @uatu/spec/defaults/properties bundle

* feat(sample-app): exercise new LTL operators + defaults

spec.ts now imports eventually/next/now/from from @uatu/spec and
noUncaughtExceptions from @uatu/spec/defaults/properties. It declares
three properties that exercise the new surface:

- accountCountNonNegative: plain always() safety
- addAccountAdvances: always(now(x).implies(next(y)))
- eventuallyLoggedIn: eventually(p).within(30, "seconds")
- noUncaughtExceptions: imported default

The weighted actions root uses from() for random phone/name sampling
and entries for taps/swipes/waitOnce/pressKey built-ins.

SampleApplication gains a debug hook gated on the system property
uatu.inject_error so the e2e run can synthesize an Uatu.reportError and
verify noUncaughtExceptions violates.

cmd/uatu/test_run.go adds a subpath alias so specs importing
"@uatu/spec/defaults/properties" resolve against the in-tree source
when running from the uatu checkout. The spec-integration tests swap
the old click-counter fixtures for the new login hierarchy.

* feat(trace): record swipe/key/wait details + exceptions

trace.Step gains an Exceptions array so the trace captures the
class/message/stackTrace for each SDK-reported throwable in a step.
trace.Action gains FromX/FromY/ToX/ToY/Key/DurationMillis so the full
payload of Swipe/PressKey/Wait actions is visible in trace.jsonl.

sample-app's debug error hook now gates on ApplicationInfo.DEBUGGABLE
instead of a system property (adb setprop fails on non-rooted
emulators).

internal/agent/protocol.go

@@ -34,7 +34,8 @@ type Message struct {
 	Platform        string `json:"platform,omitempty"`
 	AppPackage      string `json:"app_package,omitempty"`
 
-	Snapshots map[string]json.RawMessage `json:"snapshots,omitempty"`
+	Snapshots  map[string]json.RawMessage `json:"snapshots,omitempty"`
+	Exceptions []Exception                `json:"exceptions,omitempty"`
 
 	Extractor string          `json:"extractor,omitempty"`
 	Result    json.RawMessage `json:"result,omitempty"`
@@ -43,6 +44,14 @@ type Message struct {
 	Reason string `json:"reason,omitempty"`
 }
 
+// Exception mirrors an uncaught throwable captured by the SDK.
+type Exception struct {
+	Class      string `json:"class"`
+	Message    string `json:"message,omitempty"`
+	StackTrace string `json:"stack_trace,omitempty"`
+	UnixMillis int64  `json:"unix_millis,omitempty"`
+}
+
 func Hello(version, platform, appPackage string) Message {
 	return Message{
 		Type:            MessageTypeHello,

internal/driver/driver.go

@@ -19,14 +19,26 @@ type Driver interface {
 	Tap(ctx context.Context, x, y int) error
 	TapSelector(ctx context.Context, selector string) error
 	InputText(ctx context.Context, text string) error
+	Swipe(ctx context.Context, fromX, fromY, toX, toY int, duration time.Duration) error
+	PressKey(ctx context.Context, key string) error
 
 	Hierarchy(ctx context.Context) (string, error)
 	Screenshot(ctx context.Context) (Image, error)
+	// RecentLogs returns logcat entries at or after `since`, filtered to
+	// `minLevel` or above. An empty minLevel defaults to "E".
+	RecentLogs(ctx context.Context, since time.Time, minLevel string) ([]LogEntry, error)
 
 	WaitForIdle(ctx context.Context, duration time.Duration) error
 	Health(ctx context.Context) (Health, error)
 }
 
+type LogEntry struct {
+	UnixMillis int64
+	Level      string
+	Tag        string
+	Message    string
+}
+
 type Image struct {
 	PNG    []byte
 	Width  int

internal/driver/maestro/client.go

@@ -77,6 +77,45 @@ func (c *Client) InputText(ctx context.Context, text string) error {
 	return err
 }
 
+func (c *Client) Swipe(ctx context.Context, fromX, fromY, toX, toY int, duration time.Duration) error {
+	_, err := c.stub.Swipe(ctx, &driverpb.SwipeRequest{
+		From:           &driverpb.Point{X: int32(fromX), Y: int32(fromY)},
+		To:             &driverpb.Point{X: int32(toX), Y: int32(toY)},
+		DurationMillis: duration.Milliseconds(),
+	})
+	return err
+}
+
+func (c *Client) PressKey(ctx context.Context, key string) error {
+	_, err := c.stub.PressKey(ctx, &driverpb.PressKeyRequest{Key: key})
+	return err
+}
+
+func (c *Client) RecentLogs(ctx context.Context, since time.Time, minLevel string) ([]driver.LogEntry, error) {
+	sinceMillis := int64(0)
+	if !since.IsZero() {
+		sinceMillis = since.UnixMilli()
+	}
+	response, err := c.stub.RecentLogs(ctx, &driverpb.RecentLogsRequest{
+		SinceUnixMillis: sinceMillis,
+		LevelAtLeast:    minLevel,
+	})
+	if err != nil {
+		return nil, err
+	}
+	entries := response.GetEntries()
+	result := make([]driver.LogEntry, 0, len(entries))
+	for _, entry := range entries {
+		result = append(result, driver.LogEntry{
+			UnixMillis: entry.GetUnixMillis(),
+			Level:      entry.GetLevel(),
+			Tag:        entry.GetTag(),
+			Message:    entry.GetMessage(),
+		})
+	}
+	return result, nil
+}
+
 func (c *Client) Hierarchy(ctx context.Context) (string, error) {
 	response, err := c.stub.Hierarchy(ctx, &driverpb.Empty{})
 	if err != nil {

internal/driver/mock/mock.go

@@ -16,8 +16,11 @@ const (
 	ActionTap         ActionKind = "tap"
 	ActionTapSelector ActionKind = "tap_selector"
 	ActionInputText   ActionKind = "input_text"
+	ActionSwipe       ActionKind = "swipe"
+	ActionPressKey    ActionKind = "press_key"
 	ActionHierarchy   ActionKind = "hierarchy"
 	ActionScreenshot  ActionKind = "screenshot"
+	ActionRecentLogs  ActionKind = "recent_logs"
 	ActionWaitForIdle ActionKind = "wait_for_idle"
 	ActionHealth      ActionKind = "health"
 )
@@ -28,8 +31,14 @@ type Action struct {
 	LauncherActivity string
 	ClearState       bool
 	X, Y             int
+	FromX, FromY     int
+	ToX, ToY         int
+	Duration         time.Duration
 	Selector         string
 	Text             string
+	Key              string
+	LogLevel         string
+	LogSince         time.Time
 	Idle             time.Duration
 }
 
@@ -43,6 +52,7 @@ type Driver struct {
 	HierarchyJSON string
 	ImageData     driver.Image
 	HealthInfo    driver.Health
+	LogEntries    []driver.LogEntry
 	Failures      map[ActionKind]error
 }
 
@@ -117,6 +127,39 @@ func (d *Driver) InputText(ctx context.Context, text string) error {
 	return nil
 }
 
+func (d *Driver) Swipe(ctx context.Context, fromX, fromY, toX, toY int, duration time.Duration) error {
+	if err := d.failure(ActionSwipe); err != nil {
+		return err
+	}
+	d.record(Action{
+		Kind:     ActionSwipe,
+		FromX:    fromX,
+		FromY:    fromY,
+		ToX:      toX,
+		ToY:      toY,
+		Duration: duration,
+	})
+	return nil
+}
+
+func (d *Driver) PressKey(ctx context.Context, key string) error {
+	if err := d.failure(ActionPressKey); err != nil {
+		return err
+	}
+	d.record(Action{Kind: ActionPressKey, Key: key})
+	return nil
+}
+
+func (d *Driver) RecentLogs(ctx context.Context, since time.Time, minLevel string) ([]driver.LogEntry, error) {
+	if err := d.failure(ActionRecentLogs); err != nil {
+		return nil, err
+	}
+	d.record(Action{Kind: ActionRecentLogs, LogSince: since, LogLevel: minLevel})
+	d.mutex.Lock()
+	defer d.mutex.Unlock()
+	return append([]driver.LogEntry(nil), d.LogEntries...), nil
+}
+
 func (d *Driver) Hierarchy(ctx context.Context) (string, error) {
 	if err := d.failure(ActionHierarchy); err != nil {
 		return "", err

internal/ltl/evaluator.go

@@ -1,12 +1,16 @@
 package ltl
 
-import "fmt"
+import (
+	"fmt"
+	"time"
+)
 
 type Verdict int
 
 const (
 	VerdictHolds Verdict = iota
 	VerdictViolated
+	VerdictPending
 )
 
 func (v Verdict) String() string {
@@ -15,46 +19,210 @@ func (v Verdict) String() string {
 		return "holds"
 	case VerdictViolated:
 		return "violated"
+	case VerdictPending:
+		return "pending"
 	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.
+// Evaluator reduces a formula across observed steps using residual-formula
+// semantics. Each step either resolves pending obligations (to holds or
+// violated) or carries them forward as residuals. Once a single obligation
+// violates, the overall verdict latches to Violated.
 type Evaluator struct {
-	formula  Formula
+	root     Formula
+	pending  []Formula
 	violated bool
 }
 
 func NewEvaluator(formula Formula) *Evaluator {
-	return &Evaluator{formula: formula}
+	return &Evaluator{root: 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.
+// running verdict. Uses the real wall clock for deadline-bound operators;
+// callers that need reproducible time should use ObserveAt.
 func (e *Evaluator) Observe() Verdict {
+	return e.ObserveAt(time.Now())
+}
+
+// ObserveAt is like Observe but takes the current step time explicitly.
+func (e *Evaluator) ObserveAt(now time.Time) Verdict {
 	if e.violated {
 		return VerdictViolated
 	}
-	if !holdsAtCurrentStep(e.formula) {
-		e.violated = true
-		return VerdictViolated
+
+	fresh := rootObligation(e.root)
+	obligations := append(e.pending, fresh)
+	e.pending = e.pending[:0]
+
+	for _, obligation := range obligations {
+		result := reduce(obligation, now)
+		switch result.status {
+		case statusHolds:
+			// drop
+		case statusViolated:
+			e.violated = true
+			e.pending = nil
+			return VerdictViolated
+		case statusPending:
+			e.pending = append(e.pending, result.formula)
+		}
+	}
+
+	if len(e.pending) > 0 {
+		return VerdictPending
 	}
 	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))
+// rootObligation returns the formula to instantiate at each step. An outer
+// Always is stripped so its inner is re-evaluated every step; any other root
+// formula is itself re-instantiated each step (matching the v0.1 semantics
+// where a bare Thunk is re-observed on every call).
+func rootObligation(root Formula) Formula {
+	if always, ok := root.(AlwaysFormula); ok {
+		return always.Inner
 	}
+	return root
+}
+
+type residualStatus int
+
+const (
+	statusHolds residualStatus = iota
+	statusViolated
+	statusPending
+)
+
+type reduceResult struct {
+	status  residualStatus
+	formula Formula
+}
+
+func holds() reduceResult    { return reduceResult{status: statusHolds} }
+func violated() reduceResult { return reduceResult{status: statusViolated} }
+func pending(f Formula) reduceResult {
+	return reduceResult{status: statusPending, formula: f}
+}
+
+func reduce(formula Formula, now time.Time) reduceResult {
+	switch concrete := formula.(type) {
+	case PureFormula:
+		if concrete.Value {
+			return holds()
+		}
+		return violated()
+
+	case ThunkFormula:
+		if concrete.Func() {
+			return holds()
+		}
+		return violated()
+
+	case NowFormula:
+		return reduce(concrete.Inner, now)
+
+	case NextFormula:
+		// Next defers the inner obligation to the following step without
+		// evaluating it now.
+		return pending(concrete.Inner)
+
+	case EventuallyFormula:
+		// First-reduction deadline resolution: if the formula was built with
+		// a relative duration, fix the absolute deadline to (now + duration)
+		// so subsequent reductions compare against a stable value.
+		if !concrete.HasDeadline && concrete.Duration > 0 {
+			concrete.Deadline = now.Add(concrete.Duration)
+			concrete.HasDeadline = true
+		}
+		innerResult := reduce(concrete.Inner, now)
+		if innerResult.status == statusHolds {
+			return holds()
+		}
+		if concrete.HasStepBound && concrete.StepBound <= 1 {
+			return violated()
+		}
+		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
+			return violated()
+		}
+		next := concrete
+		if concrete.HasStepBound {
+			next.StepBound = concrete.StepBound - 1
+		}
+		return pending(next)
+
+	case ImpliesFormula:
+		antecedent := reduce(concrete.Antecedent, now)
+		switch antecedent.status {
+		case statusHolds:
+			return reduce(concrete.Consequent, now)
+		case statusViolated:
+			return holds()
+		case statusPending:
+			return pending(ImpliesFormula{
+				Antecedent: antecedent.formula,
+				Consequent: concrete.Consequent,
+			})
+		}
+
+	case OrFormula:
+		left := reduce(concrete.Left, now)
+		right := reduce(concrete.Right, now)
+		if left.status == statusHolds || right.status == statusHolds {
+			return holds()
+		}
+		if left.status == statusViolated && right.status == statusViolated {
+			return violated()
+		}
+		if left.status == statusViolated {
+			return pending(right.formula)
+		}
+		if right.status == statusViolated {
+			return pending(left.formula)
+		}
+		return pending(OrFormula{Left: left.formula, Right: right.formula})
+
+	case AndFormula:
+		left := reduce(concrete.Left, now)
+		right := reduce(concrete.Right, now)
+		if left.status == statusViolated || right.status == statusViolated {
+			return violated()
+		}
+		if left.status == statusHolds && right.status == statusHolds {
+			return holds()
+		}
+		if left.status == statusHolds {
+			return pending(right.formula)
+		}
+		if right.status == statusHolds {
+			return pending(left.formula)
+		}
+		return pending(AndFormula{Left: left.formula, Right: right.formula})
+
+	case NotFormula:
+		inner := reduce(concrete.Inner, now)
+		switch inner.status {
+		case statusHolds:
+			return violated()
+		case statusViolated:
+			return holds()
+		case statusPending:
+			return pending(NotFormula{Inner: inner.formula})
+		}
+
+	case AlwaysFormula:
+		innerResult := reduce(concrete.Inner, now)
+		if innerResult.status == statusViolated {
+			return violated()
+		}
+		next := AlwaysFormula{Inner: concrete.Inner}
+		if innerResult.status == statusHolds {
+			return pending(next)
+		}
+		return pending(AndFormula{Left: innerResult.formula, Right: next})
+	}
+
+	panic(fmt.Sprintf("ltl: unsupported formula type %T", formula))
 }

internal/ltl/evaluator_test.go

@@ -3,6 +3,7 @@ package ltl
 import (
 	"strings"
 	"testing"
+	"time"
 )
 
 func observe(formula Formula, count int) []Verdict {
@@ -119,5 +120,5 @@ func TestObserve_PanicsOnUnknownFormulaType(t *testing.T) {
 			t.Errorf("expected panic on unsupported formula type")
 		}
 	}()
-	holdsAtCurrentStep(unsupportedFormula{})
+	reduce(unsupportedFormula{}, time.Now())
 }

internal/ltl/formula.go

@@ -1,10 +1,12 @@
 package ltl
 
-import "fmt"
+import (
+	"fmt"
+	"strings"
+	"time"
+)
 
-// 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+.
+// Formula is the AST of a temporal logic property.
 type Formula interface {
 	isFormula()
 	describe() string
@@ -22,19 +24,125 @@ type ThunkFormula struct {
 	Func func() bool
 }
 
+// NowFormula marks its inner formula for evaluation at the current step only.
+// Primarily used so that now(...).implies(...) parses unambiguously.
+type NowFormula struct {
+	Inner Formula
+}
+
+// NextFormula obliges its inner formula to hold at the next step (not this one).
+type NextFormula struct {
+	Inner Formula
+}
+
+// EventuallyFormula obliges its inner formula to hold at some step within the
+// given bound. An unbounded eventually never triggers a violation within a
+// finite run.
+//
+// When Duration is non-zero and Deadline is the zero time, the evaluator
+// resolves the absolute deadline on first reduction using the observation
+// time. This matches the "within N seconds of obligation instantiation"
+// semantics used by nested Always(Eventually(...).within(...)) formulas.
+type EventuallyFormula struct {
+	Inner        Formula
+	StepBound    int
+	HasStepBound bool
+	Duration     time.Duration
+	Deadline     time.Time
+	HasDeadline  bool
+}
+
+type ImpliesFormula struct {
+	Antecedent Formula
+	Consequent Formula
+}
+
+type OrFormula struct {
+	Left  Formula
+	Right Formula
+}
+
+type AndFormula struct {
+	Left  Formula
+	Right Formula
+}
+
+type NotFormula struct {
+	Inner Formula
+}
+
 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 Now(inner Formula) Formula { return NowFormula{Inner: inner} }
+
+func Next(inner Formula) Formula { return NextFormula{Inner: inner} }
+
+func Eventually(inner Formula) Formula { return EventuallyFormula{Inner: inner} }
+
+func EventuallyWithinSteps(inner Formula, steps int) Formula {
+	return EventuallyFormula{Inner: inner, StepBound: steps, HasStepBound: true}
+}
+
+func EventuallyBefore(inner Formula, deadline time.Time) Formula {
+	return EventuallyFormula{Inner: inner, Deadline: deadline, HasDeadline: true}
+}
+
+func EventuallyWithin(inner Formula, duration time.Duration) Formula {
+	return EventuallyFormula{Inner: inner, Duration: duration}
+}
+
+func Implies(antecedent, consequent Formula) Formula {
+	return ImpliesFormula{Antecedent: antecedent, Consequent: consequent}
+}
+
+func Or(left, right Formula) Formula { return OrFormula{Left: left, Right: right} }
+
+func And(left, right Formula) Formula { return AndFormula{Left: left, Right: right} }
+
+func Not(inner Formula) Formula { return NotFormula{Inner: inner} }
+
+func (AlwaysFormula) isFormula()     {}
+func (PureFormula) isFormula()       {}
+func (ThunkFormula) isFormula()      {}
+func (NowFormula) isFormula()        {}
+func (NextFormula) isFormula()       {}
+func (EventuallyFormula) isFormula() {}
+func (ImpliesFormula) isFormula()    {}
+func (OrFormula) isFormula()         {}
+func (AndFormula) isFormula()        {}
+func (NotFormula) 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(...)" }
+func (n NowFormula) describe() string    { return "Now(" + n.Inner.describe() + ")" }
+func (n NextFormula) describe() string   { return "Next(" + n.Inner.describe() + ")" }
+func (e EventuallyFormula) describe() string {
+	parts := []string{e.Inner.describe()}
+	if e.HasStepBound {
+		parts = append(parts, fmt.Sprintf("steps=%d", e.StepBound))
+	}
+	if e.HasDeadline {
+		parts = append(parts, "deadline="+e.Deadline.Format(time.RFC3339Nano))
+	} else if e.Duration > 0 {
+		parts = append(parts, "within="+e.Duration.String())
+	}
+	return "Eventually(" + strings.Join(parts, ", ") + ")"
+}
+func (i ImpliesFormula) describe() string {
+	return "Implies(" + i.Antecedent.describe() + ", " + i.Consequent.describe() + ")"
+}
+func (o OrFormula) describe() string {
+	return "Or(" + o.Left.describe() + ", " + o.Right.describe() + ")"
+}
+func (a AndFormula) describe() string {
+	return "And(" + a.Left.describe() + ", " + a.Right.describe() + ")"
+}
+func (n NotFormula) describe() string { return "Not(" + n.Inner.describe() + ")" }
 
 // Describe returns a debug-friendly representation of the formula.
 func Describe(formula Formula) string { return formula.describe() }

internal/ltl/formula_test.go

@@ -0,0 +1,193 @@
+package ltl
+
+import (
+	"strings"
+	"testing"
+	"time"
+)
+
+func TestDescribe_NowNextEventually(t *testing.T) {
+	now := Always(Now(Pure(true)))
+	if got := Describe(now); !strings.Contains(got, "Now") || !strings.Contains(got, "Always") {
+		t.Errorf("Describe(Always(Now(Pure(true)))) = %q", got)
+	}
+	next := Always(Next(Pure(false)))
+	if got := Describe(next); !strings.Contains(got, "Next") {
+		t.Errorf("Describe next = %q", got)
+	}
+	ev := Always(EventuallyWithinSteps(Pure(true), 3))
+	if got := Describe(ev); !strings.Contains(got, "Eventually") || !strings.Contains(got, "steps=3") {
+		t.Errorf("Describe eventually = %q", got)
+	}
+}
+
+func TestDescribe_ImpliesOrAndNot(t *testing.T) {
+	implies := Implies(Pure(true), Pure(false))
+	if got := Describe(implies); !strings.Contains(got, "Implies") {
+		t.Errorf("Describe implies = %q", got)
+	}
+	or := Or(Pure(true), Pure(false))
+	if got := Describe(or); !strings.Contains(got, "Or") {
+		t.Errorf("Describe or = %q", got)
+	}
+	and := And(Pure(true), Pure(false))
+	if got := Describe(and); !strings.Contains(got, "And") {
+		t.Errorf("Describe and = %q", got)
+	}
+	not := Not(Pure(true))
+	if got := Describe(not); !strings.Contains(got, "Not") {
+		t.Errorf("Describe not = %q", got)
+	}
+}
+
+func TestAlways_Now_ViolatesImmediately(t *testing.T) {
+	evaluator := NewEvaluator(Always(Now(Pure(false))))
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Errorf("step 1: got %v, want violated", got)
+	}
+}
+
+func TestAlways_Next_PendingThenViolated(t *testing.T) {
+	y := true
+	evaluator := NewEvaluator(Always(Next(Thunk(func() bool { return y }))))
+
+	if got := evaluator.Observe(); got != VerdictPending {
+		t.Errorf("step 1: got %v, want pending", got)
+	}
+	y = false
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Errorf("step 2: got %v, want violated", got)
+	}
+}
+
+func TestAlways_Next_StaysPendingWhileInnerHolds(t *testing.T) {
+	evaluator := NewEvaluator(Always(Next(Thunk(func() bool { return true }))))
+	for index := range 3 {
+		if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending {
+			t.Errorf("step %d: got %v, want pending", index+1, got)
+		}
+	}
+}
+
+func TestAlways_NowImpliesEventuallyWithin_ViolatesWhenYLate(t *testing.T) {
+	// always(now(() => x).implies(eventually(() => y).within(3, "steps")))
+	// x = true only at step 1; y = true only at step 4.
+	xValues := []bool{true, false, false, false, false}
+	yValues := []bool{false, false, false, true, true}
+	step := 0
+	predX := Thunk(func() bool { return xValues[step] })
+	predY := Thunk(func() bool { return yValues[step] })
+
+	formula := Always(Implies(Now(predX), EventuallyWithinSteps(predY, 3)))
+	evaluator := NewEvaluator(formula)
+
+	verdicts := make([]Verdict, 0, 5)
+	for range 5 {
+		verdicts = append(verdicts, evaluator.Observe())
+		step++
+	}
+
+	// Step 1: X true, eventually(Y, 3) spawned pending. Pending.
+	// Step 2: pending eventually decrements (Y false). Pending.
+	// Step 3: eventually bound exhausted (Y still false). Violated.
+	if verdicts[0] != VerdictPending {
+		t.Errorf("step 1: got %v, want pending", verdicts[0])
+	}
+	if verdicts[1] != VerdictPending {
+		t.Errorf("step 2: got %v, want pending", verdicts[1])
+	}
+	if verdicts[2] != VerdictViolated {
+		t.Errorf("step 3: got %v, want violated", verdicts[2])
+	}
+}
+
+func TestAlways_NowImpliesEventuallyWithin_HoldsWhenYInBound(t *testing.T) {
+	// Same formula, y = true at step 3 (within the 3-step bound).
+	xValues := []bool{true, false, false}
+	yValues := []bool{false, false, true}
+	step := 0
+	predX := Thunk(func() bool { return xValues[step] })
+	predY := Thunk(func() bool { return yValues[step] })
+
+	formula := Always(Implies(Now(predX), EventuallyWithinSteps(predY, 3)))
+	evaluator := NewEvaluator(formula)
+
+	verdicts := make([]Verdict, 0, 3)
+	for range 3 {
+		verdicts = append(verdicts, evaluator.Observe())
+		step++
+	}
+
+	if verdicts[0] != VerdictPending {
+		t.Errorf("step 1: got %v, want pending", verdicts[0])
+	}
+	if verdicts[1] != VerdictPending {
+		t.Errorf("step 2: got %v, want pending", verdicts[1])
+	}
+	if verdicts[2] != VerdictHolds {
+		t.Errorf("step 3: got %v, want holds", verdicts[2])
+	}
+}
+
+func TestEventually_DeadlineViolation(t *testing.T) {
+	base := time.Unix(0, 0)
+	deadline := base.Add(1 * time.Second)
+	formula := Always(EventuallyBefore(Pure(false), deadline))
+	evaluator := NewEvaluator(formula)
+
+	// Well before deadline: pending.
+	if got := evaluator.ObserveAt(base.Add(100 * time.Millisecond)); got != VerdictPending {
+		t.Errorf("pre-deadline: got %v, want pending", got)
+	}
+	// At or past deadline: violated.
+	if got := evaluator.ObserveAt(base.Add(2 * time.Second)); got != VerdictViolated {
+		t.Errorf("post-deadline: got %v, want violated", got)
+	}
+}
+
+func TestEventually_RelativeDurationResolvesOnFirstReduce(t *testing.T) {
+	base := time.Unix(0, 0)
+	// One-shot Eventually (not wrapped in Always) with a 1s relative deadline.
+	evaluator := NewEvaluator(EventuallyWithin(Pure(false), 1*time.Second))
+
+	if got := evaluator.ObserveAt(base); got != VerdictPending {
+		t.Errorf("creation step: got %v, want pending", got)
+	}
+	if got := evaluator.ObserveAt(base.Add(500 * time.Millisecond)); got != VerdictPending {
+		t.Errorf("mid-window: got %v, want pending", got)
+	}
+	if got := evaluator.ObserveAt(base.Add(2 * time.Second)); got != VerdictViolated {
+		t.Errorf("past-window: got %v, want violated", got)
+	}
+}
+
+func TestOr_OneBranchHolds(t *testing.T) {
+	evaluator := NewEvaluator(Always(Or(Pure(false), Pure(true))))
+	if got := evaluator.Observe(); got != VerdictHolds {
+		t.Errorf("or(false,true): got %v, want holds", got)
+	}
+}
+
+func TestAnd_OneBranchViolatesLatches(t *testing.T) {
+	evaluator := NewEvaluator(Always(And(Pure(true), Pure(false))))
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Errorf("and(true,false): got %v, want violated", got)
+	}
+}
+
+func TestNot_InvertsPure(t *testing.T) {
+	holds := NewEvaluator(Always(Not(Pure(false))))
+	if got := holds.Observe(); got != VerdictHolds {
+		t.Errorf("not(false): got %v, want holds", got)
+	}
+	violates := NewEvaluator(Always(Not(Pure(true))))
+	if got := violates.Observe(); got != VerdictViolated {
+		t.Errorf("not(true): got %v, want violated", got)
+	}
+}
+
+func TestVerdict_StringPending(t *testing.T) {
+	if got := VerdictPending.String(); got != "pending" {
+		t.Errorf("VerdictPending.String() = %q", got)
+	}
+}

internal/runner/runner.go

@@ -56,6 +56,8 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 	summary := Summary{StartTime: time.Now()}
 	deadline := summary.StartTime.Add(options.Duration)
 	stepIndex := 0
+	var lastAction *verifier.Action
+	var lastLogTime time.Time
 	for time.Now().Before(deadline) {
 		if err := ctx.Err(); err != nil {
 			break
@@ -82,7 +84,20 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			return summary, fmt.Errorf("step %d snapshot: %w", stepIndex, err)
 		}
 
-		if err := options.Verifier.PushSnapshot(verifier.Snapshots(snapshot.Snapshots), tree); err != nil {
+		logs := collectLogs(ctx, options.Driver, lastLogTime)
+		lastLogTime = stepStart
+
+		exceptions := decodeExceptions(snapshot)
+
+		if err := options.Verifier.PushSnapshot(verifier.SnapshotInput{
+			Snapshots:  verifier.Snapshots(snapshot.Snapshots),
+			Tree:       tree,
+			LastAction: lastAction,
+			StepTime:   stepStart,
+			RunStart:   summary.StartTime,
+			Logs:       logs,
+			Exceptions: exceptions,
+		}); err != nil {
 			return summary, fmt.Errorf("step %d push: %w", stepIndex, err)
 		}
 		screen, screenErr := screenFromSnapshot(snapshot.Snapshots)
@@ -108,6 +123,7 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			Screen:     screen,
 			Snapshots:  snapshot.Snapshots,
 			Action:     traceAction,
+			Exceptions: traceExceptions(exceptions),
 			Violations: violations,
 		}
 		if err := options.TraceWriter.WriteStep(step); err != nil {
@@ -129,6 +145,10 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			if err := applyAction(ctx, options.Driver, nextAction, tree); err != nil {
 				return summary, fmt.Errorf("step %d apply: %w", stepIndex, err)
 			}
+			actionCopy := nextAction
+			lastAction = &actionCopy
+		} else {
+			lastAction = nil
 		}
 
 		idleCtx, idleCancel := context.WithTimeout(ctx, options.IdleTimeout)
@@ -222,11 +242,71 @@ func applyAction(ctx context.Context, drv driver.Driver, action verifier.Action,
 			}
 		}
 		return drv.InputText(ctx, action.Text)
+	case verifier.ActionKindSwipe:
+		duration := time.Duration(action.DurationMillis) * time.Millisecond
+		if duration <= 0 {
+			duration = 250 * time.Millisecond
+		}
+		return drv.Swipe(ctx, action.FromX, action.FromY, action.ToX, action.ToY, duration)
+	case verifier.ActionKindPressKey:
+		if action.Key == "" {
+			return nil
+		}
+		return drv.PressKey(ctx, action.Key)
+	case verifier.ActionKindWait:
+		duration := time.Duration(action.DurationMillis) * time.Millisecond
+		if duration <= 0 {
+			return nil
+		}
+		timer := time.NewTimer(duration)
+		defer timer.Stop()
+		select {
+		case <-ctx.Done():
+			return ctx.Err()
+		case <-timer.C:
+			return nil
+		}
 	default:
 		return fmt.Errorf("unknown action kind %q", action.Kind)
 	}
 }
 
+// collectLogs pulls recent error-level log entries from the driver since the
+// previous fetch. A failure is warned-on but not fatal: log capture is a
+// best-effort observability channel, not a correctness dependency.
+func collectLogs(ctx context.Context, drv driver.Driver, since time.Time) []verifier.LogEntry {
+	entries, err := drv.RecentLogs(ctx, since, "E")
+	if err != nil {
+		return nil
+	}
+	result := make([]verifier.LogEntry, 0, len(entries))
+	for _, entry := range entries {
+		result = append(result, verifier.LogEntry{
+			UnixMillis: entry.UnixMillis,
+			Level:      entry.Level,
+			Tag:        entry.Tag,
+			Message:    entry.Message,
+		})
+	}
+	return result
+}
+
+func decodeExceptions(snapshot agent.Message) []verifier.Exception {
+	if len(snapshot.Exceptions) == 0 {
+		return nil
+	}
+	result := make([]verifier.Exception, 0, len(snapshot.Exceptions))
+	for _, e := range snapshot.Exceptions {
+		result = append(result, verifier.Exception{
+			Class:      e.Class,
+			Message:    e.Message,
+			StackTrace: e.StackTrace,
+			UnixMillis: e.UnixMillis,
+		})
+	}
+	return result
+}
+
 func resolveCoordinates(action verifier.Action, tree *hierarchy.Tree) (int, int, bool) {
 	if action.X > 0 && action.Y > 0 {
 		return action.X, action.Y, true
@@ -251,15 +331,40 @@ func fetchHierarchy(ctx context.Context, drv driver.Driver) (*hierarchy.Tree, er
 }
 
 func traceActionFor(action verifier.Action) *trace.Action {
-	traceAction := &trace.Action{Kind: string(action.Kind)}
+	traceAction := &trace.Action{Kind: string(action.Kind), X: action.X, Y: action.Y}
 	switch action.Kind {
 	case verifier.ActionKindTap:
-		// Selector lives in the trace step's action.text field for now —
-		// trace.Action only has X/Y/Text and we don't resolve coordinates
-		// at the runner layer.
 		traceAction.Text = action.On
 	case verifier.ActionKindInputText:
 		traceAction.Text = action.Text
+	case verifier.ActionKindSwipe:
+		traceAction.FromX = action.FromX
+		traceAction.FromY = action.FromY
+		traceAction.ToX = action.ToX
+		traceAction.ToY = action.ToY
+		traceAction.DurationMillis = action.DurationMillis
+		traceAction.X = 0
+		traceAction.Y = 0
+	case verifier.ActionKindPressKey:
+		traceAction.Key = action.Key
+	case verifier.ActionKindWait:
+		traceAction.DurationMillis = action.DurationMillis
 	}
 	return traceAction
 }
+
+func traceExceptions(exceptions []verifier.Exception) []trace.Exception {
+	if len(exceptions) == 0 {
+		return nil
+	}
+	result := make([]trace.Exception, 0, len(exceptions))
+	for _, e := range exceptions {
+		result = append(result, trace.Exception{
+			Class:      e.Class,
+			Message:    e.Message,
+			StackTrace: e.StackTrace,
+			UnixMillis: e.UnixMillis,
+		})
+	}
+	return result
+}

internal/trace/writer.go

@@ -16,14 +16,28 @@ type Step struct {
 	Screen     string                     `json:"screen,omitempty"`
 	Snapshots  map[string]json.RawMessage `json:"snapshots,omitempty"`
 	Action     *Action                    `json:"action,omitempty"`
+	Exceptions []Exception                `json:"exceptions,omitempty"`
 	Violations []string                   `json:"violations,omitempty"`
 }
 
 type Action struct {
-	Kind string `json:"kind"`
-	X    int    `json:"x,omitempty"`
-	Y    int    `json:"y,omitempty"`
-	Text string `json:"text,omitempty"`
+	Kind  string `json:"kind"`
+	X     int    `json:"x,omitempty"`
+	Y     int    `json:"y,omitempty"`
+	FromX int    `json:"from_x,omitempty"`
+	FromY int    `json:"from_y,omitempty"`
+	ToX   int    `json:"to_x,omitempty"`
+	ToY   int    `json:"to_y,omitempty"`
+	Key   string `json:"key,omitempty"`
+	Text  string `json:"text,omitempty"`
+	DurationMillis int `json:"duration_millis,omitempty"`
+}
+
+type Exception struct {
+	Class      string `json:"class"`
+	Message    string `json:"message,omitempty"`
+	StackTrace string `json:"stack_trace,omitempty"`
+	UnixMillis int64  `json:"unix_millis,omitempty"`
 }
 
 type Meta struct {

internal/verifier/ax_integration_test.go

@@ -31,7 +31,7 @@ func TestStateAxFindWorks(t *testing.T) {
 		globalThis.count = __uatu__.extract(state => state.ax.findAll("id:select_language").length);
 	`)
 
-	if err := verifier.PushSnapshot(Snapshots{}, tree); err != nil {
+	if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{}, Tree: tree}); err != nil {
 		t.Fatal(err)
 	}
 

internal/verifier/bindings.go

@@ -2,6 +2,7 @@ package verifier
 
 import (
 	"fmt"
+	"time"
 
 	"github.com/dop251/goja"
 )
@@ -11,6 +12,9 @@ type ActionKind string
 const (
 	ActionKindTap       ActionKind = "Tap"
 	ActionKindInputText ActionKind = "InputText"
+	ActionKindSwipe     ActionKind = "Swipe"
+	ActionKindPressKey  ActionKind = "PressKey"
+	ActionKindWait      ActionKind = "Wait"
 )
 
 type Action struct {
@@ -21,6 +25,13 @@ type Action struct {
 	// Tap/InputText. Zero means the runner must resolve On against the
 	// current hierarchy.
 	X, Y int
+	// Swipe coordinates (raw px). Used only for ActionKindSwipe.
+	FromX, FromY int
+	ToX, ToY     int
+	// DurationMillis is the Swipe gesture duration or the Wait duration.
+	DurationMillis int
+	// Key is the logical key name for ActionKindPressKey.
+	Key string
 }
 
 type extractorState struct {
@@ -32,15 +43,51 @@ type formulaState struct {
 	predicate goja.Callable
 }
 
+type specKind int
+
 const (
-	tagFormula            = "__uatuFormula"
-	tagActionGenerator    = "__uatuActionGenerator"
-	tagInternalKind       = "__uatuKind"
-	tagSelector           = "__uatuSelector"
-	internalKindActions   = "actions"
-	internalKindWeighted  = "weighted"
-	internalKindBuiltinTaps   = "taps"
-	internalKindBuiltinSwipes = "swipes"
+	specKindPure specKind = iota
+	specKindThunk
+	specKindNow
+	specKindNext
+	specKindEventually
+	specKindImplies
+	specKindOr
+	specKindAnd
+	specKindNot
+	specKindAlways
+)
+
+// formulaSpec is the Go-side registry entry that mirrors a chainable JS
+// formula handle. Handles reference specs by index; chaining creates new
+// specs that reference their operands' indices.
+type formulaSpec struct {
+	kind specKind
+
+	pureValue      bool
+	predicateIndex int
+
+	childA int
+	childB int
+
+	stepBound    int
+	hasStepBound bool
+	duration     time.Duration
+}
+
+const (
+	tagFormula          = "__uatuFormula"
+	tagFormulaSpecIndex = "__uatuFormulaSpec"
+	tagActionGenerator  = "__uatuActionGenerator"
+	tagInternalKind     = "__uatuKind"
+	tagSelector         = "__uatuSelector"
+
+	internalKindActions         = "actions"
+	internalKindWeighted        = "weighted"
+	internalKindBuiltinTaps     = "taps"
+	internalKindBuiltinSwipes   = "swipes"
+	internalKindBuiltinWaitOnce = "waitOnce"
+	internalKindBuiltinPressKey = "pressKey"
 )
 
 // installRuntimeBindings exposes globalThis.__uatu__ to the loaded spec.
@@ -53,24 +100,51 @@ func (v *Verifier) installRuntimeBindings() error {
 	if err := uatu.Set("always", v.bindAlways); err != nil {
 		return err
 	}
+	if err := uatu.Set("now", v.bindNow); err != nil {
+		return err
+	}
+	if err := uatu.Set("next", v.bindNext); err != nil {
+		return err
+	}
+	if err := uatu.Set("eventually", v.bindEventually); err != nil {
+		return err
+	}
 	if err := uatu.Set("actions", v.bindActions); err != nil {
 		return err
 	}
 	if err := uatu.Set("weighted", v.bindWeighted); err != nil {
 		return err
 	}
+	if err := uatu.Set("from", v.bindFrom); err != nil {
+		return err
+	}
 	if err := uatu.Set("tap", v.bindTap); err != nil {
 		return err
 	}
 	if err := uatu.Set("inputText", v.bindInputText); err != nil {
 		return err
 	}
+	if err := uatu.Set("swipe", v.bindSwipe); err != nil {
+		return err
+	}
+	if err := uatu.Set("pressKey", v.bindPressKey); err != nil {
+		return err
+	}
+	if err := uatu.Set("wait", v.bindWait); err != nil {
+		return err
+	}
 	if err := uatu.Set("taps", v.builtinGenerator(internalKindBuiltinTaps)); err != nil {
 		return err
 	}
 	if err := uatu.Set("swipes", v.builtinGenerator(internalKindBuiltinSwipes)); err != nil {
 		return err
 	}
+	if err := uatu.Set("waitOnce", v.builtinGenerator(internalKindBuiltinWaitOnce)); err != nil {
+		return err
+	}
+	if err := uatu.Set("pressKeys", v.builtinGenerator(internalKindBuiltinPressKey)); err != nil {
+		return err
+	}
 
 	return v.runtime.GlobalObject().Set("__uatu__", uatu)
 }
@@ -92,25 +166,178 @@ func (v *Verifier) bindExtract(call goja.FunctionCall) goja.Value {
 	return handle
 }
 
+// bindAlways accepts either a predicate function (legacy shape) or a formula
+// handle (new shape). Both produce a formula handle tagged with
+// __uatuFormulaSpec.
 func (v *Verifier) bindAlways(call goja.FunctionCall) goja.Value {
 	if len(call.Arguments) != 1 {
 		panic(v.runtime.NewTypeError("always requires exactly one argument"))
 	}
+	arg := call.Arguments[0]
+	if predicate, ok := goja.AssertFunction(arg); ok {
+		thunkIndex := v.registerThunk(predicate)
+		return v.makeFormulaHandle(specKindAlways, formulaSpec{
+			kind:   specKindAlways,
+			childA: thunkIndex,
+		})
+	}
+	childIndex, ok := v.extractSpecIndex(arg)
+	if !ok {
+		panic(v.runtime.NewTypeError("always argument must be a predicate or formula"))
+	}
+	return v.makeFormulaHandle(specKindAlways, formulaSpec{
+		kind:   specKindAlways,
+		childA: childIndex,
+	})
+}
+
+func (v *Verifier) bindNow(call goja.FunctionCall) goja.Value {
+	thunkIndex := v.requirePredicate(call, "now")
+	return v.makeFormulaHandle(specKindNow, formulaSpec{
+		kind:   specKindNow,
+		childA: thunkIndex,
+	})
+}
+
+func (v *Verifier) bindNext(call goja.FunctionCall) goja.Value {
+	thunkIndex := v.requirePredicate(call, "next")
+	return v.makeFormulaHandle(specKindNext, formulaSpec{
+		kind:   specKindNext,
+		childA: thunkIndex,
+	})
+}
+
+func (v *Verifier) bindEventually(call goja.FunctionCall) goja.Value {
+	thunkIndex := v.requirePredicate(call, "eventually")
+	return v.makeFormulaHandle(specKindEventually, formulaSpec{
+		kind:   specKindEventually,
+		childA: thunkIndex,
+	})
+}
+
+func (v *Verifier) requirePredicate(call goja.FunctionCall, name string) int {
+	if len(call.Arguments) != 1 {
+		panic(v.runtime.NewTypeError(name + " requires exactly one argument"))
+	}
 	predicate, ok := goja.AssertFunction(call.Arguments[0])
 	if !ok {
-		panic(v.runtime.NewTypeError("always argument must be a function"))
+		panic(v.runtime.NewTypeError(name + " argument must be a function"))
 	}
+	return v.registerThunk(predicate)
+}
 
-	formula := &formulaState{predicate: predicate}
-	v.formulas = append(v.formulas, formula)
-	formulaIndex := len(v.formulas) - 1
+// registerThunk stores a predicate in v.formulas and returns its index, which
+// reduce can later invoke via formulaThunk.
+func (v *Verifier) registerThunk(predicate goja.Callable) int {
+	spec := formulaSpec{kind: specKindThunk}
+	// predicateIndex points into v.formulas, which is a parallel slice.
+	spec.predicateIndex = len(v.formulas)
+	v.formulas = append(v.formulas, &formulaState{predicate: predicate})
+	v.formulaSpecs = append(v.formulaSpecs, spec)
+	return len(v.formulaSpecs) - 1
+}
 
+// registerSpec appends a spec and returns its index.
+func (v *Verifier) registerSpec(spec formulaSpec) int {
+	v.formulaSpecs = append(v.formulaSpecs, spec)
+	return len(v.formulaSpecs) - 1
+}
+
+// makeFormulaHandle registers the spec and returns a JS handle exposing
+// chainable combinators. Eventually handles additionally expose .within.
+func (v *Verifier) makeFormulaHandle(kind specKind, spec formulaSpec) *goja.Object {
+	index := v.registerSpec(spec)
+	return v.formulaHandle(kind, index)
+}
+
+func (v *Verifier) formulaHandle(kind specKind, index int) *goja.Object {
 	handle := v.runtime.NewObject()
 	_ = handle.Set(tagFormula, true)
-	_ = handle.Set("__uatuIndex", formulaIndex)
+	_ = handle.Set(tagFormulaSpecIndex, index)
+	// Keep __uatuIndex as an alias so older property shapes that read it keep
+	// working during backward-compat transitions.
+	_ = handle.Set("__uatuIndex", index)
+
+	_ = handle.Set("implies", v.binaryChain(index, specKindImplies))
+	_ = handle.Set("or", v.binaryChain(index, specKindOr))
+	_ = handle.Set("and", v.binaryChain(index, specKindAnd))
+	_ = handle.Set("not", v.unaryChain(index, specKindNot))
+
+	if kind == specKindEventually {
+		_ = handle.Set("within", v.eventuallyWithin(index))
+	}
+
 	return handle
 }
 
+func (v *Verifier) binaryChain(selfIndex int, kind specKind) func(call goja.FunctionCall) goja.Value {
+	return func(call goja.FunctionCall) goja.Value {
+		if len(call.Arguments) != 1 {
+			panic(v.runtime.NewTypeError("operator requires exactly one argument"))
+		}
+		otherIndex, ok := v.extractSpecIndex(call.Arguments[0])
+		if !ok {
+			panic(v.runtime.NewTypeError("operator argument must be a formula"))
+		}
+		return v.makeFormulaHandle(kind, formulaSpec{
+			kind:   kind,
+			childA: selfIndex,
+			childB: otherIndex,
+		})
+	}
+}
+
+func (v *Verifier) unaryChain(selfIndex int, kind specKind) func(call goja.FunctionCall) goja.Value {
+	return func(call goja.FunctionCall) goja.Value {
+		return v.makeFormulaHandle(kind, formulaSpec{
+			kind:   kind,
+			childA: selfIndex,
+		})
+	}
+}
+
+func (v *Verifier) eventuallyWithin(selfIndex int) func(call goja.FunctionCall) goja.Value {
+	return func(call goja.FunctionCall) goja.Value {
+		if len(call.Arguments) != 2 {
+			panic(v.runtime.NewTypeError("within requires (amount, unit)"))
+		}
+		amount := call.Argument(0).ToInteger()
+		unit := call.Argument(1).String()
+		base := v.formulaSpecs[selfIndex]
+		if base.kind != specKindEventually {
+			panic(v.runtime.NewTypeError("within only applies to eventually"))
+		}
+		switch unit {
+		case "steps":
+			base.stepBound = int(amount)
+			base.hasStepBound = true
+		case "milliseconds":
+			base.duration = time.Duration(amount) * time.Millisecond
+		case "seconds":
+			base.duration = time.Duration(amount) * time.Second
+		default:
+			panic(v.runtime.NewTypeError("within unit must be 'milliseconds', 'seconds', or 'steps'"))
+		}
+		return v.makeFormulaHandle(specKindEventually, base)
+	}
+}
+
+// extractSpecIndex reads __uatuFormulaSpec from a JS formula handle.
+func (v *Verifier) extractSpecIndex(value goja.Value) (int, bool) {
+	if value == nil || goja.IsNull(value) || goja.IsUndefined(value) {
+		return 0, false
+	}
+	object := value.ToObject(v.runtime)
+	if object == nil {
+		return 0, false
+	}
+	indexValue := object.Get(tagFormulaSpecIndex)
+	if indexValue == nil || goja.IsUndefined(indexValue) {
+		return 0, false
+	}
+	return int(indexValue.ToInteger()), true
+}
+
 func (v *Verifier) bindActions(call goja.FunctionCall) goja.Value {
 	if len(call.Arguments) != 1 {
 		panic(v.runtime.NewTypeError("actions requires a single generator argument"))
@@ -143,6 +370,34 @@ func (v *Verifier) bindWeighted(call goja.FunctionCall) goja.Value {
 	return handle
 }
 
+// bindFrom returns a `{ generate }` that picks uniformly at random from the
+// provided items using the verifier's seeded rng.
+func (v *Verifier) bindFrom(call goja.FunctionCall) goja.Value {
+	if len(call.Arguments) != 1 {
+		panic(v.runtime.NewTypeError("from requires an array argument"))
+	}
+	itemsValue := call.Arguments[0]
+	itemsObject := itemsValue.ToObject(v.runtime)
+	if itemsObject == nil {
+		panic(v.runtime.NewTypeError("from argument must be an array"))
+	}
+	lengthValue := itemsObject.Get("length")
+	if lengthValue == nil {
+		panic(v.runtime.NewTypeError("from argument must be array-like"))
+	}
+	length := int(lengthValue.ToInteger())
+
+	handle := v.runtime.NewObject()
+	_ = handle.Set("generate", func(goja.FunctionCall) goja.Value {
+		if length == 0 {
+			return goja.Undefined()
+		}
+		index := v.rng.IntN(length)
+		return itemsObject.Get(fmt.Sprintf("%d", index))
+	})
+	return handle
+}
+
 func (v *Verifier) bindTap(call goja.FunctionCall) goja.Value {
 	parameters := call.Argument(0).ToObject(v.runtime)
 	if parameters == nil {
@@ -166,6 +421,43 @@ func (v *Verifier) bindInputText(call goja.FunctionCall) goja.Value {
 	return handle
 }
 
+func (v *Verifier) bindSwipe(call goja.FunctionCall) goja.Value {
+	parameters := call.Argument(0).ToObject(v.runtime)
+	if parameters == nil {
+		panic(v.runtime.NewTypeError("Swipe requires {from, to}"))
+	}
+	handle := v.runtime.NewObject()
+	_ = handle.Set("kind", "Swipe")
+	_ = handle.Set("from", parameters.Get("from"))
+	_ = handle.Set("to", parameters.Get("to"))
+	if duration := parameters.Get("durationMillis"); duration != nil && !goja.IsUndefined(duration) {
+		_ = handle.Set("durationMillis", duration)
+	}
+	return handle
+}
+
+func (v *Verifier) bindPressKey(call goja.FunctionCall) goja.Value {
+	parameters := call.Argument(0).ToObject(v.runtime)
+	if parameters == nil {
+		panic(v.runtime.NewTypeError("PressKey requires {key}"))
+	}
+	handle := v.runtime.NewObject()
+	_ = handle.Set("kind", "PressKey")
+	_ = handle.Set("key", parameters.Get("key"))
+	return handle
+}
+
+func (v *Verifier) bindWait(call goja.FunctionCall) goja.Value {
+	parameters := call.Argument(0).ToObject(v.runtime)
+	if parameters == nil {
+		panic(v.runtime.NewTypeError("Wait requires {durationMillis}"))
+	}
+	handle := v.runtime.NewObject()
+	_ = handle.Set("kind", "Wait")
+	_ = handle.Set("durationMillis", parameters.Get("durationMillis"))
+	return handle
+}
+
 func (v *Verifier) builtinGenerator(kind string) *goja.Object {
 	handle := v.runtime.NewObject()
 	_ = handle.Set(tagActionGenerator, true)

internal/verifier/marshal.go

@@ -3,6 +3,7 @@ package verifier
 import (
 	"encoding/json"
 	"fmt"
+	"time"
 
 	"github.com/dop251/goja"
 
@@ -12,13 +13,23 @@ import (
 // Snapshots is the per-step extractor output forwarded by the SDK.
 type Snapshots map[string]json.RawMessage
 
-// stateObject builds a JS-side `{ snapshots, ax }` matching the State type
-// from pkg/spec-api. ax is backed by the parsed uiautomator hierarchy when
-// one is provided.
-func stateObject(runtime *goja.Runtime, snapshots Snapshots, tree *hierarchy.Tree) (*goja.Object, error) {
+type stateInput struct {
+	snapshots  Snapshots
+	tree       *hierarchy.Tree
+	lastAction *Action
+	stepTime   time.Time
+	runStart   time.Time
+	logs       []LogEntry
+	exceptions []Exception
+}
+
+// stateObject builds the JS-side `state` object matching the State type from
+// pkg/spec-api. Fields beyond snapshots/ax are included when the caller
+// populated them on stateInput.
+func stateObject(runtime *goja.Runtime, input stateInput) (*goja.Object, error) {
 	state := runtime.NewObject()
 	snapshotsObject := runtime.NewObject()
-	for key, raw := range snapshots {
+	for key, raw := range input.snapshots {
 		value, err := jsonToJSValue(runtime, raw)
 		if err != nil {
 			return nil, fmt.Errorf("snapshot %q: %w", key, err)
@@ -30,7 +41,19 @@ func stateObject(runtime *goja.Runtime, snapshots Snapshots, tree *hierarchy.Tre
 	if err := state.Set("snapshots", snapshotsObject); err != nil {
 		return nil, err
 	}
-	if err := state.Set("ax", accessibilityObject(runtime, tree)); err != nil {
+	if err := state.Set("ax", accessibilityObject(runtime, input.tree)); err != nil {
+		return nil, err
+	}
+	if err := state.Set("lastAction", lastActionObject(runtime, input.lastAction)); err != nil {
+		return nil, err
+	}
+	if err := state.Set("time", runtimeMillis(input.stepTime, input.runStart)); err != nil {
+		return nil, err
+	}
+	if err := state.Set("logs", logsArray(runtime, input.logs)); err != nil {
+		return nil, err
+	}
+	if err := state.Set("exceptions", exceptionsArray(runtime, input.exceptions)); err != nil {
 		return nil, err
 	}
 	return state, nil
@@ -88,6 +111,74 @@ func elementObject(runtime *goja.Runtime, element *hierarchy.Element, selector s
 	return object
 }
 
+func lastActionObject(runtime *goja.Runtime, action *Action) goja.Value {
+	if action == nil {
+		return goja.Null()
+	}
+	object := runtime.NewObject()
+	_ = object.Set("kind", string(action.Kind))
+	if action.On != "" {
+		_ = object.Set("on", action.On)
+	}
+	if action.Text != "" {
+		_ = object.Set("text", action.Text)
+	}
+	switch action.Kind {
+	case ActionKindSwipe:
+		from := runtime.NewObject()
+		_ = from.Set("x", action.FromX)
+		_ = from.Set("y", action.FromY)
+		to := runtime.NewObject()
+		_ = to.Set("x", action.ToX)
+		_ = to.Set("y", action.ToY)
+		_ = object.Set("from", from)
+		_ = object.Set("to", to)
+		if action.DurationMillis > 0 {
+			_ = object.Set("durationMillis", action.DurationMillis)
+		}
+	case ActionKindPressKey:
+		_ = object.Set("key", action.Key)
+	case ActionKindWait:
+		_ = object.Set("durationMillis", action.DurationMillis)
+	}
+	return object
+}
+
+func runtimeMillis(stepTime, runStart time.Time) int64 {
+	if stepTime.IsZero() || runStart.IsZero() {
+		return 0
+	}
+	return stepTime.Sub(runStart).Milliseconds()
+}
+
+func logsArray(runtime *goja.Runtime, logs []LogEntry) *goja.Object {
+	array := runtime.NewArray()
+	for index, entry := range logs {
+		item := runtime.NewObject()
+		_ = item.Set("unixMillis", entry.UnixMillis)
+		_ = item.Set("level", entry.Level)
+		_ = item.Set("tag", entry.Tag)
+		_ = item.Set("message", entry.Message)
+		_ = array.Set(fmt.Sprintf("%d", index), item)
+	}
+	return array
+}
+
+func exceptionsArray(runtime *goja.Runtime, exceptions []Exception) *goja.Object {
+	array := runtime.NewArray()
+	for index, exception := range exceptions {
+		item := runtime.NewObject()
+		_ = item.Set("class", exception.Class)
+		_ = item.Set("message", exception.Message)
+		_ = item.Set("stackTrace", exception.StackTrace)
+		if exception.UnixMillis > 0 {
+			_ = item.Set("unixMillis", exception.UnixMillis)
+		}
+		_ = array.Set(fmt.Sprintf("%d", index), item)
+	}
+	return array
+}
+
 func jsonToJSValue(runtime *goja.Runtime, raw json.RawMessage) (goja.Value, error) {
 	if len(raw) == 0 {
 		return goja.Undefined(), nil
@@ -99,7 +190,7 @@ func jsonToJSValue(runtime *goja.Runtime, raw json.RawMessage) (goja.Value, erro
 	return runtime.ToValue(generic), nil
 }
 
-// jsValueToAction converts a JS-side {kind, on?, into?, text?} into a Go Action.
+// jsValueToAction converts a JS-side action object into a Go Action.
 func jsValueToAction(runtime *goja.Runtime, value goja.Value) (Action, error) {
 	if value == nil || goja.IsNull(value) || goja.IsUndefined(value) {
 		return Action{}, fmt.Errorf("nil action")
@@ -120,11 +211,60 @@ func jsValueToAction(runtime *goja.Runtime, value goja.Value) (Action, error) {
 		text := object.Get("text")
 		x, y := coordinatesOf(runtime, into)
 		return Action{Kind: ActionKindInputText, On: selectorOf(runtime, into), Text: stringOf(text), X: x, Y: y}, nil
+	case "Swipe":
+		from := object.Get("from")
+		to := object.Get("to")
+		fromX, fromY := coordinatesOf(runtime, from)
+		toX, toY := coordinatesOf(runtime, to)
+		if fromX == 0 && fromY == 0 {
+			fromX, fromY = pointCoordinates(runtime, from)
+		}
+		if toX == 0 && toY == 0 {
+			toX, toY = pointCoordinates(runtime, to)
+		}
+		return Action{
+			Kind:           ActionKindSwipe,
+			FromX:          fromX,
+			FromY:          fromY,
+			ToX:            toX,
+			ToY:            toY,
+			DurationMillis: intField(object, "durationMillis"),
+		}, nil
+	case "PressKey":
+		return Action{Kind: ActionKindPressKey, Key: stringOf(object.Get("key"))}, nil
+	case "Wait":
+		return Action{Kind: ActionKindWait, DurationMillis: intField(object, "durationMillis")}, nil
 	default:
 		return Action{}, fmt.Errorf("unknown action kind %q", kind)
 	}
 }
 
+// pointCoordinates reads a plain {x, y} literal (not an AX element), which is
+// how Swipe endpoints are commonly expressed in specs.
+func pointCoordinates(runtime *goja.Runtime, value goja.Value) (int, int) {
+	if value == nil || goja.IsNull(value) || goja.IsUndefined(value) {
+		return 0, 0
+	}
+	object := value.ToObject(runtime)
+	if object == nil {
+		return 0, 0
+	}
+	x := object.Get("x")
+	y := object.Get("y")
+	if x == nil || y == nil {
+		return 0, 0
+	}
+	return int(x.ToInteger()), int(y.ToInteger())
+}
+
+func intField(object *goja.Object, name string) int {
+	value := object.Get(name)
+	if value == nil || goja.IsUndefined(value) || goja.IsNull(value) {
+		return 0
+	}
+	return int(value.ToInteger())
+}
+
 func selectorOf(runtime *goja.Runtime, value goja.Value) string {
 	if value == nil || goja.IsNull(value) || goja.IsUndefined(value) {
 		return ""

internal/verifier/spec_integration_test.go

@@ -14,10 +14,9 @@ const sampleAppHierarchyXML = `<?xml version="1.0" encoding="UTF-8"?>
 <hierarchy rotation="0">
   <node index="0" class="android.widget.FrameLayout" package="dev.uatu.sample" bounds="[0,0][1080,2400]">
     <node index="0" class="android.widget.LinearLayout" bounds="[64,96][1016,2336]">
-      <node index="0" class="android.widget.TextView" text="Clicks: 0" bounds="[100,200][900,300]" />
-      <node index="1" class="android.widget.Button" text="Click me" clickable="true" enabled="true" bounds="[400,800][680,920]" />
-      <node index="2" class="android.widget.TextView" text="Username: " bounds="[100,1000][900,1080]" />
-      <node index="3" class="android.widget.EditText" content-desc="username_field" clickable="true" enabled="true" bounds="[100,1200][900,1320]" />
+      <node index="0" class="android.widget.TextView" text="Sign in" bounds="[100,200][900,300]" />
+      <node index="1" class="android.widget.EditText" content-desc="phone_field" clickable="true" enabled="true" bounds="[100,400][900,520]" />
+      <node index="2" class="android.widget.Button" text="Continue" clickable="true" enabled="true" bounds="[400,800][680,920]" />
     </node>
   </node>
 </hierarchy>`
@@ -34,9 +33,16 @@ func bundleSampleAppSpec(t *testing.T) string {
 	if err != nil {
 		t.Fatal(err)
 	}
+	defaultsPath, err := filepath.Abs("../../pkg/spec-api/src/defaults/properties.ts")
+	if err != nil {
+		t.Fatal(err)
+	}
 	bundle, err := bundler.Bundle(bundler.Options{
 		EntryFile: specPath,
-		Aliases:   map[string]string{"@uatu/spec": apiPath},
+		Aliases: map[string]string{
+			"@uatu/spec":                    apiPath,
+			"@uatu/spec/defaults/properties": defaultsPath,
+		},
 	})
 	if err != nil {
 		t.Fatal(err)
@@ -44,9 +50,10 @@ func bundleSampleAppSpec(t *testing.T) string {
 	return string(bundle.JavaScript)
 }
 
-// TestSampleAppSpecTapsClickMe verifies the bundled sample-app spec emits a
-// Tap on the "Click me" button when that button is present in the hierarchy.
-func TestSampleAppSpecTapsClickMe(t *testing.T) {
+// TestSampleAppSpecFiresLoginActions verifies the bundled sample-app spec
+// emits Tap/InputText actions targeting the login screen elements when they
+// are present in the hierarchy.
+func TestSampleAppSpecFiresLoginActions(t *testing.T) {
 	v := newVerifier(t)
 	if err := v.Load(bundleSampleAppSpec(t)); err != nil {
 		t.Fatal(err)
@@ -57,85 +64,67 @@ func TestSampleAppSpecTapsClickMe(t *testing.T) {
 		t.Fatal(err)
 	}
 	snapshots := Snapshots{
-		"app_state":   json.RawMessage(`"running"`),
-		"click_count": json.RawMessage(`0`),
+		"route":         json.RawMessage(`"login"`),
+		"logged_in":     json.RawMessage(`false`),
+		"account_count": json.RawMessage(`0`),
 	}
-	if err := v.PushSnapshot(snapshots, tree); err != nil {
+	if err := v.PushSnapshot(SnapshotInput{Snapshots: snapshots, Tree: tree}); err != nil {
 		t.Fatal(err)
 	}
 
-	tapHits := 0
-	inputHits := 0
+	tapContinueHits := 0
+	typePhoneHits := 0
 	for range 400 {
 		action, err := v.NextAction()
 		if err != nil {
 			continue
 		}
 		switch {
-		case action.Kind == ActionKindTap && action.On == "text:Click me":
-			tapHits++
-		case action.Kind == ActionKindInputText && action.On == "desc:username_field" && action.Text == "alice":
-			inputHits++
+		case action.Kind == ActionKindTap && action.On == "text:Continue":
+			tapContinueHits++
+		case action.Kind == ActionKindInputText && action.On == "desc:phone_field":
+			typePhoneHits++
 		}
 	}
-	if tapHits == 0 {
-		t.Fatal("tapClickMe never fired on sample-app hierarchy")
+	if tapContinueHits == 0 {
+		t.Fatal("tapContinue never fired on sample-app hierarchy")
 	}
-	if inputHits == 0 {
-		t.Fatal("typeUsername never fired on sample-app hierarchy")
+	if typePhoneHits == 0 {
+		t.Fatal("typePhone never fired on sample-app hierarchy")
 	}
 }
 
-// TestSampleAppSpecPropertiesHold checks the three properties declared in the
-// sample-app spec evaluate correctly across a realistic snapshot sequence.
-func TestSampleAppSpecPropertiesHold(t *testing.T) {
+// TestSampleAppSpecPropertiesEvaluate checks the properties declared in the
+// sample-app spec evaluate sensibly across a small snapshot sequence. The
+// spec mixes safety and liveness properties; Pending verdicts are expected
+// for liveness properties that haven't had time to resolve yet.
+func TestSampleAppSpecPropertiesEvaluate(t *testing.T) {
 	v := newVerifier(t)
 	if err := v.Load(bundleSampleAppSpec(t)); err != nil {
 		t.Fatal(err)
 	}
 
-	steps := []struct {
-		appState   string
-		clickCount int
-		username   string
-		want       map[string]ltl.Verdict
-	}{
-		{"running", 0, "", map[string]ltl.Verdict{
-			"appIsRunning":             ltl.VerdictHolds,
-			"clickCountNonNegative":    ltl.VerdictHolds,
-			"clickCountNeverDecreases": ltl.VerdictHolds,
-			"usernameNeverShrinks":     ltl.VerdictHolds,
-		}},
-		{"running", 5, "alice", map[string]ltl.Verdict{
-			"appIsRunning":             ltl.VerdictHolds,
-			"clickCountNonNegative":    ltl.VerdictHolds,
-			"clickCountNeverDecreases": ltl.VerdictHolds,
-			"usernameNeverShrinks":     ltl.VerdictHolds,
-		}},
-		{"running", 3, "al", map[string]ltl.Verdict{
-			"appIsRunning":             ltl.VerdictHolds,
-			"clickCountNonNegative":    ltl.VerdictHolds,
-			"clickCountNeverDecreases": ltl.VerdictViolated,
-			"usernameNeverShrinks":     ltl.VerdictViolated,
-		}},
+	tree, err := hierarchy.Parse(sampleAppHierarchyXML)
+	if err != nil {
+		t.Fatal(err)
 	}
-
-	for index, step := range steps {
-		stateRaw, _ := json.Marshal(step.appState)
-		countRaw, _ := json.Marshal(step.clickCount)
-		usernameRaw, _ := json.Marshal(step.username)
-		if err := v.PushSnapshot(Snapshots{
-			"app_state":   stateRaw,
-			"click_count": countRaw,
-			"username":    usernameRaw,
-		}, nil); err != nil {
-			t.Fatalf("step %d: %v", index, err)
-		}
-		got := v.EvaluateProperties()
-		for property, want := range step.want {
-			if got[property] != want {
-				t.Errorf("step %d %q: got %v, want %v", index, property, got[property], want)
-			}
-		}
+	snapshots := Snapshots{
+		"route":         json.RawMessage(`"login"`),
+		"logged_in":     json.RawMessage(`false`),
+		"account_count": json.RawMessage(`0`),
+	}
+	if err := v.PushSnapshot(SnapshotInput{Snapshots: snapshots, Tree: tree}); err != nil {
+		t.Fatal(err)
+	}
+	verdicts := v.EvaluateProperties()
+	if verdicts["accountCountNonNegative"] != ltl.VerdictHolds {
+		t.Errorf("accountCountNonNegative: got %v, want holds", verdicts["accountCountNonNegative"])
+	}
+	if verdicts["noUncaughtExceptions"] != ltl.VerdictHolds {
+		t.Errorf("noUncaughtExceptions: got %v, want holds", verdicts["noUncaughtExceptions"])
+	}
+	// Liveness: eventuallyLoggedIn hasn't resolved yet.
+	if verdicts["eventuallyLoggedIn"] != ltl.VerdictPending {
+		t.Errorf("eventuallyLoggedIn: got %v, want pending", verdicts["eventuallyLoggedIn"])
 	}
 }

internal/verifier/verifier_test.go

@@ -60,10 +60,10 @@ func TestPushSnapshot_UpdatesExtractorCurrentAndPrevious(t *testing.T) {
 	verifier := newVerifier(t)
 	mustLoad(t, verifier, helloSpec)
 
-	if err := verifier.PushSnapshot(Snapshots{
+	if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{
 		"screen":         json.RawMessage(`"customer_ledger"`),
 		"ledger.balance": json.RawMessage(`1500`),
-	}, nil); err != nil {
+	}}); err != nil {
 		t.Fatal(err)
 	}
 
@@ -78,7 +78,7 @@ func TestPushSnapshot_UpdatesExtractorCurrentAndPrevious(t *testing.T) {
 	}
 
 	// Push again: previous should mirror the prior current.
-	if err := verifier.PushSnapshot(Snapshots{"ledger.balance": json.RawMessage(`2000`)}, nil); err != nil {
+	if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{"ledger.balance": json.RawMessage(`2000`)}}); err != nil {
 		t.Fatal(err)
 	}
 	balanceValue = verifier.runtime.GlobalObject().Get("balance").ToObject(verifier.runtime)
@@ -105,7 +105,7 @@ func TestEvaluateProperties_HoldsThenViolates(t *testing.T) {
 	}
 	for index, testCase := range cases {
 		raw, _ := json.Marshal(testCase.balance)
-		if err := verifier.PushSnapshot(Snapshots{"ledger.balance": raw}, nil); err != nil {
+		if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{"ledger.balance": raw}}); err != nil {
 			t.Fatal(err)
 		}
 		verdicts := verifier.EvaluateProperties()
@@ -118,7 +118,7 @@ func TestEvaluateProperties_HoldsThenViolates(t *testing.T) {
 func TestNextAction_FromActionsGenerator(t *testing.T) {
 	verifier := newVerifier(t)
 	mustLoad(t, verifier, helloSpec)
-	_ = verifier.PushSnapshot(Snapshots{}, nil)
+	_ = verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{}})
 
 	action, err := verifier.NextAction()
 	if err != nil {
@@ -142,7 +142,7 @@ func TestNextAction_WeightedSelectsByWeight(t *testing.T) {
 			[99, tapAway],
 		);
 	`)
-	_ = verifier.PushSnapshot(Snapshots{}, nil)
+	_ = verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{}})
 
 	awayCount := 0
 	homeCount := 0
@@ -168,7 +168,7 @@ func TestNextAction_EmptyGeneratorReturnsErrNoAction(t *testing.T) {
 	mustLoad(t, verifier, `
 		globalThis.actions = __uatu__.actions(() => []);
 	`)
-	_ = verifier.PushSnapshot(Snapshots{}, nil)
+	_ = verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{}})
 
 	_, err := verifier.NextAction()
 	if !errors.Is(err, ErrNoAction) {
@@ -183,7 +183,7 @@ func TestInputText_RoundTrip(t *testing.T) {
 			__uatu__.inputText({ into: "id:phone", text: "+919876543210" }),
 		]);
 	`)
-	_ = verifier.PushSnapshot(Snapshots{}, nil)
+	_ = verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{}})
 
 	action, err := verifier.NextAction()
 	if err != nil {
@@ -202,7 +202,7 @@ func TestPushSnapshot_FeedsSnapshotsToExtractorState(t *testing.T) {
 	mustLoad(t, verifier, `
 		globalThis.captured = __uatu__.extract(state => state.snapshots["k"]);
 	`)
-	if err := verifier.PushSnapshot(Snapshots{"k": json.RawMessage(`"hello"`)}, nil); err != nil {
+	if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{"k": json.RawMessage(`"hello"`)}}); err != nil {
 		t.Fatal(err)
 	}
 	value := verifier.runtime.GlobalObject().Get("captured").ToObject(verifier.runtime).Get("current")

internal/verifier/worker.go

@@ -4,6 +4,7 @@ import (
 	"errors"
 	"fmt"
 	"math/rand/v2"
+	"time"
 
 	"github.com/dop251/goja"
 
@@ -12,15 +13,23 @@ import (
 )
 
 type Verifier struct {
-	runtime    *goja.Runtime
-	extractors []*extractorState
-	formulas   []*formulaState
+	runtime      *goja.Runtime
+	extractors   []*extractorState
+	formulas     []*formulaState
+	formulaSpecs []formulaSpec
 
-	properties      map[string]int // property name -> formula index
+	properties      map[string]int // property name -> formula-spec index
 	actionGenerator goja.Value
 
 	evaluators map[string]*ltl.Evaluator
 
+	lastTree       *hierarchy.Tree
+	lastAction     *Action
+	lastLogs       []LogEntry
+	lastExceptions []Exception
+	stepTime       time.Time
+	runStart       time.Time
+
 	rng *rand.Rand
 }
 
@@ -62,13 +71,16 @@ func (v *Verifier) Load(source string) error {
 			if handle == nil {
 				return fmt.Errorf("property %q is not an object", name)
 			}
-			indexValue := handle.Get("__uatuIndex")
-			if indexValue == nil {
+			specIndex, ok := v.extractSpecIndex(handle)
+			if !ok {
 				return fmt.Errorf("property %q was not produced by always()", name)
 			}
-			index := int(indexValue.ToInteger())
-			v.properties[name] = index
-			v.evaluators[name] = ltl.NewEvaluator(ltl.Always(ltl.Thunk(v.formulaThunk(index))))
+			formula, err := v.buildFormula(specIndex)
+			if err != nil {
+				return fmt.Errorf("property %q: %w", name, err)
+			}
+			v.properties[name] = specIndex
+			v.evaluators[name] = ltl.NewEvaluator(formula)
 		}
 	}
 
@@ -79,11 +91,125 @@ func (v *Verifier) Load(source string) error {
 	return nil
 }
 
+// buildFormula walks the formula-spec registry and produces a Go ltl.Formula
+// tree rooted at the given spec index. Specs built at the top level are
+// always wrapped in Always unless the top-level spec is already an Always.
+func (v *Verifier) buildFormula(rootIndex int) (ltl.Formula, error) {
+	inner, err := v.buildFormulaNode(rootIndex)
+	if err != nil {
+		return nil, err
+	}
+	if _, ok := inner.(ltl.AlwaysFormula); ok {
+		return inner, nil
+	}
+	return ltl.Always(inner), nil
+}
+
+func (v *Verifier) buildFormulaNode(index int) (ltl.Formula, error) {
+	if index < 0 || index >= len(v.formulaSpecs) {
+		return nil, fmt.Errorf("formula spec index %d out of range", index)
+	}
+	spec := v.formulaSpecs[index]
+	switch spec.kind {
+	case specKindPure:
+		return ltl.Pure(spec.pureValue), nil
+	case specKindThunk:
+		return ltl.Thunk(v.formulaThunk(spec.predicateIndex)), nil
+	case specKindNow:
+		child, err := v.buildFormulaNode(spec.childA)
+		if err != nil {
+			return nil, err
+		}
+		return ltl.Now(child), nil
+	case specKindNext:
+		child, err := v.buildFormulaNode(spec.childA)
+		if err != nil {
+			return nil, err
+		}
+		return ltl.Next(child), nil
+	case specKindEventually:
+		child, err := v.buildFormulaNode(spec.childA)
+		if err != nil {
+			return nil, err
+		}
+		formula := ltl.EventuallyFormula{Inner: child}
+		if spec.hasStepBound {
+			formula.StepBound = spec.stepBound
+			formula.HasStepBound = true
+		}
+		if spec.duration > 0 {
+			formula.Duration = spec.duration
+		}
+		return formula, nil
+	case specKindImplies:
+		left, err := v.buildFormulaNode(spec.childA)
+		if err != nil {
+			return nil, err
+		}
+		right, err := v.buildFormulaNode(spec.childB)
+		if err != nil {
+			return nil, err
+		}
+		return ltl.Implies(left, right), nil
+	case specKindOr:
+		left, err := v.buildFormulaNode(spec.childA)
+		if err != nil {
+			return nil, err
+		}
+		right, err := v.buildFormulaNode(spec.childB)
+		if err != nil {
+			return nil, err
+		}
+		return ltl.Or(left, right), nil
+	case specKindAnd:
+		left, err := v.buildFormulaNode(spec.childA)
+		if err != nil {
+			return nil, err
+		}
+		right, err := v.buildFormulaNode(spec.childB)
+		if err != nil {
+			return nil, err
+		}
+		return ltl.And(left, right), nil
+	case specKindNot:
+		child, err := v.buildFormulaNode(spec.childA)
+		if err != nil {
+			return nil, err
+		}
+		return ltl.Not(child), nil
+	case specKindAlways:
+		child, err := v.buildFormulaNode(spec.childA)
+		if err != nil {
+			return nil, err
+		}
+		return ltl.Always(child), nil
+	default:
+		return nil, fmt.Errorf("unknown formula spec kind %d", spec.kind)
+	}
+}
+
 // PushSnapshot updates the JS-side state and refreshes every extractor's
 // current/previous values in registration order. Passing a nil tree is
 // allowed and yields an empty ax scope.
-func (v *Verifier) PushSnapshot(snapshots Snapshots, tree *hierarchy.Tree) error {
-	state, err := stateObject(v.runtime, snapshots, tree)
+func (v *Verifier) PushSnapshot(input SnapshotInput) error {
+	v.lastTree = input.Tree
+	v.lastAction = input.LastAction
+	v.lastLogs = input.Logs
+	v.lastExceptions = input.Exceptions
+	v.stepTime = input.StepTime
+	if v.runStart.IsZero() {
+		v.runStart = input.RunStart
+	}
+
+	state, err := stateObject(v.runtime, stateInput{
+		snapshots:  input.Snapshots,
+		tree:       input.Tree,
+		lastAction: input.LastAction,
+		stepTime:   input.StepTime,
+		runStart:   v.runStart,
+		logs:       input.Logs,
+		exceptions: input.Exceptions,
+	})
 	if err != nil {
 		return fmt.Errorf("build state: %w", err)
 	}
@@ -102,12 +228,47 @@ func (v *Verifier) PushSnapshot(snapshots Snapshots, tree *hierarchy.Tree) error
 	return nil
 }
 
+// SnapshotInput bundles everything a step feeds into the verifier. Fields
+// other than Snapshots are optional; callers that only have snapshots can
+// populate Snapshots alone and leave the rest zero.
+type SnapshotInput struct {
+	Snapshots  Snapshots
+	Tree       *hierarchy.Tree
+	LastAction *Action
+	StepTime   time.Time
+	RunStart   time.Time
+	Logs       []LogEntry
+	Exceptions []Exception
+}
+
+// LogEntry mirrors a logcat line captured between steps.
+type LogEntry struct {
+	UnixMillis int64
+	Level      string
+	Tag        string
+	Message    string
+}
+
+// Exception mirrors an SDK-captured uncaught throwable.
+type Exception struct {
+	Class      string
+	Message    string
+	StackTrace string
+	UnixMillis int64
+}
+
 // EvaluateProperties returns each registered property's running verdict
-// after the most recent PushSnapshot.
+// after the most recent PushSnapshot. The step time passed in PushSnapshot is
+// forwarded to each evaluator so deadline-bound operators see the snapshot's
+// wall clock rather than time.Now().
 func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict {
 	verdicts := map[string]ltl.Verdict{}
+	stepTime := v.stepTime
+	if stepTime.IsZero() {
+		stepTime = time.Now()
+	}
 	for name, evaluator := range v.evaluators {
-		verdicts[name] = evaluator.Observe()
+		verdicts[name] = evaluator.ObserveAt(stepTime)
 	}
 	return verdicts
 }
@@ -178,13 +339,90 @@ func (v *Verifier) resolveGenerator(generator goja.Value) (Action, error) {
 			return Action{}, err
 		}
 		return v.resolveGenerator(picked)
-	case internalKindBuiltinTaps, internalKindBuiltinSwipes:
-		return Action{}, ErrNoAction
+	case internalKindBuiltinTaps:
+		return v.generateRandomTap()
+	case internalKindBuiltinSwipes:
+		return v.generateRandomSwipe()
+	case internalKindBuiltinWaitOnce:
+		return Action{Kind: ActionKindWait, DurationMillis: 500}, nil
+	case internalKindBuiltinPressKey:
+		return v.generateRandomPressKey()
 	default:
 		return Action{}, fmt.Errorf("unknown generator kind %q", kindValue.String())
 	}
 }
 
+// generateRandomTap picks a visible, tappable element from the last
+// hierarchy snapshot and returns a Tap action targeting its center.
+func (v *Verifier) generateRandomTap() (Action, error) {
+	if v.lastTree == nil {
+		return Action{}, ErrNoAction
+	}
+	candidates := make([]*hierarchy.Element, 0, len(v.lastTree.Elements))
+	for _, element := range v.lastTree.Elements {
+		if !element.Clickable || !element.Enabled {
+			continue
+		}
+		if element.Bounds.Right-element.Bounds.Left <= 0 || element.Bounds.Bottom-element.Bounds.Top <= 0 {
+			continue
+		}
+		candidates = append(candidates, element)
+	}
+	if len(candidates) == 0 {
+		return Action{}, ErrNoAction
+	}
+	picked := candidates[v.rng.IntN(len(candidates))]
+	x, y := picked.Bounds.Center()
+	return Action{Kind: ActionKindTap, X: x, Y: y}, nil
+}
+
+// generateRandomSwipe emits a swipe over a random enabled element or the
+// whole screen, in a random direction. Returns ErrNoAction only when we have
+// no tree to size a gesture off of.
+func (v *Verifier) generateRandomSwipe() (Action, error) {
+	if v.lastTree == nil || len(v.lastTree.Elements) == 0 {
+		return Action{}, ErrNoAction
+	}
+	element := v.lastTree.Elements[v.rng.IntN(len(v.lastTree.Elements))]
+	cx, cy := element.Bounds.Center()
+	if cx <= 0 || cy <= 0 {
+		return Action{}, ErrNoAction
+	}
+	// Pick a direction: 0=up 1=down 2=left 3=right; magnitude 200-600 px.
+	magnitude := 200 + v.rng.IntN(401)
+	toX, toY := cx, cy
+	switch v.rng.IntN(4) {
+	case 0:
+		toY = cy - magnitude
+	case 1:
+		toY = cy + magnitude
+	case 2:
+		toX = cx - magnitude
+	case 3:
+		toX = cx + magnitude
+	}
+	if toX < 0 {
+		toX = 0
+	}
+	if toY < 0 {
+		toY = 0
+	}
+	return Action{
+		Kind:           ActionKindSwipe,
+		FromX:          cx,
+		FromY:          cy,
+		ToX:            toX,
+		ToY:            toY,
+		DurationMillis: 250,
+	}, nil
+}
+
+func (v *Verifier) generateRandomPressKey() (Action, error) {
+	// Keep exploration gentle: only "back" for now. Home/menu would navigate
+	// away from the app under test.
+	return Action{Kind: ActionKindPressKey, Key: "back"}, nil
+}
+
 func (v *Verifier) pickFromResult(result goja.Value) (Action, error) {
 	if result == nil || goja.IsUndefined(result) || goja.IsNull(result) {
 		return Action{}, ErrNoAction