F* における検証されたプログラミング
チュートリアル
The F* Team
MSR, MSR-Inria, Inria

(訳注: この日本語マニュアルは Verified programming in F* の翻訳です。 翻訳に参加するには 翻訳リポジトリ を参照してください。)

1. イントロダクション

F* は検証指向のプログラミング言語で、Microsoft Research, MSR-Inria, Inria によって開発されています。 それは、型付で正格な関数型プログラミング言語である ML 族の言語の伝統を受け継いでいます。 けれども、その型システムは ML のそれよりも著しく豊かで、表明されて半自動的に検査される関数的な正確さの仕様を許します。 このチュートリアルは F* における検証されたプログラミングの最初の体験を提供します。 論文とテクニカルレポートを含む F* に関するより多くの情報が F* ウェブサイト で見つかります。

もし ML 族の関数型プログラミング言語 (例: OCaml, F#, Standard ML) や Haskell に馴染みがあれば、それは役立つでしょうもし馴染みがなくても、この文書で基本的な概念を簡単に説明します。より多くのバックグラウンドを知りたい場合には、Web 上に無料の有用な文書が多数あります。例えば、TryF#, F# for fun and profit, Introduction to Caml, Real World OCaml などです。

F* を試したりこのチュートリアルの検証の練習問題を解く最も簡単な方法は オンライン F* エディタ を使ってウェブブラウザ上で直接動かすことです。 それぞの練習問題の本体中にある “エディタに読み込む” リンクをクリックすることで、それぞれの練習問題に必要なボイラープレートコードをオンラインエディタに読み込むことができます。 それぞれの練習問題でのあなた進捗はウェブブラウザのローカルストレージに保存されるので、(例えばウェブブラウザがクラッシュなどしても) 後であなたのコードを復帰できます。 (訳注: この文書では上記の オンライン F* エディタ との連携は使えません。“エディタに読み込む” リンクをクリックすると、相当するソースコードをダウンロードできます。)

また F* をローカルのマシンにインストールしてこの練習問題を解くこともできます。 F* はオープンソースでクロスプラットフォームです。 Windows, Linux, MacOS X 向けの バイナリパッケージ をダウンロードでき、またこれらの 手順 を用いて github 上のソースコード から F* をコンパイルできます。

お好きなテキストエディタを使って F* コードを編集できます。 そして Emacs, Atom, Vim には F* を特別にサポートする拡張があり、シンタックスハイライトやインタラクティブな開発ができます。 エディタのサポート の詳細は F* wiki を参照してください。

デフォルトでは F* は入力されたコードを検証するだけで、それを実行しません。 F* コードを実行するためには、OCaml や F# にエクストラクトし、OCaml や F# コンパイラを使ってコンパイルする必要があります。 F* コード実行 の詳細は F* wiki を参照してください。

1.1. はじめての F* プログラム: アクセスコントロールの単純なモデル

ファイルに対するアクセスコントロールの単純なモデルからはじめましょう。 この中で、一般的な関数型プログラミング由来のいくつかの基本的なコンセプトと、いくつかの F* 固有の機能を見ることになるでしょう。

ファイルの単純なアクセスコントロールをモデル化したいとしましょうあるファイルは読み書き可能で、一方で他のファイルはアクセスできません。 それぞれのファイルに対する権限を表わすポリシーを作り、このポリシーに照らしてプログラムのファイルアクセスのパターンをチェックし、アクセスできないファイルが決っして間違ってアクセスされてないことを静的に保証したいのです。

このシナリオでのモデル (これは後の章でより現実的にします) は3つの簡単なステップで進展します。

  1. 単純な純粋関数を使ってポリシーを定義します。
  1. プログラムにおけるセキュリティセンシティブなプリミティブを特定し、それらをポリシーを使って保護します。
  1. プログラムの残りを書きます。ポリシーで保護されたプリミティブは決っして不適切にアクセスされないことを F* の型検査器は静的に検証することを保証されます。

1.1.1. ポリシーを定義する

F* の構文は OCaml 構文と F# の non-light 構文に基づいています。 F* プログラムは数個のモジュールで構成されます。 それぞれのモジュールはそのモジュールの名前を定義する module 宣言ではじまります。 その本体は多数の定義と任意に ‘main’ 式を含みます。

ここでは2つのモジュールがあります: 1つは FileName と呼ばれ、もう1つは (Access-Control Lists を表わす) ACLs と呼ばれます:

module FileName
  type filename = string

module ACLs
  open FileName

  (* canWrite is a function specifying whether or not a file f can be written *)
  let canWrite (f:filename) = 
    match f with 
      | "demo/tempfile" -> true
      | _ -> false

  (* canRead is also a function ... *)
  let canRead (f:filename) = 
    canWrite f               (* writeable files are also readable *)
    || f="demo/README"       (* and so is this file *)

エディタに読み込む

FileName モジュールは型シノニムを定義します: filename をモデル化するのに string を使えます。 ACLs モジュールははじめに FileName モジュールを open するので、その型シノニムは直接使えるようになります。(そうしない場合、長いフル修飾された名前: FileName.filename で呼び出す必要があります。)

その後 ACLs は2つのブール関数としてセキュリティポリシーを定義します: canWritecanRead です: canWrite 関数はその引数 fパターンマッチ式 を使って検査します: f="demo/tempfile" であったらブール true を返し、そうでなければ false を返します。 関数 canRead も同様ですファイルが書き込み可能もしくは "demo/README" ファイルであったなら、そのファイルは読み出し可能です。

1.1.2. ポリシーをファイルアクセスプリミティブと結びつける

ポリシーを強制するためには、ファイルを読み書きを実際に実装するプログラムのプリミティブにポリシーを接続する必要があります。

F* は別に実装された外部のモジュールへのインターフェイスを指定する機能を提供しています。 例えば、ファイルの入出力操作は OS によって実装されていますが、例えば .NET や OCaml のような下層のフレームワークを通じて F* プログラム中で有効にできます。 次のように、そのフレームワークによって提供された単純なインターフェイスを表現できます:

module FileIO
  open ACLs
  open FileName
  assume val read  : f:filename{canRead f}  -> string
  assume val write : f:filename{canWrite f} -> string -> unit

エディタに読み込む

ここでは、ACLs モジュールを使う FileIO と呼ばれる インターフェイス を定義しました。 より重要なことは、FileIO は2つの関数 readwrite を提供し、それらはおそらく相当するファイル操作を実装しています。

assume val 表記を使って、FileIOreadwrite 操作 (それらは です) を提供すると 宣言 しましたが、ここではそれらの値を 定義していません それらは外部のモジュールで提供されます。 assume val の使用はC言語や他のプログラミング言語の extern キーワードと良く似ています。

extern を使って値を宣言するとき、その型シグニチャも提供します。

もちろん、これらの宣言の重要な点は型シグニチャにおける canReadcanWrite の使用です。 それらによってセキュリティセンシティブな関数の型をポリシーに接続できます。

1.1.3. プログラムを書き、そのセキュリティを検証する

コード片がアクセスコントロールポリシーに従っていることをチェックするのは退屈でエラーしやすいでしょう。 たとえそれぞれのアクセスがセキュリティチェックで保護されていたとしても、どうすればそれぞれのチェックが適切であることを確認できるでしょうか? F* を使うことで、この種のコードレビューを自動化できます。

ここではいくらか単純な信頼できないクライアントコードを示します。 このコードは共通のファイル名を定義する FileIO を使い、それから複数のファイルを読み書きする staticChecking と呼ばれる関数を使います。

module UntrustedClientCode
  open FileIO
  open FileName
  let passwd  = "demo/password"
  let readme  = "demo/README"
  let tmp     = "demo/tempfile"

  let staticChecking () =
    let v1 = read tmp in
    let v2 = read readme in
    (* let v3 = read passwd in -- invalid read, fails type-checking *)
    write tmp "hello!"
    (* ; write passwd "junk" -- invalid write , fails type-checking *)

エディタに読み込む

型検査器は、この信頼できないコードがセキュリティポリシーと共にコンパイルされるされることを静的に保証します。 tmpreadme の読み出しと tmp への書き込みはポリシーで許されているので、このプログラムの型検査は成功します。 一方、password ファイルを読んだり "junk" を書き込む行のコメントを外すと、F* 型検査器は passwd ファイルがそれぞれ型 f:filename{canRead f}f:filename{canWrite f} を持たないことを訴えます。 例えば、この write のコメントを外すと、次のようなエラーメッセージが得られます:

Error ex1a-safe-read-write.fst(38,2-47,5): The following problems were found:
    Subtyping check failed; expected type f:filename{(canWrite f)};
    got type string (ex1a-safe-read-write.fst(43,17-43,23))

このチュートリアルを読み進めることで、このメッセージの意味がより理解できるようになるでしょう。 ここでは、F*canWrite passwdtrue に評価されると期待しているのに、この場合成立しないことを意味しています。

上記の staticChecking 関数は、セキュリティポリシーを指定し、ポリシーの完全で正確な調停を型検査を通じて静的に強制するのにどのように F* を使うことができるかを説明しています。 ここで、ポリシーのチェックは全て静的に行なわれる必要はなく、プログラマが追加した動的なチェックが型システムによって検討されることを説明します。 具体的には、ポリシーを調べてポリシーが許可するときだけ read を行ない、そうでなければ例外を発生させる checkedRead 関数を実装してみましょう。

  exception InvalidRead
  val checkedRead : filename -> string
  let checkedRead f =
    if ACLs.canRead f then FileIO.read f else raise InvalidRead

エディタに読み込む

checkRead 型は入力ファイル f の条件を強制していないことに注意してください。 ACLs.canRead f チェックが成功したなら、型検査器は FileIO.read f 安全であることがわかります。

練習問題 1a:
ファイル名 f と文字列 s を引数に取り、ポリシーをチェックしてファイル f が書き込み可能か確認し、書き込み可能な場合のみ sf に書き込む checkedWrite という名前の関数を書いてください。 そのファイルが書き込み可能でなかったら、checkedWrite は例外を発生させます。 checkedRead に関して事前条件はありません。

  assume val checkedWrite : filename -> string -> unit

エディタに読み込む

回答
  exception InvalidWrite
  let checkedWrite f s =
    if ACLs.canWrite f then FileIO.write f s else raise InvalidWrite

エディタに読み込む

これで、staticCheckingreadwritecheckedReadcheckedWrite で置き換えることで、passwd へのアクセスが型付けできます。

  let dynamicChecking () =
    let v1 = checkedRead tmp in
    let v2 = checkedRead readme in
    let v3 = checkedRead passwd in (* this raises exception *)
    checkedWrite tmp "hello!";
    checkedWrite passwd "junk" (* this raises exception *)

エディタに読み込む

checkedReadcheckedWrite は F* によってコンパイル時にあらかじめ行なわれたのと同じチェックを実行時に延期させ、それらのチェックが成功した場合のみその入出力アクションを行なうため、これは安全です。

2. 基本: 型と作用

全てを知らされていませんでしたが、F* 独特の機能のいくつかを最初の例で既に見てきました。 より詳細に見てみましょう。

2.1. リファインメント型

F* の1つの特徴的な機能はリファインメント型の使用です。 この機能を既に2度使いました。 例えば、型 f:filename{canRead f} は型 filenameリファインメント です。 filename 値のサブセットのみがこの型、すなわち述語 canRead を満たす型を持つので、それはリファインメントなのです。 FileIO.write の型のリファインメントも同様です。 伝統的な ML 族の言語では、このような型は表現できません。

一般に、F* におけるリファインメント型は x:t{phi(x)} の形を取ります。 このときそれは型 t のリファインメントで、その要素 x は式 phi(x) を満たします。 今のところ、phi(x) は式を評価すると得られる純粋なブールであると考えることができます。 詳細には 3.5 で、より一般化します。

2.2. 推論された型と計算のための作用

canReadcanWrite のような関数の型を書きませんでしたが、(ML 族の他の言語と同様に) F* は (その型が正しいなら) プログラムの型を推論します。 けれども、F* によって推論される型は ML で表現される型よりもより詳細です。 例えば、型推論に加えて、F* は式の 副作用 (例: 例外、状態など) も推論します。

例えば、ML では (canRead "foo.txt") は型 bool を持つと推論されます。 けれども、F* では (canRead "foo.txt" : Tot bool) と推論します。 これは canRead "foo.txt" 純粋で全域な式で、常にブールに評価されることを示しています。 ついでに言うと、型と作用 Tot t を持つと推論された式は、(コンピュータが十分なリソースを持っていれば) t で型付けされた結果に評価されることが保証されます。 そしてこの式は無限ループに入らず、プログラムの状態を読み書きせず、例外を発生せず、入出力を行なわず、その他の作用を引き起こしません。

一方、(FileIO.read "foo.txt") のような式は型と作用 ML string を持つと推論されます。 これはこの項が任意の作用 (ループ、入出力、例外発生、ヒープの変更など) を持つ可能性があり、けれどももしそれがリターンしたなら、常に文字列を返すことを意味しています。 作用の生 ML はデフォルト、つまり全ての ML プログラムの暗黙の作用を表わしています。

TotML は取りうる作用の全てではありません。 それ以外に次のような作用があります:

作用 {Tot, Dv, ST, Exn, ML} は束として配置されます。 Tot は (その他全ての作用より下位である) 下限に、ML は (その他全ての作用より上位である) 上限に配置され、STExn は関係がありません。 これは特定の作用を共なう計算が、作用の順序においてその作用より大きいその他の作用を持つと扱えることを意味しています私達はこの機能を サブ作用 と呼んでいます。

実際、F* では、独自の作用と作用の順序を構成でき、F* にそれらの作用を推論させることができますしかしそれはより高度な機能で、このチュートリアルの範囲外です。

今後は (例えば Tot が作用で int が結果の型である Tot int のような) 型と作用のペアを、単に型と呼ぶことにします。.

2.3. 関数型

F* は関数型言語で、関数は関数型が割り当てられた第一級の値です。 例えば ML では、ある整数が正であるか判別する関数には型 int -> bool が与えられます。 すなわち、この関数は整数を引数に取り、ブールを結果として生成します。 同様に、整数の最大値を計算する関数 max には型 int -> int -> int が与えられます。 すなわち、この関数は2つの整数を取り、1つの整数を生成します。 F* における関数型はより詳細で、引数と返り値の型だけでなく、関数本体の作用も捕捉します。 このように、全ての関数値は t1 -> ... -> tn -> E t のような型を持ちます。 このとき t1 .. tn は引数それぞれの型で; E は関数本体の作用; そして t はその結果の型です。 (*上級者への注意: これは作用でインデックスされた依存した関数に一般化されます。) F* では、上記の純粋関数には作用 Tot を使った型が与えられます:

val is_positive : int -> Tot bool
let is_positive i = i > 0

val max : int -> int -> Tot int
let max i1 i2 = if i1 > i2 then i1 else i2

ファイルの内容を読むような、純粋でない関数には同様に作用が与えられます:

val read : filename -> ML string

(OCaml や F# と同様に、Haskell や Coq と異なり) F*値渡し の関数型言語で、関数の引数はその関数に渡される前に、完全に評価されて値になります。 値は (直接の) 作用を持たないので、関数の引数の型は作用の注釈を持ちません。 一方で、関数の本体は非自明な計算を行なうかもしれません。 そのため上記で説明したように、その結果は常に型と作用の両方で与えられます。

練習問題 2a:
上記で見てきたように、定義が予想される型を持つことを F* にチェックさせるために val を使います。 canReadcanWrite について 1.1.1 から予測される型を書いて、それをチェックするよう F* に支持してください。

module FileName
  type filename = string

module ACLs
  open FileName

  val canWrite : unit (* write a correct and precise type here *)
  let canWrite (f:filename) =
    match f with 
      | "demo/tempfile" -> true
      | _ -> false

  val canRead : unit (* write correct and precise type here *)
  let canRead (f:filename) =
    canWrite f               (* writeable files are also readable *)
    || f="demo/README"       (* and so is this file *)

エディタに読み込む

回答
val canRead: filename -> Tot bool
val canWrite: filename -> Tot bool

エディタに読み込む

2.3.1. デフォルトの作用は ML

注釈がない場合、F* は、入出力を行なうかもしれないか、停止しないかもしれない関数を、作用 ML を持つと (ときに保守的に) 推論します。 そのため、下記どちらの関数も型 (int -> ML int) を持つと推論されます。 (注意: 再帰関数は ML 族の言語では let rec で定義されます。)

let hello_incr i = IO.print_string "hello"; i + 1
let rec loop i = i + loop (i - 1)

もし明示的な注釈を与えると、これらの関数により正確な型を割り当てることができます:

val hello_incr i : int -> IO int
let hello_incr i = IO.print_string "hello"; i + 1

val loop : int -> Dv int
let rec loop i = i + loop (i - 1)

プログラムを ML から F* に移植するために、私達はデフォルトの作用を ML に選び、通常はそれを書かずに済むようにしました。 そのため hello_incrloop を表わす通常の ML シグニチャを以下の示すように書くことができます。 これはより明示的な (int -> ML int) と単に同義です。

val hello_incr: int -> int
val loop: int -> int

2.3.2. 計算する関数

もし関数型プログラミングの初学者なら、はじめて読む際にこの章を飛ばしてください。

ときに、なんらかの計算を行なった後に関数を返すことが有用です。 例えば、次の関数は新しいカウンタを作り、それを init で初期化します。

let new_counter init =
  let c = ST.alloc init in
  fun () -> c := !c + 1; !c

F*new_counter が型 int -> ST (unit -> ST int) を持つと推論します。 型によるとこの関数は、整数が与えられ、参照を読み書きもしくは確保するかもしれず、それから unit -> ST unit 型の関数を返します。 この型を書いて、F* にチェックさせることができます; もしくはサブ作用を使って、下記のように型を書いて new_counter が上手く型付けできることを F* にチェックさせることもできます。

val new_counter: int -> ML (unit -> int)

上記の型、int -> ML (unit -> ML int) の短縮形は、int -> unit -> int と同じでは ありません 。 注意してください。 後者は int -> Tot (unit -> ML int) の短縮形です。

3. 整数を扱う関数の最初の証明

アクセスコントロールリストの最初の例では、どのように F* の型システムがセキュリティ属性の自動的な検査に使うことができるか示しました。 けれども、より興味深いセキュリティに関連したプログラミングと検証を行なう前に、F* の基礎についてより理解を深める必要があります。 ここで戻って、整数を扱う単純な関数のプログラミングと性質の証明を見てみましょう。

3.1. 静的に検査される表明

F* のコードにおける性質を証明する1つの方法は表明を書くことです。

let a = assert (max 0 1 = 1)

最初の表明は max に関する明らかな性質です。 別の言語で assert と呼ばれる構成物を見たことがあるかもしれません一般に、そのような assert はコードの性質を 実行時に 検査するために使われ、その表明条件が true でない場合には表明に失敗した例外が発生します。

F* では、表明は実行時の意味を持ちません。 その代わりに、F* はその表明条件が真であることを静的に証明しようとします。 そのため実行時に検査されたとしても決っして失敗しません。

この場合、max 0 1 = 1 の証明は簡単です。 裏で F*max の定義と表明された性質を Z3 と呼ばれる定理証明器に渡して、その性質を自動的に証明します。

max のより一般的な性質を表明して、自動的に検査することができます。例えば次のようになります:

let a = assert (forall x y. max x y >= x
                 && max x y >= y
                 && (max x y = x || max x y = y))

3.2. 階乗とフィボナッチ関数

階乗関数を見てみましょう:

let rec factorial n = if n = 0 then 1 else n * factorial (n - 1)

以前解説した通り、注釈がない場合、F* はこの関数の型を int -> int であると推論します。これは int -> ML int の短縮形ですこれは F* がこの factorial が (もしくはどのような再帰関数が) 純粋で全域関数であることを自動的に証明しようとしないことを意味しています。 実際、階乗は任意の整数に対して全域関数ではないのです! factorial (-1) を考えてみましょう。

Remark. F*int 型は任意精度の整数を表わします。

けれども、factorial 関数は非負の整数については全域関数です。 これを実際に書いた場合、検査を F* に支持できます:

val factorial: x:int{x>=0} -> Tot int

上記の行にはいくつかの主張があります:

このように書くと、F*factorial がこれら全ての性質を満たすことを自動的に証明します。 もちろん、証明における主な興味は x が非負の場合に factorial x が実際に停止するかどうかです。 これがどのように行なわれるかその詳細は章 5 で議論しますが、この場合 F* が非負な数値に対する全ての再帰的な呼び出しは以前の呼び出しでの引数より厳密に小さくなることを証明できると理解すれば十分です。 これは無限に続くかない (最終的に基底ケース 0 に収束する) ので、F*factorial の型に関する主張に同意します。

非負な整数 (もしくは自然数) の型はありふれたもので、それは省略して定義できます。 (実際、F* では標準の prelude 中でこれは既に定義済みです。)

type nat = x:int{x>=0}

練習問題 3a:
factorial には他にどのような型を与えられるでしょうか? それらを書いて、F* が同意するかどうか確認してください。 それらの型の意味を言葉で表現してください。

val factorial: x:int{x>=0} -> Tot int
let rec factorial n = if n = 0 then 1 else n * factorial (n - 1)

エディタに読み込む

回答

factorial に対して多くの正しい型があります。 次はその内のいくつかです:

val factorial: int -> int                     (* inferred by default *)
val factorial: int -> ML int                  (* same as above *)
val factorial: nat -> Tot int                 (* total function on nat inputs *)
val factorial: nat -> Tot nat                 (* stronger result type *)
val factorial: nat -> Tot (y:int{y>=1})       (* even stronger result type *)

エディタに読み込む

練習問題 3b:
フィボナッチ関数に対して型をいくつか与えてください。

let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

エディタに読み込む

回答
module Fibonacci

(* val fibonacci : nat -> Tot nat *)
(* val fibonacci : int -> int *)
(* val fibonacci : int -> ML int (same as above) *)
val fibonacci : int -> Tot (x:nat{x>0})
let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

エディタに読み込む

3.3. 補題

factorial 関数を書いて、型 (nat -> Tot nat) を与えたとしましょう。 すると例えば x > 2 ならば factorial x > x といったような、他の性質が気になるでしょう。 1つの方法は factorial の型を修正して、その型を F* に再度証明させることです。 しかしこれは常に柔軟なわけではありません。 x > 3 ならば factorial x > 2 * x も証明したいとしたらどうなるでしょうか: factorial の型に対するこれらの性質による汚染は、明確に実用的ではありません。

けれども、factorial に関するさらなる性質を証明するために、factorial を定義して nat -> Tot nat のような一般的な型を与えた後に、F* では (補題と呼ばれる) 他の関数を書くことができます。

補題は、常に単純な unit の値 () を返す ゴースト 全域関数です。 計算上、補題それ自体は役立ちませんそれらは作用を持たず、常に同じ値を返します。それならばポイントはなんでしょうか? そのポイントは、補題によって返される値の型がプログラムに関する有用な性質を有していることにあります。

factorial に関する最初の補題として、それが正の数を常に返すことを証明してみましょう。

val factorial_is_positive: x:nat -> GTot (u:unit{factorial x > 0})
let rec factorial_is_positive x =
  match x with
  | 0 -> ()
  | _ -> factorial_is_positive (x - 1)

この補題のステートメントは factorial_is_positive に与えられた型です。 それは x:nat に対するゴースト全域関数で、リファインメント factorial x > 0 と共にユニットを返します。 次の3行で factorial_is_positive を定義しており、x に対する帰納による証明を使ってこの補題を証明しています。 ここでの基本的なコンセプトは、全域関数を使ったプログラミングによって他の純粋な式に関する証明を書けることです。 この章の残りでこのような証明について詳細に議論します。

Remark. F* では (計算上無意味な) ゴーストであるような式は1つの作用です。 factorial_is_positive の型における作用 GTot は、それがゴーストで全域関数であることを示しています。

3.3.1. 依存関数型

この補題のステートメントをもう少しよく見てみましょう。

val factorial_is_positive: x:nat -> GTot (u:unit{factorial x > 0})

これは F* における 依存関数型 です。 なぜ 依存 するのでしょうか? その結果の型はパラメータ x:nat に依存しているのです。 例えば、factorial_is_positive 0 は型 Tot (u:unit{factorial 0 > 0)) を持ちます。 これは factorial_is_positive 1 の型と異なります。

依存関数を紹介したので、関数型の一般的な形を少し詳しく見てみましょう:

x1:t1 -> ... -> xn:tn[x1 ... xn-1] -> E t[x1 ... xn]

関数の正規のパラメータそれぞれは xi と名付けられていて、それらの名前のスコープはそれに続く最初の矢印の右側です。 表記 t[x1 ... xm]t 中に変数 x1 ... xm が自由出現することを示しています。

3.3.2. リファインメント型と補題に対するシンタックスシュガー

引数が2より大きいとき、factorial がその引数より厳密に大きいことをどうやって明記すべきでしょうか? 次は最初の試みです:

val factorial_is_greater_than_arg1: x:(y:nat{y > 2}) -> GTot (u:unit{factorial x > x})

これは上手く行きますが、2つの名前が必要になるため、関数の引数の型は少し不恰好です: y はそのドメインを 2 より大きい自然数に制限するためで、x は返り値の型で引数に言及するためです。 このパターンはありふれていて、F* はそのためのシンタックスシュガーを提供していますfactorial に与えた最初の型で既に見てきました。 それを使うことで、上記の型と等価で、より簡潔な次のような型を書くことができます。

val factorial_is_greater_than_arg2: x:nat{x > 2} -> GTot (u:unit{factorial x > x})

もう1つの疑いようのない不恰好な点は補題の返り値の型で、それは unit 型のリファインメントを含んでいます。 これを簡潔にするために、F*Lemma キーワードを提供していて、作用 GTot の代わりに使うことができます。

例えば、factorial_is_greater_than_arg2 の型は (下記の) factorial_is_greater_than_arg3 の型と等価で、それは少し読み書きしやすいでしょう。

val factorial_is_greater_than_arg3: x:nat{x > 2} -> Lemma (factorial x > x)

また都合が良ければ、次のように書くこともできます:

val factorial_is_greater_than_arg4: x:nat -> Lemma (requires (x > 2))
                                              (ensures (factorial x > x))

requires の後の式は関数/補題の 事前条件 で、ensures の後の式はその 事後条件 です。

3.3.3. 帰納によって証明された単純な補題について詳細に

ここで factorial_is_greater_than_arg の証明を詳細に見てみましょう。 それは次のようになります:

let rec factorial_is_greater_than_arg x =
  match x with
  | 3 -> ()
  | _ -> factorial_is_greater_than_arg (x - 1)

この証明は (let rec で示された) 再帰関数です; この関数は x に対する場合分けで定義されています。

最初のケースは、引数が 3 で; そのため factorial 3 > 3 を証明する必要があります。 F* はこの性質に相当する証明を生成し、前に提供された factorial の定義が与えられたとき、それを証明できるかどうかを確かめるよう Z3 に要求しますZ3 は factorial 3 = 6 であり、もちろん 6 > 3 で、このケースの証明は完了します。 これはこの帰納の基底ケースです。

ケースは順番に解釈されるため、2番目のケースに辿り着いた場合、最初のケースに当てはまらないことを知っています。 すなわち、2番目のケースでは factorial_is_greater_than_arg の型から x:nat{x > 2} を、前のケースに当てはまらなかったので x <> 3 であることを知っています。 別の言い方をすると、2つ目のケースは帰納ステップで、x > 3 のときの証明を扱います。

くだけた表現をすると、このケースの証明は、次で与えられる帰納法の仮定を使って行なわれます:

forall n, 2 < n < x ==> factorial n > n

そしてゴールは factorial x > x を証明することです。 もしくは等価に、factorial (x - 1) > x - 1 が既知であるときに x * factorial (x - 1) > x を証明することでう; さらにもしくは x*x - x > x を証明することになりこれは x > 3 のとき真です。 どのように F* でこれが形式的に行なわれるか見てみましょう。

全域再帰関数を定義するとき、定義されるその関数 (この場合 factorial_is_greater_than_arg) はその定義の本体で使うことができます。 しかしそれは再帰呼び出しが停止することを確認できる型である場合のみです。 このケースでは、定義本体中の factorial_is_greater_than_arg の型は:

n:nat{2 < n && n < x} -> Lemma (factorial n > n)

これはもちろん正確に帰納法の仮定です。 2番目のケースで factorial_is_greater_than_arg (x - 1) を呼び出すことで、実質的に帰納法の仮定を使用して factorial (x - 1) > x - 1 を証明し、2 < x - 1 && x - 1 < x を証明できますこれを Z3 に証明させると、このケースでは x > 3 であることを知っているのでそれは成功します。 最後に、x > 3 と 帰納法の仮定を使って得られた性質からゴールである factorial x > x を証明しなければなりません: Z3 は再びこれをたやすく証明してくれます。

練習問題 3c:
フィボナッチ関数の次の性質を証明してください:

val fibonacci : nat -> Tot nat
let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

val fibonacci_greater_than_arg : n:nat{n >= 2} -> Lemma (fibonacci n >= n)

エディタに読み込む

回答
let rec fibonacci_greater_than_arg n =
  match n with
  | 2 -> ()
  | _ -> fibonacci_greater_than_arg (n-1)

エディタに読み込む

3.4. Admit

証明を構築する際、証明の部品を仮定して別の部品に集中することはしばしば有用です。 例えば、ケース分析を行なっている際、ケースは自明で F* が自動的に解決できるのか、ケースが手動での証明を必要としているのかしばしば知りたくなります。 1つのケースの全てを承認 (admit) することでこれを実現できます。 F* が補題を自動的に証明できるなら、そのケースは自明です。 このような目的のために、F*admit 関数を提供していて、それは次のように使います:

    let rec factorial_is_greater_than_arg x =
      match x with
      | 3 -> ()
      | _ -> admit()

この型検査には成功するので、帰納の基底ケースは自明に証明され、帰納ケースにフォーカスすべきであることがわかります。

3.5. boolType の詳細

もしこのタイトルが不可解に思えたなら、はじめて読む際にこの章をスキップすることができます。 けれどもリファインメント型で量化された式を使いはじめるなら、この章を理解しているか確かめるべきです。

以前、リファイメント型は x:t{phi(x)} の形を取ると言及しました。 その初期の形では、phi は実際には型で、値 x:t 上の述語です。 型の代わりにブール関数を使うことができ、次のような変換を加えることで、型にブールを暗黙に反感します:

b2t (b:bool) : Type = (b == true)

== は等式の述語を表わす型コンストラクタです; それは = とは異なり、値のペアを比較するブール関数です。 加えて == はヘテロジニアスです: その型にかかわらず、どのような値のペアに関して等式を主張することができます。 対照的に = はホモジニアスです。

命題の結合 /\, \/, ~ はそれぞれ論理積, 論理和, 否定を表わし、それらは型コンストラクタです。 また単方向と双方向の論理包含を表わす ==><==> もあります。 対照的に &&, ||, not はブール関数です。

bool から Type への暗黙の変換のために、これら2つの間の差異をほとんど気にせずに済みます。 けれども、量化を共なうリファインメント式を書きはじめるなら、両者の差異は明白になります。

全称量化 forall と存在量化 existsType でのみ有効です。 ブール関数と量化を含むリファインメントを混ぜる場合、命題の結合を使う必要があります。 例えば、次の式は正しい形です:

canRead e /\ forall x. canWrite x ==> canRead x

これは次のようなより複雑な形の短縮形です:

b2t(canRead e) /\ forall x. b2t(canWrite x) ==> b2t(canRead x)

一方、次の式は正しくありません; F* はこれを拒否します:

canRead e && forall x. canWrite x ==> canRead x

その理由はこの量化は型で、その一方 && はブールを期待しているためです。 ブールは型に変換できますが、別の方向の変換はありません。

4. 単純な帰納型

次は F* での (イミュータブルな) リストの標準的な定義です。

type list 'a =
  | Nil  : list 'a
  | Cons : hd:'a -> tl:list 'a -> list 'a

F* でのデータ型のコンストラクタにはいくつかの重要な慣習があります。

list 型は F* の標準の prelude で定義されていて、全ての F* プログラム中で暗黙的に有効です。 リストコンストラクタに対して特別な (しかし標準的な) 構文が提供されています:

(例えば Cons を部分適用するといった) 有用な場面では、NilCons のようなコンストラクタを明示的に書くことができます。

4.1. リストに対する基本的な関数の証明

リストに対する通常の関数は、他の ML 方言と同様に F* でも書くことができます。 次は length 関数です:

val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl

length の型は、この関数が 'a 型の値のリストに対する全域関数で、非負の整数を返すことを証明しています。

練習問題 4a:
次は2つのリストを連結する append 関数です。

let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2

エディタに読み込む

長さがその引数の長さの和となるようなリストを常に返すような型を append 与えてください。

回答
    l1:list 'a -> l2:list 'a -> Tot (l:list 'a{length l = length l1 + length l2})

エディタに読み込む

練習問題 4b:
append に以下のような弱い型を与えた後、前の練習問題と同じ性質を補題を使って証明してください。

val append:list 'a -> list 'a -> Tot (list 'a)

エディタに読み込む

回答
val append_len: l1:list 'a -> l2:list 'a
             -> Lemma (requires True)
                      (ensures (length (append l1 l2) = length l1 + length l2)))
let rec append_len l1 l2 = match l1 with
    | [] -> ()
    | hd::tl -> append_len tl l2

エディタに読み込む

練習問題 4c:
xl 中に存在するかどうかを判定する関数 mem: x:'a -> l:list 'a -> Tot bool を定義してください。 その後、その関数が次の性質を満たすことを証明してください。

val append_mem:  l1:list 'a -> l2:list 'a -> a:'a
        -> Lemma (ensures (mem a (append l1 l2)  <==>  mem a l1 || mem a l2))

エディタに読み込む

回答

val mem: 'a -> list 'a -> Tot bool
let rec mem a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl

val append_mem:  l1:list 'a -> l2:list 'a -> a:'a
    -> Lemma (ensures (mem a (append l1 l2)  <==>  mem a l1 || mem a l2))
let rec append_mem l1 l2 a = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2 a

エディタに読み込む

4.2. 本質的に型となるのか、もしくは補題を証明するか?

前章の練習問題のように、関数の型を強化したり、その関数に関する分離した補題を書くことで性質を証明できます私達はそれらをそれぞれ ‘intrinsic’ スタイルと ‘extrinsic’ スタイルと呼んでいます。 どちらのスタイルが向いているかは好みと利便性の問題です: (例えば lengthnat を返すといったような) 一般に有用な性質は intrinsic な仕様が相応しいでしょう; より具体的な性質は補題で表明して証明した方が良いでしょう。 けれども次の例のようにいくつかの場合では、型で直接関数の性質を証明するのは不可能なときがあります補題に頼らねばなりません。

val reverse: list 'a -> Tot (list 'a)
let rec reverse = function
  | [] -> []
  | hd::tl -> append (reverse tl) [hd]

リストを二度逆順する関数が恒等関数であることを証明してみましょう。 リファインメント型を使って reverse の型にこの性質を 明記 することができます。

val reverse: f:(list 'a -> Tot (list 'a)){forall l. l = f (f l)}

けれども、F* はこれを reverse の有効な型として許容しません: この性質を証明するには2つの分離された帰納が必要で、そのどちらも F* は自動的に行ないません。

その代わりに、2つの補題を使ってこの性質を証明できます。 それらの補題は次のようになります:

let snoc l h = append l [h]

val snoc_cons: l:list 'a -> h:'a -> Lemma (reverse (snoc l h) = h::reverse l)
let rec snoc_cons l h = match l with
  | [] -> ()
  | hd::tl -> snoc_cons tl h

val rev_involutive: l:list 'a -> Lemma (reverse (reverse l) = l)
let rec rev_involutive l = match l with
  | [] -> ()
  | hd::tl -> rev_involutive tl; snoc_cons (reverse tl) hd

rev_involutiveCons ケースでは、帰納法の仮定だけでなく上記せ証明済みの補題 snoc_cons も明示的に適用しています。

練習問題 4d:
逆順が単射であることを証明してください。例えば

val rev_injective: l1:list 'a -> l2:list 'a
                -> Lemma (requires (reverse l1 = reverse l2))
                         (ensures  (l1 = l2))

エディタに読み込む

回答

おそらくこのような答えになったでしょう:

val snoc_injective: l1:list 'a -> h1:'a -> l2:list 'a -> h2:'a 
                 -> Lemma (requires (snoc l1 h1 = snoc l2 h2))
                          (ensures (l1 = l2 && h1 = h2))
let rec snoc_injective l1 h1 l2 h2 = match l1, l2 with
  | _::tl1, _::tl2 -> snoc_injective tl1 h1 tl2 h2
  | _ -> ()

val rev_injective1: l1:list 'a -> l2:list 'a 
                -> Lemma (requires (reverse l1 = reverse l2))
                         (ensures  (l1 = l2)) (decreases l1)
let rec rev_injective1 l1 l2 =
  match l1,l2 with
  | h1::t1, h2::t2 ->
      // assert(reverse (h1::t1) = reverse (h2::t2));
      // assert(snoc (reverse t1) h1  = snoc (reverse t2) h2);
      snoc_injective (reverse t1) h1 (reverse t2) h2;
      // assert(reverse t1 = reverse t2 /\ h1 = h2);
      rev_injective1 t1 t2
      // assert(t1 = t2 /\ h1::t1 = h2::t2)
  | _, _ -> ()

エディタに読み込む

これは退屈な証明ではないでしょうか。 次はより簡潔な証明です。

val rev_injective2: l1:list 'a -> l2:list 'a 
                -> Lemma (requires (reverse l1 = reverse l2))
                         (ensures  (l1 = l2))
let rev_injective2 l1 l2 = rev_involutive l1; rev_involutive l2

エディタに読み込む

証明 rev_injective2 は全ての対合関数が単射であるというアイデアに基づいています。 reverse が対合であることはすでに証明しました。 そのため l1 に一度、l2.に一度、その補題を呼び出すことができます。 これで SMT ソルバに reverse (reverse l1) = l1reverse (reverse l2) = l2 という情報を与え、これは証明を完了するに十分です。 証明を構築するとき、補題はいつもあなたの友達なのです!

4.3. リストに対する高階関数

4.3.1. マップ

リストに対する高階関数、すなわち引数として別の関数を取る関数を書くことができます。 次はおなじみの map です:

  let rec map f l = match l with
    | [] -> []
    | hd::tl -> f hd :: map f tl

これは関数 f とリスト l を取り、l のそれぞれの要素に f を適用して新しいリストを生成します。 より正確には map f [a1; ...; an] はリスト [f a1; ...; f an] を生成します。 例えば:

map (fun x -> x + 1) [0;1;2] = [1;2;3]

通常、仕様がない場合、F*map の型を ('a -> 'b) -> list 'a -> list 'b と推論します。 明確に書くと、map の型は ('a -> ML 'b) -> Tot (list 'a -> ML (list 'b)) です。 f の型もデフォルトでは作用 ML を持つ関数となることに注意してください。

