Syntax-Phase Requirements Ledger

Input artifact for 16-syntax.md (the surface design). Compiled from the original 17-probe syntax wave (2026-07-17), the ten systems-safety probes (2026-07-21), the proposal docs' sketched forms, and the toolchain constraints. Every entry cites its source. Taste forks (§4) go to Veronica with previews; everything in §1–§3 is evidence, not taste. R37–R50 are semantic pressure on the next syntax revision, not settled spellings.

1. Hard requirements from probes

Guards, path conditions, mutability

• R1. Operands immutable by default; SSA before obligation emission. "Operand immutability… deletes the stale-guard class at the syntax level, which is the cheapest possible fix"; elaboration SSA-renames before obligations. (probes/guard-inference/; committed in 03 §3.)
• R2. Variant names type-checked at every mention; guards never written at the claim site. Wave-1's only bugs were hand-written variant-index typos; guards are inferred from the enclosing if/match path condition. (probes/interval-caps/, probes/guard-inference/.)
• R3. Inference-reliable forms must be the idiomatic forms: match over operands; variant-set tests op is Load | Store closed under &&/||/!; let-bound predicate aliases; comparisons vs comptime constants; early-exit if bad { return }; comptime for with the loop var in indices. Steer let d = decode(raw); match d { … } over match decode(raw). (probes/guard-inference/.)
• R4. narrow!(cond) ergonomic exactly at dataflow boundaries, diagnostic quoting the dropped conjunct verbatim. (probes/guard-inference/.)
• R5. Guard/obligation display renders sets, not disjunctions (op ∈ {Load, Store}); at_most = 1 renders as "mutually exclusive". (probes/guard-inference/, probes/interval-caps/, probes/core-calculus/.)
• R6. Obligation identity includes the harvested path condition — render it: "discharged under condition opcode==Add; unconditional claim still open." (probes/core-calculus/ wave 3.)

Refinement-predicate surface

• R7. Infix Presburger refinements (AST builders were ~3× keystrokes); mod/div restricted to constant right-operands by the grammar — the Presburger fence is syntactic, not a checker error. (probes/protocol-catalog/.)
• R8. Monus vs checked subtraction forced explicit — monus silently absorbed a near-bug (blocked := valid − ready); struck twice. (probes/protocol-catalog/, probes/protocol-catalog-chi/.)
• R9. prev(x) / latched sugar for two-cycle temporal refinements, else stability refinements become hand-managed ghost counters. (probes/protocol-catalog/.)
• R10. repeat N in protocol bodies — last-beat guards were off-by-one bait; counters stay internal. (probes/protocol-catalog/.)
• R11. Conditional-refinement sugar (if broadcast { snpSent = N-1 }). (probes/protocol-catalog-chi/.)
• R12. Named invariants mandatory in bundle syntax — cross-invariant diagnostics fall out of naming (P-9). (probes/protocol-catalog/.)

Protocols, sessions, ordering

• R13. session<line = addr div 64> { binds txn } — declarative per-message key bindings, plus per-message key/field mapping (key by tgt on one message, src on another). (probes/protocol-hazards/, probes/protocol-catalog-chi/.)
• R14. key_set = lines(addr, len) syntax — one event joining k keyed orders; start-line-only keying is machine-refuted. (probes/protocol-hazards/.)
• R15. related_by relations required symmetric or checked both orientations. (probes/protocol-hazards/; normative in 04 §4.)
• R16. Shared protocol-level constants (granule) — line size appeared twice, would drift. (probes/protocol-hazards/.)
• R17. Explicit quiescence-point notion for session composition (mid-trace vs end-of-trace acceptance). (probes/protocol-catalog-chi/.)
• R18. from/to role tags on protocol messages even pre-phase-3 — role-less dir: was pure noise; binary dual is no participant's view of a 3-role body. (probes/protocol-catalog-chi/.)

Widths and comptime

