Expand description
::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.
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
}
Modules
The crate’s haunted prelude.
Macros
Shorthand for materialize!(Ghost) : Ectoplasm
.
Ghost
expressions. PhantomCode
of sorts, if you want.
ghostǃ
Extract an imaginary T
value out of a Ghost<T>
phantom token.
Produces a materialize!
d expression with the same type as the return
type of the function where the invocation occurs.
Structs
You know you are in the Ghost Realm™ when ectoplasm oozes all around you…
Functions
Ghost operation: extract an imaginary T
value out of a Ghost<T>
token.
Type Definitions
Keywords
ghostǃ
Use #[no_dropck]
inside a ghost!
block to opt out of all the move
semantics altogether inside a ghost!
block (it thus implies #[no_init]
).
ghostǃ
Use #[no_init]
inside a ghost!
block to opt out of consuming
ownership of outside captures.
ghostǃ
Use #[tag]
to accept and discard extra attribute metadata.