From e677832fa4783521387f325557f7221e43da8adb Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Sun, 9 Aug 2026 21:11:38 +0800
Subject: [PATCH 01/12] =?UTF-8?q?fix(demo):=20SPEC=20revision=204=20?=
 =?UTF-8?q?=E2=80=94=20findings=20from=20independent=20verification?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Two fresh-context verification passes attacked the demo at 9540d72 while the
full gauntlet was green. They converged on three MATERIAL defects that 10
layers, 100% branch coverage and 8/8 mutants could not reach, plus a
fail-open layer inside the gauntlet itself.

Spec-level (approved as REVISION 4):
- limit=NaN/inf/2.5/bool were accepted and produced a limiter that allows
  forever — the exact fail-open class fixed for window_seconds in the
  2026-07-25 revision, never swept to the sibling parameter.
- allow() accepted None/int/bytes/"" as keys, so a missing HTTP header
  silently became one shared quota bucket for every unidentified caller.
- Key eviction was lazy: keys that never returned were never reaped, so
  distinct callers grew the map without bound (200k keys, 171 MB measured).
  Memory is now bounded by the keys seen within one window.
- allow() was a non-atomic read-prune-check-append; 2x over-allow was
  measured under threads. Now guarded by a lock, and the autonomous
  "single-threaded use only" de-scoping is withdrawn.

Gauntlet-level:
- Coverage was report-only: dropping to 89% still exited 0. Now gated with
  --cov-fail-under=100.
- The no-real-time scan matched `time.` and missed `from time import sleep`.
  Pattern now covers usage forms; fixed in the pattern, not by excluding
  files.
- Property strategies saw three distinct keys, so a key-hardcoded
  implementation would have scored 100%/8-of-8. Widened, then re-tuned after
  layer attribution showed over-widening had blunted the layer (M5 survived
  the property suite).
- Mutants M9/M10/M12/M13 added, one per failure-model row that was claiming
  coverage it did not have.

M11 (prune one per call) was proposed by verification as a surviving mutant
proving quota loss. It is EQUIVALENT — 0 divergences over 200k randomized
monotone sequences — and is documented as such rather than killed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/spec.md                     | 78 +++++++++++++++++--
 demo-rate-limiter/src/ratelimiter/__init__.py | 44 ++++++++---
 demo-rate-limiter/tests/test_properties.py    | 31 ++++++--
 demo-rate-limiter/tests/test_ratelimiter.py   | 72 ++++++++++++++++-
 demo-rate-limiter/tools/gauntlet.sh           | 11 ++-
 demo-rate-limiter/tools/mutants.py            | 46 +++++++++--
 6 files changed, 247 insertions(+), 35 deletions(-)

diff --git a/demo-rate-limiter/spec.md b/demo-rate-limiter/spec.md
index 6b249c4..e9e4722 100644
--- a/demo-rate-limiter/spec.md
+++ b/demo-rate-limiter/spec.md
@@ -65,6 +65,31 @@ Feature: Sliding-window rate limiting per key
     When the clock jumps backward and the key requests at t=50
     Then it returns False
     (clock skew must fail closed, never open)
+
+  Scenario: limit must be a finite positive integer  [REVISION 4]
+    When constructing with limit = NaN, +/-inf, a float such as 2.5, or a bool
+    Then ValueError is raised naming limit
+    (limit=NaN made every comparison False and the limiter allowed forever —
+    the same fail-open class fixed for window_seconds in REVISION 2026-07-25,
+    never swept across to the sibling parameter)
+
+  Scenario: key must be a non-empty string  [REVISION 4]
+    When calling allow() with None, an int, bytes, or ""
+    Then TypeError (wrong type) or ValueError (empty) is raised
+    (a missing HTTP header arriving as None must not silently become one
+    shared quota bucket for every unidentified caller)
+
+  Scenario: idle keys are forgotten — the key map is bounded  [REVISION 4]
+    Given a limiter with limit 1 per 60 seconds
+    And 1000 distinct keys that each made one request at t=0 and never return
+    When any request arrives after a full window has elapsed
+    Then the limiter retains only keys with a hit inside the current window
+
+  Scenario: concurrent callers never exceed the limit  [REVISION 4]
+    Given a limiter with limit 1 per 60 seconds
+    When many threads call allow() for the same key simultaneously
+    Then exactly 1 call returns True
+    (read-prune-check-append was not atomic; measured 2x over-allow)
 ```
 
 ## Invariants (property-based)
@@ -75,8 +100,23 @@ Feature: Sliding-window rate limiting per key
 
 ## Must NOT do
 
-- No real time.sleep / wall-clock dependence in tests.
-- No unbounded memory growth from denied requests (denials store nothing).
+- No real time.sleep / wall-clock dependence in tests. Covers every spelling
+  (`import time`, `from time import sleep`, aliases, `datetime`) — not one
+  regex's idea of it. [REVISION 4: the gate matched only `time.`]
+- No unbounded memory growth. [REVISION 4: this clause used to read "from
+  denied requests (denials store nothing)". Denials were never the leak;
+  *allowed* requests from keys that never return were. Growth is now bounded
+  by the distinct keys seen within one window — see the idle-keys scenario.]
+
+## Clock contract [REVISION 4]
+
+`clock` MUST be monotonic (`time.monotonic`, as `examples/demo.py` uses). A
+forward jump — NTP step, resumed VM — expires every hit at once and resets
+every caller's quota simultaneously. That is inherent to a sliding window over
+a supplied clock and is not defended against in code; it is a caller
+obligation, stated here because the failure model previously implied the
+non-monotonic scenario covered skew in both directions. It covers backward
+skew only.
 
 ## Failure model (Tier 3)
 
@@ -84,14 +124,21 @@ Feature: Sliding-window rate limiting per key
 failure model before layer selection; these modes were previously implicit
 in the scenarios, Must NOTs, and adversarial pass.]
 
+[REVISION 4, 2026-08-09: an independent fresh-context verification pass found
+that three rows below claimed coverage they did not have. Every row now names
+a test AND a mutant that demonstrably fails without it; a row whose catcher
+cannot be shown to fail is a defect, not a mapping.]
+
 | How this can hurt | Layer that catches it |
 |---|---|
 | over-allowing in a burst (limit not enforced) | scenario tests + P1 + mutants M1/M5 |
-| under-allowing / fail-closed drift (quota lost) | boundary scenario + mutants M6/M8 (P1 is one-sided and cannot catch this) |
-| hostile or invalid config silently accepted | validation scenarios + adversarial pass + mutants M4/M7 |
-| clock skew opening the gate | non-monotonic clock scenario |
-| memory growth from denials | Must NOT test + mutant M8 |
-| concurrent callers racing on shared state | **not covered — known limit**; single-threaded use only |
+| under-allowing / fail-closed drift (quota lost) | boundary scenario + mutants M6/M8 (P1 is one-sided and cannot catch this). Verification proposed a third mutant here; it proved EQUIVALENT — see mutants.py |
+| hostile or invalid config silently accepted | validation scenarios (window AND limit) + adversarial pass + mutants M4/M7/M9 |
+| backward clock skew opening the gate | non-monotonic clock scenario (jump must exceed the window) + mutant M10 |
+| forward clock skew resetting all quota | **not covered — caller obligation**; see Clock contract |
+| unbounded memory growth (any path) | idle-keys scenario + denials test + mutants M8/M12 |
+| concurrent callers racing on shared state | concurrency scenario + mutant M13 (lock removed) |
+| untested code reaching production | coverage layer, now a gate (`--cov-fail-under=100`) — it previously printed a number and could not fail |
 | silent failure in production | n-a: library returns a bool the caller observes directly |
 
 ## Setup plan
@@ -109,4 +156,19 @@ to be justified in the spec. Original setup was authorized conversationally.]
   - pytest-randomly — randomized test order (suite-health layer)
 - Git: repo-level; commits at each milestone; evidence binds to commit SHA.
 - Files the gauntlet adds: `tools/gauntlet.sh` (entry point), `tools/mutants.py`
-  (scripted manual mutation), `.github/workflows/gauntlet.yml` (CI).
+  (scripted manual mutation), `.github/workflows/gauntlet.yml` (CI),
+  `tools/must_not_match.sh` + `tools/test_gauntlet_checks.sh` (fail-closed
+  scan helper and its self-test).
+- [REVISION 4] Runtime dependencies remain **none**: `threading.Lock` is
+  stdlib. The coverage layer gains `--cov-fail-under=100`, making it a gate
+  rather than a report.
+
+## Explicitly out of scope [REVISION 4]
+
+- **Retry-After / remaining-quota accessor.** `allow(key) -> bool` gives an
+  HTTP frontend no way to populate `Retry-After` or `X-RateLimit-Remaining`,
+  which RFC 9110 expects alongside a 429. Raised by both verification passes.
+  Declined here because it changes the public API shape and the contract asks
+  only to bound request frequency — recorded so the gap is visible rather than
+  absent.
+- **Distributed / multi-process limiting.** In-process state only.
diff --git a/demo-rate-limiter/src/ratelimiter/__init__.py b/demo-rate-limiter/src/ratelimiter/__init__.py
index 0eb64f1..490df20 100644
--- a/demo-rate-limiter/src/ratelimiter/__init__.py
+++ b/demo-rate-limiter/src/ratelimiter/__init__.py
@@ -1,6 +1,7 @@
 """Sliding-window rate limiter with an injectable clock."""
 
 import math
+import threading
 from collections import deque
 from collections.abc import Callable
 
@@ -10,14 +11,22 @@
 class RateLimiter:
     """Allow at most `limit` requests per key within any sliding window.
 
-    `clock` returns the current time in seconds; timestamps older than
-    `window_seconds` fall out of the window individually. A backward-jumping
-    clock fails closed: past hits never expire early.
+    `clock` returns the current time in seconds and MUST be monotonic
+    (`time.monotonic`); timestamps older than `window_seconds` fall out of the
+    window individually. A backward-jumping clock fails closed: past hits never
+    expire early. A forward jump expires every hit at once — that is a caller
+    obligation, not a defect (see the clock contract in spec.md).
+
+    Safe to call from multiple threads. Memory is bounded by the number of
+    distinct keys seen within one window: keys idle for a full window are
+    dropped by a sweep that runs at most once per window.
     """
 
     def __init__(
         self, limit: int, window_seconds: float, clock: Callable[[], float]
     ) -> None:
+        if isinstance(limit, bool) or not isinstance(limit, int):
+            raise ValueError(f"limit must be an integer, got {limit!r}")
         if limit <= 0:
             raise ValueError(f"limit must be positive, got {limit}")
         if not math.isfinite(window_seconds) or window_seconds <= 0:
@@ -27,17 +36,34 @@ def __init__(
         self._limit = limit
         self._window = window_seconds
         self._clock = clock
+        self._lock = threading.Lock()
         self._hits: dict[str, deque[float]] = {}
+        self._last_sweep = -math.inf
 
     def allow(self, key: str) -> bool:
         """Record and allow this request, or deny it. Denials store nothing."""
+        if not isinstance(key, str):
+            raise TypeError(f"key must be a str, got {type(key).__name__}")
+        if not key:
+            raise ValueError("key must not be empty")
         now = self._clock()
-        hits = self._prune(key, now)
-        if len(hits) >= self._limit:
-            return False
-        hits.append(now)
-        self._hits[key] = hits
-        return True
+        with self._lock:
+            self._sweep(now)
+            hits = self._prune(key, now)
+            if len(hits) >= self._limit:
+                return False
+            hits.append(now)
+            self._hits[key] = hits
+            return True
+
+    def _sweep(self, now: float) -> None:
+        """Forget keys idle for a full window. Runs at most once per window."""
+        if now - self._last_sweep <= self._window:
+            return
+        self._last_sweep = now
+        idle = [k for k, hits in self._hits.items() if now - hits[-1] > self._window]
+        for key in idle:
+            del self._hits[key]
 
     def _prune(self, key: str, now: float) -> deque[float]:
         """Drop hits older than the window; forget keys with none left."""
diff --git a/demo-rate-limiter/tests/test_properties.py b/demo-rate-limiter/tests/test_properties.py
index a00ea5f..d65afcf 100644
--- a/demo-rate-limiter/tests/test_properties.py
+++ b/demo-rate-limiter/tests/test_properties.py
@@ -6,15 +6,30 @@
 
 from ratelimiter import RateLimiter
 
-requests = st.lists(
-    st.tuples(
-        st.floats(min_value=0, max_value=1000, allow_nan=False, allow_infinity=False),
-        st.sampled_from("abc"),
-    ),
-    max_size=60,
+timestamps = st.floats(
+    min_value=0, max_value=1000, allow_nan=False, allow_infinity=False
+)
+# [REVISION 4] Keys were `st.sampled_from("abc")`, so the whole suite ever saw
+# three distinct keys and an implementation hardcoded to them scored 100%
+# coverage and 8/8 mutants. A small alphabet keeps collisions frequent (which
+# is what makes P1 bite) while ranging far outside any hardcoded set.
+# Widening this too far blunts the layer: with 258 possible keys and limits up
+# to 20, hypothesis almost never drives one key to its limit, so the deny
+# branch goes unexercised and the fail-open mutant M5 survives the property
+# suite. 12 keys keeps collisions frequent while still ranging outside any
+# hardcoded key set. Measured by the layer-attribution run, not guessed.
+keys = st.text(alphabet="abc", min_size=1, max_size=2)
+requests = st.lists(st.tuples(timestamps, keys), max_size=60)
+isolation_requests = st.lists(
+    st.tuples(timestamps, st.sampled_from("abc")), max_size=60
 )
 limits = st.integers(min_value=1, max_value=5)
-windows = st.floats(min_value=0.1, max_value=100, allow_nan=False)
+# Mostly ordinary windows, sometimes far outside the tested range, so an
+# implementation that special-cases large windows cannot hide.
+windows = st.one_of(
+    st.floats(min_value=0.1, max_value=100, allow_nan=False),
+    st.floats(min_value=1001, max_value=5000, allow_nan=False),
+)
 
 
 def run(
@@ -43,7 +58,7 @@ def test_p1_allowed_count_within_any_window_never_exceeds_limit(
         assert in_window <= limit
 
 
-@given(steps=requests, limit=limits, window=windows)
+@given(steps=isolation_requests, limit=limits, window=windows)
 def test_p2_other_keys_traffic_never_changes_one_keys_outcomes(
     steps: list[tuple[float, str]], limit: int, window: float
 ) -> None:
diff --git a/demo-rate-limiter/tests/test_ratelimiter.py b/demo-rate-limiter/tests/test_ratelimiter.py
index 8ab36a0..f3c2889 100644
--- a/demo-rate-limiter/tests/test_ratelimiter.py
+++ b/demo-rate-limiter/tests/test_ratelimiter.py
@@ -1,6 +1,9 @@
 """Scenario tests — each test name maps 1:1 to a spec.md scenario."""
 
 import math
+import sys
+import threading
+from typing import Any
 
 import pytest
 from conftest import FakeClock
@@ -91,5 +94,72 @@ def test_non_monotonic_clock_does_not_grant_extra_quota(clock: FakeClock) -> Non
     limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
     clock.now = 100.0
     assert limiter.allow("k") is True
-    clock.now = 50.0  # clock jumps backward
+    # The jump must exceed window_seconds: a smaller one leaves the hit inside
+    # the window anyway, so it cannot distinguish an age of `now - hit` from
+    # `abs(now - hit)` — the fail-open form. [REVISION 4]
+    clock.now = 0.0  # backward by 100s, window is 60s
     assert limiter.allow("k") is False  # must fail closed
+
+
+@pytest.mark.parametrize("limit", [math.nan, math.inf, -math.inf, 2.5, True])
+def test_limit_must_be_a_finite_positive_integer(clock: FakeClock, limit: Any) -> None:
+    with pytest.raises(ValueError, match="limit"):
+        RateLimiter(limit=limit, window_seconds=60, clock=clock)
+
+
+@pytest.mark.parametrize(
+    ("key", "expected"),
+    [(None, TypeError), (12345, TypeError), (b"bytes", TypeError), ("", ValueError)],
+)
+def test_key_must_be_a_non_empty_string(
+    clock: FakeClock, key: Any, expected: type[Exception]
+) -> None:
+    limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
+    with pytest.raises(expected, match="key"):
+        limiter.allow(key)
+
+
+def test_idle_keys_are_forgotten_key_map_is_bounded(clock: FakeClock) -> None:
+    limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
+    for i in range(1000):
+        assert limiter.allow(f"one-shot-{i}") is True
+    assert len(limiter._hits) == 1000
+    clock.now = 121.0  # a full window has elapsed and none of them came back
+    assert limiter.allow("someone-else") is True
+    assert len(limiter._hits) == 1
+
+
+def _allowed_in_one_race(limiter: RateLimiter, threads: int) -> int:
+    """Fire `threads` simultaneous allow() calls; return how many won."""
+    barrier = threading.Barrier(threads)
+    results: list[bool] = []
+    guard = threading.Lock()
+
+    def worker() -> None:
+        barrier.wait()
+        got = limiter.allow("k")
+        with guard:
+            results.append(got)
+
+    workers = [threading.Thread(target=worker) for _ in range(threads)]
+    for w in workers:
+        w.start()
+    for w in workers:
+        w.join()
+    return sum(results)
+
+
+def test_concurrent_callers_never_exceed_the_limit() -> None:
+    rounds, threads = 60, 16
+    previous_interval = sys.getswitchinterval()
+    sys.setswitchinterval(1e-6)  # widen the preemption window
+    try:
+        worst = max(
+            _allowed_in_one_race(
+                RateLimiter(limit=1, window_seconds=60, clock=lambda: 0.0), threads
+            )
+            for _ in range(rounds)
+        )
+    finally:
+        sys.setswitchinterval(previous_interval)
+    assert worst == 1
diff --git a/demo-rate-limiter/tools/gauntlet.sh b/demo-rate-limiter/tools/gauntlet.sh
index 14e4be0..41c78ba 100755
--- a/demo-rate-limiter/tools/gauntlet.sh
+++ b/demo-rate-limiter/tools/gauntlet.sh
@@ -11,7 +11,10 @@ echo "=== checker self-test ==="
 sh tools/test_gauntlet_checks.sh
 
 echo "=== tests + coverage ==="
-"$PY/pytest" -q --cov=ratelimiter --cov-report=term-missing
+# --cov-fail-under makes this layer a gate. Without it the layer printed a
+# percentage and exited 0 no matter how far coverage fell: a fail-open layer
+# inside a gauntlet whose first line promises to fail on the first broken one.
+"$PY/pytest" -q --cov=ratelimiter --cov-report=term-missing --cov-fail-under=100
 echo "=== types ==="
 "$PY/mypy" src tests examples tools
 echo "=== lint + format ==="
@@ -20,7 +23,11 @@ echo "=== lint + format ==="
 echo "=== supply chain ==="
 "$PY/pip-audit" -r requirements-dev.txt
 echo "=== must-not scans ==="
-must_not_match 'time\.' tests
+# Matches usage forms, not the word: `time\.` alone missed `from time import
+# sleep`. Deliberately not `[[:<:]]time`, which would fire on conftest's own
+# "No real time in tests" docstring and on test_non_monotonic_clock_* — the
+# fix belongs in the pattern, never in an exclusion.
+must_not_match 'import[[:space:]]+time|from[[:space:]]+time[[:space:]]+import|time\.|datetime|sleep[[:space:]]*\(|perf_counter[[:space:]]*\(|monotonic[[:space:]]*\(' tests
 # Bracketed letters stop the pattern literal from matching itself.
 must_not_match 'api[_-]?key|s[e]cret|pass[w]ord|t[o]ken|private[_-]?key' src tests tools examples
 echo "must-not scans clean"
diff --git a/demo-rate-limiter/tools/mutants.py b/demo-rate-limiter/tools/mutants.py
index c415a65..b011031 100644
--- a/demo-rate-limiter/tools/mutants.py
+++ b/demo-rate-limiter/tools/mutants.py
@@ -26,7 +26,7 @@
     ),
     (
         "M3 drop recording of allowed hit",
-        "        hits.append(now)\n",
+        "            hits.append(now)\n",
         "\n",
     ),
     (
@@ -36,8 +36,8 @@
     ),
     (
         "M5 deny becomes allow (fail open)",
-        "            return False",
-        "            return True",
+        "                return False",
+        "                return True",
     ),
     (
         "M6 prune from wrong end",
@@ -51,10 +51,42 @@
     ),
     (
         "M8 denial records the attempt (memory leak)",
-        "        if len(hits) >= self._limit:\n            return False",
-        "        if len(hits) >= self._limit:\n"
-        "            hits.append(now)\n"
-        "            return False",
+        "            if len(hits) >= self._limit:\n                return False",
+        "            if len(hits) >= self._limit:\n"
+        "                hits.append(now)\n"
+        "                return False",
+    ),
+    # [REVISION 4] M9-M13 each pin a failure-model row that an independent
+    # verification pass showed was claiming coverage it did not have.
+    (
+        "M9 drop limit type/finiteness validation (limit=NaN allows forever)",
+        "        if isinstance(limit, bool) or not isinstance(limit, int):\n"
+        '            raise ValueError(f"limit must be an integer, got {limit!r}")\n',
+        "",
+    ),
+    (
+        "M10 clock skew fails open (absolute age)",
+        "while hits and now - hits[0] > self._window:",
+        "while hits and abs(now - hits[0]) > self._window:",
+    ),
+    # M11 (prune at most one expired hit per call: `while` -> `if`) is
+    # deliberately absent. A verification pass reported it as a surviving
+    # mutant proving "under-allowing drift"; it is in fact EQUIVALENT. If the
+    # head is expired, pruning one already leaves len <= limit-1, so both
+    # forms allow; if the head is not expired then under a monotone clock no
+    # entry is expired, so the deques are identical. Confirmed by differential
+    # test over 200k randomized monotone sequences: 0 divergences. Killing it
+    # would require a test asserting non-behavior — anti-gaming rule 4.
+    (
+        "M12 never forget idle keys (unbounded key-space growth)",
+        "        idle = [k for k, hits in self._hits.items() "
+        "if now - hits[-1] > self._window]\n",
+        "        idle: list[str] = []\n",
+    ),
+    (
+        "M13 drop the lock (concurrent over-allow)",
+        "        with self._lock:",
+        "        if True:",
     ),
 ]
 

From e21059491b7312183d837d20ababe66bd6efa2a9 Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 01:12:26 +0800
Subject: [PATCH 02/12] =?UTF-8?q?fix(demo):=20REVISION=204b=20=E2=80=94=20?=
 =?UTF-8?q?second=20verification=20round,=20incl.=20a=20mutation=20harness?=
 =?UTF-8?q?=20that=20reported=20kills=20it=20never=20executed?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The round-2 verifier found the mutation layer itself was fail-open. CPython
validates a cached .pyc against (source mtime in whole seconds, source size);
M4 and M5 are both exactly one byte shorter than the original and adjacent, so
M5 -- the fail-open mutant -- could run M4's bytecode and be reported KILLED
without executing. Reproduced directly: clean cache gives True/True, M4-then-M5
in one second gives True/False. The bias is always toward inflating the kill
count, so it can never surface as a red gauntlet.

- mutants.py clears __pycache__, runs pytest with PYTHONDONTWRITEBYTECODE, and
  hard-fails if a cache reappears. New --negative-control runs a killer and a
  strictly-equivalent mutant of identical size under one pinned mtime; it is a
  gauntlet gate, and it was proven non-vacuous by removing the cache defence
  and watching the equivalent mutant be misreported as KILLED.
- The first negative control was itself vacuous: it waited for two writes to
  land in the same second instead of pinning the mtime, and passed with the
  defence removed. Its C2 was also not strictly equivalent (the sweep throttle
  differs at now - last_sweep == window, which the memory bound now contracts).

Historical check, stated precisely: on 9540d72 the runner was structurally
vulnerable and exactly one adjacent pair could collide (M4/M5, both 1675
bytes). Re-derived under a sound procedure, all 8 historical mutants are
genuinely killed, M5 included. The published 8/8 is therefore correct in
outcome even though the procedure that produced it was unsound; whether that
archived run took the collision path cannot be determined, and does not change
the number.

Other round-2 findings:
- window_seconds had no type guard: True built a 1.0s window, "60" raised a
  bare TypeError. Validation extracted to _validate() so the constructor stays
  inside the complexity budget.
- Nothing pinned key identity: every key in the suite was lowercase, so
  key.lower() survived everything. Scenario + M14.
- P2's key strategy was left on sampled_from("abc") directly beneath the
  comment explaining why that was too narrow; the target key is now taken from
  the data instead of hardcoded, so the property cannot hold vacuously.
- The under-allowing row cited M6 (which over-allows) and M8 (claimed by the
  memory row); it now cites the mutant its scenario actually kills.
- Secret scan now covers .github, spec.md and the dependency files.
- The no-real-time claim is downgraded to what a regex can enforce, and the
  concurrency tests' deadlock-guard timeouts are declared as an exception
  rather than excluded from the scan.
- Clock finiteness and the cardinal (vs temporal) memory residual are recorded
  as accepted caller obligations.
- Concurrency: a deterministic fault-injection atomicity test now kills M13
  5/5; the threaded stress test goes to 400 rounds (measured 5.9% per-round
  detection; at 60 rounds the mutant survived 1 run in 50) and corroborates
  rather than carries the row.
- __pycache__ is cleared at gauntlet start; the scans were grepping bytecode.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/spec.md                     |  90 ++++++++++---
 demo-rate-limiter/src/ratelimiter/__init__.py |  31 +++--
 demo-rate-limiter/tests/test_properties.py    |  21 ++-
 demo-rate-limiter/tests/test_ratelimiter.py   |  61 ++++++++-
 demo-rate-limiter/tools/gauntlet.sh           |  22 +++-
 demo-rate-limiter/tools/mutants.py            | 122 ++++++++++++++++--
 6 files changed, 299 insertions(+), 48 deletions(-)

