仕様への適合

ステータス：active
対象読者：コントリビューター、レビュアー
権威：エンジニアリング適合性ガイド。QED 形式仕様と現在のコード／テストに従属する
範囲：コード／テストの対応付け、実装の整合、コントリビューターの義務、ドキュメント例の規則
最終レビュー: 2026-10-08

本書は、現在の MoonBit エンジニアリングラインが QED 形式仕様とどのように整合しているか、また周辺のエンジニアリングが現在のコアに適合するために何をすべきかを記録する。

本書は新たな規範の層ではない。その役割は、「論文の要件」「現在のコード」「現在のテスト」「周辺エンジニアリングの義務」を同じ表にまとめることである。

規範の根拠

QED における現在の権威関係は次のとおり。

QED 形式仕様が唯一の規範的根拠である。
doc/attachments/qed_formal_spec.typ が仕様のソースファイルである。
現在のコードとテストが、実際に出荷されている現状を決定する。
ドキュメントガバナンスが、ドキュメントの階層と引用規則を定める。
ユーザーマニュアルは、現在のリポジトリにおける実装契約を記述する。
本書は、エンジニアリング上の適合性、コードとテストの対応、およびコントリビュータ向けチェックリストを記述する。

Part II 適合性の Lean アンカーは、主に次の場所にある。

formal_verification/QEDFV/Engineering/Conformance.lean
formal_verification/QEDFV/Spec/Items.lean
formal_verification/QEDFV/Audit/AppendixG.lean
formal_verification/QEDFV/Audit/PartI.lean

実装済みと未実装

実装済みでテスト済み

現在、安定したコードと回帰テストに裏付けられている部分は次のとおり。

型付き項/型のコア
不透明な定理オブジェクトと検査済みの基本規則
スコープ付きシグネチャスタックと定義履歴の規律
DefOK / TypeDefOK / SpecOK ゲート
定数の同一性、スキーマインスタンス、定義上の整合性、型言語の許容性に関する定理の許容性
定数の同一性を凍結した、解決済みのエラボレーション境界
parser の正規化と raw-offset 契約
タクティクへの直接依存を持たない、parser 所有のゴールローワリング境界
表層の結合子に対する、基底に裏付けられたローワリング契約
正準な定義定理に裏付けられた結合子の認識
監査証明書と、実行可能な保守的リプレイフック
logic 層における定義定理 / 展開 / リプレイのヘルパー
カーネルの Thm へリプレイされる、サポート対象の命題定理スクリプト経路

実装済みだが意図的に部分的なもの

次の部分は存在するが、カバー範囲はまだ限定されている。

tactics における Goal / ProofState / ステップ実行と ps_qed の成功経路
prover における定理スクリプトドライバ
定理名に基づくリプレイは、現状では安定した命題の小さなカタログのみをカバーする
parser は現在、定理ヘッダの束縛子、逐次的な by 本体、最小限の構造化分岐ブロック構文をサポートしている。定理ヘッダには 0 個以上の (name : type) 束縛子を付けられる。本体は 1 行の theorem ... := by step; step; ... としても、theorem ... := by に続けて改行区切りのステップ列を置くブロックとしても書ける。split / left / right は引き続き最小限の分岐ブロック構文を伴うことができ、parser は束縛子/ゴール/ステップの生のスパンを保持する。分岐本体の実際のスケジューリングと責任帰属は prover が扱う
定理スクリプトは現在、hole / hole <name> による未完了の証明ステップもサポートする。定理ヘッダの束縛子は、ゴールのローワリング、証明状態のローカル、cmd の診断へ確実に入る、出荷済みの量化子向けサーフェスとなった。生の forall / ∀ 定理ゴールも、ゴール限定の糖衣構文として出荷済みのローワリング経路に入るが、項レベルの構文ではない
parser 側の parse_let / parse_def_function は、スクリプト外のユーティリティサーフェスとして形式化されている

これらの層は、「任意のユーザー証明から信頼できる定理を生成できる」完全なフロントエンドではない。

未実装

次は現在実装されておらず、欠けている機能として明示的に扱うべきである。

より豊富な証明ブロック
昇格された書き換え/簡約タクティク / コマンドサーフェス
辞書渡し
型クラスフロントエンド
インスタンス環境 / インスタンス探索
制約解決
メタ変数 / hole
局所的な型推論
高階単一化
任意のスクリプト / 任意のタクティクの組み合わせに対する完全な定理再構成

コードとテストの対応

