feat(verifier): goja runtime hosting the spec API

Installs globalThis.__uatu__ with extract, always, actions,
weighted, tap, inputText, and stub taps/swipes. Load runs the
bundled spec, then pulls properties + actions out of globalThis.
PushSnapshot rebuilds state.snapshots and refreshes every
extractor handle's current/previous in registration order so
chained extractors observe up-to-date values.

Properties are wired through internal/ltl as Always(Thunk(...)),
so verdicts latch to violated as soon as a predicate returns
false. NextAction resolves actions/weighted recursively with a
seedable rand source for reproducible runs.

internal/verifier/bindings.go

@@ -0,0 +1,169 @@
+package verifier
+
+import (
+	"fmt"
+
+	"github.com/dop251/goja"
+)
+
+type ActionKind string
+
+const (
+	ActionKindTap       ActionKind = "Tap"
+	ActionKindInputText ActionKind = "InputText"
+)
+
+type Action struct {
+	Kind ActionKind
+	On   string
+	Text string
+}
+
+type extractorState struct {
+	getter goja.Callable
+	handle *goja.Object
+}
+
+type formulaState struct {
+	predicate goja.Callable
+}
+
+const (
+	tagFormula            = "__uatuFormula"
+	tagActionGenerator    = "__uatuActionGenerator"
+	tagInternalKind       = "__uatuKind"
+	internalKindActions   = "actions"
+	internalKindWeighted  = "weighted"
+	internalKindBuiltinTaps   = "taps"
+	internalKindBuiltinSwipes = "swipes"
+)
+
+// installRuntimeBindings exposes globalThis.__uatu__ to the loaded spec.
+func (v *Verifier) installRuntimeBindings() error {
+	uatu := v.runtime.NewObject()
+
+	if err := uatu.Set("extract", v.bindExtract); err != nil {
+		return err
+	}
+	if err := uatu.Set("always", v.bindAlways); 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("tap", v.bindTap); err != nil {
+		return err
+	}
+	if err := uatu.Set("inputText", v.bindInputText); 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
+	}
+
+	return v.runtime.GlobalObject().Set("__uatu__", uatu)
+}
+
+func (v *Verifier) bindExtract(call goja.FunctionCall) goja.Value {
+	if len(call.Arguments) != 1 {
+		panic(v.runtime.NewTypeError("extract requires exactly one argument"))
+	}
+	getter, ok := goja.AssertFunction(call.Arguments[0])
+	if !ok {
+		panic(v.runtime.NewTypeError("extract argument must be a function"))
+	}
+
+	handle := v.runtime.NewObject()
+	_ = handle.Set("current", goja.Undefined())
+	_ = handle.Set("previous", goja.Undefined())
+
+	v.extractors = append(v.extractors, &extractorState{getter: getter, handle: handle})
+	return handle
+}
+
+func (v *Verifier) bindAlways(call goja.FunctionCall) goja.Value {
+	if len(call.Arguments) != 1 {
+		panic(v.runtime.NewTypeError("always requires exactly one argument"))
+	}
+	predicate, ok := goja.AssertFunction(call.Arguments[0])
+	if !ok {
+		panic(v.runtime.NewTypeError("always argument must be a function"))
+	}
+
+	formula := &formulaState{predicate: predicate}
+	v.formulas = append(v.formulas, formula)
+	formulaIndex := len(v.formulas) - 1
+
+	handle := v.runtime.NewObject()
+	_ = handle.Set(tagFormula, true)
+	_ = handle.Set("__uatuIndex", formulaIndex)
+	return handle
+}
+
+func (v *Verifier) bindActions(call goja.FunctionCall) goja.Value {
+	if len(call.Arguments) != 1 {
+		panic(v.runtime.NewTypeError("actions requires a single generator argument"))
+	}
+	if _, ok := goja.AssertFunction(call.Arguments[0]); !ok {
+		panic(v.runtime.NewTypeError("actions argument must be a function"))
+	}
+	handle := v.runtime.NewObject()
+	_ = handle.Set(tagActionGenerator, true)
+	_ = handle.Set(tagInternalKind, internalKindActions)
+	_ = handle.Set("generate", call.Arguments[0])
+	return handle
+}
+
+func (v *Verifier) bindWeighted(call goja.FunctionCall) goja.Value {
+	entries := v.runtime.NewArray()
+	for index, argument := range call.Arguments {
+		object := argument.ToObject(v.runtime)
+		if object == nil {
+			panic(v.runtime.NewTypeError(fmt.Sprintf("weighted entry %d must be a [number, generator] tuple", index)))
+		}
+		if err := entries.Set(fmt.Sprintf("%d", index), object); err != nil {
+			panic(v.runtime.NewGoError(err))
+		}
+	}
+	handle := v.runtime.NewObject()
+	_ = handle.Set(tagActionGenerator, true)
+	_ = handle.Set(tagInternalKind, internalKindWeighted)
+	_ = handle.Set("entries", entries)
+	return handle
+}
+
+func (v *Verifier) bindTap(call goja.FunctionCall) goja.Value {
+	parameters := call.Argument(0).ToObject(v.runtime)
+	if parameters == nil {
+		panic(v.runtime.NewTypeError("Tap requires {on}"))
+	}
+	handle := v.runtime.NewObject()
+	_ = handle.Set("kind", "Tap")
+	_ = handle.Set("on", parameters.Get("on"))
+	return handle
+}
+
+func (v *Verifier) bindInputText(call goja.FunctionCall) goja.Value {
+	parameters := call.Argument(0).ToObject(v.runtime)
+	if parameters == nil {
+		panic(v.runtime.NewTypeError("InputText requires {into, text}"))
+	}
+	handle := v.runtime.NewObject()
+	_ = handle.Set("kind", "InputText")
+	_ = handle.Set("into", parameters.Get("into"))
+	_ = handle.Set("text", parameters.Get("text"))
+	return handle
+}
+
+func (v *Verifier) builtinGenerator(kind string) *goja.Object {
+	handle := v.runtime.NewObject()
+	_ = handle.Set(tagActionGenerator, true)
+	_ = handle.Set(tagInternalKind, kind)
+	return handle
+}

