# proposal/12-related-work.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/04eb9cf6eeb9719c7af75415695bb35b50afff34/proposal/12-related-work.md)

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

Visibility: public

Requested revision: 04eb9cf6eeb9719c7af75415695bb35b50afff34

Requested commit: 04eb9cf6eeb9719c7af75415695bb35b50afff34

Commit: 04eb9cf6eeb9719c7af75415695bb35b50afff34

Blob: 75bf816779ab01bf1838960d88418517c2e12c4c

Size: 22117 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/04eb9cf6eeb9719c7af75415695bb35b50afff34/proposal/12-related-work.md?format=markdown)

```
# Related Work

What we take, and what we reject, from each line of prior art. Grounded in the 2026-07-17 research briefs, the 2026-07-21 systems-safety probe wave, and primary sources cited inline. This doc doubles as the extraction source for a whitepaper's related-work and positioning sections (D-001).

## Hardware languages with typed time

**Filament** (Nigam, Azevedo de Amorim, Sampson — _Modular Hardware Design with Timeline Types_, PLDI 2023). Event-parameterized signatures, availability intervals, delay = initiation interval; checking collapses to linear inequalities, all benchmarks under 1 s; caught real latency bugs in a published generator (5/14 Aetherling designs). **Take:** the whole static-interval capability model ([03 §3](03-time-and-resources.md)); the lesson that interval checking can be solver-free when delays are static. **Reject/extend:** path-insensitive sharing (worst-case spans on one event) — we add Tier-2 disjointness obligations; no dynamic latency, no multi-clock, no speculation (all confirmed limits).

**Lilac / parameterized Filament** (arXiv:2401.02570): parametric latency-abstract interfaces, Z3-discharged obligations — the template for our comptime-parametric intervals.

**Anvil** (Yu et al., ASPLOS 2026): abstract time points with dynamic durations, lifetimes/loans, event-graph checking; typed a CVA6 TLB replacement with <1% overhead — but ~2× power vs Filament on a static pipelined ALU. **Take:** the north-star direction for dynamic latency ([OP-8](open-problems.md)) and the evidence that it isn't free. **Reject for committed scope:** dynamic intervals in the checker; we route dynamic latency through protocols.

**HazardFlow** (Jang et al., PLDI 2024): stall/bypass/discard-and-restart as _hazard interfaces_ generalizing valid-ready; standing challenge to per-module interval typing's modularity. Tracked in [03 north star](03-time-and-resources.md) and [04 north star](04-protocols-and-streams.md).

## Rule-based and pipeline languages

**Bluespec/BSV**: guarded atomic rules, ORAAT semantics, compiler-derived schedules. **The central negative lesson (D-031):** cycle behavior as an opaque compiler artifact makes users code _at the compiler_; conflict resolution degrades to module-local, stringly `descending_urgency` pragmas; conservative implicit conditions block rules on resources their taken path never touches. Strata's answers: explicit schedule witnesses, first-class cross-module arbitration, path-sensitive Tier-2 obligations.

**Kôika** (Bourgeat et al., PLDI 2020): user-written schedules, deterministic cycle-accurate semantics, Coq-verified compiler. **Take:** schedules belong to the user/witness, not the analysis; verified lowering as a north-star bar. **Note:** shipped without a module system — a warning about metatheory cost crowding out engineering.

**PDL** (Zagieboylo et al., PLDI 2022): one-instruction-at-a-time semantics; typed locks with reserve/block/release; **speculation as typed spawn/verify/kill with statuses** — the proof that speculation typestate is checkable ([05 §2](05-speculation-authority-effects.md)). Its boundaries (trusted lock RTL, branch-shaped speculation only, informal metatheory) define exactly where our committed design must be honest too. **SpecVerilog** (CCS 2023) is the reference for the deferred information-flow story.

**Cement2** ([Xiao et al., 2025](https://arxiv.org/abs/2511.15073)): temporal hardware transactions in a Rust-embedded HDL, including inter-cycle relationships and multi-cycle rules across latency-sensitive and latency-insensitive regions. **Take:** direct evidence that transactional semantics can remain cycle-aware and produce competitive FPGA implementations. **Difference:** Cement2 targets productive temporal construction and synthesis; Strata additionally needs separate capability/resource judgments, contract-generated verification, evidence custody, fault/lifecycle schemas, and release assurance.

## Type-theory ingredients

**QTT / Idris 2** (Brady, ECOOP 2021): `{0,1,ω}` grades practical at scale; the real payoff is _checked erasure_; no multiplicity polymorphism, and users trip on erased-argument matching. Directly sets D-024 and the phase-modality erasure semantics ([02 §2–3](02-type-system-core.md)). **Granule** (Orchard et al., ICFP 2019): menu-of-semirings works, user-defined algebras are a paper series — sets the north-star boundary. **Dependent multiplicities** (GrTT ESOP 2021; ICFP 2023/2025 lines): no production implementation — deferred (D-023).

**Rast** (Das & Pfenning, FSCD 2020; CONCUR 2020): session types + Presburger refinements; equality undecidable, practical semi-algorithm that terminates with hints. Sets D-027 wholesale ([04 §2](04-protocols-and-streams.md)). Context-free session subtyping undecidability (CONCUR 2023) reinforces the catalog-first stance (D-015).

**Guarded type theory** (Nakano; Clocked Cubical Type Theory; Guarded Cubical Agda): proof-assistant-only today. **Clash** is the practice baseline: domain-indexed signals work well, but causality is _untyped_ — register-free feedback typechecks and hangs. Our single-clock `later` (D-029) is scoped to beat exactly that, nothing more.

**LiquidHaskell / Flux** (PLDI 2023): the engineering canon for SMT-backed refinements — QF fragments + liquid inference + boundary annotations; PLE opt-in only; ownership keeps refinements pure; plugin-grade incrementality decides adoption. Sets D-025 ([06 §1](06-refinements-and-evidence.md)).

**Typestate** (Plaid, Obsidian, Rust embedded HALs): dies as a language primitive under annotation burden (Plaid dead; Obsidian's user studies showed real learning cost); thrives as a zero-cost library pattern over move semantics. Sets D-026 ([02 §6](02-type-system-core.md)).

**Iris** (resource algebras, authoritative state): the semantic model we point at for authority/fragments ([05 north star](05-speculation-authority-effects.md)) — never user-facing.

## Compiler infrastructure

**CIRCT** (LLVM incubator; firtool releases ~weekly, 2026): hw/comb/seq/sv stable and active; arc (arcilator) and moore very active; **pipeline/ssp stale, handshake abandoned in-tree** (Dynamatic vendored it out — the churn-cost precedent); circt-bmc/lec real but early, counterexample extraction unlanded; debug/HGLDD provenance Chisel/VCS-shaped with UHDI in flight; no C++ API stability, textual MLIR + pinned releases is the durable contract. Sets D-032/D-033 wholesale ([07 §2](07-compiler-architecture.md)). **Calyx**, **FIRRTL**: the precedent that rich frontends own their ingestion IR.

## Architectural contracts, memory models, and information flow

**FAVA** ([Formal Hardware Verification for Architects](https://fava.stanford.edu/)) is the closest academic cluster to the systems-assurance expansion: its bottom-up tools synthesize verified microarchitectural execution paths, memory-consistency specifications, coherence specifications, and leakage contracts from designs, with deployment on substantial CPU modules. RTL2MµPATH and SynthLC are especially close to Strata's architectural-event and observer ambitions. **Take:** automatically generated, architecture-facing formal contracts can scale beyond toy pipelines; relational leakage contracts and memory relations deserve dedicated models rather than protocol assertions. **Difference:** FAVA verifies existing RTL from metadata. Strata proposes a source language and architectural IR whose typed intent, optimizer permissions, physical custody, fault/lifecycle contracts, and release assurance all feed the same summaries. FAVA is a strong nearest neighbor, not evidence that the integrated language architecture is already solved.

**PipeCheck/COATCheck/RealityCheck/PipeProof/TriCheck** establish microarchitectural happens-before graphs, translation-aware ordering, modular and all-program hardware MCM verification, and hardware/software/ISA compatibility. **herdtools7** ([project](https://github.com/herd/herdtools7)) is the executable-model/litmus baseline. **Take:** Strata memory contracts must export first-class architectural events and relations, explicitly state completeness, and bind to standard executable models rather than invent a private notion of RVWMO. **Difference:** Strata's claim is compositional custody from source summaries through RTL and release artifacts, not a stronger memory-model solver. Until mixed-size/per-byte, translation, coherence, DMA, and interrupt cases validate against a standard model, the result stays `obligation`.

**Hardware-Software Contracts for Secure Speculation** ([Guarnieri et al., 2020](https://arxiv.org/abs/2006.03841)), SpecVerilog, IODINE, UPEC, SynthLC, and leakage-contract work show that security must be stated against an observation model and often checked relationally. **Take:** named observer projections, two-run noninterference, and explicit declassification authority. **Reject:** a single linear `Secret < Public` label hierarchy as sufficient for cycle/cache/contention/debug/power leakage. Strata keeps implementation equivalence and noninterference as distinct facts; physical power leakage remains model/measurement evidence.

**Formalizing Memory Accesses and Interrupts** ([Achermann et al., 2017](https://arxiv.org/abs/1703.06571)) demonstrates why address spaces, translation paths, DMA, and interrupt topology require one system-level model. Capability architectures and IOMMU APIs provide adjacent authority mechanisms. **Take:** DMA consumes owner-minted, bounded mapping leases with opaque generations and issue-time authorization snapshots; process death, unmap, device reset, and IOMMU invalidation revoke authority through explicit lifecycle events. **Difference:** the proposal connects the same contract to RTL interfaces, driver bindings, IOMMU requirements, runtime monitors, and formal obligations; the small probe establishes the contract shape, not a verified OS/hypervisor stack.

## Optimization under semantics

**ROVER** (Coward, Drane, Constantinides — Intel/Imperial, TCAD 2024; ARITH'22 lineage): equality saturation over word-level datapath RTL with bitwidth-dependent rewrite rules; up to 63% area reduction on Intel production blocks; legality via per-rule verification plus a **rewrite-chain certificate** checkable step-by-step by industrial LEC — the existence proof for our level-B/D proof-carrying scheme at industrial scale ([07 §4–5](07-compiler-architecture.md)). **SEER** (ASPLOS 2024): e-graph superoptimization over MLIR-hosted IR, up to 38× perf within 1.4× area. **E-Syn** (DAC 2024): Boolean-level e-graphs with physical cost extraction. **ASPEN** (MLCAD 2025): LLM-_proposed_ e-graph rules, verifier-admitted — direct prior art for P-8. **Take:** e-classes with certificates are proven. **Our delta:** rules guarded by weaker observational equivalences (`TransactionEquivalent`) and discharged Tier-2 obligations — every existing system works at bit-exact + width side-conditions. **Dahlia** (Nigam et al., PLDI 2020): affine "predictable" types making memory-banking legality a type fact — the closest cousin to our fact-families table. **Cummings SNUG'99** (`full_case parallel_case`, "the evil twins"): the canonical documentation of the pragma soundness holes our typed facts replace. **Carloni's LID theory / elastic circuits / Murray & Betz FPGA'14:** the retiming-behind-elastic-interfaces legality story and its measured cost.

## Language engineering (Rust/Zig lessons)

Mined for mechanisms and failure modes, not features ([02 §4,8–10](02-type-system-core.md), [07 §6–7](07-compiler-architecture.md)): Rust's `generic_const_exprs` stall (type equality of unevaluated expressions — sets D-037's width-algebra closure); coherence/orphan tension (dissolved by named adapters, D-038); `?`-marked propagation (adopted as a canonical `Bypass/Poison` node); Drop's failures — safe leaking, unsolved async Drop — (sets D-039: linearity, not destructors); `// SAFETY:` comments as social-only enforcement (upgraded to machine-readable assumptions, [06 §5](06-refinements-and-evidence.md)); rust-analyzer's body-edit invariant and matklad's coarse-beats-query-graph retrospective (vindicates summary architecture); editions and mechanical semver (uniquely _total_ over summaries, D-043); MIR→Miri (sets D-046); clippy's machine-applicable lints. Zig: explicit allocators (→ `ResourceCtx`, D-041); result-location semantics' failure (sets D-040: no consumer-driven inference); lazy-analysis ecosystem hazard (sets D-042: eager library boundaries); `@setEvalBranchQuota` failure catalog (sets D-044); `anytype` blame ambiguity (sets D-038's hybrid bounds); comptime-assert-as-proof (feeds D-036). **Spatial** (PLDI 2018): behavior-invariant design parameters + HyperMapper DSE — the precedent D-035 turns into a typing judgment. **Chisel's Definition/Instance API and Diplomacy:** the monomorphization-dedup and parameter-negotiation problems solved post-hoc that D-045 and summary-round elaboration solve by construction.

