Commit 02d61030 authored by Hai Dang's avatar Hai Dang
Browse files

more update to README

parent 0317f23a
Pipeline #42813 passed with stage
in 24 minutes and 31 seconds
......@@ -12,10 +12,13 @@ To build and run the Rust code, you will need to
The Rust examples in the paper can be found in [`ghostcell/examples/`](ghostcell/examples/).
More specifically:
- For Section 2, see `branded_vec.rs`.
- For Section 3, see `dlist_arena_paper.rs`. The doubly-linked list API and implementation is in [`ghostcell/src/dlist_arena.rs`](ghostcell/src/dlist_arena.rs)
- For Section 2, see [`branded_vec.rs`]((ghostcell/examples/branded_vec.rs).
- For Section 3, see [`dlist_arena_paper.rs`](ghostcell/examples/dlist_arena_paper.rs).
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)
To run an example, use `cargo run --example branded_vec` from the [`ghostcell`](ghostcell) directory.
To run an example, use `cargo run --example branded_vec` from the [`ghostcell`] directory.
## Benchmarks
......@@ -34,7 +37,7 @@ Our Coq proof is based on the RustBelt formalization at https://gitlab.mpi-sws.o
This version is known to compile with:
- Coq 8.11.0
- Coq 8.11.2
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris) (see the [`opam`](opam) file for the exact version).
## Building from source
......@@ -59,3 +62,6 @@ followed by `make build-dep`.
The `BrandedVec` soundness proof is in `theories/typing/lib/brandedvec.v`.
The `GhostCell` soundness proof is in `theories/typing/lib/ghostcell.v`.
[`ghostcell`]: ghostcell/
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment