RustBeltの examples/get_x.v をいじってみた。
From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section get_x.
Context `{typeG Σ}.
Definition get_x : val :=
funrec: <> ["p"] :=
let: "p'" := !"p" in
letalloc: "r" <- "p'" +ₗ #0 in
delete [ #1; "p"] ;; return: ["r"].
Lemma get_x_type :
typed_val get_x (fn(∀ α, ∅; &uniq{α} Π[int; int]) → &shr{α} int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
inv_vec p=>p. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
End get_x.
これはだいたい以下のようなプログラムを表しているようだ。
fn get_x<'a>(p: &'a mut (i32, i32)) -> &'a i32 { &p.0 }
ただし、現在のλRustでは整数型はひとつしかなく、無限に大きな整数を保持可能で、サイズは1である (ポインタのサイズも1)。
これを
fn fst<'a, T, U>(p: &'a mut (T, U)) -> &'a T { &p.0 }
に一般化してみた。試行錯誤の結果、以下のようにすると上手くいくことがわかった。
From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section get_x.
Context `{typeG Σ}.
Definition get_x T U `{!TyWf T} `{!TyWf U} : val :=
funrec: <> ["p"] :=
let: "p'" := !"p" in
letalloc: "r" <- "p'" +ₗ #0 in
delete [ #1; "p"] ;; return: ["r"].
Lemma get_x_type T U `{!TyWf T} `{!TyWf U} :
typed_val (get_x T U) (fn(∀ α, ∅; &uniq{α} Π[T; U]) → &shr{α} T).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
inv_vec p=>p. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
iApply (type_letalloc_1 (&shr{α}T)); [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
End get_x.
同様に、
fn snd<'a, T, U>(p: &'a mut (T, U)) -> &'a U { &p.1 }
は以下のように定義できた。
From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section snd.
Context `{typeG Σ}.
Definition snd T U `{!TyWf T} `{!TyWf U} : val :=
funrec: <> ["p"] :=
let: "p'" := !"p" in
letalloc: "r" <- "p'" +ₗ #(T.(ty_size)) in
delete [ #1; "p"] ;; return: ["r"].
Lemma snd_type T U `{!TyWf T} `{!TyWf U} :
typed_val (snd T U) (fn(∀ α, ∅; &uniq{α} Π[T; U]) → &shr{α} U).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
inv_vec p=>p. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
iApply (type_letalloc_1 (&shr{α}U)); [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
End snd.
わかったこと
lrust.typing.typingをインポートするとよくて、lrust.typing.lib.*にCell等のライブラリがあるlrust.typing.examplesに例がある`{typeG Σ}は共通のコンテキストとして出てくる- まずMIRもどきを
Definitionで与え、あとからLemmaで型をつける。 - ライフタイムの多相性はλRustで扱われているが、型多相性はメタレベルで表現する。
funrecは関数定義。!はメモリを読む。deleteはサイズと先頭番地を引数に取りヒープまたはスタックを解放する。 (ヒープとスタックは同等に扱われる)#xは定数リテラル。+ₗはポインタと整数の足し算。- 型は
typeで、これは@type _ H(Hは冒頭のContextで宣言されているやつ) - 不正な再帰型を避けるために、各型がwell-formedであることの保証を持ち回す必要がある。これは
`{!TyWf T}で実現できる。 ∀α, ∅; Tは生存期間に関する量化で、∅は多分境界がないことを意味している。&uniq{α} Tと&shr{α} Tは&'a mut Tと&'a T。Π[A; B; C]は(A, B, C)std::mem::size_of::<T>()が欲しいときは#(T.(ty_size))と書く- unsized typeのサポートは今のところなくて、
typeは全部Sizedな型を表す
