Verusによるmimallocの検証

spec fn gt_any(x: nat, ls: Seq<nat>) -> bool
{
    forall|i: int| 0 <= i && i < ls.len() ==> x >= ls[i]
}

fn main() {
    assert(!gt_any(1, seq![1, 2, 3]));
    assert(gt_any(3, seq![1, 2, 3]));
}

struct S { x: usize }

impl S {
    // 古いself.xがインクリメントしてもオーバフローしない範囲ならば、
    // self.inc()の呼び出し後には、正しくインクリメントされて返り値もその値になっている
    fn safe_inc(&mut self) -> (r: usize)
        requires
            0 <= old(self).x, // カンマ区切りで並べることができる(.. && .. 相当)
            old(self).x < usize::MAX
        ensures r == self.x == old(self).x + 1
    {
        self.x = self.x + 1; self.x
    }
}

impl S {
    spec fn view(&self) -> int {
        self.x as int
    }
}

// allocation
let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();
// free
p.free(Tracked(points_to)); // points_to moved here
// use after free
p.write(Tracked(&mut points_to), 5); // fails because points_to moved above

use vstd::prelude::*;
use vstd::simple_pptr::*;
#[derive(Clone, Copy)]
pub struct Node {
    next: Option<PPtr<Node>>,
    x: usize
}

pub struct LList {
    first: Option<PPtr<Node>>,
    // すべてのノードへのポインタとトークンを追跡
    gs: Tracked<GhostState>
}

pub struct GhostState {
    // 追加時のリストの長さをキーにして各ノードへのポインタのトークンを格納している
    tracked perms: Map<nat, PointsTo<Node>>,
    // 追加された順に各ノードへのポインタが格納されている
    ghost ptrs: Seq<PPtr<Node>>
}

impl LList {
    // リンクリストのノードを追加順に並べたもの
    // (self.firstから辿っていったときの要素のリストを*逆順にしたもの*)
    pub closed spec fn view(&self) -> Seq<usize> {
        // 添字を引数に取るクロージャでSeqを生成する
        Seq::<usize>::new(
            self.gs@.ptrs.len(), // 長さ
            // permsはノードの追加時のリストの長さがキーなため､最後に追加した要素が先頭になる
            |i: int| { self.gs@.perms[i as nat].value().x },
        )
    }

    // ノードへのポインタを追跡しているSeqを使って､与えられた添字から次のノードを返す
    pub closed spec fn next_of(&self, i: nat) -> Option<PPtr<Node>> {
        if i == 0 {
            None
        } else {
            // 添字が若いほど追加した時点が古い(i.e. リストの後の方にある)ためi-1が次のノードとなる
            Some(self.gs@.ptrs[i as int - 1])
        }
    }

    // 与えられた添字に対して対応するノードのGhostState内の状態とメモリ上の表現が
    // 整合していることを示す
    pub closed spec fn wf_node(&self, i: nat) -> bool {
        &&& self.gs@.perms.dom().contains(i)
            &&& self.gs@.perms[i].pptr() == self.gs@.ptrs[i as int]
            &&& self.gs@.perms[i].mem_contents() matches MemContents::Init(node)
            && node.next == self.next_of(i)
    }

    pub closed spec fn wf(&self) -> bool {
        &&& forall|i: nat| 0 <= i && i < self.gs@.ptrs.len() ==> self.wf_node(i)
            &&& if self.gs@.ptrs.len() == 0 {
                self.first.is_none()
            } else {
                self.first == Some(self.gs@.ptrs[self.gs@.ptrs.len() - 1])
            }
    }

    pub fn push_front(&mut self, v: usize)
        // 実行の前後で内部構造の整合性が保たれること､
        // viewによる表現が期待通り更新されることを保証する
        requires old(self).wf(),
        ensures
            self.wf(),
            // リストに要素が追加される
            self@ =~= old(self)@.push(v) // =~= はコンテナのための等号
    {
        if let Some(old_first) = self.first {
            proof {
                assert(self.wf_node((self.gs@.ptrs.len() - 1) as nat));
            }
            let (node, Tracked(mut perm)) = PPtr::<Node>::new(Node { next: Some(old_first.clone()) , x: v});
            self.first = Some(node);

            proof {
                // ghost stateの更新: ノードへのポインタとその権限を追加
                self.gs@.ptrs = self.gs@.ptrs.push(node);
                self.gs.borrow_mut().perms.tracked_insert((self.gs@.ptrs.len() - 1) as nat, perm);

                assert(forall|i: nat| i < self.gs@.ptrs.len() && old(self).wf_node(i)
                    ==> self.wf_node(i));
                assert forall|i: int| 0 <= i && i  < old(self)@.len()
                    implies old(self)@[i] == self@[i]
                by {
                    assert(old(self).wf_node(i as nat));
                }
                assert(self@ =~= old(self)@.push(v));
            }
        } else {
            // まだリストが空な場合
            let (node, Tracked(mut perm)) = PPtr::<Node>::new(Node { next: None, x: v });
            self.first = Some(node);
            proof {
                // ghost stateの更新: ノードへのポインタとその権限を追加
                self.gs@.ptrs = self.gs@.ptrs.push(node);
                self.gs.borrow_mut().perms.tracked_insert(
                    (self.gs@.ptrs.len() - 1) as nat,
                    perm,
                );
            }
        }
    }


    pub fn pop_front(&mut self) -> (r: Option<usize>)
        requires
            old(self).wf()
        ensures
            self.wf(),
            // リストが空ならNone
            old(self)@.len() == 0 ==> r == None::<usize>,
            // さもなければ先頭ノードの値を返して、リストが縮小する
            old(self)@.len() > 0 ==> r == Some(old(self)@.last())
                && self@ =~= old(self)@.drop_last()
    {
        if let Some(old_first) = self.first {
            assert(self.wf_node((self.gs@.ptrs.len() - 1) as nat));
            // ghost stateの更新: 一番目のノードへの権限を削除
            let tracked old_first_perm = self.gs.borrow_mut()
                .perms.tracked_remove((self.gs@.ptrs.len() - 1) as nat);
            // ノードへのポインタをデリファレンス、領域を解放
            let old_first_node = old_first.into_inner(Tracked(old_first_perm));
            self.first = old_first_node.next;
            proof {
                // ghost stateの更新: ノードへのポインタを削除
                self.gs@.ptrs = self.gs@.ptrs.drop_last();
                assert(forall|i: nat|
                    i < self@.len() && old(self).wf_node(i) ==> self.wf_node(i));

                assert forall|i: int| 0 <= i && i  < self@.len()
                    implies old(self)@[i] == self@[i]
                by {
                    assert(old(self).wf_node(i as nat));
                }
            }
            Some(old_first_node.x)
        } else {
            None
        }
    }
}