天泣記

いつのまにか CertiCoq が公開されていたので、動かしてみた。 (CertiCoq というのは、証明された Gallina のコンパイラ。 Gallina は Coq の中に入っている依存型で ML っぽい言語)

<URL:https://github.com/PrincetonUniversity/certicoq>

コンパイルはだいたい README.md に書いてあるとおりでいけた。

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

opam switch -A 4.05.0 coq87
eval `opam config env`

opam install coq.8.7.1
opam pin add coq 8.7.1

opam install coq-template-coq coq-ext-lib coq-squiggle-eq.dev coq-paramcoq

make

make install

sh make_plugin.sh

make install

make_plugin.sh はちょっと変で、stat -f "%m" file というのコマンドは手元では動かない。 (mtime を調べているっぽいが... そういう stat コマンドがあるかどうかよくわからない -> NetBSD 1.6 発祥の stat にあるようだ。) 適当にいじってどうにかした。

次のステップは plugin/README.md に書いてあり、CertiCoq Compile ref. というコマンドが使えるようになるようだ。

試しに以下のようにしてみる。

From CertiCoq Require Import CertiCoq.
Definition nat3 := 3.
CertiCoq Compile nat3.

すると、Top.nat3.c というファイルが生成された。内容は以下のとおり。

struct thread_info;
struct thread_info {
  unsigned int *alloc;
  unsigned int *limit;
  struct heap *heap;
  unsigned int args[1024];
};

extern void body(struct thread_info *tinfo);

extern void garbage_collect(unsigned int *, struct thread_info *);

extern _Bool is_ptr(unsigned int);

unsigned int const body_info_0100111[2] = { 6, 0, };

void body(struct thread_info *tinfo)
{
  unsigned int x110;
  unsigned int x111;
  unsigned int kapf_0000111;
  unsigned int k_1000111;
  unsigned int *alloc;
  unsigned int *limit;
  unsigned int *args;
  alloc = (*tinfo).alloc;
  limit = (*tinfo).limit;
  args = (*tinfo).args;
  if (!(*body_info_0100111 <= limit - alloc)) {
    (garbage_collect)(body_info_0100111, tinfo);
    alloc = (*tinfo).alloc;
  }
  x110 = 1U;
  x111 = (unsigned int) (alloc + 1U);
  alloc = alloc + 2U;
  *((unsigned int *) x111 + -1) = 1024U;
  *((unsigned int *) x111 + 0) = x110;
  kapf_0000111 = (unsigned int) (alloc + 1U);
  alloc = alloc + 2U;
  *((unsigned int *) kapf_0000111 + -1) = 1024U;
  *((unsigned int *) kapf_0000111 + 0) = x111;
  k_1000111 = (unsigned int) (alloc + 1U);
  alloc = alloc + 2U;
  *((unsigned int *) k_1000111 + -1) = 1024U;
  *((unsigned int *) k_1000111 + 0) = kapf_0000111;
  *(args + 1U) = k_1000111;
  return;
}

まぁ、まじめなコンパイラなので、もとのコードは想像しにくい。

これを動かすためのコードを探すと、theories/Runtime にそれっぽいのがあった。 theories/Runtime/Makefile には three というサンプルプログラムを作るルールが書いてあるのだが、ソースが見当たらない。なので、必要な runtime だけビルドしてみる。

cd ~/coq/certicoq/theories/Runtime
make main.o nogc.o

で、さっき生成した Top.nat3.c のところに戻って、コンパイルしてみる。 (コンパイルオプションは theories/Runtime/Makefile に書いてあったもの)

gcc -m32 -g -O2 ~/coq/certicoq/theories/Runtime/main.o ~/coq/certicoq/theories/Runtime/nogc.o Top.nat3.c

で、実行してみる。

% ./a.out
Time taken 0 seconds 0 milliseconds
0(0(0(0)))

まぁ、動いたんですかね。

次は、自然数の 3 じゃなくて、10 を試してみる。

Definition nat10 := 10.
CertiCoq Compile nat10.

これで Top.nat10.c が生成され、実行すると以下のようになる。

% ./a.out
Time taken 0 seconds 0 milliseconds
0(0(0(0(0(0(0(0(0(0(0))))))))))

まぁ、0 の数がコンストラクタの数なのだろう、たぶん。

3 が 0(0(0(0))) ということは S が 3個と O が 1個。 10 が 0(0(0(0(0(0(0(0(0(0(0)))))))))) ということは S が 10個と O が 1個。

nat も素朴にコンストラクタで構成するわけだな。

では、この前報告した strict evaluation だと無限再帰になるやつを試してみよう。

Definition fstarg (x y : bool) := x.
Fixpoint f (z : bool) := fstarg true (f z).
Definition g := f true.

CertiCoq Compile g.

これで Top.g.c が生成され、コンパイルして実行してみる。

% gcc -m32 -g -O2 ~/coq/certicoq/theories/Runtime/main.o ~/coq/certicoq/theories/Runtime/nogc.o Top.g.c
(警告省略)
% ./a.out
Ran out of heap, and no garbage collector present!

お、GC が必要ですか。

さっきの　theories/Runtime で make gc.o として GC を作ってもう一回。

% gcc -m32 -g -O2 ~/coq/certicoq/theories/Runtime/main.o ~/coq/certicoq/theories/Runtime/gc.o Top.g.c
% ./a.out
Ran out of generations

こんどはしばらく時間がたった後にエラーになった。まぁこれは CertiCoq の責任じゃない (Coq でどうにかすべき) だろうけど。

#2 CertiCoq で依存型をコンパイルする

Gallina 全体を扱うということは、依存型を扱う必要がある。 proof elimination で消えてしまうものはいいとして、消えないもの、とくに以下のような、値によって型が変わるものをどう扱うか気になる。 (以下の例では、bool な b の値によって f1 と f2 の返値は bool か nat か変化する)

Definition ft (b : bool) :=
  if b then bool else nat.

Definition f1 (b : bool) : ft b :=
  match b return ft b with
  | true => true
  | false => 0
  end.

Definition f2 (b : bool) : ft b :=
  match b return ft b with
  | true => false
  | false => 1
  end.

CertiCoq Compile f1.
CertiCoq Compile f2.

というわけで CertiCoq でコンパイルして、f1 と f2 のコンパイル結果の違いを眺めるなどしてみたところ、たぶん、uniform representation という気がする。つまり、任意の値は (ポインタかもしれないけど) 1 word で表現できるというやつである。そういう表現であれば、OCaml の Obj.magic 相当 (あるいは、C の pointer や整数の cast) が可能であり、依存型であっても動作するコードを生成するのはなんとかなる。

GC (というか、メモリ管理) のところを調べれば確認できるだろ、ということで以下のあたりをながめるとやはりそれっぽい。

というか、なんか見覚えがある感じの構造や用語が... おぉ、gc.h の先頭に The current Certicoq code generator uses Ocaml object formats と書いてある。やはり。

天泣記

2018-04-07 (Sat)

2018-04-12 (Thu)

2018-04-19 (Thu)

2018-04-26 (Thu)

2018-04-28 (Sat)