• R19. DEPTH: Nat1 (or where DEPTH >= 1) as the path of least resistance — positivity converts the clog2 cliff into proofs. (probes/width-algebra/.)
• R20. "Left Presburger" fix-it for reflect on Var·Var; constant-multiply vs general multiply distinct at the surface or via fix-it. (probes/width-algebra/; 02 §4 clause 6.)
• R21. clog2 spelled as HDL users expect; interpreted-symbol set documented closed. (probes/width-algebra/.)
• R22. Budgets syntactically declaration-attribute-only (no raise API as a syntactic fact); discharge predicates barred from remaining(). (probes/exhaustive-discharge/.)
• R23. Derived-bound discharge result type has no overrun constructor; ineligibility routes to the declared path; product domains use entry-function parameters. (probes/static-eval-bounds/.)

Epochs, speculation, reset

• R24. stamped T one-keyword override on port types; users never write Stamped<T,D> — elaboration introduces it. (probes/pinning-inference/.)
• R25. bind epoch as a match-like fresh/stale form (match rebind(x) { Fresh(v) => …, Stale(x) => … }); rebinds the whole coordinate — the (tag, mask) pair is elaboration-only. (probes/epoch-containment/, probes/epoch-trees/.)
• R26. same_epoch(a, b) obligation atom as the surface source of SameEpoch evidence. (probes/pinning-inference/.)
• R27. Crosses<A,B> vs Stamped redundancy owned by elaboration. (probes/epoch-containment/.)
• R28. ResetWitness name kept at reset sites, judgment unified with squash contract; many-flush-site &ResetWitness needs a worked ω-borrow-during-Resetting rule. (probes/epoch-trees/, probes/epoch-containment/.)
• R29. Token states carry both facets structurally — SquashPending lacks the authority interface, never parallel booleans; ghost death-event state nameable in the 07 contract format. (probes/squash-semantics/, probes/squash-cdc/.)
• R30. CDC mirror-chain synthesized from bind epoch over a stamped stream (~40 hand-written lines otherwise, with a real Kill-sweep-order bug); Resolve/Kill minted from one linear epoch-resolution capability. (probes/squash-cdc/.)
• R31. CommitProof documented as "path fully resolved"; mask width is an ordinary capacity bound, no new syntax. (probes/epoch-trees/.)

Grades, linearity, diagnostics

• R32. Failure-arm disposition errors point at the offending arm, not GradeMismatch used=ω at the binder. (probes/core-calculus/.)
• R33. "Monitors watch wires, they don't take tokens" — the mandated diagnostic for linear values in state-refinement bounds. (probes/core-calculus/ wave 3; 02 §3.)
• R34. N-ary destructuring — right-nested ⊗ is clumsy. (probes/core-calculus/.)
• R35. Region markers for observational-equivalence bounds (elastic / cycleobs) as surface constructs. (probes/eclass-rewrite/.)
• R36. Peripheral but binding: pass declarations 5–8 lines with per-category verbs (probes/ledger-passes/); semver spec ships a polarity table + "strictly refining" + canonical encoding (probes/summary-semver/); pinning diagnostics render the forcing-evidence provenance chain (probes/pinning-inference/).

Systems safety and custody

