SlimeJava — 乾坤一擲

「全 Java 対応」とは、全部を Rust に書き換えることではない。全 Java を受理することである。

約 6 万件差分 + SMT 全 2³² 入力機械証明 + Hybrid 330 プログラム + 例外境界 1,053 件 + 「初の非空・本物」HybridDemo total=550 一致 — SlimeJava は LLM 業界の「ほぼ等価」と次元の違う道を歩む。

序章 — なぜ乾坤一擲か

ソフトウェア業界の現代的論争 — 「LLM ベース変換 vs 形式手法」「確率的 AI vs 決定論的 AI」「ニューラル vs シンボリック」 — は、1960 年に Lisp と COBOL がほぼ同時に生まれた分岐点に起源を持つ。60 年の数理 ↔ IT 工学の分離を、Java という業界中心言語で修復する試みが SlimeJava である。

本稿は SlimeJava 単体に絞り、その設計哲学・実証データ・誠実な限界開示・将来計画を一気通貫で記す。Java を扱う全エンジニア、監査担当者、CTO、研究者に向けた乾坤一擲の論考である。

第 1 章 — 設計哲学:「意味を理解しない、構造を転写する」

「理解」しないからこそ bit-exact

Java の意味論を「理解して」書き直すアプローチには、構造的欠陥がある。

「意味を理解する」アプローチ SlimeJava

解釈が人によって揺れる構造は曖昧さなく一意

揺れが移行に持ち込まれる構造保存で揺れゼロ

「ほぼ等価」が限界 1 ビット完全一致

LLM 確率的生成 LLM 不在・経路上に確率なし

SlimeJava はソースを構造(曖昧さなく一意)として扱い、Slot IR へ射影 (π) し、構造を保存したまま Rust へ転写する。意味の層を通らないので結果は数学的に厳密 — 何度実行しても出力は 1 ビット一致する。

絶対ルール:isolate, don't confabulate

「ほぼ等価」「意味的に同じ」出力は決して出しません。

入力が静的サブセット外の構文を含む場合、SlimeJava はその関数を隔離帯へ送り、黙って訳しません — 該当理由を返します。

推測で変換するくらいなら、変換しない。

これは技術選択ではなく哲学的決定である。LLM 業界が「とにかく出力する」のと正反対の立場。

第 2 章 — 全 Java 対応 Hybrid Bit-Exact Isolate

「全 Java 対応」の再定義

「全 Java 対応」とは、全部を Rust に書き換えることではない

(オブジェクト/String/double/反射は bit-exact に Rust 化できない)

全 Java を受理することである。

任意の Java を 3 領域に自動分割し、領域ごとに最も強い正直な保証を貼る:

領域変換先保証

静的核(整数/制御/配列/ビット) → 純 Rust 100% bit-exact(+ SMT で全入力形式証明可)

動的(オブジェクト/String/double/HashMap/反射) → Java のまま、決定論 JVM Isolate 固定 JVM 前提 95-99%(CI 維持)

真の非決定性(seed 無 random/実時刻/I/O/真の並行) → reject bit-exact 保証なし(明示)

核心:動的 Java を Rust で再発明しない。動的は Java(決定論 JVM)に意味を生成させる。理解しないことによって bit-exact を守る — SlimeJava の哲学を動的領域へ拡張。SlimePython §14 と同型構造。

受理率(実測)— 静的のみ 37% の壁を突破

コーパス(実コード) 静的→Rust 動的→JVM Isolate 非決定性→reject Hybrid 受理率

実 OpenJDK Integer/Long/Math/Short 17.5% 82.1% 0.4% 99.6%

実アプリ(19,950 メソッド) 0.5% 98.2% 1.3% 98.7%

動的多用(reflection/ラムダ) 1.6% 98.4% 0% 100%

