refactor(runner): emit onset-only violations to trace and summary

Switch the per-step violation list from the sticky verdict map to the
verifier's onset set. Each property now appears exactly once across a
run: at the step it first violates, not on every subsequent step where
the residual stays false. Removes the dead violationNames helper.

internal/runner/runner.go

@@ -165,8 +165,8 @@ func Run(ctx context.Context, options Options) (Summary, error) {
 			screen = tree.Elements[0].Screen
 		}
 		logger.Info("step", "index", stepIndex, "screen", screen, "nodes", treeSize)
-		verdicts := options.Verifier.EvaluateProperties()
-		violations := violationNames(verdicts)
+		options.Verifier.EvaluateProperties()
+		violations := options.Verifier.NewlyViolatedProperties()
 		for _, name := range violations {
 			if predicateErr := options.Verifier.PredicateError(name); predicateErr != nil {
 				logger.Warn("predicate error", "step", stepIndex, "property", name, "err", predicateErr)
@@ -266,16 +266,6 @@ func validate(options Options) error {
 	return nil
 }
 
-func violationNames(verdicts map[string]ltl.Verdict) []string {
-	var names []string
-	for name, verdict := range verdicts {
-		if verdict == ltl.VerdictViolated {
-			names = append(names, name)
-		}
-	}
-	return names
-}
-
 // 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