test(spec): guard the step unit on the authoring surface

Claude-Session: https://claude.ai/code/session_01A5KmftdEJ49A9z5mF5ESrX

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);
 }

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;
 }
 

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);