Commit df6c8179 authored by Hai Dang's avatar Hai Dang
Browse files

more update to README

parent 02d61030
Pipeline #42817 passed with stage
in 23 minutes and 32 seconds
......@@ -22,16 +22,16 @@ To run an example, use `cargo run --example branded_vec` from the [`ghostcell`]
## 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`, the benchmarks are in `ghostcell/benches/dlist.rs`.
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/dlist.rs`](ghostcell/benches/dlist.rs).
The benchmark results are in `benchmarks-data`; open `report/index.html` in a browser to view them.
You can run the benchmarks again from the `ghostcell` directory with the command `cargo bench`.
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.
# Coq proof
Our Coq proof is based on the RustBelt formalization at https://gitlab.mpi-sws.org/iris/lambda-rust.
Our Coq proof is based on the [RustBelt formalization](https://gitlab.mpi-sws.org/iris/lambda-rust).
## Prerequisites
......@@ -60,8 +60,8 @@ followed by `make build-dep`.
## Where to find the proofs
The `BrandedVec` soundness proof is in `theories/typing/lib/brandedvec.v`.
The `GhostCell` soundness proof is in `theories/typing/lib/ghostcell.v`.
The `BrandedVec` soundness proof is in [`theories/typing/lib/brandedvec.v`](theories/typing/lib/brandedvec.v).
The `GhostCell` soundness proof is in [`theories/typing/lib/ghostcell.v`](theories/typing/lib/ghostcell.v).
[`ghostcell`]: ghostcell/
[`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