形式手法特論：コンパイラの「正しさ」は証明できるか？ by チェシャ猫

テーマ

定理証明：複雑なロジックと事実上無限の入力を持つソフトウェアに対して、テストケースの網羅性に依存せず、論理的に挙動を保証する手法およびその実例

想定する参加者層（前提知識）

• 計算機科学に興味があるが敷居の高さを感じている方
• 設計と一体化した品質保証に興味がある方
• 形式手法や定理証明に関する前提知識は仮定しません
• 特定の CPU 命令セットに関する前提知識は仮定しません
• 特定のコンパイラバックエンドに関する前提知識は仮定しません
• 型システムに関する理論的な前提知識は仮定しませんが、何らかの静的型付き言語によるプログラミング経験は前提とします
• 基本情報技術者試験に出題されるような計算機アーキテクチャの初歩、例えば「メモリとは何か」のような知識は前提とします

トーク概要

本セッションでは、定理証明支援系 Lean を用いたコンパイラの実装技法を解説します。ただしこれは本質的にはコンパイラのトークではありません。頭の痛い複雑なロジックや、うんざりするほど多様な入力データと戦っている、すべてのソフトウェアエンジニアに贈る新しい世界への招待状です。

今日、プログラムを書く際に一緒に単体テストを書くことは、一種のマナーとして広く普及しています。しかし、かつて Dijkstra はこう言いました。「テストではバグの存在を示すことはできても、不在を示すことはできない」つまりテストが成功していたとしても、それはたまたまテストケースが不足していてバグを踏まなかった可能性が否定できない、というのです。一方で、仮に全通りのテストケースを生成してバグの不在を示そうとした場合、組み合わせの爆発により膨大な数のテストが必要になってしまいます。例えば「長さ 3 以下の char の配列を受け取る関数」をテストするだけでも入力パターンは 16,843,009 通り。通常の任意長の配列を受け取る関数ならば文字通り「無限個のテストケース」が必要です。

本セッションで紹介する定理証明は、文字通り、この「無限個のテストケース」を扱うための手法であるといえるでしょう。テストしたい関数の性質を型レベルの制約として表現することで、単体テストのような実行時ではなく静的な型検査時に、かつ「任意の char 配列」のような事実上無限個のテストケースに対して関数の性質を保証できます。

いくつかある定理証明支援系の中でも、Lean は単に証明を記述するだけでなく、実際に動くプログラミング言語であるという面で近年注目を浴びています。一例として、Amazon Web Service では、認可ポリシー記述言語である Cedar の開発と最適化のために、この Lean を採用しています。認可ポリシーエンジンの実装は「ロジックが複雑」「あらゆるパターンに対応する必要がある」「最終結果がぱっと見で分からない」「ミスがあると被害が甚大」という点で、まさに定理証明向きの事例と言えます。また、国内においてもちょうど日本語書籍『ゼロから始める Lean 言語入門』が出版されたばかりで、今 Lean が盛り上がりつつあるのは間違いないでしょう。

本セッションでは、Lean を利用して、自作言語をコンパイルしてシンプルな CPU 上で動かすための「証明付きコンパイラ」を実装します。コンパイラもまた、複雑なロジックと多様な入力が求められるソフトウェアの典型です。ところで、引数と戻り値を持つ個別の関数のテストならともかく、ここで言う「コンパイラの正しさ」とは何でしょう？ コンパイルしたプログラムの挙動が正しいこと？ ではその「正しい」とはどういう状況か、定義できるでしょうか？

この問いへの答えとして、今回の解説では、コンパイラの性質を「ソース言語の意味論」と「ターゲット言語の意味論」の間をつなぐものとして定式化し、実装したコンパイラが意味論を保存することを証明します。また、コンパイラの挙動を保証するための理論的な解説に加え、実際に動くプログラムを書けるという Lean の特性を活かして、「インタプリタ」「VM」そしてその間をつなぐ「コンパイラ」をそれぞれ実装し、簡単なプログラムをコンパイルして動かす様子もお見せします。

受講にあたって必要なものは、プログラミング経験者であれば普通に知っている程度の知識と、ほんの少しの知的好奇心だけです。定理証明や特定の CPU 命令セットに関する前提知識は要求しませんし、それどころかコンパイラとしては、最適化も行わない、本当に素朴な実装しかしません。むしろ「コンパイラの正しさとは何か？」を題材として、複雑なプログラムの挙動も数学的にきちんと定式化できるのだ、そしてそのための理論や考え方は、他ならぬあなた自身とも無関係の世界ではないのだ、という感動を味わって頂ければと思います。