歯が痛くて倒れていた

8月中旬頃、突然奥歯(の中の神経)に激痛が起こりました(結局明確な原因は不明)。
2週間くらいしてようやく普通の生活が出来るようになりました。あまりに酷い状態だったので書き留めておきます。

どんな状態だったかというと：

• 常に痛い。何もして無くても神経が痛い。でも痛くてじっとしてもいられないので家の中を徘徊し続けた。ただし歩いても痛い。詰みじゃん。
• 食べられない。4日間くらいお茶とポカリだけで生きていた。痛い以外の感情がないからか空腹感全くは感じない。今にして思うとちょっとやばいな。
• 痛み止めが効いている間は大体普通の生活が出来る。ただし効果は4〜5時間で切れ、かつ1日3錠までなので、任意の9時間(24 - (5 * 3))はのたうち回ることが確定。朝4時から5時間くらいうろうろし続けるのは心折れそうだった。
• 寝られない。痛いと寝られないんですね。初めて知りました。心配しなくても起きる方も痛み止めが切れる時刻にちゃんと起きます。人体って凄いね(^q^)。

他：
症状が出たのがコミケ直後だったので、会社でコミケで調子のってぶっ倒れたヤツみたいな扱いだったのが悲しかった。
原因はよく分からないから無関係という主張も出来ないんだけど…。

terraformのチュートリアルを読んだ

terraformのチュートリアルを一通り読んで実行した。

• チュートリアルを実行するのに必要な知識が全てチュートリアル内にあり、かなり分かりよい
• ほぼ写経で動く(1度AWSのよく分からないエラーが出たけど)
• 記述が古い箇所がある(動きはする)
• その時点でのconfiguration全体に自信が持てないことがある(remote backends(最後の節)は特に)

terraformの感想

便利そう。途中でエラーが出ても(何かを修正してやり直せば)設定通りの状態にしてくれる(はずな)ので安心感がある。

静的コード解析の会#6で発表してきた

静的コード解析の会#6でVeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…)

前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。
が、今回の発表では多重集合、整礎関係、実際の処理系で検査できるコードについての説明まで入れることが出来たので、これで一通りの内容を盛り込めたと思います(ただしシーケンシャルなプログラムに限る…)。
参照している論文はModular termination verificationです。

(多分)怪しげな記述や展開のよく分からないページがありますが、がんばって作ったので興味がある人は是非眺めてみて下さい。
個人的なおすすめはStatic Recursionパターンの検証方法のあたり(資料の末尾の方)です。

会場からは、

• 処理系が(もっと)がんばれ
• 発表の構成が悪い(直接そうは言われてないけど)

という感じの反応が得られました…orz。

感想

これまで何度かVeriFastに関する発表をしてるし、(呑みながら)議論もしてきたので聴衆の理解度が高くて非常に楽しい発表になりました。ありがとうございました。

また、懇親会でマルチスレッドの扱いについて質問がありました。通常の(部分正当性の)検査では問題無くスレッドが扱えますが、停止性検査については全く把握できていないので基本的なアイディアだけでも押さえておきたいと思っています。
参照した論文のTR版にマルチスレッドに関する議論があるようです。

参考リンク

• VeriFast
• Bart先生の論文
• 静的コード解析の会#6

SMLでSHA2アルゴリズムを実装しました

SMLでSHA2(Secure Hash Algorithm)というハッシュアルゴリズムを実装しました。
https://github.com/eldesh/sha2_sml.gitに公開してあります。現在のところSML/NJで動作を確認しています。
#こういう基本的な部品から実装して行くのが重要です。たぶん。

実装内容

RFC6234を実装しました。

	SHA224	SHA256	SHA384	SHA512	SHA512/224	SHA512/256
実装	✔	✔	✔	✔

SHA224,SHA256,SHA384,SHA512を実装してあります。他にSHA-512/224とSHA-512/256というのがありますがこちらは未実装です。
また入力として文字列とバイト(Word8.word)列しか受け取れず、(8の倍数で無い)ビットの列は入力できません。

インストール方法

readme.rstに書いてあります。
各コマンドの詳細を知りたい方は先日のエントリ(SMLUnitのインストールを通してSML/NJ向けのライブラリのインストール方法を解説する)を参照して下さい :)

使用例

インストールが出来たとして、使用する様子を紹介します。

