# proposal/16-syntax.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/e6a02b540546a94678ee1108222cd3050d40076f/proposal/16-syntax.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: e6a02b540546a94678ee1108222cd3050d40076f Requested commit: e6a02b540546a94678ee1108222cd3050d40076f Commit: e6a02b540546a94678ee1108222cd3050d40076f Blob: e786ec1da61502cf4cc54740fad8708febd9bacd Size: 60422 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/e6a02b540546a94678ee1108222cd3050d40076f/proposal/16-syntax.md?format=markdown) ```` # Committed-Core Surface Syntax The complete surface for Strata's committed core, designed against [15-syntax-requirements.md](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 | Fork | Pick | | ----------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | Component flavor | **Value-flow**: inputs as parameters, outputs as return type; no in/out/inout keywords; bidirectionality via protocol endpoint types | | Generics | **Rust split**: bare `<>` in type position, mandatory `::<>` turbofish in expression position; lexer emits single `>`, parser glues | | Bindings | **`let` / `reg` / `inst`** triad, `comptime`/`ghost` prefixes — binder form makes phase syntactically recoverable per token (14 §19) | | Terminators | **Semicolons** for statements (including `requires`); **comma-lists** for all data-shaped declaration bodies (fmt trailing-comma steering, 14 §2) | | Registers (D-079) | `reg name: T reset(v);` declares; `name <- expr;` is the next-cycle write. **No `= expr` next-value form at the declaration.** One meaning per token: `=` binds combinational values, `<-` is the visible Later-boundary write; multi-arm updates stay natural (sequential last-write-wins per body, elaborating to a priority mux) | | Tiebreaker | **Rust when unsure** — resolves: `#[attr]`, `where`, `::` paths, `//`+`///` comments, `..`/`..=` ranges, match/pattern syntax, snake_case/CamelCase | ## 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): ``` accept await bundle by claim clock_domain comptime component const contract counter differential_test discharge div domain elastic else enum experiment expect false fn for from ghost halt handshake if impl in inst interface invariant is latch let loop match mem mod msg mut no_reset on opaque ordering port preserve process property protocol prove pub quiesce recv reg repeat require requires resource retain return role rule sealed send sequence session solve stage stamped state state_machine static strategy stream struct to true type unsafe use where while* with at_most cycleobs ``` (`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. | Unit class | v1 closed table | | ---------------- | ---------------- | | rate denominator | `cycle` | | count | `txns`, `evals` | | frequency | `MHz`, `GHz` | | time | `ns`, `us`, `ms` | **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>` 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): ``` pub component MemoryController( requests: Consumer>, ) -> (resp: Producer>, dram_cmd: Producer>) where OUTSTANDING <= 64 { ... } ``` 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>` — encoding is semantics, not a `#[repr]` layout hint. Discriminants checked to fit exactly. ``` pub enum Opcode: Bits<7> { Load = 0b000_0011, Store = 0b010_0011, } ``` **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, 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: ``` let fifo = inst Fifo:: { push }; // pun connects `push` let out = fifo; // value-flow result ``` One protocol-connect form, checked by duality (04 §3): passing a producer value to a `Consumer

