::鬼魂

为有趣和盈利™类型检查不存在的 Phantom 代码。

原因

有时你可能想编写应该像真实 Rust 代码一样进行类型检查（例如，借用检查）的 Rust 代码，即使这些代码永远不会被执行/影响或甚至到达代码生成。

为什么？好吧，这个需求非常特殊。但是代码验证工具可以从这中受益，因此有一个提议要添加一些语言特性来支持这一点。

这个包是一个演示，说明大多数这样的特性都可以通过现有的稳定 Rust 代码实现，这要归功于宏、类型推断和 if false（+ 不可达代码路径）技巧。

use ::ghosts::vestibule::*;

type Nat = u64;

fn fibo (
    ghost_ctx: Ectoplasm,
    n: Ghost<Nat>,
) -> Nat
{
    let n = ghost_ctx.materialize(n);
    ghost!(#[tag(decreases)] #[no_init] { n });
    match n {
        | 0 => 0,
        | 1 => 1,
        | _ => {
            fibo(ghost_ctx, ghost!(n - 1))
            +
            fibo(ghost_ctx, ghost!(n - 2))
        },
    }
}

fn lemma_fibo_is_monotonic (
    ghost_ctx: Ectoplasm,
    i: Ghost<Nat>,
    j: Ghost<Nat>,
)
{
    let i = ghost_ctx.materialize(i);
    let j = ghost_ctx.materialize(j);
    ghost!(#[tag(requires)] #[no_init] { i <= j });
    ghost!(#[tag(ensures)] #[no_init] { i <= j });
    ghost!(#[tag(ensures)] #[no_init] {
        fibo(ghost_ctx, ghost!(i)) <= fibo(ghost_ctx, ghost!(j))
    });
    ghost!(#[tag(decreases)] #[no_init] { j - 1 });

    match () {
        | _case if i < 2 && j < 2 => {},
        | _case if i == j => {},
        | _case if i == j - 1 => {
            lemma_fibo_is_monotonic(ghost_ctx, ghost!(i), ghost!(j - 1));
        },
        | _default => {
            lemma_fibo_is_monotonic(ghost_ctx, ghost!(i), ghost!(j - 1));
            lemma_fibo_is_monotonic(ghost_ctx, ghost!(i), ghost!(j - 2));
        },
    }
}

fn fibo_fits_u64 (
    ghost_ctx: Ectoplasm,
    n: Ghost<Nat>,
) -> bool
{
    fibo(ghost_ctx, n) <= 0xffff_ffff_ffff_ffff
}

fn assume (
    _: bool
)
{}

fn fibo_impl (n: u64)
  -> u64
{
    ghost!(#[tag(requires)] #[no_init] |ectoplasm| {
        fibo_fits_u64(ectoplasm, ghost!(n))
    });
    ghost!(#[tag(ensures)] #[no_init] |ectoplasm| {
        materialize_return!() == fibo(ectoplasm, ghost!(n))
    });

    if n == 0 {
        return 0;
    }
    let mut prev: u64 = 0;
    let mut cur: u64 = 1;
    let mut i: u64 = 1;
    while i < n {
        ghost!(#[tag(invariant)] #[no_init] |ectoplasm| [
            i > 0,
            i <= n,
            fibo_fits_u64(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] n as Nat),
            ),
            fibo_fits_u64(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] i as Nat),
            ),
            cur == fibo(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] i),
            ),
            prev == fibo(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] { i as Nat - 1 }),
            ),
        ]);
        ghost!(#[tag(proof)] {
            assume(cur as Nat + prev <= 0xffff_ffff_ffff_ffff);
        });
        let new_cur = cur + prev;
        prev = cur;
        cur = new_cur;
        i += 1;
        ghost!(#[tag(proof)] |ectoplasm| {
            lemma_fibo_is_monotonic(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] { i }),
                ghost!(#[tag(spec_expr)] #[no_init] { n }),
            );
        });
    }
    cur
}