# proposal/07-compiler-architecture.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/6c85305ce0ccf51e9a5b344011865ac991b2528b/proposal/07-compiler-architecture.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: 6c85305ce0ccf51e9a5b344011865ac991b2528b Requested commit: 6c85305ce0ccf51e9a5b344011865ac991b2528b Commit: 6c85305ce0ccf51e9a5b344011865ac991b2528b Blob: e4948e30a87b434fec61ba7d4db5e41055778f68 Size: 37222 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/6c85305ce0ccf51e9a5b344011865ac991b2528b/proposal/07-compiler-architecture.md?format=markdown) ```` # Compiler Architecture The IR stack, the CIRCT lowering strategy, the semantic ledger, proof-carrying passes, and incremental summaries. Principles in force: P-3 (meaning survives lowering), P-5 (architecture recognizable until explicit boundaries), P-6 (deterministic elaboration). ## Committed design ### 1. The stack ``` Typed source → comptime elaboration (typed graph construction, P-6 budgeted) → Architectural IR (Strata-owned: components, canonical arch nodes, judgments, contracts) → Verification IR (Strata-owned: assertions, symbolic values, strategies, monitors — [08]) → Structural IR = CIRCT hw/comb/seq (+ sv for emission) → SystemVerilog / simulation / formal backends ``` Canonical architectural nodes (`Reduce`, `Arbitrate`, `Buffer`, `CrossClock`, `Pipeline`, `Reorder`, `Reserve/Commit/Cancel`, `Decode`, `Memory`, `TransactionTable`) survive until the Architectural→Structural boundary, carrying their laws (P-5, D-022). Scheduling happens _within_ the Architectural IR as schedule witnesses ([03 §4](03-time-and-resources.md)) — see §2 for why we don't use CIRCT's scheduling dialects. The Architectural IR ships with a **reference interpreter** as its executable semantics (D-046 — the Miri lesson: a mid-level IR's killer app is the interpreter that becomes the de-facto dynamic semantics). It serves as fast functional simulation before lowering and as the oracle that translation validation compares against (P-8 needs a reference semantics regardless; this makes it a tool, not a document). A **design-lint tier** runs over the ledger, outside the type system, clippy-style — leveled, and emitting machine-applicable P-9 repair objects ("CDC without typed bridge", "arbiter without fairness evidence", "estimated fanout > N") — the agent loop's cheapest feedback currency. ### 2. CIRCT integration (D-032, resolves D-020) Grounded in the 2026 state of the project: - **Entry point: textual MLIR at `hw`/`comb`/`seq` (+ `sv`, `verif`) against a pinned firtool release.** These core dialects are stable and actively maintained; textual MLIR/CLI is the integration contract CIRCT actually keeps (weekly firtool releases), whereas C++ linkage means chasing MLIR+CIRCT churn with explicit no-stability policy. We do _not_ enter via the FIRRTL dialect: it would discard Strata's type/architecture information (width inference, early aggregate lowering, no parametric polymorphism at that level). - **Own the architectural dialect out-of-tree.** Every frontend with rich semantics (Chisel→firrtl, slang→moore) owns its ingestion representation. The Dynamatic project's experience — vendoring the Handshake dialect out of CIRCT to control its destiny — is the cautionary precedent; we start out-of-tree by design rather than retreat to it. - **Do not build on `pipeline`, `ssp`, `fsm`, or `handshake`.** Measured activity shows pipeline/ssp stale and handshake abandoned in-tree; ssp's own docs scope it to prototyping. Strata's scheduling semantics are too load-bearing to rest on research leftovers — schedule witnesses live in our IR and lower directly to `seq` registers. - **Simulation:** arcilator (`arc`, very active) for fast cycle-accurate simulation of the structural IR; emitted SV for commercial/Verilator flows. **Synthesis-adjacent:** watch `synth`/`circt-synth` (AIG synthesis + longest-path timing) as a pre-vendor estimation backend for the [cost model](10-fpga-loop.md). - **Formal (D-033):** circt-bmc/circt-lec are real but early — bounded, practically single-clock, and **counterexample extraction is not yet wired**, which is disqualifying for a platform whose currency is counterexamples-become-tests ([08 §5](08-verification-platform.md)). Committed primary open backend: Yosys/SymbiYosys (witness traces work today) over emitted SV; circt-lec for combinational equivalence where signatures match; migrate toward circt-bmc as it matures (the SMT dialect now lives upstream in MLIR — good sign). Re-evaluate each phase. - **Provenance stays in Strata IR.** CIRCT's debug dialect + HGLDD is Chisel/VCS-shaped and can't yet express enums, subfields, or stable IDs through lowering (UHDI is in-flight, not landed). Strata's ledger (§3) is the provenance source of truth; we emit `loc`-based comments into SV (solid today) and adopt UHDI export when it lands. ### 2b. The exit boundary: no derived win dies at emission (D-073, D-074) The enemy at the SV boundary isn't syntax — it's **re-derivation**: anything expressed as inferable RTL invites vendor synthesis to re-discover (or fail to discover) what we already proved. P-3's "no silent drops" extends to the toolchain exit: every ledger fact leaving Strata takes one of three accounted exits — and the exits are **one dial, not three bins** (verification-hardened, 2026-07-17): the more a fact is baked and fenced, the cheaper its verification; the more is delegated, the harder equivalence checking gets. The choice is made per-node and recorded, with the resulting _achievable equivalence class_ a ledger fact. - **Exit 1 — Bake.** Derived wins applied before emission, emitted as already-transformed structure. Chosen _per fact_, not as a blanket rule: **explicit primitive where the evidence is load-bearing on structure** (vendor restructuring would destroy or unverify it); **vendor-recognizable inference pattern plus attribute** (`ram_style`, `use_dsp`) where vendor packing/retiming is wanted — and in the inference case the fact moves to Exit 3: the check confirms the pattern actually matched, converting inference from an unchecked contract into a checked one. (The blanket "always instantiate primitives" rule is explicitly rejected — it fights UG901-class vendor guidance and forfeits DSP/carry-chain packing and retiming around macros.) The forcing case is derived don't-cares (D-069): SV expresses don't-cares only as unchecked, sim/synth-divergent assertions (`casex`, x-assignment — the Sutherland/Cummings mismatch literature), so proven don't-cares are either spent by our own structural optimization pre-emission or exit via RTLIL, never as `casex`. - **Exit 2 — Delegate.** Physical-knowledge facts travel as the constraint bundle: generated multicycle/false-path **candidate certificates** from `During` stability and schedule facts; floorplan constraints from `ResourceCtx`; fanout budgets. Timing exceptions are category-specific and per-vendor (XDC ≠ SDC ≠ Quartus-SDC; `-setup N` usually needs its `-hold N-1`): source semantics proves the intended exception, not that a backend selector names exactly those post-synthesis paths. Admission therefore mandates Exit 3's exact, nonempty intended-vs-actual path-manifest, lineage, precedence, clock/mode, and setup/hold checks; retiming, cloning, or schedule/clock/mode/netlist changes invalidate the certificate (D-086, `probes/physical-constraints/`). Fencing uses the per-vendor attribute table (AMD `DONT_TOUCH` — the one that survives P&R, vs `KEEP`/`KEEP_HIERARCHY`; Intel's split `preserve`/`noprune`/`keep`), **scoped to minimal cells, never hierarchies**, and _inverted from industry practice_: fences protect proven structure from re-derivation while elastic-contract regions are explicitly released for vendor retiming. Delegation = permission grant + fence + mandatory boundary validation, all ledger-derived. - **Exit 3 — Verify.** What can't bake or fence emits as netlist-bound assertions plus post-synthesis equivalence checking — **at the class the dial permits**: fenced/baked regions get combinational LEC (EQY-tractable today, with its Vivado post-synthesis flow); regions released for retiming/re-encoding need sequential EC (commercial EC-FPGA class) or drop to assertion + simulation evidence, _recorded as such_ in the evidence lattice. Boundary losses are caught and named, never silently shipped; `fact_dropped_at_boundary` is a lint ([14 §14](14-toolchain.md)). The emission pass produces a **boundary ledger report** — baked/delegated/verified/dropped per fact — so the boundary has the same accountability as every pass (P-3, D-019). **Dual emission (D-074).** SV is demoted to _exchange format_ — the container for committed decisions + constraint bundle + checks — kept because vendor P&R and signoff ingest nothing else. **RTLIL joins as the lossless reference path**, under D-032's pinning discipline (RTLIL is Yosys's internal format with no cross-version stability guarantee — the contract is _pinned-version interchange_, exactly like pinned firtool): SymbiYosys consumes it directly via `read_rtlil` with no Verilog re-parse; proven don't-cares stay don't-cares (`x` in case patterns, formal cells); and it opens the fully open flow — Yosys `synth_*` → `write_json` → nextpnr — where Exit-2 facts become Exit-1 (we drive placement directly), making the open flow the instrument that _measures what the vendor boundary costs, per design_. FIRRTL stays rejected (D-032); Calyx is the wrong altitude; EDIF the wrong trade for FPGA-first. ### 3. The semantic ledger (D-019) Every architectural/structural node is queryable for its facts: identity/provenance (stable ID, source expr, comptime call, config, lowering lineage); representation (logical type, encoding, width, unit, scale, rounding, overflow, calibration identity); temporal (domain, event relations, availability, latency bounds); protocol (trace type, ordering relations, capacity); architectural memory (events, reads-from/coherence/program/dependency/fence relations, visibility/atomicity scope, completeness); resource (capabilities consumed/produced, exclusivity, mapping leases); effects/authority (including debug, test, fault-injection, reconfiguration); validity/invalidation (epoch family, generation, death event, freshness, repair/validation); observer projections and declared equivalence/noninterference facts; proof (owned assumptions, guarantees, obligations, evidence, expiry); optimization (equivalence class, permitted transforms); physical (intended constraints, actual netlist bindings, estimates, measurements, target/tool/mode/seed); and assurance dependencies/residue. This schema is the thin waist, not a requirement that every node populate every category. Contract-family presence controls which categories are live. A pass touching no memory event cannot invalidate memory completeness merely because the schema knows that category; a pass that clones or retimes a node with a bound timing certificate must invalidate its lineage-dependent binding. Ledger coverage metrics are therefore reported both globally and per active contract family. Passes declare, per fact **category**: `preserve | transform | discharge | weaken | invalidate`. **The default for anything undeclared is `invalidate`** — sound by construction. Erosion (everything invalidated, ledger useless) is countered by per-pass ledger-coverage metrics in CI and full annotations on the small set of core passes we own ([OP-6](open-problems.md)). Ledger entries are machine-readable; the provenance queries of P-3 ("why does this register exist?", "which contract generated this assertion?") are ledger queries. ### 4. Optimization under equivalence classes and contracts Named observational equivalences — `BitExact`, `CycleExact`, `TransferTraceEquivalent`, `TransactionEquivalent`, `ArchitecturallyEquivalent`, `Refinement` — parameterize legality. Each pass declares what it preserves and what it may change (retiming: preserves TransactionEquivalent, may change CycleExact, requires elastic-latency contract; encoding change: preserves ArchitecturalEquivalent). The optimizer's problem statement is contract-shaped: _find I refining architectural contract C subject to latency/throughput/area/clock constraints_ — choosing among flat/tree/pipelined/shared implementations that the equivalence facts (associativity, commutativity, purity, recorded on the architectural node) make legal. Proof-carrying levels per transformation: (A) trusted/verified local rewrites; (B) generated equivalence obligations discharged by SAT/SMT/LEC on a local miter; (C) contract-refinement proofs; (D) translation validation of the concrete result. Agent-proposed rewrites are _always_ level B or D (P-8) — the model proposes, the deterministic verifier admits. ### 5. Optimization under semantics: ending hardware's pre-compiler era **The state of practice.** RTL synthesis today operates the way C compilers did before aggressive optimization was trusted: locally, conservatively, and beneath the level where the interesting decisions live. This is not because the transformations are unknown — retiming, resource sharing, topology selection, encoding changes are all textbook — but because legality is unprovable from a netlist. By the time a design reaches the optimizer, an arbiter is muxes and comparators, a reduction is a comparator tree with its associativity discarded, and two mutually-exclusive datapaths are indistinguishable from two concurrent ones. The designer hand-optimizes topology the way programmers hand-unrolled loops in 1985, and the tool's role is to not break it. The evidence that meaning is destroyed early is structural, not anecdotal: every system that preserved any semantic fact through lowering immediately harvested optimizations from it. CIRCT's `comb-int-range-narrowing` pass reduces comb-op bitwidths from interval dataflow analysis, and its companion `comb-overflow-annotating` derives no-overflow facts the same way — the infrastructure literally re-derives, at the structural level, facts that `Index` and `Occupancy<0..=8>` state at the source, and the rediscovered version is strictly weaker: interval analysis is path-insensitive and cannot recover relational facts (`head != tail` when non-empty) that Tier-1/Tier-2 refinements carry natively. Filament's timeline types, checking all benchmarks in under a second, license resource sharing across time that netlist-level tools must either forgo or verify expensively after the fact — and the same types, merely _checking_ published generator output, caught incorrect latencies in 5 of 14 Aetherling-generated designs: even generators get timing wrong without types ([12](12-related-work.md)). **What the substrate changes.** Strata's optimizer receives, for every architectural node, the facts that make aggressive transformation legal: - **Algebraic laws.** A `Reduction{max}` node carries associativity and commutativity. Flat (15 comparators), balanced-tree (depth 4), pipelined-tree, and shared-serial implementations become one equivalence class; the surrounding contract (throughput ≥ 1/cycle, latency ≤ 2) prunes it; the physical model ranks the survivors. Today each of these is a manual rewrite plus a re-verification cycle. - **Exclusivity proofs.** A Tier-2 obligation (`is_add(op) ∧ is_addr_calc(op) = false`, [06 §1](06-refinements-and-evidence.md)) discharged once licenses sharing a single adder across conditional paths — the case Bluespec's conservative implicit-condition analysis famously cannot express, forcing users to restructure code around the scheduler ([12](12-related-work.md)). PDL demonstrated path-sensitive sharing checks via SMT are practical; we make their conclusions optimizer permissions. - **Range and encoding facts.** `Index`, `Occupancy<0..=8>`, and one-hot invariants ([02 §4](02-type-system-core.md)) license width narrowing, comparison elimination, unreachable-case pruning, and encoding selection with a recorded logical↔encoded bijection — inputs strictly stronger than anything recoverable by bit-level analysis. - **Scoped observability.** The named equivalence classes of §4 turn "may I retime this?" from a global assertion of faith into a local check: the contract declares what downstream consumers observe, so a pass that preserves `TransactionEquivalent` may freely break `CycleExact` behind an elastic interface. Every pass declares what it preserves; every nontrivial transformation is proof-carrying or translation-validated (§4, levels A–D). These four families are not exhaustive. Further judgment-derived facts license further transformations, each with prior art establishing the optimization and Strata supplying the sound fact ([12](12-related-work.md)): | Typed fact | Optimization licensed | Prior art for the optimization | | ---------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | --------------------------------------------------------------------------------------------------------------------------- | | Purity/idempotence on a node | Recompute-vs-fanout tradeoffs, safe register/logic duplication | software rematerialization; fanout-driven duplication | | Refinement-derived don't-cares (case unreachable) | Don't-care-driven SAT sweeping and resynthesis — stated, not rediscovered | ODC-based resynthesis (Zhu et al. DAC'06; ABC) | | Access-pattern refinements on `Memory` nodes | Banking/partitioning, port sharing, LSQ elimination where ordering is proven | Dahlia's affine memory types (PLDI'20); HLS partitioning | | Elastic/latency-insensitive protocol contracts | Retiming and stage insertion/removal that preserve `TransactionEquivalent` while breaking `CycleExact` | Leiserson–Saxe; Carloni LID; elastic circuits | | Typed enable/validity conditions | Clock-gating insertion, incl. sequential gating from "unobserved for k cycles" facts | commercial sequential clock gating (rediscovers these via model checking) | | Temporal stability + schedule/capture facts (`During`) | Generated category-specific multicycle/false-path candidate certificates, admitted only after exact post-synthesis path binding and precedence validation (D-086) | generation has prior art; semantic-plus-netlist certificate custody is the claim | | Initialization facts ("no read before first write") | Reset-less registers, sound X-optimization | the unsound status quo is documented (ARM's "Dangers of Living with an X") | | Flow-sensitive narrowing facts (harvested from match arms and guards, D-069) | Width narrowing, don't-cares, decoder pruning on dominated nodes — the checker's path-sensitive knowledge, free | CIRCT's interval analysis rediscovers only the path-insensitive fraction | | Comptime-computed value sets (decode tables are comptime data, D-022/D-069) | Reachable-value sets per field, stamped `StaticallyDerived` — don't-cares for SAT sweeping, decoder pruning, encoding selection, ledger-linked by the D-036 table hash | — | | Likelihood facts, `Estimated` or `Measured` (D-071) | Asymmetric _cost_ choices: zero-latency arm assignment on shared units, mux-tree defaults, arbitration priority defaults, `Variant` selection (D-035), gating aggressiveness, rare-path stage placement — never legality | software PGO; stronger here because D-052 stable node identity keeps profiles attached across reformats and re-elaborations | **Narrowing is harvested, not dropped (D-069).** Inside a match arm or past a guard, the typechecker already knows `opcode ∈ {Load, Store}` or `count < DEPTH`; those facts are written to the ledger on the nodes they dominate rather than discarded at the end of checking. User assertions (`narrow!(p)`) are _claims, never trusted_: they route through the normal discharge machinery ([06 §1](06-refinements-and-evidence.md)) and are usable by passes only at their earned evidence level. **Optimization profiles are objective vectors, not semantics (D-070).** `small`/`fast`/`low-power` are weightings on the already-contract-shaped search above — one semantics, one legality oracle, different rankings. Attachment is _regional_ via `ResourceCtx` (D-041): a cold config block inside a hot core inherits `minimize(area)` while the issue path carries `maximize(frequency)`; the chosen profile per region is a ledger fact. **`safe` is explicitly not a profile**: safety is judgments plus evidence gates, and no profile may strengthen or weaken either — an "-O0 is safer" culture is the failure mode this rule exists to prevent. The legitimate fourth axis is _hardening/debuggability_ (materialized generation tags, retained reset trees, debug-identity-preserving encodings), which rides the existing proof-only→production-encoded spectrum ([02 §5](02-type-system-core.md)). **Hardware PGO falls out of existing machinery (D-071).** Workload runs on the [FPGA loop](10-fpga-loop.md) produce per-branch and occupancy counters; those land as `Measured` ledger facts; the contract-shaped search re-runs with the new cost inputs. Observable semantics stay protected by the equivalence-class checks — likelihood licenses cost choices, never legality. One caution logged where it belongs: hint-driven timing asymmetry is a side-channel generator by construction, which interacts with the deferred information-flow story ([05 §6](05-speculation-authority-effects.md)) — a design-group lint flags it near labeled secrets ([14 §14](14-toolchain.md)). **The pragma confession.** Commercial tools already accept designer-asserted semantic facts — as unchecked strings. Every one is a known soundness hole with a typed replacement: `full_case`/`parallel_case` (the classic sim/synth-mismatch pair, Cummings SNUG'99) become typed exhaustiveness and a discharged Tier-2 exclusivity obligation; `ram_style` becomes the `Memory` node's typed read-during-write semantics plus evidence-ranked encoding selection; retiming attributes become scoped observability (legal exactly where an elastic contract makes `CycleExact` unobservable); `fsm_encoding=safe` becomes reachability refinements with the recovery assumption visible in the unsafe surface; `dont_touch` — which exists to defend hand structure against unsound-by-ignorance optimization — is mostly obsoleted by proof-carrying passes plus provenance. Every one of these attributes is the industry confessing that synthesis needs semantic facts it cannot recover, and accepting them without proof. Strata's contribution is not new facts but sound custody of the ones designers already assert. The optimizer's problem statement becomes contract-shaped: _find an implementation refining architectural contract C subject to latency/throughput/area/clock constraints_ — a search problem with a deterministic legality oracle rather than a pass pipeline with folklore ordering. This is not speculative: equality saturation over word-level RTL is already industrial — ROVER (Intel/Imperial, TCAD 2024) achieves up to 63% area reduction on production datapath blocks using bitwidth-dependent rewrite rules, emitting its rewrite sequence as a chain of small LEC-checkable steps (exactly our level-B/D certificates), and SEER (ASPLOS 2024) runs e-graph superoptimization over MLIR-hosted IR. What none of them has — and where Strata's equivalence classes become e-classes with something new to say — is rules guarded by _weaker observational equivalences_ (`TransactionEquivalent` behind elastic interfaces) and by discharged Tier-2 obligations, rather than bit-exact equivalence plus width side-conditions ([12](12-related-work.md)). **Probe-validated, with an infrastructure verdict (2026-07-17, `probes/eclass-rewrite/`, SUPPORTS-SETTLED).** The delta works end-to-end in an egg prototype: rules declaring preserved equivalence classes, applicability gated on region-inherited bounds, obligation-guarded sharing (same graph + one discharged fact = different optimum), cycle-exact observers blocking rewrites at accepted cost, mixed-region extraction composing in one e-graph, and rewrite-chain certificates whose claim is the meet of per-step classes — ROVER's certificate plus our delta, essentially free. But stock egg fights region scoping on three structural fronts: hash-consing is _anti-regional_ (identical subterms under different bounds share one e-class and must take the strictest bound, costing the permissive region its legal rewrite), bounds are inherited attributes while egg's analyses are bottom-up-only, and a natural self-referential retiming rule sent the extractor into a non-terminating fixpoint. Verdict for the north star: build the eq-sat engine with the equivalence bound in e-class identity (or egglog with the bound as a relation column) — a conditions-on-egg retrofit is the wrong architecture. **Why this compounds with agents.** A legality oracle is exactly the interface that makes agent-proposed optimization admissible ([09 §2](09-agent-system.md)): the model proposes a rewrite with a structured claim (what's preserved, what's invalidated, what validation is required); translation validation or a local equivalence check admits or rejects it (P-8). This is how decades of accumulated heuristic development — the gap between `cc` and `-O3` — can be compressed: the search is cheap to propose and safe to accept, so it can run continuously against the [experiment database](09-agent-system.md)'s measured results. **The honest boundary.** Hardware cost is spatial and physical. Placement, congestion, and fanout are `Measured` evidence, never derived facts (P-7, [10](10-fpga-loop.md)) — so the ceiling is not "the compiler perfectly optimizes" but "the compiler explores a provably-legal space orders of magnitude larger than today's, and physical feedback ranks the survivors." That is precisely the division of labor that made software compilers trustworthy: semantics decide _may_, measurement decides _should_. ### 6. Incremental summaries A compiled component exports: interface types; effect/requirement rows; protocol types; active contract-family schemas; assumptions and their owners; guarantees with evidence and expiry; temporal relations and resource schedules; validity/invalidation behavior; wait-for and fairness summaries where declared; partial memory-event relations plus completeness; observer projections/security obligations; power/reconfiguration lifecycle and region ABI where declared; unsafe/authority surface; first-class stable obligations; artifact dependency hashes and target/tool pins; implementation/config hashes; cost estimates; and explicit uncovered residue. Recompilation triggers only on relevant changes; composition checks guarantees against owned assumptions, protocol refinement, interval/resource compatibility, progress ownership, relation completeness, lifecycle compatibility, evidence validity, and residue—without reopening bodies. The summary format is sparse and versioned. Optional families are absent, not filled with `unknown`; `unknown` is reserved for a declared family whose proof outcome is an obligation. Assurance graphs are derived from these summaries and primary artifacts, but never appear as evidence inputs to them (D-090). The architecture rule, stated in rust-analyzer's words: **editing inside a component body never invalidates global derived data** — only summary changes propagate. We deliberately choose coarse per-component summaries over fine-grained query memoization (matklad's retrospective on query-based compilers: coarse + summaries is "simpler, faster, and simpler to make faster"); the summary firewall is the invariant, not a query graph. Three ecosystem consequences fall out nearly free (D-042, D-043): - **Mechanically checked semver.** A summary captures interface, protocol, timing contract, guarantees, and unsafe surface — so compatibility is _decidable and total_: a weakened guarantee, widened assumption, or slower schedule is mechanically a major version. Software ecosystems bolt semver-checking onto API surface only; no one can check timing compatibility. Strata can, because timing is in the summary. - **Editions.** Per-component language-edition pinning with summary-level composition: summaries are edition-neutral, so decades-old frozen IP composes with current code without AST-level interop. Hardware IP lifetimes demand this from day one. - **Eager library boundaries (the anti-Zig rule).** Zig checks only referenced decls, and its own team flags the consequence: published libraries ship broken never-instantiated paths. Fatal for hardware generators, whose config spaces are huge and whose customers instantiate corners the author never did. Strata: lazy elaboration is fine for _user_ builds, but a _published_ component requires definition-checked generator bounds ([02 §8](02-type-system-core.md)) plus a declared **config coverage set** — the instantiations actually elaborated and checked, recorded in the summary as `Tested` evidence ([06 §3](06-refinements-and-evidence.md)). ### 7. Comptime evaluator Typed, deterministic, effect-declared, budgeted (D-021, P-6). Reports per-module elaboration cost (calls, generated components/nodes, peak memory, dominant generator). Emits canonical architectural nodes only (D-022) — the evaluator has no API for constructing raw structural primitives outside an explicit `lower { }` boundary. **Comptime is staged partial evaluation whose residual is the Architectural IR — not the Structural IR.** This is the precise statement of what D-022 buys, and it is where every prior generator system leaks: Lava, Bluespec elaboration, and Chisel all residualize _primitive_ graphs. Chisel forces concrete at its stage boundary exactly what our optimizer needs symbolic: topology (a `reduceTree` call _is_ a tree; the flat and serial variants are different source), schedules (pipelining is manual register insertion), encodings, and parameter identity (a Scala `Int` leaves no trace of which knob produced which structure — Chisel's Diplomacy exists because one-shot elaboration can't defer inter-module parameters; in Strata that's just two deterministic elaboration rounds over exported summaries). The phase modalities of [02 §2](02-type-system-core.md) are the staging annotations: `static` is stage 0, `reflect` is cross-stage persistence. Comptime makes concrete anything whose variation changes the _contract_ (counts, port lists, protocol choices); it keeps symbolic anything the optimizer may legally vary within an equivalence class. **Design-space parameters (D-035).** Building on Spatial's behavior-invariant `DesignParam` (which drove practical multi-objective DSE), a generator can declare knobs the optimizer owns: ``` comptime param STAGES: Nat in 1..=6 // optimizer-owned knob comptime fixed DEPTH: Nat = config.queue_depth // user-owned config, not sweepable objective { throughput >= 1/cycle; latency <= 4; minimize area } ``` A `param` carries a **contract-invariance obligation**: the component's exported summary must be identical (or refining, per §4's equivalences) at every point in its range — Spatial's promise made a typing judgment. A knob that changes the contract is a type error: it must become `fixed`. Where topology depends on a param, comptime emits a `Variant` region (a small family of canonical-node graphs indexed by the param — never soup), and the chosen point is a ledger fact with evidence (`chosen STAGES=3, Measured, experiment-id`), so P-2/P-3 survive the sweep. This inverts the HLS-pragma-DSE cost structure: legality is checked by a deterministic oracle _before_ any synthesis run is spent, and the sweep itself is driven by the [FPGA loop](10-fpga-loop.md) and [agents](09-agent-system.md) under P-8. **Memoized instance identity (D-045).** Comptime calls are memoized on `(generator identity, argument values, config hash)` — sound _by construction_ because of D-021's determinism (Rust cannot cache proc-macro expansion precisely because macros are nondeterministic and effectful; we bought this for free). This is Chisel's hard-won `Definition`/`Instance` discipline (added after years of fragile post-hoc dedup) baked into the evaluator: one definition per parameter set, instances recorded in the ledger as `instance-of D`, structural dedup at the IR only as backstop. `comptime for` emits `Replicate{N, body}` with one body and a symbolic count, so the _sharing_ decision stays with the optimizer (P-5) rather than being forced by elaboration. **Resource contexts (D-041).** Generators receive an explicit `ResourceCtx` value — clock/reset domain, memory-port pool, area budget, optionally a floorplan region — and everything they build draws from it. This is Zig's explicit-allocator idea translated: the capability to consume resources is a value you pass, so no library can hide its resource appetite (P-2 made structural). An instrumented ctx in tests reports per-generator budget violations (the leak-detector analog); a failing ctx tests generator behavior at resource exhaustion; and the ctx is the natural hook for placement constraints without new type machinery. **Budget mechanics (D-044).** Zig's `@setEvalBranchQuota` catalog of failures dictates the design: budgets are _declarative_ per-declaration attributes (never imperatively raised mid-evaluation), _scoped and compositional_ (a generator's budget bounds its callees), _attributed_ (exhaustion diagnostics name the dominant call path and its consumption profile, per P-9), and _readable_ by the budgeted code. **Exhaustive evaluation as proof (D-036).** Because the evaluator is deterministic, typed, budgeted, and already in the trusted base, exhaustive concrete evaluation of a pure predicate over a small finite domain _is a proof_ — see [06 §1](06-refinements-and-evidence.md) for the discharge form and its evidence tag. ## North star - In-tree CIRCT ingestion dialect once the architectural IR is stable and there's community pull. - circt-bmc as primary BMC once counterexample extraction and multi-clock land. - Mechanized core calculus for the committed judgment set ([OP-7](open-problems.md)) with the IR verifier generated from it. - Equality-saturation-based exploration over architectural nodes — semantics probe-validated (`probes/eclass-rewrite/`); requires custom e-graph infrastructure with the equivalence bound in e-class identity rather than stock egg (hash-consing is anti-regional). - Observer projections in the Architectural-IR interpreter, with implementation equivalence kept distinct from two-run noninterference (D-085, `probes/observer-flow/`). - Partial memory-event summaries and model refinement as a dedicated architectural relation judgment, not protocol metadata (D-084, `probes/memory-consistency/`). - Approximation-aware passes consuming representation semantics plus explicit error-budget certificates (D-088, `probes/numeric-error/`), and DFT insertion preserving functional plus security observers under authority premises (D-089, `probes/dft-debug/`). ## Open problems touching this doc [OP-3](open-problems.md), [OP-6](open-problems.md), [OP-7](open-problems.md). ````