Graphiti Artefact ASPLOS 2026

Graphiti: Formally Verified Out-of-Order Execution in Dataflow Circuits A Artifact Appendix A.1 Abstract The main contribution of the paper is a verified rewriting algorithm based on an abstract graph semantics, and an implementation of the out-of-order optimisation, together with a verified loop rewrite. This artefact will therefore mainly be describing and documenting the Graphiti artefact, and show that the rewriting algorithm, as well as the loop rewrite, have been fully verified without admitting any additional axioms in the Lean 4 theorem prover. Additionally, in the evaluation section we also show performance results of the dataflow graphs that we generate compared to Vericert (an existing verified HLS tool), Dynamatic with the in-order loop and Dynamatic with the out-oforder loop transformation. Unfortunately, this evaluation is currently performed quite manually and is therefore more difficult reproduce, although we believe that this is not the primary claim of the paper compared to the completed proof. A.2 Artifact check-list (meta-information) •Compilation: Lean v4.26.0-rc2 and rustc >=1.86.0 • Run-time environment: VirtualBox VM for experiments • How much disk space required (approximately)?: 100GB for VM and experiments • How much time is needed to prepare workflow (approximately)?: 20 mins • How much time is needed to complete experiments (approximately)?: 30 mins • Publicly available?: https://github.com/VCA-EPFL/graphiti/ tree/asplos VM and docker: https://zenodo.org/records/17942754 •Code licenses (if publicly available)?: Apache-2.0 •Archived (provide DOI)?: 10.5281/zenodo.17942754 A.3 Description A.3.1 How to access. The code for the Graphiti rewriting framework, as well as the loop rewrite proof can be found on GitHub: https://github.com/VCA-EPFL/graphiti/tree/asplos A build of graphiti is also available in a Docker image. We have also provided a VM image to reproduce the runtime results. Both are available at the following location: https://zenodo.org/records/17942754. A.3.2 Software dependencies. These software dependencies assume an installation of Linux. If the Docker image is being used, then everything will already have been built in the /graphiti folder, so appendix A.3.2 and appendix A.4 can be skipped. For the VM, appendix A.3.3 is needed. To compile and run the Graphiti framework, one needs to install Lean 4 using elan and rustc using cargo . To do so, follow the instructions at https://lean-lang.org/install/ manual/. Once that is finished, executing which lake should return $HOME/.elan/bin/lake. Similarly, install rustc by following the instructions at https://rust-lang.org/tools/install/. Once that is done, make sure that $HOME/.cargo/bin is in the path: export PATH $HOME/.cargo/bin:$PATH Executing which cargo should return $HOME/.cargo/bin/cargo . A.3.3 Software dependencies for the reproducing the evaluation results in the VM. Dynamatic requires a version of Gurobi 13.0 to be installed and available in the path. We cannot distribute this software together with the VM, so this software also has to be installed in the VM. Gurobi provide a free academic license which can be used to perform the experiments. To install it, follow the instructions: https:// www.gurobi.com/academia/academic-program-and-licenses/. After installing Gurobi in the VM and installing the Gurobi license in the $HOME directory of the VM, the following file needs to be changed to and sourced to be able to run Gurobi: • line 2 of /home/dynamatic/Dynamatic/etc/dynamatic/ Regression_test/init_gurobi.sh needs to be updated to reflect the installation directory of Gurobi. To check whether gurobi is installed: source $HOME/Dynamatic/etc/dynamatic/Regression_test/init_gurobi.sh gurobi_cl $GUROBI_HOME/examples/data/afiro.mps should output something ending in: Optimal objective -4.647531429e+02 A.4 Installation First clone the Graphiti repository and checkout the asplos branch: git clone -b asplos https://github.com/VCA-EPFL/graphiti Next, enter the directory, and run: make setup bin/graphiti_oracle This will setup and install the right version of Lean, as well as compile and install the oracle used to guide the rewrites associated with the pure generation, which is implemented in Rust. Finally, running the following two commands will compile the project and ensure that everything on the Lean side is setup correctly. lake build graphiti lake test If the following is printed (in a single line) then everything is setup correctly and is ready to be evaluated. info: GraphitiTest/Core/AppliedLoopRewrite.lean:80:0: 'Graphiti.run'_refines_applied' depends on axioms: [propext, Classical.choice, Quot.sound] Access through Docker: To install the docker image, run: docker load --input docker-graphiti.tar.gz To run a container, run the following command: docker run -it --rm --workdir=/graphiti --entrypoint=/bin/bash 65e21363ff2f 13 Yann Herklotz, Ayatallah Elakhras, Martina Camaioni, Paolo Ienne, Lana Josipović, and Thomas Bourgeat A.5 Evaluation and expected results A.5.1 Evaluating the Lean 4 artefact. This section will provide a description and mapping from the paper to the Lean 4 artefact so that the theorems that were verified in Lean 4 can be checked to be consistent with what is described in the paper. This is the main part of the artefact evaluation. We will start with the main directory layout. •Graphiti : Contains the main Graphiti library code and all the proofs. •Main.lean : Contains the top-level application code which reads and writes dot-files. •benchmarks/post-processed : Contains dot-files that were manually processed after coming from Dynamatic so that they are ready to be rewritten. •benchmarks/transformed : Benchmark output once the loop rewrite was applied. Next, we discuss the location of the formalisation: •ExprHigh: Graphiti/Core/ExprHigh.lean line 22. •ExprLow: Graphiti/Core/ExprLow.lean line 33. • Component specifications: Graphiti/Core/Component.lean: contains all the implementations of the components shown in table 1. • Rewrite in figure 3a:Graphiti/Core/Rewrites/CombineMux. lean line 50: this file shows the matcher , which is an algorithm that can find the LHS of the graph in a larger graph. It then shows the lhs , which is the graph corresponding to the LHS of the rewrite, and rhs , which shows the RHS of the rewrite. • Rewrite in figure 3b:Graphiti/Core/Rewrites/JoinSplitElim. lean line 39. • Rewrite in figure 3c:Graphiti/Core/Rewrites/JoinSplitLoopCond. lean line 40. • Rewrite in figure 3d:Graphiti/Core/Rewrites/LoopRewrite. lean line 119. • The rewriter in section 4.2:Graphiti/Core/ExprLow.lean line 199. • The more sophisticate rewriter mentioned in section 4.2: Graphiti/Core/Rewriter.lean line 234. • The fork component from section 4.3:Graphiti/Core/Component. lean line 116. • M:Graphiti/Core/Module.lean line 55. • Refinement with simulation relation 𝜑 :Graphiti/Core/ModuleLemmas. lean line 938. •Refinement: Graphiti/Core/ModuleLemmas.lean line 1088. • ·[· ·]:Graphiti/Core/Module.lean line 143. • · ] ·:Graphiti/Core/Module.lean line 156. •Environment: Graphiti/Core/Environment.lean line 55. • Replacement refines on ExprLow: Graphiti/Core/ExprLowLemmas. lean line 1627. • Replacement refines on ExprHigh: Graphiti/Core/RewriterLemmas. lean line 356. • lemma 5.1:Graphiti/Core/Rewrites/LoopImplementationProof. lean line 255. • lemma 5.2:Graphiti/Core/Rewrites/LoopImplementationProof. lean line 1324. • theorem 5.3:Graphiti/Core/Rewrites/LoopImplementationProof. lean line 1641. Finally, we show that we can apply the verified loop rewrite to the verified rewrite algorithm and get a combined correctness theorem of applying the loop rewrite in a larger graph: GraphitiTest/Core/AppliedLoopRewrite.lean line 65 We then print all the axioms on line 80 and show that the only axioms are: [propext, Classical.choice, Quot.sound] Which are standard axioms of Lean 4. A.5.2 Running the rewriter on some graphs. To run Graphiti on some input graphs and observe the transformation: lake exe graphiti \ benchmarks/post-processed/matvec.dot \ # benchmark to run --oracle $(pwd)/bin/graphiti_oracle \ # path to oracle --reverse \ # undo pure generation -o out.dot # path to output file The input and output file can then be compared. The output file out.dot should contain a node with type : TaggerUntagger . For example, shown in the file: benchmarks/post-processed/ matvec.dot on line 62. Any other file in the benchmarks/post-processed folder can be passed to Graphiti to observe its output. Some additional useful options that can be passed to Graphiti: •-l out.json : provides a detailed log of which rewrites were applied where. •--no-dynamatic-dot : provides a nicer dot graph for visualization purposes with Graphviz. •--parse-only : parses the file without performing any rewrites, can be useful to visualize the input graphs in a nicer way with Graphviz. For example, to view the dot graph in a visual way with Graphviz: dot -Tpng out.dot -o out.png A.5.3 Evaluating the performance results. This section assumes that you are in the VM that was shared in the Zenodo link. VM username and password: •username: dynamatic •password: dynamatic In this artefact we are unfortunately not providing full scripts and instructions to perform the complete evaluation. We are instead providing the raw results which were used to plot the graph in figure 8, as well as instructions to retrieve the cycle count using simulation for the various tools. Note: there might be slight discrepancies in the cycle counts due to improvements we made to the timing analysis of components in Dynamatic. These were manually added to the Dynamatic graphs after they were generated, and are therefore not present when evaluating the Dynamatic tools end-toend without intervening. Finally, we have also not included an environment to simulate the Vericert results, however, 14 Graphiti: Formally Verified Out-of-Order Execution in Dataflow Circuits the benchmarks that were run, together with the branch in Vericert that implements floating point operations is available to view at, with instructions to run the simulations and synthesise the hardware: https://github.com/ymherklotz/ vericert/tree/dev/floating-point/benchmarks/dynamatic. For the Vericert results, Vivado 2019.2 is required for both the simulation and synthesis results. For Dynamatic, Vivado 2019.2 is only required for the synthesis results. First, make sure you have a terminal open and have followed the instructions to install Gurobi. Next, make sure that Gurobi is available in the path: source $HOME/Dynamatic/etc/dynamatic/Regression_test/init_gurobi.sh gurobi_cl $GUROBI_HOME/examples/data/afiro.mps Next, follow the directory to the regression tests: cd $HOME/Dynamatic/etc/dynamatic/Regression_test To run a specific benchmark with a specific tool, you can use the three scripts ( run_df_io.sh , run_df_ooo.sh , run_graphiti.sh ) with one of the benchmarks ( gemm, gsum_many, gsum_single, img_avg, matvec, mvt) in the directory: ./run_df_ooo.sh matvec This will produce the output files in: df_ooo/matvec/sim/ VHDL_OUT. To check the cycle count of that particular run: tail -n7 df_ooo/matvec/sim/VHDL_OUT/transcript Towards the top of the file there should be: # Time: 3738 ns Iteration: 1 The period is assumed to be 4ns, and there is a reset delay of 30ns, which means to calculate the exact cycle count one has to do: (3738-30) / 4 = 927 These results can then be compared against the CSV file located in the Graphiti GitHub repository under: https://github. com/VCA-EPFL/graphiti/blob/asplos/benchmarks/raw_results. csv. Note that running this benchmark with Graphiti ( ./run_graphiti.sh ), will take a pregenerated dot graph that was generated by Graphiti and slightly tweaked to make it compile through the existing Dynamatic back end. Synthesis for area and delay results. To reproduce the results for delay, area and execution time, Vivado 2019.2 is required. Unfortunately, this cannot be distributed with the VM, and so will have to be set-up manually. Assuming that vivado is in the path, the following instructions can be used to reproduce the results. After having run the relevant run_df_io.sh command for the benchmark that should be synthesised, one can then copy the benchmark folder (for example df_io/matvec ) to a machine where Vivado 2019.2 is installed. Then, from within that copied folder, one can execute: cd synth vivado -mode batch -source synthesize_4.tcl This should produce a few report files. These can be summarised running a script in the same directory as the one vivado was executed in. This script is located at: /home/ dynamatic/Dynamatic/etc/dynamatic/Regression_test/scripts/ report.sh It will generate a file called synth_p_r_summary.rpt with all the information that was reported in the benchmarks/ raw_results.csv file. Reproducing the figure. To reproduce the figure, you need to have gnuplot installed. Then, from the base of the graphiti repository: cd benchmarks gnuplot -e "set terminal jpeg; set output 'results_graph.jpg'" results_graph.gp This should produce the following image: https://github. com/VCA-EPFL/graphiti/blob/asplos/benchmarks/results_graph. jpg. 15