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

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) — 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.
• 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). 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).

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

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) 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). PDL demonstrated path-sensitive sharing checks via SMT are practical; we make their conclusions optimizer permissions.
• Range and encoding facts. Index<QUEUE_SIZE>, Occupancy<0..=8>, and one-hot invariants (02 §4) 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):

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

Hardware PGO falls out of existing machinery (D-071). Workload runs on the FPGA loop produce per-branch and occupancy counters; those land as Measured<Workload> 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) — a design-group lint flags it near labeled secrets (14 §14).

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

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): 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'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) — 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) plus a declared config coverage set — the instantiations actually elaborated and checked, recorded in the summary as Tested evidence (06 §3).

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

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 and agents 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 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) 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, OP-6, OP-7.