# proposal/06-refinements-and-evidence.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/54efc08232a7296ff1ec4dc6e45d9649c9364dad/proposal/06-refinements-and-evidence.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: 54efc08232a7296ff1ec4dc6e45d9649c9364dad Requested commit: 54efc08232a7296ff1ec4dc6e45d9649c9364dad Commit: 54efc08232a7296ff1ec4dc6e45d9649c9364dad Blob: 5e66a20a99bdb57f350f271031a8b8f35c2e1a41 Size: 14895 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/54efc08232a7296ff1ec4dc6e45d9649c9364dad/proposal/06-refinements-and-evidence.md?format=markdown) ```` # Refinements, Proofs, and Evidence How Strata states facts stronger than structural types, who discharges them, and how strong the resulting knowledge is. Principles in force: P-7 (claims carry evidence), P-9 (diagnostics are the product). ## Committed design ### 1. Three refinement tiers (D-016) The refinement language is deliberately constrained; unconstrained predicates make checking undecidable, errors unpredictable, and incremental compilation impossible. Surface syntax names the tier, so nobody — human or agent — confuses "structurally proved" with "no counterexample found under a bound": ``` requires static { issue_width <= entries } // Tier 1 requires solve { !(is_load(op) && is_store(op)) } // Tier 2 requires prove { every_request_eventually_responds() } // Tier 3 ``` **Tier 1 — intrinsic, compiler-complete.** Linear integer arithmetic over static naturals, bit-vector equalities, finite-set membership, constant ranges, clock/domain identity, structural sizes, fixed-interval non-overlap. Checked by decision procedures inside the typechecker; failure is a definitive type error. **Tier 2 — solver-backed.** Path conditions, bounded arithmetic, mutual exclusivity, local state invariants, protocol index constraints. Discharged by SMT with a fixed budget. **A timeout or unknown is never an error and never flaky**: it produces a first-class `Obligation` recorded in the component summary ([07](07-compiler-architecture.md)), which downstream consumers may discharge, assume (visibly), or gate on. The three stable outcomes — `proved / refuted / obligation` — are part of the summary contract (this is the fix for [OP-3](open-problems.md)). **Tier 3 — proof obligations.** Liveness, unbounded invariants, deadlock freedom, global ordering, inductive invariants. Never required to compile; discharged by external artifacts (model checker runs, inductive proofs, translation validation) whose _results_ enter the evidence system below. **A fourth discharge path: comptime-exhaustive evaluation (D-036).** Because the comptime evaluator is deterministic, typed, budgeted, and already in the trusted base (P-8), exhaustively evaluating a pure predicate over a small finite domain _is a proof_: ``` requires solve exclusive(decode) discharge by comptime_exhaustive(opcode: Bits<7>) // 2^7 evaluations, budget-gated ``` Applicability is checked: the predicate must be `static`/`ghost`-phase evaluable, the domain a finite type with a canonical enumerator, and the run must fit the declared P-6 budget — _checked up front against a declared per-evaluation cost bound that is then enforced as a hard cap inside each evaluation_ (probe finding, `probes/exhaustive-discharge/`): without the hard cap, an estimated per-eval cost lets a hidden expensive path pass the gate and exhaust mid-run. With it, the outcomes are four and all deterministic — `proved / refuted(counterexamples) / rejected-up-front(zero steps spent) / eval-cost-overrun(named offending value)` — reproducible by P-6 determinism, never a timeout. Two further probe-derived rules: discharge predicates are barred from reading the remaining budget (a predicate branching on `remaining()` makes the proof budget-relative, colliding with purity — the one exception to D-044's "readable" property), and a checker `Exhausted`/overrun outcome maps to the standard `obligation` outcome downstream, not an error. **Wave-2 refinement (`probes/static-eval-bounds/`): the bound is derived by default.** For the analyzable slice (straight-line + static-bound loops + match + non-recursive calls), the per-eval bound is computed by static analysis — _exactly tight_ (1.0×) on all realistic discharge predicates tested (decode exclusivity, one-hot, Gray adjacency, FIFO wrap), sound over 10,000 randomized evaluations. The derived path has **three** outcomes (`proved / refuted / rejected-up-front`) with the hard cap demoted to an internal never-fires assert; ineligibility (recursion, data-dependent trip counts — the documented frontier, since size-bounding recursion needs a termination measure the trusted base shouldn't carry) routes to the declared-bound path, where the four-outcome contract including user-visible `eval-cost-overrun` stands. Declared bounds remain for out-of-slice shapes and for tightening at the budget boundary. On failure it yields a concrete counterexample row, feeding the counterexample-becomes-test loop ([08 §5](08-verification-platform.md)) with zero witness-extraction machinery. One soundness condition the ledger enforces: exhaustive evaluation proves a fact about the _comptime function_; it counts as a fact about the _hardware_ only because D-022 guarantees the architectural node was generated from that same table — the ledger records the table hash linking evidence to node. Preference order: Tier 1 > comptime-exhaustive (where applicable) > Tier-2 SMT. Precedents: Zig `comptime assert`, Rust const-eval assertions, and the generate-and-check stance generally. **Assertions are claims, and narrowing is a fact source (D-069).** Flow-sensitive narrowing — what the checker knows inside a match arm or past a guard — is harvested into the [ledger](07-compiler-architecture.md) automatically; no assertion needed and nothing to trust. A user `narrow!(p)` assertion is never itself evidence: it routes through this section's machinery — Tier 1/Tier 2 if provable, `comptime_exhaustive` for small domains, otherwise a first-class `Obligation` usable only at `Assumed` evidence — and P-7's consumer pattern holds: an optimizer pass states the minimum evidence it requires before acting on one. **Term-level refinements are two sorts (D-016 as amended, wave-3 `probes/core-calculus/`).** A refinement predicate may mention (i) static indices — a **static refinement**: Tier-1 machinery as above, erased with the types — or (ii) the runtime values of hardware-phase, hardware-grade term variables — a **state refinement** (`Occupancy<0..=CAP>` over a counter, `x < depth_reg`), which is a ghost observation: the predicate is over the `observe`-projection of the trace, and its introduction emits a first-class `Obligation` (with the harvested D-069 path condition) compiled to monitors/assertions ([08](08-verification-platform.md)) — never a Tier-1 fact. Three calculus-mandated rules: (1) variables in refinement position are used at grade 0 — mention never consumes and never _counts as_ consumption (both directions of the naive rule are demonstrably unsound); (2) a refinement in hardware content may not name an erased (grade-0 or ghost) variable — erasure would strand the predicate's meaning; spec-only (ghost) refinements may name anything, since they erase together; (3) a state refinement acquires static strength only through the discharge channel (its _unconditional_ obligation recorded discharged in Ψ), never by subsumption — and an obligation formula that escapes its variable's binder is re-indexed to the binder's port (erased binders reject the escape). **Engineering commitments (D-025), imported from LiquidHaskell/Flux experience:** - Tier-2 logic stays in the quantifier-free decidable fragment (QF-LIA + QF-BV + EUF); quantified invariants are Tier 3 by definition. - Liquid-style inference for boring invariants; user annotations only at component boundaries. - Any PLE-style proof-by-evaluation automation is opt-in per module, never global (LH's superlinear-blowup lesson). - Refinement failures report inferred vs expected predicate _plus_ the relevant variable context, and we invest early in counterexample surfacing — the documented UX gap of every SMT-backed system. - The checker is architected like a plugin with binder-level incrementality; re-check only what changed. - Refinements stay pure by leaning on the linearity discipline for mutable state (the Flux lesson: ownership keeps refinements out of spatial logic). ### 2. Named refinement types Common refinements get names rather than raw predicates — `Index`, `Occupancy<0..=CAP>`, `CreditCount<0..=MAX>` — because names compose into diagnostics and into optimizer facts (range-driven width narrowing, mux pruning) better than anonymous predicates. See [02 §4](02-type-system-core.md). ### 3. The evidence lattice (D-017) Facts the compiler must never silently infer as truth — max frequency, area, power, post-placement fanout, metastability, unbounded liveness, environmental fairness, vendor-primitive correctness — carry explicit evidence: ``` Declared | Assumed | StaticallyDerived | Tested | ExhaustivelyEvaluated | BoundedProved | InductivelyProved | TranslationValidated | Measured ``` (`ExhaustivelyEvaluated` sits at `BoundedProved` strength — it is a bounded proof whose bound is the whole domain — but is cheaper to audit and natively yields counterexample rows; see §1's fourth discharge path.) Guarantees carry evidence **sets**, not single levels — the no-duplicate-response example below already shows why (testing, bounded formal, and mutation validation establish different things and accumulate). The semver probe (`probes/summary-semver/`) made this load-bearing: with single-level evidence, an author who _adds_ `Measured` alongside an existing proof gets punished with a forced MAJOR because the levels are incomparable; with sets, adding evidence is monotone refinement and mechanically MINOR. Consumers' `require evidence >= X` checks against the set's best entry on the relevant axis. These are not one linear order (measurement and proof establish different things); each guarantee names its evidence, e.g.: ``` guarantee no_duplicate_response evidence: Tested<17.2e9 txns>, BoundedProved, MutationValidated frequency: Measured<842 MHz, vu19p, vivado-2026.1> ``` **Consumers state minimum evidence.** An optimizer pass may `require guarantee G with evidence >= BoundedProved`; a release gate may demand `InductivelyProved` or an approved waiver; an agent report must quote evidence levels verbatim ([09](09-agent-system.md)). Evidence for physical facts is produced by the [FPGA loop](10-fpga-loop.md); evidence for behavioral facts by the [verification platform](08-verification-platform.md); mutation-validation of properties is itself an evidence producer ([08 §6](08-verification-platform.md)). **Generated assurance cases are derived indexes, never evidence (D-090).** A machine-maintained hazard → guarantee → assumption → artifact graph records assumption ownership, content hashes, expiry, design/tool/target pins, evidence sets, checker diversity, release diffs, and uncovered residue. It may gate a release and make weakening visible, but it has no evidence strength of its own and may not cite itself or replace the primary artifacts it summarizes (`probes/assurance-cases/`). ### 4. Contracts Components declare `assume`/`guarantee` pairs (unchanged in spirit from `rough-1.md` §17). Composition checks that provided guarantees satisfy required assumptions at the summary level ([07](07-compiler-architecture.md)). Component substitution is **refinement, not equality**: replacement B is legal when it assumes no more and guarantees no less, with explicit care for liveness (a B that is safe-but-stalls does not refine an A that guaranteed progress). Contracts compile into static checks, simulation assertions, formal properties, monitors, test targets, and coverage goals — one declaration, many artifacts (claim 3 of the [vision](00-vision.md)). Advanced contracts are sparse schema families over that same envelope, not new universal typing judgments (D-091): fault/detect/correct/contain/recover; mapping leases; finite progress summaries; architectural memory relations; observer-relative security; power/reconfiguration lifecycle; DFT/debug authority; numeric budgets; and assurance ownership. A family defines its fields, composition polarity, generated artifacts, evidence consumers, and invalidators. If a component does not declare a family, its summary contains no placeholder fields or obligations for it. Missing facts inside a declared family become explicit obligations or residue, never absence-as-success. ### 5. Granular unsafe `unsafe` is categorized — `clock_crossing`, `timing`, `reset`, `primitive`, `proof_assumption`, `external_effect`, `uninitialized_use`, `encoding` — each suspending only its own judgment. Every unsafe declaration must state what it _assumes_ and what it _guarantees_; the guarantees enter the evidence system as `Assumed` or better (an imported verified artifact upgrades them). The compiler reports the aggregate unsafe surface per build. **Invariants are structural, not social.** Rust's "safe abstraction over unsafe core" works, but its invariant documentation is a `// SAFETY:` comment enforced by a lint — and the Rustonomicon's own insight is that the soundness boundary is the _module_, not the block, because unsafe code relies on invariants maintained by the safe code around it. Strata makes this machine-checked: every granular unsafe block names a machine-readable assumption (a Ψ-fact tagged `Assumed`), and the enclosing component's summary must either discharge it (Tier 2/3) or re-export it. The aggregate unsafe report then lists _invariants and who holds them_, not block counts. ## North star - Tier-2/3 boundary automation: obligation clustering, lemma suggestion, agent-assisted invariant search (the [formal agent](09-agent-system.md) proposes; the solver disposes). - Relational refinements (two-execution properties) parameterized by named observer projections as the entry path for the deferred information-flow story (D-023/D-085; `probes/observer-flow/`; SpecVerilog is the reference point, [12](12-related-work.md)). Implementation equivalence and noninterference remain distinct facts. - Finite compositional progress summaries with `proved/refuted/obligation`, explicit assumption ownership, and rank/escape certificates; unbounded/state-dependent/fairness cases remain Tier 3 (D-083, `probes/progress-waitfor/`). - Numeric error transformers and enclosing budgets over exact unit/scale/rounding/overflow representation semantics (D-088, `probes/numeric-error/`). - Proof artifact portability: inductive proofs as content-addressed artifacts checkable by an independent small checker, so the trusted base stays small (P-8). ## Open problems touching this doc [OP-3](open-problems.md) (stable obligations vs summary caching — the design above is the committed mitigation; probing should attack whether `obligation` outcomes really stay stable across solver versions), [OP-4](open-problems.md) (obligation generation vs the checker-becomes-scheduler line), [OP-5](open-problems.md) (explaining solver failures). ````