## Physical flows and the vendor boundary

Added with the exit-boundary/physical decisions (D-073–D-076), all adversarially verified 2026-07-17. **RapidWright** (Lavin & Kaviani, FCCM 2018): open API for direct placement/routing on AMD/Xilinx — the existence proof for Exit-2-becomes-Exit-1, and its pre-implemented modules are the boundary case for D-075 (locked-placement timing as `Measured` evidence on an artifact, never a type). **RapidLayout** (FPL 2020/TRETS 2022): evolutionary placement DSE beating manual constraints 5–6× — the D-076 loop demonstrated. **AutoBridge/TAPA** (FPGA 2021 Best Paper): floorplan-coupled pipelining, 147→297 MHz over 43 designs — the restructure-and-constrain-around-the-placer result. **DSO.ai / Cerebrus / AlphaChip**: industrial learned flow-search (~20% PPA); Strata's learned model similarly ranks, while deterministic contract-legality checks precede ranking and backend/physical claims still require downstream evidence. **EQY / OneSpin EC-FPGA**: the Exit-3 reality — combinational LEC open and tractable for fenced regions; sequential EC (retiming, re-encoding) commercial-only, which is why the bake↔delegate dial determines the achievable equivalence class. **Blue Pearl**: prior art for _generating_ SDC exceptions; D-086 and `probes/physical-constraints/` establish the missing custody rule — source semantics constructs a candidate, while exact post-synthesis path binding and precedence validation admit it. **Yosys RTLIL / nextpnr**: pinned-version interchange (RTLIL has no cross-version stability guarantee) and the JSON-netlist ingestion path. **Sutherland SNUG 2013 / Cummings**: the sim/synth-divergence literature behind "SV expresses don't-cares only unsoundly." **Rust's `&mut`→noalias**: the software precedent for safety-facts-as-optimizer-permissions — proved for one fact, with a multi-year LLVM-miscompilation saga that is evidence _for_ per-transformation certificates; Strata generalizes the pattern across the substrate with evidence-gated permissions, which no surveyed system has.