型注釈を追加することで、map異なる 型を与えることができます:

val map: ('a -> Tot 'b) -> list 'a -> Tot (list 'b)

この型は F* が推論した型のサブタイプでもスーパータイプでもありません。

作用に対するパラメトリック多相はありません: map にもっと汎用的な型を与えたいと思うかもしれません。 あらゆる作用 E を共ない、同じ作用を持つ関数を返す関数を許容したいと思うでしょう。 これは作用に対して多相の一種を要求することになりますが、F* はそのような多相をサポートしていません。 このためいくらかードの重複を誘発します。 私達はこれを解決するために、アドホックなオーバライド機構を用いて、値に対して1つ以上の型を書けるようになるよう計画しています。

4.3.2. 検索

練習問題 4e:

ブール関数 f とリスト l が与えられると、f が真になる l の最初の要素を返す find 関数を定義します。 要素が見つからないときは findNone を返します; このためいつもの option 型を使います (これは以下に示されていますが、F* の標準 prelude でも有効です)。

    type option 'a =
       | None : option 'a
       | Some : 'a -> option 'a

    let rec find f l = match l with
      | [] -> None
      | hd::tl -> if f hd then Some hd else find f tl

エディタに読み込む

findSome x を返すなら f x = true であることを証明してください。 これは intrinsic と extrinsic どちらで行なうのが良いでしょうか? 両方の方法で解いてください。

回答
module Find

type option 'a =  
   | None : option 'a
   | Some : 'a -> option 'a