internal/verifier/marshal.go

@@ -0,0 +1,84 @@
+package verifier
+
+import (
+	"encoding/json"
+	"fmt"
+
+	"github.com/dop251/goja"
+)
+
+// 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 currently a stub returning nothing.
+func stateObject(runtime *goja.Runtime, snapshots Snapshots) (*goja.Object, error) {
+	state := runtime.NewObject()
+	snapshotsObject := runtime.NewObject()
+	for key, raw := range snapshots {
+		value, err := jsonToJSValue(runtime, raw)
+		if err != nil {
+			return nil, fmt.Errorf("snapshot %q: %w", key, err)
+		}
+		if err := snapshotsObject.Set(key, value); err != nil {
+			return nil, err
+		}
+	}
+	if err := state.Set("snapshots", snapshotsObject); err != nil {
+		return nil, err
+	}
+
+	accessibility := runtime.NewObject()
+	if err := accessibility.Set("find", runtime.ToValue(func(string) goja.Value { return goja.Undefined() })); err != nil {
+		return nil, err
+	}
+	if err := accessibility.Set("findAll", runtime.ToValue(func(string) []goja.Value { return nil })); err != nil {
+		return nil, err
+	}
+	if err := state.Set("ax", accessibility); err != nil {
+		return nil, err
+	}
+	return state, nil
+}
+
+func jsonToJSValue(runtime *goja.Runtime, raw json.RawMessage) (goja.Value, error) {
+	if len(raw) == 0 {
+		return goja.Undefined(), nil
+	}
+	var generic any
+	if err := json.Unmarshal(raw, &generic); err != nil {
+		return nil, fmt.Errorf("decode JSON: %w", err)
+	}
+	return runtime.ToValue(generic), nil
+}
+
+// jsValueToAction converts a JS-side {kind, on?, into?, text?} 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")
+	}
+	object := value.ToObject(runtime)
+	kindValue := object.Get("kind")
+	if kindValue == nil {
+		return Action{}, fmt.Errorf("action missing kind")
+	}
+	kind := kindValue.String()
+	switch kind {
+	case "Tap":
+		on := object.Get("on")
+		return Action{Kind: ActionKindTap, On: stringOf(on)}, nil
+	case "InputText":
+		into := object.Get("into")
+		text := object.Get("text")
+		return Action{Kind: ActionKindInputText, On: stringOf(into), Text: stringOf(text)}, nil
+	default:
+		return Action{}, fmt.Errorf("unknown action kind %q", kind)
+	}
+}
+
+func stringOf(value goja.Value) string {
+	if value == nil || goja.IsNull(value) || goja.IsUndefined(value) {
+		return ""
+	}
+	return value.String()
+}

