Merge branch 'relaunch-signal-and-badge-reach' into trial-merge

internal/runner/composition_reread_test.go

@@ -0,0 +1,297 @@
+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"
+)
+
+// 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 a transaction 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, or on every one of them.
+type submitsOnTapDriver struct {
+	*mockdriver.Driver
+	composingRead 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(1)
+	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) {
+	if read := d.reads.Add(1); d.everyRead || read == d.composingRead {
+		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, 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)
+		}
+	})
+}
+
+// Holding an action back is bounded. A screen that changes shape under every
+// pair of reads (a live list, a spinner mounting and unmounting) would
+// otherwise take the whole run: nothing verified, nothing tapped, and a green
+// summary at the end of it.
+func TestRunner_AScreenThatNeverSettlesDoesNotStallTheRun(t *testing.T) {
+	state := newHarnessWithSpec(t, specWithFolioPredicates(t))
+	device := &submitsOnTapDriver{Driver: state.mock, 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.SkippedVerification != 5 {
+		t.Fatalf("the run verified some step of a screen that never settled: skipped %d of 5",
+			summary.SkippedVerification)
+	}
+	if device.committed.Load() == 0 {
+		t.Error("the fuzzer never acted across 5 steps; a screen that keeps moving must " +
+			"cost the run a step or two, not all of them")
+	}
+}
+
+type traceLine struct {
+	Step       int      `json:"step"`
+	Violations []string `json:"violations"`
+}
+
+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/foreground_guard_last_action_test.go

@@ -0,0 +1,287 @@
+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
+}
+
+// No device answers Snapshot and Hierarchy off different trees, and the runner
+// reads both per step, so 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)
+		}
+	})
+}

internal/runner/runner.go

@@ -52,6 +52,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.
@@ -89,11 +94,13 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 		return Summary{}, err
 	}
 	_, pageExtractors := extractorSource.(webSource)
+	rereadHierarchy := driverIsAndroid(ctx, options, logger)
 
 	summary := Summary{StartTime: time.Now()}
 	deadline := summary.StartTime.Add(options.Duration)
 	stepIndex := 0
 	consecutiveApplyFailures := 0
+	heldSteps := 0
 	var lastAction *verifier.Action
 	var lastLogTime time.Time
 	for time.Now().Before(deadline) {
@@ -110,8 +117,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
@@ -132,7 +154,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 {
@@ -173,8 +196,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
@@ -247,18 +272,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)
+		// 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.
+		//
+		// Bounded, because a screen that never settles must not stall the whole
+		// run: past the bound the runner acts anyway, which is where it was
+		// before this held anything back.
+		held := skippedVerification && heldSteps < maxHeldSteps
+		if held {
+			heldSteps++
+			logger.Warn("screen still moving; holding this step's action back",
+				"step", stepIndex, "held", heldSteps)
+		} else {
+			heldSteps = 0
+		}
+
+		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)
+			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())
@@ -266,7 +317,7 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			logger.Warn("residual encode failed", "step", stepIndex, "err", residualErr)
 		}
 
-		applySkipped := false
+		applySkipped := held
 		if nextErr == nil && !appIsForeground(ctx, options) {
 			// The app left the foreground between observe and apply (a prior
 			// action's gesture settling late, or an async navigation). The
@@ -311,9 +362,12 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 				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,
@@ -396,6 +450,10 @@ func RenderSummary(w io.Writer, summary Summary, platform string) {
 			fmt.Fprintf(w, "  step %d: %v\n", violation.StepIndex, violation.Properties)
 		}
 	}
+	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, ", "))
@@ -445,20 +503,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",
@@ -471,7 +547,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
@@ -481,15 +557,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)
@@ -497,7 +573,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
@@ -931,10 +1007,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:
@@ -970,6 +1053,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)
@@ -978,6 +1064,88 @@ 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.
+//
+// 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.
+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 {
@@ -1148,6 +1316,14 @@ func encodeResiduals(residuals map[string]ltl.Formula) (map[string]json.RawMessa
 // would be spent doing nothing.
 const maxConsecutiveApplyFailures = 3
 
+// maxHeldSteps bounds how many steps in a row the runner will decline to act on
+// because their screen was still moving. It is a livelock bound, not a settle
+// budget: a screen that changes shape under every pair of reads (a live list, a
+// spinner that mounts and unmounts) would otherwise take the whole run without
+// the fuzzer ever touching it. Two is what the measured cases need, which came
+// one step at a time and never twice in a row.
+const maxHeldSteps = 2
+
 // isWDADrop reports that the sidecar could not restart the iOS XCTest
 // runner: the channel is gone for good and the run must abort. Transient
 // drops are classified by the sidecar itself (it reconnects and surfaces

internal/runner/runner_test.go

@@ -196,6 +196,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)
 
@@ -1073,8 +1090,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)
@@ -1894,8 +1918,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/uncertain_last_action_test.go

