Time and Resources

The Φ (timing) and Δ (capability) judgments from 02 §1: 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 (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).

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<T, E>, During<T, [E1, E2)>. 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:

Uses claim intervals; the checker proves non-overlap against the resource's capacity. Latency and initiation interval are distinct: Unit<Latency<4>, 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.

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

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; it never invents unstated cycle semantics. Arbitration among conflicting resource users is likewise first-class (arbitrate { policy, guarantees, liveness } — 04 §6), never a compiler-chosen urgency order.

5. Guarded feedback (D-013, D-029)

A register is delay : (init: T, next: Signal<T>) → Later<Clock, Signal<T>>; 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), 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<Id>; 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. Credit protocols (tokens exchanged across an interface) live in 04 §4.

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)
• Revocable intervals: capability intervals truncatable by a squash event — the missing piece for speculation (05, OP-1). 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, OP-4, OP-8.