(* The intrinsic style is more convenient in this case *)
val find : f:('a -> Tot bool) -> list 'a -> Tot (option (x:'a{f x}))
let rec find f l = match l with
  | [] -> None
  | hd::tl -> if f hd then Some hd else find f tl

(* Extrinsically things are more verbose, since we are basically duplicating
   the structure of find in find_some. It's still not too bad. *)

val find' : f:('a -> Tot bool) -> list 'a -> Tot (option 'a)
let rec find' f l = match l with
  | [] -> None
  | hd::tl -> if f hd then Some hd else find' f tl

val find_some : f:('a -> Tot bool) -> l:list 'a -> x:'a -> Lemma
                  (requires (find' f l = Some x))
                  (ensures (f x = true))
let rec find_some f l x =
  match l with
  | [] -> ()
  | hd::tl -> if f hd then () else find_some f tl x

エディタに読み込む

練習問題 4f:
次のようなリストに対する fold_left 関数を定義してください:

fold_left f [b1; ...; bn] a = f (bn, ... (f b2 (f b1 a)))

(fold_left Cons l [] = reverse l) を証明してください。 (この証明はこれまで解いてきた練習問題より難しいでしょう。)

val fold_left_cons_is_reverse: l:list 'a -> l':list 'a ->
      Lemma (fold_left Cons l l' = append (reverse l) l')

エディタに読み込む

回答
val fold_left: f:('b -> 'a -> Tot 'a) -> l:list 'b -> 'a -> Tot 'a
let rec fold_left f l a = match l with
  | Nil -> a
  | Cons hd tl -> fold_left f tl (f hd a)

val append_cons: l:list 'a -> hd:'a -> tl:list 'a ->
                 Lemma (append l (Cons hd tl) = append (append l (Cons hd Nil)) (tl))
let rec append_cons l hd tl = match l with
  | Nil -> ()
  | Cons hd' tl' ->
    append_cons tl' hd tl

val snoc_append: l:list 'a -> h:'a -> Lemma (snoc l h = append l (Cons h Nil))
let rec snoc_append l h = match l with
  | Nil -> ()
  | Cons hd tl ->
    snoc_append tl h

val reverse_append: tl:list 'a -> hd:'a ->
                  Lemma (reverse (Cons hd tl) = append (reverse tl) (Cons hd Nil))
let reverse_append tl hd = snoc_append (reverse tl) hd

val fold_left_cons_is_reverse: l:list 'a -> l':list 'a ->
                             Lemma (fold_left Cons l l' = append (reverse l) l')
let rec fold_left_cons_is_reverse l l' = match l with
  | Nil -> ()
  | Cons hd tl ->
    fold_left_cons_is_reverse tl (Cons hd l');
    append_cons (reverse tl) hd l';
    reverse_append tl hd

エディタに読み込む

4.4. 帰納型に対して暗黙に定義された関数

帰納型のそれぞれの定義対して、F* は多くの有用な関数を自動的に導入します: それぞれのコンストラクタには、discriminator が手に入り; それぞれのコンストラクタのそれぞれの引数には、projector が手に入ります。 実行例として (以下に繰り返し示す) リスト型を使ってこれらを次に説明します。

type list 'a =
  | Nil  : list 'a
  | Cons : hd:'a -> tl:list 'a -> list 'a

4.4.1. Discriminator

discriminator はブール値の全域関数で、項が個別のコンストラクタの適用であるかどうか調べます。 list 型に対して、2つの discriminator が手に入ります:

val is_Nil: list 'a -> Tot bool
let is_Nil xs = match xs with [] -> true | _ -> false

val is_Cons: list 'a -> Tot bool
let is_Cons xs = match xs with _::_-> true | _ -> false

4.4.2. Projector

Cons コンストラクタの型から、F* は次のシグニチャを生成します:

val Cons.hd : l:list 'a{is_Cons l} -> Tot 'a
val Cons.tl : l:list 'a{is_Cons l} -> Tot (list 'a)

(ここでは Cons.hd は限定された名前です)

これは、Cons の型での名前 hdtl が意味がある理由を示しています: それらは自動生成された projector の名前に相当します。 もしデータコンストラクタの引数に名前をつけなかったら、F* は名前を自動生成します。 (とはいえ、これらの名前は引数の位置から導出され、その形は仕様化されていません; そのため、自分自身で引数に名前をつけるのは良い習慣です。)

練習問題 4g:
その型が Cons.hdCons.tl の型にマッチする (hdtl という名前の) 関数を書いてください。

module HdTl

val hd : l:list 'a{is_Cons l} -> Tot 'a
val tl : l:list 'a{is_Cons l} -> Tot (list 'a)

エディタに読み込む

回答
val hd : l:list 'a{is_Cons l} -> Tot 'a
let hd l =
  match l with
  | h :: t -> h

val tl : l:list 'a{is_Cons l} -> Tot (list 'a)
let tl l =
  match l with
  | h :: t -> t

エディタに読み込む

練習問題 4h:
リストの n 番目の要素を返す関数を書いてください。 それが全域関数であることを保証する型を与えてください。

(* ここにコードを書いてください *)

エディタに読み込む

回答
val nth : l:list 'a -> n:nat{n < length l} -> 'a
let rec nth l n =
  match l with
  | h :: t -> if n = 0 then h else nth t (n-1)

エディタに読み込む

4.5. タプルとレコード

F* はタプルに対するシンタックスシュガーを提供しています。 タプルは単なる帰納型です: 28 サイズのタプルは標準 prelude で定義されています。 (もし必要なら追加できます。) 次は prelude におけるペアの定義です:

type tuple2 'a 'b =
  | MkTuple2: _1:'a -> _2:'b -> tuple2 'a 'b

MkTuple2 5 7 の代わりに (5, 7) と書くことができ、ペアには tuple2 int int を短縮した型 (int * int) を与えることができます。

この表記は、prelude で定義された関連した tupleN データ型と同じサイズのタプルを生成します。

また F* はレコードに対する構文も提供します。 けれどもレコードは (タプルと同じように) 単一コンストラクタのデータ型に内部で要約されます。 次はこの例です:

type triple 'a 'b 'c = {fst:'a; snd:'b; third:'c}
let f x = x.fst + x.snd + x.third

F* はこのプログラムを受け付け、f に型 (triple int int int -> Tot int) を与えます。

これは次のようなより冗長なソースコードを等価です:

type triple 'a 'b 'c =
  | MkTriple: fst:'a -> snd:'b -> third:'c -> triple 'a 'b 'c

let f x = MkTriple.fst x + MkTriple.snd x + MkTriple.third x

5. 停止性の証明

F* は全ての純粋な関数は停止することが証明されています。 F* で使われている停止性の検査は syntactic condition ではなく semantic criterion に基づいています。 F* の停止性検査の基本の概略を説明しますより興味深いプログラムを書くためには停止性について理解が必要になります。

5.1. 値に対する整礎半順序

F* で関数の停止を証明するために、ある尺度を提供します: それはその関数の引数に依存した純粋な式です。 F* はそれぞれの再帰呼び出しでこの尺度が厳密に減少することを検査します。 呼び出しにおける引数に対するこの尺度は、F* の値に対する整礎半順序に従って、前回の呼び出しでの尺度と比較されます。 この順序で v1v2 より 小さい とき、v1 << v2 と書きます。

もし RS に対する半順序で、R に関する S 中の無限降鎖がなければ、集合 S に対する関係 R は整礎半順序です。 例えば、自然数の集合 nat である S を取るとき、整数の順序 < は整礎半順序です (実際にはこれは全順序です)。

この尺度はそれぞれの再帰呼び出しで厳密に減少し、かつ無限降鎖がないので、これは再帰呼び出しで関数が最終的に停止することを保証します。

5.1.1. 減少関係

  1. 整数に対する順序: i, j : nat が与えられたとき、i << j <==> i < j が得られます。

    注意: 単なる 順序なので、負の整数は << 関係ではありません。

  2. 帰納型に対するサブ項順序: (Dv1 から vn の引数に適用されたコンストラクタであるような) 帰納型のどのような値 D v1 ... vn に対しても、全ての i において v_i << v が得られます。 すなわち、正しく型付けされた項のサブ項はその項より小さくなります。 (この規則の例外は次の lex_t です。)

  3. lex_t に対する辞書式順序: 以下で説明します。

5.1.2. 辞書式順序のペア

昔ながらの関数 ackermann を見てみましょう:

val ackermann: m:nat -> n:nat -> Tot nat
let rec ackermann m n =
  if m=0 then n + 1
  else if n = 0 then ackermann (m - 1) 1
  else ackermann (m - 1) (ackermann m (n - 1))

なぜこれは停止するのでしょうか? それぞれの再帰呼び出しにおいて、全ての引数が前回の呼び出しでの引数より厳密に小さく ならない ケースがあります。 例えば2番目の分岐において n0 から 1 に増加します。 けれどもこの関数は実際に停止し、F* はそれを証明します。

その理由は、全ての再帰呼び出しにおいてそれぞれの引数は減少していませんが、それらを一緒に取るとき、引数 (m,n) の順序ペアはペアの 辞書式順序 に従って減少しているからです。

標準 prelude では、F* は次の帰納型を定義しています:

type lex_t =
  | LexTop  : lex_t
  | LexCons : #a:Type -> a -> lex_t -> lex_t

(# 記号は1番目の引数が暗黙的であるとマークしています。8.3.1 を見てください。)

lex_t の辞書式順序 は次のようになります:

次のシンタックスシュガーを使えます:

%[v1;...;vn](LexCons v1 ... (LexCons vn LexTop)) の短縮形です

5.2. 停止性証明の詳細

次の形を使って再帰による関数を定義しているとしましょう:

val f: y1:t1 -> .. -> yn:tn -> Tot t
let rec f x1 .. xn = e

通常 ML では e を型検査するとき、再帰的に束縛された関数 f に、型 y1:t1 -> .. -> yn:tn -> Tot te を用いることができます。 この型はプログラマによって正確に書き下されます。 けれどもこの型は、f の呼び出しが無限の再帰呼び出しを誘発してしまわないことを保証するのに十分ではありません。

停止性を証明するために (すなわちを無限の深い再帰呼び出しを除外するために)、F* は再帰関数の型検査に異なる規則を用います。 次に示すより制限された型においてのみ、再帰的に束縛された名前 fe で用いることができます:

   y1:t1
-> ...
-> yn:tn{%[y1;...;yn] << %[x1;...;xn]}
-> Tot t

すなわち、デフォルトでは F* は関数のパラメータが (全ての関数型のパラメータを除いてパラメータが出現する順序で) そのパラメータの辞書式順序に従って減少することを要求します。 (このデフォルトを上書きする方法があります 5.2.2 を見てください。)

いくつかの例でこれがどのように働くのか見てみましょう。

5.2.1. アッカーマン

F*ackermann 関数

1.  let rec ackermann m n =
2.    if m=0 then n + 1
3.    else if n = 0 then ackermann (m - 1) 1
4.    else ackermann (m - 1)
5.                   (ackermann m (n - 1))

が停止することを自動的に示すことができます。このときその型は次のようになります:

ackermann : nat -> nat -> Tot nat

F* はこの関数にデフォルトの停止性メトリクスを与えます。 そのためこの関数は次のように展開されます:

ackermann : m:nat -> n:nat -> Tot nat (decreases %[m;n])

decreases 節は次の章で議論します。 この例では、この節は ackermann の本体中の再帰呼び出しを表わす次のようなより制限された型を F* 型検査器に使わせます:

ackermann: m':nat
        -> n':nat{%[m';n'] << %[m;n]}
        -> Tot nat

ackermann への3つの再帰呼び出しそれぞれにおいて、その引数が非負であるだけでなく、それらが上記のリファインメント式に従って前回の引数より小さくなることも証明する必要があります。

5.2.2. decreases 節

もちろん、ときどき再帰関数のデフォルト尺度を上書きする必要があります。 もし単純に ackermann 関数の引数を入れ換えたら、デフォルト尺度はもはや働きません。 そして、最初に m を比較してから n を比較するような辞書式順序を選択する decreases 節を明示的に追加する必要があります:

val ackermann_swap: n:nat -> m:nat -> Tot nat (decreases %[m;n])
let rec ackermann_swap n m =
   if m=0 then n + 1
   else if n = 0 then ackermann_swap 1 (m - 1)
   else ackermann_swap (ackermann_swap (n - 1) m)
                       (m - 1)

この任意の decreases 節は作用 Tot の2番目の引数です。 一般にこれはその関数の引数の全域の式です。

練習問題 5a:
次はリストの逆順関数のより効率的な (末尾再帰の) 変種です。

val rev : l1:list 'a -> l2:list 'a -> Tot (list 'a) (decreases l2)
let rec rev l1 l2 =
  match l2 with
  | []     -> l1
  | hd::tl -> rev (hd::l1) tl

エディタに読み込む

以前の単純な実装に対して、この効率的な実装が正しいことを示す次の補題を証明してください:

val rev_is_ok : l:list 'a -> Lemma (rev [] l = reverse l)

エディタに読み込む

回答
val append_assoc : xs:list 'a -> ys:list 'a -> zs:list 'a -> Lemma
      (ensures (append (append xs ys) zs = append xs (append ys zs)))
let rec append_assoc xs ys zs =
  match xs with
  | [] -> ()
  | x::xs' -> append_assoc xs' ys zs

val rev_is_ok_aux : l1:list 'a -> l2:list 'a -> Lemma
      (ensures (rev l1 l2 = append (reverse l2) l1)) (decreases l2)
let rec rev_is_ok_aux l1 l2 =
  match l2 with
  | [] -> ()
  | hd::tl  -> rev_is_ok_aux (hd::l1) tl; append_assoc (reverse tl) [hd] l1

val append_nil : xs:list 'a -> Lemma
      (ensures (append xs [] = xs))
let rec append_nil xs =
  match xs with
  | [] -> ()
  | _::tl  -> append_nil tl

val rev_is_ok : l:list 'a -> Lemma (rev [] l = reverse l)
let rev_is_ok l = rev_is_ok_aux [] l; append_nil (reverse l)

エディタに読み込む

練習問題 5b:
(変更!) 次はフィボナッチ関数のより効率的な (末尾再帰の) 変種です。

val fib : nat -> nat -> n:nat -> Tot nat (decreases n)
let rec fib a b n =
  match n with
  | 0 -> a
  | _ -> fib b (a+b) (n-1)

エディタに読み込む

以前の単純な実装に対して、この効率的な実装が正しいことを示す次の補題を証明してください:

val fib_is_ok : n:nat -> Lemma (fib 1 1 n = fibonacci n)

エディタに読み込む

回答
val fib_is_ok_aux : i:nat -> n:nat{i<=n} ->
      Tot (u:unit{fib (fibonacci i) (fibonacci (i+1)) (n-i) = fibonacci n})
      (decreases (n-i))
let rec fib_is_ok_aux i n =
  if i=n then ()
  else fib_is_ok_aux (i+1) n

val fib_is_ok : n:nat -> Lemma (fib 1 1 n = fibonacci n)
let fib_is_ok n = fib_is_ok_aux 0 n

エディタに読み込む

5.3. 相互再帰関数

相互再帰関数に対しても、停止性の証明に対する同じ戦略が使えます。 相互再帰関数の場合、 F* の停止性検査器は、全ての直接もしくは相互再帰呼び出しが呼び出された関数の停止性メトリクスを減少させることを要求します。 これは非常に強い要求です。 次の例を考えてみましょう:

val foo : l:list int -> Tot int
val bar : l:list int -> Tot int
let rec foo l = match l with
    | [] -> 0
    | x::xs -> bar xs
and bar l = foo l

(bar を通して) foo は常にサブリストに対して呼び出されるので、この関数は停止します。 けれども bar からの foo 呼び出しはより小さなリストに対してではありません。 デフォルトのメトリクスを用いるとこの例は検査できません。

2つの関数が停止することを F* に納得させるために、カスタムのメトリクスを使うことができます:

val foo : l:list int -> Tot int (decreases %[l;0])
val bar : l:list int -> Tot int (decreases %[l;1])

foobar のメトリクスは両方とも、1つ目は引数 l で2つ目は 0 もしくは 1 であるような辞書式のタプルです。 foo からの bar 呼び出しは l を減少させ、bar からの foo 呼び出しは l を同じ値で保ちますが2番目の要素を 1 から 0 に減少させます。

6. これまでの要素をまとめる

ここで、これまで学んできた様々な機能を練習する2つの完全なプログラムを見てみましょう。 そのぞれの練習では、それらのプログラムを修正したり一般化したりするための練習問題があります。

6.1. リストのクイックソート

プログラムの検証に対する標準的な例は、様々なソートアルゴリズムが正しいことを証明することです。

整数のリストからはじめて、いくつかの性質を表現しましょう。 整数のリストを昇順にソートする関数 sorted からはじめて、ソートアルゴリズムが真であることを言いたいのです。

  val sorted: list int -> Tot bool
  let rec sorted l = match l with
      | [] -> true
      | [x] -> true
      | x::y::xs -> x <= y && sorted (y::xs)

ソートアルゴリズム sort が与えられたとき、次の性質を証明したいとします。 このとき mem は、先のリストの練習問題でのリストのメンバーシップ関数です (章 4.1 を見てください)。

sorted (sort l) /\ ( forall i. mem i l <==> mem i (sort l) )

この仕様が改良できることを以降で見てみましょう。

6.1.1. クイックソートを実装する

次はクイックソートアルゴリズムの単純な実装です。 この実装は常にリストの1つ目の要素をピボットとして取り出し; リストの残りをピボット以上の要素を含む区画とそれ以外を含む区画に分け; それらの区画を再帰的にソートし; そして返る前に中央にピボッドを挿入します。

let rec sort l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo  = partition (fun x -> pivot <= x) tl in
    append (sort lo) (pivot::sort hi)

練習問題 6a:
partition 関数を書いて、それが全域であることを証明してください。

val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)

エディタに読み込む

回答

次の定義は F* のリストライブラリに含まれています。

val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2

エディタに読み込む

6.1.2. sort を明記する

本質的に sort を検証します。 けれどもいくつか追加の補題を使う必要があります。 次は仕様の最初の試みです。 F* にこれを証明させてみてください。

val sort0: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l <==> mem i m) })

当然これはいくつかの点で失敗します:

  1. この関数が全域であることの証明に失敗します。 どうすればそれぞれの sort 呼び出しが小さくなる引数を取ることを主張できるでしょうか? 直感的にそれぞれの再帰呼び出しにおいて、引数として渡されるリストの長さは、tl の区画なので、厳密に小さくなります。 これを表わすために、decreases 節を追加する必要があります。
  1. ソートの性質とメンバーシップの性質の両方の証明に失敗しますpartitionsorted 関数に関する補題が必要です。

再び挑戦してみましょう:

val sort: l:list int -> Tot (m:list int{sorted m
                                     /\ forall i. mem i l <==> mem i m})
                            (decreases (length l))

そして次は partitionsorted に関する2つの補題です:

 val partition_lemma: f:('a -> Tot bool)
    -> l:list 'a
    -> Lemma (requires True)
             (ensures ((length (fst (partition f l))
                      + length (snd (partition f l)) = length l
                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                  /\ (forall x. mem x l = (mem x (fst (partition f l))
                                        || mem x (snd (partition f l)))))))
 let rec partition_lemma f l = match l with
   | [] -> ()
   | hd::tl -> partition_lemma f tl

Remark. 仕様中で fst (partition f l) のような繰り返されるサブ項は、型における let 束縛を必要としています。 後の章でこれを行なう方法を紹介しますいくつか追加の機構を導入します。

 val sorted_concat_lemma: l1:list int{sorted l1}
                       -> l2:list int{sorted l2}
                       -> pivot:int
                       -> Lemma (requires ((forall y. mem y l1 ==> not (pivot <= y))
                                        /\ (forall y. mem y l2 ==> pivot <= y)))
                                (ensures (sorted (append l1 (pivot::l2))))
 let rec sorted_concat_lemma l1 l2 pivot = match l1 with
  | [] -> ()
  | hd::tl -> sorted_concat_lemma tl l2 pivot

最後に、以前の練習問題で示した補題の全称量化された変種 append_mem も必要になります:

 val append_mem:  l1:list 'a
               -> l2:list 'a
               -> Lemma (requires True)
                        (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
 let rec append_mem l1 l2 = match l1 with
   | [] -> ()
   | hd::tl -> append_mem tl l2

これらの補題とともに、クイックソートの実装に戻りましょう。 不幸にも、これらの補題を使っても、クイックソートの元の実装が正しいことをまだ証明できません。 (章 4.1 の) rev_injective の証明で見たように、それらの性質を使うために明示的に補題を呼び出す必要があります。 すぐに上手く行きますが、証明を通すために補題を呼び出して sort をどうやって修正するのか見てみましょう。

let cmp i j = i <= j
val sort_tweaked: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l = mem i m)})
                                    (decreases (length l))
let rec sort_tweaked l = match l with
  | [] -> []
  | pivot::tl ->
    let hi', lo' = partition (cmp pivot) tl in
    partition_lemma (cmp pivot) tl;
    let hi = sort_tweaked hi' in
    let lo = sort_tweaked lo' in
    append_mem lo (pivot::hi);
    sorted_concat_lemma lo hi pivot;
    append lo (pivot::hi)

これは上手く行きますが、少し不恰好です。 補題を呼び出して実装を汚す必要があっただけでなく、それらの呼び出しのために、それらの補題への引数のために名前を束縛できるようにコードを書き換えなければなりませんでした。 これは改善することができます。

6.1.3. SMT 補題: intrinsic と extrinsic な証明のギャップを埋める

もし partitionsorted に補題を使って早明した性質を捕捉するより豊かな intrinsic な型を与えたいだけなら、クイックソートの実装を汚したくありませんでした。 これは intrinsic な証明スタイルを使う重要な利点ですpartition (fun x -> pivot <= x) tl のような関数の全ての呼び出しは、その関数に関して本質的に証明された全ての性質を直接持っています。

けれども、アプリケーション特有の型を持つ一般目的の関数の型に対する汚染もまたひどいものでしょう。 sorted の型を sorted_concat_lemma によって証明された性質で改良することを考えてみましょう。 sorted は一般的な仕様で挿入ソートやマージソートでも働くのに対して、この補題はクイックソートに高度に特化されています。 その型を汚すことは役立たずです。 そのため困難に陥いっているようです。

もし補題によって関数 f について証明された性質を、遡って直接 f と結びつける方法があったら良いと思いませんか? 全ての適用 f x が直接その補題の性質を持てるようにするのです。 F* は、このような intrinsic と extrinsic な証明のギャップを埋める方法を提供します。

仮に次のような partition_lemma の型を書いたとします唯一の違いは最後の行で、[SMTPat (partition f l)] を追加しています。 この行は、項 partition f l の全ての出現とその補題によって証明された性質を関連付けるよう、F* と SMT ソルバに支持します。

val partition_lemma: f:('a -> Tot bool)
  -> l:list 'a
  -> Lemma (requires True)
           (ensures ((length (fst (partition f l))
                    + length (snd (partition f l)) = length l
                /\ (forall x. mem x (fst (partition f l)) ==> f x)
                /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                /\ (forall x. mem x l = (mem x (fst (partition f l))
                                      || mem x (snd (partition f l)))))))
                     [SMTPat (partition f l)]

同様に、次は sorted_concat_lemma の改良された型です。 このとき、補題の性質を特化した項にのみ関連付けるよう、F* と SMT ソルバに支持します: その項は次のような形です。

sorted (append 11 (pivot::l2))

受け入れ可能な検証時間にするために、より特化したパターンを与えることで、SMT ソルバが補題をより区別して適用するようになります。

val sorted_concat_lemma: l1:list int{sorted l1}
                      -> l2:list int{sorted l2}
                      -> pivot:int
                      -> Lemma (requires ((forall y. mem y l1 ==> not (pivot <= y))
                                       /\ (forall y. mem y l2 ==> pivot <= y)))
                               (ensures (sorted (append l1 (pivot::l2))))
                         [SMTPat (sorted (append l1 (pivot::l2)))]

最後に、同じ方法で append_mem の型も改良します:

val append_mem:  l1:list 'a
              -> l2:list 'a
              -> Lemma (requires True)
                       (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
                       [SMTPat (append l1 l2)]
let rec append_mem l1 l2 = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2

Remark. SMTPat は注意深く使ってください! もし悪いパターンを指定すると、検証エンジンは予測できないパフォーマンスになってしまいます。 SMTPat の詳細を理解するために、SMT ソルバの量化に対するパターン (別名、トリガー) を少し研究しなければなりません。

これらの改良されたシグニチャを使って、元に行なっていたのと同じ sort を書き、その関数に望んだ型を与えることができます。 SMT ソルバは与えた補題から必要な性質を暗黙的に導出します。

let cmp i j = i <= j
val sort: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l = mem i m)})
                            (decreases (length l))
let rec sort l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (cmp pivot) tl in
    append (sort lo) (pivot::sort hi)

6.1.4. 練習問題

練習問題 6b:
(次に与える) 実装からはじめて、単なる整数のリストの代わりに任意の要素の型を持つリストで動作できるように、sort を一般化してください。 それが正しいことを証明してください。

(* "エディタに読み込む" リンクのコードからはじめてください *)

エディタに読み込む

回答
module QuickSortPoly


val mem: 'a -> list 'a -> Tot bool
let rec mem a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl


val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2


