# proposal/decisions.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/7a7a1544c70f936a726ff076a85218064160dee5/proposal/decisions.md)

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

Visibility: public

Requested revision: 7a7a1544c70f936a726ff076a85218064160dee5

Requested commit: 7a7a1544c70f936a726ff076a85218064160dee5

Commit: 7a7a1544c70f936a726ff076a85218064160dee5

Blob: 2613cf11e5d6f71afd1df6d16353456df13eaeec

Size: 51747 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/7a7a1544c70f936a726ff076a85218064160dee5/proposal/decisions.md?format=markdown)

```
# Decisions Register

Every contestable call in the proposal, one row per decision. The probing phase attacks this register: each `DRAFT` decision gets an adversarial pass that tries to break its rationale, and its status moves to `SETTLED` or `CONTESTED`.

Format: **ID · Decision · Status · Confidence** — rationale, alternatives rejected, where it's used.

## Charter decisions (made by Veronica, 2026-07-17)

### D-001 · Purpose: hybrid build charter · SETTLED

A build charter at heart — concrete, actionable, written for us and for agents working on it — but clean enough to extract a public whitepaper or grant proposal later. Consequence: docs lead with decisions and mechanisms, not persuasion; related-work and motivation are still first-class so extraction is cheap.

### D-002 · Scope: full platform · SETTLED

Language, type system, compiler, verification generation, testing, formal, synthesis/FPGA loop, and agent layer are all in scope, each with its own doc. Depth varies by maturity; the two-track rule (D-003) keeps ambition honest.

### D-003 · Two-track documentation · SETTLED

Every technical doc separates a **committed** design (phase-mapped, buildable) from a **north star** (full design, deferred features, open interaction problems). The single most criticized flaw of `refine-1.md` was specifying a north star with no staging; this rule is the structural fix.

### D-004 · Substrate: new frontend lowering to CIRCT · SETTLED (mapping details DRAFT)

Strata gets its own parser, typechecker, elaborator, and architectural IR; it lowers into CIRCT/MLIR for structural IR, SystemVerilog emission, simulation (arcilator), and formal infrastructure (circt-bmc/circt-lec). Rejected: embedded DSL (comptime, custom judgments, and diagnostics all fight the host language — the Chisel lesson); fully standalone toolchain (years of duplicated backend work for no semantic gain). The _precise dialect entry points_ are a separate decision (D-020, pending research). See [07-compiler-architecture.md](07-compiler-architecture.md).

### D-005 · Target: FPGA-first, ASIC-clean · SETTLED

The agentic loop requires fast, cheap, automated implementation feedback; only FPGAs provide it. Core semantics must not bake in FPGA assumptions (the evidence layer is target-tagged, [06-refinements-and-evidence.md](06-refinements-and-evidence.md)), but cost models, the physical-evidence pipeline, and Phase 1–4 tooling target FPGA flows.

### D-006 · Working name: Strata · SETTLED (trivially reversible)

Chosen by Claude. Names the central thesis — stratified semantic judgments over one substrate. Neutral, greppable, renameable.

### D-007 · Decision latitude: full, via this register · SETTLED

Claude makes remaining technical calls after research, logging each here with rationale, alternatives, and confidence. Probing attacks the register.

### D-008 · Resourcing frame: agent-amplified small team · SETTLED

1–3 humans plus heavy agent labor, multi-year horizon. Consequences: phases must be serially achievable, each phase must produce something independently useful, and the platform should be used to build itself as early as possible (the verification and agent tooling is dogfooded on Strata's own components).

## Technical decisions (made by Claude; all DRAFT until probed)

### D-010 · Stratified judgments, not one composite type · DRAFT · high

A term has one payload type plus separate judgments for time, usage, protocol, effects, and refinements — not a `Stream<8 params>` mega-generic. Rationale: the dimensions obey different laws (nominal vs arithmetic vs linear vs behavioral) and a composite type makes both source and type-equality pathological. Adopted from `refine-1.md` §1. See [02-type-system-core.md](02-type-system-core.md).

### D-011 · Four phase modalities: static / hardware / ghost / symbolic · DRAFT · high

Explicit conversion operators between phases (`reflect`, `reify`, `symbolize`, `observe`). Proofs and specs are erased by construction, not by convention. See [02-type-system-core.md](02-type-system-core.md).

### D-012 · Temporal capabilities over affine resource ownership · SETTLED (committed scope; probe: `probes/interval-caps/`) · high

Resources are typed with availability over event intervals (Filament/Anvil lineage), not consumed-once objects. An affine model cannot express latency ≠ initiation interval, which is the common case. See [03-time-and-resources.md](03-time-and-resources.md). Committed scope starts with fixed-latency intervals; dynamic intervals are staged.

### D-013 · Guarded feedback via a `later` modality · SETTLED as amended (probe: `probes/core-calculus/` — FIX-ω required: feedback-body usage is ω-promoted, the found-and-fixed grades×later unsoundness) · high

Combinational-loop rejection is compositional (feedback ports demand next-cycle values) rather than a post-elaboration graph check only. The graph check remains as a backstop. See [03-time-and-resources.md](03-time-and-resources.md).

### D-014 · Nominal generativity for clocks, resets, epochs, ID namespaces · DRAFT · high

Two structurally identical clock domains are distinct types; transaction/branch/queue IDs are opaque newtypes, optionally epoch- and generation-indexed. Cheapest high-value item in the whole design. See [02-type-system-core.md](02-type-system-core.md).

### D-015 · Protocols as session-typed trace languages, tiered · SETTLED as amended (probe: `probes/protocol-catalog/` — catalog gains `bundle`/`layer` operators, `burst_dyn`, and the monomorphization rule for multiplying parameters; CHI-lite is the designated re-probe) · high

Committed: a fixed catalog of built-in protocol schemas (ready/valid, credit, burst, request/response) with checkable parameters. North star: user-defined refinement session types. Rationale: general refinement-session subtyping has undecidability and inference problems; a catalog gives 90% of the value with predictable checking. See [04-protocols-and-streams.md](04-protocols-and-streams.md).

### D-016 · Tiered refinements: intrinsic / solver / proof · SETTLED as amended (probes: `probes/exhaustive-discharge/` + `probes/static-eval-bounds/` — fourth discharge path with derived bounds; `probes/core-calculus/` wave 3 — term-level refinements as two sorts, static vs state, with three calculus-mandated rules) · high

Tier 1 decidable (linear arithmetic, ranges, finite sets) and compiler-complete; Tier 2 SMT-backed where timeout yields an explicit obligation, never a flaky error; Tier 3 external proof artifacts. Surface syntax distinguishes the tiers (`requires static` / `requires solve` / `requires prove`). See [06-refinements-and-evidence.md](06-refinements-and-evidence.md).

### D-017 · Evidence lattice for physical and unbounded facts · DRAFT · high

Frequency, area, liveness, vendor-primitive correctness are never inferred as truth; they carry evidence tags (`Estimated`, `Tested`, `BoundedProved`, `InductivelyProved`, `TranslationValidated`, `Measured`). Gates (optimizer legality, release criteria) demand minimum evidence strengths. See [06-refinements-and-evidence.md](06-refinements-and-evidence.md).

### D-018 · Speculation as epoch-indexed authority capabilities · SETTLED for committed scope, as amended (probes: `probes/squash-semantics/` — OP-1 resolved for flat epochs, firewall relaxed to consumables-crossing-boundaries, five-invariant squash contract; `probes/epoch-containment/` — OP-2 narrowed, five absorption mechanisms committed, 96% clean) · high

`Speculative<T, Epoch>` values plus capability-gated effects (commit/cancel/external-write authorities), not a boolean tag. The squash/revocation interaction with temporal capabilities is a named open problem ([open-problems.md](open-problems.md) OP-1), and committed scope deliberately under-claims here. See [05-speculation-authority-effects.md](05-speculation-authority-effects.md).

### D-019 · Semantic ledger with conservative invalidation default · SETTLED with riders (probe: `probes/ledger-passes/` — structural touch-sets required; proof facts invalidate per-equivalence, not per-category) · high

IR facts (temporal, protocol, resource, proof, provenance) travel in a ledger; passes declare preserve/transform/discharge/invalidate per fact _category_, with "invalidates everything not mentioned" as the sound default. Rationale: refine-1's "no silent drops" as a hard rule is an unenforceable authoring burden; the conservative default keeps soundness while letting precision grow incrementally. See [07-compiler-architecture.md](07-compiler-architecture.md).

### D-020 · CIRCT entry points · RESOLVED → D-032

Superseded by D-032 after the CIRCT state-of-2026 research brief.

### D-021 · Comptime is typed, deterministic, effect-declared, budgeted · DRAFT · high

No wall clock, network, or undeclared reads; elaboration cost is tracked and reportable. Non-negotiable early because it is impossible to retrofit once generators exist. See [01-design-principles.md](01-design-principles.md) P-6.

### D-022 · Comptime emits canonical architectural nodes, never primitive soup · DRAFT · high

`tree_reduce(max)` elaborates to a `Reduction` node with algebraic facts, not comparators. Hard language rule from day one (impossible to retrofit); it is what keeps the optimizer able to reason. See [01-design-principles.md](01-design-principles.md) P-5 and [07-compiler-architecture.md](07-compiler-architecture.md).

### D-023 · Deferred to north star: general graded coeffects, dependent multiplicities, information-flow labels, power/voltage domains · DRAFT · high

Each is research-grade with unclear interactions; the ledger and judgment structure are designed to accommodate them later. See [11-roadmap.md](11-roadmap.md).

## Research-grounded decisions (made by Claude from the 2026-07-17 briefs; all DRAFT until probed)

### D-024 · Usage grades: `{0,1,ω}` semiring, nothing richer in core · DRAFT · high

The QTT semiring proven practical in Idris 2, whose experience says the payoff is checked erasure; no multiplicity polymorphism in v1 (Idris 2 lacks it too, deliberately). Hardware quantities (per-cycle, replicated-N) are temporal capabilities, not grades. Rejected: Granule-style pluggable algebras in core (menu-of-semirings is north star; user-defined algebras are a research program); dependent multiplicities (no production implementation exists). See [02 §3](02-type-system-core.md).

### D-025 · Refinement engine follows the LiquidHaskell/Flux canon · DRAFT · high

QF-LIA + QF-BV + EUF only in Tier 2; liquid inference internally, annotations at boundaries; PLE-style automation opt-in per module (LH's blowup lesson); linearity keeps refinements pure (Flux's lesson); binder-level incremental re-checking; counterexample surfacing prioritized as the known UX gap. See [06 §1](06-refinements-and-evidence.md).

### D-026 · Typestate is a library pattern over linearity, never a language primitive · DRAFT · high

The survival evidence: Plaid dead, Obsidian stuck in academia (user studies showed annotation cost), Rust HAL typestate deployed at scale as zero-cost phantom states over move semantics. Requirements on the core listed in [02 §6](02-type-system-core.md); transitions return async `Process` protocols since hardware transitions take time and can fail.

### D-027 · User protocols: Rast-lineage, Presburger refinements, check-only, hints on failure · DRAFT · medium

Binary session types + linear-arithmetic refinements; user-written invariants; type equality via a sound-incomplete bisimulation semi-algorithm that terminates asking for an explicit declaration (Rast's recipe). Rejected: refinement inference (doesn't exist); complete subtyping (undecidable, CONCUR 2020/2023). Refines D-015. Phase 3+. See [04 §2](04-protocols-and-streams.md).

### D-028 · Verification backbone assembled from proven pieces + named gaps · DRAFT · high

Hypothesis-style integrated (choice-sequence) shrinking as the shrinker architecture; Cascade-class valid-by-construction generation as the fuzzing bar; RVFI-class commit-level lockstep vs Spike/Sail as the differential backbone (TestRIG is the existence proof, generalized beyond Haskell/ISA); MCY-style mutation scoring as the property-quality oracle; SymbiYosys-witness-as-fuzz-seed as the open pipeline nobody has built (HyPFuzz proved it closed-tool). The four documented field gaps Strata claims are listed in [08](08-verification-platform.md).

### D-029 · Single-clock `later` modality committed; multi-clock guarded quantification deferred · DRAFT · medium

Full clocked type theory exists only in proof assistants; the unary case is simple and beats the practice baseline (Clash typechecks register-free feedback and hangs). Cross-domain feedback must use typed CDC bridges, sidestepping the multi-clock modality entirely in committed scope. See [03 §5](03-time-and-resources.md).

### D-030 · Representation types: distinct numeric domains, no overloaded `+` · DRAFT · high

`Bits/UInt/SInt/Index/OneHot/Gray/Encoded` distinct; arithmetic operations name their width semantics (`wrapping_add`, `full_add`, `checked_add`, ...); all conversions explicit. See [02 §4](02-type-system-core.md).

### D-031 · Schedules are explicit witnesses; cycle behavior is never a compiler artifact · DRAFT · high

The Bluespec negative lesson (users code at the opaque scheduler; stringly urgency pragmas) plus the Kôika/Filament positive lessons (user-visible schedule / schedule in types). `Algorithm → Scheduled<A,S> → Implemented<A,S,I>`; arbitration first-class with real identifiers and cross-module scope. See [03 §4](03-time-and-resources.md), [04 §6](04-protocols-and-streams.md).

### D-032 · CIRCT contract: textual hw/comb/seq/sv/verif MLIR against pinned firtool; architectural dialect owned out-of-tree · DRAFT · high (resolves D-020)

Grounded in measured dialect activity: hw/comb/seq stable-active, arc/moore very active, **pipeline/ssp stale and handshake abandoned in-tree** (Dynamatic vendored it out — the churn precedent), no C++ API stability. We do not enter via FIRRTL (loses our types); we do not build scheduling on their scheduling dialects (ours lives in the architectural IR); provenance stays in the Strata ledger (CIRCT debug/HGLDD can't carry it yet; adopt UHDI export when it lands). See [07 §2](07-compiler-architecture.md).

### D-033 · Formal backends: SymbiYosys primary, circt-lec for combinational EC, circt-bmc adopted when counterexample extraction lands · DRAFT · high

circt-bmc currently cannot emit counterexample traces — disqualifying for a platform whose loop is witness→test; SymbiYosys witnesses work today. Re-evaluate each phase boundary. See [07 §2](07-compiler-architecture.md), [08 §5](08-verification-platform.md).

### D-034 · Dynamic latency via protocols in committed scope; Anvil-style dynamic intervals are north star with an entry criterion · DRAFT · medium

Anvil demonstrates dynamic event patterns are typeable but currently loses ~2× to Filament on static pipelines — not yet a free lunch. Committed: static intervals (Filament-lineage, solver-free or Lilac-style Z3) + outstanding-count refinements at boundaries. Entry criterion for promotion in [03 north star](03-time-and-resources.md). Pairs with OP-8.

## Deep-dive decisions (optimizer/comptime/Rust-Zig briefs, 2026-07-17; all DRAFT until probed)

### D-035 · Design-space parameters: typed, contract-invariant, optimizer-owned · DRAFT · medium

`comptime param` knobs carry a contract-invariance obligation (exported summary identical or refining at every range point — Spatial's behavior-invariant `DesignParam` made a typing judgment); `comptime fixed` for user-owned config. Topology-varying knobs emit `Variant` regions of canonical nodes. Chosen points are ledger facts with evidence. Inverts the HLS-pragma-DSE cost structure: legality checked before synthesis runs are spent. See [07 §7](07-compiler-architecture.md).

### D-036 · Comptime-exhaustive discharge, evidence tag `ExhaustivelyEvaluated` · SETTLED as amended (probe: `probes/exhaustive-discharge/` — per-eval cost bound enforced as hard cap; four deterministic outcomes; predicates barred from budget reads) · high

Exhaustive evaluation of pure predicates over small finite domains as a fourth discharge path (Tier 1 > exhaustive > Tier-2 SMT where applicable): deterministic, never times out (budget-gated up front), yields native counterexample rows, ledger-linked by table hash to the generated node (else generate-and-check gap). Precedents: Zig comptime assert, Rust const-eval asserts. See [06 §1](06-refinements-and-evidence.md), [07 §7](07-compiler-architecture.md).

### D-037 · Width-algebra closure: normalization, never evaluation, in type positions · SETTLED as amended (probe: `probes/width-algebra/` — ℕ₊ positivity for depth params, ℤ-modeling + width≥0 obligation, written confluence argument required, reflect fix-it diagnostics; cliff mapped and accepted) · high

Width expressions in types live in a closed canonically-normalizable algebra (Presburger + clog2/max/min as interpreted symbols); everything else passes through `reflect` of a fully-evaluated static value. Direct design-against of Rust's `generic_const_exprs` five-year stall, whose failure was type equality of unevaluated expressions. See [02 §4](02-type-system-core.md).

### D-038 · Interfaces: coherence + named adapters + sealed keyword + definition-checked bounds with blame rule · DRAFT · medium

Coherent lawful interfaces (deterministic instance selection, P-6); third-party integration adapters as named explicitly-instantiated components (dissolving the orphan-rule conflict — explicit instantiation is idiomatic in hardware); `sealed interface` as the protocol-catalog mechanism (D-015); generator params carry definition-checked bounds (blame: bound violation = caller, body error = author) while bodies use full comptime — the Rust/Zig hybrid neither has. See [02 §8](02-type-system-core.md).

### D-039 · No destructors; grade-1 linearity is the release protocol · DRAFT · high

No Drop, no defer-as-cleanup: Rust made leaking safe so Drop can't carry protocol guarantees, and async Drop's decade-long failure shows time-taking cleanup doesn't fit scope exit — and hardware release always takes time and can fail. Must-consume linearity + explicit release returning `Process<During,Success,Failure>`; errdefer-style failure-disposition checking on multi-step acquisition. See [02 §9](02-type-system-core.md).

### D-040 · No consumer-driven inference, ever · DRAFT · high

Widths/encodings/buffering never inferred from an expression's destination. Zig's result-location semantics (consumer context influencing producer semantics) caused years of footguns and is slated for removal by its own team. Vindicates D-030. See [02 §4](02-type-system-core.md).

### D-041 · Generators receive explicit `ResourceCtx` values · DRAFT · medium

Zig's explicit-allocator idea translated: clock/reset domain, port pools, area budgets, floorplan region passed as a value, so no generator hides its resource appetite (P-2 made structural); instrumented ctx = per-generator budget leak detector; failing ctx tests exhaustion behavior; natural placement hook. See [07 §7](07-compiler-architecture.md). _Extended by D-070: the ctx also carries the regional optimization profile._

### D-042 · Eager library boundaries with config coverage sets · DRAFT · medium

Lazy elaboration for user builds; published components require definition-checked bounds plus a declared config coverage set recorded in the summary as `Tested` evidence. Designs against Zig's documented ecosystem failure (shipped-broken never-instantiated paths). See [07 §6](07-compiler-architecture.md).

### D-043 · Summary-based semver (mechanical, timing-inclusive) and per-component editions · SETTLED as amended (probe: `probes/summary-semver/` — strictly-refining wording, canonical summary encoding, per-field polarity table, evidence sets per guarantee, totality backstop) · high

Summaries make compatibility decidable and total — weakened guarantee, widened assumption, or slower schedule is mechanically major; no software ecosystem can check timing compat. Editions pin per component; composition is summary-level and edition-neutral (hardware IP lives for decades). See [07 §6](07-compiler-architecture.md).

### D-044 · Budget mechanics: declarative, scoped, attributed, readable · SETTLED as amended (probe: `probes/exhaustive-discharge/` — all four properties demonstrated; one carve-out: discharge predicates cannot read remaining budget, preserving proof purity) · high

The four fixes to Zig's `@setEvalBranchQuota` failures (imperative raising, global counter, unattributed exhaustion, unintuitive placement). Fills in P-6/D-021 mechanics. See [07 §7](07-compiler-architecture.md).

### D-045 · Memoized instance identity in the evaluator · DRAFT · high

Comptime calls memoized on (generator, args, config-hash) — sound by construction from D-021 determinism (the thing Rust proc-macros can't have); Chisel's Definition/Instance discipline baked in rather than post-hoc dedup; `Replicate{N, body}` keeps sharing an optimizer decision. See [07 §7](07-compiler-architecture.md).

### D-046 · Architectural-IR reference interpreter as executable semantics · DRAFT · medium

The Miri lesson: a mid-level IR's killer app is an interpreter that becomes the de-facto dynamic semantics. Ours doubles as fast pre-lowering functional simulation and the oracle for translation validation against arcilator/emitted SV. See [07 §1](07-compiler-architecture.md).

### D-047 · forge: Cargo-lineage packaging with summaries as the unit of exchange · DRAFT · high

One manifest, lockfile-pinned resolution, single registry with immutable versions — plus the three hardware-strengthened departures: manifest-acknowledged unsafe surfaces (unacknowledged = resolution error), proof artifacts as first-class content-addressed dependencies, and contract-typed dependency slots resolved by summary refinement. Version bumps are _computed_ from summary diffs (`forge publish` refuses contradicted numbers); patch releases ship equivalence certificates. See [13-package-system.md](13-package-system.md).

### D-048 · Language modules are namespaces; no textual inclusion, no preprocessor; features are typed configuration · DRAFT · high

Canonical paths, explicit imports, declared visibility with the summary as the public surface, one-definition rule at resolution. No `include`, no `ifdef` — comptime config is the only conditionality, and a feature is either contract-invariant (additively composable) or a variant (a different summary, hence a different resolvable artifact); incompatible variant demands are a named resolution error. Each rule is the negation of a documented SystemVerilog failure mode. See [13 §5–6](13-package-system.md).

## Toolchain decisions (fmt/lint briefs + Veronica's charter answers, 2026-07-17)

### D-049 · `strata fmt`: zero-config, 100 columns, edition-versioned style, hard publish gate · core SETTLED, mechanism DRAFT · high

No config file, no output-affecting flags; **100 columns** and **fmt-clean as a hard `forge publish` gate (never a build gate)** settled by Veronica. Style versions with the edition (opt-in evolution, no ambient churn). Rejected: rustfmt option surface (drift), Black stable/preview channels (churn), compile-gating (punishes exploration and agent intermediate states). See [14 §1](14-toolchain.md).

### D-050 · In-band steering; formatter never writes steering tokens · SETTLED

Zig-fmt lineage settled by Veronica over fully-deterministic Prettier-style: trailing comma → one-per-line, blank lines → grouping, nothing else. The anti-Black rule (never _insert_ a trailing comma) avoids the magic-trailing-comma ratchet. See [14 §2](14-toolchain.md).

### D-051 · No vertical alignment; one entry per line in declaration blocks · DRAFT · high

Alignment is the top diff-churn and idempotence-bug source (gofmt tabwriter; Verible's four policies for one construct). Editors may align locally. See [14 §3](14-toolchain.md).

### D-052 · Formatted text is presentation; identity is structural (provenance-stability rule) · DRAFT · high

Normative rule: `fmt(s)` and `s` elaborate to identical IR, ledger identities, summaries, memo keys — only spans differ. Path-based ledger identity with a span side-table; summary hashes exclude trivia; ban on comptime reflection over source text/columns; reformat-only changes are mechanically a patch. Rejected: hashing fmt output as canon (couples cache correctness to formatter idempotence — a formatter bug must never be a miscompile). See [14 §4](14-toolchain.md).

### D-053 · fmt invariants CI-fuzzed; anchored comments; no `fmt: off` in v1 · DRAFT · high

Idempotence, AST round-trip (incl. comment anchors), cross-platform determinism, parse-errors untouched. See [14 §5](14-toolchain.md).

### D-054 · `strata fmt` formats the whole package surface incl. `forge.toml` · DRAFT · medium

One command formats a package; registry-rendered manifests match local. (Claude's call; couples language tool to manifest format — reversible.) See [14 §6](14-toolchain.md).

### D-055 · Lint tier: non-load-bearing declarative queries over the ledger (R-LINT-1) · DRAFT · high

Lints read facts, never assert (sandboxed third-party lints by construction); each declares fact categories read and is auto-silenced on invalidation. No `correctness` group — anything wrong is a judgment; the SpyGlass/Verilator triage confirms the high-value legacy checks all become judgments or die with Verilog's weaknesses. Rejected: extensible type-system plugins (erodes P-8), everything-a-judgment (P-7 forbids estimates bearing load), syntax-keyed lints (imports the legacy FP budget). See [14 §7–8](14-toolchain.md).

### D-056 · Groups `suspicious/design/pedantic/nursery/forge`; severity is consumer policy; default warn for every audience · posture SETTLED, taxonomy DRAFT

Veronica chose **warn-for-everyone** over the recommended agent/human asymmetry: one lint culture; strictness comes from explicit, visible consumer policy (release gates, agent configs), never baked-in audience tiers. Groups are precision/maturity statements with telemetry-gated demotion. See [14 §9](14-toolchain.md).

### D-057 · Suppression is `expect` with mandatory reason, as a pass-maintained ledger fact · DRAFT · high

No bare `allow`; RFC-2383 stale-detection native; node/component scope only; optional evidence backing and edition-keyed `review_by`; transitive suppression-surface roll-up beside the unsafe surface. Grounded in Rust's allow-culture postmortem and the FSE 2025 suppression study. See [14 §10](14-toolchain.md).

### D-058 · Repair applicability verified via summary diff, not declared · SETTLED (probe: `probes/summary-semver/` — implemented as a 6-line wrapper over the semver diff; the reuse claim is real) · high

MachineApplicable iff the typed edit leaves the summary bit-identical or refining — reusing the mechanical-semver machinery; fixes clippy's wrong-MA bug class. See [14 §11](14-toolchain.md).

### D-059 · Diff-time surfacing; telemetry-driven demotion · DRAFT · high

Default presentation on the summary diff (Infer's ~70% vs ~zero fix-rate result); full-tree in aggregate report/gates; per-lint effective-usefulness from the experiment DB drives auto-demotion (Tricorder's <10% threshold). See [14 §9](14-toolchain.md).

### D-060 · Publish gate "adjudicated, not clean"; three-ring lint governance · SETTLED

Both settled by Veronica: publish requires zero _unaddressed_ `suspicious`/`design` findings (every survivor `expect`-ed with reason; suppression surface published and registry-queryable); catalog governance = core-owned global groups (nursery-first, telemetry-gated), package-scoped lints, register-event promotion; third parties never touch `suspicious`. See [14 §12–13](14-toolchain.md).

## Language-server decisions (strata-ls brief + Veronica's charter answers, 2026-07-17)

### D-061 · strata-ls is the resident compiler; phase-1 gate at Tier A · gate SETTLED, mechanism DRAFT · high

One binary hosts parser/checkers/evaluator/ledger/lint; `strata build` and strata-ls are two drivers over one library. Phase-1 gating (Tier A only) settled by Veronica — the one-frontend property is cheap now, brutal to retrofit (rustc/rust-analyzer library-ification, Kotlin K2 rewrite, zls's no-semantics gap are the evidence base). Speed from existing machinery: summary firewall as invalidation boundary, durability tiers over summaries, body-local recheck, cancellation — no salsa-class query graph. Rejected: separate LS codebase (the split we designed against); per-request compiler spawn (no warm memo cache). See [14 §15](14-toolchain.md).

### D-062 · One tree for parser, fmt, LSP — D-052's AST with error tolerance · DRAFT · high

Additive requirements: lossless on invalid input, ERROR/MISSING containment with incomplete-but-present nodes (resilient-LL), incremental reparse, and path-based identity defined over recovered trees (ERROR nodes get deterministic paths — broken code is the LSP's diet). Rejected: tree-sitter as the compiler tree (unpredictable GLR recovery; upstream disclaims frontend use); a separate IDE tree (second frontend by the back door). See [14 §16](14-toolchain.md).

### D-063 · Editor comptime tiering: bounds / active config / on demand · DRAFT · high

Tier A keystroke-level with zero elaboration (D-037 normalization + D-038 bounds make this possible — the tier zls structurally cannot have); Tier B one memo-warm pinned instantiation under D-044 budgets (the cache rust-analyzer hacks around, sound here by D-021); Tier C background/on-demand for other coverage points, SMT, lint. Each field failure mode (zls, clangd templates, r-a proc-macros) is pre-fixed by a named existing decision. See [14 §17](14-toolchain.md).

### D-064 · Active config = pinned coverage-set point, visible picker · SETTLED (UI), DRAFT (mechanics)

Veronica settled the visible status-bar picker defaulting to a designated-primary coverage entry (new one-line publisher obligation). Candidates are declared/checked/evidence-carrying (D-042) rather than build-system folklore. Corollary: the coverage set becomes the IDE's menu — authors gain editor features by declaring coverage, strengthening D-042's incentives. See [14 §17](14-toolchain.md).

### D-065 · LSP feature tiers by phase · DRAFT · medium

Phase 1 (gated): Tier-A diagnostics, completion/goto/hover, phase-modality semantic-token modifiers, in-process fmt, verified repair objects as code actions (`needsConfirmation` on contract-changing ones), P-9 object in `Diagnostic.data`, tree-sitter + Zed extension. Phase 2: Tiers B/C, ledger-fact hovers/inlay hints, provenance/structure-report/ledger-query custom requests, coverage-corner lens, waveform trace anchors. See [14 §19](14-toolchain.md).

### D-066 · tree-sitter-strata: compiler parser is truth; grammar is conformance-tested presentation · DRAFT · high

One org-owned grammar repo (pre-empting Zig's fragmentation), per-editor query dirs, presentation-only (no semantic conclusions — R-LS-1 corollary). Normative CI rule: grammar parses the compiler's full corpus with zero ERROR/MISSING on accepted files; grammar changes ride parser-change PRs. Zed as reference client settled under D-061's answer set. See [14 §18](14-toolchain.md).

### D-067 · Agent access: same daemon, native multi-session; `strata-ls/*` under register governance · governance SETTLED, mechanism DRAFT

Agents attach as JSON sessions to the same daemon (same checkers, ledger, memo-warm state); MCP adapter is phase-2 packaging. Each new custom request is a batched register event with `lsp-extensions.md` + CI doc-hash (settled — undocumented extensions rot; the doc is the agent contract). Session identity yields per-audience repair telemetry free. See [14 §20](14-toolchain.md).

### D-068 · Repair telemetry: schema now, first-party only, external default-off · DRAFT (Claude's call) · high-confidence-conservative

The repair-success event schema is the experiment DB's existing schema; collection from external users defaults off and is revisited at registry launch. D-059's demotion loop and OP-5's dashboards run on first-party data through phase 2. See [14 §20–21](14-toolchain.md).

## Optimizer-input decisions (2026-07-17, drafted by Veronica, integrated; all DRAFT until probed)

### D-069 · Every typechecker narrowing becomes a ledger fact; assertions are claims routed through the tiers · SETTLED (probe: `probes/guard-inference/` — one analysis, two projections; failure-weakens-guards safety direction; 9/12 patterns infer exactly, `narrow!` only at dataflow boundaries) · high

Three mechanisms, one pipeline: flow-sensitive narrowing (match arms, guards) is harvested onto dominated nodes as range/membership facts — completing the 07 §5 argument against rediscovery, since CIRCT's interval analysis is path-insensitive and ours is the checker's own path-sensitive knowledge, free; `narrow!(p)` assertions are never trusted — they route through Tier 1/2, `comptime_exhaustive` (D-036), or become an `Obligation` usable only at `Assumed` (P-7 consumer pattern holds); comptime-computed value sets from decode tables stamp `StaticallyDerived` don't-cares, ledger-linked by the D-036 table hash. See [07 §5](07-compiler-architecture.md), [06 §1](06-refinements-and-evidence.md), [02 §4](02-type-system-core.md).

### D-070 · Modes are objective profiles over one semantics, composed through ResourceCtx; safety is never a mode · DRAFT · high

`small`/`fast`/`low-power` are objective vectors on the contract-shaped search — no mode-dependent meaning; regional attachment via D-041's ctx (cold config block inherits `minimize(area)` inside a `maximize(frequency)` core); chosen profile per region is a ledger fact. `safe` explicitly rejected as a mode — safety is judgments + evidence gates, now stated in P-1 ("no -O0 is safer"). The legitimate fourth axis is hardening/debuggability, riding the existing proof-only→production-encoded spectrum (02 §5). See [07 §5](07-compiler-architecture.md), [01](01-design-principles.md).

### D-071 · Likelihood is evidence (`Estimated`/`Measured`), licensing cost choices, never legality · DRAFT · medium

Declared or (preferably) FPGA-loop-measured likelihood facts license asymmetric cost decisions — arm latency assignment, mux defaults, arbitration priority defaults, `Variant` selection, gating aggressiveness, rare-path stage placement — with observable semantics protected by the equivalence-class checks. Hardware PGO = workload counters → `Measured<Workload>` facts on stable node identities (D-052 keeps profiles attached across reformats — stronger than software PGO's source-location anchoring) → re-run the search. Logged caution: hint-driven timing asymmetry is a side-channel generator by construction; `likelihood_timing_secret_adjacent` lint watches the intersection with the deferred info-flow story. See [07 §5](07-compiler-architecture.md), [10 §3](10-fpga-loop.md), [14 §14](14-toolchain.md), [05 §6](05-speculation-authority-effects.md).

### D-072 · Implementation language: Rust for all tooling; TS/Bun only for throwaway probes · SETTLED (Veronica, 2026-07-17)

The compiler, strata-ls, forge, fmt, lint, and all shipped tooling are Rust. TS with Bun is permitted for quick logical probes and prototypes, which are rewritten in Rust if promoted — probe repos state their language and this rule in `probes/README.md`. Consequences: rowan/egg/proptest-class crates are natural dependencies; the CIRCT boundary stays textual MLIR (D-032), avoiding C++ linkage from Rust.

## Boundary and physical decisions (drafted by Veronica, adversarially verified, integrated 2026-07-17)

### D-073 · Exit-boundary discipline: every ledger fact exits baked, delegated, or verified — one dial, accounted · DRAFT (verification-hardened) · high

Drafted by Veronica, adversarially verified before integration (three corrections applied): baking is per-fact policy with _checked inference_ as a legal exit form (blanket "never inference patterns" struck — it fights vendor guidance and forfeits packing/retiming); SV's don't-care problem is _unsound expression_ (sim/synth divergence), not inexpressibility; and the exits are coupled — the bake↔delegate choice determines the achievable equivalence class at Exit 3 (combinational LEC for fenced regions, sequential-EC-or-assertion-grade for released ones), recorded per node. Boundary ledger report + `fact_dropped_at_boundary` lint make losses named diagnostics. D-086 later contests the timing-exception special case: semantic generation yields a candidate, and exact post-synthesis validation is mandatory. See [07 §2b](07-compiler-architecture.md).

### D-074 · Dual emission: RTLIL alongside SV; SV demoted to exchange format · DRAFT (verification-hardened) · medium

RTLIL under pinned-version interchange discipline (it is Yosys-internal with no stability guarantee — same contract shape as pinned firtool, D-032); direct `read_rtlil` into SymbiYosys (no re-parse); don't-cares and formal cells expressible; open flow = Yosys synth → `write_json` → nextpnr (corrected: nextpnr ingests JSON, not RTLIL), where Exit-2 facts become Exit-1 and the vendor-boundary cost becomes measurable per design. D-032 unchanged; SV's role formally "exchange format under the exit discipline." See [07 §2b](07-compiler-architecture.md).

### D-075 · Physical information: four channels in, one door closed · DRAFT (verification-hardened) · high

Evidence, coeffect obligations, search inputs, budgets-vs-estimates are the four channels; physical facts never enter type equality or judgment soundness. Hardened wording: post-P&R timing is a function of (design, context, target, tool, seed) — sound term-alone judgments must quantify over contexts (too loose to bear load) or freeze context (then it's `Measured` evidence about an artifact); composition has no frame rule. RapidWright pre-implemented modules are the boundary case: locked-placement timing as evidence on an artifact, never a type. Survey confirmed no counterexample (Filament/Anvil/Spade type cycle-level only; PipelineC treats frequency as parameter + measurement). See [10 §5](10-fpga-loop.md).

### D-076 · Release-full spatial optimization: objective profile + compute budget over the measured search loop · DRAFT (verification-hardened) · medium

Drives the search around the vendor placer (RapidLayout/AutoBridge prior art; direct placement scoped to AMD/Xilinx via RapidWright; open flow for deeper ownership); learned ranking models with industrial precedent named (DSO.ai/Cerebrus/AlphaChip); Strata performs deterministic contract-legality checks before ranking while backend and physical claims still require evidence. Monotonicity is only QoR-relative: keep-the-best over legality-checked candidates against a pinned measurement protocol; more compute does not strengthen contracts or evidence. See [10 north star](10-fpga-loop.md).

## Systems-safety extension decisions (probe wave, 2026-07-21)

### D-081 · Fault contracts separate occurrence, detection, correction, containment, and invalidation · SUPPORTS-SETTLED for model scope (`probes/fault-health/`) · high

`HealthEpoch` stays nominally distinct from the reset/speculation tree. Both reuse a factored invalidation kernel (generativity, authority revocation, stale rejection, optional drain), while only resource-owning specializations inherit conservation/occupancy obligations. A corrected transient need not kill health; an uncorrectable fault may invalidate at detection, but containment must separately cover occurrence→detection.

### D-082 · Mapped regions are enforced leases with bounded borrows and opaque generations · SUPPORTS-SETTLED for model scope (`probes/dma-iommu/`) · high

DMA never receives integer address authority: the mapping owner mints bounded operation borrows; every physical issue is mediated, snapshots authorization and target, and drains against that snapshot. Unmap/invalidation completion waits for translation retirement. Full opaque generations bear authority; wrapping wire projections never do. Mapping epochs remain owner-validated rather than ambient.

### D-083 · Progress summaries have stable `proved/refuted/obligation` outcomes · SUPPORTS-DRAFT (`probes/progress-waitfor/`) · medium

Finite wait summaries export held resources, release events, protocol phase, VC, fairness class, and named assumption ownership. Acyclicity, well-founded ranks, and independently provisioned escape resources may prove progress; closed reachable SCCs refute it; state/fairness-dependent cases remain obligations. Weak fairness proves no finite bound, and circular assume/guarantee ownership is never a proof.

### D-084 · Memory consistency is a separate architectural relation judgment · SUPPORTS-WITH-OBLIGATIONS (`probes/memory-consistency/`) · medium

Core/cache/DMA/interconnect summaries export partial program-order, reads-from, coherence, dependency, fence, atomicity, and visibility relations with explicit completeness. Composition checks a selected architectural model; missing completeness produces an obligation. A protocol-legal trace can still expose illegal memory behavior, so protocol monitors cannot discharge this judgment.

### D-085 · Observer projections are semantic; noninterference remains relational · SUPPORTS-NORTH-STAR (`probes/observer-flow/`) · high

The reference semantics admits `Obs<O>: Trace → Observation`; implementation equivalence and two-run noninterference remain different ledger facts. Declassification consumes named policy authority. Observer relations form a preorder with real incomparability (cycle/cache and debug/contention in the probe), not one clearance chain; power observations remain model/measurement evidence.

### D-086 · Timing exceptions are candidate certificates until exact post-synthesis validation · CONTESTED (`probes/physical-constraints/`) · high

D-073's sound-by-construction qualifier is withdrawn. Source schedule/stability facts justify an intended category-specific exception, but admission requires exact nonempty intended-vs-actual netlist path binding, lineage, precedence, setup/hold, mode, and clock checks. Retiming, cloning, schedule/clock/mode/netlist changes invalidate the certificate. Timing exception delegation therefore mandates Exit 3.

### D-087 · Power and reconfiguration are lifecycle/invalidation protocols, not labels · SUPPORTS-DRAFT (`probes/power-reconfig/`) · medium

Isolation gates authority at crossings; retention and DVFS evidence carry validity epochs; quiescence is assembled from closed sessions and returned tokens; replacement requires ABI refinement plus independent authenticity/target/design evidence and mints a region generation. Power loss and replacement reuse invalidation shape but keep distinct transition protocols and physical assumptions.

### D-088 · Numeric meaning and numeric budgets split across representation and contracts · SUPPORTS-DRAFT (`probes/numeric-error/`) · medium

Unit, scale, width/signedness, rounding, overflow policy, and attached calibration identity determine bit denotation and belong in representation semantics. Ranges, saturation reachability, correlation symbols, freshness, approximation bounds, and remaining budgets are contracts/evidence; transformations require certificates against the final budget.

### D-089 · DFT/debug are authority effects and proof-carrying transformations · SUPPORTS-DRAFT (`probes/dft-debug/`) · high

Scan, JTAG/debug, trace, fault injection, and ECO writes require distinct scoped authorities minted by authenticated lifecycle transitions. Secret/scan policy survives in the ledger. Insertion proves functional observer equivalence plus security-observer refinement under fuse, mode, power, and isolation premises; ordinary bit/cycle equivalence is insufficient.

### D-090 · Assurance cases are derived custody graphs, never evidence · SUPPORTS-PROVISIONAL (`probes/assurance-cases/`) · high

Generated hazard→guarantee→assumption→artifact graphs track ownership, hashes, expiry, design/tool/target pins, evidence sets, diversity, release diffs, and residue. Their deterministic reports gate releases but cannot cite themselves or strengthen the primary artifacts they summarize.

## Syntax decisions (2026-07-17)

### D-077 · Syntax charter: value-flow components, Rust-split generics, let/reg/inst, semicolons + comma-list bodies; tiebreaker = Rust when unsure · SETTLED (Veronica)

Chosen from rendered previews after the landscape research (Spade/Veryl/Chisel/Bluespec lessons; agent-friendliness evidence: ~55% of LLM Verilog failures are syntax-class in exactly the spots Strata deletes). The standing tiebreaker resolves all minor forks (`#[attr]`, `where`, `::` paths, comments, ranges, naming) toward Rust; overrides require a logged hardware-semantic reason. See [16-syntax.md](16-syntax.md) §2.

### D-078 · The committed-core surface design of 16-syntax.md · DRAFT-COMPLETE (pending fmt dry-run + blind regeneration) · high

Complete for the R1–R36 committed core, reconciled from the syntax probe wave (syntax-grammar, syntax-corpus-core, syntax-corpus-verif): all item/statement/expression/type/pattern forms, protocol two-dialect rule, verification surface (contract assume/guarantee/claim with evidence sets, named requires/discharge, strategy fn, state_machine, property, differential_test, experiment), epoch surface with the unit-epoch normalization rule, quantity/evidence literal grammar with a closed unit table, R1–R36 traceability table, rejected-constructs register (standalone `connect` rejected; `is_pow2` deferred pending its D-037 confluence-interaction argument; `T @ 'E` sugar adopted on parse evidence), and the full normative EBNF appendix. Notable calls unchanged: `Nat1` (R19), no bare `-` on hardware integers (R8), half-open little-endian slicing, no tick-literals, named-only instantiation with punning, one duality-checked connect form, apostrophe labels for domains and events, `stamped`/`rebind`/`same_epoch` as the entire user-facing epoch surface. R37–R50 are excluded until D-091's dedicated systems-safety surface wave. Settles only via: (1) fmt dry-run over both corpora against the 16 §13 rules; (2) blind regeneration of the corpora from the spec alone. See [16-syntax.md](16-syntax.md).

### D-079 · `reg` forms: declaration + `<-` next-cycle write, no `=` next-value form · SETTLED (main line)

`reg name: T reset(v);` declares (reset value mandatory unless the domain is `no_reset` or the register is explicitly `uninit` per 02 §6); updates are `name <- expr;` statements — the next-cycle write, sequential last-write-wins within a body, elaborating to a priority mux. There is NO `= expr` next-value form at the declaration. Rationale: one meaning per token — `=` binds combinational values, `<-` is the visible Later-boundary write; multi-arm updates stay natural. Resolves the draft-internal contradiction both corpus probes hit independently (core F1/G7, verif F1/G-S34: the same `= e` position read as reset value in one example and next value in the other — agents would emit frozen registers). See [16-syntax.md](16-syntax.md) §2, §5.

### D-080 · Grammar-evidence decisions: no-brace generics, header struct-literal forbid, hard-reserved keywords, Meta micro-grammar · SETTLED (probe evidence)

From `probes/syntax-grammar/` (resilient-LL parser + tree-sitter, 21 tests green, 3000 mutated inputs lossless + deterministic): (1) the restricted D-037 angle-bracket algebra makes bare `<>` unambiguous — `>` always closes, `,` always separates; no brace fallback; lexer never emits `>>`/`>=`, parser glues. (2) Struct literals are forbidden at the top level of `if`/`match`/`for` headers and match-arm guards (parenthesize to opt in) — always-allow was measured ambiguous (GLR-only), failing resilient-LL and generation-commitment requirements. (3) The flagged soft keywords `state`, `on`, `preserve`, `at_most` are hard-reserved (each soft keyword degrades highlighting/recovery). (4) The Meta micro-grammar for attribute/`expect` metadata is committed — budgets (R22) get real structure, never balanced-token soup. Also: `;` canonical on `requires` (GAP-19), interface bounds in `where` (LL(2)), where-lists take no trailing comma. See [16-syntax.md](16-syntax.md) §3, §6, §9, §16.

### D-091 · Systems-safety architecture uses a semantic thin waist, sparse opt-in contract families, and backend evidence packages · PROBE-SUPPORTED-DRAFT · high

D-081–D-090 do not add ten universal term judgments. The foundational model grows only reusable semantic vocabulary: stable identity/lineage, generic invalidation, architectural events/relations, observer projections, exact numeric denotation, and extensible authority. Fault/recovery, mapping, progress, memory-model, power/reconfiguration, relational-security, DFT, and assumption-ownership schemas are sparse opt-in component contracts. Campaigns, model/relational checks, netlist binding, translation validation, numeric certificates, and assurance graphs live in verification/evidence packages. Absent families impose no annotations or placeholder obligations. The systems-safety surface is not part of D-078: R37–R50 require a dedicated corpus/grammar/fmt/blind-regeneration wave. Rationale: preserve the existing stratified calculus and ordinary usability while allowing all families to share custody and release evidence. See [00](00-vision.md), [01](01-design-principles.md) P-12/P-13, [07](07-compiler-architecture.md), [08](08-verification-platform.md), and [15](15-syntax-requirements.md).

## Memory model decisions (2026-08-19)

### D-092 · `mem` reuses the existing Array type; registered reads; one read port + one write port in v0 · DRAFT · high

`mem name: [T; N];` gets no new `Type` variant — `TypeKind::Array` already exists and already backs both `reg`-array declarations and `mem` declarations in the fixture corpus, so this is a new storage-class declarator over existing type vocabulary, not a new type. Reads are registered (1-cycle latency), not combinational: real BRAM primitives are inherently synchronous, and a combinational-read `mem` would just duplicate `reg [T; N]`, which already covers that case. v0 supports one read port and one write port, concurrently usable — forced by `fifo.strata`'s same-cycle push/pop, not a simplicity choice. Indexed reads and writes both accept any `Index<N>`-typed index, constant or runtime; `Index<N>` already proves boundedness by construction (D-030), so no separate bounds-check pass or constant-index restriction is needed or wanted. Rejected: compile-time-constant-only write indices (`fifo.strata` and `epoch_soc.strata` already index writes with runtime register values; restricting to constants would make the motivating fixtures uncheckable for no safety gain). `fifo.strata`/`cdc_bridge.strata` will need a one-cycle body rework once this lands — expected, since `mem` today has zero downstream semantics past the parser. See [17-memory-model.md](17-memory-model.md).

<!-- Next ID: D-093. Add inline in docs and register here. -->

```