文法リファレンス
wirespec 言語の完全な形式文法を EBNF（拡張バッカス・ナウア記法）で示します。
EBNF 記法
| 記法 | 意味 |
|---|---|
{ x } | x の 0 回以上の繰り返し |
[ x ] | オプションの x（0 回または 1 回） |
| `x | y` |
"text" | リテラルキーワードまたは句読点 |
NAME | 識別子トークン（大文字 = 終端記号） |
; | 規則終端記号 |
トップレベル宣言
wirespec のソースファイルは、アノテーション、モジュール/インポート宣言、トップレベルアイテムを任意の順序で並べたものです。
file = { annotation | module_decl | import_decl | top_item } ;
module_decl = "module" dotted_name ;
import_decl = "import" dotted_name [ "." NAME ] ;
top_item = const_def | enum_def | flags_def | type_def
| packet_def | frame_def | capsule_def | static_assert_def ;module_decl は現在のファイルのモジュール識別子を宣言します（例: module quic.varint）。import_decl は特定の名前またはモジュール全体をスコープに導入します（例: import quic.varint.VarInt）。
定義
定数、列挙型、フラグ
const_def = "const" NAME ":" type_ref "=" literal ;
enum_def = "enum" NAME ":" type_ref "{" enum_member { "," enum_member } "}" ;
enum_member = NAME "=" literal ;
flags_def = "flags" NAME ":" type_ref "{" flags_member { "," flags_member } "}" ;
flags_member = NAME "=" literal ;
static_assert_def = "static_assert" expr ;enum は基礎型を持つ整数定数の名前付きセットです。flags は構文的には同じですが、値がビット演算で組み合わせるフラグであることを意味します。static_assert はコンパイル時に式を評価し、失敗するとコンパイルエラーになります。
型定義
type_def = { annotation } "type" NAME "=" type_body ;
type_body = "{" field_list "}" | type_expr | varint_block ;
varint_block = "varint" "{" varint_param { "," varint_param } "}" ;
varint_param = NAME ":" ( NAME | INTEGER ) ;type Name = TypeExpr は型エイリアスで、新しいワイヤレイアウトは導入しません。type Name = { ... }（波括弧あり）はフィールド構造を持つ計算型/依存型を定義します。varint { ... } は継続ビット方式の可変長整数エンコーディング（MQTT Remaining Length、LEB128 など）を定義します。
パケット定義
packet_def = { annotation } "packet" NAME "{" field_list "}" ;packet は固定構造のバイナリレコードで、フィールドは宣言順にパースされます。生成される C 構造体には各ワイヤフィールドのメンバと、条件付きフィールドの bool has_X が含まれます。
フレーム定義
frame_def = { annotation } "frame" NAME "="
"match" NAME ":" type_ref "{" frame_branch { frame_branch } "}" ;
frame_branch = pattern "=>" NAME "{" field_list "}"
| pattern "=>" NAME "{}" ;frame は先頭の判別子フィールドでディスパッチするタグ付きユニオンです。各ブランチはタグ値のパターンに対してマッチされます。すべての値がカバーされない場合、網羅性のために _ ワイルドカードブランチが必須です。
カプセル定義
capsule_def = { annotation } "capsule" NAME "{"
{ field "," }
"payload" ":" "match" capsule_tag "within" NAME
"{" frame_branch { frame_branch } "}" "}" ;
capsule_tag = NAME | "(" expr ")" ;capsule は TLV（Type-Length-Value）コンテナです。payload の前にヘッダフィールドを置き、within NAME でペイロードのバイト境界サブスコープを設定します。タグにはフィールド名か、ヘッダフィールドからの括弧付き式を使えます。
フィールド
フィールドは packet、frame ブランチ、capsule ヘッダ、計算 type の本体内に現れます。
field_list = { field_item [ "," ] } ;
field_item = field | derived_field | require_clause ;
field = { annotation } NAME ":" type_expr ;
derived_field = "let" NAME ":" type_ref "=" expr ;
require_clause = "require" expr ;| 種類 | 構文 | ワイヤ上? | 構造体内? |
|---|---|---|---|
| ワイヤフィールド | name: T | Yes | Yes |
| オプションフィールド | name: if COND { T } | 条件付き | bool has_name; T name; |
| 導出フィールド | let name: T = expr | No | Yes |
| 検証 | require EXPR | No | No（実行時チェック） |
フィールドは同スコープ内で後に宣言されたフィールドから参照できます（上から下の順序）。前方参照はコンパイルエラーです。
型式
type_expr = type_ref
| "match" NAME "{" match_branch { "," match_branch } "}"
| "if" expr "{" type_expr "}"
| "[" type_expr ";" array_size "]"
| "bytes" "[" bytes_spec "]" ;
match_branch = pattern "=>" type_expr ;
array_size = expr | "fill" ;
bytes_spec = INTEGER
| "remaining"
| "length" ":" expr
| "length_or_remaining" ":" expr ;bytes_spec バリアント：
| バリアント | 意味 |
|---|---|
bytes[N] | 固定 N バイト |
bytes[remaining] | 現在のスコープの残りバイトをすべて消費 |
bytes[length: EXPR] | EXPR バイト（EXPR は非オプション整数類似型でなければならない） |
bytes[length_or_remaining: EXPR] | EXPR が非 null の場合は EXPR バイト、そうでなければ残り（EXPR は Option[整数類似型] でなければならない） |
remaining と fill はキーワードであり、式ではありません。スコープ内の最後のワイヤフィールドとして使う必要があります。
パターン
パターンは frame のタグマッチやインライン match の型式に現れます。
pattern = literal | literal "..=" literal | "_" ;範囲の意味（Rust と同じ）：
| 演算子 | 意味 | 文脈 |
|---|---|---|
..= | 閉区間 [start, end] | パターンのみ |
.. | 半開区間 [start, end) | スライス、量化子（exists i in 0..N） |
例：
0x02..=0x03— 0x02 と 0x03（両端含む）にマッチ_— ワイルドカード、任意にマッチ（最後のブランチでなければならない）paths[0..count]— スライス式、半開区間
式
式は結合力の低い順から高い順への優先順位階層に従います。重要: ビット演算子は比較演算子より強く結合します。 C/Java とは逆で、a & mask == 0 は (a & mask) == 0 とパースされます。
expr = coalesce_expr ;
coalesce_expr = or_expr [ "??" or_expr ] ;
or_expr = and_expr { "or" and_expr } ;
and_expr = compare_expr { "and" compare_expr } ;
compare_expr = bitor_expr [ cmp_op bitor_expr ] ;
cmp_op = "==" | "!=" | "<" | "<=" | ">" | ">=" ;
bitor_expr = bitxor_expr { "|" bitxor_expr } ;
bitxor_expr = bitand_expr { "^" bitand_expr } ;
bitand_expr = shift_expr { "&" shift_expr } ;
shift_expr = add_expr { ( "<<" | ">>" ) add_expr } ;
add_expr = mul_expr { ( "+" | "-" ) mul_expr } ;
mul_expr = unary_expr { ( "*" | "/" | "%" ) unary_expr } ;
unary_expr = ( "!" | "-" ) unary_expr | postfix_expr ;
postfix_expr = primary_expr { "." NAME | "[" expr "]" | "[" expr ".." expr "]" } ;
primary_expr = literal
| qualified_name [ "(" [ expr { "," expr } ] ")" ]
| "fill" "(" expr "," expr ")"
| "(" expr ")" ;
qualified_name = NAME { "::" NAME } ;優先順位テーブル（低い順から高い順）：
| レベル | 演算子 | 備考 |
|---|---|---|
| 1（最低） | ?? | Option[T] の null 合体 |
| 2 | or | 論理 OR |
| 3 | and | 論理 AND |
| 4 | == != < <= > >= | 比較 |
| 5 | | | ビット OR |
| 6 | ^ | ビット XOR |
| 7 | & | ビット AND |
| 8 | << >> | ビットシフト |
| 9 | + - | 加算・減算 |
| 10 | * / % | 乗算・除算・剰余 |
| 11 | ! -（単項） | 論理 NOT・否定 |
| 12（最高） | . [i] [a..b] | メンバアクセス・インデックス・スライス |
?? は Option[T] をアンラップします（optional_field ?? default_value）。fill(value, count) は配列初期化の組み込み関数です。状態コンストラクタは :: 修飾で呼び出します（PathState::Active(pid, 0, 0)）。
アノテーション
アノテーションは定義やフィールドの前に置き、コンパイラやコードジェネレータにメタデータを伝えます。
annotation = "@" NAME [ "(" annotation_arg { "," annotation_arg } ")" ]
| "@" NAME NAME
| "@" NAME STRING ;
annotation_arg = NAME "=" literal | NAME | literal ;例：
@endian big— モジュールレベルまたはフィールドレベルのバイト順@doc("RFC 9000 Section 17")— ドキュメント文字列@strict— 実行時に非正規エンコーディングを拒否@checksum(internet)— RFC 1071 Internet チェックサム検証@max_len(1024)— フィールドごとの配列キャパシティオーバーライド
終端記号
literal = INTEGER | HEX | BINARY | STRING | "true" | "false" | "null" ;
type_ref = PRIMITIVE | NAME ;
dotted_name = NAME { "." NAME } ;
PRIMITIVE = "u8" | "u16" | "u32" | "u64"
| "u16be" | "u16le"
| "u32be" | "u32le"
| "u64be" | "u64le"
| "u24" | "u24be" | "u24le"
| "i8" | "i16" | "i32" | "i64"
| "bit"
| "bits" "[" INTEGER "]" ;整数リテラルは十進数（42）、十六進数（0x2a）、二進数（0b00101010）に対応します。null は Option[T] の不在値を表す組み込みリテラルです。bool は予約済みセマンティック型名で、PRIMITIVE ではなく、let バインディングと guard 条件でのみ使えます。
状態機械文法（拡張）
状態機械はトップレベルで定義し、階層的なプロトコルオートマトンを構成できます。コア文法を state machine、transition、verify 宣言で拡張しています。
状態機械の構造
top_item += state_machine_def ;
state_machine_def = "state" "machine" NAME "{" { sm_item } "}" ;
sm_item = state_decl | initial_decl | transition_def | verify_def ;
state_decl = "state" NAME [ "{" sm_field_list "}" ] [ "[" "terminal" "]" ] ;
sm_field_list = { NAME ":" type_expr [ "=" literal ] "," } ;
initial_decl = "initial" NAME ;各状態はデフォルト値付きの関連データフィールドを持てます。[terminal] は到達後に出ていく遷移のない終端状態を示します。initial で開始状態を指定します。
遷移
transition_def = "transition" ( NAME | "*" ) "->" NAME
"{" { transition_clause } "}" ;
transition_clause = "on" NAME [ "(" param_list ")" ]
| "guard" expr
| "action" "{" assignment { ";" assignment } [ ";" ] "}"
| "delegate" postfix_expr "<-" NAME ;
assignment = postfix_expr ( "=" | "+=" ) expr ;
param_list = NAME ":" type_expr { "," NAME ":" type_expr } ;節の多重度（構文ではなく意味上の制約）：
| 節 | 出現回数 | 制約 |
|---|---|---|
on | 1 回以上 | 複数イベントで遷移を共有可能 |
guard | 0 または 1 回 | src フィールドのみ参照可能 |
action | 0 または 1 回 | delegate と共存不可 |
delegate | 0 または 1 回 | 自己遷移（S -> S）のみ。action と共存不可 |
* は任意のソース状態にマッチするワイルドカードです。具体的なソース状態は * より優先されます。同じ (状態, イベント) ペアが重複するとコンパイルエラーです。
action ブロック内では、src が読み取り専用のソース状態データ、dst が書き込み専用のデスティネーション状態データです。代入間にはセミコロンが必須です。
delegate はイベントを子状態機械にルーティングします（delegate src.paths[path_id] <- event）。子は src のコピー上でインプレースに更新され、子の状態が変わると child_state_changed が親に再ディスパッチされます。
Verify 宣言
verify_def = "verify" NAME
| "verify" "property" NAME ":" vfy_leads_to ;verify NAME は組み込みプロパティを呼び出します（例: verify NoDeadlock、verify AllReachClosed）。verify property NAME: FORMULA はユーザー定義のテンポラルロジックプロパティを宣言します。
Verify 式文法
Verify 式は有界 TLA+ 検証器（Phase 3+）でチェックされるテンポラルロジックプロパティを記述します。優先順位は ~>（最低）からアトム（最高）の順です。
vfy_leads_to = vfy_implies { "~>" vfy_implies } ;
vfy_implies = vfy_or { "->" vfy_or } ;
vfy_or = vfy_and { "or" vfy_and } ;
vfy_and = vfy_unary { "and" vfy_unary } ;
vfy_unary = "not" vfy_unary
| "[]" vfy_unary
| "<>" vfy_unary
| vfy_atom ;
vfy_atom = postfix_expr "in_state" "(" NAME ")"
| "in_state" "(" NAME ")"
| postfix_expr cmp_op expr
| "all" "(" postfix_expr "," vfy_unary ")"
| "exists" NAME "in" expr ".." expr ":" vfy_unary
| "(" vfy_leads_to ")" ;テンポラル演算子：
| 演算子 | 意味 |
|---|---|
[] | 常に（ボックス — すべての将来状態で成立） |
<> | いつか（ダイヤモンド — ある将来状態で成立） |
~> | リードトゥー（P ~> Q は P が成立するときはいつか Q が成立することを意味する） |
-> | 含意（論理的含意、非テンポラル） |
組み込み述語：
| 述語 | 意味 |
|---|---|
in_state(S) | 現在の状態が S である |
all(collection, predicate) | コレクションのすべての要素が述語を満たす |
exists i in 0..N: formula | [0, N) に式を満たす i が存在する |
状態依存フィールドアクセス規則: 状態 S で宣言されたフィールドは、in_state(S) で論理的に支配された部分式内でのみ参照できます。テンポラル演算子 [] / <> は支配を断ちます。ガードなしで状態固有のフィールドにアクセスするとコンパイルエラーです。
# OK: in_state(Connected) によって支配されている
verify property Bounded:
[] (in_state(Connected) -> active_path_count <= 4)
# OK: in_state がフィールド参照をガード
verify property NonEmpty:
in_state(Connected) and active_path_count > 0 -> ...
# エラー：[] が支配を断つ — フィールドにアクセス不可
# in_state(Connected) -> [] active_path_count <= 4verify 式では裸のフィールド名が現在の状態データを参照します。src / dst は遷移専用のバインディングなので使えません。
拡張文法：将来の機能
以下の生成規則は仕様の完全性のために記載していますが、未実装です。
ASN.1 統合（Phase 2.5+）
top_item += "extern" "asn1" STRING "{" { NAME "," } "}" ;
field += NAME ":" "asn1" "(" NAME "," "encoding" ":" NAME ")" ;パラメトリック型（将来）
type_def = { annotation } "type" NAME [ "(" param_list ")" ] "=" type_body ;
packet_def = { annotation } "packet" NAME [ "(" param_list ")" ] "{" field_list "}" ;パラメトリック型は具体的なユースケースが出るまで保留中です。現在の本番文法は非パラメトリック形式です。