VeriFastのDockerイメージを作りました

C言語/Java検証器であるVeriFastのDockerイメージを公開しました。
> https://hub.docker.com/r/eldesh/verifast/

現時点(2017/8/24)での開発ヘッドをビルドしてあります*1。リリース版は公式サイトでバイナリが配布されているのでそちらを使いましょう。

このイメージはgitのコミットハッシュをタグにしてあり、latestタグは無いので明示的にこれを指定してDockerイメージを取得する必要があります。

つまり以下のようにすると

$ docker pull eldesh/verifast:93c7917

取得できます。

使い方

デフォルトではvfideというVeriFastのGUIフロントエンドが起動するので、以下のように環境変数 DISPLAY の設定が必要です。

// 例: ディスプレイ 192.168.1.2:0 を使う
$ docker run -e DISPLAY=192.168.1.2:0 eldesh/verifast:93c7917

当然ながらverifastコマンドもインストールされているので、明示すれば使うことが出来ます。

// ボリューム some-vol にあるコードを検査
$ docker run -v some-vol:/src eldesh/verifast:93c7917 verifast /src/hoge.c

ついでにZ3サポートも付いています。

// SMTソルバとしてZ3を使う
$ docker run -v some-vol:/src eldesh/verifast:93c7917 verifast -prover z3v4.5 /src/hoge.c

*1:テストをパスすることを確認しているのでこのバージョンでチュートリアルを解いても問題無いです

SML#3.3.0のDockerイメージを作った

Dockerの練習として SML#3.3.0 の入ったDockerイメージを作ってみました。> https://hub.docker.com/r/eldesh/smlsharp/

$ docker pull eldesh/smlsharp:3.3.0

とやれば使えるはず。ベースイメージは centos:centos7.3.1611 です。
LLVMのサイズが強敵でした。

使用例

$ sudo docker pull eldesh/smlsharp:3.3.0
Trying to pull repository docker.io/eldesh/smlsharp ...
3.3.0: Pulling from docker.io/eldesh/smlsharp
45a2e645736c: Already exists
85c1b05ddc2b: Pull complete
5112e2b943c9: Pull complete
Digest: sha256:801b4d8f650ff25be594ecacab6029e6afc3992c3d4cebe8edc0454a1dde9ed3
$ sudo docker run -it --rm --name SMLSharp eldesh/smlsharp:3.3.0
SML# 3.3.0 (2017-06-20 18:17:19 JST) for x86_64-pc-linux-gnu with LLVM 3.7.1
# val puts = _import "puts" : string -> int;
val puts = fn : string -> int
# puts "Hello, SML#";
Hello, SML#
val it = 12 : int

デフォルトで rlwrap 越しに起動するのでで履歴にアクセス出来て便利です。

Dockerイメージのアップロードが謎の失敗

VMware Player上のCentOSからDockerHubへのDockerイメージのアップロードが謎の理由で失敗する。
当然 docker login 済み。

以下のようになる。

smlsharp-3.3.0$ sudo docker push eldesh/smlsharp:3.3.0
The push refers to a repository [docker.io/eldesh/smlsharp]
5216ccdd4424: Pushing [==================================================>] 549.2 MB
bdc4c3dd2305: Layer already exists
34e7b85d83e4: Layer already exists
unauthorized: authentication required

なぜ最後に認証情報を確認するんだろう…？

ともかくログは以下のようになっていた。

smlsharp-3.3.0$ cat /var/log/messages
.
.
Aug  7 18:12:14 localhost kernel: XFS (dm-4): Unmounting Filesystem
Aug  7 18:12:20 localhost dockerd-current: time="2017-08-07T18:12:20.802131012+09:00" level=error msg="Upload failed: unauthorized: authentication required"
Aug  7 18:12:20 localhost dockerd-current: time="2017-08-07T18:12:20.804147067+09:00" level=error msg="Attempting next endpoint for push after error: unauthorized: authentication required"
Aug  7 18:14:50 localhost dockerd-current: time="2017-08-07T18:14:50.518246440+09:00" level=info msg="{Action=auth, Username=eldesh, LoginUID=1000, PID=35534}"
.
.

VMの時刻が大幅に間違っているのを直したら正常に動作するようになった。

