Skip to content

Instantly share code, notes, and snippets.

@satos---jp

satos---jp/tips.md

Last active Oct 18, 2020
Embed
What would you like to do?
FStar Tips

https://github.com/satos---jp/fstar-tips で書き直し中

For fstar users

入門

オプションについて

  • #set-options#reset-options で、型検査のやりかたを一時的に変更できる
  • --lax を付けると、refinement部分の型検査を飛ばしてくれるので高速にできる
    • #set-options "--lax" #reset-options --lax を用いると一部分だけ型検査ができる
  • --cache_checked_modules を付けて型検査しておくと、.cacheが生成されて、そのファイルをopenするコードが高速に検査できる
  • --detail_errors を付けると、error箇所を全部出してくれるのでえらい
    • パターンマッチなどで、どのパターンで落ちてどれでは落ちてないかが一斉にわかる
  • ときたま、--detail_errors をつけても詳しいエラー箇所が判明しない場合がある。そのようなときは、--z3rlimit [自然数] をつけて検証時間を伸ばすとよいことがある

Extractする際の注意事項

  • intZ.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 に変換される.

Tips

  • 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) 型へのダウンキャストは自動では行ってくれないので、型注釈を付けてやる必要がある。

For OCaml users

今後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になる
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.