VPS builds verified binary parsers and serializers in Rust and Verus. This repository contains the implementation and evaluation material for the paper.
| Paper section | Source code |
|---|---|
| Design: malleability | combinators/choice and combinators/mapped |
| Design: recursion | combinators/recursive/ |
| Formalization and trait system | core/spec.rs, core/proof.rs and combinators/ |
| Efficient parser and serializer APIs | core/exec/ |
| ASN.1 BER, DER, and CMS case study | asn1/, vps-asn1/, and the CMS schema |
| CBOR case study | cbor/ |
| Evaluation | evaluation/README.md, RESULTS.md, and generate_eval_plots.py |
The TLS and Bitcoin case studies use the existing Vest language. The compiler
in vest-dsl-vps/ ports that language to a backend that emits VPS combinators;
the language itself is not a contribution. baselines/ contains the original
Vest implementation used in the paper's direct comparison.
The project uses cargo verus and the vstd version pinned in each manifest.
cargo test --manifest-path vps-lib/Cargo.toml
cargo test --manifest-path vest-dsl-vps/Cargo.toml
cargo test --manifest-path vps-asn1/Cargo.toml
cd vps-lib
cargo verus verify -- --expand-errorsGenerated-code suites can be rebuilt and verified with make generate and
make verify in vest-dsl-vps/test/ and vps-asn1/test/.
See evaluation/README.md for the short reproduction
commands. The large Bitcoin runtime input is not stored here; its checksum and
setup instructions are in
evaluation/corpora/bitcoin/README.md.