## Verification and testing

**Cascade** (USENIX Security 2024): valid-by-construction entangled programs, 28–97× coverage, 37 bugs/28 CVEs, built-in reduction — the generation bar to meet ([08 §3](08-verification-platform.md)). **TestRIG/QuickCheckVEngine** (Cambridge): QuickCheck + RVFI-DII lockstep with real shrinking — the differential-PBT existence proof; Haskell/ISA-bound, which is our generalization opening. **Hypothesis integrated shrinking**: the shrinker architecture (D-028). **HyPFuzz** (USENIX Security 2023) / **FormalFuzzer**: formal-witness-as-seed works, closed-tool-bound — the open pipeline is unbuilt ([08 §5](08-verification-platform.md)). **RFUZZ / DifuzzRTL / TheHuzz**: the coverage-proxy caution. **riscv-dv, RVFI, RVVI, riscof, riscv-formal**: the differential/conformance baseline we bind to rather than reinvent. **MCY / Certitude, VERT**: mutation scoring precedent ([08 §6](08-verification-platform.md)). **cocotb (+Hypothesis folklore), chiseltest (unmaintained), ChiselVerify, SpinalSim**: the gap analysis — no maintained typed-PBT-with-shrinking framework exists for hardware.

## Faults, power, DFT, physical constraints, and assurance