領域	現在の実装	回帰テストのカバー範囲
型付きコア + 境界変換	`src/kernel/types.mbt`, `src/kernel/terms.mbt`	`src/kernel/kernel_terms_test.mbt`, `src/kernel/kernel_types_test.mbt`
スコープ付き状態 + 拡張ゲート	`src/kernel/sig.mbt`	`src/kernel/kernel_sig_test.mbt`, `src/kernel/kernel_audit_test.mbt`
基本規則 + 許容性	`src/kernel/thm.mbt`	`src/kernel/kernel_thm_test.mbt`, `src/kernel/kernel_thm_wbtest.mbt`, `src/kernel/kernel_audit_test.mbt`
解決済みエラボレーション境界	`src/elab/resolved.mbt`	`src/elab/elab_test.mbt`
parser ブリッジ + 正規化/raw-offset 契約	`src/parser/parser.mbt`	`src/parser/parser_test.mbt`
parser からタクティクへの明示的なゴールブリッジ	`src/parser/parser.mbt`, `src/prover/prover.mbt`	`src/parser/parser_test.mbt`, `src/prover/prover_positive_corpus_test.mbt`
表層結合子の基底展開	`src/logic/prop_prelude.mbt`, `src/logic/prop_foundation.mbt`, `src/logic/prop_tools.mbt`	`src/logic/prop_prelude_test.mbt`, `src/logic/prop_tools_test.mbt`, `src/parser/parser_test.mbt`
命題定理のリプレイ/カタログの種	`src/logic/prop_bool_theorems.mbt`, `src/logic/prop_refs.mbt`, `src/logic/prop_replay.mbt`	`src/logic/prop_bool_theorems_test.mbt`, `src/logic/prop_refs_test.mbt`, `src/logic/prop_replay_test.mbt`
運用上の証明スクリプト + M1 サブセットのリプレイ	`src/tactics/proof_state.mbt`, `src/prover/prover.mbt`	`src/tactics/proof_state_test.mbt`, `src/tactics/tactics_test.mbt`, `src/prover/prover_test.mbt`, `src/prover/prover_positive_corpus_test.mbt`, `src/prover/prover_negative_corpus_test.mbt`
ファイル優先の `cmd` 統合サーフェス	`src/cmd/cmd.mbt`	`src/cmd/cmd_wbtest.mbt`
量化子向け束縛子 / 生の `forall` のコーパス + CLI 契約	`src/prover/corpus.mbt`, `src/prover/prover_mapping_matrix_test.mbt`, `src/cmd/cmd_corpus_wbtest.mbt`	`src/cmd/cmd_corpus_wbtest.mbt`, `src/cmd/cmd_wbtest.mbt`, `src/prover/prover_mapping_matrix_test.mbt`
形式的な Part I / Part II 適合性パック	`formal_verification/QEDFV/Audit/PartI.lean`, `formal_verification/QEDFV/Engineering/Conformance.lean`	`lake build`

特に注意すべき回帰ポイント:

src/kernel/kernel_audit_test.mbt は、def ヘッドの単調性、typedef ウィットネスの妥当性、const-id のずれ、型付き beta/trans のガード、保守的リプレイといった高リスクのシナリオをすでにカバーしている。
src/parser/parser_test.mbt は、正規化/raw-offset 契約と、bool でない結合子のフェイルクローズによる拒否をすでにカバーしている。
src/parser/parser_test.mbt は現在、定理ヘッダの束縛子、構造化分岐ブロックの解析、raw スパンの回帰もカバーしている。
src/parser/parser_test.mbt と src/prover/prover_positive_corpus_test.mbt は合わせて、parser 所有のゴールローワリングと、tactics.Goal への上位層による明示的ブリッジの契約を現在固定している。
src/prover/prover_test.mbt は、スクリプトのスケジューリング、分岐パスの帰属、構造化分岐ブロックにおけるステップ責任の規約を現在固定している。
src/prover/prover_test.mbt は、サポート対象の M1 サブセットに対する Ok((KernelState, Thm)) の正例と、直接クローズ / 含意に裏付けられたいくつかの定理名経路をカバーしている。
src/prover/prover_positive_corpus_test.mbt / src/prover/prover_negative_corpus_test.mbt は、出荷済みサブセットの正準スクリプトコーパスを保持しており、機能のカバー範囲と正直な失敗の規約を固定するために使われる。
src/prover/prover_test.mbt、src/prover/prover_mapping_matrix_test.mbt、src/cmd/cmd_corpus_wbtest.mbt は、未完了の証明 / hole 報告の構造化契約と、正準な未完了コーパスのアンカーも現在カバーしている。
src/prover/prover_mapping_matrix_test.mbt と src/cmd/cmd_corpus_wbtest.mbt は、ネストした分岐の未完了経路と、安定した空マーカーのレンダリングも現在カバーしている。
src/cmd/cmd_corpus_wbtest.mbt と src/cmd/cmd_wbtest.mbt は、出荷済みの量化子向け束縛子 / 生の forall スクリプトに対する成功 / 失敗 / 未完了の CLI 契約を、ゴール、ローカル、分岐パス、ステップ責任を含めて現在固定している。
src/prover/prover_mapping_matrix_test.mbt は、正例 / 負例 / 未完了の正準ケース id、量化子束縛子 / 生の forall のケース id、機能タグ、ユーザーマニュアルの公開サンプルのアンカーを、一組の回帰制約に現在束ねている。
src/cmd/cmd_wbtest.mbt は、成功時のレンダリング、parse/io/usage の失敗、タクティク失敗コンテキストのレンダリング、分岐パスのレンダリング、ファイル優先の argv ワークフローを現在カバーしている。

