fix(runner): a read the driver cannot make is recorded, not counted as passed

collectLogs, captureMetrics and driverIsAndroid now separate an unsupported
read from a failed one: the first is not warned as a device fault and lands on
Summary.UnsupportedReads, which RenderSummary prints. Without it a green iOS run
was indistinguishable from a run over an app that logged nothing.

internal/runner/runner.go

@@ -79,6 +79,11 @@ type Summary struct {
 	// A run at zero never touched the app, whatever its step count says, so its
 	// empty violation list is the reading of an instrument that measured nothing.
 	DispatchedActions int
+	// UnsupportedReads names the device reads the driver could not perform at
+	// all, deduped. A property over a channel the driver never opened holds on
+	// every step and reports as a property that passed, so a run whose logs
+	// were never read has to say the logs were never read.
+	UnsupportedReads []string
 	// GeneratorActions counts the dispatched actions the generator chose. The
 	// spec's setup drives the app into its starting position before the
 	// generator is consulted, so a run at zero here explored nothing however
@@ -132,7 +137,11 @@ 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)
+	unsupportedReads := map[string]bool{}
+	rereadHierarchy, healthRead := driverIsAndroid(ctx, options, logger)
+	if !healthRead {
+		noteUnsupportedRead(unsupportedReads, unsupportedReadHealth, logger)
+	}
 
 	summary := Summary{StartTime: time.Now()}
 	deadline := summary.StartTime.Add(options.Duration)
@@ -181,6 +190,7 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 		var screenshotPNG []byte
 		var metrics *trace.Metrics
 		var logs []verifier.LogEntry
+		var logsRead, metricsRead bool
 
 		// gctx is bound to the errgroup so a returned error (or outer
 		// cancellation) propagates to every sibling read rather than leaving
@@ -198,18 +208,24 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			return nil
 		})
 		g.Go(func() error {
-			metrics = captureMetrics(gctx, options, logger, si)
+			metrics, metricsRead = captureMetrics(gctx, options, logger, si)
 			return nil
 		})
 		logSince := lastLogTime
 		g.Go(func() error {
-			logs = collectLogs(gctx, options.Driver, logger, si, logSince)
+			logs, logsRead = collectLogs(gctx, options.Driver, logger, si, logSince)
 			return nil
 		})
 		// All goroutines write to local variables and return nil, so the Wait
 		// error is always nil; ignored intentionally.
 		_ = g.Wait()
 		observeCancel()
+		if !logsRead {
+			noteUnsupportedRead(unsupportedReads, unsupportedReadLogs, logger)
+		}
+		if !metricsRead {
+			noteUnsupportedRead(unsupportedReads, unsupportedReadMetrics, logger)
+		}
 
 		navigations := collectNavigations(ctx, navigationReporter, logger, stepIndex)
 
@@ -565,13 +581,29 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 	}
 
 	summary.UnsupportedVerbs = options.Verifier.UnsupportedVerbs()
+	if len(unsupportedReads) > 0 {
+		summary.UnsupportedReads = slices.Sorted(maps.Keys(unsupportedReads))
+	}
 	summary.EndTime = time.Now()
 	return summary, nil
 }
 
+// noteUnsupportedRead records a device read the driver cannot perform and warns
+// the first time it is seen, so the live log says once what the summary says at
+// the end instead of repeating it on every step of the run.
+func noteUnsupportedRead(reads map[string]bool, name string, logger *slog.Logger) {
+	if reads[name] {
+		return
+	}
+	reads[name] = true
+	logger.Warn("the driver cannot perform this read; anything reading it holds vacuously",
+		"read", name)
+}
+
 // RenderSummary writes the human-facing run summary: step count, each violation
