# proposal/08-verification-platform.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/a0828f65437c5a864898323290e15e77383c4a52/proposal/08-verification-platform.md)

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

Visibility: public

Requested revision: a0828f65437c5a864898323290e15e77383c4a52

Requested commit: a0828f65437c5a864898323290e15e77383c4a52

Commit: a0828f65437c5a864898323290e15e77383c4a52

Blob: 3e00bab96c0f6381258e1ab00d8b553014a66786

Size: 9098 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/a0828f65437c5a864898323290e15e77383c4a52/proposal/08-verification-platform.md?format=markdown)

```
# Verification Platform

How declarations become verification artifacts, and how testing, formal, and mutation compose into evidence. Principles in force: P-7 (claims carry evidence), P-11 (dogfooded on Strata's own components first).

The research landscape validates the platform thesis directly: the strongest existing results (Cascade, TestRIG) each implement _one slice_ of this design bespokely, and the cross-cutting gaps — no maintained PBT-with-shrinking for hardware, no open BMC-witness-as-seed pipeline, no general semantic shrinker, no property-quality scoring loop — are exactly what an integrated, type-driven platform can claim. (D-028)

## Committed design

### 1. Declarations generate infrastructure

A stream/contract declaration ([04 §8](04-protocols-and-streams.md)) generates: payload-stability assertions, transfer-event definitions, outstanding-count tracking, capacity/ordering checks, legal + adversarial generators, cancellation tests, coverage bins, field-aware mutators, and semantic shrink rules. One `#[derive(...)]` on a payload type yields packed representations, waveform metadata, symbolic values, constrained generators, and shrink rules ([02](02-type-system-core.md) reflection). Nothing here is hand-maintained; it is compiled from the same judgments the typechecker uses (the [vision](00-vision.md)'s claim 3).

### 2. Property-based testing with integrated shrinking

- **Strategies** are typed, state-aware generator functions (weighted, model-conditioned — `rough-1.md` §18 stands).
- **Stateful rule-based testing**: `state_machine` blocks with rules, preconditions, and invariants driving DUT + reference model in lockstep.
- **Shrinker architecture (D-028): Hypothesis-style integrated shrinking** — shrink the generator's _choice sequence_, not the produced value, so every shrunk case is valid by construction and strategies compose shrinkage for free. This is the state of the art in software PBT and precisely what no hardware framework offers (cocotb+Hypothesis integration is folklore without working shrinking; chiseltest is unmaintained). TestRIG/QuickCheckVEngine proves the concept end-to-end for CPUs — QuickCheck-shrunk instruction sequences diffed over RVFI found real pipeline bugs — but is Haskell- and ISA-bound; Strata generalizes it to any typed interface.
- **Semantic shrinking** preserves dependency structure (data/memory deps, branch preconditions, transaction relationships, privilege/protocol state) during reduction. Cascade's automated program pruning is the nearest precedent and is bespoke to its generator; ours falls out of typed strategies + choice-sequence shrinking.

### 3. Fuzzing, structured

Field lessons baked in: valid-by-construction, long, control/data-entangled inputs beat byte-stream mutation (Cascade: 28–97× coverage vs prior fuzzers, 37 new bugs — its "asymmetric ISA pre-simulation" trick generalizes to "generate against the reference model's view"); coverage proxies (mux-toggle, control-register) are weak signals to be _combined_, not trusted individually. Strata's coverage model spans RTL branch/condition/toggle, functional, protocol-state, architectural/microarchitectural novelty, queue occupancy, hazard combinations, assertion proximity, and differential divergence; the corpus manager retains by semantic value.

### 4. Metamorphic and differential testing

- Metamorphic properties (NOP insertion, latency perturbation, burst splitting, speculation-path variation preserve committed state) as first-class `#[metamorphic]` declarations.
- **Differential backbone (D-028): commit-level lockstep over an RVFI-class interface.** For RISC-V targets: RVFI(-DII)-style per-retired-instruction comparison against Spike/Sail, riscv-dv-compatible trace diffing as the coarse mode; the platform generalizes the interface so non-CPU components (caches, NoCs) get the same treatment against their reference models. This is current best practice (TestRIG, RVVI lockstep) rather than invention — the novelty is generation from types.

### 5. Formal-assisted testing

