This repository contains the port of IronSync's Node Replication proofs to Verus. The proof uses the IronSync methodology that was ported to Verus. The toolchain will produce a library crate that then can be used in Rust programs.
See the LICENSE file.
Obtaining Verus
Before you can verify the node-replication crate, you will need to obtain and build Verus. You can do that by initializing the Verus submodule with
$ bash tools/setup-verus.sh
Alternatively, you can initialize the Verus git submodule manually.
Building Verus
Then to build Verus, you can follow the instructions in the Verus repository. Alternatively, you can also build Verus using the provided script:
bash tools/build-verus.sh
The script obtains the dependencies and builds Verus.
To verify the node-replication crate, you can use the following command:
$ bash tools/verify-node-replication.sh
If you see an output like the following, then this means that verification was successful:
Verifying 'verified-node-replication/src/lib.rs' ...
verification results:: 254 verified, 0 errors
Simply add a dependency to verified-node-replication and Verus builtin to your Cargo.toml:
builtin = { path = "verus/source/builtin" }
verified-node-replication = { path = "verified-node-replication" }Paths relative to the repository root. See the examples directory for some examples on how to use NR.
We implemented a few benchmarks that compare the verified implementation with upstream (unverified) node replication, and IronSync's Dafny-based node replication. See the benchmarks directory for more information.