sha2_sml$ sml
- CM.make "libsha2sml.cm";
(* ... snip ... *)
val it = true : bool
- Sha256.hashString "abc";
val it = - : ?.Sha256.word Sha256.t
- Sha256.toString it;
val it = "BA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015AD"
  : string

念のためsha256sumコマンドで確認します。

$ echo -n "abc" | sha256sum | tr [:lower:] [:upper:]
BA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015AD  -

やりました。

テスト

NISTのCAVPのshort/longのケース全て。それに加えてNESSIE*1のテストベクタの一部を使っています。*2。

全部パスしてるので、まぁ大体正しく実装出来てるんでしょう。きっと。
あとは処理系的に入力サイズが大きいとき不安。4GB超えた辺りとか。

まとめ

実装に思いの外時間がかかりました。ダメですね。RFCは分かりづらいような気もする

超重要なアルゴリズムなんですがRFCの日本語訳が見つからなかったのが意外でした。あと、NISTのサイトにもSHA2の定義はあるんですが、RFCの方が大分冗長ですね。

リンク

• https://tools.ietf.org/html/rfc6234
• NESSIE
• Cryptographic Algorithm Validation Program

*1:ネッシー？

*2:NESSIEさん、テストベクタのこのフォーマットはちょっと酷いんじゃ無いですかね…

定理証明支援系 matita のdockerイメージを作った

Matitaという定理証明系のdockerイメージを作りました。

MatitaはBologna(ボローニャ)大学で作られた、OCaml(+lablgtk)製の、依存型に基づく定理証明器です。
Leanの論文から参照されていたので知りました。
定理証明器の研究用途に作成されたようなので実用するものでは無さそうですが*1、検証器の実装に興味がある人には面白そうです。

最新版にはパッケージが無いようですし、ビルドも面倒なのでdockerイメージを作りました。 > eldesh/matita

使い方

$ docker pull eldesh/matita:0.99.3

IDEとして使用するため環境変数DISPLAYを指定して起動します。
# /usr/local/matita/matitacというのがCLIを提供するようですがよく分かりません*2。

$ docker run -it --rm -e DISPLAY=192.168.1.2:0 eldesh/matita:0.99.3

使い方を知るには/usr/local/matita/lib/tutorialにチュートリアルがあるのでこれを読むと良さそうです。

IDEの様子

私自身もまだ全く理解してませんが、ちょっとだけGUIの様子を紹介します。

左のペインがソースコードです。右下はmatitaのログのようです。
CoqIDEのように上から行毎にチェックを進め、右上のペインに現在の証明ゴールと前提が表示されています。
面白いのは[?3120][?3119]と表示されているタブで、これは各タブが各サブゴール毎の画面になっています。

分岐した後に各枝がどういった証明図(?)になっているのか簡単に分かるというのは便利そうです。

• matita official web site

*1:実用とは？

*2:-extract_ocamlというオプションもあるので気になりますね

SMLUnitのインストールを通してSML/NJ向けのライブラリのインストール方法を解説する

SML/NJにはCM(CompilationManager)というビルドツールが付いてきます。
以前は基本的な使い方を書きました>CompileManager(SML用make)の使い方。今回の記事ではSMLUnitというユニットテストライブラリを例にCMで管理するライブラリのインストール方法を説明します。

SMLUnitのインストール

SMLUnitというSML向けのユニットテストライブラリがあります*1。
このライブラリをSML/NJから使う際は以下のようにインストールします*2。

# 新
$ LOCAL_LIB=~/.smlnj/lib
$ mkdir -p $LOCAL_LIB
$ echo 'CM.stabilize true "smlunitlib.cm";' | sml
$ echo "smlunitlib.cm $LOCAL_LIB/smlunitlib.cm" >> ~/.smlnj-pathconfig
$ mkdir -p $LOCAL_LIB/smlunitlib.cm
$ cp -R .cm $LOCAL_LIB/smlunitlib.cm/.cm

上記のインストール方法は私がここ数日で見直したモノで、以前は以下の手順でした。

# 旧
$ SMLNJ_ROOT=<SML/NJをインストールした場所>
$ echo 'CM.stabilize true "smlunitlib.cm";' | sml
$ echo "smlunitlib.cm smlunitlib.cm" >> $SMLNJ_ROOT/lib/pathconfig
$ mkdir -p $SMLNJ_ROOT/lib/smlunitlib.cm
$ cp -R src/main/.cm $SMLNJ_ROOT/lib/smlunitlib.cm/.cm