Fault simulation, ECC/parity, lockstep, TMR, scrubbing, replay, ISO 26262-oriented safety flows, and commercial fault-campaign tools already cover individual resilience mechanisms deeply. Strata does not replace their engines. Its proposed contribution is a source-level `Detect/Correct/Contain/Recover` contract whose values and authority become stale at explicit health invalidation, from which monitors, mutants, campaign manifests, and residue are generated. The key probe result is separation: fault occurrence, detection, correction, containment, and invalidation are not interchangeable evidence events.

**IEEE 1801 UPF** ([IEEE 1801-2024](https://standards.ieee.org/ieee/1801/7466/)) is the power-intent baseline for domains, states, isolation, retention, and implementation/verification refinement. FPGA partial-reconfiguration work treats fabric area as a runtime resource. **Take:** interoperability with established electrical/implementation intent and vendor reports. **Difference:** Strata's source contract is a digital lifecycle and authority protocol—`Off → Isolated → Retained → Powering → Resetting → Active`—with quiescence, validity epochs, ABI refinement, and reconfiguration authenticity. It does not claim to prove electrical power behavior; that enters as characterized external evidence.

Commercial DFT and debug flows already insert scan, MBIST, test access, and trace at industrial scale. Strata's claim is not better insertion: scan/JTAG/trace/fault injection/ECO become scoped authority effects, and insertion must preserve both functional behavior and declared security observers under named lifecycle premises. Likewise, formal verification of asynchronous interfaces ([Schmaltz, 2011](https://arxiv.org/abs/1103.2246)) supports the boundary used here: prove the digital protocol assuming a characterized synchronizer/interface contract; record physical characterization separately.

Timing-constraint generation has prior art, but SDC/XDC selectors and precedence confer authority over post-synthesis objects. D-086's delta is custody: source timing/stability facts create only a candidate; exact nonempty intended-vs-actual path binding, lineage, setup/hold pairing, mode, and clock checks admit the implemented certificate. Retiming, cloning, or netlist/tool/mode changes invalidate it.

**OMG SACM** ([Structured Assurance Case Metamodel 2.3](https://www.omg.org/spec/SACM/2.3/About-SACM)) standardizes auditable claims, argument, and evidence exchange. Goal-structured assurance practice and safety standards already require explicit claims and supporting evidence. **Take:** interoperable hazard→claim→assumption→artifact structure. **Difference:** Strata derives that graph from semantic summaries and artifact manifests, tracks hashes/expiry/tool/target pins and release diffs, and makes self-citation invalid. The assurance case never becomes evidence and never upgrades the artifacts it summarizes.

## Commercial EDA suites

Synopsys, Cadence, and Siemens EDA collectively offer industrial-strength formal/property checking, lint/CDC/RDC, low-power verification, equivalence, timing/signoff, DFT/test, fault/safety, simulation, emulation, and physical implementation. For example, Synopsys' own [static/formal portfolio](https://www.synopsys.com/verification/static-and-formal-verification.html) spans VC Formal, VC SpyGlass, VC LP, and timing-constraint management; Cadence Jasper/Xcelium/Modus and Siemens Questa/Tessent/Calibre cover corresponding clusters. These tools are stronger and more mature than Strata could initially be in their specialties.

The comparison is architectural, not solver-by-solver. Commercial flows consume RTL, SVA, UPF, SDC, waiver databases, test plans, and tool-specific reports maintained across multiple systems. Strata proposes to generate and bind those artifacts from one typed semantic source, retain validity and assumption custody through lowering, and compose their results into release-visible guarantees and residue. Success means making specialist tools better-grounded evidence producers—not replacing them.

## LLM/agentic hardware design

**VerilogEval / RTLLM / OpenLLM-RTL / TuRTLe / CVDP**: the benchmark landscape. Failure-mode studies (2026): dominant failures are late syntax/synthesizability/reference errors — eliminated by construction in a typed substrate; the residual is semantic hallucination (HaVen 2025), answered by generated verification ([09](09-agent-system.md)). **ChipNeMo** (assistant, not autonomous design), **AutoChip** (compiler-feedback iteration), validation-first multi-agent work (2026): the field converging on Strata's claim 5 — none of them own the language layer, which is the differentiation.

## Positioning in one paragraph

Chisel/SpinalHDL give metaprogrammed structure; Bluespec/Kôika give atomic semantics; Filament/Anvil give typed time/resources; Cement2 gives temporal transactions; HazardFlow/PDL capture pipeline hazards, resources, and speculation; Calyx/Dahlia expose control/resource structure; CIRCT supplies broad IR infrastructure; FAVA and the Check suite provide the nearest architectural-contract verification cluster; commercial EDA suites provide mature specialist analyses and signoff. Strata should not claim superiority in any one of those domains. Its defensible claim is the integration boundary: **no current system appears to make typed design intent, generated verification, transformation permissions, physical certificate custody, fault/lifecycle semantics, and release assurance consumers of one shared semantic model.** The probes show a plausible thin waist and expose its limits; the roadmap's integrated targets must show that the composition remains usable and sound at scale.

```