# proposal/15-syntax-requirements.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb/proposal/15-syntax-requirements.md)

Repository: [versecafe/strata](https://git.cafe/versecafe/strata)

Visibility: public

Requested revision: 7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb

Requested commit: 7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb

Commit: 7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb

Blob: 150fbcead9ec095ac41aaa020f6a03d931cdc69d

Size: 16855 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/7eadab2a0cb1cd9f2bb8ebfe16a5fc70d4c478fb/proposal/15-syntax-requirements.md?format=markdown)

```
# 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.

```