正直な分離:受理率 99% は「全 Java を扱える」だが ≠「全部 Rust 化」。bit-exact で Rust に剥がれ、軽さ・起動 41×・SMT 全入力形式証明の恩恵を受けるのは静的核(上表の左列)だけ。残りは決定論 JVM Isolate で Java のまま(固定 JVM 前提 95-99%、cross-version drift は CI で潰す運用範囲)。真の非決定性は reject。「Hybrid 全体で常に 100%」とは決して言わない(AI 罠 17 回避)。

第 3 章 — 穴なし証明:差分ファジング約 6 万ケース

テストは「穴がある」は示せても「穴が無い」は厳密証明できない。だから C コンパイラ検証で使われる差分ファジング(Csmith 流) で攻める:ランダムな subset Java を大量生成し、Java(= 二の補数 wrapping の正本)と生成 Rust を byte 突合。1 件のズレも穴とみなし、出たら直す。

手法中身ケース結果

ランダム差分ファズ(スカラ) 2,250 本のランダム subset Java 53,932 ✅ 全 byte 一致

ランダム差分ファズ(配列込み) 1,440 本(配列 index 読み書き・length・new・OOB 例外を追加) 50,460 ✅ 全 byte 一致

全極値の総当たり全二項演算 × 極値² {MIN,MIN+1,-1,0,1,2,MAX-1,MAX}・シフト量・int↔long 昇格 2,900 ✅ 全 byte 一致

実 OpenJDK Integer/Long verbatim 自己完結 23 本 603 ✅ 全 SHA-256 一致

合計約 6 万ケースで Java と完全 byte 一致、逸脱 0。実 19,950 メソッドを通しても誤受理(false-accept)ゼロ。

正直な但し書き

差分テスト = テスト空間での穴の不在を高い確度で示すもの。形式証明ではない(それには verified validator / Coq)。「穴なし」は実務的な意味である。空虚な主張を避け、未測定の範囲を 100% とは言わない。

第 4 章 — 形式検証: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 万ケースの差分テスト。「形式証明ではない」という弱点を実質的に潰す。LLM 変換ツール(「意味的にほぼ等価」)とは次元が違う。

第 5 章 — Java 整数の「隠れトラップ」を Rust で再現

Java と Rust は整数の意味論が違う。naive に + を + へ写すと静かに壊れる(Rust の + は overflow で panic / 定数ならコンパイル拒否)。SlimeJava は右列を機械的に生成し、Java の挙動を 1 ビット違わず再現する。

Java 構文 Java 意味論生成する bit-exact Rust

a + b a * b 二の補数で wrap a.wrapping_add(b) 他

a / b a % b MIN/-1=MIN、0方向丸め、0除算は例外非ゼロ証明できる所は plain、できない所は Result + ? で例外を写す

a << b / >> / >>> シフト量 &31(long は &63)、算術 / 論理 wrapping_shl/shr、>>> は as uN 経由

-a(-MIN) -MIN=MIN a.wrapping_neg()

int × long numeric promotion → long 各被演算子を as i64 昇格

例外も bit-exact

Java の a/0 は ArithmeticException: / by zero を投げる。SlimeJava はこれを捨てず、Rust の Result + ? で例外伝播ごと写し、両言語とも例外時に同一バイト列を出力する。正常値だけでなく、プログラムの観測可能な振る舞い全体(例外含む)が一致する。

例外境界 marshaling — 1,053 件全一致

静的核(Rust)が throw した例外を、Java 境界へ同一例外(型 + 文面)で再現する:

EXN\t<toString> を Rust が出力

Java スタブが class 名で振り分け同型を再 throw

toString 完全一致

/0(ArithmeticException)・配列 OOB(Index N out of bounds for length L)・new int[-n](NegativeArraySize)を境界越しに 1,053 件検証、全一致。

第 6 章 — 自動パーティショナ + 規模検証

混在 Java を 1 コマンドで:分類 → 静的核を Rust ディスパッチャへ → 動的を Isolate Java へ(静的呼び出しは境界経由で Rust へ委譲)→ Hybrid 実行 → 原 Java と byte 一致 + 証明書。

