FStar Tips

2020/09/15

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

# 疑問

# お役立ちサイト

# HyperStack/HyperHeapに関するもの

適宜以下を仮定。

module HS = FStar.HyperStack
module HSST = FStar.HyperStack.ST

## FStar.HyperHeapがない

いつの間にか消えた。おそらくHeapのモデルが変わったとき だと推測されるが、定かではない。 代わりにFStar.Monotonic.HyperHeapが生えたが、これは直接使うことを意図されていないとコメントに書いてある。 代わりにFStar.HyperStackopenする。

このあたり、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.modifiesHS.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.containsHS.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 = ()

# その他

## SMTPatに複数の条件を並べる

連言でつなぎたい場合はセミコロンで区切って書く:

[SMTPat (hoge); SMTPat (piyo)]

選言でつなぎたい場合はSMTPatOrを使う:

[SMTPatOr [
  [SMTPat (hoge)];
  [SMTPat (piyo)]
]]

## assertで簡易補題を作る

assertするとそれがZ3に渡されるので、証明の文脈が増える。これを使って簡易的な補題とできる。 例えば何もなしではforallがうまくトリガーされない場合に、 assertを用いて明示的に真の命題を書くことでトリガーできる。

## Z3にunknownと言われたとき

基本的にZ3がunknownといった時はなんの情報もないことを念頭に、 うまくいったものを書き連ねる。

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

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

## @@Tot

なので左側にくる関数がSTATE effectなどをもてない。

## 篩型の中に書けるのはPureGhostのみ

STATEはかけないっぽい。正確な範囲は要検証。

## Heap.equalmodifies_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が足りない

おおよそ各々100くらいにしておけば足りる。以下はそれで足りなかったときの対処方法:

## GTotTot

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な関数以外は再帰が止まる必要がない

型のところに現れることがないため。

## StringChar

どちらも(余計なことに)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を証明するLemmaSMTPatp xを記述する。 Lemmaに余計な注文がつかない(requiresが使えないなど)というメリットが大きいので、 基本的にはこの手法を使うべき。ただしZ3の探索時間が伸びることと、 SMTPatに記述できないパターンが存在する(等号やパターンマッチなど)ことがデメリットである。

forall_introを使用する場合、p xを証明するLemmaforall_introを適用することで 目的の命題を得る。ここで適用できるLemmaにはいくつか条件があり、その最たるものが requires節が使用できないことである。requiresを必要とする補題を証明したい場合は、 FStar.Classical.move_requiresを使用する。 以下はリストの等価性に関する補題lem_list_equalityforall_intromove_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;
      }
このエントリーをはてなブックマークに追加