気づいたことを雑にまとめる。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。

## `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を使えばできる、と書きたかったのだが、いま試したら補題無しで動いた。要調査。

# `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

FStar Tips

2020/09/15

(Last edited on 2021/01/11)