From 349a0644acf0d13806451ce6ed2502bb63b4357f Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Fri, 14 Aug 2026 17:50:37 +0530
Subject: [PATCH] test(spec): guard the step unit on the authoring surface

Claude-Session: https://claude.ai/code/session_01A5KmftdEJ49A9z5mF5ESrX
---
 pkg/spec/src/ltl.ts       | 4 +++-
 pkg/spec/src/types.ts     | 4 ++++
 pkg/spec/test/api.test.ts | 6 ++++++
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/pkg/spec/src/ltl.ts b/pkg/spec/src/ltl.ts
index 3ef5b63..aa5f4e9 100644
--- a/pkg/spec/src/ltl.ts
+++ b/pkg/spec/src/ltl.ts
@@ -14,7 +14,9 @@ export function next(predicate: () => boolean): Formula {
 
 // An unbounded `eventually` never forces a violation within a finite run.
 // Prefer `.within(n, unit)` when you want the verifier to fail a property
-// that stalls.
+// that stalls. `"steps"` counts observed steps rather than wall-clock time,
+// which is what keeps the window the same size across runs of different
+// speeds.
 export function eventually(predicate: () => boolean): EventuallyFormula {
   return globalThis.__sanderling__.eventually(predicate);
 }
diff --git a/pkg/spec/src/types.ts b/pkg/spec/src/types.ts
index 66394a6..32677d0 100644
--- a/pkg/spec/src/types.ts
+++ b/pkg/spec/src/types.ts
@@ -203,6 +203,10 @@ export interface Formula {
 }
 
 export interface EventuallyFormula extends Formula {
+  // `"milliseconds"` and `"seconds"` bound the window in wall-clock time, which
+  // is what a user-perceived deadline means. `"steps"` bounds it in observed
+  // steps, so the same window costs the same regardless of how long each step
+  // took: use it for anything compared across runs of different speeds.
   within(amount: number, unit: "milliseconds" | "seconds" | "steps"): Formula;
 }
 
diff --git a/pkg/spec/test/api.test.ts b/pkg/spec/test/api.test.ts
index 60647fd..ce9590b 100644
--- a/pkg/spec/test/api.test.ts
+++ b/pkg/spec/test/api.test.ts
@@ -203,6 +203,12 @@ test("eventually().within forwards unit and amount", () => {
   assert.deepEqual(runtime.withinCalls[0], { amount: 3, unit: "seconds" });
 });
 
+test("eventually().within forwards the step unit unchanged", () => {
+  const runtime = installFakeRuntime();
+  eventually(() => true).within(1915, "steps");
+  assert.deepEqual(runtime.withinCalls[0], { amount: 1915, unit: "steps" });
+});
+
 test("formula chaining exposes implies/or/and/not", () => {
   const runtime = installFakeRuntime();
   const a = now(() => true);