mirror of
https://github.com/priyanshujain/sanderling.git
synced 2026-10-02 19:17:10 +00:00
* fix(ltl): give every thunk a construction identity Two distinct unnamed predicates both described as "Thunk(...)", so obligation collapse merged their residuals and could drop a live violation. Identity is assigned at construction and the fields are unexported, so a thunk cannot be built without one. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(ltl): reduce a thrown-predicate residual instead of panicking The verifier substitutes an ErrorFormula for the residual of a property whose predicate threw, and that residual is fed back in on the next step. reduce had no case for it, so the run crashed. It re-reports the same failure now. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(ltl): make a bounded always the dual of a bounded eventually G<=n(f) and not F<=n(not f) disagreed on traces where the inner was still pending when the window closed, so nnf's negation normal form was not semantics preserving. Both sides now range over the observations at which their inner can definitely resolve: the eventually keeps a pending inner as a disjunct, and the always discharges vacuously at window close. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(ltl): arm a one-shot root once per run A root that carries its own horizon is one obligation for the whole run, not one per observation. Re-instantiating a top-level eventually monitored G F<=n(p) instead of F<=n(p) and left one live obligation per step behind; a bounded always restarted its window every step and never closed. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(verifier): stop wrapping a top-level eventually in always `eventually(p).within(300, "seconds")` as a property meant "within 300 seconds of every step", which spawned an obligation per step with its own resolved deadline. A 553-step run carried 553 of them and serialized a 75 KB residual. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(ltl): serialize the resolved deadline of a bounded window Two obligations spawned at different steps from one duration-bounded formula differ only in the deadline the evaluator resolved for them, so they serialized identically and the trace erased a distinction the evaluator makes. The authored window stays in amount/unit; the resolved deadline rides alongside. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(verifier): split a witness's origin step from its detection step A deferred obligation spans two steps: the one that armed it and the one whose reduction failed. They were conflated under one index, so the extractor snapshot (which is the detecting step's state) was reported against the origin step. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(runner): record a witness's detection step in the trace Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * feat(replay-ui): show the step a violation was detected at The witness evidence is the detecting step's state, so say which step that is and let a reader jump to it. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(verifier): record the extractor state the predicates actually read On the web path extractor bodies are evaluated in V8 and injected here, but only the goja value was replaced. The trace diff and the violation witness therefore described a state no property ever saw. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * refactor(spec): one candidate producer over one target-eligibility rule Both hosts routed verbs themselves and both policies enumerated their own actions, and all four drifted. Web sent `swipes` to scrollable containers only, so swipe-to-dismiss on a list row was reachable on native and unreachable on web; the model policy folded gestures its own way and could not reach what the seeded picker drew. A host now reports facts about every element and never decides which verb may act on it: targets.ts acceptsTarget owns that for both. pick.ts builtinCandidates is the single enumeration, and the model policy reads it through __sanderlingEnumerateBuiltin__ instead of reimplementing it in Go. Gesture verbs change with it: scrolls stay vertical over scrollable containers, swipes go free-form in all four directions from any element with real bounds. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(runner): name a builtin scroll by its drag origin A builtin gesture carries endpoints and no selector, so every scroll rendered as "Scroll down " in the prompt's recent-action memory and two scrollable regions were indistinguishable. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(chrome): clear storage over cdp instead of scripting an opaque origin Launch runs while the tab is still on about:blank, whose opaque origin denies storage access, so localStorage.clear() threw SecurityError and every web run died at launch. Storage.clearDataForOrigin needs no navigation. The exception helper lands here because "Uncaught" is what hid this for so long. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(chrome): enable the swiftshader webgl fallback Headless Chrome runs with --disable-gpu, and without this flag it refuses the software WebGL backend: getContext returns null, so a canvas-rendered app paints nothing and every screenshot is identical black. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(web): resolve testTag through data-testid or id Compose Multiplatform emits its testTag into the element id, which the native table already accepts via the resource-id alias. The two web selector tables were the only place that rejected it. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * test(spec): type-check the spec api as part of make test The fake runtime in api.test.ts did not return a chainable handle from extract, so the file had not type-checked since named() was added. Wiring the check into make test stops it drifting again. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * docs(manual): one-shot eventually and the gesture verbs Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
385 lines
14 KiB
Go
385 lines
14 KiB
Go
package verifier
|
|
|
|
import (
|
|
"strings"
|
|
"testing"
|
|
|
|
"github.com/priyanshujain/sanderling/internal/hierarchy"
|
|
)
|
|
|
|
// enumTreeJSON exercises every labeling path: a clickable wrapper whose own text
|
|
// is empty but whose child Text reads "Add credit" (descendant borrowing), an
|
|
// editable field labeled by its hint, a text-labeled button, a DISABLED button,
|
|
// and a scrollable list (the only valid scroll origin).
|
|
const enumTreeJSON = `{
|
|
"attributes": {"bounds": "[0,0,1080,2400]"},
|
|
"children": [
|
|
{"attributes": {"resource-id": "AddCredit", "bounds": "[0,100,1080,200]"}, "clickable": true, "enabled": true, "children": [
|
|
{"attributes": {"text": "Add credit", "bounds": "[0,100,540,200]"}, "children": []}
|
|
]},
|
|
{"attributes": {"resource-id": "Amount", "class": "EditText", "hintText": "Amount", "bounds": "[0,300,1080,400]"}, "enabled": true, "children": []},
|
|
{"attributes": {"resource-id": "SignIn", "text": "Sign in", "bounds": "[0,450,1080,550]"}, "clickable": true, "enabled": true, "children": []},
|
|
{"attributes": {"resource-id": "Off", "text": "Off", "bounds": "[0,600,1080,700]"}, "clickable": true, "enabled": false, "children": []},
|
|
{"attributes": {"resource-id": "List", "scrollable": "true", "bounds": "[0,800,1080,2000]"}, "children": []}
|
|
]
|
|
}`
|
|
|
|
// enumVerifier loads a spec whose actions root is the given plain-object graph
|
|
// and stages the given tree, so Candidates walks a controlled action tree. The
|
|
// spec is bundled with the goja runtime entry because the model arm reads the
|
|
// picker's own builtin enumeration out of that bundle.
|
|
func enumVerifier(t *testing.T, actionsJS, treeJSON string) *Verifier {
|
|
t.Helper()
|
|
v := newVerifier(t)
|
|
loadActionSpec(t, v, "globalThis.actions = "+actionsJS+";")
|
|
tree, err := hierarchy.Parse(treeJSON)
|
|
if err != nil {
|
|
t.Fatalf("parse tree: %v", err)
|
|
}
|
|
v.lastTree = tree
|
|
return v
|
|
}
|
|
|
|
func findCandidate(candidates []ActionCandidate, description string) (ActionCandidate, bool) {
|
|
for _, candidate := range candidates {
|
|
if candidate.Description == description {
|
|
return candidate, true
|
|
}
|
|
}
|
|
return ActionCandidate{}, false
|
|
}
|
|
|
|
func hasCandidate(candidates []ActionCandidate, description string) bool {
|
|
_, ok := findCandidate(candidates, description)
|
|
return ok
|
|
}
|
|
|
|
func TestCandidatesLabelsControlsByVisibleText(t *testing.T) {
|
|
v := enumVerifier(t, "{kind:'builtin', verb:'taps'}", enumTreeJSON)
|
|
candidates := v.Candidates()
|
|
|
|
// The empty-text clickable wrapper is labeled by its child Text, NOT its
|
|
// resource-id.
|
|
if !hasCandidate(candidates, `Tap "Add credit"`) {
|
|
t.Errorf("want Tap \"Add credit\" (descendant text), got %v", descriptions(candidates))
|
|
}
|
|
// The plain text button is labeled by its own text.
|
|
if !hasCandidate(candidates, `Tap "Sign in"`) {
|
|
t.Errorf("want Tap \"Sign in\", got %v", descriptions(candidates))
|
|
}
|
|
// Descriptions are never the opaque resource-id.
|
|
if hasCandidate(candidates, `Tap "AddCredit"`) {
|
|
t.Error("labeled a control by its resource-id instead of visible text")
|
|
}
|
|
// Indices are dense and 1-based.
|
|
for i, candidate := range candidates {
|
|
if candidate.Index != i+1 {
|
|
t.Errorf("candidate %d has Index %d, want %d", i, candidate.Index, i+1)
|
|
}
|
|
}
|
|
}
|
|
|
|
func TestCandidatesDropsDisabledControls(t *testing.T) {
|
|
v := enumVerifier(t, "{kind:'builtin', verb:'taps'}", enumTreeJSON)
|
|
for _, candidate := range v.Candidates() {
|
|
if strings.Contains(candidate.Description, "Off") {
|
|
t.Errorf("disabled control surfaced as %q", candidate.Description)
|
|
}
|
|
}
|
|
}
|
|
|
|
func TestCandidatesTypingExposesInputType(t *testing.T) {
|
|
v := enumVerifier(t, "{kind:'builtin', verb:'typing'}", enumTreeJSON)
|
|
candidates := v.Candidates()
|
|
candidate, ok := findCandidate(candidates, `Type into "Amount" (number)`)
|
|
if !ok {
|
|
t.Fatalf("want typing candidate with input type, got %v", descriptions(candidates))
|
|
}
|
|
if !candidate.LLMText {
|
|
t.Error("builtin typing must flag LLMText so the model supplies the value")
|
|
}
|
|
if candidate.InputType != "number" {
|
|
t.Errorf("InputType = %q, want number", candidate.InputType)
|
|
}
|
|
}
|
|
|
|
func TestCandidatesLabelsEditableFieldByHintNotTypedValue(t *testing.T) {
|
|
// A field already showing "99" must still be labeled by its purpose (the
|
|
// hint), not by its transient content, so the description stays stable.
|
|
tree := `{
|
|
"attributes": {"bounds": "[0,0,400,800]"},
|
|
"children": [
|
|
{"attributes": {"resource-id": "Amt", "class": "EditText", "hintText": "Amount", "text": "99", "bounds": "[0,0,400,100]"}, "enabled": true, "children": []}
|
|
]
|
|
}`
|
|
v := enumVerifier(t, "{kind:'builtin', verb:'typing'}", tree)
|
|
candidates := v.Candidates()
|
|
if hasCandidate(candidates, `Type into "99" (number)`) || hasCandidate(candidates, `Type into "99"`) {
|
|
t.Errorf("editable field labeled by its typed value: %v", descriptions(candidates))
|
|
}
|
|
if !hasCandidate(candidates, `Type into "Amount" (number)`) {
|
|
t.Errorf("want the field labeled by its hint, got %v", descriptions(candidates))
|
|
}
|
|
}
|
|
|
|
func TestCandidatesKeepsGestureVerbsDistinct(t *testing.T) {
|
|
v := enumVerifier(t,
|
|
"{kind:'weighted', branches:[[1,{kind:'builtin',verb:'scrolls'}],[1,{kind:'builtin',verb:'swipes'}]]}",
|
|
enumTreeJSON)
|
|
candidates := v.Candidates()
|
|
|
|
// `scrolls` folds to one directional pair over the single scrollable
|
|
// container, which is what keeps the list short.
|
|
if !hasCandidate(candidates, "Scroll down") || !hasCandidate(candidates, "Scroll up") {
|
|
t.Errorf("want directional scrolls, got %v", descriptions(candidates))
|
|
}
|
|
if got := count(candidates, "Scroll down"); got != 1 {
|
|
t.Errorf("Scroll down appears %d times, want 1 over the one container", got)
|
|
}
|
|
// `swipes` is a different verb, not a second name for the scroll: a
|
|
// free-form drag from any element, named by the control it starts on. That
|
|
// is what puts swipe-to-dismiss on a row within the model's reach.
|
|
if !hasCandidatePrefix(candidates, `Swipe "Sign in"`) {
|
|
t.Errorf("want a swipe naming the non-scrollable row, got %v", descriptions(candidates))
|
|
}
|
|
if hasCandidatePrefix(candidates, "Scroll \"") {
|
|
t.Errorf("scroll candidates must stay container-scoped: %v", descriptions(candidates))
|
|
}
|
|
}
|
|
|
|
func hasCandidatePrefix(candidates []ActionCandidate, prefix string) bool {
|
|
for _, candidate := range candidates {
|
|
if strings.HasPrefix(candidate.Description, prefix) {
|
|
return true
|
|
}
|
|
}
|
|
return false
|
|
}
|
|
|
|
func TestCandidatesWeightsCombineAcrossPaths(t *testing.T) {
|
|
// A single clickable reached through two equal branches: its weight sums to
|
|
// the full distribution.
|
|
oneClickable := `{
|
|
"attributes": {"bounds": "[0,0,400,800]"},
|
|
"children": [
|
|
{"attributes": {"resource-id": "SignIn", "text": "Sign in", "bounds": "[0,0,400,100]"}, "clickable": true, "enabled": true, "children": []}
|
|
]
|
|
}`
|
|
v := enumVerifier(t,
|
|
"{kind:'weighted', branches:[[1,{kind:'builtin',verb:'taps'}],[1,{kind:'builtin',verb:'taps'}]]}",
|
|
oneClickable)
|
|
candidates := v.Candidates()
|
|
if len(candidates) != 1 {
|
|
t.Fatalf("want one deduped candidate, got %v", descriptions(candidates))
|
|
}
|
|
candidate := candidates[0]
|
|
if !candidate.Weighted {
|
|
t.Fatal("candidate under a weighted tree must be Weighted")
|
|
}
|
|
if candidate.Weight != 100 {
|
|
t.Errorf("summed weight = %d, want 100", candidate.Weight)
|
|
}
|
|
}
|
|
|
|
func TestCandidatesWeightReflectsBranchShare(t *testing.T) {
|
|
v := enumVerifier(t,
|
|
"{kind:'weighted', branches:[[1,{kind:'builtin',verb:'taps'}],[3,{kind:'builtin',verb:'typing'}]]}",
|
|
enumTreeJSON)
|
|
candidates := v.Candidates()
|
|
tap, ok := findCandidate(candidates, `Tap "Sign in"`)
|
|
if !ok {
|
|
t.Fatalf("missing tap candidate: %v", descriptions(candidates))
|
|
}
|
|
if tap.Weight != 25 {
|
|
t.Errorf("tap weight = %d, want 25 (1/4 share)", tap.Weight)
|
|
}
|
|
typing, ok := findCandidate(candidates, `Type into "Amount" (number)`)
|
|
if !ok {
|
|
t.Fatalf("missing typing candidate: %v", descriptions(candidates))
|
|
}
|
|
if typing.Weight != 75 {
|
|
t.Errorf("typing weight = %d, want 75 (3/4 share)", typing.Weight)
|
|
}
|
|
}
|
|
|
|
func TestCandidatesUnweightedTreeShowsNoWeight(t *testing.T) {
|
|
v := enumVerifier(t, "{kind:'builtin', verb:'taps'}", enumTreeJSON)
|
|
for _, candidate := range v.Candidates() {
|
|
if candidate.Weighted || candidate.Weight != 0 {
|
|
t.Errorf("%q carries a weight despite no weighted node", candidate.Description)
|
|
}
|
|
}
|
|
}
|
|
|
|
func TestCandidatesCallsAuthoredLeafOnce(t *testing.T) {
|
|
actions := `{kind:'actions', generate: () => [
|
|
{kind:'Tap', on:'id:SignIn'},
|
|
{kind:'Tap', on:'id:Off'},
|
|
{kind:'InputText', into:'id:Amount', text:'42'}
|
|
]}`
|
|
v := enumVerifier(t, actions, enumTreeJSON)
|
|
candidates := v.Candidates()
|
|
|
|
// Authored Tap resolves its selector to the visible-text label.
|
|
if !hasCandidate(candidates, `Tap "Sign in"`) {
|
|
t.Errorf("authored tap missing: %v", descriptions(candidates))
|
|
}
|
|
// A disabled authored target is dropped.
|
|
for _, candidate := range candidates {
|
|
if strings.Contains(candidate.Description, "Off") {
|
|
t.Errorf("authored action on disabled control surfaced: %q", candidate.Description)
|
|
}
|
|
}
|
|
// Authored InputText replays its own sampled value (LLM does not supply it).
|
|
authored, ok := findCandidate(candidates, `Type "42" into "Amount"`)
|
|
if !ok {
|
|
t.Fatalf("authored typing missing: %v", descriptions(candidates))
|
|
}
|
|
if authored.LLMText {
|
|
t.Error("authored InputText must not request an LLM-supplied value")
|
|
}
|
|
if authored.Action.Text != "42" {
|
|
t.Errorf("authored text = %q, want 42", authored.Action.Text)
|
|
}
|
|
}
|
|
|
|
func TestCandidatesSurfaceAuthoredUntargetedActions(t *testing.T) {
|
|
// A spec that authors a swipe, a key press, or a wait must reach the model
|
|
// with all three: the seeded picker executes whatever the leaf returns, so a
|
|
// kind the enumeration drops is an action only one policy can take.
|
|
actions := `{kind:'actions', generate: () => [
|
|
{kind:'Swipe', from:{x:10,y:600}, to:{x:10,y:100}, durationMillis: 250},
|
|
{kind:'PressKey', key:'back'},
|
|
{kind:'Wait'}
|
|
]}`
|
|
candidates := enumVerifier(t, actions, enumTreeJSON).Candidates()
|
|
for _, want := range []string{"Swipe from (10,600) to (10,100)", "Press back", "Wait"} {
|
|
if !hasCandidate(candidates, want) {
|
|
t.Errorf("authored %q missing: %v", want, descriptions(candidates))
|
|
}
|
|
}
|
|
}
|
|
|
|
func TestCandidatesOffRouteLeafYieldsNothing(t *testing.T) {
|
|
v := enumVerifier(t, "{kind:'actions', generate: () => []}", enumTreeJSON)
|
|
if got := v.Candidates(); len(got) != 0 {
|
|
t.Errorf("off-route leaf should yield no candidates, got %v", descriptions(got))
|
|
}
|
|
}
|
|
|
|
func TestCandidatesSkipsCrossFadeFrames(t *testing.T) {
|
|
// Two route *Screen tags alive at once is a NavHost cross-fade: its layout is
|
|
// mid-animation (collapsed coordinate space), so the LLM must NOT act on it.
|
|
crossFade := `{
|
|
"attributes": {"bounds": "[0,0,320,640]"},
|
|
"children": [
|
|
{"attributes": {"resource-id": "LedgerScreen", "bounds": "[0,0,320,640]"}, "children": [
|
|
{"attributes": {"resource-id": "TxnSubmit", "text": "Add credit", "bounds": "[20,332,300,380]"}, "clickable": true, "enabled": true, "children": []}
|
|
]},
|
|
{"attributes": {"resource-id": "AddTransactionScreen", "bounds": "[0,0,320,640]"}, "children": []}
|
|
]
|
|
}`
|
|
v := enumVerifier(t, "{kind:'builtin', verb:'taps'}", crossFade)
|
|
if got := v.Candidates(); len(got) != 0 {
|
|
t.Errorf("cross-fade frame should yield no candidates, got %v", descriptions(got))
|
|
}
|
|
// The seeded policy is skipped by the SAME guard, in the shared producer,
|
|
// so neither arm acts on a mid-animation layout.
|
|
if got := v.targets(); len(got) != 0 {
|
|
t.Errorf("cross-fade frame should yield no host targets, got %d", len(got))
|
|
}
|
|
}
|
|
|
|
func TestCandidatesNilWithoutTreeOrActions(t *testing.T) {
|
|
withActions := newLoadedVerifier(t, "globalThis.actions = {kind:'builtin', verb:'taps'};")
|
|
if got := withActions.Candidates(); got != nil {
|
|
t.Errorf("Candidates with no tree = %v, want nil", got)
|
|
}
|
|
noActions := newLoadedVerifier(t, "globalThis.properties = {};")
|
|
tree, _ := hierarchy.Parse(enumTreeJSON)
|
|
noActions.lastTree = tree
|
|
if got := noActions.Candidates(); got != nil {
|
|
t.Errorf("Candidates with no actions root = %v, want nil", got)
|
|
}
|
|
}
|
|
|
|
func descriptions(candidates []ActionCandidate) []string {
|
|
out := make([]string, len(candidates))
|
|
for i, candidate := range candidates {
|
|
out[i] = candidate.Description
|
|
}
|
|
return out
|
|
}
|
|
|
|
func count(candidates []ActionCandidate, description string) int {
|
|
n := 0
|
|
for _, candidate := range candidates {
|
|
if candidate.Description == description {
|
|
n++
|
|
}
|
|
}
|
|
return n
|
|
}
|
|
|
|
func TestLLMConfigDetectsMarker(t *testing.T) {
|
|
v := newLoadedVerifier(t, `globalThis.generator = { kind: "llm", config: { model: "vendor/model" } };`)
|
|
config, ok := v.LLMConfig()
|
|
if !ok {
|
|
t.Fatal("LLMConfig not detected for llm marker")
|
|
}
|
|
if config.Model != "vendor/model" {
|
|
t.Errorf("model = %q, want vendor/model", config.Model)
|
|
}
|
|
if config.Instructions != "" {
|
|
t.Errorf("instructions = %q, want empty when unset", config.Instructions)
|
|
}
|
|
}
|
|
|
|
func TestLLMConfigReadsInstructions(t *testing.T) {
|
|
v := newLoadedVerifier(t, `globalThis.generator = { kind: "llm", config: { model: "m", instructions: "find bugs" } };`)
|
|
config, ok := v.LLMConfig()
|
|
if !ok {
|
|
t.Fatal("LLMConfig not detected")
|
|
}
|
|
if config.Instructions != "find bugs" {
|
|
t.Errorf("instructions = %q, want %q", config.Instructions, "find bugs")
|
|
}
|
|
}
|
|
|
|
func TestLLMConfigAbsentForSeededSpec(t *testing.T) {
|
|
v := newLoadedVerifier(t, `globalThis.actions = { kind: "builtin", verb: "taps" };`)
|
|
if _, ok := v.LLMConfig(); ok {
|
|
t.Error("LLMConfig should be false when no generator is declared")
|
|
}
|
|
}
|
|
|
|
func TestSampleInputErrorsWithoutBundle(t *testing.T) {
|
|
v := newLoadedVerifier(t, `globalThis.actions = { kind: "llm", config: { model: "m" } };`)
|
|
if _, err := v.SampleInput(); err == nil {
|
|
t.Error("expected SampleInput to error when the sampler is not installed")
|
|
}
|
|
}
|
|
|
|
func TestSampleInputDrawsFromCorpus(t *testing.T) {
|
|
v := newLoadedVerifier(t, `globalThis.__sanderlingSampleInput__ = () => "sampled";`)
|
|
got, err := v.SampleInput()
|
|
if err != nil {
|
|
t.Fatalf("SampleInput: %v", err)
|
|
}
|
|
if got != "sampled" {
|
|
t.Errorf("SampleInput = %q, want sampled", got)
|
|
}
|
|
}
|
|
|
|
func newLoadedVerifier(t *testing.T, source string) *Verifier {
|
|
t.Helper()
|
|
v, err := New()
|
|
if err != nil {
|
|
t.Fatalf("New: %v", err)
|
|
}
|
|
if err := v.Load(source); err != nil {
|
|
t.Fatalf("Load: %v", err)
|
|
}
|
|
return v
|
|
}
|