@@ -22,7 +22,7 @@ import (
 //
 // 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 uncertainApplySpecTemplate = `
+const submitCountingSpecTemplate = `
 import { actions, always, extract, next, Tap } from "@sanderling/spec";
 import {
   committedTransactionsExceedSubmits,
@@ -90,12 +90,16 @@ func (d *dispatchThenFailDriver) Snapshot(context.Context) (string, driver.Image
 	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(uncertainApplySpecTemplate, predicates)
+	spec := fmt.Sprintf(submitCountingSpecTemplate, predicates)
 
 	run := func(t *testing.T, commitsPerTap int64) []ViolationRecord {
 		t.Helper()

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

internal/runner/web_last_action_test.go

@@ -72,7 +72,7 @@ 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","applied":true,"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)
 	}
@@ -112,7 +112,7 @@ func TestRunner_WebInstallsAnUnconfirmedActionWithItsFateUnknown(t *testing.T) {
 		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,"on":"id:TxnSubmit"}`
+	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)
 	}

internal/verifier/marshal.go

@@ -353,9 +353,20 @@ func lastActionFields(action *Action) []actionField {
 	if action.Applied {
 		applied = true
 	}
+	// A relaunch between two readings is not "no action happened", which is
+	// what dropping the action reported instead: the app restarted after an
+	// action that did run. Only the positive report is a fact the runner can
+	// vouch for, so the other side is null rather than false: a target whose
+	// foreground the runner cannot read (web, iOS) never relaunches the app and
+	// still cannot promise it never restarted.
+	var relaunched any
+	if action.Relaunched {
+		relaunched = true
+	}
 	fields := []actionField{
 		{key: "kind", value: string(action.Kind)},
 		{key: "applied", value: applied},
+		{key: "relaunched", value: relaunched},
 	}
 	if action.On != "" {
 		fields = append(fields, actionField{key: "on", value: action.On})

internal/verifier/marshal_test.go

@@ -169,6 +169,7 @@ func TestLastAction_WebJSONMatchesTheGojaObject(t *testing.T) {
 		{"nil", nil},
 		{"Tap", &Action{Kind: ActionKindTap, On: "id:TxnSubmit", X: 12, Y: 34}},
 		{"TapApplied", &Action{Kind: ActionKindTap, On: "id:TxnSubmit", Applied: true}},
+		{"TapRelaunched", &Action{Kind: ActionKindTap, On: "id:TxnSubmit", Applied: true, Relaunched: true}},
 		{"TapWithoutSelector", &Action{Kind: ActionKindTap, X: 12, Y: 34}},
 		{"DoubleTap", &Action{Kind: ActionKindDoubleTap, On: `desc:say "hi" <b>`}},
 		{"InputText", &Action{Kind: ActionKindInputText, On: "id:field", Text: "50"}},
@@ -233,3 +234,51 @@ func TestLastAction_SeparatesNoActionFromAnActionOfUnknownFate(t *testing.T) {
 		})
 	}
 }
+
+// The runner relaunches the app when it leaves the foreground, which used to be
+// reported to the spec as "no action ran between these two readings". The
+// action did run; what a property cannot assume across it is that app state was
+// continuous, so the relaunch is its own fact on an action that keeps its
+// confirmed dispatch.
+func TestLastAction_ReportsARelaunchSeparatelyFromTheDispatch(t *testing.T) {
+	verifier := newVerifier(t)
+	mustLoad(t, verifier, `
+		globalThis.continuity = __sanderling__.extract(state =>
+			state.lastAction === null ? "no action"
+			: state.lastAction.applied !== true ? "unconfirmed"
+			: state.lastAction.relaunched === true ? "applied across a relaunch"
+			: state.lastAction.relaunched === null ? "applied, no relaunch reported"
+			: "unreadable");
+	`)
+
+	for _, testCase := range []struct {
+		name   string
+		action *Action
+		want   string
+	}{
+		{"nothing ran", nil, "no action"},
+		{
+			"confirmed, app stayed",
+			&Action{Kind: ActionKindTap, On: "id:TxnSubmit", Applied: true},
+			"applied, no relaunch reported",
+		},
+		{
+			"confirmed, app relaunched after it",
+			&Action{Kind: ActionKindTap, On: "id:TxnSubmit", Applied: true, Relaunched: true},
+			"applied across a relaunch",
+		},
+	} {
+		t.Run(testCase.name, func(t *testing.T) {
+			if err := verifier.PushSnapshot(SnapshotInput{
+				Snapshots:  Snapshots{},
+				LastAction: testCase.action,
+			}); err != nil {
+				t.Fatal(err)
+			}
+			handle := verifier.runtime.GlobalObject().Get("continuity").ToObject(verifier.runtime)
+			if got := handle.Get("current").String(); got != testCase.want {
+				t.Errorf("the spec read %q, want %q", got, testCase.want)
+			}
+		})
+	}
+}

