diff --git a/CLAUDE.md b/CLAUDE.md
index 9bd85abb307..a1fa03ce2e5 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -6,6 +6,8 @@ Read these docs before working:
 - `MODELING.md` — DSL modeling philosophy. **Especially M9: DFS the concept DAG.**
   Before defining any new type, DFS from `dsl/std/` to find the existing concept
   it should attach to. See the concept DAG layers in MODELING.md.
+- `CODING.md` — Rust implementation style (Google C++-style, pure functions, data + free functions).
+- `TESTING.md` — test discipline (hermetic, behavior-driven, unit-first; mocks over full-pipeline compile).
 - `src/v2/DESIGN.md` — compiler design principles.
 
 ## Key Commands
diff --git a/CODING.md b/CODING.md
new file mode 100644
index 00000000000..b3767e675d9
--- /dev/null
+++ b/CODING.md
@@ -0,0 +1,339 @@
+# Coding — gunbc
+
+**Philosophy.** Google C++-style functional/imperative. Data +
+pure functions, not objects with hidden state. Every function
+reads as `input → output`. Interfaces are precise contracts a
+reader can understand without reading the body.
+
+This document covers **Rust implementation style** in
+`src/v3/compiler/src/`. For the concepts the compiler **models**,
+see `MODELING.md`. For the invariants the compiler **proves**,
+see `INVARIANTS.md`. For the shape of tests, see `TESTING.md`.
+
+## Adoption
+
+This document describes the live discipline for **new code and
+refactors**. The existing compiler does not satisfy every
+prescription — notable divergences today include some files >500
+lines (`emit.rs`, `dag.rs`, `algebra.dag`), some `impl` blocks
+over 20 methods on `Dag`, and some pipeline functions whose
+bodies exceed ~50 lines.
+
+**Enforcement stance:** reviewers should flag a NEW PR that
+violates these guidelines as a `KEEP_ITERATING` signal. An
+EXISTING file that violates them is documented debt, not a
+present failure — it migrates on touch or via a dedicated paydown
+lane. This keeps the doc honest against the live-state invariant
+without forcing a blocking refactor backlog.
+
+## Five principles
+
+### 1. Pure functions by default
+
+Most functions in `src/v3/compiler/src/` are structurally pure:
+`(input, dag: &Dag, ...) -> Output`. No global mutation. No
+hidden state. Given the same inputs, return the same output.
+
+"Pure" in Rust-with-&mut terms:
+
+- `fn f(&self, x) -> Y` — pure reader over `self`, no mutation.
+- `fn f(&mut self, x) -> Y` — acceptable when `self` is an
+  accumulator whose final state is the caller's intended
+  output. The function is still logically
+  `(old_self, x) → new_self` — Rust's borrow checker is the
+  optimizer. Concrete example in the compiler today:
+  `lower::lower_into(dag: &mut Dag, module: &SurfaceModule)`
+  and its siblings in `lower.rs` consume a surface-AST and
+  push nodes onto the threaded `Dag`. The caller owns the
+  Dag; `lower_into` is a pure-by-borrow mutation of it.
+- `fn f(x) -> Y` (free function) — preferred when the body
+  doesn't reference `self`. Don't hang a function off a type
+  unless the function genuinely needs that type's invariants.
+
+**Impurity is an escape hatch, not a default.** If a function
+reads a global, mutates shared state, prints to stderr, or
+reaches the filesystem, it should be named in a way that makes
+that obvious (`write_*`, `emit_to_*`, `log_*`), and it should
+live at the edges of the system — the bootstrap, `main`,
+CLI wrappers, the regen binaries.
+
+### 2. Data + free functions, not objects
+
+Most compiler state is **data structures** (`Dag`, `Declaration`,
+`Node`, `OperationEffect`, `SymbolicCost`, …) that are operated
+on by **free functions** (`compile_to_dag`, `analyze_workflow`,
+`cost_of`, `emit_rust_module`, …). Types don't own the behavior;
+behavior operates on the types.
+
+This is the shape the lenses enforce: a lens IS a pure function
+`fn analyze(dag: &Dag) -> Report`. It doesn't live as a method
+on `Dag`. The lens is external; `Dag` stays a data structure.
+`feedback_lenses_not_passes` names the same principle:
+*"analyses are lenses over physics; zero heuristics."*
+
+**Avoid:** deep method chains on a god object, trait hierarchies
+that encode domain concepts, builder patterns with fluent
+interfaces.
+
+**Prefer:** a small number of data types with many free
+functions that consume them. Grouping by **concept** (the
+shape of the data) rather than by **actor** (a class that
+"does" things).
+
+### 3. Clear interfaces
+
+A function's signature should tell the reader what it does
+without reading the body:
+
+- Names describe the mapping, not the mechanism
+  (`cost_of`, not `compute_cost_via_walk`).
+- Input types describe exactly what's needed, nothing more
+  (`fn f(dag: &Dag, port: PortId)`, not
+  `fn f(ctx: &FullCtx)` when only `dag` and `port` matter).
+- Output types are structured (`CostLookup`, not `Option<i64>`;
+  `CompositionVerdict`, not a `bool` with a sibling error).
+- Error paths are in the type, not in comments or undocumented
+  panics (`Result<T, StructuredError>`, `Option<T>` when
+  absence is meaningful, typed diagnostic enums).
+
+**Anti-signal:** a function taking `&mut Everything` and
+returning `()` is usually hiding what it does. Split it.
+
+### 4. Explicit dependencies
+
+A function's inputs include every piece of state it reads. No
+globals, no thread-locals, no "pick up config from an
+environment variable." If a function needs a `Dag`, the caller
+passes a `&Dag`. If it needs a target language, the caller
+passes a `TargetLanguageId`. The signature IS the dependency
+list.
+
+This makes the code testable by construction. The unit test
+constructs a minimal instance of each input, calls the
+function, asserts on the output. No setup hooks, no fixture
+frameworks.
+
+Acceptable exceptions (impure, documented):
+- **Bootstrap**: `Dag::new()` loads std files at initialization
+  time; the list of files is static. Localized to one place.
+- **Build scripts**: `build.rs` has legitimate filesystem and
+  stdout side effects by definition.
+- **Regen binaries**: `src/bin/regen_*.rs` write files to disk;
+  that's their job.
+- **Test harness**: `cached_compile_to_dag` holds a module-level
+  `OnceLock` map for per-test-binary amortization. Documented
+  as a performance cache, not an expressive dependency.
+
+### 5. Small and composable
+
+Functions do one thing. If a function does two things, it's
+two functions. Composition happens at the call site; the
+callee doesn't know who called it.
+
+- Function bodies over ~50 lines are a smell. Either the
+  function is doing too much, or its input/output types are
+  under-specified and the body is compensating with ad-hoc
+  unpacking.
+- Module files over ~500 lines are a smell for the same
+  reason — they typically bundle multiple distinct behaviors
+  that would read better as separate modules.
+- `impl` blocks over ~20 methods on a single type are a smell:
+  the type is accreting responsibilities that don't all
+  belong to its invariants.
+
+## What "pure" means in gunbc Rust
+
+| Rust shape | Purity status |
+|---|---|
+| `fn f(x: T) -> U` (free function, no globals) | pure |
+| `fn f(&self, x: T) -> U` (method, reader only) | pure |
+| `fn f(&mut self, x: T) -> U` (method, accumulator) | pure-by-borrow — caller threads the accumulator |
+| `fn f(x: &mut T) -> U` (caller's data mutated) | pure-by-borrow — same shape, free-function form |
+| `fn f(x: T)` returning `()` with `println!`/`writeln!` | impure (side-effecting) — should be at the edge |
+| `fn f(x: T) -> U` reading a `static mut` | impure — avoid |
+| `fn f(x: T) -> U` reading a `LazyLock<Mutex<...>>` cache | impure — documented amortization only |
+
+**A good rule of thumb:** if you can replace `&mut T` with
+`(T) -> T` and the code still reads naturally, the function
+was always pure. The `&mut` is a Rust-imposed borrow-checker
+shape, not a semantics change.
+
+## Interface design conventions
+
+**Return structured carriers, not primitives.** `cost_of(port)
+-> CostLookup` (where `CostLookup = FoundCost(i64) |
+MissingCost`) is better than `cost_of(port) -> i64` with 0
+meaning "missing." The typed carrier forces the caller to
+distinguish. See `feedback_fail_closed_discipline` (C-8).
+
+**Fail-closed at boundaries.** A function that can't produce
+its declared output returns a diagnostic or `None` — never a
+silent default. `feedback_fail_closed_is_boundary`.
+
+**Typed handles over raw ids.** A function taking `ParamRef` is
+better than a function taking `(NodeId, usize)` with a comment
+"slot must be < member.params.len()". The typed handle carries
+the witness. `feedback_state_space_vs_behavioral_invariants`.
+
+**Accessors named for what they return, not how they compute.**
+`port_of(bool_ref) -> PortId` is better than
+`extract_port_from_witnessed_ref(bool_ref) -> PortId`. The
+body is the implementation; the name is the contract.
+
+**Names are namespaces, not aliases.** See
+`feedback_naming_is_aliasing` — a `TypeAlias` declaration is a
+namespace into the substrate, not a new type. Treat Rust
+wrappers (newtypes) the same way: they carry the witness, they
+don't duplicate the underlying structure.
+
+## Anti-patterns
+
+### Builder patterns with mutable fluent interfaces
+
+```rust
+// ❌ fluent mutable builder
+let result = Builder::new()
+    .with_flag(true)
+    .with_option(x)
+    .with_context(ctx)
+    .build()?;
+```
+
+Most "builders" are struct literals in disguise. Prefer:
+
+```rust
+// ✅ data constructor
+let config = EmitConfig {
+    flag: true,
+    option: x,
+    context: ctx,
+};
+let result = emit(&config)?;
+```
+
+The struct-literal form makes dependencies explicit, omits no
+fields by accident, and doesn't hide invariants in method
+ordering.
+
+### Trait hierarchies for domain concepts
+
+```rust
+// ❌ trait for a domain concept
+trait CostLens {
+    fn analyze(&self, dag: &Dag) -> CostReport;
+    fn bound_for(&self, port: PortId) -> Option<CostBound>;
+    // ...10 more methods
+}
+impl CostLens for LinearCostLens { ... }
+impl CostLens for PolynomialCostLens { ... }
+```
+
+Traits are for **interfaces the language needs** (`Clone`,
+`PartialEq`, `Iterator`), not for domain concepts. Domain
+concepts are **data + free functions**: `SymbolicCost` is a
+data type; `cost_of`, `dominates`, `sequential` are free
+functions over it. Polymorphism is pattern-matching on variants,
+not dynamic dispatch.
+
+### Hidden state as expressive dependency
+
+```rust
+// ❌ function with hidden expressive dependency
+static LOADED_SPEC: LazyLock<Mutex<Option<TargetSpec>>> = ...;
+fn emit_rust(dag: &Dag) -> Result<String, EmitError> {
+    let spec = LOADED_SPEC.lock().unwrap().clone().expect("spec loaded");
+    // ...
+}
+```
+
+The spec is a **dependency**. Pass it in:
+
+```rust
+// ✅ explicit dependency
+fn emit_rust(dag: &Dag, spec: &TargetSpec) -> Result<String, EmitError> {
+    // ...
+}
+```
+
+**Distinct from:** hidden state for **performance amortization
+with documented dissolution**. A `LazyLock<Mutex<...>>` cache
+that memoizes pure-function results (e.g. test
+`cached_compile_to_dag`) is acceptable — the cache is not
+expressive (the output is identical with or without it), the
+cost saved is real, and the cache's lifetime and invalidation
+story are named in code comments. See the table below; keep
+such caches at the edges (test harness, bootstrap-once caches
+inside `Dag`), never in lens / emitter / inference bodies.
+
+### God functions / god modules
+
+```rust
+// ❌ one function does five things
+fn emit_rust_module(dag: &Dag) -> Result<String, EmitError> {
+    // 300 lines: build indexes, walk declarations, render types,
+    // render functions, render values, invoke rustfmt, apply
+    // correction style, emit diagnostics
+}
+```
+
+Each of those is a distinct behavior. Compose them at the call
+site:
+
+```rust
+// ✅ small composable pieces
+let indexes = RealizationIndexes::build(dag)?;
+let declarations = render_declarations(dag, &indexes)?;
+let functions = render_functions(dag, &indexes)?;
+let formatted = format_rust(&declarations, &functions)?;
+emit_rust_module(dag, &indexes, &declarations, &functions)
+```
+
+The top-level function is a pipeline stitch; each stage has
+clear input → output.
+
+### Hidden panic surface
+
+```rust
+// ❌ unwrap inside library code
+fn find_cost(dag: &Dag, port: PortId) -> i64 {
+    dag.nodes().iter()
+        .find(|n| n.id() == port.node_id())
+        .unwrap()  // panics on unknown port
+        .cost
+        .unwrap()  // panics on missing cost
+}
+```
+
+Panics are contract violations, not error paths. Library code
+returns `Result` or `Option`. Only `main` and test code
+`unwrap()`.
+
+## When impurity is acceptable
+
+The compiler's edges necessarily interact with the outside
+world. Impurity is fine in these specific **roles**, and should
+be clearly labeled (rustdoc on the module or function):
+
+| Role | Kind of impurity | Why acceptable |
+|---|---|---|
+| **Build script** (`compiler/build.rs`) | filesystem, codegen | build-time concern by definition |
+| **Code-generation binaries** (`compiler/src/bin/regen_*.rs`) | filesystem writes | their job is to materialize generated files |
+| **Bootstrap** (single-call-site inside `Dag::new()`) | loads std files at init | std files are frozen at build; amortized once per process |
+| **Test amortization caches** (module-local `LazyLock<Mutex<…>>` memoizing pure-function results inside `tests/`) | per-test-binary memoization | cache's existence does not change observable output; documented scope + dissolution |
+
+Everywhere else — library code, lenses, substrate walks,
+emitters, inference, lowering — should be pure in the Rust
+sense described above.
+
+If you want to add a new impurity surface, identify its role
+first. If the role isn't in the table, the function probably
+belongs inside a library-pure API and the impure part should
+be split out to an edge.
+
+## Related
+
+- `MODELING.md` — what to model in `std/`
+- `INVARIANTS.md` — invariants the compiler enforces
+- `TESTING.md` — test discipline (this document is the
+  production-code twin)
+- `THESIS.md` — what the compiler is for
diff --git a/TESTING.md b/TESTING.md
new file mode 100644
index 00000000000..fd4d377985a
--- /dev/null
+++ b/TESTING.md
@@ -0,0 +1,341 @@
+# Testing — gunbc
+
+**Philosophy.** Google C++-style: hermetic, behavior-driven, unit-first.
+Each test names an **interface** and a **behavior** that interface
+promises. Heavy integration tests are an exception, not the rule.
+Dependency injection + minimal-constructed inputs are the default;
+full-pipeline `compile_to_dag(...)` is reserved for tests whose
+subject genuinely is the pipeline.
+
+## Adoption
+
+This document describes the live discipline for **new code and
+refactors**. The existing test suite does not satisfy every
+prescription — known divergences (large integration-test share,
+imperative substrate walks, exhaustive testgen validation) are
+documented in the *Migration audit* section below, with refactor
+priorities tracked against ROADMAP.
+
+**Enforcement stance:** reviewers should flag a NEW PR that
+violates these guidelines as a `KEEP_ITERATING` signal. An
+EXISTING file that violates them is documented debt, not a
+present failure — it migrates on touch or via a dedicated paydown
+lane. This keeps the doc honest against the live-state invariant
+without forcing a blocking refactor backlog.
+
+## Five principles
+
+### 1. Hermetic
+
+Each test declares its own inputs and assertions. No cross-test
+mutable state. No fixture that "sets things up" across many
+tests — if two tests need the same input, they each declare it.
+The runtime (e.g. `cached_compile_to_dag`, `.dag`-native test
+runner under DB-15 R2) amortizes identical inputs behind the
+scenes; the **logical** hermeticity stays at the test level.
+
+### 2. Behavior-driven, not implementation-driven
+
+A test names the **interface** and the **behavior**:
+
+- Interface: `cost_of(dag, port) -> CostLookup`
+- Behavior: *"returns `FoundCost(n)` where n grows linearly with
+  input list size"*
+
+Not: *"the resulting HashMap has 3 keys in alphabetical order."*
+Implementation details of how a cost is computed are not the
+contract; the contract is what the caller can rely on. Tests
+that break on internal refactors pin the wrong surface.
+
+### 3. Cost of change
+
+A good test survives any refactor that preserves semantics. If
+`Dag`'s internal storage changes from `Vec<Declaration>` to
+`BTreeMap<DeclarationId, Declaration>`, tests that asked
+"is there a declaration named X?" still pass. Tests that asked
+"is index 7 of the declarations vec equal to X?" break — and
+shouldn't have existed. Pin behavior, not layout.
+
+### 4. One claim per test
+
+Each `#[test]` (or `data foo: TestClaim`) makes **one**
+structural claim. Multi-claim tests bundle unrelated behaviors
+and obscure which contract broke when CI goes red. The test
+name should read like a sentence — subject, verb, object, under
+what condition:
+
+```rust
+#[test]
+fn cost_of_empty_fold_returns_constant_zero() { ... }
+
+#[test]
+fn cost_of_linear_fold_scales_with_source_port_size() { ... }
+```
+
+Not:
+
+```rust
+#[test]
+fn cost_lens_works() {  // what behavior?
+    // 20 lines, 6 assertions, 3 unrelated claims
+}
+```
+
+### 5. Mocks over compile
+
+The default for unit tests is to **construct a minimal `Dag`**
+with the structural shape under test, not to compile a source
+string. Compiling `"let x = 1 + 2"` and then asserting
+"there's a Transform node for `+`" exercises the entire
+pipeline (parse + lower + infer) as a side effect of testing
+one structural invariant. If that test fails, the root cause
+could be anywhere in ~30k lines of compiler code.
+
+Instead, construct the exact shape under test and run the lens
+against it.
+
+**Availability today — honest read of the current tree.** The
+public surface of `Dag` is narrow: `Dag::new()`,
+`declaration_by_name`, typed handle accessors, primitive shape
+lookups. Crate-private there's one builder helper
+(`Dag::alloc_port`); a full minimal-construction API
+(`push_value`, `push_transform`, `push_bind`, etc.) **does
+not yet exist**. This means the guidance above is today more
+aspiration than available workflow.
+
+**Tracked follow-up:** land a public (or at minimum
+`pub(crate)`-with-test-harness-access) builder surface on
+`Dag` covering the behaviors lenses analyze. The absence of
+that surface is the single biggest blocker to the
+`~75% unit` target ratio.
+
+**Practical guidance for now:**
+
+- For crate-internal unit tests (`#[cfg(test)] mod tests`
+  inside `src/v3/compiler/src/`): `alloc_port` and the other
+  `pub(crate)` APIs are in scope. Write tests that need only
+  those.
+- For integration tests in `tests/`: `compile_to_dag(small_fixture)`
+  is the practical entry point today. Keep the fixture
+  minimal (single `let`, single `fn`) and assert on the lens
+  output, not pipeline intermediates.
+- When you find yourself wanting a `push_*` helper that
+  doesn't exist, proposing it is the right move — see the
+  follow-up above.
+
+Full-pipeline `compile_to_dag` is the **intended** entry point
+for:
+- **Integration tests** — deliberate end-to-end coverage of the
+  pipeline itself
+- **Thesis tests** — claims about user-facing behavior, where
+  the source text is part of the interface
+- **Boundary tests** — target-language roundtrips (rustc, go, python)
+
+**Scope clarifier:** the "mocks over compile" anti-pattern applies
+to lens / accessor / single-pass tests where the subject under
+test is narrower than the whole pipeline. For the three
+categories above, `compile_to_dag` **is** the correct entry point
+— the pipeline is the unit. Don't force minimal-`Dag` construction
+where the test legitimately targets end-to-end behavior.
+
+## Test layers (target ratios)
+
+| Layer | Share of tests | What belongs here | Typical time per test |
+|---|---|---|---|
+| **Unit** | ~75% | lenses, single-pass behaviors, accessors, typed handles, substrate walks against hand-built `Dag` | <5ms |
+| **Integration** | ~15% | multi-stage pipeline behaviors, fixed-point convergence, cross-stage invariants | <100ms |
+| **Boundary** | ~10% | rustc/go/python roundtrips, emitted-module behavior | <2s |
+| Thesis | across the above | claims in the thesis vocabulary (cost bounds, parallelism, structural invariants). Write as whichever layer is natural — usually unit or integration | — |
+
+**Red-flag ratios** — if your suite is >30% integration or any
+test takes >2s locally (cold bootstrap aside), the suite is
+drifting into heavy-integration territory. See
+`feedback_test_timeout_2s`.
+
+## Mocks and dependency injection
+
+Prefer passing `&Dag` / `&dyn Lens` / etc. over globals. Prefer
+constructing the minimal Dag shape over compiling source.
+Prefer typed-carrier assertions over name-keyed lookups (a test
+that does `dag.declaration_by_name("Foo")` is pinning the name,
+not the structure — use typed `DeclarationId` handles once
+resolved).
+
+**Constructing a minimal Dag — eventual shape.** Builder
+helpers on `Dag` that produce specific shapes (value literals,
+transforms, binds, port allocations) are the intended mocking
+surface. Today only `alloc_port` exists as a `pub(crate)`
+helper; the rest are the tracked follow-up named earlier in
+this document. When proposing a new helper, match the natural
+per-variant granularity of `Behavior` / `TypeConnective`.
+
+**When compile IS the unit** — parser / lowering / inference
+tests legitimately test the compile pipeline. Those tests use
+`compile_to_dag(source, file)` because the **pipeline itself**
+is the interface they're testing. That's fine. Most lens and
+accessor tests are not in this category.
+
+## `.dag`-native testing (DB-15 R2 trajectory)
+
+The long-term shape: tests are **declarations** in `.dag`, not
+Rust imperative harnesses. Each test is a
+`data test_foo: TestClaim = { name, source, predicate }`
+declaration. The test runner reads the declaration graph,
+amortizes identical `source` compiles via the dependency walk
+(not via `OnceLock`-cached Rust state), and evaluates each
+predicate structurally.
+
+At that point the hermetic principle still holds — each
+`TestClaim` declaration is its own unit, the runtime just
+shares the compile work when sources match. Rust integration
+tests collapse to two residual categories:
+
+- **Compiler-internal unit tests** inside `src/v3/compiler/src/`
+  (`#[cfg(test)] mod tests`) for Rust-only helpers
+- **Boundary tests** that must invoke external processes
+  (rustc, go, python)
+
+Everything else ports to `.dag`.
+
+Until DB-15 R2's runtime lands, write Rust integration tests
+that match the guidelines above so the eventual port is a
+rewrite of shape, not of intent.
+
+**Post-R2 shape:** once DB-15 R2 ships, most of this document
+collapses into "see `dsl/std/verification.dag` for the test
+surface." The Rust-side residual is: compiler-internal unit
+tests (`#[cfg(test)] mod tests`) inside `src/v3/compiler/src/`,
+and boundary tests that invoke external toolchains. Everything
+else ports to `.dag`.
+
+## Anti-patterns
+
+### Don't compile a full source to test a single lens
+
+```rust
+// ❌ anti-pattern
+#[test]
+fn cost_lens_handles_fold() {
+    let dag = compile_to_dag(
+        "let total: Int = fold(singleton(1), 0, |acc, x| acc + x)",
+        "fold.v3"
+    ).expect("compiles");
+    let total = find_bind_by_name(&dag, "total");
+    assert_eq!(cost_of(&dag, &total.value), CostLookup::FoundCost(3));
+}
+```
+
+What's wrong: the test exercises parse, lowering, inference,
+and cost — a failure anywhere reports "the cost lens broke."
+And the `"let total: Int = fold(...)"` fixture is now a
+coupled input for both the parser and the cost lens.
+
+```rust
+// ✅ unit: construct the shape the cost lens analyzes
+#[test]
+fn cost_of_fold_over_linear_source_returns_linear() {
+    let mut dag = Dag::new();
+    let source = dag.alloc_port_with_linear_shape(/* size_var */);
+    let fold = dag.push_fold_transform(source, /* init, body */);
+    assert!(matches!(
+        cost_of(&dag, &fold.output()),
+        CostLookup::FoundCost(SymbolicCost::LinearCost(_)),
+    ));
+}
+```
+
+### Don't assert on implementation details
+
+```rust
+// ❌ pinning layout
+assert_eq!(dag.declarations().len(), 247);
+assert_eq!(dag.declarations()[3].name, Some("OrderedRing".into()));
+
+// ❌ pinning error message text
+assert!(diagnostic.detail().contains("missing field"));
+
+// ❌ pinning HashMap iteration order
+let keys: Vec<_> = report.unused.keys().collect();
+assert_eq!(keys, vec!["foo", "bar"]);
+```
+
+```rust
+// ✅ pinning structure
+assert!(dag.declaration_by_name("OrderedRing").is_some());
+assert!(matches!(diagnostic, Diagnostic::FieldNotFound { .. }));
+assert!(report.unused.contains_key("foo"));
+assert!(report.unused.contains_key("bar"));
+```
+
+### Don't use cross-test shared state
+
+Shared setup via `OnceLock` or `lazy_static` is a runtime
+amortization (see `cached_compile_to_dag`) — it speeds up
+compiles that happen to repeat across tests, but each test's
+**logical** inputs stay per-test. A test that reads from a
+shared `Arc<Mutex<Report>>` populated by earlier tests is not
+hermetic and will fail under `--test-threads=1` or random
+ordering.
+
+### Don't write tests that span multiple behaviors
+
+If a test needs three distinct assertions to "tell the whole
+story," split into three tests. Each failure then points at
+exactly one broken contract.
+
+### Don't test private state through public surfaces
+
+Tests should exercise public interfaces. If you need to inspect
+a private field, the interface is under-specified — either
+expose the fact structurally (a new typed accessor, a lens
+output field) or accept that the private state isn't part of
+the contract and shouldn't be tested.
+
+## Naming convention
+
+`<subject>_<verb>_<object>_<condition>`:
+
+- `cost_of_empty_fold_returns_constant_zero`
+- `field_access_on_non_conj_type_is_rejected_with_diagnostic`
+- `branch_arm_of_returns_none_for_non_bool_port`
+- `workflow_effect_linear_chain_composes_idempotent_when_all_ops_idempotent`
+
+Tests named `test_X`, `foo_works`, `basic_thing`, or
+`regression_N` are under-specified — the reader can't tell what
+the test proves without reading the body. The name IS the
+contract claim.
+
+## Migration audit (current state)
+
+The v3 integration suite has ~357 tests across 29 files. Most
+predate these guidelines. Rough current breakdown:
+
+| Category | Files | Tests | Status |
+|---|---|---|---|
+| Thesis / behavior | 2 | 28 | well-shaped; port to `.dag` under DB-15 R2 |
+| Substrate walks | 4 | 100 | imperative Rust assertions of structural shapes; candidates for lens-based consolidation |
+| Lens outputs | 6 | 60 | natural fit for `.dag`-native declarations |
+| Class-5 boundary | 6 | 19 | keep in Rust until runtime is `.dag`-native |
+| Target emission | 4 | 54 | keep; boundary tests |
+| Milestone / feature | 4 | 80 | mixed; `m0_acceptance` likely subsumed by later milestones |
+| Testgen / meta | 1 | 3 | over-expensive; reshape or `#[ignore]`-by-default |
+| Smoke / low-value | 4 | 32 | consolidate or delete (`real_stdlib_parse_smoke` is weakest) |
+
+Refactor targets, in order of ROI:
+1. **Audit `m0_acceptance.rs`** — 41 tests from M0 skeleton; cross-check coverage against later milestones and delete overlaps.
+2. **Collapse `m1_substrate_test.rs`** — 91 imperative substrate-walk assertions into ~20 lens-based structural claims.
+3. **Reshape `m1_5_testgen_test.rs`** — spot-check instead of exhaustive compile-every-claim.
+4. **Port thesis + lens tests to `.dag`** once DB-15 R2 runtime lands.
+
+See `docs/design-test-infra.md` and ROADMAP §Lane 2 Stage 2c for
+the DB-15 trajectory. This document is the near-term discipline
+for Rust-side tests while that runtime matures.
+
+## Related
+
+- `INVARIANTS.md` — project-level invariants; some have direct
+  test implications (fail-closed, illegal-states-unrepresentable)
+- `MODELING.md` — what to model in `std/`; tests should exercise
+  the modeled concepts, not rebuild them
+- `docs/design-test-infra.md` (DB-15) — the `.dag`-native test
+  infrastructure this document is the stopgap for