WS1 follow-ups: concurrency stage-2 + the remaining STRIDE mechanisms (M-3..M-7)

Tracking issue for the work that follows the WS1 stage-1 landing (`8859fab`,
`\guarded_by` / `\stable_check`). That commit went directly to `master`; from here,
each item below should land via a **branch + PR** (the review discipline this issue
establishes). Context: the parent repo's `extended-stride-coverage-impl.md` (§2.1 macsl
bucket) and `macsl/docs/ws-mechanisms.md` (the design stubs).

### Done (on master)
- [x] **WS1 stage-1 (M-1)** — `\guarded_by(L)` + `\stable_check`, `\held`/`\stable`
uninterpreted predicates, `race_session/audit/priv` + `stable_check` red controls
(red without the obligation, green with). Build green, `tests/run.sh` 46/46.
- ⚠️ **Bound (documented in `docs/usage.md`):** stage-1 establishes *lock-held-at-access*
only, **not** check-then-act atomicity. A green `\guarded_by` suite is **not** "races
handled"; the race-family crosswalk cell stays `TRUSTED`, never `PROVED`, until stage-2.
- [x] **M-8** ATT&CK technique tags on the red controls.
- [x] **M-9 / Issue 4** `\fuel` adopted as the canonical step-budget spine; `\cost` / `\resource`
as projections, `\noninterference(\cost)` the timing variant (`docs/`).

### Follow-ups (each via its own PR)
- [ ] **WS1 stage-2 (M-2)** — the rely-guarantee / concurrent-separation prover lane for genuine
2-thread atomicity proofs (isolated like the `leg1` switch). Promotes the race cell to `PROVED`.
Triggers a mandatory `sl-auditor` re-audit (new evidence base).
- [ ] **WS3 (M-3)** — principal-identity binding: `authorized(current_principal, OP)` as the
`\precond` (bind a capability to an identity, not a boolean) + `forged_principal` red control.
- [ ] **WS4 (M-4)** — tamper-evident log: hash-chain `\postcond` with one axiomatic uninterpreted
`H` + `splice_log` red control.
- [ ] **WS5 (M-5)** — cost-channel / stateful noninterference + `\declassify` (grows the `axiom-wp`
hardened set — admit-free `*_hardened.v` + Lean twin per new cost lemma; Issue 6).
- [ ] **WS6 (M-6)** — implement the `\fuel` / `\cost` / `\resource` contexts (vocabulary already
fixed in M-9).
- [ ] **WS7 (M-7)** — lattice-parametric flow `\flow(L)` (folds vertical EoP + horizontal RBAC).

Designs for all of the above are in `docs/ws-mechanisms.md` (stubs, not implementations — no faked proofs).

Start with docs/ws-mechanisms.md and the corresponding section of extended-stride-coverage-impl.md to choose one follow-up, then run tests/run.sh to confirm the baseline. Done means implementing one scoped mechanism through its own branch and PR, preserving the stated red-control or proof expectations, and completing any required sl-auditor re-audit.

Written by the indexing model from the issue text.