` 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. ``` let decoded = decode(instr); // combinational; IMMUTABLE (R1) let mut acc = init; // mutation is marked, rare let (a, b, c) = triple; // n-ary destructuring (R34) if let Some(item) = pushed { ... } // rust if-let reg rd_ptr: Index reset(0); // D-079: declaration, reset mandatory* rd_ptr <- rd_ptr.incr_wrap(); // next-cycle write; last-write-wins per body buf[wr_ptr] <- item; // element write (same statement form) retain reg saved: ConfigState reset(dflt);// survives warm reset; reset() = POR only mem buf: [T; DEPTH]; // un-reset storage; reads need an // initializedness argument or unsafe(uninitialized_use) inst — expression form only: `let x = inst C { ... };` (bare `inst x = ...;` rejected, §15) comptime let LANES = cfg.lanes; // static phase comptime for i in 0..LANES { ... } // static loop; also an expression (array per iteration) comptime param STAGES: Nat in 1..=6; // design-space knob (07 §7) comptime fixed DEPTH: Nat = cfg.depth; // user-owned config ghost let trace = observe(bus); // ghost phase, erased ``` \* `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): ``` requires solve mem_has_base_reg(opcode: Bits<7>) { if entry_for_encoding(opcode).class is Mem { entry_for_encoding(opcode).has_rs1 } }; discharge mem_has_base_reg by comptime_exhaustive(opcode); requires static { DEPTH mod 2 == 0 }; requires prove home_serves_all { every_request_eventually_responds(requests, resp) }; ``` 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`; `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 — ``` let (out, popped) = handshake ready_valid:: { valid: !empty, payload: head }; let (out, _sent) = handshake ready_valid:: from opt_value; // Option drives valid/payload let pushed = push.accept(ready = !full); // drives ready, yields Option ``` `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): | Level | Operators | | -------------- | --------------------------------------------------------------------------------------- | | assign | `=` (to `let mut` targets; lvalue-checked) | | range | `..`, `..=` | | or | `\|\|` | | and | `&&` | | compare / test | `==` `!=` `<` `<=` `>` `>=` · `is` variant-set | | concat | `++` (bit concat; widths sum in the D-037 algebra) | | shift | `<<`, `>>` (glued) | | additive | `+`, `-` (grammatical; hardware integers reject bare `-` — R8) | | multiplicative | `*` · `div`/`mod` with **ConstAtom right operand by grammar** (the R7 Presburger fence) | | unary | `!`, `-` | | postfix | call, `.method`, `::` turbofish, `[i]` index/slice, `?` | - **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::()`, `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` 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::` 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`): ``` let granted = arbitrate dram_issue { inputs: [read_q, write_q], eligibility: |r| r.ready, policy: oldest_first(key = |r| r.age, tie_break = round_robin), resource: dram_cmd_port, guarantee exclusive_grant: at_most_one_grant_per_cycle(), liveness weak_fairness: fair_grants() under continuously_ready(dram_cmd_port), }; ``` - **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 ``` Type = ["stamped"] ['domain] TypeCore ["@" 'Event] TypeCore = Path | (T1, T2) | [T; N] | fn(A) -> B // fn types comptime-phase only ``` - **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 { 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`, `Bits`, `UInt`, `OneHot`, `Gray`, `Encoded`, `Handle`. - **`stamped T`** — the one epoch keyword users write (§12). **`T @ 'E`** availability sugar for `At` 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

` / `Producer

