← ワークベンチ ROADMAP · v0.4.0 → v1.0 v0.4.0 DOI: 10.5281/zenodo.23722094

Rul (.rl) 技術ロードマップ — v0.4エンジンからv1.0汎用システム言語へ

29オペコードの列指向計算エンジン (v0.4) から、AI生成ソフトウェアにおいてRustやGoを代替する汎用システム言語 (v1.0) へと拡張する4マイルストーンのロードマップ。

[0x01] STRATEGY

なぜデータパイプラインから開始したのか (v0.1 〜 v0.4)

汎用言語の機能を追加する前に16バイトのバイナリ命令形式が実機のシリコン上で機能することを証明するため、v0.1からv0.4までは配列・ベクトル処理パイプライン(29オペコード)に限定しました。その結果、約5.78 ns/ノードのO(N)検証、約6.4 µsの単体ELF64コンパイル、51.53 GB/sのスループットを実証しました。

[0x02] SIX-MONTH ROADMAP TO v1.0

v1.0 汎用システムプログラミング言語への4つのマイルストーン

v0.1.0 → v0.4.0 · 出荷済み本番ベースライン ✓ 本番稼働中

29オペコード列指向SSA-DAGコア、ホワイトボックストレーサー&線形スキャンAVX2 ELF64 AOT

実機ハードウェア上で16バイトバイナリ命令形式、単一パスO(N)検証器(約5.8 ns/ノード)、3層実行エンジン、rul-mcpサーバー、LLVM不要のLinux ELF64コンパイラ(約6.4 µs)を実証しました。

  • 01. 29オペコードにわたる64バイトRulHeader、16バイトArenaDescriptor、16バイトProofEntry、16バイトNodeFrame。
  • 02. 無損失の双方向 .rls <-> .rl アセンブラ、単体 rul CLI、rul-bench、6ツールの rul-mcp サーバー。
  • 03. 80 MB配列で 51.53 GB/s(C言語の4.72倍)を達成する線形スキャンYMMレジスタアロケータ (ymm2..ymm13)。
v0.5 · マイルストーン 1(1〜2ヶ月目) ● 開発進行中

汎用制御フロー、モジュール関数、複合データ型

16バイト命令セットを数値配列以外にも拡張し、汎用スカラ、構造体、列挙型、UTF-8文字列、ハッシュマップ、条件分岐、停止証明付きループをサポートします。

  • 01. i64、i32、u8、f32、固定レイアウト構造体、代数的タグ付き共用体、検証済みUTF-8文字列、Arenaハッシュマップのファーストクラスサポート。
  • 02. SelectBranch:両方の分岐が同一のメモリバージョン状態で合流することを要求する条件分岐(O(1)で検査)。
  • 03. RegionLoop & Call:ProofEntryの停止証人を持つ有界ループと、全プログラムのインライン化なしで検証されるモジュール関数。
v0.6 – v0.7 · マイルストーン 2(2〜3ヶ月目) ○ 計画済み

O(N) 時間でのRust級ヒープ所有権と構造体ライフタイム

32ビットTokenOpバージョンと16バイトProofEntry証人を、フラット配列からリージョンベースのヒープ割り当てと構造体フィールド借用へと一般化します。

  • 01. 線形所有権トークンに紐づく決定論的リージョンヒープ割り当てと解放。GCポーズもmalloc/free断片化もゼロ。
  • 02. 互いに素な構造体フィールドの更新とゼロコピー部分スライスのライフタイムを1命令あたりO(1)で検証するProofEntry証人。
  • 03. 何秒もかかる借用チェッカーの制約解決なしで、use-after-free、二重解放、エイリアシングを完全に防止。
v0.8 – v0.9 · マイルストーン 3(4〜5ヶ月目) ○ 計画済み

Goスタイルの決定論的並行処理と CapabilityMask 制御OS I/O

軽量タスク、所有権を転送するチャネル、ファイル・ネットワーク・プロセスのシステムコールを制御する細粒度ヘッダ権限ビットを導入します。

  • 01. 型付きチャネル経由のバッファ送信は送信側トークンをAffineConsumeし受信側へ所有権を移転 — GCなしでロード時にデータ競合を排除。
  • 02. 64ビット RulHeader.capability_mask を拡張し、ファイル読み書き、ネットワークソケット、タイマー、サブプロセスを厳格にゲート制御。
  • 03. CAP_NONE (0x0) を持つ .rl バイナリは、実行開始前にあらゆるネットワークやディスク呼び出しから数学的に遮断されます。
v1.0 · マイルストーン 4(6ヶ月目) ○ 計画済み

マルチアーキテクチャ・ネイティブバックエンド (x86_64, ARM64, WASI) と形式的健全性証明

LLVMなしでLinux、macOS、Windows、WebAssembly向けの単体実行ファイルを出力し、Kaniモデル検査と50プログラムのv1.0適合テストスイートで保証します。

  • 01. Linux、macOS、Windows向けの x86_64 および AArch64 (ARM64) ゼロLLVMネイティブコード生成と決定論的WASIモジュール。
  • 02. バイナリデコーダ、O(N)検証器、ネイティブコード生成にわたるKani有界モデル検査証明と継続的差分ファジング。
  • 03. 凍結された .rl v1.0 バイナリ仕様と公開50プログラム適合テストスイート。
[0x03] ARCHITECTURAL DISCIPLINE

3つのコアエンジニアリング原則(非目標 Non-Goals)

1. バックトラック・ソルバーの排除 (No Backtracking)

すべての安全性プロパティ(型、所有権、境界、ループ停止、I/O権限)は単一の順方向パス O(N) で検証可能でなければなりません。

2. ガベージコレクタの排除 (No Garbage Collector)

GC停止も隠れたランタイムスレッドもゼロ。メモリの寿命はバージョン付きArenaとRegionで明示的に追跡されます。

3. サイレントフォールバックの排除 (No Silent Fallbacks)

すべての実行層(Tier 0、Tier 1、Tier 2、ELF64 AOT)は一致する結果を返すか、決定論的エラーでフェイルクローズしなければなりません。