$ slimejava-partition HybridDemo2.java
partition: STATIC=[sumw]  ISOLATE=[main]  REJECT=[]
原 Java : weighted=550 avg=110.0000 label=Q3-report
Hybrid  : weighted=550 avg=110.0000 label=Q3-report
検証    : ✅ byte-identical (sha256 b46bd2e5…)

規模検証

ランダム混在 Java を大量生成して検証:330 プログラム全 byte 一致、静的核 10,800 本を Rust 化、境界呼び出し 2,259 件を検証(逸脱 0)。

HashMap・double・TreeMap・sort・String 整形と動的機能を跨いで実証済み。

第 7 章 — 性能:価値は「軽さ・予測可能性」

throughput(ホット定常)は 3 者互角。Rust が勝つのは別軸:

軸 JVM GraalVM-native Rust(SlimeJava 出力)

ホット throughput(定常) 3 者ほぼ互角 — 「Rust 化で速い」はホット整数では成立しない

起動(短命) 23.4 ms 1.25 ms 0.57 ms(JVM比 ~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 バウンドな処理(取引・リアルタイム・課金)で決定的。

→ 価値は「速い」でなく「軽い・予測可能・bit-exact」。出力は全条件で bit-exact のまま。

第 8 章 — 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 のまま正直に)。

第 9 章 — 三者協働構造:実走で炙り出された AI の限界

実走レポート(2026-06-13 → 2026-06-14 → 第三走)

走主な収穫

初回(2026-06-13) AI 予測の崩壊 + 6 穴炙り出し

第二走(2026-06-14) 私の前回診断訂正(複合代入ではなく i++) + 3 修正

第三走多重宣言 + 拡張 for + LargeScaleMix 真の Hybrid

AI 自身も検証対象である

AI(LLM)が試験コードと予測分類を出した時、実機が予測表を構造的に崩した。さらに「複合代入 += ^= が原因」という AI の診断自体が誤っていた。実機が ++ がトークナイザに無く i++ が二つの + に分解される という真因を返した。

これは AI 意味揺らぎ vs Bit-exact の生きた実証である。

主体揺らぎ状態役割

AI 構造的に揺らぐ提案・補完

実機 / Slot IR 構造的に揺らがない検証・判定

検証ハーネス揺らぎ可能 Java の split(" ") のバグで誤報寸前

人間構造発見の知性不変量抽出・境界設計・誠実開示

→ 「AI も検証ハーネスも揺らぐ、実機だけが揺らがない、人間が構造化する」という三者協働構造。これがドメイン斜め読み工学の Java 領域実装。

累計進捗

指標修正前(初回実走) 現在

projected 11 18

真の end-to-end Hybrid byte-diff 0(全 vacuous) 2(HybridDemo / LargeScaleMix)

修正した穴 — 5 点(++/-- ・ getenv ・ vacuous cert ・多重宣言・拡張 for)

第 10 章 — 残る穴と次のアクション

残る未修正穴(整数核で落ちる)

穴落ちるメソッド性質

文字列リテラル throw new X("msg") safeDiv, signDiv, signMod tokenizer 拡張必要

byte[] 引数 fnv1a64 型システム拡張必要

boolean 型/リテラル divModConsistent parser + 型システム拡張必要

塞げば STATIC は 18 → 24 程度へ拡大。

意味境界として正しく弾いているもの

メソッド弾く理由

reverse void の配列 in-place 破壊(a[i]=a[j])は Java 参照渡し vs Rust Vec 値渡しで意味が変わる

make(int[] 返し) dispatcher が i64 しか返さない protocol 制約

→ parser 穴ではなく意味境界。「対応できる」と「対応すべき」を厳密区別。

中期テーマ:②層 Lisp-JIT

3 層モデル:

層計算保証

① 静的射影(SlimeJava 静的核) 整数 / 論理 byte 一致(SHA-256)

② Lisp-JIT 実行時確定後 bit-exact byte 一致(確定後)

③ 意味判定原理的非再現意味同値 + 残差

