# proposal/03-time-and-resources.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/e6a02b540546a94678ee1108222cd3050d40076f/proposal/03-time-and-resources.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: e6a02b540546a94678ee1108222cd3050d40076f Requested commit: e6a02b540546a94678ee1108222cd3050d40076f Commit: e6a02b540546a94678ee1108222cd3050d40076f Blob: c0c333f9613511a23f725b9d1ffc44a75c3e3d52 Size: 12146 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/e6a02b540546a94678ee1108222cd3050d40076f/proposal/03-time-and-resources.md?format=markdown) ```` # Time and Resources The `Φ` (timing) and `Δ` (capability) judgments from [02 §1](02-type-system-core.md): events, temporal capabilities, guarded feedback, and the separation of the three notions of time. Principles in force: P-2 (cost visible), P-5 (schedules are witnesses, not compiler artifacts). ## Committed design ### 1. Three notions of time — never merged 1. **Logical architectural time** — a partial order over events (`issue(op) < complete(op)`, `commit after execute`). Stable under all optimization. 2. **Clocked schedule time** — events mapped to cycles in a named clock domain (`complete(op) = issue(op) + 3 @ CoreClock`). Changed by retiming/scheduling passes, which must preserve the architectural order. 3. **Physical time** — picoseconds, setup/hold, routing. Never a type; always [evidence](06-refinements-and-evidence.md) (`Measured`, `Estimated`). There is no single `Latency` type. A retiming pass changes layer 2 while a preserved layer-1 relation is its correctness condition ([07 §4](07-compiler-architecture.md)). ### 2. Events as the base timing vocabulary Named symbolic events (`accept(r)`, `issue(op)`, `produce(x)`, `flush(e)`, `reset_release(d)`) with constraints between them; value types carry event indices: `At`, `During`. Absolute stage numbers are sugar for events. Rationale from research: both Filament (intervals relative to events) and Anvil (contracts over abstract time points) demonstrate relative events compose where absolute stages don't. ### 3. Temporal capabilities (D-012) A physical unit is not consumed by use; its availability over time is. The core object: ``` Capability // e.g. WritePort ``` Uses claim intervals; the checker proves non-overlap against the resource's capacity. **Latency and initiation interval are distinct**: `Unit, II<1>>` legally has four results in flight — inexpressible in a consumed-once model, natural here. **Committed scope: static intervals (Filament-lineage).** With delays and offsets static (possibly comptime-parametric), non-overlap collapses to linear integer inequalities — Filament's checker needs no general solver and checks all its benchmarks in under a second; the parametric case (Lilac) discharges symbolic obligations via Z3 in seconds. Both are proven-practical territory. Concretely committed: - per-instance busy intervals with conflict-freedom checking; - delay well-formedness (an event's II ≥ every interval it schedules); - pipelined composition checks (scheduler's delay ≥ scheduled component's delay); - comptime-parametric widths/latencies via Tier-1/Tier-2 [refinements](06-refinements-and-evidence.md). **Committed scope: conditional use.** Conditional uses of one unit generate a Tier-2 disjointness obligation — in general **cardinality form**: _at most `capacity − (unconditional claims)` of the guards may be simultaneously true_, of which the pairwise `is_add(op) ∧ is_addr_calc(op) = false` is the two-claim special case (probe-sharpened wording, `probes/interval-caps/`). This is deliberately _more_ than Filament (which is path-insensitive: shared invocations charge worst-case spans on one event) and is grounded in PDL, whose path-sensitive abstract interpretation over branch conditions, discharged by Z3, handles exactly the conditional-reserve case. The checker only _generates_ obligations; it never schedules ([OP-4](open-problems.md)) — the probe demonstrated the line concretely: the check is a pure function over the design, repairs are suggestion values (move / replicate / guard), and the two tiers exchange exactly one artifact type in one direction. Two probe-found details the one-line rule understates, both resolved in wave 2 (`probes/interval-caps/`, oracle-validated against brute-force unrolled simulation over 3×lcm cycles, 2000 random designs, zero disagreement): - **The modulo-II rule.** A pipelined resource fires at every G + k·II, so a claim `[G+i, G+j)` occupies residues `{(i..j) mod II}` in ℤ/II, and conflict-freedom is capacity-checking at every residue — solver-free and finite because of the `length ≤ II` wellformedness rule, which is load-bearing independently: an overlong claim must be rejected _even when capacity would absorb the occupancy_ (occupancy counting alone provably misses that case). - **II-mismatch composition: reject, never double-book.** An II=2 component under an II=1 schedule is a composition violation, not a capacity problem — raising capacity does not lift it, because what's double-booked is _initiation ability_, and admitting it would force the checker to invent a firing-to-instance binding, i.e. to schedule ([OP-4](open-problems.md)). The two legal encodings — slow the scheduling event, or declare explicit per-instance resources — both check clean. Replication is always explicit. - **Obligation deduplication** (canonical guard multiset + bound as the key) is confirmed load-bearing: 496 → 3 obligations on a 1000-invocation design, 271µs check, verdict-equivalent. Guards are **inferred from branch path conditions** using type-checked variant names — never written by hand a second time (the probe's only bugs were hand-written guard/variant mismatches; a syntax-phase requirement). A discharge-tier `Exhausted` maps to the standard `obligation` outcome. Measured headroom: 500 invocations check in ~114 µs. **Guard inference validated (wave 2, `probes/guard-inference/`, SUPPORTS-SETTLED).** One analysis walk yields both per-use guards and D-069 narrowing facts — provably two projections of one normal form — and its inferred guards are value-identical to the wave-1 hand-written ones, feeding the interval checker unchanged. The structural safety property: **inference failure always weakens the guard, which makes the cardinality obligation strictly harder** — degradation is safe by direction, so `narrow!` is a precision mechanism, never a soundness one. Completeness boundary: 9/12 natural patterns infer exactly (anything testing operands against constants/variants, through let-bound aliases — the dominant decode-dispatch shape); only genuine dataflow (var-vs-var, arithmetic-derived tests, mutation, computed scrutinees) needs `narrow!`, so users encounter it at dataflow boundaries, not per-branch. Mutation between test and use drops the stale conjunct and flags it — a guard never lies. Two implementation notes carried forward: the obligation guard language needs bounded-int atoms (an exact `n ≤ 7` guard is otherwise untranslatable; discharge stays solver-free via representative values), and guard emission wants SSA form first. Syntax-phase recommendation: operand immutability by default deletes the stale-guard class outright. **Dynamic latency (D-034) — via protocols, not intervals.** Variable-latency interaction (cache misses, arbitration) is typed at component boundaries through protocol contracts and outstanding-count refinements ([04](04-protocols-and-streams.md)), not through the interval checker. Anvil shows event patterns with dynamic durations can be typed (event-graph interval containment), but it's a 2025 prototype that _loses to Filament on static pipelines_ (~2× power on a pipelined ALU) — evidence that dynamic-event typing is not yet a free lunch. North star below. ### 4. Schedules are explicit witnesses (D-031) The single strongest lesson from the Bluespec lineage: **never make cycle-level behavior an artifact of opaque compiler analysis.** BSV's ORAAT semantics underdetermines cycle behavior; users demonstrably "code at the compiler," and conflict resolution degrades to stringly `descending_urgency` pragmas. Kôika's fix (user-visible schedule) and Filament's (schedule in interface types) both work; Strata's committed form: ``` Algorithm → Scheduled → Implemented ``` `S` is a schedule witness — produced by the designer, by search, or by an agent, but always _inspectable, diffable, and checkable_ against `A`'s architectural event order. The optimizer replaces `S` freely under the [equivalence-class rules](07-compiler-architecture.md); it never invents unstated cycle semantics. Arbitration among conflicting resource users is likewise first-class (`arbitrate { policy, guarantees, liveness }` — [04 §6](04-protocols-and-streams.md)), never a compiler-chosen urgency order. ### 5. Guarded feedback (D-013, D-029) A register is `delay : (init: T, next: Signal) → Later>`; feedback is legal only through `Later`. An unguarded combinational cycle fails _compositionally_ — a component's feedback port demands `Later<_, T>` in its signature, so safety is known without opening bodies (critical for agent composition). The post-elaboration graph check remains as a backstop. **Committed: single-clock `later` per domain.** Research status is honest here: full clocked type theory exists only inside proof assistants (Guarded Cubical Agda); no programming language ships it. But the unary case — `later` = "next cycle in this domain" — is far simpler, and the comparison point is Clash, where a register-free feedback loop _type-checks_ and manifests as simulation divergence or a synthesis-time combinational loop. Typing causality is a genuine, claimable improvement over the state of practice. Multi-clock guarded quantification (∀κ) is DEFERRED; cross-domain feedback must pass through a typed CDC bridge ([04 §7](04-protocols-and-streams.md)), which sidesteps the multi-clock modality entirely in committed scope. **Calculus-mandated rule (wave 2, `probes/core-calculus/` — a found-and-fixed unsoundness):** the feedback rule requires **FIX-ω** — usage inside a feedback body is ω-promoted, because feedback re-executes every cycle and the naive rule let a 1-graded value be spent once _per cycle_, a bug neither QTT nor guarded recursion alone can express. The corollary is load-bearing and pleasant: ω-graded _periodic_ capabilities (initiation intervals) remain usable in feedback — II is precisely how linearity reconciles with per-cycle reuse. ### 6. Capacity and credits as conserved tokens Queue capacity is linear tokens, not an integer annotation: enqueue consumes `FreeSlot ⊗ Payload → OccupiedSlot`; dequeue returns the slot. Gives no-overflow/no-underflow/no-lost-entry/one-response-per-request as conservation laws the checker tracks structurally. Surface stays ordinary (`queue.reserve()?`); tokens are the elaborated semantics. Under speculation, conservation is _per-epoch_ — `granted(E) = live(E) + retired(E) + reclaimed(E)` — which is exactly the squash-contract form of [05 §3](05-speculation-authority-effects.md). Credit _protocols_ (tokens exchanged across an interface) live in [04 §4](04-protocols-and-streams.md). ## North star - **Dynamic-latency capabilities**: Anvil-style event patterns (`e ▷ #N | ω`) and lifetimes/loans in the event-graph style, once the static-pipeline regression is understood. Entry criterion: expresses a non-blocking cache's response contract without worst-case padding, checked in seconds, without losing Filament-class results on static pipelines. ([OP-8](open-problems.md)) - **Revocable intervals**: capability intervals truncatable by a squash event — the missing piece for speculation ([05](05-speculation-authority-effects.md), [OP-1](open-problems.md)). Confirmed absent from the entire Filament/Anvil line; precedents to reconcile are PDL's speculation contracts and HazardFlow's discard-and-restart hazard interfaces. - **Cross-stage hazard interfaces**: HazardFlow's observation that stall/bypass/restart create dependencies per-module interval typing can't modularize is a standing challenge to our composition story; track it explicitly during phase-2 probing. - Placement/locality as coeffect-style implementation constraints (`requires placement_distance(rf) <= D`) — obligations for the physical flow, never type equality. ## Open problems touching this doc [OP-1](open-problems.md), [OP-4](open-problems.md), [OP-8](open-problems.md). ````