fix(runner): a bounded hold puts the swallow back one step later

the hold carries one action; letting the runner act again while the verifier
is still skipped overwrites it, so the carried action reaches no spec. hold
for as long as the verifier is skipped, and settle on a held step so the
reread pair is not tighter than the window the detector was measured over.

internal/runner/composition_reread_test.go

@@ -133,22 +133,25 @@ func TestRunner_AStepWhoseTreeChangedBetweenReadsIsNotVerified(t *testing.T) {
 	})
 }
 
-// submitsOnTapDriver commits a transaction on every tap, shows the running
+// submitsOnTapDriver commits commitsPerTap transactions on every tap, shows the
-// total in the tree, and grows a row under the hierarchy read that follows the
+// running total in the tree, and grows a row under the hierarchy read that
-// paired Snapshot: on one chosen step, or on every one of them.
+// 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
-	composingRead int64
+	commitsPerTap    int64
-	everyRead     bool
+	composingRead    int64
-	reads         atomic.Int64
+	composingThrough int64
-	committed     atomic.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)
+	d.committed.Add(d.commitsPerTap)
 	return nil
 }
 
@@ -157,7 +160,10 @@ func (d *submitsOnTapDriver) Snapshot(context.Context) (string, driver.Image, er
 }
 
 func (d *submitsOnTapDriver) Hierarchy(context.Context) (string, error) {
-	if read := d.reads.Add(1); d.everyRead || read == d.composingRead {
+	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
@@ -188,7 +194,11 @@ func TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt(t *testing.T) {
 	run := func(t *testing.T, composingRead int64) (Summary, int64) {
 		t.Helper()
 		state := newHarnessWithSpec(t, spec)
-		device := &submitsOnTapDriver{Driver: state.mock, composingRead: composingRead}
+		device := &submitsOnTapDriver{
+			Driver:        state.mock,
+			commitsPerTap: 1,
+			composingRead: composingRead,
+		}
 
 		ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
 		defer cancel()
@@ -243,13 +253,92 @@ func TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt(t *testing.T) {
 	})
 }
 
-// Holding an action back is bounded. A screen that changes shape under every
+// One skipped step is held; a run of them has to be held too. A bound that lets
-// pair of reads (a live list, a spinner mounting and unmounting) would
+// the runner act again while the verifier is still being skipped puts back the
-// otherwise take the whole run: nothing verified, nothing tapped, and a green
+// exact swallow the hold exists to prevent, only later: the action drawn on the
-// summary at the end of it.
+// step past the bound overwrites the one the hold was carrying, and the carried
-func TestRunner_AScreenThatNeverSettlesDoesNotStallTheRun(t *testing.T) {
+// 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, everyRead: true}
+	device := &submitsOnTapDriver{Driver: state.mock, commitsPerTap: 1, everyRead: true}
 
 	ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
 	defer cancel()
@@ -264,13 +353,17 @@ func TestRunner_AScreenThatNeverSettlesDoesNotStallTheRun(t *testing.T) {
 	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 device.committed.Load() == 0 {
+	if got := device.committed.Load(); got != 0 {
-		t.Error("the fuzzer never acted across 5 steps; a screen that keeps moving must " +
+		t.Errorf("the fuzzer applied %d action(s) onto a screen no property would judge; "+
-			"cost the run a step or two, not all of them")
+			"each one is an action no spec will ever be told about", got)
 	}
 }
 

internal/runner/runner.go

@@ -100,7 +100,6 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 	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) {
@@ -287,16 +286,16 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 		// 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
+		// Unbounded, because lastAction holds exactly one action: any bound that
-		// run: past the bound the runner acts anyway, which is where it was
+		// let the runner act again while the verifier was still being skipped
-		// before this held anything back.
+		// would overwrite the action the hold was carrying, and that is the same
-		held := skippedVerification && heldSteps < maxHeldSteps
+		// 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 {
-			heldSteps++
 			logger.Warn("screen still moving; holding this step's action back",
-				"step", stepIndex, "held", heldSteps)
+				"step", stepIndex)
-		} else {
-			heldSteps = 0
 		}
 
 		var nextAction verifier.Action
@@ -401,7 +400,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.
+		applied := nextErr == nil && !applySkipped &&
+			nextAction.Kind != verifier.ActionKindWait
+		if held || applied {
 			idleCtx, idleCancel := context.WithTimeout(ctx, options.IdleTimeout)
 			idleErr := options.Driver.WaitForIdle(idleCtx, options.IdleTimeout)
 			if idleErr != nil && idleCtx.Err() == nil {
@@ -1316,14 +1324,6 @@ 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