• R37. Fault contracts separate five named moments: occurrence, detection, correction, containment, and invalidation/recovery. Syntax must not collapse detected into contained. (probes/fault-health/, D-081.)
• R38. Health epochs are nominally distinct from reset/speculation epochs while sharing an elaboration-only invalidation kernel; stale/repaired/independently-validated dispositions must be nameable. (probes/fault-health/.)
• R39. DMA accepts a borrowed mapped-region capability, never a raw integer address authority. Region parameters include address space, permission, owner, lifetime, and opaque mapping generation; issue-time snapshots are explicit in the contract IR. (probes/dma-iommu/, D-082.)
• R40. Blocking operations name held resources and release events; assumptions name owners. Progress declarations expose fairness class, ranking/escape evidence, and proved/refuted/obligation, with finite bounds syntactically distinct from eventual progress. (probes/progress-waitfor/, D-083.)
• R41. Memory models use first-class event/relation declarations for po, rf, co, dependencies, fences, atomicity, and visibility; every partial export has an explicit completeness marker. They do not hide inside protocol syntax. (probes/memory-consistency/, D-084.)
• R42. Observers are named projections, not security labels. Two-run noninterference and one-run implementation equivalence require distinct declarations; declassification consumes named authority. (probes/observer-flow/, D-085.)
• R43. Physical exceptions have intended and bound phases. A source false_path/multicycle declaration denotes a candidate with a schedule/stability witness; a backend-bound manifest and validation result are separate artifacts. (probes/physical-constraints/, D-086.)
• R44. Power domains are lifecycle protocols, not annotations: Off → Isolated → Retained → Powering → Resetting → Active, with typed transition authority, crossing isolation, retention validity, and DVFS evidence expiry. (probes/power-reconfig/, D-087.)
• R45. Reconfiguration regions expose quiescence, ABI refinement, authenticity/target evidence, and a fresh region generation. No live session/token may cross replacement. (probes/power-reconfig/.)
• R46. Numeric types spell unit, scale, rounding, and overflow policy; contracts spell error budgets, correlation, range, and calibration freshness. Approximation is an evidence-producing transform, not implicit arithmetic. (probes/numeric-error/, D-088.)
• R47. Debug, scan, trace, fault injection, test mode, and ECO writes are distinct scoped authority effects. Authenticated lifecycle transitions mint them; production-unreachability and secret/scan policy are expressible claims. (probes/dft-debug/, D-089.)
• R48. Assurance declarations name hazards, guarantees, assumptions, owners, artifacts, expiry, and residue, but cannot inhabit an evidence position. Self-citation must be unrepresentable. (probes/assurance-cases/, D-090.)
• R49. Optional contract families remain visibly opt-in. Their syntax belongs on component/contracts, not on every signal/type, and absent families emit no placeholder obligations. (All ten systems-safety probes; P-13.)
• R50. Every external artifact reference carries content hash plus relevant tool, target, mode, and design pins. Expiry/invalidation is declarative and machine-diffable. (probes/physical-constraints/, probes/assurance-cases/.)

2. Already-sketched surface forms (provisional notation of record)

• Stream declaration — stream LoadRequests { payload:, domain {}, protocol …, flow { acceptance: at_most 1/cycle, outstanding: 0..=8 }, identity {}, ordering {}, authority {} } (04 §8).
• Protocol declaration — protocol Burst<const N: usize, T> { send Header { length: N }; repeat N { send Beat<T>; } recv Completion; } (04 §2); catalog forms ready_valid { payload_stable_while_blocked }, credit<N>, burst<N>/burst_dyn { max_len }, request_response { matched_by: Id, faults: allowed }, Process<During, Success, Failure>; operators bundle, layer, session<key>, hazard_lock (04 §1).
• Ordering relations — PreservesOrder<Input.Accept, Output.Transfer, key = TxnId>, CommitsIn<ProgramOrder>, related_by = overlaps(a, b) (04 §4).
• Arbitrate — arbitrate { inputs:, eligibility: |r| r.ready, policy: oldest_first(key = r.age), resource:, guarantee { … } liveness { … } } (04 §6). Internal inconsistency: guarantee{}/liveness{} have no :/comma unlike other fields.
• Requires tiers + discharge — requires static { … } / requires solve { … } / requires prove { … }; discharge by comptime_exhaustive(opcode: Bits<7>); narrow!(p) (06 §1).
• Evidence/contracts — guarantee no_duplicate_response evidence: Tested<…>; require guarantee G with evidence >= BoundedProved (06 §3–4).
• Suppression — expect(lint = …, reason = "…", evidence = …, review_by = edition(2028)) (14 §10).
• Comptime — comptime param STAGES: Nat in 1..=6, comptime fixed DEPTH: Nat = config.queue_depth, comptime for, lower { }, ResourceCtx (07 §7).
• Phase operators — reflect, reify, symbolize, observe (02 §2).
• Time — delay(init, next) -> Later<Clock, Signal<T>>; At<T,E>, During<T,[E1,E2)>; Capability<Resource, [Execute+2, Execute+3)>; Algorithm<A> → Scheduled<A,S> → Implemented<A,S,I> (03 §2–5).
• Iteration forms — comptime for, combinational_fold, pipelined_fold::<Stages<K>>, sequential_fold (02 §7) — turbofish already sketched, as in cross_clock::<B>(bridge) (04 §7).
• Types — Bits<N>, UInt<N>, Index<N>, OneHot<N>, Encoded<T,E>, Occupancy<0..=CAP>, Handle<R,Slot,Gen,Epoch>, Stamped<T,D>; named ops wrapping_add/full_add/checked_add; conversions wrap_to/saturate_to/checked_to/sign_extend_to (02 §4).
• Declarations — clock_domain { … }, opaque type TransactionId = Bits<8>, sealed interface, no_reset, granular unsafe <category> (02 §5/§8, 05 §4, 06 §5).
• Speculation — Speculation<E> { predict:, allocate:, write_internal: }, commit(v, proof), cancel(epoch, token), bind epoch (05 §2/§4).
• Attributes — #[encoding(auto where preserves_debug_identity)] (one sighting, 02 north star); D-044 budgets need a spelling; experiment declarations named but never sketched (10 §3). Combinators map/filter/zip/buffer/batch/broadcast/tap/partition, queue.reserve()?, ?-style stall/fault propagation (04 §5, 03 §6, 02 §10).

