# ghostcell

**Repository Path**: FakedWeiss/ghostcell

## Basic Information

- **Project Name**: ghostcell
- **Description**: A novel safe and zero-cost borrow-checking paradigm from the GhostCell paper.
http://plv.mpi-sws.org/rustbelt/ghostcell/paper.pdf
- **Primary Language**: Rust
- **License**: BSD-3-Clause
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2021-09-05
- **Last Updated**: 2024-06-04

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# GhostCell: Separating Permissions from Data in Rust

This is the artifact accompanying our paper.
It consists of two parts: a Rust implementation with examples and benchmarks, and a Coq proof.

# Rust implementation

To build and run the Rust code, you will need to
[install cargo](https://doc.rust-lang.org/stable/cargo/getting-started/installation.html).


## Source code and Benchmarks

The source code for `GhostCell` and for the benchmarks that we ran can be found in [`ghostcell`].
The `GhostCell` code is in [`ghostcell/src/lib.rs`](ghostcell/src/lib.rs), the benchmarks are in [`ghostcell/benches`](ghostcell/benches).

The benchmark results are in [`benchmarks-data`](benchmarks-data); open [`report/index.html`](benchmarks-data/report/index.html) in a browser to view them.
You can run the benchmarks again from the [`ghostcell`] directory with the command `cargo bench`.
You can filter benchmarks to run by keywords, for example `cargo bench "ghostcell"` will run all GhostCell benchmarks.

## Examples

The Rust examples in the paper can be found in [`ghostcell`](ghostcell).
More specifically:
- For Section 2, see [`branded_vec.rs`](ghostcell/examples/branded_vec.rs).
- For Section 3.2, see [`dlist_arena_paper.rs`](ghostcell/examples/dlist_arena_paper.rs) for the example client shown in the paper.
  The doubly-linked list API and implementation is in [`ghostcell/src/dlist_arena.rs`](ghostcell/src/dlist_arena.rs).
- [`dlist_arc.rs`](ghostcell/examples/dlist_arc.rs) contains an example using a doubly-linked list built with `GhostCell` and `Arc`.
  The implementation is in [`ghostcell/src/dlist_arc.rs`](ghostcell/src/dlist_arc.rs).
- For Section 3.3, see [`ghostcell/src/dfs_arena.rs`](ghostcell/src/dfs_arena.rs) for the Graph and DFS iterator.

To run an example, use `cargo run --example branded_vec` from the [`ghostcell`] directory.

# Coq proof

Our Coq proof is part of the [RustBelt formalization](https://gitlab.mpi-sws.org/iris/lambda-rust).
Please follow the instructions there to get access to and build the most up-to-date version.
Alternatively, in this artifact we provide a snapshot of the Coq proof (see details where to find the proofs below) and its dependencies (except for Coq itself).

## How to build the snapshot in this artifact

- Install Coq. We have tested this with version 8.13.1. (In the VM, Coq is already installed.)
- Build the `stdpp` dependency: go to the `stdpp` directory and run `make -jN` to build, where `N` is the number of CPU cores you want to use.
  Then run `make install` to install the library.
- Build the `iris` dependency: go to the `iris` directory, similarly run `make -jN` and then `make install`.
- Build the the Coq proof: go to the root directory of this artifact and run `make -jN`.

## Where to find the proofs

- The `BrandedVec` soundness proof (§4.3) is in [`theories/typing/lib/brandedvec.v`](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/lib/brandedvec.v).
- The `GhostCell` soundness proof (§4.4) is in [`theories/typing/lib/ghostcell.v`](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/lib/ghostcell.v).
- The new version of the "lifetime equalization" rule (§4.2) is `type_equivalize_lft` in [`theories/typing/programs.v`](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/programs.v).
  The example that motivated the rule is [`theories/typing/examples/nonlexical.v`](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/examples/nonlexical.v).

[`ghostcell`]: ghostcell