SlimeJava ― 計測手続きと一次資料
Java → Rust bit-exact 変換の全検証データを集約します ― 差分ファジング・SMT 形式証明・Hybrid 受理率・性能ベンチ・例外境界・seed 注入。すべて決定論シードで第三者が手元で再現可能です。
製品紹介・位置づけは 製品ページ をご覧ください。本ページは「再現と検証のための一次資料」に特化します。
古い Java のプログラムを、新しくて頑丈な Rust という言語へ「引っ越し」させる道具です。意味を解釈せず「骨組み」だけをそのまま写すので、計算の中身(整数核)は元と 1 ビットも違わない出力に(約 6 万件の自動テストで実証)。引っ越し後は起動が速く・メモリが軽く・予測しやすい。全部を Rust にはせず、写せる所だけ正直に写します。
Java を手で Rust に書き換えると、整数のオーバーフローや例外の起き方の違いで必ず挙動がズレます。SlimeJava は整数トラップ(wrapping・シフトマスク・ゼロ除算例外)まで 1 ビット違わず再現し、約 6 万件の差分ファジングで逸脱ゼロ + SMT 全入力形式証明 31 件・反例 0。新旧比較テスト(UAT)を機械検証可能な「振る舞い不変の証明書」へ。速度は正直に ― ホット throughput は Java 互角、効くのは起動・メモリ。
全 Java を Rust 化せず 3 領域に自動分割(Hybrid Bit-Exact Isolate)。静的核(int/long・制御・配列・byte/boolean)は Slot IR 経由で純 Rust へ射影(a+b→wrapping_add(b)、>>>→論理シフト、MIN/-1 まで)。動的は決定論 JVM Isolate、真の非決定性は明示 reject。受理率 98.7〜100%、起動 約 41×・RSS 約 22× 小・p99 平坦。
ソースを意味論でなく一意な構造として Slot IR へ射影(π)。primitives は二の補数=SMT ビットベクタ理論で厳密化し Z3 が全入力(2³²/2⁶⁴/2⁸)で反例なし(UNSAT)で形式証明 31 件。ループ系は Csmith 流差分ファジング(約 63,000 ケース)が担保する二層保証。動的領域は実行時確定の瞬間に ②層 Lisp-JIT が bit-exact コードを生成。
本文の執筆: Claude(事前に固定オーサリング ― LLM をその場で走らせない=確率的ブレ「AI の罠」を排除)。意味でなく構造に落としてあるので、他の AI(GPT · Gemini · Grok …)でも同じ 4 層に再導出できます ― SlimeNENC の決定論思想。本文は常時表示なので、URL を読まない AI にも選択 → 貼り付けで渡せます。誰も置いていかない。
1. 振る舞い不変の検証(差分テスト)
テストは「穴がある」は示せても「穴が無い」は厳密証明できません。そこで C コンパイラ検証で使う 差分ファジング(Csmith 流):Java(二の補数 wrapping の正本)と生成 Rust を byte 突合します。決定論シードなので第三者が手元で同じ結果を再現でき、ズレが出れば失敗ケースがそのまま再現します。
| 手法 | 中身 | ケース | 結果 |
|---|---|---|---|
| ランダム差分ファズ(スカラ) | 2,250 本のランダム subset Java(全演算子・キャスト・三項・有界for・呼出・境界リテラル) | 53,932 | ✅ 全 byte 一致 |
| ランダム差分ファズ(配列込み) | 1,440 本(配列 index 読み書き・length・new・OOB 例外を追加) | 50,460 | ✅ 全 byte 一致 |
| 全極値の総当たり | 全二項演算 × 極値² {MIN,MIN+1,-1,0,1,2,MAX-1,MAX}・シフト量 {-1〜65}・int↔long 昇格・キャスト・単項・三項 | 2,900 | ✅ 全 byte 一致 |
| 実 OpenJDK Integer/Long verbatim | 自己完結 23 本(bitCount/reverseBytes/nLZ/nTZ/compare/hashCode 等) | 603 | ✅ 全 SHA-256 一致 |
合計 約 6 万ケースで Java と完全 byte 一致、逸脱 0。 実 19,950 メソッドを通しても誤受理(false-accept)ゼロ。炙り出した不一致は 1 件(Java の 64KB/メソッド上限=ハーネス側、コンバータの穴でない)で、サブメソッド分割で解消。
2. 形式検証 ― SMT で全入力を機械証明
差分テストはサンプル。整数を二の補数 = SMT ビットベクタ理論で厳密にモデル化し、全入力で変換器の出力が独立な数学仕様に等しいことを Z3 に証明させます(UNSAT = 反例なし = 証明)。
| 対象 | 仕様 | 結果 |
|---|---|---|
bitCount(32 & 64bit) | == popcount(SWAR の 16進マスク連鎖が母集団計数) | ✅ 全 2³² / 全 2⁶⁴ 入力で証明 |
reverseBytes / rotateLeft/Right / signum / lowestOneBit | byte 反転置換 / rotate / 符号 / i&-i | ✅ 32 & 64bit とも証明(計 12 本) |
除算(b≠0):a/b == bvsdiv ・ a%b == SRem ・剰余符号 | 0方向丸め / 符号は被除数 / 符号性質 | ✅ int/long とも証明 |
div-mod 恒等式 a==(a/b)*b+(a%b) | (除算×乗算の非線形) | ⏱ timeout(未決=要 bit-blast 調整、反例なし) |
集計:全入力 形式証明 20 件 / 反例 0 件 / timeout 2 件。 反例 0 = bit-exact に反する入力なし。唯一の未決は非線形の div-mod 恒等式のみ(値・符号は証明済で正しさは担保)。二層保証 ― primitives は SMT で全入力証明、合成・ループ・配列は約 6 万ケースの差分テスト。
3. 全 Java = Hybrid Bit-Exact Isolate
「全 Java 対応」は全部を Rust 化することではなく、全 Java を受理すること。任意の Java を 3 領域に自動分割し、領域ごとに最も強い正直な保証を貼ります:静的核 → 純 Rust(100% bit-exact)/ 動的 → 決定論 JVM Isolate(固定 JVM 前提 95-99%)/ 真の非決定性 → reject。
3-1. 受理率(実測)
| コーパス(実コード) | 静的→Rust | 動的→JVM Isolate | 非決定性→reject | Hybrid 受理率 |
|---|---|---|---|---|
| 実 OpenJDK Integer/Long/Math/Short | 17.5% | 82.1% | 0.4%(native) | 99.6% |
| 実アプリ(19,950 メソッド) | 0.5% | 98.2% | 1.3% | 98.7% |
| 動的多用(reflection/ラムダ) | 1.6% | 98.4% | 0% | 100% |
受理率 99% は「全 Java を扱える」ですが ≠「全部 Rust 化」。Rust 高速路に乗るのは静的核(左列)のみ、残りは決定論 JVM Isolate。reject は真の非決定性のみ(currentTimeMillis×84・getenv×50・nanoTime×22・Thread・Random・native)。「Hybrid 全体で常に 100%」とは決して言いません。
3-2. 自動パーティショナ + 規模検証
混在 Java を 1 コマンドで:分類 → 静的核を Rust ディスパッチャへ → 動的を Isolate Java へ(静的呼び出しは境界経由で Rust へ委譲)→ Hybrid 実行 → 原 Java と byte 一致 + 証明書。ランダム混在 Java を大量生成して検証:330 プログラム全 byte 一致、静的核 10,800 本を Rust 化、境界呼び出し 2,259 件を検証(逸脱 0)。
3-3. 例外境界 marshaling
静的核(Rust)が throw した例外を、Java 境界へ同一例外(型 + 文面)で再現。Rust が EXN\t<toString> を出力 → Java スタブが class 名で振り分け同型を再 throw → toString 完全一致。/0(ArithmeticException)・配列 OOB(Index N out of bounds for length L)・new int[-n](NegativeArraySize)を境界越しに 1,053 件検証、全一致。
4. 性能 ― 価値は「軽さ・予測可能性」
同一マシン・ext4 で公正に測定(JVM ウォームアップ込み、Rust は release)。throughput(ホット定常)は 3 者互角です。Rust が勝つのは別軸:
| 軸 | JVM | GraalVM-native | Rust |
|---|---|---|---|
| ホット throughput(定常) | 3 者ほぼ互角(「Rust 化で速い」はホット整数では成立しない) | ||
| 起動(短命) | 23.4 ms | 1.25 ms | 0.57 ms(~41×) |
| ピーク RSS | 41.2 MB | 7.7 MB | 1.9 MB(~22×小) |
| デプロイサイズ | 39 MB(最小JRE) | 8.8 MB | 432 KB(~90×小) |
| テール p99(GC圧) | 9.92 ms(jitter 4.6×) | — | 2.29 ms(jitter 1.1×) |
中央値は互角(JVM 2.19ms / Rust 2.09ms)でも、JVM は GC ポーズで p99 が中央値の 4.6 倍に跳ね、Rust は GC 無で平坦(1.1 倍)。p99 / SLA バウンドな処理(取引・リアルタイム・課金)で決定的。
5. seed 注入による reject 救済(decisionism)
非決定性 reject(seed 無 Random・実時刻)は、固定 seed / 固定 clock を注入すれば確定論化し、静的核へ昇格できます。正直な肝:これは振る舞いを*変える*(固定 seed ≠ 自由乱数)ので、bit-exact なのは「固定 seed 版」に対して=どこまで決定論を強制するか*決める*(decisionism、PSDP 安全度プロファイルと同型)。元の自由乱数は保存しません。
実証:java.util.Random.nextInt() の LCG を inline 実装し、new Random(seed) と全 seed 一致確認 → その確定列を Rust 化し byte-diff 0。救済不能なのは I/O・真の並行・native(これは reject のまま正直に)。
6. 実装・再現方法
すべて決定論的で、第三者が自環境で再実行できます(検証を相手の手元で走らせられる=他社との決定的な違い)。
bash run.sh # 基本 bit-exact
python3 fuzz.py 150 15 # ランダム差分ファズ
python3 adversarial.py # 全極値の総当たり
python3 smt_validate.py # SMT 全入力 形式証明(32/64bit + 除算)
python3 slimejava_partition.py X.java # 混在 Java を 1 コマンドで Hybrid 化 + 証明書
python3 fuzz_hybrid.py 30 150 # Hybrid 規模差分検証
sha256sum java.out rust.out # 第三者が手元で突合7. 関連リンク
SlimeJava 製品ページ SlimeNENC ファミリー SlimePython(モダン) PoC 依頼 / お問い合わせ