Committed-Core Surface Syntax

The complete surface for Strata's committed core, designed against 15-syntax-requirements.md R1–R36 and reconciled from the syntax probe wave: probes/syntax-grammar/ (resilient-LL + tree-sitter grammar, 26 GAP designs), probes/syntax-corpus-core/ (hardware corpus, 31-entry gap ledger), probes/syntax-corpus-verif/ (verification/protocol corpus, G-S1–G-S38). Charter picks (D-077) are SETTLED; reg forms are SETTLED (D-079); the grammar-evidence decisions are SETTLED (D-080). The whole document is DRAFT-COMPLETE (D-078) pending the fmt dry-run and blind-regeneration passes. Standing tiebreaker: Rust style when unsure.

The 2026-07-21 systems-safety wave added requirements R37–R50 but did not run a syntax/corpus probe for them. This document therefore does not pretend to settle spellings for health contracts, mapping leases, progress summaries, memory events, observers, power/reconfiguration, physical certificate binding, numeric budgets, DFT authority, or assurance cases. Their architectural homes and syntax constraints are settled provisionally; their surface forms require a dedicated corpus, grammar, formatter, and blind-regeneration wave before joining this specification (D-091).

1. Design rules

1. Ride the Rust distribution (P-11): agents are the first users; ~55% of LLM Verilog failures are syntax-class errors concentrated where Verilog diverges from software convention — divergence from Rust is spent only on hardware semantics (component, inst, reg, domains, events, protocols).
2. Keyword-anchored, locally resolvable: every major form opens with a unique keyword — resilient-LL recovery points, tree-sitter fidelity, and generation commitment points are the same property. No symbol-operator polysemy (Chisel's :=/<> zoo is the cautionary tale).
3. Redundancy that checks: named-only connection, named invariants, mandatory reasons — every redundant name is a slot where a hallucinated connection fails loudly. Never make anyone write the same fact twice unchecked: infer it or check the duplicate (R2).
4. No layout semantics: explicit terminators and braces survive generation truncation and keep D-052 structural identity trivial.
5. One way to write each thing: where sugar exists (punning, elided clocks, T @ 'E) it is the fmt-canonical form, so corpus and formatter agree.

2. Settled charter (Veronica, 2026-07-17) + D-079

3. Lexical structure

Identifiers. [A-Za-z_][A-Za-z0-9_]*. Convention (lint-enforced, not grammar): CamelCase types/variants/evidence constructors, snake_case values/functions/schemas, lowercase keywords.

Apostrophe labels. 'ident is one token: temporal validity — clock domains ('core) and events ('Exec) share the grammar, deliberately resonant with Rust lifetimes. There are no char literals; 'x is always a label.

Keywords (hard-reserved). Every form-opening word plus the four soft keywords the grammar probe flagged as recovery hazards (state, on, preserve, at_most — D-080):

(while reserved unused, Rust-lean.) Soft (position-only) words, ordinary identifiers elsewhere: param, fixed, reset, related_by, key_set, binds, scope, over, under, evidence, assume, guarantee, liveness, arbitrate, sweep, as, at, cycle and the unit idents. narrow, weighted, config are special only as ident!.

Integer literals. Unsuffixed integers are static-phase polymorphic naturals checked to fit exactly (too wide = error, never truncation — D-030); 0x/0b/decimal with _ separators. No tick-literals ever (8'hFF needs context-sensitive lexing and truncates silently — D-048). Explicit form where inference is absent: UInt::<8>(0xFF).

Quantity literals (verif corpus, G-S5): NUMBER unit where unit comes from the closed, edition-versioned unit table, legal only in quantity positions (evidence arguments, flow entries, #[schedule], experiment entries): 17.2e9 txns, 842 MHz, 1/cycle. N/cycle is a grammatical Rate, not division — / exists nowhere else in the language. Decimal-fraction/exponent numerals (17.2e9, 0.3, 1.0e-6) are legal only inside quantity and metadata positions; there are no hardware floats.

String literals. Metadata positions only (reason =, attribute args, tool versions like "vivado-2026.1" — bare vivado-2026.1 is lexer poison). No hardware string type exists.

Comments. //, /// doc (item-anchored), //! module doc — anchored trivia per D-053; never column-significant.

The > discipline (D-080). The lexer never emits >> or >=: it emits single > (and =); the parser glues byte-adjacent > > into shift and > = into >= in expression-operator position only. Consumer<ready_valid<T>> needs no splitting — each > closes one level. <, <=, <<, ::< lex directly. ..=/.. are single tokens. No context-sensitive lexing anywhere (the tree-sitter co-grammar, D-066, depends on this).

4. Items

Every item form opens with a unique keyword (design rule 2). Items take #[attributes], /// docs, and visibility pub / pub(package) (module-private default; pub(crate) etc. deferred).

component — value-flow: inputs are parameters, the output is the return type. Multi-output components use named tuple returns (G-S35: contracts and require guarantee must name outputs):

Statefulness is visible at the use site: components instantiate with inst, functions call bare. A component's operation surface (port items, §5) is reachable through a borrowed handle parameter table: &TxnTable; an inst value coerces to its value-flow result where one is expected (core G19). Item-position unsafe surface: pub unsafe(clock_crossing) component AsyncFifo<'src, 'dst, T, const DEPTH: Nat1>(...).

fn / comptime fn — pure/combinational functions and generators. ghost fn declares monitor-phase functions (relations, predicates); refinement/ghost integers are mathematical, so bare - is legal there (never on hardware integers, R8).

interface / sealed interface / impl — Rust-trait-shaped (D-038): member fn ...; signatures, associated type Grant;, impl Path for Type { }. sealed interface is the protocol-catalog mechanism.

enum — Rust bodies plus explicit encodings (G-S1): the ascription makes it Encoded<Opcode, Bits<7>> — encoding is semantics, not a #[repr] layout hint. Discriminants checked to fit exactly.

struct — Rust bodies, comma-lists, unit structs struct Active;, grade-0 phantom type params legal unused.

opaque type / type alias — pub(package) opaque type TxnId = Handle<...>; (declaring module owns mint/open); plain pub type Addr = UInt<44>;.

const — const TXN_ENTRIES: Nat1 = 16; — item-position, implicitly static-phase (comptime let is the body-local form).

clock_domain — declared once, referenced by name (R2): clock_domain core { clock: CoreClock, reset: CoreReset { polarity: active_low, deassert: sync }, }; no_reset as a marker entry declares a reset-free (unit-epoch) domain.

resource — resource adder: Unit<Latency<0>, II<1>> = share(wrapping_add); — abstract, = share(f) bound, or arrays [Unit<...>; N] = replicate(f) (replication always explicit).

protocol / bundle / stream — §10. state_machine / strategy fn / property / differential_test / experiment — §11.

use / mod — Rust use-trees (use a::b::{C, D};, ::*, as); pkg:: is the current package root; pub mod x; + pub use re-exports define the package surface (13 §6).

discharge — statement-positioned, §5.

Instantiation is named-only with punning — positional connection does not exist:

One protocol-connect form, checked by duality (04 §3): passing a producer value to a Consumer<P> parameter is the connection. A standalone connect statement was drafted in the core corpus and never needed — rejected (§15).

5. Statements

Component/fn bodies are statement lists terminated by ;; block-like expressions (match/if/for/domain/blocks) in statement position take no ;. Comma-lists are reserved for data-shaped braces (struct/enum/contract/arbitrate/protocol/bundle/stream/clock_domain bodies) — the two disciplines never share a brace pair.

* reset(v) is mandatory unless the ambient domain is no_reset or the register is explicitly uninit (02 §6). Unwritten paths hold. reg is never inferred from code shape (kills latch inference and blocking/nonblocking outright).

Obligations and discharge (named forms — verif G-S2/G-S3; ; canonical, D-080/GAP-19):

Names are mandatory on solve/prove (discharge and diagnostics address by name), optional on static. The binder on the requires is the finite domain the discharge strategy enumerates. narrow!(cond); at dataflow boundaries only (R4); the weakened-guard diagnostic quotes the dropped conjunct. require guarantee mem.no_duplicate_response with evidence >= BoundedProved; states a consumer's evidence floor (§11).

Pipeline and time. stage; is the bare separator; stage 'Name; additionally binds the event label used by .at('Name) claims. Values crossing a stage; are auto-piped; inserted registers are named in the structure report. Region markers: elastic { ... } (TransactionEquivalent bound) and cycleobs { ... } (CycleExact), R35.

Multi-cycle control (core G24): sequence { ... } elaborates to an FSM; await bool_expr; waits; await process_expr runs a Process to completion yielding Result<S, F>; halt diverges (types as !); loop { } as in Rust. Typestate transitions construct Process values with the process { step:, done:, ok:, err:, } block (core G23).

Handshake endpoints (core G11/G12): the value-flow introduction/elimination forms for protocol endpoints —

accept returning Some implies the ready expression held that cycle (a stated protocol-semantics fact feeding guard inference).

Other statements: port name(args) -> Ret { body } (component-body only; elaborates to a request_response endpoint; body-less port log(pkt: stamped TracePkt); declares); domain 'core { ... } blocks (expressions; escaping values carry their domain tag); unsafe(category, reason = "...") { expr } granular unsafe; return expr;; assert expr; (ghost/test phase only); contract { ... } blocks (§11); resource declarations; expect exists only as the #[expect] attribute (§9), never a statement.

6. Expressions

match/if are expressions (R3/R5); blocks yield their trailing expression. Variant names resolve against the scrutinee's declared enum type (R2).

Precedence (low → high; comparisons non-associative, Rust-lean):

• Variant-set tests: op is Load | Store, closed under &&/||/! (R3); diagnostics render op ∈ {Load, Store} (R5). Idiom the docs and lints teach: bind then match — let d = decode(raw); match d { ... } — let-bound scrutinees and predicate aliases are what guard inference traces.
• Arithmetic is named methods: wrapping_add, full_add, checked_add, saturating_add; subtraction forces the choice — checked_sub (Option) vs monus (floors at zero). Conversions: wrap_to::<N>(), saturate_to, checked_to, sign_extend_to (no as). No compound assignment (+=) — exception: session counters (§10), which are math naturals.
• Bit slicing: little-endian bit weight, half-open ranges — x[0..8] is the low byte, x[msb] sugar; never Verilog [7:0]. x[0..k] ++ x[k..N] widths sum. Named Encoded fields displace raw slicing (lint on raw slices of typed values).
• ? propagates stall/fault through the canonical Bypass/Poison node: a Bubble<T> unwraps or kills the dominated region; Bubble::of(x) re-wraps (core G28). Also queue.reserve()?.
• Turbofish is mandatory in expression position (UInt::<8>(0xFF), x.wrap_to::<4>(), overlaps::<W> inside relation args — F15's fix-it: "expression position: write ::<"). Domain labels ride along: AsyncFifo::<'core, 'dbg, T, 8>.
• Event expressions: 'Exec, 'G + 2; resource claims adder.at('Exec)(a, b) — guards on conditional claims are never written (R2), they are inferred from if/match path conditions and rendered in set form with the harvested path condition (R5/R6).
• Struct literals are FORBIDDEN at the top level of if/match/for headers and match-arm guards (D-080; Rust's rule): if x == S { } parses S as a path and { } as the body; parenthesize to opt in — if a == (Grant { slot: 0 }) { b }. Functional-record-update ..rest is legal (CacheAddress { offset: 0, ..arbitrary() }).
• arbitrate is an expression — a named architectural node whose output flows on (G-S23, resolving both 15 §3 flags: guarantee/liveness join the comma-list with mandatory names; eligibility/keys are explicit closures, never a magic r):

• Predicate position shares the expression grammar with two deltas: implication sugar if cond { pred } means !cond || pred (R11; predicate position only — the expression-side error must say so), and div/mod keep the syntactic fence. Interpreted predicate symbols (closed set): clog2, max, min, prev (R9 stability), accepted, transferred, outstanding, same_epoch.
• Phase operators are plain calls: reflect(x), reify(x), symbolize(x), observe(x).

7. Types

• Generic parameters: type params with Rust bounds T: Ord + Encode; const params const DEPTH: Nat1 with optional ranges const N: Nat in 1..=6; label params 'src, 'dst (domains/events — the Rust-lifetime grammar accepts all four positions unchanged: params, type args Epoch<'core>, signal prefixes x: 'core Bool, turbofish).
• where takes both interface bounds and Tier-1 infix predicates: where DEPTH <= 1024, T: Encode (D-080: bound-vs-predicate needs LL(2), committed). Where-lists take no trailing comma (not a braced body).
• Positivity is a type (R19): Nat1 is the standard depth/count parameter type (where N >= 1 also legal; Nat1 is the path of least resistance). Width expressions in <> follow the D-037 closed algebra (clog2/max/min spelled exactly so, R21); leaving it triggers the "left Presburger" fix-it (R20).
• The angle-bracket sub-language (D-080): inside <...> the grammar excludes comparisons, shifts, &&/||, and struct literals, so > always closes and , always separates — bare <> in type position needs no symbol table and no brace fallback. A bare path argument is type-or-const until name resolution (as in Rust). Trailing commas are legal in <> lists (fmt wrap rule, §13). Schema config blocks are type-position only: burst_dyn<Flit> { max_len: 8 } (expression position would collide with struct literals — same class as the header rule).
• Refinement types: Occupancy<0..=ENTRIES> (state refinement, 06 §1), Index<N>, Bits<N>, UInt<N>, OneHot<N>, Gray<N>, Encoded<T,E>, Handle<R,Slot,Gen,Epoch>.
• stamped T — the one epoch keyword users write (§12). T @ 'E availability sugar for At<T, 'E> is adopted (§15): it parsed cleanly through both grammar implementations and is the fmt-canonical form; annotation only for deviation from the ambient stage.
• Endpoints: Consumer<P> / Producer<P> for binary protocols; View<Bundle, Role> is the per-role projection for ≥3-role bundles (G-S22; binary duality is provably no participant's view of a 3-role body).

8. Patterns

Rust patterns: _, literals, ranges 0..=3 =>, or-patterns A | B, tuple (n-ary, R34), Path(p1, p2), Path { field, .. }, mut x, if let. A bare lowercase path binds; a bare CamelCase path is a unit variant, resolved against the scrutinee's declared enum (R2 — wave-1's only bugs were hand-written variant-index typos). Match arms: Pattern [if guard] => expr, — exhaustive over enums; arm attributes legal.

9. Attributes and the Meta micro-grammar

#[attr] (F6, tiebreaker), declaration-position only. The Meta micro-grammar is committed (D-080 — attribute/expect metadata is structured, never a balanced-token soup):

The canonical inhabitants:

• #[budget(comptime_steps = 20_000_000, per_eval = derived)] — budgets are attributes and only attributes (R22); no raise API exists syntactically; per_eval = <n> is the declared-path override (R23).
• #[schedule(latency <= 2, throughput >= 1/cycle)] — on architectural nodes.
• #[expect(lint = ..., reason = "...", evidence = ..., review_by = edition(2028))] — suppression (D-057); on any item, statement, or declaration entry; never an inner attribute; one lint per attribute (G-S30).
• #[derive(Pack, Arbitrary, Shrink, Waveform, Symbolic)] — the five artifact families (08 §1).
• #[metamorphic(relation = f)], #[symmetric] (checked, R15), #[encoding(auto where preserves_debug_identity)].

10. Protocols, sessions, ordering

Two protocol dialects, one item (G-S10 rule; never mixed in one body): role-less binary bodies use the sequential dialect; bodies declaring roles use the msg + state session dialect.

Sequential dialect (catalog-style):

Session dialect (D-027's first customer — roles, families, ghost state, guarded FSM):

Counter updates after the target state are name = e / name += e (-= never arises: math naturals, total assignments or increments). from/to tags are mandatory once ≥2 roles exist (R18).

bundle — channels with roles, shared constants, cross-channel invariants (named, R12), session attachments, and quiesce points:

The session<key = expr> clause is its own mini-grammar (a diagnostic label binding, not generic args — tree-sitter uses a dedicated session_key node).

Ordering — a bundle/stream clause: PreservesOrder<A.Accept, B.Transfer, key = TxnId>, group = id, related_by = overlaps::<W> (relations #[symmetric]-checked, R15), key_set = lines(addr, len) (R14 — one event joins every keyed order; start-line-only keying is machine-refuted), CommitsIn<ProgramOrder>. Relation args are the most heterogeneous bracket context in the language; they get a dedicated relation_args production (F12).

stream — every entry name: value, (G-S36): payload:, domain: Core (a clock_domain reference), protocol: ready_valid { payload_stable_while_blocked }, flow: { acceptance: at_most(1/cycle), outstanding: 0..=8, latency: dynamic }, identity:, ordering:, authority: { speculative: BranchEpoch, cancellation: BranchRecovery }.

11. Verification surface

contract blocks (core G13 + verif G-S4 merged) — component-body position, comma-list entries, three entry kinds plus flavors:

claim carries physical facts — evidence about an artifact, never a guarantee of the term (D-075). Evidence literals: Ctor<args> with quantity literals, idents, name = literal pairs, strings (G-S5); evidence is a set (D-017), bracketed. Contract predicates take the ports/outputs they constrain — which is what forces named returns (G-S35). Inside contracts and requires, result names a single anonymous output (core G14).

Consumer evidence floor: require guarantee mem.no_duplicate_response with evidence >= BoundedProved; — >= compares against the set's best entry on the relevant axis.

Obligations: requires static/solve/prove + named discharge (§5). State refinements over runtime values are 06 §1's second sort; "monitors watch wires, they don't take tokens" (R33) fires on linear values in bounds. Failure-arm disposition diagnostics point at the arm (R32 — checker duty).

Generators: strategy fn name(state: &Model) -> T { ... } with weighted! { 25 => e, ... } arms (G-S24); generator binders param in strategy_expr in rule/property parameter lists, bare name: Type = the type's derived default strategy (G-S25).

state_machine (rule-based lockstep testing, G-S26 — distinct from session FSMs):

property — #[metamorphic(relation = f)] property name(binders) { stmts; assert rel(a, b); }. assert is the ghost/test-phase assertion (hardware claims stay requires/narrow!).

differential_test — comma-list block: dut: RvCore::<Rv32iMinCfg>, reference:, interface:, lockstep:, strategies: [..], coverage: [..], on_divergence: [..],.

experiment (G-S29 — designed from nothing):

Every sweep point must satisfy the DUT's where bounds up front (D-042).

12. Epoch surface

The entire user-facing epoch vocabulary is three forms (R24–R26) plus the reset witness:

• Everything else is inferred (pinning inference is local+principal, 05 §4): no epoch annotations in user signatures; Stamped<T,D> and Crosses are elaboration-owned (R27); the CDC mirror chain is synthesized from rebind over a stamped stream (R30); token states carry facets structurally (R29).
• pkt.map(|p| ...) transforms the payload under a sealed coordinate — transport stays epoch-oblivious (core G22).
• Unit-epoch normalization rule (core F8, committed): stamped over a no_reset (unit-epoch) domain is the identity — so a multi-hop crossing that would produce stamped (stamped T) through a unit-epoch fabric collapses, and the inner coordinate is the one that survives.
• ResetWitness (R28): ResetWitness::mint() at the lifecycle transition, &w ω-borrows at flush sites, w.close() linear consumption — one death event per assertion, unified with the squash contract. retain reg reads elaborate as stamped (the register legally outlives reset, core G30).

13. fmt interactions (pointers into 14)

Additions the corpus waves demanded; normative text lives in 14:

1. Decode-table row idiom: fixed-arity row constructors (entry(...)) keep table rows one-per-line under no-alignment; raw struct-literal rows explode 7×-vertical. Style-guide idiom + pedantic lint (verif verdict 1).
2. on-arm wrap rule: session-FSM guards that exceed 100 cols break before =>, indent one level (verif verdict 4).
3. Generic-arg wrap rule: over-long <...> lists break after <, one argument per line, trailing comma legal in <> lists (verif verdict 5 — new relative to the charter).
4. Manifest proof sub-tables: [proofs.<name>] one-key-per-line is the canonical form (inline tables can't fit a content hash in 100 cols) — D-054 spec addition (verif verdict 8).
5. Where-lists take no trailing comma (not braced bodies); requires normalizes to ;; data bodies steer via trailing comma, statement bodies are immune — the disciplines never collide in one brace pair.
6. Known-awkward but accepted: the three-line guarantee/predicate/with evidence stanza; positional booleans in row constructors (style guide: prefer small enums).

14. Requirement traceability

Committed core (R1–R36 → section)

Fence caveat (grammar probe): the grammar fences out compound div/mod right operands (the non-linearity); const-ness of a bare identifier is a trivial name-resolution check — non-constant expressions are grammatically impossible; non-const names are a resolution error.

Systems-safety extension (R37–R50)

R37–R50 remain requirements, not syntax. The extension wave must demonstrate all of the following before adding keywords or grammar productions here:

1. Sparse opt-in surface: a FIFO using no advanced contract family has an unchanged AST and summary.
2. Separation checks: occurrence/detection/containment, eventual/bounded progress, implementation-equivalence/noninterference, intended/bound physical constraints, and evidence/assurance cannot collapse into ambiguous forms.
3. One contract envelope: families reuse contract, named entries, assumptions/guarantees, requires, evidence sets, and metadata rather than each inventing a top-level mini-language unless a corpus proves that impossible.
4. Stable artifact references: content hash, tool/target/mode/design pins, owner, validity, and expiry fit the existing Meta micro-grammar or force one explicit revision.
5. Parser and formatter evidence: resilient-LL and tree-sitter agree; mutation recovery remains local; representative MSHR, CHI/NoC, DMA–IOMMU, power/reconfiguration, DFT, numeric, and assurance examples survive blind regeneration.

15. Rejected and deferred constructs

Rejected (recorded so they are not re-invented):

• Standalone connect a => b; — drafted in the core corpus, never needed: named-argument instantiation is the duality-checked connect (G6; one way to write each thing).
• reg ... = next declaration-site next-value form — D-079: one meaning per token; <- is the only Later-boundary write. (Supersedes core G7's optional inline form and verif G-S34.)
• Brace fallback for generic args — the restricted angle-bracket algebra suffices (D-080).
• Always-allow struct literals in headers — measured ambiguous (GLR-only); forbid + parenthesize (D-080).
• Bare inst name = expr; binder (grammar GAP-18 sugar) — corpus never used it; let x = inst ... is the one form.
• Bare discharge by ... without a target name (core F5) and unnamed guarantee {}/liveness {} blocks in arbitrate — named entries are mandatory (G-S23).
• Implicit-r arbitrate fields (key = r.age) — explicit closures only (F6/F10).
• session<txn> shorthand — label ≠ field in the computed case (verif F5).
• Named call arguments — Rust has none; the divergence budget is spent on hardware semantics (verif F9).
• Statement-form expect(...) — #[expect] attribute only (G-S30). Tick-literals, as casts, bare - on hardware integers, += outside session counters, vertical alignment — per charter and 14.

Resolved this pass: T @ 'E availability sugar is ADOPTED — it parsed cleanly in both the resilient-LL and tree-sitter implementations (GAP-24) and is the fmt-canonical spelling of At<T, 'E>.

Deferred, with reasons:

• is_pow2 in the width algebra — candidate interpreted symbol awaiting its D-037 confluence-interaction argument; until then the blessed idiom is clog2(DEPTH + 1) == clog2(DEPTH) + 1 (core F9).
• pub(crate)-style finer visibility beyond pub(package) — no corpus demand (GAP-04, G-S33).
• at_most 1 per cycle alternative rate spelling — only needed if / ever wants to mean division at comptime (grammar note).
• Conservation-justified state-refinement discharge (core F4) and event provenance in purely combinational components (core F11) — real gaps, semantics-side; tracked for 03/06, not syntax.

16. Appendix: the complete grammar

The reconciled surface grammar. This EBNF is normative and matches the prose above; it updates the probe's GRAMMAR.ebnf for D-079 (reg/<-), D-080 hard-reservations, and every corpus-won construct. Notation: ISO-flavored EBNF; CommaList(X) = [ X { "," X } [ "," ] ].

Register

D-077 (charter, SETTLED — Veronica), D-078 (this spec, DRAFT-COMPLETE), D-079 (reg forms, SETTLED), D-080 (grammar-evidence decisions, SETTLED) in decisions.md. Remaining gates before D-078 settles: the fmt dry-run (D-049–D-053 over both corpora, §13 rules) and the blind-regeneration pass (a fresh agent rewrites the corpora from this document alone; divergence measures spec completeness).