diff --git a/demo-rate-limiter/spec.md b/demo-rate-limiter/spec.md
index e9e4722..8ea4e90 100644
--- a/demo-rate-limiter/spec.md
+++ b/demo-rate-limiter/spec.md
@@ -71,13 +71,31 @@ Feature: Sliding-window rate limiting per key
     Then ValueError is raised naming limit
     (limit=NaN made every comparison False and the limiter allowed forever —
     the same fail-open class fixed for window_seconds in REVISION 2026-07-25,
-    never swept across to the sibling parameter)
+    never swept across to the sibling parameter. limit=2.5 was not "silently
+    treated as 2": len(hits) >= 2.5 is false at 2, so it allowed 3.)
+
+  Scenario: window_seconds must be a number  [REVISION 4b]
+    When constructing with window_seconds = True, "60", or None
+    Then ValueError is raised naming window_seconds
+    (the sweep ran one way only: window_seconds=True built a 1.0-second
+    window, and "60" raised a bare TypeError from math.isfinite instead of
+    naming the parameter the invalid-construction scenario promises)
+
+  Scenario: keys are compared as exact strings  [REVISION 4b]
+    Given a limiter with limit 1 per 60 seconds
+    When "Alice" and "alice" each make a request
+    Then both are allowed — they are different callers
+    (every key elsewhere in the suite is lowercase, so any normalisation of
+    the key was structurally invisible to the whole gauntlet)
 
   Scenario: key must be a non-empty string  [REVISION 4]
     When calling allow() with None, an int, bytes, or ""
     Then TypeError (wrong type) or ValueError (empty) is raised
-    (a missing HTTP header arriving as None must not silently become one
-    shared quota bucket for every unidentified caller)
+    (CONTRACT HARDENING, not a reproduced fail-open: None as a key made every
+    unidentified caller share one bucket, which limits too strictly or lets
+    callers exhaust each other's quota — it never let anyone past the limit.
+    Approved as a deliberate tightening for an HTTP-facing API, and recorded
+    separately from the defects that were demonstrated.)
 
   Scenario: idle keys are forgotten — the key map is bounded  [REVISION 4]
     Given a limiter with limit 1 per 60 seconds
@@ -100,9 +118,19 @@ Feature: Sliding-window rate limiting per key
 
 ## Must NOT do
 
