気づいたことを雑にまとめる。Markdown で"F*“とかくとバックスラッシュが必要でダルいので、 適宜"FStar"で代用する。
# 疑問
- 別の fst を参照する場合に、参照先の fst が検証できなくても参照元で使えるのなんとかならんの
- 検証できない場合は落ちてる気もする
- fsti をまともに検証してくれない
- 仮定なのでそれはそうと言ってしまえばそれまでだが
val
に書いてある内容だけで矛盾する場合でも、エラーをださずに良くわからない検証をして結果死ぬことが多い。
- 仮定なのでそれはそうと言ってしまえばそれまでだが
delta_only
が謎- 再帰関数が定義できない?
- 定義が見えない(fsti/fst で分けて定義されている)場合には展開できない?
# お役立ちサイト
- FStar tutorial
- 必要な情報のほとんどすべてがここで揃う。typo も多いし行間が空きまくっているが、貴重な情報源。
- 後半情報が古い。たとえば HyperHeap の API は現在と大きく異なる。
- FStar wiki
- 残りの情報のほとんどすべてがここで揃う。行間が空きまくっているが、貴重な情報源。
- 情報が古い項目がある
- satos—jp さんの FStar Tips
# 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
があるので、通常意識しなくてもすむ。
# 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 ();
()
# その他
## 複数ファイルを検証する方法
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)
##
ある関数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 を用いて明示的に真の命題を書くことでトリガーできる。
##
Z3 にunknown
と言われたとき
基本的に Z3 がunknown
といった時はなんの情報もないことを念頭に、
うまくいったものを書き連ねる。
fuel
・ifuel
・z3rlimit
を増やす。- 驚くほどこれでうまく行く。
- 再帰関数の場合は
decreases
を明記する。 - warning を潰す
##
FStar にInternal error: unexpected unresolved (universe) uvar in deep_compress
と言われた時
FStar の内部エラーで、基本的には FStar のバグに見える。解消にうまくいったものを書き連ねる。 上にあるもののほうが確度が高い。
- 再帰関数を定義するときに
let
に全ての制約を書くと起こりやすく、 これをval
とlet
に分けると解消することが多い。 - 複数のファイルにまたがって依存関係がある場合、それらを全て
fstar.exe
に渡す。 - 再帰関数の
(decreases ...)
を消す。
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 が足りない
z3rlimit
を増やしたいところを#push-options "--z3rlimit 100"
と#pop-options
で囲む。UInt8.shift_left
が入っている関数op_Multiply
で代用。
##
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
に余計な注文がつかない(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;
}
参考。
## テンプレート
// 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