pathconfigファイルの詳細は後述しますが、ライブラリの配置場所を指定しています。

以前と違って新しい方法では処理系がインストールされたディレクトリやそれ以下のファイル($SMLNJ_ROOT/lib/pathconfig)を書き換える必要がありません。
見ての通りCMはビルド時に$HOME/.smlnj-pathconfigも読みに行くのです。非常に行儀が良くなりましたね。

Dockerイメージから使う

上記のような方法を採ると、ホスト側にライブラリをインストールしておき、それをDockerイメージから読み込むこともより簡単に出来ます。

例としてSMLUnitを上の方法でインストールした上で、それをDockerイメージから利用する方法を以下に示します。

$ ls ~/.smlnj/lib/
smlunitlib.cm
$ docker run -it --rm -v $HOME:$HOME -e HOME=$HOME eldesh/smlnj:110.82
- CM.make "$/smlunitlib.cm";
(* ... snip ... *)
- open SMLUnit;
(* ... signatureだばー ... *)

出来ました。

しかし $HOME を差し替えているのが微妙に気持ち悪いですね？
実は CM_LOCAL_PATHCONFIG という環境変数で直接 pathconfig ファイルを指定することも出来ます！

$ docker run -it --rm -v $HOME:$HOME -e CM_LOCAL_PATHCONFIG=$HOME/.smlnj-pathconfig eldesh/smlnj:110.82
- CM.make "$/smlunitlib.cm";
(* ... snip ... *)
- open SMLUnit;
(* ... signatureだばー ... *)

やりました。
以上で真っ当にライブラリをインストール;利用出来る環境になりました。

CMの詳細な動作

CMはライブラリを探す際以下のように動作します。

1. CM_PATHCONFIG が定義されていたらそれを読む
2. CM_PATHCONFIG が定義されてなければ $SML_ROOT/lib/pathconfig を読む
3. CM_LOCAL_PATHCONFIG が定義されていたらそれを読む
4. CM_LOCAL_PATHCONFIG が定義されていなければ $HOME/.smlnj-pathconfig を読む

pathconfig ファイルはライブラリの名前とその場所を指定する設定ファイルで、構文と意味は以下の通りです。

• 行毎にファイル先頭から処理される
• 二つのトークンから成る行は '<ライブラリ名> <ライブラリパス>' と解釈され、エントリが追加される
• 一つのトークンのみから成る行は '<ライブラリ名>' と解釈され、その名前のエントリは削除される
• '-'(マイナス)のみの行はそれ以前の内容を全てリセットする
• 空行は無視される

#以上の内容は CM公式マニュアル §3.4 Anchor configurationに書いてあります。

まとめ

まとめると、SML/NJ向けのライブラリをインストールする際は以下のような手順で行うと良さそうです。

$ LOCAL_LIB=~/.smlnj/lib
$ mkdir -p $LOCAL_LIB
$ echo 'CM.stabilize true <インストールしたいライブラリのCMファイル>;' | sml
$ echo "<インストールするライブラリ名> <インストール先>" >> ~/.smlnj-pathconfig
$ mkdir -p <インストール先>
$ cp -R .cm <インストール先>/.cm

リンク

• CM公式マニュアル
• eldesh/SMLUnit
• SML/NJ Dockerイメージ(非公式)

*1:SML#には処理系本体に同梱されているのでそちらを使いましょう

*2:SMLUnit/readme.md Setup>SML/NJ参照

MLtonのdockerイメージを作りました

SMLの最適化コンパイラであるMLtonのDockerイメージを作りました。

MLtonは開発は行われているのですが、長らくリリースが出ていないため使いづらい状態です。あとなぜか私の手元だとビルドに失敗したりします*1。
そこで現状の開発ヘッドをビルドしたイメージを作りました。

• latest タグでgithubのmaster
• 20130715 タグが現状最新のリリース

に対応します。

使い方

一応使い方書きますと:

$ docker pull eldesh/mlton:latest

このように取得できます。

で、(例えば)以下のように実行します。

$ ls
main.sml main.mlb
$ docker run --rm -v `pwd`:`pwd` --workdir=`pwd` eldesh/mlton:latest -output main main.mlb
$ ./main

*1:このイメージビルド時にはてきとーなパッチ当ててます