Skip to content

docs: record the property-invariant wave in the audit delivery log #602

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ndycode wants to merge 1 commit into
base: main
Choose a base branch
from
Open

docs: record the property-invariant wave in the audit delivery log #602

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 35 additions & 0 deletions docs/audits/AUDIT_2026-06-10.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -242,6 +242,41 @@ tracking issue and a maintainer MCP-auth test — not PRs; it also skips

---

### 5.3 Property-invariant wave (added 2026-06-11, after the direct-coverage merge)

With direct coverage converged (§5.2), the remaining test risk was
example-blindness: the pure state machines, parsers, and formatters were
pinned at hand-picked points but not across their input spaces. This wave
adds fast-check property suites for every such module, following the
conventions #574/#575 established (plain `fc.assert`, explicit vitest
imports, injectable clocks or scoped fake timers, per-iteration namespacing
for module state). The dedup-idempotence bug #579 found earlier in the
cycle is the method's strongest precedent.

Outcome worth recording: across roughly fifty properties, **no production
bug was found** — the implementations held against every generated
counterexample — while the review cycle caught **three latent defects in
the test harnesses themselves** (a padding/content conflation in #595, an
expiry-inheritance model divergence in #594, a dropped async-property
promise in #600), and fast-check found two more harness modeling gaps
before push (#592, #594). The wave hardened the tests as much as it
verified the code.

| PR | Suite | Pins |
|----|-------|------|
| [#592](https://github.com/ndycode/codex-multi-auth/pull/592) | `test/property/circuit-breaker.property.test.ts` | availability is a faithful prediction of the next `canExecute` under any event sequence; exact open-window timing incl. `getTimeUntilReset`; threshold exactness; window expiry; half-open probe discipline |
| [#593](https://github.com/ndycode/codex-multi-auth/pull/593) | `test/property/auth-rate-limit.property.test.ts` | sliding-window oracle equivalence through decorated id spellings (trim+lowercase bucketing); `AuthRateLimitError` payload fidelity; over-recorded bursts never wedge a bucket past one quiet window |
| [#594](https://github.com/ndycode/codex-multi-auth/pull/594) | `test/property/session-affinity.property.test.ts` | TTL/upsert model equivalence; LRU capacity with newest-write survival; stale write-version conflicts; `forgetAccount`+`reindexAfterRemoval` as an array splice; prune exactness under lazy reaps; `clearAll` (#474) |
| [#595](https://github.com/ndycode/codex-multi-auth/pull/595) | `test/property/table-formatter.property.test.ts` | every line of any table keeps the exact layout display width under CJK/emoji content (ui-02); fit preservation per alignment incl. the default; truncation to prefix+ellipsis on either alignment; zero-width columns |
| [#596](https://github.com/ndycode/codex-multi-auth/pull/596) | `test/property/health.property.test.ts` | healthy-classification oracle incl. status partition edges; open AND half-open circuits disqualify (fake-timer probe); shared-email circuit aliasing via the SUT's own identity key; report flag exactness |
| [#597](https://github.com/ndycode/codex-multi-auth/pull/597) | `test/property/model-map.property.test.ts` | closed world (every resolution lands on a profile key); idempotence; prefix+casing invariance incl. combined mutation; codex dominance and its general-GPT-5 inverse; full alias-map fidelity |
| [#598](https://github.com/ndycode/codex-multi-auth/pull/598) | `test/property/display-width.property.test.ts` | totality/bounds over joiner-modifier soup; plain-alphabet additivity (the table formatter's assumption); truncation self-consistency, budget monotonicity, and self-enforcing 2-column cluster granularity; `parseKey` totality |
| [#599](https://github.com/ndycode/codex-multi-auth/pull/599) | `test/property/forecast.property.test.ts` | recommendation soundness over the reachable domain; ready dominance by minimal risk; shortest-delayed-wait fallback; blocker-class guidance for empty pools (the `exhausted`-flag guard); permutation invariance; summary partition |
| [#600](https://github.com/ndycode/codex-multi-auth/pull/600) | `test/property/context-overflow.property.test.ts` | the seven overflow phrases behind the 400 gate at any casing/position; noise never classifies; the synthetic SSE round-trips as Responses-API dialect (recovery-01) and never re-classifies — no recursion |
| [#601](https://github.com/ndycode/codex-multi-auth/pull/601) | `test/property/env-policy-parsing.property.test.ts` | `parseBooleanEnv` literal contract and negative totality; policy keys as non-leaking sha256 handles with accountId>email precedence; tag normalization as idempotent fixpoints, null exactly on whitespace-only input |

---

## 6. Findings investigated and REJECTED (do not re-report)

Recorded so future audits do not re-litigate them; each was claimed by an automated pass and disproven by hand.
Expand Down