RustBelt試行中: get_x の一般化

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 な型を表す