これは何か: Almide を 0 から作り直す v1 の、証明・信頼アーキテクチャの 完成形を一枚で示す構想文書。手順ではなく、出来上がった姿を記述する。 この会話/既存文書を読んでいない人が、頭から読んで理解できるよう、独自語彙は すべてその場で定義する。 兄弟文書: trust-layer(カテゴリ戦略 L0-L4)、 receipt-logic(受領書の形式)、 completeness-by-construction(意味論台帳)、 certification-grade(認証級硬化)。 本文書はそれらの着地形を一つの絵に畳んだもの。
AI がプログラムを大量・高速に書く時代になり、ソフトウェアのボトルネックは 「書けるか」から「信じられるか」へ移った。コードはほぼ無料で湧くが、 湧いたコードを人間が全部読んで安全性を確認することは、もう不可能。
これまでソフトの信頼は 「誰が書いたか」(著者の評判 + 人間レビュー)で 担保してきた。だが著者が機械になると、評判は蓄積せず、書く速さに読む速さが 追いつかず、壊れても責任を問う相手がいない。人格に紐づく信頼は機械の著者に スケールしない。
残る唯一の道は、著者ではなく成果物そのものを検証すること。 「信じてください」ではなく「自分で確かめてください」にする。 Almide v1 は、これを言語とツールチェーンのアーキテクチャそのものにする。
コンパイラの正しさは証明しない。小さな検査器の健全性だけを証明し、 コンパイラには各ビルドで「証明書」を吐かせ、検査器が毎回それを照合する。
根拠は、世の中の単純な非対称性 ―― 作るのは難しいが、確かめるのは桁違いに 易しい(数独を解くのは大変だが、解けた数独の検算は一瞬)。
帰結:
- コンパイラ(規模不問・10 万行でよい)は バグがあってよい。 変な出力を出しても、付随する証明書が成立しないので検査器が弾く。
- 証明しなければならないのは 検査器の健全性ただ一つ: 「検査器が受理したなら、成果物はその性質を持つ」。 この定理はコンパイラの中身に一切言及しない ―― だから 10 万行は 晴れて 信頼不要(untrusted) になる。
これが「証明のためにコンパイラを完璧に作る」という発想を構造的に不要にする。
| 語 | 意味 |
|---|---|
| ALS (Almide Language Specification) | 言語の 規範意味論。「各プログラムが何を意味するか」を形式的に定義した唯一の正典。コンパイラも参照実行器も、これに従う/これを実装する側であって、意味を勝手に定めない。 |
| 証明書 / witness | コンパイラが成果物に添える、機械が検算できる根拠。「メモリは全部後始末した」「変な所に書いていない」等を、検査器が照合できる形で書いたもの。 |
| 証明書形式 | witness を書くための、わざと極限まで単純にした言語。単純なほど意味が曖昧にならず、独立した読み取り実装を誰でも書ける。 |
| 検査器 (checker) | 証明書を読み、成果物と照らして「成立」を確認する小さなプログラム(数百〜千行)。ここだけが信頼対象。 |
| refine(リファインメント) | 「忠実に実装している」の形式版。「実物 a は モデル M を refine する」= a の観測可能な振る舞いは M が許すものだけ、の意味。 |
| 信頼基底 (TB, Trusted Base) | その主張を受け入れるとき、疑わずに信じると決めたものの集合。小さいほど良い。 |
| Coq / Rocq | 証明を書き、極小の中核(カーネル)が穴の有無を厳密に再検査する道具。どれだけ巨大な自動化を使っても、最後はカーネルだけが信頼対象になる(=信頼を小さく絞る仕組み)。 |
| CompCert | 正しさが数学的に証明された C コンパイラ。安全臨界分野で実際に資格化利用された前例を持つ唯一格。 |
| CertiCoq | Coq の関数(Gallina)を CompCert の入力まで 検証済みにコンパイルする道具。これにより「検査器を Coq の論理から一歩も出さずに機械語まで」届けられる。 |
| DO-178C / DO-330 | 航空ソフトの認証ルール(178C)と、その中でツールを公式に認めるための規定(330)。 |
| Thompson 穴 | 「コンパイラ自体に裏切りが仕込まれていたら、ソースを読んでも見えない」という古典的問題。検査器を検証済みコンパイラで作ることで閉じる。 |
信頼基底はただ一つ、Coq カーネル。他のすべては、それに対して証明済みか、 さもなくば信頼不要。この二択しかない。
┌────────────── 規範意味論 ALS(Coq 内の形式意味論)──────────────┐
│ すべてのプログラムの意味は、ここだけが定める │
└───────────────────────────┬───────────────────────────────────┘
refine │ refine
┌──────────────┘ │ └──────────────┐
非信頼コンパイラ 性質 P {メモリ安全・stack 均衡・ 参照実行器
(規模不問・バグ可) name 全域・capability 上界・型 (ALS の実行像)
│ concretize・終端挙動} = ALS に対して定義
▼
( wasm バイト列 a , 証明書束 c ) ── 継ぎ目は「証明書形式」ただ一つ
│ (極限まで単純・意味論を完全文書化)
├──► 性質検査器 K K(c, a) = 受理 ⟹ a は P を全部満たす
└──► 翻訳検査器 V V(a, ALS(s)) = 受理 ⟹ a の挙動は ALS(s) を refine
│
K・V は Gallina 関数として書かれ、Coq で健全性を証明され、
CertiCoq + CompCert で機械語化され、独立 2 実装(うち 1 つは機械語まで検証)が
一致して初めて通り、DO-330 で資格化される唯一の対象。
コンパイルと証明書発行は同一の行為。 各解析パスの出力が、そのまま witness。 コンパイラは証明書形式だけを話し、検査器は証明書形式だけを聞く。互いの内部を 知らない ―― これがアーキテクチャの唯一の継ぎ目。
規範は ALS 一点。 意味を定めるのは ALS だけ。コンパイラも参照実行器も 二つのバックエンドも、すべて「ALS の refinement」。だから二ターゲットの バイト一致は事後確認ではなく、同じ系から自然に出る帰結。
検査器は二つある、と最初から認める。
- 性質検査器 K ―― 成果物 a が性質 P を満たすことを証明書で確認。
- 翻訳検査器 V ―― 出たバイト列 a が ALS(s) を refine することを毎ビルド確認。 審査者の必殺質問「証明したのはモデルで、実際に飛ぶ実物では?」への答え。
両者とも小さく、両者とも Coq 証明済み、両者とも機械語まで検証、両者とも 資格化対象。共通の「成果物意味論ライブラリ」を共有し、資格化の重複を減らす。
WASM が正典の信頼成果物。 rustc は「コンパイラを建てた 1 回」だけ入り、 成果物の経路には一切入らない(= 信頼すべき土台が最小)。 可読 Rust → Ferrocene は第二の資格化経路として、同じく ALS の refinement として並ぶ。
多様性と監査。 検査器は異チーム・異言語の独立 2 実装が一致して初めて通る。
全定理の使用公理は固定の標準集合に収まることをゲートで毎回確認し(Coq の
Print Assumptions ⊆ 標準)、信頼を勝手に広げるワザ(証明内でコンパイラ実行を
信用する類)はゼロ。
| 区分 | 中身 | 正しさは |
|---|---|---|
| 信頼不要(untrusted) | parser・checker・全 codegen パス・optimizer・wasm emitter(= ほぼ全コード量) | 不要。バグってよい。検査器が出力を毎回検証する |
| 信頼(trusted, =資格化対象) | 性質検査器 K・翻訳検査器 V・証明書形式の意味論 | Coq で健全性証明 + 機械語まで検証 + 独立 2 実装一致 |
| 信頼基底(TB, 疑わない) | Coq カーネル / CompCert・CertiCoq の TB / ハードウェア / ALS が意図どおりか | 証明では消せない底(§8) |
急所: 航空審査(DO-330)が公式に検査するのは、性質検査器 K と翻訳検査器 V だけ。10 万行のコンパイラは審査リストに載らない。「公式に審査される対象」を コンパイラ全体から数百行の検査器に絞りきる ―― これがこの設計の最大の効用。 CompCert が「コンパイラを一度証明した」のに対し、Almide は 「ビルドごとに、資格化済みの小検査器が証明書を照合する」。
各成果物の証明書束は、検査済みの性質を主張へ畳む。各主張は 信頼基底が公理集合に収まり、反証手続きが公開されている(詳細は receipt-logic):
- C-SAFE ―― capability 有界・未定義動作なし(成果物単独で検証可。最強)
- C-REPRO ―― 同一ソースは任意ホストで byte 同一
- C-FAITHFUL ―― 観測挙動が ALS を refine する
- C-PROVEN ―― カーネル検査済みの全称性質(RC 均衡・stack 均衡等)
第三者は自分のマシンで make verify を走らせ、全主張を手元で再導出する。
CI は信頼基底に入っていない ―― CI は礼儀としての先行実行にすぎない。
「絶対的な意味論を完全に被覆」は CompCert 級に発散するので狙わない。代わりに:
完全性(U) = 使用目的 U に必要な主張集合 C(U) が列挙され、全主張が検査器を 持ち、全 TB が公理集合に収まる状態。
- U₁ = サンドボックス内エージェント実行: C(U₁) = { capability 上界・ エラー時終端挙動・決定性・再現性 }。ほぼ C-SAFE/C-REPRO で構成。
- U₂ = 無監督の本番運用: C(U₁) + C-FAITHFUL の被覆。
受領書は どの用途を証明したか を明記する。「Almide は完全」とは言わず、 「U₁ に対して完全、U₂ に対して n/n」と数えられる形にする。
どんな検証体制でも残る、証明では消せない信頼基底:
- Coq カーネル(小さく、世界中で精査済み。信じるのが標準)
- CompCert / CertiCoq 自身の TB
- ハードウェア / OS
- ALS が我々の意図どおりか ―― これだけは証明不能で、参照実行器・ 日次 MSR 測定・実使用によって経験的にしか確かめられない
この 4 つを既知制限文書に明記することが、残り全部を「証明済み」と呼ぶ資格に なる。「全部完璧です」より「ここまで証明済み、ここからは信じてください」と線を 引く方が、審査では強い。
- コンパイラ全体の証明(CompCert 級フルプルーフ)。代わりに検査器健全性 + per-build 証明書に畳む。
- 絶対意味論の完全被覆。完全性は使用目的に相対化する(§7)。
- 新規論理の自作。論理は精査の蓄積そのものが要件 ―― 借りる(Coq)。 独自にできるのは証明書形式・検査器・検査器の独立実装であって、論理ではない。
- 常用二論理。証明対象が検査器健全性に潰れているため、TB は Coq 単一に 絞る(探索的証明を別系で試作するのは可、常用は TB 増)。
- 公理の隠蔽。TB は隠さず台帳に書く(§8)。
- 検査器の肥大。検査は生成より易しくあり続けること ―― 育ちすぎた検査器は それ自体が次の信頼問題になる。単純さと多様性で守る。
- 捨てる: コンパイラの実装コード(フェーズ構造に証明を後付けした v0 の本体)。
- 運ぶ: 知識。spec corpus・oracle registry・12 リリースで見つけた 既知エッジケース(#484 級)は、v1 コンパイラの 差分テスト / ファズの オラクルとして初日から再利用する。コンパイラは作り直しても、 知識は作り直さない。
信頼境界を軸に組まれ、証明書を吐く非信頼コンパイラと、**ALS を正典に据えた 二つの極小検査器(性質・翻訳)**が、Coq 単一 TB で健全性証明され機械語まで 検証され、毎ビルド wasm へ翻訳検証され、第三者が手元で全主張を再導出できる ―― 信じる対象が「数百行の検査器一個」に絞りきられ、10 万行は晴れて信頼不要に なった状態。これが v1 の着地形。