val append_mem:  l1:list 'a
              -> l2:list 'a
              -> Lemma (requires True)
                       (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
                       [SMTPat (append l1 l2)]
let rec append_mem l1 l2 = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2


val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl


(* Specification of sortedness according to some comparison function f *)
val sorted: ('a -> 'a -> Tot bool) -> list 'a -> Tot bool
let rec sorted f l = match l with
    | [] -> true
    | [x] -> true
    | x::y::xs -> f x y && sorted f (y::xs)


val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2


val partition_lemma: f:('a -> Tot bool)
   -> l:list 'a
   -> Lemma (requires True)
            (ensures ((length (fst (partition f l))
                     + length (snd (partition f l)) = length l
                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                  /\ (forall x. mem x l = (mem x (fst (partition f l))
                                        || mem x (snd (partition f l)))))))
            [SMTPat (partition f l)]
let rec partition_lemma f l = match l with
    | [] -> ()
    | hd::tl -> partition_lemma f tl


(* Defining a new predicate symbol *)
opaque type total_order (a:Type) (f: (a -> a -> Tot bool)) =
    (forall a. f a a)                                           (* reflexivity   *)
    /\ (forall a1 a2. (f a1 a2 /\ a1<>a2)  <==> not (f a2 a1))  (* anti-symmetry *)
    /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)        (* transitivity  *)

val sorted_concat_lemma: f:('a -> 'a -> Tot bool)
                      -> l1:list 'a{sorted f l1}
                      -> l2:list 'a{sorted f l2}
                      -> pivot:'a
                      -> Lemma (requires (total_order 'a f
                                       /\ (forall y. mem y l1 ==> not (f pivot y))
                                       /\ (forall y. mem y l2 ==> f pivot y)))
                               (ensures (sorted f (append l1 (pivot::l2))))
                               [SMTPat (sorted f (append l1 (pivot::l2)))]
let rec sorted_concat_lemma f l1 l2 pivot = match l1 with
    | [] -> ()
    | hd::tl -> sorted_concat_lemma f tl l2 pivot


val sort: f:('a -> 'a -> Tot bool){total_order 'a f}
       -> l:list 'a
       -> Tot (m:list 'a{sorted f m /\ (forall i. mem i l = mem i m)})
              (decreases (length l))
let rec sort f l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (f pivot) tl in
    append (sort f lo) (pivot::sort f hi)

エディタに読み込む

練習問題 6c:
sort の仕様は不完全です。 なぜですか? 上記と同じ仕様を持ち、けれどリストのいくつかの要素を捨ててしまうような sort の変種を書けますか?

(* "エディタに読み込む" リンクのコードからはじめてください *)

エディタに読み込む

回答

この仕様は結果のリストが最初のリストの置換であることを保証していません: この仕様は要素を捨てたり繰り返したりすることができてしまいます。

module QuickSortPoly


val mem: 'a -> list 'a -> Tot bool
let rec mem a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl


(* append now duplicates the elements of the first list *)
val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: hd :: append tl l2


val append_mem:  l1:list 'a
              -> l2:list 'a
              -> Lemma (requires True)
                       (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
                       [SMTPat (append l1 l2)]
let rec append_mem l1 l2 = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2


val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl


val sorted: list int -> Tot bool
let rec sorted l = match l with
    | [] -> true
    | [x] -> true
    | x::y::xs -> x <= y && sorted (y::xs)


val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2


val partition_lemma: f:('a -> Tot bool)
                   -> l:list 'a
                   -> Lemma (requires True)
                            (ensures ((length (fst (partition f l)) + length (snd (partition f l)) = length l
                                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                                  /\ (forall x. mem x l = (mem x (fst (partition f l)) || mem x (snd (partition f l)))))))
                            [SMTPat (partition f l)]
let rec partition_lemma f l = match l with
    | [] -> ()
    | hd::tl -> partition_lemma f tl


val sorted_concat_lemma: l1:list int{sorted l1}
                      -> l2:list int{sorted l2}
                      -> pivot:int
                      -> Lemma (requires ((forall y. mem y l1 ==> not (pivot <= y))
                                       /\ (forall y. mem y l2 ==> pivot <= y)))
                               (ensures (sorted (append l1 (pivot::l2))))
                               [SMTPat (sorted (append l1 (pivot::l2)))]
let rec sorted_concat_lemma l1 l2 pivot = match l1 with
    | [] -> ()
    | hd::tl -> sorted_concat_lemma tl l2 pivot


opaque type match_head (l1:list int) (l2:list int) =
  (l1 = [] /\ l2 = []) \/
  (exists h t1 t2. l1 = h::t1 /\ l2 = h::t2)

val dedup: l:list int{sorted l} -> Tot (l2:list int{sorted l2 /\ (forall i. mem i l = mem i l2) /\ match_head l l2})
  let rec dedup l =
    match l with
    | [] -> []
    | [x] -> [x]
    | h::h2::t ->
      if h = h2 then dedup (h2::t)
      else  h::dedup (h2::t)


let cmp i j = i <= j
val sort: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l = mem i m)})
                            (decreases (length l))
let rec sort l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (cmp pivot) tl in
    let l' = append (sort lo) (pivot::sort hi) in
    dedup l'

エディタに読み込む

練習問題 6d:
この仕様を修正して、sort がリスト中のどのような要素も捨てないことを保証してください。 sort がこの仕様に合致することを証明してください。

(* この問題か練習問題 6b の答からはじめてください *)

エディタに読み込む

回答
module QuickSortNoDiscard


(* Instead of a Boolean check that an element belongs to a list, count
the number of occurrences of an element in a list *)
val count : 'a -> list 'a -> Tot nat
let rec count (x:'a) (l:list 'a) = match l with
  | hd::tl -> if hd=x then 1 + count x tl else count x tl
  | [] -> 0

let mem x l = count x l > 0


val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2


val append_count: l:list 'a -> m:list 'a
               -> Lemma (requires True)
                        (ensures (forall x. count x (append l m) = (count x l + count x m)))
let rec append_count l m = match l with
  | [] -> ()
  | hd::tl -> append_count tl m


val append_mem: l:list 'a -> m:list 'a
               -> Lemma (requires True)
                        (ensures (forall x. mem x (append l m) = (mem x l || mem x m)))
let append_mem l m = append_count l m


val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl


(* Specification of sortedness according to some comparison function f *)
val sorted: ('a -> 'a -> Tot bool) -> list 'a -> Tot bool
let rec sorted f l = match l with
    | [] -> true
    | [x] -> true
    | x::y::xs -> f x y && sorted f (y::xs)


val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2


val partition_lemma: f:('a -> Tot bool)
                   -> l:list 'a
                   -> Lemma (requires True)
                            (ensures ((length (fst (partition f l)) + length (snd (partition f l)) = length l
                                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                                  /\ (forall x. mem x l = (mem x (fst (partition f l)) || mem x (snd (partition f l))))
                                  /\ (forall x. count x l = (count x (fst (partition f l)) + count x (snd (partition f l)))))))
let rec partition_lemma f l = match l with
    | [] -> ()
    | hd::tl -> partition_lemma f tl


(* Defining a new predicate symbol *)
opaque type total_order (a:Type) (f: (a -> a -> Tot bool)) =
    (forall a. f a a)                                           (* reflexivity   *)
    /\ (forall a1 a2. (f a1 a2 /\ a1<>a2)  <==> not (f a2 a1))  (* anti-symmetry *)
    /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)        (* transitivity  *)

val sorted_concat_lemma: a:Type
                      -> f:(a -> a -> Tot bool)
                      -> l1:list a{sorted f l1}
                      -> l2:list a{sorted f l2}
                      -> pivot:a
                      -> Lemma (requires (total_order a f
                                       /\ (forall y. mem y l1 ==> not (f pivot y))
                                       /\ (forall y. mem y l2 ==> f pivot y)))
                               (ensures (sorted f (append l1 (pivot::l2))))
let rec sorted_concat_lemma f l1 l2 pivot = match l1 with
    | [] -> ()
    | hd::tl -> sorted_concat_lemma f tl l2 pivot


val sort: f:('a -> 'a -> Tot bool){total_order 'a f}
       -> l:list 'a
       -> Tot (m:list 'a{sorted f m /\ (forall i. mem i l = mem i m) /\ (forall i. count i l = count i m)})
              (decreases (length l))
let rec sort f l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (f pivot) tl in
    partition_lemma (f pivot) tl;
    let lo' = sort f lo in
    let hi' = sort f hi in
    append_count lo' (pivot::hi');
    append_mem lo' (pivot::hi');
    sorted_concat_lemma f lo' hi' pivot;
    append lo' (pivot::hi')

エディタに読み込む

練習問題 6e:
挿入ソートを実装し、同じ性質を証明してください。

val sort : l:list int -> Tot (m:list int{sorted m /\ (forall x. mem x l == mem x m)})

エディタに読み込む

回答
module InsertionSort
open Prims.PURE

(* Check that a list is sorted *)
val sorted: list int -> Tot bool
let rec sorted l = match l with
    | [] -> true
    | [x] -> true
    | x::y::xs -> (x <= y) && (sorted (y::xs))

(* Definition of the [mem] function *)
val mem: int -> list int -> Tot bool
let rec mem a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl

(* A lemma to help Z3 *)
val sorted_smaller: x:int
                ->  y:int
                ->  l:list int
                ->  Lemma (requires (sorted (x::l) /\ mem y l))
                          (ensures (x <= y))
                          [SMTPat (sorted (x::l)); SMTPat (mem y l)]
let rec sorted_smaller x y l = match l with
    | [] -> ()
    | z::zs -> if z=y then () else sorted_smaller x y zs

(* Insertion function *)
val insert : i:int -> l:list int{sorted l} -> Tot (m:list int{sorted m /\ (forall x. mem x m <==> x==i \/ mem x l)})
let rec insert i l = match l with
  | [] -> [i]
  | hd::tl ->
     if i <= hd then
       i::l
     else
       (* Solver implicitly uses the lemma: sorted_smaller hd (Cons.hd i_tl) tl *)
       hd::(insert i tl)

(* Insertion sort *)
val sort : l:list int -> Tot (m:list int{sorted m /\ (forall x. mem x l == mem x m)})
let rec sort l = match l with
    | [] -> []
    | x::xs -> insert x (sort xs)

エディタに読み込む

7. ケーススタディ: 単純型付きラムダ計算

ここでより大きなケーススタディを見てみましょう: 単純型付きラムダ計算 (STLC) に対する型検査の健全性を証明します。 もし STLC に馴染みがなければ、Software Foundations 本 (日本語訳) を参照して、その原文のやさしい導入を読むことができます (Coq に関する部分は無視することができます)。 ここでのその形式化と証明は Software Foundations に密接に従います。 けれども私達の証明は Coq の証明よりも短かく、より読み易いでしょう。

7.1. 構文

F* の帰納データ型 ty で STLC の型を表わしましょう。

type ty =
  | TBool  : ty
  | TArrow : ty -> ty -> ty

唯一の基本型 (TBool) としてブールを考えます。 関数型は2つの型引数を取る TArrow コンストラクタで表わされます。 例えば TArrow TBool TBool と書くと、ブールを引数に取りブールを返す関数の型を表わします。 これは F* の構文では bool -> bool と書き、論文表記では $\mathsf{bool} \to \mathsf{bool}$ と書きます。

データ型 exp による STLC の式を表わしましょう。

type exp =
  | EVar   : int -> exp
  | EApp   : exp -> exp -> exp
  | EAbs   : int -> ty -> exp -> exp
  | ETrue  : exp
  | EFalse : exp
  | EIf    : exp -> exp -> exp -> exp

変数はコンストラクタ EVar で修飾された整数の “名前” として表わされます。 変数はラムダ抽象 (EAbs) によって “束縛され” ます。 例えば、ブールの恒等関数は EAbs 0 TBool (EVar 0) と書けます。 論文表記ではこの関数を $(\lambda x:\mathsf{bool}.~x)$ と書きます。 引数 (TBool) の型注釈はとても単純な型検査を許します。 単純にするために、ここれでは型推論を考えていません。 恒等関数を ETrue 定数に適用する式は次のように書きます:

EApp (EAbs 0 TBool (EVar 0)) ETrue

(論文表記では $(\lambda x:\mathsf{bool}.~x)~\mathsf{true}$ になります。)

この言語は条件分岐 (if-then-else) も持っています。 例えば、ブールの “否定” 関数は次のように書けます:

EAbs 0 TBool (EIf (EVar 0) EFalse ETrue)

(論文表記では $\lambda x:\mathsf{bool}.~\mathsf{if }~x~\mathsf{ then~false~else~true}$ になります。)

7.2. 操作的意味論

STLC の標準的なスモールステップ値渡しインタープリタを定義しましょう。 式の評価に成功した最終結果は と呼ばれます。 is_value を定義して、関数とブール定数は値であると主張しましょう。 これは式に対するブールの述語 (全域関数) です:

val is_value : exp -> Tot bool
let is_value e =
  match e with
  | EAbs _ _ _
  | ETrue
  | EFalse     -> true
  | _          -> false

EAbs, ETrue, EFalse のケースは同じ右辺 (true) を共有しています。 これは定義の重複を防止する方法の1つです。

関数適用に意味論を与えるために、e' 中の xe で置換する関数 subst x e e' を定義しましょう:

val subst : int -> exp -> exp -> Tot exp
let rec subst x e e' =
  match e' with
  | EVar x' -> if x = x' then e else e'
  | EAbs x' t e1 ->
      EAbs x' t (if x = x' then e1 else (subst x e e1))
  | EApp e1 e2 -> EApp (subst x e e1) (subst x e e2)
  | ETrue -> ETrue
  | EFalse -> EFalse
  | EIf e1 e2 e3 -> EIf (subst x e e1) (subst x e e2) (subst x e e3)

その式を横断して、変数 (EVar x') に辿り着いたらそれが置換したい変数 x かどうかチェックし、もしそうならそれを e で置換します。 ラムダ抽象 (EAbs x' t e1) に対して、もし xx' が異なっていたら本体 e1 の中のみを置換します; もしそれらが同じならその本体を変更しません。 その理由は e1 中の x はラムダ抽象によって束縛されているからです: それは、単にたまたまグローバルな名前 x と同じ綴りである新しいローカルな名前です。 ローカルな x でシャドウイングされているため、グローバルな x はこのスコープではアクセスできません。 他のケースは簡単です。

上級者への注意: 全ての変数が外のラムダで束縛された閉じた式のみを簡約するので、(実際閉じた値の) 閉じた式のみを置換します。 それには置換のこのナイーブな定義は十分です。 もし他の式中の値を置換する式 e が自由変数を含むような場合を考慮するなら、置換がより複雑になるか値の表現を変更しなければなりません。

値の定義と置換の定義が与えられたので、これでスモールステップインタープリタを定義できます。 そのインタープリタの関数 step は式 e を取り、e をシングルステップに簡約した式を返すか、エラーの場合には None を返します。 (この言語における全てのエラーは型エラーで、これは型システムによって静的に防止されます。)

val step : exp -> Tot (option exp)
let rec step e =
  match e with
  | EApp e1 e2 ->
      if is_value e1 then
        if is_value e2 then
          match e1 with
          | EAbs x t e' -> Some (subst x e2 e')
          | _           -> None
        else
          match (step e2) with
          | Some e2' -> Some (EApp e1 e2')
          | None     -> None
      else
        (match (step e1) with
        | Some e1' -> Some (EApp e1' e2)
        | None     -> None)
  | EIf e1 e2 e3 ->
      if is_value e1 then
        match e1 with
        | ETrue   -> Some e2
        | EFalse  -> Some e3
        | _       -> None
      else
        (match (step e1) with
        | Some e1' -> Some (EIf e1' e2 e3)
        | None     -> None)
  | _ -> None

適用の式 EApp e1 e2 を複数のステップで実行します。 最初に e1 を値に簡約し、それから e2 を値に簡約し、そしてもし e1 が抽象 EAbs x t e' であるなら形式的な引数 x を実際の引数 e2 で置換して続きます。 もしそうでなければ、None を返すことで (関数でない値を引数に適用したという) 動的な型エラーを発生させます。 EIf e1 e2 e3 について、最初にガード e1 を簡約し: もしそのガードが true に簡約されたら e2 の簡約を続行し、 もしそのガードが false に簡約されたら e3 の簡約を続行し、 そしてもしそのガードがそれ以外 (例えば関数) に簡約されたら動的な型エラーを報告します。 None -> None の場合はエラーをトップレベルに伝搬させます。

assert (step (EApp (EAbs 0 TBool (EVar 0))) ETrue)) = Some ETrue)
assert (step (EApp ETrue ETrue) = None)

7.3. 型検査器

型を項に割り当てるために、自由変数の型についての仮定を知る必要があります。 そのため型環境に対して型付けが発生しますスコープでの値からそれらの型への写像です。 整数の変数名を取りオプショナルな型を返す関数として、そのような部分写像を表わしましょう:

type env = int -> Tot (option ty)

空の環境、すなわち最初にスコープに値がないような環境、における閉じた項の型検査からはじめましょう。

val empty : env
let empty _ = None

束縛が起きると、その型環境を拡張します。

val extend : env -> int -> ty -> Tot env
let extend g x t x' = if x = x' then Some t else g x'

例えば、環境 extend g x t において本体 e を最初に型検査することで、型環境 g において EAbs x t e を型検査します。

型検査器は環境 g と式 e を取る全域関数で、e の型もしくは、e の型が正しくないなら None を生成します。

val typing : env -> exp -> Tot (option ty)
let rec typing g e =
  match e with
  | EVar x -> g x
  | EAbs x t e1 ->
      (match typing (extend g x t) e1 with
      | Some t' -> Some (TArrow t t')
      | None    -> None)
  | EApp e1 e2 ->
      (match typing g e1, typing g e2 with
      | Some (TArrow t11 t12), Some t2 -> if t11 = t2 then Some t12 else None
      | _                    , _       -> None)
  | ETrue  -> Some TBool
  | EFalse -> Some TBool
  | EIf e1 e2 e3 ->
      (match typing g e1, typing g e2, typing g e3 with
      | Some TBool, Some t2, Some t3 -> if t2 = t3 then Some t2 else None
      | _         , _      , _       -> None)

変数は単純に環境から検索されます。 抽象 EAbs x t e1 に対して、上記で説明したように、環境 extend g x t の下で本体 e1 を型検査します。 もしそれが成功して型 t' を生成したら、全体の抽象には型 TArrow t t' が与えられます。 適用 EApp e1 e2 に対して、e1e2 を別々に型検査します。 そしてもし e1 が関数型 TArrow t11 t12 を持ちかつ e2 が型 t11 を持つなら、全体の適用は型 t12 を持ちます。 ETrueEFalse は型 TBool を持ちます。 条件分岐に対して、そのガードが型 TBool を持ちかつ2つのブランチが同じ型を持つことを要求します。 そしてまたこのブランチの型は条件分岐の型です。

7.4. 健全性の証明

STLC のために progress と preservation を証明しましょう。 progress 定理は、閉じた型が正しい項が (直接に) 動的な型エラーを生成しないことを示します: 型が正しい項は値であるか、評価ステップを取れます。 その証明は実直な帰納になります。

val progress : e:exp -> Lemma
      (requires (is_Some (typing empty e)))
      (ensures (is_value e \/ (is_Some (step e))))
let rec progress e =
  match e with
  | EApp e1 e2 -> progress e1; progress e2
  | EIf e1 e2 e3 -> progress e1; progress e2; progress e3
  | _ -> ()

Variables are not well-typed in the empty environment, so the theorem holds vacuously for variables. Boolean constants and abstractions are values, so the theorem holds trivially for these. All these simple cases are proved automatically by F*. For the remaining cases we need to use the induction hypothesis, but otherwise the proofs are fully automated. Under the hood F* and Z3 are doing quite a bit of work though.

In case e = (EApp e1 e2) F* and Z3 automate the following intuitive argument: We case split on the first instance of the induction hypothesis (is_value e1 \/ (is_Some (step e1))).

The intuitive proof of the EIf case is similar.

The preservation theorem (sometimes also called “subject reduction”) states that when a well-typed expression takes a step, the result is a well-typed expression of the same type. In order to show preservation we need to prove a couple of auxiliary results for reasoning about variables and substitution.

The case for function application has to reason about “beta reduction” steps, i.e. substituting the formal argument of a function with an actual value. To see that this step preserves typing, we need to know that the substitution itself does. So we prove a substitution lemma, stating that substituting a (closed) term v for a variable x in an expression e preserves the type of e. The tricky cases in the substitution proof are the ones for variables and for function abstractions. In both cases, we discover that we need to take an expression e that has been shown to be well-typed in some context g and consider the same expression e in a slightly different context g'. For this we prove a context invariance lemma, showing that typing is preserved under “inessential changes” to the context gin particular, changes that do not affect any of the free variables of the expression. For this, we need a definition of the free variables of an expressioni.e., the variables occurring in the expression that are not bound by an abstraction.

A variable x appears free in e if e contains some occurrence of x that is not under an abstraction labeled x:

val appears_free_in : x:int -> e:exp -> Tot bool
let rec appears_free_in x e =
  match e with
  | EVar y -> x = y
  | EApp e1 e2 -> appears_free_in x e1 || appears_free_in x e2
  | EAbs y _ e1 -> x <> y && appears_free_in x e1
  | EIf e1 e2 e3 ->
      appears_free_in x e1 || appears_free_in x e2 || appears_free_in x e3
  | ETrue
  | EFalse -> false

We also need a technical lemma connecting free variables and typing contexts. If a variable x appears free in an expression e, and if we know that e is well typed in context g, then it must be the case that g assigns some type to x.

val free_in_context : x:int -> e:exp -> g:env -> Lemma
      (requires (is_Some (typing g e)))
      (ensures (appears_free_in x e ==> is_Some (g x)))
let rec free_in_context x e g =
  match e with
  | EVar _
  | ETrue
  | EFalse -> ()
  | EAbs y t e1 -> free_in_context x e1 (extend g y t)
  | EApp e1 e2 -> free_in_context x e1 g; free_in_context x e2 g
  | EIf e1 e2 e3 -> free_in_context x e1 g;
                    free_in_context x e2 g; free_in_context x e3 g

The proof is a straightforward induction. As a corollary for g=empty we obtain that expressions typable in the empty environment have no free variables.

val typable_empty_closed : x:int -> e:exp -> Lemma
      (requires (is_Some (typing empty e)))
      (ensures (not(appears_free_in x e)))
      [SMTPat (appears_free_in x e)]
let typable_empty_closed x e = free_in_context x e empty

The quantifier pattern [SMTPat (appears_free_in x e)] signals F* that it should feed this lemma to the SMT solver using this pattern.

Sometimes, we know that typing g e = Some t, and we will need to replace g by an “equivalent” context g'. We still need to define formally when two environments are equivalent. A natural definition is extensional equivalence of functions:

opaque logic type Equal (g1:env) (g2:env) =
                 (forall (x:int). g1 x = g2 x)

According to this definition two environments are equivalent if have the same domain and they map all variables in the domain to the same type. We remark Equal in particular and logical formulas in general are “types” in F*, thus the different syntax for this definition.

The context invariance lemma uses in fact a weaker variant of this equivalence in which the two environments only need to agree on the variables that appear free in an expression e:

opaque logic type EqualE (e:exp) (g1:env) (g2:env) =
                 (forall (x:int). appears_free_in x e ==> g1 x = g2 x)

The context invariance lemma is then easily proved by induction:

