https://github.com/satos---jp/fstar-tips で書き直し中
- まずは https://www.fstar-lang.org/tutorial/ を読む。(6章あたりまで読むと、ある程度証明付きで書くことができるようになる)
- 困った時は https://github.com/FStarLang/FStar/wiki を調べる
#set-optionsと#reset-optionsで、型検査のやりかたを一時的に変更できる--laxを付けると、refinement部分の型検査を飛ばしてくれるので高速にできる#set-options "--lax"#reset-options --laxを用いると一部分だけ型検査ができる
--cache_checked_modulesを付けて型検査しておくと、.cacheが生成されて、そのファイルをopenするコードが高速に検査できる--detail_errorsを付けると、error箇所を全部出してくれるのでえらい- パターンマッチなどで、どのパターンで落ちてどれでは落ちてないかが一斉にわかる
- ときたま、
--detail_errorsをつけても詳しいエラー箇所が判明しない場合がある。そのようなときは、--z3rlimit [自然数]をつけて検証時間を伸ばすとよいことがある
intはZ.tに変換されるtype t = | A of int * intは| A of (Prims.int * Prims.int)に，type t = | A : int -> int -> tは| A of Prims.int * Prims.intに変換される．
-
Lemma (P ==> Q)よりもLemma (requires P) (ensures (fun r -> Q))のほうがだいたいよい- 右の形で型宣言されたLemmaを使うと、Pを満たしていないところで使おうとした場合にエラーを出してくれるが、左では出ない。
-
型注釈を書けば書くほど通りやすくなる
- let宣言には
let f (x1:型注釈) ... (xn:型注釈) : fの型注釈 = ...と書くと注釈できる - funなどには、
(fun x -> ...) <: (型注釈)など<:を用いて型注釈を書く必要があることがある - キャストは必要で、たとえば
(option (v:t{prop v}))と(w:(option t){match w with Some v -> prop v | _ -> True})は自動キャストはしてくれない。- ほかにも、
(list (v:t{p v}))型から(list t)型へのダウンキャストは自動では行ってくれないので、型注釈を付けてやる必要がある。
- ほかにも、
- let宣言には
今後FStarに移植されるかもしれないOCamlコードを書くひと向けの話
let f x =
let rec aux y =
みたいな感じでinner-let-recを書くとfstarでは
(Warning 242) Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types と言われたりするので避けておくとよい
-
実際、たまにinnner let recを外に出すと検証が通ったりすることがある
-
.fstiでの定義順と.fstでの定義順を合わせる必要があるので、 .mli での定義順と .ml での定義順を合わせてほしい
-
as pattern はない
-
when はあるが、使うのを避けるべき
- ((Error 236) When clauses are not yet supported in --verify mode; they will be some day) と言われる
-
polymorphic variant はない
-
type t = A | Bみたいな型宣言をする際に、Aの前に|が要る -
演算子の優先順位があやしい
v >>= function | ...が、functionにかっこをつけないとerrorになる