Zenn
Open7

Separation Logicの学習メモ

coq
nozonozo

環境構築

WSL2(Ubuntu)+vscodeな環境でやる。vscodeにはvscoqという拡張があるのでそれを使う。

https://github.com/coq-community/vscoq

vscoqのインストール手順に書いてある通りだけど、以下の手順をUbuntu上で実行する。これでcoqの実行環境とvscoq拡張を使う準備が完了する。

$ sudo apt install opam
$ opam init
$ opam pin add coq 8.18.0
$ opam install vscoq-language-server

Software FoundationsのVolume 6のソースコードをダウンロードする。
https://softwarefoundations.cis.upenn.edu/slf-current/slf.tgz

ソースを展開してmakeを実行して、vscodeを起動する。

$ tar xzf slf.tgz
$ cd slf/
$ make
$ code .

vscodeの拡張からvscoqを探してインストールする。その後、vscoqの設定の"Vscoq:Path"という項目に以下を設定する。（opamでインストールした時のデフォルトのパス）

/home/<user_name>/.opam/default/bin/vscoqtop
nozonozo

Basic : triple_incr

最初の例は次のプログラムを対象にSeparation Logicを考えるというもの。
<{}>で囲われたプログラムはCoq上で定義されたOCamlライクな言語(詳しい定義はAPPENDIXにある)で、関数incrは参照'pが指す整数を＋１するプログラムを表す。

Definition incr : val :=
  <{ fun 'p ⇒
      let 'n = ! 'p in
      let 'm = 'n + 1 in
      'p := 'm }>.

Separation Logicでプログラムincr pの仕様を記述すると以下のようになる。
triple <プログラム> <事前条件> <事後条件>という形で記述される。

Lemma triple_incr : ∀ (p:loc) (n:int),
  triple <{ incr p }>
    (p ~~> n)
    (fun _ ⇒ (p ~~> (n+1))).

この３つ組を"Separation Logic triple"という。"Hoare triple"のSeparation Logic版みたいなものと考えればよさそう。

"Hoare triple"の意味はVolume 2で以下のように説明されている。「プログラムcがPを満たす初期状態のもとで実行が終了するならば終了状態がQを満たす」ことを{P} c {Q}と表す。
Separation LogicではP, Qがメモリ状態を表す。

A Hoare triple is a claim about the state before and after executing a command. The standard notation is

{P} c {Q}

meaning:

  • If command c begins execution in a state satisfying assertion P,
  • and if c eventually terminates in some final state,
  • then that final state will satisfy the assertion Q.

triple_incrの事前条件(p ~~> n)において、pは関数incrの引数として与えられた参照セルの"location"、つまりメモリ上のアドレスを示す。p ~~> nはpが指すアドレスの内容が値nであるメモリ状態を表す。

プログラムincr pが実行されたとき、pが指すアドレスの内容が＋１されるので、メモリ状態はp ~~> (n+1)になるはずである。

triple_incrの事後条件は(fun _ ⇒ (p ~~> (n+1)))という形になっている。プログラムが何か意味のある値を返す場合は、fun r = ...として返り値をrに束縛して扱うことができるが、関数incrは参照先の値を＋１するだけで返り値は意味を持たないUnit型で返ってくるため_で捨てている。

まとめると、Separation Logicで表現された仕様{p ~~> n} incr p {p ~~> (n+1)}は、「プログラムincr pがメモリ状態p ~~> nを満たす初期状態のもとで実行が終了するならば終了メモリ状態がp ~~> (n+1)を満たす」ことを表している。

nozonozo

triple_incrは仕様を定義しただけなので、この仕様が正しいか証明する。
とは言っても、この時点ではSeparation Logicの推論規則について説明がないので雰囲気だけ見ておく(後ろのコースで説明されるらしい)。

証明は以下のように書ける。
証明を開始するxwp、関数呼び出しに関する推論を行うxapp、ある状態の記述が別の状態を含むことを証明するxsimplなどのtacticを使っている。

Lemma triple_incr : forall (p:loc) (n:int),
  triple <{ incr p }>
    (p ~~> n)
    (fun _ => (p ~~> (n+1))).
Proof.
  xwp.
  xapp.
  xapp.
  xapp.
  xsimpl.
Qed.

以下に各ステップのゴールを横並びに書き出してみた。