smlsharp-3.3.0$ date -s 2017/08/08 01:17:00
smlsharp-3.3.0$ docker push eldesh/smlsharp:3.3.0
The push refers to a repository [docker.io/eldesh/smlsharp]
5216ccdd4424: Pushed
bdc4c3dd2305: Layer already exists
34e7b85d83e4: Layer already exists
3.3.0: digest: sha256:c5df978cac256fe7d605398051fd12705337c05fed10e1e2b5f8a1a39ef12775 size: 950
smlsharp-3.3.0$

時々この手のエラー踏むよね…。

ちなみに~/.docker/config.json を設定しろというissueが挙がってけど今回は無関係だった*1。

環境

• Linux 3.10.0-514.26.2.el7.x86_64 GNU/Linux
• CentOS Linux release 7.3.1611 (Core)
• Docker version 1.12.6, build 88a4867/1.12.6

*1:関係無いけどまさかパスワードを生で送ってるわけじゃないよね…？

ML勉強会#2 と ProofSummit2017 に参加した

ProofSummit2017とML勉強会#2に参加してきました。
とりあえず二日連続はつらいものがあった。

個々の感想

• SML#の話は良かった。言語や処理系の機能が列挙されていると個人的に楽しい。そういう意味ではATSも楽しいんだけど、機能(のアップデート)が少なかったし、楽しさの半分は岡部さん自身が面白いことに由来している気もする。

• OCamlのjupyterの話。blasのラッパーしか無さそうならSMLで実装もアリかなと思っていたけど、意外と環境が整っていそうなのでOCaml+Jupyterを試してみようという気になった。

• autorewriteの話のストーリーが良かった。既存の部品を使って問題がうまく解決されている(と思う)。

• tanakaさんのCoqの話は楽しいような気がした。でもtrusted baseが小さいという主張はなんかだまされた感がある。(C側の実装をVeriFastで検証しませう？)

• パワーの溢れる若者が機械学習で自動証明の話をしていた。まだちょっと無理がある印象。証明戦略の選択をする話とかはまずSMTソルバとかでやってみてうまくいくことを確認してからでもいいんじゃないかという気がした。まぁ研究は野心的なことをやるべきなのかも知れないけど。そういえば発表中に出て来たものはほとんど対象がHOLだったし、自動化し易いのかな。

全体の感想

