PSDP — 検証記録と取り下げ台帳
本ページは PSDP 製品ページから開発過程を分離した一次資料です。 2026-08-17 〜 18 に実施したリリース前試験、独立した別エンジンによる監査、 そこで崩れた自社の主張と、その後の修正の経緯を記録します。 製品ページには、この検証を通過した内容だけを掲載しています。
この頁の目的は、自社に都合の悪い記録を残すことです。 崩れた主張は取り消し線で残し、いつ・何によって崩れたかを書きます。 「壊れないこと」を売る製品が、自社の主張が壊れたときに黙るわけにはいきません。
1. 停止した主張 取り下げ
2026-08-17、独立監査 (別 AI エンジンによる整合性監査) の指摘を全件こちらで再現しました。すべて再現しました。 実測値・digest 自体は合格 (架空の兆候なし)。崩れたのは一般化と検査器です。
| 取り下げた主張 | 崩れた理由 (再現済) |
|---|---|
使えません。build が埋めた record_sha256 を verify が
一度も照合していませんでした。build ba2f77d1… / verify 4c202cca… でも判定は VALID。
prev_hash 連鎖・Ed25519 署名・重複キー・必須値・型範囲の検査も未実装でした。
ハッシュは飾りで、何も証明していませんでした。(修正済 → §4) | |
崩れました。反例 2 件 —
① FROM sales JOIN lines … ORDER BY sales.id は JOIN 後に主キーが重複するのに [OK]
② u INT UNIQUE に対する ORDER BY u は PostgreSQL が NULL を複数許すのに [OK]。
原因は FROM の最初の表しか見ず JOIN を認識していない / UNIQUE の NOT NULL を確認していない。 | |
偽です。反例 a=253, b=1, c=-253 →
(a+b)+c = 0 / a+(b+c) = 1。訂正: 値がすべて整数 かつ どの分割順序でもすべての途中和の絶対値が 253 以内。 非負に限れば総和条件で十分ですが、金額は返品・値引き・赤伝で負値が出るため、 「銭単位の整数なら並列 SUM 可」という助言も相殺のある会計では危険として停止しました。 | |
| 誤りでした。自分の実測表を数え直すと 5 件中 4 件が「速いが壊れる」 (数値計算 6.11× / 画像ディザ 5.47× / 表計算 2.05× / RDB 判定違反。遅いのは TCP パケット分割 0.43× のみ)。 正しくは「誤分割は速くなることの方が多い。だからこそ誘惑が強く、検証機が要る」。 | |
BigDecimal.add は結合的 |
限定が要ります。無制限精度の exact add に限ります。
MathContext を伴う overload は各回丸めるので非結合
(MathContext(3), a=1.00, b=0.006, c=0.006 → 1.02 / 1.01)。 |
第 2 次監査で否定されました。実体は「意見つきの grep」でした。
ORDER BY を 3 つ含む .sql を食わせて「0 箇所 / 危険 0 / 未判定 0・終了コード 0」=
空ファイルと出力が同じで CI を素通り。
解析ロジックの中は fail-closed でも、入口が fail-open でした。 |
累積した停止事由 7 件のうち、fail-open が 3 件でした。 「fail-closed が製品の一線」と宣言しながら、実装は fail-open だった、という形です。 現在の受け入れ判定は「自動修正・安全証明・成功報酬判定には使用不可。 人間が再確認する検索補助としてのみ条件付きで使用可」です。
1-b. ★★「偽受理ゼロ」の正しい読み方
旧版の入口は、実質 compute(seed) → 2 次元 float 配列という専用 signature でした。
実在 Python 102,750 関数で完全適合は 0 件。
意味の判定に到達する前に、形で全件が落ちていたのです。
したがって「公式 fixture だけが通る」のは、それが規約用 kernel だったからであって、
「危険なコードを意味的に拒否できた」という意味ではありません。
★ 偽受理ゼロを、一般コードに対する安全性として読んではいけません。
| 野良コード試験が直接支持したこと | 状態 |
|---|---|
| 旧 signature Admission では実在コードへの到達率がほぼゼロ | 確定 |
規約適合 kernel では bit-exact 性が成立(6 言語で 0xe718490618e7f144 一致) | 確定 |
| 汎用の意味 Admission はこれから構築する | 未着手 |
★★ この 3 点をひとつの原理にまとめたのが、製品ページの中心契約です。
「PSDP は、意味同値性を証明できた区間だけを並列化する。証明できない区間は、元の逐次実行を維持する。」
この一文なら、並列化しなかった 4 件・HNSW だけ artifact 凍結で通した判断・
bit-exact の証拠・意味 Admission への転換が、すべて同じ製品原理の帰結として並びます。
「証明できた区間」の範囲が今は規約の内側にとどまる、というのが現在地です。
2. 旧掲載値の扱い 一次記録の再確認待ち
旧製品ページに掲載していた次の数字は、2026-08-17 の試験で一次記録 (bench 出力・ログ・CSV) を発見できませんでした。 「存在しない」ことの証明ではなく、「今回の探索範囲では出てこなかった」という状態です。 記録が出るまで製品ページからは下ろしています。
| 旧掲載 | 現在の状態 |
|---|---|
| 2.97 〜 4.23 倍 (行列乗算 N=700) | 取り直しました。総仕事量 200,000 task 固定・20 コアで
Go 4.05× / C# 2.81×。桁も順位 (Go > C#) も一致し、誇張ではありませんでした。
ただし検体が違います — 変換器に同梱されているのは matmul の N=16 だけで
(22 変換器を全数調査)、N=700 の一次記録は見つかっていません。製品ページは実測値と条件に差し替えました。 |
| 障害ロールバック 90 / 90 | 一次記録を発見できず。掲載を停止。 |
| TPC-H Q1 / Q6 4.38 〜 5.20× | 一次記録を発見できず。掲載を停止。 |
| CDC replay 4.26× | 2026-08-17 の実測では逆に遅くなりました (0.46 〜 1.00×)。epoch 構築コスト勝ち。 掲載を停止し、「効かない」と記録します。 |
| SQLite WAL reader 9.76× | 一次記録を発見できず。掲載を停止。 |
| AVX-512 3072 / 3072 bit-exact PASS | 一次記録を発見できず。掲載を停止。 なお AVX-512 の 0.93 〜 1.04× (memory-bound) を数値計算全体へ一般化したのは誤りでした。 |
| SlimeTree-VSAM 統合で PostgreSQL 比 1,900 〜 3,800 倍 | 「合成」と自ら明記していた見込値ですが、合成元が上記 2.97 〜 4.23× (matmul のみ) のため 掲載を停止。 |
| ビルド時にバイトコードを読んで並列箇所を発見し「注入」する | この機構の実装は全文検索で見つかりませんでした。
実体は compute(seed) 規約に従った kernel を並列実行 driver で包む wrapper 生成器です。
掲載を停止。 |
| ★★ 自社の実測が否定しました。待ちが支配する処理こそ最大の倍率が出ています —
実 TCP 16.88× (4 分野で最大) / 往復遅延律速 8.57× /
N+1 の画面 5.95×。しかもCPU 消費は 0.63〜0.71 倍に減ります
(スレッドはブロックしているだけで CPU を食わない)。
DB は実際にはキャッシュから返ることが多く、その分並列化が素直に効きます。
射程外なのはデバイス帯域で詰まっている純 I/O だけで、
旧記述は「I/O = 遅い = 手が出ない」と読ませる誤った一般化でした。掲載を停止。 ★ ただし待ちの並列化は接続占有 (conn-ms) を増やすため (6.34 → 8.47)、N+1 は1 本にまとめる方が 15 分の 1 (0.42 conn-ms)。 手段の選択自体が判定対象です。 | |
| FFT / Conv2D / LU 分解を bit-exact 並列化 | 該当検体が存在しません。掲載を停止 (適用候補ではあります)。 |
| bit-exact 378 / 378 | 実在し、再現しました (golden d2fc575a50086c6f)。
ただし Track A の実行モデルは自ら sequential in topological (phase) order と明記しており、
生成物にスレッドは 1 つもありません。
= 決定性の実証であって、並列性能の実証ではありません。
製品ページでは速度と別ブロックに分けて掲載しています。 |
3. 検証機の来歴 — 修正のたびに新しい欠陥を作りました
解析器は Rust で実装しています。以下は作り込んだ欠陥の記録です。
| v1 の事故 | 既定判定が「可換」= fail-open だったため、顧客が書く形の素の JDBC バッチで
7 ループ中 2 つを誤判定。特に customerNet.merge(cust, net[i], Double::sum) を
「そのまま並列化可」と答えました。実測すると 471/512 顧客でビット不一致、
さらに run1 と run2 でも 478/512 不一致 = 顧客別売上が毎晩違う値になるコードです。 |
|---|---|
| v2 の変更 | ① 既定を未判定 = 並列化しない (fail-closed) ② 共有コレクションへの merge / put / compute で畳み込む値が浮動小数なら非可換 ③ JDBC オブジェクトは非可換 ④ ループ変数添字のローカル配列書き込みだけ無条件可換 ⑤ ローカルコレクションは条件付。 |
| v3 (BigDecimal) | BigDecimal.add の畳み込みは値もスケールも結合的 (scale=max は結合的) →
並列化して bit-exact。同じ集計が double では 471/512 不一致、BigDecimal では 0/512 一致・4.38×。★ ただし ADD…ROUNDED (畳み込みの中に setScale) は非可換。
実測で HALF_EVEN が 0.01 ずれました。HALF_UP は一致しましたがそれはたまたまです。★★ 「丸めがあるか」ではなく「丸めが畳み込みの中にあるか」で分けます。 |
| 監査で作り込んだ 欠陥 (記録) |
① JOIN / nullable UNIQUE を塞いだら list.add / sb.append / break を全部 OK にする false-safe を3 件新造② それを塞いだら Math.floor() を「外部作用」と誤認して本物の危険判定を未判定へ落とす③ 純粋関数の除外を入れたら分岐の書き方を誤り効いていなかった ④ PURE 除外リストに Arrays Collections を入れていたため Arrays.fill が [OK]⑤ 型解決がリスト順で上書きされ、別メソッドの int total が double total に勝っていた⑥ 根本原因: recv.method( の形しか見ておらず、helper(x) のような
修飾なし呼び出しが 1 つも見えていなかった。この 1 穴が指摘のほとんどを説明しました。 |
| 現在 | 修正版では示せない限り未判定に落とす方向に倒しています。 pgjdbc 601 ファイルの推移: v1 OK 47 (誤警告 1・未検査 0 = fail-open) → 現 OK 4 / 危険 0 / 未判定 72 / 未検査と明示 568。 安全側ですが、使い物になるかは別問題で、この問いは未解決です。 |
| 未対応 | 正規表現ベースのまま (正式な構文解析への置き換えが製品化条件) /
while(rs.next()) 直書き・Stream API 未対応 /
prev_hash の実連鎖検査は形式しか見ていない / 異 CPU・異 OS での digest 再測定は未実施。 |
4. 評価設計 — この表以外で性能を語りません
監査の提案を受け、2 × 3 表を採用しました。3 値では 実在の欠陥が [OK] に入るセル (偽安全判定) が抜け落ちます。
| 実行で確認した事実 \ 判定 | 危険 | 未判定 | OK |
|---|---|---|---|
| 順序依存あり | 真陽性 | 棄権による未検出 | ★ 偽安全判定 |
| 順序依存を確認できず | 偽陽性候補 | 棄権 | 真陰性候補 |
- 棄権と偽安全判定は重さが違います。棄権は人が見るので拾える余地が残りますが、 OK は人が見ないので出荷されます。偽安全判定は単独の停止条件で、加重平均に混ぜません。
- 非対称性: 順序を変えて差が出た = 順序依存の実証。 変わらなかった = 安全の証明にはなりません。だから行 2 は「順序非依存」ではなく「確認できず」です。
- 順序を変える手段のうち実測済は、更新による物理移動 / エンジン差し替え / 並列度変更。 fetch size・入力分布は未実施。差が出なかった手段は「安全」ではなく「その手段では出なかった」と記録します。
- ラベルの単位は
(コード, 入力, 実行条件, 観測契約)。 コード単位に丸めると「更新前は緑」を再現します。
評価の枠を 3 回間違えた記録:
① カバー率 (OK の割合) を製品価値の指標にした ② 「未判定は指摘しないだけ」と棄権を無害扱いした
③ 正解ラベルを自分で付けて「再現率 6%」を出しかけた。
都合の良い枠も自罰的な枠も同じく無効で、正解ラベルを自分で決めた時点で数字は死にます。
2×3 表を採用したのは、正解が実行から来るため枠を選ぶ余地が構造から消えるからです。
さらに「分母を見ずに 0 を良い数字として読む」を 3 回、
「適合率の分母を偽陽性率に流用する」を 1 回やりました。
例: 「pgjdbc 601 ファイルで誤警告 0」は実績になりません — 危険判定そのものが 0 件 = 分母 0 = 評価不能です。
正しい言い方は「危険判定 0 件。よって偽陽性も観測されていないが、誤警告率は評価不能」。
5. 観測契約 — ラベルの第 4 次元
実在の Common Lisp 会計ソフト (cl-ledger, commit b0174f56 / SBCL) を、
同じ 3 仕訳の全 6 順列で実行しました。
| 観測対象 | 6 順列の結果 |
|---|---|
| 最終貸借表 | 6 / 6 同一 |
| ランニング残高 | 6 / 6 別結果 |
同じコード・同じ入力・同じ環境で、ラベルが逆になります。
したがって正解ラベルの単位は (コード, 入力, 実行条件, 観測契約) であり、
観測契約を書かない「bit-exact」は無効です。
これは自分の実測でも既に起きていました — ORDER BY 欠陥は
内訳は違うのに合計は完全同一 (3,238,609.2700000014) でした。
合計だけを観測していたら検出できていませんでした。気づいて書いたのに、一般化しませんでした。
6. 分野別の実測 (2026-08-17 〜 18)
| 分野 / 検体 | 実測 | 読み方 |
|---|---|---|
| 行列乗算 / 画像畳み込み / 表計算 / 実 TCP (Rust, std のみ) | 6.67× / 6.30× / 5.35× / 16.88× | 正しい軸で分割すればスレッド 1〜20 のどれでも digest dfcf3fee29d7d15c 固定。
違反版はスレッド数ごとに全部違う値。
★ 正しい軸は分野ごとに全部違います (行 / 位相 / 接続 / id レンジ) =
分野を広げるほど判定器の作り込みが要ります。 |
| RDB 夜間バッチ (PostgreSQL 16.14 実サーバ ほか 5 エンジン) | fetch 分割で 3.26 〜 5.81× | bit-exact は 20/20 完全 (違反腕は全部壊れた)。律速は fetchで、 app 側だけ並列化しても全体 1.05×。50 万行から効き始めます。 |
| EC 受注バッチ (税率 / クーポン / ポイント / 切り捨て) | 2.98 〜 4.54× (5 エンジン bit-exact) | 違反腕は 6.09× で、しかも税額の下位ビットが変わります
(…767999999E8 → …768000002E8)。 |
| EC オンライン (買い物履歴 N+1) | 50 注文 5.95× / 200 注文 5.29× | CPU 消費は 0.63 〜 0.71 倍に「減り」ます (待ちの並列化はスレッドがブロックするだけ)。 ★ ただし conn-ms は 6.34 → 8.47 と増え、 1 本にまとめる方が 0.42 conn-ms = 15 分の 1。 並列化はこの問題には間違った道具です。 |
| 負荷試験 (プール 16 本共有) | 交差点は同時 8 〜 16 | 同時 1〜8 は並列が圧勝 (応答 3.3× / スループット 3.5×)、
同時 16 以降は逐次が圧勝。
★ 素朴な実装はデッドロックします (接続を 1 本ずつ borrow すると同時 8 で停止)。
Semaphore.acquire(n) の全部か無かの確保で解消。 |
| 競合 (実 PostgreSQL / C# Npgsql) | 単一口座 0.96× / 楽観ロック 0.10× | 正しくやると逐次より 10.2 倍おそく、壊れた版とは 87.6 倍差。 93% 喪失版が速いのは更新の 93% を捨てている = 仕事をしていないから。 ★ 競合行に楽観ロックは誤った道具で、行ロック / 直列化の方が 9.9 倍はやく、しかも正しい。 |
| 取り込み律速 (cl-ledger 50 万仕訳) | 貸借表 1.06× | 初回 5.208s / キャッシュ後 0.308s = 読込・binder 構築が 94.1%。 集計を無限コアで並列化しても伸びません。訴求点は集計でなく取り込みの並列化ですが、 取り込み並列化はソース無改変ではできません。 |
| RAG 順位 (Haystack 2.31.0) | 同点 24 文書 → top5 が 100 種類 | Haystack の欠陥ではなく「同点をどう解くか決めていない」。 同点 24 から top5 は順序つき 5,100,480 通りすべて同資格。 ★ ID 二次順序でコストほぼゼロで決定論化できます (今回唯一の「タダの正しさ」。f64 残高は型改修が要り、競合行は 10.2 倍おそい)。 |
7. 律速は 4 種類あります
| CPU (取り込み) 律速 | 1.06× — 集計を並列化しても伸びない |
|---|---|
| fetch 律速 | 3.26 〜 5.81× — 効くが、fetch 自体の書き換えが要る |
| 往復遅延律速 | 8.57× — 最も効く |
| ★ 競合律速 | 1.00× — 効かない。勘定系が実際に持つのはここ (統制勘定・在庫・採番) |
8.57× が出る条件 (競合なし) と、現実 (競合あり) は違います。 適用判定の目安: 計算部分が全体の 20% 未満 → 対象外 / 20〜50% → 金額が整数か BigDecimal なら条件付 / 50% 超 → 候補。加えて double 建てかつ観測契約にランニング残高が入る場合は対象外、メモリ律速も対象外。
8. 検証できていないこと 未検証
- ★★ ソース無改変のまま速くなった実測は 0 件です。
掲載しているすべての速度は、並列実行部をこちらで
ExecutorService等で実装して測っています。 正しい位置づけは「変換ツールが完璧に動いたときの上限」であり、 実装も測定も無い状態です (未解決)。 - 検証機の検出性能は未測定です。安全な対照集合が 3 件しかなく、分母 3 では性能を語れません。
- トランザクション間の異常 (lost update・デッドロック・分離レベル) は構造的に対象外です。 「検証機合格 = 導入可否」を範囲を明記せずに名乗ると、偽安全判定と同じ害になります。
- Java の速度実測が 0 件です。本流 (Track A) は逐次実行、変換器 6 本のうち 3 本は
new Thread(を task ごとに作るため構造的にスレッド数を振れません。 - 変換器同梱の検体は行列乗算 1 本です。EC・RDB の実測は変換器を通していません。
- 異 CPU・異 OS での digest 再測定は未実施です (digest は機械が違っても一致するはず / 絶対時間は一致しない、が設計上の前提)。
- 一次記録の探索範囲は
SlimeNENC配下と HP バックアップまでです。他ドライブは未探索のため、 §2 の「発見できず」は「存在しない」ことの証明ではありません。 - 言語別オプション (SlimeJava2Java / SlimeCSharp2CSharp / SlimeGo2Go / SlimeRust2Rust ほか) はすべて未実装です。Go / No-Go 判定用の検体 (BigDecimal の残高推移・EC バッチ 1 本) の作成が次の作業で、最優先は SlimeJava2Java (Java の倍率実測が 0 件のため)。
- 保証の二段構え (前段 = 同一言語内で bit-exact / 後段 = 並列度・スレッド数・DB エンジン・言語をまたいでも完全一致) のうち、後段は実測が揃っています (
0xe718490618e7f144/dfcf3fee29d7d15c/ DB 5 エンジン同一ビット)。前段を自動変換で出す部分が未実装です。
9. 測定条件 (再現のために)
| DB エンジン | PostgreSQL 16.14 (実サーバ) / H2 / HSQLDB 2.7.3 / SQLite / Derby |
|---|---|
| 実装言語 | Rust (標準ライブラリのみ) / Java / C# (.NET 8) / Go 1.22 |
| 速度測定の原則 | 総仕事量を固定して並列度だけを変えます (200,000 task 固定・20 コア)。 「スレッド = タスク」の実装は同一仕事量でスレッド数を振れないため、速度を測れません。 |
| 罠 (実測) | ★ H2 はクエリ結果をキャッシュします (初回 941ms → 2 回目 0.3ms)。
best-of-N で測ると 3,000 倍速く見えます。冷 (初回) も併記します。 ★ localhost PostgreSQL (RTT ≒ 0.05ms) の測定は待ちを大幅に過小評価します。 本番は往復ごとに RTT が乗ります。 ★ 他社トップページの TTFB を比較に使う場合、HTTP 202 / size 0 の bot 即答は ページ生成時間ではありません。 |
| 陰性対照 | すべての測定に判定違反の腕を置いています。 違反腕が壊れることまで確認して初めて、測定が成立したと見なします。 |
