---
name: wspec-access-model
description: "W-SPEC (milestone A ACCESS-CONTROL): TLA+ access-model spec authored + TLC-verified on spec/access-model @e217543; 8 weakened variants each killing a distinct invariant; blocked from CI until the spec pilot lands on origin."
metadata: 
  node_type: memory
  type: project
  originSessionId: 8d605b6b-3ae2-438f-91d8-9d74a3a6a050
  modified: 2026-07-30T02:13:34.132Z
---

**W-SPEC = the TLA+ access-model spec**, milestone A (ACCESS-CONTROL, releases#20), dispatched to chert by doyle 2026-07-29. Lands LAST, right before doyle assembles the golden branch. Branch `spec/access-model` (worktree `.worktrees/access-model`, off main @ffc7e9e), pushed to origin **@e217543**, 3 commits. `REQ-SPEC-ACCESS-MODEL` minted, doc stage active.

**Checked properties** (doyle-ruled; `specs/access_model/AccessModel.tla`): TOTALITY (`InvTotality` no fall-through / `InvUniqueTierMatch` single-valued / `InvPrecedence` scope order / `InvChainOrder` full 8-tier order), FAIL-CLOSED (`InvFailClosed`, keyed on RAW store health so a guard reclassifying an error path as healthy is caught), NO-REMOTE-FLIP (`InvNoRemoteFlip`, witness variable), NO-UNAUTHENTICATED-ALLOW (`InvNoUnauthenticatedAllow` = hazard 7.5 formalized), MINT-IS-LOUD (`InvMintIsLoud`). Main cfg green **123,842 states ~14s**; MaxWrites=3 (measured: 4 is also green at 1,297,836 states / ~95s — recorded as a measured exclusion, not an argued one). `stampAuthentic` is nondeterministic at Init so ONE run covers both the W1 world (tier 1 inert) and the W2b world (authenticated sender stamp).

**⭐ The deliverable is the kill-mapping, not the green run.** Eight `weakened/*.cfg` variants, each tripping a DISTINCT target invariant — that is what proves no invariant is vacuous. FailOpenDegrade + MintFailOpens → InvFailClosed; ForgedSenderTier1 → InvNoUnauthenticatedAllow; GossipFlipsPosture → InvNoRemoteFlip; NoChainBottom → InvTotality; NodeEntryWins → InvPrecedence; SubnetWildcardWins → InvChainOrder; SilentReMint → InvMintIsLoud. doyle ruled weakened variants MAY encode rejected designs (not only shipped-and-fixed bugs), provided each cfg comment names its provenance class.

**⭐⭐ Spec-discovered defect (ruled, product one-liner on todlando's W2 stack): the baseline mint is per-PROCESS.** ADR-0053's mint-on-first-load says "a restart re-mints (boot is a first load)". So delete the store + get the daemon restarted ⇒ empty re-mint: every rule gone, node back at unconfigured-open, **health OK and the chain perfectly total — no verdict invariant can catch it**. The node has no memory outside the store, so it cannot distinguish a malicious wipe from a true first boot. Ruling: the mint must be **LOUD** (diagnostic names the EVENT, not the loss — the wiped rule count is unknowable post-deletion); loudness is the whole defense because monitoring sees what the node cannot judge.

**⭐ The fidelity gate caught a defect in its own author's edit.** `SilentReMint` first ran GREEN — correctly: a bulk edit had swallowed MintOnLoad's `UNCHANGED` clause, so the mint counters never incremented and `InvMintIsLoud` was vacuously true. **A variant that fails to fail is the signal `weakened/` exists to produce.** Recorded in the commit message rather than quietly fixed.

**How to apply / traps:**
- TLC litters the spec dir with `states/` + `*_TTrace_*.{tla,bin}`. These MUST be gitignored — CI's weakened runner does `mod=$(basename "$specdir"/*.tla .tla)`, so a stray second `.tla` breaks the glob.
- A cfg's basename MUST equal the module filename for the main config (CI derives `-config $mod.cfg $mod.tla`), so a spec dir can hold only ONE must-pass cfg. Alternative worlds have to ride the main model via nondeterministic Init, not a second cfg.
- Ruled A1 (doyle): same-node loopback SURVIVES the degrade like the reply exemption — adversary is REMOTE agents, a local actor already has file access, so denying loopback buys no security and self-DoSes a degraded node.
- SOURCES.txt is fully populated INCLUDING paths that do not exist yet — the drift gate keys on paths a PR touches, so listing the milestone's target modules arms it the moment they appear. doyle sequences W-SPEC last so no build PR ever hits the armed gate; `[spec-nochange]` is the fallback.

**REBASED ONTO THE PILOT 2026-07-29 (todlando in doyle's seat, doyle's session died on a spend limit).** Branch now **@f54bd7b on origin**, rebased onto pilot `@fdb4b42`: `200d5b4` rebase + `57ac30e` (8 `\* expects:` lines, each cfg's `INVARIANTS` narrowed to the one declared name) + `f54bd7b` (specs/README.md record). Old tip `e217543` preserved on origin at `backup/access-model-pre-rebase` — todlando's push protocol: push the backup ref FIRST, then **assert the old sha is reachable from an ORIGIN ref** (`git branch -r --contains`, confirmed against `git ls-remote`, not local tracking), only then `--force-with-lease` (never bare `--force`; lease refuses if origin moved since your fetch — so do NOT fetch first, a stale tracking ref makes the lease stricter).
- **Narrowing is free, and it is also the trap probe.** TLC halts at the FIRST violation, so a nine-name list on a variant built to violate never verified the other eight — it only widened what the gate accepts. And if a variant now goes GREEN post-narrowing, its real kill was a different invariant the broad list was masking.
- **All 8 flip exactly ONE guard**, so none carries RenameFollow's 2-flip/2-expects shape (see [[tla-spec-pilot-progress]]).
- **⭐ Seed filed, not dispatched: `InvUniqueTierMatch` is killed by NO variant** ⇒ zero fidelity pin, so nothing in the battery would notice if it silently stopped being checked. `TypeOK` is unkilled in both specs but is arguably defensible (type invariant every well-formed variant satisfies by construction); an access invariant is not. Recorded in `specs/README.md` as an open question for the gater.
- **Still owed, box-gated** (hfenduleam is gate box AND CI runner; a golden run was in flight): the 8 post-narrowing fidelity checks, one main-cfg re-check, and `traceable-reqs check` — the last deferred as co-tenant I/O under the extended disposal rule 3 (a recursive walk over the scan roots is not free; todlando confirmed it costs real seconds).
- ✅ **RESOLVED BY MEASUREMENT 2026-07-30 — the cfg comment is WRONG and 123,842 is right.** Measured at `f54bd7b` on hfenduleam, tla2tools v1.7.4: **437,678 states generated, 123,842 distinct** (exactly one such line in the log, population counted not sampled). The tracked comment's *"Measured: 123,746"* does not reproduce, and it is NOT a moved-bounds story — `AccessModel.tla` blob `9b1fef5e8cc0` and `AccessModel.cfg` blob `214a8c48aaab` are byte-identical at `e217543` and `f54bd7b`. ⭐⭐ **And this is genuinely INDEPENDENT provenance, unlike the same-artifact re-readings we kept having to caveat:** 123,842 was already measured on **kitsubito under TLC 2.19** on 2026-07-29 (see [[tla-spec-pilot-progress]], 14/14 compat run) — so two boxes, two TLC versions ~2 years apart, same number. 123,746 has never been reproduced by anyone. Fix pending doyle's word: one comment-only commit, CONSTANTS/INVARIANTS untouched.

**⚠ Blocked on:** the spec pilot (tla CI job + ADR-0035 + specs/README.md) still rides `spec/brain-handoff-pilot`, which has NO PR on origin. So W-SPEC gets no CI check until that lands on main and I rebase (README spec-map row + wave-2 backlog ride that follow-up). doyle ruled **I open that PR on his GO-PR ping, not before** (origin PRs still trigger the OLD full ci.yml on both boxes). I own three verdicts on that PR: java preflight, the tla job itself, and the tla2tools sha pin.

**Open:** CI pins tla2tools 1.8.0 sha `9e27b5e1…`; two independent fetches of that exact URL now give `cc4803dc…` (4485995 bytes, valid jar — it is what I model-checked with). If it trips, verify against a second source and record old→new sha in the bump commit — never just replace a pin.

Related: [[tla-spec-pilot-progress]], [[mirror-repo-ci-dead]], [[access-control-grill-2026-07]], [[agent-roles]].