Target: `queue full ∧ older unresolved store ∧ mispredict ∧ translation fault`. Pipeline: encode as reachability cover → BMC produces witness → witness becomes executable prefix/corpus seed → structured mutation of continuations → failure → shrink → generalize. HyPFuzz proved the loop works but is JasperGold-bound; **the open-source version of this pipeline effectively does not exist** — SymbiYosys `cover` witnesses exist, using them as fuzz seeds doesn't. That's ours to build on the [committed formal backend](07-compiler-architecture.md) (SymbiYosys first, circt-bmc when its counterexample extraction lands).

### 6. Property validation and mutation scoring

Agent-generated (and human-generated) properties are untrusted candidates ([09](09-agent-system.md)): checked for vacuity, unreachable antecedents, over-strong assumptions, exclusion of legal behavior — and scored by **mutation testing**: inject dropped responses, duplicated transactions, delayed flushes, arbitration corruption; a property that catches no mutants is flagged. Open tooling precedent: MCY (mutations + formal filtering of equivalent mutants); emerging pattern: mutation as assertion-quality oracle (VERT). Mutation results feed the [evidence lattice](06-refinements-and-evidence.md) as `MutationValidated<mutant-classes>`.

### 7. Dogfood targets (P-11)

Phase order of verification targets mirrors the [roadmap](11-roadmap.md): Strata's own stdlib FIFOs/arbiters/CDC bridges first (their contracts are the catalog schemas' reference implementations), then a cache + memory controller, then a small pipelined core with the full differential + formal-assisted loop.

### 8. Systems-safety contract compilers

Each optional contract family generates a different artifact package; none is silently treated as a type proof:

| Contract family | Generated artifacts | Honest result boundary |
| --- | --- | --- |
| Fault/health | occurrence→detection monitors, containment windows, stale-value rejection, ECC/parity/lockstep/replay campaigns, permanent/transient mutants | coverage is over declared fault classes and injection sites, not arbitrary physical failure |
| Mapping leases | DMA/IOMMU/interrupt lifecycle tests, issue-time authorization monitors, unmap-drain and stale-descriptor campaigns | assumes modeled hardware mediation and owner validation |
| Progress | finite wait-for graph, SCC/ranking/escape checks, arbitration starvation tests | `proved / refuted / obligation`; weak fairness never manufactures finite `N` |
| Memory model | event-relation export, completeness checks, litmus generation, herd/model-adapter comparison | bounded suites are evidence, not all-program refinement; full RVWMO awaits mixed-size/per-byte validation |
| Observer security | two-run harnesses, declassification-authority checks, cache/contention/debug observation comparisons | model-relative noninterference; power observations require physical evidence |
| Power/reconfiguration | lifecycle monitors, isolation/retention/quiescence checks, stale-generation tests, replacement-ABI/authenticity obligations | digital protocol proof assumes characterized electrical behavior |
| Numeric accuracy | unit/scale checks, range campaigns, transformation error certificates, calibration-expiry tests | correlation and approximation models are explicit assumptions |
| DFT/debug | authenticated-mode reachability, scan/trace policy checks, functional and security-observer translation validation | insertion proof is conditional on fuse/mode/power/isolation premises |
| Assurance | deterministic hazard→guarantee→assumption→artifact graph, release diff, expiry and residue report | the graph summarizes evidence and never counts as evidence |

Campaigns are declaration-derived but remain scored like any other verification artifact: mutation adequacy, coverage, boundedness, target/tool pins, and expiry are visible. Missing ownership, incomplete event relations, stale artifacts, and unsupported backend semantics produce obligations or release failures—not optimistic defaults.

## North star

- Coverage-novelty metrics learned from traces (microarchitectural-state novelty beyond hand-defined bins).
- Formal generalization of shrunk counterexamples into proven property strengthenings.
- Cross-run corpus transfer between design variants via architectural-IR-level mapping (an experiment-database service, [09 §4](09-agent-system.md)).
- Standard-model adapters for RVWMO/Arm-style mixed-size memory behavior, commercial fault/safety tools, power-aware simulation, and DFT/signoff flows; adapters import evidence without placing those tools in Strata's semantic trusted base.
- Independent-checker diversity for high-consequence certificates and assurance claims.

## Open problems touching this doc

None owned; consumes [OP-3](open-problems.md) obligation stability (summaries drive which properties re-verify) and feeds [OP-5](open-problems.md) (failure explanations reuse the diagnostic vocabulary).

```