blog.anqou.net
rss
author
tags

FStar Tips

#tech

この記事はもともと別場所にて公開していました。

気づいたことを雑にまとめる。Markdown で”F*“とかくとバックスラッシュが必要でダルいので、適宜”FStar”で代用する。

#疑問

#お役立ち文献

#インストールに関するもの

大抵はopam pin add fstar --dev-repoすると入る。

##macOS で FStar をインストールする

2021 年 6 月 6 日時点の情報。master のハッシュは c037e4c。環境は macOS High Sierra（バージョン 10.13.6）。MacBook Air (13-inch, 2017).

opam pin add fstar --dev-repoすると Z3 4.8.5 のインストールで libgomp が見つからずこける。

追記：2021 年 9 月 21 日にも成功を確認。

#LowStar/KreMLin に関するもの 

module P = LowStar.Printf
module B = LowStar.Buffer
module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module M = LowStar.Modifies

##KreMLin をビルドする

README のとおりにすると（opamで必要なライブラリを入れて、ルートでmake）、途中でFSTAR_HOMEとKREMLIN_HOMEを指定しろというエラーが出る。前者は FStar のレポジトリをgit cloneしたディレクトリ、後者は KreMLin のレポジトリをgit cloneしたディレクトリを指定すれば良い： 

$ FSTAR_HOME=~/workspace/FStar_ KREMLIN_HOME=~/workspace/kremlin make

ただし FStar の方はビルドされている必要がある。特にulibのビルドが必要なため、 make -C ulibしておく。

##KreMLin で FStar コードを C コードにコンパイルする

KreMLin のルートディレクトリにあるkrmlを使う。単純な場合なら、必要なものを全て引数に渡せばいい。ただし-drop WasmSupportをつけておく。以下はKreMLin のドキュメントに載っている例。 

// intro.fst
module Intro

module P = LowStar.Printf
module C = LowStar.Comment
module B = LowStar.Buffer

open FStar.HyperStack.ST
open LowStar.BufferOps

let main (): St Int32.t =
  push_frame ();
  let b: B.buffer UInt32.t = B.alloca 0ul 8ul in
  b.(0ul) <- 255ul;
  C.comment "Calls to printf are desugared via meta-programming";
  let s = "from Low*!" in
  P.(printf "Hello from %s\nbuffer contents: %xul\n"
    s 8ul b done);
  pop_frame ();
  0l

// main.c
##include "Intro.h"
int main() { Intro_main(); }

以上を作って次のように食わせるとa.outができる： 

$ ~/workspace/kremlin/krml intro.fst main.c -drop WasmSupport

実行ファイルでなく、静的ライブラリにしたい場合は、一度Makefile.basicを作らせてからそれを手で実行する必要がある。また、使いたいときはlibkremlin.aをリンクする必要がある。 

$ ~/workspace/kremlin/krml -skip-compilation intro.fst -drop WasmSupport -o libintro.a
$ KREMLIN_HOME=~/workspace/kremlin/ make -f Makefile.basic
$ gcc -I ~/workspace/kremlin/kremlib/dist/minimal \
      -I ~/workspace/kremlin/kremlib \
      -I ~/workspace/kremlin/include \
      -L ~/workspace/kremlin/kremlib/dist/generic \
      -L . \
      main.c -lintro -lkremlib

##スタックを一時的に使う

HST.push_frame ()とHST.pop_frame ()で全体を囲う。スタックにはB.allocaを用いてデータを配置する。

##スタック・ヒープに変更を加えていないことを主張する

M.modifies M.loc_none h h'とする。

HST.push_frame ()とHST.pop_frame ()に囲われていて、 B.allocaで確保した領域のみを使用している場合はこれを満たす。

#HyperStack/HyperHeap に関するもの

適宜以下を仮定。 

module HS = FStar.HyperStack
module HSST = FStar.HyperStack.ST

##FStar.HyperHeapがない

いつの間にか消えた。おそらくHeap のモデルが変わったとき だと推測されるが、定かではない。代わりにFStar.Monotonic.HyperHeapが生えたが、これは直接使うことを意図されていないとコメントに書いてある。代わりにFStar.HyperStackをopenする。

このあたり、heap に関する FStar tutorial の説明は全般的に古い。多分 2014（要調査）年付近で止まっているのだと思う。

##disjoint なリージョンなら書き換えても影響がない

形式化するとこう。 

