# proposal/00-vision.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7/proposal/00-vision.md)

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

Visibility: public

Requested revision: 3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7

Requested commit: 3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7

Commit: 3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7

Blob: 070a28a526ff9d739bc6add873a9b36d5d868248

Size: 11838 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7/proposal/00-vision.md?format=markdown)

````
# Vision

## Thesis

Language models can already generate plausible RTL. What they cannot do is engineer hardware, because they operate inside semantically weak environments: ambiguous specifications, token-level source manipulation, errors discovered late through simulation, and feedback that arrives as noise. **Strata** is a bet that the binding constraint on agentic hardware design is not model capability but substrate quality.

Strata is therefore three things at once:

1. **A hardware language** in which a large class of hardware failures — truncation, clock- and reset-domain violations, resource conflicts, protocol misuse, speculative leaks into irreversible effects, uninitialized state — become compile-time type errors with machine-actionable diagnostics.
2. **A verification and engineering platform** in which interface declarations generate their own verification infrastructure, every claim carries explicit evidence, and agents operate over typed architectural objects — with compilers, simulators, solvers, synthesis tools, and FPGA measurements as their ground truth.
3. **A systems-assurance substrate** in which failures of the environment and assumptions—faults, revoked mappings, lost progress, illegal memory observations, power transitions, reconfiguration, debug/test authority, and physical exceptions—are explicit contracts with owned assumptions, generated campaigns, validity conditions, and release-visible residue.

The unifying idea, inherited from `refine-1.md` and giving the project its working name: hardware facts should remain **alive** across the whole flow —

```
source intent
  → typed architectural fact
  → optional system contract
  → optimizer permission
  → proof obligation
  → structural implementation
  → physical evidence
  → release assurance
```

— instead of collapsing into bits and wires at elaboration. Once that chain is preserved, the type checker, optimizer, formal engine, testing system, debugger, and agent layer become different consumers of one semantic substrate rather than separate tools reconstructing meaning after the fact.

The expansion deliberately does not turn every axis into a term-level type rule. The architecture has a **thin waist**:

```text
source language
  │
  ├─ foundational semantics
  │    identity + lineage + invalidation + events + observers
  │    + exact numeric denotation + authority categories
  │
  ├─ opt-in contract schemas
  │    fault/recovery | leases | progress | memory models
  │    power/reconfiguration | relational security | ownership
  │
  └─ generated verification and custody
       campaigns | model checking | relational checks | netlist binding
       translation validation | numeric certificates | assurance graphs
```

The existing stratified judgments remain intact. Contract schemas compose summaries and generate obligations; backend packages discharge those obligations at explicitly recorded evidence levels. A design pays surface and verification cost only for the contract families it invokes.

## The six claims

The project stands on six falsifiable claims (from `rough-1.md`, refined and extended):

1. **Compile-time conversion.** A large class of hardware failures currently found in simulation or silicon can be converted into type failures, without making ordinary synchronous design feel like theorem proving.
2. **Typed metaprogramming.** Hardware generators should compute over typed hardware structures (Zig-style comptime over a typed graph), not source-token streams.
3. **Interfaces carry semantics.** An interface declares not just signals but timing, protocol, ordering, capacity, authority, and verification meaning — and those declarations _generate_ checkers, monitors, test strategies, and proof obligations.
4. **Structured testing beats blind fuzzing.** State-aware generation, semantic shrinking, metamorphic properties, and formal-assisted seeding outperform random mutation per unit of compute.
5. **Agents above a deterministic substrate.** Autonomous engineering works when every agent claim is validated by deterministic tools, every fact carries evidence, and diagnostics are precise enough to turn repair into targeted search.
6. **Assumption failure can share the substrate.** Fault recovery, software/hardware memory authority, progress, memory behavior, information flow, power/reconfiguration, physical exceptions, DFT/debug, and assurance can consume one semantic and evidence chain without becoming one unusable mega-judgment.

## What success looks like

- **Phase-1 success:** an expert designs FIFOs, arbiters, and pipelines in Strata and the generated SystemVerilog is as good as hand-written, while a class of CDC/width/reset bugs is structurally impossible. ([roadmap](11-roadmap.md))
- **Mid-term success:** a memory subsystem or small core is built where every stream contract generates its assertions and tests, failures shrink to minimal reproducers automatically, and agents close simple repair loops end-to-end without human triage.
- **North-star success:** an agent team, directed by a small human team, carries a processor from spec through verified FPGA prototype and release assurance, with transformations validated, every physical claim evidence-tagged, faults and lifecycle changes exercised, and all residual assumptions owned — while humans review decisions and uncovered residue, not diffs.

The first systems-safety proving wave is concrete: a fault-contracted MSHR with ECC/replay/stale-response rejection; a wait-for checker over CHI/NoC-style dependencies; a DMA–IOMMU–interrupt slice with mapping leases; and netlist-bound false-path/multicycle certificates. The ten small executable probes establish the required semantic separations; these four integrated targets test whether those separations survive realistic composition.

