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":

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), 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).

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:

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) 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 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) — 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<N>, 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.

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:

(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.:

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). Evidence for physical facts is produced by the FPGA loop; evidence for behavioral facts by the verification platform; mutation-validation of properties is itself an evidence producer (08 §6).

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). 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).

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<VendorDoc> 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 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). 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 (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 (obligation generation vs the checker-becomes-scheduler line), OP-5 (explaining solver failures).