FStar Tips

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

# 疑問

別のfstを参照する場合に、参照先のfstが検証できなくても参照元で使えるのなんとかならんの
- 検証できない場合は落ちてる気もする
fstiをまともに検証してくれない
- 仮定なのでそれはそうと言ってしまえばそれまでだがvalに書いてある内容だけで矛盾する場合でも、エラーをださずに良くわからない検証をして結果死ぬことが多い。

# お役立ちサイト

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

# Tactics

## タクティックとは

Meta-F*という論文でFStarにCoqのようなtacticsが導入された。 assert (...) by (...) という形で証明に使える。 Wikiに情報がまとめられているが、詳細はulib/FStar.Tactics.*.fstを読むと分かる。

open FStar.Tacticsしておく。

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

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

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

# その他

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

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

## 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を明記する。

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

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

再帰関数の(decreases ...)を消す。
複数のファイルにまたがって依存関係がある場合、それらを全てfstar.exeに渡す。
letに全ての制約を書いている場合、これをvalとletに分ける。

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

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

2020/09/15