## What Strata is not

- Not a high-level synthesis tool: the designer states architecture; cost stays visible ([principles](01-design-principles.md) P-2).
- Not a proof assistant: proofs are one tier of a graded assurance story, demanded only where cheaper evidence is insufficient ([evidence](06-refinements-and-evidence.md)).
- Not an LLM-in-the-loop compiler: models are untrusted proposal generators outside the trusted base ([agents](09-agent-system.md)).
- Not a replacement for specialist signoff engines: Strata supplies semantic intent, custody, obligations, and release composition; commercial timing, formal, CDC/RDC, low-power, DFT, and safety tools remain backend evidence producers.
- Not a claim that bounded models prove unbounded systems: weak fairness does not yield a finite latency bound, litmus suites are not full memory-model proofs, digital interface contracts do not prove analog behavior, and assurance reports never upgrade the artifacts they summarize.

## The optimization claim, stated honestly

(Positioning language for extraction; fact-checked 2026-07-17 — every claim below survived adversarial verification, several only after correction.)

The gap between `cc` and `-O3` — a durable 2–3× on real workloads — was not won by better peepholes but by the compiler being _licensed_ to restructure: language rules (aliasing, UB-as-assumption) and IR advances (SSA) made whole-program transformation legal to _assume_. Hardware never got that license — today the designer hand-picks topology and the tool's job is to not break it. Strata's version of the license is stronger than C's ever was: proved and evidence-gated, not assumed — and the per-design deltas are larger than software's (topology selection alone is worth up to 63% area on production datapaths, per ROVER). The honest counterweight is Proebsting's law: _marginal_ compiler gains are slow; the claim here is not a faster treadmill but a one-time altitude change — moving hardware optimization from "don't break my netlist" to licensed restructuring.

`dont_touch` is two confessions in one attribute: **distrust** — the optimizer will break structure whose meaning it cannot see (CDC chains, exclusivity) — and **missing vocabulary** for legitimate boundaries (DFT, ECO anchors, physical cells). Strata answers the first with proof-carrying passes and keeps the second as typed, scoped declarations instead of strings.

The demo that matters: contract-driven topology selection with rewrite-chain certificates — change one constraint, watch the structure change, no RTL edit, checkable chain attached. Scoped precisely, because the pieces exist separately: HLS does constraint-driven restructuring (over scheduled C, not designer-stated architecture); ROVER ships bit-exact rewrite certificates. Nothing does **certified restructuring under contract-scoped observational equivalence** — rewrites legal because a _weaker-than-bit-exact_ equivalence (`TransactionEquivalent` behind an elastic interface) is what the surrounding contract observes.

The compounding inversion, with its precedent named: Rust proved that type-level safety facts can become optimizer permissions — `&mut`'s noalias guarantee licenses optimizations C cannot soundly have (and its multi-year LLVM-miscompilation saga is _evidence for_ our per-transformation certificates, not against them). Strata generalizes the pattern from one fact to the whole substrate — algebraic, exclusivity, range, encoding, temporal, observability — with permissions gated on _earned evidence levels_, which no surveyed system does. The narrow, survivable form of the safety-vs-cost inversion: **compile-time correctness facts carry zero area and license area reduction** — along the specification axis, more precision means smaller. (Runtime safety mechanisms — ECC, lockstep — still cost what they cost; refinements do nothing against bit flips, and we don't claim otherwise.)

Three caveats keep this credible, and they are commitments, not hedges: hardware cost is spatial — semantics decide _may_, measurement decides _should_ (P-7); trust is earned per-transformation — the certificates are the adoption mechanism for a signoff culture, not garnish; and **the certificate chain ends at Strata's emitted output** — vendor synthesis and P&R below it are unverified and seed-nondeterministic, which is exactly why boundary losses are measured and named ([07](07-compiler-architecture.md)), why certificate cost at full-SoC scale is honestly unmeasured, and why the trusted base itself (evaluator, interpreter, ledger) points at the mechanized-calculus north star ([open-problems OP-7](open-problems.md)).

## Where the risk is

The honest core risk, named up front: Strata already composes eight type disciplines that exist separately in research; the systems-safety expansion then asks optional contracts, relational checks, physical evidence, and assurance custody to share that model without contaminating ordinary code or overstating evidence. The ten probes support the partition but do not establish scale. Full RVWMO/coherence composition, unbounded progress, analog/power leakage, electrical power intent, vendor timing semantics, and industrial diagnostic usability remain open. The [open problems](open-problems.md) names those boundaries; the [roadmap](11-roadmap.md) is sequenced so the project produces value if any advanced family remains backend-only or deferred.

The competitive claim is correspondingly narrow: specialist academic systems and commercial suites are stronger in individual domains. 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. Strata must prove that integration advantage without claiming better solvers, P&R, timing, DFT, or fault engines.

````