気づいたことを雑にまとめる。Markdownで"F*“とかくとバックスラッシュが必要でダルいので、 適宜"FStar"で代用する。
# 疑問
- 関数の内部でheapって参照できへんの
- 別のfstを参照する場合に、参照先の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。
##
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.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 = ()
# その他
##
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に分ける。
##
@@は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が足りない
おおよそ各々100くらいにしておけば足りる。以下はそれで足りなかったときの対処方法：
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;
}
