diff --git a/demo-rate-limiter/evidence.md b/demo-rate-limiter/evidence.md index e95bbc3..255ca24 100644 --- a/demo-rate-limiter/evidence.md +++ b/demo-rate-limiter/evidence.md @@ -1,15 +1,30 @@ # 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 `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). 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. 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.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 @@ -23,97 +38,173 @@ 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`; +- 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 -- **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. diff --git a/demo-rate-limiter/spec.md b/demo-rate-limiter/spec.md index 6b249c4..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,99 +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: request at the exact window boundary is still limited + 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 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, or a negative limit, or window_seconds <= 0 + 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/always allows is a security bug) + (a limiter that silently never or always allows is a security bug) + + 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 + (every comparison against NaN is false, so the limiter allowed forever) - 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 + 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 - 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] + 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 - 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 + When "Alice", "alice", "alice " and " " each make a request + Then all are allowed — they are four different callers - Scenario: non-monotonic clock does not grant extra quota + Scenario: concurrent callers never exceed the limit 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) + 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 + 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 pruning and sweeping assume that order) + + 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: 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, so residency reaches 2W before the dropping sweep) + + 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 + + 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 + + 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 + + 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 ``` ## 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 -- No real time.sleep / wall-clock dependence in tests. -- No unbounded memory growth from denied requests (denials store nothing). +- **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; (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. + +## 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. ## 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.] +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 | 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) | -| 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 | -| 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). + (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 + +- **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. 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/src/ratelimiter/__init__.py b/demo-rate-limiter/src/ratelimiter/__init__.py index 0eb64f1..2434c85 100644 --- a/demo-rate-limiter/src/ratelimiter/__init__.py +++ b/demo-rate-limiter/src/ratelimiter/__init__.py @@ -1,49 +1,99 @@ """Sliding-window rate limiter with an injectable clock.""" import math +import threading from collections import deque from collections.abc import Callable __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. - `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 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__( self, limit: int, window_seconds: float, clock: Callable[[], float] ) -> None: - 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 + 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.""" - now = self._clock() - hits = self._prune(key, now) - if len(hits) >= self._limit: - return False - hits.append(now) - self._hits[key] = hits - return True + 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") + # 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: + 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.""" + # 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] + 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.""" + """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() - 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 a00ea5f..a6c0576 100644 --- a/demo-rate-limiter/tests/test_properties.py +++ b/demo-rate-limiter/tests/test_properties.py @@ -6,15 +6,35 @@ 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) +# 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. 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) -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,14 +63,20 @@ 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: + 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 8ab36a0..f37f408 100644 --- a/demo-rate-limiter/tests/test_ratelimiter.py +++ b/demo-rate-limiter/tests/test_ratelimiter.py @@ -1,6 +1,10 @@ -"""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 +import threading +from typing import Any import pytest from conftest import FakeClock @@ -91,5 +95,277 @@ 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) + + +@pytest.mark.parametrize("window", [True, "60", None]) +def test_window_seconds_must_be_a_number(clock: FakeClock, window: Any) -> None: + # 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 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 + 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: + # _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 + 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_a_key_is_dropped_by_the_first_sweep_after_one_idle_window( + clock: FakeClock, +) -> None: + # 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 + 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 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 + 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_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: + # 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 + 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: + # 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 + 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" + + +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_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_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"]) + # 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}" + + +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 + # 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: + 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..b53c727 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 @@ -11,7 +14,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,11 +26,28 @@ echo "=== lint + format ===" echo "=== supply chain ===" "$PY/pip-audit" -r requirements-dev.txt echo "=== must-not scans ===" -must_not_match 'time\.' 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 +# Matches usage forms, not the word: `time\.` alone missed `from time import +# 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 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 +# 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|BEGIN[[:space:]]+[A-Z ]*PRIVATE' \ + 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 c415a65..ce11199 100644 --- a/demo-rate-limiter/tools/mutants.py +++ b/demo-rate-limiter/tools/mutants.py @@ -5,14 +5,27 @@ 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), 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 = [ ( "M1 flip limit comparison >= to >", @@ -26,7 +39,7 @@ ), ( "M3 drop recording of allowed hit", - " hits.append(now)\n", + " hits.append(now)\n", "\n", ), ( @@ -36,8 +49,8 @@ ), ( "M5 deny becomes allow (fail open)", - " return False", - " return True", + " return False", + " return True", ), ( "M6 prune from wrong end", @@ -51,15 +64,191 @@ ), ( "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', + "", + ), + ( + "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', + "", + ), + ( + "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:", + ), + # [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", + ), + # [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:", + ), + # [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", + ), + # [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: 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:"), + ( + "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 @@ -67,23 +256,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: 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" diff --git a/skills/old-coder/SKILL.md b/skills/old-coder/SKILL.md index b21502a..297aafa 100644 --- a/skills/old-coder/SKILL.md +++ b/skills/old-coder/SKILL.md @@ -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 @@ -212,6 +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. + 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/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 ` (or pyright) | | Lint + format | ruff | `ruff check . && ruff format --check .` | -| Changed-line coverage | coverage.py | `pytest --cov= --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= --cov-branch --cov-report=term-missing --cov-fail-under=` — 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: - Entry point: +- Independent verification: + (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 | | 0 known vulns; new deps: none (or list, each ↔ SPEC justification) | | Suite health | | randomized order (seed ), all passed | +### Independent verification (never omit; see verifier.md) +- Verifier: ; fresh context; which inputs it received; + what correlation that breaks and what it does not. +- Rounds: (cap ); verdict per round. +- Attacked: . +- 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: . + ### Skipped layers - : (or "none") diff --git a/skills/old-coder/references/verifier.md b/skills/old-coder/references/verifier.md new file mode 100644 index 0000000..57ddc9e --- /dev/null +++ b/skills/old-coder/references/verifier.md @@ -0,0 +1,173 @@ +# VERIFY: fresh-context adversarial verification + +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 + +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. + +**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 + +| 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: ; fresh context; given repo @ + task + contract + SPEC + entry point. Not given the builder's conversation. + Correlation broken: task context. Not broken: model. +- Rounds: (cap ). Round verdict: . +- Attacked: + — what was tried, not only what was found. +- Findings: / (or "none survived the attacks listed above") +- Canary: +- Fixed after the last verified state, therefore unverified: +``` + +## 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.