Rul (.rl) v0.4 バイナリ仕様書 — 128ビットISAとO(N)検証器
Rul (.rl) v0.4 公式バイナリレイアウト仕様：64バイトRulHeader、16バイトArenaDescriptor、16バイトProofEntry、29オペコードの128ビットNodeFrame、および単一パスO(N)検証規則。
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
すべての実行可能なRulプログラムは、直接ゼロコピー・メモリマッピング (mmap) のために16バイトおよび64バイト境界に整列されたフラットなバイナリ .rl イメージです。コア実行エンジンにはテキスト字句解析器やASTパーサーは一切含まれません。
1. バイナリ・ファースト
src/transpiler.rs により境界にて約8.8 µsで無損失の双方向 .rls <-> .rl 変換を実行。
2. トポロジカル SSA-DAG
すべての命令ノード i は i 未満の被演算子のみを参照でき、停止性を数学的に保証します。
3. 安全性と意図の分離
レイヤー1が5.78 ns/ノードでメモリと境界の安全性を証明し、レイヤー2が AssertContract と rul trace を検証します。
[0x02] SECTION 1 OF .RL
RulHeader（64バイト、キャッシュライン整列）
| バイト位置 | フィールド | 型 | 説明 |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | 正規マジック署名：b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | Arena、Proof、Node セクション全体に対する64ビット FNV-1a 整合性ハッシュ |
| 16..24 | capability_mask | u64 | ハードウェアI/Oサンドボックスマスク (0x00 = 純粋計算, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | 16バイト ArenaDescriptor エントリの数 |
| 28..32 | proof_count | u32 | 16バイト ProofEntry 境界証明書の数 |
| 32..36 | node_count | u32 | 128ビット（16バイト）NodeFrame 命令の数 |
| 36..40 | output_node | u32 | 主要出力SSAノードの0始まりインデックス |
| 40..64 | reserved | [u8; 24] | ヘッダを64バイトCPUキャッシュラインに整列させるゼロ埋めパディング |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor（16バイト）＆ ProofEntry（16バイト）
| バイト位置 | ArenaDescriptor | 型 | 説明 |
|---|---|---|---|
| 0..4 | arena_id | u32 | 列指向 Arena 識別子 (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | 均質な列の要素数（Shape長） |
| 8 | type_lane | u8 | 要素の型とSIMDレーン幅（例：0x18 = f64x8） |
| 9 | mutability | u8 | 0 = 不変入力 | 1 = 線形可変領域 |
| 10..12 | alignment | u16 | バイト整列要件（AVX-512 / キャッシュライン向けに64バイト） |
| 12..16 | initial_version | u32 | 初期 AffineToken バージョン（1から開始） |
| バイト位置 | ProofEntry | 型 | 説明 |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | 被演算子の origin_arena に厳密にバインドされた対象 Arena ID |
| 4..8 | bound_lo | u32 | 非負の下限インデックス |
| 8..12 | bound_hi | u32 | 上限インデックス <= effective_target_len |
| 12..16 | witness_node | u32 | 証人SSAインデックスノード（Gather 命令の in_b） |
[0x04] SECTION 4 OF .RL
128ビット NodeFrame レイアウト（16バイト）
アルゴリズム・レーン（何を計算するか：Opcode / 被演算子） スケジュール・レーン（どう実行するか：SIMD / マルチコア） 証明レーン（安全性：バージョンチケット / 境界証明）
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITS8ビット・レジスタ内訳 · BYTE 2 (b16..b23) 0x12
0 2^7
0 2^6
0 2^5
1 2^4
0 2^3
0 2^2
1 2^1
0 2^0
フィールド: schedule_hint 型: u8
✓ ロード時に検査される O(N) 検証器の不変条件 (~5.78 ns) (fusion_group << 4) | exec_policy
直交ハードウェアスケジュールバイト：0x11 (SimdStream) を 0x12 (MultiCore) に変更しても安全性証明を変えずにCPU実行を並列化します。
ノード #3: 中間ヒープ割り当てゼロでL1キャッシュレジスタ内で融合実行される要素ごとの8レーンベクトル二乗 ($n0 * $n0)。
[0x05] 29-OPCODE ISA (v0.4.0)
完全29オペコード命令セット (v0.4.0)
| HEX | OPCODE | カテゴリ | セマンティクス | 説明 |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | ReadLease を保持して ArenaDescriptor[in_a] から列スライスをロード。 |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | 命令フレームに直接埋め込まれた64ビット IEEE-754 浮動小数点スカラ定数。 |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | ProofEntry によって証明された列 in_a のゼロコピー部分スライス。 |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | AffineToken を消費する線形インプレース更新 (ver -> ver + 1)。 |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | 要素ごとのSIMD加算 (VADDPD)。 |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | 要素ごとのSIMD減算 (VSUBPD)。 |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | 要素ごとのSIMD乗算 (VMULPD)。 |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | 要素ごとの IEEE-754 SIMD除算 (VDIVPD)。 |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | 分岐なしの大なり述語マスク (VCMPPD)。 |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | マスク外のレーンをゼロにする分岐なし述語選択 (VANDPD)。 |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | 分岐なしの要素ごと最小値 (VMINPD)。 |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | 分岐なしの要素ごと最大値 (VMAXPD)。 |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | 分岐なしの小なり述語マスク。 |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | 分岐なしの等価述語マスク。 |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | IEEE-754 符号ビット消去による分岐なし絶対値。 |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | ハードウェアSIMD平方根 (VSQRTPD)。 |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | -Infinity 方向への分岐なし丸め (VROUNDPD)。 |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | +Infinity 方向への分岐なし丸め (VROUNDPD)。 |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | 要素ごとの自然対数ステンシル。 |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | 要素ごとの自然指数関数ステンシル。 |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | 一致する要素を連続的に詰めるストリームコンパクション。 |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | スカラへの8アキュムレータ水平加算リダクション。 |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | スカラへの水平最大値リダクション。 |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | ProofEntry によって保証された間接インデックスギャザー。 |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | スカラへの水平最小値リダクション。 |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | ビット単位のブールマスク論理積 (AND)。 |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | ビット単位のブールマスク論理和 (OR)。 |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | 権限ゲート付きハードウェアリングバッファ出力 (CAP_NET_RING)。 |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | 出力が有限かつ非NaNであることを検証する実行時ドメイン契約。 |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
4つの単一パス O(N) 線形検証規則
1. トポロジカルSSA規則
インデックス i のすべてのノードは in_a < i かつ in_b < i を満たす必要があり、閉路を数学的に防ぎます。
2. 線形メモリ所有権の保存
ReadLease(a, ver) は live_version[a] == ver を検査。AffineConsume(a, ver) は可変性を確認し checked_add(1) でバージョンを更新します。
3. 起源バインド境界証明
ArenaSlice と Gather は ProofEntry.target_arena == origin_arena かつ bound_lo <= bound_hi <= effective_target_len を検証します。
4. ゼロトラスト CapabilityMask
ハードウェアI/Oオペコード (0x30 RingEnqueue) は RulHeader.capability_mask 内の対応ビットを要求し、無い場合は実行前に拒否されます。