ドキュメントの例のソース契約

ドキュメントが計画中の機能を出荷済みであるかのように提示することを防ぐため、ドキュメントの例は現在、次のソース制約に従わなければならない。

README.md は現在出荷されているサブセットの要約のみを公開し、独自に新たな例の意味論を創作しない。
ユーザーマニュアルの実行可能な定理スクリプトの例は、既存の回帰テストのカバー範囲に由来していなければならない。
定理を生成する正例スクリプトは、現在 src/prover/prover_test.mbt と src/prover/prover_positive_corpus_test.mbt を主なアンカーとしている。
出荷済みサブセットの負例 / 正直な失敗の例は、現在 src/prover/prover_negative_corpus_test.mbt を主なアンカーとしている。
正準な未完了証明の例は、現在 src/prover/prover_test.mbt、src/prover/prover_mapping_matrix_test.mbt、src/cmd/cmd_corpus_wbtest.mbt を主なアンカーとしている。ルートレベルの未完了と、ネストした分岐の未完了の両方のサンプルを同期させておかなければならない。
量化子向け束縛子 / 生の forall の例も現在、src/prover/corpus.mbt、src/prover/prover_mapping_matrix_test.mbt、src/cmd/cmd_corpus_wbtest.mbt を主なアンカーとしており、公開ドキュメントはこれらの正準ケース id のみを引用できる。
公開ドキュメントにおけるケース id から例のアンカーへの対応は、現在 src/prover/prover_mapping_matrix_test.mbt を主なアンカーとしている。
タクティクレベルの例、ローカルが名前に優先する衝突、誤ったモードによる正直な失敗は、現在 src/tactics/proof_state_test.mbt を主なアンカーとしている。
パッケージページ(api/、design/、tutorial/)に引用される定理スクリプトは上記のアンカーのスクリプトを再利用しており、新たなスクリプトの意味論を導入しない。
パッケージページの MoonBit API の例は、現在のコードの公開関数を呼び出し、結果を assert_eq、assert_true、または inspect スナップショットで記録する完全なプログラムである。そのようなブロックはすべて、ページを変更する前に現在のコードに対してコンパイルされ実行される。実行を意図しないブロックは moonbit nocheck でフェンスされる。
ドキュメントが公開サンプルを追加、変更、削除する場合は、対応する回帰テストも同時に追加、変更、削除しなければならない。

Part II の適合性義務

Lean は現在、周辺エンジニアリングの Part II の義務をエンジニアリング上の義務として明示的に述べている。中核となる項目は次のとおり。

ruleFidelity
boundaryFidelity
scopeFidelity
replayTraceFidelity
gateFidelity
certificateNonAuthority
conservativeReplayFidelity

コントリビュータ向けには、より実行しやすいチェックリストとして次の規則がある。

コントリビュータチェックリスト

logic が提供してよいのは、検査済みラッパー、定義/展開ヘルパー、リプレイヘルパー、非権威的な定理参照の整理のみであり、カーネルを迂回して新たな規則を作ってはならない。
parser は local > const と正規化 + raw-offset 契約を保持し、logic と同じ結合子契約を共有しなければならない。
elab は解決済みの同一性を凍結しなければならず、後の型付けで const-id やスキーマのずれに遭遇した場合は、フェイルクローズしなければならない。
tactics が ps_qed を通じて定理を渡してよいのは、logic を経由したリプレイがシーケントと整合する Thm を構築した場合のみであり、そうでなければフェイルクローズしなければならない。
ps_qed における最終受理は、現在は厳密に正規化されたシーケントの等価性を用いなければならず、形状を考慮した互換性のみに基づいて結果を受理していた古い境界を残してはならない。
prover が Ok と Thm を返すのはリプレイが成功した場合のみであり、それ以外は正直なエラーを返し続ける。
cmd は新たな非権威的な統合層にしかなってはならず、第二の証明カーネルになってはならない。
拡張証明書は監査成果物にしかなってはならず、定理受理の代替として扱ってはならない。

