Formal Verification - Lean4 Integration

[ivan-randjelovic-cp]

This pull request showcases Lean 4 formal verification framework. In it we demonstrate what formal verification of a small part of xrpld looks like: less-than Number operator.

Of course, alongside this one function we had to bring in the entire build process and scaffolding to have FFI unit tests (tests verifying that Lean 4 implementation is faithful to C++).

Our goals with this integration is to provide formal verification without a huge overhead for C++ software engineers. The FFI unit tests will only cover crucial aspects of the formally verified codebase that should not change often.

Here is our recommendation on how to navigate this pull request:

• docs/formal-verification/README.md is a good starting point in which we explain the motivation and technical details of implementing Lean 4 into xrpld

If you are a person of action rather than a reader of markdowns, you may want to look into the files directly:

• external/lean4-deps and external/lean4 introduce Conan recipes to install Lean 4 dependencies. These are entirely optional and can be enabled with with the build option -o formal_verification=True on conan install.
• cmake/ made changes to XrplCore.cmake, XrplSettings.cmake, and introduced XrplLean4.cmake let you build Lean 4 models and FFI unit tests with cmake option -Dformal_verification=ON (which requires -Dxrpld=ON -Dtests=ON).
• formal_verification/XRPL/Model is how the code is modeled in Lean 4.
• formal_verification/XRPL/FFI contains functions that expose Lean 4 to C++.
• formal_verification/XRPL/Properties contains theorems and proofs.

The one proof you should start with is in: formal_verification/XRPL/Compare.lean. This theorem depends on some other theorems and lemmas, which will be encapsulated in Common directories. Because this PR represents a part of a bigger picture, we left those helper theorems separated - but in reality they are reused by other theorems.

Finally, we direct you to look at:

• docs/formal_verification/lean4.md

This document is a crash-course in Lean 4 and might make it easier for you to read Lean 4 code. Fair warning: it might also get you to stay up at night reading about type theory and studying proofs and tactics!

[github-actions]

This PR has conflicts, please resolve them in order for the PR to be reviewed.