Luna Flow
日本語

ワークスペース監査（2026-04-18）

  • ステータス：point-in-time audit（時点監査）
  • 対象読者：メンテナー、コントリビューター
  • 権威：段階的な監査。QED 形式仕様、現在のコード／テスト、実装ドキュメントに従属する
  • 範囲：監査対象のベースラインで依然として重要なリスク、不足点、フォローアップ項目
  • 最終レビュー：2026-04-18

日付: 2026-04-18

本レポートは、リポジトリの真実の源の順序に照らして現在のワークスペースを監査する。

  1. QED 形式仕様
  2. 現在のコードと回帰テスト
  3. 実装向けドキュメント（ユーザーマニュアル、仕様への適合）
  4. トップレベルの要約ドキュメント(README.md、application.typ)

本監査で用いた検証ベースライン:

  • moon test -> 通過(276/276)
  • formal_verification/lake build -> 通過

これらのゲートが緑であることは、現在のベースラインでワークスペースが内部的に整合していることを示す。計画されたすべての製品機能がすでに出荷済みであることを、それだけで意味するわけではない。

前回の監査以降に解決されたもの

以前に報告されたリスクのうち、次のものは現在の指摘事項ではなくなった。

  • 型言語の許容性が、信頼される定理 / 文の境界で強制されるようになった。
  • 結合子の認識が、生のヘッド名の受理ではなく、定義定理に裏付けられるようになった。
  • bool でない表層結合子は、ユーザーが到達可能な経路でクラッシュする代わりに、構造化エラーでフェイルクローズするようになった。
  • 定理名インベントリ、exact / apply のモード境界、正準な正例 / 負例スクリプトコーパスが、いずれも明示され、回帰テストでカバーされるようになった。
  • ファイル優先の cmd サーフェスが存在するようになり、回帰テストでカバーされ、文字列のみの生の報告に代えて構造化されたタクティク失敗コンテキストを用いる。
  • 現在の M4 スライスが出荷済み経路に統合された。定理ヘッダの束縛子、逐次的なブロック本体の定理スクリプト解析、生の束縛子/ゴール/ステップのスパン、構造化されたフロントエンド診断のすべてが回帰テストでカバーされている。
  • ProofState の最終的な定理検証が厳密に正規化されたシーケントの一致へ厳格化され、従来の広い一致の挙動を拒否する回帰テストが追加された。
  • 選言のラップのリプレイが、連言のマージと同じ、ゴール全体に対する明示的な事後条件の規律を強制するようになった。
  • ローカルの exact ウィットネスは、有効な仮定のエイリアスのみに凍結され、ローカルのシャドーイングが同名の定理エントリへ素通りすることはなくなった。
  • 正準な prover コーパスとマッピング表のカバー範囲が、強化されたリプレイ/最終定理の契約と整合するようになり、H5 は古い広いコーパス契約に依存しなくなった。
  • 最小限の M4b が主要な定理スクリプト経路で出荷された。split / left / right の構造化分岐ブロックが解析・リプレイされ、parser/prover/cmd の回帰テストでカバーされ、安定した分岐パスで診断される。

したがって本監査は、現在もなお重大な問題とギャップのみに焦点を当てる。

指摘事項

[P2] Lean ラインは論文/適合性パックにとどまり、MoonBit 実装の直接的な証明ではない

なぜ重要か

これは MoonBit カーネルのバグではないが、誠実なコミュニケーションのために重要な状態の境界である。lake build が証明するのは論文のモデルと抽象的な適合性の義務である。現在の MoonBit ソースツリーを Lean の Realization へ機械的に結びつけるものではない。

根拠

  • formal_verification/QEDFV/Engineering/Conformance.lean は、抽象的な実現と義務について推論している。
  • トレーサビリティと規則対応のファイルは論文/適合性の成果物であり、MoonBit のシンボルへの生成されたリンクではない。
  • リポジトリのドキュメントはすでに、Lean ラインを実装の直接検証ではなく論文優先のものとして扱っている。

影響

  • 公開する保証の表現は正確でなければならない。
  • lake build は「仕様/適合性パックが閉じている」と読むべきであり、「MoonBit プログラムが Lean と機械検査により等価である」と読んではならない。

必要なフォローアップ

  • この境界についてドキュメントを正確に保つ。
  • 具体的な MoonBit と Lean の結びつけの道筋が新たなマイルストーンとして導入された場合にのみ、より強い主張を後から追加する。

起票済みタスク

  • A6

依然として重要なテスト上のギャップ

現在のテストスイートは強力だが、次のギャップは今後の段階で依然として重要である。

  1. 現在の最小限の分岐ブロックのスライスを超える、より豊富な証明ブロックの拡張。
  2. 正準な未完了ケースを超える、より豊富な hole / 未完了の証明の報告。
  3. 量化子向けフロントエンドと、その信頼に関わるローワリング契約。
  4. 将来の CLI 機能はいずれも、第二のスクリプト表を分岐させず、現在の正例 / 負例コーパスを再利用し続けなければならない。

総合評価

  • カーネルと、現在の定理を生成する命題サブセットは、前回の監査スナップショットが記述していたよりも大幅に強い状態にある。
  • 今回のレビューでは、現在の出荷済み経路における、検査済みカーネルの健全性の直接的な破れは見つからなかった。
  • 次の最も重要な作業は以下のとおり。
    1. 新たな構造化分岐ブロックのサーフェスを、同じ検査済みのローワリング / リプレイ境界に載せ続ける。
    2. ロードマップを、よりリッチなユーザー向け証明体験(スクリプト、ゴール、証明ブロック、量化子フロントエンド)へと進める。
    3. フロントエンドの拡大に合わせて、コーパス + ドキュメント + 適合性の保守を継続する。
  • 書き換え/簡約のラインは研究段階にとどまる。
  • Lean ラインは緑のままで価値があるが、より強い実装との結びつけが後から明示的に追加されない限り、論文/適合性パックとして記述され続けるべきである。