このチェックリストの目的は、実行可能なフロントエンドを、論文が忠実な実現と呼ぶものへ段階的に圧縮していくことであり、周辺エンジニアリングに第二の論理体系を加えることではない。

周辺の整合

現在のワークスペースのエンジニアリング主線は、意図的な統合である。

parser は、「状態内に同名のプレリュード定数が存在することに依存する」方式から、「基底に裏付けられたビルダー + 解決/ローワリング契約」へ移行した。
Logic は、「表層シンボル名の登録」から、「定義済み定数 + 定義定理 + 展開/リプレイのヘルパー + 小さな定理カタログ + 共有の定理インベントリ」へ進んだ。
Tactics/prover は、純粋な運用上のプロトタイプから、「サポート対象のサブセットがカーネルの Thm へリプレイされ、サポート表と正直な失敗が正準コーパスで固定される」段階へ移行した。

周辺エンジニアリングが現在のコアに適合し続けるために、引き続き次のことを行うべきである。

共有の定理インベントリと正準コーパスの上に、リプレイビルダーを拡張する。
新たに出荷する機能を正準コーパス / マッピング表 / マニュアルのアンカーへ書き戻し、ドキュメントが実装に遅れないようにする。
ゴール / hole / 未完了の証明の診断を正式なフロントエンド契約とし、それらが証明オブジェクトではないことを引き続き明示する。
定理ヘッダの束縛子による出荷済みの量化子向け経路、および生の forall 定理ゴールの糖衣構文について、parser/ローワリング/リプレイの境界を明示し続ける。
cmd が、エラー文字列を独自に解釈せず、prover の構造化された失敗契約を再利用し続けるようにする。
現在のファイル優先ワークフローの上で、フロントエンドの表現力を拡張し続ける。

これらの作業は既存のツールを再利用すべきである。

logic_prop_def_*
logic_prop_unfold_*
logic_apply_fun_eq*
logic_beta_normalize_eq
logic_eq_mp_bool
logic_eq_sym
logic_prop_replay_*

tactic/prover の内部でしか成り立たず、カーネル経路へリプレイできない、別個のアドホックな証明意味論を作ってはならない。

残る未出荷のサーフェス

まだ出荷されていない機能には次のものがある。

定理カタログはまだ小さく、より自然なスクリプトを大量にサポートするには足りない。ただし、現在の出荷済みサブセットのインベントリ、モード境界、コーパスはすでに固定されている。
正準コーパスは、H5 統合ゲートを完了させるために、強化用の回帰テストをまだ補う必要がある。
定理スクリプトの本体は最小限の M4b 構造化分岐ブロックをすでにサポートしているが、より豊富な証明ブロックはまだ実装されていない。
hole / 未完了の証明は出荷済みの定理スクリプトサーフェスに入ったが、hole の補完 / メタ変数の権限はまだ実装されていない。
定理ヘッダの束縛子による量化子向けサーフェスは出荷済みである。生の forall / ∀ 定理ゴールのフロントエンドも、ゴール限定の糖衣構文としてサポートされている。
parser 側のユーティリティサーフェスはスクリプト外の API に統合された。今後は、ドキュメントとテストを同期させておくだけでよい。
Lean ラインは現在、MoonBit ソースの直接的な機械化証明ではなく、論文/適合性パックである。

したがって、現状のより正確な評価は次のとおり。

Part I のコアと Part II の主要な適合性規約は整っている。
サポート対象のサブセットに対して定理を生成するフロントエンドはすでに存在する。
しかし、より完全で忠実な実現はなお統合が進められている途中である。

検証ゲート

現在推奨される論文整合 / エンジニアリング適合性のゲートは次のとおり。

moon build
moon test
cd formal_verification
lake build

マージまたはリリースの凍結を準備する際には、次も実行する。

moon info
moon fmt
moon test
cd formal_verification
lake build

ローカルチェックの結果:

2026-10-08、MoonBit moonc v0.10.14: moon check --target all は警告なしで、moon test は wasm、wasm-gc、js、native の各ターゲットで通過した(357 テスト)
2026-04-05: lake build は通過した。formal_verification/ はそれ以降変更されていない

変更が信頼境界、スコープ、ゲート、結合子契約、証明スクリプト、またはドキュメント規約に及ぶ場合は、次も確認する。