val piyopiyo : h:HS.mem -> h':HS.mem -> r1:HS.ref nat -> r2:HS.ref nat -> Lemma
  (requires (HS.contains h r1 /\ HS.contains h r2 /\
             HS.disjoint (HS.frameOf r1) (HS.frameOf r2) /\
             h' == HS.upd h r1 0))
  (ensures (HS.sel h r2 = HS.sel h' r2))
let piyopiyo h h' r1 r2 = ()

##HS.updで形式化すると disjoint が FStar に見えない

同じことをHS.modifiesやHS.modifies_oneで書いて連言でつなぐと見える場合がある。

##HyperHeap と単一ヒープにおいて、disjoint を書くときの本質的な違い

参照が入ったリストを相手にするとき、後者なら必ず再帰が必要になる。前者なら、リストの中身がすべて同じリージョンにあると仮定できれば、一つのリージョンについて言及すればいい。なおHS.modifiesは引数にリージョンをとる。

##includes, extends, disjoint

FIXME: コードも turorial もようわからん。要調査

グラフの位置関係の述語。共通の祖先を持たなければ disjoint。親子の関係なら extends。親子もしくは自分自身なら includes。

##HS.refのアドレスをとる

HS.as_addrを使う。

##HSST.op_Colon_Equalsを使う

HS.refに対しては使えず、HSST.refに対して使う必要がある。これらの違いについては要調査。 

val fugafuga : r:HSST.ref 'a -> v:'a -> HSST.ST unit
  (requires (fun h -> h `HS.contains` r))
  (ensures (fun _ _ _ -> true))
let fugafuga r v =
  HSST.op_Colon_Equals r v

##HS.containsとHS.live_region

HS.live_regionをみたす region に対してHS.updでき、これをするとHS.containsをみたすようになる。 

val tmptmp14 : h:HS.mem -> rb:HS.ref 'a -> va:'a -> Lemma
  (requires (HS.live_region h (HS.frameOf rb)))
  (ensures (
     let h' = HS.upd h rb va in
     h' `HS.contains` rb
  ))
let tmptmp14 h rb va = ()

##2 つのmodifiesをmodifiesの推移律でSet.unionを使って一つにまとめる

ヒープがh1、h2、h3と遷移するときに、h1からh2のときのmodifies集合と、 h2からh3のときのそれをSet.unionをつかってまとめてh1からh3のそれとしたい。

HS.lemma_modifies_transを使えばできる、と書きたかったのだが、いま試したら補題無しで動いた。要調査。

##ST の関数内部で heap を参照する

HSST.get ()が使える。

#LowStar.Bufferに関するもの

##LowStar.Bufferとは

C 言語の配列を表すための Low*用のコンテナ。OCaml のBigarrayをモデル化するときに使える。本体はLowStar.Monotonic.Buffer.mbufferにある。monotonic な要素が必要ない場合は LowStar.Buffer.bufferが使える。

以下ではLowStar.BufferのことをLSB、LowStar.Monotonic.BufferのことをLSMBと書く。文脈が明らかな場合は適宜省略する。

##64bit の添字に対応させる

LSMBは添字としてUInt32.tを使用している。これをUInt64.tに変えるためには LowStar.Monotonic.Buffer.fst/fstiのU32をU64に置き換えたものを新たに作る。

##LSMB.mbufferをGhostに読み出す・書き換える

getとg_updが使える。

##LSMB.mbufferのgetとg_updが対応することを示す

要するにg_updした後にgetすればg_updした内容と同じ内容が読み込めるということを示したい。実はこれを行う補題がLSMBには存在しない（！）ため、自分で次のように作る必要がある。補題の本体は()のみで構わない。 

val lem_get_g_upd1 (#a:Type0) (#rrel #rel:srel a) (b:mbuffer a rrel rel)
                   (i:nat) (v:a) (h:HS.mem) : Lemma
  (requires (i < length b /\ live h b))
  (ensures (get (g_upd b i v h) b i == v))
  [SMTPat (get (g_upd b i v h) b i)]

val lem_get_g_upd2 (#a:Type0) (#rrel #rel:srel a) (b:mbuffer a rrel rel)
                   (i:nat) (j:nat) (v:a) (h:HS.mem) : Lemma
  (requires (i < length b /\ j < length b /\ live h b /\ i <> j))
  (ensures (get (g_upd b i v h) b j == get h b j))
  [SMTPat (get (g_upd b i v h) b j)]

##g_updとloc_buffer_from_toを結びつける

g_upd_modifies_strongが使える。

##LSMB.mbufferの一部を書き換えたことを主張する

FStar.ModifiesGenを使用して基本的なmodifiesやlocが整備されているため、これらを使うことでLSMB.bufferの書き換えに言及できる。

とくにLSMB.bufferの一部分を書き換えた場合には LSMB.loc_buffer_from_toが使える。全体を書き換えた場合はLSMB.loc_bufferを使う。

##HSST.refについてLSMB.modifiesを使う

LSMB.loc_mreferenceで包む。

##loc_includes (loc_buffer ...) (loc_buffer_from_to ...)を示す

補題loc_includes_loc_buffer_loc_buffer_from_toを使う。

##loc_disjoint (loc_mreference a) bでbに書き込んだときにaが変わらないことを言う

要するに buffer と disjoint な参照の内容は変化しないというやつ。 LSMB.modifies_mreference_elimが使える。SMTPatがあるので、通常意識しなくてもすむ。

##HS.modifiesをLSMB.modifiesに変換する

LSMB.modifies_loc_regions_introが使える。 

val piyopiyo
  (h h':HS.mem)
  (b:LSB.buffer Char.char)
  (r:HST.ref int)
  : Lemma
  (requires (
     LSB.live h b /\
     0 < LSB.length b /\
     HS.disjoint (HS.frameOf r) (LSB.frameOf b) /\
     HS.modifies (Set.as_set [HS.frameOf r]) h h'
  ))
  (ensures (
     LSB.get h b 0 = LSB.get h' b 0
  ))
let piyopiyo h h' b r =
  LSB.modifies_loc_regions_intro (Set.as_set [HS.frameOf r]) h h';
  assert (
    let open LSMB in
    loc_disjoint (loc_region_only true (HS.frameOf r)) (loc_buffer b) /\
    modifies (loc_region_only true (HS.frameOf r)) h h'
  );
  // LSB.modifies_buffer_elim requires "LSB.live h b"
  ()

FIXME: HSとLSBのヒープの変換をする関数を表かなにかでまとめる

#Tactics

##タクティックとは

Meta-F*という論文で FStar に Coq のような tactics が導入された。 assert (...) by (...) という形で証明に使える。各assertは別々のクエリとして Z3 に投げられるため、Z3 rlimit の指定もassert毎に適用されることになる。 Wiki に情報がまとめられているが、詳細はulib/FStar.Tactics.*.fstを読むと分かる。

open FStar.Tacticsしておく。

##仮定で項書換えを行う

ゴールを予めA ==> Bという形にしておき、 let h : binder = implies_intro () inとして仮定hを入手してからrewrite hとする。ゴールを書き換えない方法は良くわからない。poseがterm -> binderの関数だが、うまく使えない。

##現在のゴールを表示する

dump ()タクティックを使う。

##簡約して正しいことを証明する

norm [...]を使う。引数として簡約手法を表すdeltaやzetaをリストで渡す。使えるものはFStar.Tactics.Builtins.fstやFStar.Pervasives.fstに書いてある。

一部の関数だけを簡約する場合はdelta_onlyが使える。再帰関数をこれで簡約する場合はその後ろにdelta_onlyを繋げる。

matchを簡約する場合はiotaを使う。

##現在のゴールを Z3 に投げつけて解決させる

smt ()を使う。

いま明らかになっている仮定から素直な演繹で証明できるはずにもかかわらず assertが失敗する場合に、smtを単体で使う（assert (...) by (smt ())）と、独立に Z3 rlimit が指定されることになるので、うまく行く場合がある。

##ビット演算が絡む等号に関する証明を行う

bv_tacが使える。実用的にはBVモジュールに定義されているbv64_tacが使える。これはUInt64用のため、それ以外に適用する場合（例えばUInt8）はBV.fstをコピーして、中の64を8に書き換えるとbv8_tacなどが使えるようになる。 

val lem (c:UInt8.t) : Lemma
  (ensures (
     let c = c `UInt8.logand` 0xfcuy in
     (c `UInt8.logand` 0x03uy) = 0uy /\ (c `UInt8.logand` 2uy = 0uy)
  ))
let lem c =
  let c = c `UInt8.logand` 0xfcuy in
  assert (c `UInt8.logand` 0x03uy == 0uy) by bv8_tac ();
  assert (c `UInt8.logand` 2uy == 0uy) by bv8_tac ();
  ()

#その他

##リストに対する invariant を再帰関数を使わずに書く

例えばリストを受け取る以下のような関数があったとして 

let f (l:list int) : int = ...

l の中身が 2 以上であることを保証したいときは、再帰関数を使って 

let rec pre inv (l:list int) : Type0 =
  match l with
  | [] -> True
  | x :: xs -> x >= 2 /\ pre xs

let f (l:list int) : Pure int (requires (inv l)) (ensures (fun _ -> True)) = ...

と書く方法もあるが、そんなことせずに素直に 

type int_le_2 = i:int{i >= 2}

let f (l:list int_le_2) : Type0 = ...

と書けばよい。

##通るはずの tuple の subtype check に失敗する

例えば次のようなコードが検証を通らない 

let hogehoge (n:nat * int) : int * int = n

次のように書き換えると通る 

let hogehoge (n:nat * int) : int * int = (fst n, snd n)

##OCaml のコードを漸進的に検証する

この場合、元々ある OCaml ファイル（例えばfoo.ml）の一部が検証されていて、一部は検証されていないという状況になる。これをうまくまとめてビルドするためには、モジュールの循環参照を避けるために複数ファイルに分ける必要がある。

以下にベストプラクティスをまとめる。気付き次第追記。 

include Foo_Common
module O = Foo_OCaml
module F = Foo_FStar

let func_not_verified = O.func_not_verified
let func_verified = F.func_verified

これほど細かくファイルを分ける必要がない場合や、逆にこの分割では解決できない場合もあるので、コードに応じて柔軟に対応する。

##STATEとTotの関数を組み合わせて使う

Totエフェクトの関数呼び出しの引数においてSTATEエフェクトの関数呼び出しの結果を使うとエラーが出る。このようなときは一度呼び出し結果をletで束縛すればよい。 

(* ill-formed *)
pure_func (stateful_func arg)
(* well-formed *)
let r = stateful_func arg in
pure_func r

##コード抽出ができるように FStar をビルドする

F*はmasterならなんでもよい。検証だけなら Docker Hub からdocker pull fstarlang/fstarで落とすのが楽。ただしコード抽出をする場合はsatos さんのこのパッチを取り込む必要がある。おすすめは F*の GitHub repo をgit cloneしてきて、このパッチを適用してcommitして、その後でopam install /path/to/fstar/repoしてローカルインストールすること。

Z3 は別途引っ張ってくる必要がある。F*開発者がテストしているバイナリを取ってきて、中身のbin/z3を~/.local/bin/にでも放り込むのが早い。

##==>と/\の演算子優先順位

/\の方が強いので 

A /\ B /\ C ==> D

は 

(A /\ B /\ C) ==> D

と結合する。

##z3rlimit=0 は無制限

ヘルプには書いていないように見えるが、例えばZ3 のソースコードをみると書いてある。

##OCaml コードを FStar コードに移植する

例えばa.mlというファイルを FStar に移植するときには次のようにする。

またa.mlから呼び出されている OCaml コードについてはインタフェースファイルを用意する必要がある。例えばb.mlを呼び出している場合は次のようにする。

a_fstar.fstからはB_fstarを用いる。必要なものは全てこのモジュールにincludeされている。

##抽出した OCaml コードの最適化

OCaml コードを FStar に移植し、コード抽出によって検証された OCaml コードを得る場合には、元々の OCaml コードとほぼ等価なコードを得ることが多い。そのため、検証による性能劣化は起こりにくい。しかし、場合によっては、 FStar コンパイラが挟むラッパーコードやその他要因によって、速度が遅くなる場合がある。

速度が遅くなった場合に、その原因を探るにはプロファイラを使うのが良い。 OCaml コンパイラはバージョン 4.09.1 から gprof のサポートを落としてしまったため、代わりにperfコマンドを用いる（参考）。 

## 実際にプログラムを実行して、プロファイルを取る
$ perf record --call-graph=dwarf -- ./your-program.exe arguments
## プロファイルの結果を見る
$ perf report

環境によってはsudoを前置する必要があるかもしれない。

FStar.UInt8.uint_to_tなどの、FStar における machine integer を OCaml の integer に変換する関数は、大量に呼び出すと抽出後コードの速度低下を招く。これらの関数は、例えば FStar 中で0uyのように machine integer のリテラルを用いると、コード抽出後の OCaml コードに挿入されるため問題になる。これを防ぐためには、トップレベルで次のように使用するリテラルを定義しておき、関数内部ではこれを用いれば良い。 

let uint8_255 = 255uy (* トップレベルで定義する *)
(* 以降では255uyの代わりにuint8_255を用いる *)

HyperStack.ST.getもまた、大量に呼び出すと抽出後コードの速度低下を招くため、注意が必要である。

##exists x の x を取り出す

Zulip での解答によると、できない。 Z3 は古典論理で動くのと、そういうふうに FStar が設計されていないためと書いてある。

##依存するファイルを全て検証する方法

Wiki には--verify_allを使えと書いてあるが、 このオプションは問題が多かったために消えた。代わりに--dep makeオプションでMakefileを作り、これを使う。

ちなみに--dep graphを使うとモジュール間の依存関係をグラフで見ることができる。使うときは次のようにするとキレイなグラフになる。 

$ dot -Tpng -odep.png <(cat dep.graph | grep -v fstar_ | grep -v prims)

##STATE effect で停止性を示す

STATE effect では停止性が要求されない（発散するような関数が書ける）が、これは本来STATE effect とは関係のない話で、歴史的な理由らしい。停止性を要求するSTATE effect は一応 FStar の examples ディレクトリにあるが、問題が多く使わないほうが良さそう。

##検証でのみ使用する引数を作る

Ghost.erasedが使える。例えば検証でのみ使うfuel:natという引数を持つ関数を作る場合は次のようにする。 

let hoge (fuel:Ghost.erased nat) = ...

FStar.Ghost内で適切にGhost.hideとGhost.revealのSMTPatが定義されているため、この場合のfuelは通常のnatと同じように使える。ただし抽出結果のコードに現れるような使い方はできない。おそらくこれは「GHOST effect の部分でのみ使える」というのと同値だが確証がない。要調査。

Ghost.erased Xはコード抽出するとunit型になるため、 hogeに余計に()を渡すグルーコードは必要になる。

##複数ファイルからコード抽出する方法

単にfstar.exe --codegen OCaml a.fst b.fstのようにしてもよいが、この手法では依存関係にある全てのファイルからコード抽出されてしまい、 OCaml でのビルドがうまくいかない場合がある。

examples/sample_project/Makefileを参考にして--extract_moduleオプションを使うこともできるが、 fstar.exeによるとこのオプションは非推奨のようだ。 Wikiにかかれているオプションも古い。代わりに--extractオプションを使って次のように書けばよい。 

fstar.exe --codegen OCaml --extract "+A" a.fst
fstar.exe --codegen OCaml --extract "+B" b.fst

二つをまとめて次のようにも書ける。 

fstar.exe --codegen OCaml --extract "+A +B" a.fst b.fst

ただしこの場合 Z3 に提示される情報が上のものと変わり、必要な Z3 rlimit が増える場合がある。

##UInt32.tをInt32.tに変換・逆変換したい

Int.Cast.uint32_of_int32とInt.Cast.int32_of_uint32が使えるが、これらはn = Int.Cast.uint32_of_int32 (Int.Cast.int32_of_uint32 n)が（あるいはその逆が）示せない。これらを示す必要がある場合はInt.from_uintとInt.to_uintを使って次のようにすればよい。 

let int32_of_uint32 (ui:UInt32.t) : Tot Int32.t =
  Int32.int_to_t (Int.from_uint (UInt32.v ui))

let uint32_of_int32 (i:Int32.t) : Tot UInt32.t =
  UInt32.uint_to_t (Int.to_uint (Int32.v i))

let int32_of_uint32_of_int32 (i:Int32.t) : Lemma
  (ensures (int32_of_uint32 (uint32_of_int32 i) = i))
  [SMTPat (int32_of_uint32 (uint32_of_int32 i) = i)]
= ()

let uint32_of_int32_of_uint32 (ui:UInt32.t) : Lemma
  (ensures (uint32_of_int32 (int32_of_uint32 ui) = ui))
  [SMTPat (uint32_of_int32 (int32_of_uint32 ui) = ui)]
= ()

##外部モジュールに存在するはずの関数が参照できない

そのモジュールがそのファイルで初めて出てくる場合、読み込まれていないので対話的には見えない場合がある。その場合（fstar-mode.el ならC-C C-Rなどして）ファイルを再読込すると見える。

##UInt32.tを little endian でエンコード・デコードしたい

普通の（C や ML の）プログラムにおいて 32bit 整数値を little endian でエンコード・デコードする場合、シフトや論理和・論理積といったビット演算を多用するが、これらは FStar と相性が悪く、例えばエンコードとデコードの結果が一致するなどを証明するのは一筋縄でいかない。基本的にビット演算は避けて、代わりに加減乗除を使うほうがよい。

実際に加減乗除で同様のことを行っている例としてexamplesディレクトリの Crypto.Symmetric.Bytesがある。ファイル単体でコピーしてくると後半は動かないが、上述のことをしたいだけであれば後半をコメントアウトすれば使える。 Crypto.Symmetric.Bytes.little_bytesなどを参照のこと。

##fuelとifuelとz3rlimitの違い

fstar.exe --helpより（順番は適宜入れ替えた）： 

  --initial_fuel non-negative integer  Number of unrolling of recursive functions to try initially (default 2)
  --initial_ifuel non-negative integer  Number of unrolling of inductive datatypes to try at first (default 1)
  --max_fuel non-negative integer  Number of unrolling of recursive functions to try at most (default 8)
  --max_ifuel non-negative integer  Number of unrolling of inductive datatypes to try at most (default 2)
  --min_fuel non-negative integer  Minimum number of unrolling of recursive functions to try (default 1)
  --fuel non-negative integer or pair of non-negative integers  Set initial_fuel and max_fuel at once
  --ifuel non-negative integer or pair of non-negative integers  Set initial_ifuel and max_ifuel at once
  --z3rlimit positive_integer  Set the Z3 per-query resource limit (default 5 units, taking roughtly 5s)

基本的にfuelとifuelは証明の一部と思ったほうが良い。適切な値を 1 単位で指定する。一方でz3rlimitは Z3 の挙動によって変わるので、大雑把に大きめの値にしておく。ファイル全体として--fuel 0 --ifuel 0 --z3rlimit 0をデフォルトにしておき、必要に応じて各々を調整するのがベター。

##ある関数fの中でのみ、ある補題lのSMTPatを有効にする

FIXME: もっと直接的な方法を見つける。多分タクティックとか使えばできそう

関数f本体の中でlと全く同じ補題l'を定義し、それにSMTPatをつける。 l'の関数本体はlの呼び出しのみで良い。

##tuple を返す関数の検証で不安定になる

tuple のままで検証する。分解すると証明が不安定になりがち。

例えば 

let f x : Ghost (requires (...)) (ensures fun r -> let a, b, c = r in p a b c) =
  ...
  assert (let a, b, c = r in p a b c);
  r

よりも 

let f x : Ghost (requires (...)) (ensures (fun r -> p r)) =
  ...
  assert (p r);
  r

のほうがよい。

##ある命題だけコマンドラインから検証させる

--admit_except (HogeModule.piyo_func, 2)オプションが使える。

##Z3 に投げられている SMT2 ファイルを吐かせる

Wikiを参考に--log_queriesオプションを指定する。 

fstar.exe --query_stats --z3refresh --log_queries --print_z3_statistics --admit_except (HogeModule.piyo_func, 2) fuga.fst

##見かけ同じ型が異なるとエラーが出る

--print_universesと--print_implicitsを使うと型の詳細が分かる。

##GTot Type0を返す関数のコード抽出をやめる

Type0を返す場合inline_for_extractionをつけても効果はない。

Ghost.erased・Ghost.hideが使える。Ghost.hideは型Tの式を受け取りGhost.erased Tを返す。

Type0を返すような関数をGhost.erasedとGhost.hideのどちらで包むべきかは良くわからない。型上はどちらでも包めるので、検証がうまく行く方を使うことになる。

##Emacs で実行するときとターミナルから実行するときとで必要なz3rlimitが異なる

実は Emacs から対話的に実行するときには FStar に--ideオプションが渡されていて、これが渡されるか否かで Z3 へ発行されるクエリが異なるようだ。 GitHub に Issue はたっているが解決していない。

別の要因として、Emacs 側では--use_hintsをつけていて、コマンドライン側ではつけていないと、ヒントのせいで Emacs 側では通るということが起きうる。

##variant のマッチ

原則match-withを使って variant にマッチさせる。ifなども使えるように見えるが、検証がうまくいかない場合がある。とくに OCaml から書き換えるときに見逃しがちなので注意が必要。

##Totの引数と戻り値に事前条件・事後条件を書きたい

Pureを使う。 

val f : n:int -> Pure int
  (requires (n > 0))
  (ensures (fun r -> r > n))
let f n = n + n

GTotの場合はGhostを使う。

ただしエラーが読みにくくなる（subtype check failedになる）。

##SMTPatに複数の条件を並べる

連言でつなぎたい場合はセミコロンで区切って書く： 

[SMTPat (hoge); SMTPat (piyo)]

選言でつなぎたい場合はSMTPatOrを使う： 

[SMTPatOr [
  [SMTPat (hoge)];
  [SMTPat (piyo)]
]]

##assert を補題っぽく使う

assertするとそれが Z3 に渡されるので、証明の文脈が増える。これを使って簡易的な補題とできる。例えば何もなしではforallがうまくトリガーされない場合に、 assert を用いて明示的に真の命題を書くことでトリガーできる。あるいは SMTPat がうまく動かないときに、パターンにマッチするように assert を書くことで証明を通すことができる。

##Z3 にunknownと言われたとき

基本的に Z3 がunknownといった時はなんの情報もないことを念頭に、うまくいったものを書き連ねる。

##FStar にInternal error: unexpected unresolved (universe) uvar in deep_compressと言われた時

FStar の内部エラーで、基本的には FStar のバグに見える。解消にうまくいったものを書き連ねる。上にあるもののほうが確度が高い。

GitHub に Issue がたっていた。最小再現コードがあるのがえらすぎる。そのうち改善されそう。

##@@はTot

なので左側にくる関数がSTATE effect などをもてない。

##篩型の中に書けるのはPureやGhostのみ

STATEはかけないっぽい。正確な範囲は要検証。

##Heap.equalとmodifies_noneの関係

FIXME: 間違っていそうなので要調査

Heap.equalは外延的等価性を確認する。つまり操作の結果おなじアドレスに同じ値が入っていればいい。 modifies_noneはヒープに手を加えていないことを確認する。したがって前者が後者を含意する。 

val hogehogehoge : h:Heap.heap → h':Heap.heap → Lemma
  (requires (Heap.equal h h'))
  (ensures (modifies_none h h'))
let hogehogehoge h h' = ()

##fuel/ifuel/z3rlimit が足りない

##GTotとTot

GTotはコード抽出されない GHOST の Tot。

Tot は GTot の subtype っぽい？　 GTot が要求されているところに Tot を渡すことはできるが、その逆はできない。つまり次のようなコードは通らない。 

assume val hogehoge : f:(nat -> Tot nat) -> nat

let f (m:nat) : GTot nat = m

let piyopiyo x = hogehoge f

##PUREな関数以外は再帰が止まる必要がない

型のところに現れることがないため。

##StringとChar

どちらも（余計なことに）Unicode に対応しているので、OCaml の意味論と異なる。つまりChar.charは 4 バイトくらい持つ可能性があるので整数値に変換すると符号なし 32bit になり、 String.lengthは保持する文字列のバイト数と一般には一致しない。

詳細はWikiを参照。

String.makeがコード抽出するとちゃんと動かないのもこのあたりが原因っぽい。要調査。

##existsを消去する

exists (x:a). p xかつforall (x:a{p x}). goalならばgoalを結論できる、というのを FStar.Classical.exists_elim経由で行う。examples/crypto/OPLSS.Log.fstなどに利用例がある。 

let exists_x : squash (exists (x:a). p x) = () in
FStar.Classical.exists_elim
  goal
  exists_x
  (fun x -> p_x_implies_goal x)

##forall x. p x を証明する

FStar.Classical.forall_introを使用する方法とSMTPatを使用する方法の二種類があり、どちらも一長一短ある。forall_introのコメントに詳細な説明がある。

SMTPatを使用する場合は、p xを証明するLemmaにSMTPatでp xを記述する。このときにLemmaをうまくネストするとSMTPatの効力がスコープ外に出ないので便利である参考。 Lemmaに余計な注文がつかない（requiresが使えないなど）というメリットが大きいので、基本的にはこの手法を使うべき。ただし Z3 の探索時間が伸びることと、 SMTPatに記述できないパターンが存在する（等号やパターンマッチなど）ことがデメリットである。

forall_introを使用する場合、p xを証明するLemmaにforall_introを適用することで目的の命題を得る。ここで適用できるLemmaにはいくつか条件があり、その最たるものが requires節が使用できないことである。requiresを必要とする補題を証明したい場合は、 FStar.Classical.move_requiresを使用する。以下はリストの等価性に関する補題lem_list_equalityを forall_introとmove_requiresを使用して証明する例。この場合、SMTPatが使えない。 

val lem_list_equality' : #a:eqtype -> l1:list a -> l2:list a -> j:nat -> Lemma
  (requires (
     List.Tot.Base.length l1 = List.Tot.Base.length l2 /\
     List.Tot.Base.length l1 > 0 /\ j < List.Tot.Base.length l1 - 1 /\
     (forall (i:nat{i < List.Tot.Base.length l1}). List.Tot.Base.index l1 i =
                                             List.Tot.Base.index l2 i)
  ))
  (ensures (
     List.Tot.Base.length l1 = List.Tot.Base.length l2 /\
     List.Tot.Base.length l1 > 0 /\ j < List.Tot.Base.length l1 - 1 /\ (
     match l1, l2 with
     | _ :: t1, _ :: t2 ->
         List.Tot.Base.index t1 j = List.Tot.Base.index t2 j
     | _ -> false)
  ))
let lem_list_equality' #a l1 l2 j =
  match l1, l2 with
  | h1 :: t1, h2 :: t2 ->
      calc (==) {
        List.Tot.Base.index t1 j;
        == {}
        List.Tot.Base.index (h1 :: t1) (j + 1);
        == {}
        List.Tot.Base.index l1 (j + 1);
        == {}
        List.Tot.Base.index l2 (j + 1);
        == {}
        List.Tot.Base.index (h2 :: t2) (j + 1);
        == {}
        List.Tot.Base.index t2 j;
      }
  | _ -> ()

val lem_list_equality'' : #a:eqtype -> l1:list a -> l2:list a -> j:nat -> Lemma
  (ensures
    (
     List.Tot.Base.length l1 = List.Tot.Base.length l2 /\
     List.Tot.Base.length l1 > 0 /\ j < List.Tot.Base.length l1 - 1 /\
     (forall (i:nat{i < List.Tot.Base.length l1}). List.Tot.Base.index l1 i =
                                             List.Tot.Base.index l2 i)
    ) ==> (
     List.Tot.Base.length l1 = List.Tot.Base.length l2 /\
     List.Tot.Base.length l1 > 0 /\ j < List.Tot.Base.length l1 - 1 /\ (
     match l1, l2 with
     | _ :: t1, _ :: t2 ->
         List.Tot.Base.index t1 j = List.Tot.Base.index t2 j
     | _ -> false)
    )
  )
let lem_list_equality'' #a l1 l2 j =
  FStar.Classical.move_requires_3 lem_list_equality' l1 l2 j

val lem_list_equality : #a:eqtype -> l1:list a -> l2:list a -> Lemma
  (requires (List.Tot.Base.length l1 = List.Tot.Base.length l2 /\
            (forall (i:nat{i < List.Tot.Base.length l1}). List.Tot.Base.index l1 i =
                                                   List.Tot.Base.index l2 i)
  ))
  (ensures (l1 = l2))
let rec lem_list_equality #a l1 l2 =
  match l1, l2 with
  | [], [] -> ()
  | h1 :: t1, h2 :: t2 ->
      calc (==) {
        h1;
        == {}
        List.Tot.Base.index l1 0;
        == {}
        List.Tot.Base.index l2 0;
        == {}
        h2;
      };
      calc (==) {
        l1;
        == {}
        h1 :: t1;
        == {}
        h2 :: t1;
        == {FStar.Classical.forall_intro (lem_list_equality'' l1 l2); lem_list_equality t1 t2}
        h2 :: t2;
        == {}
        l2;
      }

要するにforall x. p xを証明したい場合、f : x:a -> Lemma (p x)を書いた上で： 

FStar.Classical.forall_intro (FStar.Classical.move_requires f);

と書くと、だいたいうまく行く。うまく行かないときもある。

参考。

##@の結合性の証明

つまり(l1 @ l2) @ l3 == l1 @ (l2 @ l3)の証明。 

val list_concat_assoc (l1 l2 l3:list 'a) : Lemma ((l1 @ l2) @ l3 == l1 @ (l2 @ l3))
##push-options "--fuel 1 --ifuel 1"
let rec list_concat_assoc l1 l2 l3 =
  match l1 with
  | [] -> ()
  | hd1 :: tl1 ->
      calc (==) {
        (l1 @ l2) @ l3;
        == {}
        ((hd1 :: tl1) @ l2) @ l3;
        == {}
        (hd1 :: (tl1 @ l2)) @ l3;
        == {}
        hd1 :: ((tl1 @ l2) @ l3);
        == {list_concat_assoc tl1 l2 l3}
        hd1 :: (tl1 @ (l2 @ l3));
        == {}
        (hd1 :: tl1) @ (l2 @ l3);
        == {}
        l1 @ (l2 @ l3);
      }
##pop-options

##Set.as_setを使った検証が通らない

（なぜか分からないが）Set.as_setはSet.as_set'のnormalize_termとして定義されており、定義の展開状況によっては通るはずの検証が通らない場合がある。 --fuel 1をつけると通る（ことがある）。

##(requires (p x))(ensures (q x))の補題lemをp x ==> q xにして使う

(FStar.Classical.move_requires lem) x;とする。

##P \/ Q, P ==> R, Q ==> SからR \/ Sを示したい

P ==> Rをlem1、Q ==> Sをlem2とすると 

FStar.Classical.move_requires lem1;
FStar.Classical.move_requires lem2;

と書く。

FIXME: FStar.Classical.or_elimというそのものな補題があるが、これの使い方はよくわからない。おそらく 

FStar.Classical.or_elim #(P) #(Q) #(fun () -> R \/ S) lem1 lem2

と書けばよいのだが、手元では意図通り動かなかった。ちなみに上のFStar.Classical.move_requiresに直す手法はFstar.Classical.or_elimの証明で使われている。

##テンプレート 

// Pureを使えばrequiresとensuresが書ける。引数に篩型として書いてもいいけど、読みにくくなる。
val f (n:int) : Pure int
  (requires (n > 0))
  (ensures (fun r -> r > n))
let f n = n + n

// ST
val f (n:ref int) : ST int
  (requires (fun h -> sel h n > 0))
  (ensures (fun h r h' -> r = sel h' n /\ r > sel h n))
let f n = n := !n + !n