This repository contains the artifacts discussed in my master's thesis Verified Paging for x86-64 in Rust.
The contents of the repository are as follows:
- The thesis itself thesis.pdf.
- The directory verified-page-table contains the main artifact, a page table implementation formally verified for functional correctness on x86-64. (A few proof steps are incomplete, refer to the thesis for details.)
- The directory erased-verified-page-table contains a version of the implementation where all specification and proof code was removed. Note that this is a slightly older version than the one in verified-page-table but the relevant functions are mostly unchanged.
- The directory evaluation/verifier_evaluation contains the data discussed in Section 12.1 of the thesis and instructions for how to reproduce the data.
- The directory evaluation/benchmarks/nros_benchmarks contains the data discussed in Section 12.3.1 of the thesis.
- The directory evaluation/benchmarks/single-threaded-benchmarks contains the data discussed in Section 12.3.2 of the thesis and instructions for how to reproduce the data.
- The directory verus_examples contains the code used to introduce Verus in Chapter 3 of the thesis.