Plebeia-Fstar

This directory contains the artifact for the paper, "Verification of a Merkle Patricia Tree library using F*". It includes the original OCaml source code for the Merkle Patricia Tree library Plebeia, together with the F* code used to verify parts of it. The Docker image has been tested to build on Ubuntu. However, because this artifact depends on an older version of the fstar opam library, the build may fail in certain environments. Specifically, it fails to build on macOS systems equipped with an M3 chip. Building and Running the Docker Image Build the image: docker build -t plebeia-fstar . Run the image: docker run -it --rm plebeia-fstar Pre-built Docker image is available at https://doi.org/10.5281/zenodo.19487932. Building and Verifying in the Docker Image Build Plebeia using the original OCaml files: Run ./build_ml.sh to build Plebeia with the original OCaml files. Build Plebeia using OCaml files extracted from F* files: Run ./build_fstar.sh to build Plebeia by replacing specific components with extracted OCaml files from F*. This script also verifies that every .fst and .fsti file is valid using the corresponding .checked files in the fstar/checked_files/ directory. If you want to regenerate the .checked files, you can execute the ./generate_checked.sh script. Testing: In both build settings, the compiled library can be tested by running dune runtest pretest and dune runtest tests. Benchmark: The benchmark described in Section 4.6 can be executed by running (cd tests/benchmark/; /usr/bin/time dune exec ./benchmark.exe million). Directory Structure ml/: Contains the original OCaml files for Plebeia. fstar/: Contains the .fst and .fsti F* files, as well as .ml OCaml files for handling gaps between extracted files and the original files. tests/ and pretest/: Contain the test code for Plebeia. These can be executed via dune runtest. msync/: Contains the OCaml wrapper for the msync system call used in Plebeia. plebeia_docs/: Contains the original documentation for Plebeia. dune_fstar and dune_ml: Dune configuration files that are copied during the build process. Proof Structure This part explains the mapping between the proof described in the "Verification of Plebeia with F*" section of the paper and the actual F* source files. All files referenced below are located in the fstar/ directory. Structural Invariants Tree (node) invariants are defined in node_type_fstar.fst, and zipper (cursor) invariants are defined in cursor_fstar.Type.fst. Zipper-manipulating functions are defined in cursor_fstar.fst, and the preservation of invariants is expressed within their types. Functional Correctness Each tree-manipulation function is proven to be faithful to its specification, which is expressed as a pure function. The specifications for the functions in cursor_fstar.fst are defined in cursor_fstar.Spec.fst. The file functionality_proof.fst proves that the specifications are homomorphic to their modelized versions (i.e., the implementation based on key–value stores defined in list_mptmodel.fst). Data-Persistence Process Functions related to the data-persistence process are defined in node_storage_load_fstar.fst and node_storage_store_fstar.fst. Their functionalities are expressed within their types. Relative Collision Resistance of the Merkle Hash of Plebeia tree The property is formalized as a reduction function from a Merkle hash collision to an attack on the underlying hash function. This function is defined in hash_collision_proof.fst.