コンパイラの形式的検証ってどうやるの？

Coqによる形式検証付きのC言語コンパイラがある。
https://en.wikipedia.org/wiki/CompCert
これはどういうことなのだろう。

🤨🤔😑😨😱

引き算のみができる言語のコンパイラを考える。

元の言語：

a - b

ターゲットの言語：

PUSH a
PUSH b
MINUS

🤨🤔😑😨😱

これらの言語に対して抽象構文木を定義する。この部分は証明ができない。

元の言語：

data Expr =
   Num Int
 | Minus Int Int

ターゲットの言語：

data Instr =
   PUSH Prelude.Int
 | MINUS

type Prog = List Instr

🤨🤔😑😨😱

各言語の操作的意味論を定義する評価関数を定義する。これらはそれぞれの言語の意味を定義するものなので証明の対象ではない。

元の言語：

eval :: Expr -> Int
eval e =
  case e of {
   Num n -> n;
   Minus e1 e2 -> sub e1 e2}

ターゲットの言語：

execute :: Prog -> Stack -> Stack
execute ps s =
  case ps of {
   ([]) -> s;
   (:) i p' ->
    case i of {
     PUSH n -> execute p' ((:) n s);
     MINUS ->
      case s of {
       ([]) -> s;
       (:) n1 l ->
        case l of {
         ([]) -> s;
         (:) n2 s' -> execute p' ((:) (sub n2 n1) s')}}}}

🤨🤔😑😨😱

コンパイラは以下のように定義する。

compile :: Expr -> Prog

🤨🤔😑😨😱

コンパイラの検証で証明すべき命題は以下である。

forall e:Expr, eval e = execute $ compile e

コンパイラ関数compileが各言語の意味を保存していることを証明することである。

🤨🤔😑😨😱

コンパイラの証明において、証明できるのは以下のSTEP2のみである。

文字列から抽象構文木を作成するパーサー
抽象構文木をターゲットの言語に変換するコンパイラ
ターゲットの言語の実行

🤨🤔😑😨😱

Coqによる実装

Eval.vで以下を保存。

Require Import ssreflect.
Require Import List.

Definition ret_nat (n:nat) : nat := n.

Inductive expr : Type :=
  | Num (n: nat)
  | Minus (n1 n2: nat).

Inductive instr := 
  | PUSH (n: nat)
  | MINUS.

Definition prog := list instr.
Definition stack := list nat.

Definition eval (e: expr) : nat :=
  match e with
  | Num n => n
  | Minus e1 e2 => e1 - e2
  end.

Fixpoint execute (ps:prog) (s:stack) : stack :=
  match ps with
  | nil => s
  | cons (PUSH n) p' => execute p' (n :: s)
  | cons MINUS p' =>
    match s with
    | n1 :: n2 :: s' => execute p' ((n2 - n1) :: s')
    | _ => s
    end
  end.

Definition compile (e:expr) : prog :=
  match e with
  | Num n => (PUSH n) :: nil
  | Minus e1 e2 => (PUSH e1) :: (PUSH e2) :: MINUS :: nil
  end.

Theorem compiler_correctness: forall e : expr,
  cons (eval e) nil = execute (compile e) nil.
Proof.
  elim => [n | n1 n2].
  by [].
  by [].
Qed.

Require Extraction.
Require Import ExtrHaskellNatInt.
Require Import ExtrHaskellBasic.
Extraction Language Haskell.
Extraction "Eval.hs" eval compile execute.

🤨🤔😑😨😱

Main.hsで以下を保存する

import Eval

main :: IO ()
main = do
  let e = Minus 22 11
  print $ [eval e]
  print $ execute (compile e) []

以下を実行する。

$ coqc Eval.v; ghc Main.hs; ./Main

🤨🤔😑😨😱

まとめ

コンパイラの証明は言語間で抽象構文木を変換を変換したときに両者の意味が保存していることである。

このスクラップは2025/01/18にクローズされました