3. Formatter/parser constraints on syntax (from 14-toolchain.md)

• Trailing-comma steering (§2) requires comma-separated, trailing-comma-legal lists in every braced construct — the protocol sketch's semicolons and arbitrate's bare blocks conflict; pick one list discipline; every {} body needs a defined one-per-line form.
• No alignment, one entry per line, 100 cols (§1, §3): no construct may depend on columnar layout (decode tables must read one-entry-per-line); no fmt: off escape hatch exists.
• fmt never inserts steering tokens (§2) — the trailing comma must not be semantically significant.
• Provenance stability (§4): no layout-sensitive literals; anonymous inline constructs need deterministic emission indices (R12's mandatory names help).
• Resilient-LL + lossless tree (§16): distinct leading keywords per declaration form are good anchors; local error containment; comments are anchored trivia — no column-significant comments.
• Tree-sitter co-grammar (§18): no context-sensitive lexing — indicts raw </> generics lexing; turbofish is the sketched mitigation; the fork is F3.
• Semantic tokens carry phase modifiers (§19) — phase must be syntactically recoverable per token (from binder form, not whole-program inference).

4. Open taste forks (to Veronica, with previews)

• F1 — component vs module vs entity. Lean: component (prose consistency).
• F2 — hardware binding keyword: let/signal/wire; R1 forces immutable-by-default regardless; phase-token rendering mildly favors distinct binder forms per phase.
• F3 — generics delimiters: [] vs <>+turbofish vs <>+call-syntax. Technical lean against raw <> (lexing ambiguity vs §18); infix Presburger must stay legal inside type arguments (R7, R19).
• F4 — statement terminators: semicolons vs newline-significant. Declaration bodies should be comma-lists regardless (fmt steering).
• F5 — expression-orientation: R3/R11 lean into match/if as expressions.
• F6 — attribute syntax: #[…] vs @…; must be LL-anchored, declaration-position-only for budgets (R22).
• F7 — literals: no Verilog 7'b… context-sensitive lexing (§18); width from the type, explicit conversions (D-030/D-040).
• F8 — capitalization: codify the de-facto CamelCase types/variants, snake_case fields/functions, lowercase keywords.
• F9 — checked-vs-monus spelling: named methods match the wrapping_add family (lean) vs operators (-|).
• F10 — positivity spelling: Nat1 type vs where DEPTH >= 1 clause; must be the path of least resistance, not an expert annotation.