merge origin/master into llm-recording-and-analysis

both sides independently fixed the same three bugs, so each one had to pick a
winner rather than keep both implementations.

extractor encoding: master's recordableValue in worker.go wins over ours in
marshal.go, since master's is pinned by extractor_encoding_test.go and ours had
no tests. our error semantics stay: encodeExtractorValue still returns an error
instead of nil, so an extractor cannot vanish from the trace silently.

apply errors: only the residual generic branch takes master's unconfirmed copy,
where the device may have committed the action before the call failed. the
finer branches that know nothing was dispatched keep lastAction = nil, and our
actionSkipReason taxonomy stays alongside master's held/skippedVerification.

selector matching: our matchAttr with matchSelectorKind wins over master's
match, since ours also handles idPrefix. matchSelector now calls it, which git
did not flag as a conflict and left calling a function our side had deleted.

the ltl doc comment takes master's correction: an unbounded eventually that
never fires IS violated at run end.

internal/runner/composition_reread_test.go

@@ -0,0 +1,509 @@
+package runner
+
+import (
+	"bytes"
+	"context"
+	"encoding/json"
+	"fmt"
+	"os"
+	"path/filepath"
+	"strings"
+	"sync/atomic"
+	"testing"
+	"time"
+
+	"github.com/priyanshujain/sanderling/internal/driver"
+	mockdriver "github.com/priyanshujain/sanderling/internal/driver/mock"
+	"github.com/priyanshujain/sanderling/internal/trace"
+)
+
+// homeWithRows is one settled route whose list holds rows. A row arriving
+// between two reads is what a Compose lazy list mounting over several frames
+// looks like from the runner's side.
+func homeWithRows(rows int) string {
+	var children strings.Builder
+	for row := range rows {
+		fmt.Fprintf(&children,
+			`,{"attributes":{"resource-id":"TxnRow%d","class":"android.view.View"},"children":[]}`, row)
+	}
+	return fmt.Sprintf(
+		`{"attributes":{"resource-id":"HomeScreen","class":"android.view.View"},"children":[
+		  {"attributes":{"resource-id":"TxnList","class":"android.view.View"},"children":[]}%s
+		]}`, children.String())
+}
+
+// composesLateDriver answers the paired Snapshot with the frame the step
+// records and the hierarchy read that follows with a tree that has grown a row,
+// for the first composingReads reads of the run. After that both reads describe
+// the same screen.
+type composesLateDriver struct {
+	*mockdriver.Driver
+	composingReads int64
+	reads          atomic.Int64
+}
+
+func (d *composesLateDriver) Snapshot(context.Context) (string, driver.Image, error) {
+	return homeWithRows(1), driver.Image{PNG: []byte("png"), Width: 1, Height: 1}, nil
+}
+
+func (d *composesLateDriver) Hierarchy(context.Context) (string, error) {
+	if d.reads.Add(1) <= d.composingReads {
+		return homeWithRows(2), nil
+	}
+	return homeWithRows(1), nil
+}
+
+// A route can settle before its content composes, so a tree read the moment the
+// route arrives can describe a screen that is still filling in. Verifying that
+// step compares a half-composed frame against a settled one and convicts an app
+// that did nothing wrong. Two reads a read apart see it happening, and the step
+// they disagree on is one the verifier must never be handed.
+//
+// The always-false property is the witness: it fires on the first step the
+// verifier evaluates, so the step index of its violation says exactly which
+// step reached the verifier.
+func TestRunner_AStepWhoseTreeChangedBetweenReadsIsNotVerified(t *testing.T) {
+	run := func(t *testing.T, composingReads int64) (Summary, string) {
+		t.Helper()
+		state := newHarnessWithSpec(t, violationSpec)
+		device := &composesLateDriver{Driver: state.mock, composingReads: composingReads}
+
+		ctx, cancel := context.WithTimeout(context.Background(), 10*time.Second)
+		defer cancel()
+		summary, err := Run(ctx, Options{
+			Duration:    time.Hour,
+			IdleTimeout: 20 * time.Millisecond,
+			MaxSteps:    3,
+			Driver:      device,
+			Verifier:    state.verifier,
+			TraceWriter: state.writer,
+		})
+		if err != nil {
+			t.Fatalf("Run: %v", err)
+		}
+		if summary.Steps != 3 {
+			t.Fatalf("steps = %d, want 3", summary.Steps)
+		}
+		return summary, state.writer.Directory()
+	}
+
+	t.Run("the step it changed on is skipped, the next one is judged", func(t *testing.T) {
+		summary, directory := run(t, 1)
+		if len(summary.Violations) != 1 {
+			t.Fatalf("violations = %v, want exactly one", summary.Violations)
+		}
+		violation := summary.Violations[0]
+		if violation.Properties[0] != "balanceNonNegative" {
+			t.Fatalf("violated %v, want balanceNonNegative", violation.Properties)
+		}
+		if violation.StepIndex != 2 {
+			t.Errorf("the property first judged step %d, want 2; the verifier was handed "+
+				"a screen that grew a row while the runner was reading it",
+				violation.StepIndex)
+		}
+		if summary.SkippedVerification != 1 {
+			t.Errorf("the run reports %d step(s) judged by nothing, want 1",
+				summary.SkippedVerification)
+		}
+		// Skipped is not lost: the step is still recorded, screenshot and all,
+		// so the run can be replayed over the frame nothing judged.
+		steps := traceSteps(t, directory)
+		if len(steps) != 3 {
+			t.Fatalf("trace holds %d step(s), want 3", len(steps))
+		}
+		if len(steps[0].Violations) != 0 {
+			t.Errorf("step 1 recorded violations %v; it was never verified", steps[0].Violations)
+		}
+		screenshot := filepath.Join(directory, "screenshots", "step-00001.png")
+		if _, err := os.Stat(screenshot); err != nil {
+			t.Errorf("expected the skipped step's screenshot at %s: %v", screenshot, err)
+		}
+	})
+
+	// The control. Two reads that agree must verify as they always did,
+	// otherwise the case above is just a runner that verifies nothing.
+	t.Run("two reads that agree verify the step", func(t *testing.T) {
+		summary, _ := run(t, 0)
+		if len(summary.Violations) != 1 {
+			t.Fatalf("violations = %v, want exactly one", summary.Violations)
+		}
+		if got := summary.Violations[0].StepIndex; got != 1 {
+			t.Errorf("the property first judged step %d, want 1; a settled screen must be "+
+				"verified on the step it was read", got)
+		}
+	})
+}
+
+// submitsOnTapDriver commits commitsPerTap transactions on every tap, shows the
+// running total in the tree, and grows a row under the hierarchy read that
+// follows the paired Snapshot: on one chosen step, on the run of steps from
+// composingRead through composingThrough, or on every one of them.
+type submitsOnTapDriver struct {
+	*mockdriver.Driver
+	commitsPerTap    int64
+	composingRead    int64
+	composingThrough int64
+	everyRead        bool
+	reads            atomic.Int64
+	committed        atomic.Int64
+}
+
+func (d *submitsOnTapDriver) Tap(context.Context, int, int) error       { return d.commit() }
+func (d *submitsOnTapDriver) TapSelector(context.Context, string) error { return d.commit() }
+
+func (d *submitsOnTapDriver) commit() error {
+	d.committed.Add(d.commitsPerTap)
+	return nil
+}
+
+func (d *submitsOnTapDriver) Snapshot(context.Context) (string, driver.Image, error) {
+	return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), driver.Image{}, nil
+}
+
+func (d *submitsOnTapDriver) Hierarchy(context.Context) (string, error) {
+	read := d.reads.Add(1)
+	composing := d.everyRead || read == d.composingRead ||
+		(read >= d.composingRead && read <= d.composingThrough)
+	if composing {
+		return fmt.Sprintf(homeWithTxnCountComposing, d.committed.Load()), nil
+	}
+	return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil
+}
+
+// The same tree with one more row in it, which is what the reread sees while
+// the screen is still filling in.
+const homeWithTxnCountComposing = `{"attributes":{"resource-id":"HomeScreen"},"children":[
+	{"attributes":{"resource-id":"TxnCount","text":"%d"},"children":[]},
+	{"attributes":{"resource-id":"TxnSubmit","bounds":"[40,80,240,160]"},"children":[],"clickable":true,"enabled":true},
+	{"attributes":{"resource-id":"TxnRowLate"},"children":[]}
+]}`
+
+// Skipping a step is only free if nothing the spec needs goes missing with it.
+// The action a step applies is reported to the spec on the NEXT step the
+// verifier accepts, so a skipped step in between swallows the action before it:
+// the transaction it committed still turns up in the next reading, and
+// submitCommitsOneTransactionPerAction sees a rise nothing in its window
+// accounts for. That is the conviction #77 and #78 are about, arriving through
+// the skip rather than through the runner's report.
+//
+// So a frame the verifier will not look at is not one to act on either, which
+// is also what #75 asked for: the fuzzer must not tap into a screen that is
+// still filling in.
+func TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt(t *testing.T) {
+	spec := specWithFolioPredicates(t)
+
+	run := func(t *testing.T, composingRead int64) (Summary, int64) {
+		t.Helper()
+		state := newHarnessWithSpec(t, spec)
+		device := &submitsOnTapDriver{
+			Driver:        state.mock,
+			commitsPerTap: 1,
+			composingRead: composingRead,
+		}
+
+		ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
+		defer cancel()
+		summary, err := Run(ctx, Options{
+			Duration:    time.Hour,
+			IdleTimeout: 20 * time.Millisecond,
+			MaxSteps:    3,
+			Driver:      device,
+			Verifier:    state.verifier,
+			TraceWriter: state.writer,
+		})
+		if err != nil {
+			t.Fatalf("Run: %v", err)
+		}
+		if summary.Steps != 3 {
+			t.Fatalf("steps = %d, want 3", summary.Steps)
+		}
+		return summary, device.committed.Load()
+	}
+
+	t.Run("a submit is not lost to the step that follows it", func(t *testing.T) {
+		summary, committed := run(t, 2)
+		if summary.SkippedVerification != 1 {
+			t.Fatalf("the run skipped %d step(s), want 1; the reread never fired, so this "+
+				"proves nothing", summary.SkippedVerification)
+		}
+		if committed == 0 {
+			t.Fatal("the device committed nothing; a runner that never acts passes this " +
+				"test without meaning anything")
+		}
+		if len(summary.Violations) != 0 {
+			t.Errorf("the counting property convicted a healthy app: %v\n"+
+				"one transaction per submit rose, and a submit went unreported because "+
+				"the step after it was skipped", summary.Violations)
+		}
+	})
+
+	// The control: with nothing composing, every step is verified and the same
+	// app is judged clean, so the case above is not just a runner that stopped
+	// judging.
+	t.Run("every step verified, same app, no violation", func(t *testing.T) {
+		summary, committed := run(t, 0)
+		if summary.SkippedVerification != 0 {
+			t.Fatalf("the run skipped %d step(s), want 0", summary.SkippedVerification)
+		}
+		if committed != 3 {
+			t.Fatalf("the device committed %d transaction(s), want 3", committed)
+		}
+		if len(summary.Violations) != 0 {
+			t.Errorf("the counting property convicted a healthy app: %v", summary.Violations)
+		}
+	})
+}
+
+// One skipped step is held; a run of them has to be held too. A bound that lets
+// the runner act again while the verifier is still being skipped puts back the
+// exact swallow the hold exists to prevent, only later: the action drawn on the
+// step past the bound overwrites the one the hold was carrying, and the carried
+// action is never reported to any spec.
+//
+// The screen composes on steps 3 through 5 of 6 and the device commits one
+// transaction per tap throughout, so the property has a clean pair to judge
+// (step 2 to step 6) and nothing in between it can be told about except the
+// action step 2 applied.
+func TestRunner_ARunOfSkippedStepsReportsEveryActionItApplied(t *testing.T) {
+	spec := specWithFolioPredicates(t)
+
+	run := func(t *testing.T, commitsPerTap int64) (Summary, int64) {
+		t.Helper()
+		state := newHarnessWithSpec(t, spec)
+		device := &submitsOnTapDriver{
+			Driver:           state.mock,
+			commitsPerTap:    commitsPerTap,
+			composingRead:    3,
+			composingThrough: 5,
+		}
+
+		ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
+		defer cancel()
+		summary, err := Run(ctx, Options{
+			Duration:    time.Hour,
+			IdleTimeout: 20 * time.Millisecond,
+			MaxSteps:    6,
+			Driver:      device,
+			Verifier:    state.verifier,
+			TraceWriter: state.writer,
+		})
+		if err != nil {
+			t.Fatalf("Run: %v", err)
+		}
+		if summary.Steps != 6 {
+			t.Fatalf("steps = %d, want 6", summary.Steps)
+		}
+		if summary.SkippedVerification != 3 {
+			t.Fatalf("the run skipped %d step(s), want 3; the reread never fired across "+
+				"the run this test is about", summary.SkippedVerification)
+		}
+		return summary, device.committed.Load()
+	}
+
+	t.Run("no submit is lost to the run of skipped steps", func(t *testing.T) {
+		summary, committed := run(t, 1)
+		if committed == 0 {
+			t.Fatal("the device committed nothing; a runner that never acts passes this " +
+				"test without meaning anything")
+		}
+		if len(summary.Violations) != 0 {
+			t.Errorf("the counting property convicted a healthy app: %v\n"+
+				"one transaction per submit rose, and a submit went unreported because "+
+				"the runner acted on a step the verifier skipped", summary.Violations)
+		}
+		if committed != 3 {
+			t.Errorf("the device committed %d transaction(s), want 3: one per verified "+
+				"step (1, 2 and 6) and none from a step nothing would judge", committed)
+		}
+	})
+
+	// The control. Without it a green above proves nothing: a property handed
+	// no comparable pair is silently vacuous and reports the same empty list.
+	t.Run("two transactions per tap still convicts across the same run", func(t *testing.T) {
+		summary, _ := run(t, 2)
+		if len(summary.Violations) == 0 {
+			t.Fatal("the counting property missed a double submit; the skipped steps left " +
+				"it with nothing to judge, so the case above proves nothing")
+		}
+		if got := summary.Violations[0].Properties[0]; got != "submitCommitsOneTransactionPerAction" {
+			t.Errorf("violated %v, want submitCommitsOneTransactionPerAction",
+				summary.Violations[0].Properties)
+		}
+	})
+}
+
+// A screen that changes shape under every pair of reads (a live list, a spinner
+// mounting and unmounting) costs the run its actions: an action applied onto it
+// would be the one the next verified step never hears about, and there is no
+// next verified step. What the run must not do is come back green off that,
+// which is what the "judged by nothing" count and the run's outcome are for.
+func TestRunner_AScreenThatNeverSettlesActsOnNothingAndSaysSo(t *testing.T) {
+	state := newHarnessWithSpec(t, specWithFolioPredicates(t))
+	device := &submitsOnTapDriver{Driver: state.mock, commitsPerTap: 1, everyRead: true}
+
+	ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
+	defer cancel()
+	summary, err := Run(ctx, Options{
+		Duration:    time.Hour,
+		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    5,
+		Driver:      device,
+		Verifier:    state.verifier,
+		TraceWriter: state.writer,
+	})
+	if err != nil {
+		t.Fatalf("Run: %v", err)
+	}
+	if summary.Steps != 5 {
+		t.Fatalf("steps = %d, want 5; the run stalled instead of finishing its budget",
+			summary.Steps)
+	}
+	if summary.SkippedVerification != 5 {
+		t.Fatalf("the run verified some step of a screen that never settled: skipped %d of 5",
+			summary.SkippedVerification)
+	}
+	if got := device.committed.Load(); got != 0 {
+		t.Errorf("the fuzzer applied %d action(s) onto a screen no property would judge; "+
+			"each one is an action no spec will ever be told about", got)
+	}
+}
+
+// homeWithTicker is one settled route holding a total that ticks and a button
+// whose measured bounds shift under it. The nodes, their ids and their classes
+// are the same in every rendering of it.
+const homeWithTicker = `{"attributes":{"resource-id":"HomeScreen","class":"android.view.View"},"children":[
+	{"attributes":{"resource-id":"Total","class":"android.widget.TextView","text":"%s"},"children":[]},
+	{"attributes":{"resource-id":"TxnSubmit","class":"android.widget.Button","bounds":"%s"},"children":[]}
+]}`
+
+// The same route with a node in it that was not there a read ago.
+const homeWithTickerAndRow = `{"attributes":{"resource-id":"HomeScreen","class":"android.view.View"},"children":[
+	{"attributes":{"resource-id":"Total","class":"android.widget.TextView","text":"120.00"},"children":[]},
+	{"attributes":{"resource-id":"TxnSubmit","class":"android.widget.Button","bounds":"[40,80,240,160]"},"children":[]},
+	{"attributes":{"resource-id":"TxnRowLate","class":"android.view.View"},"children":[]}
+]}`
+
+// rereadsDriver answers the paired Snapshot with one fixed tree and the
+// hierarchy read that follows with another, so a test can say exactly what
+// moved between the two reads the detector compares.
+type rereadsDriver struct {
+	*mockdriver.Driver
+	snapshotTree string
+	rereadTree   string
+}
+
+func (d *rereadsDriver) Snapshot(context.Context) (string, driver.Image, error) {
+	return d.snapshotTree, driver.Image{}, nil
+}
+
+func (d *rereadsDriver) Hierarchy(context.Context) (string, error) {
+	return d.rereadTree, nil
+}
+
+// What the two reads are compared ON is the whole feature. Comparing the values
+// in the tree instead of the nodes in it would fire on every step of a screen
+// with a total on it or a measure pass in flight, and a runner that skips every
+// step verifies nothing while reporting no violations: green and vacuous, which
+// is a worse answer than the composition the comparison set out to catch.
+//
+// The always-false property is the witness: it fires on the first step that
+// reaches the verifier, so its presence and its step index say whether the step
+// was judged at all.
+func TestRunner_OnlyAChangeOfShapeCostsAStepItsVerdict(t *testing.T) {
+	settled := fmt.Sprintf(homeWithTicker, "120.00", "[40,80,240,160]")
+	cases := []struct {
+		name     string
+		reread   string
+		verified bool
+	}{
+		{
+			name:     "a total that ticked between the two reads",
+			reread:   fmt.Sprintf(homeWithTicker, "121.00", "[40,80,240,160]"),
+			verified: true,
+		},
+		{
+			name:     "a measure pass that moved the button",
+			reread:   fmt.Sprintf(homeWithTicker, "120.00", "[40,84,240,164]"),
+			verified: true,
+		},
+		{
+			name:     "a node that was not in the tree a read ago",
+			reread:   homeWithTickerAndRow,
+			verified: false,
+		},
+	}
+
+	for _, testCase := range cases {
+		t.Run(testCase.name, func(t *testing.T) {
+			state := newHarnessWithSpec(t, violationSpec)
+			device := &rereadsDriver{
+				Driver:       state.mock,
+				snapshotTree: settled,
+				rereadTree:   testCase.reread,
+			}
+
+			ctx, cancel := context.WithTimeout(context.Background(), 10*time.Second)
+			defer cancel()
+			summary, err := Run(ctx, Options{
+				Duration:    time.Hour,
+				IdleTimeout: 20 * time.Millisecond,
+				MaxSteps:    3,
+				Driver:      device,
+				Verifier:    state.verifier,
+				TraceWriter: state.writer,
+			})
+			if err != nil {
+				t.Fatalf("Run: %v", err)
+			}
+			if summary.Steps != 3 {
+				t.Fatalf("steps = %d, want 3", summary.Steps)
+			}
+
+			if !testCase.verified {
+				if summary.SkippedVerification != 3 {
+					t.Errorf("the run judged %d of 3 steps whose tree grew a node between "+
+						"the two reads; a screen still composing must reach no property",
+						3-summary.SkippedVerification)
+				}
+				if len(summary.Violations) != 0 {
+					t.Errorf("a skipped step reached the verifier anyway: %v",
+						summary.Violations)
+				}
+				return
+			}
+			if summary.SkippedVerification != 0 {
+				t.Fatalf("the run judged nothing: %d of 3 steps were skipped over a tree "+
+					"whose nodes never changed", summary.SkippedVerification)
+			}
+			if len(summary.Violations) != 1 {
+				t.Fatalf("violations = %v, want exactly one", summary.Violations)
+			}
+			if got := summary.Violations[0].StepIndex; got != 1 {
+				t.Errorf("the property first judged step %d, want 1", got)
+			}
+		})
+	}
+}
+
+type traceLine struct {
+	Step             int                              `json:"step"`
+	Violations       []string                         `json:"violations"`
+	ExtractorChanges map[string]trace.ExtractorChange `json:"extractor_changes"`
+}
+
+func traceSteps(t *testing.T, directory string) []traceLine {
+	t.Helper()
+	body, err := os.ReadFile(filepath.Join(directory, "trace.jsonl"))
+	if err != nil {
+		t.Fatal(err)
+	}
+	var steps []traceLine
+	for _, raw := range bytes.Split(bytes.TrimSpace(body), []byte("\n")) {
+		var line traceLine
+		if err := json.Unmarshal(raw, &line); err != nil {
+			t.Fatalf("decode trace line: %v", err)
+		}
+		steps = append(steps, line)
+	}
+	return steps
+}

