Files
sanderling/internal/verifier/bindings.go
T
pj 9abd0511bd fix(verifier): refresh predicate errors per step
EvaluateProperties short-circuits once an Always-property latches to
violated, so the underlying goja predicate stops being called and
formula.err keeps whatever it threw at step 1. The runner logs
PredicateError every step a property is violated, which made every
subsequent log line repeat the step-1 throw. That looks like the spec
runtime is seeing stale state, but it is just stale error reporting.

EvaluateProperties now invokes every registered predicate once per step
purely to refresh formula.err. Verdicts are unaffected. The thunk
itself stops latching so the new value wins on whichever path runs first.
2026-04-26 15:44:01 +07:00

445 lines
13 KiB
Go

package verifier
import (
"fmt"
"time"
"github.com/dop251/goja"
)
type extractorState struct {
getter goja.Callable
handle *goja.Object
}
type formulaState struct {
predicate goja.Callable
// err holds the goja error from this thunk's most recent invocation, or
// nil if the latest call succeeded. The thunk returns false on error so
// the LTL evaluator marks the property violated; PredicateError surfaces
// the underlying cause for the current step.
err error
}
type specKind int
const (
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 = "__sanderlingFormula"
tagFormulaSpecIndex = "__sanderlingFormulaSpec"
tagActionGenerator = "__sanderlingActionGenerator"
tagInternalKind = "__sanderlingKind"
tagSelector = "__sanderlingSelector"
internalKindActions = "actions"
internalKindWeighted = "weighted"
internalKindBuiltinTaps = "taps"
internalKindBuiltinSwipes = "swipes"
internalKindBuiltinWaitOnce = "waitOnce"
internalKindBuiltinPressKey = "pressKey"
)
// installRuntimeBindings exposes globalThis.__sanderling__ to the loaded spec.
func (v *Verifier) installRuntimeBindings() error {
sanderling := v.runtime.NewObject()
if err := sanderling.Set("extract", v.bindExtract); err != nil {
return err
}
if err := sanderling.Set("always", v.bindAlways); err != nil {
return err
}
if err := sanderling.Set("now", v.bindNow); err != nil {
return err
}
if err := sanderling.Set("next", v.bindNext); err != nil {
return err
}
if err := sanderling.Set("eventually", v.bindEventually); err != nil {
return err
}
if err := sanderling.Set("actions", v.bindActions); err != nil {
return err
}
if err := sanderling.Set("weighted", v.bindWeighted); err != nil {
return err
}
if err := sanderling.Set("from", v.bindFrom); err != nil {
return err
}
if err := sanderling.Set("tap", v.bindTap); err != nil {
return err
}
if err := sanderling.Set("inputText", v.bindInputText); err != nil {
return err
}
if err := sanderling.Set("swipe", v.bindSwipe); err != nil {
return err
}
if err := sanderling.Set("pressKey", v.bindPressKey); err != nil {
return err
}
if err := sanderling.Set("wait", v.bindWait); err != nil {
return err
}
if err := sanderling.Set("taps", v.builtinGenerator(internalKindBuiltinTaps)); err != nil {
return err
}
if err := sanderling.Set("swipes", v.builtinGenerator(internalKindBuiltinSwipes)); err != nil {
return err
}
if err := sanderling.Set("waitOnce", v.builtinGenerator(internalKindBuiltinWaitOnce)); err != nil {
return err
}
if err := sanderling.Set("pressKeys", v.builtinGenerator(internalKindBuiltinPressKey)); err != nil {
return err
}
return v.runtime.GlobalObject().Set("__sanderling__", sanderling)
}
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
}
// bindAlways accepts either a predicate function (legacy shape) or a formula
// handle (new shape). Both produce a formula handle tagged with
// __sanderlingFormulaSpec.
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(name + " argument must be a function"))
}
return v.registerThunk(predicate)
}
// 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(tagFormulaSpecIndex, index)
// Keep __sanderlingIndex as an alias so older property shapes that read it keep
// working during backward-compat transitions.
_ = handle.Set("__sanderlingIndex", 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 __sanderlingFormulaSpec 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"))
}
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
}
// 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 {
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) 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)
_ = handle.Set(tagInternalKind, kind)
return handle
}