# proposal/14-toolchain.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/596445afea8642bb9f8858aaae0e14a0d2d30061/proposal/14-toolchain.md)

Repository: [versecafe/strata](https://git.cafe/versecafe/strata)

Visibility: public

Requested revision: 596445afea8642bb9f8858aaae0e14a0d2d30061

Requested commit: 596445afea8642bb9f8858aaae0e14a0d2d30061

Commit: 596445afea8642bb9f8858aaae0e14a0d2d30061

Blob: ef8d808d6bddf8d03f68b5517f0abe455aa36d39

Size: 27600 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/596445afea8642bb9f8858aaae0e14a0d2d30061/proposal/14-toolchain.md?format=markdown)

````
# Toolchain: strata fmt, strata lint, strata-ls

The canonical formatter, the ledger-lint tier, and the language server. The section's actual thesis: **three tools, one tree, one ledger, one diagnostic vocabulary** — fmt owns the tree's fidelity, lint queries the ledger, and the language server renders both without ever growing its own approximation of anything. Principles in force: P-6 (determinism extends to tooling), P-9 (diagnostics are the product), P-7 (estimates never bear load), P-11 (agents and humans query one substrate). Charter answers from Veronica (2026-07-17) are marked SETTLED in the [register](decisions.md).

## strata fmt

### 1. Zero-config, day one (D-049)

No config file; no flags that affect output (only `--check`/`--diff`). Line width is **100 columns**, baked (SETTLED — 80 forces ugly wraps on typed port declarations, 120 hurts side-by-side diff review, our dominant reading mode). The style versions with the **edition** (D-043), so style evolution is opt-in per component, never ambient — this replaces both rustfmt's option drift and Black's stable/preview churn. `fmt`-clean is a **hard `forge publish` gate and never a build gate** (SETTLED): strict at the library boundary, permissive during exploration — the Verilog landscape's lesson is that formatters without an ecosystem gate never take (Verible), and Strata negates the three structural reasons SV formatters failed: no preprocessor (D-048), a language born with its formatter, and a publish step to hang the gate on.

### 2. In-band steering (D-050, SETTLED)

