9600dev/mmr/mmr-verification

MMR Verification Skill

MMR trades real money behind a double-arm. Safety here is not "write careful code" — it's a set of gates that make the unsafe change fail loudly before it ships. This skill is the operating manual for those gates. Read it before touching trading-critical code; follow it when a gate goes red.

The governing idea: convert conventions into invariants that can't be silently skipped. A rule enforced by "remember to check X" rots; a rule enforced by a type, a property, or a gate cannot.

The division of labor (read this first)

• `tests/invariants/` is the human-owned spec. It states the safety

properties as executable checks (exit-class orders are never refused, gates fail closed, a sized order never exceeds its notional, no-PASS strategies can't arm, the proposal state machine's terminal states are immutable).

• You own the implementation; you do NOT own the spec. If your change

makes an invariant go red, the implementation is wrong — fix it. Do not weaken, delete, or loosen a property to make code pass. A pre-commit guard (scripts/invariants_guard.py) refuses any commit that stages both tests/invariants/ and trader/**, precisely so a property can't be edited in the same breath as the code it checks. Changing the spec is a deliberate, separately-reviewed human act.

• Every counterexample becomes a pinned regression. When a property (or a

field incident) surfaces a concrete failing case, add that exact case as a named regression test before landing the fix. It stays forever.

The gates, and how to run them

Run everything through `uv run` (the project is uv-managed; ty and pre-commit are dev-only and never enter the container).

1. Type-check gate — ty on the kernel

trader/trading/ is the enforced scope. The capability types (e.g. the ApprovedOrder token the gate mints and the executioner requires) make "this order went through the gate" a type invariant — a path that skips the gate cannot construct the argument, and ty says so.

uv run ty check trader/trading/            # see all diagnostics
uv run python scripts/ty_gate.py           # the gate: fails on NEW diagnostics

The gate baselines the pre-existing diagnostics (scripts/ty_baseline.json) and fails only on regressions, so new code must type-clean while the legacy set is burned down per-file. When you legitimately reduce the count by fixing a file, re-record the baseline — a human-reviewed act:

uv run python scripts/ty_gate.py --update

Do not add blanket # ty: ignore. A genuine false positive (e.g. **kwargs unpacking, ib_async stub strictness) gets a targeted # ty: ignore[rule] with a one-line reason; anything that looks like a real type error is a real type error until proven otherwise.

2. Property layer — Hypothesis

Properties live in tests/invariants/. They assert universally-quantified facts, not examples. Run them like any test, in the canonical env:

uv run python -m pytest tests/invariants/ -q

When Hypothesis prints a falsifying example, that example is the spec telling you the code is wrong. Reproduce it, add it as a pinned regression, then fix.

3. Contracts + symbolic execution — deal + CrossHair (pure kernel)

The pure kernel functions carry deal pre/postconditions — order_math.whole_shares_for_notional / _floor_shares_for_notional, the position_sizing helpers (_confidence_scale / _volatility_multiplier / compute_atr), and data/proposal_transitions.py (is_valid_transition / is_known_status). They run at runtime (a violation raises) and are the spec CrossHair checks symbolically:

uv run python scripts/crosshair_check.py

CrossHair reasons about whole input domains, not sampled examples (it already caught a denormal price*multiplier underflow that crashed instead of refusing). A counterexample is either a real bug (fix + pin the case) or a mis-stated contract (correct the @deal.pre/@deal.ensure to the true documented behavior) — never weaken a contract to hide a bug. When you add or change a contracted pure function, add its @deal contract and re-run this. It's also a manual-stage pre-commit hook (too slow per-commit): uv run pre-commit run crosshair-check --hook-stage manual. Note: deal is a RUNTIME dep — deploying contracted code needs a container image rebuild.

4. Mutation testing — mutmut ("verify the verifier")

Confirms the tests actually catch bugs, by mutating the kernel and checking the suite fails. Config lives in pyproject.toml [tool.mutmut] (scope = the pure kernel). Run and score:

scripts/run_mutation.sh                     # run the pass (all 4 kernel modules)
uv run python scripts/mutation_score.py     # per-module killed/survived table

Always via `scripts/run_mutation.sh`, never a bare `mutmut run` — mutmut 3.x silently skips every @deal-decorated function (which is the entire contracted safety kernel: whole_shares_for_notional, the position_sizing helpers, the proposal transitions) and reports a false 100%. The runner patches mutmut to mutate their bodies (never the contract lambdas). A naive run gives a reassuring score that tested nothing that matters.

A surviving mutant = a code change no test noticed = a real test gap (add a test that kills it) OR a documented equivalent mutant (state the reason explicitly — an unreachable boundary, a semantically-identical rewrite). Do not edit production code to raise the score — that games the metric; only ADD tests. Run this after changing a kernel function or its tests.

5. Strategy gauntlet — "no hash, no live"

No strategy deploys or arms without a PASS recorded for the exact source hash. Before deploying/enabling a strategy (especially auto_execute):

mmr strategies gauntlet strategies/<file>.py --class <Class>

Stages: S1 import allowlist (AST — denies socket/subprocess/os/ib_async/ importlib/eval/exec/… and dynamic-import call forms; S1 is a static advisory scan, not a sandbox), S2 lookahead (assert_no_lookahead), S3 nasty-market battery (gaps/halts/NaN/zero-volume — must not crash, must emit well-formed signals), S4 PSR (record-only unless --min-psr), S5 DSR (record-only unless --min-dsr). Record-only stages never change the verdict, but when PSR/DSR fall below their bar (the gate, else 0.95 advisory) the result carries edge_credible: false + warnings, and deploy/enable/mmr strategies repeat it: a PASS is "safe to run", not "has an edge". deploy/enable refuse without a PASS for the current (hash, class); there is no override flag — edit the file, re-run the gauntlet.

6. Full suite

uv run python -m pytest tests/ --timeout=60 -q --ignore=tests/test_ibrx_async.py

The workflow, end to end

1. Before editing trading-critical code, know which invariant governs it.

If none does and the change is safety-relevant, the property is missing — flag it (a human adds it to tests/invariants/).

1. Make the change in the implementation only.
2. Run the gates: ty_gate.py, the invariants suite, the full suite. A

red property means your code is wrong, not the property.

1. Any counterexample → pinned regression test first, then fix.
2. Commit — the pre-commit hooks (uv run pre-commit run --all-files to

check ahead of time) enforce the ty gate and the spec-protection guard. If the guard fires, split your spec and implementation changes into separate commits.

1. Deploying trading code (not dev tooling) follows the operational

checklist in docs/OPERATIONAL_STATE.md: outside market hours, snapshot DBs, sync/rebuild, restart, mmr verify, gauntlet the roster in-container.

What NOT to do

• Do not weaken a property, widen an allowlist, or raise a limit to make a

test pass. That inverts the entire safety model.

• Do not gate-bypass in trading code (skip_risk_gate is already deprecated

and ignored server-side; exit-class classification, not a flag, decides what the gate exempts).

• Do not add a runtime dependency casually — it forces a container image

rebuild and widens the trusted surface. Dev tooling (ty, pre-commit) stays dev-only.

• Do not silence ty broadly. Targeted, reasoned # ty: ignore[rule] only.

See also: docs/SAFETY_ROADMAP.md (what shipped and what's next), CLAUDE.md (architecture + the exit-class boundary), and the mmr-skill skill (operating the platform).