` for binary protocols; `View` 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): ``` Attribute = "#" "[" Meta "]" Meta = Path [ "(" CommaList(MetaItem) ")" ] MetaItem = Meta | IDENT "=" MetaValue | Predicate | Literal MetaValue = Literal | QuantityLit | Rate | Path | "derived" | IDENT "(" CommaList(MetaValue) ")" ``` 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 = ` 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): ``` protocol Burst { const granule = 64, // R16 shared constants send Header { length: N }, repeat N { send Beat }, // R10: no hand-rolled beat counters if broadcast { send Snoop }, // R11 conditional refinement recv Completion, quiesce, // R17 acceptance point invariant beats_bounded: accepted(Beat) <= N, // names mandatory (R12) } ``` _Session dialect_ (D-027's first customer — roles, families, ghost state, guarded FSM): ``` protocol ChiReadSharedTxn { role Requester, role Home, role Peer[N_RN - 1], // role family; cardinality monomorphized msg ReadShared: ReqFlit from Requester to Home, msg Snoop: SnpFlit from Home to Peer[tgt], // indexed by a payload field counter snp_sent: 0..=N_RN - 1, // session-scoped ghost naturals counter snp_pend[peer: Index]: 0..=1, // keyed family latch requester: Index, // open-time binding invariant resp_bounded: snp_rcvd <= snp_sent, accept state Idle { // `accept` marks retirement states on ReadShared(req) => Snooping { requester = req.src, snp_sent = 0 }, }, state Snooping { on SnpResp(r) if snp_pend[r.src] == 1 => Snooping { snp_rcvd += 1, snp_pend[r.src] = 0 }, on CompData(_) if snp_rcvd == snp_sent && if bcast { snp_sent == N_RN - 1 } => AwaitAck, }, } ``` 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: ``` bundle ChiPort { const granule = 64, role Rn, role Hn, role Sn, req: credit, 4> from Rn to Hn, dat: layer, credit<4>> from Hn to Rn, // layer combinator (type-level) vc: [layer { max_len: 8 }, credit<4>>; VCS] from Sn to Hn, // array channel; // invariants apply per element invariant comp_bounded_by_req: accepted(dat) <= accepted(req), session lifecycle: ChiReadSharedTxn over { // spawn-per-key + projection ReadShared: req, Snoop: snp, CompData: dat, CompAck: ack, }, session line_serial: hazard_lock { // R13; div fence applies binds: txn, // per-message key bindings (addr-less messages inherit at open) scope: lifecycle, // lock acquire/release rides the named session's open/retire }, quiesce maintenance_barrier: at(maint.Accept), // R17; end-of-trace implicit } ``` The `session` 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`, `group = id`, `related_by = overlaps::` (relations `#[symmetric]`-checked, R15), `key_set = lines(addr, len)` (R14 — one event joins every keyed order; start-line-only keying is machine-refuted), `CommitsIn`. 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: ``` contract { assume payload_stable: requests.payload_stable_while_blocked(), guarantee no_duplicate_response: exactly_one_response_per_request(requests, resp) with evidence [ Tested<17.2e9 txns>, BoundedProved, MutationValidated, ], claim frequency: Measured<842 MHz, vu19p, "vivado-2026.1">, } contract cdc { ordering: preserved, capacity: DEPTH, ... } contract death { drain_within_cycles: 64 } // or drain_within_responses: N ``` `claim` carries physical facts — evidence about an artifact, never a guarantee of the term (D-075). Evidence literals: `Ctor` 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): ``` state_machine CacheLockstep { state { model: CacheModel, dut: DutHandle, } rule load(addr in cache_address(&model)) if dut.can_accept() { ...; } invariant committed_loads_match_model { assert_eq(dut.x(), model.x()); } } ``` **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::, reference:, interface:, lockstep:, strategies: [..], coverage: [..], on_divergence: [..],`. **experiment** (G-S29 — designed from nothing): ``` experiment mem_ctrl_depth_sweep on MemoryController { target: vu19p, variants: sweep { OUTSTANDING: [8, 16, 32], BANKS: 1..=2 }, // or any comptime Sweep expr workloads: [stream_copy(bytes = 1_048_576, seed = 7)], // explicit seeds (P-6) measures: [fmax, luts, occupancy(of = self.occupancy)], // self = the DUT instance faults: [dropped_response(rate = 1.0e-6, seed = 23)], budget: { builds: 24, board_hours: 8 }, evidence: Measured, } ``` 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: ``` port log(pkt: stamped TracePkt); // R24: the ONE epoch keyword users write let sealed = stamp(head); // introduction — legal only where the surrounding // port/return type says `stamped` match rebind(pkt) { // R25: bind-epoch as match; whole coordinate Fresh(p) => consume(p), Stale(p) => { stale_drops <- stale_drops.wrapping_add(1); drop_it(p) }, } requires solve diff_same(a, b) { same_epoch(a, b) }; // R26 ``` - Everything else is inferred (pinning inference is local+principal, 05 §4): no epoch annotations in user signatures; `Stamped` 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.]` 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) | R | Section | R | Section | R | Section | | ---------------------------------- | -------- | -------------------------- | ------- | ----------------------- | -------------------- | | R1 immutability | §5 | R13 session keys | §10 | R25 rebind | §12 | | R2 checked names / inferred guards | §4 §6 §8 | R14 key_set | §10 | R26 same_epoch | §12 | | R3 is-sets, bind-then-match | §6 | R15 related_by symmetric | §10 §9 | R27 Crosses elab-owned | §12 | | R4 narrow! | §5 | R16 protocol consts | §10 | R28 ResetWitness | §12 | | R5 set rendering | §6 | R17 quiesce | §10 | R29 structural facets | §12 | | R6 path-condition identity | §6 §11 | R18 role tags | §10 | R30 mirror chain | §12 | | R7 infix Presburger + fence | §6 §7 | R19 Nat1 | §7 | R31 CommitProof wording | lands in 05 | | R8 monus vs checked_sub | §6 | R20 left-Presburger fix-it | §7 | R32 arm-anchored diags | checker | | R9 prev(x) | §6 | R21 clog2, closed symbols | §3 §7 | R33 monitor diagnostic | §11 | | R10 repeat N | §10 | R22 budget attrs only | §9 | R34 n-ary destructuring | §5 §8 | | R11 conditional refinement | §6 §10 | R23 no overrun ctor | §9 | R35 region markers | §5 | | R12 named invariants | §10 | R24 stamped | §12 | R36 pass/semver/pinning | 07/13 formats; §13.4 | 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` 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`. **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 } [ "," ] ]`. ```ebnf (* ---------- 0. Lexical ---------- *) IDENT = ident_start { ident_continue } ; LABEL = "'" IDENT ; (* domains and events; never a char literal *) INT_LITERAL = dec_literal | hex_literal | bin_literal ; (* "_" separators legal *) NUM_LITERAL = dec_literal [ "." dec_literal ] [ ("e"|"E") ["-"] dec_literal ] ; (* fraction/exponent forms legal ONLY inside QuantityLit / MetaValue *) STRING_LITERAL = '"' { string_char | escape } '"' ; (* metadata positions only *) BOOL_LITERAL = "true" | "false" ; QuantityLit = NUM_LITERAL UnitIdent ; (* 842 MHz, 17.2e9 txns — closed unit table *) Rate = ConstExpr "/" "cycle" ; (* the only "/" in the language *) COMMENT = "//" rest | "///" rest | "//!" rest ; (* anchored trivia *) (* Lexer: never emits ">>" or ">="; parser glues adjacent ">" ">" / ">" "=" in expression-operator position only. "..="/".." are single tokens. Hard-reserved keywords per 16 §3; soft words are keywords only in the positions shown below. No context-sensitive lexing. *) (* ---------- 1. Source file and items ---------- *) SourceFile = { Item } ; Item = { Attribute } { DOC_COMMENT } [ Visibility ] [ UnsafeQual ] ItemKind ; Visibility = "pub" [ "(" "package" ")" ] ; UnsafeQual = "unsafe" "(" IDENT ")" ; (* item-position unsafe surface *) ItemKind = Component | FnItem | GhostFn | StrategyFn | Protocol | Bundle | Stream | Interface | ImplItem | EnumItem | StructItem | OpaqueType | TypeAlias | ClockDomain | ResourceItem | Experiment | StateMachine | Property | DifferentialTest | UseItem | ModItem | ConstItem ; Component = "component" IDENT [ GenericParams ] ParamClause [ "->" ReturnType ] [ WhereClause ] Block ; ReturnType = Type | "(" CommaList( IDENT ":" Type ) ")" ; (* named tuple returns, G-S35 *) FnItem = [ "comptime" ] "fn" IDENT [ GenericParams ] ParamClause [ "->" Type ] [ WhereClause ] ( Block | ";" ) ; (* ";" in interfaces only *) GhostFn = "ghost" FnItem ; StrategyFn = "strategy" FnItem ; (* G-S24; body may use weighted! *) ParamClause = "(" CommaList( Param ) ")" ; Param = { Attribute } IDENT ( ":" Type | "in" Expr ) ; (* "in strategy_expr" generator binders: rule/property/strategy params only *) GenericParams = "<" CommaList( GenericParam ) ">" ; GenericParam = IDENT [ ":" Bound ] | "const" IDENT ":" Type [ "=" ConstExpr ] [ "in" RangeConst ] | LABEL ; (* domain/event params: <'src, 'dst, T> *) Bound = Path { "+" Path } ; WhereClause = "where" WherePred { "," WherePred } ; (* NO trailing comma *) WherePred = IDENT ":" Bound | Predicate ; Interface = [ "sealed" ] "interface" IDENT [ GenericParams ] [ WhereClause ] "{" { InterfaceMember } "}" ; InterfaceMember= { Attribute } ( FnItem | ConstItem | "type" IDENT ";" ) ; ImplItem = "impl" [ GenericParams ] Path [ GenericArgs ] [ "for" Type ] [ WhereClause ] "{" { Item } "}" ; EnumItem = "enum" IDENT [ GenericParams ] [ ":" Type ] (* encoding ascription, G-S1 *) "{" CommaList( EnumVariant ) "}" ; EnumVariant = { Attribute } IDENT [ "(" CommaList( Type ) ")" | "{" CommaList( Field ) "}" | "=" INT_LITERAL ] ; (* checked to fit exactly *) StructItem = "struct" IDENT [ GenericParams ] [ WhereClause ] ( ";" | "{" CommaList( { Attribute } [ Visibility ] Field ) "}" ) ; Field = IDENT ":" Type ; OpaqueType = "opaque" "type" IDENT [ GenericParams ] "=" Type ";" ; TypeAlias = "type" IDENT [ GenericParams ] "=" Type ";" ; ConstItem = "const" IDENT [ ":" Type ] "=" Expr ";" ; UseItem = "use" UseTree ";" ; UseTree = Path [ "::" ( "*" | "{" CommaList( UseTree ) "}" ) ] [ "as" IDENT ] ; ModItem = "mod" IDENT ( ";" | "{" { Item } "}" ) ; ClockDomain = "clock_domain" IDENT "{" CommaList( DomainEntry ) "}" ; DomainEntry = "clock" ":" Type | "reset" ":" Type [ "{" CommaList( IDENT ":" IDENT ) "}" ] | "no_reset" ; ResourceItem = "resource" IDENT ":" Type [ "=" Expr ] ";" ; (* share(f) / replicate(f) *) (* ---------- 2. Protocols / bundles / streams (16 §10) ---------- *) Protocol = "protocol" IDENT [ GenericParams ] [ WhereClause ] "{" CommaList( SeqEntry ) "}" (* role-less: sequential *) | "protocol" IDENT [ GenericParams ] [ WhereClause ] "{" CommaList( SessEntry ) "}" ; (* roles present: session *) (* one node kind, two dialects; never mixed (G-S10) *) SeqEntry = ("send" | "recv") IDENT [ GenericArgs ] [ "{" CommaList( Field | FieldBind ) "}" ] | "repeat" ConstExpr "{" CommaList( SeqEntry ) "}" | "if" Predicate "{" CommaList( SeqEntry ) "}" | "const" IDENT "=" ConstExpr | "quiesce" | "invariant" IDENT ":" Predicate ; FieldBind = IDENT ":" ConstExpr ; SessEntry = "role" IDENT [ "[" ConstExpr "]" ] (* role family *) | "msg" IDENT ":" Type "from" RoleRef "to" RoleRef | "counter" IDENT [ "[" IDENT ":" Type "]" ] ":" RangeConst | "latch" IDENT ":" Type | "invariant" IDENT ":" Predicate | "const" IDENT "=" ConstExpr | [ "accept" ] "state" IDENT [ "{" CommaList( OnArm ) "}" ] ; RoleRef = IDENT [ "[" IDENT "]" ] ; (* Peer[tgt]: payload field *) OnArm = "on" IDENT "(" Pattern ")" [ "if" Predicate ] "=>" IDENT [ "{" CommaList( CounterUpdate ) "}" ] ; CounterUpdate = CounterRef ( "=" | "+=" ) Expr ; CounterRef = IDENT [ "[" Expr "]" ] ; Bundle = "bundle" IDENT [ GenericParams ] "{" CommaList( BundleEntry ) "}" ; BundleEntry = "const" IDENT "=" ConstExpr | "role" IDENT [ "[" ConstExpr "]" ] | IDENT ":" ChannelType [ "from" RoleRef "to" RoleRef ] | "invariant" IDENT ":" Predicate | SessionAttach | "quiesce" IDENT ":" "at" "(" Expr ")" | "ordering" ":" "{" CommaList( IDENT ":" OrderingRel ) "}" ; ChannelType = Type | "[" Type ";" ConstExpr "]" ; (* array channels, G-S38 *) SessionAttach = "session" "<" IDENT "=" KeyExpr ">" IDENT ":" Type ( "over" "{" CommaList( IDENT ":" IDENT ) "}" | "{" CommaList( IDENT ":" Expr ) "}" ) ; (* hazard_lock config *) KeyExpr = ConstExpr ; (* div fence applies (R13) *) OrderingRel = Path "<" CommaList( RelationArg ) ">" ; (* dedicated node kind (F12) *) RelationArg = EventPath | IDENT "=" ( Expr | Path Turbofish ) ; EventPath = IDENT { "." IDENT } ; Stream = "stream" IDENT [ GenericParams ] "{" CommaList( StreamEntry ) "}" ; StreamEntry = IDENT ":" ( Type | Expr | "{" CommaList( StreamEntry ) "}" ) ; (* payload/domain/protocol/flow/identity/ordering/authority; flow entries: acceptance: at_most(Rate), outstanding: range *) (* ---------- 3. Verification items (16 §11) ---------- *) StateMachine = "state_machine" IDENT [ GenericParams ] "{" "state" "{" CommaList( Field ) "}" { RuleItem | SmInvariant } "}" ; RuleItem = "rule" IDENT ParamClause [ "if" Expr ] Block ; SmInvariant = "invariant" IDENT Block ; Property = "property" IDENT ParamClause Block ; (* + #[metamorphic] attr *) DifferentialTest = "differential_test" IDENT "{" CommaList( IDENT ":" Expr ) "}" ; Experiment = "experiment" IDENT "on" Path "{" CommaList( ExpEntry ) "}" ; ExpEntry = IDENT ":" ( Expr | SweepLit | "{" CommaList( IDENT ":" Expr ) "}" | "[" CommaList( Expr ) "]" | EvidenceLit ) ; SweepLit = "sweep" "{" CommaList( IDENT ":" ( "[" CommaList(ConstExpr) "]" | RangeConst ) ) "}" ; EvidenceLit = Path "<" CommaList( EvidenceArg ) ">" ; EvidenceArg = QuantityLit | IDENT | IDENT "=" Literal | STRING_LITERAL ; (* ---------- 4. Attributes: the committed Meta micro-grammar (16 §9) ---------- *) Attribute = "#" "[" Meta "]" ; Meta = Path [ "(" CommaList( MetaItem ) ")" ] ; MetaItem = Meta | IDENT "=" MetaValue | Predicate | Literal ; MetaValue = Literal | QuantityLit | Rate | Path | "derived" | IDENT "(" CommaList( MetaValue ) ")" ; (* ---------- 5. Statements (16 §5) ---------- *) Block = "{" { Stmt } [ Expr ] "}" ; Stmt = LetStmt | RegStmt | RegUpdate | MemStmt | ComptimeStmt | GhostStmt | RequiresStmt | DischargeStmt | RequireGuarantee | NarrowStmt | AssertStmt | StageStmt | PortStmt | SequenceStmt | ForStmt | ReturnStmt | RegionStmt | ContractBlock | ResourceItem | Item | ExprStmt | ";" ; LetStmt = "let" [ "mut" ] Pattern [ ":" Type ] "=" Expr ";" ; RegStmt = [ "retain" ] "reg" IDENT ":" Type [ "reset" "(" Expr ")" ] [ "uninit" ] ";" ; (* D-079: reset mandatory unless no_reset domain or uninit; NO "=" form *) RegUpdate = LValue "<-" Expr ";" ; (* next-cycle write; last-write-wins per body *) LValue = IDENT { "[" Expr "]" | "." IDENT } ; MemStmt = "mem" IDENT ":" "[" Type ";" ConstExpr "]" ";" ; ComptimeStmt = "comptime" ( LetStmt | ForStmt | Block | "param" IDENT ":" Type "in" RangeConst ";" | "fixed" IDENT ":" Type "=" Expr ";" ) ; GhostStmt = "ghost" LetStmt ; RequiresStmt = "requires" ("static" | "solve" | "prove") [ IDENT [ ParamClause ] ] "{" Predicate "}" ";" ; (* name mandatory on solve/prove; ";" canonical, "," accepted + fmt-normalized *) DischargeStmt = "discharge" IDENT "by" IDENT "(" CommaList( IDENT | Expr ) ")" ";" ; RequireGuarantee = "require" "guarantee" Path "with" "evidence" ">=" Path ";" ; NarrowStmt = "narrow" "!" "(" Predicate ")" ";" ; AssertStmt = "assert" Expr ";" ; (* ghost/test phase only *) StageStmt = "stage" [ LABEL ] ";" ; PortStmt = "port" IDENT ParamClause [ "->" Type ] ( Block | ";" ) ; SequenceStmt = "sequence" Block ; (* await/halt/loop legal inside *) ForStmt = "for" Pattern "in" Expr Block ; ReturnStmt = "return" [ Expr ] ";" ; RegionStmt = ( "elastic" | "cycleobs" ) Block ; ContractBlock = "contract" [ IDENT ] "{" CommaList( ContractEntry ) "}" ; ContractEntry = "assume" IDENT ":" Predicate | "guarantee" IDENT ":" Predicate [ "with" "evidence" "[" CommaList(EvidenceLit) "]" ] | "claim" IDENT ":" EvidenceLit | IDENT ":" ( Expr | EvidenceLit ) ; (* flavored: cdc / death entries *) ExprStmt = Expr ";" | BlockLikeExpr ; (* match/if/for/domain/blocks need no ";" *) (* ---------- 6. Expressions (16 §6) ---------- *) Expr = AssignExpr ; AssignExpr = RangeExpr [ "=" AssignExpr ] ; (* lvalue-checked post-parse *) RangeExpr = OrExpr [ ( ".." | "..=" ) OrExpr ] | ( ".." | "..=" ) OrExpr ; OrExpr = AndExpr { "||" AndExpr } ; AndExpr = CmpExpr { "&&" CmpExpr } ; CmpExpr = ConcatExpr [ CmpOp ConcatExpr ] | ConcatExpr "is" VariantSet ; CmpOp = "==" | "!=" | "<" | "<=" | ">" | ">=" ; (* ">"/" >=" glued *) VariantSet = Path { "|" Path } ; ConcatExpr = ShiftExpr { "++" ShiftExpr } ; ShiftExpr = AddExpr { ( "<<" | ">>" ) AddExpr } ; AddExpr = MulExpr { ( "+" | "-" ) MulExpr } ; MulExpr = UnaryExpr { "*" UnaryExpr | ( "div" | "mod" ) ConstAtom } ; (* THE PRESBURGER FENCE (R7): div/mod right operand is a ConstAtom by grammar; const-ness of a Path is a resolution check *) ConstAtom = INT_LITERAL | Path ; UnaryExpr = ( "!" | "-" ) UnaryExpr | PostfixExpr ; PostfixExpr = PrimaryExpr { Postfix } ; Postfix = "." IDENT [ Turbofish ] [ CallArgs ] | Turbofish CallArgs | CallArgs | "[" Expr "]" | "?" ; Turbofish = "::" "<" CommaList( GenericArg ) ">" ; (* mandatory in expr position *) CallArgs = "(" CommaList( Expr | ClosureExpr | IDENT "=" Expr ) ")" ; (* IDENT "=" only in builtin forms: accept(ready = e), policy keys, measures *) PrimaryExpr = Literal | QuantityLit (* quantity positions only *) | Path | Path StructLiteralBody (* restricted: see CondExpr *) | "(" CommaList( Expr ) ")" | "[" CommaList( Expr ) "]" | Block | IfExpr | IfLetExpr | MatchExpr | LoopExpr | InstExpr | HandshakeExpr | ArbitrateExpr | DomainExpr | ProcessExpr | AwaitExpr | "halt" | ClosureExpr | UnsafeExpr | MacroExpr | LABEL [ ("+"|"-") ConstAtom ] ; (* event expr: 'G + 2 *) Path = IDENT { "::" IDENT } ; StructLiteralBody = "{" CommaList( IDENT [ ":" Expr ] | ".." Expr ) "}" ; (* punning + FRU *) InstExpr = "inst" Path [ Turbofish ] StructLiteralBody ; (* named-only + punning *) HandshakeExpr = "handshake" Path Turbofish ( StructLiteralBody | "from" Expr ) ; (* core G11 *) ArbitrateExpr = "arbitrate" [ IDENT ] "{" CommaList( ArbEntry ) "}" ; ArbEntry = "inputs" ":" Expr | "eligibility" ":" ClosureExpr | "policy" ":" Expr | "resource" ":" Expr | "guarantee" IDENT ":" Predicate | "liveness" IDENT ":" Predicate [ "under" Expr ] ; (* names mandatory, G-S23 *) DomainExpr = "domain" LABEL Block ; (* an expression *) ProcessExpr = "process" "{" CommaList( IDENT ":" ( Stmt-fragment | Expr ) ) "}" ; (* step: , done: Bool, ok: S, err: Option — core G23 *) AwaitExpr = "await" Expr ; (* inside sequence only *) LoopExpr = "loop" Block ; IfExpr = "if" CondExpr Block [ "else" ( IfExpr | Block ) ] ; IfLetExpr = "if" "let" Pattern "=" CondExpr Block [ "else" Block ] ; MatchExpr = "match" CondExpr "{" CommaList( MatchArm ) "}" ; MatchArm = { Attribute } Pattern [ "if" CondExpr ] "=>" Expr ; CondExpr = Expr ; (* StructLiteralBody FORBIDDEN at top level (D-080); transitively through operators, not through parens/args *) ClosureExpr = "|" CommaList( Pattern [ ":" Type ] ) "|" Expr ; UnsafeExpr = "unsafe" "(" IDENT [ "," "reason" "=" STRING_LITERAL ] ")" Block ; MacroExpr = IDENT "!" "{" CommaList( MacroArm | IDENT ":" Expr ) "}" ; MacroArm = INT_LITERAL "=>" Expr ; (* weighted! / config! *) Literal = INT_LITERAL | BOOL_LITERAL | STRING_LITERAL ; (* ---------- 7. Predicates ---------- *) Predicate = Expr | "if" Expr "{" Predicate "}" ; (* implication sugar, predicate position only (R11): !cond || pred. Predicates share the Expr grammar (one precedence table); tier membership is semantic EXCEPT the div/mod fence, which is syntactic. Interpreted symbols (closed): clog2 max min prev accepted transferred outstanding same_epoch. *) (* ---------- 8. Types (16 §7) ---------- *) Type = [ "stamped" ] [ LABEL ] TypeCore [ "@" EventExpr ] (* T @ 'E adopted *) | "&" Type ; (* port-surface borrows, ghost borrows *) TypeCore = Path [ GenericArgs ] [ TypeConfigBlock ] | "(" CommaList( Type ) ")" | "[" Type ";" ConstExpr "]" | "fn" "(" CommaList( Type ) ")" [ "->" Type ] ; (* comptime-phase only *) TypeConfigBlock= "{" CommaList( IDENT [ ":" ConstExpr ] ) "}" ; (* schema config; TYPE POSITION ONLY *) EventExpr = LABEL [ ("+"|"-") ConstAtom ] ; GenericArgs = "<" CommaList( GenericArg ) ">" ; GenericArg = IDENT "=" ConstExpr | RangeConst | TypeOrConst | LABEL ; TypeOrConst = Type | ConstExpr ; (* unified on Path prefix; elaboration sorts *) RangeConst = [ ConstExpr ] ( ".." | "..=" ) ConstExpr ; (* Angle-bracket sub-language: NO comparisons, shifts, "&&"/"||", struct literals inside "<...>" — ">" always closes, "," always separates; no symbol table, no brace fallback (D-080). *) ConstExpr = ConstMul { ("+" | "-") ConstMul } ; (* "-" = monus at type level *) ConstMul = ConstPrimary { "*" ConstPrimary | ("div" | "mod") ConstAtom } ; ConstPrimary = INT_LITERAL | Path [ GenericArgs ] | ("clog2" | "max" | "min") "(" CommaList( ConstExpr ) ")" | "(" ConstExpr ")" ; (* ---------- 9. Patterns (16 §8) ---------- *) Pattern = PatternNoAlt { "|" PatternNoAlt } ; PatternNoAlt = "_" | Literal | INT_LITERAL ("..=" | "..") INT_LITERAL | Path [ "(" CommaList( Pattern ) ")" | "{" CommaList( IDENT [ ":" Pattern ] | ".." ) "}" ] | "(" CommaList( Pattern ) ")" | "mut" IDENT ; (* ---------- 10. Resilient-LL anchors (informative) ---------- *) (* Every ItemKind and most statements open with a unique hard keyword; the item-recovery set is FIRST(Item), the statement set adds the statement openers + ";" "}". ERROR nodes wrap skipped tokens; MISSING tokens are zero-width; text(tree) == input on ALL inputs (D-062). *) ``` ## 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](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). ````