# proposal/open-problems.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb/proposal/open-problems.md)

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

Visibility: public

Requested revision: 7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb

Requested commit: 7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb

Commit: 7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb

Blob: 8fb9f15e7250f63570267a4aed67df04e2a5e58e

Size: 21580 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb/proposal/open-problems.md?format=markdown)

```
# Open Problems

Known-unsolved design problems, mostly _interactions between_ individually-solved disciplines. Each entry states the problem, why it's hard, what the committed design does meanwhile, and what a resolution must deliver. The probing phase should try to (a) sharpen these, (b) find ones we missed, (c) kill or solve any it can.

## OP-1 · Speculation squash × temporal capabilities

**Problem.** An epoch squash must revoke resource grants that in-flight speculative operations already hold: scheduled intervals on shared units, linear slot tokens, credits. Linear/temporal typing has no standard story for _revocation_ — consumption is forever, but a flushed load's queue slot comes back.
**Why hard.** Naively, every capability becomes epoch-indexed and every use site needs a squash-path proof; that destroys the "modest surface burden" promise. Iris-style resource algebras can express reclaim, but the wave-2 probe showed committed scope doesn't need them: conservation counters + generative epochs suffice once fragments cannot escape component boundaries; the RA machinery becomes load-bearing only in the phase-3 fragment-escaping regime.
**Committed stance.** Phase-scoped under-claiming: speculative operations may only hold capabilities whose reclamation is structural (slots owned by a queue that itself handles squash; the type system checks the queue's squash contract once, at the component boundary, not per use). See [05-speculation-authority-effects.md](05-speculation-authority-effects.md).
**Research status (2026-07-17).** Confirmed genuine gap: neither Filament nor Anvil has any notion of a revoked/truncated interval (verified against both papers). Existing precedents to reconcile: PDL's typed speculation contracts (spawn/verify/kill with statuses — proves the typestate side is checkable) and HazardFlow's discard-and-restart hazard interfaces. No system combines them with interval/event types.
**Resolution must deliver.** A revocation rule sound w.r.t. the temporal-capability semantics, with errors expressible in the P-9 vocabulary.
**Probe result (wave 2, `probes/squash-semantics/`, RESOLVED-COMMITTED-SCOPE).** Revocation semantics designed and executable: authority revokes synchronously (tag compare), capacity drains within a declared bound `D` keyed on death events; squash contract = five checkable invariants (conservation / occupancy-sum / no-stale-authority / bounded drain / generativity) verified once at the component boundary, Tier-1 lookup at use sites. Crux settled: **claims are commitments** — squash is not a guard; the evaporation alternative is machine-refuted (physical double-drive in 300/300 random traces) and would need temporal-guard discharge the OP-4 line forbids. Intervals never revoke; only consumable tokens do. Firewall _relaxed_: speculative raw interval claims on shared units are legal without contracts; the prohibition narrows to consumable tokens crossing component boundaries. Residue (not blocking committed scope): epoch trees, squash × CDC crossing, unbounded-latency drains, revocation-horizon claims. "Resolution must deliver" is met for flat epochs: the rule is sound w.r.t. temporal-capability semantics and ships with its P-9 vocabulary.
**Wave-3 update (`probes/epoch-trees/`): the epoch-tree residue is RESOLVED and the two ambient axes unify.** Epochs form a tree rooted at the reset epoch; squash = one death event over a victim set; the five-invariant contract holds per-epoch and in aggregate with a single non-stacking drain bound; the chain-with-masks realization real OoO cores use provably implements the tree semantics (coordinate-liveness ≡ tree-liveness, property-checked). Reset **is** the root's subtree squash — same flush operation, no special case — and treating reset/speculation as independent ambient parameters is machine-refuted (150/150 witnesses: pre-reset speculative values retire under a dead generation). `ResetWitness` reset contracts are squash-contract instances: one mechanism. Remaining residue: multipath-fetch commit _ordering_ (contract itself is fetch-shape-agnostic), squash × CDC (probe in flight), heterogeneous per-subtree drain bounds (shape obvious), finite mask width (an ordinary capacity obligation).

## OP-2 · Reset epochs × everything

**Problem.** If reset creates a new system epoch invalidating old-epoch capabilities ([05](05-speculation-authority-effects.md)), then nearly every stateful type is epoch-indexed, and epoch parameters threaten to infect every signature.
**Why hard.** The value is real (stale-token bugs across reset are nasty); the cost is pervasive indexing — precisely the failure mode that killed heavyweight region systems.
**Committed stance.** Epochs are implicit ambient parameters within a reset domain; only values that _cross_ domains or _outlive_ a reset (retention registers, persistent handles) surface epoch indices. Whether this inference actually stays implicit under composition is the open question.
**Resolution must deliver.** An elaboration rule showing epoch indices stay out of ≥95% of user-written signatures on realistic designs.
**Probe result (wave 2, `probes/epoch-containment/`, NARROWED — bare rule refuted, mechanisms pass).** On a 52-signature boundary-heavy SoC corpus: the bare ambient rule yields **63.5% clean — FAIL**, with transport infection the killer (the fabric domain went 0/6; an arbiter over heterogeneous epochs isn't even typeable without existentials). With five absorption mechanisms (now committed design in [05 §4](05-speculation-authority-effects.md): `Stamped<T,D>` existentials + `bind epoch`, opaque minting-component-validated IDs, `no_reset` unit epochs, CDC-below-epochs, linear `ResetWitness`): **96.2% — PASS**, residue = the two signatures where a free epoch variable is load-bearing. Candidate general rule: _single-occurrence absorption_ — a free epoch variable is forced iff a signature relates ≥2 epoch-bearing values. The probe also fixed the criterion's definition (surfacing = free epoch variable; opaque carriers don't count) — without it the criterion was unmeasurable. Remaining items all closed in wave 3: the pinning analysis is a real inference pass — **local, principal, decidable** (`probes/pinning-inference/`: monotone join on a finite lattice, per-SCC summary fixpoint, 52/52 corpus agreement, 96.2% reproduced; epoch elision is inferred, not written — [05 §4](05-speculation-authority-effects.md)); the two ambient axes unify as one tree with reset at the root (`probes/epoch-trees/` — independent axes machine-refuted); and `ResetWitness` is a squash-contract instance under ONE epoch-death contract (`probes/squash-cdc/`). **OP-2 is RESOLVED for committed scope.**

## OP-3 · Subtyping decidability × summary-based composition

**Problem.** Incremental compilation composes components via summaries without reopening bodies ([07](07-compiler-architecture.md)); protocol refinement subtyping in full generality is undecidable, and "incomplete algorithm + solver" gives unpredictable results — poison for summary caching and for agents relying on definitive answers.
**Committed stance.** Protocol catalog with decidable parametric compatibility (D-015); Tier-2 solver checks always produce one of three _stable_ outcomes (`proved` / `refuted` / `obligation`), and `obligation` is a first-class summary entry, not a failure.
**Stakes raised by the package system.** Contract-typed dependency slots ([13 §2](13-package-system.md)) make resolution itself summary subtyping at ecosystem scale: if Tier-2 outcomes drift across solver versions, _dependency resolution_ becomes flaky — a strictly worse failure than a flaky build.
**Probe result (2026-07-17, `probes/protocol-catalog/`, SUPPORTS-SETTLED).** The coverage probe ran: AXI4-Lite, credit NoC, WRAP/INCR bursts, and OOO same-ID matching all land in the catalog _given_ four additions now specified in [04 §1](04-protocols-and-streams.md) (`bundle` and `layer` operators, `burst_dyn`, and the comptime-monomorphization rule for multiplying parameters). Nothing needed phase-3 user protocols. Confirmations: ordering-as-separate-judgment is forced (per-key FIFO order is refinement-inexpressible), and keyed-schema trace refinement is exactly the undecidability zone the committed design already fences. Remaining coverage risk: CHI-lite — untried, and the likeliest first genuine phase-3 case; it is the designated re-probe.
**Resolution must deliver.** Evidence that the catalog covers real designs (probe: take AXI4, CHI-lite, a credit NoC protocol, and try to express them), a user-defined-protocol story whose subtyping is decidable or honestly obligation-generating, and solver-version-stable outcomes for the resolution-facing subset.

## OP-4 · Grades and capabilities under path conditions

**Problem.** Conditional resource use (`if is_add { use adder }` / `if is_addr_calc { use adder }`) requires path-sensitive disjointness to justify sharing. Making the type checker discharge these turns it into a scheduler — the exact trap P-5 warns about for comptime.
**Committed stance.** The checker only _generates_ disjointness obligations; a distinct, bounded solver tier discharges them or the user arbitrates/replicates. The line between "checker generates obligation" and "checker schedules" needs a crisp formal statement.
**Probe result (2026-07-17, `probes/interval-caps/`).** The line held under implementation, with a candidate formal statement: _the check is a pure function over the design (no mutation, no reordering); repairs are suggestion values the checker never selects among; and the checker and discharge tiers exchange exactly one artifact type (the cardinality-form disjointness obligation) in exactly one direction_ — no interval data enters discharge, no propositional reasoning enters the checker. Remaining for full resolution: the checker↔*optimizer* exchange (sharing decisions the optimizer makes under discharged obligations) wasn't in probe scope.
**Resolution must deliver.** A characterization of which sharing decisions belong to typechecking, which to the optimizer, and how the two exchange facts without circularity — the probe's purity/one-artifact/one-direction statement is the candidate to formalize.

## OP-5 · Multi-judgment diagnostics

**Problem.** With five-plus interacting judgments, a single bad connection can fail in several dimensions at once, some via solver timeouts. Explaining _which_ judgment failed, _why_, and _what repairs exist_ is an unsolved UX problem at this scale — and P-9 makes it load-bearing for the entire agent thesis.
**Committed stance.** P-9 gating: a judgment doesn't ship without its diagnostic vocabulary. Errors are structured objects (violated judgment, facts, provenance, repairs) before they are English.
**Delivery vehicle.** strata-ls is the designated harness ([14 §21](14-toolchain.md)): multi-judgment failures render as one primary diagnostic naming its judgment with related facts attached; every repair acceptance/rejection is an experiment-DB event keyed by (judgment, repair, audience) — so "measure repair success given only the diagnostic" becomes standing telemetry, not a study.
**Resolution must deliver.** A worked diagnostic taxonomy over the phase-2 judgment set, user-tested (or agent-tested: measure repair success rate given only the diagnostic); per-judgment repair-success dashboards from strata-ls telemetry by end of phase 2, cited by the P-9 ship-gate for new judgments.

## OP-6 · Semantic ledger authoring burden

**Problem.** "Passes never silently drop facts" (P-3) implies every pass classifies its effect on every fact category. MLIR experience says analyses get invalidated wholesale in practice; the conservative default ("invalidates everything not mentioned", D-019) is sound but erodes toward useless if nobody annotates.
**Committed stance.** Conservative default + ledger-coverage metrics reported per pass, so erosion is visible; the small set of core passes we own get full annotations.
**Probe result (2026-07-17, `probes/ledger-passes/`, SUPPORTS-SETTLED with riders).** Erosion quantified on a 100-node/370-fact design over 12-pass pipelines: survival ≈ Π(1−touchᵢ) over the _union of lazy touch-sets_ (order-independent — invalidation is absorbing); at 25% lazy passes, provenance and protocol facts drop below 50%; full-lazy ends near zero. The committed mitigation holds: with core passes annotated, all categories survive at 100% end-to-end and provenance/verification-generation inputs fully work. Two riders now part of the design: (a) touch-set tracking must be structural — one _opaque_ pass with an unbounded touch set zeroes the ledger in a single step; (b) proof facts need finer-than-category invalidation — tag each proof with the equivalence it assumes and invalidate per-equivalence-break, else honest retiming annotations still gut the proof category. Metrics should report absolute counts alongside percentages (small categories are noisy).
**Resolution must deliver.** Evidence after phase 2 that ledger precision on the hot path (elaborate → schedule → emit) stays high enough that downstream consumers (verification generation, provenance queries) actually work — now with the two riders as implementation requirements.

## OP-7 · One semantic model

**Problem.** `refine-1.md`'s closing requirement — the eight disciplines must form _one_ semantic model with one metatheory — is asserted, not designed. Pairwise soundness is not composition soundness.
**Committed stance.** The committed phases only combine disciplines whose pairwise interaction is understood (see [11-roadmap.md](11-roadmap.md) phase gates). A core-calculus document (to be promoted to `15-core-calculus.md`) is the designated home for the real answer; mechanization of at least the phase-2 fragment is a north-star milestone.
**Probe result (wave 2, `probes/core-calculus/`, FRAGMENT-SOUND as amended — GAPS-FOUND(2), both repaired).** λ-strata⁰ formalizes the phase-1/2 fragment (23 typing + 4 WF rules, Rust checker with 86 tests, one function per rule). The thesis was demonstrated concretely: **two real cross-discipline unsoundnesses existed** — (1) _grades × later_: the naive feedback rule accepts a 1-graded value spent once per cycle; neither QTT nor guarded recursion alone can express the bug; fixed by FIX-ω (ω-promotion of feedback-body usage), whose corollary — ω-graded periodic capabilities remain usable in feedback — is exactly how linearity reconciles with initiation intervals; (2) _erasure × elaboration_: "erasure commutes with elaboration" is false once `reflect` exists; fixed by an elaboration-closedness premise on T-REFLECT (D-037's clause 2 doing double duty). All other attempted breaks are blocked by named, tested rules — including the branch-join rule _deriving_ D-039's errdefer discipline, and overlapping guards correctly deferring to discharge (the OP-4 line reproduced inside the calculus). Wave-1/2 amendments (positivity, cardinality obligations, modulo-II) turned out to be exactly the lemma premises, unreshaped — the probes were doing metatheory without knowing it. Lemma statuses: four PROVEN-SKETCH (one with proviso, one conditional), productivity PLAUSIBLE-STATED. Honest residue: term-level refinements × grades is the designated re-probe; symbolic event bases out of fragment; the D-037 production confluence argument is still owed.
**Resolution must deliver.** A core calculus for the committed feature set with type-soundness proven or mechanized, before phase 3 features stack on it — now concretely staged: the checker stays green as a phase-2 gate with per-feature break-hunt reruns; **full mechanization (est. 2–4 person-months, Lean/Coq) is the phase-3 entry gate**, not the phase-2 exit.

## OP-8 · Dynamic-latency temporal capabilities

**Problem.** Fixed-latency intervals (Filament-style) are well understood; dynamic latency (cache misses, arbitration) needs symbolic event constraints (`response ≥ request + 1`) and their interaction with capability non-overlap checking is much less mapped. Anvil points a direction; maturity unknown pending research brief.
**Research status (2026-07-17).** Anvil (ASPLOS 2026) shows dynamic event patterns are typeable via event-graph interval containment, but it is a first-release prototype that currently loses ~2× in power to Filament on a static pipelined ALU — dynamic-event typing is not yet compatible with keeping static-pipeline quality. Promotion criterion recorded in [03](03-time-and-resources.md).
**Committed stance.** Phase 2 ships fixed-latency capabilities; dynamic latency enters via protocols (outstanding-count refinements) rather than via the interval checker.
**Resolution must deliver.** A decidable (or obligation-generating) non-overlap story for symbolic intervals.

## OP-9 · Fault-model completeness and health composition

**Problem.** The fault probe separates occurrence, detection, correction, containment, recovery, and invalidation for a bounded MSHR model. Real fault campaigns must cover spatially correlated faults, common-cause failures, latent multi-bit corruption, clock loss, memory-array behavior, and faults in the protection logic itself.
**Committed stance.** Health contracts enumerate fault classes, injection sites, detection/containment bounds, trustworthy residue, and coverage. Unlisted classes remain residue; a campaign never implies environmental qualification.
**Resolution must deliver.** An integrated MSHR/ECC/replay target, mutation adequacy against protection-logic faults, and a mapping from declared fault coverage to independent safety-tool/physical evidence without double-counting.

## OP-10 · Compositional progress beyond finite summaries

**Problem.** Finite wait-for SCC/rank/escape checks catch practical deadlocks but do not prove arbitrary protocol liveness, and weak fairness does not provide finite response bounds. Abstraction can also erase the dependency that closes a cycle.
**Committed stance.** Stable `proved/refuted/obligation`; explicit assumption ownership; only independently provisioned escape resources, well-founded ranks, or checked acyclicity discharge the decidable core.
**Resolution must deliver.** CHI/NoC/reset-drain corpus results with seeded deadlocks, abstraction-sound summary rules, and a clear handoff from conditional progress summaries to model checking or theorem proving.

## OP-11 · Full memory-model and translation composition

**Problem.** The probe proves protocol legality and architectural memory legality are distinct, but full RVWMO/Arm-style models include mixed-size/per-byte behavior, dependencies, translation, speculation, coherence, DMA, and interrupts. Partial summaries can become unsound if completeness is overstated.
**Committed stance.** First-class events/relations plus explicit completeness; bounded litmus/model checks are evidence, not universal proofs.
**Resolution must deliver.** Validation against a standard executable model, mixed-size and address-translation cases, component-summary composition theorems or conservative obligations, and an RTL-linking story.

## OP-12 · Observer adequacy and physical leakage

**Problem.** Noninterference is only as meaningful as the observer projection. Cycle, contention, cache, debug, and power observers are incomparable in places; physical leakage is probabilistic and target-dependent, not fully represented by digital traces.
**Committed stance.** Named observer projections in semantics; two-run relational verification; explicit declassification authority; physical power observations remain measured/model evidence.
**Resolution must deliver.** Observer adequacy criteria, composition rules across hardware/software speculation contracts, and a calibrated path from digital leakage models to measurement without promoting correlation to proof.

## OP-13 · Vendor-bound physical, power, and DFT semantics

**Problem.** Exact selector precedence, retiming/cloning lineage, setup/hold pairing, scan insertion, UPF power semantics, RDC, and reconfiguration behavior vary by backend and version. Source intent alone cannot prove what a vendor artifact means.
**Committed stance.** Candidate certificates plus exact nonempty post-transform binding and validation; dependency manifests invalidate on relevant design/tool/target/mode changes; digital guarantees remain conditional on characterized electrical assumptions.
**Resolution must deliver.** At least two vendor adapters and one open-flow adapter, seeded selector/precedence/lineage failures, DFT and power-aware translation validation, and measured false-positive/false-negative behavior.

## OP-14 · Assurance-case scale, standards, and epistemic independence

**Problem.** A custody graph can become a large, circular dashboard that appears authoritative while merely restating correlated artifacts. Tool diversity, assumption ownership, evidence incompatibility, expiry, and release diffs must remain visible at SoC scale.
**Committed stance.** Assurance cases are deterministic derived graphs and never evidence. Self-citation and circular ownership are rejected; uncovered residue is mandatory output.
**Resolution must deliver.** Export/interchange with an established assurance metamodel (for example OMG SACM), incremental scaling measurements, diversity/correlation rules, and a seeded study showing that stale, circular, incompatible, and missing evidence cannot yield a green release.

```