internal/verifier/worker.go

@@ -0,0 +1,232 @@
+package verifier
+
+import (
+	"errors"
+	"fmt"
+	"math/rand/v2"
+
+	"github.com/dop251/goja"
+
+	"github.com/priyanshujain/uatu/internal/ltl"
+)
+
+type Verifier struct {
+	runtime    *goja.Runtime
+	extractors []*extractorState
+	formulas   []*formulaState
+
+	properties      map[string]int // property name -> formula index
+	actionGenerator goja.Value
+
+	evaluators map[string]*ltl.Evaluator
+
+	rng *rand.Rand
+}
+
+type Option func(*Verifier)
+
+func WithRand(rng *rand.Rand) Option {
+	return func(v *Verifier) { v.rng = rng }
+}
+
+func New(options ...Option) (*Verifier, error) {
+	verifier := &Verifier{
+		runtime:    goja.New(),
+		properties: map[string]int{},
+		evaluators: map[string]*ltl.Evaluator{},
+		rng:        rand.New(rand.NewPCG(0, 0)),
+	}
+	for _, option := range options {
+		option(verifier)
+	}
+	if err := verifier.installRuntimeBindings(); err != nil {
+		return nil, fmt.Errorf("install bindings: %w", err)
+	}
+	return verifier, nil
+}
+
+// Load executes the bundled spec source. The spec is expected to assign its
+// property formulas to globalThis.properties and its root action generator
+// to globalThis.actions.
+func (v *Verifier) Load(source string) error {
+	if _, err := v.runtime.RunString(source); err != nil {
+		return fmt.Errorf("run spec: %w", err)
+	}
+
+	propertiesValue := v.runtime.GlobalObject().Get("properties")
+	if propertiesValue != nil && !goja.IsUndefined(propertiesValue) && !goja.IsNull(propertiesValue) {
+		propertiesObject := propertiesValue.ToObject(v.runtime)
+		for _, name := range propertiesObject.Keys() {
+			handle := propertiesObject.Get(name).ToObject(v.runtime)
+			if handle == nil {
+				return fmt.Errorf("property %q is not an object", name)
+			}
+			indexValue := handle.Get("__uatuIndex")
+			if indexValue == nil {
+				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))))
+		}
+	}
+
+	if actionsValue := v.runtime.GlobalObject().Get("actions"); actionsValue != nil && !goja.IsUndefined(actionsValue) && !goja.IsNull(actionsValue) {
+		v.actionGenerator = actionsValue
+	}
+
+	return nil
+}
+
+// PushSnapshot updates the JS-side state and refreshes every extractor's
+// current/previous values in registration order.
+func (v *Verifier) PushSnapshot(snapshots Snapshots) error {
+	state, err := stateObject(v.runtime, snapshots)
+	if err != nil {
+		return fmt.Errorf("build state: %w", err)
+	}
+	if err := v.runtime.GlobalObject().Set("state", state); err != nil {
+		return fmt.Errorf("set state: %w", err)
+	}
+	for index, extractor := range v.extractors {
+		previous := extractor.handle.Get("current")
+		_ = extractor.handle.Set("previous", previous)
+		newValue, err := extractor.getter(goja.Undefined(), state)
+		if err != nil {
+			return fmt.Errorf("extractor %d: %w", index, err)
+		}
+		_ = extractor.handle.Set("current", newValue)
+	}
+	return nil
+}
+
+// EvaluateProperties returns each registered property's running verdict
+// after the most recent PushSnapshot.
+func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict {
+	verdicts := map[string]ltl.Verdict{}
+	for name, evaluator := range v.evaluators {
+		verdicts[name] = evaluator.Observe()
+	}
+	return verdicts
+}
+
+// NextAction resolves the root action generator into a single Action.
+// Returns ErrNoAction when the generator yields nothing actionable.
+func (v *Verifier) NextAction() (Action, error) {
+	if v.actionGenerator == nil {
+		return Action{}, ErrNoAction
+	}
+	return v.resolveGenerator(v.actionGenerator)
+}
+
+var ErrNoAction = errors.New("verifier: no action available")
+
+func (v *Verifier) formulaThunk(index int) func() bool {
+	return func() bool {
+		formula := v.formulas[index]
+		result, err := formula.predicate(goja.Undefined())
+		if err != nil {
+			panic(fmt.Errorf("predicate panic: %w", err))
+		}
+		return result.ToBoolean()
+	}
+}
+
+func (v *Verifier) resolveGenerator(generator goja.Value) (Action, error) {
+	object := generator.ToObject(v.runtime)
+	if object == nil {
+		return Action{}, fmt.Errorf("generator is not an object")
+	}
+	kindValue := object.Get(tagInternalKind)
+	if kindValue == nil {
+		return Action{}, fmt.Errorf("generator missing internal kind tag")
+	}
+	switch kindValue.String() {
+	case internalKindActions:
+		generateValue := object.Get("generate")
+		generate, ok := goja.AssertFunction(generateValue)
+		if !ok {
+			return Action{}, fmt.Errorf("actions handle missing generate function")
+		}
+		result, err := generate(goja.Undefined())
+		if err != nil {
+			return Action{}, fmt.Errorf("generate: %w", err)
+		}
+		return v.pickFromResult(result)
+	case internalKindWeighted:
+		entries := object.Get("entries").ToObject(v.runtime)
+		if entries == nil {
+			return Action{}, fmt.Errorf("weighted handle missing entries")
+		}
+		picked, err := v.pickWeighted(entries)
+		if err != nil {
+			return Action{}, err
+		}
+		return v.resolveGenerator(picked)
+	case internalKindBuiltinTaps, internalKindBuiltinSwipes:
+		return Action{}, ErrNoAction
+	default:
+		return Action{}, fmt.Errorf("unknown generator kind %q", kindValue.String())
+	}
+}
+
+func (v *Verifier) pickFromResult(result goja.Value) (Action, error) {
+	if result == nil || goja.IsUndefined(result) || goja.IsNull(result) {
+		return Action{}, ErrNoAction
+	}
+	object := result.ToObject(v.runtime)
+	if object == nil {
+		return Action{}, ErrNoAction
+	}
+	lengthValue := object.Get("length")
+	if lengthValue == nil {
+		return jsValueToAction(v.runtime, result)
+	}
+	length := int(lengthValue.ToInteger())
+	if length == 0 {
+		return Action{}, ErrNoAction
+	}
+	pick := v.rng.IntN(length)
+	return jsValueToAction(v.runtime, object.Get(fmt.Sprintf("%d", pick)))
+}
+
+func (v *Verifier) pickWeighted(entries *goja.Object) (goja.Value, error) {
+	lengthValue := entries.Get("length")
+	if lengthValue == nil {
+		return nil, fmt.Errorf("weighted entries missing length")
+	}
+	length := int(lengthValue.ToInteger())
+	if length == 0 {
+		return nil, ErrNoAction
+	}
+
+	weights := make([]float64, length)
+	generators := make([]goja.Value, length)
+	totalWeight := 0.0
+	for index := range length {
+		entry := entries.Get(fmt.Sprintf("%d", index)).ToObject(v.runtime)
+		if entry == nil {
+			return nil, fmt.Errorf("weighted entry %d not an array", index)
+		}
+		weight := entry.Get("0").ToFloat()
+		generator := entry.Get("1")
+		if weight < 0 {
+			weight = 0
+		}
+		weights[index] = weight
+		generators[index] = generator
+		totalWeight += weight
+	}
+	if totalWeight == 0 {
+		return nil, ErrNoAction
+	}
+	pick := v.rng.Float64() * totalWeight
+	cumulative := 0.0
+	for index := range length {
+		cumulative += weights[index]
+		if pick < cumulative {
+			return generators[index], nil
+		}
+	}
+	return generators[length-1], nil
+}