Type-check non-existing `Phantom` code for Fun And Profit

Last update: May 13, 2022

::ghosts

Type-check non-existing Phantom code for Fun And Profitâ„¢.

Repository Latest version Documentation MSRV unsafe forbidden License CI

image

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
{
    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,
    j: Ghost,
)
{
    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 => {
            // reveal_with_fuel(fibo, 2);
            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,
) -> 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
}

GitHub

https://github.com/danielhenrymantilla/ghosts.rs
You might also like...

Generate bindings to use Rust code in Qt and QML

Generate bindings to use Rust code in Qt and QML

Rust Qt Binding Generator This code generator gets you started quickly to use Rust code from Qt and QML. In other words, it helps to create a Qt based

May 27, 2022

Code for connecting an RP2040 to a Bosch BNO055 IMU and having the realtime orientation data be sent to the host machine via serial USB

Code for connecting an RP2040 (via Raspberry Pi Pico) to a Bosch BNO055 IMU (via an Adafruit breakout board) and having the realtime orientation data be sent to the host machine via serial USB.

Feb 14, 2022

Removes generated and downloaded files from code projects to free up space

makeclean Removes generated and downloaded files from code projects to free up space. Features: List, cleans and archives projects depending on how lo

Mar 11, 2022

Rust library to scan files and expand multi-file crates source code as a single tree

syn-file-expand This library allows you to load full source code of multi-file crates into a single syn::File. Features: Based on syn crate. Handling

Apr 7, 2022

Migrate C code to Rust

Migrate C code to Rust

C2Rust helps you migrate C99-compliant code to Rust. The translator (or transpiler) produces unsafe Rust code that closely mirrors the input C code. T

May 24, 2022

Mix async code with CPU-heavy thread pools using Tokio + Rayon

tokio-rayon Mix async code with CPU-heavy thread pools using Tokio + Rayon Resources Documentation crates.io TL;DR Sometimes, you're doing async stuff

May 12, 2022

Minimal, flexible framework for implementing solutions to Advent of Code in Rust

This is advent_of_code_traits, a minimal, flexible framework for implementing solutions to Advent of Code in Rust.

Apr 17, 2022

Waits until the exit code of a program is zero

Waitz A rust utility to wait that a program exits with 0. You need to wait for something to start up and don't know when it finishes?

Apr 10, 2022

Sample code for compute shader 101 training

Sample code for Compute Shader 101 This repo contains sample code to help you get started writing applications using compute shaders.

May 26, 2022
Related tags
Check for SHA256 collisions.
Check for SHA256 collisions.

Coll SHA256 Collision Finder What's This? I was curious how long it might take to find a collision for an SHA256 hash created from an arbitrary file o

Jan 9, 2022
tiny_id is a Rust library for generating non-sequential, tightly-packed short IDs.

tiny_id tiny_id is a Rust library for generating non-sequential, tightly-packed short IDs. Most other short ID generators just string together random

Jan 19, 2022
CBOR (binary JSON) for Rust with automatic type based decoding and encoding.

THIS PROJECT IS UNMAINTAINED. USE serde_cbor INSTEAD. This crate provides an implementation of RFC 7049, which specifies Concise Binary Object Represe

May 22, 2022
Error context library with support for type-erased sources and backtraces, targeting full support of all features on stable Rust

Error context library with support for type-erased sources and backtraces, targeting full support of all features on stable Rust, and with an eye towards serializing runtime errors using serde.

Feb 12, 2022
A memory efficient immutable string type that can store up to 24* bytes on the stack

compact_str A memory efficient immutable string type that can store up to 24* bytes on the stack. * 12 bytes for 32-bit architectures About A CompactS

Apr 30, 2022
Mononym is a library for creating unique type-level names for each value in Rust.

Mononym is a library for creating unique type-level names for each value in Rust.

May 15, 2022
An annotated string type in Rust, made up of string slices

A string type made up of multiple annotated string slices.

Feb 14, 2022
Type-safe IPC for Tauri using GraphQL

Tauri Plugin graphql A plugin for Tauri that enables type-safe IPC through GraphQL. Install Rust [dependencies] tauri-plugin-graphql = "0.2" JavaScrip

May 18, 2022
The most fundamental type for async synchronization: an intrusive linked list of futures

wait-list This crate provides WaitList, the most fundamental type for async synchronization. WaitList is implemented as an intrusive linked list of fu

May 9, 2022
Detect if code is running inside a virtual machine (x86 and x86-64 only).

inside-vm Detect if code is running inside a virtual machine. Only works on x86 and x86-64. How does it work Measure average cpu cycles when calling c

Nov 15, 2021