Formal Verification - Lean4 Integration

.cspell.config.yaml

@@ -4,6 +4,7 @@ ignorePaths:
   - CMakeUserPresets.json
   - Doxyfile
   - docs/**/*.puml
+  - formal_verification/**/*.lean
   - cmake/**
   - LICENSE.md
   - .clang-tidy
@@ -129,6 +130,7 @@ words:
   - gpgcheck
   - gpgkey
   - hotwallet
+  - hrange
   - hwaddress
   - hwrap
   - ifndef
@@ -212,6 +214,7 @@ words:
   - nullptr
   - nunl
   - Nyffenegger
+  - olean
   - onlatest
   - ostr
   - pargs
@@ -299,6 +302,7 @@ words:
   - takergets
   - takerpays
   - ters
+  - Thrane
   - TMEndpointv2
   - trixie
   - tx

.gitignore

@@ -16,6 +16,7 @@ Release/
 /.venv/
 /build/
 /db/
+.lake
 /out.txt
 /Testing/
 /tmp/

BUILD.md

@@ -315,6 +315,24 @@ You can then build and test as usual, with the generated `xrpld` binary containi
 
 See [Sanitizers docs](./docs/build/sanitizers.md) for more details.
 
+## Formal verification
+
+Build with the `formal_verification` option (needs `xrpld` and `tests`), then
+run the Lean 4 cross-validation suite. `--lockfile-partial` lets Conan add the
+`lean4` toolchain, which is opt-in and not pinned in `conan.lock`:
+
+```bash
+# once per machine
+conan export ../external/lean4
+conan export ../external/lean4-deps
+
+conan install .. --output-folder . --build missing --settings build_type=Release -o formal_verification=True --lockfile-partial
+cmake -DCMAKE_TOOLCHAIN_FILE:FILEPATH=build/generators/conan_toolchain.cmake -DCMAKE_BUILD_TYPE=Release -Dxrpld=ON -Dtests=ON -Dformal_verification=ON ..
+cmake --build . --target xrpld && ./xrpld --unittest=formal_verification
+```
+
+See [formal verification docs](./docs/formal-verification/README.md) for more details.
+
 ## Options
 
 | Option           | Default Value | Description                                                                   |

cmake/XrplCore.cmake

@@ -273,10 +273,18 @@ if(xrpld)
             CONFIGURE_DEPENDS
             "${CMAKE_CURRENT_SOURCE_DIR}/src/test/*.cpp"
         )
+        # The Lean cross-validation tests need the Lean FFI symbols, which
+        # are only linked when formal_verification is enabled.
+        if(NOT formal_verification)
+            list(FILTER sources EXCLUDE REGEX "/src/test/formal_verification/")
+        endif()
         target_sources(xrpld PRIVATE ${sources})
     endif()
 
     target_link_libraries(xrpld Xrpl::boost Xrpl::opts Xrpl::libs xrpl.libxrpl)
+
+    include(XrplLean4)
+
     exclude_if_included(xrpld)
     # define a macro for tests that might need to
     # be excluded or run differently in CI environment

cmake/XrplLean4.cmake

@@ -0,0 +1,55 @@
+# Builds the Lean4 FFI library and links it into xrpld when formal_verification is on (default OFF).
+
+if(NOT formal_verification)
+    return()
+endif()
+
+if(NOT TARGET xrpld OR NOT tests)
+    message(FATAL_ERROR "formal_verification=ON requires xrpld and tests")
+endif()
+
+foreach(_var IN ITEMS LEAN4_BINDIR LEAN4_DEPS_PACKAGES LEAN4_DEPS_ARCHIVE)
+    if(NOT ${_var})
+        message(
+            FATAL_ERROR
+            "formal_verification=ON needs ${_var} from the Conan toolchain"
+        )
+    endif()
+endforeach()
+
+find_package(lean4 REQUIRED)
+
+set(lean4_src ${CMAKE_SOURCE_DIR}/formal_verification)
+set(lean4_model_archive ${lean4_src}/.lake/build/lib/libXRPL_XRPLModel.a)
+
+# Mount the dep packages (mathlib .olean files) so lake can resolve the model's imports.
+set(lean4_lake ${lean4_src}/.lake)
+file(MAKE_DIRECTORY ${lean4_lake})
+file(REMOVE_RECURSE ${lean4_lake}/packages)
+file(CREATE_LINK ${LEAN4_DEPS_PACKAGES} ${lean4_lake}/packages SYMBOLIC)
+
+# Build the model archive where DEPENDS on the model sources so edits trigger a rebuild.
+file(
+    GLOB_RECURSE lean4_model_sources
+    CONFIGURE_DEPENDS
+    ${lean4_src}/XRPL/*.lean
+)
+add_custom_command(
+    OUTPUT ${lean4_model_archive}
+    COMMAND ${LEAN4_BINDIR}/lake build XRPLModel:static
+    DEPENDS ${lean4_model_sources} ${lean4_src}/lakefile.toml
+    WORKING_DIRECTORY ${lean4_src}
+    COMMENT "formal_verification: Lean4 model build"
+    VERBATIM
+)
+add_custom_target(lean4_model DEPENDS ${lean4_model_archive})
+
+# Static link into xrpld
+add_dependencies(xrpld lean4_model)
+target_link_libraries(
+    xrpld
+    ${lean4_model_archive}
+    ${LEAN4_DEPS_ARCHIVE}
+    lean4::lean4
+)
+message(STATUS "formal_verification: Lean4 linked into xrpld")

cmake/XrplSettings.cmake

@@ -30,6 +30,12 @@ if(tests)
     endif()
 endif()
 
+option(
+    formal_verification
+    "Link the Lean 4 formal verification FFI and build its cross-validation tests (requires tests)"
+    OFF
+)
+
 # Enabled by default so every header is compiled on its own as the main file of
 # its own compile_commands.json entry - this is what lets clang-tidy (and clangd
 # and IDEs) analyse a header's own includes directly. The per-header objects are

conanfile.py

@@ -1,3 +1,4 @@
+import os
 import re
 
 from conan.tools.cmake import CMake, CMakeToolchain, cmake_layout
@@ -17,6 +18,7 @@ class Xrpl(ConanFile):
         "assertions": [True, False],
         "coverage": [True, False],
         "fPIC": [True, False],
+        "formal_verification": [True, False],
         "jemalloc": [True, False],
         "rocksdb": [True, False],
         "shared": [True, False],
@@ -48,6 +50,7 @@ class Xrpl(ConanFile):
         "assertions": False,
         "coverage": False,
         "fPIC": True,
+        "formal_verification": False,
         "jemalloc": False,
         "rocksdb": True,
         "shared": False,
@@ -128,9 +131,18 @@ def configure(self):
         if self.settings.compiler in ["clang", "gcc"]:
             self.options["boost"].without_cobalt = True
 
+    def _lean_version(self):
+        # formal_verification/lean-toolchain pins "leanprover/lean4:vX.Y.Z".
+        path = os.path.join(self.recipe_folder, "formal_verification", "lean-toolchain")
+        with open(path, encoding="utf-8") as f:
+            return f.read().strip().split(":v")[1]
+
     def requirements(self):
         self.requires("boost/1.91.0", force=True, transitive_headers=True)
         self.requires("date/3.0.4", transitive_headers=True)
+        if self.options.formal_verification:
+            self.requires(f"lean4/{self._lean_version()}", transitive_headers=True)
+            self.requires(f"lean4-deps/{self._lean_version()}")
         if self.options.jemalloc:
             self.requires("jemalloc/5.3.1")
         self.requires("lz4/1.10.0", force=True)
@@ -164,6 +176,13 @@ def generate(self):
         tc.variables["tests"] = self.options.tests
         tc.variables["assert"] = self.options.assertions
         tc.variables["coverage"] = self.options.coverage
+        tc.variables["formal_verification"] = self.options.formal_verification
+        if self.options.formal_verification:
+            lean4 = self.dependencies["lean4"].cpp_info
+            lean4_deps = self.dependencies["lean4-deps"].cpp_info
+            tc.variables["LEAN4_BINDIR"] = lean4.bindirs[0]
+            tc.variables["LEAN4_DEPS_PACKAGES"] = lean4_deps.get_property("packages")
+            tc.variables["LEAN4_DEPS_ARCHIVE"] = lean4_deps.get_property("archive")
         tc.variables["jemalloc"] = self.options.jemalloc
         tc.variables["rocksdb"] = self.options.rocksdb
         tc.variables["BUILD_SHARED_LIBS"] = self.options.shared