The stance that survived large ecosystems is zero options _plus_ steering read from the source itself (zig fmt lineage; Prettier froze its options and calls them a historical mistake; rustfmt's knobs produced per-project drift):

- trailing comma → one-per-line; no trailing comma → single line if it fits;
- blank lines are user-controlled grouping, preserved (collapsed to a max of one);
- **the anti-Black rule: `strata fmt` never inserts a steering token.** Black's one deep regret (the magic trailing comma) came from the formatter writing trailing commas it then re-read as user directives — a one-way ratchet. We read steering; we never write it.

### 3. Layout doctrine: no vertical alignment (D-051)

`stream {}` / `contract {}` / port lists / match arms format one entry per line, single space around `:`/`=`, grouping via blank lines. Vertical alignment is the single largest source of diff churn and idempotence bugs in the gofmt/Verible record (one long field re-aligns its neighbors; Verible ships four alignment policies for one construct — option creep in miniature). Editors may render elastic alignment locally.

### 4. Formatted text is presentation; identity is structural (D-052)

Nothing in the compiler keys on formatted bytes — the Unison/Dhall move (hash normalized structure, not text), made mandatory by the documented history of formatter idempotence bugs (gofmt and zig fmt both, root cause almost always comment attachment). A formatter bug must never be a miscompile or a spurious version bump. **The provenance-stability rule, normative:**

> For any source `s` accepted by the parser: elaboration of `fmt(s)` and `s` produce identical Architectural IR, identical ledger facts and identities, identical summaries, and identical memoization keys. Only recorded source spans may differ.

Mechanism: elaboration input is the AST, with a hard ban on comptime reflection over source text, columns, or comment contents (source layout is an undeclared input under P-6); **ledger identity is path-based** — `(canonical path, generator identity, memo key, deterministic emission index)` — with spans in a side table re-derived on every parse; summary hashes exclude trivia and spans. Corollaries: a reformat-only change is _mechanically a patch_ with a reflexive equivalence certificate — no version bump ([13 §3](13-package-system.md)); P-9 diagnostics carry both the stable node ID (for agents — a repair survives a concurrent reformat) and the current span (for humans).

### 5. Verified invariants (D-053)

CI-fuzzed from day one: idempotence (`fmt∘fmt = fmt`), AST round-trip including comment count and anchors, cross-platform determinism, parse-error input returned untouched. Comments are trivia attached to anchor nodes (leading/trailing/dangling), never floating byte offsets. No `fmt: off` directive in v1 (a documented bug magnet; gofmt lives without one).

### 6. Scope (D-054)

`strata fmt` formats the whole package surface including `forge.toml` (canonical key order, one dependency per line) — one command formats a package, and registry-rendered manifests look identical to local ones.

## strata lint

### 7. The soundness line (D-055)

> **R-LINT-1.** A lint is never load-bearing. No judgment, obligation discharge, optimization-legality decision, summary compatibility check, or resolution outcome may depend on a lint's firing, silence, or suppression. Anything whose violation makes a design _wrong_ is a judgment or an unsafe-category boundary, never a lint.

Corollaries: there is no `correctness` lint group — the group clippy had to deny-by-default is the group Strata deletes, because its contents are type judgments here; suppressing every lint changes no semantics, summary, or version, only the aggregate report; a lint discovered to be load-bearing is a bug filed against the type system, and its promotion to a judgment is a register event.

The triage of the commercial rule decks backs this up: SpyGlass/Verilator's high-value checks — unsynchronized CDC, width mismatch, latch inference, multiple drivers, undriven ports, combinational loops, reset-domain mixing, uninitialized state — **all become judgments**; a large second class (unsynthesizable constructs, `full_case`/`parallel_case` verification, X-propagation decks, sensitivity lists, blocking/nonblocking, `ifdef` hygiene, sim/synth-mismatch decks) **dies entirely** as artifacts of Verilog's weaknesses; what remains for lint is the genuinely advisory band — evidence gaps, physical estimates, missed optimizations, ecosystem hygiene. Full table in the research brief; condensed into the catalog below.

### 8. Architecture: declarative queries over the ledger (D-055)

A lint is a declarative query over ledger facts ([07 §3](07-compiler-architecture.md)) — the CodeQL model — never visitor code with assertion power: lints read facts, never write them, which makes third-party lints sandboxed by construction. Each lint declares the fact categories it reads; a pass that invalidates a category silences (never falsifies) downstream lints. The structural advantage over Infer/CodeQL-class tools: they _reconstruct_ facts and spend their false-positive budget on analysis error; Strata's lints consume already-adjudicated facts, so the residual FP surface is judgment-of-taste only — exactly what levels and suppression-with-reason are for.

### 9. Groups, posture, surfacing (D-056, D-059)

Groups are a **precision/maturity statement**: `suspicious` (near-zero FP or it gets demoted), `design`, `pedantic` (opt-in), `nursery` (incubating — every new lint starts here), `forge` (manifest/ecosystem hygiene). Severity is **consumer policy**, never hard-coded by the lint; **the default posture is warn, for every audience** (SETTLED — one lint culture for humans and agents; release gates and agent policies may tighten explicitly, and their tightening is visible policy, not baked-in tiering).

Surfacing follows the Infer deployment lesson (diff-time review ≈70% fix rate; batch ≈ zero): default presentation is on the **summary diff**; full-tree results live in the aggregate report and gates. Every firing, suppression, and repair-acceptance is an [experiment-database](09-agent-system.md) record; per-lint effective usefulness (repair-accepted ÷ fired, tracked per audience) drives Tricorder-style automatic demotion to `nursery`.

### 10. Suppression: `expect` with mandatory reason (D-057)

There is no bare `allow`. The only suppression form:

```
expect(lint = cdc_reconvergence,
       reason = "flags recombine ≥3 cycles after either edge; window proven in tb_corr",
       evidence = Tested<corr_corpus>,     // optional: reason backed by a fact
       review_by = edition(2028))          // optional expiry, edition-keyed
```

Rules: `reason` is required (Rust proved optional reasons are never written; SpyGlass waiver files prove it at deck scale); a suppression is a **ledger fact** on the node it covers, pass-maintained like any fact — a pass transforming the node must preserve/transform/invalidate it, and an invalidated suppression re-arms the lint (the "alert when nearby code changes" recommendation, made sound); RFC-2383 semantics are native — an `expect` whose lint no longer fires is itself a diagnostic (`suppression_stale`), machine-applicably removable; scope is a node or component, never a file or tree; the suppression surface rolls up transitively in the aggregate report next to the unsafe surface, registry-queryable.

### 11. Repair applicability is verified, not declared (D-058)

Repair objects carry clippy's applicability taxonomy, but machine-applicability is _checked_: a repair is MachineApplicable iff applying the typed edit leaves the component summary bit-identical or strictly refining — the same summary diff that powers mechanical semver ([13 §3](13-package-system.md)). Clippy asserts applicability and has a recurring wrong-MA bug class; Strata verifies it with machinery that exists anyway. Contract-changing repairs (MI) state their impact in the structured-claim form agents already use ([09 §2](09-agent-system.md)).

### 12. Publish gate: adjudicated, not clean (D-060, SETTLED)

`forge publish` requires zero **unaddressed** `suspicious`/`design` diagnostics — every survivor must be an `expect`-with-reason — and publishes the suppression surface (counts, reasons, ages) in the summary, mirroring unsafe-surface acknowledgment ([13 §2](13-package-system.md)). Hard lint-clean would convert every false positive into a publish blocker and breed the reason-less mass-suppression culture the FSE 2025 suppression study documents; no bar reproduces crates.io, where lint status is invisible at the registry.

### 13. Governance: three rings (D-060, SETTLED)

(1) The core team owns `suspicious`/`design`/`pedantic`; the only path in is nursery-first with telemetry-gated promotion. (2) Any package may ship **scoped lints** — sandboxed ledger queries applying to its own consumers (a protocol library legitimately knows what misuse of _its_ contracts looks like). (3) Scoped→global promotion is a decisions-register event requiring cross-package telemetry. Third parties never add to `suspicious`: that group's near-zero-FP promise is the tier's credibility.

### 14. Starter catalog (v0, all entering via `nursery`)

Keyed on ledger facts; each ships a P-9 repair object. Condensed — MA = verified machine-applicable, MI = contract-changing candidate, PH = placeholder/plan:

**suspicious:** `cdc_bridge_assumed_only` (CrossClock guarantee at `Assumed` only → MI swap registry bridge / PH attach evidence) · `cdc_reconvergence` (two crossings sharing provenance, recombined without correlation contract → MI insert `During` window obligation) · `arbiter_no_fairness_evidence` (→ PH generated fairness property) · `obligation_assumed_at_top` (Tier-2 obligation re-exported as `Assumed` to build root → MI `comptime_exhaustive` where domain qualifies) · `counterexample_unpromoted` (DB counterexample with no regression test → MA emit test) · `assumption_holder_distant` (unsafe Ψ-fact discharged outside enclosing summary) · `assumption_ownership_cycle` (progress/availability assumptions form a closed owner cycle → MI add independent escape/rank / PH environment owner) · `declared_relation_incomplete` (memory-model contract omits required completeness without exporting an obligation) · `certificate_stale` (artifact dependency manifest invalidated by design/tool/target/mode/clock/calibration/lifecycle change → PH regenerate) · `assurance_self_support` (assurance graph appears in its own evidence closure; hard rejection, no suppression) · `suppression_stale` (→ MA delete) · `suppression_expired` (→ PH renew or fix).

**design:** `likelihood_timing_secret_adjacent` (likelihood-asymmetric timing on a path a labeled-secret value could ride — the D-071 side-channel caution as a lint; fires only where security labels exist, silent otherwise → MI equalize arm timing / PH declassification review) · `fault_contract_unmutated` (declared fault class has no injected mutant/campaign coverage → PH generate campaign) · `health_detection_without_containment` (detection bound exists but occurrence→containment window does not → PH add containment claim) · `progress_bound_from_weak_fairness` (finite `N` rests only on weak fairness → MI weaken to eventual / PH add quantitative premise) · `observer_contract_unexercised` (declared observer has no relational property or measurement plan) · `estimated_fanout_exceeds` (→ MI duplicate driver licensed by purity fact) · `comb_depth_vs_clock` (→ MI pipeline behind `TransactionEquivalent`) · `buffer_capacity_unjustified` (no `Occupancy` refinement → MI add named refinement / PH sizing experiment) · `equivalence_overpinned` (pinned `CycleExact`, consumers observe only `TransactionEquivalent` → MA relax, provably unobservable) · `replicate_shareable` (discharged exclusivity + low utilization → MI shared-serial variant) · `dead_architecture` (→ MA remove / MA expect for intentional taps) · `reset_removable` (no-read-before-first-write proven → MI reset-less register) · `config_coverage_edge_gap` (→ MA extend coverage corners) · `chosen_param_unevidenced` (D-035 choice without `Measured` backing → PH sweep experiment).

**pedantic:** `latency_bound_slack` (→ MA tighten to derived bound; refining ⇒ minor) · `evidence_below_gate` (→ PH verification-plan entry) · `multicycle_unexploited` (stability fact, no timing candidate → MI emit intended candidate plus mandatory post-synthesis binding plan, never an admitted exception) · `assurance_residue_unowned` (residue has no named disposition owner) · `budget_headroom_low` (→ MA raise declarative budget / MI restructure dominant generator).

**nursery:** `stage_never_occupied` (zero occupancy across all `Tested` corpora) · `vendor_assumption_upgradable` (registry indexes a refining proof artifact → MA import it).

**forge:** `dependency_evidence_downgrade` (lockfile update lowers depended-on evidence → MA pin) · `suppression_surface_growth` (transitive roll-up grew → PH review checklist by age × severity) · `fact_dropped_at_boundary` (emission's boundary ledger report shows a fact that neither baked, delegated, nor verified — [07 §2b](07-compiler-architecture.md) → MI choose an exit / MA `expect` with reason).

## strata-ls

### 15. The resident compiler; there is no second frontend (D-061, phase-1 gate SETTLED)

The field's verdict is unanimous: every ecosystem studied either paid for two frontends and paid again to merge them — rustc/rust-analyzer via mandated library-ification, Kotlin's K1 IDE reimplementation replaced wholesale by K2, Dart settling for shared-components, zls shipping _no semantic diagnostics at all_ while Zig waits on its compiler-as-server endgame — or built one frontend from day one and never had the problem (Roslyn). Strata designs after the verdict: **strata-ls is a long-lived daemon hosting the one compiler**; `strata build` and strata-ls are two drivers over one library. Ships as a **phase-1 gate, Tier A only** (SETTLED — the one-frontend property is cheap on day one and brutal to retrofit; the language is used through the LSP from month one).

Interactive speed comes from machinery the proposal already has, not new query infrastructure: the summary firewall is the invalidation boundary; durability tiers map onto existing structure (registry summaries > workspace summaries > open bodies); body edits re-check one body against unchanged summaries; in-flight work cancels on edit. No salsa-class fine-grained memoization — Strata's declare-before-use modules, no preprocessor (D-048), and deterministic comptime (D-021) are exactly the language properties that make coarse map-reduce sufficient (matklad's "Against Query-Based Compilers", already load-bearing in [07 §6](07-compiler-architecture.md)).

**Normative invariants:**

> **R-LS-1 (no second judgment path).** Every diagnostic, completion, hover, or inlay hint is produced by the same checkers, over the same tree and summaries, as `strata build`. The LSP layer may _select, schedule, and render_; it may never _approximate_. Editor/batch divergence on identical input+config is a P0 bug class with its own CI oracle (fuzz both drivers, diff structured diagnostics).
> **R-LS-2 (body-edit isolation).** An edit whose exported summary is unchanged invalidates nothing outside that body; Tier-A latency is independent of workspace size.
> **R-LS-3 (budgeted elaboration in-editor).** D-044 budgets apply unmodified; exhaustion is a P-9 diagnostic naming the dominant call path, never a hung server. The editor may apply _stricter_ interactive budgets, never looser (looser would accept what the build rejects, violating R-LS-1).
> **R-LS-4 (config honesty).** Every elaboration-derived artifact names its config point; bound-level facts are the only unlabeled facts.
> **R-LS-5 (stable anchors).** All diagnostics, repairs, and `strata-ls/*` responses reference nodes by path-based identity (D-052) plus current span — agent-held references survive reformats and concurrent edits.

### 16. One tree, three consumers (D-062)

The D-052/D-053 trivia-attached anchor-node AST is the single tree for parser, fmt, and LSP, with additive requirements: lossless for _all_ inputs including invalid (`text(tree) == input`); error containment via ERROR-wrapped skipped tokens and zero-width MISSING tokens, with incomplete-but-present nodes for half-typed code (the resilient-LL discipline — the shape completion needs); incremental reparse with green-subtree reuse; and **path-based identity defined over recovered trees too** — ERROR nodes get deterministic paths, because broken code is the LSP's main diet and its diagnostics need anchors. Trivia stays anchored leading/trailing/dangling (the Roslyn/Swift model fmt already requires; rust-analyzer regrets not having it). Tree-sitter is explicitly _not_ this tree (GLR recovery is unpredictable, upstream disclaims compiler-frontend use); its role is §18. The D-053 fuzz suite gains an LSP clause: every mutated/truncated input round-trips and yields diagnostics, never a parser failure.

### 17. Comptime in the editor: three tiers (D-063, D-064; active-config UI SETTLED)

The field's three strategies all have documented failure modes — zls's no-semantics gap (can't analyze without monomorphizing from `main`), clangd's heuristic dependent contexts, rust-analyzer's never-invalidate proc-macro cache hack — and each is pre-fixed by an existing Strata decision:

- **Tier A — every keystroke, no elaboration.** All decidable judgments over the edited body against D-038 definition-checked bounds and imported summaries: width algebra (D-037 — normalization not evaluation is _why_ width errors work without running comptime), phases, grades, protocol-catalog compatibility, with D-038's blame rule assigning bound-violation vs body errors. Completion, goto, hover from bound-level types. This is the tier zls structurally cannot have.
- **Tier B — active config, debounced, budget-bounded.** One pinned instantiation kept incrementally elaborated, memo-warm via D-045 (a body edit re-runs only comptime calls whose memo keys changed — the caching rust-analyzer wants and can't have, sound here by D-021 construction). Yields concrete widths/latencies as inlay hints, ledger-fact hovers, elaboration diagnostics — all tagged with their config point (R-LS-4).
- **Tier C — on demand / background.** Remaining coverage points ("check all corners" code lens), Tier-2 SMT, design lint — streamed via pull-diagnostics refresh, never blocking. OP-3's stable `obligation` outcome means "not yet known" is a first-class editor answer.

**Active config (D-064, SETTLED as a visible picker):** the "which instantiation am I looking at?" question every ecosystem answers with build-system folklore (clangd compile-commands, rust-analyzer cargo features) is answered here by the D-042 coverage set — declared, checked, evidence-carrying. Default is a **designated-primary coverage entry** (a new one-line publisher obligation); switching is a status-bar picker persisted in workspace state. Corollary that strengthens D-042's incentive story: the coverage set is no longer just a publish artifact — it is the IDE's menu, so authors gain editor features by declaring coverage.

### 18. Tree-sitter grammar and the Zed reference client (D-066; editor target SETTLED)

Zed is the reference client (SETTLED): its extension surface is small (`extension.toml` pinning the grammar rev, `config.toml`, `.scm` queries, one WASM shim wiring `language_server_command`), it forces the tree-sitter deliverable, and for this team the agent session (§20) is arguably the real first client; VS Code follows as packaging, agent-buildable against the documented extension surface.

One `tree-sitter-strata` repo under the project org (pre-empting Zig's four-competing-grammars fragmentation), per-editor query directories (`highlights`/`brackets`/`outline`/`indents`/`injections`/`textobjects`/`runnables` — Zed conventions; Neovim/Helix differ). **The coexistence rule, normative: the compiler's parser is the sole source of truth, and CI runs the tree-sitter grammar over the compiler's full test/fuzz corpus (shared with D-053) — any compiler-accepted file producing ERROR/MISSING nodes, or compiler-rejected file parsing cleanly beyond declared tolerance, fails the build.** Grammar updates ride the same PR as parser syntax changes. The grammar is presentation-only: no tool may derive semantic conclusions from it (corollary of R-LS-1). Strata's language properties — no preprocessor, no context-sensitive lexing (D-048) — are exactly what makes SV nearly un-grammar-able and Strata cleanly grammar-able.

### 19. Hardware-native editor features (D-065 phase tiers)

The features with no software analog are all **renderings of ledger queries the batch compiler already answers** — the LSP adds presentation, not analysis. Phase 1 (gated): daemon, incremental sync, Tier-A pull diagnostics, completion/goto/references/hover, semantic tokens with **phase-modality modifiers** (`static`/`hardware`/`ghost`/`symbolic` as token modifiers — ghost code renders dimmed, degrading gracefully in clients that ignore unknown modifiers), in-process `strata fmt`, code actions from P-9 repair objects (D-058-verified MachineApplicable → `quickfix` + `isPreferred`; contract-changing repairs behind the protocol's native `needsConfirmation` annotation — a delivery-side seatbelt on top of D-058's fix), the full P-9 object riding `Diagnostic.data`, tree-sitter grammar + Zed extension with corpus conformance in CI. Phase 2 (ungated, matures with the elaborator): Tiers B/C; ledger-fact hovers and inlay hints (inferred width, clock domain, latency/II, evidence tag — with label-part links to the defining contract); `strata-ls/provenance` ("why does this register exist" as an editor command), `strata-ls/structureReport` (P-2 cost lens), `strata-ls/ledgerQuery`; unsafe/suppression-surface lenses; coverage-corner code lens; `strata-ls/traceAnchor` mapping node IDs ↔ emitted signal paths for Surfer/VaporView-class waveform viewers and counterexample→source navigation ([08 §5](08-verification-platform.md)'s loop, landed in the editor). Prior art stops almost exactly where this list starts: Verible LS/svls/veridian are syntax-level; VHDL-LS resolves names fast but elaborates nothing; only the commercial DVT IDE has elaboration-aware navigation.

Custom requests are namespaced `strata-ls/*`, each documented in an `lsp-extensions.md` with a CI doc-code hash check, and **each new request is a batched register event** (SETTLED — the extension doc is the contract agents build against; rust-analyzer's hash check exists because undocumented extensions rotted).

### 20. Agent access: same daemon, session-multiplexed (D-067)

strata-ls is multi-session by design (the Dart analysis-server shape; LSP's 1:1 assumption handled natively rather than by ra-multiplex-style bolt-ons): editors attach over stdio/socket, agents attach over a JSON session speaking standard LSP plus the `strata-ls/*` set — same checkers, same ledger, same memo-warm state. Agents get exactly what the wire already carries: P-9 objects with stable node IDs, verified applicability, evidence tags. A thin MCP adapter is phase-2 packaging. Session identity gives per-audience telemetry for free (§21). Telemetry consent (D-068): the event schema is designed now (it is the experiment DB's schema), external collection defaults off, first-party only through phase 2, revisited at registry launch.

### 21. The OP-5 measurement harness

OP-5 demands a worked multi-judgment diagnostic taxonomy "user-tested (or agent-tested: measure repair success rate given only the diagnostic)" — and until now had no delivery vehicle. strata-ls is it: multi-judgment failures render as one primary diagnostic naming its judgment, with `relatedInformation` carrying the cross-judgment facts (P-4's "no cross-judgment soup" as a rendering rule); every repair acceptance, rejection, or manual-fix-instead is an experiment-database event keyed by (judgment/lint, repair, audience) — the same repair-accepted÷fired stream D-059 uses for lint demotion, extended to judgment diagnostics. The Infer deployment lesson (diff-time ≈70% fix rate vs batch ≈0) predicts the editor channel dominates repair uptake, making it the right place to instrument first. OP-5's "resolution must deliver" gains: _per-judgment repair-success dashboards from strata-ls telemetry by end of phase 2, cited by the P-9 ship-gate for new judgments._

## North star

- Scoped-lint authoring as a first-class forge artifact kind, with the ring-2/ring-3 promotion pipeline instrumented end to end.
- Formatter-aware merge (structural three-way merge over the canonical AST — the D-052 identity layer makes this tractable).
- Lint-usefulness telemetry published per lint on the registry, closing the Tricorder loop ecosystem-wide.
- VS Code extension (packaging over the stable `lsp-extensions.md`; agent-buildable).
- Waveform-viewer co-development: `strata-ls/traceAnchor` adopted by an open viewer so click-signal→go-to-driver ships outside commercial IDEs for the first time.
- Editor-embedded schedule/pipeline visualization rendered from schedule witnesses ([03 §4](03-time-and-resources.md)).

## Open problems touching this doc

Consumes [OP-6](open-problems.md) (suppressions are pass-maintained ledger facts — ledger erosion would silently disarm re-arming) and feeds [OP-5](open-problems.md) — strata-ls is OP-5's designated delivery vehicle and measurement harness (§21): repair objects are the diagnostic vocabulary's highest-volume consumer, and per-judgment repair-success telemetry is how the P-9 ship-gate gets its data.

````