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.

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), 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.

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.

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. 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.

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.

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.

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.

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.

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 OP-1), and committed scope deliberately under-claims here. See 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.

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 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 P-5 and 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.

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.

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.

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; 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.

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.

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.

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.

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, 04 §6.

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.

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, 08 §5.

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. 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.

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, 07 §7.

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.

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.

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.

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.

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. 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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, 06 §1, 02 §4.

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, 01.

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, 10 §3, 14 §14, 05 §6.

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.

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.

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.

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.

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 §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.

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 §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 §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, 01 P-12/P-13, 07, 08, and 15.

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.

Grade system decisions (2026-08-19)

D-093 · v0 usage grades: grade 0 (erasure) only, attached to ghost let/ghost fn; grade 1, phase modalities, and typestate all deferred whole · DRAFT · high

D-024's {0,1,ω} semiring and D-011's phase modalities are pure spec today — zero code representation anywhere in crates/. The one piece of surface syntax that already parses toward this space, ghost fn/ghost let (crates/strata-syntax/src/parser.rs), is completely inert downstream: strata-hir::item_name discards ghost-ness when naming a function, and lower_block has no arm for GhostStmt, so a ghost let binding lowers to StatementKind::Unsupported and is not represented in HIR at all. v0 finishes exactly this: grade 0 ("erased, compile-time-only, no runtime witness") becomes real, checked via a second one-bit taint pass structurally identical to the existing mem_tainted/reject_if_tainted mechanism (crates/strata-check/src/lib.rs), rejecting a grade-0 value at any hardware-sink boundary (register-update target, mem-write value, output value). Grades attach only to let bindings and whole functions — not parameters, not struct fields, not reg/mem (which are runtime storage by definition and can never be grade 0). Rejected for v0: grade-1 linear enforcement (no concrete binding class exists yet — protocol capability tokens, D-039's natural target, have zero checker representation) and full {0,1,ω} usage-counting (needs a context-splitting linear-typing discipline, genuinely new checker infrastructure, not an extension of the taint pass). OP-7's ω-promotion soundness concern (grade-1 values used inside later-guarded feedback bodies must be ω-promoted, per the wave-2 core-calculus probe's FIX-ω) is not reached by grade-0-only scope — no binding in v0 is ever grade 1 — but is recorded as a hard obligation: FIX-ω must ship atomically with any future grade-1-inside-feedback support, not as a follow-up. Phase modalities (D-011) beyond the grade-0/ghost overlap the spec itself already asserts ("the erasure grade 0 is the semantics of static and ghost binders") are deferred as a separate future decision — different axis (classification, not usage-count), no forcing fixture. Typestate-over-linearity (D-026) is deferred whole, not partially scoped, because it is structurally downstream of grade 1 ("consume the old-state value linearly"), not parallel to it. See 18-grade-system.md.

Linearity decisions (2026-08-19)

D-094 · v0 linearity: a new linear let qualifier, straight-line + single-Select-branch exactly-once checking, no capability-token type, OP-7 unreachable by omission not by choice · DRAFT · high

Re-verified against current crates/: strata-check still has zero Capability/Process<_>/protocol representation, and — new finding — strata-syntax/strata-hir already parse a substantial protocol surface (protocol item declarations with send/recv/msg/role/counter/latch/repeat/if/const/quiesce/invariant entries, session<K> attach, process{...} expressions, all reaching ItemKind::Protocol in HIR) that nonetheless reaches nothing in strata-check — the same "parses and does nothing" pattern as pre-D-093 ghost, but for a full protocol-declaration feature, not the capability-token value D-039 needs. Unlike grade 0, grade 1 has no already-parsing linear-shaped binder to finish (ghost is phase/erasure-shaped, not consumption-shaped) — confirmed by grep, nothing named linear/once/grade exists in the parser. v0 therefore adds the smallest possible new surface syntax, a linear let qualifier structurally identical to ghost let, and explicitly does not add D-039's Capability<Resource> type, acquire/release operators, or the errdefer discharge-obligation check (declining the same scope-multiplication D-093 §2 already declined once). The context-splitting checking discipline replaces local_taint/local_grade's flat HashMap<LocalId, bool> OR-taint with a new local_linear: HashMap<LocalId, LinearBinding> tracking per-binding use counts (Zero/One/Many), with a real join rule at the one branching form the checked IR has today (CheckedExprKind::Select, an if-else expression): consumed identically in both arms is one safe use (only one arm runs), consumed in exactly one arm is rejected naming the unconsumed arm, any straight-line double-use is rejected outright; an end-of-scope sweep rejects never-consumed bindings. match-as-statement and if-without-else stay out of scope because StatementKind::If/Match don't exist in HIR at all yet (confirmed: everything but Let/GhostLet/Register/RegUpdate/Mem/Expr/Return falls to Unsupported) — a parser/HIR prerequisite this doc doesn't take on. OP-7's ω-promotion trap is not reached, but more strongly than grade 0's version of the same disposition: grep for delay/Later/feedback across strata-hir/strata-check returns nothing, so there is no next-argument position for the checker to exclude or include — the trap is unreachable by omission at a lower layer, not by a checking-rule choice. D-093 §7's FIX-ω commitment is restated and sharpened: whoever implements delay/Later<_,_> must, in the same change, either ω-promote linear references found inside next arguments or reject them until that promotion ships — silently applying this doc's straight-line counting inside feedback would reproduce OP-7's exact bug. See 19-linearity.md.

Guarded feedback decisions (2026-08-19)

D-095 · delay/Later<Clock, T> v0: a delay(init, next) builtin (no new grammar), one non-nested call per component, reg <- expr is NOT an informal Later judgment, FIX-ω resolved as branch (b) (structural rejection) · DRAFT · high

Re-verified once more: grep for "delay"/Later/guarded/feedback across strata-syntax/strata-hir/strata-check still returns nothing, and — unlike every prior doc in this series — no fixture anywhere in the corpus uses delay or guarded feedback, so this v0 is scoped directly off D-013/D-029's committed delay : (init: T, next: Signal<T>) → Later<Clock, Signal<T>> signature rather than a forcing example. Central architectural finding, checked directly against StatementKind::RegisterUpdate handling in crates/strata-check/src/lib.rs: reg <- expr is not, even informally, a Later-typed judgment — it type-checks the update value against the register's plain element type T with ordinary same-cycle equality, and the only "guarded-feedback vocabulary" D-092/D-093 referenced is a single boolean bypass in the unrelated mem-taint pass, not a modal type. Later<Clock, T> is therefore new judgment, not existing machinery finished — but it needs zero new strata-syntax grammar, since delay(init, next) parses today as an ordinary ExprKind::Call; the work is entirely in strata-check (a new CheckedExprKind::Delay { init, next } node, promoted from an unchecked Call the way D-092 promoted Index) and a new TypeKind::Later { domain, inner } variant — investigated and rejected reuse of TypeKind::Stamped (that's D-014 epoch-generativity, a different axis from clock-cycle timing). v0 scopes to exactly one, non-nested delay call per component, init restricted to a same-cycle non-self-referential expression, next referring only to that same delay's own settled value — no mutual/multi-delay feedback, no multi-clock guarded quantification (∀κ, already DEFERRED per D-013 §5 directly). Lowering is unchanged from today's reg/seq.firreg path: Later<'d,T> is a purely compile-time causality proof, so no new arch-IR node or CIRCT op is needed. FIX-ω, the obligation D-093 §7 and D-094 §5/§7 both named and declined to resolve, is resolved here as branch (b): any linear-tracked binding referenced inside a delay's next argument is rejected outright (a new reject_linear_in_feedback_next structural walk plus one new linear_uses match arm that never lets next contribute a use upward), landed in this same change — not branch (a) (ω-promoting linear references found in next), because that requires first deciding what "consumed via feedback" means for a grade-1 binding's end-of-scope obligation, a real separate type-system design question the calculus's own FIX-ω corollary (ω-graded periodic capabilities remain usable in feedback) does not settle for grade-1 bindings specifically. Branch (b) is sound, fully specified with no new UseCount variant and no change to linear_uses's existing reconciliation algebra, and closes OP-7's exact gap; branch (a) is named north star, not a further deferral. See 20-guarded-feedback.md.