The physical-evidence layer: how implementation reality feeds back into the semantic substrate. Principles in force: P-2 (cost visible), P-7 (physical facts are evidence, never types), D-005 (FPGA-first, ASIC-clean).

Committed design

1. Pre-synthesis estimation

Components carry structure reports (comparator counts, reduction depth, register counts, estimated LUTs/delay) computed from architectural nodes before any vendor tool runs — these are Estimated<Model> evidence, explicitly weaker than Measured. Budgets (#[budget(max_latency, max_luts, max_fanout)]) check against estimates early and against measurements late. Candidate open estimation backend: circt-synth's AIG + longest-path timing analysis over our emitted structural IR (07 §2) — giving a vendor-independent delay/area signal cheap enough to run in CI.

2. Structured synthesis feedback

Vendor tool output is parsed into structured diagnostics anchored to provenance: critical path reported as a chain of source-level structures (via the ledger), with candidate improvements stated in architectural vocabulary (hierarchical priority encoder, added pipeline stage, split allocation groups, fanout reduction) — consumable by the synthesis agent. Objectives/constraints (#[optimize(objectives, constraints)]) define the optimizer's contract-shaped problem (07 §4).

3. Hardware-in-the-loop experiments

experiment declarations (comptime-generated variant sweeps × workloads × measurements) drive: automated bitstream builds, deployment, execution, trace/counter capture, fault injection, randomized I/O timing, and simulation-vs-hardware comparison. Every run is reproducible (P-6 determinism extends to experiment definitions) and lands in the experiment database as Measured<Target, ToolVersion> evidence attached to the design hash.

Captured per-branch and occupancy counters double as the hardware-PGO source (D-071): they land as Measured<Workload> likelihood facts on stable node identities, and the contract-shaped search re-runs against them (07 §5) — profile-guided cost ranking with the profile attached to the design by node identity, not by fragile source location.

4. Evidence discipline

Frequency, area, power, and fanout claims in any summary or agent report must cite their evidence tag. A design promoted through a release gate needs measurement on the gate's named target; simulation IPC and estimated frequency never silently substitute (P-7). Divergence between simulation and FPGA measurement is itself a first-class result (it indicts either the model or the design) and is retained in the experiment database.

Physical and lifecycle evidence is invalidation-sensitive. Retiming, cloning, clock/mode changes, DVFS points, power intent, scan insertion, reconfiguration, netlist revision, vendor-tool version, target, or seed invalidate exactly the certificates whose dependency manifests name those facts. Reuse requires re-binding and re-checking, not filename equality.

5. Physical information: four channels in, one door closed (D-075)

Physical information genuinely enters the language through four channels — as evidence (Measured<842MHz, vu19p, tool> ledger facts ranking candidates and gating releases, D-017), as coeffect obligations (placement_distance(rf) <= D, fanout/depth budgets — stated in source, discharged at implementation), as search inputs (D-071 Measured<Workload> counters on stable node identities re-running the contract-shaped search), and as budgets vs estimates (P-2, circt-synth-class early signals). The single closed door: physical facts never participate in type equality or judgment soundness. The precise form (verification-hardened, 2026-07-17): post-P&R timing is a function of (design, context, target, tool, seed), not of the design term — any judgment sound for the term alone must either quantify over all contexts, yielding bounds too loose to bear load, or freeze the context, at which point it is a measured fact about an artifact, which is exactly what the evidence lattice stores. And composition offers no frame rule: adding neighbors invalidates a physical-timing judgment on an untouched subterm (congestion, routing), so tight bounds aren't compositional and compositional bounds aren't tight. The boundary case that proves the rule: RapidWright-style pre-implemented modules — placed-and-locked macros with carried timing — are supported as Measured evidence on a reusable artifact, never as a type. (Cycle-level timing, by contrast, is a function of the design and is typed — 03; the door closes exactly at the physical layer.)

North star

ASIC flow adapters: same evidence schema, Measured<Process, ToolVersion> from signoff tools; CDC/timing signoff reports imported as evidence artifacts.
Fleet-scale HIL: many boards, scheduled like CI, with the corpus manager targeting hardware-only behaviors (I/O timing races) simulation can't reach.
Learned cost models trained on the experiment database's estimate-vs-measured pairs, tightening §1 estimates per target. Industrial precedent exists and is acknowledged rather than ignored: Synopsys DSO.ai and Cadence Cerebrus run learned search over opaque flows (reported ~20% PPA), Google's RL placement (AlphaChip) the same for macros — the delta is that Strata's candidates pass deterministic legality checks under declared contracts before ranking; backend and physical claims still require downstream evidence (D-076).
Netlist-custody adapters that resolve intended false/multicycle/generated-clock constraints to exact nonempty post-synthesis path manifests and check lineage, precedence, setup/hold pairing, mode, and clocks before admission. Source semantics creates a candidate certificate; only the bound artifact earns evidence (D-086).
Power/DFT/reconfiguration adapters: import IEEE 1801-class power intent and vendor reports as external artifacts; validate isolation/retention/test/reconfiguration contracts against the emitted and implemented design; preserve the boundary between digital guarantees and characterized electrical assumptions.
Fault-injection HIL across transient/permanent campaigns, with injected model, physical mechanism, coverage, target, and recovery observation attached to each result. FPGA fault injection validates declared campaigns, not radiation/environmental equivalence without separate evidence.
Release-full spatial optimization (D-076) — composes from existing machinery, no new semantics: on vendor flows Strata drives the search around the placer (regions, constraints, restructuring per D-041 + the Exit-2 bundle, 07 §2b) — the prior art is direct (RapidLayout's evolutionary placement DSE via RapidWright beat manual Vivado constraints 5–6×; AutoBridge's floorplan-coupled pipelining took 43 designs from 147→297 MHz average), with direct-placement ownership scoped honestly to AMD/Xilinx (RapidWright has no Intel-side equivalent) and the open RTLIL→nextpnr flow as where deeper ownership arrives. P-7 makes it structurally a measured search loop, never a closed-form solve: legality from the semantic substrate, ranking from this loop, cost models learned from the experiment DB. And because placement is NP-hard, "release-full" is an objective profile (D-070) plus a compute budget — under a keep-the-best policy over contract-legal candidates against a pinned measurement protocol, additional compute is monotone in best-measured QoR; it does not strengthen the contracts or physical evidence.

Open problems touching this doc

None owned. Feeds the evidence lattice; consumes ledger provenance (OP-6 erosion would degrade §2's source-anchored feedback — a concrete consumer to test against).