Language Reference
This is the complete reference for the wirespec language. It is organized as a lookup resource. For a narrative introduction, see the Language Tour.
Types
Primitive Integer Types
| Type | Width | Signedness | C Mapping |
|---|---|---|---|
u8 | 8 bits | Unsigned | uint8_t |
u16 | 16 bits | Unsigned | uint16_t |
u24 | 24 bits | Unsigned | uint32_t (lower 24 bits) |
u32 | 32 bits | Unsigned | uint32_t |
u64 | 64 bits | Unsigned | uint64_t |
i8 | 8 bits | Signed | int8_t |
i16 | 16 bits | Signed | int16_t |
i32 | 32 bits | Signed | int32_t |
i64 | 64 bits | Signed | int64_t |
u24 stores a 3-byte unsigned integer in a uint32_t. The parse function reads exactly 3 bytes; the serialize function writes exactly 3 bytes. Common in TLS record headers.
Explicit-Endian Integer Types
| Type | Width | Endianness | C Mapping |
|---|---|---|---|
u16be | 16 bits | Big-endian | uint16_t |
u16le | 16 bits | Little-endian | uint16_t |
u24be | 24 bits | Big-endian | uint32_t |
u24le | 24 bits | Little-endian | uint32_t |
u32be | 32 bits | Big-endian | uint32_t |
u32le | 32 bits | Little-endian | uint32_t |
u64be | 64 bits | Big-endian | uint64_t |
u64le | 64 bits | Little-endian | uint64_t |
i16be | 16 bits | Big-endian | int16_t |
i16le | 16 bits | Little-endian | int16_t |
i32be | 32 bits | Big-endian | int32_t |
i32le | 32 bits | Little-endian | int32_t |
i64be | 64 bits | Big-endian | int64_t |
i64le | 64 bits | Little-endian | int64_t |
An explicit-endian type always uses its declared endianness, regardless of any @endian module annotation. This lets you mix endianness within a single struct.
Bit Types
| Type | Width | C Mapping |
|---|---|---|
bit | 1 bit | Part of BitGroup → uint8_t / uint16_t / uint32_t |
bits[N] | N bits | Part of BitGroup → uint8_t / uint16_t / uint32_t |
bit is exactly equivalent to bits[1]. Consecutive bit and bits[N] fields are automatically grouped into a single read operation — see BitGroup Packing.
Byte Types
| Syntax | Semantics | C Mapping |
|---|---|---|
bytes[N] | Fixed N bytes | wirespec_bytes_t (zero-copy) |
bytes[length: EXPR] | EXPR bytes, EXPR must be integer-like | wirespec_bytes_t |
bytes[remaining] | All remaining bytes in current scope | wirespec_bytes_t |
bytes[length_or_remaining: EXPR] | If EXPR is Some, use value; if None, consume remaining | wirespec_bytes_t |
All byte variants generate wirespec_bytes_t — a zero-copy view into the input buffer:
typedef struct { const uint8_t *ptr; size_t len; } wirespec_bytes_t;No allocation is performed. The pointer references the original input buffer.
Semantic Types
| Type | Kind | Allowed Positions | C Mapping |
|---|---|---|---|
bool | Semantic type (not a wire type) | let bindings, guard conditions | bool |
bool cannot appear as a wire field. It is the natural result type of comparison and logical expressions used in let bindings. The type checker treats bool as a reserved builtin name; user code must not define a type, field, or variable named bool.
bytes Spec Variants
The four forms of bytes[...] cover every common protocol pattern:
bytes[N] — Fixed Length
Reads or writes exactly N bytes. N must be a compile-time integer literal.
reset_token: bytes[16], # always 16 bytes
random: bytes[32], # always 32 bytesbytes[length: EXPR] — Length-Prefixed
Reads or writes the number of bytes given by EXPR. EXPR is evaluated at parse/serialize time and must produce an integer-like value (a prior field or arithmetic over prior fields).
packet MqttString {
length: u16,
data: bytes[length], # reads exactly 'length' bytes
}
# Arithmetic over prior fields is permitted
data: bytes[length: length - 8], # subtract header overheadEXPR must have an integer-like type (u8, u16, u32, u64, or a semantic integer codec such as VarInt). Using a non-integer-like type is a compile error.
bytes[remaining] — Scope Remainder
Consumes every byte remaining in the current scope. Must be the last wire field in its scope. let bindings and require clauses may follow, but no wire fields may.
_ => Unknown { data: bytes[remaining] }, # catch-all branch
0x0b => ReadRsp { value: bytes[remaining] },bytes[length_or_remaining: EXPR] — Optional-Length
EXPR must have type Option[T] where T is an integer-like type. If EXPR is present (non-null), that many bytes are read. If EXPR is absent (null), all remaining bytes in the scope are consumed.
0x08..=0x0f => Stream {
length_raw: if frame_type & 0x02 { VarInt },
data: bytes[length_or_remaining: length_raw],
# ↑ if length_raw is present, use it; otherwise consume the rest
},Using a plain (non-optional) integer for length_or_remaining is a compile error — use bytes[length: EXPR] instead.
Continuation-Bit VarInt
The varint { } block defines a variable-length integer type using a per-byte continuation flag. This covers MQTT Remaining Length, Protocol Buffers varint, and LEB128.
type MqttLength = varint {
continuation_bit: msb, # which bit is the continuation flag
value_bits: 7, # data bits per byte
max_bytes: 4, # maximum encoded bytes (overflow → error)
byte_order: little, # lower-order groups come first
}Parameters
| Parameter | Values | Description |
|---|---|---|
continuation_bit | msb or lsb | Bit position of the continuation flag within each byte |
value_bits | Positive integer | Number of data bits carried per byte |
max_bytes | Positive integer | Maximum number of bytes before WIRESPEC_ERR_OVERFLOW |
byte_order | little or big | Byte significance order: little = lower-order groups first (MQTT, Protobuf); big = higher-order groups first |
If the continuation bit is still set after max_bytes bytes have been consumed, the parser returns WIRESPEC_ERR_OVERFLOW.
In C, the value is decoded into the smallest unsigned integer type that can represent the maximum value. For MqttLength (max 4 bytes, 28 data bits), the C field type is uint32_t.
Expression Language
Precedence Table
Operators are listed from lowest to highest binding. Operators on the same row have equal precedence.
| Level | Operator(s) | Associativity | Notes |
|---|---|---|---|
| 1 | ?? | Left | Coalesce: Option[T] ?? T → T |
| 2 | or | Left | Logical OR |
| 3 | and | Left | Logical AND |
| 4 | == != < <= > >= | None (non-associative) | Comparison |
| 5 | | | Left | Bitwise OR |
| 6 | ^ | Left | Bitwise XOR |
| 7 | & | Left | Bitwise AND |
| 8 | << >> | Left | Bit shift |
| 9 | + - | Left | Addition and subtraction |
| 10 | * / % | Left | Multiplication, division, modulo |
| 11 | ! - | Right | Unary logical NOT, unary negation |
| 12 | . [] [..] | Left | Member access, index, slice |
| 13 | () literals names | — | Primary expressions |
Bitwise vs Comparison Precedence
Bitwise operators (& | ^) bind tighter than comparison operators (== != < <= > >=) in wirespec. This is the opposite of C and Java.
| Expression | wirespec parsing | C parsing |
|---|---|---|
a & mask == 0 | (a & mask) == 0 | a & (mask == 0) |
flags | 0x04 != 0 | (flags | 0x04) != 0 | flags | (0x04 != 0) |
wirespec's rule matches programmer intent: bit-mask tests almost always want the comparison to apply to the masked result. The C rule is a notorious bug source that requires extra parentheses in almost every real usage.
The ?? Coalesce Operator
?? unwraps an Option[T] value with a fallback:
Option[T] ?? T → Tlet offset: u64 = offset_raw ?? 0, # 0 if offset_raw is absentIf offset_raw is present, ?? returns its value. If absent (null), it returns the right operand. The right operand must have the same type T as the unwrapped option.
Range Operators
| Operator | Meaning | Context |
|---|---|---|
..= | Inclusive range [start, end] | Pattern matching only |
.. | Half-open range [start, end) | Slice expressions, quantifiers |
0x02..=0x03 => Ack { ... }, # matches 2 and 3 inclusive
paths[0..active_path_count], # elements 0 through count-1Literals
| Form | Example | Type |
|---|---|---|
| Decimal integer | 42, 255 | Integer |
| Hex integer | 0x06, 0x1c | Integer |
| Binary integer | 0b00, 0b11 | Integer |
| String | "hello" | String (annotations only) |
| Boolean | true, false | bool |
| Null | null | Option null literal |
Field Kinds
Summary Table
| Kind | Syntax | On Wire? | In C Struct? | Notes |
|---|---|---|---|---|
| Wire | name: T | Yes | Yes | Consumes bytes during parse |
| Optional | name: if COND { T } | Conditional | Yes | bool has_name; T name; in C |
| Derived | let name: T = EXPR | No | Yes | Computed from prior fields |
| Validation | require EXPR | No | No | Runtime check; error → WIRESPEC_ERR_CONSTRAINT |
Wire Fields
A wire field consumes bytes from the input in declaration order.
src_port: u16,
dst_port: u16,
length: u16,
checksum: u16,Optional Fields
An optional field is present on the wire only when COND evaluates to true. COND may reference any wire field or let field declared above.
ecn_counts: if frame_type == 0x03 { EcnCounts },
offset_raw: if frame_type & 0x04 { VarInt },
packet_id: if qos > 0 { u16 },In C:
bool has_ecn_counts;
ecn_counts_t ecn_counts;To use an optional field's value in a subsequent expression, either guard with the same condition or use ?? to provide a default.
Derived Fields (let)
A let field does not consume any bytes. It computes a value from prior fields and stores it in the struct.
let offset: u64 = offset_raw ?? 0,
let fin: bool = (frame_type & 0x01) != 0,
let qos: u8 = (type_and_flags & 0x06) >> 1,let may reference any wire field or prior let field declared in the same scope. bool is the only semantic type permitted as a let target; it cannot be a wire field.
The serialize function recomputes the expression from the struct's wire fields; the stored value is not used for serialization.
Validation (require)
require EXPR adds a runtime check that fires during parse. If EXPR is false, the parser returns WIRESPEC_ERR_CONSTRAINT.
require length >= 8,
require length <= MAX_CID_LENGTH,
require data_offset >= 5,
require type_and_flags & 0x0F == 0x02,require may appear anywhere among the fields; it can reference any wire or let field declared above it. It does not appear in the C struct.
Compile-Time Assertions (static_assert)
static_assert EXPR is evaluated at compile time. If it fails, the compiler reports an error before generating any code.
const MAX_CID_LENGTH: u8 = 20
static_assert MAX_CID_LENGTH <= 255Field Visibility and Ordering
Fields within a packet, frame branch, or capsule body are visible to all fields declared after them in the same scope (top to bottom):
- A
bytes[length: X]field may reference a fieldXdeclared above it. - An
if CONDfield may reference any field declared above. - A
letfield may reference any wire or priorletfield declared above. - A
requireclause may reference any wire orletfield declared above. - A field must not reference itself or any field declared below it — this is a compile error.
Scope Rules
bytes[remaining] and [T; fill] consume the rest of the current scope and must be the last wire field in that scope. let bindings and require clauses may follow.
Scope Boundaries
Each of the following constructs forms an independent scope:
| Construct | Scope |
|---|---|
packet Foo { ... } | The entire { ... } body |
Each branch of a frame | Each => Name { ... } body |
capsule header fields | Fields before the within clause |
Each branch of a capsule within | Each => Name { ... } body |
if COND { T } | The single field T inside the condition |
Where bytes[remaining] is Legal
# Branch body — OK
frame F = match tag: u8 {
0 => A { data: bytes[remaining] },
1 => B { x: u8, data: bytes[remaining] },
}
# capsule within branch — OK
capsule C {
type: u8, length: u16,
payload: match type within length {
0 => D { entries: [Entry; fill] },
_ => Unknown { data: bytes[remaining] },
},
}Where bytes[remaining] is Illegal
# NOT OK: wire field follows remaining
packet Bad {
data: bytes[remaining], # compile error: wire field follows
trailer: u8,
}Integer-Like Types
The following types are accepted wherever an integer-like value is required: array counts, byte lengths (bytes[length: ...]), and scope lengths (within EXPR).
- Primitives:
u8,u16,u24,u32,u64 - Semantic integer codecs: User-defined types built with
varint { }(e.g.VarInt,MqttLength) resolve to an underlying unsigned integer. These are also accepted.
Signed integers (i8, i16, i32, i64), bool, bytes, composite types, enums (unless their underlying type is integer-like), and non-integer Options are not integer-like. Using them as an array count or byte length is a compile error.
BitGroup Packing
Consecutive bit and bits[N] fields are automatically grouped into a single wire read. The rules:
- The sum of bits in the group must be a multiple of 8 (whole bytes) — checked at compile time.
- Under
@endian big(the default): the first declared field occupies the most significant bits. - Under
@endian little: the first declared field occupies the least significant bits. - Each field is extracted with shift and mask operations in the generated C.
# From examples/ip/ipv4.wspec (big-endian)
packet IPv4Header {
version: bits[4], # high 4 bits of byte 0
ihl: bits[4], # low 4 bits of byte 0
dscp: bits[6], # high 6 bits of byte 1
ecn: bits[2], # low 2 bits of byte 1
total_length: u16, # separate u16 field
...
}Generated C:
uint8_t _b0 = buf[pos++];
out->version = (_b0 >> 4) & 0x0f;
out->ihl = (_b0 >> 0) & 0x0f;
uint8_t _b1 = buf[pos++];
out->dscp = (_b1 >> 2) & 0x3f;
out->ecn = (_b1 >> 0) & 0x03;A BitGroup boundary occurs when a non-bit field is encountered, or at the end of the struct.
Reserved Identifiers
The following names have special meaning in the wirespec type checker or runtime. User code must not define types, fields, variables, or events with these names.
| Name | Kind | Permitted Context |
|---|---|---|
bool | Builtin semantic type | let binding type, guard expression result |
null | Builtin literal value | Option[T] comparisons, right operand of ?? |
fill | Keyword and builtin function | Array size expression ([T; fill]); initializer expression (fill(value, count)) |
remaining | Keyword | bytes_spec only: bytes[remaining] |
in_state | Builtin predicate | guard, verify, and all() in state machines |
all | Builtin quantifier | guard and verify in state machines |
child_state_changed | Internal event | Emitted by delegate; cannot be used as a user-defined event name |
src | Transition binding | guard and action blocks inside state machine transitions |
dst | Transition binding | action blocks inside state machine transitions |
Attempting to define a type, constant, field, or on-event named with one of these identifiers is a compile error.
Top-Level Declarations
module
module quic.varint
module ble.att
module mqttDeclares the module identity of the current file. The dotted name maps to a file path: quic.varint is resolved from quic/varint.wspec (or quic/varint.wspec) on the include path. At most one module declaration is permitted per file. It must appear before any other declarations.
import
import quic.varint.VarInt
import quic.varint # imports the module itselfMakes a name from another module available in the current file. Cyclic imports are a compile error. Relative imports are not supported.
const
const MAX_CID_LENGTH: u8 = 20
const QUIC_VERSION_1: u32 = 0x00000001Defines a compile-time constant. The type must be a primitive integer type. Constants are usable anywhere an integer literal is accepted.
enum
enum ContentType: u8 {
ChangeCipherSpec = 20,
Alert = 21,
Handshake = 22,
ApplicationData = 23,
}Defines a named set of integer values. The underlying wire type follows :. Enum types can be used as match tags in frame and capsule definitions. In C, an enum becomes a typedef enum.
flags
flags PacketFlags: u8 {
KeyPhase = 0x04,
SpinBit = 0x20,
FixedBit = 0x40,
}Like enum, but values are intended as bitmasks. In C, a flags type becomes a typedef enum. The distinction from enum is semantic documentation.
type
Two forms:
Type alias — introduces no new wire layout:
type AttHandle = u16le
type Uuid16 = u16leComputed type — a dependent record whose field types depend on earlier field values:
@strict
type VarInt = {
prefix: bits[2],
value: match prefix {
0b00 => bits[6],
0b01 => bits[14],
0b10 => bits[30],
0b11 => bits[62],
},
}Continuation-bit VarInt — a variable-length integer with a per-byte continuation flag:
type MqttLength = varint {
continuation_bit: msb,
value_bits: 7,
max_bytes: 4,
byte_order: little,
}packet
A fixed sequence of named fields. The canonical wirespec building block for protocol headers.
packet UdpDatagram {
src_port: u16,
dst_port: u16,
length: u16,
checksum: u16,
require length >= 8,
data: bytes[length: length - 8],
}frame
A tagged union. The tag field is read first, then the payload layout is selected by pattern matching.
frame AttPdu = match opcode: u8 {
0x02 => ExchangeMtuReq { client_rx_mtu: u16le },
0x03 => ExchangeMtuRsp { server_rx_mtu: u16le },
0x0a => ReadReq { handle: AttHandle },
0x0b => ReadRsp { value: bytes[remaining] },
_ => Unknown {},
}Pattern forms:
| Pattern | Matches |
|---|---|
0x06 | Exact value |
0x02..=0x03 | Inclusive range [0x02, 0x03] |
_ | Any value (catch-all, required for exhaustiveness) |
capsule
A TLV (Type-Length-Value) container. A header section is followed by a within EXPR clause that constrains the payload parse to exactly EXPR bytes.
capsule MqttPacket {
type_and_flags: u8,
remaining_length: MqttLength,
payload: match (type_and_flags >> 4) within remaining_length {
1 => Connect { ... },
3 => Publish { ... },
_ => Unknown { data: bytes[remaining] },
},
}The tag expression (before within) can be:
- A plain field name:
match content_type within length - A parenthesized expression over header fields:
match (type_and_flags >> 4) within remaining_length
If the payload branch consumes fewer bytes than EXPR, the parser returns WIRESPEC_ERR_TRAILING_DATA. If it tries to read beyond EXPR, it returns WIRESPEC_ERR_SHORT_BUFFER.
static_assert
static_assert MAX_CID_LENGTH <= 255Evaluated at compile time. A failure prevents code generation.
Annotations
Annotations appear immediately before the definition they annotate.
| Annotation | Applies To | Phase | Effect |
|---|---|---|---|
@endian big | Module (top of file) | 1 | Set default endianness to big-endian |
@endian little | Module (top of file) | 1 | Set default endianness to little-endian |
@strict | type definition | 1 | Reject non-canonical encodings with WIRESPEC_ERR_NONCANONICAL |
@checksum(internet) | Field (u16) | 1 | RFC 1071 Internet Checksum: verify on parse, auto-compute on serialize |
@checksum(crc32) | Field (u32) | 1 | IEEE 802.3 CRC-32: verify on parse, auto-compute on serialize |
@checksum(crc32c) | Field (u32) | 1 | Castagnoli CRC-32C: verify on parse, auto-compute on serialize |
@checksum(fletcher16) | Field (u16) | 1 | RFC 1146 Fletcher-16: verify on parse, auto-compute on serialize |
@max_len(N) | Array field | 1 | Override per-field array capacity to N elements |
@doc("...") | Any definition | 1 | Documentation string (not yet used in codegen) |
@derive(...) | Definition | 2+ | Reserved for future use |
@verify(bound=N) | State machine | 3+ | TLA+ bounded verification depth |
At most one @checksum annotation per packet or frame branch. The field type must match the algorithm's requirement (see table above).
Arrays
Count-Bound Arrays
ack_ranges: [AckRange; ack_range_count], # count from a prior field
cipher_suites: [u16; cipher_suites_length / 2], # arithmetic countThe count expression must evaluate to an integer-like type. The actual count is checked against the field's capacity at runtime.
Fill Arrays
entries: [Entry; fill], # consume the rest of the current scope[T; fill] reads as many T elements as the current scope can hold. Must be the last wire field in its scope.
Fill-Within Arrays
extensions: [Extension; fill] within extensions_length,Creates a sub-scope of extensions_length bytes and reads Extension elements until the sub-scope is exhausted. Under-read → WIRESPEC_ERR_TRAILING_DATA. Over-read → WIRESPEC_ERR_SHORT_BUFFER.
Array Capacity (C Backend)
Arrays are stack-allocated at fixed capacity. The default is WIRESPEC_MAX_ARRAY_ELEMENTS (64), defined in wirespec_runtime.h. Override globally with -DWIRESPEC_MAX_ARRAY_ELEMENTS=N.
Per-field override:
@max_len(1024)
large_items: [Item; count], # capacity 1024 for this field onlyIf the count on the wire exceeds the capacity, the parser returns WIRESPEC_ERR_CAPACITY.
Modules and Imports
module quic.varint # declare this file's module identity
import quic.varint.VarInt # import VarInt from quic/varint.wspecA module name maps to a file path on the include path (-I CLI flag). The compiler resolves imports, detects cycles, and produces a topological ordering for C #include directives.
Rules:
- By default, all declarations are public. If any item in a module has
export, only exported items are visible to importers (the resolver enforces this). - Circular imports are a compile error.
- Relative imports are not supported; all imports are absolute module paths.
- A file without a
moduledeclaration can still be compiled (single-file mode).
State Machine Declarations
State machines are introduced with state machine Name { }. Full state machine syntax is covered in the State Machines Guide. This section summarizes the keywords and reserved names.
Keywords
| Keyword | Role |
|---|---|
state machine | Introduces a state machine definition |
state | Declares a state, optionally with associated data fields |
initial | Designates the initial state |
transition | Declares a transition from one state (or *) to another |
on | Specifies the event that triggers a transition |
guard | Boolean precondition; transition fires only when true |
action | Assignment block executed when the transition fires |
delegate | Forwards an event to a child state machine field |
verify | Declares a verification property (Phase 3) |
[terminal] | Marks a state as a final state (no outgoing transitions required) |
src and dst Bindings
Inside a transition:
srcrefers to the current state's data (read-only inguardandaction)dstrefers to the next state's data (write-only inaction)
src and dst are only valid inside guard and action blocks. They are not valid in verify properties (which use bare field names to refer to the current state).
delegate Semantics
delegate src.field <- event forwards event to a child state machine:
dstis implicitly initialized as a copy ofsrc.- The child field in
dstreceives the event and transitions in place. - If the child transitions to a different state,
child_state_changedis issued to the parent as a new event. child_state_changedis silently discarded if no parent transition handles it (the only event type exempt from the "unhandled event → error" rule).
delegate is only permitted on self-transitions (same source and target state). A transition may not contain both delegate and action.
all() Quantifier
guard all(src.paths[0..src.active_path_count], in_state(Closed))all(collection, predicate) returns true when every element of collection satisfies predicate. In Phase 1, in_state(S) is the only supported predicate form. all() is a builtin special form, not a general higher-order function.
Error Codes
The C backend generates functions that return wirespec_result_t. All possible values:
| Code | Meaning |
|---|---|
WIRESPEC_OK | Success |
WIRESPEC_ERR_SHORT_BUFFER | Not enough bytes in the input |
WIRESPEC_ERR_INVALID_TAG | Tag value matched no pattern and no _ catch-all |
WIRESPEC_ERR_CONSTRAINT | A require expression evaluated to false |
WIRESPEC_ERR_OVERFLOW | Integer overflow (length too large, or varint max_bytes exceeded) |
WIRESPEC_ERR_INVALID_STATE | State machine received an unhandled event |
WIRESPEC_ERR_TRAILING_DATA | within scope was not fully consumed |
WIRESPEC_ERR_NONCANONICAL | @strict type was encoded in a non-minimal form |
WIRESPEC_ERR_CAPACITY | Array count exceeded the field's allocated capacity |
WIRESPEC_ERR_CHECKSUM | @checksum verification failed on parse |
WIRESPEC_ERR_SCOPE_UNDERFLOW | Sub-cursor underflow (internal) |
WIRESPEC_ERR_ARRAY_OVERFLOW | Array index out of bounds (internal) |
Grammar Summary
The complete formal grammar is in the Grammar Reference. The most commonly needed productions:
file = { annotation | module_decl | import_decl | top_item }
top_item = const_def | enum_def | flags_def | type_def
| packet_def | frame_def | capsule_def | static_assert_def
type_expr = type_ref
| "match" NAME "{" match_branch { "," match_branch } "}"
| "if" expr "{" type_expr "}"
| "[" type_expr ";" array_size "]"
| "bytes" "[" bytes_spec "]"
bytes_spec = INTEGER
| "remaining"
| "length" ":" expr
| "length_or_remaining" ":" expr
pattern = literal | literal "..=" literal | "_"