internal/verifier/types.go

@@ -38,6 +38,12 @@ type Action struct {
 	// when the apply call failed and nothing can say whether the action
 	// reached the app. The spec is told which of the two it is.
 	Applied bool
+	// Relaunched, like Applied, is meaningful only on state.lastAction: the
+	// runner brought the app back to the foreground after this action, so the
+	// two readings the spec compares straddle a restart. The action still
+	// happened; what a property cannot assume across it is that app state ran
+	// continuously from one reading to the next.
+	Relaunched bool
 }
 
 // LogEntry mirrors a logcat line captured between steps.

pkg/spec/src/types.ts

@@ -109,8 +109,17 @@ export interface ExceptionRecord {
  * tap landed. Null is unknown, not "it did not happen" (`state.lastAction` is
  * itself null for that), so a property attributing an effect to this action
  * has to decline unless `applied` is true.
+ *
+ * `relaunched` is true when the runner had to bring the app back to the
+ * foreground after this action, so the previous reading and the current one
+ * straddle a restart. The action itself still happened; what a property cannot
+ * assume across it is that app state ran continuously between the two readings,
+ * and one demanding an effect of this action has to decline. Null is "not
+ * reported", which is weaker than "the app never restarted": a target whose
+ * foreground the runner cannot read never relaunches the app and cannot promise
+ * that either.
  */
-export type LastAction = Action & { applied: true | null };
+export type LastAction = Action & { applied: true | null; relaunched: true | null };
 
 export interface State {
   snapshots: Snapshots;

replay-ui/sanderling/spec.ts

@@ -170,11 +170,44 @@ const switchATab = actions(() => {
   return tabs.length === 0 ? [] : [Tap({ on: from(tabs).generate() })];
 });
 
+// badgeCountMatchesThePanel needs two readings on ONE step: the badge, which a
+// tab strip renders only for a step that HAS a violation, and a violations
+// panel to compare it against, which exists while the properties or violations
+// tab is selected. Undirected actions put both on the same step 0 times in the
+// 80 of the first dogfood run: the property was reachable in principle and
+// judged nothing in practice.
+//
+// Both halves have to be aimed at. Aiming at the step alone just moved the
+// misses to the other side, 0 judged either way. So this selects a step the
+// list marks as violating, and once standing on one, opens a panel if none is
+// up. It opens the AFTER panel's, because the before panel's screenshot is what
+// screenshotShowsTheSelectedStep reads and covering that up trades one
+// property's evidence for another's.
+const violatingRows = extract("violatingRows", (s) =>
+  s.ax.findAll({ "data-testid": "step-row" }).filter((row) => dataOf(row, "violations") === "true"),
+);
+const afterPropertiesTabs = extract("afterPropertiesTabs", (s) =>
+  s.ax
+    .findAll([{ "data-testid": "state-after" }, { "data-testid": "tab" }])
+    .filter((tab) => dataOf(tab, "tabId") === "properties"),
+);
+
+const showAViolatingStepWithItsPanel = actions(() => {
+  const rows = violatingRows.current;
+  if (!rows.some((row) => dataOf(row, "active") === "true")) {
+    return rows.length === 0 ? [] : [Tap({ on: from(rows).generate() })];
+  }
+  if (violationPanelCounts.current.length > 0) return [];
+  const tabs = afterPropertiesTabs.current;
+  return tabs.length === 0 ? [] : [Tap({ on: from(tabs).generate() })];
+});
+
 // defaultActions carries the rest: the jump-to-violation button, the theme
 // toggle, the link back to the run list, and the scrolling.
 export const actionsRoot = weighted(
   [30, selectAStep],
   [20, navigateByKeyboard],
   [25, switchATab],
+  [20, showAViolatingStepWithItsPanel],
   [25, defaultActions],
 );

replay-ui/src/components/Tabs.css

@@ -6,8 +6,15 @@
   font-family: var(--font-mono);
 }
 
+/* Wrapping is what keeps the last tabs reachable. In a narrow column the five
+   tabs are wider than the panel, and the overflow scrolls .detail-panel-body,
+   which carries that tab's own panel out of the column with it. In a 756px
+   viewport (what a headless run gets) Properties and Violations then sit under
+   the neighbouring panel, where neither a person nor the fuzzer can click
+   them. */
 .tabs-header {
   display: flex;
+  flex-wrap: wrap;
   gap: 0;
   border-bottom: 1px solid var(--border);
   flex: 0 0 auto;