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<S>, Writes<S>, Allocates<R>, Releases<R>, Sends<P>, Receives<P>, Raises<E>.
• Temporal — how the operation occupies time/resources: Combinational, Registers<Clock>, Schedules<R, Interval>, Crosses<A,B>, MayStall. (These are requirements/coeffects — they consume capabilities, they don't mutate state.)
• Authority — what privilege is required: Requires<CommitAuthority>, Requires<ResetAuthority>, Requires<ExternalVisibilityAuthority>.

Effect rows are inferred bottom-up and appear in component summaries; 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<T, Epoch> / Committed<T> / Architectural<T> — but the tag is not the mechanism. The mechanism is which effects are authorized under which epoch:

Epochs are generative (02 §5); 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<E> 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<E> 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 for the bridge-as-carrier clauses.

This resolves OP-1 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<OldEpoch>, QueueToken<OldEpoch>, Speculation<OldEpoch>). Reset sequencing is a lifecycle protocol (Active → Resetting → HeldReset → Initializing → Active) using the typestate pattern; incompatible reset assumptions between components become composition errors.

Committed containment of the indexing blast radius (OP-2): 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<T, D>, 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<A,B> 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<T, D> 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<T> 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, 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) 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 (squash × capabilities — the §3 rule is the committed firewall), OP-2 (epoch indexing blast radius — §4 containment is the committed bet).