Towards Formally Verified Smart Contracts Compilation (FM'26 Artifact)

Abstract. This artifact includes a verification tool to automatically prove the correctness of the results of the liveness analysis stage of the official Solidity compiler solc. It contains scripts to automatically reproduce the experiments presented in Section 5 of the paper (Experimental Evaluation), which includes the solc's liveness results—obtained from more than 1,500 smart contracts--that our tool can automatically verify in negligible time. The verification tool has two main components defined and verified using the Rocq system. The first one is a formalization of a small-step semantics for YUL-IR programs in Control Flow Graph and Single Static Assignment form (YUL-IR CFG-SSA). These YUL-IR CFG-SSA programs are produced directly by the smart contract compiler, in our case the solc Solidity compiler. The second component is a liveness checker that accepts a YUL-IR CFG-SSA program and determines if the liveness information produced by the solc compiler is correct wrt. the small-step semantics. This checker is verified in Rocq. Since the compiled YUL-IR CFG-SSA program is produced by the solc compiler as a JSON file and the Rocq components work on Rocq datatypes, we have developed in Python a syntactical translator JSON --> Rocq to connect these stages. Requirements for Using the Artifact Docker. AMD64 architecture. Contents of the Artifact License.txt: GPL-3.0. Readme.md: Step-by-step instructions on how to use the artifact. foryu_amd64.tar: Docker image foryu:amd64 of a container of Ubuntu 24.04 with all the dependencies installed: 1. Rocq 8.20.1 (released Jan 2025) with the first package pick from Jan 2025. 2. Python 3.12.3. 3. A clone of the FORYU verification framework repository (https://github.com/costa-group/foryu). fm26.log: log showing the results obtained by the artifact for the experiments used in the paper (1,550 smart contracts from the semantic test suite of the official solc compiler). How to Reproduce the Experiments 1. Load the foryu_amd64.tar file as a Docker image: $ docker load -i foryu_amd64.tar 2. Execute the Bash interpreter inside the foryu:amd64 Docker image: $ docker run --rm -it foryu:amd64 /bin/bash 3. Once inside the Docker image, go to the `/root/foryu` directory: # cd /root/foryu 4. Smoke test: Launch the script fm26_subset.sh to verify the liveness information of a subset of 5 smart contracts from the test suite. It requires around 30 seconds on an Intel i7-4790 CPU at 3.60 GHz with 16 GB of RAM. # ./fm26_subset.sh filename,nblocks,ninstrs,time_translation(ns),time_compilation(ns),time_checker(ns),verdict benchmark/fm26/constructor_payable_constructor__payable_constructor_standard_input_cfg.json,2,7,35420898,3696453919,1747725,LIVENESS_VALID benchmark/fm26/isoltestTesting_balance_with_balance__balance_with_balance_standard_input_cfg.json,2,7,34352379,4781551781,1686683,LIVENESS_VALID benchmark/fm26/viaYul_smoke_test__smoke_test_standard_input_cfg.json,4,9,35221536,3660930186,1682949,LIVENESS_VALID benchmark/fm26/constants_constant_variables__constant_variables_standard_input_cfg.json,4,9,46328732,4074733955,1882506,LIVENESS_VALID benchmark/fm26/receive_ether_and_data__ether_and_data_standard_input_cfg.json,6,12,34628054,3847882263,1964217,LIVENESS_VALID 5. Complete experiments from Section 5 of the paper: To execute the full test suite, launch the script fm26.sh to verify the liveness information of all the smart contracts. It requires between 4 and 5 hours on an Intel i7-4790 CPU at 3.60 GHz with 16 GB of RAM. The complete output can be found in the file fm26.log included in the artifact. # ./fm26.sh filename,nblocks,ninstrs,time_translation(ns),time_compilation(ns),time_checker(ns),verdict benchmark/fm26/exponentiation_signed_base__signed_base_standard_input_cfg.json,36,117,38301703,5653300233,2135167,LIVENESS_VALID benchmark/fm26/types_nested_tuples__nested_tuples_standard_input_cfg.json,36,72,43061425,5637260411,2056568,LIVENESS_VALID benchmark/fm26/constants_function_unreferenced__function_unreferenced_standard_input_cfg.json,30,59,38180468,5491688881,2600047,LIVENESS_VALID benchmark/fm26/virtualFunctions_virtual_override_changing_mutability_public__virtual_override_changing_mutability_public_standard_input_cfg.json,36,62,37641855,10214420320,2405639,LIVENESS_VALID benchmark/fm26/array_dynamic_arrays_in_storage__dynamic_arrays_in_storage_standard_input_cfg.json,70,191,40278222,11653605509,2568446,LIVENESS_VALID benchmark/fm26/array_dynamic_arrays_in_storage__dynamic_arrays_in_storage_standard_input_cfg.json,70,191,40278222,11653605509,2568446,LIVENESS_VALID benchmark/fm26/freeFunctions_new_operator__new_operator_standard_input_cfg.json,50,140,38138844,6742961202,2100051,LIVENESS_VALID benchmark/fm26/state_block_basefee__block_basefee_standard_input_cfg.json,15,31,38638268,4537592343,2213384,LIVENESS_VALID benchmark/fm26/viaYul_loops_simple__simple_standard_input_cfg.json,66,126,37345157,6147589440,2767875,LIVENESS_VALID ...