::ghosts

Type-check non-existing Phantom code for Fun And Profit™.

Rationale

Sometimes you may want to write Rust code that ought to be type-checked (e.g., borrow-checked) in the same fashion as real Rust code even though that code is never intended to be run / to affect or even reach code generation.

Why? Well, ok, this need is incredibly niche. But code verification tools can benefit from this, so [there is a proposal out there] to add a bunch of magic language features just to support this.

This crates is a demonstration of the vast majority of such features being achievable within already existing Stable Rust code, thanks to macros, type inference, and if false (+ unreachable code paths) tricks.

```rust use ::ghosts::vestibule::*;

type Nat = u64;

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

fn lemmafiboismonotonic ( ghostctx: Ectoplasm, i: Ghost, j: Ghost, ) { let i = ghostctx.materialize(i); let j = ghostctx.materialize(j); ghost!(#[tag(requires)] #[noinit] { i <= j }); ghost!(#[tag(ensures)] #[noinit] { i <= j }); ghost!(#[tag(ensures)] #[noinit] { fibo(ghostctx, ghost!(i)) <= fibo(ghostctx, ghost!(j)) }); ghost!(#[tag(decreases)] #[noinit] { 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 fibofitsu64 ( ghostctx: Ectoplasm, n: Ghost, ) -> bool { fibo(ghostctx, n) <= 0xffffffffffff_ffff }

fn assume ( _: bool ) {}

fn fiboimpl (n: u64) -> u64 { ghost!(#[tag(requires)] #[noinit] |ectoplasm| { fibofitsu64(ectoplasm, ghost!(n)) }); ghost!(#[tag(ensures)] #[noinit] |ectoplasm| { materializereturn!() == 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

} ```