-- No real time.sleep / wall-clock dependence in tests. Covers every spelling
-  (`import time`, `from time import sleep`, aliases, `datetime`) — not one
-  regex's idea of it. [REVISION 4: the gate matched only `time.`]
+- The limiter under test is never driven by a real clock, and no test makes
+  time pass by sleeping. [REVISION 4, amended: the gate matched only `time.`
+  and missed `from time import sleep`. The wording here previously claimed to
+  cover "every spelling", which a regex cannot do — dynamic imports, renamed
+  helpers, and a caller's own `sleep()` all escape it. The gate blocks known
+  direct wall-clock imports and calls; that is its actual scope.]
+  **Declared exception**: the concurrency tests use `Event.wait(timeout=)` and
+  `Thread.join(timeout=)` as deadlock guards, and the atomicity test asserts
+  that a blocked thread is still alive after 0.2s. That last assertion is a
+  genuine wall-clock dependence, accepted deliberately: the alternative is a
+  concurrency test that can hang forever. It is one-sided — it can only fail
+  spuriously if a thread is starved for 0.2s — and no limiter in any test
+  reads a real clock.
 - No unbounded memory growth. [REVISION 4: this clause used to read "from
   denied requests (denials store nothing)". Denials were never the leak;
   *allowed* requests from keys that never return were. Growth is now bounded
@@ -118,26 +146,54 @@ obligation, stated here because the failure model previously implied the
 non-monotonic scenario covered skew in both directions. It covers backward
 skew only.
 
+`clock` MUST also return a finite number. [REVISION 4b] A NaN reading is
+recorded as a hit that can never expire by pruning — `now - nan > window` is
+always false — so it permanently consumes one slot of that key's quota until
+an idle window lets the sweep drop the key. The spec sweeps NaN out of
+`limit` and `window_seconds`; the third injection point is the clock itself,
+and it is a caller obligation rather than a check, because validating every
+reading would put a branch on the hot path for a fault `time.monotonic` cannot
+produce.
+
+## Accepted residual risk [REVISION 4b]
+
+The memory bound is **temporal, not cardinal**: keys idle for a window are
+forgotten, but nothing caps how many distinct keys appear *within* one window.
+An attacker who controls the key — which, per the stated deployment, is an IP
+or a request header — can still drive the map arbitrarily large inside a
+single window, and because the sweep is throttled to once per window the
+worst-case retention is closer to two windows than one. This is accepted, not
+overlooked: a cardinality cap needs an eviction policy (which caller gets
+forgotten?), and evicting a live key silently resets its quota — a fail-open
+worse than the memory it saves. Recorded here so the residual reads as
+accepted rather than absent, in the same register as the clock contract.
+
 ## Failure model (Tier 3)
 
 [REVISION 3, 2026-07-27: retrofitted — the skill now requires an explicit
 failure model before layer selection; these modes were previously implicit
 in the scenarios, Must NOTs, and adversarial pass.]
 
-[REVISION 4, 2026-08-09: an independent fresh-context verification pass found
-that three rows below claimed coverage they did not have. Every row now names
-a test AND a mutant that demonstrably fails without it; a row whose catcher
-cannot be shown to fail is a defect, not a mapping.]
+[REVISION 4, 2026-08-09, amended 4b: independent fresh-context verification
+found rows below claiming coverage they did not have. The standard is now:
+every covered mode must name and demonstrate an **appropriate falsification
+procedure** — a test, a mutant, fault injection, a benchmark, a rollback
+rehearsal, whatever actually fits the risk. Not "a test AND a mutant", which
+just breeds mutants written to fill a table. A row whose catcher cannot be
+shown to fail is a defect, not a mapping.]
 
-| How this can hurt | Layer that catches it |
+| How this can hurt | Falsification procedure, demonstrated |
 |---|---|
-| over-allowing in a burst (limit not enforced) | scenario tests + P1 + mutants M1/M5 |
-| under-allowing / fail-closed drift (quota lost) | boundary scenario + mutants M6/M8 (P1 is one-sided and cannot catch this). Verification proposed a third mutant here; it proved EQUIVALENT — see mutants.py |
-| hostile or invalid config silently accepted | validation scenarios (window AND limit) + adversarial pass + mutants M4/M7/M9 |
-| backward clock skew opening the gate | non-monotonic clock scenario (jump must exceed the window) + mutant M10 |
+| over-allowing in a burst (limit not enforced) | scenario tests + P1; mutants M1/M5 killed |
+| under-allowing / fail-closed drift (quota lost) | boundary scenario, demonstrated by killing M2. [4b: this row previously cited M6/M8 — M6 in fact **over**-allows, and M8 is killed by the memory row's tests. Verification also proposed a `while`→`if` mutant here; it proved EQUIVALENT, see mutants.py] |
+| hostile or invalid config silently accepted | validation scenarios for limit, window_seconds AND key + adversarial pass; mutants M4/M7/M9/M15 killed |
+| backward clock skew opening the gate | non-monotonic clock scenario, jump exceeding the window; mutant M10 killed |
 | forward clock skew resetting all quota | **not covered — caller obligation**; see Clock contract |
-| unbounded memory growth (any path) | idle-keys scenario + denials test + mutants M8/M12 |
-| concurrent callers racing on shared state | concurrency scenario + mutant M13 (lock removed) |
+| a non-finite clock reading freezing a hit in the window | **not covered — caller obligation**; see Clock contract [4b] |
+| caller identity silently merged (key normalisation) | exact-strings scenario; mutant M14 killed [4b] |
+| unbounded memory growth (any path) | idle-keys scenario + denials test; mutants M8/M12 killed |
+| concurrent callers racing on shared state | **fault injection**: the atomicity test constructs the interleaving and kills M13 deterministically. The threaded stress test corroborates statistically (measured 5.9% per-round detection, 400 rounds) but cannot be the sole catcher — at 60 rounds the lock-removal mutant was observed surviving 1 run in 50 |
+| the mutation layer reporting kills it never ran | **negative control**: a killer and a strictly-equivalent mutant of identical size under one pinned mtime; proven non-vacuous by removing the cache defence and watching the control go red [4b] |
 | untested code reaching production | coverage layer, now a gate (`--cov-fail-under=100`) — it previously printed a number and could not fail |
 | silent failure in production | n-a: library returns a bool the caller observes directly |
 
diff --git a/demo-rate-limiter/src/ratelimiter/__init__.py b/demo-rate-limiter/src/ratelimiter/__init__.py
index 490df20..f6935b2 100644
--- a/demo-rate-limiter/src/ratelimiter/__init__.py
+++ b/demo-rate-limiter/src/ratelimiter/__init__.py
@@ -8,6 +8,26 @@
 __all__ = ["RateLimiter"]
 
 
+def _validate(limit: int, window_seconds: float) -> None:
+    """Reject any configuration that would silently never or always allow.
+
+    Extracted from __init__ so that adding the window_seconds type guard did
+    not push the constructor to the top of the complexity budget. `bool` is
+    excluded explicitly: it is a subclass of int, so True would otherwise be
+    accepted as a limit of 1 and a window of 1.0 second.
+    """
+    if isinstance(limit, bool) or not isinstance(limit, int):
+        raise ValueError(f"limit must be an integer, got {limit!r}")
+    if limit <= 0:
+        raise ValueError(f"limit must be positive, got {limit}")
+    if isinstance(window_seconds, bool) or not isinstance(window_seconds, int | float):
+        raise ValueError(f"window_seconds must be a number, got {window_seconds!r}")
+    if not math.isfinite(window_seconds) or window_seconds <= 0:
+        raise ValueError(
+            f"window_seconds must be positive and finite, got {window_seconds}"
+        )
+
+
 class RateLimiter:
     """Allow at most `limit` requests per key within any sliding window.
 
@@ -25,14 +45,7 @@ class RateLimiter:
     def __init__(
         self, limit: int, window_seconds: float, clock: Callable[[], float]
     ) -> None:
-        if isinstance(limit, bool) or not isinstance(limit, int):
-            raise ValueError(f"limit must be an integer, got {limit!r}")
-        if limit <= 0:
-            raise ValueError(f"limit must be positive, got {limit}")
-        if not math.isfinite(window_seconds) or window_seconds <= 0:
-            raise ValueError(
-                f"window_seconds must be positive and finite, got {window_seconds}"
-            )
+        _validate(limit, window_seconds)
         self._limit = limit
         self._window = window_seconds
         self._clock = clock
@@ -70,6 +83,4 @@ def _prune(self, key: str, now: float) -> deque[float]:
         hits = self._hits.get(key, deque())
         while hits and now - hits[0] > self._window:
             hits.popleft()
-        if not hits:
-            self._hits.pop(key, None)
         return hits
diff --git a/demo-rate-limiter/tests/test_properties.py b/demo-rate-limiter/tests/test_properties.py
index d65afcf..857c739 100644
--- a/demo-rate-limiter/tests/test_properties.py
+++ b/demo-rate-limiter/tests/test_properties.py
@@ -20,9 +20,12 @@
 # hardcoded key set. Measured by the layer-attribution run, not guessed.
 keys = st.text(alphabet="abc", min_size=1, max_size=2)
 requests = st.lists(st.tuples(timestamps, keys), max_size=60)
-isolation_requests = st.lists(
-    st.tuples(timestamps, st.sampled_from("abc")), max_size=60
-)
+# P2 needs the target key to recur, so it keeps a small pool — but the pool is
+# no longer three single characters. The widening above was applied to P1 only
+# in the first pass, directly under the comment explaining it; P2 was left
+# behind and killed none of M1/M5/M12 in attribution.
+isolation_keys = st.sampled_from(["a", "ab", "Ab", "b", "bc", "c "])
+isolation_requests = st.lists(st.tuples(timestamps, isolation_keys), max_size=60)
 limits = st.integers(min_value=1, max_value=5)
 # Mostly ordinary windows, sometimes far outside the tested range, so an
 # implementation that special-cases large windows cannot hide.
@@ -62,10 +65,16 @@ def test_p1_allowed_count_within_any_window_never_exceeds_limit(
 def test_p2_other_keys_traffic_never_changes_one_keys_outcomes(
     steps: list[tuple[float, str]], limit: int, window: float
 ) -> None:
+    if not steps:
+        return
     steps.sort(key=lambda s: s[0])
+    # Take the target from the data rather than hardcoding "a": with a wider
+    # key pool a fixed target is often absent, and the property then holds
+    # vacuously over two empty lists.
+    target = steps[0][1]
     clock_full = FakeClock()
     full = run(RateLimiter(limit, window, clock_full), clock_full, steps)
-    only_a = [s for s in steps if s[1] == "a"]
+    only_target = [s for s in steps if s[1] == target]
     clock_solo = FakeClock()
-    solo = run(RateLimiter(limit, window, clock_solo), clock_solo, only_a)
-    assert [o for o in full if o[1] == "a"] == solo
+    solo = run(RateLimiter(limit, window, clock_solo), clock_solo, only_target)
+    assert [o for o in full if o[1] == target] == solo
diff --git a/demo-rate-limiter/tests/test_ratelimiter.py b/demo-rate-limiter/tests/test_ratelimiter.py
index f3c2889..b3de758 100644
--- a/demo-rate-limiter/tests/test_ratelimiter.py
+++ b/demo-rate-limiter/tests/test_ratelimiter.py
@@ -119,6 +119,25 @@ def test_key_must_be_a_non_empty_string(
         limiter.allow(key)
 
 
+@pytest.mark.parametrize("window", [True, "60", None])
+def test_window_seconds_must_be_a_number(clock: FakeClock, window: Any) -> None:
+    # The 2026-07-25 NaN sweep ran on window_seconds and the REVISION 4 sweep
+    # ran on limit and key; window_seconds never got a type guard, so
+    # window_seconds=True built a 1.0-second window and "60" raised a bare
+    # TypeError from math.isfinite instead of naming the parameter.
+    with pytest.raises(ValueError, match="window_seconds"):
+        RateLimiter(limit=1, window_seconds=window, clock=clock)
+
+
+def test_keys_are_compared_as_exact_strings(clock: FakeClock) -> None:
+    # Every key anywhere else in the suite is lowercase, so any normalisation
+    # of the key (case-folding, trimming) was structurally invisible.
+    limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
+    assert limiter.allow("Alice") is True
+    assert limiter.allow("alice") is True  # a different caller, not the same one
+    assert limiter.allow("Alice") is False
+
+
 def test_idle_keys_are_forgotten_key_map_is_bounded(clock: FakeClock) -> None:
     limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
     for i in range(1000):
@@ -149,8 +168,48 @@ def worker() -> None:
     return sum(results)
 
 
+def test_allow_is_atomic_a_second_caller_cannot_interleave(clock: FakeClock) -> None:
+    """Deterministic counterpart to the stress test below: fault injection.
+
+    The stress test is a statistical detector (measured per-round detection
+    rate 5.9%), so it can only bound the miss probability, never eliminate it.
+    Here the interleaving is constructed: a one-shot gate holds the first
+    caller inside the critical section. Holding the lock, the second caller
+    blocks before reaching the gate; without it, the second caller walks in,
+    sees state the first has not written yet, and is allowed.
+    """
+    limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
+    inside, release = threading.Event(), threading.Event()
+    original_prune = limiter._prune
+    gated: list[int] = []
+
+    def prune_once_gated(key: str, now: float) -> Any:
+        if not gated:
+            gated.append(1)
+            inside.set()
+            release.wait(timeout=5)
+        return original_prune(key, now)
+
+    limiter._prune = prune_once_gated  # type: ignore[method-assign]
+    results: list[bool] = []
+    first = threading.Thread(target=lambda: results.append(limiter.allow("k")))
+    first.start()
+    assert inside.wait(timeout=5), "first caller never entered the critical section"
+    second = threading.Thread(target=lambda: results.append(limiter.allow("k")))
+    second.start()
+    second.join(timeout=0.2)
+    assert second.is_alive(), "second caller entered while the first held the lock"
+    release.set()
+    first.join(timeout=5)
+    second.join(timeout=5)
+    assert sorted(results) == [False, True]
+
+
 def test_concurrent_callers_never_exceed_the_limit() -> None:
-    rounds, threads = 60, 16
+    # 400 rounds at a measured per-round detection rate of 5.9% puts the miss
+    # probability near 3e-11; at the original 60 rounds it was 2.7e-2, and the
+    # mutant that removes the lock was observed surviving 1 run in 50.
+    rounds, threads = 400, 16
     previous_interval = sys.getswitchinterval()
     sys.setswitchinterval(1e-6)  # widen the preemption window
     try:
diff --git a/demo-rate-limiter/tools/gauntlet.sh b/demo-rate-limiter/tools/gauntlet.sh
index 41c78ba..367db5f 100755
--- a/demo-rate-limiter/tools/gauntlet.sh
+++ b/demo-rate-limiter/tools/gauntlet.sh
@@ -3,6 +3,9 @@
 set -e
 cd "$(dirname "$0")/.."
 rm -f .coverage coverage.xml   # stale artifacts from previous runs
+# Bytecode caches are both a correctness hazard for the mutation layer and
+# binary noise the must-not scans would grep through.
+find . -name __pycache__ -type d -prune -exec rm -rf {} +
 PY=.venv/bin
 
 . tools/must_not_match.sh
@@ -27,11 +30,26 @@ echo "=== must-not scans ==="
 # sleep`. Deliberately not `[[:<:]]time`, which would fire on conftest's own
 # "No real time in tests" docstring and on test_non_monotonic_clock_* — the
 # fix belongs in the pattern, never in an exclusion.
+#
+# Scope is deliberately narrower than the Must NOT's ambition: it catches real
+# time being read or slept on, not every way a test could depend on wall
+# clock. `Event.wait(timeout=)` and `Thread.join(timeout=)` are NOT matched —
+# they are deadlock guards in the concurrency tests, declared as an exception
+# in spec.md rather than excluded here. A pattern cannot decide intent, so the
+# spec says what the gate actually covers instead of claiming more.
 must_not_match 'import[[:space:]]+time|from[[:space:]]+time[[:space:]]+import|time\.|datetime|sleep[[:space:]]*\(|perf_counter[[:space:]]*\(|monotonic[[:space:]]*\(' tests
-# Bracketed letters stop the pattern literal from matching itself.
-must_not_match 'api[_-]?key|s[e]cret|pass[w]ord|t[o]ken|private[_-]?key' src tests tools examples
+# Bracketed letters stop the pattern literal from matching itself. The path
+# list now includes CI config and metadata: workflows are where credentials
+# actually appear, and scanning only src/tests/tools/examples missed them.
+must_not_match 'api[_-]?key|s[e]cret|pass[w]ord|t[o]ken|private[_-]?key' \
+  src tests tools examples spec.md pyproject.toml requirements-dev.txt ../.github
 echo "must-not scans clean"
 echo "=== mutation ==="
+# Negative control first: a killer and a strictly-equivalent mutant of
+# identical size under one pinned mtime. If bytecode ever leaks between runs,
+# the equivalent one inherits the killer's verdict and the whole kill count is
+# inflated — silently, and only ever upward.
+"$PY/python" tools/mutants.py --negative-control
 "$PY/python" tools/mutants.py
 echo "=== real execution ==="
 "$PY/python" examples/demo.py
diff --git a/demo-rate-limiter/tools/mutants.py b/demo-rate-limiter/tools/mutants.py
index b011031..a5a76c4 100644
--- a/demo-rate-limiter/tools/mutants.py
+++ b/demo-rate-limiter/tools/mutants.py
@@ -5,14 +5,28 @@
 suite (e.g. a single test) for layer-attribution or prove-it-can-fail runs.
 """
 
+import os
+import shutil
 import subprocess
 import sys
 from pathlib import Path
 
 ROOT = Path(__file__).resolve().parent.parent
 TARGET = ROOT / "src/ratelimiter/__init__.py"
+PYCACHE = TARGET.parent / "__pycache__"
 PYTEST = ROOT / ".venv/bin/pytest"
 
+# CPython validates a cached .pyc against (source mtime in whole seconds,
+# source size). Two mutants of identical size written inside the same second
+# are indistinguishable to that check, so the second one silently runs the
+# first one's bytecode. M4 and M5 are both exactly one byte shorter than the
+# original and adjacent in the list, so M5 -- the fail-open mutant -- was
+# reported KILLED on the strength of M4's code. The bias is toward inflating
+# the kill count, which can never surface as a red gauntlet. Both defences are
+# needed: removing the cache stops a stale read, DONTWRITEBYTECODE stops a new
+# one being created mid-run.
+MUTANT_ENV = {**os.environ, "PYTHONDONTWRITEBYTECODE": "1"}
+
 MUTANTS = [
     (
         "M1 flip limit comparison >= to >",
@@ -60,8 +74,22 @@
     # verification pass showed was claiming coverage it did not have.
     (
         "M9 drop limit type/finiteness validation (limit=NaN allows forever)",
-        "        if isinstance(limit, bool) or not isinstance(limit, int):\n"
-        '            raise ValueError(f"limit must be an integer, got {limit!r}")\n',
+        "    if isinstance(limit, bool) or not isinstance(limit, int):\n"
+        '        raise ValueError(f"limit must be an integer, got {limit!r}")\n',
+        "",
+    ),
+    (
+        "M14 normalise the key (distinct callers share one bucket)",
+        '            raise ValueError("key must not be empty")\n',
+        '            raise ValueError("key must not be empty")\n'
+        "        key = key.lower()\n",
+    ),
+    (
+        "M15 drop window_seconds type guard (window=True means 1 second)",
+        "    if isinstance(window_seconds, bool) or not isinstance("
+        "window_seconds, int | float):\n"
+        '        raise ValueError(f"window_seconds must be a number, '
+        'got {window_seconds!r}")\n',
         "",
     ),
     (
@@ -91,7 +119,83 @@
 ]
 
 
+# Negative control for the harness itself: two mutants of IDENTICAL size (each
+# one byte shorter than the original), a killer followed by a proven-equivalent
+# one. If bytecode caching ever leaks between runs again, the equivalent mutant
+# inherits the killer's result and is misreported as KILLED. Run with
+# --negative-control; exercised by tools/test_gauntlet_checks.sh.
+# Both mutations are length-preserving, so the two mutated files are the same
+# size; with a pinned mtime the (mtime, size) collision is constructed, not
+# waited for. C2 must be STRICTLY equivalent: `or` over two side-effect-free
+# isinstance checks is commutative. An earlier attempt used the sweep throttle
+# (`<=` -> `<`), which differs at now - last_sweep == window and so can change
+# the key map — not equivalent once the memory bound is part of the contract,
+# and it would have turned red the day a test pinned that boundary.
+CONTROL = [
+    ("C1 killer (control)", "if limit <= 0:", "if limit >= 0:"),
+    (
+        "C2 equivalent (control)",
+        "if isinstance(limit, bool) or not isinstance(limit, int):",
+        "if not isinstance(limit, int) or isinstance(limit, bool):",
+    ),
+]
+
+
+def run_mutant(
+    original: str, old: str, new: str, pytest_target: str, pin_mtime: float = 0.0
+) -> int:
+    """Apply one mutant and return pytest's exit code, with no stale bytecode.
+
+    `pin_mtime` is used only by the negative control: pinning both control
+    mutants to one mtime makes the (mtime, size) collision deterministic
+    instead of depending on two writes happening to land in the same second.
+    """
+    TARGET.write_text(original.replace(old, new))
+    if pin_mtime:
+        os.utime(TARGET, (pin_mtime, pin_mtime))
+    shutil.rmtree(PYCACHE, ignore_errors=True)
+    result = subprocess.run(
+        [str(PYTEST), "-q", "-x", pytest_target],
+        cwd=ROOT,
+        capture_output=True,
+        text=True,
+        env=MUTANT_ENV,
+    )
+    if PYCACHE.exists():
+        raise RuntimeError(
+            "bytecode cache reappeared during a mutant run: results are not "
+            "trustworthy (PYTHONDONTWRITEBYTECODE had no effect)"
+        )
+    return result.returncode
+
+
+def negative_control() -> int:
+    """Prove the harness can still tell a killer from an equivalent mutant."""
+    original = TARGET.read_text()
+    try:
+        pinned = 1_600_000_000.0  # identical mtime for both, see run_mutant
+        codes = [
+            run_mutant(original, old, new, "tests", pin_mtime=pinned)
+            for _, old, new in CONTROL
+        ]
+    finally:
+        TARGET.write_text(original)
+        # The control pins an mtime and leaves cache state behind; neither may
+        # leak into the real mutation run that follows.
+        shutil.rmtree(PYCACHE, ignore_errors=True)
+    if TARGET.read_text() != original:
+        raise RuntimeError("negative control did not restore the source file")
+    ok = codes == [1, 0]
+    for (name, _, _), code in zip(CONTROL, codes, strict=True):
+        verdict = {1: "KILLED", 0: "SURVIVED"}.get(code, f"ERROR (exit {code})")
+        print(f"  {name}: {verdict}")
+    print("  negative control: " + ("ok" if ok else "FAILED — harness misreports"))
+    return 0 if ok else 1
+
+
 def main() -> int:
+    if len(sys.argv) > 1 and sys.argv[1] == "--negative-control":
+        return negative_control()
     pytest_target = sys.argv[1] if len(sys.argv) > 1 else "tests"
     original = TARGET.read_text()
     killed = 0
@@ -99,23 +203,17 @@ def main() -> int:
     try:
         for name, old, new in MUTANTS:
             assert original.count(old) == 1, f"{name}: pattern not unique"
-            TARGET.write_text(original.replace(old, new))
-            result = subprocess.run(
-                [str(PYTEST), "-q", "-x", pytest_target],
-                cwd=ROOT,
-                capture_output=True,
-                text=True,
-            )
+            returncode = run_mutant(original, old, new, pytest_target)
             # Only exit code 1 (tests ran and at least one failed) is a kill.
             # 0 = survived; anything else (collection error, usage error, no
             # tests collected) means nothing was verified — never count it.
-            if result.returncode == 1:
+            if returncode == 1:
                 status = "KILLED"
                 killed += 1
-            elif result.returncode == 0:
+            elif returncode == 0:
                 status = "SURVIVED"
             else:
-                status = f"ERROR (pytest exit {result.returncode}, no tests verified)"
+                status = f"ERROR (pytest exit {returncode}, no tests verified)"
                 errors += 1
             print(f"{name}: {status}")
     finally:

From 49afb2b9d2c9cee2f5a0ee22094ad69a25a059b5 Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 01:32:08 +0800
Subject: [PATCH 03/12] =?UTF-8?q?fix(demo):=20REVISION=204c=20=E2=80=94=20?=
 =?UTF-8?q?the=20lock=20did=20not=20cover=20the=20clock=20read?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Round 3 found that REVISION 4's own concurrency fix was incomplete: the lock
covered check-and-append but `now = self._clock()` sat outside it. Two callers
can therefore commit in the opposite order from which they read the clock,
leaving the deque unsorted. _prune breaks fail-closed; _sweep breaks fail-open
— it judges a key by a stale newest-hit and forgets one that still has a live
hit, resetting that caller's quota. Reproduced: limit=2 window=60 with hits
[100.0, 99.0] allows 3 requests inside one window, violating P1 and approved
contract item (d).

The mutant that IS the fix (M16, read the clock outside the lock) survived the
entire suite before this change: both existing concurrency tests hold time
constant, so no test could distinguish the two lock placements. The new test
gates the clock itself to force two callers to read different values, and
asserts the recorded hits stay ascending.

Cost recorded in the clock contract: `clock` must not call back into the same
limiter, which would now deadlock.

Other round-3 findings:
- The 4b clock contract claimed a NaN-poisoned key would eventually be swept.
  It cannot — _sweep uses the same comparison. The key is immortal and its
  caller denied forever, which falsifies the temporal memory bound for that
  path; both sentences corrected rather than softened.
- Key normalisation coverage was case-folding only; key.strip() survived,
  helped by a P2 pool containing "c " but not "c". Padding and whitespace-only
  keys are now pinned, pool fixed, M17 added.
- _sweep's expiry boundary was unpinned while _prune's was; the surviving
  mutant was fail-open (forgets a key with a live hit). Scenario + M18.
- Secret scan missed "-----BEGIN RSA PRIVATE KEY-----" (space separator).
- source_state.sh did not hash .github/workflows, so evidence could rebind to
  a tree whose CI config had silently changed.
- _prune's docstring still described key-forgetting it no longer does.
- The negative control validates the two cache defences as a conjunction, not
  individually; the comment now states the asymmetry instead of "both needed".

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/spec.md                     | 58 +++++++++++++----
 demo-rate-limiter/src/ratelimiter/__init__.py | 10 ++-
 demo-rate-limiter/tests/test_properties.py    |  2 +-
 demo-rate-limiter/tests/test_ratelimiter.py   | 64 ++++++++++++++++++-
 demo-rate-limiter/tools/gauntlet.sh           |  2 +-
 demo-rate-limiter/tools/mutants.py            | 26 +++++++-
 demo-rate-limiter/tools/source_state.sh       |  4 ++
 7 files changed, 145 insertions(+), 21 deletions(-)

diff --git a/demo-rate-limiter/spec.md b/demo-rate-limiter/spec.md
index 8ea4e90..38da2a7 100644
--- a/demo-rate-limiter/spec.md
+++ b/demo-rate-limiter/spec.md
@@ -81,12 +81,34 @@ Feature: Sliding-window rate limiting per key
     window, and "60" raised a bare TypeError from math.isfinite instead of
     naming the parameter the invalid-construction scenario promises)
 
-  Scenario: keys are compared as exact strings  [REVISION 4b]
+  Scenario: keys are compared as exact strings  [REVISION 4b, widened in 4c]
     Given a limiter with limit 1 per 60 seconds
-    When "Alice" and "alice" each make a request
-    Then both are allowed — they are different callers
-    (every key elsewhere in the suite is lowercase, so any normalisation of
-    the key was structurally invisible to the whole gauntlet)
+    When "Alice", "alice", "alice " and " " each make a request
+    Then all are allowed — they are four different callers
+    (every key elsewhere in the suite was lowercase and unpadded, so key
+    normalisation was structurally invisible. Case was pinned in 4b and
+    trimming still survived it, so padding is pinned too. A whitespace-only
+    key is a valid caller by the same rule: the contract is "non-empty str",
+    and deciding that " " is not a real caller is the caller's business.)
+
+  Scenario: the sweep keeps a key whose newest hit is exactly one window old
+    [REVISION 4c]
+    Given a limiter with limit 1 per 60 seconds
+    And another key's request at t=0 that arms the sweep, and "k" at t=1
+    When any request arrives at t=61, firing the sweep
+    Then "k" is still limited — its hit is exactly 60s old, not older
+    (the exact-boundary scenario pins _prune's comparison; _sweep re-implements
+    the same age test and nothing pinned it, so a >= there forgot a key that
+    still had a live hit and reset that caller's quota)
+
+  Scenario: concurrent commits never invert against the clock read
+    [REVISION 4c]
+    Given two callers whose clock reads are forced to return different values
+    When the caller that read the earlier value commits second
+    Then the recorded hits are still in ascending order
+    (both _prune and _sweep assume that order; the lock originally covered
+    check-and-append but not the clock read, and every other concurrency test
+    held time constant so the whole class of ordering races was invisible)
 
   Scenario: key must be a non-empty string  [REVISION 4]
     When calling allow() with None, an int, bytes, or ""
@@ -146,15 +168,23 @@ obligation, stated here because the failure model previously implied the
 non-monotonic scenario covered skew in both directions. It covers backward
 skew only.
 
-`clock` MUST also return a finite number. [REVISION 4b] A NaN reading is
-recorded as a hit that can never expire by pruning — `now - nan > window` is
-always false — so it permanently consumes one slot of that key's quota until
-an idle window lets the sweep drop the key. The spec sweeps NaN out of
-`limit` and `window_seconds`; the third injection point is the clock itself,
-and it is a caller obligation rather than a check, because validating every
-reading would put a branch on the hot path for a fault `time.monotonic` cannot
+`clock` MUST also return a finite number. [REVISION 4b, corrected in 4c] A NaN
+reading is recorded as a hit that can never expire: `now - nan > window` is
+always false, in `_prune` **and in `_sweep`**. Revision 4b claimed the sweep
+would eventually reclaim such a key; it cannot — the sweep uses the same
+comparison. Measured: once a key's newest hit is NaN, the key is retained
+through t=1e18 and that caller is denied forever. **This falsifies the
+temporal memory bound for NaN-poisoned keys**, which is stated here rather
+than left to be inferred. The third NaN injection point is the clock itself,
+and it stays a caller obligation rather than a check because validating every
+reading puts a branch on the hot path for a fault `time.monotonic` cannot
 produce.
 
+`clock` MUST NOT call back into the same limiter. [REVISION 4c] The clock is
+read inside the critical section, so a reentrant clock deadlocks on a
+non-reentrant lock. This is the price of the fix for the ordering race and is
+recorded as an obligation rather than hidden.
+
 ## Accepted residual risk [REVISION 4b]
 
 The memory bound is **temporal, not cardinal**: keys idle for a window are
@@ -190,7 +220,9 @@ shown to fail is a defect, not a mapping.]
 | backward clock skew opening the gate | non-monotonic clock scenario, jump exceeding the window; mutant M10 killed |
 | forward clock skew resetting all quota | **not covered — caller obligation**; see Clock contract |
 | a non-finite clock reading freezing a hit in the window | **not covered — caller obligation**; see Clock contract [4b] |
-| caller identity silently merged (key normalisation) | exact-strings scenario; mutant M14 killed [4b] |
+| caller identity silently merged (key normalisation) | exact-strings scenario, covering case AND padding; mutants M14/M17 killed. [4c: the row previously cited case-folding only, and `key.strip()` survived it — the P2 pool held `"c "` but not `"c"`, so no two members could merge] |
+| a caller's quota reset by the sweep at the exact boundary | sweep-boundary scenario; mutant M18 killed [4c] |
+| concurrent commits inverted against the clock read | clock-ordering scenario (gated clock forces two callers to read different values); mutant M16 killed. [4c: the lock covered check-and-append but not the clock read. Both earlier concurrency tests held time constant, so no test could tell the two placements apart] |
 | unbounded memory growth (any path) | idle-keys scenario + denials test; mutants M8/M12 killed |
 | concurrent callers racing on shared state | **fault injection**: the atomicity test constructs the interleaving and kills M13 deterministically. The threaded stress test corroborates statistically (measured 5.9% per-round detection, 400 rounds) but cannot be the sole catcher — at 60 rounds the lock-removal mutant was observed surviving 1 run in 50 |
 | the mutation layer reporting kills it never ran | **negative control**: a killer and a strictly-equivalent mutant of identical size under one pinned mtime; proven non-vacuous by removing the cache defence and watching the control go red [4b] |
diff --git a/demo-rate-limiter/src/ratelimiter/__init__.py b/demo-rate-limiter/src/ratelimiter/__init__.py
index f6935b2..3997c8f 100644
--- a/demo-rate-limiter/src/ratelimiter/__init__.py
+++ b/demo-rate-limiter/src/ratelimiter/__init__.py
@@ -59,8 +59,14 @@ def allow(self, key: str) -> bool:
             raise TypeError(f"key must be a str, got {type(key).__name__}")
         if not key:
             raise ValueError("key must not be empty")
-        now = self._clock()
+        # The clock read belongs inside the lock. Read outside it, two callers
+        # can commit in the opposite order from which they read the clock, and
+        # the deque that _prune and _sweep both assume is ascending stops being
+        # so; _sweep then reads a stale newest-hit and forgets a key that still
+        # has a live hit, resetting that caller's quota. Cost: `clock` must not
+        # call back into this limiter (see the clock contract).
         with self._lock:
+            now = self._clock()
             self._sweep(now)
             hits = self._prune(key, now)
             if len(hits) >= self._limit:
@@ -79,7 +85,7 @@ def _sweep(self, now: float) -> None:
             del self._hits[key]
 
     def _prune(self, key: str, now: float) -> deque[float]:
-        """Drop hits older than the window; forget keys with none left."""
+        """Drop hits older than the window. Forgetting keys is _sweep's job."""
         hits = self._hits.get(key, deque())
         while hits and now - hits[0] > self._window:
             hits.popleft()
diff --git a/demo-rate-limiter/tests/test_properties.py b/demo-rate-limiter/tests/test_properties.py
index 857c739..13a918f 100644
--- a/demo-rate-limiter/tests/test_properties.py
+++ b/demo-rate-limiter/tests/test_properties.py
@@ -24,7 +24,7 @@
 # no longer three single characters. The widening above was applied to P1 only
 # in the first pass, directly under the comment explaining it; P2 was left
 # behind and killed none of M1/M5/M12 in attribution.
-isolation_keys = st.sampled_from(["a", "ab", "Ab", "b", "bc", "c "])
+isolation_keys = st.sampled_from(["a", "ab", "Ab", "b", "bc", "c", "c "])
 isolation_requests = st.lists(st.tuples(timestamps, isolation_keys), max_size=60)
 limits = st.integers(min_value=1, max_value=5)
 # Mostly ordinary windows, sometimes far outside the tested range, so an
diff --git a/demo-rate-limiter/tests/test_ratelimiter.py b/demo-rate-limiter/tests/test_ratelimiter.py
index b3de758..76d1094 100644
--- a/demo-rate-limiter/tests/test_ratelimiter.py
+++ b/demo-rate-limiter/tests/test_ratelimiter.py
@@ -130,14 +130,32 @@ def test_window_seconds_must_be_a_number(clock: FakeClock, window: Any) -> None:
 
 
 def test_keys_are_compared_as_exact_strings(clock: FakeClock) -> None:
-    # Every key anywhere else in the suite is lowercase, so any normalisation
-    # of the key (case-folding, trimming) was structurally invisible.
+    # Every key anywhere else in the suite is lowercase and unpadded, so any
+    # normalisation of the key was structurally invisible. Case-folding was
+    # pinned first; trimming survived that fix, so padding is pinned too, and
+    # a whitespace-only key is a valid distinct caller by the same rule.
     limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
     assert limiter.allow("Alice") is True
     assert limiter.allow("alice") is True  # a different caller, not the same one
+    assert limiter.allow("alice ") is True  # and so is this one
+    assert limiter.allow(" ") is True  # non-empty, therefore a caller
     assert limiter.allow("Alice") is False
 
 
+def test_sweep_keeps_a_key_whose_newest_hit_is_exactly_window_old(
+    clock: FakeClock,
+) -> None:
+    # The boundary scenario above pins _prune's comparison; _sweep re-implements
+    # the same age test and nothing pinned it, so a >= there silently forgot a
+    # key that still had a live hit and reset that caller's quota.
+    limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
+    assert limiter.allow("other") is True  # t=0, arms the sweep clock
+    clock.now = 1.0
+    assert limiter.allow("k") is True
+    clock.now = 61.0  # sweep fires; k's only hit is exactly 60s old
+    assert limiter.allow("k") is False
+
+
 def test_idle_keys_are_forgotten_key_map_is_bounded(clock: FakeClock) -> None:
     limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
     for i in range(1000):
@@ -205,6 +223,48 @@ def prune_once_gated(key: str, now: float) -> Any:
     assert sorted(results) == [False, True]
 
 
+def test_clock_is_read_inside_the_critical_section() -> None:
+    """The lock must cover the clock read, not just the check-and-append.
+
+    Both other concurrency tests hold time constant, so they cannot see this:
+    with one clock value no ordering between threads is observable. If the
+    read happens outside the lock, two callers can commit in the opposite
+    order from which they read the clock, leaving the deque unsorted — and
+    _sweep then judges the key by a stale newest-hit and deletes a key that
+    still has a live hit, resetting that caller's quota. Fail-open.
+    """
+    times = iter([99.0, 100.0])
+    first_read, second_done = threading.Event(), threading.Event()
+    gated: list[int] = []
+
+    def gated_clock() -> float:
+        value = next(times)
+        if not gated:
+            gated.append(1)
+            first_read.set()
+            # Read inside the lock, the second caller is blocked and this
+            # cannot be satisfied, so it times out and the order stays
+            # correct. Read outside, the second caller finishes and inverts.
+            second_done.wait(timeout=0.3)
+        return value
+
+    limiter = RateLimiter(limit=5, window_seconds=60, clock=gated_clock)
+    first = threading.Thread(target=lambda: limiter.allow("k"))
+    first.start()
+    assert first_read.wait(timeout=5), "first caller never read the clock"
+
+    def second_caller() -> None:
+        limiter.allow("k")
+        second_done.set()
+
+    second = threading.Thread(target=second_caller)
+    second.start()
+    first.join(timeout=5)
+    second.join(timeout=5)
+    hits = list(limiter._hits["k"])
+    assert hits == sorted(hits), f"commits inverted, deque unsorted: {hits}"
+
+
 def test_concurrent_callers_never_exceed_the_limit() -> None:
     # 400 rounds at a measured per-round detection rate of 5.9% puts the miss
     # probability near 3e-11; at the original 60 rounds it was 2.7e-2, and the
diff --git a/demo-rate-limiter/tools/gauntlet.sh b/demo-rate-limiter/tools/gauntlet.sh
index 367db5f..db811b6 100755
--- a/demo-rate-limiter/tools/gauntlet.sh
+++ b/demo-rate-limiter/tools/gauntlet.sh
@@ -41,7 +41,7 @@ must_not_match 'import[[:space:]]+time|from[[:space:]]+time[[:space:]]+import|ti
 # Bracketed letters stop the pattern literal from matching itself. The path
 # list now includes CI config and metadata: workflows are where credentials
 # actually appear, and scanning only src/tests/tools/examples missed them.
-must_not_match 'api[_-]?key|s[e]cret|pass[w]ord|t[o]ken|private[_-]?key' \
+must_not_match 'api[_-]?key|s[e]cret|pass[w]ord|t[o]ken|private[_ -]?key|BEGIN[[:space:]]+[A-Z ]*PRIVATE' \
   src tests tools examples spec.md pyproject.toml requirements-dev.txt ../.github
 echo "must-not scans clean"
 echo "=== mutation ==="
diff --git a/demo-rate-limiter/tools/mutants.py b/demo-rate-limiter/tools/mutants.py
index a5a76c4..f991c3f 100644
--- a/demo-rate-limiter/tools/mutants.py
+++ b/demo-rate-limiter/tools/mutants.py
@@ -23,8 +23,11 @@
 # original and adjacent in the list, so M5 -- the fail-open mutant -- was
 # reported KILLED on the strength of M4's code. The bias is toward inflating
 # the kill count, which can never surface as a red gauntlet. Both defences are
-# needed: removing the cache stops a stale read, DONTWRITEBYTECODE stops a new
-# one being created mid-run.
+# needed, but not symmetrically. DONTWRITEBYTECODE alone leaves the negative
+# control green: with no .pyc written during the run, a stale one can only be
+# the pristine pre-run file, which biases toward a false SURVIVED — a red
+# gauntlet, not a silent inflation. Removing it is caught by a separate
+# tripwire below. The rmtree is what closes the between-mutants leak.
 MUTANT_ENV = {**os.environ, "PYTHONDONTWRITEBYTECODE": "1"}
 
 MUTANTS = [
@@ -116,6 +119,25 @@
         "        with self._lock:",
         "        if True:",
     ),
+    # [REVISION 4c] A third verification round found the lock covered the
+    # check-and-append but not the clock read, and that no test could tell the
+    # two placements apart because every concurrency test held time constant.
+    (
+        "M16 read the clock outside the lock (commits invert, deque unsorted)",
+        "        with self._lock:\n            now = self._clock()\n",
+        "        now = self._clock()\n        with self._lock:\n",
+    ),
+    (
+        "M17 strip the key (trailing-space caller merged with the bare one)",
+        '            raise ValueError("key must not be empty")\n',
+        '            raise ValueError("key must not be empty")\n'
+        "        key = key.strip()\n",
+    ),
+    (
+        "M18 sweep expiry boundary > to >= (forgets a key with a live hit)",
+        "if now - hits[-1] > self._window]\n",
+        "if now - hits[-1] >= self._window]\n",
+    ),
 ]
 
 
diff --git a/demo-rate-limiter/tools/source_state.sh b/demo-rate-limiter/tools/source_state.sh
index 4a3f9ca..6d15547 100755
--- a/demo-rate-limiter/tools/source_state.sh
+++ b/demo-rate-limiter/tools/source_state.sh
@@ -9,6 +9,10 @@ if git rev-parse --short HEAD >/dev/null 2>&1; then
 else
   printf "commit: (no git)\n"
 fi
+# ../.github/workflows decides whether the gauntlet runs at all in CI, so it
+# belongs in the state the evidence binds to; omitting it let CI config change
+# silently under an unchanged hash.
 tree_hash=$(find src tests tools examples pyproject.toml requirements-dev.txt spec.md \
+  ../.github/workflows \
   -type f -not -path "*__pycache__*" | sort | xargs shasum -a 256 | shasum -a 256 | cut -c1-16)
 printf "tree:   %s\n" "$tree_hash"

From d65acbefa2f7f397ee657a8ea9ceca8c2e4a2788 Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 01:51:21 +0800
Subject: [PATCH 04/12] =?UTF-8?q?fix(demo):=20REVISION=204d=20=E2=80=94=20?=
 =?UTF-8?q?round=204=20passed;=20its=20accuracy=20defects=20fixed?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Round 4 returned VERDICT passed with no MATERIAL finding: the core semantics
survived a 180k-op differential fuzz (0 divergences) and 17 fresh mutants, and
every home-grown gate was fed known-bad input and failed closed — including
the negative control's specific non-vacuity claim, which reproduced stepwise
exactly as documented.

Its four MINOR findings were accuracy defects, and two of them had real teeth:

- The memory bound was documented as one window in both the class docstring
  and the Must NOT. It is two: the sweep is throttled to once per window, so a
  key can sit idle for just under 2W. Only the residual-risk section had it
  right, and the idle-keys test probed at exactly 2W so it passed under either
  reading and pinned neither. New test pins both sides.
- A backward clock jump suspended the sweep entirely: the throttle compared
  now against a _last_sweep it could no longer reach. Measured 20,001 keys
  retained across seven windows of monotone time. The docstring's "a backward
  jumping clock fails closed" was true of quota and false of memory. Fixed in
  code rather than documented away: the throttle is now two-sided, so a
  negative delta re-arms it at the new time. M20 pins it.
- The sweep throttle was an asserted design property with no catcher —
  deleting its bookkeeping left the suite green while turning every request
  into an O(distinct keys) scan. Test + M19.
- Declared exception (h) named one wall-clock dependence; there are two, and
  they fail in opposite directions. The 0.3s wait in the clock-ordering test
  is not a deadlock guard: on healthy code it always times out, and its
  spurious direction is a false PASS — a surviving fail-open mutant. Measured
  margin ~470x, so accepted, but now described accurately.
- The NaN-clock paragraph described the never-expiring hit as the whole mode;
  NaN also destroys the sweep throttle permanently.
- P2's comment claimed an attribution the measurement contradicts.

The must-not time scan matched `time.` inside ordinary prose ("sweep time.
After"); narrowed to attribute access, in the pattern rather than by excluding
files, and verified to still catch real `time.sleep`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/spec.md                     | 40 +++++++++++----
 demo-rate-limiter/src/ratelimiter/__init__.py | 15 ++++--
 demo-rate-limiter/tests/test_properties.py    |  4 +-
 demo-rate-limiter/tests/test_ratelimiter.py   | 50 +++++++++++++++++++
 demo-rate-limiter/tools/gauntlet.sh           |  2 +-
 demo-rate-limiter/tools/mutants.py            | 13 +++++
 6 files changed, 108 insertions(+), 16 deletions(-)

diff --git a/demo-rate-limiter/spec.md b/demo-rate-limiter/spec.md
index 38da2a7..6a1b983 100644
--- a/demo-rate-limiter/spec.md
+++ b/demo-rate-limiter/spec.md
@@ -146,17 +146,28 @@ Feature: Sliding-window rate limiting per key
   cover "every spelling", which a regex cannot do — dynamic imports, renamed
   helpers, and a caller's own `sleep()` all escape it. The gate blocks known
   direct wall-clock imports and calls; that is its actual scope.]
-  **Declared exception**: the concurrency tests use `Event.wait(timeout=)` and
-  `Thread.join(timeout=)` as deadlock guards, and the atomicity test asserts
-  that a blocked thread is still alive after 0.2s. That last assertion is a
-  genuine wall-clock dependence, accepted deliberately: the alternative is a
-  concurrency test that can hang forever. It is one-sided — it can only fail
-  spuriously if a thread is starved for 0.2s — and no limiter in any test
-  reads a real clock.
+  **Declared exception** [corrected in 4d]: the concurrency tests use
+  `Event.wait(timeout=)` and `Thread.join(timeout=)`. Most are deadlock guards,
+  but TWO are genuine wall-clock dependences and they fail in OPPOSITE
+  directions, which the 4b wording got wrong by naming only the first:
+  (1) the atomicity test asserts a blocked thread is still alive after 0.2s —
+  spurious failure only, if a thread is starved that long;
+  (2) `second_done.wait(timeout=0.3)` in the clock-ordering test is not a
+  guard at all: on healthy code it ALWAYS times out (a fixed 0.3s per suite
+  run), and on the mutant that moves the clock read outside the lock the kill
+  depends on the second caller finishing inside that budget. Its spurious
+  direction is therefore a false PASS — a surviving fail-open mutant, the
+  worse direction. Measured margin is ~470x (0.06-0.63ms of 300ms), so it is
+  accepted, not ignored. No limiter in any test reads a real clock.
 - No unbounded memory growth. [REVISION 4: this clause used to read "from
   denied requests (denials store nothing)". Denials were never the leak;
-  *allowed* requests from keys that never return were. Growth is now bounded
-  by the distinct keys seen within one window — see the idle-keys scenario.]
+  *allowed* requests from keys that never return were. Growth is bounded by
+  the distinct keys seen within TWO windows — see the idle-keys scenario.
+  REVISION 4d: this clause and the class docstring both said "one window" and
+  were literally false. Because the sweep is throttled to once per window, a
+  key can sit idle for just under 2W before the sweep that drops it runs. Only
+  the residual-risk section had it right; the idle-keys test probed at 2W, so
+  it passed under either reading and pinned neither.]
 
 ## Clock contract [REVISION 4]
 
@@ -178,7 +189,16 @@ temporal memory bound for NaN-poisoned keys**, which is stated here rather
 than left to be inferred. The third NaN injection point is the clock itself,
 and it stays a caller obligation rather than a check because validating every
 reading puts a branch on the hot path for a fault `time.monotonic` cannot
-produce.
+produce. [4d] A NaN reading also destroys the sweep throttle permanently:
+`_last_sweep` becomes NaN, every subsequent comparison against it is false,
+and the sweep then runs an O(distinct keys) scan on every request for the
+life of the process. The 4c paragraph described the never-expiring hit as if
+that were the whole mode; it is not.
+
+`clock` is the only constructor parameter with no validation. That is
+deliberate — a non-callable clock raises TypeError at the first `allow()`,
+which is loud and fail-closed, not the silent acceptance the hostile-config
+row is about. [4d]
 
 `clock` MUST NOT call back into the same limiter. [REVISION 4c] The clock is
 read inside the critical section, so a reentrant clock deadlocks on a
diff --git a/demo-rate-limiter/src/ratelimiter/__init__.py b/demo-rate-limiter/src/ratelimiter/__init__.py
index 3997c8f..2434c85 100644
--- a/demo-rate-limiter/src/ratelimiter/__init__.py
+++ b/demo-rate-limiter/src/ratelimiter/__init__.py
@@ -37,9 +37,12 @@ class RateLimiter:
     expire early. A forward jump expires every hit at once — that is a caller
     obligation, not a defect (see the clock contract in spec.md).
 
-    Safe to call from multiple threads. Memory is bounded by the number of
-    distinct keys seen within one window: keys idle for a full window are
-    dropped by a sweep that runs at most once per window.
+    Safe to call from multiple threads. Memory is bounded by the distinct
+    keys seen within TWO windows, not one: a key is dropped by the first sweep
+    that runs more than a window after its last hit, and sweeps are throttled
+    to at most one per window, so worst-case retention is just under 2W. The
+    bound is temporal, not cardinal — see the accepted residual risk in
+    spec.md.
     """
 
     def __init__(
@@ -77,7 +80,11 @@ def allow(self, key: str) -> bool:
 
     def _sweep(self, now: float) -> None:
         """Forget keys idle for a full window. Runs at most once per window."""
-        if now - self._last_sweep <= self._window:
+        # The lower bound matters: after a backward clock jump `now` sits below
+        # _last_sweep, and a one-sided `<= window` test then suspends the sweep
+        # until the clock catches up — measured 20,001 keys retained. Treating a
+        # negative delta as "sweep now" re-arms the throttle at the new time.
+        if 0 <= now - self._last_sweep <= self._window:
             return
         self._last_sweep = now
         idle = [k for k, hits in self._hits.items() if now - hits[-1] > self._window]
diff --git a/demo-rate-limiter/tests/test_properties.py b/demo-rate-limiter/tests/test_properties.py
index 13a918f..a6c0576 100644
--- a/demo-rate-limiter/tests/test_properties.py
+++ b/demo-rate-limiter/tests/test_properties.py
@@ -23,7 +23,9 @@
 # P2 needs the target key to recur, so it keeps a small pool — but the pool is
 # no longer three single characters. The widening above was applied to P1 only
 # in the first pass, directly under the comment explaining it; P2 was left
-# behind and killed none of M1/M5/M12 in attribution.
+# behind. What the widening fixed is the strip()-merge blindness (the pool held
+# "c " but not "c", so no two members could merge). It did NOT change P2's
+# attribution: measured, P2 alone still kills none of M1/M5/M12.
 isolation_keys = st.sampled_from(["a", "ab", "Ab", "b", "bc", "c", "c "])
 isolation_requests = st.lists(st.tuples(timestamps, isolation_keys), max_size=60)
 limits = st.integers(min_value=1, max_value=5)
diff --git a/demo-rate-limiter/tests/test_ratelimiter.py b/demo-rate-limiter/tests/test_ratelimiter.py
index 76d1094..b4e40da 100644
--- a/demo-rate-limiter/tests/test_ratelimiter.py
+++ b/demo-rate-limiter/tests/test_ratelimiter.py
@@ -156,6 +156,56 @@ def test_sweep_keeps_a_key_whose_newest_hit_is_exactly_window_old(
     assert limiter.allow("k") is False
 
 
+def test_the_memory_bound_is_two_windows_not_one(clock: FakeClock) -> None:
+    # The docstring and the Must NOT both said "one window" and were literally
+    # false: because the sweep is throttled, a key can stay idle for nearly two
+    # windows. The old idle-keys test probed at 2x the window, so it passed
+    # under either reading and pinned neither. This pins both sides.
+    limiter = RateLimiter(limit=5, window_seconds=60, clock=clock)
+    assert limiter.allow("armer") is True  # t=0, arms the sweep clock
+    clock.now = 1.0
+    assert limiter.allow("idle") is True  # last hit at t=1
+    clock.now = 60.9  # sweep fires: drops armer, keeps idle
+    assert limiter.allow("probe") is True
+    clock.now = 100.0  # idle for 99s — already longer than one window
+    assert limiter.allow("probe") is True
+    assert "idle" in limiter._hits, "one window is not the real bound"
+    clock.now = 121.0  # next sweep is now due
+    assert limiter.allow("probe") is True
+    assert "idle" not in limiter._hits, "two windows must be the bound"
+
+
+def test_backward_clock_skew_does_not_suspend_the_sweep(clock: FakeClock) -> None:
+    # The throttle compares now against the last sweep time. After a backward
+    # jump, now stays below it and the sweep never runs again until the clock
+    # catches up — measured 20,001 keys retained across seven windows of
+    # monotone time. The quota side fails closed under skew; the memory side
+    # did not, and no test looked at len(_hits) after a jump.
+    limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
+    clock.now = 1_000_000.0
+    assert limiter.allow("arm") is True
+    clock.now = 0.0  # clock jumps backward
+    for i in range(200):
+        clock.now = i * 2.0
+        limiter.allow(f"key-{i}")
+    assert len(limiter._hits) < 100, f"sweep suspended: {len(limiter._hits)} keys held"
+
+
+def test_the_sweep_is_throttled_to_once_per_window(clock: FakeClock) -> None:
+    # "at most once per window" carries the accepted-residual-risk argument,
+    # but nothing pinned it: deleting the throttle bookkeeping made the sweep
+    # run an O(keys) scan on every request and the whole suite stayed green.
+    limiter = RateLimiter(limit=5, window_seconds=60, clock=clock)
+    assert limiter.allow("k") is True
+    assert limiter._last_sweep == 0.0
+    clock.now = 30.0
+    assert limiter.allow("k") is True
+    assert limiter._last_sweep == 0.0, "swept again inside the same window"
+    clock.now = 61.0
+    assert limiter.allow("k") is True
+    assert limiter._last_sweep == 61.0, "did not sweep after a full window"
+
+
 def test_idle_keys_are_forgotten_key_map_is_bounded(clock: FakeClock) -> None:
     limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
     for i in range(1000):
diff --git a/demo-rate-limiter/tools/gauntlet.sh b/demo-rate-limiter/tools/gauntlet.sh
index db811b6..a20811c 100755
--- a/demo-rate-limiter/tools/gauntlet.sh
+++ b/demo-rate-limiter/tools/gauntlet.sh
@@ -37,7 +37,7 @@ echo "=== must-not scans ==="
 # they are deadlock guards in the concurrency tests, declared as an exception
 # in spec.md rather than excluded here. A pattern cannot decide intent, so the
 # spec says what the gate actually covers instead of claiming more.
-must_not_match 'import[[:space:]]+time|from[[:space:]]+time[[:space:]]+import|time\.|datetime|sleep[[:space:]]*\(|perf_counter[[:space:]]*\(|monotonic[[:space:]]*\(' tests
+must_not_match 'import[[:space:]]+time|from[[:space:]]+time[[:space:]]+import|time\.[a-zA-Z_]|datetime|sleep[[:space:]]*\(|perf_counter[[:space:]]*\(|monotonic[[:space:]]*\(' tests
 # Bracketed letters stop the pattern literal from matching itself. The path
 # list now includes CI config and metadata: workflows are where credentials
 # actually appear, and scanning only src/tests/tools/examples missed them.
diff --git a/demo-rate-limiter/tools/mutants.py b/demo-rate-limiter/tools/mutants.py
index f991c3f..ef9c8d3 100644
--- a/demo-rate-limiter/tools/mutants.py
+++ b/demo-rate-limiter/tools/mutants.py
@@ -138,6 +138,19 @@
         "if now - hits[-1] > self._window]\n",
         "if now - hits[-1] >= self._window]\n",
     ),
+    # [REVISION 4d] Round 4 found the throttle was an asserted design property
+    # with no catcher, and that a one-sided comparison suspended it entirely
+    # under backward skew.
+    (
+        "M19 drop the sweep throttle (O(keys) scan on every request)",
+        "        self._last_sweep = now\n",
+        "",
+    ),
+    (
+        "M20 one-sided sweep throttle (backward skew suspends reclamation)",
+        "if 0 <= now - self._last_sweep <= self._window:",
+        "if now - self._last_sweep <= self._window:",
+    ),
 ]
 
 

From d0b506cbcede1b5bd2b0c3ee59c0ecfab390966d Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 02:06:40 +0800
Subject: [PATCH 05/12] =?UTF-8?q?fix(demo):=20REVISION=204e=20=E2=80=94=20?=
 =?UTF-8?q?round=205=20findings;=20the=204d=20fix=20introduced=20a=20new?=
 =?UTF-8?q?=20false=20claim?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Round 5 found no behavioural defect and every executable layer fail-closed on
demand, but failed the project's own accuracy standard with one MATERIAL:

The 4d clock-contract paragraph claimed a NaN reading "destroys the sweep
throttle permanently ... an O(distinct keys) scan on every request for the
life of the process". False. _sweep unconditionally re-anchors _last_sweep
after its early return, so the next finite reading heals the throttle.
Measured: nan, then 100.0 at t=100, still 100.0 at t=101/102/110. The true
cost of one NaN reading is one extra sweep. This was written by the revision
that fixed the previous inaccuracy in the same paragraph, which is the point
worth recording: a fix round can introduce a fresh MATERIAL of the same class.

Also fixed:
- The memory bound omitted its load-bearing qualifier. Sweeping happens only
  inside allow(), so while traffic is silent nothing is reclaimed at all:
  1000 keys survive ~166,000 idle windows and drop only on the next request.
  The bound is "keys seen in the two windows preceding the most recent
  request". Now pinned by a test across an idle gap, not just asserted.
- The sweep throttle's own boundary was the last age comparison in the file
  with no test behind it (_prune's had M2, _sweep's had M18). tools/mutants.py
  had even noted the gap in passing and used it to justify a different control
  rather than closing it. Test + M21.
- The -inf sentinel had the same shape: every clock in the suite starts at 0.0
  or beyond a window, so replacing it with 0.0 was invisible. Test + M22.
- mutants.py had the two cache defences backwards. Measured three ways:
  removing the rmtree alone leaves the control green; removing
  PYTHONDONTWRITEBYTECODE alone trips the tripwire; only removing both plus
  the tripwire reproduces the misreport. DONTWRITEBYTECODE closes the leak.
- mutants.py claimed --negative-control was exercised by
  test_gauntlet_checks.sh; it is not — that script covers must_not_match only.
  A false cross-reference inside the layer meant to prove the mutation ran.
- Five tests existed only as prose while the test module claims a 1:1 map to
  spec scenarios; scenarios added. Two demonstrated failure modes from 4d had
  a test and a mutant but no failure-model row; rows added.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/spec.md                   | 64 ++++++++++++++++++---
 demo-rate-limiter/tests/test_ratelimiter.py | 27 +++++++++
 demo-rate-limiter/tools/mutants.py          | 31 ++++++++--
 3 files changed, 109 insertions(+), 13 deletions(-)

diff --git a/demo-rate-limiter/spec.md b/demo-rate-limiter/spec.md
index 6a1b983..89d702e 100644
--- a/demo-rate-limiter/spec.md
+++ b/demo-rate-limiter/spec.md
@@ -125,6 +125,43 @@ Feature: Sliding-window rate limiting per key
     When any request arrives after a full window has elapsed
     Then the limiter retains only keys with a hit inside the current window
 
+  Scenario: the key map is bounded by two windows, not one  [REVISION 4e]
+    Given a limiter with limit 5 per 60 seconds
+    And "armer" at t=0 and "idle" at t=1, then a request at t=60.9
+    When a request arrives at t=100 — "idle" has been idle for 99s
+    Then "idle" is still retained; only at t=121 is it forgotten
+    (the sweep is throttled to once per window, so worst-case retention is
+    just under 2W. The old idle-keys test probed at exactly 2W and so passed
+    under either reading, pinning neither.)
+
+  Scenario: nothing is reclaimed while traffic is silent  [REVISION 4e]
+    Given 50 one-shot keys at t=0
+    When the clock advances by ~166,000 windows and no request is made
+    Then all 50 are still resident; the map shrinks only on the next request
+    (sweeping happens inside allow(), so the bound is "keys seen in the two
+    windows preceding the most recent request", not two windows of wall time)
+
+  Scenario: the sweep is throttled to at most once per window  [REVISION 4e]
+    Given a limiter with limit 5 per 60 seconds and a request at t=0
+    When further requests arrive at t=30 and at t=60 (delta exactly one window)
+    Then no further sweep has run; the sweep at t=61 does run
+    (the throttle carries the accepted-residual-risk argument, and its own
+    boundary was the last age comparison in the file with no test behind it)
+
+  Scenario: the first call always sweeps  [REVISION 4e]
+    Given a fresh limiter with a 60-second window
+    When the very first request arrives at t=30
+    Then a sweep has run
+    (the -inf sentinel exists for exactly this; every other clock in the suite
+    starts at 0.0 or beyond a window, so a 0.0 sentinel was indistinguishable)
+
+  Scenario: a backward clock jump does not suspend reclamation  [REVISION 4e]
+    Given a limiter armed at t=1,000,000
+    When the clock jumps back to 0 and 200 one-shot keys arrive over 400s
+    Then the sweep still runs and the map does not grow without bound
+    (a one-sided throttle left `now` permanently below the last sweep time —
+    measured 20,001 keys retained across seven windows of monotone time)
+
   Scenario: concurrent callers never exceed the limit  [REVISION 4]
     Given a limiter with limit 1 per 60 seconds
     When many threads call allow() for the same key simultaneously
@@ -162,7 +199,13 @@ Feature: Sliding-window rate limiting per key
 - No unbounded memory growth. [REVISION 4: this clause used to read "from
   denied requests (denials store nothing)". Denials were never the leak;
   *allowed* requests from keys that never return were. Growth is bounded by
-  the distinct keys seen within TWO windows — see the idle-keys scenario.
+  the distinct keys seen in the TWO windows preceding the most recent
+  request — see the idle-keys scenario. The qualifier is load-bearing
+  [REVISION 4e]: sweeping happens only inside `allow()`, so while traffic is
+  silent nothing is reclaimed at all. Measured: 1000 one-shot keys, clock
+  advanced by ~166,000 windows with no requests, still 1000 keys resident;
+  the map drops to 1 only when the next request arrives. Peak resident set is
+  not released until traffic resumes.
   REVISION 4d: this clause and the class docstring both said "one window" and
   were literally false. Because the sweep is throttled to once per window, a
   key can sit idle for just under 2W before the sweep that drops it runs. Only
@@ -189,11 +232,16 @@ temporal memory bound for NaN-poisoned keys**, which is stated here rather
 than left to be inferred. The third NaN injection point is the clock itself,
 and it stays a caller obligation rather than a check because validating every
 reading puts a branch on the hot path for a fault `time.monotonic` cannot
-produce. [4d] A NaN reading also destroys the sweep throttle permanently:
-`_last_sweep` becomes NaN, every subsequent comparison against it is false,
-and the sweep then runs an O(distinct keys) scan on every request for the
-life of the process. The 4c paragraph described the never-expiring hit as if
-that were the whole mode; it is not.
+produce. [4d, corrected in 4e] A NaN reading also disturbs the sweep
+throttle, but NOT permanently: `_last_sweep` becomes NaN and every comparison
+against it is false, so the very next request sweeps — and that sweep
+unconditionally re-anchors `_last_sweep` to a finite value, after which the
+throttle behaves normally. Measured: nan, then 100.0 at t=100, still 100.0 at
+t=101/102/110. The total cost of one NaN reading is **one extra sweep**. The
+4d text claimed an unbounded per-request scan "for the life of the process";
+that was false, and it was written by the revision that fixed the previous
+inaccuracy in this same paragraph. (A clock stuck at NaN forever is a
+different matter and is not what that sentence described.)
 
 `clock` is the only constructor parameter with no validation. That is
 deliberate — a non-callable clock raises TypeError at the first `allow()`,
@@ -245,7 +293,9 @@ shown to fail is a defect, not a mapping.]
 | concurrent commits inverted against the clock read | clock-ordering scenario (gated clock forces two callers to read different values); mutant M16 killed. [4c: the lock covered check-and-append but not the clock read. Both earlier concurrency tests held time constant, so no test could tell the two placements apart] |
 | unbounded memory growth (any path) | idle-keys scenario + denials test; mutants M8/M12 killed |
 | concurrent callers racing on shared state | **fault injection**: the atomicity test constructs the interleaving and kills M13 deterministically. The threaded stress test corroborates statistically (measured 5.9% per-round detection, 400 rounds) but cannot be the sole catcher — at 60 rounds the lock-removal mutant was observed surviving 1 run in 50 |
-| the mutation layer reporting kills it never ran | **negative control**: a killer and a strictly-equivalent mutant of identical size under one pinned mtime; proven non-vacuous by removing the cache defence and watching the control go red [4b] |
+| the mutation layer reporting kills it never ran | **negative control**: a killer and a strictly-equivalent mutant of identical size under one pinned mtime. Non-vacuity measured three ways [4e]: removing the rmtree alone leaves it green, removing PYTHONDONTWRITEBYTECODE alone trips a RuntimeError tripwire, and removing both plus the tripwire produces the advertised misreport. The 4b wording credited the rmtree; DONTWRITEBYTECODE is what closes the leak |
+| the sweep degrading to an O(distinct keys) scan per request (availability) | throttle scenario + first-call scenario; mutants M19/M21/M22 killed [4e] |
+| backward skew suspending memory reclamation | backward-jump scenario; mutant M20 killed. [4e: the skew row above covers the quota side only — "fails closed" was true of quota and false of memory] |
 | untested code reaching production | coverage layer, now a gate (`--cov-fail-under=100`) — it previously printed a number and could not fail |
 | silent failure in production | n-a: library returns a bool the caller observes directly |
 
diff --git a/demo-rate-limiter/tests/test_ratelimiter.py b/demo-rate-limiter/tests/test_ratelimiter.py
index b4e40da..4912ecd 100644
--- a/demo-rate-limiter/tests/test_ratelimiter.py
+++ b/demo-rate-limiter/tests/test_ratelimiter.py
@@ -175,6 +175,30 @@ def test_the_memory_bound_is_two_windows_not_one(clock: FakeClock) -> None:
     assert "idle" not in limiter._hits, "two windows must be the bound"
 
 
+def test_the_first_call_always_sweeps(clock: FakeClock) -> None:
+    # The -inf sentinel exists so the first call is never throttled. Every
+    # other clock in the suite starts at 0.0 or past a full window, so a
+    # sentinel of 0.0 would have been indistinguishable.
+    limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
+    clock.now = 30.0
+    assert limiter.allow("k") is True
+    assert limiter._last_sweep == 30.0, "first call did not sweep"
+
+
+def test_memory_is_not_reclaimed_while_traffic_is_silent(clock: FakeClock) -> None:
+    # The sweep runs only inside allow(), so the bound is "keys seen in the two
+    # windows preceding the most recent request" — not two windows of wall
+    # time. Every other memory test probes after issuing a request, which is
+    # exactly the case the lazy sweep handles.
+    limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
+    for i in range(50):
+        assert limiter.allow(f"k{i}") is True
+    clock.now = 10_000_000.0  # ~166,000 windows pass with no traffic
+    assert len(limiter._hits) == 50, "nothing is reclaimed without a request"
+    assert limiter.allow("probe") is True
+    assert len(limiter._hits) == 1
+
+
 def test_backward_clock_skew_does_not_suspend_the_sweep(clock: FakeClock) -> None:
     # The throttle compares now against the last sweep time. After a backward
     # jump, now stays below it and the sweep never runs again until the clock
@@ -201,6 +225,9 @@ def test_the_sweep_is_throttled_to_once_per_window(clock: FakeClock) -> None:
     clock.now = 30.0
     assert limiter.allow("k") is True
     assert limiter._last_sweep == 0.0, "swept again inside the same window"
+    clock.now = 60.0  # delta is exactly one window: still throttled
+    assert limiter.allow("k") is True
+    assert limiter._last_sweep == 0.0, "swept at the boundary; <= means <="
     clock.now = 61.0
     assert limiter.allow("k") is True
     assert limiter._last_sweep == 61.0, "did not sweep after a full window"
diff --git a/demo-rate-limiter/tools/mutants.py b/demo-rate-limiter/tools/mutants.py
index ef9c8d3..87e6e32 100644
--- a/demo-rate-limiter/tools/mutants.py
+++ b/demo-rate-limiter/tools/mutants.py
@@ -23,11 +23,14 @@
 # original and adjacent in the list, so M5 -- the fail-open mutant -- was
 # reported KILLED on the strength of M4's code. The bias is toward inflating
 # the kill count, which can never surface as a red gauntlet. Both defences are
-# needed, but not symmetrically. DONTWRITEBYTECODE alone leaves the negative
-# control green: with no .pyc written during the run, a stale one can only be
-# the pristine pre-run file, which biases toward a false SURVIVED — a red
-# gauntlet, not a silent inflation. Removing it is caught by a separate
-# tripwire below. The rmtree is what closes the between-mutants leak.
+# needed only as a belt-and-braces pair, and an earlier version of this
+# comment had the roles backwards. Measured three ways: removing the rmtree
+# alone leaves the control green; removing DONTWRITEBYTECODE alone trips the
+# tripwire below with a RuntimeError; only removing both AND the tripwire
+# reproduces the misreport. DONTWRITEBYTECODE is what actually closes the
+# leak — with no .pyc written during a run there is nothing to inherit — and
+# gauntlet.sh clears __pycache__ before the layer starts anyway. The rmtree
+# covers the case of running this script directly on a dirty tree.
 MUTANT_ENV = {**os.environ, "PYTHONDONTWRITEBYTECODE": "1"}
 
 MUTANTS = [
@@ -151,6 +154,20 @@
         "if 0 <= now - self._last_sweep <= self._window:",
         "if now - self._last_sweep <= self._window:",
     ),
+    # [REVISION 4e] The throttle's own boundary was the last age comparison in
+    # the file with no test behind it -- _prune's had M2, _sweep's had M18.
+    # The sentinel had the same shape: every clock in the suite starts at 0.0
+    # or beyond a window, so its purpose was structurally invisible.
+    (
+        "M21 sweep-throttle boundary <= to < (sweeps early, delays cleanup)",
+        "if 0 <= now - self._last_sweep <= self._window:",
+        "if 0 <= now - self._last_sweep < self._window:",
+    ),
+    (
+        "M22 sweep sentinel -inf to 0.0 (first call skips its sweep)",
+        "self._last_sweep = -math.inf",
+        "self._last_sweep = 0.0",
+    ),
 ]
 
 
@@ -158,7 +175,9 @@
 # one byte shorter than the original), a killer followed by a proven-equivalent
 # one. If bytecode caching ever leaks between runs again, the equivalent mutant
 # inherits the killer's result and is misreported as KILLED. Run with
-# --negative-control; exercised by tools/test_gauntlet_checks.sh.
+# --negative-control; run as a gate by tools/gauntlet.sh before the real
+# mutation pass. (It is NOT part of test_gauntlet_checks.sh, which covers
+# must_not_match only — an earlier comment here claimed otherwise.)
 # Both mutations are length-preserving, so the two mutated files are the same
 # size; with a pinned mtime the (mtime, size) collision is constructed, not
 # waited for. C2 must be STRICTLY equivalent: `or` over two side-effect-free

From 66df5cd3b100c0fd598adb0d443658f47ea811ed Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 02:22:53 +0800
Subject: [PATCH 06/12] =?UTF-8?q?fix(demo):=20REVISION=204f=20=E2=80=94=20?=
 =?UTF-8?q?round=206;=20last=20fix=20round,=20verification=20stops=20here?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Round 6 found no fail-open and no surviving mutant that changes an allow/deny
outcome, but two findings had teeth:

- _sweep's idle threshold had its BOUNDARY pinned (M18 kills >=) and its
  MAGNITUDE unpinned: `> window * 1.5`, and even `* 1.99`, left 40 tests, 100%
  coverage and 21/21 mutants green while inflating the human-approved
  two-window retention bound by up to 50%. Every memory test asserted deletion
  only at age >= 2W, so any threshold in (W, 2W) satisfied all of them. The
  twin function's magnitude WAS pinned; this one was not. Test + M23.
- test_clock_is_read_inside_the_critical_section asserted only that the deque
  was sorted. A one-element list is trivially sorted, so a second caller that
  died satisfied it vacuously — demonstrated with a double-clock-read mutant
  that raised out of the gated clock while the test still reported 1 passed.
  It now asserts both callers committed.

Prose corrections, all mine:
- "worst-case retention is just under 2W" is false; 2W is attained, and the
  sweep that drops a key runs strictly later than 2W after its last hit.
- The stress test's per-round detection rate was quoted as 5.9%. Re-measured
  against the real source mutant rather than a Python replica: 3.7% here, so
  the 400-round miss probability is ~3e-7, not 3e-11. Now marked
  machine-dependent.
- The negative control's comment said its mutants are "each one byte shorter
  than the original" and, nine lines later, "length-preserving". The second is
  true; the first describes M4/M5.
- The time-scan comment justified its pattern partly with an invented claim
  (that a word-boundary pattern would fire on test_non_monotonic_clock_*,
  a name containing no "time").
- The test module claimed a 1:1 test-to-scenario map; it is 24 tests to 22
  scenarios, the rest mapping to a Must NOT or a failure-model row.
- The silent-traffic measurement quotes 1000 keys where the scenario uses 50.

Six rounds of fresh-context verification stop here. Rounds 1-3 found five
behavioural defects; rounds 4-6 found one behavioural gap and a steady stream
of prose inaccuracies, two of which were introduced by the round that fixed
the previous one. Remaining known items are disclosed in evidence.md rather
than chased, because a rule of "fix every finding, then re-verify" only
terminates when a round returns the empty set, and prose has no such fixpoint.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/spec.md                   | 15 +++++++++++----
 demo-rate-limiter/tests/test_ratelimiter.py | 21 ++++++++++++++++++++-
 demo-rate-limiter/tools/gauntlet.sh         |  9 ++++++---
 demo-rate-limiter/tools/mutants.py          | 17 ++++++++++++++---
 4 files changed, 51 insertions(+), 11 deletions(-)

diff --git a/demo-rate-limiter/spec.md b/demo-rate-limiter/spec.md
index 89d702e..4bcb8b7 100644
--- a/demo-rate-limiter/spec.md
+++ b/demo-rate-limiter/spec.md
@@ -200,10 +200,17 @@ Feature: Sliding-window rate limiting per key
   denied requests (denials store nothing)". Denials were never the leak;
   *allowed* requests from keys that never return were. Growth is bounded by
   the distinct keys seen in the TWO windows preceding the most recent
-  request — see the idle-keys scenario. The qualifier is load-bearing
+  request — see the idle-keys scenario. Precisely [REVISION 4f]: a key is
+  resident at an age of at most exactly 2W when any request is observed, and
+  the sweep that drops it runs strictly LATER than 2W after its last hit.
+  Earlier wording said "just under 2W", which is false in both readings —
+  2W is attained (armer t=0, idle t=40, probes at t=100 and t=160 leave idle
+  resident at age exactly 120.0). The qualifier below is load-bearing
   [REVISION 4e]: sweeping happens only inside `allow()`, so while traffic is
-  silent nothing is reclaimed at all. Measured: 1000 one-shot keys, clock
-  advanced by ~166,000 windows with no requests, still 1000 keys resident;
+  silent nothing is reclaimed at all. Measured with 1000 one-shot keys, clock
+  advanced by ~166,000 windows with no requests, still 1000 keys resident
+  (the scenario and its test use 50, which is the same behaviour at a size
+  that keeps the suite fast);
   the map drops to 1 only when the next request arrives. Peak resident set is
   not released until traffic resumes.
   REVISION 4d: this clause and the class docstring both said "one window" and
@@ -292,7 +299,7 @@ shown to fail is a defect, not a mapping.]
 | a caller's quota reset by the sweep at the exact boundary | sweep-boundary scenario; mutant M18 killed [4c] |
 | concurrent commits inverted against the clock read | clock-ordering scenario (gated clock forces two callers to read different values); mutant M16 killed. [4c: the lock covered check-and-append but not the clock read. Both earlier concurrency tests held time constant, so no test could tell the two placements apart] |
 | unbounded memory growth (any path) | idle-keys scenario + denials test; mutants M8/M12 killed |
-| concurrent callers racing on shared state | **fault injection**: the atomicity test constructs the interleaving and kills M13 deterministically. The threaded stress test corroborates statistically (measured 5.9% per-round detection, 400 rounds) but cannot be the sole catcher — at 60 rounds the lock-removal mutant was observed surviving 1 run in 50 |
+| concurrent callers racing on shared state | **fault injection**: the atomicity test constructs the interleaving and kills M13 deterministically. The threaded stress test corroborates statistically (per-round detection measured against the real source mutant at 3.7% on this machine — an earlier 5.9% came from a Python replica, not the mutant; 400 rounds puts the miss probability near 3e-7, and the rate is machine-dependent) but cannot be the sole catcher — at 60 rounds the lock-removal mutant was observed surviving 1 run in 50 |
 | the mutation layer reporting kills it never ran | **negative control**: a killer and a strictly-equivalent mutant of identical size under one pinned mtime. Non-vacuity measured three ways [4e]: removing the rmtree alone leaves it green, removing PYTHONDONTWRITEBYTECODE alone trips a RuntimeError tripwire, and removing both plus the tripwire produces the advertised misreport. The 4b wording credited the rmtree; DONTWRITEBYTECODE is what closes the leak |
 | the sweep degrading to an O(distinct keys) scan per request (availability) | throttle scenario + first-call scenario; mutants M19/M21/M22 killed [4e] |
 | backward skew suspending memory reclamation | backward-jump scenario; mutant M20 killed. [4e: the skew row above covers the quota side only — "fails closed" was true of quota and false of memory] |
diff --git a/demo-rate-limiter/tests/test_ratelimiter.py b/demo-rate-limiter/tests/test_ratelimiter.py
index 4912ecd..f5c9cf0 100644
--- a/demo-rate-limiter/tests/test_ratelimiter.py
+++ b/demo-rate-limiter/tests/test_ratelimiter.py
@@ -1,4 +1,5 @@
-"""Scenario tests — each test name maps 1:1 to a spec.md scenario."""
+"""Scenario tests. Most map 1:1 to a spec.md scenario; the rest map to a
+Must NOT clause or to a failure-model row (24 tests, 22 scenarios)."""
 
 import math
 import sys
@@ -156,6 +157,21 @@ def test_sweep_keeps_a_key_whose_newest_hit_is_exactly_window_old(
     assert limiter.allow("k") is False
 
 
+def test_a_key_is_dropped_by_the_first_sweep_after_one_idle_window(
+    clock: FakeClock,
+) -> None:
+    # _sweep's boundary was pinned (M18 kills >=) but its MAGNITUDE was not:
+    # `> window * 1.5` and even `* 1.99` left the whole gauntlet green while
+    # inflating the approved two-window bound to three. Every memory test
+    # asserted deletion only at age >= 2W, so any threshold in (W, 2W) passed.
+    limiter = RateLimiter(limit=5, window_seconds=60, clock=clock)
+    assert limiter.allow("armer") is True  # t=0, arms the sweep clock
+    assert limiter.allow("idle") is True  # t=0
+    clock.now = 61.0  # first sweep after t=0; idle is 61s old, one window+
+    assert limiter.allow("probe") is True
+    assert "idle" not in limiter._hits, "idle threshold is larger than a window"
+
+
 def test_the_memory_bound_is_two_windows_not_one(clock: FakeClock) -> None:
     # The docstring and the Must NOT both said "one window" and were literally
     # false: because the sweep is throttled, a key can stay idle for nearly two
@@ -339,6 +355,9 @@ def second_caller() -> None:
     first.join(timeout=5)
     second.join(timeout=5)
     hits = list(limiter._hits["k"])
+    # Both assertions matter: a one-element list is trivially sorted, so a
+    # second caller that died would satisfy the ordering check vacuously.
+    assert len(hits) == 2, f"a caller never committed: {hits}"
     assert hits == sorted(hits), f"commits inverted, deque unsorted: {hits}"
 
 
diff --git a/demo-rate-limiter/tools/gauntlet.sh b/demo-rate-limiter/tools/gauntlet.sh
index a20811c..81ae35a 100755
--- a/demo-rate-limiter/tools/gauntlet.sh
+++ b/demo-rate-limiter/tools/gauntlet.sh
@@ -27,9 +27,12 @@ echo "=== supply chain ==="
 "$PY/pip-audit" -r requirements-dev.txt
 echo "=== must-not scans ==="
 # Matches usage forms, not the word: `time\.` alone missed `from time import
-# sleep`. Deliberately not `[[:<:]]time`, which would fire on conftest's own
-# "No real time in tests" docstring and on test_non_monotonic_clock_* — the
-# fix belongs in the pattern, never in an exclusion.
+# sleep`. Deliberately not `[[:<:]]time`, which fires on conftest's own "No
+# real time in tests" docstring, on `timestamps`, on `timeout=` and on prose
+# like "hold time constant" — the fix belongs in the pattern, never in an
+# exclusion. (An earlier version of this comment also claimed it would fire on
+# test_non_monotonic_clock_*; that was invented — the name has no "time" in
+# it at all.)
 #
 # Scope is deliberately narrower than the Must NOT's ambition: it catches real
 # time being read or slept on, not every way a test could depend on wall
diff --git a/demo-rate-limiter/tools/mutants.py b/demo-rate-limiter/tools/mutants.py
index 87e6e32..9fb7c75 100644
--- a/demo-rate-limiter/tools/mutants.py
+++ b/demo-rate-limiter/tools/mutants.py
@@ -168,12 +168,23 @@
         "self._last_sweep = -math.inf",
         "self._last_sweep = 0.0",
     ),
+    # [REVISION 4f] The idle threshold's boundary was pinned but its magnitude
+    # was not: 1.5x and 1.99x both survived the entire gauntlet, inflating the
+    # approved two-window bound by up to 50%.
+    (
+        "M23 inflate the idle threshold 1.5x (retention bound silently grows)",
+        "if now - hits[-1] > self._window]\n",
+        "if now - hits[-1] > self._window * 1.5]\n",
+    ),
 ]
 
 
-# Negative control for the harness itself: two mutants of IDENTICAL size (each
-# one byte shorter than the original), a killer followed by a proven-equivalent
-# one. If bytecode caching ever leaks between runs again, the equivalent mutant
+# Negative control for the harness itself: two mutants of IDENTICAL size, a
+# killer followed by a proven-equivalent one. (Both are length-PRESERVING, so
+# all three files are the same size; an earlier version of this comment also
+# said "each one byte shorter than the original", which describes M4/M5, not
+# these. Only C1 == C2 matters for the collision.)
+# If bytecode caching ever leaks between runs again, the equivalent mutant
 # inherits the killer's result and is misreported as KILLED. Run with
 # --negative-control; run as a gate by tools/gauntlet.sh before the real
 # mutation pass. (It is NOT part of test_gauntlet_checks.sh, which covers

From 680c67e87673a8377d6f8561163116a90a7fc773 Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 02:26:22 +0800
Subject: [PATCH 07/12] evidence: rebind to 66df5cd after six verification
 rounds

Numbers from one fresh run at commit 66df5cd / tree 402ed5f682f8543f:
41 tests, 100% branch coverage (gated), 22/22 mutants with the harness
negative control green, all layers clean.

Records what the six fresh-context rounds cost and produced, that the A/B
design failed, that verification was stopped deliberately rather than run to
a fixpoint, and which post-round-6 fixes are therefore unverified.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/evidence.md | 240 ++++++++++++++++++++++------------
 1 file changed, 160 insertions(+), 80 deletions(-)

diff --git a/demo-rate-limiter/evidence.md b/demo-rate-limiter/evidence.md
index e95bbc3..0482769 100644
--- a/demo-rate-limiter/evidence.md
+++ b/demo-rate-limiter/evidence.md
@@ -1,15 +1,22 @@
 # Evidence Report — Sliding-Window Rate Limiter (Tier 3)
 
-- Spec approval: **not obtained (autonomous run)** — confidence claim is
-  correspondingly reduced; `spec.md` is the artifact to review after the fact.
-- Source state: git commit `d6e17b1`; sha256 tree hash `50433e0a4acc8507` —
-  reproduce both with `./tools/source_state.sh` (works from any directory).
+- Spec approval: **obtained** for REVISION 4 (2026-08-09) — the human approved
+  each contract change item by item before implementation. Earlier revisions
+  (2026-07-25, 2026-07-27) were autonomous and are still unapproved; treat
+  them as the weaker part of the spec.
+- Independent verification: **six fresh-context rounds**, the last against
+  commit `d0b506c`. See "Independent verification" below — including what the
+  final round found and what was deliberately left unfixed.
+- Source state: git commit `66df5cd`; sha256 tree hash `402ed5f682f8543f` —
+  reproduce both with `./tools/source_state.sh` (works from any directory;
+  now includes `.github/workflows`, which decides whether the gauntlet runs
+  in CI at all).
 - Toolchain: pinned in `requirements-dev.txt` (local run: Python 3.14.3;
   CI runs the same gauntlet on 3.12 via `.github/workflows/gauntlet.yml`).
 - Entry point: `./tools/gauntlet.sh` reruns every layer below.
 
 All numbers are from one final fresh run of the entry point, executed
-2026-08-08 after the last code edit.
+2026-08-10 after the last code edit.
 
 ## Spec → Test mapping
 
@@ -23,97 +30,170 @@ Status legend: pass / fail / unverified / n-a.
 | window slides — old requests expire individually | test_ratelimiter.py::test_window_slides_old_requests_expire_individually | pass |
 | keys are isolated | test_ratelimiter.py::test_keys_are_isolated | pass |
 | invalid construction is rejected | test_ratelimiter.py::test_invalid_construction_is_rejected (4 params) | pass |
-| non-finite window is rejected (spec revision) | test_ratelimiter.py::test_non_finite_window_is_rejected (3 params) | pass |
+| non-finite window is rejected | test_ratelimiter.py::test_non_finite_window_is_rejected (3 params) | pass |
 | non-monotonic clock does not grant extra quota | test_ratelimiter.py::test_non_monotonic_clock_does_not_grant_extra_quota | pass |
-| request at the exact window boundary is still limited (spec revision 2) | test_ratelimiter.py::test_request_at_exact_window_boundary_is_still_limited + mutant M2 | pass |
+| request at the exact window boundary is still limited | test_ratelimiter.py::test_request_at_exact_window_boundary_is_still_limited + M2 | pass |
+| limit must be a finite positive integer (R4) | test_ratelimiter.py::test_limit_must_be_a_finite_positive_integer (5 params) + M9 | pass |
+| window_seconds must be a number (R4b) | test_ratelimiter.py::test_window_seconds_must_be_a_number (3 params) + M15 | pass |
+| key must be a non-empty string (R4) | test_ratelimiter.py::test_key_must_be_a_non_empty_string (4 params) | pass |
+| keys are compared as exact strings (R4b/4c) | test_ratelimiter.py::test_keys_are_compared_as_exact_strings + M14/M17 | pass |
+| sweep keeps a key exactly one window old (R4c) | test_ratelimiter.py::test_sweep_keeps_a_key_whose_newest_hit_is_exactly_window_old + M18 | pass |
+| a key is dropped by the first sweep after one idle window (R4f) | test_ratelimiter.py::test_a_key_is_dropped_by_the_first_sweep_after_one_idle_window + M23 | pass |
+| the key map is bounded by two windows, not one (R4e) | test_ratelimiter.py::test_the_memory_bound_is_two_windows_not_one | pass |
+| nothing is reclaimed while traffic is silent (R4e) | test_ratelimiter.py::test_memory_is_not_reclaimed_while_traffic_is_silent | pass |
+| the sweep is throttled to at most once per window (R4e) | test_ratelimiter.py::test_the_sweep_is_throttled_to_once_per_window + M19/M21 | pass |
+| the first call always sweeps (R4e) | test_ratelimiter.py::test_the_first_call_always_sweeps + M22 | pass |
+| a backward clock jump does not suspend reclamation (R4e) | test_ratelimiter.py::test_backward_clock_skew_does_not_suspend_the_sweep + M20 | pass |
+| idle keys are forgotten — the key map is bounded (R4) | test_ratelimiter.py::test_idle_keys_are_forgotten_key_map_is_bounded + M12 | pass |
+| concurrent callers never exceed the limit (R4) | test_ratelimiter.py::test_concurrent_callers_never_exceed_the_limit (statistical; see notes) | pass |
+| concurrent commits never invert against the clock read (R4c) | test_ratelimiter.py::test_clock_is_read_inside_the_critical_section + M16 | pass |
 | Invariant P1 (window count ≤ limit) | test_properties.py::test_p1_allowed_count_within_any_window_never_exceeds_limit | pass |
 | Invariant P2 (key independence) | test_properties.py::test_p2_other_keys_traffic_never_changes_one_keys_outcomes | pass |
-| Must NOT: denials store nothing (no memory growth) | test_ratelimiter.py::test_must_not_denials_store_nothing + mutant M8 | pass |
-| Must NOT: no real sleep/wall-clock in tests | layer: must-not scan in `tools/gauntlet.sh` (`time\.` over tests/) → no matches (FakeClock only) | pass |
+| Must NOT: denials store nothing (no memory growth) | test_ratelimiter.py::test_must_not_denials_store_nothing + M8 | pass |
+| Must NOT: the limiter is never driven by a real clock | layer: must-not scan in `tools/gauntlet.sh` over tests/ → no matches | pass |
+| failure-model row: allow() is atomic | test_ratelimiter.py::test_allow_is_atomic_a_second_caller_cannot_interleave + M13 | pass |
 
 ## Gauntlet (final fresh run: `./tools/gauntlet.sh`)
 
 | Layer | Command | Result |
 |---|---|---|
 | Checker self-test | `sh tools/test_gauntlet_checks.sh` (first layer; asserts the must-not scan fails on a planted pattern, passes on a clean tree, and fails closed with a distinct rc 2 when the scan itself breaks) | 3/3 expectations ok |
-| Tests | `pytest -q --cov=ratelimiter` | 17 passed, 0 failed |
+| Mutation harness negative control | `python tools/mutants.py --negative-control` (a killer and a strictly-equivalent mutant of identical size under one pinned mtime) | C1 KILLED, C2 SURVIVED — ok |
+| Tests | `pytest -q --cov=ratelimiter` | 41 passed, 0 failed |
 | Types | `mypy src tests examples tools` (strict) | 0 errors in 6 files |
-| Lint + format + complexity | `ruff check . && ruff format --check .` (includes mccabe complexity budget ≤ 8) | 0 warnings, 8 files formatted |
-| Changed-line coverage | `pytest --cov … --cov-report=term-missing` | 29/29 statements, 10/10 branches (100%; entire module is new, so changed lines = all lines) |
-| Mutation | `python tools/mutants.py` (manual, scripted; only pytest exit 1 counts as a kill — error exits are flagged, never counted) | 8/8 killed |
+| Lint + format + complexity | `ruff check . && ruff format --check .` (mccabe ≤ 8) | 0 warnings, 8 files formatted |
+| Changed-line coverage | `pytest --cov … --cov-fail-under=100` | 49/49 statements, 20/20 branches (100%). **This layer is a gate**; before 2026-08-09 it printed a percentage and exited 0 no matter how far coverage fell |
+| Mutation | `python tools/mutants.py` (manual, scripted; only pytest exit 1 counts as a kill; `__pycache__` cleared and `PYTHONDONTWRITEBYTECODE` set per mutant) | 22/22 killed |
 | Property-based | hypothesis, 2 properties | 100 examples each, 0 falsified |
 | Real execution | `python examples/demo.py` (real `time.monotonic`) | burst of 5 → `[True, True, True, False, False]`; other key unaffected; allowed again after window |
-| Supply chain | `pip-audit -r requirements-dev.txt` | no known vulnerabilities; runtime dependencies: **none** (stdlib only), dev toolchain pinned & justified in spec setup plan |
-| Secret scan | must-not scan in `tools/gauntlet.sh` (api key / secret / password / token / private key over src, tests, tools, examples) | clean, no matches |
-| License check | — | n-a: zero runtime dependencies, nothing redistributed beyond this repo's own MIT code; dev tools are not shipped |
-| Suite health | pytest-randomly (order shuffled every run; seed printed in non-quiet runs) | 17 passed in randomized order |
+| Supply chain | `pip-audit -r requirements-dev.txt` | no known vulnerabilities; runtime dependencies: **none** (stdlib only; `threading` is stdlib) |
+| Secret scan | must-not scan in `tools/gauntlet.sh` over src, tests, tools, examples, spec.md, pyproject.toml, requirements-dev.txt and `../.github` | clean, no matches |
+| License check | — | n-a: zero runtime dependencies, nothing redistributed beyond this repo's own MIT code |
+| Suite health | pytest-randomly (order shuffled every run) | 41 passed in randomized order, 10/10 consecutive runs |
+
+## Layer attribution
+
+- Property suite alone: **3/22** mutants killed (M1, M3, M5). The properties
+  are single-threaded and never construct an invalid limiter, so validation,
+  key-identity, memory, sweep and concurrency mutants are all outside their
+  reach by construction.
+- Scenario suite alone: **22/22**. The headline mutation score is carried
+  entirely by the scenario tests.
 
 ## Skipped layers
 
 - Tool-based mutation (mutmut): unverified compatibility with Python 3.14;
-  replaced with the scripted manual procedure (`tools/mutants.py`, 8 mutants:
-  comparison flips, boundary off-by-ones, dropped statements, fail-open
-  inversion, wrong-end pruning, dropped validation, denial-side write).
+  replaced with the scripted manual procedure (`tools/mutants.py`, 22 mutants).
+- Shell lint (shellcheck) for the four scripts that implement half the gates:
+  **not run**, no tool installed. Every Python file gets three static layers
+  and the shell gets none. Known gap, raised by verification round 4.
+
+## Independent verification
+
+Six rounds, each a fresh agent context given only the task contract, the
+approved SPEC, the repository at an exact source state, and the gauntlet entry
+point — never the builder's reasoning, and never the draft of this report.
+Each ran against a different commit; a round that raised a finding never
+judged its own fix.
+
+| Round | Commit | Behavioural defects | Description / mapping defects | Verdict |
+|---|---|---|---|---|
+| 1 (two arms) | `9540d72` | 3 material, found by both arms independently | 2 | failed |
+| 2 | `e677832` | 1 material (the mutation harness) | 5 | failed |
+| 3 | `e210594` | 1 material (lock scope) | 6 | failed |
+| 4 | `49afb2b` | 1 (backward skew) | 3 | passed |
+| 5 | `d65acbe` | 0 | 6 (1 rated material) | failed |
+| 6 | `d0b506c` | 1 gap (sweep threshold magnitude) | 6 | failed |
+
+What rounds 1–3 found, none of which the ten green layers could reach: a
+one-shot-key memory leak usable as a remote DoS against the component meant
+to *prevent* one; `limit=NaN`/`inf` producing a limiter that always allows;
+2× over-allow under threads; and a mutation runner reporting kills for
+mutants it never executed.
+
+Rounds 4–6 found one behavioural gap and a steady stream of inaccuracies in
+the prose — and **two of those were introduced by the round that fixed the
+previous one**. That is the honest shape of the result: verification does not
+converge just because one round comes back clean.
+
+**Verification stopped after round 6, deliberately.** A rule of "fix every
+finding, then start a new verifier" only terminates when a round returns the
+empty set, and prose has no such fixpoint. The findings below were fixed after
+round 6 and are therefore **not independently verified**:
+
+- the sweep threshold magnitude test and mutant M23;
+- the vacuous-pass assertion added to the clock-ordering test;
+- the six prose corrections listed in commit `66df5cd`.
 
 ## Honest notes
 
-- **Spec approval was never obtained**: the demo ran autonomously, so the
-  spec/tests/implementation/evidence share one author and the
-  correlation-breaking human review has not happened. Treat `spec.md` as the
-  review surface.
-- Three scenario tests passed immediately when written (**keys are isolated**,
-  **non-monotonic clock**, **Must NOT: denials store nothing**): the per-key
-  deque design provides these inherently. Each was proven non-vacuous by a
-  targeted mutant run (M5/M6/M8 respectively — M8 was run against the new test
-  alone and killed).
-- **Spec revision during the task**: the Tier 3 adversarial pass found that
-  `window_seconds=NaN` passed the original `<= 0` validation; the spec was
-  revised visibly, a RED test watched failing, then the finiteness check
-  implemented (killed as M7).
-- **Layer attribution** (fresh, 2026-07-27, all 8 mutants): mutants vs the
-  property suite alone give 3/8 killed (M1, M3, M5). Survivors and why:
-  M4/M7 (validation — properties never construct invalid limiters), M2
-  (exact boundary — stochastic inputs rarely hit it), M6/M8 (fail-closed
-  direction — P1 is one-sided, "never exceeds limit" cannot catch
-  under-allowing or hidden writes). The headline 8/8 is carried by the
-  scenario tests; a lower-bound property remains a known improvement.
-- **Flaky kill found on rerun** (2026-07-27): M2's kill turned out to depend
-  on hypothesis randomly hitting the exact `age == window` boundary — a rerun
-  reported it SURVIVED. Fixed properly: spec revision 2 added the boundary
-  behavior, a deterministic test was written and proven non-vacuous against
-  M2 alone. Property-based kills are stochastic; deterministic behaviors
-  deserve deterministic tests.
-- **Checker negative controls** (2026-08-06, prompted by a community issue on
-  fail-open checkers): the two must-not greps were folded into
-  `tools/gauntlet.sh` with explicit exit-code handling (grep rc 1 = pass,
-  rc 0 = forbidden pattern found, rc ≥ 2 = broken check — both fail). Each
-  failure branch was proven able to fire with one-off controls: a planted
-  `time.sleep` fixture (failed as required), a chmod-000 unreadable file
-  (failed closed), a nonexistent scan path (failed closed); fixtures removed
-  after. Those one-off controls are now standing: `tools/test_gauntlet_checks.sh`
-  runs as the gauntlet's first layer and asserts all three outcomes against the
-  real `must_not_match` sourced from `tools/must_not_match.sh`, so a regression
-  in the helper fails the run rather than passing vacuously (contributed in
-  PR #3). Post-merge tightening (2026-08-08): the broken-scan branch now
-  returns rc 2, distinct from the pattern-present rc 1, and the self-test
-  asserts the distinction — so a regression that mixes up the two failure
-  branches cannot pass either. Proven non-vacuous with a throwaway mutant:
-  reverting the helper to `return 1` made the self-test fail as required
-  (want rc 2, got rc 1), then the helper was restored. During the fold-in
-  the secret scan caught its own pattern literal in
-  the script — a true positive, resolved by bracketing letters in the pattern
-  (`s[e]cret`), not by excluding the file. This repo's own history includes a
-  fail-open checker: `tools/mutants.py` originally counted any nonzero pytest
-  exit as a kill, so usage errors (exit 4/5) would have faked whole-batch
-  kills; fixed earlier (only exit 1 counts, errors invalidate the run).
-- **Git history note**: the demo originally ran without git (restores were
-  verified by suite rerun + tree hash). The repo is now under git; source
-  state above cites the commit.
-- **Spec revision 3 is a retrofit** (2026-07-27): the failure-model and
-  setup-plan sections were added after implementation to comply with the
-  current skill; the original setup was authorized conversationally, not via
-  spec approval. The failure-mode→layer mapping was reconstructed, not
-  design-driven — a fresh Tier 3 task would write it first.
-- Remaining known limits (out of spec scope): not thread-safe (no locking —
-  named in the failure model as the uncovered mode); a NaN-returning *clock*
-  fails closed but is not rejected.
+- **The A/B experiment that started this failed.** The design was to plant a
+  defect in one copy and verify a clean copy as a false-positive control. The
+  "clean" arm was not clean: it independently invented the exact mutation that
+  had been planted in the other arm and reported it as a real finding, which
+  it was. The planted defect only made an existing spec/test hole explicit,
+  so the arms were not distinguishable and no false-positive rate could be
+  measured. This is an exploratory adversarial case study, not a successful
+  A/B benchmark, and nothing here supports a general claim about verifier
+  accuracy. Two false positives did occur, both caused by the harness feeding
+  a subdirectory instead of the repository and a tree polluted by an editable
+  install — verifier noise was a function of input quality, on n=2.
+- **All six verifier rounds ran on the same model as the builder.** Their
+  convergence shows the findings are reproducible, not that they are
+  independent of model bias. The correlation this breaks is context, not
+  model.
+- **The concurrency scenario's stress test is statistical.** Per-round
+  detection against the real source mutant measured 3.7% on this machine
+  (an earlier 5.9% in this report came from a Python replica rather than the
+  mutant); at 400 rounds the miss probability is ~3e-7, and the rate is
+  machine-dependent. It is deliberately **not** the catcher for that row —
+  the deterministic fault-injection test is, and it kills M13 5/5. At the
+  original 60 rounds the lock-removal mutant was observed surviving 1 run in
+  50, which is why the row was restructured.
+- **Two tests depend on real wall-clock time**, declared in spec.md: one
+  asserts a blocked thread is still alive after 0.2s (spurious direction:
+  failure) and one waits up to 0.3s for a racing caller (spurious direction:
+  a false PASS, i.e. a surviving fail-open mutant — the worse direction).
+  Measured margin ~470×.
+- **Equivalent mutants, classified rather than killed**: a `while`→`if`
+  under-prune proposed by verification as a defect proved equivalent under a
+  monotone clock (0 divergences over 200k randomized sequences), as did
+  several sweep-timing variants. Killing them would need tests asserting
+  non-behaviour, which anti-gaming rule 4 forbids.
+- **The historical 8/8 mutation figure, stated precisely.** The runner used
+  before 2026-08-09 was vulnerable to `.pyc` reuse between same-size mutants
+  written in the same second, and exactly one adjacent pair could collide
+  (M4/M5, both 1675 bytes). Re-derived on the historical source under a sound
+  procedure, all 8 are genuinely killed, M5 included. The published figure is
+  therefore **correct in outcome even though the procedure that produced it
+  was unsound**; whether that archived run took the collision path cannot be
+  determined, and does not change the number.
+- **A negative control that was itself vacuous.** The first version of the
+  mutation harness's negative control waited for two writes to land in the
+  same second rather than pinning the mtime, and passed with the defence
+  removed. It was caught only because the control was tested for its ability
+  to fail. Its second version used a control mutant that was not strictly
+  equivalent. Both are recorded because "prove the checker can fail" is a
+  rule this project states, and it took two attempts to satisfy it here.
+- **Three defects were introduced by fixes** in this sequence: the lock added
+  in REVISION 4 did not cover the clock read (found in round 3); the NaN
+  paragraph corrected in 4d contained a fresh false claim (round 5); and the
+  "just under 2W" bound written in 4e was wrong (round 6).
+- **Layer attribution moved during the work.** Widening the property
+  strategies to answer one finding *weakened* the property layer — the
+  fail-open mutant M5 stopped being killed by the properties, because with
+  258 possible keys and limits up to 20 hypothesis almost never drove a key
+  to its limit. Re-tuned to 12 keys and limits 1–5, measured rather than
+  guessed. Without the Tier 3 attribution requirement this regression would
+  have been invisible: the full suite stayed green throughout.
+- **Known gaps left open**: the memory bound is temporal, not cardinal —
+  unbounded distinct keys *within* one window is accepted residual risk;
+  forward clock skew, NaN clock readings and reentrant clocks are caller
+  obligations, not defended in code; there is no `Retry-After` accessor; the
+  shell scripts have no lint layer; and evidence is generated on Python 3.14
+  while CI gates on 3.12.
+- **Spec revisions 2026-07-25 and 2026-07-27 remain unapproved**, and the
+  revision-3 failure model was a retrofit reconstructed after implementation
+  rather than written before it.
+- **Git history note**: the demo originally ran without git. The repo is now
+  under git; source state above cites the commit.

From 8b88bda7085f3839454e160ae6ca1e18e1fcfdc1 Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 14:21:10 +0800
Subject: [PATCH 08/12] docs(demo): prune the spec back to a contract
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

spec.md had grown to 339 lines against a 99-line implementation, most of it
forensics: what an earlier revision claimed, which mutant a row used to cite,
what a verification round measured. That material is real but it belongs in
evidence.md's honest notes and in git, not in the one artifact a human is
supposed to read before any code exists.

The contract is unchanged — same scenarios, same invariants, same Must NOTs,
same clock obligations, same residual risk, same failure-model rows and the
same falsification procedures. What is gone is the archaeology; a short
revision-history section points at where it lives. 339 -> 255 lines.

Comments in the tests and tooling got the same treatment: the reason a value
or a pattern is what it is stays, the account of what a previous revision got
wrong goes.

Gauntlet green after the prune: 41 tests, 100% branch coverage, negative
control ok, 22/22 mutants.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/spec.md                   | 400 ++++++++------------
 demo-rate-limiter/tests/test_ratelimiter.py |  45 +--
 demo-rate-limiter/tools/gauntlet.sh         |  19 +-
 demo-rate-limiter/tools/mutants.py          |  50 +--
 4 files changed, 202 insertions(+), 312 deletions(-)

diff --git a/demo-rate-limiter/spec.md b/demo-rate-limiter/spec.md
index 4bcb8b7..2f7bb29 100644
--- a/demo-rate-limiter/spec.md
+++ b/demo-rate-limiter/spec.md
@@ -4,6 +4,15 @@ A library class `RateLimiter(limit, window_seconds, clock)` answering
 `allow(key) -> bool`: at most `limit` allowed requests per `key` within any
 sliding `window_seconds` interval. `clock` is an injected callable returning
 current time in seconds (the mock boundary — no real sleeping in tests).
+Intended deployment: in front of a public HTTP API, so callers are untrusted
+and the key space is attacker-controlled.
+
+This document is the contract. How each clause was arrived at — including the
+defects that six rounds of independent verification found and the two that a
+fix round introduced — is in `evidence.md`'s honest notes and in git history,
+deliberately not here.
+
+## Behaviour
 
 ```gherkin
 Feature: Sliding-window rate limiting per key
@@ -14,326 +23,233 @@ Feature: Sliding-window rate limiting per key
     Then all 3 return True
 
   Scenario: request over the limit is denied
-    Given a limiter with limit 3 per 60 seconds
-    And a key made 3 allowed requests at t=0
+    Given a limiter with limit 3 per 60 seconds and 3 allowed requests at t=0
     When the key makes a 4th request at t=59
     Then it returns False
 
   Scenario: denied requests do not consume quota
     Given a limiter with limit 1 per 60 seconds
-    And a key made 1 allowed request at t=0 and 5 denied requests at t=10
+    And 1 allowed request at t=0 and 5 denied requests at t=10
     When the window expires at t=61
     Then the next request returns True
-    (denials at t=10 must not have extended or refilled anything)
 
   Scenario: window slides — old requests expire individually
-    Given a limiter with limit 2 per 10 seconds
-    And allowed requests at t=0 and t=5
+    Given a limiter with limit 2 per 10 seconds and requests at t=0 and t=5
     When the key requests at t=10.1
     Then it returns True   # the t=0 request left the window
     When the key requests at t=10.2
-    Then it returns False  # t=5 and t=10.1 still inside
+    Then it returns False  # t=5 and t=10.1 are still inside
 
   Scenario: keys are isolated
-    Given a limiter with limit 1 per 60 seconds
-    And key "a" has exhausted its quota at t=0
+    Given a limiter with limit 1 per 60 seconds and key "a" exhausted at t=0
     When key "b" requests at t=0
     Then it returns True
 
-  Scenario: invalid construction is rejected
-    When constructing with limit 0, or a negative limit, or window_seconds <= 0
-    Then ValueError is raised naming the bad parameter
-    (a limiter that silently never/always allows is a security bug)
-
-  Scenario: non-finite window is rejected  [REVISION 2026-07-25: found by the
-    adversarial pass — NaN slipped through the "<= 0" check and produced a
-    window that never slides; inf silently disables expiry]
-    When constructing with window_seconds = NaN or +/-inf
-    Then ValueError is raised naming window_seconds
-
   Scenario: request at the exact window boundary is still limited
-    [REVISION 2026-07-27: mutant M2's kill turned out to depend on hypothesis
-    randomly hitting the exact boundary — no deterministic test covered it]
-    Given a limiter with limit 1 per 60 seconds
-    And an allowed request at t=0
+    Given a limiter with limit 1 per 60 seconds and an allowed request at t=0
     When the key requests at exactly t=60
     Then it returns False  # a hit expires only when its age EXCEEDS the window
 
   Scenario: non-monotonic clock does not grant extra quota
-    Given a limiter with limit 1 per 60 seconds
-    And an allowed request at t=100
-    When the clock jumps backward and the key requests at t=50
-    Then it returns False
-    (clock skew must fail closed, never open)
+    Given a limiter with limit 1 per 60 seconds and a request at t=100
+    When the clock jumps backward by more than the window and the key requests
+    Then it returns False  # skew must fail closed, never open
+
+  Scenario: invalid construction is rejected
+    When constructing with limit 0, a negative limit, or window_seconds <= 0
+    Then ValueError is raised naming the bad parameter
+    (a limiter that silently never or always allows is a security bug)
 
-  Scenario: limit must be a finite positive integer  [REVISION 4]
+  Scenario: limit must be a finite positive integer
     When constructing with limit = NaN, +/-inf, a float such as 2.5, or a bool
     Then ValueError is raised naming limit
-    (limit=NaN made every comparison False and the limiter allowed forever —
-    the same fail-open class fixed for window_seconds in REVISION 2026-07-25,
-    never swept across to the sibling parameter. limit=2.5 was not "silently
-    treated as 2": len(hits) >= 2.5 is false at 2, so it allowed 3.)
+    (every comparison against NaN is false, so the limiter allowed forever)
 
-  Scenario: window_seconds must be a number  [REVISION 4b]
-    When constructing with window_seconds = True, "60", or None
+  Scenario: window_seconds must be a positive finite number
+    When constructing with window_seconds = NaN, +/-inf, True, "60", or None
     Then ValueError is raised naming window_seconds
-    (the sweep ran one way only: window_seconds=True built a 1.0-second
-    window, and "60" raised a bare TypeError from math.isfinite instead of
-    naming the parameter the invalid-construction scenario promises)
 
-  Scenario: keys are compared as exact strings  [REVISION 4b, widened in 4c]
+  Scenario: key must be a non-empty string
+    When calling allow() with None, an int, bytes, or ""
+    Then TypeError (wrong type) or ValueError (empty) is raised
+    (a missing HTTP header arriving as None must not become one shared bucket
+    for every unidentified caller)
+
+  Scenario: keys are compared as exact strings
     Given a limiter with limit 1 per 60 seconds
     When "Alice", "alice", "alice " and " " each make a request
     Then all are allowed — they are four different callers
-    (every key elsewhere in the suite was lowercase and unpadded, so key
-    normalisation was structurally invisible. Case was pinned in 4b and
-    trimming still survived it, so padding is pinned too. A whitespace-only
-    key is a valid caller by the same rule: the contract is "non-empty str",
-    and deciding that " " is not a real caller is the caller's business.)
 
-  Scenario: the sweep keeps a key whose newest hit is exactly one window old
-    [REVISION 4c]
+  Scenario: concurrent callers never exceed the limit
     Given a limiter with limit 1 per 60 seconds
-    And another key's request at t=0 that arms the sweep, and "k" at t=1
-    When any request arrives at t=61, firing the sweep
-    Then "k" is still limited — its hit is exactly 60s old, not older
-    (the exact-boundary scenario pins _prune's comparison; _sweep re-implements
-    the same age test and nothing pinned it, so a >= there forgot a key that
-    still had a live hit and reset that caller's quota)
+    When many threads call allow() for the same key simultaneously
+    Then exactly 1 call returns True
 
   Scenario: concurrent commits never invert against the clock read
-    [REVISION 4c]
-    Given two callers whose clock reads are forced to return different values
+    Given two callers whose clock reads return different values
     When the caller that read the earlier value commits second
     Then the recorded hits are still in ascending order
-    (both _prune and _sweep assume that order; the lock originally covered
-    check-and-append but not the clock read, and every other concurrency test
-    held time constant so the whole class of ordering races was invisible)
-
-  Scenario: key must be a non-empty string  [REVISION 4]
-    When calling allow() with None, an int, bytes, or ""
-    Then TypeError (wrong type) or ValueError (empty) is raised
-    (CONTRACT HARDENING, not a reproduced fail-open: None as a key made every
-    unidentified caller share one bucket, which limits too strictly or lets
-    callers exhaust each other's quota — it never let anyone past the limit.
-    Approved as a deliberate tightening for an HTTP-facing API, and recorded
-    separately from the defects that were demonstrated.)
+    (both pruning and sweeping assume that order)
 
-  Scenario: idle keys are forgotten — the key map is bounded  [REVISION 4]
-    Given a limiter with limit 1 per 60 seconds
-    And 1000 distinct keys that each made one request at t=0 and never return
+  Scenario: idle keys are forgotten — the key map is bounded
+    Given 1000 distinct keys that each made one request at t=0 and never return
     When any request arrives after a full window has elapsed
     Then the limiter retains only keys with a hit inside the current window
 
-  Scenario: the key map is bounded by two windows, not one  [REVISION 4e]
-    Given a limiter with limit 5 per 60 seconds
-    And "armer" at t=0 and "idle" at t=1, then a request at t=60.9
+  Scenario: a key is dropped by the first sweep after one idle window
+    Given "armer" and "idle" both at t=0
+    When a request arrives at t=61, firing the sweep
+    Then "idle" is gone  # the idle threshold is one window, not more
+
+  Scenario: the sweep keeps a key whose newest hit is exactly one window old
+    Given "other" at t=0 arming the sweep, and "k" at t=1
+    When a request arrives at t=61, firing the sweep
+    Then "k" is still limited — its hit is exactly 60s old, not older
+
+  Scenario: the key map is bounded by two windows, not one
+    Given "armer" at t=0 and "idle" at t=1, then a request at t=60.9
     When a request arrives at t=100 — "idle" has been idle for 99s
     Then "idle" is still retained; only at t=121 is it forgotten
-    (the sweep is throttled to once per window, so worst-case retention is
-    just under 2W. The old idle-keys test probed at exactly 2W and so passed
-    under either reading, pinning neither.)
+    (the sweep is throttled, so residency reaches 2W before the dropping sweep)
 
-  Scenario: nothing is reclaimed while traffic is silent  [REVISION 4e]
+  Scenario: nothing is reclaimed while traffic is silent
     Given 50 one-shot keys at t=0
     When the clock advances by ~166,000 windows and no request is made
     Then all 50 are still resident; the map shrinks only on the next request
-    (sweeping happens inside allow(), so the bound is "keys seen in the two
-    windows preceding the most recent request", not two windows of wall time)
 
-  Scenario: the sweep is throttled to at most once per window  [REVISION 4e]
-    Given a limiter with limit 5 per 60 seconds and a request at t=0
-    When further requests arrive at t=30 and at t=60 (delta exactly one window)
+  Scenario: the sweep is throttled to at most once per window
+    Given a limiter with a 60-second window and a request at t=0
+    When further requests arrive at t=30 and at t=60
     Then no further sweep has run; the sweep at t=61 does run
-    (the throttle carries the accepted-residual-risk argument, and its own
-    boundary was the last age comparison in the file with no test behind it)
 
-  Scenario: the first call always sweeps  [REVISION 4e]
+  Scenario: the first call always sweeps
     Given a fresh limiter with a 60-second window
     When the very first request arrives at t=30
     Then a sweep has run
-    (the -inf sentinel exists for exactly this; every other clock in the suite
-    starts at 0.0 or beyond a window, so a 0.0 sentinel was indistinguishable)
 
-  Scenario: a backward clock jump does not suspend reclamation  [REVISION 4e]
+  Scenario: a backward clock jump does not suspend reclamation
     Given a limiter armed at t=1,000,000
     When the clock jumps back to 0 and 200 one-shot keys arrive over 400s
     Then the sweep still runs and the map does not grow without bound
-    (a one-sided throttle left `now` permanently below the last sweep time —
-    measured 20,001 keys retained across seven windows of monotone time)
-
-  Scenario: concurrent callers never exceed the limit  [REVISION 4]
-    Given a limiter with limit 1 per 60 seconds
-    When many threads call allow() for the same key simultaneously
-    Then exactly 1 call returns True
-    (read-prune-check-append was not atomic; measured 2x over-allow)
 ```
 
 ## Invariants (property-based)
 
-- P1: for any request sequence on one key, allowed count within any window of
-  `window_seconds` (by the times the limiter saw) never exceeds `limit`.
-- P2: interleaving traffic from other keys never changes one key's outcomes.
+- **P1**: for any request sequence on one key, the allowed count within any
+  window of `window_seconds` never exceeds `limit`.
+- **P2**: interleaving traffic from other keys never changes one key's outcomes.
 
 ## Must NOT do
 
-- The limiter under test is never driven by a real clock, and no test makes
-  time pass by sleeping. [REVISION 4, amended: the gate matched only `time.`
-  and missed `from time import sleep`. The wording here previously claimed to
-  cover "every spelling", which a regex cannot do — dynamic imports, renamed
-  helpers, and a caller's own `sleep()` all escape it. The gate blocks known
-  direct wall-clock imports and calls; that is its actual scope.]
-  **Declared exception** [corrected in 4d]: the concurrency tests use
-  `Event.wait(timeout=)` and `Thread.join(timeout=)`. Most are deadlock guards,
-  but TWO are genuine wall-clock dependences and they fail in OPPOSITE
-  directions, which the 4b wording got wrong by naming only the first:
+- **No real clock in tests.** The limiter under test is never driven by a real
+  clock, and no test makes time pass by sleeping. The gate that enforces this
+  is a regex over `tests/`; its scope is known direct wall-clock imports and
+  calls. Dynamic imports, renamed helpers and a caller's own `sleep()` escape
+  it, and the gate does not claim otherwise.
+
+  *Declared exception.* Two assertions in the concurrency tests do depend on
+  real elapsed time, and they fail in opposite directions:
   (1) the atomicity test asserts a blocked thread is still alive after 0.2s —
-  spurious failure only, if a thread is starved that long;
-  (2) `second_done.wait(timeout=0.3)` in the clock-ordering test is not a
-  guard at all: on healthy code it ALWAYS times out (a fixed 0.3s per suite
-  run), and on the mutant that moves the clock read outside the lock the kill
-  depends on the second caller finishing inside that budget. Its spurious
-  direction is therefore a false PASS — a surviving fail-open mutant, the
-  worse direction. Measured margin is ~470x (0.06-0.63ms of 300ms), so it is
-  accepted, not ignored. No limiter in any test reads a real clock.
-- No unbounded memory growth. [REVISION 4: this clause used to read "from
-  denied requests (denials store nothing)". Denials were never the leak;
-  *allowed* requests from keys that never return were. Growth is bounded by
-  the distinct keys seen in the TWO windows preceding the most recent
-  request — see the idle-keys scenario. Precisely [REVISION 4f]: a key is
-  resident at an age of at most exactly 2W when any request is observed, and
-  the sweep that drops it runs strictly LATER than 2W after its last hit.
-  Earlier wording said "just under 2W", which is false in both readings —
-  2W is attained (armer t=0, idle t=40, probes at t=100 and t=160 leave idle
-  resident at age exactly 120.0). The qualifier below is load-bearing
-  [REVISION 4e]: sweeping happens only inside `allow()`, so while traffic is
-  silent nothing is reclaimed at all. Measured with 1000 one-shot keys, clock
-  advanced by ~166,000 windows with no requests, still 1000 keys resident
-  (the scenario and its test use 50, which is the same behaviour at a size
-  that keeps the suite fast);
-  the map drops to 1 only when the next request arrives. Peak resident set is
+  spurious failure only; (2) the clock-ordering test waits up to 0.3s for a
+  racing caller — on healthy code that wait always times out, and its spurious
+  direction is a false PASS, i.e. a surviving fail-open mutant. Measured margin
+  ~470×. Accepted deliberately: the alternative is a test that can hang.
+
+- **No unbounded memory growth.** Growth is bounded by the distinct keys seen
+  in the **two** windows preceding the most recent request. Precisely: a key is
+  resident at an age of at most exactly 2W whenever a request is observed, and
+  the sweep that drops it runs strictly later than 2W after its last hit. The
+  qualifier is load-bearing — sweeping happens only inside `allow()`, so while
+  traffic is silent nothing is reclaimed at all and the peak resident set is
   not released until traffic resumes.
-  REVISION 4d: this clause and the class docstring both said "one window" and
-  were literally false. Because the sweep is throttled to once per window, a
-  key can sit idle for just under 2W before the sweep that drops it runs. Only
-  the residual-risk section had it right; the idle-keys test probed at 2W, so
-  it passed under either reading and pinned neither.]
-
-## Clock contract [REVISION 4]
-
-`clock` MUST be monotonic (`time.monotonic`, as `examples/demo.py` uses). A
-forward jump — NTP step, resumed VM — expires every hit at once and resets
-every caller's quota simultaneously. That is inherent to a sliding window over
-a supplied clock and is not defended against in code; it is a caller
-obligation, stated here because the failure model previously implied the
-non-monotonic scenario covered skew in both directions. It covers backward
-skew only.
-
-`clock` MUST also return a finite number. [REVISION 4b, corrected in 4c] A NaN
-reading is recorded as a hit that can never expire: `now - nan > window` is
-always false, in `_prune` **and in `_sweep`**. Revision 4b claimed the sweep
-would eventually reclaim such a key; it cannot — the sweep uses the same
-comparison. Measured: once a key's newest hit is NaN, the key is retained
-through t=1e18 and that caller is denied forever. **This falsifies the
-temporal memory bound for NaN-poisoned keys**, which is stated here rather
-than left to be inferred. The third NaN injection point is the clock itself,
-and it stays a caller obligation rather than a check because validating every
-reading puts a branch on the hot path for a fault `time.monotonic` cannot
-produce. [4d, corrected in 4e] A NaN reading also disturbs the sweep
-throttle, but NOT permanently: `_last_sweep` becomes NaN and every comparison
-against it is false, so the very next request sweeps — and that sweep
-unconditionally re-anchors `_last_sweep` to a finite value, after which the
-throttle behaves normally. Measured: nan, then 100.0 at t=100, still 100.0 at
-t=101/102/110. The total cost of one NaN reading is **one extra sweep**. The
-4d text claimed an unbounded per-request scan "for the life of the process";
-that was false, and it was written by the revision that fixed the previous
-inaccuracy in this same paragraph. (A clock stuck at NaN forever is a
-different matter and is not what that sentence described.)
-
-`clock` is the only constructor parameter with no validation. That is
-deliberate — a non-callable clock raises TypeError at the first `allow()`,
-which is loud and fail-closed, not the silent acceptance the hostile-config
-row is about. [4d]
-
-`clock` MUST NOT call back into the same limiter. [REVISION 4c] The clock is
-read inside the critical section, so a reentrant clock deadlocks on a
-non-reentrant lock. This is the price of the fix for the ordering race and is
-recorded as an obligation rather than hidden.
-
-## Accepted residual risk [REVISION 4b]
-
-The memory bound is **temporal, not cardinal**: keys idle for a window are
-forgotten, but nothing caps how many distinct keys appear *within* one window.
-An attacker who controls the key — which, per the stated deployment, is an IP
-or a request header — can still drive the map arbitrarily large inside a
-single window, and because the sweep is throttled to once per window the
-worst-case retention is closer to two windows than one. This is accepted, not
-overlooked: a cardinality cap needs an eviction policy (which caller gets
-forgotten?), and evicting a live key silently resets its quota — a fail-open
-worse than the memory it saves. Recorded here so the residual reads as
-accepted rather than absent, in the same register as the clock contract.
 
-## Failure model (Tier 3)
+## Clock contract
+
+`clock` is a caller obligation on three axes. None is checked in code, because
+each check would put a branch on the hot path for a fault the recommended
+clock cannot produce.
+
+- **Monotonic** (`time.monotonic`, as `examples/demo.py` uses). A forward jump
+  — NTP step, resumed VM — expires every hit at once and resets every caller's
+  quota simultaneously. That is inherent to a sliding window over a supplied
+  clock. Backward skew *is* handled: it fails closed for quota, and the sweep
+  re-arms rather than suspending.
+- **Finite.** A NaN reading is recorded as a hit that can never expire, in
+  pruning or in sweeping, so that key is retained forever and its caller is
+  denied forever — which suspends the memory bound for that key. A NaN also
+  costs one extra unthrottled sweep; the throttle re-anchors on the next
+  finite reading.
+- **Non-reentrant.** The clock is read inside the critical section, so a clock
+  that calls back into the same limiter deadlocks.
+
+`clock` is also the one constructor parameter with no validation: a
+non-callable clock raises TypeError at the first `allow()`, which is loud and
+fail-closed rather than silently accepted.
+
+## Accepted residual risk
+
+The memory bound is **temporal, not cardinal**. Keys idle for a window are
+forgotten, but nothing caps how many distinct keys appear *within* one window,
+so an attacker controlling the key can still drive the map arbitrarily large
+inside a single window. Accepted, not overlooked: a cardinality cap needs an
+eviction policy, and evicting a live key silently resets its quota — a
+fail-open worse than the memory it saves.
 
-[REVISION 3, 2026-07-27: retrofitted — the skill now requires an explicit
-failure model before layer selection; these modes were previously implicit
-in the scenarios, Must NOTs, and adversarial pass.]
+## Failure model (Tier 3)
 
-[REVISION 4, 2026-08-09, amended 4b: independent fresh-context verification
-found rows below claiming coverage they did not have. The standard is now:
-every covered mode must name and demonstrate an **appropriate falsification
-procedure** — a test, a mutant, fault injection, a benchmark, a rollback
-rehearsal, whatever actually fits the risk. Not "a test AND a mutant", which
-just breeds mutants written to fill a table. A row whose catcher cannot be
-shown to fail is a defect, not a mapping.]
+Every covered mode names a **falsification procedure that has been
+demonstrated to fail** — a test, a mutant, fault injection, whatever fits the
+risk. Not "a test AND a mutant", which only breeds mutants written to fill a
+table. A row whose catcher cannot be shown to fail is a defect, not a mapping.
 
 | How this can hurt | Falsification procedure, demonstrated |
 |---|---|
-| over-allowing in a burst (limit not enforced) | scenario tests + P1; mutants M1/M5 killed |
-| under-allowing / fail-closed drift (quota lost) | boundary scenario, demonstrated by killing M2. [4b: this row previously cited M6/M8 — M6 in fact **over**-allows, and M8 is killed by the memory row's tests. Verification also proposed a `while`→`if` mutant here; it proved EQUIVALENT, see mutants.py] |
-| hostile or invalid config silently accepted | validation scenarios for limit, window_seconds AND key + adversarial pass; mutants M4/M7/M9/M15 killed |
-| backward clock skew opening the gate | non-monotonic clock scenario, jump exceeding the window; mutant M10 killed |
-| forward clock skew resetting all quota | **not covered — caller obligation**; see Clock contract |
-| a non-finite clock reading freezing a hit in the window | **not covered — caller obligation**; see Clock contract [4b] |
-| caller identity silently merged (key normalisation) | exact-strings scenario, covering case AND padding; mutants M14/M17 killed. [4c: the row previously cited case-folding only, and `key.strip()` survived it — the P2 pool held `"c "` but not `"c"`, so no two members could merge] |
-| a caller's quota reset by the sweep at the exact boundary | sweep-boundary scenario; mutant M18 killed [4c] |
-| concurrent commits inverted against the clock read | clock-ordering scenario (gated clock forces two callers to read different values); mutant M16 killed. [4c: the lock covered check-and-append but not the clock read. Both earlier concurrency tests held time constant, so no test could tell the two placements apart] |
-| unbounded memory growth (any path) | idle-keys scenario + denials test; mutants M8/M12 killed |
-| concurrent callers racing on shared state | **fault injection**: the atomicity test constructs the interleaving and kills M13 deterministically. The threaded stress test corroborates statistically (per-round detection measured against the real source mutant at 3.7% on this machine — an earlier 5.9% came from a Python replica, not the mutant; 400 rounds puts the miss probability near 3e-7, and the rate is machine-dependent) but cannot be the sole catcher — at 60 rounds the lock-removal mutant was observed surviving 1 run in 50 |
-| the mutation layer reporting kills it never ran | **negative control**: a killer and a strictly-equivalent mutant of identical size under one pinned mtime. Non-vacuity measured three ways [4e]: removing the rmtree alone leaves it green, removing PYTHONDONTWRITEBYTECODE alone trips a RuntimeError tripwire, and removing both plus the tripwire produces the advertised misreport. The 4b wording credited the rmtree; DONTWRITEBYTECODE is what closes the leak |
-| the sweep degrading to an O(distinct keys) scan per request (availability) | throttle scenario + first-call scenario; mutants M19/M21/M22 killed [4e] |
-| backward skew suspending memory reclamation | backward-jump scenario; mutant M20 killed. [4e: the skew row above covers the quota side only — "fails closed" was true of quota and false of memory] |
-| untested code reaching production | coverage layer, now a gate (`--cov-fail-under=100`) — it previously printed a number and could not fail |
-| silent failure in production | n-a: library returns a bool the caller observes directly |
+| over-allowing in a burst | scenario tests + P1; M1/M5 killed |
+| under-allowing / quota lost | boundary scenario; M2 killed (P1 is one-sided and cannot see this) |
+| hostile or invalid config accepted | validation scenarios for limit, window_seconds and key; M4/M7/M9/M15 killed |
+| backward clock skew opening the gate | non-monotonic scenario, jump exceeding the window; M10 killed |
+| backward skew suspending reclamation | backward-jump scenario; M20 killed |
+| forward skew resetting all quota | **not covered — caller obligation** |
+| a non-finite clock reading freezing a hit | **not covered — caller obligation** |
+| caller identity merged by normalisation | exact-strings scenario, case and padding; M14/M17 killed |
+| quota reset by the sweep at the boundary | sweep-boundary scenario; M18 killed |
+| the retention bound silently inflating | first-sweep scenario; M23 killed (the boundary was pinned long before the magnitude was) |
+| unbounded memory growth (any path) | idle-keys + silent-traffic scenarios; M8/M12 killed |
+| the sweep degrading to an O(keys) scan | throttle + first-call scenarios; M19/M21/M22 killed |
+| concurrent callers racing on shared state | **fault injection**: the atomicity test constructs the interleaving and kills M13 deterministically. The threaded stress test only corroborates — it is statistical (see evidence.md) |
+| commits inverted against the clock read | clock-ordering scenario with a gated clock; M16 killed |
+| the mutation layer reporting kills it never ran | **negative control**: a killer and a strictly-equivalent mutant of identical size under one pinned mtime, proven non-vacuous by removing the defence |
+| untested code reaching production | coverage layer, a gate at `--cov-fail-under=100` |
+| silent failure in production | n-a: the library returns a bool the caller observes directly |
 
 ## Setup plan
 
-[REVISION 3, 2026-07-27: retrofitted — the skill now requires dependencies
-to be justified in the spec. Original setup was authorized conversationally.]
-
-- Runtime dependencies: **none** — stdlib (`collections.deque`, `math`) suffices.
-- Dev toolchain (pinned in `requirements-dev.txt`, never shipped):
-  - pytest + pytest-cov + coverage — test runner and changed-line coverage
-  - mypy — strict type checking
-  - ruff — lint, format, and complexity budget (mccabe ≤ 8)
-  - hypothesis — property-based invariants P1/P2
-  - pip-audit — vulnerability audit of the pinned toolchain
-  - pytest-randomly — randomized test order (suite-health layer)
-- Git: repo-level; commits at each milestone; evidence binds to commit SHA.
+- Runtime dependencies: **none** — `collections.deque`, `math` and
+  `threading.Lock` are stdlib.
+- Dev toolchain (pinned in `requirements-dev.txt`, never shipped): pytest +
+  pytest-cov + coverage (tests and changed-line coverage), mypy (strict types),
+  ruff (lint, format, mccabe ≤ 8), hypothesis (P1/P2), pip-audit (toolchain
+  vulnerabilities), pytest-randomly (suite health).
+- Git: repo-level; commits at each milestone; evidence binds to a commit SHA.
 - Files the gauntlet adds: `tools/gauntlet.sh` (entry point), `tools/mutants.py`
-  (scripted manual mutation), `.github/workflows/gauntlet.yml` (CI),
-  `tools/must_not_match.sh` + `tools/test_gauntlet_checks.sh` (fail-closed
-  scan helper and its self-test).
-- [REVISION 4] Runtime dependencies remain **none**: `threading.Lock` is
-  stdlib. The coverage layer gains `--cov-fail-under=100`, making it a gate
-  rather than a report.
+  (scripted mutation + its negative control), `tools/must_not_match.sh` and
+  `tools/test_gauntlet_checks.sh` (fail-closed scan helper and its self-test),
+  `tools/source_state.sh`, `.github/workflows/gauntlet.yml` (CI).
 
-## Explicitly out of scope [REVISION 4]
+## Explicitly out of scope
 
 - **Retry-After / remaining-quota accessor.** `allow(key) -> bool` gives an
   HTTP frontend no way to populate `Retry-After` or `X-RateLimit-Remaining`,
-  which RFC 9110 expects alongside a 429. Raised by both verification passes.
-  Declined here because it changes the public API shape and the contract asks
-  only to bound request frequency — recorded so the gap is visible rather than
-  absent.
+  which RFC 9110 expects alongside a 429. Declined: it changes the public API
+  shape, and the contract asks only to bound request frequency. Recorded so
+  the gap is visible rather than absent.
 - **Distributed / multi-process limiting.** In-process state only.
+
+## Revision history
+
+Revisions 1–3 (2026-07-25 → 07-27) were made autonomously during the original
+build and were never human-approved; the failure model in revision 3 was
+retrofitted after implementation. Revision 4 and its amendments (2026-08-09 →
+08-10) were approved item by item before implementation, and each amendment
+answers a specific finding from an independent verification round. The
+per-revision forensics live in `evidence.md` and in git.
diff --git a/demo-rate-limiter/tests/test_ratelimiter.py b/demo-rate-limiter/tests/test_ratelimiter.py
index f5c9cf0..f37f408 100644
--- a/demo-rate-limiter/tests/test_ratelimiter.py
+++ b/demo-rate-limiter/tests/test_ratelimiter.py
@@ -122,19 +122,16 @@ def test_key_must_be_a_non_empty_string(
 
 @pytest.mark.parametrize("window", [True, "60", None])
 def test_window_seconds_must_be_a_number(clock: FakeClock, window: Any) -> None:
-    # The 2026-07-25 NaN sweep ran on window_seconds and the REVISION 4 sweep
-    # ran on limit and key; window_seconds never got a type guard, so
-    # window_seconds=True built a 1.0-second window and "60" raised a bare
-    # TypeError from math.isfinite instead of naming the parameter.
+    # bool is an int subclass, so window_seconds=True would build a 1.0-second
+    # window; "60" would raise a bare TypeError instead of naming the parameter.
     with pytest.raises(ValueError, match="window_seconds"):
         RateLimiter(limit=1, window_seconds=window, clock=clock)
 
 
 def test_keys_are_compared_as_exact_strings(clock: FakeClock) -> None:
-    # Every key anywhere else in the suite is lowercase and unpadded, so any
-    # normalisation of the key was structurally invisible. Case-folding was
-    # pinned first; trimming survived that fix, so padding is pinned too, and
-    # a whitespace-only key is a valid distinct caller by the same rule.
+    # Every key elsewhere in the suite is lowercase and unpadded, so key
+    # normalisation is otherwise structurally invisible. Case, padding and a
+    # whitespace-only key are all pinned: the contract is "non-empty str".
     limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
     assert limiter.allow("Alice") is True
     assert limiter.allow("alice") is True  # a different caller, not the same one
@@ -146,9 +143,8 @@ def test_keys_are_compared_as_exact_strings(clock: FakeClock) -> None:
 def test_sweep_keeps_a_key_whose_newest_hit_is_exactly_window_old(
     clock: FakeClock,
 ) -> None:
-    # The boundary scenario above pins _prune's comparison; _sweep re-implements
-    # the same age test and nothing pinned it, so a >= there silently forgot a
-    # key that still had a live hit and reset that caller's quota.
+    # _sweep re-implements _prune's age comparison, so it needs its own
+    # boundary test: a >= there forgets a key that still has a live hit.
     limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
     assert limiter.allow("other") is True  # t=0, arms the sweep clock
     clock.now = 1.0
@@ -160,10 +156,9 @@ def test_sweep_keeps_a_key_whose_newest_hit_is_exactly_window_old(
 def test_a_key_is_dropped_by_the_first_sweep_after_one_idle_window(
     clock: FakeClock,
 ) -> None:
-    # _sweep's boundary was pinned (M18 kills >=) but its MAGNITUDE was not:
-    # `> window * 1.5` and even `* 1.99` left the whole gauntlet green while
-    # inflating the approved two-window bound to three. Every memory test
-    # asserted deletion only at age >= 2W, so any threshold in (W, 2W) passed.
+    # Pins the idle threshold's MAGNITUDE, not just its boundary: every other
+    # memory test asserts deletion only at age >= 2W, so any threshold in
+    # (W, 2W) satisfies them all.
     limiter = RateLimiter(limit=5, window_seconds=60, clock=clock)
     assert limiter.allow("armer") is True  # t=0, arms the sweep clock
     assert limiter.allow("idle") is True  # t=0
@@ -173,10 +168,8 @@ def test_a_key_is_dropped_by_the_first_sweep_after_one_idle_window(
 
 
 def test_the_memory_bound_is_two_windows_not_one(clock: FakeClock) -> None:
-    # The docstring and the Must NOT both said "one window" and were literally
-    # false: because the sweep is throttled, a key can stay idle for nearly two
-    # windows. The old idle-keys test probed at 2x the window, so it passed
-    # under either reading and pinned neither. This pins both sides.
+    # The throttle means residency reaches 2W. Pins both sides, so a bound of
+    # one window and a bound of three are each rejected.
     limiter = RateLimiter(limit=5, window_seconds=60, clock=clock)
     assert limiter.allow("armer") is True  # t=0, arms the sweep clock
     clock.now = 1.0
@@ -216,11 +209,9 @@ def test_memory_is_not_reclaimed_while_traffic_is_silent(clock: FakeClock) -> No
 
 
 def test_backward_clock_skew_does_not_suspend_the_sweep(clock: FakeClock) -> None:
-    # The throttle compares now against the last sweep time. After a backward
-    # jump, now stays below it and the sweep never runs again until the clock
-    # catches up — measured 20,001 keys retained across seven windows of
-    # monotone time. The quota side fails closed under skew; the memory side
-    # did not, and no test looked at len(_hits) after a jump.
+    # A one-sided throttle leaves `now` permanently below the last sweep time
+    # after a backward jump, suspending reclamation entirely. Quota fails
+    # closed under skew; memory has to be checked separately.
     limiter = RateLimiter(limit=1, window_seconds=60, clock=clock)
     clock.now = 1_000_000.0
     assert limiter.allow("arm") is True
@@ -232,9 +223,9 @@ def test_backward_clock_skew_does_not_suspend_the_sweep(clock: FakeClock) -> Non
 
 
 def test_the_sweep_is_throttled_to_once_per_window(clock: FakeClock) -> None:
-    # "at most once per window" carries the accepted-residual-risk argument,
-    # but nothing pinned it: deleting the throttle bookkeeping made the sweep
-    # run an O(keys) scan on every request and the whole suite stayed green.
+    # The throttle carries the accepted-residual-risk argument, so it needs a
+    # catcher of its own: without one, the sweep degrades to an O(keys) scan
+    # on every request invisibly.
     limiter = RateLimiter(limit=5, window_seconds=60, clock=clock)
     assert limiter.allow("k") is True
     assert limiter._last_sweep == 0.0
diff --git a/demo-rate-limiter/tools/gauntlet.sh b/demo-rate-limiter/tools/gauntlet.sh
index 81ae35a..b53c727 100755
--- a/demo-rate-limiter/tools/gauntlet.sh
+++ b/demo-rate-limiter/tools/gauntlet.sh
@@ -27,19 +27,14 @@ echo "=== supply chain ==="
 "$PY/pip-audit" -r requirements-dev.txt
 echo "=== must-not scans ==="
 # Matches usage forms, not the word: `time\.` alone missed `from time import
-# sleep`. Deliberately not `[[:<:]]time`, which fires on conftest's own "No
-# real time in tests" docstring, on `timestamps`, on `timeout=` and on prose
-# like "hold time constant" — the fix belongs in the pattern, never in an
-# exclusion. (An earlier version of this comment also claimed it would fire on
-# test_non_monotonic_clock_*; that was invented — the name has no "time" in
-# it at all.)
+# sleep`. Deliberately not a bare word-boundary match on `time`, which fires
+# on conftest's own "No real time in tests" docstring, on `timestamps`, on
+# `timeout=` and on ordinary prose — the fix belongs in the pattern, never in
+# an exclusion.
 #
-# Scope is deliberately narrower than the Must NOT's ambition: it catches real
-# time being read or slept on, not every way a test could depend on wall
-# clock. `Event.wait(timeout=)` and `Thread.join(timeout=)` are NOT matched —
-# they are deadlock guards in the concurrency tests, declared as an exception
-# in spec.md rather than excluded here. A pattern cannot decide intent, so the
-# spec says what the gate actually covers instead of claiming more.
+# Scope is narrower than the Must NOT's ambition: `Event.wait(timeout=)` and
+# `Thread.join(timeout=)` are NOT matched. They are declared in spec.md as an
+# exception rather than excluded here, because a pattern cannot decide intent.
 must_not_match 'import[[:space:]]+time|from[[:space:]]+time[[:space:]]+import|time\.[a-zA-Z_]|datetime|sleep[[:space:]]*\(|perf_counter[[:space:]]*\(|monotonic[[:space:]]*\(' tests
 # Bracketed letters stop the pattern literal from matching itself. The path
 # list now includes CI config and metadata: workflows are where credentials
diff --git a/demo-rate-limiter/tools/mutants.py b/demo-rate-limiter/tools/mutants.py
index 9fb7c75..ce11199 100644
--- a/demo-rate-limiter/tools/mutants.py
+++ b/demo-rate-limiter/tools/mutants.py
@@ -17,20 +17,13 @@
 PYTEST = ROOT / ".venv/bin/pytest"
 
 # CPython validates a cached .pyc against (source mtime in whole seconds,
-# source size). Two mutants of identical size written inside the same second
-# are indistinguishable to that check, so the second one silently runs the
-# first one's bytecode. M4 and M5 are both exactly one byte shorter than the
-# original and adjacent in the list, so M5 -- the fail-open mutant -- was
-# reported KILLED on the strength of M4's code. The bias is toward inflating
-# the kill count, which can never surface as a red gauntlet. Both defences are
-# needed only as a belt-and-braces pair, and an earlier version of this
-# comment had the roles backwards. Measured three ways: removing the rmtree
-# alone leaves the control green; removing DONTWRITEBYTECODE alone trips the
-# tripwire below with a RuntimeError; only removing both AND the tripwire
-# reproduces the misreport. DONTWRITEBYTECODE is what actually closes the
-# leak — with no .pyc written during a run there is nothing to inherit — and
-# gauntlet.sh clears __pycache__ before the layer starts anyway. The rmtree
-# covers the case of running this script directly on a dirty tree.
+# source size), so two mutants of identical size written inside the same
+# second are indistinguishable to it and the second silently runs the first
+# one's bytecode. M4 and M5 are such a pair. The bias is always toward
+# inflating the kill count, which can never surface as a red gauntlet.
+# DONTWRITEBYTECODE is what closes the leak: with no .pyc written during a run
+# there is nothing to inherit. The rmtree covers running this script directly
+# on a dirty tree; the tripwire below catches the env var being lost.
 MUTANT_ENV = {**os.environ, "PYTHONDONTWRITEBYTECODE": "1"}
 
 MUTANTS = [
@@ -179,23 +172,18 @@
 ]
 
 
-# Negative control for the harness itself: two mutants of IDENTICAL size, a
-# killer followed by a proven-equivalent one. (Both are length-PRESERVING, so
-# all three files are the same size; an earlier version of this comment also
-# said "each one byte shorter than the original", which describes M4/M5, not
-# these. Only C1 == C2 matters for the collision.)
-# If bytecode caching ever leaks between runs again, the equivalent mutant
-# inherits the killer's result and is misreported as KILLED. Run with
-# --negative-control; run as a gate by tools/gauntlet.sh before the real
-# mutation pass. (It is NOT part of test_gauntlet_checks.sh, which covers
-# must_not_match only — an earlier comment here claimed otherwise.)
-# Both mutations are length-preserving, so the two mutated files are the same
-# size; with a pinned mtime the (mtime, size) collision is constructed, not
-# waited for. C2 must be STRICTLY equivalent: `or` over two side-effect-free
-# isinstance checks is commutative. An earlier attempt used the sweep throttle
-# (`<=` -> `<`), which differs at now - last_sweep == window and so can change
-# the key map — not equivalent once the memory bound is part of the contract,
-# and it would have turned red the day a test pinned that boundary.
+# Negative control for the harness itself: a killer and a strictly-equivalent
+# mutant. Both mutations are length-preserving, so the two mutated files are
+# the same size, and with a pinned mtime the (mtime, size) collision is
+# constructed rather than waited for. If bytecode ever leaks between runs
+# again, C2 inherits C1's verdict and is misreported as KILLED.
+#
+# C2 must be STRICTLY equivalent: `or` over two side-effect-free isinstance
+# checks is commutative. Anything merely "equivalent under today's tests"
+# turns red the day a test pins it.
+#
+# Run as a gate by tools/gauntlet.sh before the real mutation pass; it is not
+# part of test_gauntlet_checks.sh, which covers must_not_match only.
 CONTROL = [
     ("C1 killer (control)", "if limit <= 0:", "if limit >= 0:"),
     (

From 4a9fdc5be421b25d2ad05e397ca9ee0590a084f7 Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 14:21:59 +0800
Subject: [PATCH 09/12] evidence: rebind to 8b88bda after the spec prune

Same numbers (41 tests, 100% gated coverage, 22/22 mutants, control green);
new source state, plus a note that the spec was pruned to a contract and
where the forensics went.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/evidence.md | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/demo-rate-limiter/evidence.md b/demo-rate-limiter/evidence.md
index 0482769..f58ac08 100644
--- a/demo-rate-limiter/evidence.md
+++ b/demo-rate-limiter/evidence.md
@@ -7,7 +7,7 @@
 - Independent verification: **six fresh-context rounds**, the last against
   commit `d0b506c`. See "Independent verification" below — including what the
   final round found and what was deliberately left unfixed.
-- Source state: git commit `66df5cd`; sha256 tree hash `402ed5f682f8543f` —
+- Source state: git commit `8b88bda`; sha256 tree hash `c80e8cccf0a1ed3a` —
   reproduce both with `./tools/source_state.sh` (works from any directory;
   now includes `.github/workflows`, which decides whether the gauntlet runs
   in CI at all).
@@ -18,6 +18,12 @@
 All numbers are from one final fresh run of the entry point, executed
 2026-08-10 after the last code edit.
 
+`spec.md` was deliberately pruned back to a contract afterwards (339 → 255
+lines). Every clause, invariant, obligation and failure-model row survives;
+what was removed is the per-revision forensics, which lives in the honest
+notes below and in git. The spec is the artifact a human reads before any
+code exists, and it had stopped being readable as one.
+
 ## Spec → Test mapping
 
 Status legend: pass / fail / unverified / n-a.

From 8fbe331d3a149b2700876c62be55fa876e54d42a Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 15:20:05 +0800
Subject: [PATCH 10/12] skill: add VERIFY, plus two gauntlet rules the
 experiment produced
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

VERIFY — a fresh-context adversarial pass before EVIDENCE is finalized,
Tier 3, marked experimental. 40 lines in SKILL.md carrying only the
non-negotiables; the protocol lives in references/verifier.md behind a hard
gate ("not performed until that file has been read in full"), so Tier 1/2
never load it.

The rule that distinguishes this from the version I would have written before
running it: grade the findings. A behavioural finding is fixed and re-verified
in a new context; a description-or-mapping finding is fixed and disclosed and
does NOT buy another round. Without the split, "fix every finding" times
"re-verify after any change" only terminates when a round returns the empty
set, and prose has no such fixpoint. Rounds are capped at two by default.

references/verifier.md carries the four inputs (including the task contract:
the request PLUS every human-approved change since, or legitimate scope
revisions read as spec gaps), blind-first, the attack order, the
prove-divergence-before-reporting-a-survivor rule, the four states, the report
template, and what one case study actually showed — including that its A/B
design failed and that its late rounds were negative value.

Two rules from the same experiment that belong to GAUNTLET, not VERIFY:

- A coverage layer must exit nonzero when its threshold is missed. This repo's
  own coverage layer printed a percentage and exited 0; dropping to 89% left
  the gauntlet green. A layer that cannot fail is a report.
- A negative control proves one known-bad case reaches the checker's failure
  path. It does not prove the checker recognises every violation of the rule
  it serves — a grep gate can fail closed perfectly and still guard a spelling
  rather than a behaviour. And a negative control must itself be shown
  non-vacuous by removing the defence it validates: the first one written here
  passed with the defence removed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 skills/old-coder/SKILL.md               |  61 ++++++++-
 skills/old-coder/references/gauntlet.md |  13 +-
 skills/old-coder/references/verifier.md | 158 ++++++++++++++++++++++++
 3 files changed, 226 insertions(+), 6 deletions(-)
 create mode 100644 skills/old-coder/references/verifier.md

diff --git a/skills/old-coder/SKILL.md b/skills/old-coder/SKILL.md
index b21502a..194cb2b 100644
--- a/skills/old-coder/SKILL.md
+++ b/skills/old-coder/SKILL.md
@@ -24,8 +24,8 @@ basis of trust.
 
 ```
 SPEC → (human approves spec, not code) → RED → GREEN → REFACTOR → GAUNTLET → EVIDENCE
-                                          ↑_____________________|
-                                              repeat per behavior
+                                          ↑_____________________|          ↘ [VERIFY] ↗
+                                              repeat per behavior         Tier 3, capped
 ```
 
 ### 1. SPEC — the only thing the human reads before code
@@ -106,7 +106,7 @@ or a tool is unavailable, record that in the evidence report with the reason.
 | Full test suite | regressions | project's test command, zero NEW failures (baseline note below) |
 | Static types | whole classes of bugs | tsc / mypy / etc., zero new errors |
 | Lint + format | latent bugs, drift | project's linter, zero new warnings |
-| Coverage on changed lines | untested code paths | every changed/added line executed by a test; branch coverage where the tool supports it. Global % is vanity — changed-line coverage is the constraint |
+| Coverage on changed lines | untested code paths | every changed/added line executed by a test; branch coverage where the tool supports it. Global % is vanity — changed-line coverage is the constraint. **This layer must exit nonzero when its threshold is missed** (`--cov-fail-under`, `diff-cover --fail-under`, equivalent): a layer that prints a percentage and exits 0 is a report, not a gauntlet layer, and it will sit there green while coverage falls |
 | Mutation testing | tests that assert nothing | see `references/gauntlet.md`. No mutation tool? Do manual mutation: introduce 3–5 plausible bugs into the new code one at a time (flip a comparison, off-by-one a bound, drop a condition, return early); the suite must kill every one. Restore after |
 | Property-based tests | edge cases you didn't imagine | for parsing, math, serialization, anything with invariants (round-trip, idempotence, ordering) — add hypothesis/fast-check properties |
 | Complexity budget | unmaintainable output | new functions small and single-purpose; if a function needs a paragraph to explain, split it |
@@ -137,7 +137,17 @@ gate code is a hard failure of the layer, never a pass; no `|| true`, no
 its pass**: run it once against a known-bad input (a negative control) and
 watch it fail — the RED principle applied to checkers, exactly like the
 throwaway mutant for an immediately-passing test. Record the control in
-EVIDENCE.
+EVIDENCE. Be precise about what that buys: **a negative control proves one
+known-bad case reaches the checker's failure path. It does not prove the
+checker recognizes every violation of the constraint it claims to enforce.**
+A grep gate can fail closed perfectly and still guard a spelling rather than
+a behavior. When the gate's coverage is narrower than the rule it serves, say
+so where the rule is written, rather than letting the rule imply more.
+
+Prove a negative control is itself non-vacuous the same way you prove a test:
+temporarily remove or break the defence it validates, and watch the control go
+red. A control that passes with the defence removed is measuring nothing —
+this is a one-time proof, not a permanent extra layer.
 
 Equivalent-mutant note — with a mutation tool, a survivor is not automatically
 a failure: some mutants are semantically equivalent to the original and cannot
@@ -146,7 +156,46 @@ EVIDENCE rather than adding a meaningless test to kill them — that would
 violate anti-gaming rule 4. Hand-written mutants (the manual procedure) get no
 such excuse: you chose them, so choose real bugs.
 
-### 6. EVIDENCE — the only thing the human reads after code
+### 6. VERIFY — fresh-context adversarial pass (Tier 3, experimental)
+
+One agent authored the spec, the tests, the implementation, the checkers, and
+the report that grades them. VERIFY adds a second agent at the end, with a
+fresh context, that attacks the work before EVIDENCE is finalized. It reduces
+**task-context** correlation — your framing, your justifications, the
+assumption you carried since turn 3. If the verifier runs on the same model
+or model family, model-level blind spots remain; a different model narrows
+those too. Neither is independence in a strong sense, and EVIDENCE says so.
+
+Marked experimental: it is expensive, and the evidence for it so far is one
+case study (`references/verifier.md`), not a benchmark.
+
+The non-negotiable rules — **the protocol is `references/verifier.md`, and
+VERIFY has not been performed until that file has been read in full and
+executed. Missing or unreadable → `blocked`, never `passed`.**
+
+- **Tier 3 runs it by default.** Skipping is a declared reduction in EVIDENCE,
+  never a silent one.
+- **Fresh context, four inputs only**: the task contract (the request plus
+  every requirement the human has approved since), the approved SPEC, the repo
+  at an exact source state, the gauntlet entry point. Never your conversation.
+- **Blind first, compare second.** The verifier reproduces and attacks alone,
+  records what it found, and only then sees the draft EVIDENCE. That record is
+  append-only afterwards.
+- **It fixes nothing.** A verifier that patches code becomes an author. A SPEC
+  gap goes back to the **human**, never to the builder to self-amend.
+- **Grade the findings, or this never terminates.** A **behavioural** finding
+  (the code does the wrong thing; a gate cannot fail) is fixed and re-verified
+  in a *new* verifier context. A **description or mapping** finding (the spec,
+  a comment, or EVIDENCE says something untrue about code that is correct) is
+  fixed and disclosed, and does **not** buy another round. Without this split,
+  "fix every finding" times "re-verify after every change" is a loop that ends
+  only when a round returns the empty set — and prose has no such fixpoint.
+- **Cap the rounds.** Two by default; more needs explicit human approval.
+- **Four states in EVIDENCE**: `passed` finalizes; `failed` and `blocked`
+  (verification could not be completed) do not; `not performed` finalizes only
+  as a declared downgrade, following the same rule as an unapproved spec.
+
+### 7. EVIDENCE — the only thing the human reads after code
 
 End with a report the human can trust without opening a single source file
 (template in `references/gauntlet.md`):
@@ -212,6 +261,8 @@ Scale effort to blast radius, and say which tier you chose:
   (tool-based if available) + adversarial pass — one explicit step trying to
   break your own implementation with hostile inputs before declaring done.
   Failure modes deliberately not covered go in EVIDENCE as known limits.
+  Then add VERIFY (§6): the adversarial pass is you attacking your own work
+  and shares your blind spots; a fresh context does not.
 
 ## Setup
 
diff --git a/skills/old-coder/references/gauntlet.md b/skills/old-coder/references/gauntlet.md
index 2094ef4..aea70a2 100644
--- a/skills/old-coder/references/gauntlet.md
+++ b/skills/old-coder/references/gauntlet.md
@@ -10,7 +10,7 @@ Makefile / CI config first). These are the defaults when nothing exists.
 | Tests | pytest | `pytest -q` |
 | Types | mypy | `mypy <pkg>` (or pyright) |
 | Lint + format | ruff | `ruff check . && ruff format --check .` |
-| Changed-line coverage | coverage.py | `pytest --cov=<pkg> --cov-branch --cov-report=term-missing` then verify the lines you touched appear covered; `diff-cover coverage.xml` automates changed-line % against git |
+| Changed-line coverage | coverage.py | `pytest --cov=<pkg> --cov-branch --cov-report=term-missing --cov-fail-under=<n>` — without the threshold flag the layer prints a number and exits 0, so it can never fail; `diff-cover coverage.xml --fail-under=100` gates changed lines specifically |
 | Mutation | mutmut (3+) | configure `[tool.mutmut] source_paths = ["src/"]` in pyproject.toml, then `mutmut run` (target one module with `mutmut run "my_module*"`); survivors = weak tests |
 | Property-based | hypothesis | `@given(...)` strategies for invariants |
 
@@ -196,6 +196,8 @@ scenario so the evidence report's spec→test mapping is mechanical.
   in prose is working-directory-sensitive and will fail to reproduce
 - Toolchain: <pinned versions file, e.g. requirements-dev.txt>
 - Entry point: <single command that reruns every layer>
+- Independent verification: <not performed | passed | failed | blocked>
+  (Tier 3; protocol and full template in `verifier.md`)
 
 ### Spec → Test mapping
 Status is one of: **pass / fail / unverified / n-a**. A row mapped to
@@ -219,6 +221,15 @@ Status is one of: **pass / fail / unverified / n-a**. A row mapped to
 | Supply chain | <cmd> | 0 known vulns; new deps: none (or list, each ↔ SPEC justification) |
 | Suite health | <cmd> | randomized order (seed <n>), all passed |
 
+### Independent verification (never omit; see verifier.md)
+- Verifier: <host / model family>; fresh context; which inputs it received;
+  what correlation that breaks and what it does not.
+- Rounds: <n> (cap <m>); verdict per round.
+- Attacked: <what was tried, not only what was found>.
+- Findings: behavioural (fixed, then re-verified in a new context) vs
+  description/mapping (fixed and disclosed, no new round).
+- Fixed after the last verified state, therefore unverified: <list | none>.
+
 ### Skipped layers
 - <layer>: <reason>  (or "none")
 
diff --git a/skills/old-coder/references/verifier.md b/skills/old-coder/references/verifier.md
new file mode 100644
index 0000000..b78e838
--- /dev/null
+++ b/skills/old-coder/references/verifier.md
@@ -0,0 +1,158 @@
+# VERIFY: fresh-context adversarial verification
+
+The protocol for SKILL.md §6. Read it in full before claiming VERIFY was
+performed; the summary in SKILL.md is not the protocol.
+
+## Inputs — exactly four
+
+Give the verifier:
+
+1. **The task contract.** The user's original request *plus every requirement,
+   scope change and spec revision a human has explicitly approved since*. Not
+   just the first message: without the approved changes, a legitimate scope
+   revision reads as a spec gap and the verifier reports a false positive.
+   Not the surrounding discussion either — no builder reasoning, defences,
+   suggestions, or unapproved explanations.
+2. **The approved SPEC.**
+3. **The repository at an exact source state** (commit SHA, or a tree hash
+   when git is absent).
+4. **The gauntlet entry point.**
+
+Withhold the builder's conversation and the draft EVIDENCE. If a claim needs
+the builder's justification to stand, it is not proven.
+
+The verifier reads the implementation freely — it is an attacker, not the
+human whose review you are trying to make optional.
+
+## Two phases
+
+**Blind.** The verifier reproduces and attacks on its own and records: the
+source state it observed, the numbers it got, its attack list, its initial
+findings. **Then** it is shown the draft EVIDENCE and compares. The blind
+record is append-only afterwards — comparison may add findings, never rewrite
+what the blind pass saw. Without this the verifier is anchored to the
+builder's framing and its fresh context is wasted.
+
+## Attack order
+
+Record what was tried at each surface, including the attacks that found
+nothing. The attack list is the deliverable; findings are a bonus.
+
+1. **The run.** Execute the entry point from the stated source state. Numbers
+   that disagree with the draft EVIDENCE mean the draft is wrong, not the run.
+   First confirm the environment actually tests the tree it claims to —
+   a copied virtualenv, a stale install, or a cached artifact can silently
+   exercise the original sources and make every later result meaningless.
+2. **The spec against the contract.** The one failure class a test suite
+   structurally cannot catch. What would a caller reasonably expect, given the
+   stated deployment, that no scenario or Must NOT covers? Approved exclusions
+   are not findings — but an approved exclusion *described inaccurately* is.
+3. **The tests.** Try to make the suite pass wrongly: implementation keyed to
+   test inputs, mocks swallowing the logic, assertions that cannot fail. Invent
+   mutants the builder did not choose; the builder's mutant list encodes the
+   builder's blind spots. Watch for tests that pin less than they claim — a
+   boundary pinned in one function and not in its twin, a magnitude left free
+   while its boundary is fixed, an assertion satisfied by a caller that never
+   arrived.
+4. **The checkers.** Feed every home-grown gate a known-bad input and confirm
+   it fails. Then ask the harder question: does it cover the constraint it
+   claims, or only one spelling of it?
+5. **The mapping, both directions.** Every scenario, Must NOT and
+   failure-model row must name a falsification procedure that can be made to
+   fail. Also look the other way: tests with no scenario, and demonstrated
+   failure modes with no row.
+
+**Before reporting any surviving mutant, prove it diverges.** Construct a
+concrete input where mutant and original disagree. A survivor you cannot make
+disagree is an equivalent mutant, and reporting it as a defect sends the
+builder to write a test that asserts non-behavior.
+
+## The verifier fails closed too
+
+- "Looks good" is not a verdict.
+- It fixes nothing. Findings return through the normal loop. A **SPEC gap goes
+  to the human**, never to the builder to self-amend. An EVIDENCE number that
+  disagrees with the rerun is a report defect: fix the report, then a full
+  fresh run.
+- If it cannot complete verification — missing tool, no fresh context
+  available, this file unreadable — that is `blocked`, not a skip.
+- **Optional canary.** Run it once against a build with a planted defect and
+  watch it catch it. Plant in an isolated copy, never in the candidate; the
+  verifier must not know the defect's location or kind; a missed canary voids
+  that verdict. A caught canary is a floor, not a capability proof: it shows
+  the verifier can reject one obvious error, nothing about coverage.
+
+## Grading findings — the rule that makes this terminate
+
+| Finding | Response |
+|---|---|
+| **Behavioural**: the code does the wrong thing, or a gate cannot fail | fix, then re-verify in a **new** verifier context |
+| **Description / mapping**: the spec, a comment or EVIDENCE says something untrue about code that is correct | fix and disclose; **no new round** |
+
+Without this split, "fix every finding" times "start a new verifier after any
+change" is a loop that terminates only when a round returns the empty set.
+Prose has no such fixpoint.
+
+Cap at two rounds by default. More needs explicit human approval, recorded.
+
+## Four states, recorded in EVIDENCE
+
+| State | May EVIDENCE be finalized? |
+|---|---|
+| `passed` | yes |
+| `failed` | no |
+| `blocked` — verification could not be completed | no |
+| `not performed` | only as a declared downgrade, with the reason, exactly like an unapproved spec |
+
+EVIDENCE records the verdict, the verifier's host and model family, whether
+the context was fresh, which inputs it received, the attack list, each finding
+and its resolution, and any canary. When findings were fixed **after** the
+last verified state, say which — they are not independently verified.
+
+## Report template
+
+```markdown
+### Independent verification
+- Verifier: <host / model family>; fresh context; given repo @ <state> + task
+  contract + SPEC + entry point. Not given the builder's conversation.
+  Correlation broken: task context. Not broken: model.
+- Rounds: <n> (cap <m>). Round <k> verdict: <passed|failed|blocked>.
+- Attacked: <run | spec vs contract | test-gaming | checker coverage | mapping>
+  — what was tried, not only what was found.
+- Findings: <behavioural: ... → fix + round n+1> / <description: ... → fixed,
+  disclosed> (or "none survived the attacks listed above")
+- Canary: <planted defect → caught | MISSED, verdict void | not run>
+- Fixed after the last verified state, therefore unverified: <list | none>
+```
+
+## What one case study showed
+
+Six rounds against a 99-line Python rate limiter that was already passing ten
+gauntlet layers, 100% branch coverage and 8/8 mutation, with a
+multiply-rebound evidence report. Same model as the builder throughout, so
+this measures reproducibility, not model independence. Roughly 550k tokens.
+
+- **Rounds 1–3 found five behavioural defects** nothing in the gauntlet could
+  reach: an unbounded key map usable as a remote memory-exhaustion attack
+  against the component meant to prevent one; `limit=NaN` producing a limiter
+  that always allowed; 2× over-allow under threads; a lock that covered
+  check-and-append but not the clock read; and — the most transferable one —
+  a mutation runner reporting kills for mutants it never executed, because
+  two same-size mutants written in the same second shared a bytecode cache.
+  That last defect could only ever inflate the score, so it could never
+  surface as a red gauntlet.
+- **Rounds 4–6 found one behavioural gap and a stream of prose inaccuracies**,
+  two of which were introduced by the round that fixed the previous one. That
+  is why a single clean round does not mean converged, and why the grading
+  rule above exists. The marginal round was clearly negative by round 5.
+- **An A/B design failed.** Planting a defect in one copy and verifying a
+  clean copy as a false-positive control did not work: the "clean" copy was
+  not clean — it independently invented the planted mutation and correctly
+  reported it. No false-positive rate could be measured. The two false
+  positives that did occur were both caused by feeding the verifier a
+  subdirectory instead of the repository, and a tree polluted by an editable
+  install. **Verifier noise tracked input quality.**
+- **Verification's late-stage output is not bugs.** It is the discovery that
+  SPEC and EVIDENCE are describing code that does something else — which
+  matters precisely because those two documents are the only things the human
+  reads.

From 3504c4adac1edb6c2e5ebdd16ccf31a7f47639fa Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 17:08:32 +0800
Subject: [PATCH 11/12] skill: move independent verification out of the loop
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It was numbered step 6, between GAUNTLET and EVIDENCE, which put it alongside
RED/GREEN/GAUNTLET and implied it is the same kind of thing. It is not. Every
gauntlet layer is a command that returns an exit code in seconds; this is an
agent that takes minutes and returns prose a human has to grade — findings to
classify, equivalent mutants to rule out, false positives to dismiss. Framing
it as a stage promised a fit the form does not have, and it quietly spent the
one resource this skill otherwise guards: human attention.

Now a Tier 3 assurance option after Calibration, with the loop back to its six
stages. Content unchanged; position and self-description are not.

Two things the earlier framing left unsaid and now says:

- The gauntlet is not what is in question. It proves the code satisfies every
  constraint the spec expresses and does that well. Verification exists
  because the SPEC can be incomplete and EVIDENCE can describe code that does
  something else — not because the layers are inadequate. Without that line,
  "you also need another agent" reads as a retreat from the skill's own claim
  that constraints replace inspection.
- Grading findings buys termination by giving up completeness, and the case
  study proves it: the round that this rule would have skipped is the round
  that found an unpinned threshold magnitude. The cap is likewise not a
  spending limit — it converts silent spending into someone's decision, which
  is exactly what was missing when six rounds ran unchecked.

On Tier 3, `not performed` is now stated as the default that needs no apology.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 skills/old-coder/SKILL.md               | 106 ++++++++++++++----------
 skills/old-coder/references/verifier.md |  19 ++++-
 2 files changed, 79 insertions(+), 46 deletions(-)

diff --git a/skills/old-coder/SKILL.md b/skills/old-coder/SKILL.md
index 194cb2b..297aafa 100644
--- a/skills/old-coder/SKILL.md
+++ b/skills/old-coder/SKILL.md
@@ -24,8 +24,8 @@ basis of trust.
 
 ```
 SPEC → (human approves spec, not code) → RED → GREEN → REFACTOR → GAUNTLET → EVIDENCE
-                                          ↑_____________________|          ↘ [VERIFY] ↗
-                                              repeat per behavior         Tier 3, capped
+                                          ↑_____________________|
+                                              repeat per behavior
 ```
 
 ### 1. SPEC — the only thing the human reads before code
@@ -156,46 +156,7 @@ EVIDENCE rather than adding a meaningless test to kill them — that would
 violate anti-gaming rule 4. Hand-written mutants (the manual procedure) get no
 such excuse: you chose them, so choose real bugs.
 
-### 6. VERIFY — fresh-context adversarial pass (Tier 3, experimental)
-
-One agent authored the spec, the tests, the implementation, the checkers, and
-the report that grades them. VERIFY adds a second agent at the end, with a
-fresh context, that attacks the work before EVIDENCE is finalized. It reduces
-**task-context** correlation — your framing, your justifications, the
-assumption you carried since turn 3. If the verifier runs on the same model
-or model family, model-level blind spots remain; a different model narrows
-those too. Neither is independence in a strong sense, and EVIDENCE says so.
-
-Marked experimental: it is expensive, and the evidence for it so far is one
-case study (`references/verifier.md`), not a benchmark.
-
-The non-negotiable rules — **the protocol is `references/verifier.md`, and
-VERIFY has not been performed until that file has been read in full and
-executed. Missing or unreadable → `blocked`, never `passed`.**
-
-- **Tier 3 runs it by default.** Skipping is a declared reduction in EVIDENCE,
-  never a silent one.
-- **Fresh context, four inputs only**: the task contract (the request plus
-  every requirement the human has approved since), the approved SPEC, the repo
-  at an exact source state, the gauntlet entry point. Never your conversation.
-- **Blind first, compare second.** The verifier reproduces and attacks alone,
-  records what it found, and only then sees the draft EVIDENCE. That record is
-  append-only afterwards.
-- **It fixes nothing.** A verifier that patches code becomes an author. A SPEC
-  gap goes back to the **human**, never to the builder to self-amend.
-- **Grade the findings, or this never terminates.** A **behavioural** finding
-  (the code does the wrong thing; a gate cannot fail) is fixed and re-verified
-  in a *new* verifier context. A **description or mapping** finding (the spec,
-  a comment, or EVIDENCE says something untrue about code that is correct) is
-  fixed and disclosed, and does **not** buy another round. Without this split,
-  "fix every finding" times "re-verify after every change" is a loop that ends
-  only when a round returns the empty set — and prose has no such fixpoint.
-- **Cap the rounds.** Two by default; more needs explicit human approval.
-- **Four states in EVIDENCE**: `passed` finalizes; `failed` and `blocked`
-  (verification could not be completed) do not; `not performed` finalizes only
-  as a declared downgrade, following the same rule as an unapproved spec.
-
-### 7. EVIDENCE — the only thing the human reads after code
+### 6. EVIDENCE — the only thing the human reads after code
 
 End with a report the human can trust without opening a single source file
 (template in `references/gauntlet.md`):
@@ -261,8 +222,65 @@ Scale effort to blast radius, and say which tier you chose:
   (tool-based if available) + adversarial pass — one explicit step trying to
   break your own implementation with hostile inputs before declaring done.
   Failure modes deliberately not covered go in EVIDENCE as known limits.
-  Then add VERIFY (§6): the adversarial pass is you attacking your own work
-  and shares your blind spots; a fresh context does not.
+  The adversarial pass is you attacking your own work and shares your blind
+  spots; where a spec gap would be expensive, consider independent
+  verification below — a different kind of assurance, not another layer.
+
+## Independent verification (Tier 3 option, experimental)
+
+The gauntlet is not what is in question here. It proves the code satisfies
+every constraint the spec expresses, and it does that well. What no layer can
+check is whether the **spec expresses the right constraints**, or whether
+EVIDENCE honestly describes the code that shipped. Human spec approval is this
+skill's answer to the first — but it happens before any code exists, so it
+cannot catch anything you did afterwards.
+
+Independent verification is a second answer for stakes that justify one: a
+fresh-context agent that attacks the finished work before EVIDENCE is signed.
+It reduces **task-context** correlation — your framing, your justifications,
+the assumption you carried since turn 3. On the same model or model family,
+model-level blind spots remain. Neither is independence in a strong sense, and
+EVIDENCE says so.
+
+**It is not a gauntlet layer.** Every layer is a command that returns an exit
+code in seconds. This is an agent that takes minutes, costs tokens on the
+order of a small task, and returns **prose someone has to judge** — findings
+to grade, equivalent mutants to rule out, false positives to dismiss. It
+spends the one resource this skill otherwise guards carefully: human
+attention. Reach for it when a spec gap would be expensive and the code is
+already green, not because a task feels important.
+
+Marked experimental: the evidence for it is one case study, written up in
+`references/verifier.md`, not a benchmark.
+
+The non-negotiable rules — **the protocol is `references/verifier.md`, and
+verification has not been performed until that file has been read in full and
+executed. Missing or unreadable → `blocked`, never `passed`.**
+
+- **Fresh context, four inputs only**: the task contract (the request plus
+  every requirement the human has approved since), the approved SPEC, the repo
+  at an exact source state, the gauntlet entry point. Never your conversation.
+- **Blind first, compare second.** The verifier reproduces and attacks alone,
+  records what it found, and only then sees the draft EVIDENCE. That record is
+  append-only afterwards.
+- **It fixes nothing.** A verifier that patches code becomes an author. A SPEC
+  gap goes back to the **human**, never to the builder to self-amend.
+- **Grade the findings, or this never terminates.** A **behavioural** finding
+  (the code does the wrong thing; a gate cannot fail) is fixed and re-verified
+  in a *new* verifier context. A **description or mapping** finding (the spec,
+  a comment, or EVIDENCE says something untrue about code that is correct) is
+  fixed and disclosed, and does **not** buy another round. Without this split,
+  "fix every finding" times "re-verify after every change" is a loop that ends
+  only when a round returns the empty set — and prose has no such fixpoint.
+  The trade is real: grading buys termination by giving up completeness, and a
+  behavioural gap can survive inside a round you chose not to run.
+- **Cap the rounds.** Two by default; more needs explicit human approval. The
+  cap does not stop the spending, it makes the spending someone's decision.
+- **Four states in EVIDENCE**: `passed` finalizes; `failed` and `blocked`
+  (verification could not be completed) do not; `not performed` finalizes only
+  as a declared downgrade, following the same rule as an unapproved spec. On
+  Tier 3, `not performed` is the default and needs no apology — say so and
+  claim correspondingly less.
 
 ## Setup
 
diff --git a/skills/old-coder/references/verifier.md b/skills/old-coder/references/verifier.md
index b78e838..57ddc9e 100644
--- a/skills/old-coder/references/verifier.md
+++ b/skills/old-coder/references/verifier.md
@@ -1,7 +1,13 @@
 # VERIFY: fresh-context adversarial verification
 
-The protocol for SKILL.md §6. Read it in full before claiming VERIFY was
-performed; the summary in SKILL.md is not the protocol.
+The protocol for the "Independent verification" section of SKILL.md. Read it
+in full before claiming verification was performed; the summary in SKILL.md is
+not the protocol.
+
+This is not a gauntlet layer and should not be run like one. Every layer is a
+command returning an exit code; this is an agent returning prose that a human
+has to grade. It exists because the gauntlet can only check what the spec
+says — the gauntlet is not what is in question.
 
 ## Inputs — exactly four
 
@@ -93,7 +99,16 @@ Without this split, "fix every finding" times "start a new verifier after any
 change" is a loop that terminates only when a round returns the empty set.
 Prose has no such fixpoint.
 
+**Be clear about the trade.** Grading buys termination by giving up
+completeness. A behavioural gap can live inside a round you chose not to run —
+in the case study below, the round that would have been skipped under this
+rule is the one that found an unpinned threshold magnitude. That is the price,
+and it is worth paying, because the alternative is a process with no stopping
+condition at all. Say in EVIDENCE which rounds were not run.
+
 Cap at two rounds by default. More needs explicit human approval, recorded.
+The cap does not stop the spending; it makes the spending someone's decision,
+which is the part that was missing when this protocol was first drafted.
 
 ## Four states, recorded in EVIDENCE
 

From 55c8467879c643e20e170e21dc3e1867b886f516 Mon Sep 17 00:00:00 2001
From: "Li, Amazing Ang" <d0u.gie@hotmail.com>
Date: Mon, 10 Aug 2026 17:19:21 +0800
Subject: [PATCH 12/12] evidence: the spec prune belongs in the unverified list
 too

The prune of spec.md (339 -> 255 lines, 8b88bda) came after the last verified
state and was not listed alongside the other post-round-6 changes. No clause
changed, but it is a large edit to the document a verifier attacks hardest,
and omitting it is the same accuracy defect six rounds kept finding.

Also notes why the cited commit is not HEAD: later commits touch only skills/,
which is outside the hashed tree, so the binding is current rather than stale.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 demo-rate-limiter/evidence.md | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/demo-rate-limiter/evidence.md b/demo-rate-limiter/evidence.md
index f58ac08..255ca24 100644
--- a/demo-rate-limiter/evidence.md
+++ b/demo-rate-limiter/evidence.md
@@ -10,7 +10,9 @@
 - Source state: git commit `8b88bda`; sha256 tree hash `c80e8cccf0a1ed3a` —
   reproduce both with `./tools/source_state.sh` (works from any directory;
   now includes `.github/workflows`, which decides whether the gauntlet runs
-  in CI at all).
+  in CI at all). Commits after `8b88bda` on this branch touch only
+  `skills/`, which is outside the hashed tree — hence the same hash at a
+  later HEAD, not a stale binding.
 - Toolchain: pinned in `requirements-dev.txt` (local run: Python 3.14.3;
   CI runs the same gauntlet on 3.12 via `.github/workflows/gauntlet.yml`).
 - Entry point: `./tools/gauntlet.sh` reruns every layer below.
@@ -129,7 +131,10 @@ round 6 and are therefore **not independently verified**:
 
 - the sweep threshold magnitude test and mutant M23;
 - the vacuous-pass assertion added to the clock-ordering test;
-- the six prose corrections listed in commit `66df5cd`.
+- the six prose corrections listed in commit `66df5cd`;
+- the prune of `spec.md` from 339 to 255 lines in commit `8b88bda`. No clause
+  was changed, but it is a large edit to the document a verifier attacks
+  hardest, and it was made after the last verified state.
 
 ## Honest notes