# proposal/05-speculation-authority-effects.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/6e774a8a98ad63868774cf1558e6159b6a8b6593/proposal/05-speculation-authority-effects.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: 6e774a8a98ad63868774cf1558e6159b6a8b6593 Requested commit: 6e774a8a98ad63868774cf1558e6159b6a8b6593 Commit: 6e774a8a98ad63868774cf1558e6159b6a8b6593 Blob: 39966c6c2837b2c8d0e9a4873760d6846691dea5 Size: 18329 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/6e774a8a98ad63868774cf1558e6159b6a8b6593/proposal/05-speculation-authority-effects.md?format=markdown) ```` # Speculation, Authority, and Effects The `Effects` judgment and the authority system: what an operation does, what privilege it needs, and how speculative work is prevented from becoming irrevocable. Principles in force: P-1 (speculative values cannot reach irreversible effects), P-8 (authority is capability-gated, not convention). ## Committed design ### 1. Effects in three categories A flat effect list conflates different questions. Strata splits: - **Behavioral** — what state transition occurs: `Reads`, `Writes`, `Allocates`, `Releases`, `Sends

`, `Receives

`, `Raises`. - **Temporal** — how the operation occupies time/resources: `Combinational`, `Registers`, `Schedules`, `Crosses`, `MayStall`. (These are requirements/coeffects — they consume [capabilities](03-time-and-resources.md), they don't mutate state.) - **Authority** — what privilege is required: `Requires`, `Requires`, `Requires`. Effect rows are inferred bottom-up and appear in [component summaries](07-compiler-architecture.md); a `Combinational` function structurally cannot mutate, latch, allocate, cross clocks, or send. A summary reads as effects + requirements + guarantees (e.g. _writes QueueState; requires one QueueWritePort during [Issue, Issue+1) and one free slot; guarantees occupancy' = occupancy + 1_) — consumable by optimizer and agents alike. ### 2. Speculation as epoch-indexed authority (D-018) `Speculative` / `Committed` / `Architectural` — but the tag is not the mechanism. The mechanism is _which effects are authorized under which epoch_: ``` Speculation { predict: PredictAuthority, // update predictors freely allocate: ReclaimableAuthority, // grab entries a squash can reclaim write_internal: RollbackAuthority, // mutate state a squash can roll back } commit(v: Speculative, proof: CommitProof) -> Committed cancel(epoch: Speculation, token: CancelToken) -> ReclaimedResources write_mmio(req: Authorized) // no speculative path exists ``` Epochs are generative ([02 §5](02-type-system-core.md)); a stale epoch's values cannot be confused with a new epoch's even under counter wraparound (logical identity; encoded generation + wraparound obligation physically). **Epoch shape (probe-established, wave 3, `probes/epoch-trees/`):** within one reset domain, epochs form a _tree_ rooted at the domain's current reset epoch; unresolved branches are the interior nodes. Squashing an epoch kills it and all live descendants as **one death event over a victim set**: the §3 squash contract holds per-epoch and in aggregate over the victim set, with a single drain bound D per flush — child drains complete within any enclosing bound and never stack with tree depth (each epoch dies at most once; an earlier-killed child keeps its own, tighter death event). Generativity in victim-set form: every victim compares below the flush's allocator watermark, so ids minted after a flush are never its victims — and _no id-range test characterizes victimhood_; flushes are keyed by their death events, never by epoch order. The committed _realization_ is the chain-with-masks encoding real OoO cores implement: a value's epoch coordinate is the pair (reset-generation tag, mask of unresolved ancestor branches) — a compressed root-path — and an operation dies iff any coordinate component dies. This encoding provably implements the tree semantics (property-checked over random trees and squash orders), so committing to branch-shaped chains forecloses nothing: nested speculation is the same contract on a bushier tree (north star; the one genuinely open piece there is commit _ordering_ under multipath fetch, not the squash contract). `CommitProof` generalizes from "oldest epoch" to "path fully resolved": commit requires an empty branch mask under a live reset generation. **Research grounding.** PDL (PLDI 2022) is the proof of concept that this shape is statically checkable: speculative threads carry a status; typing rules forbid speculative/unknown threads from releasing write locks or committing; every speculative ID must be verified or killed; misspeculation rollback is auto-inserted. Two PDL boundaries we consciously inherit-and-improve: PDL's guarantees stop at trusted lock implementations (ours stop at component squash contracts, below — same shape, but contract-checked once per component), and PDL restricts speculation to branch-prediction shapes (committed scope accepts a similar restriction; generality is north star). ### 3. The squash boundary (the OP-1 firewall) The committed design deliberately under-claims. **Rule: speculative operations may only hold capabilities whose reclamation is structural.** Concretely: a speculative load may allocate a load-queue entry because the load queue _component_ declares a squash contract — checked once at the component boundary (Tier-2/Tier-3 obligations). What speculative code may **not** do is spend _consumable_ tokens (slots, credits) into a component that has no squash contract for the epoch domain — such a token is genuinely gone on squash. Raw temporal _interval_ capabilities on shared units are legal for speculative ops with no contract at all: claims are commitments (a squashed op's claimed interval stays busy — probe-validated, `probes/squash-semantics/`), so nothing needs reclaiming and the wave-1 interval checker runs with zero epoch data. The typechecker enforces two rules: `RollbackAuthority` gates writes only to state owned by components with squash contracts for `E`, and consumable allocations by speculative ops require the owning component's contract (SPEC-ALLOC — a Tier-1 summary lookup). **The squash contract has exact content** (probe-resolved, wave 2): per epoch `E`, conservation `granted(E) = live(E) + retired(E) + reclaimed(E)` with monotone counters; occupancy = Σ_E live(E) ≤ capacity; synchronous authority revocation at `death(E)` (no dead-epoch token authorizes anything, including during drain); capacity drain bounded by a declared `D` **keyed on the death event, not epoch order** (generative ids created after a flush also compare ≥ its victims — a real spec trap the property tester caught); epoch generativity. Verified once at the component boundary (Tier-2/3); the split is _authority revokes synchronously, capacity drains_ — a flushed load's outstanding miss cannot be un-sent, so its slot (`SquashPending`: capacity without authority) frees only when the dead response returns. Diagnostics: `stale-authority`, `unreclaimable-capability`, `drain-overrun`. Full semantics: `probes/squash-semantics/DESIGN.md`. **Across a clock-domain crossing** (probe-resolved, wave 3, `probes/squash-cdc/`) the contract survives with two generalizations and no new invariants: a death event acquires per-domain observation points (`death_src`, `death_dst` = the in-band Kill marker's arrival), I3 holds per domain keyed on _local_ observation, and I4's drain clock is denominated in far-side response events plus a synchronizer tail — still keyed on the death event, never on epoch order. Global safety weakens from synchronous revocation (physically impossible across domains) to **no-stale-commit**: far-side retirement is gated on in-band `Resolve`, and `Resolve`/`Kill` are per-epoch exclusive, so a value that raced past its own death can be speculatively consumed but never retired. Cross-domain conservation composes as the sum of the two domains' closed ledgers plus the channel. See [04 §7](04-protocols-and-streams.md) for the bridge-as-carrier clauses. This resolves [OP-1](open-problems.md) for committed scope (flat epochs). The evaporation alternative — squash as a guard on interval claims — is machine-refuted (physical double-drive in 300/300 random traces) and would require temporal-guard discharge the OP-4 line forbids. ### 4. Reset as an epoch transition (D-018 continued; OP-2 stance) Reset is not a bit; it creates a new system epoch invalidating old-epoch tokens (`TransactionId`, `QueueToken`, `Speculation`). Reset sequencing is a lifecycle protocol (`Active → Resetting → HeldReset → Initializing → Active`) using the [typestate pattern](02-type-system-core.md); incompatible reset assumptions between components become composition errors. **Committed containment of the indexing blast radius ([OP-2](open-problems.md)):** the epoch is an _ambient implicit_ within a reset domain — elaborated as one hidden epoch parameter per domain, reader-threaded. A signature _surfaces_ an epoch only if it contains a free epoch variable; opaque epoch-carrying types do not surface it. The containment mechanisms are part of the committed design (probe-established 2026-07-17, `probes/epoch-containment/` — the bare rule alone was refuted at 63% clean; with mechanisms, 96%): 1. values received across a domain boundary arrive as existential packages `Stamped`, opened by a scoped `bind epoch` that re-establishes ambient — never as free-variable-indexed types (without this, transport components are _untypeable_: an arbiter holds requests from heterogeneous epochs); 2. allocated-entry references (`TransactionId`) are opaque newtypes whose minting component alone checks epoch/generation validity — stale rejection is a `Result`, not an index; 3. domains declared `no_reset` have the unit runtime epoch and index nothing; 4. raw CDC primitives sit below the epoch abstraction — their reset validity is the `Crosses` bridge contract; 5. reset-phase operations take an opaque linear `ResetWitness` minted once per transition; **unification with the §3 squash contract is now probe-resolved (wave 3, `probes/squash-cdc/`): there is ONE epoch-death contract**, parameterized by the death event (branch squash = suffix of the live chain; reset = the degenerate whole-domain death), the drain clock (local cycles, or far-side response events for crossing capacity), and the bound D — with I1–I5 verbatim and one checker for both instantiations. `ResetWitness`'s linearity is "one death event per assertion"; the recovery epoch is minted at sequence re-entry to `Active` (mid-sequence the domain validly has no live epoch). The drain _channel_ is below the contract: squash drains through normal operation, reset through the reset-sequence protocol, and a response outliving the sequence is dropped by the post-Active tag compare — which is I3 applied to responses, guaranteed by I5, not a new obligation. Components declare one death contract; the separate reset-contract shape is deleted. Types invalidated-by-contract at reset (`QueueToken`) are _not_ epoch-indexed; only values that legally outlive or cross are. Free epoch variables remain exactly where they are load-bearing: signatures relating two or more epoch-bearing values, and the ghost reflection API. **Reset and speculation are one tree (wave 3, `probes/epoch-trees/`):** the reset epoch is the _root_ of the domain's epoch tree and speculation epochs are its descendants; reset **is** the root's subtree squash — the same flush operation and the same five-invariant contract as §3, with no special case (probe-checked: reset mid-speculation turns in-flight launched requests into draining SquashPending tokens whose stale completions are dropped in the new generation — the DMA stale-rejection feature of this section's containment probe is the §3 drain protocol, and the reset drain bound is the same declared D keyed on the reset's death event). Consequently mechanism (v)'s `ResetWitness` reset contract _is_ a squash-contract instance — one mechanism, as anticipated. Treating the two epochs as independent ambient parameters instead is unsound: without the tree edge, a pre-reset speculative value retires under a dead reset generation (machine-refuted, witnesses in 150/150 random traces). Containment is unaffected by the second axis: the ambient remains **one** implicit — the component's current tree position, carried physically as the (reset tag, branch mask) coordinate — and no value legally holds a live speculation coordinate under a stale reset coordinate, because speculation never outlives reset (subtree death). Hence no signature gains a second index, R1 gains the corollary _speculative types are never reset-epoch-indexed_, and the M1–M5 clean-signature counts stand. **Epoch elision is inferred, not written (probe-established 2026-07-17, `probes/pinning-inference/`):** user signatures carry no epoch annotations. Elaboration assigns one epoch metavariable per epoch-indexed signature position and solves **per component against imported summaries only** — a monotone join on a finite lattice (unconstrained < ambient < unpinnable), with same-epoch relations unifying metavariables; port-graph cycles resolve by per-SCC summary fixpoint. Inference is therefore local (a body edit re-elaborates one component; dependents only if its summary changed), deterministic, and **principal**: the least solution is the unique most-absorbed typing. Pinning succeeds only for positions whose index domain is the host domain and whose relation class carries no cross-boundary or outlives-reset evidence; every unpinnable single-occurrence position lowers to `Stamped` automatically (existential introduction is elaboration's job — with it, transport infection cannot occur, even for components generic over domains: domain parameters are rigid, so their positions are never pinnable and absorb existentially for all instantiations at once). A free epoch variable surfaces **iff** a same-epoch relation joins two or more unpinnable positions in one signature, or the signature is the reflection API — the single-occurrence absorption rule, now mechanized (52/52 corpus agreement, 96.2% clean reproduced). Unconstrained positions default to ambient (**pin-unless-forced**); the explicit `stamped` annotation is the override for intentionally epoch-agnostic ports. What remains declarative: R1 (which types index — legally-outlives vs invalidated-by-contract is design intent) and mechanism _selection_; inference decides only ambient / existential / free. ### 5. Reset/clock/power domain typing - Reset domains: polarity, sync/async deassertion, and initialization typing as in `rough-1.md` §6.4 — all Tier-1 checks over nominal domains. - Uninitialized state: `Uninitialized` cannot reach architectural state (P-1); path-sensitive exceptions (mux where the select provably masks the unknown leg) are Tier-2 obligations, not blanket bans. - Power/voltage domains: electrical semantics and implementation remain DEFERRED (D-023); the digital lifecycle/authority contract is a probe-supported north-star schema (D-087). Domain identity generalizes, while level shifter, isolation, retention, DVFS, and RDC claims remain conditional on imported physical evidence. ### 6. Information flow DEFERRED (D-023), by explicit choice: hardware noninterference leaks through timing, contention, and speculation, and doing it honestly is a research program (SpecVerilog — security labels capturing _speculative_ erasure conditions at RTL, CCS 2023 — is the reference point). The systems-safety probe (`probes/observer-flow/`, D-085) fixes the eventual boundary: the reference semantics supplies observer projections, while noninterference is a separate two-run relational contract; architectural implementation equivalence cannot discharge it unless it names the same observer set. Observers form a preorder with incomparability, not one clearance hierarchy, and declassification consumes explicit policy authority. Committed hooks only: the label slot exists in the [semantic ledger](07-compiler-architecture.md), and the authority system above already blocks the _architectural_ speculative-leak channel (speculative values cannot reach externally visible effects without commit authority). One optimizer interaction is named now rather than discovered later: likelihood-driven timing asymmetry (D-071) is a side-channel generator by construction, so wherever labels exist, the `likelihood_timing_secret_adjacent` lint ([14 §14](14-toolchain.md)) watches the intersection. ## North star - Revocation-horizon claims (the precise form of claims-are-commitments: only a claim's pre-launch prefix evaporates on squash) — a performance-only refinement; multipath-fetch commit ordering (the one epoch-tree residue — the squash contract itself is fetch-shape-agnostic and resolved, `probes/epoch-trees/`); and the squash × CDC residue: epoch-tree × CDC, multi-hop crossings, marker-capacity reservation, reset of the bridge itself (the CDC-bridge case itself is now committed — probe-resolved, `probes/squash-cdc/`). - General speculation shapes beyond branch-epoch (value prediction, speculative coherence). - An Iris-inspired resource-algebra semantic core for authority (authoritative queue state + fragments as response rights) as the _model_ under the surface capabilities — never as user-facing syntax. - A generic invalidation kernel shared by reset/speculation, component-local health, mapping, power, and reconfiguration domains without merging their epoch identities. Fault occurrence, detection, correction, containment, and invalidation stay separate; only resource owners inherit conservation/drain obligations (D-081, `probes/fault-health/`). - Information-flow labels riding the ledger slot, SpecVerilog-style, selecting observer-indexed relational contracts rather than becoming ordinary secrecy casts (D-085). - Authenticated lifecycle authorities for scan/debug/trace/fault-injection/ECO effects; DFT insertion must preserve functional and security observers (D-089, `probes/dft-debug/`). - Power and partial-reconfiguration lifecycles where isolation is a crossing authority gate and quiescence is assembled from closed sessions and returned tokens (D-087, `probes/power-reconfig/`). ## Open problems touching this doc [OP-1](open-problems.md) (squash × capabilities — the §3 rule is the committed firewall), [OP-2](open-problems.md) (epoch indexing blast radius — §4 containment is the committed bet). ````