Hybrid は ②層完成前の中間解として明確に位置づけられている。

第 11 章 — 第三者再現:6 コマンドで完結

すべて決定論的で、第三者が自環境で再実行できる(検証を相手の手元で走らせられる = LLM 系との決定的な違い)。

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       # 第三者が手元で突合

LLM ベース変換ツールはこれを構造的に提供できない。

第 12 章 — LLM 変換ツールとの次元的差異

観点 LLM ベース変換 SlimeJava

保証確率的(「ほぼ等価」) SHA-256 同値 + SMT 全入力証明

検証規模統計サンプル約 6 万差分 + SMT 20 件全入力(40 億)+ Hybrid 330

動的領域対応ブラックボックス Hybrid 98.7-100% 受理 + 領域別保証明示

例外境界ベスト・エフォート toString 完全一致 1,053 件

性能訴求「速い」「軽い・予測可能・bit-exact」(p99 4.3×)

第三者再現不能 6 コマンドで完結

契約要件適合 × ⭕(機械証明 + 証明書)

AI 罠 17 頻発「Hybrid 全体で常に 100%」と言わない

LLM 変換ツールは原理的に確率モデル。SlimeJava は数理モデル。同じ「Java → Rust」を扱うが、軸が直交する。

第 13 章 — 1960 年以降の分離との接続

Lisp(1958)= 数理軸の極北、COBOL(1959)= IT 工学軸の極北。両者がほぼ同時に生まれ、60 年逆方向に発展した。SlimeJava は Java の整数核を二の補数(数理)として扱い、動的領域を JVM Isolate(工学)に委譲することで、両軸を Slot IR で再合流させる。

修復対象 SlimeJava の解

Java 整数の数学性二の補数 wrapping を bit-exact 再現

Java 動的性 Hybrid JVM Isolate で工学的に委譲

数理と工学の境界 partition CLI で構造的に分離

検証の信頼性 SMT 全入力証明 + audit chain

→ SlimeJava は 60 年の分離を Java で修復する事業。

結論 — 乾坤一擲の総括

SlimeJava の核心 5 点

「全 Java 対応」を「全 Java 受理」と再定義 — Hybrid 受理率 98.7-100%

SMT で全 2³² 入力機械証明 — 20 件証明済 / 反例 0 / LLM と次元が違う

Hybrid 規模検証 330 プログラム + 例外境界 1,053 件 — 真の bit-exact 実証

性能の別軸(起動 41× / RSS 22× / footprint 90× / p99 4.3×) — SLA バウンドで決定的

第三者再現 6 コマンド — 検証を相手の手元で走らせられる

哲学的決定打

「理解しないことによって bit-exact を守る」

これは禅問答ではなく、60 年の数理 ↔ IT 工学分離の修復解である。LLM 業界が「理解する AI」を志向する中、SlimeJava は「理解しない構造主義」を選択する。それが Java で監査適合 + bit-exact を成立させる唯一の道である。

残る課題

3 穴(文字列リテラル / byte[] / boolean) — 中期で順次対応、STATIC 18 → 24 へ

②層 Lisp-JIT — 動的領域の段階昇格

cross-version drift(95-99% → 99.9%) — CI で継続

適用対象

金融バッチ・課金・トレーディング(p99 SLA バウンド)

暗号プリミティブ(integer hash / SWAR / xorshift)

監査要件下の業務基幹(SOX / FISC / FFIEC)

規制業界の Java/Kotlin 移行(bit-exact 必須)

短命プロセス(サーバレス / cron / per-request)

LLM 業界と次元が違う

LLM 変換ツールは「意味的にほぼ等価」を提供する。SlimeJava は「1 ビット完全一致 + SMT 全入力機械証明 + 第三者再現可能」を提供する。同じ問題に異なる軸で答える。

→ Java を扱う全エンジニアは、両軸の存在を知るべきである。そして監査・救済・千年継承を志向するなら、SlimeJava 軸しか選択肢がない。

これが SlimeJava の乾坤一擲である。