PRE (p ~~> n)                        -xapp-> PRE (p ~~> n)                       -xapp-> PRE (p ~~> n)                       -xapp-> p ~~> (n + 1) ==> p ~~> (n + 1)
CODE <[                                      CODE <[                                     CODE <[
  Let v := `(App val_get p) in                                                           
`(Let v0 := `(App val_add v 1) in            Let v := `(App val_add n 1) in              
`(App val_set p v0)) ]>                      `(App val_set p v) ]>                       App val_set p <{ {n + 1} }> ]>
POST (fun _ : val => p ~~> (n + 1))          POST (fun _ : val => p ~~> (n + 1))         POST (fun _ : val => p ~~> (n + 1))

各ステップの推論は以下の通り。

  • xwpを適用した直後のゴールは左端の状態になる。incr pの中身が展開される。
  • １つ目のxappでv = !pの推論が進む。vがnに置き換わる。
  • ２つ目のxappでv = n+1の推論が進む。vがn+1に置き換わる。
  • ３つ目のxappでp := n+1の推論が進む。事前条件のメモリ状態が更新されp ~~> (n + 1) ==> p ~~> (n + 1)というゴールが得られる。

最後のH1 ==> H2は両方が一致することをチェックする。xsimplを適用することで解決する。
一応これで証明は完了した。

nozonozo

Basic : triple_example_let

次は返り値がある関数の例。関数example_letは整数nを引数にとり、最終的に2*nを返す。

Definition example_let : val :=
  <{ fun 'n ⇒
      let 'a = 'n + 1 in
      let 'b = 'n - 1 in
      'a + 'b }>.

プログラムexample_let nの仕様は以下のように書ける。

Lemma triple_example_let : ∀ (n:int),
  triple (example_let n)
    \[]
    (fun r ⇒ \[r = 2*n]).

事前条件の\[]は空のメモリ状態を表している。別の言い方をすると、このプログラムは事前に割り当てられたデータに干渉することはないことを表すことになる。

事後条件のfun r ⇒ \[r = 2*n]の\[...]も空のメモリ状態を表している。rにはプログラムの返り値が束縛されていて、r = 2*nという述語で返り値が2*nであることを表している。このように空のメモリ状態\[P]の中の述語Pを"pure facts"と呼ぶ。(メモリ操作以外の純粋な部分に関する述語だからpureなのかな？)

triple_example_letの証明は新しいことがなさそうなので省略。

nozonozo

Basic triple_incr_two

次は参照が複数ある例。関数incr_twoは参照を２つ引数にとり、それぞれ＋１する。

Definition incr_two : val :=
  <{ fun 'p 'q ⇒
       incr 'p;
       incr 'q }>.

プログラムincr_two p qの仕様は以下のように書ける。

Lemma triple_incr_two : ∀ (p q:loc) (n m:int),
  triple (incr_two p q)
    (p ~~> n \* q ~~> m)
    (fun _ ⇒ p ~~> (n+1) \* q ~~> (m+1)).

事前条件のp ~~> n \* q ~~> mは２つの参照p ~~> nとq ~~> mが存在して、かつ、それらが互いに異なる参照であることを\*が表している。\*は"separating conjunction"と呼ばれ、"star"オペレータとも言う。

事後条件のp ~~> (n+1) \* q ~~> (m+1)は、各参照の内容が＋１されることを表している。

p ~~> n, \[], H1 \* H2は"heap predicates"と呼ばれる。

nozonozo

仕様triple_incr_twoは関数incr_twoに異なる２つの参照を与えた場合のみについて言及している。そのため、関数incr_twoに同一の参照を与えるプログラムをtriple_incr_twoで推論しようとすると証明が詰まる。

関数incr_twoに同一の参照を与えるプログラムaliased_callを以下のように定義する。

Definition aliased_call : val :=
  <{ fun 'p ⇒
       incr_two 'p 'p }>.

プログラムaliased_callは同じ参照について＋１を２回実行するので仕様は以下のように書ける。

Lemma triple_aliased_call : ∀ (p:loc) (n:int),
  triple (aliased_call p)
    (p ~~> n)
    (fun _ ⇒ p ~~> (n+2)).

仕様triple_aliased_callの証明を以下のように進めるとxappで詰まる。
(この証明ではtriple_incr_twoを推論に使うことを明示していないが、本編では#[global] Hint Resolve triple_incr_two : triple.という定義をしているので、おそらく自動で使われている。)

forall p n, triple (aliased_call p) (p ~~> n) (fun _ : val => p ~~> (n + 2))

  - xwp ->

PRE (p ~~> n)
CODE <[ App incr_two p p ]>
POST (fun _ : val => p ~~> (n + 2))

  - xapp ->

\[] ==> p ~~> ?m \* ((fun _ : val => p ~~> (n + 1) \* p ~~> (?m + 1)) \--* (fun _ : val => p ~~> (n + 2)))