val context_invariance : e:exp -> g:env -> g':env
                     -> Lemma
                          (requires (EqualE e g g'))
                          (ensures (typing g e == typing g' e))
let rec context_invariance e g g' =
  match e with
  | EAbs x t e1 ->
     context_invariance e1 (extend g x t) (extend g' x t)

  | EApp e1 e2 ->
     context_invariance e1 g g';
     context_invariance e2 g g'

  | EIf e1 e2 e3 ->
     context_invariance e1 g g';
     context_invariance e2 g g';
     context_invariance e3 g g'

  | _ -> ()

Because Equal is a stronger relation than EqualE we obtain the same property for Equal:

val typing_extensional : g:env -> g':env -> e:exp -> Lemma
                           (requires (Equal g g'))
                           (ensures (typing g e == typing g' e))
let typing_extensional g g' e = context_invariance e g g'

We can use these results to show the following substitution lemma:

val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
      g:env -> Lemma
        (requires ( is_Some (typing empty v) /\
              is_Some (typing (extend g x (Some.v (typing empty v))) e)))
        (ensures (is_Some (typing empty v) /\
                  typing g (subst x v e) ==
                  typing (extend g x (Some.v (typing empty v))) e))
let rec substitution_preserves_typing x e v g =
  let Some t_x = typing empty v in
  let gx = extend g x t_x in
  match e with
  | ETrue -> ()
  | EFalse -> ()
  | EVar y ->
     if x=y
     then context_invariance v empty g (* uses lemma typable_empty_closed *)
     else context_invariance e gx g

  | EApp e1 e2 ->
     substitution_preserves_typing x e1 v g;
     substitution_preserves_typing x e2 v g

  | EIf e1 e2 e3 ->
     substitution_preserves_typing x e1 v g;
     substitution_preserves_typing x e2 v g;
     substitution_preserves_typing x e3 v g

  | EAbs y t_y e1 ->
     let gxy = extend gx y t_y in
     let gy = extend g y t_y in
     if x=y
     then typing_extensional gxy gy e1
     else
       (let gyx = extend gy x t_x in
        typing_extensional gxy gyx e1;
        substitution_preserves_typing x e1 v gy)

The proof proceeds by induction on the expression e; we give the intuition of the two most interesting cases:

We now have the tools we need to prove preservation: if a closed expression e has type t and takes an evaluation step to e', then e' is also a closed expression with type t. In other words, the small-step evaluation relation preserves types.

val preservation : e:exp -> Lemma
        (requires(is_Some (typing empty e) /\ is_Some (step e) ))
        (ensures(is_Some (step e) /\
                 typing empty (Some.v (step e)) == typing empty e))
let rec preservation e =
  match e with
  | EApp e1 e2 ->
     if is_value e1
     then (if is_value e2
           then let EAbs x _ ebody = e1 in
                substitution_preserves_typing x ebody e2 empty
           else preservation e2)
     else preservation e1

  | EIf e1 _ _ ->
      if not (is_value e1) then preservation e1

We only have two cases to consider, since only applications and conditionals can take successful execution steps. The case for e = EIf e1 e2 e3 is simple: either e1 is a value and thus the conditional reduces to e2 or e3 which by the typing hypothesis also have type t, or e1 takes a successful step and we can apply the induction hypothesis. We use the Some.v projector for options with the following type:

  Some.v : x:(option 'a){is_Some x} -> Tot 'a

which requires F* to prove that indeed e1 can take a step; this is immediate since we know that the whole conditional takes a step and we know that e1 is not a value.

The case for e = EApp e1 e2 is a bit more complex. If e1 steps or if e1 is a value and e2 steps then we just apply the induction hypothesis. If both e1 and e2 are values it needs to be the case that e1 is an abstraction EAbs x targ ebody and step e = subst x e2 ebody. From the typing assumption we have typing (extend empty x tags) ebody = Some t and typing empty e2 = Some targ, so we can use the substitution lemma to obtain that typing empty (subst x e2 ebody) = Some t, which concludes the proof.

7.5. Exercises for STLC

練習問題 7a:
Define a typed_step step function that takes a well-typed expression e that is not a value and produces the expression to which e steps. Give typed_step the following strong type (basically this type captures both progress and preservation):

  val typed_step : e:exp{is_Some (typing empty e) /\ not(is_value e)} ->
                   Tot (e':exp{typing empty e' = typing empty e})

エディタに読み込む

(Hint: the most direct solution to this exercise fits on one line)

回答
    let typed_step e = progress e; preservation e; Some.v (step e)

エディタに読み込む

練習問題 7b:
To add pairs to this formal development we add the following to the definition of types, expressions, values, substitution, and step:

type ty =
  ...
  | TPair : ty -> ty -> ty

type exp =
  ...
  | EPair  : exp -> exp -> exp
  | EFst   : exp -> exp
  | ESnd   : exp -> exp

エディタに読み込む

(note the extra rec in is_value below!)

let rec is_value e =
  match e with
  ...
  | EPair e1 e2 -> is_value e1 && is_value e2

let rec subst x e e' =
  match e' with
  ...
  | EPair e1 e2 -> EPair (subst x e e1) (subst x e e2)
  | EFst e1 -> EFst (subst x e e1)
  | ESnd e1 -> ESnd (subst x e e1)

let rec step e =
  ...
  | EPair e1 e2 ->
      if is_value e1 then
        if is_value e2 then None
        else
          (match (step e2) with
          | Some e2' -> Some (EPair e1 e2')
          | None     -> None)
      else
        (match (step e1) with
        | Some e1' -> Some (EPair e1' e2)
        | None     -> None)
  | EFst e1 ->
      if is_value e1 then
        (match e1 with
        | EPair v1 v2 -> Some v1
        | _           -> None)
      else
        (match (step e1) with
        | Some e1' -> Some (EFst e1')
        | None     -> None)
  | ESnd e1 ->
      if is_value e1 then
        (match e1 with
        | EPair v1 v2 -> Some v2
        | _           -> None)
      else
        (match (step e1) with
        | Some e1' -> Some (ESnd e1')
        | None     -> None)

エディタに読み込む

Add cases to typing for the new constructs and fix all the proofs.

回答

We extend the typing and appears_free_in functions with cases for EPair, EFst, and ESnd:

val typing : env -> exp -> Tot (option ty)
let rec typing g e =
...
  | EPair e1 e2 ->
      (match typing g e1, typing g e2 with
      | Some t1, Some t2 -> Some (TPair t1 t2)
      | _      , _       -> None)
  | EFst e1 ->
      (match typing g e1 with
      | Some (TPair t1 t2) -> Some t1
      | _                  -> None)
  | ESnd e1 ->
      (match typing g e1 with
      | Some (TPair t1 t2) -> Some t2
      | _                  -> None)

val appears_free_in : x:int -> e:exp -> Tot bool
...
  | EPair e1 e2 -> appears_free_in x e1 || appears_free_in x e2
  | EFst e1 -> appears_free_in x e1
  | ESnd e1 -> appears_free_in x e1

エディタに読み込む

The proofs of the lemmas are also easy to extend by just calling the induction hypothesis:

val free_in_context : x:int -> e:exp -> g:env -> Lemma
      (requires (is_Some (typing g e)))
      (ensures (appears_free_in x e ==> is_Some (g x)))
let rec free_in_context x e g =
...
  | EPair e1 e2 -> free_in_context x e1 g; free_in_context x e2 g
  | EFst e1
  | ESnd e1 -> free_in_context x e1 g

val context_invariance : e:exp -> g:env -> g':env
                     -> Lemma
                          (requires (EqualE e g g'))
                          (ensures (typing g e == typing g' e))
let rec context_invariance e g g' =
...
| EPair e1 e2 ->
     context_invariance e1 g g';
     context_invariance e2 g g'

  | EFst e1
  | ESnd e1 -> context_invariance e1 g g'

val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
      g:env{is_Some (typing empty v) &&
            is_Some (typing (extend g x (Some.v (typing empty v))) e)} ->
      Tot (u:unit{typing g (subst x v e) ==
                  typing (extend g x (Some.v (typing empty v))) e})
let rec substitution_preserves_typing x e v g =
...
  | EPair e1 e2 ->
     (substitution_preserves_typing x e1 v g;
      substitution_preserves_typing x e2 v g)

  | EFst e1
  | ESnd e1 ->
      substitution_preserves_typing x e1 v g

エディタに読み込む

As for the other cases, the preservation proof when e = EPair e1 e2 follows the structure of the step function. If e1 is not a value then it further evaluates, so we apply the induction hypothesis to e1. If e1 is a value, then since we know that the pair evaluates, it must be the case that e2 is not a value and further evaluates, so we apply the induction hypothesis to it. The cases for EFst and ESnd are similar.

val preservation : e:exp{is_Some (typing empty e) /\ is_Some (step e)} ->
      Tot (u:unit{typing empty (Some.v (step e)) == typing empty e})
let rec preservation e =
...
  | EPair e1 e2 ->
      (match is_value e1, is_value e2 with
      | false, _     -> preservation e1
      | true , false -> preservation e2)

  | EFst e1
  | ESnd e1 ->
      if not (is_value e1) then preservation e1

エディタに読み込む

練習問題 7c:
We want to add a let construct to this formal development. We add the following to the definition of expressions:

type exp =
  ...
  | ELet  : int -> exp -> exp -> exp

エディタに読み込む

Add cases for ELet to all definitions and proofs.

Load answer in editor

練習問題 7d:
Define a big-step interpreter for STLC as a recursive function eval that given a well-typed expression e either produces the well-typed value v to which e evaluates or it diverges if the evaluation of e loops. Give eval the following strong type ensuring that v has the same type as e (basically this type captures both progress and preservation):

  val eval : e:exp{is_Some (typing empty e)} ->
             Dv (v:exp{is_value v && typing empty v = typing empty e})

エディタに読み込む

The Dv effect is that of potentially divergent computations. We cannot mark this as Tot since a priori STLC computations could loop, and it is hard to prove that well-typed ones don't, while defining an interpreter.

回答

Here is a solution that only uses typed_step (suggested by Santiago Zanella):

val eval : e:exp{is_Some (typing empty e)} ->
           Dv (v:exp{is_value v && typing empty v = typing empty e})
let rec eval e =
  if is_value e then e
  else eval (typed_step e)

エディタに読み込む

or using the progress and preservation lemmas instead of typed_step (suggested by Guido Martinez):

val eval : e:exp{is_Some (typing empty e)} ->
  Dv (v:exp{is_value v && typing empty v = typing empty e})
let rec eval e = match step e with
  | None -> progress e; e
  | Some e' -> preservation e; eval e'

Here is another solution that only uses the substitution lemma:

val eval' : e:exp{is_Some (typing empty e)} ->
            Dv (v:exp{is_value v && typing empty v = typing empty e})
let rec eval' e =
  let Some t = typing empty e in
  match e with
  | EApp e1 e2 ->
     (let EAbs x _ e' = eval' e1 in
      let v = eval' e2 in
      substitution_preserves_typing x e' v empty;
      eval' (subst x v e'))
  | EAbs _ _ _
  | ETrue
  | EFalse     -> e
  | EIf e1 e2 e3 ->
     (match eval' e1 with
      | ETrue  -> eval' e2
      | EFalse -> eval' e3)
  | EPair e1 e2 -> EPair (eval' e1) (eval' e2)
  | EFst e1 ->
     let EPair v1 _ = eval' e1 in v1
  | ESnd e1 ->
     let EPair _ v2 = eval' e1 in v2
  | ELet x e1 e2 ->
     (let v = eval' e1 in
      substitution_preserves_typing x e2 v empty;
      eval' (subst x v e2))

エディタに読み込む

8. Higher kinds, indexed types, implicit arguments, and type-level functions

So far, we have mostly programmed total functions and give them specifications using rich types. Under the covers, F* has a second level of checking at work to ensure that the specifications that you write are also meaningfulthis is F*'s kind system. Before moving on to more advanced F* features, you'll have to understand the kind system a little. In short, just as types describe properties of programs, kinds describe properties of types.

8.1. Type: The type of types

The basic construct in the kind system is the constant Type, which is the basic type of a type. For example, just as we say that 0 : int (zero has type int), we also say int : Type (int has kind Type), bool : Type, nat : Type etc.

8.2. Arrow kinds

Beyond the base types, consider types like list int, list bool etc. These are also types, of course, and in F* list int : Type and list bool : Type. But, what about the unapplied type constructor listit's not a Type on its own; it only produces a Type when applied to a Type. In that sense, list is type constructor. To describe this, just as we use the -> type constructor to describe functions at the level of programs, we use the -> kind constructor to describe functions at the level of types. As such, we write list : Type -> Type, meaning that it produces a Type when applied to a Type.

8.3. Indexed types and implicit arguments

Beyond inductive types like list, F* also supports inductive type families, or GADTs. For example, here is one definition of a vector, a length-indexed list.

type vector : Type -> nat -> Type =
   | Nil :  vector 'a 0
   | Cons : hd:'a -> n:nat -> tl:vector 'a n -> vector 'a (n + 1)

Here, we define a type constructor vector : Type -> nat -> Type, which takes two arguments: it produces a Type when applied first to a Type and then to a nat.

The point is to illustrate that just as functions at the level of programs may take either type- or term-arguments, types themselves can take either types or pure expressions as arguments.

8.3.1. Implicit arguments

When writing functions over terms with indexed types, it is convenient to mark some arguments as implicit, asking the type-checker to infer them rather than having to provide them manually.

For example, the type of a function that reverses a vector can be written as follows:

val reverse_vector: #a:Type -> #n:nat -> vector a n -> Tot (vector a n)

This indicates that reverse_vector expects three arguments, but the # sign mark the first two arguments as implicit. Given a term v : vector t m, simply writing reverse_vector v will type-check as vector t minternally, F* elaborates the function call to reverse_vector #t #m v, instantiating the two implicit arguments automatically. To view what F* inferred, you can provide the --print_implicits argument to the compiler, which will cause all implicitly inferred arguments to be shown in any message from the compiler. Alternatively, you can write reverse_vector #t #m v yourself to force the choice of implicit arguments manually.

When you write a type like 'a -> M t wp (note the “ticked” variable 'a), this is simply syntactic sugar for #a:Type -> a -> M t wp, with every occurrence of 'a replaced by a in M t wpin other words, the “ticked” type variable is an implicit type argument. With this in mind, the definition of vector is desugared to:

type vector : Type -> nat -> Type =
   | Nil :  #a:Type -> vector a 0
   | Cons : #a:Type -> hd:a -> n:nat -> tl:vector a n -> vector a (n + 1)

One could go further and also define the Cons constructor's n argument to be implicit, like so:

type vector : Type -> nat -> Type =
   | Nil :  #a:Type -> vector a 0
   | Cons : #a:Type -> hd:a -> #n:nat -> tl:vector a n -> vector a (n + 1)

With this, given v: vector int m, we can write Cons 0 v to build a vector int (m + 1).

8.4. Dependent kind arrows and type function

Even some of the built-in type constructors can be given kinds. Consider the refinement type constructor: _:_{_}, whose instances include types we've seen before, like x:int{x >= 0}, which is the type nat, of course. With less syntactic sugar, you can view the type x:int{phi(x)} as the application of a type constructor refinement to two arguments int and a refinement formula fun x -> phi(x). As discussed in Section 3.5, the formula phi(x) is itself a Type. Thus, the kind of the refinement constructor is a:Type -> (a -> Type) -> Type, meaning it takes two arguments; first, a type a; then a second argument, a predicate on a (whose kind depends on a); and then bulids a Type.

The type fun x -> phi(x) is type function, a lambda abstraction at the level of types, which when applied to a particular value, say, 0, reduces as usual to phi(0).

8.5. Kind abbreviations

F* allows top-level declarations to define abbreviations for kinds. For example, one can write:

kind Predicate (a:Type) = a -> Type

Now, the kind Predicate a is an abbreviation for a -> Type.

9. Specifying effects

F* provides a mechanism to define new effects. As mentioned earlier, the system is already configured with several basic effects, including non-termination, state and exceptions. In this section, we look briefly at how effects are defined, using the PURE and STATE effects for illustration.

On a first reading, you may wish to skip this section and proceed directly to the next chapter.

9.1. Background: Generating compact verification conditions

Type inference in F* is based on a weakest pre-condition calculus for higher order programs. For every term e, F* computes WP e, which captures the semantics of e as a predicate transformer. If you want to prove some property P about the result of e (i.e., a post-condition), it suffices to prove WP e P of the initial configuration in which e is executed (i.e., a pre-condition).

Let's start by considering a very simple, purely functional programming language with only the following forms:

b ::= x | true | false
e ::= b | let x = e1 in e2 | assert b | if b then e1 else e2

For this tiny language, the post-conditions P that you may want to prove are predicates on the boolean results of a computation, while the pre-conditions are just propositions. Defining WP e for this language is fairly straightforward:

WP b P                      = P b
WP (let x = e1 in e2) P     = WP e1 (fun x -> WP e2 P)
WP (assert b) P             = b /\ P b
WP (if b then e1 else e2) P = (b ==> WP e1 P) /\ ((not b) ==> WP e2 P)

This is nice and simple, but it has a significant drawback, particularly in the fourth rule: the post-condition formula P is duplicated across the branches. As several branching expressions are sequenced, this leads to an exponential blowup in the size of the verification condition.

This problem with WP computations is well knownFlanagan and Saxe and Leino both study this problem and provide equivalent solutions. In essence, they show that for a first-order, assignment-free guarded command language the weakest pre-condition can be computed in a size nearly linear in the size of the program. Then, they show that first-order imperative WHILE language can be converted into SSA form and then into a guarded command language.

In the context of F*, we generalize the results of Flanagan and Saxe, and Leino, to the setting of a higher-order language. The main technical idea is a new “Double Dijkstra Monad. Given a program, F* infers a monadic computation type indexed by (1) a WP, the weakest pre-condition predicate transformer; and (2) a WLP, the weakest liberal pre-condition predicate transformer. Intuitively, WLP e Q is sufficient to guarantee that if e contains no internal assertion failures, then its result satisfies P; in contrast, the WP e P is sufficient to guarantee both that e's internal assertions succeed and that its result satisfies P.

Here's the definition of WLP for our small example langauge.

WLP b P                      = P b
WLP (let x = e1 in e2) P     = WLP e1 (fun x -> WLP e2 P)
WLP (assert b) P             = b ==> P b
WLP (if b then e1 else e2) P = (b ==> WLP e1 P) /\ ((not b) ==> WLP e2 P)

The only difference with the WP is in the case of assertions. For a WLP, rather than requiring a proof of the assertion, we try to prove the post-condition assuming the assertion succeeds.

How does this help us? Let's see.

First, you can prove the following property about WLP.

(Identity 1)
           WLP e P
      <==> forall x. P x \/ WLP e (fun y -> y <> x)

Here's one way to read formula (1): Proving that P is true of the typed result of a computation (the LHS) is equivalent to proving that for every x, we either have P x or we can prove that the result of the computation is not x (the RHS).

Armed with identity (1) above, we can also prove the following identity:

(Identity 2)
          WP e P
     <==> WP e (fun x -> True) /\ WLP e P
     <==> WP e (fun x -> True) /\ (forall x. P x \/ WLP e (fun y -> y <> x)) (by (1))

That is, in order to prove that a computation e has no internal assertion failures and produces a result satisfying P, one can equivalently prove (a) that e has no internal assertion failures (i.e., WP e (fun x -> True)) and then prove (b) that e's result satisfies P (i.e, WLP e P).

Finally, we come back to our rule for conditional expressions, which we can restate as follows (using identities (1) and (2)):

WP (if b then e1 else e2) P
=    (b ==> WP e1 (fun x -> True))
  /\ ((not b) ==> WP e2 (fun x -> True))
  /\ (forall y. P y \/ ((b ==> WLP e1 (fun x -> x<>y)
                     /\ (not b) ==> WLP e2 (fun x -> x<>y)))

In this form, the post-condition P is no longer duplicated across the branches of the computation and we avoid the exponential blowup (at the cost of computing both the WP and the WLP).

WPs and WLPs are convenient for type inferencefor loop- and recursion-free code, we can simply compute the most precise verification condition for a program without further annotation. However, programmers are often more comfortable writing specification in terms of pre- and post-conditions, rather than predicate transformers. As we will see shortly, computing both the WP and the WLP allows F* to move between the two styles without a loss in precision (computing just the WP alone would not allow this).

9.2. Computation types

Expressions in F* are given computation types C. In its most primitive form, each effect in F* introduces a computation type of the form M t1..tn t wp wlp. The M t1..tn indicates the name of the effect M and several user-defined indexes t1..tn. The type t indicates the type of the result of the computation; wp is a predicate transformer that is not weaker than the weakest pre-condition of e; and wlp is a predicate transformer not weaker than the weakest liberal pre-condition of e. For the sake of brevity, we call wp the weakest pre-condition and wlp the weakest liberal pre-condition.

For the purposes of the presentation here, we start by discussing a simplified form of these C types, i.e, we will consider computation types of the form M t wp wlp, those that have a non-parameterized effect constructor M (and generalize to the full form towards the end of this chapter).

A computation e has type M t wp wlp if when run in an initial configuration satisfying wp post, it (either runs forever, if allowed, or) produces a result of type t in a final configuration f such that post f is true, all the while exhibiting no more effects than are allowed by M. In other words, M is an upper bound on the effects of e; t is its result type; and wp is a predicate transformer that for any post-condition of the final configuration of e, produces a sufficient condition on the initial configuration of e. The wlp is similar, except it is liberal with respect to the internal assertions of e in the sense described in the previous section.

These computation types (specifically their predicate transformers) form what is known as a Dijkstra monad. Some concrete examples should provide better intuition.

Remark. We follow an informal syntactic convention that the non-abbreviated all-caps names for computation types are the primitive formsother forms are derived from these.

For example, the computation type constructor PURE is a more primitive version of Pure, which we have used earlier in this tutorial. By the end of this chapter, you will see how Pure, Tot, etc. are expressed in terms of PURE. Likewiwse STATE is the primitive form of ST; EXN is the primitive form of Exn; etc.

9.3. The PURE effect

The PURE effect is primitive in F*. No user should ever have to (re-)define it. Its definition is provided once and for all in lib/prims.fst. It's instructive to look at its definition inasmuch as it provides some insight into how F* works under the covers. It also provides some guidance on how to define new effects. We discuss a fragment of it here.

The type of pure computations is PURE t wp wlp where wp, wlp : (t -> Type) -> Type. This means that pure computations produce t-typed results and are decribed by predicate transformers that transform result predicates (post-conditions of kind t -> Type) to pre-conditions, which are propositions of kind Type.

Seen another way, the signatures of the wp and wlp have the following formthey transform pure post-conditions to pure pre-conditions.

kind PurePost (a:Type) = a -> Type
kind PurePre = Type
kind PureWP (a:Type) = PurePost a -> PurePre

For example, one computation type for 0 is PURE int return_zero return_zero where

return_zero = fun (p:(int -> Type)) -> p 0

This means that in order to prove any property p about the result of the computation 0 is suffices to prove p 0which is of course what you would expect. The type return_zero is an instance of the more general form below:

type return_PURE (#a:Type) (x:a) = fun (post: PurePost a) -> post x

When sequentially composing two pure computations using let x = e1 in e2, if e1: PURE t1 wp1 wlp1 and e2: (x:t1 -> PURE t2 (wp2 x) (wlp2 x)), we type the composed computation as

PURE t2 (bind_PURE wp1 wp2) (bind_PURE wlp1 wlp2)

where:

type bind_PURE (#a:Type) (#b:Type)
               (wp1: PureWP a)
               (wp2: a -> PureWP b)
 = fun (post:PurePost b) -> wp1 (fun (x:a) -> wp2 x post)

One can show that return_PURE and bind_PURE together form a monad.

9.3.1. Pure and Tot

The Pure effect is an abbreviation for PURE that allows you to write specifications with pre- and post-conditions instead of predicate transformers. It is defined as follows:

effect Pure (a:Type) (pre:Type) (post: a -> Type) =
       PURE a (fun (p:PurePost a) -> pre /\ forall (x:a). post x ==> p x)
              (fun (p:PurePost a) -> forall (x:a). pre /\ post x ==> p x)

That is Pure a pre post is a computation which when pre is true produces a result v:a such that post v is true.

The Tot effect is defined below:

effect Tot (a:Type) =
       PURE a (fun (p:PurePost a) -> forall (x:a). p x)
              (fun (p:PurePost a) -> forall (x:a). p x)

This means that a computation type Tot a only reveals that the computation always terminates with an a-typed result.

9.3.2. From predicate transformers to pre- and post-conditions

We have just seen how the definition of Pure a pre post unfolds into the PURE effect. It is also possible to go in the other direction, turning a specification written in the PURE a wp wlp style into a Pure a pre post. However, whereas F* will always automatically unfold the definition of Pure in terms of PURE as needed, it will not automatically transform the more primitive PURE effect into the derived form Pure. Instead, one uses an explicit coercion for this purpose, with the signature shown below.

type as_requires (#a:Type) (wp:PureWP a)  = wp (fun x -> True)
type as_ensures  (#a:Type) (wlp:PureWP a) (x:a) = ~ (wlp (fun y -> ~(y=x)))
assume val as_Pure: #a:Type -> #b:(a -> Type)
          -> #wp:(x:a -> PureWP (b x))
          -> #wlp:(x:a -> PureWP (b x))
          -> =f:(x:a -> PURE (b x) (wp x) (wlp x))
          -> x:a -> Pure (b x) (as_requires (wp x))
                               (as_ensures (wlp x))

Remark. The second last argument to as_Pure is named f and is tagged with an equality constraint, written by preceding the bound variable name with the equality symbol, i.e., =f. Given an application as_Pure g, the equality constraint on the f argument of as_Pure instructs F*'s type inference engine to unify the type of g with the expected type of f. Without this constraint, by default, F* will try to prove that the type of g is a subtype of the expected type of f. In cases like this, where an argument mentions several implicit arguments that need to be inferred (a, b, wp, wlp, in this case), the equality constraint produces better inference resutls.

One way to understand this type is as follows: as_Pure f coerces the type of f which has a PURE (b x) wp wlp effect to an equivalent function type written in terms of Pure. The pre-condition of the resulting function type is easily computed from the wp, using as_requires wp, which is just the weakest pre-condition of the trivial post-condition.

Computing the post-condition is a bit more subtle, and is accomplished with the as_ensures wlp function. Perhaps the easiest way to understand it is by studying the roundtrip transformation of PURE to Pure and back to PURE. The key step below is in the transformation from (b) to (c), where we see that by ensuring ~wlp (fun y -> y <> x), we make use precisely of the Identity 1 from the previous section. Given only a wp without a wlp, we would be stuck not being able to construct as_ensures.

(a) Pure t (as_requires wp)
           (as_ensures wlp)

= (definition)

(b) PURE t (fun post -> wp (fun x -> True) /\ forall y. ~(wlp (fun y' -> y<>y')) ==> post y)
           (fun post -> forall y. wp (fun x -> True) /\  ~(wlp (fun y’ -> y<>y')) ==> post y)

= (unfolding ==> and double negation)

(c) PURE t (fun post -> wp (fun x -> True) /\ forall y.  wlp (fun y' -> y<>y’) \/ post y)
           (fun post -> forall y. not (wp (fun x -> True)) \/ wlp (fun y’ -> y<>y’) \/ post y)

= (folding ==>)

(d) PURE t (fun post -> wp (fun x -> True) /\ forall y.  wlp (fun y’ -> y<>y’) \/ post y)
           (fun post -> forall y. wp (fun x -> True) ==> (wlp (fun y’ -> y<>y’) \/ post y))

= (rearranging quantifier)

(e) PURE t (fun post -> wp (fun x -> True) /\ forall y.  wlp (fun y’ -> y<>y’) \/ post y)
           (fun post -> wp (fun x -> True) ==> forall y. (wlp (fun y’ -> y<>y’) \/ post y))

= (identity 1)

(f) PURE t (fun post -> wp (fun x -> True) /\ wlp (fun y’ -> post y’))
           (fun post -> wp (fun x -> True) ==> wlp (fun y’ -> post y’))

<: (strengthening wlp, eta reduction)

(g) PURE t (fun post -> wp (fun x -> True) /\ wlp post)
            wlp

= (identity 2, eta)

(h) PURE t wp wlp

Here are a few small examples using this coercion to move from PURE to Pure.

val f : x:int -> PURE int (fun 'p -> x > 0 /\ 'p (x + 1)) (fun 'p -> x > 0 ==> 'p (x + 1))
let f x = assert (x > 0); x + 1

val h : #req:(int -> Type)
     -> #ens:(int -> int -> Type)
     -> =f:(x:int -> Pure int (req x) (ens x))
     -> y:int -> Pure int (req y) (ens y)
let h f x = f x

val g : x:int -> Pure int (x > 0) (fun y -> y == x + 1)
let g = h (as_Pure f)

練習問題 9a:

Work out the roundtrip unfolding a Pure t pre post into a PURE effect and then back to a Pure using the as_Pure coercion. Prove that after this round trip, the resulting type is logically equivalent to the type you started with.

回答
Pure t p q

= (definition)

PURE t wp wlp
  where wp  = fun post -> p /\ forall (y:t). q y ==> post y
    and wlp = fun post -> forall (y:t). p /\ q y ==> post y

<:  (definition)

  Pure t (p /\ forall (y:t). q y ==> True)
         (fun y -> not (forall (z:t). p /\ q z ==> (y<>z)))

=  (simplification/de Morgan)

Pure t (p)
       (fun y -> exists (z:t). p /\ q z /\ y=z)

= (replacing existential by equality)

   Pure t p
          (fun y -> p /\ q y)

<: (weakening post-condition, eta)

   Pure t p q

9.4. The STATE effect

Stateful programs operate on an input heap producing a result and an output heap. The computation type STATE t wp wlp describes such a computation, where wp, wlp : StateWP t has the signature below.

kind StatePost t = t -> heap -> Type
kind StatePre    = heap -> Type
kind StateWP t   = StatePost t -> StatePre

In other words, WPs and WLPs for stateful programs transform stateful post-conditions (relating the t-typed result of a computation to the final heap) into a pre-condition, a predicate on the input heap.

The type heap is axiomatized in lib/heap.fst and is one model of the primitive heap provided by the F* runtime system. Specifically, we have functions to select, update, and test the presence of a reference in a heap.

module Heap
assume type heap
assume val sel : #a:Type -> heap -> ref a -> Tot a
assume val upd : #a:Type -> heap -> ref a -> a -> Tot heap
assume val contains : #a:Type -> heap -> ref a -> a -> Tot bool

These functions are interpreted using standard axioms, which allows the SMT solver to reason about heaps, for instance:

assume SelUpd1:       forall (a:Type) (h:heap) (r:ref a) (v:a).
                      {:pattern (sel (upd h r v) r)}
                      sel (upd h r v) r = v

assume SelUpd2:       forall (a:Type) (b:Type) (h:heap) (k1:ref a) (k2:ref b) (v:b).
                      {:pattern (sel (upd h k2 v) k1)}
                      k2=!=k1 ==> sel (upd h k2 v) k1 = sel h k1

The Heap library axiomatizes several other functionsthe interested reader refer to lib/heap.fst for more details.

Remark. Note, although sel is marked as a total function, the axioms underspecify its behavior, e.g., sel h r has no further interpretation unless h can be proven to be an upd.

Also note the use of the {:pattern ...} form in the axioms above. This provides the SMT solver with a trigger for the quantifiers, in effect orienting the equalities in SelUpd1 and SelUpd2 as left-to-right rewritings.

The functions sel and upd provide a logical theory of heaps. At the programmatic level, we require stateful operations to allocate, read and write references in the current heap of the program. The signatures of these stateful primitives are provided in lib/st.fst, as illustrated (in slightly simplified form) below.

Let's start with the signature of read:

assume val read: #a:Type -> r:ref a -> STATE a (wp_read r) (wp_read r)
where wp_read r = fun (post:StatePost a) (h0:heap) ->  post (sel h0 r) h0

This says that read r returns a result v:a when r:ref a; and, to prove for any post-condition post:StatePost a relating the v to the resulting heap, it suffices to prove post (sel h0 r) h0 when read r is run in the initial heap h0.

Next, here's the signature of write:

assume val write: #a:Type -> r:ref a -> v:a -> STATE unit (wp_write r) (wp_write r)
where wp_write r = fun (post:StatePost a) (h0:heap) -> post () (upd h0 r v)

This says that write r v returns a a unit-typed result when r:ref a and v:a; and, to prove any post-condition post:StatePost a relating the () to the resulting heap, it suffices to prove post () (upd h0 r v) when write r v is run in the initial heap h0.

Remark. F* provides support for user-defined custom operators. To allow you to write !r for read r and r := v instead of ST.write r v, we define

let op_Bang x = ST.read x

and

let op_Colon_Equals x v = ST.write x v

As with the PureWP, the predicate transformers StateWP t form a monad, as shown by the combinators below.

type return_STATE (#a:Type) (v:a) = fun (post:StatePost a) (h0:heap) -> post v h0

type bind_STATE (#a:Type) (wp1:StateWP a) (wp2:a -> StateWP b)
     = fun (post:StatePost b) (h0:heap) -> wp1 (fun (x:a) -> wp2 x post) h0

9.4.1. The ST effect

ST is to STATE what Pure is to PURE: it provides a way to write stateful specifications using pre- and post-conditions instead of predicate transformers. It is defined as shown below (in lib/st.fst):

effect ST (a:Type) (pre:StatePre) (post: (heap -> StatePost a)) = STATE a
  (fun (p:StatePost a) (h:heap) ->
     pre h /\ (forall a h1. (pre h /\ post h a h1) ==> p a h1)) (* WP *)
  (fun (p:StatePost a) (h:heap) ->
     (forall a h1. (pre h /\ post h a h1) ==> p a h1))          (* WLP *)

As before, we can also define a coercion to move to ST from STATE.

type as_requires (#a:Type) (wp:STWP_h heap a)  = wp (fun x h -> True)
type as_ensures  (#a:Type) (wlp:STWP_h heap a) (h0:heap) (x:a) (h1:heap)
  = ~ (wlp (fun y h1' -> y<>x \/ h1<>h1') h0)
val as_ST: #a:Type -> #b:(a -> Type)
          -> #wp:(x:a -> STWP_h heap (b x))
          -> #wlp:(x:a -> STWP_h heap (b x))
          -> =f:(x:a -> STATE (b x) (wp x) (wlp x))
          -> x:a -> ST (b x) (as_requires (wp x))
                             (as_ensures (wlp x))

And here's a small program that uses this coercion.

let f x = !x * !x

val h : #req:(ref int -> heap -> Type)
     -> #ens:(ref int -> heap -> int -> heap -> Type)
     -> =f:(x:ref int -> ST int (req x) (ens x))
     -> y:ref int -> ST int (req y) (ens y)
let h f x = f x

val g : x:ref int -> ST int (fun h -> True) (fun h0 y h1 -> h0=h1 /\ y >= 0)
let g = h (as_ST f)

9.4.2. The St effect

We define another abbreviation on top of ST for stateful programs with trivial pre- and post-conditions.

  effect St (a:Type) = ST a (fun h -> True) (fun _ _ _ -> True)

9.5. Lifting effects

When programming with multiple effects, you can instruct F* to automatically infer a specification for your program with a predicate transformer that captures the semantics of all the effects you use. The way this works is that F* computes the least effect for each sub-term of your program, and then lifts the specification of each sub-term into some larger effect, as may be needed by the context.

For example, say you write:

let y = !x in y + 1

The sub-term !x has the STATE effect; whereas the sub-term y+1 is PURE. Since the whole term has at least STATE effect, we'd like to lift the pure sub-computation to STATE. To do this, you can specify that PURE is a sub-effect of STATE, as follows (adapted from lib/prims.fst):

sub_effect
  PURE   ~> STATE = fun (a:Type) (wp:PureWP a) (p:StatePost a) (h:heap) ->
                    wp (fun a -> p a h)

This says that in order to lift a PURE compuataion to STATE, we lift its wp:PureWP a (equivalently for its wlp) to a StateWP a that says that that pure computation leaves the state unmodified.

Note that the type of PURE ~> STATE is (a:Type) -> PureWP a -> StatePost a -> heap -> Type which corresponds to (a:Type) -> PureWP a -> StateWP a since:

kind StateWP a   = StatePost a -> StatePre
kind StatePre    = heap -> Type

9.6. Indexed computation types

Finally, as mentioned earlier, in its full form a computation type has the shape M t1..tn t wp wlp, where t1..tn are some user-chosen indices to the effect constructor M.

This is convenient in that it allows effects to be defined parametrically, and specific effects derived just by instantiation.

For example, the STATE effect is actually defined as an instance of a more general parameterized effect STATE_h (mem:Type), which is parametric in the type of the memory used by the state monad.

Specifically, we have in lib/prims.fst

new_effect STATE = STATE_h heap

However, as we will see in subsequent sections, it is often convenient to define other variants of the state monad using different memory structures.

10. Verifying Stateful Programs

In the previous chapter, we saw how F*'s ST monad was specified. We now look at several programs illustrating its use. If you skipped the previous chapter, you should be okwe'll explain what's needed about the ST monad as we go along, although, eventually, you'll probably want to refer to the previous chapter for more details.

10.1. Stateful access control

We'll start with a simple example, based on the access control example from 1.1. A restriction of that example was that the access control policy was fixed by the two functions canWrite and canRead. What if we want to administer access rights using an access control list (ACL)? Here's one simple way to model itof course, a full implementation of stateful access control would have to pay attention to many more details.

The main idea is to maintain a reference that holds the current access control list. In order to access a resource, we need to prove that the current state contains the appropriate permission.

Here's how it goes:

module DynACLs

open FStar.List
open FStar.Heap (* we open the Heap namespace to use stateful primitives *)

type file = string

(* Each entry is an element in our access-control list *)
type entry =
  | Readable of string
  | Writable of string
type db = list entry

(* The acls reference stores the current access-control list, initially empty *)
val acls : ref (list entry)
let acls = ref []

(* We define two pure functions that test whether
   the suitable permission exists in some db *)
let canRead db file =
  is_Some (find (function Readable x | Writable x -> x=file) db)

let canWrite db file =
  is_Some (find (function Writable x -> x=file | _ -> false) db)

(*
   Here are two stateful functions which alter the access control list.
   In reality, these functions may themselves be protected by some
   further authentication mechanism to ensure that an attacker cannot
   alter the access control list

   F* infers a fully precise predicate transformer semantics for them
*)
let grant e  = acls := e::!acls
let revoke e = acls := filter (fun e' -> e<>e') !acls

(* Next, we model two primitives that provide access to files *)

(* We use two heap predicates, which will serve as stateful pre-conditions *)
type CanRead (f:file) (h:heap)  = b2t (canRead  (sel h acls) f)
type CanWrite (f:file) (h:heap) = b2t (canWrite (sel h acls) f)

(* In order to call `read`, you need to prove
   the `CanRead f` permission exists in the input heap *)
assume val read:   f:file -> ST string
       (requires (CanRead f))
       (ensures (fun h s h' -> h=h'))

(* Likewise for `delete` *)
assume val delete: f:file -> ST unit
       (requires (CanWrite f))
       (ensures (fun h s h' -> h=h'))

(* Then, we have a top-level API, which provides protected
   access to a file by first checking the access control list.

   If the check fails, it raises a fatal exception using `failwith`.
   As such, it is defined to have effect `All`, which combines
   both state and exceptions.

   Regardless, the specification proves that `checkedDelete`
   does not change the heap.
 *)
val checkedDelete: file -> All unit
    (requires (fun h -> True))
    (ensures (fun h x h' -> h=h'))
let checkedDelete file =
  if canWrite !acls file
  then delete file
  else failwith "unwritable"

(* Finally, we have a top-level client program *)
val test_acls: file -> unit
let test_acls f =
  grant (Readable f);     (* ok *)
  let _ = read f in       (* ok --- it's in the acl *)
  (* delete f;               not ok --- we're only allowed to read it *)
  checkedDelete f;          (* ok, but fails dynamically *)
  revoke (Readable f);
  (* let _ = read f in *)   (* not ok any more *)
  ()

練習問題 10a:
Write down some types for grant and revoke that are sufficiently precise to allow the program to continue to type-check.

val grant : e:entry -> ST unit (requires (fun h -> True))
                               (ensures (fun h x h' -> True))
let grant e = ST.write acls (e::ST.read acls)

val revoke: e:entry -> ST unit (requires (fun h -> True))
                               (ensures (fun h x h' -> True))
let revoke e =
  let db = List.filterT (fun e' -> e<>e') (ST.read acls) in
  ST.write acls db

エディタに読み込む

回答
val grant : e:entry -> ST unit (requires (fun h -> True))
                               (ensures (fun h x h' -> sel h' acls = e::sel h acls))
let grant e = ST.write acls (e::ST.read acls)

val revoke: e:entry -> ST unit (requires (fun h -> True))
                               (ensures (fun h x h' -> not(List.mem e (sel h' acls))))
let revoke e =
  let db = List.filter (fun e' -> e<>e') (ST.read acls) in
  ST.write acls db

エディタに読み込む

10.2. Reasoning about (anti-)aliased heap structures

A central problem in reasoning about heap-manipulating programs has to do with reasoning about updates to references in the presence of aliasing. In general, any two references (with compatible types) can alias each other (i.e, they may refer to the same piece of memory), so updating one can also change the contents of the other. In this section, we'll look at two small but representative samples that illustrate how this form of reasoning can be done in F*.

10.2.1. Dynamic frames

For our first example, we define the type of a 2-dimensional mutable point. The refinement on y ensures that the references used to store each coordinate are distinct.

type point =
  | Point : x:ref int -> y:ref int{y<>x} -> point

Allocating a new point is straightforward:

let new_point x y =
  let x = ST.alloc x in
  let y = ST.alloc y in
  Point x y

As is moving a point by a unit along the x-axis.

let shift_x p = Point.x p := !(Point.x p) + 1

Now, things get a bit more interesting. Let's say we have a pair of points, p1 and p2, we want to shift p1, and reason that p2 is unchanged. For example, we'd like to identify some conditions that are sufficient to prove that the assertion in the program below always succeeds.

let shift_p1 (p1:point) (p2:point) =
    let p2_0 = !(Point.x p2), !(Point.y p2)  in //p2 is initially p2_0
    shift_x p1;
    let p2_1 = !(Point.x p2), !(Point.y p2) in
    assert (p2_0 = p2_1)                        //p2 is unchanged

If you give this program (reproduced in its entirety below) to F*, it will report no errors. This may surprise you: after all, if you call shift_p1 p p the assertion will indeed fail. What's going on here is that for functions in the ST effect, F* infers a most precise type for it, and if the programmer did not write down any other specification, this precise inferred type is what F* will use. This means that without an annotation on shift_p1, F* does not check that the assertion will succeed on every invocation of shift_p1; instead, using the inferred type it will aim to prove that the assertion will succeed whenever the function is called. Let's try:

val test0: unit -> St unit
let test0 () =
  let x = new_point 0 0 in
  shift_p1 x x

Here, we wrote a specification for test0, asking it to have trivial pre-condition. When we ask F* to check this, it complains at the call to shift_p1 x x, saying that the assertion failed.

If we try calling shift_p1 with two distinct points, as below, then we can prove that the assertion succeeds.

val test1: unit -> St unit
let test1 () =
  let x = new_point 0 0 in
  let y = new_point 0 0
  shift_p1 x y

In simple code like our example above, it is a reasonable trade-off to let F* infer the most precise type of a function, and to have it check later, at each call site, that the those calls are safe.

As you write larger programs, it's a good idea to write down the types you expect, at least for tricky top-level functions. To see what these types look like for stateful programs, let's decorate each of the top-level functions in our example with the typesfor these tiny functions, the types can often be larger than the code itself; but this is just an exercise. Typically, one wouldn't write down the types of such simple functions.

10.2.2. A type for shift_x and the Heap.modifies predicate

Let's start with shift_x, since it is the simplest:

Here's one very precise type for it:

val shift_x : p:point -> ST unit
  (requires (fun h -> True))
  (ensures (fun h0 _ h1 -> h1=upd h0 (Point.x p) (sel h0 (Point.x p) + 1)))

Another, less precise but more idiomatic type for it is:

val shift_x : p:point -> ST unit
  (requires (fun h -> True))
  (ensures (fun h0 _ h1 -> modifies (only (Point.x p)) h0 h1))

Informally, ensures-clause above says that the heap after calling this function (h1) differs from the initial heap h0 only at Point.x (and possibly some newly allocated locations). Let's look at it in more detail.

The predicate modifies is defined in the module Heap (lib/heap.fst). First, let's look at its signature, which says that it relates a set aref to a pair of heaps. The type aref is the type of a reference, but with the type of referent abstracted. As such, the first argument to modifies is a set of heterogenously typed references.

  type aref =
    | Ref : #a:Type -> ref a -> aref
  let only x = Set.singleton (Ref x)
  type modifies : set aref -> heap -> heap -> Type

The definition of modifies follows:

type modifies mods h0 h1 =
  Heap.equal h1 (Heap.concat h1 (Heap.restrict (Set.complement mods) h0))

Heap.equal: Heap.equal is an equivalence relation on heap capturing the notion of extensional equality; i.e., two heaps are extensionally equal if they map each reference to the same value.

Heap.concat: Each reference r in the heap concat h h' contains a value that is the same as in h, except if the r is in h', in which case it's value is whatever value h' contains at r. More formally:

   sel r (concat h h')
   = if contains h' r then sel h' r else sel h r

Heap.restrict The function restrict s h provides a way to shrink the domain of the heap h to be at most s. Specifically:

  contains (restrict s h) r = Set.mem (Ref r) s && contains h r

Altogether, the definition of modifies says that for every reference r, if r is not in the set mods and r if the heap h0 contains r, then sel h1 r = sel h0 r, i.e., it hasn't changed. Otherwise, sel h1 r = sel h1 rmeaning we know nothing else about it.

Remark. We define the following infix operators to build sets of heterogenous references.

let op_Hat_Plus_Plus (#a:Type) (r:ref a) (s:set aref) =
    Set.union (Set.singleton (Ref r)) s

let op_Plus_Plus_Hat (#a:Type) (s:set aref) (r:ref a) =
    Set.union s (Set.singleton (Ref r))

let op_Hat_Plus_Hat (#a:Type) (#b:Type) (r1:ref a) (r2:ref b) =
    Set.union (Set.singleton (Ref r1)) (Set.singleton (Ref r2))

10.2.3. A type for new_point and freshness of references

Here's a precise type for new_point, with its definition reproduced for convenience.

val new_point: x:int -> y:int -> ST point
  (requires (fun h -> True))
  (ensures (fun h0 p h1 ->
                modifies Set.empty h0 h1
                /\ fresh (Point.x p ^+^ Point.y p) h0 h1
                /\ Heap.sel h1 (Point.x p) = x
                /\ Heap.sel h1 (Point.y p) = y))
let new_point x y =
  let x = ST.alloc x in
  let y = ST.alloc y in
  Point x y

The modifies clause says the function modifies no existing referencethat's easy to see, it only allocates new references.

In the body of the definition, we build Point x y and the type of Point requires us to prove that x <> y. The only way to prove that is if we know that ref returns a distinct reference each time, i.e., we need freshness.

The type of ST.alloc gives us the freshness we need to prove that x <> y. The type below says that the returned reference does not exists in the initial heap and does exist in the final heap (initialized appropriately).

val alloc:  #a:Type -> init:a -> ST (ref a)
    (requires (fun h -> True))
    (ensures (fun h0 r h1 -> fresh (only r) h0 h1 /\ h1==upd h0 r init))

type fresh (refs:set aref) (h0:heap) (h1:heap) =
  forall (a:Type) (r:ref a). mem (Ref r) refs
                         ==> not(contains h0 a) /\ contains h1 a

Coming back to the type of new_point: By stating that the new heap contains both Point.x and Point.y, we provide the caller with enough information to prove that any references that it might allocate subsequently will be different from the references in the newly allocated point. For example, the assertion in the code below succeeds, only because new_point guarantees that the heap prior to the allocation of z contains Point.x p; and ST.alloc guarantees that z is different from any reference that exists in the prior heap. Carrying Heap.contains predicates in specifications is important for this reason.

let p = new_point () in
let z = ST.alloc 0 in
assert (Point.x p <> z)

On the other hand, since the ST library we are working with provides no ability to deallocate a reference (other versions of it do; see, for example, lib/stperm.fst), we know that if we have a value v:ref t, that the current heap must contain it. Capturing this invariant, the ST library also provides the following primitive (whose implementation is a noop).

val recall: #a:Type -> r:ref a -> ST unit
  (requires (fun h -> True))
  (ensures (fun h0 _ h1 -> h0=h1 /\ Heap.contains h1 r))

Using this, we can write the following code.

val f : ref int -> St unit
let f (x:ref int) =
  recall x;         //gives us that the initial heap contains x, for free
  let y = ST.alloc 0 in
  assert (y <> x)

As a matter of style, we prefer to keep the use of recall to a minimum, and instead carry Heap.contains predicates in our specifications, as much as possible.

10.2.4. A type for shift_p1

Now, we have all the machinery we need to give shift_p1 a sufficiently strong type to prove that its assertion will never fail (if its pre-condition is met).

val shift_p1: p1:point
           -> p2:point{   Point.x p2 <> Point.x p1
                       /\ Point.y p2 <> Point.x p1 }
           -> ST unit
    (requires (fun h -> True))
    (ensures (fun h0 _ h1 -> modifies (only (Point.x p1)) h0 h1))

In order to prove that the assignment to Point.x p1 did not change p2, we need to know that Point.x p1 does not alias either component of p2. In general, if p1 can change arbitrarily, we also need the other two conjuncts, i.e., we will need that the references of p1 and p2 are pairwise distinct.

Remark. A note on style: we could have placed the refinement on p2 within the requires clause. However, since the refinement is independent of the state, we prefer to write it in a manner that makes its state independence explicit.

練習問題 10b:
Change shift_x to the function shift below that moves both the x and y components of its argument by some amount. Prove that calling this function in shift_p1 does not change p2.

let shift p = Point.x p := 17; Point.y p := 18

エディタに読み込む

回答
let shift p = Point.x p := 17; Point.y p := 18

エディタに読み込む

11. Lightweight framing with hyper-heaps

The style of the previous section is quite general. But, as programs scale up, specifying and reasoning about anti-aliasing can get to be quite tedious. In this chapter, we look at an alternative way of proving stateful programs correct by making use of a more structured representation of memory that we call a “HyperHeap”. First, we illustrate the problem of scaling up the approach of the previous chapter to even slightly larger examples

  type a = b

11.1. Flying robots

johnnysokko

Let's have some fun with flying robots. Maybe you've seen this classic Japanese TV series from the 60s. https://​en.​wikipedia.​org/​wiki/​Giant_​Robo_(​tokusatsu)​. Let's build a tiny model of this flying robot.

Our bot has a 3d-point representing its position; and two arms, both in polar coordinates.

  type bot = {
    pos:point;
    left:arm;
    right:arm
  }
  and point = {
    x:ref int;
    y:ref int;
    z:ref int;
  }
  and arm = {
    polar:ref int;
    azim:ref int
  }

Our bot has an invariant: whenever it is flying, it has its arms up.

flying

We can write a function to make our robot fly, which sets its arms up and then shoots the robot into the sky.

  let fly b =
    b.left.polar := 0;
    b.right.polar := 0;
    b.z := 100

Now, we'd like to prove properties like the following:

  //initially, in h0: b1 not flying, b2 not flying
      fly b1
  //in h1: b1 flying, b2 not flying

To prove this property, and to prove that the bot's invariant is maintained, we need many anti-aliasing invariants, including the following (stated informally).

forall r1, r2. r1 in refs_in b1
              /\ r2 in refs_in b2 ==> r1 <> r2
refs in b.left.arm `disjoint` refs in b.pos
refs in b.right.arm `disjoint` refs in b.pos
refs in b.left.arm `disjoint` refs in b.right.arm

As you can see, what started out as a bit of fun programming is now a painful exercise in managing anti-aliasing invariants. Worse, even if we state all these invariants, proving that they are preserved involves reasoning about a quadratic number of inequalities between the all the references in each robot, as well as a further quadratic inequalities among the references of each bot.

F*'s effect mechanism provides an alternative to this tedium. Instead of working with the primitive ST effect (and its flat model of memory via the heap type) that we have been working with so far, we can define easily define a different, more structured view of memory as a new effect. One such alternative is the HyperHeap, a model of memory which provides a convenient built-in notion of disjoint sets of references.

11.2. Hyper-heaps

So far, we have been working with the heap type, a flat, typed-map from references to their contents. The ref type is abstractit has no structure and only supports equality operations. Conceptually, it looks like this:

heap

A hyper-heap provides organizes the heap into many disjoint fragments, or regions. Each region is collectively addressed by a region identifier, and these identifiers are organized in a tree-shaped hierarchy. Each region is itself a map from typed references to values, just like our heaps from before. The picture below depicts the structure.

hyperheap

At the top-level we have regions R0 ... Rn, each associated with a fragment of heap references. Region identifiers R0.0 ... R0.m are within the hierarchy rooted at R0; each has a set of references distinct from all other regions (including its parent R0); and so on.

The HyperHeap module in F*'s standard library defines this structure, a type rid for region ids, and a type rref (r:rid) (a:Type), which is the type of a reference in region r that points to an a-typed value. We prove that values of type rref r a are in an injection with values of type ref ameaning that hyper-heaps are in 1-1 correspondence with the underlying heap, except, as we will see, the additional structure provided helps with stating and proving memory invariants.

The module HyperHeap defines (see lib/hyperheap.fsi, for its abstract specification):

type t = Map.t rid heap
new_effect STATE = STATE_h t
effect ST (a:Type) (pre:t -> Type) (post:t -> a -> t -> Type) =
       STATE a (fun 'p m0 -> pre m0 /\ (forall x m1. post m0 x m1 ==> 'p x m1))
               (fun 'p m0 ->  (forall x m1. pre m0 /\ post m0 x m1 ==> 'p x m1))

That is HyperHeap.STATE and HyperHeap.ST are just like the STATE and ST we've been working with, except that instead of the type of memory being a flat heap, the memory has type HyperHeap.t, a map from region ids rid to heaps.

11.2.1. The type of region identifiers, rid

The type rid is abstract to clients, with a few operations on it revealing its hierarchical structure. Specifically, we have three functions:

type rid
val root : rid
val includes : rid -> rid -> Tot bool
val extends  : rid -> rid -> Tot bool
let disjoint i j = not (includes i j) && not (includes j i)

One way to think of rid is as a list int, where includes i j if and only if i is a prefix of j; and extends i j is true if i = _::j. However, while this may provide you with some intuition, formally, the only properties that these functions are known to satisfy are revealed by the following lemmas:

val lemma_includes_refl: i:rid
-> Lemma (requires (True))
         (ensures (includes i i))
         [SMTPat (includes i i)]

val lemma_disjoint_includes: i:rid -> j:rid -> k:rid
-> Lemma (requires (disjoint i j /\ includes j k))
         (ensures (disjoint i k))
         [SMTPat (disjoint i j);
          SMTPat (includes j k)]

val lemma_extends_includes: i:rid -> j:rid
-> Lemma (requires (extends j i))
         (ensures (includes i j))
         [SMTPat (extends j i)]

val lemma_extends_disjoint: i:rid -> j:rid -> k:rid
-> Lemma (requires (extends j i /\ extends k i /\ j<>k))
         (ensures (disjoint j k))
         [SMTPat (extends j i);
          SMTPat (extends k i)]

11.2.2. The type of region-indexed references: rref

Next, we have a type rref for region-indexed references, as a funtion as_ref that coerces an rref to its underlying heap reference.

Remark. The functions as_ref and ref_as_rref have effect GTot, indicating that they are ghostly total functions. A subsequent chapter will describe ghost effects in more detail. For now, it suffices to know that computations with effect GTot can only be used in specifications. Concrete executable programs cannot use GTot. In this case, the GTot effect is used to ensure that client programs of HyperHeap cannot break the abstraction of the rref type, except in their specifications.

  type rref : rid -> Type -> Type
  val as_ref      : #a:Type -> #id:rid -> r:rref id a -> GTot (ref a)
  val ref_as_rref : #a:Type -> i:rid -> r:ref a -> GTot (rref i a)
  val lemma_as_ref_inj: #a:Type -> #i:rid -> r:rref i a
      -> Lemma (requires (True))
               (ensures ((ref_as_rref i (as_ref r) = r)))
         [SMTPat (as_ref r)]

The functions Heap.sel and Heap.upd are adapted to work with hyper-heaps instead; in effect, we select first the region i corresponding to rref i a and then perform the select/update within the heap within that region. An important point to note is that although the rid type is structured hierarchically, the map of all regions is itself flat. Thus, selecting the region corresponding to i is constant time operation (rather than requiring a tree traversal). As we will see below, this is crucial for good automation in proofs.

let sel (#a:Type) (#i:rid) (m:t) (r:rref i a) = Heap.sel (Map.sel m i) (as_ref r)
let upd (#a:Type) (#i:rid) (m:t) (r:rref i a) (v:a)
  = Map.upd m i (Heap.upd (Map.sel m i) (as_ref r) v)

11.2.3. Stateful operations on regions and references

Creating a new region HyperHeap also provides four main stateful functions. The first of these, new_region r0, allocates a new, empty region rooted at r0

val new_region: r0:rid -> ST rid
      (requires (fun m -> True))
      (ensures (fun (m0:t) (r1:rid) (m1:t) ->
                           extends r1 r0
                        /\ fresh_region r1 m0 m1
                        /\ m1=Map.upd m0 r1 Heap.emp))

Allocating a reference in a region The function ralloc r v allocates a new reference in region r and initializes its contents to v.

val ralloc: #a:Type -> i:rid -> init:a -> ST (rref i a)
    (requires (fun m -> True))
    (ensures (fun m0 x m1 ->
                    Let (Map.sel m0 i) (fun region_i ->
                    not (Heap.contains region_i (as_ref x))
                    /\ m1=Map.upd m0 i (Heap.upd region_i (as_ref x) init))))

Reading and writing references These next two operations are written !r and r := v, for dereference and assignment of rref's, respectively.

val op_Bang: #a:Type -> #i:rid -> r:rref i a -> ST a
  (requires (fun m -> True))
  (ensures (fun m0 x m1 -> m1=m0 /\ x=Heap.sel (Map.sel m0 i) (as_ref r)))

val op_Colon_Equals: #a:Type -> #i:rid -> r:rref i a -> v:a -> ST unit
  (requires (fun m -> True))
  (ensures (fun m0 _u m1 -> m1=Map.upd m0 i (Heap.upd (Map.sel m0 i) (as_ref r) v)))

11.2.4. Framing conditions for hyper-heaps: modifies revised

Finally, we redefine modifies clauses to work with hyper-heaps instead of heaps. Crucially, given a region ids r1, ..., rn, we intend to write modifies (r1 ^++ ... ++^ rn) h0 h1 to mean that h1 may differ from h0 in all regions rooted at some region in the set {r1, ..., rn} (and, as before, any other regions that are newly allocated in h1). As we will see, generalizing modifies clauses to work with hierarchical region names is a crucial feature, both for compactness of specifications and for better automation.

type modifies (s:Set.set rid) (m0:t) (m1:t) =
  Map.Equal m1 (Map.concat m1 (Map.restrict (Set.complement (mod_set s)) m0))

where
val mod_set : Set.set rid -> GTot (Set.set rid)
and forall (x:rid) (s:Set.set rid).
           Set.mem x (mod_set s) <==> (exists (y:rid). Set.mem y s /\ includes y x)

Remark. The interpretation of Map.restrict, Map.concat and Map.Equal is analogous to the counterparts for Heap discussed in the previous section.

The definition of mod_set s is non-constructive, since deciding Set.mem x (mod_set s) requires finding a witness in s, and element y of s, such that includes y x. As such, we mark it as a ghost function with the GTot effect.

11.3. Robot, fly!

We now look at the use of hyper-heaps to solve our problem of programming our robots.

The main idea is to define our data structures in a way that distinct components of the robot are allocated in distinct regions, thereby maintaining an invariant that the components do not interfere. For example, by allocating the left arm and the right arm of the robot in distinct regions, we know that the arms do not alias each othermoving one arm does not disturb the other.

Here's how it goes:

Each type carries an extra implicit parameter, recording the region in which its mutable references reside. Within a region, we get no free anti-aliasing propertiesso, for those references, we write explicit inequalities that say, for example, that the x, y and z fields of a point are not aliased.

For the bot itself, we say that its components are allocated in disjoint sub-regions of r, the region of the bot. Note that the hierarchical region names allow us to state this conveniently. With just a flat namespace of regions, we would had to have explicitly specified the set of regions that are transitively allocated within a bot (possibly breaking the abstraction of sub-objects, which would have to reveal how many regions they used.)

module Robot
open Util
open Heap
open HyperHeap

type point =
  | Point : #r:rid
          -> x:rref r int
          -> y:rref r int
          -> z:rref r int{x<>y /\ y<>z /\ x<>z}
          -> point

type arm =
  | Arm : #r:rid
       -> polar:rref r int
       -> azim:rref r int{polar <> azim}
       -> arm

type bot =
  | Bot : #r:rid
       -> pos  :point{includes r (Point.r pos)}
       -> left :arm  {includes r (Arm.r left)}
       -> right:arm  {includes r (Arm.r right)
                        /\ disjoint (Point.r pos) (Arm.r left)
                        /\ disjoint (Point.r pos) (Arm.r right)
                        /\ disjoint (Arm.r left)  (Arm.r right)}
       -> bot

Next, we define our robot invariant: whenever it is flying, its arms are up. Additionally, we state that all the regions of the bot are included in the heap. This is a matter of taste: alternatively, we could have omitted the contains predicates in our invariant, and resorted to ST.recall (its analog for hyper-heaps), to prove that a region exists whenever we need that property.

let flying (b:bot) (h:HyperHeap.t) =
    sel h (Point.z (Bot.pos b)) > 0

let arms_up (b:bot) (h:HyperHeap.t) =
    sel h (Arm.polar (Bot.right b)) = 0
    && sel h (Arm.polar (Bot.left b)) = 0

type robot_inv (b:bot) (h:HyperHeap.t) =
  Map.contains h (Bot.r b)
  /\ Map.contains h (Point.r (Bot.pos b))
  /\ Map.contains h (Arm.r (Bot.left b))
  /\ Map.contains h (Arm.r (Bot.right b))
  /\ (flying b h ==> arms_up b h)

Now, we come to the code that builds new points, arms, and robots. In each case, the caller specifies r0, the region within which the object is to be allocated. We create a new sub-region of r0, allocate the object within in, prove that the region is fresh (meaning the initial heap does not contain that region, while the final heap does), and that the object is initialized as expected. Inthe case of new_robot, we also prove that the the returned bot satisfies the robot invariant.

val new_point: r0:rid -> x:int -> y:int -> z:int -> ST point
    (requires (fun h0 -> True))
    (ensures (fun h0 p h1 ->
          modifies Set.empty h0 h1
          /\ extends (Point.r p) r0
          /\ fresh_region (Point.r p) h0 h1
          /\ sel h1 (Point.x p) = x
          /\ sel h1 (Point.y p) = y
          /\ sel h1 (Point.z p) = z))
let new_point r0 x y z=
  let r = new_region r0 in
  let x = ralloc r x in
  let y = ralloc r y in
  let z = ralloc r z in
  Point x y z

val new_arm: r0:rid -> ST arm
    (requires (fun h0 -> True))
    (ensures (fun h0 x h1 ->
          modifies Set.empty h0 h1
          /\ extends (Arm.r x) r0
          /\ fresh_region (Arm.r x) h0 h1))
let new_arm r0 =
  let r = new_region r0 in
  let p = ralloc r 0 in
  let a = ralloc r 0 in
  Arm p a

val new_robot: r0:rid -> ST bot (requires (fun h0 -> True))
                                (ensures (fun h0 x h1 ->
                                      modifies Set.empty h0 h1
                                      /\ extends (Bot.r x) r0
                                      /\ fresh_region (Bot.r x) h0 h1
                                      /\ robot_inv x h1))
let new_robot r0 =
  let r = new_region r0 in
  let p = new_point r 0 0 0 in
  let left = new_arm r in
  let right = new_arm r in
  Bot #r p left right

Next, we write our function fly, which sets the robots arms up, and shoots it up to fly. As an illustration, we show that we can also modify some other reference arbitrarily, and the anti-aliasing properties of our invariant suffice to prove that this assignment does not mess with the robot invariant.

val fly: b:bot -> ST unit
  (requires (robot_inv b))
  (ensures (fun h0 _u h1 ->
              modifies (only (Bot.r b)) h0 h1
              /\ robot_inv b h1
              /\ flying b h1))
let fly b =
  Arm.polar (Bot.left b)  := 0;
  Arm.polar (Bot.right b) := 0;
  Point.z (Bot.pos b)     := 100
  Arm.azim (Bot.right b)  := 17;

Finally, if we're given two robots, b0 and b1, we know that they are allocated in disjoint regions, and satisfy the robot invariant, then we can fly one, not impact the invariant of the other; then fly the other, and have both of them flying at the end.

val fly_robots: b0:bot
             -> b1:bot{disjoint (Bot.r b0) (Bot.r b1)}
             -> ST unit
    (requires (fun h -> robot_inv b0 h /\ robot_inv b1 h))
    (ensures (fun h0 x h1 ->
              modifies (Bot.r b0 ^+^ Bot.r b1) h0 h1
              /\ robot_inv b0 h1
              /\ robot_inv b1 h1
              /\ flying b0 h1
              /\ flying b1 h1))
let fly_robots b0 b1 =
  fly b0;
  fly b1

練習問題 11a:
Extend this example by adding a function which takes a list of robots, each in a region disjoint from all others, and fly all of them.

val fly_robot_army: ...

エディタに読み込む

回答
val fly_robot_army:  #rs:Set.set rid
        -> bs:bots rs
        -> ST unit
           (requires (fun h -> (forall b.{:pattern (trigger b)}
                                            (trigger b /\ mem b bs ==> robot_inv b h))))
           (ensures  (fun h0 _u h1 ->
                          modifies rs h0 h1
                           /\ (forall b.{:pattern (trigger b)}
                                  (trigger b /\ mem b bs ==> robot_inv b h1 /\ flying b h1))))

エディタに読み込む

11.4. Why hyper-heaps work

The style of dynamic frames and explicit inequalities between objects is not incompatible with hyper-heaps: as we've also seen, within a region, we resort to pairwise inequalities, as usual. However, using hyper-heaps where possible, as we've just seen, makes specifications much more concise. As it turns out, they also make verifying programs much more efficient. On some benchmarks, we've noticed a speedup in verification time of more than a factor of 20x when using hyper-heaps for disjointness invariants. In this section, we look a bit more closely at what's happening under the covers and why hyper-heaps help.

First, without hyper heaps, consider a computation f () run in a heap h0 and producing a heap h1 related by modifies {x1,...,xn} h0 h1, for some set of references {x1...xn}. Consider also some predicate Q = fun h -> P (sel h y1) ... (sel h yn), which is initially true in h0. We would like to prove that if Q h1 is also true. In other words, we need to prove the formula:

Expanding definitions:
  P (sel h0 y1) ... (sel h0 ym)
  /\ h1 = concat h1 (restrict (complement {x1..xn}) h0)
  ==> P (sel h1 y1) ... (sel h1 ym)

In general, for an arbitrary uninterpreted predicate P, to prove this, one must prove an quadratic number of inequalities, e.g., to prove that sel h1 y1 = sel h0 y1, requires proving that y1 is not equal to any the {x1..xn}.

However, if one can group related references into regions (meaning related references are generally read and updated together), one can do much better. For example, moving to hyper-heaps, suppose we place all the {x1..xn} in a region included by rx. Suppose {y1,...,ym} are all allocated in some region ry. Now, our goal is to prove

  P (Heap.sel (Map.sel h0 ry) y1) ... (Heap.sel (Map.sel h0 ry) ym)
  /\ h1 = concat h1 (restrict (mod_set {rx}) h0)
  ==> P (Heap.sel (Map.sel h1 ry) y1) ... (Heap.sel (Map.sel h1 ry) ym)

To prove this, we only need to prove that Map.sel h0 ry = Map.sel h1 ry, which involves proving not (included rx ry). Having proven this fact, the SMT solver simply unifies the representation of all occurrences of these sub-terms everywhere in the formula above and concludes the proof immediately. Thus, in such (arguably common) cases, what initially required quadratic number of reasoning steps, now only requires a constant number of steps!

In more general scenarios, we may still have to perform a quadratic number of reasoning steps, but with hyper-heaps, we are quadratic only in the number of regions involved, which are often much smaller than the number of references that they may contain. The use of region hierarchies serves to further reduce the number of region identifiers that one refers to, making the constants smaller still. Of course, in the degenerate case where one has just one reference per region, this devolves back to the performance one would get without regions at all.

12. Cryptography examples

12.1. MAC

We begin with our cryptographic library.

module MAC
open Array
open SHA1

Message authentication codes (MACs) provide integrity protection based on keyed cryptographic hashes. We define an F* module that implements this functionality.

We attach an authenticated property to each key used as a pre-condition for MACing and a postcondition of MAC verification.

opaque type key_prop : key -> text -> Type
type pkey (p:(text -> Type)) = k:key{key_prop k == p}

(In the RPC example below we will use a key of type pkey reqresp where

opaque logic type reqresp (msg:text) =
    (exists s. msg = request s /\ Request s)
 \/ (exists s t. msg = response s t /\ Response s t)

)

Next, we define the types of functions that a MAC library is supposed to provide:

val keygen: p:(text -> Type) -> pkey p
val mac:    k:key -> t:text{key_prop k t} -> tag
val verify: k:key -> t:text -> tag -> b:bool{b ==> key_prop k t}

12.2. Cryptographic Capabilities for Accessing Files

We extend the acls2.fst example with cryptographic capabilities, so that our trusted ACLs library can now issue and accept HMACSHA1 tags as evidence that a given file is readable.

What is the advantage of capabilities over the refinements already provided in acls2.fst?

練習問題 12a:
Relying on acls2.fst and mac.fst, implement a pair of functions with the following specification, and verify them by typing under the security assumption that HMACSHA1 is INT-CPA.

val issue:  f:file{ canRead f } -> SHA1.tag
val redeem: f:file -> m:SHA1.tag -> u:unit{ canRead f }

エディタに読み込む

To this end, assume given a UTF8 encoding function from strings to bytes, with the following specification:

assume val utf8: s:string  -> Tot (seq byte)

assume UTF8_inj:
  forall s0 s1.{:pattern (utf8 s0); (utf8 s1)}
    equal (utf8 s0) (utf8 s1) ==> s0==s1

回答
val issue: f:file{ canRead f } -> SHA1.tag
val redeem: f:file -> m:SHA1.tag -> u:unit{ canRead f }

let issue f = MAC.mac k (utf8 f)
let redeem f t = if MAC.verify k (utf8 f) t then () else failwith "bad capability"

How would we extend it to also cover CanWrite access?

12.3. Secure RPC

We describe a simple secure RPC implementation, which consists of three modules: Mac, our library for MACs, Format, a module for message formatting, and RPC, a module for the rest of the protocol code. (Placing the formatting functions request and response in a separate module is convenient to illustrate modular programming and verification.)

12.3.1. Secure RPC protocol

To start with we consider a single client and server. The security goals of our RPC protocol are that (1) whenever the server accepts a request message s from the client, the client has indeed sent the message to the server and, conversely, (2) whenever the client accepts a response message t from the server, the server has indeed sent the message in response to a matching request from the client.

To this end, the protocol uses message authentication codes (MACs) computed as keyed hashes, such that each symmetric MAC key kab is associated with (and known to) the pair of principals a and b. Our protocol may be informally described as follows. An Authenticated RPC Protocol:

1. client->server  utf8 s | (mac kab (request s))
2. server->client  utf8 t | (mac kab (response s t))

In the protocol narration, each line indicates an intended communication of data from one principal to another.

utf8 marshalls strings such as s and t into byte arrays that can be send over the network. | written also append is a function concatenating bytes. request and response build message digests (the authenticated values). These functions may for instance be implemented as tagged concatenations of their utf8-encoded arguments. These functions will be detailed in the Format module.

Below we give an implementation of the protocol using these functions, the functions of the ‘Mac’ module, and networking functions

assume val send: message -> unit
assume val recv: (message -> unit) -> unit

These functions model an untrusted network controlled by the adversary, who decides through their implementation when to deliver messages.

Two events, record genuine requests and responses

logic type Request : string -> Type
logic type Response : string -> string -> Type

in the following protocol

let client (s:string16) =
  assume (Request s);
  send (append (utf8 s) (mac k (request s)));
  recv (fun msg ->
    if length msg < macsize then failwith "Too short"
    else
      let (v, m') = split msg (length msg - macsize) in
      let t = iutf8 v in
      if verify k (response s t) m'
      then assert (Response s t))

let server () =
  recv (fun msg ->
    if length msg < macsize then failwith "Too short"
    else
      let (v,m) = split msg (length msg - macsize) in
      if length v > 65535 then failwith "Too long"
      else
        let s = iutf8 v in
        if verify k (request s) m
        then
          ( assert (Request s);
            let t = "22" in
            assume (Response s t);
            send (append (utf8 t) (mac k (response s t)))))

The assert guarantee that messages that are received by a party have been sent by its peer.

12.3.2. Formating code

The Format module used by the protocol implementation exports among others the following types and functions.

type message = seq byte
type msg (l:nat) = m:message{length m==l}

val request : string -> Tot message
let request s = append tag0 (utf8 s)

val response: string16 -> string -> Tot message
let response s t =
  let lb = uint16_to_bytes (length (utf8 s)) in
  append tag1 (append lb (append (utf8 s) (utf8 t)))

We require 3 lemmas on message formats:

For authentication properties, we require both functions to be injective, so that authenticating the bytes unambiguously authenticate the text before marshalling.

練習問題 12b:
Try to state this formally as three lemmas.

回答
val req_resp_distinct:
  s:string -> s':string16 -> t':string ->
  Lemma (requires True)
        (ensures (request s <> response s' t'))
        [SMTPat (request s); SMTPat (response s' t')]

val req_components_corr:
  s0:string -> s1:string ->
  Lemma (requires (request s0 == request s1))
        (ensures  (s0==s1))

val resp_components_corr:
  s0:string16 -> t0:string -> s1:string16 -> t1:string ->
  Lemma (requires (response s0 t0 == response s1 t1))
        (ensures  (s0==s1 /\ t0==t1))

練習問題 12c:
Prove these three lemmas.

回答
let req_resp_distinct s s' t' =
  assert (Array.index (request s) 0 <> Array.index (response s' t') 0)
let req_components_corr s0 s1 = ()
let resp_components_corr s0 t0 s1 t1 = ()

Remark. In the lecture we also saw an extended protocol where we have a population of principals, represented as concrete strings ranged over by a and b, that intend to perform various remote procedure calls (RPCs) over a public network. The RPCs consist of requests and responses, both also represented as strings. The security goals of our RPC protocol are that (1) whenever a principal b accepts a request message s from a, principal a has indeed sent the message to b and, conversely, (2) whenever a accepts a response message t from b, principal b has indeed sent the message in response to a matching request from a.

12.4. Verified Padding

We intend to MAC and/or encrypt plaintexts of variable sizes using fixed-sized algorithms, such as those that operate on 256-bit blocks, such as AES.

To this end, we use the following classic padding scheme (used for instance in TLS).

module Pad
open Array

(* two coercions from uint8 <--> n:int { 0 <= n < 255 } *)
assume val n2b: n:nat {( n < 256 )} -> Tot uint8
assume val b2n: b:uint8 -> Tot (n:nat { (n < 256) /\ n2b n = b })

type bytes = seq byte (* concrete byte arrays *)
type nbytes (n:nat) = b:bytes{length b == n} (* fixed-length bytes *)

let blocksize = 32
type block = nbytes blocksize
type text = b:bytes {(length b < blocksize)}

let pad n = Array.create n (n2b (n-1))

let encode (a:text) = append a (pad (blocksize - length a))

let decode (b:block) =
  let padsize = b2n(index b (blocksize - 1)) + 1 in
  if op_LessThan padsize blocksize then
    let (plain,padding) = split b (blocksize - padsize) in
    if padding = pad padsize
    then Some plain
    else None
  else None

練習問題 12d:
What do these function do? Write as precise as possible typed specifications for these functions. In particular show that decoding cancels out encoding.

回答
val pad: n:nat { 1 <= n /\ n <= blocksize } -> Tot (nbytes n)
val encode: a: text -> Tot block
val decode: b:block -> Tot (option (t:text { Array.equal b (encode t)}))

練習問題 12e:
Is it a good padding scheme? What are its main properties?

Prove a lemma that expresses its injectivity.

Provide examples of other schemes, both good and bad.

回答

A padding scheme should be invertible. For authentication properties, we require it to be injective, so that authenticating a padded text unambiguously authenticate the text before padding. For instance:

val inj: a: text -> b: text -> Lemma (requires (Array.equal (encode a) (encode b)))
                                     (ensures (Array.equal a b))
                                     [SMTPat (encode a); SMTPat (encode b)]
                                     (decreases (length a))
let inj a b =
  if length a = length b
  then ()
  else let aa = encode a in
       let bb = encode b in
       cut (Array.index aa 31 =!= Array.index bb 31)

In this context, another good padding scheme is to append a 1 then enough zeros to fill the block. One could also format the message by explicitly including its length. A bad scheme is to fill the rest of the block with zeros (or random values), as the same padded text may then be parsed into several texts ending with 0s.

練習問題 12f:
Relying on that specification, implement and verify a MAC interface for messages of type text, i.e., of less than blocksize bytes, using the MAC interface below, which only supports messages of type block.

To this end, we assume given an implementation of the following module (adapted from mac.fst)

module BMAC
open Pad

let keysize = 16 (* these are the sizes for SHA1 *)
let macsize = 20
type key = nbytes keysize
type tag = nbytes macsize

opaque type key_prop : key -> block -> Type
type pkey (p:(block -> Type)) = k:key{key_prop k == p}

assume val keygen: p:(block -> Type) -> pkey p
assume val mac:    k:key -> t:block{key_prop k t} -> tag
assume val verify: k:key -> t:block -> tag -> b:bool{b ==> key_prop k t}

Write a similar module that accepts texts instead of blocks: first the implementations for keygen, mac, and verify, then type annotations to derive their authentication property (on texts) from the one of BMAC (on blocks).

回答
module TMAC
open Pad

let keysize = BMAC.keysize
let macsize = BMAC.macsize
type key = BMAC.key
type tag = BMAC.tag

opaque type bspec (spec: (text -> Type)) (b:block) =
  (forall (t:text). b = encode t ==> spec t)

opaque type key_prop : key -> text -> Type
type pkey (p:(text -> Type)) =
  k:key{key_prop k == p /\ BMAC.key_prop k == bspec p}

val keygen: p:(text -> Type) -> pkey p
val mac:    p:(text -> Type) -> k:pkey p -> t:text{p t} -> tag
val verify: p:(text -> Type) -> k:pkey p -> t:text -> tag -> b:bool{b ==> p t}

let keygen (spec: text -> Type) =
  let k = BMAC.keygen (bspec spec) in
  assume (key_prop k == spec);
  k

let mac (p:text -> Type) k t = BMAC.mac k (encode t)
let verify k t tag = BMAC.verify k (encode t) tag

練習問題 12g:
(1) Can we similarly construct a MAC scheme for texts with type text:bytes {length text <= n}? (2) Implement, then verify this construction.

回答

(1) Yes, using two keys: one for text:bytes {length b = n} and another for text:bytes {length b}.

(2) Code:

module MAC2
open Array
open Pad

type text2 = b:bytes { length b <=  blocksize }

let keysize = 2 * BMAC.keysize
let macsize = BMAC.macsize
type key = | Keys: k0:BMAC.key -> k1:BMAC.key -> key
type tag = BMAC.tag

opaque type bspec0 (spec: (text2 -> Type)) (b:block) =
  (forall (t:text). b = encode t ==> spec t)

opaque type bspec1 (spec: (text2 -> Type)) (b:block) =
  spec b

opaque type key_prop : key -> text2 -> Type

type pkey (p:(text2 -> Type)) =
  k:key{ key_prop k == p
      /\ BMAC.key_prop (Keys.k0 k) == bspec0 p
      /\ BMAC.key_prop (Keys.k1 k) == bspec1 p }

val keygen: p:(text2 -> Type) -> pkey p
val mac:    p:(text2 -> Type) -> k:pkey p -> t:text2{p  t} -> tag
val verify: p:(text2 -> Type) -> k:pkey p -> t:text2 -> tag -> b:bool{b ==> p t}

let keygen (spec: text2 -> Type) =
  let k0 = BMAC.keygen (bspec0 spec) in
  let k1 = BMAC.keygen (bspec1 spec) in
  let k = Keys k0 k1 in
  assert (BMAC.key_prop k0 == bspec0 spec);
  assert (BMAC.key_prop k1 == bspec1 spec);
  assume (key_prop k == spec);
  k

let mac (Keys k0 k1) t =
  if length t < blocksize
  then BMAC.mac k0 (encode t)
  else BMAC.mac k1 t

let verify (Keys k0 k1) t tag =
  if length t < blocksize
  then BMAC.verify k0 (encode t) tag
  else BMAC.verify k1 t tag

練習問題 12h:
What about MAC schemes for texts of arbitrary lengths? Hint: have a look e.g. at the HMAC construction.

13. Advanced cryptographic examples

13.1. Stateful Authenticated Encryption

A typical guarantee provided by a secure channel protocol is that messages are received in the same order in which they were sent. To achieve this, we construct a stateful, authenticated encryption scheme from a (stateless) “authenticated encryption with additional data” (AEAD) scheme (Rogaway 2002). Two counters are maintained, one each for the sender and receiver. When a message is to be sent, the counter value is authenticated using the AEAD scheme along with the rest of the message payload and the counter is incremented. The receiver, in turn, checks that the sender’s counter in the message matches hers each time a message is received and increments her counter.

Cryptographically, the ideal functionality behind this scheme involves associating a stateful log with each instance of a encryptor/decryptor key pair. At the level of the stateless functionality, the guarantee is that every message sent is in the log and the receiver only accepts messages that are in the logno guarantee is provided regarding injectivity or the order in which messages are received. At the stateful level, we again associate a log with each key pair and here we can guarantee that the sends and receives are in injective, order-preserving correspondence. Proving this requires relating the contents of the logs at various levels, and, importantly, proving that the logs associated with different instances of keys do not interfere. We give this proof in F*.

We start with a few types provided by the AEAD functionality.

module AEAD
type encryptor = Enc : #r:rid -> log:rref r (seq entry) -> key -> encryptor
and decryptor =  Dec : #r:rid -> log:rref r (seq entry) -> key -> decryptor
and entry =  Entry : ad:nat -> c:cipher -> p:plain -> basicEntry

An encryptor encapsulates a key (an abstract type whose hidden representation is the raw bytes of a key) with a log of entries stored in the heap for modeling the ideal functionality. Each entry associates a plain text p, with its cipher c and some additional data ad:nat. The log is stored in a region r, which we maintain as an additional (erasable) field of Enc. The decryptor is similar. It is worth pointing out that although AEAD is a stateless functionality, its cryptographic modeling involves the introduction of a stateful log. Based on a cryptographic assumption, one can view this log as ghost.

On top of AEAD, we add a Stateful layer, providing stateful encryptors and decryptors. StEnc encapsulates an encryption key provided by AEAD together with the sender's counter, ctr, and its own log of stateful entries, associates plain-texts with ciphers. The log and the counter are stored in a region r associated with the stateful encryptor. StDec is analogous.

module Stateful
type st_enc = StEnc : #r:rid -> log: rref r (seq st_entry) -> ctr: rref r nat
           -> key:encryptor{extends (Enc.r key) r} -> st_enc
and st_dec =  StDec : #r:rid -> log: rref r (seq st_entry) -> ctr: rref r nat
           -> key:decryptor{extends (Dec.r key) r} -> st_dec
and st_entry = StEntry : c:cipher -> p:plain -> st_entry

Exploiting the hierarchical structure of hyper-heaps, we store the AEAD.encryptor in a distinct sub-region of rthis is the meaning of the extends relation. By doing this, we ensure that the state associated with the AEAD encryptor is distinct from both log and ctr. By allocating distinct instances k1 and k2 in disjoint regions, we can prove that using k1 (say decrypt k1 c) does not alter the state associated with k2. In this simplified setting with just three references, the separation provided is minimal; when manipulating objects with sub-objects that contain many more references (as in our full development), partitioning them into separate regions provides disequalities between their references for free.

練習問題 13a:
Look at the following code, what happens in case of decryption failure?

type statefulEntry =
  | StEntry : c:cipher -> p:plain -> statefulEntry

type st_encryptor (i:rid) =
  | StEnc : log: rref i (seq statefulEntry) ->
            ctr: rref i nat ->
            key:encryptor i ->
            st_encryptor i

type st_decryptor (i:rid) =
  | StDec : log: rref i (seq statefulEntry) ->
            ctr: rref i nat ->
            key:decryptor i ->
            st_decryptor i

  ...

val stateful_enc : #i:rid -> e:st_encryptor i -> p:plain -> ST cipher
  (requires (fun h -> st_enc_inv e h))
  (ensures (fun h0 c h1 ->
            st_enc_inv e h1
         /\ HyperHeap.modifies (Set.singleton i) h0 h1
         /\ Heap.modifies (refs_in_e e) (Map.sel h0 i) (Map.sel h1 i)
         /\ sel h1 (StEnc.log e) = snoc (sel h0 (StEnc.log e)) (StEntry c p)))
let stateful_enc i (StEnc log ctr e) p =
    let c = enc e (op_Bang ctr) p in
    op_Colon_Equals log (snoc (op_Bang log) (StEntry c p));
    op_Colon_Equals ctr (op_Bang ctr + 1);
    c

val stateful_dec: #i:rid -> d:st_decryptor i -> c:cipher -> ST (option plain)
  (requires (fun h -> st_dec_inv d h))
  (ensures (fun h0 p h1 ->
        st_dec_inv d h0    //repeating pre
        /\ st_dec_inv d h1
        /\ HyperHeap.modifies (Set.singleton i) h0 h1
        /\ Heap.modifies !{as_ref (StDec.ctr d)} (Map.sel h0 i) (Map.sel h1 i)
        /\ Let (sel h0 (StDec.ctr d)) (fun (r:nat{r=sel h0 (StDec.ctr d)}) ->
           Let (sel h0 (StDec.log d))
           (fun (log:seq statefulEntry{log=sel h0 (StDec.log d)}) ->
           (is_None p ==> (r = Seq.length log           //nothing encrypted yet
                          || StEntry.c (Seq.index log r) <> c //wrong cipher
                            ) /\ sel h1 (StDec.ctr d) = r)
        /\ (is_Some p ==>
                  ((sel h1 (StDec.ctr d) = r + 1)
                   /\ StEntry.p (Seq.index log r) = Some.v p))))))

let stateful_dec _id (StDec _ ctr d) c =
  let i = op_Bang ctr in
  cut(trigger i);
  match dec d (op_Bang ctr) c with
    | None -> None
    | Some p -> op_Colon_Equals ctr (op_Bang ctr + 1); Some p

エディタに読み込む

13.2. Encryption

Next we will look into constructing basic encryption schemes from even lower level cryptographic primitives.

The basis of our first encryption example is the interface of a symmetric encryption scheme based on a block cipher, say AES. It uses a one block initialization vector (IV) that is XORed to the plaintext. The masked value is then enciphered. The ciphertext consists of the IV and this enciphered block.

module AES
open Array

type bytes = seq byte
type nbytes (n:nat) = b:bytes{length b == n}

let blocksize = 32 (* 256 bits *)

type plain  = nbytes blocksize
type cipher = nbytes (2 * blocksize)  (* including IV *)

let keysize = 16 (* 128 bits *)
type key = nbytes keysize

assume val gen: unit -> key
assume val dec: key -> cipher -> Tot plain
(* this function is pure & complete *)
assume val enc: k:key -> p:plain -> c:cipher

練習問題 13b:
Refine the type of the encryption function to model the correctness property: A correctly generated ciphertext, decrypts to its plaintext.

assume val enc: k:key -> p:plain -> c:cipher

エディタに読み込む

回答
assume val enc: k:key -> p:plain -> c:cipher{ dec k c = p }
(* this function is not pure (samples IV);
   the refinement captures functional correctness *)

We model perfect secrecy by typing using type abstraction. As concrete cryptographic algorithms such as the one above talk about bytes, we now introduce the notion of a symmetric encryption scheme that enforces type abstraction for safe keys.

A scheme is parameterized by a key type k for keys and a plain type p that abstractly defines plaintexts.

Keys are abstract to enforce a well typed key usage regime on well typed users of the module.

module SymEnc (* a multi-key symmetric variant; for simplicity:
                 (1) only using AES above; and (2) parsing is complete *)

type r = AES.plain

(* CPA variant: *)
opaque type Encrypted: #k: Type -> p:Type -> k -> AES.bytes -> Type
(* an opaque predicate, keeping track of honest encryptions *)

type cipher (p:Type) (k:Type) (key:k) = c:AES.cipher { Encrypted p key c }

The type of cipher records the plain type, key type, and key it was generated for.

type keyT: Type -> Type =
  | Ideal    : p:Type -> AES.key -> i:int -> keyT p
  | Concrete : p:Type -> AES.key -> i:int -> keyT p

Keys record whether they were correctly generated Ideal in which case their usage will provide security by type abstraction, or not, in which they are just concrete keys that can be leaked to the adversary.

type scheme: Type -> Type =
  | Scheme:  p:Type -> k:Type ->
             keyrepr: (k -> AES.key) ->
             keygen:  (bool -> k) ->
             encrypt: (key:k -> p -> cipher p k key) ->
             decrypt: (key:k -> cipher p k key -> p) ->
             scheme p

A scheme records a plain type p, a function keyrepr for breaking key abstraction, a key generation function keygen, and encryption and decryption functions encrypt and decrypt.

type entry (p:Type) (k:Type) =
  | Entry : key:k -> c:cipher p k key -> plain:p -> entry p k

To create a cryptographic scheme one needs to provide a plain function for turning bytes into the plain type values and a repr function for turning plain type values into bytes.

val create: p: Type -> plain: (r -> p) -> repr: (p -> r) -> scheme p

The create function instantiates the scheme using the AES module.

let create (p:Type) plain repr =
  let c = ST.alloc 0 in
  let log : ref (list (entry p (keyT p))) = ST.alloc [] in

  let keygen : bool -> keyT p = fun safe ->
    let i = !c in
    c := !c + 1;
    let kv = AES.gen() in
    if safe
    then Ideal    p kv i
    else Concrete p kv i in

  let keyrepr k : AES.key =
    match k with
    | Ideal kv _ -> failwith "no way!"
    | Concrete kv _ -> kv in

  let encrypt: (k:keyT p -> p -> cipher p (keyT p) k) = fun k text ->
    match k with
    | Ideal kv _ ->
       let c = AES.enc kv AES.dummy in
       assume (Encrypted p k c);
       log := Entry k c text :: !log;
       c

    | Concrete kv _ ->
       let rep = repr text in
       (* NS: need the let-binding because repr is impure and we can't
          substitute it in the type of 'enc' *)
       let c = AES.enc kv rep in
       assume (Encrypted p k c);
       c in

  let decrypt: key:keyT p -> cipher p (keyT p) key -> p = fun k c ->
    match k with
    | Ideal kv _ -> (match List.find (fun (Entry k' c' _) -> k=k' && c= c') !log with
                     | Some e -> Entry.plain e
                     | _ -> failwith "never")
    | Concrete kv _ -> plain (AES.dec kv c)  in

  Scheme p (keyT p) keyrepr keygen encrypt decrypt

Relying on basic cryptographic assumptions (IND-CPA), the ideal implementation never accesses plaintexts when using Ideal keys!

Formally, the Ideal branch can be typed using an abstract plaintype: encrypt encrypts a constant AES block c and logs Entry k c text decrypt returns text when Entry k c text is in the log. As IND-CPA requires that only ciphertext that have previously been encrypted are decrypted, this is guaranteed by typing to be always the case.

Here is how such a symmetric encryption scheme would be used in an example:

module SampleEncrypt
open SymEnc
let plain (x:AES.plain) = x
let repr (x:AES.plain) = x

let test() =
  let p = failwith "nice bytes" in
  let Scheme keyrepr keygen encrypt decrypt = SymEnc.create (AES.plain) plain repr in
  let k0 = keygen true in
  let k1 = keygen true in
  let c = encrypt k0 p in
  let p' = decrypt k0 c in
  assert( p == p');                // this succeeds, as we enforce functional correctness
  (* let p'' = decrypt k1 c in     // this rightfully triggers an error *)
  ()