• 発表にはストーリーがある(かつ明確な)方が良い。どこが主張で、今どの辺について喋ってるのか分からないとつらい。どの辺が重要なのか判定不能なので一瞬でも聞き逃すとリカバリ不能になる(というかする気がなくなる_(:3」∠)_。例えばコード生成について話してるけど、それ以降で高階型推論についての考察が始まるのか、シンタックスについてのコダワリが語られるのか、生成系の証明が始まるのかで注視するとこが違ってくる。聞きながらググるべき事の選定にも効いてくる(かも知れない)。

• 特にそれが有名で無い場合は、紹介or提案or実装している言語or処理系or論理体系の大雑把な能力の説明があった方が良い。命題論理か述語論理か、一階か高階か、コンパイラかインタプリタか、型推論は完全性を持つのかなどなど。

• あと発表と無関係だけどJavaScriptへの殺意が高まった

ゼロから作るDeep Learningを読んだ

ゼロから作るDeep Learningを読み終わりました。おおよそ一ヶ月くらいかかりました。

機械学習自体(とpython)の全くの素人状態から読みましたが、とりあえず、単独で読み切れる本です。
その点は良いですね。

本全体を通して、MNISTと言われる手書き数字のデータセットを使って識別器を作っていきます。(と言っても形になるのはだいぶ後の方ですが。)

タイトルでは「ゼロから作る」と言ってますが、全部を作るとは言ってません。気をつけて下さい。
画像系のDeep Learningで重要になる(らしい)CNNの説明は最後辺りの章で出てきますが、「バックプロパゲーションは自明だから(リポジトリ中の)コード読んどいてね。」という感じになっています。加えて重要なアルゴリズムである im2col についても同様の扱いです。
他に注意点として、関数の導入時点での実装が使用時点では使えないというケースがあります。これについては文中に注意書きがありますが、使えない実装を紹介されても困りますよね…。

あとはエラッタが多い印象です。出来るだけ新しい版を買った方がいいと思います。
(エラッタは公式のgithubリポジトリにまとまっています。)

まとめると、

• 一人で読める
• deep learningについて基本なことが平易に書いてある(気がする)
• CNNについてはさほど丁寧じゃない
• pythonは破綻した言語

静的コード解析の会で停止性検証について発表してきた

静的コード解析の会#2でVeriFastによる停止性検証の導入の話をしてきました*1。
本当は私自身も発表するほど分かってないのですが、それでも楽しい部分はあるので「これまで理解している内容を詰め込んでみた」という感じでまとめてみました。(前日深夜から突貫だったので超眠かった…)

今回の発表で伝わったかは怪しいですが、停止性のために最低限の機能を導入し、既存の機能を活かした仕組みはとても素晴らしいと思います。
楽しい部分を端的に挙げると、

• 多重集合のある種の順序関係からどんどん「関数を呼ぶ権利」が出てくる
• 関数の順序関係をコード上の大小関係で決めた

まぁこれだけ聞いても絶対分からないので、詳しく知りたい方はModular termination verificationを読みましょう。

振り返り

前回に引き続きVeriFastの話ですが、今回の内容は前回と比べて取っつきにくい内容でした。
理論的にも難しい割には、そもそも停止性なんて検証して何がうれしいのかから分かりづらいと思い、検証のモチベーションから始めています。

VeriFastでは動的束縛を伴う(=関数ポインタを使った)関数の相互再帰関数といった、かなり複雑な関数の停止性を検証することが出来ます。が、発表としては面白い具体例をほとんど出せなかったのは悔やまれるところです。

他の人の発表では @tanaka_akr さんのCoq2Cの話を聞き逃したのが残念でした…。

次回

このスライドでは序論といった範囲止まりですので、実際にC言語(あるいはJava)コードの停止性を検査するために覚えるべきことはもう少しあります。
次回はそのあたりまで理解して紹介できたらいいなぁという気持ちです。

あとは、今回の発表中から意図的に省いた単語として「整礎(関係|集合)」というモノがあるのですが、これは多重集合などと言うモノを持ち出した意味をはっきり述べるために必須の概念ですので、…勉強しておきます。はい。

*1:前回の発表> http://d.hatena.ne.jp/eldesh/20161121/1479703222

静的コード解析の会 第0回 でVeriFastについて発表してきた

#静的コード解析の会 第0回でC言語(とJava)の検証器であるVeriFastについて発表してきました。

資料は公開してあるので興味ある人は見てください。動画もあります。
> https://metasepi.connpass.com/event/42141/presentation/

結構(私の理解が)きわどい質問も出ましたが、大体伝えたかった内容は伝わったんじゃないかと思います。
個人的には手ぶらで(ぐだぐだ)発表したProofSummit2016のリベンジでもあったので資料はかなり頑張って作りました。(内容は全然違いますが

本当に詳しく知りたい人は公式チュートリアル読むべきなのですが、これは結構ヘビーな量と内容です。これに対して私の発表は「忙しい人向けの入門」といった感じなのでお気軽にどうぞ(^^)

他の発表について

CSPというのを初めて知りました。プロセス代数というのは(多分大学生の時に)聞いたことはあったんですが、通信するプリミティブがあるなぁ、くらいのことしか分かりませんでした。
今になって説明を聞くと、多少理論的な話や記号が出てもビビらなくなったし、なんとなく理解できる部分も増えていたので嬉しみがありました(なお、日本語力は低下したもよう…)
あとCMLに似てますね(これは多分関係が逆だけど)。

自分がここ数年多少なりとも理論的な話として勉強してきた内容は、主に(型付き)ラムダ計算とその意味論だったので、実装でも仕様でもない(あるいはどちらにもなる？)ものと意味論を扱うというのは新鮮でした。

他には具体的に気になったものとしてトレース意味論というのが紹介されていました。これはプログラムの副作用を形式的に扱う方面でも出てきてよく分からなかったんですが、CSPでの扱いはかなり明快だなという感じを受けました。(プロセス間の作用が初めから限定されているから当たり前か？
あとは「coinductive」という単語も出ていたので、それを持ち出す気持ちくらいは知りたいなという感じです。

気になるワードは他にも幾つか出ていたので忘れないうちにフォローしておきたいですね。

最後にInferですが、やはり残念だという結論のようです…。
個人的には少なくともFalse Positiveは出てほしくないですねぇ。
ヒューリスティクスでなく理論的基礎がしっかりしているということに期待出来る/したいのはそこだと思うので。

次回

来年(2017)の2月に第1回を開催するみたいです。
私もネタはあるので体力があれば発表するかも知れません。