internal/runner/element_extractor_trace_test.go

@@ -4,6 +4,7 @@ import (
 	"bufio"
 	"context"
 	"encoding/json"
+	"fmt"
 	"os"
 	"path/filepath"
 	"testing"
@@ -12,124 +13,109 @@ import (
 	"github.com/priyanshujain/sanderling/internal/trace"
 )
 
-// elementExtractorSpec records accessibility elements directly, the shape an
-// author reaches for when the question is "what was on screen at this step":
-// one element and the list a generator would have been offered.
+// elementExtractorSpec reads a live ax element, the shape every field and
+// button in examples/folio/sanderling/spec.ts is extracted with. The property
+// is false the moment the field is on screen, so the run records a witness
+// whose only interesting content is that element.
 const elementExtractorSpec = `
-import { actions, extract } from "@sanderling/spec";
-extract("field", state => state.ax.find({ testTag: "LoginEmail" }));
-extract("rows", state => state.ax.findAll({ testTag: "Row" }));
-globalThis.properties = {};
+import { actions, always, extract } from "@sanderling/spec";
+const amountField = extract("amountField", s => s.ax.find({ "resource-id": "TxnAmountField" }));
+globalThis.properties = {
+  noAmountField: always(() => amountField.current === undefined),
+};
 globalThis.actions = actions(() => []);
 `
 
-const elementExtractorHierarchy = `{
-  "attributes": {"class": "android.widget.LinearLayout", "bounds": "[0,0,1080,2340]"},
+const amountFieldTreeJSON = `{
+  "attributes": {"resource-id": "root", "bounds": "[0,0,400,800]"},
+  "enabled": true,
   "children": [
-    {"attributes": {"resource-id": "LoginEmail", "class": "android.widget.EditText",
-      "text": "[email protected]", "bounds": "[10,20,200,60]"}, "children": []},
-    {"attributes": {"resource-id": "Row", "class": "android.widget.TextView",
-      "text": "first", "bounds": "[0,100,1080,200]"}, "children": []},
-    {"attributes": {"resource-id": "Row", "class": "android.widget.TextView",
-      "text": "second", "bounds": "[0,200,1080,300]"}, "children": []}
+    {"attributes": {"resource-id": "TxnAmountField", "text": "199", "bounds": "[0,100,400,160]"},
+     "editable": true, "enabled": true, "children": []}
   ]
 }`
 
-// TestRunner_TraceRecordsElementValuedExtractors pins that an extractor holding
-// an accessibility element reaches the trace. Elements carry host functions
-// (find/findAll), which json.Marshal refuses; the encoder used to answer nil
-// and the diff then emitted no entry, so the run finished clean with the
-// extractor missing from every step and no error anywhere.
+// TestRunner_TraceRecordsElementValuedExtractors is the guard on the artifact a
+// person opens to decide whether a conviction is real. An element-valued
+// extractor used to reach the trace as null on the goja hosts (ios, android):
+// its exported value carries the element's find/findAll host functions, which
+// json.Marshal refuses, so the encoding failed and both the per-step diff and
+// the witness recorded nothing. A witness that reads null for the field the
+// property fired on describes a state the property could not have fired in,
+// which is worse than a blank.
 func TestRunner_TraceRecordsElementValuedExtractors(t *testing.T) {
 	state := newHarnessWithSpec(t, elementExtractorSpec)
-	state.mock.HierarchyJSON = elementExtractorHierarchy
+	state.mock.HierarchyJSON = amountFieldTreeJSON
 
 	ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second)
 	defer cancel()
-	if _, err := Run(ctx, Options{
-		Duration:    100 * time.Millisecond,
+	summary, err := Run(ctx, Options{
+		Duration:    time.Hour,
 		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    2,
 		Driver:      state.mock,
 		Verifier:    state.verifier,
 		TraceWriter: state.writer,
-	}); err != nil {
+	})
+	if err != nil {
 		t.Fatalf("Run: %v", err)
 	}
-
-	field, rows := elementChangesFromTrace(t, state.directory)
-	if field == nil {
-		t.Fatal("no extractor change for the element-valued extractor reached the trace")
-	}
-	if rows == nil {
-		t.Fatal("no extractor change for the element-list extractor reached the trace")
+	if !containsProperty(summary.Violations, "noAmountField") {
+		t.Fatalf("noAmountField did not violate, so the element never reached a predicate: %v",
+			summary.Violations)
 	}
 
-	var element map[string]any
-	if err := json.Unmarshal(field, &element); err != nil {
-		t.Fatalf("field value is not a JSON object: %v (%s)", err, field)
-	}
-	if got := element["id"]; got != "LoginEmail" {
-		t.Errorf("field.id = %v, want LoginEmail", got)
-	}
-	if got := element["text"]; got != "[email protected]" {
-		t.Errorf("field.text = %v, want [email protected]", got)
-	}
-	if got := element["class"]; got != "android.widget.EditText" {
-		t.Errorf("field.class = %v, want android.widget.EditText", got)
-	}
-	bounds, ok := element["bounds"].(map[string]any)
-	if !ok {
-		t.Fatalf("field.bounds missing or not an object: %v", element["bounds"])
-	}
-	if bounds["left"] != float64(10) || bounds["top"] != float64(20) ||
-		bounds["right"] != float64(200) || bounds["bottom"] != float64(60) {
-		t.Errorf("field.bounds = %v, want left/top/right/bottom 10/20/200/60", bounds)
-	}
-	for _, key := range []string{"find", "findAll"} {
-		if _, present := element[key]; present {
-			t.Errorf("field carries the host function %q into the trace", key)
-		}
-	}
-
-	var list []map[string]any
-	if err := json.Unmarshal(rows, &list); err != nil {
-		t.Fatalf("rows value is not a JSON array: %v (%s)", err, rows)
-	}
-	if len(list) != 2 {
-		t.Fatalf("rows recorded %d elements, want 2", len(list))
-	}
-	if list[0]["text"] != "first" || list[1]["text"] != "second" {
-		t.Errorf("rows recorded %v, want the two Row elements in tree order", list)
-	}
-}
-
-// elementChangesFromTrace returns the first recorded value of each extractor.
-func elementChangesFromTrace(t *testing.T, directory string) (field, rows json.RawMessage) {
-	t.Helper()
-	file, err := os.Open(filepath.Join(directory, "trace.jsonl"))
+	file, err := os.Open(filepath.Join(state.writer.Directory(), "trace.jsonl"))
 	if err != nil {
 		t.Fatal(err)
 	}
 	defer file.Close()
 
+	type traceLine struct {
+		Step             int                              `json:"step"`
+		ExtractorChanges map[string]trace.ExtractorChange `json:"extractor_changes"`
+		Witnesses        map[string]trace.Witness         `json:"witnesses"`
+	}
+	changes, witnesses := 0, 0
 	scanner := bufio.NewScanner(file)
 	scanner.Buffer(make([]byte, 0, 64*1024), 8*1024*1024)
 	for scanner.Scan() {
-		var line struct {
-			ExtractorChanges map[string]trace.ExtractorChange `json:"extractor_changes"`
-		}
+		var line traceLine
 		if err := json.Unmarshal(scanner.Bytes(), &line); err != nil {
 			t.Fatalf("trace line decode: %v", err)
 		}
-		if change, ok := line.ExtractorChanges["field"]; ok && field == nil {
-			field = change.Curr
+		if change, ok := line.ExtractorChanges["amountField"]; ok {
+			changes++
+			assertAmountField(t, fmt.Sprintf("step %d extractor_changes", line.Step), change.Curr)
 		}
-		if change, ok := line.ExtractorChanges["rows"]; ok && rows == nil {
-			rows = change.Curr
+		for name, witness := range line.Witnesses {
+			witnesses++
+			assertAmountField(t, fmt.Sprintf("step %d %s witness", line.Step, name),
+				witness.Extractors["amountField"])
 		}
 	}
 	if err := scanner.Err(); err != nil {
 		t.Fatalf("scan trace: %v", err)
 	}
-	return field, rows
+	if changes == 0 {
+		t.Error("amountField never appears in extractor_changes; the element the run read is not in the trace")
+	}
+	if witnesses == 0 {
+		t.Error("no witness reached the trace; nothing was compared")
+	}
+}
+
+// assertAmountField reads the recorded element the way a person opening the
+// trace would: the field's text is the number the property was judged on.
+func assertAmountField(t *testing.T, where string, recorded json.RawMessage) {
+	t.Helper()
+	var element struct {
+		Text string `json:"text"`
+	}
+	if err := json.Unmarshal(recorded, &element); err != nil {
+		t.Fatalf("%s: decode %s: %v", where, recorded, err)
+	}
+	if element.Text != "199" {
+		t.Errorf("%s: recorded element is %s, want its text to read 199", where, recorded)
+	}
 }

internal/runner/foreground_guard_last_action_test.go

@@ -0,0 +1,365 @@
+package runner
+
+import (
+	"context"
+	"fmt"
+	"path/filepath"
+	"sync/atomic"
+	"testing"
+	"time"
+
+	"github.com/priyanshujain/sanderling/internal/driver"
+	mockdriver "github.com/priyanshujain/sanderling/internal/driver/mock"
+)
+
+const guardedBundleID = "app.folio"
+
+// committingDevice is a device whose submit taps commit transactions the next
+// hierarchy read shows, and which can say how many it has committed so a test
+// can prove the taps landed before reading anything into a verdict.
+type committingDevice interface {
+	driver.DeviceDriver
+	commits() int64
+}
+
+// leavesForegroundAfterSubmitDriver is the condition the app-scope guard exists
+// for: the submit tap lands and commits, and the app is no longer the
+// foreground app by the time the next step looks. Folio's transactions are in
+// sqlite, so the commit survives the relaunch and the next reading shows it.
+type leavesForegroundAfterSubmitDriver struct {
+	*mockdriver.Driver
+	commitsPerTap int64
+	committed     atomic.Int64
+	away          atomic.Bool
+}
+
+func (d *leavesForegroundAfterSubmitDriver) Tap(context.Context, int, int) error {
+	return d.commitThenLeave()
+}
+
+func (d *leavesForegroundAfterSubmitDriver) TapSelector(context.Context, string) error {
+	return d.commitThenLeave()
+}
+
+func (d *leavesForegroundAfterSubmitDriver) commitThenLeave() error {
+	d.committed.Add(d.commitsPerTap)
+	d.away.Store(true)
+	return nil
+}
+
+func (d *leavesForegroundAfterSubmitDriver) commits() int64 { return d.committed.Load() }
+
+func (d *leavesForegroundAfterSubmitDriver) Launch(
+	ctx context.Context,
+	bundleID string,
+	clearState bool,
+	env map[string]string,
+) error {
+	d.away.Store(false)
+	return d.Driver.Launch(ctx, bundleID, clearState, env)
+}
+
+func (d *leavesForegroundAfterSubmitDriver) ForegroundApp(context.Context) (string, error) {
+	if d.away.Load() {
+		return "com.android.launcher", nil
+	}
+	return guardedBundleID, nil
+}
+
+func (d *leavesForegroundAfterSubmitDriver) FocusedWindowApp(ctx context.Context) (string, error) {
+	return d.ForegroundApp(ctx)
+}
+
+func (d *leavesForegroundAfterSubmitDriver) Snapshot(context.Context) (string, driver.Image, error) {
+	return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), driver.Image{}, nil
+}
+
+// The runner reads both per step and compares them, so a device that answered
+// them off different trees would make every step of this test transitional and
+// judged by nothing. The sidecar serves both off one read path (snapshotTree)
+// for the same reason; this one answers them off the same commit count.
+func (d *leavesForegroundAfterSubmitDriver) Hierarchy(context.Context) (string, error) {
+	return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil
+}
+
+// obscuredAfterSubmitDriver is the other half of the same guard: the app stays
+// the resumed activity, but a system window (the notification shade) owns the
+// focused window when the next step looks, and the guard presses back to
+// collapse it.
+type obscuredAfterSubmitDriver struct {
+	*mockdriver.Driver
+	commitsPerTap int64
+	committed     atomic.Int64
+	obscured      atomic.Bool
+}
+
+func (d *obscuredAfterSubmitDriver) Tap(context.Context, int, int) error {
+	return d.commitThenObscure()
+}
+
+func (d *obscuredAfterSubmitDriver) TapSelector(context.Context, string) error {
+	return d.commitThenObscure()
+}
+
+func (d *obscuredAfterSubmitDriver) commitThenObscure() error {
+	d.committed.Add(d.commitsPerTap)
+	d.obscured.Store(true)
+	return nil
+}
+
+func (d *obscuredAfterSubmitDriver) commits() int64 { return d.committed.Load() }
+
+func (d *obscuredAfterSubmitDriver) PressKey(ctx context.Context, key string) error {
+	if key == "back" {
+		d.obscured.Store(false)
+	}
+	return d.Driver.PressKey(ctx, key)
+}
+
+func (d *obscuredAfterSubmitDriver) ForegroundApp(context.Context) (string, error) {
+	return guardedBundleID, nil
+}
+
+func (d *obscuredAfterSubmitDriver) FocusedWindowApp(context.Context) (string, error) {
+	if d.obscured.Load() {
+		return "com.android.systemui", nil
+	}
+	return guardedBundleID, nil
+}
+
+func (d *obscuredAfterSubmitDriver) Snapshot(context.Context) (string, driver.Image, error) {
+	return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), driver.Image{}, nil
+}
+
+func (d *obscuredAfterSubmitDriver) Hierarchy(context.Context) (string, error) {
+	return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil
+}
+
+// runTwoSubmitSteps drives two steps of the shipped folio counting property
+// against a device that commits on every tap, and hands back what the property
+// decided. Both steps have to run: the first arms the comparison, the second is
+// where the guard fires and the pair is judged.
+func runTwoSubmitSteps(
+	t *testing.T,
+	state *harness,
+	device committingDevice,
+	commitsPerTap int64,
+) []ViolationRecord {
+	t.Helper()
+	ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
+	defer cancel()
+	summary, err := Run(ctx, Options{
+		Duration:    time.Hour,
+		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    2,
+		BundleID:    guardedBundleID,
+		Driver:      device,
+		Verifier:    state.verifier,
+		TraceWriter: state.writer,
+	})
+	if err != nil {
+		t.Fatalf("Run: %v", err)
+	}
+	if summary.Steps != 2 {
+		t.Fatalf("steps = %d, want 2; the run never reached the step that judges the pair",
+			summary.Steps)
+	}
+	if got := device.commits(); got != commitsPerTap*2 {
+		t.Fatalf("the device committed %d transaction(s), want %d; the taps never reached it",
+			got, commitsPerTap*2)
+	}
+	return summary.Violations
+}
+
+func countMockActions(state *harness, kind mockdriver.ActionKind, key string) int {
+	count := 0
+	for _, action := range state.mock.Actions() {
+		if action.Kind != kind {
+			continue
+		}
+		if key != "" && action.Key != key {
+			continue
+		}
+		count++
+	}
+	return count
+}
+
+func specWithFolioPredicates(t *testing.T) string {
+	t.Helper()
+	predicates, err := filepath.Abs("../../examples/folio/sanderling/predicates.ts")
+	if err != nil {
+		t.Fatal(err)
+	}
+	return fmt.Sprintf(submitCountingSpecTemplate, predicates)
+}
+
+// A relaunch is not proof that nothing ran before it. The submit was dispatched
+// and confirmed; what the relaunch changed is that the app restarted between
+// the two readings the property compares. Reporting "no action" for it hands
+// submitCommitsOneTransactionPerAction a transaction rise of one against a
+// window of zero submits, which is the conviction #77 fixed for the apply-error
+// path, manufactured here out of the scope guard instead.
+func TestRunner_ARelaunchDoesNotConvictTheSubmitCountingProperty(t *testing.T) {
+	spec := specWithFolioPredicates(t)
+
+	run := func(t *testing.T, commitsPerTap int64) []ViolationRecord {
+		t.Helper()
+		state := newHarnessWithSpec(t, spec)
+		device := &leavesForegroundAfterSubmitDriver{
+			Driver:        state.mock,
+			commitsPerTap: commitsPerTap,
+		}
+		violations := runTwoSubmitSteps(t, state, device, commitsPerTap)
+		if countMockActions(state, mockdriver.ActionLaunch, "") == 0 {
+			t.Fatal("the app was never relaunched, so the guard this test is about never ran")
+		}
+		return violations
+	}
+
+	t.Run("one transaction per tap is not a double submit", func(t *testing.T) {
+		if violations := run(t, 1); len(violations) != 0 {
+			t.Errorf("the counting property convicted a healthy app: %v\n"+
+				"one transaction rose against a submit the runner confirmed, and the "+
+				"spec was told no action happened because the app was relaunched",
+				violations)
+		}
+	})
+
+	// The control. Without it a green above proves nothing: a property that
+	// never sees a comparable pair is silently vacuous and reports the same
+	// empty violation list.
+	t.Run("two transactions per tap still convicts", func(t *testing.T) {
+		violations := run(t, 2)
+		if len(violations) == 0 {
+			t.Fatal("the counting property missed a double submit; the harness never " +
+				"put the property in a position to fire, so the case above proves nothing")
+		}
+		if violations[0].Properties[0] != "submitCommitsOneTransactionPerAction" {
+			t.Errorf("violated %v, want submitCommitsOneTransactionPerAction", violations[0].Properties)
+		}
+	})
+}
+
+// The same hole through the guard's other branch. A system window holding the
+// focus says nothing about whether the tap under it ran: it was dispatched, and
+// what nobody can say afterwards is whether the app received it. That is the
+// unknown `applied` already carries, and it counts toward the submits a window
+// could hold. Reporting no action instead convicts the app of a transaction
+// with no cause.
+func TestRunner_AnOverlayDoesNotConvictTheSubmitCountingProperty(t *testing.T) {
+	spec := specWithFolioPredicates(t)
+
+	run := func(t *testing.T, commitsPerTap int64) []ViolationRecord {
+		t.Helper()
+		state := newHarnessWithSpec(t, spec)
+		device := &obscuredAfterSubmitDriver{
+			Driver:        state.mock,
+			commitsPerTap: commitsPerTap,
+		}
+		violations := runTwoSubmitSteps(t, state, device, commitsPerTap)
+		if countMockActions(state, mockdriver.ActionPressKey, "back") == 0 {
+			t.Fatal("the overlay was never dismissed, so the guard this test is about never ran")
+		}
+		if countMockActions(state, mockdriver.ActionLaunch, "") != 0 {
+			t.Fatal("a resumed-but-obscured app must not be relaunched")
+		}
+		return violations
+	}
+
+	t.Run("one transaction per tap is not a double submit", func(t *testing.T) {
+		if violations := run(t, 1); len(violations) != 0 {
+			t.Errorf("the counting property convicted a healthy app: %v\n"+
+				"one transaction rose against a submit the runner dispatched, and the "+
+				"spec was told no action happened because a system window took the focus",
+				violations)
+		}
+	})
+
+	t.Run("two transactions per tap still convicts", func(t *testing.T) {
+		violations := run(t, 2)
+		if len(violations) == 0 {
+			t.Fatal("the counting property missed a double submit; the harness never " +
+				"put the property in a position to fire, so the case above proves nothing")
+		}
+		if violations[0].Properties[0] != "submitCommitsOneTransactionPerAction" {
+			t.Errorf("violated %v, want submitCommitsOneTransactionPerAction", violations[0].Properties)
+		}
+	})
+}
+
+// reportedActionSpec puts what the runner told the spec about the last action
+// into an extractor, so a test can read it out of the trace. `applied` and
+// `relaunched` have no other producer: the runner's two guard writes are the
+// only thing that ever sets them, and every spec-side guard built on them (see
+// acrossRelaunch and confirmedApplied in the folio predicates) reads nothing
+// else. A regression in either write leaves those guards permanently off with
+// no property anywhere able to notice.
+const reportedActionSpec = `
+import { actions, always, extract, Tap } from "@sanderling/spec";
+const reportedAction = extract("reportedAction", state => {
+  const last = state.lastAction;
+  if (last == null) return "none";
+  const dispatch = last.applied === true ? "applied" : "unconfirmed";
+  const process = last.relaunched === true ? "relaunched" : "same-process";
+  return dispatch + "/" + process;
+});
+globalThis.properties = {
+  theGuardTheRunnerRanReachesTheSpec: always(
+    () => reportedAction.current !== "applied/same-process",
+  ),
+};
+globalThis.actions = actions(() => [Tap({ on: "id:TxnSubmit" })]);
+`
+
+// runReportingTheGuard drives two steps against a device whose submit tap trips
+// one of the foreground guards, and hands back what the spec read off
+// state.lastAction on the step the guard fired.
+func runReportingTheGuard(t *testing.T, device committingDevice, state *harness) string {
+	t.Helper()
+	if violations := runTwoSubmitSteps(t, state, device, 1); len(violations) != 0 {
+		t.Errorf("the spec was told the action ran untouched by any guard: %v", violations)
+	}
+	steps := traceSteps(t, state.writer.Directory())
+	if len(steps) != 2 {
+		t.Fatalf("trace holds %d step(s), want 2", len(steps))
+	}
+	change, ok := steps[1].ExtractorChanges["reportedAction"]
+	if !ok {
+		t.Fatalf("step 2 recorded no reading of the reported action: %+v", steps[1])
+	}
+	return string(change.Curr)
+}
+
+func TestRunner_TheSpecIsToldTheAppWasRelaunchedUnderTheAction(t *testing.T) {
+	state := newHarnessWithSpec(t, reportedActionSpec)
+	device := &leavesForegroundAfterSubmitDriver{Driver: state.mock, commitsPerTap: 1}
+
+	reported := runReportingTheGuard(t, device, state)
+
+	if countMockActions(state, mockdriver.ActionLaunch, "") == 0 {
+		t.Fatal("the app was never relaunched, so the write this test is about never ran")
+	}
+	if reported != `"applied/relaunched"` {
+		t.Errorf("the spec read %s off state.lastAction, want \"applied/relaunched\"; "+
+			"a property relaxed across a relaunch cannot fire on a run that never "+
+			"tells it one happened", reported)
+	}
+}
+
+func TestRunner_TheSpecIsToldAnObscuredActionWasNotConfirmed(t *testing.T) {
+	state := newHarnessWithSpec(t, reportedActionSpec)
+	device := &obscuredAfterSubmitDriver{Driver: state.mock, commitsPerTap: 1}
+
+	reported := runReportingTheGuard(t, device, state)
+
+	if countMockActions(state, mockdriver.ActionPressKey, "back") == 0 {
+		t.Fatal("the overlay was never dismissed, so the write this test is about never ran")
+	}
+	if reported != `"unconfirmed/same-process"` {
+		t.Errorf("the spec read %s off state.lastAction, want "+
+			"\"unconfirmed/same-process\"; a system window held the focused window, "+
+			"so whether the app received the tap is exactly what nobody can say",
+			reported)
+	}
+}

internal/runner/runner.go

@@ -57,6 +57,11 @@ type Summary struct {
 	EndTime    time.Time
 	Steps      int
 	Violations []ViolationRecord
+	// SkippedVerification counts the steps whose tree was still moving when it
+	// was read, so no property judged them. A green run that skipped most of
+	// its steps checked almost nothing, and nothing else in the output would
+	// say so.
+	SkippedVerification int
 	// UnsupportedVerbs lists verbs the picker requested that the platform
 	// could not dispatch, deduped, so the report can flag a spec exercising
 	// gestures this target does not support.
@@ -105,6 +110,7 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 	_, pageExtractors := extractorSource.(webSource)
 	exceptionReporter, _ := options.Driver.(driver.ExceptionReporter)
 	navigationReporter, _ := options.Driver.(driver.NavigationReporter)
+	rereadHierarchy := driverIsAndroid(ctx, options, logger)
 
 	summary := Summary{StartTime: time.Now()}
 	deadline := summary.StartTime.Add(options.Duration)
@@ -126,8 +132,23 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 		// backed out of (or otherwise left) the app, relaunch it before we
 		// observe or act, so properties never evaluate against a foreign app
 		// and actions never land outside the app.
-		if ensureForeground(ctx, options, logger, stepIndex) {
-			lastAction = nil
+		//
+		// What the guard did is reported to the spec on the action it followed,
+		// because dropping that action says "nothing ran between these two
+		// readings" and the runner has no business saying that: the action ran,
+		// and a property told otherwise convicts the app of an effect with no
+		// cause. See foreground_guard_last_action_test.go.
+		guard := ensureForeground(ctx, options, logger, stepIndex)
+		if lastAction != nil {
+			switch guard {
+			case foregroundRelaunched:
+				lastAction.Relaunched = true
+			case foregroundOverlayDismissed:
+				// A system window owned the focused window, so whether the app
+				// itself ever received this action is exactly the unknown
+				// Applied already has a state for.
+				lastAction.Applied = false
+			}
 		}
 
 		// Hierarchy, metrics, and logs are independent device reads. Run
@@ -150,7 +171,8 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 		// screenshot describe the same frame, then re-fetches the pair
 		// while the tree still looks transitional.
 		g.Go(func() error {
-			tree, screenshotPNG, transitional, hierarchyErr = fetchSyncedState(gctx, options, logger, si)
+			tree, screenshotPNG, transitional, hierarchyErr = fetchSyncedState(
+				gctx, options, logger, si, rereadHierarchy)
 			return nil
 		})
 		g.Go(func() error {
@@ -159,7 +181,7 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 		})
 		logSince := lastLogTime
 		g.Go(func() error {
-			logs = collectLogs(gctx, options.Driver, logSince)
+			logs = collectLogs(gctx, options.Driver, logger, si, logSince)
 			return nil
 		})
 		// All goroutines write to local variables and return nil, so the Wait
@@ -197,8 +219,10 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			screen = tree.Elements[0].Screen
 		}
 
-		// Transitional trees describe a NavHost mid cross-fade. Pushing
-		// one would poison the verifier's previous/current extractor
+		// A transitional tree is one nothing can vouch for: a NavHost mid
+		// cross-fade, a screen that changed shape between two reads, or a
+		// hierarchy that came back empty. Pushing one would poison the
+		// verifier's previous/current extractor
 		// advance, so the next clean step would compare against this
 		// transient state and emit false-positive violations. We still
 		// record the step (hierarchy + screenshot) for replay-side
@@ -223,10 +247,11 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			// behind the hierarchy fetch; the fetch is what decides whether this
 			// step counts at all, so it has to go first.
 			//
-			// lastAction is the same value PushSnapshot hands the goja state
-			// below: the two engines evaluate this step against one action.
+			// lastAction and logs are the same values PushSnapshot hands the
+			// goja state below: the two engines evaluate this step against one
+			// action and one set of log entries.
 			overridesCtx, overridesCancel := context.WithTimeout(ctx, observationTimeout)
-			v8Overrides, overridesErr := extractorSource.ExtractorOverrides(overridesCtx, lastAction)
+			v8Overrides, overridesErr := extractorSource.ExtractorOverrides(overridesCtx, lastAction, logs)
 			overridesCancel()
 			if overridesErr != nil {
 				// Not a warning. Without the page's values this step's
@@ -281,18 +306,44 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			extractorChanges = encodeExtractorChanges(options.Verifier.ChangedExtractors())
 		} else {
 			skippedVerification = true
-			logger.Warn("transitional tree after retry budget; skipping verifier",
+			summary.SkippedVerification++
+			logger.Warn("unsettled tree; skipping verifier",
 				"step", stepIndex, "screen", screen, "nodes", treeSize)
 		}
 		logger.Info("step", "index", stepIndex, "screen", screen, "nodes", treeSize)
 
-		nextAction, nextErr := actionSource.NextAction(ctx, stepIndex)
+		// A frame the verifier would not look at is not one to act on either.
+		// #75 is the fuzzer tapping into a screen that is still filling in, and
+		// holding the action back is also what keeps the spec's view of the run
+		// continuous: the action a step applies is reported on the NEXT step the
+		// verifier accepts, so acting here would leave the action applied last
+		// step unreported for good, and a property counting actions against
+		// their effects would then see an effect whose cause the runner
+		// swallowed. See TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt.
+		//
+		// Unbounded, because lastAction holds exactly one action: any bound that
+		// let the runner act again while the verifier was still being skipped
+		// would overwrite the action the hold was carrying, and that is the same
+		// swallow arriving one step later. A screen that keeps moving therefore
+		// costs the run its actions rather than its soundness, and a run that
+		// verified nothing says so in its outcome (internal/testrun).
+		held := skippedVerification
+		if held {
+			logger.Warn("screen still moving; holding this step's action back",
+				"step", stepIndex)
+		}
+
+		var nextAction verifier.Action
+		nextErr := verifier.ErrNoAction
 		var traceAction *trace.Action
-		if nextErr == nil {
-			traceAction = traceActionFor(nextAction, tree)
-			stampActionSource(traceAction, actionSource)
-		} else if !errors.Is(nextErr, verifier.ErrNoAction) {
-			return summary, fmt.Errorf("step %d next action: %w", stepIndex, nextErr)
+		if !held {
+			nextAction, nextErr = actionSource.NextAction(ctx, stepIndex)
+			if nextErr == nil {
+				traceAction = traceActionFor(nextAction, tree)
+				stampActionSource(traceAction, actionSource)
+			} else if !errors.Is(nextErr, verifier.ErrNoAction) {
+				return summary, fmt.Errorf("step %d next action: %w", stepIndex, nextErr)
+			}
 		}
 
 		residuals, residualErr := encodeResiduals(options.Verifier.Residuals())
@@ -300,7 +351,7 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			logger.Warn("residual encode failed", "step", stepIndex, "err", residualErr)
 		}
 
-		applySkipped := false
+		applySkipped := held
 		var actionSkipped actionSkipReason
 		if nextErr == nil && !appIsForeground(ctx, options) {
 			// The app left the foreground between observe and apply (a prior
@@ -365,7 +416,13 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 					"step", stepIndex, "reason", actionSkipped, "err", err)
 				transitional = true
 				applySkipped = true
-				lastAction = nil
+				// The error says the call failed, not that the gesture never
+				// reached the app: a deadline that fires after dispatch leaves
+				// the effect committed. Reporting no action here would let a
+				// property convict the app for an effect with no cause, so the
+				// action is reported with its fate unknown instead.
+				unconfirmed := nextAction
+				lastAction = &unconfirmed
 			} else if notDispatched != "" {
 				// The action was chosen but nothing reached the driver, so the
 				// screen is exactly the one already verified: the step stays
@@ -379,12 +436,16 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 				lastAction = nil
 			} else {
 				consecutiveApplyFailures = 0
-				actionCopy := nextAction
-				lastAction = &actionCopy
+				applied := nextAction
+				applied.Applied = true
+				lastAction = &applied
 			}
-		} else {
+		} else if !held {
 			lastAction = nil
 		}
+		// A held step leaves lastAction alone on purpose: nothing ran here, and
+		// the action it points at is still the one the next verified step has to
+		// be told about.
 
 		step := trace.Step{
 			Index:               stepIndex,
@@ -429,7 +490,16 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 		// concurrent fetches observe a stable post-action state. A transient
 		// apply error means nothing landed, so the idle poll has nothing to
 		// settle and may itself hang on the same device condition.
-		if nextErr == nil && !applySkipped && nextAction.Kind != verifier.ActionKindWait {
+		//
+		// A held step settles too, and it is the only case here that waits with
+		// nothing applied. The reread that held it takes its two reads a round
+		// trip apart, which is a tighter window than the one the detector was
+		// measured over (an action and a settle); looping straight back into it
+		// would compare two reads of a composing screen closer together still,
+		// so the screen that most needs to settle is the one given least room.
+		mutated := nextErr == nil && !applySkipped &&
+			nextAction.Kind != verifier.ActionKindWait
+		if held || mutated {
 			idleCtx, idleCancel := context.WithTimeout(ctx, options.IdleTimeout)
 			idleErr := options.Driver.WaitForIdle(idleCtx, options.IdleTimeout)
 			if idleErr != nil && idleCtx.Err() == nil {
@@ -493,6 +563,10 @@ func RenderSummary(w io.Writer, summary Summary, platform string) {
 		fmt.Fprintf(w, "%d step(s) observed nothing: the device state could not be read\n",
 			summary.FailedObservations)
 	}
+	if summary.SkippedVerification > 0 {
+		fmt.Fprintf(w, "%d step(s) judged by nothing: the screen was still moving when it was read\n",
+			summary.SkippedVerification)
+	}
 	if len(summary.UnsupportedVerbs) > 0 {
 		fmt.Fprintf(w, "unsupported on %s: %s\n",
 			platform, strings.Join(summary.UnsupportedVerbs, ", "))
@@ -542,20 +616,38 @@ func resolveIdleTimeout(options Options) time.Duration {
 	return timeout
 }
 
+// foregroundGuard is what ensureForeground had to do to put the app back in
+// front. The two interventions are separate values because they are separate
+// facts about the action they follow: a relaunch leaves it confirmed but
+// straddling a restart, while a system window holding the focus leaves it
+// dispatched with no way to tell whether the app received it.
+type foregroundGuard int
+
+const (
+	foregroundIntact foregroundGuard = iota
+	foregroundOverlayDismissed
+	foregroundRelaunched
+)
+
 // ensureForeground keeps the app under test in the foreground. When the driver
 // can report the foreground app and it no longer matches the bundle under test,
-// the app is relaunched. Returns true when a relaunch happened so the caller
-// can drop the now-stale lastAction. Drivers without ForegroundChecker (web,
+// the app is relaunched. Reports what it did so the caller can pass that on to
+// the spec through the previous action. Drivers without ForegroundChecker (web,
 // iOS) are a no-op.
-func ensureForeground(ctx context.Context, options Options, logger *slog.Logger, stepIndex int) bool {
+func ensureForeground(
+	ctx context.Context,
+	options Options,
+	logger *slog.Logger,
+	stepIndex int,
+) foregroundGuard {
 	checker, ok := options.Driver.(driver.ForegroundChecker)
 	if !ok || options.BundleID == "" {
-		return false
+		return foregroundIntact
 	}
 	foreground, err := checker.ForegroundApp(ctx)
 	if err != nil {
 		logger.Warn("foreground check failed", "step", stepIndex, "err", err)
-		return false
+		return foregroundIntact
 	}
 	if foreground != "" && foreground != options.BundleID {
 		logger.Warn("app left foreground; relaunching",
@@ -568,7 +660,7 @@ func ensureForeground(ctx context.Context, options Options, logger *slog.Logger,
 		// window, so it never acts outside the app no matter how slow the
 		// relaunch settles.
 		awaitForeground(ctx, options, logger, stepIndex)
-		return true
+		return foregroundRelaunched
 	}
 	// The app is the resumed activity, but a system overlay can still own the
 	// focused window while the app stays resumed: a fuzzer swipe starting in the
@@ -578,15 +670,15 @@ func ensureForeground(ctx context.Context, options Options, logger *slog.Logger,
 	// the app again.
 	focusChecker, hasFocus := options.Driver.(driver.FocusedWindowChecker)
 	if !hasFocus {
-		return false
+		return foregroundIntact
 	}
 	focused, err := focusChecker.FocusedWindowApp(ctx)
 	if err != nil {
 		logger.Warn("focus check failed", "step", stepIndex, "err", err)
-		return false
+		return foregroundIntact
 	}
 	if focused == "" || focused == options.BundleID {
-		return false
+		return foregroundIntact
 	}
 	logger.Warn("system window obscuring app; dismissing",
 		"step", stepIndex, "focused", focused, "want", options.BundleID)
@@ -594,7 +686,7 @@ func ensureForeground(ctx context.Context, options Options, logger *slog.Logger,
 		logger.Warn("dismiss overlay failed", "step", stepIndex, "err", err)
 	}
 	settleForForeground(ctx, options)
-	return true
+	return foregroundOverlayDismissed
 }
 
 // appIsForeground reports whether the app under test currently owns the
@@ -840,11 +932,23 @@ func applyAction(ctx context.Context, drv driver.DeviceDriver, action verifier.A
 }
 
 // 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.DeviceDriver, since time.Time) []verifier.LogEntry {
+// previous fetch. A failure is warned-on but not fatal: one unreadable fetch on
+// a flaky device should not end a run. It is not free either. This fetch is the
+// whole evidence base for state.logs, so a step that could not make it leaves
+// every log property (the default noLogcatErrors included) holding on an empty
+// slice, and that has to be visible in the run's output rather than read as the
+// app having logged nothing.
+func collectLogs(
+	ctx context.Context,
+	drv driver.DeviceDriver,
+	logger *slog.Logger,
+	step int,
+	since time.Time,
+) []verifier.LogEntry {
 	entries, err := drv.RecentLogs(ctx, since, "E")
 	if err != nil {
+		logger.Warn("log fetch failed; log properties hold vacuously this step",
+			"step", step, "err", err)
 		return nil
 	}
 	result := make([]verifier.LogEntry, 0, len(entries))
@@ -1200,10 +1304,17 @@ const (
 // orthogonal case where the frame itself is transitional.
 //
 // The transitional return reports whether the retry budget was exhausted
-// on a still-transitional tree. Callers use it to skip the verifier for
-// that step so the previous/current extractor advance does not absorb
+// on a still-transitional tree, or (when reread is set) whether a second
+// hierarchy read disagreed with the first. Callers use it to skip the verifier
+// for that step so the previous/current extractor advance does not absorb
 // transient state.
-func fetchSyncedState(ctx context.Context, options Options, logger *slog.Logger, stepIndex int) (tree *hierarchy.Tree, png []byte, transitional bool, err error) {
+func fetchSyncedState(
+	ctx context.Context,
+	options Options,
+	logger *slog.Logger,
+	stepIndex int,
+	reread bool,
+) (tree *hierarchy.Tree, png []byte, transitional bool, err error) {
 	var pngBytes []byte
 	var previousJSON string
 retryLoop:
@@ -1239,6 +1350,9 @@ retryLoop:
 		case <-timer.C:
 		}
 	}
+	if reread && err == nil && !transitional && changedOnReread(ctx, options, logger, stepIndex, tree) {
+		transitional = true
+	}
 	if len(pngBytes) > 0 {
 		if writeErr := options.TraceWriter.WriteScreenshot(stepIndex, pngBytes); writeErr != nil {
 			logger.Warn("screenshot write failed", "step", stepIndex, "err", writeErr)
@@ -1247,6 +1361,98 @@ retryLoop:
 	return tree, pngBytes, transitional, err
 }
 
+// changedOnReread reads the hierarchy once more and reports whether the screen
+// changed shape while we were looking at it. A Compose route can settle before
+// its content composes (a lazy list mounts over several frames, a query lands a
+// frame late), and a tree read in that window describes a screen that is still
+// filling in. Two reads a read apart are the cheapest thing that can see it
+// happening: the round trip IS the interval, so there is no sleep here.
+//
+// The comparison only means anything because the Hierarchy RPC serves the tree
+// the snapshot's own read produces (see snapshotTree in the sidecar). Off the
+// bare device read it does not: with an IME standing open, the snapshot answers
+// with 134 nodes and the bare read with 489, and the pair then differs over
+// whether the sidecar closed a keyboard between them rather than over anything
+// the app did.
+//
+// Waiting for the change to stop was measured on an API 34 device and refused:
+// a 750ms-quiet poll capped at 2s cost a median 1434ms against 76ms for one
+// read, hit its cap on every frame it fired for, and still handed back a frame
+// that might be filling. Detecting is what the runner can act on, because a
+// step it declines to verify is at worst a missed conviction, never a false
+// one.
+//
+// A read that fails reports no change. Nothing about a dropped RPC says the
+// screen was moving, and skipping verification on it would quietly spend the
+// run's evidence on a flaky link.
+func changedOnReread(
+	ctx context.Context,
+	options Options,
+	logger *slog.Logger,
+	stepIndex int,
+	first *hierarchy.Tree,
+) bool {
+	// An empty tree is skipped by the caller anyway, so the read buys nothing.
+	if first == nil || len(first.Elements) == 0 {
+		return false
+	}
+	hierarchyJSON, err := options.Driver.Hierarchy(ctx)
+	if err != nil {
+		logger.Warn("second hierarchy read failed", "step", stepIndex, "err", err)
+		return false
+	}
+	second, err := hierarchy.Parse(hierarchyJSON)
+	if err != nil || second == nil {
+		logger.Warn("second hierarchy parse failed", "step", stepIndex, "err", err)
+		return false
+	}
+	if structuralShape(first) == structuralShape(second) {
+		return false
+	}
+	logger.Warn("screen changed between two reads; skipping verifier",
+		"step", stepIndex, "nodes", len(first.Elements), "then", len(second.Elements))
+	return true
+}
+
+// structuralShape renders what is on screen as its nodes' identities in tree
+// order: how many there are, and which ids and classes they carry.
+//
+// Text and bounds are deliberately absent. A measure pass that moves pixels is
+// not a screen still composing, and neither is a value arriving into a node
+// that already exists, which this cannot tell apart from a clock ticking. This
+// decides whether a property gets to judge at all, so it reads only what a
+// change in what is on screen can move: a detector that fires on every step of
+// a screen with a timer on it would leave the run green and vacuous, which is
+// worse than the composition it set out to catch. The trade is measured rather
+// than assumed: over 100 folio steps on an API 35 emulator, text moved under
+// an unchanged shape on 1 step, and the shape itself moved on 1 other.
+//
+// TestRunner_OnlyAChangeOfShapeCostsAStepItsVerdict is what holds the line:
+// adding either field back to the shape turns one of its cases red.
+func structuralShape(tree *hierarchy.Tree) string {
+	var shape strings.Builder
+	for _, element := range tree.Elements {
+		shape.WriteString(element.ResourceID)
+		shape.WriteByte(0x1f)
+		shape.WriteString(element.Class)
+		shape.WriteByte(0x1e)
+	}
+	return shape.String()
+}
+
+// driverIsAndroid asks the driver what it is, once per run, so the step loop
+// never repeats the RPC. It gates the reread: #75 is about Compose composition,
+// and web and iOS have their own settle paths and no measurement saying an
+// extra hierarchy read there is cheap. An unreadable answer is not android.
+func driverIsAndroid(ctx context.Context, options Options, logger *slog.Logger) bool {
+	health, err := options.Driver.Health(ctx)
+	if err != nil {
+		logger.Warn("health read failed; not rereading the hierarchy", "err", err)
+		return false
+	}
+	return health.Platform == "android"
+}
+
 func traceActionFor(action verifier.Action, tree *hierarchy.Tree) *trace.Action {
 	traceAction := &trace.Action{Kind: string(action.Kind), X: action.X, Y: action.Y}
 	switch action.Kind {

internal/runner/runner_test.go

@@ -253,6 +253,23 @@ func TestRenderSummary_OmitsUnsupportedLineWhenNone(t *testing.T) {
 	}
 }
 
+// A step nothing judged is not a step that passed. The run prints its count so
+// a green summary cannot hide a run that skipped most of its steps, which is
+// what a screen that keeps moving under the reads would produce.
+func TestRenderSummary_CountsTheStepsNothingJudged(t *testing.T) {
+	var out bytes.Buffer
+	RenderSummary(&out, Summary{Steps: 10, SkippedVerification: 4}, "android")
+	if !strings.Contains(out.String(), "4 step(s) judged by nothing") {
+		t.Errorf("expected the unjudged-step count, got:\n%s", out.String())
+	}
+
+	out.Reset()
+	RenderSummary(&out, Summary{Steps: 10}, "android")
+	if strings.Contains(out.String(), "judged by nothing") {
+		t.Errorf("a run that judged every step must not print the line, got:\n%s", out.String())
+	}
+}
+
 func TestRunner_ViolationSurfacesInSummary(t *testing.T) {
 	state := newHarnessWithSpec(t, violationSpec)
 
@@ -1507,8 +1524,15 @@ func TestRunner_UsesAtomicSnapshot(t *testing.T) {
 	if snapshotCalls == 0 {
 		t.Errorf("expected at least one Snapshot call, got %d", snapshotCalls)
 	}
-	if hierarchyCalls != 0 {
-		t.Errorf("expected zero standalone Hierarchy calls (runner must use Snapshot), got %d", hierarchyCalls)
+	// The recorded pair still comes from Snapshot. The standalone hierarchy
+	// reads are the composition detector (changedOnReread), one per step at
+	// most, and they are never the source of what the step records.
+	if hierarchyCalls > summary.Steps {
+		t.Errorf("expected at most one standalone Hierarchy call per step (runner must observe through Snapshot), got %d over %d steps",
+			hierarchyCalls, summary.Steps)
+	}
+	if snapshotCalls < summary.Steps {
+		t.Errorf("expected a Snapshot per step, got %d over %d steps", snapshotCalls, summary.Steps)
 	}
 	if screenshotCalls != 0 {
 		t.Errorf("expected zero standalone Screenshot calls (runner must use Snapshot), got %d", screenshotCalls)
@@ -2339,8 +2363,10 @@ func TestEnsureForeground_DismissesSystemOverlay(t *testing.T) {
 	logger := slog.New(slog.NewTextHandler(io.Discard, &slog.HandlerOptions{Level: slog.LevelWarn}))
 	options := Options{BundleID: "app.folio", Driver: m, IdleTimeout: 10 * time.Millisecond}
 
-	if !ensureForeground(context.Background(), options, logger, 5) {
-		t.Fatal("expected the guard to act on the focus-stealing overlay")
+	got := ensureForeground(context.Background(), options, logger, 5)
+	if got != foregroundOverlayDismissed {
+		t.Fatalf("the guard reported %v, want foregroundOverlayDismissed; "+
+			"an obscured app is not a relaunched one", got)
 	}
 	backs, relaunches := 0, 0
 	for _, a := range m.Actions() {

internal/runner/source.go

@@ -26,14 +26,15 @@ type ActionSource interface {
 // PushSnapshot. The mobile path has none (returns nil); the web path returns the
 // values its extractors computed in V8 against the real DOM.
 //
-// lastAction is the action the previous step actually applied, the same value
-// PushSnapshot hands the goja state. The web path has to install it in the page
-// before its extractors run: a spec extractor reading state.lastAction runs in
-// V8 there, and V8 has no way to know what the runner dispatched.
+// lastAction and logs are what PushSnapshot hands the goja state. The web path
+// has to install both in the page before its extractors run: a spec extractor
+// reading state.lastAction or state.logs runs in V8 there, and V8 knows neither
+// what the runner dispatched nor what the driver's log fetch returned.
 type ExtractorSource interface {
 	ExtractorOverrides(
 		ctx context.Context,
 		lastAction *verifier.Action,
+		logs []verifier.LogEntry,
 	) (map[int]json.RawMessage, error)
 }
 
@@ -44,6 +45,13 @@ type lastActionInstaller interface {
 	SetLastAction(ctx context.Context, encoded json.RawMessage) error
 }
 
+// logInstaller is the same channel for the entries this step's log fetch
+// returned. Console output reaches the driver over CDP, so the page can only
+// learn about it from the runner.
+type logInstaller interface {
+	SetLogs(ctx context.Context, encoded json.RawMessage) error
+}
+
 // gojaSource drives both action selection and (trivially) extractor overrides
 // for the mobile path, where the goja-bundled picker runs in-process and no V8
 // extractor values exist.
@@ -58,6 +66,7 @@ func (s gojaSource) NextAction(context.Context, int) (verifier.Action, error) {
 func (gojaSource) ExtractorOverrides(
 	context.Context,
 	*verifier.Action,
+	[]verifier.LogEntry,
 ) (map[int]json.RawMessage, error) {
 	return nil, nil
 }
@@ -79,24 +88,35 @@ func (s webSource) NextAction(ctx context.Context, _ int) (verifier.Action, erro
 	return verifier.DecodeAction(raw)
 }
 
-// ExtractorOverrides installs the previous step's action in the page, then
-// reads back what the spec's extractors computed against the live DOM. The
-// install is not best-effort: a web driver that cannot take it leaves
-// state.lastAction null in V8, which silently turns every action-gated
-// property vacuously true, so it is reported as an error instead.
+// ExtractorOverrides installs the previous step's action and this step's log
+// entries in the page, then reads back what the spec's extractors computed
+// against the live DOM. Neither install is best-effort: a web driver that
+// cannot take them leaves state.lastAction null and state.logs empty in V8,
+// which silently turns every action-gated property and every log property
+// vacuously true, so both are reported as errors instead.
 func (s webSource) ExtractorOverrides(
 	ctx context.Context,
 	lastAction *verifier.Action,
+	logs []verifier.LogEntry,
 ) (map[int]json.RawMessage, error) {
-	installer, ok := s.web.(lastActionInstaller)
+	actions, ok := s.web.(lastActionInstaller)
 	if !ok {
 		return nil, fmt.Errorf(
 			"web driver %T cannot install state.lastAction; every property gated "+
 				"on the last action would be vacuously true", s.web)
 	}
-	if err := installer.SetLastAction(ctx, verifier.EncodeLastAction(lastAction)); err != nil {
+	if err := actions.SetLastAction(ctx, verifier.EncodeLastAction(lastAction)); err != nil {
 		return nil, fmt.Errorf("install last action: %w", err)
 	}
+	entries, ok := s.web.(logInstaller)
+	if !ok {
+		return nil, fmt.Errorf(
+			"web driver %T cannot install state.logs; every property reading the "+
+				"log stream would be vacuously true", s.web)
+	}
+	if err := entries.SetLogs(ctx, verifier.EncodeLogs(logs)); err != nil {
+		return nil, fmt.Errorf("install logs: %w", err)
+	}
 	return s.web.EvaluateExtractors(ctx)
 }
 

internal/runner/uncertain_last_action_test.go

@@ -0,0 +1,154 @@
+package runner
+
+import (
+	"context"
+	"errors"
+	"fmt"
+	"path/filepath"
+	"sync/atomic"
+	"testing"
+	"time"
+
+	"github.com/priyanshujain/sanderling/internal/driver"
+	mockdriver "github.com/priyanshujain/sanderling/internal/driver/mock"
+)
+
+// An apply error is not proof that nothing landed. An RPC deadline that fires
+// after the tap was dispatched leaves the transaction committed, and a runner
+// that reports "no action" for it hands
+// submitCommitsOneTransactionPerAction a rise of one transaction against a
+// window of zero submits: a conviction manufactured out of the runner's own
+// uncertainty, on the property carrying most of the detection on android.
+//
+// The spec below is the real folio predicate pair, imported from the example,
+// so what this asserts is the verdict the shipped property reaches.
+const submitCountingSpecTemplate = `
+import { actions, always, extract, next, Tap } from "@sanderling/spec";
+import {
+  committedTransactionsExceedSubmits,
+  countSubmitsInWindow,
+} from "%s";
+
+let submits = 0;
+const submitsInWindow = extract("submitsInWindow", state => {
+  const window = countSubmitsInWindow({
+    previousCount: submits,
+    lastAction: state.lastAction,
+    fresh: true,
+  });
+  submits = window.next;
+  return window.reported;
+});
+
+const counts = extract("counts", state => {
+  const text = state.ax.find("id:TxnCount")?.text;
+  return text ? { Travel: parseInt(text, 10) } : null;
+});
+
+globalThis.properties = {
+  submitCommitsOneTransactionPerAction: always(
+    next(() =>
+      !committedTransactionsExceedSubmits({
+        countsBefore: counts.previous ?? null,
+        countsAfter: counts.current,
+        submitsInWindow: submitsInWindow.current,
+      }),
+    ),
+  ),
+};
+globalThis.actions = actions(() => [Tap({ on: "id:TxnSubmit" })]);
+`
+
+const homeWithTxnCount = `{"attributes":{"resource-id":"HomeScreen"},"children":[
+	{"attributes":{"resource-id":"TxnCount","text":"%d"},"children":[]},
+	{"attributes":{"resource-id":"TxnSubmit","bounds":"[40,80,240,160]"},"children":[],"clickable":true,"enabled":true}
+]}`
+
+// dispatchThenFailDriver is the device condition the runner cannot see through:
+// the tap reaches the app and commits, then the call the runner is waiting on
+// times out. Every later hierarchy read shows the committed transactions.
+type dispatchThenFailDriver struct {
+	*mockdriver.Driver
+	commitsPerTap int64
+	committed     atomic.Int64
+}
+
+func (d *dispatchThenFailDriver) Tap(context.Context, int, int) error {
+	return d.dispatchThenFail()
+}
+
+func (d *dispatchThenFailDriver) TapSelector(context.Context, string) error {
+	return d.dispatchThenFail()
+}
+
+func (d *dispatchThenFailDriver) dispatchThenFail() error {
+	d.committed.Add(d.commitsPerTap)
+	return errors.New("rpc error: code = DeadlineExceeded desc = context deadline exceeded")
+}
+
+func (d *dispatchThenFailDriver) Snapshot(context.Context) (string, driver.Image, error) {
+	return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), driver.Image{}, nil
+}
+
+func (d *dispatchThenFailDriver) Hierarchy(context.Context) (string, error) {
+	return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil
+}
+
+func TestRunner_ApplyErrorAfterDispatchDoesNotConvictTheSubmitCountingProperty(t *testing.T) {
+	predicates, err := filepath.Abs("../../examples/folio/sanderling/predicates.ts")
+	if err != nil {
+		t.Fatal(err)
+	}
+	spec := fmt.Sprintf(submitCountingSpecTemplate, predicates)
+
+	run := func(t *testing.T, commitsPerTap int64) []ViolationRecord {
+		t.Helper()
+		state := newHarnessWithSpec(t, spec)
+		device := &dispatchThenFailDriver{Driver: state.mock, commitsPerTap: commitsPerTap}
+
+		ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
+		defer cancel()
+		summary, err := Run(ctx, Options{
+			Duration:    time.Hour,
+			IdleTimeout: 20 * time.Millisecond,
+			MaxSteps:    2,
+			Driver:      device,
+			Verifier:    state.verifier,
+			TraceWriter: state.writer,
+		})
+		if err != nil {
+			t.Fatalf("Run: %v", err)
+		}
+		if summary.Steps != 2 {
+			t.Fatalf("steps = %d, want 2; the run never reached the step that judges the pair", summary.Steps)
+		}
+		if got := device.committed.Load(); got != commitsPerTap*2 {
+			t.Fatalf("the device committed %d transaction(s), want %d; the taps never reached it",
+				got, commitsPerTap*2)
+		}
+		return summary.Violations
+	}
+
+	t.Run("one transaction per tap is not a double submit", func(t *testing.T) {
+		if violations := run(t, 1); len(violations) != 0 {
+			t.Errorf("the counting property convicted a healthy app: %v\n"+
+				"one transaction rose against a submit the runner dispatched but "+
+				"could not confirm, and the spec was told no action happened",
+				violations)
+		}
+	})
+
+	// The control. Without it a green above proves nothing: a property that
+	// never sees a comparable pair is silently vacuous and reports the same
+	// empty violation list.
+	t.Run("two transactions per tap still convicts", func(t *testing.T) {
+		violations := run(t, 2)
+		if len(violations) == 0 {
+			t.Fatal("the counting property missed a double submit; the harness never " +
+				"put the property in a position to fire, so the case above proves nothing")
+		}
+		if violations[0].Properties[0] != "submitCommitsOneTransactionPerAction" {
+			t.Errorf("violated %v, want submitCommitsOneTransactionPerAction", violations[0].Properties)
+		}
+	})
+}

internal/runner/web_carrier_test.go

@@ -55,6 +55,12 @@ func (d *carrierWebDriver) Snapshot(ctx context.Context) (string, driver.Image,
 
 func (d *carrierWebDriver) InstallBundle(context.Context, []byte) error { return nil }
 
+// A web target says so. The runner's per-step hierarchy reread is android-only,
+// and a fake claiming android would take a path no chrome run takes.
+func (d *carrierWebDriver) Health(context.Context) (driver.Health, error) {
+	return driver.Health{Ready: true, Version: "fake", Platform: "web"}, nil
+}
+
 func (d *carrierWebDriver) EvaluateExtractors(context.Context) (map[int]json.RawMessage, error) {
 	d.reads++
 	return map[int]json.RawMessage{0: json.RawMessage(strconv.Itoa(d.reads))}, nil
@@ -69,6 +75,8 @@ func (d *carrierWebDriver) NextActionFromV8(context.Context) (json.RawMessage, e
 
 func (d *carrierWebDriver) SetLastAction(context.Context, json.RawMessage) error { return nil }
 
+func (d *carrierWebDriver) SetLogs(context.Context, json.RawMessage) error { return nil }
+
 // TestRunner_TransitionalStepNeverAdvancesThePageCarrier pins the ordering the
 // web path depends on. The page-side extractors must run only on steps the
 // verifier accepts: their getters advance spec state every time they evaluate,
@@ -166,6 +174,8 @@ func (d *installFailsWebDriver) SetLastAction(context.Context, json.RawMessage)
 	return errors.New("__sanderlingSetLastAction__ is not a function")
 }
 
+func (d *installFailsWebDriver) SetLogs(context.Context, json.RawMessage) error { return nil }
+
 // TestRunner_LastActionInstallFailureFailsTheRun covers the other half of the
 // same trust boundary. A run that cannot install lastAction in the page cannot
 // apply the page's extractor values either, so the step keeps goja's
@@ -194,3 +204,49 @@ func TestRunner_LastActionInstallFailureFailsTheRun(t *testing.T) {
 		t.Errorf("Run error = %v, want it to name the failed lastAction install", err)
 	}
 }
+
+// logInstallFailsWebDriver takes lastAction and refuses the logs, the shape a
+// page carrying an older published @sanderling/spec runtime has: it knows the
+// action setter and not the log one.
+type logInstallFailsWebDriver struct {
+	*installFailsWebDriver
+}
+
+func (d *logInstallFailsWebDriver) SetLastAction(context.Context, json.RawMessage) error {
+	return nil
+}
+
+func (d *logInstallFailsWebDriver) SetLogs(context.Context, json.RawMessage) error {
+	return errors.New("__sanderlingSetLogs__ is not a function")
+}
+
+// TestRunner_LogInstallFailureFailsTheRun holds the log channel to the same
+// standard as the action one. The driver having the console errors decides
+// nothing on web: the page's reading of every extractor replaces the host's, so
+// a run that cannot put the entries back into the page evaluates noLogcatErrors
+// against an empty array and reports green on a console full of errors.
+// Continuing past this is the vacuity the whole install exists to prevent.
+func TestRunner_LogInstallFailureFailsTheRun(t *testing.T) {
+	state := newHarnessWithSpec(t, carrierSpec)
+	web := &logInstallFailsWebDriver{
+		installFailsWebDriver: &installFailsWebDriver{Driver: state.mock},
+	}
+
+	ctx, cancel := context.WithTimeout(context.Background(), 10*time.Second)
+	defer cancel()
+	_, err := Run(ctx, Options{
+		Duration:    2 * time.Second,
+		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    3,
+		Driver:      web,
+		Verifier:    state.verifier,
+		TraceWriter: state.writer,
+	})
+	if err == nil {
+		t.Fatal("Run succeeded with a page that cannot take the step's logs; " +
+			"every property reading the log stream ran against an empty array")
+	}
+	if !bytes.Contains([]byte(err.Error()), []byte("install logs")) {
+		t.Errorf("Run error = %v, want it to name the failed log install", err)
+	}
+}

internal/runner/web_extractor_trace_test.go

@@ -47,6 +47,8 @@ func (d *webMockDriver) NextActionFromV8(context.Context) (json.RawMessage, erro
 
 func (d *webMockDriver) SetLastAction(context.Context, json.RawMessage) error { return nil }
 
+func (d *webMockDriver) SetLogs(context.Context, json.RawMessage) error { return nil }
+
 // TestRunner_TraceRecordsTheValueTheVerdictUsed fails if the trace and the
 // verdict disagree about an extractor. A witness is only an explanation of a
 // violation if it holds the state the violated property was evaluated against.

internal/runner/web_last_action_test.go

@@ -1,11 +1,16 @@
 package runner
 
 import (
+	"bytes"
 	"context"
 	"encoding/json"
+	"errors"
+	"log/slog"
+	"strings"
 	"testing"
 	"time"
 
+	"github.com/priyanshujain/sanderling/internal/driver"
 	mockdriver "github.com/priyanshujain/sanderling/internal/driver/mock"
 )
 
@@ -25,7 +30,8 @@ globalThis.properties = {};
 // control, so the runner has a real applied action to report on the next step.
 type tappingWebDriver struct {
 	*mockdriver.Driver
-	installed []string
+	installed     []string
+	installedLogs []string
 }
 
 func (d *tappingWebDriver) InstallBundle(context.Context, []byte) error { return nil }
@@ -43,6 +49,11 @@ func (d *tappingWebDriver) SetLastAction(_ context.Context, encoded json.RawMess
 	return nil
 }
 
+func (d *tappingWebDriver) SetLogs(_ context.Context, encoded json.RawMessage) error {
+	d.installedLogs = append(d.installedLogs, string(encoded))
+	return nil
+}
+
 func TestRunner_WebInstallsLastActionInThePage(t *testing.T) {
 	state := newHarnessWithSpec(t, lastActionSpec)
 	web := &tappingWebDriver{Driver: state.mock}
@@ -71,7 +82,114 @@ func TestRunner_WebInstallsLastActionInThePage(t *testing.T) {
 	// Every later step carries what the runner actually applied. The shape is
 	// the goja host's (internal/verifier/marshal.go lastActionFields), pinned
 	// against it by TestLastAction_WebJSONMatchesTheGojaObject.
-	const want = `{"kind":"Tap","on":"id:TxnSubmit"}`
+	const want = `{"kind":"Tap","applied":true,"relaunched":null,"on":"id:TxnSubmit"}`
+	if web.installed[1] != want {
+		t.Errorf("step 2 installed %s, want %s", web.installed[1], want)
+	}
+}
+
+// The same hole on the other channel: state.logs was hardcoded [] in
+// pkg/spec/src/web-runtime.ts, and because the page's reading of an extractor
+// replaces the host's on web, the driver's error-level entries never reached a
+// property. The default noLogcatErrors counted an empty array on every run.
+func TestRunner_WebInstallsTheStepsLogsInThePage(t *testing.T) {
+	state := newHarnessWithSpec(t, lastActionSpec)
+	state.mock.LogEntries = []driver.LogEntry{
+		{UnixMillis: 1700000000123, Level: "E", Tag: "console", Message: "boom from the page"},
+	}
+	web := &tappingWebDriver{Driver: state.mock}
+
+	ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second)
+	defer cancel()
+	if _, err := Run(ctx, Options{
+		Duration:    time.Hour,
+		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    2,
+		Driver:      web,
+		Verifier:    state.verifier,
+		TraceWriter: state.writer,
+	}); err != nil {
+		t.Fatalf("Run: %v", err)
+	}
+
+	if len(web.installedLogs) == 0 {
+		t.Fatal("the page was never handed the step's logs; every property reading " +
+			"state.logs evaluated against the empty array the page starts with")
+	}
+	// The shape is the goja host's (internal/verifier/marshal.go logFields),
+	// pinned against it by TestLogs_WebJSONMatchesTheGojaObject.
+	const want = `[{"unixMillis":1700000000123,"level":"E","tag":"console","message":"boom from the page"}]`
+	if web.installedLogs[0] != want {
+		t.Errorf("step 1 installed %s, want %s", web.installedLogs[0], want)
+	}
+}
+
+// A log fetch that fails decides the verdict of every log property: they all
+// evaluate against an empty slice and hold. That is not a fact about the app,
+// so the step it happened on has to be visible in the run's output. It used to
+// be dropped in silence, under a comment claiming it was warned about.
+func TestRunner_ReportsALogFetchItCouldNotMake(t *testing.T) {
+	state := newHarnessWithSpec(t, lastActionSpec)
+	state.mock.Failures[mockdriver.ActionRecentLogs] = errors.New("adb: device offline")
+
+	var buffer bytes.Buffer
+	logger := slog.New(slog.NewTextHandler(&buffer, &slog.HandlerOptions{Level: slog.LevelWarn}))
+
+	ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second)
+	defer cancel()
+	if _, err := Run(ctx, Options{
+		Duration:    time.Hour,
+		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    2,
+		Driver:      state.mock,
+		Verifier:    state.verifier,
+		TraceWriter: state.writer,
+		Logger:      logger,
+	}); err != nil {
+		t.Fatalf("Run: %v", err)
+	}
+
+	if !strings.Contains(buffer.String(), "adb: device offline") {
+		t.Errorf("the run never reported the failed log fetch, so noLogcatErrors "+
+			"held on evidence nobody collected; log was %q", buffer.String())
+	}
+}
+
+// failingTapWebDriver dispatches the tap and then fails the call, the shape an
+// RPC deadline takes: the page has the click, the runner has an error.
+type failingTapWebDriver struct {
+	*tappingWebDriver
+}
+
+func (d *failingTapWebDriver) Tap(context.Context, int, int) error {
+	return errors.New("rpc error: code = DeadlineExceeded desc = context deadline exceeded")
+}
+
+// The web leg of the same three states the goja host reports. "applied":null is
+// not "no action": a property gated on the last action still sees the tap and
+// decides for itself, which it cannot do if the page is handed a bare null.
+func TestRunner_WebInstallsAnUnconfirmedActionWithItsFateUnknown(t *testing.T) {
+	state := newHarnessWithSpec(t, lastActionSpec)
+	web := &failingTapWebDriver{tappingWebDriver: &tappingWebDriver{Driver: state.mock}}
+
+	ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second)
+	defer cancel()
+	if _, err := Run(ctx, Options{
+		Duration:    time.Hour,
+		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    2,
+		Driver:      web,
+		Verifier:    state.verifier,
+		TraceWriter: state.writer,
+	}); err != nil {
+		t.Fatalf("Run: %v", err)
+	}
+
+	if len(web.installed) < 2 {
+		t.Fatalf("the page was handed lastAction %d time(s); the web path never installed it",
+			len(web.installed))
+	}
+	const want = `{"kind":"Tap","applied":null,"relaunched":null,"on":"id:TxnSubmit"}`
 	if web.installed[1] != want {
 		t.Errorf("step 2 installed %s, want %s", web.installed[1], want)
 	}