-// record, and any unsupported verbs. The wall-clock duration is excluded so the
+// record, the device reads the driver could not make, and any unsupported
-// output is deterministic and snapshot-testable; the CLI prints it separately.
+// verbs. The wall-clock duration is excluded so the output is deterministic
+// and snapshot-testable; the CLI prints it separately.
 func RenderSummary(w io.Writer, summary Summary, platform string) {
 	fmt.Fprintf(w, "\nrun complete: %d steps, %d driven by the generator\n",
 		summary.Steps, summary.GeneratorActions)
@@ -602,6 +634,10 @@ func RenderSummary(w io.Writer, summary Summary, platform string) {
 		fmt.Fprintf(w, "%d step(s) judged by nothing: the screen was still moving when it was read\n",
 			summary.SkippedVerification)
 	}
+	if len(summary.UnsupportedReads) > 0 {
+		fmt.Fprintf(w, "never read on %s: %s; every property over them held vacuously\n",
+			platform, strings.Join(summary.UnsupportedReads, ", "))
+	}
 	if len(summary.UnsupportedVerbs) > 0 {
 		fmt.Fprintf(w, "unsupported on %s: %s\n",
 			platform, strings.Join(summary.UnsupportedVerbs, ", "))
@@ -1068,19 +1104,23 @@ func applyAction(ctx context.Context, drv driver.DeviceDriver, action verifier.A
 // 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.
+// app having logged nothing. The second result is false when the driver has no
+// log source at all, which is that same vacuity for the whole run.
 func collectLogs(
 	ctx context.Context,
 	drv driver.DeviceDriver,
 	logger *slog.Logger,
 	step int,
 	since time.Time,
-) []verifier.LogEntry {
+) ([]verifier.LogEntry, bool) {
 	entries, err := drv.RecentLogs(ctx, since, "E")
+	if errors.Is(err, driver.ErrNotSupported) {
+		return nil, false
+	}
 	if err != nil {
 		logger.Warn("log fetch failed; log properties hold vacuously this step",
 			"step", step, "err", err)
-		return nil
+		return nil, true
 	}
 	result := make([]verifier.LogEntry, 0, len(entries))
 	for _, entry := range entries {
@@ -1091,7 +1131,7 @@ func collectLogs(
 			Message:    entry.Message,
 		})
 	}
-	return result
+	return result, true
 }
 
 // collectExceptions reads the app's captured uncaught errors. Like log
@@ -1575,13 +1615,20 @@ func structuralShape(tree *hierarchy.Tree) string {
 // 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 {
+//
+// healthRead is false when the driver runs no readiness check at all, which is
+// not a device fault: the run records a check it never made rather than a
+// device it never confirmed was ready.
+func driverIsAndroid(ctx context.Context, options Options, logger *slog.Logger) (isAndroid, healthRead bool) {
 	health, err := options.Driver.Health(ctx)
+	if errors.Is(err, driver.ErrNotSupported) {
+		return false, false
+	}
 	if err != nil {
 		logger.Warn("health read failed; not rereading the hierarchy", "err", err)
-		return false
+		return false, true
 	}
-	return health.Platform == "android"
+	return health.Platform == "android", true
 }
 
 func traceActionFor(action verifier.Action, tree *hierarchy.Tree) *trace.Action {
@@ -1645,23 +1692,30 @@ func stampSelectorTarget(traceAction *trace.Action, action verifier.Action, tree
 	}
 }
 
-func captureMetrics(ctx context.Context, options Options, logger *slog.Logger, stepIndex int) *trace.Metrics {
+// captureMetrics samples the app's CPU and memory for this step's trace line.
+// The second result is false when the driver cannot sample at all, so a trace
+// with no metrics on any step says the sampler was never there rather than
+// reading as an app that used nothing.
+func captureMetrics(ctx context.Context, options Options, logger *slog.Logger, stepIndex int) (*trace.Metrics, bool) {
 	if options.BundleID == "" {
-		return nil
+		return nil, true
 	}
 	sample, err := options.Driver.Metrics(ctx, options.BundleID)
+	if errors.Is(err, driver.ErrNotSupported) {
+		return nil, false
+	}
 	if err != nil {
 		logger.Warn("metrics capture failed", "step", stepIndex, "err", err)
-		return nil
+		return nil, true
 	}
 	if sample.CPUPercent == 0 && sample.HeapBytes == 0 && sample.TotalMemoryBytes == 0 {
-		return nil
+		return nil, true
 	}
 	return &trace.Metrics{
 		CPUPercent:       sample.CPUPercent,
 		HeapBytes:        sample.HeapBytes,
 		TotalMemoryBytes: sample.TotalMemoryBytes,
-	}
+	}, true
 }
 
 // violationRecords groups newly-violated properties by the step their witness
@@ -1753,6 +1807,16 @@ func encodeResiduals(residuals map[string]ltl.Formula) (map[string]json.RawMessa
 	return encoded, firstErr
 }
 
+// The device reads a driver can be missing. Each names an evidence source the
+// run would otherwise report as read and empty: no log lines, no samples, a
+// device confirmed ready. They reach the summary so a green run that never
+// opened one of them cannot read as a run that opened it and found nothing.
+const (
+	unsupportedReadLogs    = "device_logs"
+	unsupportedReadMetrics = "app_metrics"
+	unsupportedReadHealth  = "device_health"
+)
+
 // actionSkipReason names why a chosen action was never dispatched. It is
 // recorded on the step so a count of executed actions is not inflated by the
 // next_action of a step that acted on nothing. Empty means the action ran.

internal/runner/runner_test.go

@@ -67,6 +67,17 @@ globalThis.properties = {
 globalThis.actions = actions(() => []);
 `
 
+// logErrorSpec's only property reads state.logs, the channel a driver without a
+// log source never opens.
+const logErrorSpec = `
+import { actions, always, extract } from "@sanderling/spec";
+const errorLines = extract(state => state.logs.filter(entry => entry.level === "E").length);
+globalThis.properties = {
+  noLoggedErrors: always(() => errorLines.current === 0),
+};
+globalThis.actions = actions(() => []);
+`
+
 const violationSpec = `
 import { actions, always } from "@sanderling/spec";
 globalThis.properties = {
@@ -348,6 +359,83 @@ func TestRenderSummary_CountsTheStepsNothingJudged(t *testing.T) {
 	}
 }
 
+// A driver that cannot read a channel is not a device that had nothing to
+// report on it. The property over state.logs holds here because nobody ever
+// looked, so the run has to say which reads it never made: without the line a
+// green iOS summary is indistinguishable from one over a silent app.
+func TestRunner_ReadsTheDriverCannotMakeAreNotPassedChecks(t *testing.T) {
+	state := newHarnessWithSpec(t, logErrorSpec)
+	state.mock.Failures[mockdriver.ActionRecentLogs] = driver.ErrNotSupported
+	state.mock.Failures[mockdriver.ActionMetrics] = driver.ErrNotSupported
+	state.mock.Failures[mockdriver.ActionHealth] = driver.ErrNotSupported
+
+	ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second)
+	defer cancel()
+	summary, err := Run(ctx, Options{
+		Duration:    5 * time.Second,
+		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    3,
+		BundleID:    "com.fixture",
+		Driver:      state.mock,
+		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 len(summary.Violations) != 0 {
+		t.Fatalf("the log property fired; this test needs it holding on the empty channel: %v",
+			summary.Violations)
+	}
+	if summary.FailedObservations != 0 {
+		t.Errorf("FailedObservations = %d: a read the driver does not have is not a device fault",
+			summary.FailedObservations)
+	}
+	want := []string{unsupportedReadMetrics, unsupportedReadHealth, unsupportedReadLogs}
+	slices.Sort(want)
+	if !slices.Equal(summary.UnsupportedReads, want) {
+		t.Errorf("UnsupportedReads = %v, want %v", summary.UnsupportedReads, want)
+	}
+
+	var rendered bytes.Buffer
+	RenderSummary(&rendered, summary, "ios")
+	if !strings.Contains(rendered.String(), "never read on ios: "+strings.Join(want, ", ")) {
+		t.Errorf("the run reports as a clean one:\n%s", rendered.String())
+	}
+}
+
+// The inverse, so the line cannot start appearing on every run: a driver that
+// answers all three reports none missing and prints nothing.
+func TestRunner_ADriverThatAnswersEveryReadReportsNoneMissing(t *testing.T) {
+	state := newHarness(t)
+
+	ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second)
+	defer cancel()
+	summary, err := Run(ctx, Options{
+		Duration:    5 * time.Second,
+		IdleTimeout: 20 * time.Millisecond,
+		MaxSteps:    2,
+		BundleID:    "com.fixture",
+		Driver:      state.mock,
+		Verifier:    state.verifier,
+		TraceWriter: state.writer,
+	})
+	if err != nil {
+		t.Fatalf("Run: %v", err)
+	}
+	if len(summary.UnsupportedReads) != 0 {
+		t.Errorf("UnsupportedReads = %v, want none", summary.UnsupportedReads)
+	}
+	var rendered bytes.Buffer
+	RenderSummary(&rendered, summary, "android")
+	if strings.Contains(rendered.String(), "never read on") {
+		t.Errorf("a run that made every read must not print the line:\n%s", rendered.String())
+	}
+}
+
 func TestRunner_ViolationSurfacesInSummary(t *testing.T) {
 	state := newHarnessWithSpec(t, violationSpec)