From 985b0ced52edafbb7bf98a7306d5fe9af0464555 Mon Sep 17 00:00:00 2001 From: Ivan Randjelovic Date: Wed, 1 Jul 2026 14:57:55 +0200 Subject: [PATCH 1/9] Formal Verification - Number.operator_lt and build config Signed-off-by: Ivan Randjelovic --- .gitignore | 1 + BUILD.md | 18 + cmake/XrplCore.cmake | 8 + cmake/XrplLean4.cmake | 55 +++ cmake/XrplSettings.cmake | 6 + conanfile.py | 19 + cspell.config.yaml | 2 + docs/formal-verification/README.md | 396 ++++++++++++++++++ external/lean4-deps/conanfile.py | 128 ++++++ external/lean4/conanfile.py | 71 ++++ formal_verification/README.md | 34 ++ formal_verification/XRPL.lean | 3 + formal_verification/XRPL/FFI/CommonFFI.lean | 11 + formal_verification/XRPL/FFI/FFI.lean | 1 + .../XRPL/FFI/Protocol/NumberFFI.lean | 14 + formal_verification/XRPL/Model/Model.lean | 1 + .../XRPL/Model/Protocol/Number.lean | 60 +++ .../XRPL/Properties/Properties.lean | 1 + .../Protocol/Number/Common/Constants.lean | 14 + .../Protocol/Number/Common/ToRatLemmas.lean | 106 +++++ .../Number/Compare/Common/Proofs.lean | 226 ++++++++++ .../Protocol/Number/Compare/Compare.lean | 11 + .../Protocol/Number/Signum/Common/Proofs.lean | 16 + formal_verification/lake-manifest.json | 176 ++++++++ formal_verification/lakefile.toml | 27 ++ formal_verification/lean-toolchain | 1 + .../formal_verification/common/LeanSuite.h | 96 +++++ .../numbers/LeanNumber_test.cpp | 199 +++++++++ .../numbers/helpers/NumberGenerators.h | 43 ++ .../numbers/helpers/NumberTypes.h | 15 + 30 files changed, 1759 insertions(+) create mode 100644 cmake/XrplLean4.cmake create mode 100644 docs/formal-verification/README.md create mode 100644 external/lean4-deps/conanfile.py create mode 100644 external/lean4/conanfile.py create mode 100644 formal_verification/README.md create mode 100644 formal_verification/XRPL.lean create mode 100644 formal_verification/XRPL/FFI/CommonFFI.lean create mode 100644 formal_verification/XRPL/FFI/FFI.lean create mode 100644 formal_verification/XRPL/FFI/Protocol/NumberFFI.lean create mode 100644 formal_verification/XRPL/Model/Model.lean create mode 100644 formal_verification/XRPL/Model/Protocol/Number.lean create mode 100644 formal_verification/XRPL/Properties/Properties.lean create mode 100644 formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean create mode 100644 formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean create mode 100644 formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean create mode 100644 formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean create mode 100644 formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean create mode 100644 formal_verification/lake-manifest.json create mode 100644 formal_verification/lakefile.toml create mode 100644 formal_verification/lean-toolchain create mode 100644 src/test/formal_verification/common/LeanSuite.h create mode 100644 src/test/formal_verification/numbers/LeanNumber_test.cpp create mode 100644 src/test/formal_verification/numbers/helpers/NumberGenerators.h create mode 100644 src/test/formal_verification/numbers/helpers/NumberTypes.h diff --git a/.gitignore b/.gitignore index 6bd34ece04c..c8d9b7a61f8 100644 --- a/.gitignore +++ b/.gitignore @@ -16,6 +16,7 @@ Release/ /.venv/ /build/ /db/ +.lake /out.txt /Testing/ /tmp/ diff --git a/BUILD.md b/BUILD.md index 847cd7bc1a0..b868a003519 100644 --- a/BUILD.md +++ b/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 | diff --git a/cmake/XrplCore.cmake b/cmake/XrplCore.cmake index 4d4a800d9a0..294567f670b 100644 --- a/cmake/XrplCore.cmake +++ b/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 diff --git a/cmake/XrplLean4.cmake b/cmake/XrplLean4.cmake new file mode 100644 index 00000000000..8c470f13c0f --- /dev/null +++ b/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") diff --git a/cmake/XrplSettings.cmake b/cmake/XrplSettings.cmake index 44a727a9940..bea8717f752 100644 --- a/cmake/XrplSettings.cmake +++ b/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 +) + option(unity "Creates a build using UNITY support in cmake." OFF) if(unity) if(NOT is_ci) diff --git a/conanfile.py b/conanfile.py index db12dcb5853..191a3191319 100644 --- a/conanfile.py +++ b/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 diff --git a/cspell.config.yaml b/cspell.config.yaml index c120c31855b..c82c67e3993 100644 --- a/cspell.config.yaml +++ b/cspell.config.yaml @@ -4,6 +4,7 @@ ignorePaths: - CMakeUserPresets.json - Doxyfile - docs/**/*.puml + - formal_verification/**/*.lean - cmake/** - LICENSE.md - .clang-tidy @@ -214,6 +215,7 @@ words: - nullptr - nunl - Nyffenegger + - olean - onlatest - ostr - pargs diff --git a/docs/formal-verification/README.md b/docs/formal-verification/README.md new file mode 100644 index 00000000000..77d44117d4e --- /dev/null +++ b/docs/formal-verification/README.md @@ -0,0 +1,396 @@ +# Formal Verification of XRPL in Lean4 + +This doc covers the Lean4 to C++ integration in `xrpld`: how a Lean4 model is +compiled and wired in so the C++ can call it. + +## Motivation + +`xrpld` contains arithmetic and protocol logic that is easy to get subtly +wrong: invariants that must hold after a number of transactions have run, +edge-case branching or rounding. Formal verification lets us examine and +prove properties that hold for **all** inputs. We do it in two steps: + +1. **Model the C++ in Lean4.** We re-implement a C++ algorithm as a Lean4 + function, a faithful line-by-line translation, then **prove properties about + it** (e.g. "the rounded result is within half a unit in the last place of the + exact result"). + +2. **Cross-validate the model against the real C++.** A proof only matters if the + model matches the shipping C++, so we run exhaustive tests that compare the two. + +The proofs tell us the modeled algorithm is correct. The cross-validation tells +us the model faithfully represents the C++. + +## Terminology + +| Term | Meaning | +| ---------------------- | ------------------------------------------------------------------------------------------ | +| **Lean4** | Functional programming language and interactive theorem prover, which can generate C code. | +| **Model** | A Lean4 function or structure that re-implements C++ logic | +| **Property / theorem** | A mathematical statement about the model, proved in Lean4 | +| **FFI** | Foreign Function Interface, bridging Lean4 and C++ | +| **`elan`** | Lean4 version manager, installs `lake` | +| **`lake`** | Lean4's build tool (the equivalent of `cmake`) | +| **`mathlib`** | Lean4's mathematics library. Large and slow to compile | + +## Overview + +- Lean4 models are in `formal_verification/XRPL/Model` under the root directory. +- C++ has unit tests in `src/test/formal_verification/` that compare Lean4 vs C++ implementation. +- For these test to work, Lean4 needs to expose its functions to C++. +- Lean4 is capable of compiling to C via FFI exports, which can then be called from C++. These exports are defined in `formal_verification/XRPL/FFI`. +- C++ side also needs FFI wrappers to abstract any complexities or memory management away from C++ developers. + +```mermaid +flowchart TD + subgraph Lean["Lean4"] + Model["Model"] + Props["Properties"] + FFI["FFI exports"] + Model --> Props + Model --> FFI + end + FFI -->|compiled to C| Lib["libXRPL_XRPLModel"] + subgraph Cpp["C++"] + Real["C++ code"] + CFFI["FFI wrappers"] + Test["Cross-validation tests"] + end + Lib --> Test + Real --> Test + CFFI --> Test +``` + +There are two use-cases of Lean4 models: + +1. Developing theorems and proofs about the model. +2. Writing unit tests to cross-verify Lean4 <-> C++ model faithfulness. + +As part of day-to-day development cycle, it is important that: + +1. Theorems always compile in Lean4 (in Lean4, "it compiles" means "its verified"). For regular workflow of most developers, this can be left to CI/CD. +2. Cross-verification unit tests always pass (it means Lean4 models have not drifted from C++). This affects developers working on formally verified code or formal verification itself. + +Integration is done as following: + +```mermaid +flowchart LR + A["Conan
Install Lean4 toolchain"] --> B["CMake
Build Lean4 model"] --> C["CMake
Build unit tests"] --> D["Run
unit tests"] + A --> E["Lean4
Build theorems"] +``` + +| Step | Motivation | Notes | +| -------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | +| Conan's recipe downloads `elan` and installs `lake` and dependencies | No C++ developer has to worry about installing the toolchain for Lean4 themselves, but the build process takes care of things automatically. | This should be optional - some C++ developers do not care about formal verification and will offload it to CI/CD. | +| CMake builds Lean4 models and cross-verification tests | If Lean4 or C++ code change, a single build command rebuilds them. | | +| Run tests | Make it easy to run cross-verification tests. | | +| Build theorems | Formal verification proof work can be done independently. | User can use `lake` installed by Conan, but they need to add it to `PATH`. Alternatively, install your own, but make sure version is correct. | + +--- + +## Project structure + +``` +formal_verification/ Lean4 project +├── XRPL/ +│ ├── Model/ Lean4 models +│ ├── FFI/ FFI exports +│ └── Properties/ Theorems about the model +├── lakefile.toml lake build config +└── lean-toolchain pins the Lean4 version + +external/lean4/conanfile.py Conan recipe +external/lean4-deps/conanfile.py Conan recipe (prebuilt mathlib) + +src/test/formal_verification/ C++ cross-validation tests +├── common/ Common code for testing +├── ffi/ FFI code on C++ side (decoding, encoding) +└── protocol/ Tests matching C++ directory structure + +cmake/XrplLean4.cmake Links the Lean4 libraries into xrpld +``` + +--- + +## The Lean4 model: translating C++ into code suitable for theorems and proofs + +A model is a translation of the C++ code. For example, Number class data structure will look like: + +```lean +inductive rounding_mode where + | to_nearest | towards_zero | downward | upward + ... + +structure Number where + negative_ : Bool + mantissa_ : UInt64 + exponent_ : Int + ... + +def Number.operator_mul (x y : Number) (mode : rounding_mode) : Except String Number := do + -- Attempt to follow C++ business logic step by step + ... +``` + +A thing to notice: + +- The result type is `Except String Number`. The C++ throws + `std::overflow_error` on overflow; the Lean4 model returns an error string. + +### What we prove + +Once the algorithm is in Lean4, we prove properties about it. There are +**theorems and lemmas** under `XRPL/Properties/`. They range from small +accessor facts to the headline theorems. + +`lake build` _is_ the check that all theorems hold. If every file compiles +with no `sorry` and only standard axioms, the proofs are sound. + +## The FFI bridge + +Lean4 compiles to C, so each `@[export]` function is a C symbol that C++ can call. + +Lean4 values live as heap-allocated `lean_object*` pointers in the C ABI, and C++ works with them through those handles. + +Before any export can be called, the Lean4 runtime and the module's initializers +must run. The base suite does this exactly once, behind a `std::once_flag`, and +serializes all Lean4 calls behind a mutex because the Lean4 runtime is +single-threaded. This is handled in `src/test/formal_verification/common/LeanSuite.h` + +Note that we only compile and initialize the model, so that the tests are buildable and runnable even while the proofs are a work in progress. + +### Memory management is hidden in a base class + +Our goal is that a test developer has least possible interaction with Lean4 +memory management. It lives in base class `LeanObjectFFI`. + +```cpp +class LeanObjectFFI +{ + lean_object* o_ = nullptr; + +public: + lean_object* raw() const noexcept { return o_; } // inspect, no refcount change + lean_object* borrow() const noexcept { lean_inc(o_); return o_; } // pass to a Lean4 call (it consumes a ref) + lean_object* give() noexcept { auto t = o_; o_ = nullptr; return t; } // transfer ownership out + + ~LeanObjectFFI() { if (o_) lean_dec(o_); } // freed automatically +}; +``` + +The rule is encoded in the names: every Lean4 `@[export]` function _consumes_ its +object arguments, so a caller passes `borrow()` to keep its handle or `give()` to +surrender it, and never calls `lean_inc` / `lean_dec` itself. A typed wrapper +builds on this so a test sees only ordinary C++ values, which is what +`NumberFFI::build` / `read` above do. + +An operation's result structure isn't kept as a handle. A RAII guard `LeanObjOwner` frees it when the fields have been copied out: + +```cpp +struct LeanNumberResult : LeanNumber +{ + bool ok; + static LeanNumberResult fromLean(lean_object* obj) + { + LeanObjOwner const guard{obj}; // lean_dec(obj) on scope exit + LeanNumberResult r; + r.mantissa = lean_ctor_get_uint64(obj, 0); + r.exponent = lean_ctor_get_uint64(obj, 8); + r.negative = lean_ctor_get_uint8(obj, 17); + r.ok = lean_ctor_get_uint8(obj, 16) == 0; + return r; + } +}; +``` + +### Number example + +#### Building and reading a value + +For example, `lean_number_build` constructs a `Number` from its fields and +hands back the handle and `lean_number_mantissa` / `_negative` / `_exponent` +read it back out. + +```lean +@[export lean_number_build] +def lean_number_build (negative : UInt8) (mantissa : UInt64) (exponent : Int64) : Number := + Number.unchecked (negative != 0) mantissa exponent.toInt + +@[export lean_number_mantissa] +def lean_number_mantissa (n : Number) : UInt64 := n.mantissa_ +``` + +On the C++ side, `NumberFFI` wraps the handle and exposes it as a plain `Number`: + +```cpp +class NumberFFI : public LeanObjectFFI +{ +public: + using CppType = Number; + static NumberFFI build(Number const& n); // C++ Number -> Lean4 + Number read() const; // Lean4 -> C++ Number +}; +``` + +#### Running a function + +A function export takes the operands' fields, calls the matching model function, and returns the result as a Lean4 structure. + +For example, `lean_number_mul` decodes its arguments into `Number` values, calls `Number.operator_mul`, and encodes the outcome: + +```lean +structure FFINumberResult where + mantissa : UInt64 + exponent : Int64 + status : UInt8 -- 0 = ok, 1 = error + negative : UInt8 + +def decodeNumber (neg : UInt8) (mant : UInt64) (exp : Int64) : Number := + Number.unchecked (neg != 0) mant exp.toInt + +def encodeResult (r : Except String Number) : FFINumberResult := + match r with + | .ok n => encodeNumber n + | .error _ => ⟨0, 0, 1, 0⟩ + +@[export lean_number_mul] +def lean_number_mul (neg1 : UInt8) (mant1 : UInt64) (exp1 : Int64) + (neg2 : UInt8) (mant2 : UInt64) (exp2 : Int64) (mode : UInt8) : FFINumberResult := + encodeResult (Number.operator_mul (decodeNumber neg1 mant1 exp1) + (decodeNumber neg2 mant2 exp2) + (decodeMode mode)) +``` + +The returned structure is a `lean_object*`. + +--- + +## The build process + +The Lean4 side is heavy: it depends on `mathlib`, which contains thousands of files that are slow to compile. The strategy is to compile it **once** and keep it warm. + +Our model is built **in-tree** by CMake when `formal_verification=ON`, while +mathlib's native objects come prebuilt from the `lean4-deps` Conan package. +`conan install` pulls the toolchain, `lean4-deps`, and `xrpld`'s own dependencies, +and after that, editing a `.lean` file and running `cmake --build` rebuilds only +what changed. + +### Compile mathlib once, keep edits incremental + +`lake exe cache get` downloads mathlib's _elaboration_ artifacts (`.olean`), so the objects are compiled locally. + +On first build, `lean4-deps` compiles mathlib's modules and caches them for reuse later. + +Two properties keep compilation after edit fast: + +- **lake is incremental** so editing the model rebuilds only the changed model + modules; mathlib is never rebuilt. +- **the dependency objects are prebuilt** so a model edit just rebuilds the + model and relinks the library. + +We link the objects into a **shared** library, passing the ~8,000 object paths in a file +instead of on the command line. + +8,000 paths on one command line overflow the OS limit (`ARG_MAX`), which is why both `ar` and lake's own `:shared` facet fails on mathlib, so CMake links them itself. + +The Lean4 build writes its artifacts into `formal_verification/.lake/` (gitignored). +Building `xrpld` needs no separate Lean4 toolchain installed, Conan provides it. + +### Wiring into xrpld + +`formal_verification` is a Conan option (declared in `conanfile.py`) mirrored into a CMake option of the same name (declared in `cmake/XrplSettings.cmake`). Default is **OFF**, so a normal `xrpld` build is unaffected. + +When the option is on, a single `cmake --build .` builds the Lean4 library first, +then links `xrpld` against it. + +> Currently, Windows support is under development. + +--- + +## Building and running the tests + +From a fresh checkout: + +```bash +mkdir .build && cd .build + +# Register the lean4 toolchain and dependencies recipes in the Conan cache (once per machine). +conan export ../external/lean4 +conan export ../external/lean4-deps + +# Resolve and build dependencies. Runs once and pulls the lean4 toolchain and lean4-deps. +conan install .. --output-folder . --build missing --settings build_type=Release \ + -o formal_verification=True --lockfile-partial + +# Configure, then build. CMake builds the Lean4 model and links the shared +# library. lake keeps later builds incremental. +cmake -DCMAKE_TOOLCHAIN_FILE:FILEPATH=build/generators/conan_toolchain.cmake \ + -DCMAKE_BUILD_TYPE=Release -Dxrpld=ON -Dtests=ON -Dformal_verification=ON .. +cmake --build . --parallel N + +# Run the cross-validation suite. +./xrpld --unittest=formal_verification +``` + +`-o formal_verification=True` pulls the `lean4` toolchain and `lean4-deps` +into the graph, and the matching `-Dformal_verification=ON` tells CMake to build +and link the Lean4 side. + +`--lockfile-partial` lets Conan add `lean4` and `lean4-deps`, which are opt-in and not pinned in `conan.lock`. + +## Testing Principles + +### Number + +`LeanNumber_test.cpp` cross-validates every `Number` operation against the Lean +model. Each case runs the operation in both implementations and asserts they +agree (`checkResult`). + +The suite involves targeted fuzzing. Inputs are chosen to push the **result** onto those boundaries, to trigger coverage of every edge case, with a random pass to cover usual inputs as a backstop. + +A `Number` is `mantissa × 10^exponent`, sign-magnitude, normalized into a fixed +mantissa range. + +#### Deterministic sweeps and a random backstop + +Every operation is tested by **targeted, deterministic sweeps** that cover the +boundaries we can enumerate, plus a **random backstop** for the interior we +cannot. + +The backstop draws operands from `randomOperand`, which returns a boundary value +about a third of the time and a uniform interior value otherwise, so random +_pairs_ also mix a boundary operand with an interior one. + +Its exponent range is `[STAmount::kMinOffset, kMaxOffset]` = `[-96, 80]`, the range real amounts occupy, since `Number` backs `STAmount`. + +Widening it to the full exponent range was measured to catch **fewer** bugs (random pairs land so far apart that additions stop cancelling); the extremes are +covered by the deterministic sweeps instead. + +#### Landing a result on a boundary + +For the rounding-sensitive operators, what matters is where the **result** lands, +not where the inputs sit. Two techniques place it there: + +- **Forward** (mul/div exponent): the result exponent is `ea + eb + L` for + multiplication and `ea − eb − L` for division (`L = mantissaLog`), so choosing + the operand exponents lands the result exponent anywhere. `sweepResultExp` + walks it across `kMinExponent` / `kMaxExponent` one step at a time, splitting + the two operand exponents unevenly so both odd and even result exponents are + hit (a "both equal" split would skip the odd ones). + +- **Backward** (everything else): pick the target result `T` and derive the + partner operand from the inverse op: `b = T − a` (add), `b = a − T` (sub), + `b = a / T` (div), `b = T / a` (mul). + +#### The operators + +Each operator is tested by the shape that fits where it can break. + +| Operator | Test case targets | +| ----------------------------- | ------------------------------------------------------------------------------------------ | +| `mul`, `div` | where the result lands: the exponent at the under/overflow edges, the mantissa at the cusp | +| `add`, `sub` | cancellation and the cusp | +| `neg`, `signum` | input edges only | +| `normalize` | its input, including un-normalized values no other operator accepts | +| `to_rep` | rounding to an integer, the only operator that does so | +| `eq` `ne` `lt` `le` `gt` `ge` | sign and exponent ordering | diff --git a/external/lean4-deps/conanfile.py b/external/lean4-deps/conanfile.py new file mode 100644 index 00000000000..74b3dbe0ce3 --- /dev/null +++ b/external/lean4-deps/conanfile.py @@ -0,0 +1,128 @@ +import os +import shutil +from io import StringIO +from pathlib import Path + +from conan import ConanFile +from conan.errors import ConanException +from conan.tools.files import copy + +DEP_TARGETS = [ + "ProofWidgets:static", + "ImportGraph:static", + "LeanSearchClient:static", + "Plausible:static", + "Aesop:static", + "Qq:static", + "Batteries:static", + "Mathlib:static", +] + +MIN_OBJECTS = 7000 + +PACKAGES_DIR = "packages" +LIB_DIR = "lib" +ARCHIVE_NAME = "libLeanDeps.a" + + +class Lean4Deps(ConanFile): + """Prebuilt Lean4 mathlib and transitive deps bundled into lib/libLeanDeps.a. + + Downloads the mathlib olean cache and compiles the dependency :static + objects (oleans + .c.o.export) once. It rebuilds when the mathlib pin changes, + not when the model changes. + """ + + name = "lean4-deps" + settings = "os", "arch" + + def set_version(self): + if self.version is None: + toolchain = Path( + self.recipe_folder, "..", "..", "formal_verification", "lean-toolchain" + ) + self.version = toolchain.read_text(encoding="utf-8").strip().split(":v")[1] + + def export_sources(self): + source_dir = Path(self.recipe_folder, "..", "..", "formal_verification") + for filename in ("lakefile.toml", "lake-manifest.json", "lean-toolchain"): + copy(self, filename, src=source_dir, dst=self.export_sources_folder) + + def build_requirements(self): + self.tool_requires(f"lean4/{self.version}") + + def build(self): + # capture lake output and log only on failure. + # lake :static archive throws ARG_MAX error on mathlib (harmless), so verify by count + log = StringIO() + try: + self.run("lake exe cache get", cwd=self.build_folder, stdout=log, stderr=log) + self.run( + "lake build " + " ".join(DEP_TARGETS), + cwd=self.build_folder, + stdout=log, + stderr=log, + ignore_errors=True, + ) + objects = self._dep_objects() + n = len(objects) + if n < MIN_OBJECTS: + raise ConanException( + f"lean4-deps: Lean4 only {n} objects compiled (expected >= {MIN_OBJECTS})" + ) + self._bundle_deps(objects) + except Exception: + self.output.error(log.getvalue()) + raise + self.output.info( + f"lean4-deps: Lean4 compiled {n} objects, bundled into {ARCHIVE_NAME}" + ) + + def _dep_objects(self): + # Native objects from `lake build :static` (cache get only fetches .olean/.c) + packages_dir = Path(self.build_folder) / ".lake" / PACKAGES_DIR + objects = [] + for dirpath, _dirs, filenames in os.walk(packages_dir): + if "/ir/Cache/" in (dirpath.replace("\\", "/") + "/"): + continue + objects += [Path(dirpath) / name for name in filenames if name.endswith(".c.o.export")] + return objects + + def _bundle_deps(self, objects): + # short-named symlinks let the toolchain's llvm-ar bundle 8000+ objects (cap error on long names) + # @file avoids ARG_MAX (command line too long) error. + build_dir = Path(self.build_folder) + symlink_dir = build_dir / "lean_deps_symlinks" + shutil.rmtree(symlink_dir, ignore_errors=True) + symlink_dir.mkdir() + + symlinks = [symlink_dir / f"obj{i}.o" for i in range(len(objects))] + for symlink, target in zip(symlinks, objects): + symlink.symlink_to(target) + + response_file = build_dir / "lean_deps_objects.rsp" + response_file.write_text( + "".join(f"{symlink}\n" for symlink in symlinks), encoding="utf-8" + ) + + archive = build_dir / ARCHIVE_NAME + self.run(f'llvm-ar qcs "{archive}" "@{response_file}"') + + def package(self): + build_dir = Path(self.build_folder) + package_dir = Path(self.package_folder) + # Copy the whole lake build tree (.olean, .c files). Exclude .c.o.export files + # as those are bundled into libLeanDeps.a and the model build never requests them + copy( + self, + "*", + src=build_dir / ".lake" / PACKAGES_DIR, + dst=package_dir / PACKAGES_DIR, + excludes=["*.c.o.export"], + ) + copy(self, ARCHIVE_NAME, src=build_dir, dst=package_dir / LIB_DIR) + + def package_info(self): + package_dir = Path(self.package_folder) + self.cpp_info.set_property("packages", str(package_dir / PACKAGES_DIR)) + self.cpp_info.set_property("archive", str(package_dir / LIB_DIR / ARCHIVE_NAME)) diff --git a/external/lean4/conanfile.py b/external/lean4/conanfile.py new file mode 100644 index 00000000000..7e3a641be4d --- /dev/null +++ b/external/lean4/conanfile.py @@ -0,0 +1,71 @@ +from pathlib import Path + +from conan import ConanFile +from conan.errors import ConanInvalidConfiguration +from conan.tools.files import copy, get + +# sha256-pinned Lean releases per platform (no elan installer) (bump with the lean-toolchain pin) +_SHA256 = { + ("Macos", "x86_64"): "47010e6040ab2441dc96c1d9a3aca1721576fdbe4da566d938b29a26502fd378", + ("Macos", "armv8"): "d63a34d12978b035f871c8448d7243eb16711b8f5b27d7e9b093a210c1117e8d", + ("Linux", "x86_64"): "b02b74bb23e93e5b05f03f51ad06274814337d107718a02b6f89dc4db1387416", + ("Linux", "armv8"): "c608141afb645c7faa3845cc5dc503890ae329a82359f9bf37358d1fab499f81", +} + +RELEASE_URL = "https://github.com/leanprover/lean4/releases/download/v{version}/lean-{version}-{os_tag}{arch_suffix}.zip" + + +class Lean(ConanFile): + """Lean 4 toolchain (lean, lake, headers, runtime) from the pinned leanprover/lean4 release. + + Version defaults from formal_verification/lean-toolchain, pass --version + when exporting outside the repo layout (e.g. the CI image). + """ + + name = "lean4" + license = "Apache-2.0" + url = "https://github.com/leanprover/lean4" + description = "The Lean 4 theorem prover and toolchain" + settings = "os", "arch" + + def set_version(self): + if self.version is None: + toolchain = Path( + self.recipe_folder, "..", "..", "formal_verification", "lean-toolchain" + ) + # "leanprover/lean4:vX" -> "X" + self.version = toolchain.read_text(encoding="utf-8").strip().split(":v")[1] + + def build(self): + os_name, arch = str(self.settings.os), str(self.settings.arch) + sha256 = _SHA256.get((os_name, arch)) + if sha256 is None: + raise ConanInvalidConfiguration(f"lean4: unsupported platform {os_name}/{arch}") + os_tag = "darwin" if os_name == "Macos" else "linux" + arch_suffix = "_aarch64" if arch == "armv8" else "" + url = RELEASE_URL.format( + version=self.version, os_tag=os_tag, arch_suffix=arch_suffix + ) + get( + self, + url, + sha256=sha256, + strip_root=True, + keep_permissions=True, + destination=Path(self.build_folder) / "toolchain", + ) + + def package(self): + copy( + self, + "*", + src=Path(self.build_folder) / "toolchain", + dst=self.package_folder, + ) + + def package_info(self): + self.cpp_info.includedirs = ["include"] + self.cpp_info.libdirs = [str(Path("lib") / "lean")] + self.cpp_info.libs = ["Lake", "leanshared"] # order matters: Lake before the runtime + self.cpp_info.bindirs = ["bin"] + self.buildenv_info.prepend_path("PATH", str(Path(self.package_folder) / "bin")) diff --git a/formal_verification/README.md b/formal_verification/README.md new file mode 100644 index 00000000000..2fd0f23c37f --- /dev/null +++ b/formal_verification/README.md @@ -0,0 +1,34 @@ +# XRPL formal verification (Lean 4) + +The Lean 4 model of XRPL, the theorems about it, and the FFI exports that the +C++ cross-validation tests call. For how the model, proofs, FFI, and build all +fit together, see +[docs/formal-verification/README.md](../docs/formal-verification/README.md). + +## Layout + +- `XRPL/Model/`: the Lean model of the C++ types (e.g. `Number`). +- `XRPL/Properties/`: theorems about the model. +- `XRPL/FFI/`: the `@[export]` wrappers the C++ tests call. + +## Building + +Nothing here is built by hand for usual use. The C++ cross-validation tests +compile this model in-tree and link it into `xrpld`, gated by the +`formal_verification` option; the Lean toolchain comes from the one `lean4` +Conan package, so it needs no separate Lean or elan install. + +## Working on the proofs directly + +Only needed when editing the Lean model or proofs by hand. You can use lake binary in `.conan2` directory or install your own. + +That requires [elan](https://github.com/leanprover/elan) (it provides the Lean +version pinned in `lean-toolchain`): + +```bash +lake exe cache get +lake build +``` + +`lake build` is the proof check: it passes only if every file elaborates with no +`sorry` and standard axioms. diff --git a/formal_verification/XRPL.lean b/formal_verification/XRPL.lean new file mode 100644 index 00000000000..b5da65c9425 --- /dev/null +++ b/formal_verification/XRPL.lean @@ -0,0 +1,3 @@ +import XRPL.FFI.FFI +import XRPL.Model.Model +import XRPL.Properties.Properties diff --git a/formal_verification/XRPL/FFI/CommonFFI.lean b/formal_verification/XRPL/FFI/CommonFFI.lean new file mode 100644 index 00000000000..8f30d8a3072 --- /dev/null +++ b/formal_verification/XRPL/FFI/CommonFFI.lean @@ -0,0 +1,11 @@ +import XRPL.Model.Protocol.Number + + +namespace XRPL.FFI + +open XRPL.Model.Protocol + +def decodeNumber (neg : UInt8) (mant : UInt64) (exp : Int64) : Number := + Number.unchecked (neg != 0) mant exp.toInt + +end XRPL.FFI diff --git a/formal_verification/XRPL/FFI/FFI.lean b/formal_verification/XRPL/FFI/FFI.lean new file mode 100644 index 00000000000..6f76ad94a11 --- /dev/null +++ b/formal_verification/XRPL/FFI/FFI.lean @@ -0,0 +1 @@ +import XRPL.FFI.Protocol.NumberFFI diff --git a/formal_verification/XRPL/FFI/Protocol/NumberFFI.lean b/formal_verification/XRPL/FFI/Protocol/NumberFFI.lean new file mode 100644 index 00000000000..70a88b4f705 --- /dev/null +++ b/formal_verification/XRPL/FFI/Protocol/NumberFFI.lean @@ -0,0 +1,14 @@ +import XRPL.FFI.CommonFFI +import XRPL.Model.Protocol.Number + + +namespace XRPL.FFI + +open XRPL.Model.Protocol (Number) + +@[export lean_number_lt] +def lean_number_lt (neg1 : UInt8) (mant1 : UInt64) (exp1 : Int64) + (neg2 : UInt8) (mant2 : UInt64) (exp2 : Int64) : UInt8 := + if Number.operator_lt (decodeNumber neg1 mant1 exp1) (decodeNumber neg2 mant2 exp2) then 1 else 0 + +end XRPL.FFI diff --git a/formal_verification/XRPL/Model/Model.lean b/formal_verification/XRPL/Model/Model.lean new file mode 100644 index 00000000000..a6c5eb6ddff --- /dev/null +++ b/formal_verification/XRPL/Model/Model.lean @@ -0,0 +1 @@ +import XRPL.Model.Protocol.Number diff --git a/formal_verification/XRPL/Model/Protocol/Number.lean b/formal_verification/XRPL/Model/Protocol/Number.lean new file mode 100644 index 00000000000..ec4ff4c810b --- /dev/null +++ b/formal_verification/XRPL/Model/Protocol/Number.lean @@ -0,0 +1,60 @@ +import Mathlib.Tactic + +set_option linter.style.nativeDecide false + +namespace XRPL.Model.Protocol + +def cMaxValue : UInt64 := 9999999999999999 + +structure MantissaRange where + min : UInt64 + max : UInt64 + hrange : max.toNat + 1 = 10 * min.toNat := by decide + hfit : cMaxValue.toNat ≤ max.toNat := by decide + +def largeRange : MantissaRange := { min := 1000000000000000000, max := 9999999999999999999 } +def minExponent : Int := -32768 +def maxExponent : Int := 32768 +def maxRep : UInt64 := 9223372036854775807 + +structure Number where + negative_ : Bool + mantissa_ : UInt64 + exponent_ : Int + deriving DecidableEq, Repr + +def Number.zero : Number := + { negative_ := false, mantissa_ := 0, exponent_ := -2147483648 } + +def Number.unchecked (negative : Bool) (mantissa : UInt64) (exponent : Int) : Number := + { negative_ := negative, mantissa_ := mantissa, exponent_ := exponent } + +def Number.isnormal (n : Number) : Prop := + n = Number.zero ∨ + (largeRange.min ≤ n.mantissa_ ∧ n.mantissa_ ≤ largeRange.max ∧ + (n.mantissa_ ≤ maxRep ∨ n.mantissa_.toNat % 10 = 0) ∧ + minExponent ≤ n.exponent_ ∧ n.exponent_ ≤ maxExponent) + +abbrev Number.isNormalized (n : Number) : Prop := n.isnormal + +def Number.toRat (n : Number) : ℚ := + let sign : Int := if n.negative_ then -1 else 1 + let m : Int := n.mantissa_.toNat + if n.exponent_ ≥ 0 then + mkRat (sign * m * (10 : Int) ^ n.exponent_.toNat) 1 + else + mkRat (sign * m) ((10 : Nat) ^ (-n.exponent_).toNat) + +def Number.operator_lt (l r : Number) : Bool := + let lneg := l.negative_ + let rneg := r.negative_ + if lneg != rneg then lneg + else if l.mantissa_ == 0 then r.mantissa_ > 0 + else if r.mantissa_ == 0 then false + else if l.exponent_ > r.exponent_ then lneg + else if l.exponent_ < r.exponent_ then !lneg + else if lneg then l.mantissa_ > r.mantissa_ + else l.mantissa_ < r.mantissa_ + + +end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Properties.lean b/formal_verification/XRPL/Properties/Properties.lean new file mode 100644 index 00000000000..a99af774f9d --- /dev/null +++ b/formal_verification/XRPL/Properties/Properties.lean @@ -0,0 +1 @@ +import XRPL.Properties.Protocol.Number.Compare.Compare diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean b/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean new file mode 100644 index 00000000000..df00d4d90bc --- /dev/null +++ b/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean @@ -0,0 +1,14 @@ +import Mathlib.Tactic + +import XRPL.Model.Protocol.Number + + +namespace XRPL.Model.Protocol + +/-- `largeRange.min.toNat = 10^18`. -/ +lemma largeRange_min_val : largeRange.min.toNat = 1000000000000000000 := by decide + +/-- `largeRange.max.toNat = 10^19 - 1`. -/ +lemma largeRange_max_val : largeRange.max.toNat = 9999999999999999999 := by decide + +end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean b/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean new file mode 100644 index 00000000000..77c65bc4cf2 --- /dev/null +++ b/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean @@ -0,0 +1,106 @@ +import Mathlib.Tactic + +import XRPL.Model.Protocol.Number +import XRPL.Properties.Protocol.Number.Common.Constants + + +namespace XRPL.Model.Protocol +/-- Extract mantissa bounds from `isNormalized` when mantissa is nonzero. -/ +lemma Number.isNormalized.mantissaBounds {n : Number} + (h : n.isNormalized) (hne : n.mantissa_ ≠ 0) : + largeRange.min ≤ n.mantissa_ ∧ n.mantissa_ ≤ largeRange.max := by + rcases h with h_zero | ⟨hmin, hmax, _, _, _⟩ + · exfalso; apply hne; rw [h_zero]; rfl + · exact ⟨hmin, hmax⟩ + +/-- `|n.toRat| = n.mantissa_.toNat * 10^n.exponent_`. -/ +lemma abs_toRat_eq (n : Number) : + |n.toRat| = (n.mantissa_.toNat : ℚ) * 10 ^ n.exponent_ := by + unfold Number.toRat + split_ifs with hneg hexp hexp + · rw [Rat.mkRat_one] + have h_to : n.exponent_ = (n.exponent_.toNat : ℤ) := (Int.toNat_of_nonneg hexp).symm + have h_neg_val : ((-1 * (n.mantissa_.toNat : Int) * (10 : Int) ^ n.exponent_.toNat : Int) : ℚ) + = -((n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_) := by + push_cast + conv_rhs => rw [h_to]; rw [zpow_natCast] + ring + rw [h_neg_val, abs_neg] + rw [abs_of_nonneg (by positivity)] + · have hneg_exp : n.exponent_ < 0 := not_le.mp hexp + have h_pow : (0 : ℚ) < (10 : ℚ) ^ n.exponent_ := zpow_pos (by norm_num) _ + rw [Rat.mkRat_eq_div] + push_cast + have h_neg_exp : n.exponent_ = -((-n.exponent_).toNat : ℤ) := by + rw [Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ -n.exponent_)]; ring + have h_val : (-1 * (n.mantissa_.toNat : ℚ)) / (10 : ℚ) ^ (-n.exponent_).toNat + = -((n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_) := by + conv_rhs => rw [h_neg_exp, zpow_neg, zpow_natCast] + field_simp + rw [h_val, abs_neg, abs_of_nonneg (by positivity)] + · rw [Rat.mkRat_one] + have h_to : n.exponent_ = (n.exponent_.toNat : ℤ) := (Int.toNat_of_nonneg hexp).symm + have h_val : ((1 * (n.mantissa_.toNat : Int) * (10 : Int) ^ n.exponent_.toNat : Int) : ℚ) + = (n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_ := by + push_cast + conv_rhs => rw [h_to]; rw [zpow_natCast] + ring + rw [h_val, abs_of_nonneg (by positivity)] + · have hneg_exp : n.exponent_ < 0 := not_le.mp hexp + rw [Rat.mkRat_eq_div] + push_cast + have h_neg_exp : n.exponent_ = -((-n.exponent_).toNat : ℤ) := by + rw [Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ -n.exponent_)]; ring + have h_val : (1 * (n.mantissa_.toNat : ℚ)) / (10 : ℚ) ^ (-n.exponent_).toNat + = (n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_ := by + conv_rhs => rw [h_neg_exp, zpow_neg, zpow_natCast] + field_simp + rw [h_val, abs_of_nonneg (by positivity)] + +/-- `n.toRat ≤ 0` when `negative_ = true`. -/ +lemma Number.toRat_nonpos_of_negative (n : Number) (hneg : n.negative_ = true) : + n.toRat ≤ 0 := by + unfold Number.toRat + rw [hneg]; simp only [if_true] + split_ifs with hexp + · rw [Rat.mkRat_one]; push_cast + have : (0 : ℚ) ≤ (n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_.toNat := by positivity + linarith + · rw [Rat.mkRat_eq_div]; push_cast + have h_m_nn : (0 : ℚ) ≤ (n.mantissa_.toNat : ℚ) := Nat.cast_nonneg _ + have h_pow_pos : (0 : ℚ) < (10 : ℚ) ^ (-n.exponent_).toNat := by positivity + have h_frac_nn : (0 : ℚ) ≤ (n.mantissa_.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent_).toNat := + div_nonneg h_m_nn (le_of_lt h_pow_pos) + have : -(1 : ℚ) * (n.mantissa_.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent_).toNat + = -((n.mantissa_.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent_).toNat) := by + field_simp + rw [this]; linarith + +/-- `0 ≤ n.toRat` when `negative_ = false`. -/ +lemma Number.toRat_nonneg_of_nonnegative (n : Number) (hneg : n.negative_ = false) : + 0 ≤ n.toRat := by + unfold Number.toRat + rw [hneg]; simp only [Bool.false_eq_true, if_false] + split_ifs + · rw [Rat.mkRat_one]; push_cast; positivity + · rw [Rat.mkRat_eq_div]; push_cast; positivity + +/-- `n.toRat = 0` iff `n.mantissa_ = 0`. -/ +lemma Number.toRat_eq_zero_iff {n : Number} : + n.toRat = 0 ↔ n.mantissa_ = 0 := by + constructor + · intro h + have habs := abs_toRat_eq n + rw [h, abs_zero] at habs + have h10_pos : (0 : ℚ) < 10 ^ n.exponent_ := zpow_pos (by norm_num) _ + have hm_zero : (n.mantissa_.toNat : ℚ) = 0 := by + nlinarith [Nat.cast_nonneg (α := ℚ) n.mantissa_.toNat] + have : n.mantissa_.toNat = 0 := by exact_mod_cast hm_zero + exact UInt64.ext this + · intro h + have hm : n.mantissa_.toNat = 0 := by rw [h]; rfl + unfold Number.toRat + simp only [hm, Nat.cast_zero] + split_ifs <;> simp + +end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean new file mode 100644 index 00000000000..6517c781902 --- /dev/null +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean @@ -0,0 +1,226 @@ +import XRPL.Properties.Protocol.Number.Common.ToRatLemmas +import XRPL.Properties.Protocol.Number.Signum.Common.Proofs + + +namespace XRPL.Model.Protocol + +/-- Strictly positive value: non-negative flag and nonzero mantissa. -/ +lemma Number.toRat_pos_of_not_negative (n : Number) (hneg : n.negative_ = false) + (hm : n.mantissa_ ≠ 0) : 0 < n.toRat := by + have h1 := Number.toRat_nonneg_of_nonnegative n hneg + have h2 : n.toRat ≠ 0 := fun h => hm (Number.toRat_eq_zero_iff.mp h) + exact lt_of_le_of_ne h1 (Ne.symm h2) + +/-- Strictly negative value: negative flag and nonzero mantissa. -/ +lemma Number.toRat_neg_of_negative' (n : Number) (hneg : n.negative_ = true) + (hm : n.mantissa_ ≠ 0) : n.toRat < 0 := by + have h1 := Number.toRat_nonpos_of_negative n hneg + have h2 : n.toRat ≠ 0 := fun h => hm (Number.toRat_eq_zero_iff.mp h) + exact lt_of_le_of_ne h1 h2 + +/-- Exponent dominance: for normalized nonzero values, a strictly smaller +exponent means a strictly smaller magnitude (`m ∈ [10^18, 10^19)` forces it). -/ +lemma abs_toRat_lt_of_exp_lt (x y : Number) + (hx : x.isNormalized) (hy : y.isNormalized) + (hxm : x.mantissa_ ≠ 0) (hym : y.mantissa_ ≠ 0) + (hexp : x.exponent_ < y.exponent_) : + |x.toRat| < |y.toRat| := by + rw [abs_toRat_eq, abs_toRat_eq] + obtain ⟨_, hxmax⟩ := hx.mantissaBounds hxm + obtain ⟨hymin, _⟩ := hy.mantissaBounds hym + have hxm_le : (x.mantissa_.toNat : ℚ) ≤ 9999999999999999999 := by + have := UInt64.le_iff_toNat_le.mp hxmax + rw [largeRange_max_val] at this + exact_mod_cast this + have hym_ge : (1000000000000000000 : ℚ) ≤ (y.mantissa_.toNat : ℚ) := by + have := UInt64.le_iff_toNat_le.mp hymin + rw [largeRange_min_val] at this + exact_mod_cast this + have hpow_x : (0 : ℚ) < 10 ^ x.exponent_ := zpow_pos (by norm_num) _ + have hpow_y : (0 : ℚ) < 10 ^ y.exponent_ := zpow_pos (by norm_num) _ + calc (x.mantissa_.toNat : ℚ) * 10 ^ x.exponent_ + ≤ 9999999999999999999 * 10 ^ x.exponent_ := + mul_le_mul_of_nonneg_right hxm_le (le_of_lt hpow_x) + _ < 1000000000000000000 * 10 ^ (x.exponent_ + 1) := by + rw [zpow_add_one₀ (by norm_num : (10 : ℚ) ≠ 0), + show (1000000000000000000 : ℚ) * (10 ^ x.exponent_ * 10) + = 10000000000000000000 * 10 ^ x.exponent_ from by ring] + exact mul_lt_mul_of_pos_right (by norm_num) hpow_x + _ ≤ 1000000000000000000 * 10 ^ y.exponent_ := by + apply mul_le_mul_of_nonneg_left _ (by norm_num) + exact zpow_le_zpow_right₀ (by norm_num) (by omega) + _ ≤ (y.mantissa_.toNat : ℚ) * 10 ^ y.exponent_ := + mul_le_mul_of_nonneg_right hym_ge (le_of_lt hpow_y) + +/-- Same exponent: magnitude order is mantissa order. -/ +lemma abs_toRat_lt_iff_of_exp_eq (x y : Number) + (hexp : x.exponent_ = y.exponent_) : + |x.toRat| < |y.toRat| ↔ x.mantissa_ < y.mantissa_ := by + rw [abs_toRat_eq, abs_toRat_eq, hexp] + have hpow : (0 : ℚ) < 10 ^ y.exponent_ := zpow_pos (by norm_num) _ + constructor + · intro h + have := lt_of_mul_lt_mul_right h (le_of_lt hpow) + rw [UInt64.lt_iff_toNat_lt] + exact_mod_cast this + · intro h + have h' : (x.mantissa_.toNat : ℚ) < y.mantissa_.toNat := by + exact_mod_cast UInt64.lt_iff_toNat_lt.mp h + exact mul_lt_mul_of_pos_right h' hpow + +/-- The signed value of a negative `Number` is the negated magnitude. -/ +private lemma toRat_eq_neg_abs (n : Number) (hneg : n.negative_ = true) : + n.toRat = -|n.toRat| := by + rw [abs_of_nonpos (Number.toRat_nonpos_of_negative n hneg)] + ring + +/-- The signed value of a non-negative `Number` is its magnitude. -/ +private lemma toRat_eq_abs (n : Number) (hneg : n.negative_ = false) : + n.toRat = |n.toRat| := by + rw [abs_of_nonneg (Number.toRat_nonneg_of_nonnegative n hneg)] + +/-- **Correctness of `operator_lt`**: on normalized values the comparison agrees +with the rational order. -/ +theorem operator_lt_iff_proof (x y : Number) + (hx : x.isNormalized) (hy : y.isNormalized) : + x.operator_lt y = true ↔ x.toRat < y.toRat := by + by_cases hsx : x.negative_ = true + · by_cases hsy : y.negative_ = true + · -- both negative: nonzero mantissas, value = −magnitude. + have hxm : x.mantissa_ ≠ 0 := Number.mantissa_ne_zero_of_negative x hx hsx + have hym : y.mantissa_ ≠ 0 := Number.mantissa_ne_zero_of_negative y hy hsy + have hxs := toRat_eq_neg_abs x hsx + have hys := toRat_eq_neg_abs y hsy + unfold Number.operator_lt + rw [hsx, hsy] + simp only [bne_self_eq_false, Bool.false_eq_true, if_false] + rw [show (x.mantissa_ == 0) = false from beq_eq_false_iff_ne.mpr hxm, + show (y.mantissa_ == 0) = false from beq_eq_false_iff_ne.mpr hym] + simp only [Bool.false_eq_true, if_false] + rcases lt_trichotomy x.exponent_ y.exponent_ with hexp | hexp | hexp + · -- ex < ey: |x| < |y| so x > y; the operator returns !lneg = false. + rw [if_neg (by omega : ¬ x.exponent_ > y.exponent_), if_pos hexp, + show (!(true : Bool)) = false from rfl] + simp only [Bool.false_eq_true, false_iff, not_lt] + have habs := abs_toRat_lt_of_exp_lt x y hx hy hxm hym hexp + rw [hxs, hys] + linarith + · -- ex = ey: sign-aware mantissa compare. + rw [if_neg (by omega : ¬ x.exponent_ > y.exponent_), + if_neg (by omega : ¬ x.exponent_ < y.exponent_), if_pos trivial, + decide_eq_true_iff] + constructor + · intro h + have habs := (abs_toRat_lt_iff_of_exp_eq y x hexp.symm).mpr h + rw [hxs, hys] + linarith + · intro h + rw [hxs, hys] at h + exact (abs_toRat_lt_iff_of_exp_eq y x hexp.symm).mp (by linarith) + · -- ex > ey: |x| > |y| so x < y; the operator returns lneg = true. + rw [if_pos hexp] + constructor + · intro _ + have habs := abs_toRat_lt_of_exp_lt y x hy hx hym hxm hexp + rw [hxs, hys] + linarith + · intro _ + rfl + · -- x negative, y non-negative: x < y always. + have hsyf : y.negative_ = false := Bool.not_eq_true _ |>.mp hsy + have hxm : x.mantissa_ ≠ 0 := Number.mantissa_ne_zero_of_negative x hx hsx + have heval : x.operator_lt y = true := by + unfold Number.operator_lt + rw [hsx, hsyf] + rfl + rw [heval] + simp only [true_iff] + have h1 := Number.toRat_neg_of_negative' x hsx hxm + have h2 := Number.toRat_nonneg_of_nonnegative y hsyf + linarith + · have hsxf : x.negative_ = false := Bool.not_eq_true _ |>.mp hsx + by_cases hsy : y.negative_ = true + · -- x non-negative, y negative: never x < y. + have hym : y.mantissa_ ≠ 0 := Number.mantissa_ne_zero_of_negative y hy hsy + have heval : x.operator_lt y = false := by + unfold Number.operator_lt + rw [hsxf, hsy] + rfl + rw [heval] + simp only [Bool.false_eq_true, false_iff, not_lt] + have h1 := Number.toRat_nonneg_of_nonnegative x hsxf + have h2 := Number.toRat_neg_of_negative' y hsy hym + linarith + · -- both non-negative. + have hsyf : y.negative_ = false := Bool.not_eq_true _ |>.mp hsy + have hxs := toRat_eq_abs x hsxf + have hys := toRat_eq_abs y hsyf + unfold Number.operator_lt + rw [hsxf, hsyf] + simp only [bne_self_eq_false, Bool.false_eq_true, if_false] + by_cases hxm : x.mantissa_ = 0 + · -- x = 0: x < y iff y is nonzero. + rw [show (x.mantissa_ == 0) = true from beq_iff_eq.mpr hxm] + simp only [if_true] + rw [decide_eq_true_iff] + have hx0 : x.toRat = 0 := Number.toRat_eq_zero_iff.mpr hxm + rw [hx0] + constructor + · intro h + have hym : y.mantissa_ ≠ 0 := by + intro hc + rw [hc] at h + exact absurd h (by decide) + exact Number.toRat_pos_of_not_negative y hsyf hym + · intro h + have hym : y.mantissa_ ≠ 0 := + fun hc => absurd (Number.toRat_eq_zero_iff.mpr hc) (ne_of_gt h) + change (0 : UInt64) < y.mantissa_ + rw [UInt64.lt_iff_toNat_lt, show (0 : UInt64).toNat = 0 from rfl] + have hne : y.mantissa_.toNat ≠ 0 := by + intro hc + apply hym + rw [← UInt64.toNat_inj, hc] + rfl + omega + · rw [show (x.mantissa_ == 0) = false from beq_eq_false_iff_ne.mpr hxm] + simp only [Bool.false_eq_true, if_false] + by_cases hym : y.mantissa_ = 0 + · -- y = 0: a positive x is never below it. + rw [show (y.mantissa_ == 0) = true from beq_iff_eq.mpr hym] + simp only [if_true] + have hy0 : y.toRat = 0 := Number.toRat_eq_zero_iff.mpr hym + rw [hy0] + simp only [Bool.false_eq_true, false_iff, not_lt] + exact le_of_lt (Number.toRat_pos_of_not_negative x hsxf hxm) + · rw [show (y.mantissa_ == 0) = false from beq_eq_false_iff_ne.mpr hym] + simp only [Bool.false_eq_true, if_false] + rcases lt_trichotomy x.exponent_ y.exponent_ with hexp | hexp | hexp + · -- ex < ey: |x| < |y| so x < y; the operator returns !lneg = true. + rw [if_neg (by omega : ¬ x.exponent_ > y.exponent_), if_pos hexp, + show (!(false : Bool)) = true from rfl] + simp only [true_iff] + have habs := abs_toRat_lt_of_exp_lt x y hx hy hxm hym hexp + rw [hxs, hys] + linarith + · -- ex = ey: mantissa compare. + rw [if_neg (by omega : ¬ x.exponent_ > y.exponent_), + if_neg (by omega : ¬ x.exponent_ < y.exponent_), + decide_eq_true_iff] + constructor + · intro h + have habs := (abs_toRat_lt_iff_of_exp_eq x y hexp).mpr h + rw [hxs, hys] + linarith + · intro h + rw [hxs, hys] at h + exact (abs_toRat_lt_iff_of_exp_eq x y hexp).mp (by linarith) + · -- ex > ey: |x| > |y| so never x < y; the operator returns lneg = false. + rw [if_pos hexp] + simp only [Bool.false_eq_true, false_iff, not_lt] + have habs := abs_toRat_lt_of_exp_lt y x hy hx hym hxm hexp + rw [hxs, hys] + linarith + + +end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean new file mode 100644 index 00000000000..3b0b446f52f --- /dev/null +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean @@ -0,0 +1,11 @@ +import XRPL.Properties.Protocol.Number.Compare.Common.Proofs + + +namespace XRPL.Model.Protocol + +theorem operator_lt_iff (x y : Number) + (hx : x.isNormalized) (hy : y.isNormalized) : + x.operator_lt y = true ↔ x.toRat < y.toRat := + operator_lt_iff_proof x y hx hy + +end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean b/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean new file mode 100644 index 00000000000..4dfb669fd8d --- /dev/null +++ b/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean @@ -0,0 +1,16 @@ +import XRPL.Properties.Protocol.Number.Common.ToRatLemmas + + +namespace XRPL.Model.Protocol + +/-- A normalized number is nonzero exactly when its mantissa is nonzero. The +only normalized value with `mantissa_ = 0` is the canonical `Number.zero` +(positive), so a negative normalized number always has a nonzero mantissa. -/ +lemma Number.mantissa_ne_zero_of_negative (n : Number) (hn : n.isNormalized) + (hneg : n.negative_ = true) : n.mantissa_ ≠ 0 := by + rcases hn with heq | ⟨hlo, _⟩ + · rw [heq] at hneg; exact absurd hneg (by decide) + · intro hm; rw [hm] at hlo; exact absurd hlo (by decide) + + +end XRPL.Model.Protocol diff --git a/formal_verification/lake-manifest.json b/formal_verification/lake-manifest.json new file mode 100644 index 00000000000..dc3caf1124e --- /dev/null +++ b/formal_verification/lake-manifest.json @@ -0,0 +1,176 @@ +{ + "version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "277a38fac8a62fad760e79889d3d1b366966e28b", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.28.0", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/david-christiansen/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "afe450eaab63fbc37bcb400d4db827538fcab805", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "06c8b4d690d9b7ef98d594672bbdaa618156215a", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "46c359dcff7e8db7f63efd17f188c3967207335c", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.87", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "XRPL", + "lakeDir": ".lake" +} diff --git a/formal_verification/lakefile.toml b/formal_verification/lakefile.toml new file mode 100644 index 00000000000..c24f8c48600 --- /dev/null +++ b/formal_verification/lakefile.toml @@ -0,0 +1,27 @@ +name = "XRPL" +version = "0.1.0" +keywords = ["math"] +defaultTargets = ["XRPL"] + +[leanOptions] +pp.unicode.fun = true # pretty-prints `fun a ↦ b` +relaxedAutoImplicit = false +weak.linter.mathlibStandardSet = true +weak.linter.style.longLine = false +weak.linter.style.emptyLine = false +weak.linter.style.show = false +maxSynthPendingDepth = 3 + +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "v4.28.0" + +[[lean_lib]] +name = "XRPL" + +# lake build XRPLModel:static +[[lean_lib]] +name = "XRPLModel" +roots = ["XRPL.Model.Model", "XRPL.FFI.FFI"] +globs = ["XRPL.Model.+", "XRPL.FFI.+"] diff --git a/formal_verification/lean-toolchain b/formal_verification/lean-toolchain new file mode 100644 index 00000000000..4c685fa085f --- /dev/null +++ b/formal_verification/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.28.0 diff --git a/src/test/formal_verification/common/LeanSuite.h b/src/test/formal_verification/common/LeanSuite.h new file mode 100644 index 00000000000..3d8eb2fac2e --- /dev/null +++ b/src/test/formal_verification/common/LeanSuite.h @@ -0,0 +1,96 @@ +#pragma once + +#include + +#include + +#include +#include +#include +#include +#include + +extern "C" void +lean_initialize_runtime_module(void); + +extern "C" lean_object* +initialize_XRPL_XRPL_FFI_FFI(uint8_t builtin, lean_object* w); + +namespace xrpl::test::formal_verification { + +// Per-thread RNG; beginCase reseeds it deterministically per case. +inline std::mt19937_64& +nextRng() +{ + thread_local std::mt19937_64 rng{0xBEEFCAFEDEADBEEFULL}; + return rng; +} + +// Base for Lean-FFI test suites. run() guards Lean init + serializes all FFI +// calls behind a mutex (Lean's runtime is single-threaded). +class LeanSuite : public beast::unit_test::Suite +{ + static std::mutex& + leanMutex() + { + static std::mutex m; + return m; + } + + static bool + ensureLeanInit() + { + static std::once_flag flag; + static bool ok = false; + std::call_once(flag, [] { + lean_initialize_runtime_module(); + lean_object* res = initialize_XRPL_XRPL_FFI_FFI(1, lean_io_mk_world()); + if (!lean_io_result_is_ok(res)) + { + lean_dec(res); + return; + } + lean_dec_ref(res); + lean_io_mark_end_initialization(); + ok = true; + }); + return ok; + } + + virtual void + runTests() = 0; + +protected: + // Pass "Suite.method" for seedRng so the per-thread RNG seed is unique + // across suites that share method names. + void + beginCase(char const* name, bool seedRng = false) + { + testcase << name; + if (seedRng) + nextRng().seed(std::hash{}(name)); + } + + template + void + runFuzz(int iterations, F&& check) + { + for (int i = 0; i < iterations; ++i) + (void)check(); + } + +public: + void + run() final + { + std::lock_guard lock(leanMutex()); + if (!ensureLeanInit()) + { + fail("Lean runtime failed to initialize"); + return; + } + runTests(); + } +}; + +} // namespace xrpl::test::formal_verification diff --git a/src/test/formal_verification/numbers/LeanNumber_test.cpp b/src/test/formal_verification/numbers/LeanNumber_test.cpp new file mode 100644 index 00000000000..f0ed5308041 --- /dev/null +++ b/src/test/formal_verification/numbers/LeanNumber_test.cpp @@ -0,0 +1,199 @@ +#include +#include + +#include +#include + +#include +#include +#include +#include +#include +#include + +extern "C" { +uint8_t +lean_number_lt(uint8_t, uint64_t, uint64_t, uint8_t, uint64_t, uint64_t); +} + +namespace xrpl::test { + +using namespace formal_verification; + +class LeanNumber_test : public LeanSuite +{ + static std::string + fmtNum(bool neg, uint64_t m, int e) + { + std::stringstream ss; + ss << (neg ? "-" : "") << m << "e" << e; + return ss.str(); + } + + static std::string + fmtNum(NumberPair const& p) + { + return fmtNum(p.leanNum.negative != 0, p.leanNum.mantissa, p.cppNum.exponent()); + } + + using LeanCmpOp = uint8_t (*)(uint8_t, uint64_t, uint64_t, uint8_t, uint64_t, uint64_t); + + // Verify Lean and C++ agree on operator< for one pair. + // Comparisons can't error, so we compare the raw bool results directly. + bool + checkCompare(std::string const& label, NumberPair const& a, NumberPair const& b) + { + auto leanCmp = [&](LeanCmpOp op) { + return op(a.leanNum.negative, + a.leanNum.mantissa, + a.leanNum.exponent, + b.leanNum.negative, + b.leanNum.mantissa, + b.leanNum.exponent) != 0; + }; + struct Case + { + char const* sym; + bool lean; + bool cpp; + }; + Case const cases[] = { + {"<", leanCmp(lean_number_lt), a.cppNum < b.cppNum}, + }; + bool ok = true; + for (auto const& c : cases) + { + if (c.lean != c.cpp) + { + std::stringstream ss; + ss << label << ' ' << c.sym << ": lean=" << c.lean << " cpp=" << c.cpp; + fail(ss.str()); + ok = false; + } + } + if (ok) + pass(); + return ok; + } + + std::vector + edgeMantissas() const + { + uint64_t const minM = Number::minMantissa(); + uint64_t const maxRep = Number::kMaxRep; + uint64_t const maxM = Number::maxMantissa(); + return { + minM, + minM + 1, + maxRep - 1, + maxRep, + Number::kMaxRep + 3, + maxM - maxM % 10, + }; + } + + std::vector> + edgeExpPairs() const + { + return { + {0, 0}, {0, 1}, {0, -1}, {0, 18}, {0, -40}, {40, 40}, {-40, -40}, {80, -96}, {-96, 80}}; + } + + std::vector + edgeExps() const + { + return {0, 1, -1, 18, -18, 40, -40, 80, -96}; + } + + // One operand: ~1/3 a random edge value, else a uniform interior value. + NumberPair + randomOperand() + { + constexpr double edgeBias = 1.0 / 3; + auto& rng = nextRng(); + std::bernoulli_distribution useEdge(edgeBias); + if (useEdge(rng)) + { + auto const ms = edgeMantissas(); + auto const es = edgeExps(); + std::uniform_int_distribution mi(0, ms.size() - 1); + std::uniform_int_distribution ei(0, es.size() - 1); + std::bernoulli_distribution sign(0.5); + return makeNumberPair(sign(rng), ms[mi(rng)], es[ei(rng)]); + } + return randomNumberPair(-96, 80); + } + +public: + void + testCompare() + { + beginCase("LeanNumber.compare", true); + NumberMantissaScaleGuard sg(MantissaRange::MantissaScale::Large); + auto const ms = edgeMantissas(); + auto const exps = edgeExpPairs(); + + for (uint64_t ma : ms) + for (bool na : {false, true}) + for (uint64_t mb : ms) + for (bool nb : {false, true}) + for (auto const& [ea, eb] : exps) + { + auto a = makeNumberPair(na, ma, ea); + auto b = makeNumberPair(nb, mb, eb); + checkCompare(fmtNum(a) + " ? " + fmtNum(b), a, b); + } + for (uint64_t m : ms) + for (bool n : {false, true}) + checkCompare( + "0 ? " + fmtNum(makeNumberPair(n, m, 0)), + makeNumberPair(false, 0, 0), + makeNumberPair(n, m, 0)); + + runFuzz(10'000, [&] { + auto a = randomOperand(); + auto b = randomOperand(); + bool ok = checkCompare(fmtNum(a) + " ? " + fmtNum(b), a, b); + ok = checkCompare(fmtNum(a) + " ? self", a, a) && ok; + return ok; + }); + } + + // Regression for XRPLF/rippled#7406: equal-exponent negative comparison. + void + testNegativeComparison() + { + beginCase("LeanNumber.negative_comparison"); + NumberMantissaScaleGuard sg(MantissaRange::MantissaScale::Large); + + auto a = makeNumberPair(true, 3'000'000'000'000'000'000ULL, 0); + auto b = makeNumberPair(true, 7'000'000'000'000'000'000ULL, 0); + + checkCompare("(-3e18) ? (-7e18)", a, b); + checkCompare("(-7e18) ? (-3e18)", b, a); + + auto lt = [](NumberPair const& l, NumberPair const& r) { + return lean_number_lt( + l.leanNum.negative, + l.leanNum.mantissa, + l.leanNum.exponent, + r.leanNum.negative, + r.leanNum.mantissa, + r.leanNum.exponent) != 0; + }; + + BEAST_EXPECT(!lt(a, b) && !(a.cppNum < b.cppNum)); // -3e18 < -7e18 is false + BEAST_EXPECT(lt(b, a) && (b.cppNum < a.cppNum)); // -7e18 < -3e18 is true + } + + void + runTests() override + { + testCompare(); + testNegativeComparison(); + } +}; + +BEAST_DEFINE_TESTSUITE(LeanNumber, formal_verification, xrpl); + +} // namespace xrpl::test diff --git a/src/test/formal_verification/numbers/helpers/NumberGenerators.h b/src/test/formal_verification/numbers/helpers/NumberGenerators.h new file mode 100644 index 00000000000..2e074e878b3 --- /dev/null +++ b/src/test/formal_verification/numbers/helpers/NumberGenerators.h @@ -0,0 +1,43 @@ +#pragma once + +#include +#include + +#include + +#include +#include + +namespace xrpl::test::formal_verification { + +struct NumberPair +{ + Number cppNum; + LeanNumber leanNum; +}; + +inline NumberPair +makeNumberPair(bool negative, uint64_t mantissa, int exponent) +{ + return { + Number{negative, mantissa, exponent, Number::Unchecked{}}, + LeanNumber{negative, mantissa, static_cast(exponent)}}; +} + +inline NumberPair +randomNumberPair(uint64_t mantMin, uint64_t mantMax, int expMin, int expMax) +{ + auto& rng = nextRng(); + std::uniform_int_distribution mantDist(mantMin, mantMax); + std::uniform_int_distribution expDist(expMin, expMax); + std::bernoulli_distribution signDist(0.5); + return makeNumberPair(signDist(rng), mantDist(rng), expDist(rng)); +} + +inline NumberPair +randomNumberPair(int expMin, int expMax) +{ + return randomNumberPair(Number::minMantissa(), Number::kMaxRep, expMin, expMax); +} + +} // namespace xrpl::test::formal_verification diff --git a/src/test/formal_verification/numbers/helpers/NumberTypes.h b/src/test/formal_verification/numbers/helpers/NumberTypes.h new file mode 100644 index 00000000000..c300fde65be --- /dev/null +++ b/src/test/formal_verification/numbers/helpers/NumberTypes.h @@ -0,0 +1,15 @@ +#pragma once + +#include + +namespace xrpl::test::formal_verification { + +// Mirrors FFINumber in xrpl-lean4/XRPL/FFI.lean. +struct LeanNumber +{ + uint8_t negative; + uint64_t mantissa; + uint64_t exponent; +}; + +} // namespace xrpl::test::formal_verification From 23a3483cc0542539661dd5f08932fa3b85fbf26a Mon Sep 17 00:00:00 2001 From: Ivan Randjelovic Date: Thu, 2 Jul 2026 14:31:12 +0200 Subject: [PATCH 2/9] Added comments and Lean 4 introduction Signed-off-by: Ivan Randjelovic --- cspell.config.yaml | 2 + external/lean4-deps/conanfile.py | 3 + external/lean4/conanfile.py | 2 + formal_verification/README.md | 157 +++++++++++++++++- formal_verification/XRPL.lean | 5 + formal_verification/XRPL/FFI/CommonFFI.lean | 1 + formal_verification/XRPL/FFI/FFI.lean | 8 + .../XRPL/FFI/Protocol/NumberFFI.lean | 3 + formal_verification/XRPL/Model/Model.lean | 4 + .../XRPL/Model/Protocol/Number.lean | 51 ++++++ .../XRPL/Properties/Properties.lean | 4 + .../Protocol/Number/Common/Constants.lean | 4 +- .../Protocol/Number/Common/ToRatLemmas.lean | 14 +- .../Number/Compare/Common/Proofs.lean | 17 +- .../Protocol/Number/Compare/Compare.lean | 3 + .../formal_verification/common/LeanSuite.h | 11 +- .../numbers/LeanNumber_test.cpp | 5 + .../numbers/helpers/NumberGenerators.h | 4 + .../numbers/helpers/NumberTypes.h | 2 +- 19 files changed, 282 insertions(+), 18 deletions(-) diff --git a/cspell.config.yaml b/cspell.config.yaml index c82c67e3993..7ea3fb0428d 100644 --- a/cspell.config.yaml +++ b/cspell.config.yaml @@ -132,6 +132,7 @@ words: - gpgcheck - gpgkey - hotwallet + - hrange - hwaddress - hwrap - ifndef @@ -244,6 +245,7 @@ words: - qbsprofile - queuable - Raphson + - rcases - rcflags - replayer - rerandomize diff --git a/external/lean4-deps/conanfile.py b/external/lean4-deps/conanfile.py index 74b3dbe0ce3..ccfcc9715b0 100644 --- a/external/lean4-deps/conanfile.py +++ b/external/lean4-deps/conanfile.py @@ -37,6 +37,7 @@ class Lean4Deps(ConanFile): settings = "os", "arch" def set_version(self): + # version follows the Lean toolchain pin if self.version is None: toolchain = Path( self.recipe_folder, "..", "..", "formal_verification", "lean-toolchain" @@ -44,6 +45,7 @@ def set_version(self): self.version = toolchain.read_text(encoding="utf-8").strip().split(":v")[1] def export_sources(self): + # The pin files are the only recipe inputs, so changing a pin makes a new package. source_dir = Path(self.recipe_folder, "..", "..", "formal_verification") for filename in ("lakefile.toml", "lake-manifest.json", "lean-toolchain"): copy(self, filename, src=source_dir, dst=self.export_sources_folder) @@ -123,6 +125,7 @@ def package(self): copy(self, ARCHIVE_NAME, src=build_dir, dst=package_dir / LIB_DIR) def package_info(self): + # Custom properties the root conanfile forwards to CMake as LEAN4_DEPS_*. package_dir = Path(self.package_folder) self.cpp_info.set_property("packages", str(package_dir / PACKAGES_DIR)) self.cpp_info.set_property("archive", str(package_dir / LIB_DIR / ARCHIVE_NAME)) diff --git a/external/lean4/conanfile.py b/external/lean4/conanfile.py index 7e3a641be4d..4f1f7df757e 100644 --- a/external/lean4/conanfile.py +++ b/external/lean4/conanfile.py @@ -37,6 +37,7 @@ def set_version(self): self.version = toolchain.read_text(encoding="utf-8").strip().split(":v")[1] def build(self): + # Downloads and unpacks the pinned release os_name, arch = str(self.settings.os), str(self.settings.arch) sha256 = _SHA256.get((os_name, arch)) if sha256 is None: @@ -64,6 +65,7 @@ def package(self): ) def package_info(self): + # Standard layout for find_package(lean4) where bin (lean, lake) goes on PATH. self.cpp_info.includedirs = ["include"] self.cpp_info.libdirs = [str(Path("lib") / "lean")] self.cpp_info.libs = ["Lake", "leanshared"] # order matters: Lake before the runtime diff --git a/formal_verification/README.md b/formal_verification/README.md index 2fd0f23c37f..7e1093900b0 100644 --- a/formal_verification/README.md +++ b/formal_verification/README.md @@ -15,7 +15,7 @@ fit together, see Nothing here is built by hand for usual use. The C++ cross-validation tests compile this model in-tree and link it into `xrpld`, gated by the -`formal_verification` option; the Lean toolchain comes from the one `lean4` +`formal_verification` option. The Lean toolchain comes from the one `lean4` Conan package, so it needs no separate Lean or elan install. ## Working on the proofs directly @@ -32,3 +32,158 @@ lake build `lake build` is the proof check: it passes only if every file elaborates with no `sorry` and standard axioms. + +## Lean 4 introduction + +Lean 4 is a functional programming language and a theorem prover. The +same compiler builds the code and checks the proofs. + +### Pure functions + +`def` defines a constant or a function. Every function is pure: no mutation, no +side effects, the result depends only on the arguments. `if` is an expression +with a value. `let` names an intermediate variable. + +```lean +def maxRep : UInt64 := 9223372036854775807 + +def Number.toRat (n : Number) : ℚ := + let sign : Int := if n.negative_ then -1 else 1 -- if returns a value + ... +``` + +`abbrev` is a transparent alias, like C++ `using`. + +### Do notation + +`do` opens a block that looks imperative: local mutation with `let mut`, `for` +loops, early `return`. It is syntax only. The compiler turns the block into the +same pure function calls, so nothing observable is mutated. + +```lean +def sumOfSquares (xs : List Nat) : Nat := Id.run do -- run the block as pure code + let mut total := 0 + for x in xs do + total := total + x * x + return total +``` + +### Numbers + +- `UInt64` wraps around, like `uint64_t`. +- `Int` and `Nat` (integers and naturals) are arbitrary precision and never + overflow. +- `ℚ` is a rational number: an exact fraction of two integers. + +The model mirrors the C++ fields with `UInt64`/`Int`. The specification +`Number.toRat` maps them into `ℚ`, where arithmetic is exact. + +### Structures + +A `structure` is a C++ struct: fields, a constructor, dot access. `deriving` +auto-generates code, here equality (`DecidableEq`) and debug printing (`Repr`). + +```lean +structure Number where + negative_ : Bool + mantissa_ : UInt64 + exponent_ : Int + deriving DecidableEq, Repr +``` + +A field can also hold a proof. An instance cannot be built without supplying +it, so every value satisfies the invariant by construction: + +```lean +structure MantissaRange where + min : UInt64 + max : UInt64 + hrange : max.toNat + 1 = 10 * min.toNat := by decide -- proof as a field +``` + +### Inductive types + +An `inductive` type lists all the ways a value can be built. A `structure` is the special case +with exactly one constructor. `Bool` itself is inductive, with constructors +`true` and `false`. Code takes values apart with `match`, and proofs do it with +case-splitting tactics like `rcases`. + +```lean +inductive Sign where + | negative + | zero + | positive +``` + +### Type classes + +A type class is a compile-time interface, close to C++ concepts. An `instance` +implements it for a concrete type, and the compiler picks the instance from the +types at the call site. That is what `deriving DecidableEq, Repr` generates +above, and it is how operators work: `a ≤ b` is notation for `LE.le a b`, +resolved from the `LE` instance of the type of `a`. + +```lean +class LE (α : Type) where -- simplified from the library + le : α → α → Prop +``` + +### Bool vs Prop + +`Bool` is a runtime value code can branch on. `Prop` is a mathematical +statement to be proven. It never executes. The symbols read: `∧` and, `∨` or, +`¬` not, `↔` if-and-only-if. + +```lean +def Number.isnormal (n : Number) : Prop := + n = Number.zero ∨ + (largeRange.min ≤ n.mantissa_ ∧ n.mantissa_ ≤ largeRange.max ∧ ...) +``` + +`isnormal` is a condition theorems assume, not code the model runs. That is why +it is a `Prop` and not a `Bool`. + +### Theorems, lemmas and proofs + +`theorem` and `lemma` mean the same thing (lemma is used for small helpers). +The statement is a `Prop`, hypotheses are named arguments, and what follows +`:=` (or `by`) is the proof. If the file compiles, the proof is correct: the +compiler is the proof checker, and there is nothing to run. + +```lean +theorem operator_lt_iff (x y : Number) + (hx : x.isNormalized) (hy : y.isNormalized) : -- given these proofs + x.operator_lt y = true ↔ x.toRat < y.toRat := -- this statement holds + operator_lt_iff_proof x y hx hy -- the proof +``` + +### Tactics + +`by` switches to tactic mode, where a proof is built step by step. The ones +used here: + +- `rw`: rewrite the goal with a known equality. +- `simp`: apply a library of simplification rules. +- `unfold`: inline a definition. +- `by_cases`, `rcases`: split into cases. +- `linarith`, `omega`, `norm_num`: close arithmetic goals. +- `decide`: evaluate a finite statement outright (fills the `by decide` fields + of `MantissaRange`). +- `calc`: chain equalities and inequalities like a paper computation. +- `sorry`: placeholder for a missing proof. It fails the build, and its absence + is what "verified" means. + +### Namespaces + +`namespace X ... end X` works like C++. Naming a definition `Number.toRat` +enables the dot call `n.toRat`, like a member function. + +### FFI + +`@[export name]` gives a function a C symbol, so the C++ tests can declare it +`extern "C"` and call it. This is the only place Lean and C++ touch. + +```lean +@[export lean_number_lt] -- exported as the C symbol "lean_number_lt" +def lean_number_lt (neg1 : UInt8) (mant1 : UInt64) (exp1 : Int64) ... +``` diff --git a/formal_verification/XRPL.lean b/formal_verification/XRPL.lean index b5da65c9425..7a1822bde83 100644 --- a/formal_verification/XRPL.lean +++ b/formal_verification/XRPL.lean @@ -1,3 +1,8 @@ +/- +Entry point of the whole Lean package: models, proofs and FFI exports. `lake build` starts +here and checks everything the three imports reach. New files never go here directly, so add +them to Model.lean, Properties.lean or FFI.lean instead. +-/ import XRPL.FFI.FFI import XRPL.Model.Model import XRPL.Properties.Properties diff --git a/formal_verification/XRPL/FFI/CommonFFI.lean b/formal_verification/XRPL/FFI/CommonFFI.lean index 8f30d8a3072..e55a490211f 100644 --- a/formal_verification/XRPL/FFI/CommonFFI.lean +++ b/formal_verification/XRPL/FFI/CommonFFI.lean @@ -5,6 +5,7 @@ namespace XRPL.FFI open XRPL.Model.Protocol +/-- Construct a `Number` from the raw fields C++ passes over the FFI. -/ def decodeNumber (neg : UInt8) (mant : UInt64) (exp : Int64) : Number := Number.unchecked (neg != 0) mant exp.toInt diff --git a/formal_verification/XRPL/FFI/FFI.lean b/formal_verification/XRPL/FFI/FFI.lean index 6f76ad94a11..dd51968985a 100644 --- a/formal_verification/XRPL/FFI/FFI.lean +++ b/formal_verification/XRPL/FFI/FFI.lean @@ -1 +1,9 @@ +/- +Root module of the FFI exports, one import per FFI file. C++ initializes exactly this module +(`initialize_XRPL_XRPL_FFI_FFI` in LeanSuite.h) and that initializes everything imported +here, so a new FFI file must be added to the imports below to be callable from C++. + +Note: this must stay a plain comment. The module docstring form (with the bang) is a +command, and commands may not precede `import`. +-/ import XRPL.FFI.Protocol.NumberFFI diff --git a/formal_verification/XRPL/FFI/Protocol/NumberFFI.lean b/formal_verification/XRPL/FFI/Protocol/NumberFFI.lean index 70a88b4f705..ce2ae674f8f 100644 --- a/formal_verification/XRPL/FFI/Protocol/NumberFFI.lean +++ b/formal_verification/XRPL/FFI/Protocol/NumberFFI.lean @@ -6,6 +6,9 @@ namespace XRPL.FFI open XRPL.Model.Protocol (Number) +/-- FFI method for `Number.operator_lt`. Each number has 3 fields: mantissa, exponent, negative +where return result is int ("1" means first number is less than second one, otherwise "0"). +The C++ tests declare this symbol `extern "C"` and call it directly. -/ @[export lean_number_lt] def lean_number_lt (neg1 : UInt8) (mant1 : UInt64) (exp1 : Int64) (neg2 : UInt8) (mant2 : UInt64) (exp2 : Int64) : UInt8 := diff --git a/formal_verification/XRPL/Model/Model.lean b/formal_verification/XRPL/Model/Model.lean index a6c5eb6ddff..040c8328249 100644 --- a/formal_verification/XRPL/Model/Model.lean +++ b/formal_verification/XRPL/Model/Model.lean @@ -1 +1,5 @@ +/- +Import every new model file here. That way the build picks it up, and the rest of the code +reaches all models through this single module. +-/ import XRPL.Model.Protocol.Number diff --git a/formal_verification/XRPL/Model/Protocol/Number.lean b/formal_verification/XRPL/Model/Protocol/Number.lean index ec4ff4c810b..5d1f905f53a 100644 --- a/formal_verification/XRPL/Model/Protocol/Number.lean +++ b/formal_verification/XRPL/Model/Protocol/Number.lean @@ -1,42 +1,78 @@ import Mathlib.Tactic +/-! +Lean model of rippled's `Number` (`include/xrpl/basics/Number.h`), a decimal floating point +type used for XRPL amount arithmetic. +-/ + set_option linter.style.nativeDecide false namespace XRPL.Model.Protocol +/-- Largest mantissa of an IOU `STAmount`, `10^16 - 1`. -/ def cMaxValue : UInt64 := 9999999999999999 +/-- Mantissa range of a normalized `Number`, mirroring the C++ `MantissaRange` where +every normalized mantissa has the same digit count. +The two proof fields make any instance a valid range by construction. -/ structure MantissaRange where min : UInt64 max : UInt64 + /-- The range spans exactly one decade. -/ hrange : max.toNat + 1 = 10 * min.toNat := by decide + /-- The range can hold the largest IOU mantissa. -/ hfit : cMaxValue.toNat ≤ max.toNat := by decide +/-- The C++ `MantissaScale::Large` range, `[10^18, 10^19 - 1]`. The model and all proofs assume this scale. -/ def largeRange : MantissaRange := { min := 1000000000000000000, max := 9999999999999999999 } + +/-- Smallest exponent of a normalized `Number` (C++ `kMinExponent`). -/ def minExponent : Int := -32768 + +/-- Largest exponent of a normalized `Number` (C++ `kMaxExponent`). -/ def maxExponent : Int := 32768 + +/-- Largest mantissa the C++ signed 64-bit rep can hold, `2^63 - 1` (C++ `kMaxRep`). -/ def maxRep : UInt64 := 9223372036854775807 +/-- Mirror of the C++ `Number`. The value it represents is `(-1)^negative_ * mantissa_ * 10^exponent_`. +Field names keep the C++ trailing underscore. -/ structure Number where negative_ : Bool mantissa_ : UInt64 exponent_ : Int deriving DecidableEq, Repr +/-- The canonical zero, what C++ `Number{}` default-constructs: positive, mantissa 0, and +the smallest `int` value as exponent. -/ def Number.zero : Number := { negative_ := false, mantissa_ := 0, exponent_ := -2147483648 } +/-- Constructs a `Number` from raw fields without normalizing, like the C++ `Unchecked` +constructor tag. This is how the FFI and the tests construct arbitrary numbers. -/ def Number.unchecked (negative : Bool) (mantissa : UInt64) (exponent : Int) : Number := { negative_ := negative, mantissa_ := mantissa, exponent_ := exponent } +/-- The C++ `isnormal()` check -/ def Number.isnormal (n : Number) : Prop := n = Number.zero ∨ (largeRange.min ≤ n.mantissa_ ∧ n.mantissa_ ≤ largeRange.max ∧ (n.mantissa_ ≤ maxRep ∨ n.mantissa_.toNat % 10 = 0) ∧ minExponent ≤ n.exponent_ ∧ n.exponent_ ≤ maxExponent) +/-- Alias of `isnormal`, the spelling used in property statements. -/ abbrev Number.isNormalized (n : Number) : Prop := n.isnormal +/-- The exact value a `Number` stands for: `sign * mantissa * 10^exponent`, as a rational. + +`ℚ` is Lean's rational number type: a fraction of two integers, always exact. +Unlike a C++ double it represents `10^exponent` exactly even for negative exponents. + +`mkRat a b` builds the fraction `a / b`. An exponent `≥ 0` scales the mantissa up into a +whole number (denominator 1). An exponent `< 0` puts `10^(-exponent)` in the denominator. +The sign flag negates the result. + +This is a proof-only specification. The C++ has no equivalent for this. -/ def Number.toRat (n : Number) : ℚ := let sign : Int := if n.negative_ then -1 else 1 let m : Int := n.mantissa_.toNat @@ -45,6 +81,21 @@ def Number.toRat (n : Number) : ℚ := else mkRat (sign * m) ((10 : Nat) ^ (-n.exponent_).toNat) +/-- The C++ `operator<(Number, Number)`. + +Lean can overload `<` just like C++ does: + +```lean +instance : LT Number where + lt l r := -- `x < y` runs the body written here + if l.negative_ != r.negative_ then l.negative_ + else ... +``` + +We use a named function instead, for two reasons. An instance is locked to exactly two +arguments, and some C++ helpers we model need more, like an asset or a rounding mode, so +named functions keep all models uniform. And the C++ name tells a C++ developer exactly +which function is being modeled. -/ def Number.operator_lt (l r : Number) : Bool := let lneg := l.negative_ let rneg := r.negative_ diff --git a/formal_verification/XRPL/Properties/Properties.lean b/formal_verification/XRPL/Properties/Properties.lean index a99af774f9d..ce045d30d33 100644 --- a/formal_verification/XRPL/Properties/Properties.lean +++ b/formal_verification/XRPL/Properties/Properties.lean @@ -1 +1,5 @@ +/- +Import every new proof file here, otherwise `lake build` will not check it. Proofs matter +only at build time, so nothing from this tree is linked into xrpld. +-/ import XRPL.Properties.Protocol.Number.Compare.Compare diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean b/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean index df00d4d90bc..ebabe81d75f 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean @@ -5,10 +5,10 @@ import XRPL.Model.Protocol.Number namespace XRPL.Model.Protocol -/-- `largeRange.min.toNat = 10^18`. -/ +/-- The lower bound of `largeRange` as a natural number: `10^18`. -/ lemma largeRange_min_val : largeRange.min.toNat = 1000000000000000000 := by decide -/-- `largeRange.max.toNat = 10^19 - 1`. -/ +/-- The upper bound of `largeRange` as a natural number: `10^19 - 1`. -/ lemma largeRange_max_val : largeRange.max.toNat = 9999999999999999999 := by decide end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean b/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean index 77c65bc4cf2..dd6b08bc823 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean @@ -5,7 +5,9 @@ import XRPL.Properties.Protocol.Number.Common.Constants namespace XRPL.Model.Protocol -/-- Extract mantissa bounds from `isNormalized` when mantissa is nonzero. -/ + +/-- A normalized number with a nonzero mantissa has its mantissa inside `largeRange`. Only +the canonical zero is exempt from the bounds. -/ lemma Number.isNormalized.mantissaBounds {n : Number} (h : n.isNormalized) (hne : n.mantissa_ ≠ 0) : largeRange.min ≤ n.mantissa_ ∧ n.mantissa_ ≤ largeRange.max := by @@ -13,7 +15,8 @@ lemma Number.isNormalized.mantissaBounds {n : Number} · exfalso; apply hne; rw [h_zero]; rfl · exact ⟨hmin, hmax⟩ -/-- `|n.toRat| = n.mantissa_.toNat * 10^n.exponent_`. -/ +/-- The magnitude of the value is `mantissa * 10^exponent`, whatever the sign flag says. +Later proofs reason about magnitudes and reattach the sign at the end. -/ lemma abs_toRat_eq (n : Number) : |n.toRat| = (n.mantissa_.toNat : ℚ) * 10 ^ n.exponent_ := by unfold Number.toRat @@ -57,7 +60,8 @@ lemma abs_toRat_eq (n : Number) : field_simp rw [h_val, abs_of_nonneg (by positivity)] -/-- `n.toRat ≤ 0` when `negative_ = true`. -/ +/-- With the negative flag set the value is at most 0. Only `≤`, since a zero mantissa +still gives value 0. -/ lemma Number.toRat_nonpos_of_negative (n : Number) (hneg : n.negative_ = true) : n.toRat ≤ 0 := by unfold Number.toRat @@ -76,7 +80,7 @@ lemma Number.toRat_nonpos_of_negative (n : Number) (hneg : n.negative_ = true) : field_simp rw [this]; linarith -/-- `0 ≤ n.toRat` when `negative_ = false`. -/ +/-- With the negative flag clear the value is at least 0. -/ lemma Number.toRat_nonneg_of_nonnegative (n : Number) (hneg : n.negative_ = false) : 0 ≤ n.toRat := by unfold Number.toRat @@ -85,7 +89,7 @@ lemma Number.toRat_nonneg_of_nonnegative (n : Number) (hneg : n.negative_ = fals · rw [Rat.mkRat_one]; push_cast; positivity · rw [Rat.mkRat_eq_div]; push_cast; positivity -/-- `n.toRat = 0` iff `n.mantissa_ = 0`. -/ +/-- The value is 0 exactly when the mantissa is 0. -/ lemma Number.toRat_eq_zero_iff {n : Number} : n.toRat = 0 ↔ n.mantissa_ = 0 := by constructor diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean index 6517c781902..9fa03c1ad7b 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean @@ -4,22 +4,24 @@ import XRPL.Properties.Protocol.Number.Signum.Common.Proofs namespace XRPL.Model.Protocol -/-- Strictly positive value: non-negative flag and nonzero mantissa. -/ +/-- A non-negative number with a nonzero mantissa has a strictly positive value. -/ lemma Number.toRat_pos_of_not_negative (n : Number) (hneg : n.negative_ = false) (hm : n.mantissa_ ≠ 0) : 0 < n.toRat := by have h1 := Number.toRat_nonneg_of_nonnegative n hneg have h2 : n.toRat ≠ 0 := fun h => hm (Number.toRat_eq_zero_iff.mp h) exact lt_of_le_of_ne h1 (Ne.symm h2) -/-- Strictly negative value: negative flag and nonzero mantissa. -/ +/-- A negative number with a nonzero mantissa has a strictly negative value. -/ lemma Number.toRat_neg_of_negative' (n : Number) (hneg : n.negative_ = true) (hm : n.mantissa_ ≠ 0) : n.toRat < 0 := by have h1 := Number.toRat_nonpos_of_negative n hneg have h2 : n.toRat ≠ 0 := fun h => hm (Number.toRat_eq_zero_iff.mp h) exact lt_of_le_of_ne h1 h2 -/-- Exponent dominance: for normalized nonzero values, a strictly smaller -exponent means a strictly smaller magnitude (`m ∈ [10^18, 10^19)` forces it). -/ +/-- Exponent dominance: between normalized nonzero values, the smaller exponent always means +the smaller magnitude. Normalization pins the mantissa inside one decade `[10^18, 10^19)`, +so no mantissa can make up for a smaller exponent. This is what lets `operator_lt` compare +exponents before mantissas. -/ lemma abs_toRat_lt_of_exp_lt (x y : Number) (hx : x.isNormalized) (hy : y.isNormalized) (hxm : x.mantissa_ ≠ 0) (hym : y.mantissa_ ≠ 0) @@ -52,7 +54,7 @@ lemma abs_toRat_lt_of_exp_lt (x y : Number) _ ≤ (y.mantissa_.toNat : ℚ) * 10 ^ y.exponent_ := mul_le_mul_of_nonneg_right hym_ge (le_of_lt hpow_y) -/-- Same exponent: magnitude order is mantissa order. -/ +/-- With equal exponents, comparing magnitudes is exactly comparing mantissas. -/ lemma abs_toRat_lt_iff_of_exp_eq (x y : Number) (hexp : x.exponent_ = y.exponent_) : |x.toRat| < |y.toRat| ↔ x.mantissa_ < y.mantissa_ := by @@ -79,8 +81,9 @@ private lemma toRat_eq_abs (n : Number) (hneg : n.negative_ = false) : n.toRat = |n.toRat| := by rw [abs_of_nonneg (Number.toRat_nonneg_of_nonnegative n hneg)] -/-- **Correctness of `operator_lt`**: on normalized values the comparison agrees -with the rational order. -/ +/-- **Correctness of `operator_lt`**: on normalized values the comparison agrees with the +order of the exact rational values. The case split retraces the C++ branches: signs differ, +one side is zero, exponents differ, exponents equal. -/ theorem operator_lt_iff_proof (x y : Number) (hx : x.isNormalized) (hy : y.isNormalized) : x.operator_lt y = true ↔ x.toRat < y.toRat := by diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean index 3b0b446f52f..25959747847 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean @@ -3,6 +3,9 @@ import XRPL.Properties.Protocol.Number.Compare.Common.Proofs namespace XRPL.Model.Protocol +/-- Top-level comparison theorem for normalized numbers. +`x.operator_lt y` is `true` exactly when the value of `x` is below the value of `y` as rationals. +In other words, the C++ comparison algorithm implements the true order on the values the numbers represent. -/ theorem operator_lt_iff (x y : Number) (hx : x.isNormalized) (hy : y.isNormalized) : x.operator_lt y = true ↔ x.toRat < y.toRat := diff --git a/src/test/formal_verification/common/LeanSuite.h b/src/test/formal_verification/common/LeanSuite.h index 3d8eb2fac2e..502512fab12 100644 --- a/src/test/formal_verification/common/LeanSuite.h +++ b/src/test/formal_verification/common/LeanSuite.h @@ -10,9 +10,12 @@ #include #include +// Generated by Lean. Starts the Lean runtime, called once. extern "C" void lean_initialize_runtime_module(void); +// Generated by Lean, one initializer per module, named initialize__. +// It first initializes every imported module, so this one root covers the whole model. extern "C" lean_object* initialize_XRPL_XRPL_FFI_FFI(uint8_t builtin, lean_object* w); @@ -26,8 +29,8 @@ nextRng() return rng; } -// Base for Lean-FFI test suites. run() guards Lean init + serializes all FFI -// calls behind a mutex (Lean's runtime is single-threaded). +// Base class for all Lean FFI test suites. Lean's runtime is single threaded, +// so run() initializes it once and holds a lock for the whole suite. class LeanSuite : public beast::unit_test::Suite { static std::mutex& @@ -37,6 +40,8 @@ class LeanSuite : public beast::unit_test::Suite return m; } + // Initializes the Lean runtime and the FFI module once per process. + // Returns false if that failed. Every suite then fails fast in run(). static bool ensureLeanInit() { @@ -57,6 +62,7 @@ class LeanSuite : public beast::unit_test::Suite return ok; } + // Test body of a derived suite. Runs with the Lean lock held. virtual void runTests() = 0; @@ -71,6 +77,7 @@ class LeanSuite : public beast::unit_test::Suite nextRng().seed(std::hash{}(name)); } + // Runs a randomized check many times. Pass/fail is recorded inside the check. template void runFuzz(int iterations, F&& check) diff --git a/src/test/formal_verification/numbers/LeanNumber_test.cpp b/src/test/formal_verification/numbers/LeanNumber_test.cpp index f0ed5308041..b6c071b035c 100644 --- a/src/test/formal_verification/numbers/LeanNumber_test.cpp +++ b/src/test/formal_verification/numbers/LeanNumber_test.cpp @@ -11,6 +11,7 @@ #include #include +// Exported by the Lean model. See formal_verification/XRPL/FFI/Protocol/NumberFFI.lean. extern "C" { uint8_t lean_number_lt(uint8_t, uint64_t, uint64_t, uint8_t, uint64_t, uint64_t); @@ -22,6 +23,7 @@ using namespace formal_verification; class LeanNumber_test : public LeanSuite { + // Formats a value like "-123e-5" for failure messages. static std::string fmtNum(bool neg, uint64_t m, int e) { @@ -190,6 +192,9 @@ class LeanNumber_test : public LeanSuite runTests() override { testCompare(); + + // Issues identified during formal verification. + // Kept here to ensure there are no regression bugs. testNegativeComparison(); } }; diff --git a/src/test/formal_verification/numbers/helpers/NumberGenerators.h b/src/test/formal_verification/numbers/helpers/NumberGenerators.h index 2e074e878b3..d1d612932b8 100644 --- a/src/test/formal_verification/numbers/helpers/NumberGenerators.h +++ b/src/test/formal_verification/numbers/helpers/NumberGenerators.h @@ -10,12 +10,14 @@ namespace xrpl::test::formal_verification { +// The real C++ Number and the Lean FFI fields wrapper. struct NumberPair { Number cppNum; LeanNumber leanNum; }; +// Construct NumberPair on both side using same args inline NumberPair makeNumberPair(bool negative, uint64_t mantissa, int exponent) { @@ -24,6 +26,7 @@ makeNumberPair(bool negative, uint64_t mantissa, int exponent) LeanNumber{negative, mantissa, static_cast(exponent)}}; } +// Construct random NumberPair (mantissa and exponent taken uniformly from the given bounds) inline NumberPair randomNumberPair(uint64_t mantMin, uint64_t mantMax, int expMin, int expMax) { @@ -34,6 +37,7 @@ randomNumberPair(uint64_t mantMin, uint64_t mantMax, int expMin, int expMax) return makeNumberPair(signDist(rng), mantDist(rng), expDist(rng)); } +// Construct random NumberPair where mantissa goes from minMantissa up to kMaxRep inline NumberPair randomNumberPair(int expMin, int expMax) { diff --git a/src/test/formal_verification/numbers/helpers/NumberTypes.h b/src/test/formal_verification/numbers/helpers/NumberTypes.h index c300fde65be..d5f5befbf6d 100644 --- a/src/test/formal_verification/numbers/helpers/NumberTypes.h +++ b/src/test/formal_verification/numbers/helpers/NumberTypes.h @@ -4,7 +4,7 @@ namespace xrpl::test::formal_verification { -// Mirrors FFINumber in xrpl-lean4/XRPL/FFI.lean. +// The Lean FFI Number with the raw fields struct LeanNumber { uint8_t negative; From c7e5faa40802ff09580c6241602bec73fa806e6e Mon Sep 17 00:00:00 2001 From: Ivan Randjelovic Date: Thu, 2 Jul 2026 16:51:12 +0200 Subject: [PATCH 3/9] Removed trailing underscores for Number fields, added c++ code examples Signed-off-by: Ivan Randjelovic --- docs/formal-verification/README.md | 8 +- formal_verification/README.md | 66 ++++++++++- .../XRPL/Model/Protocol/Number.lean | 48 ++++---- .../Protocol/Number/Common/ToRatLemmas.lean | 68 +++++------ .../Number/Compare/Common/Proofs.lean | 106 +++++++++--------- .../Protocol/Number/Signum/Common/Proofs.lean | 4 +- 6 files changed, 177 insertions(+), 123 deletions(-) diff --git a/docs/formal-verification/README.md b/docs/formal-verification/README.md index 77d44117d4e..9755b4f6eb3 100644 --- a/docs/formal-verification/README.md +++ b/docs/formal-verification/README.md @@ -122,9 +122,9 @@ inductive rounding_mode where ... structure Number where - negative_ : Bool - mantissa_ : UInt64 - exponent_ : Int + negative : Bool + mantissa : UInt64 + exponent : Int ... def Number.operator_mul (x y : Number) (mode : rounding_mode) : Except String Number := do @@ -217,7 +217,7 @@ def lean_number_build (negative : UInt8) (mantissa : UInt64) (exponent : Int64) Number.unchecked (negative != 0) mantissa exponent.toInt @[export lean_number_mantissa] -def lean_number_mantissa (n : Number) : UInt64 := n.mantissa_ +def lean_number_mantissa (n : Number) : UInt64 := n.mantissa ``` On the C++ side, `NumberFFI` wraps the handle and exposes it as a plain `Number`: diff --git a/formal_verification/README.md b/formal_verification/README.md index 7e1093900b0..ff7268bb3d5 100644 --- a/formal_verification/README.md +++ b/formal_verification/README.md @@ -36,7 +36,8 @@ lake build ## Lean 4 introduction Lean 4 is a functional programming language and a theorem prover. The -same compiler builds the code and checks the proofs. +same compiler builds the code and checks the proofs. Each Lean snippet below is +paired with the closest C++. ### Pure functions @@ -48,10 +49,16 @@ with a value. `let` names an intermediate variable. def maxRep : UInt64 := 9223372036854775807 def Number.toRat (n : Number) : ℚ := - let sign : Int := if n.negative_ then -1 else 1 -- if returns a value + let sign : Int := if n.negative then -1 else 1 -- if returns a value ... ``` +```cpp +constexpr uint64_t maxRep = 9223372036854775807; + +int const sign = n.negative_ ? -1 : 1; // like the ternary, but for any if +``` + `abbrev` is a transparent alias, like C++ `using`. ### Do notation @@ -68,6 +75,16 @@ def sumOfSquares (xs : List Nat) : Nat := Id.run do -- run the block as pure co return total ``` +```cpp +uint64_t sumOfSquares(std::vector const& xs) +{ + uint64_t total = 0; + for (auto x : xs) + total += x * x; + return total; +} +``` + ### Numbers - `UInt64` wraps around, like `uint64_t`. @@ -85,12 +102,22 @@ auto-generates code, here equality (`DecidableEq`) and debug printing (`Repr`). ```lean structure Number where - negative_ : Bool - mantissa_ : UInt64 - exponent_ : Int + negative : Bool + mantissa : UInt64 + exponent : Int deriving DecidableEq, Repr ``` +```cpp +struct Number +{ + bool negative_; + std::uint64_t mantissa_; + int exponent_; + friend bool operator==(Number const&, Number const&) = default; // ~ deriving +}; +``` + A field can also hold a proof. An instance cannot be built without supplying it, so every value satisfies the invariant by construction: @@ -115,6 +142,10 @@ inductive Sign where | positive ``` +```cpp +enum class Sign { negative, zero, positive }; +``` + ### Type classes A type class is a compile-time interface, close to C++ concepts. An `instance` @@ -128,6 +159,19 @@ class LE (α : Type) where -- simplified from the library le : α → α → Prop ``` +The closest C++ shape is a template specialized per type: + +```cpp +template +struct LE; // class LE + +template <> +struct LE // instance : LE Number +{ + static bool le(Number const& a, Number const& b); +}; +``` + ### Bool vs Prop `Bool` is a runtime value code can branch on. `Prop` is a mathematical @@ -137,7 +181,11 @@ statement to be proven. It never executes. The symbols read: `∧` and, `∨` or ```lean def Number.isnormal (n : Number) : Prop := n = Number.zero ∨ - (largeRange.min ≤ n.mantissa_ ∧ n.mantissa_ ≤ largeRange.max ∧ ...) + (largeRange.min ≤ n.mantissa ∧ n.mantissa ≤ largeRange.max ∧ ...) +``` + +```cpp +bool isnormal() const; // C++ can only check at runtime, so it returns bool ``` `isnormal` is a condition theorems assume, not code the model runs. That is why @@ -187,3 +235,9 @@ enables the dot call `n.toRat`, like a member function. @[export lean_number_lt] -- exported as the C symbol "lean_number_lt" def lean_number_lt (neg1 : UInt8) (mant1 : UInt64) (exp1 : Int64) ... ``` + +```cpp +// the matching declaration on the C++ side +extern "C" uint8_t +lean_number_lt(uint8_t, uint64_t, uint64_t, uint8_t, uint64_t, uint64_t); +``` diff --git a/formal_verification/XRPL/Model/Protocol/Number.lean b/formal_verification/XRPL/Model/Protocol/Number.lean index 5d1f905f53a..a790cbb3896 100644 --- a/formal_verification/XRPL/Model/Protocol/Number.lean +++ b/formal_verification/XRPL/Model/Protocol/Number.lean @@ -35,30 +35,30 @@ def maxExponent : Int := 32768 /-- Largest mantissa the C++ signed 64-bit rep can hold, `2^63 - 1` (C++ `kMaxRep`). -/ def maxRep : UInt64 := 9223372036854775807 -/-- Mirror of the C++ `Number`. The value it represents is `(-1)^negative_ * mantissa_ * 10^exponent_`. -Field names keep the C++ trailing underscore. -/ +/-- Mirror of the C++ `Number`. The value it represents is `(-1)^negative * mantissa * 10^exponent`. +Field names match the C++ members, without the C++ trailing underscore. -/ structure Number where - negative_ : Bool - mantissa_ : UInt64 - exponent_ : Int + negative : Bool + mantissa : UInt64 + exponent : Int deriving DecidableEq, Repr /-- The canonical zero, what C++ `Number{}` default-constructs: positive, mantissa 0, and the smallest `int` value as exponent. -/ def Number.zero : Number := - { negative_ := false, mantissa_ := 0, exponent_ := -2147483648 } + { negative := false, mantissa := 0, exponent := -2147483648 } /-- Constructs a `Number` from raw fields without normalizing, like the C++ `Unchecked` constructor tag. This is how the FFI and the tests construct arbitrary numbers. -/ def Number.unchecked (negative : Bool) (mantissa : UInt64) (exponent : Int) : Number := - { negative_ := negative, mantissa_ := mantissa, exponent_ := exponent } + { negative := negative, mantissa := mantissa, exponent := exponent } /-- The C++ `isnormal()` check -/ def Number.isnormal (n : Number) : Prop := n = Number.zero ∨ - (largeRange.min ≤ n.mantissa_ ∧ n.mantissa_ ≤ largeRange.max ∧ - (n.mantissa_ ≤ maxRep ∨ n.mantissa_.toNat % 10 = 0) ∧ - minExponent ≤ n.exponent_ ∧ n.exponent_ ≤ maxExponent) + (largeRange.min ≤ n.mantissa ∧ n.mantissa ≤ largeRange.max ∧ + (n.mantissa ≤ maxRep ∨ n.mantissa.toNat % 10 = 0) ∧ + minExponent ≤ n.exponent ∧ n.exponent ≤ maxExponent) /-- Alias of `isnormal`, the spelling used in property statements. -/ abbrev Number.isNormalized (n : Number) : Prop := n.isnormal @@ -74,12 +74,12 @@ The sign flag negates the result. This is a proof-only specification. The C++ has no equivalent for this. -/ def Number.toRat (n : Number) : ℚ := - let sign : Int := if n.negative_ then -1 else 1 - let m : Int := n.mantissa_.toNat - if n.exponent_ ≥ 0 then - mkRat (sign * m * (10 : Int) ^ n.exponent_.toNat) 1 + let sign : Int := if n.negative then -1 else 1 + let m : Int := n.mantissa.toNat + if n.exponent ≥ 0 then + mkRat (sign * m * (10 : Int) ^ n.exponent.toNat) 1 else - mkRat (sign * m) ((10 : Nat) ^ (-n.exponent_).toNat) + mkRat (sign * m) ((10 : Nat) ^ (-n.exponent).toNat) /-- The C++ `operator<(Number, Number)`. @@ -88,7 +88,7 @@ Lean can overload `<` just like C++ does: ```lean instance : LT Number where lt l r := -- `x < y` runs the body written here - if l.negative_ != r.negative_ then l.negative_ + if l.negative != r.negative then l.negative else ... ``` @@ -97,15 +97,15 @@ arguments, and some C++ helpers we model need more, like an asset or a rounding named functions keep all models uniform. And the C++ name tells a C++ developer exactly which function is being modeled. -/ def Number.operator_lt (l r : Number) : Bool := - let lneg := l.negative_ - let rneg := r.negative_ + let lneg := l.negative + let rneg := r.negative if lneg != rneg then lneg - else if l.mantissa_ == 0 then r.mantissa_ > 0 - else if r.mantissa_ == 0 then false - else if l.exponent_ > r.exponent_ then lneg - else if l.exponent_ < r.exponent_ then !lneg - else if lneg then l.mantissa_ > r.mantissa_ - else l.mantissa_ < r.mantissa_ + else if l.mantissa == 0 then r.mantissa > 0 + else if r.mantissa == 0 then false + else if l.exponent > r.exponent then lneg + else if l.exponent < r.exponent then !lneg + else if lneg then l.mantissa > r.mantissa + else l.mantissa < r.mantissa end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean b/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean index dd6b08bc823..e38115f2fa1 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean @@ -9,8 +9,8 @@ namespace XRPL.Model.Protocol /-- A normalized number with a nonzero mantissa has its mantissa inside `largeRange`. Only the canonical zero is exempt from the bounds. -/ lemma Number.isNormalized.mantissaBounds {n : Number} - (h : n.isNormalized) (hne : n.mantissa_ ≠ 0) : - largeRange.min ≤ n.mantissa_ ∧ n.mantissa_ ≤ largeRange.max := by + (h : n.isNormalized) (hne : n.mantissa ≠ 0) : + largeRange.min ≤ n.mantissa ∧ n.mantissa ≤ largeRange.max := by rcases h with h_zero | ⟨hmin, hmax, _, _, _⟩ · exfalso; apply hne; rw [h_zero]; rfl · exact ⟨hmin, hmax⟩ @@ -18,70 +18,70 @@ lemma Number.isNormalized.mantissaBounds {n : Number} /-- The magnitude of the value is `mantissa * 10^exponent`, whatever the sign flag says. Later proofs reason about magnitudes and reattach the sign at the end. -/ lemma abs_toRat_eq (n : Number) : - |n.toRat| = (n.mantissa_.toNat : ℚ) * 10 ^ n.exponent_ := by + |n.toRat| = (n.mantissa.toNat : ℚ) * 10 ^ n.exponent := by unfold Number.toRat split_ifs with hneg hexp hexp · rw [Rat.mkRat_one] - have h_to : n.exponent_ = (n.exponent_.toNat : ℤ) := (Int.toNat_of_nonneg hexp).symm - have h_neg_val : ((-1 * (n.mantissa_.toNat : Int) * (10 : Int) ^ n.exponent_.toNat : Int) : ℚ) - = -((n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_) := by + have h_to : n.exponent = (n.exponent.toNat : ℤ) := (Int.toNat_of_nonneg hexp).symm + have h_neg_val : ((-1 * (n.mantissa.toNat : Int) * (10 : Int) ^ n.exponent.toNat : Int) : ℚ) + = -((n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent) := by push_cast conv_rhs => rw [h_to]; rw [zpow_natCast] ring rw [h_neg_val, abs_neg] rw [abs_of_nonneg (by positivity)] - · have hneg_exp : n.exponent_ < 0 := not_le.mp hexp - have h_pow : (0 : ℚ) < (10 : ℚ) ^ n.exponent_ := zpow_pos (by norm_num) _ + · have hneg_exp : n.exponent < 0 := not_le.mp hexp + have h_pow : (0 : ℚ) < (10 : ℚ) ^ n.exponent := zpow_pos (by norm_num) _ rw [Rat.mkRat_eq_div] push_cast - have h_neg_exp : n.exponent_ = -((-n.exponent_).toNat : ℤ) := by - rw [Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ -n.exponent_)]; ring - have h_val : (-1 * (n.mantissa_.toNat : ℚ)) / (10 : ℚ) ^ (-n.exponent_).toNat - = -((n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_) := by + have h_neg_exp : n.exponent = -((-n.exponent).toNat : ℤ) := by + rw [Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ -n.exponent)]; ring + have h_val : (-1 * (n.mantissa.toNat : ℚ)) / (10 : ℚ) ^ (-n.exponent).toNat + = -((n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent) := by conv_rhs => rw [h_neg_exp, zpow_neg, zpow_natCast] field_simp rw [h_val, abs_neg, abs_of_nonneg (by positivity)] · rw [Rat.mkRat_one] - have h_to : n.exponent_ = (n.exponent_.toNat : ℤ) := (Int.toNat_of_nonneg hexp).symm - have h_val : ((1 * (n.mantissa_.toNat : Int) * (10 : Int) ^ n.exponent_.toNat : Int) : ℚ) - = (n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_ := by + have h_to : n.exponent = (n.exponent.toNat : ℤ) := (Int.toNat_of_nonneg hexp).symm + have h_val : ((1 * (n.mantissa.toNat : Int) * (10 : Int) ^ n.exponent.toNat : Int) : ℚ) + = (n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent := by push_cast conv_rhs => rw [h_to]; rw [zpow_natCast] ring rw [h_val, abs_of_nonneg (by positivity)] - · have hneg_exp : n.exponent_ < 0 := not_le.mp hexp + · have hneg_exp : n.exponent < 0 := not_le.mp hexp rw [Rat.mkRat_eq_div] push_cast - have h_neg_exp : n.exponent_ = -((-n.exponent_).toNat : ℤ) := by - rw [Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ -n.exponent_)]; ring - have h_val : (1 * (n.mantissa_.toNat : ℚ)) / (10 : ℚ) ^ (-n.exponent_).toNat - = (n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_ := by + have h_neg_exp : n.exponent = -((-n.exponent).toNat : ℤ) := by + rw [Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ -n.exponent)]; ring + have h_val : (1 * (n.mantissa.toNat : ℚ)) / (10 : ℚ) ^ (-n.exponent).toNat + = (n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent := by conv_rhs => rw [h_neg_exp, zpow_neg, zpow_natCast] field_simp rw [h_val, abs_of_nonneg (by positivity)] /-- With the negative flag set the value is at most 0. Only `≤`, since a zero mantissa still gives value 0. -/ -lemma Number.toRat_nonpos_of_negative (n : Number) (hneg : n.negative_ = true) : +lemma Number.toRat_nonpos_of_negative (n : Number) (hneg : n.negative = true) : n.toRat ≤ 0 := by unfold Number.toRat rw [hneg]; simp only [if_true] split_ifs with hexp · rw [Rat.mkRat_one]; push_cast - have : (0 : ℚ) ≤ (n.mantissa_.toNat : ℚ) * (10 : ℚ) ^ n.exponent_.toNat := by positivity + have : (0 : ℚ) ≤ (n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent.toNat := by positivity linarith · rw [Rat.mkRat_eq_div]; push_cast - have h_m_nn : (0 : ℚ) ≤ (n.mantissa_.toNat : ℚ) := Nat.cast_nonneg _ - have h_pow_pos : (0 : ℚ) < (10 : ℚ) ^ (-n.exponent_).toNat := by positivity - have h_frac_nn : (0 : ℚ) ≤ (n.mantissa_.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent_).toNat := + have h_m_nn : (0 : ℚ) ≤ (n.mantissa.toNat : ℚ) := Nat.cast_nonneg _ + have h_pow_pos : (0 : ℚ) < (10 : ℚ) ^ (-n.exponent).toNat := by positivity + have h_frac_nn : (0 : ℚ) ≤ (n.mantissa.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent).toNat := div_nonneg h_m_nn (le_of_lt h_pow_pos) - have : -(1 : ℚ) * (n.mantissa_.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent_).toNat - = -((n.mantissa_.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent_).toNat) := by + have : -(1 : ℚ) * (n.mantissa.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent).toNat + = -((n.mantissa.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent).toNat) := by field_simp rw [this]; linarith /-- With the negative flag clear the value is at least 0. -/ -lemma Number.toRat_nonneg_of_nonnegative (n : Number) (hneg : n.negative_ = false) : +lemma Number.toRat_nonneg_of_nonnegative (n : Number) (hneg : n.negative = false) : 0 ≤ n.toRat := by unfold Number.toRat rw [hneg]; simp only [Bool.false_eq_true, if_false] @@ -91,18 +91,18 @@ lemma Number.toRat_nonneg_of_nonnegative (n : Number) (hneg : n.negative_ = fals /-- The value is 0 exactly when the mantissa is 0. -/ lemma Number.toRat_eq_zero_iff {n : Number} : - n.toRat = 0 ↔ n.mantissa_ = 0 := by + n.toRat = 0 ↔ n.mantissa = 0 := by constructor · intro h have habs := abs_toRat_eq n rw [h, abs_zero] at habs - have h10_pos : (0 : ℚ) < 10 ^ n.exponent_ := zpow_pos (by norm_num) _ - have hm_zero : (n.mantissa_.toNat : ℚ) = 0 := by - nlinarith [Nat.cast_nonneg (α := ℚ) n.mantissa_.toNat] - have : n.mantissa_.toNat = 0 := by exact_mod_cast hm_zero + have h10_pos : (0 : ℚ) < 10 ^ n.exponent := zpow_pos (by norm_num) _ + have hm_zero : (n.mantissa.toNat : ℚ) = 0 := by + nlinarith [Nat.cast_nonneg (α := ℚ) n.mantissa.toNat] + have : n.mantissa.toNat = 0 := by exact_mod_cast hm_zero exact UInt64.ext this · intro h - have hm : n.mantissa_.toNat = 0 := by rw [h]; rfl + have hm : n.mantissa.toNat = 0 := by rw [h]; rfl unfold Number.toRat simp only [hm, Nat.cast_zero] split_ifs <;> simp diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean index 9fa03c1ad7b..ce75cdbe66a 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean @@ -5,15 +5,15 @@ import XRPL.Properties.Protocol.Number.Signum.Common.Proofs namespace XRPL.Model.Protocol /-- A non-negative number with a nonzero mantissa has a strictly positive value. -/ -lemma Number.toRat_pos_of_not_negative (n : Number) (hneg : n.negative_ = false) - (hm : n.mantissa_ ≠ 0) : 0 < n.toRat := by +lemma Number.toRat_pos_of_not_negative (n : Number) (hneg : n.negative = false) + (hm : n.mantissa ≠ 0) : 0 < n.toRat := by have h1 := Number.toRat_nonneg_of_nonnegative n hneg have h2 : n.toRat ≠ 0 := fun h => hm (Number.toRat_eq_zero_iff.mp h) exact lt_of_le_of_ne h1 (Ne.symm h2) /-- A negative number with a nonzero mantissa has a strictly negative value. -/ -lemma Number.toRat_neg_of_negative' (n : Number) (hneg : n.negative_ = true) - (hm : n.mantissa_ ≠ 0) : n.toRat < 0 := by +lemma Number.toRat_neg_of_negative' (n : Number) (hneg : n.negative = true) + (hm : n.mantissa ≠ 0) : n.toRat < 0 := by have h1 := Number.toRat_nonpos_of_negative n hneg have h2 : n.toRat ≠ 0 := fun h => hm (Number.toRat_eq_zero_iff.mp h) exact lt_of_le_of_ne h1 h2 @@ -24,60 +24,60 @@ so no mantissa can make up for a smaller exponent. This is what lets `operator_l exponents before mantissas. -/ lemma abs_toRat_lt_of_exp_lt (x y : Number) (hx : x.isNormalized) (hy : y.isNormalized) - (hxm : x.mantissa_ ≠ 0) (hym : y.mantissa_ ≠ 0) - (hexp : x.exponent_ < y.exponent_) : + (hxm : x.mantissa ≠ 0) (hym : y.mantissa ≠ 0) + (hexp : x.exponent < y.exponent) : |x.toRat| < |y.toRat| := by rw [abs_toRat_eq, abs_toRat_eq] obtain ⟨_, hxmax⟩ := hx.mantissaBounds hxm obtain ⟨hymin, _⟩ := hy.mantissaBounds hym - have hxm_le : (x.mantissa_.toNat : ℚ) ≤ 9999999999999999999 := by + have hxm_le : (x.mantissa.toNat : ℚ) ≤ 9999999999999999999 := by have := UInt64.le_iff_toNat_le.mp hxmax rw [largeRange_max_val] at this exact_mod_cast this - have hym_ge : (1000000000000000000 : ℚ) ≤ (y.mantissa_.toNat : ℚ) := by + have hym_ge : (1000000000000000000 : ℚ) ≤ (y.mantissa.toNat : ℚ) := by have := UInt64.le_iff_toNat_le.mp hymin rw [largeRange_min_val] at this exact_mod_cast this - have hpow_x : (0 : ℚ) < 10 ^ x.exponent_ := zpow_pos (by norm_num) _ - have hpow_y : (0 : ℚ) < 10 ^ y.exponent_ := zpow_pos (by norm_num) _ - calc (x.mantissa_.toNat : ℚ) * 10 ^ x.exponent_ - ≤ 9999999999999999999 * 10 ^ x.exponent_ := + have hpow_x : (0 : ℚ) < 10 ^ x.exponent := zpow_pos (by norm_num) _ + have hpow_y : (0 : ℚ) < 10 ^ y.exponent := zpow_pos (by norm_num) _ + calc (x.mantissa.toNat : ℚ) * 10 ^ x.exponent + ≤ 9999999999999999999 * 10 ^ x.exponent := mul_le_mul_of_nonneg_right hxm_le (le_of_lt hpow_x) - _ < 1000000000000000000 * 10 ^ (x.exponent_ + 1) := by + _ < 1000000000000000000 * 10 ^ (x.exponent + 1) := by rw [zpow_add_one₀ (by norm_num : (10 : ℚ) ≠ 0), - show (1000000000000000000 : ℚ) * (10 ^ x.exponent_ * 10) - = 10000000000000000000 * 10 ^ x.exponent_ from by ring] + show (1000000000000000000 : ℚ) * (10 ^ x.exponent * 10) + = 10000000000000000000 * 10 ^ x.exponent from by ring] exact mul_lt_mul_of_pos_right (by norm_num) hpow_x - _ ≤ 1000000000000000000 * 10 ^ y.exponent_ := by + _ ≤ 1000000000000000000 * 10 ^ y.exponent := by apply mul_le_mul_of_nonneg_left _ (by norm_num) exact zpow_le_zpow_right₀ (by norm_num) (by omega) - _ ≤ (y.mantissa_.toNat : ℚ) * 10 ^ y.exponent_ := + _ ≤ (y.mantissa.toNat : ℚ) * 10 ^ y.exponent := mul_le_mul_of_nonneg_right hym_ge (le_of_lt hpow_y) /-- With equal exponents, comparing magnitudes is exactly comparing mantissas. -/ lemma abs_toRat_lt_iff_of_exp_eq (x y : Number) - (hexp : x.exponent_ = y.exponent_) : - |x.toRat| < |y.toRat| ↔ x.mantissa_ < y.mantissa_ := by + (hexp : x.exponent = y.exponent) : + |x.toRat| < |y.toRat| ↔ x.mantissa < y.mantissa := by rw [abs_toRat_eq, abs_toRat_eq, hexp] - have hpow : (0 : ℚ) < 10 ^ y.exponent_ := zpow_pos (by norm_num) _ + have hpow : (0 : ℚ) < 10 ^ y.exponent := zpow_pos (by norm_num) _ constructor · intro h have := lt_of_mul_lt_mul_right h (le_of_lt hpow) rw [UInt64.lt_iff_toNat_lt] exact_mod_cast this · intro h - have h' : (x.mantissa_.toNat : ℚ) < y.mantissa_.toNat := by + have h' : (x.mantissa.toNat : ℚ) < y.mantissa.toNat := by exact_mod_cast UInt64.lt_iff_toNat_lt.mp h exact mul_lt_mul_of_pos_right h' hpow /-- The signed value of a negative `Number` is the negated magnitude. -/ -private lemma toRat_eq_neg_abs (n : Number) (hneg : n.negative_ = true) : +private lemma toRat_eq_neg_abs (n : Number) (hneg : n.negative = true) : n.toRat = -|n.toRat| := by rw [abs_of_nonpos (Number.toRat_nonpos_of_negative n hneg)] ring /-- The signed value of a non-negative `Number` is its magnitude. -/ -private lemma toRat_eq_abs (n : Number) (hneg : n.negative_ = false) : +private lemma toRat_eq_abs (n : Number) (hneg : n.negative = false) : n.toRat = |n.toRat| := by rw [abs_of_nonneg (Number.toRat_nonneg_of_nonnegative n hneg)] @@ -87,30 +87,30 @@ one side is zero, exponents differ, exponents equal. -/ theorem operator_lt_iff_proof (x y : Number) (hx : x.isNormalized) (hy : y.isNormalized) : x.operator_lt y = true ↔ x.toRat < y.toRat := by - by_cases hsx : x.negative_ = true - · by_cases hsy : y.negative_ = true + by_cases hsx : x.negative = true + · by_cases hsy : y.negative = true · -- both negative: nonzero mantissas, value = −magnitude. - have hxm : x.mantissa_ ≠ 0 := Number.mantissa_ne_zero_of_negative x hx hsx - have hym : y.mantissa_ ≠ 0 := Number.mantissa_ne_zero_of_negative y hy hsy + have hxm : x.mantissa ≠ 0 := Number.mantissa_ne_zero_of_negative x hx hsx + have hym : y.mantissa ≠ 0 := Number.mantissa_ne_zero_of_negative y hy hsy have hxs := toRat_eq_neg_abs x hsx have hys := toRat_eq_neg_abs y hsy unfold Number.operator_lt rw [hsx, hsy] simp only [bne_self_eq_false, Bool.false_eq_true, if_false] - rw [show (x.mantissa_ == 0) = false from beq_eq_false_iff_ne.mpr hxm, - show (y.mantissa_ == 0) = false from beq_eq_false_iff_ne.mpr hym] + rw [show (x.mantissa == 0) = false from beq_eq_false_iff_ne.mpr hxm, + show (y.mantissa == 0) = false from beq_eq_false_iff_ne.mpr hym] simp only [Bool.false_eq_true, if_false] - rcases lt_trichotomy x.exponent_ y.exponent_ with hexp | hexp | hexp + rcases lt_trichotomy x.exponent y.exponent with hexp | hexp | hexp · -- ex < ey: |x| < |y| so x > y; the operator returns !lneg = false. - rw [if_neg (by omega : ¬ x.exponent_ > y.exponent_), if_pos hexp, + rw [if_neg (by omega : ¬ x.exponent > y.exponent), if_pos hexp, show (!(true : Bool)) = false from rfl] simp only [Bool.false_eq_true, false_iff, not_lt] have habs := abs_toRat_lt_of_exp_lt x y hx hy hxm hym hexp rw [hxs, hys] linarith · -- ex = ey: sign-aware mantissa compare. - rw [if_neg (by omega : ¬ x.exponent_ > y.exponent_), - if_neg (by omega : ¬ x.exponent_ < y.exponent_), if_pos trivial, + rw [if_neg (by omega : ¬ x.exponent > y.exponent), + if_neg (by omega : ¬ x.exponent < y.exponent), if_pos trivial, decide_eq_true_iff] constructor · intro h @@ -130,8 +130,8 @@ theorem operator_lt_iff_proof (x y : Number) · intro _ rfl · -- x negative, y non-negative: x < y always. - have hsyf : y.negative_ = false := Bool.not_eq_true _ |>.mp hsy - have hxm : x.mantissa_ ≠ 0 := Number.mantissa_ne_zero_of_negative x hx hsx + have hsyf : y.negative = false := Bool.not_eq_true _ |>.mp hsy + have hxm : x.mantissa ≠ 0 := Number.mantissa_ne_zero_of_negative x hx hsx have heval : x.operator_lt y = true := by unfold Number.operator_lt rw [hsx, hsyf] @@ -141,10 +141,10 @@ theorem operator_lt_iff_proof (x y : Number) have h1 := Number.toRat_neg_of_negative' x hsx hxm have h2 := Number.toRat_nonneg_of_nonnegative y hsyf linarith - · have hsxf : x.negative_ = false := Bool.not_eq_true _ |>.mp hsx - by_cases hsy : y.negative_ = true + · have hsxf : x.negative = false := Bool.not_eq_true _ |>.mp hsx + by_cases hsy : y.negative = true · -- x non-negative, y negative: never x < y. - have hym : y.mantissa_ ≠ 0 := Number.mantissa_ne_zero_of_negative y hy hsy + have hym : y.mantissa ≠ 0 := Number.mantissa_ne_zero_of_negative y hy hsy have heval : x.operator_lt y = false := by unfold Number.operator_lt rw [hsxf, hsy] @@ -155,60 +155,60 @@ theorem operator_lt_iff_proof (x y : Number) have h2 := Number.toRat_neg_of_negative' y hsy hym linarith · -- both non-negative. - have hsyf : y.negative_ = false := Bool.not_eq_true _ |>.mp hsy + have hsyf : y.negative = false := Bool.not_eq_true _ |>.mp hsy have hxs := toRat_eq_abs x hsxf have hys := toRat_eq_abs y hsyf unfold Number.operator_lt rw [hsxf, hsyf] simp only [bne_self_eq_false, Bool.false_eq_true, if_false] - by_cases hxm : x.mantissa_ = 0 + by_cases hxm : x.mantissa = 0 · -- x = 0: x < y iff y is nonzero. - rw [show (x.mantissa_ == 0) = true from beq_iff_eq.mpr hxm] + rw [show (x.mantissa == 0) = true from beq_iff_eq.mpr hxm] simp only [if_true] rw [decide_eq_true_iff] have hx0 : x.toRat = 0 := Number.toRat_eq_zero_iff.mpr hxm rw [hx0] constructor · intro h - have hym : y.mantissa_ ≠ 0 := by + have hym : y.mantissa ≠ 0 := by intro hc rw [hc] at h exact absurd h (by decide) exact Number.toRat_pos_of_not_negative y hsyf hym · intro h - have hym : y.mantissa_ ≠ 0 := + have hym : y.mantissa ≠ 0 := fun hc => absurd (Number.toRat_eq_zero_iff.mpr hc) (ne_of_gt h) - change (0 : UInt64) < y.mantissa_ + change (0 : UInt64) < y.mantissa rw [UInt64.lt_iff_toNat_lt, show (0 : UInt64).toNat = 0 from rfl] - have hne : y.mantissa_.toNat ≠ 0 := by + have hne : y.mantissa.toNat ≠ 0 := by intro hc apply hym rw [← UInt64.toNat_inj, hc] rfl omega - · rw [show (x.mantissa_ == 0) = false from beq_eq_false_iff_ne.mpr hxm] + · rw [show (x.mantissa == 0) = false from beq_eq_false_iff_ne.mpr hxm] simp only [Bool.false_eq_true, if_false] - by_cases hym : y.mantissa_ = 0 + by_cases hym : y.mantissa = 0 · -- y = 0: a positive x is never below it. - rw [show (y.mantissa_ == 0) = true from beq_iff_eq.mpr hym] + rw [show (y.mantissa == 0) = true from beq_iff_eq.mpr hym] simp only [if_true] have hy0 : y.toRat = 0 := Number.toRat_eq_zero_iff.mpr hym rw [hy0] simp only [Bool.false_eq_true, false_iff, not_lt] exact le_of_lt (Number.toRat_pos_of_not_negative x hsxf hxm) - · rw [show (y.mantissa_ == 0) = false from beq_eq_false_iff_ne.mpr hym] + · rw [show (y.mantissa == 0) = false from beq_eq_false_iff_ne.mpr hym] simp only [Bool.false_eq_true, if_false] - rcases lt_trichotomy x.exponent_ y.exponent_ with hexp | hexp | hexp + rcases lt_trichotomy x.exponent y.exponent with hexp | hexp | hexp · -- ex < ey: |x| < |y| so x < y; the operator returns !lneg = true. - rw [if_neg (by omega : ¬ x.exponent_ > y.exponent_), if_pos hexp, + rw [if_neg (by omega : ¬ x.exponent > y.exponent), if_pos hexp, show (!(false : Bool)) = true from rfl] simp only [true_iff] have habs := abs_toRat_lt_of_exp_lt x y hx hy hxm hym hexp rw [hxs, hys] linarith · -- ex = ey: mantissa compare. - rw [if_neg (by omega : ¬ x.exponent_ > y.exponent_), - if_neg (by omega : ¬ x.exponent_ < y.exponent_), + rw [if_neg (by omega : ¬ x.exponent > y.exponent), + if_neg (by omega : ¬ x.exponent < y.exponent), decide_eq_true_iff] constructor · intro h diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean b/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean index 4dfb669fd8d..72dc0ffe929 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean @@ -4,10 +4,10 @@ import XRPL.Properties.Protocol.Number.Common.ToRatLemmas namespace XRPL.Model.Protocol /-- A normalized number is nonzero exactly when its mantissa is nonzero. The -only normalized value with `mantissa_ = 0` is the canonical `Number.zero` +only normalized value with `mantissa = 0` is the canonical `Number.zero` (positive), so a negative normalized number always has a nonzero mantissa. -/ lemma Number.mantissa_ne_zero_of_negative (n : Number) (hn : n.isNormalized) - (hneg : n.negative_ = true) : n.mantissa_ ≠ 0 := by + (hneg : n.negative = true) : n.mantissa ≠ 0 := by rcases hn with heq | ⟨hlo, _⟩ · rw [heq] at hneg; exact absurd hneg (by decide) · intro hm; rw [hm] at hlo; exact absurd hlo (by decide) From 995c67b34b6b6842868b302a209c337baac27b66 Mon Sep 17 00:00:00 2001 From: Ivan Randjelovic Date: Fri, 3 Jul 2026 10:54:03 +0200 Subject: [PATCH 4/9] Changes in README.md for FV Signed-off-by: Ivan Randjelovic --- formal_verification/README.md | 145 ++++++++++++++++++++-------------- 1 file changed, 85 insertions(+), 60 deletions(-) diff --git a/formal_verification/README.md b/formal_verification/README.md index ff7268bb3d5..12465b79066 100644 --- a/formal_verification/README.md +++ b/formal_verification/README.md @@ -41,31 +41,41 @@ paired with the closest C++. ### Pure functions -`def` defines a constant or a function. Every function is pure: no mutation, no -side effects, the result depends only on the arguments. `if` is an expression -with a value. `let` names an intermediate variable. +`def` defines a constant or a function. Every function is pure: it takes values +in, returns a value, and does nothing else. It cannot change its arguments or +any outside state, and the same arguments always give the same result. +The body is a single expression, so `if` yields one of two values, like the +C++ conditional operator `?:`. `let` introduces a local name for an +intermediate result, like a `const` local variable in C++, and it cannot be +reassigned. ```lean def maxRep : UInt64 := 9223372036854775807 def Number.toRat (n : Number) : ℚ := - let sign : Int := if n.negative then -1 else 1 -- if returns a value + let sign : Int := if n.negative then -1 else 1 ... ``` ```cpp constexpr uint64_t maxRep = 9223372036854775807; -int const sign = n.negative_ ? -1 : 1; // like the ternary, but for any if +double toRat(Number const& n) +{ + int const sign = n.negative_ ? -1 : 1; // the ternary mirrors Lean's if + ... +} ``` -`abbrev` is a transparent alias, like C++ `using`. +`abbrev` is an alias, like C++ `using`. ### Do notation -`do` opens a block that looks imperative: local mutation with `let mut`, `for` -loops, early `return`. It is syntax only. The compiler turns the block into the -same pure function calls, so nothing observable is mutated. +Pure code has no assignment and no loops. When an algorithm is easier to write +with them, `do` gives the C++ style back: `let mut` declares a variable that +can be updated, `for` loops over a collection, and `return` exits early. The +compiler translates the block into pure code, so nothing changes for the +caller. ```lean def sumOfSquares (xs : List Nat) : Nat := Id.run do -- run the block as pure code @@ -87,7 +97,8 @@ uint64_t sumOfSquares(std::vector const& xs) ### Numbers -- `UInt64` wraps around, like `uint64_t`. +- `UInt64` is a 64-bit unsigned integer, the same as `uint64_t`. Arithmetic + that goes past the maximum wraps around, `UInt64` max + 1 gives 0. - `Int` and `Nat` (integers and naturals) are arbitrary precision and never overflow. - `ℚ` is a rational number: an exact fraction of two integers. @@ -97,8 +108,10 @@ The model mirrors the C++ fields with `UInt64`/`Int`. The specification ### Structures -A `structure` is a C++ struct: fields, a constructor, dot access. `deriving` -auto-generates code, here equality (`DecidableEq`) and debug printing (`Repr`). +A `structure` is the Lean version of a C++ struct: named fields, a generated +constructor, and dot access like `n.mantissa`. The `deriving` line asks the +compiler to write boilerplate for the type. `DecidableEq` generates `==`, like +`operator== = default` in C++. `Repr` generates debug printing. ```lean structure Number where @@ -118,8 +131,10 @@ struct Number }; ``` -A field can also hold a proof. An instance cannot be built without supplying -it, so every value satisfies the invariant by construction: +A field can also require a proof. In the structure below, `hrange` is not +data, it is a claim about `min` and `max` that must be proven when a value is +created. A range that violates the claim does not compile, so an invalid +`MantissaRange` can never exist: ```lean structure MantissaRange where @@ -130,53 +145,77 @@ structure MantissaRange where ### Inductive types -An `inductive` type lists all the ways a value can be built. A `structure` is the special case -with exactly one constructor. `Bool` itself is inductive, with constructors -`true` and `false`. Code takes values apart with `match`, and proofs do it with -case-splitting tactics like `rcases`. +An `inductive` type declares a fixed set of options, like a C++ `enum class`. +An option can also carry data, and the type then works like `std::variant`: a +value holds exactly one of the listed options. A `structure` is the special +case with exactly one option. `Bool` itself is inductive, with constructors +`true` and `false`. `match` branches over the options, like a `switch` that +can also read the carried data. Proofs do the same case split with the tactic +`rcases`. ```lean inductive Sign where | negative | zero | positive + +def signFactor (s : Sign) : Int := + match s with + | .negative => -1 + | .zero => 0 + | .positive => 1 ``` ```cpp enum class Sign { negative, zero, positive }; + +int signFactor(Sign s) +{ + switch (s) + { + case Sign::negative: return -1; + case Sign::zero: return 0; + case Sign::positive: return 1; + } +} ``` ### Type classes -A type class is a compile-time interface, close to C++ concepts. An `instance` -implements it for a concrete type, and the compiler picks the instance from the -types at the call site. That is what `deriving DecidableEq, Repr` generates -above, and it is how operators work: `a ≤ b` is notation for `LE.le a b`, -resolved from the `LE` instance of the type of `a`. +A type class declares an operation that many types can support. An `instance` +implements it for one concrete type, like overloading a function for that type +in C++. The compiler picks the right instance from the argument types at +compile time, the same way C++ picks an overload. ```lean -class LE (α : Type) where -- simplified from the library - le : α → α → Prop +class ToText (T : Type) where + toText : T → String -- a function from T to String + +instance : ToText Sign where -- Sign can now be turned into text + toText + | .negative => "-" + | .zero => "0" + | .positive => "+" ``` -The closest C++ shape is a template specialized per type: - ```cpp -template -struct LE; // class LE - -template <> -struct LE // instance : LE Number +std::string toText(Sign s) // the "instance" for Sign { - static bool le(Number const& a, Number const& b); -}; + switch (s) + { + case Sign::negative: return "-"; + case Sign::zero: return "0"; + case Sign::positive: return "+"; + } +} ``` ### Bool vs Prop -`Bool` is a runtime value code can branch on. `Prop` is a mathematical -statement to be proven. It never executes. The symbols read: `∧` and, `∨` or, -`¬` not, `↔` if-and-only-if. +`Bool` is the ordinary `bool`: a value computed while the program runs. `Prop` +is a statement about values, like "the mantissa is within bounds". A `Prop` is +not computed but proven, once, at compile time, and it costs nothing at +runtime. The symbols read: `∧` and, `∨` or, `¬` not, `↔` if-and-only-if. ```lean def Number.isnormal (n : Number) : Prop := @@ -185,18 +224,20 @@ def Number.isnormal (n : Number) : Prop := ``` ```cpp -bool isnormal() const; // C++ can only check at runtime, so it returns bool +bool isnormal() const; // the C++ version checks one value at runtime ``` -`isnormal` is a condition theorems assume, not code the model runs. That is why -it is a `Prop` and not a `Bool`. +The model never calls its `isnormal`. Theorems take it as an assumption, "for +every normalized number ...", and stating an assumption is a job for a `Prop`, +not a `Bool`. ### Theorems, lemmas and proofs -`theorem` and `lemma` mean the same thing (lemma is used for small helpers). -The statement is a `Prop`, hypotheses are named arguments, and what follows -`:=` (or `by`) is the proof. If the file compiles, the proof is correct: the -compiler is the proof checker, and there is nothing to run. +A theorem is written like a function: the arguments are its assumptions, the +return type is the statement it claims, and the body after `:=` is the proof. +The compiler checks that the body really proves the statement, the same way it +checks that a function returns its declared type. Nothing is run. If the file +compiles, the theorem holds. `lemma` means the same, used for small helpers. ```lean theorem operator_lt_iff (x y : Number) @@ -205,22 +246,6 @@ theorem operator_lt_iff (x y : Number) operator_lt_iff_proof x y hx hy -- the proof ``` -### Tactics - -`by` switches to tactic mode, where a proof is built step by step. The ones -used here: - -- `rw`: rewrite the goal with a known equality. -- `simp`: apply a library of simplification rules. -- `unfold`: inline a definition. -- `by_cases`, `rcases`: split into cases. -- `linarith`, `omega`, `norm_num`: close arithmetic goals. -- `decide`: evaluate a finite statement outright (fills the `by decide` fields - of `MantissaRange`). -- `calc`: chain equalities and inequalities like a paper computation. -- `sorry`: placeholder for a missing proof. It fails the build, and its absence - is what "verified" means. - ### Namespaces `namespace X ... end X` works like C++. Naming a definition `Number.toRat` From 17c9f976b3221b8346920afd96827d06b6a95b46 Mon Sep 17 00:00:00 2001 From: Dejan Cabrilo Date: Thu, 9 Jul 2026 20:55:37 +0200 Subject: [PATCH 5/9] Simplify wording, introduce lean4 crash course --- docs/formal-verification/README.md | 2 +- docs/formal-verification/lean4.md | 210 ++++++++++++++++ formal_verification/README.md | 233 ------------------ .../XRPL/Model/Protocol/Number.lean | 101 +++----- .../Protocol/Number/Compare/Compare.lean | 3 +- 5 files changed, 247 insertions(+), 302 deletions(-) create mode 100644 docs/formal-verification/lean4.md diff --git a/docs/formal-verification/README.md b/docs/formal-verification/README.md index 9755b4f6eb3..8e7ec07f7e6 100644 --- a/docs/formal-verification/README.md +++ b/docs/formal-verification/README.md @@ -384,7 +384,7 @@ not where the inputs sit. Two techniques place it there: #### The operators -Each operator is tested by the shape that fits where it can break. +Each operator is tested by aiming at the targets that are likely to break it. | Operator | Test case targets | | ----------------------------- | ------------------------------------------------------------------------------------------ | diff --git a/docs/formal-verification/lean4.md b/docs/formal-verification/lean4.md new file mode 100644 index 00000000000..d60fee80383 --- /dev/null +++ b/docs/formal-verification/lean4.md @@ -0,0 +1,210 @@ +# A gentle introduction to Lean 4 + +In [README.md](README.md) we explain the need for formal verification and its benefits. +This document provides an introduction to Lean 4, the language we use to model XRPL components. + +Lean 4 is a functional programming language and a theorem prover. This means it can be used as a general-purpose programming language, but it also lets us write mathematical theorems and proofs. + +A function is defined as: `def functionName (parameters) : ReturnType := body`. For example: + +```lean +def isEven (n : UInt64) : Bool := + n % 2 == 0 +``` + +A function is called by passing arguments after the function name: + +```lean +#eval isEven 4 -- evaluates to true +#eval isEven 3 -- evaluates to false +``` + +We can now make a claim about the function we wrote: + +```lean +theorem mul_of_two_is_even (m : UInt64) : isEven (m * 2) = true := by + unfold isEven + grind +``` + +A theorem is defined as: `theorem theoremName (parameters) : Claim := proof`. The compiler checks the proof, so a theorem that compiles is a proven claim. +We now know for a fact that `isEven` returns `true` for any `UInt64` multiplied by two. + +## Data types + +Some types are easy to recognize: + +```lean +def a : UInt64 := 42 +def b : Bool := true +def s : String := "hello" +def i : Int := -5 +def n : Nat := 5 +``` + +The last one stands out: `Nat` represents a natural number, a non-negative integer. A common library used with Lean 4 is Mathlib. It provides Unicode notation for some commonly used number types: + +```lean +import Mathlib + +def a : Nat := 5 +def b : ℕ := 5 +def c : Int := -3 +def d : ℤ := -3 +def e : Rat := 3 / 2 +def f : ℚ := 3 / 2 +``` + +Compound types can be expressed as structures: + +```lean +structure Rectangle where + a : Rat + b : Rat + +def Rectangle.area (r : Rectangle) : Rat := + r.a * r.b +``` + +## Pure functions, do notation and flow control + +`def` defines a constant or a function. In Lean 4 every function is pure: it cannot produce side effects. + +Take a function like this in C++: + +```cpp +int clampScore(int x, int y) +{ + int const total = x + y; + + if (total > 100) { + return 100; + } else if (total < 10) { + return 10; + } + + return total; +} +``` + +In Lean 4, it would be rewritten as: + +```lean +def clampScore (x y : Int) : Int := + let total := x + y + + if total > 100 then + 100 + else + if total < 10 then + 10 + else + total +``` + +Regular functions cannot mutate a variable, every `if` expression has to have an `else` branch, and there are no loops, only recursion. Lean 4 provides `do` notation, which is syntactic sugar that lets us write imperative-looking code. + +```lean +def clampScore (x y : Int) : Int := Id.run do + let total := x + y + + if total > 100 then + return 100 + else if total < 10 then + return 10 + + return total +``` + +Among other things, `do` notation also supports `while` loops and mutable variables. + +## Inductive types + +An `inductive` type declares a fixed set of alternatives, like a C++ `enum class`. +(Its constructors can also carry data, which makes it closer to a `std::variant`, +but the simple form is enough here.) For example, this C++ code: +```cpp +enum class Sign { negative, zero, positive }; + +int signFactor(Sign s) +{ + switch (s) + { + case Sign::negative: return -1; + case Sign::zero: return 0; + case Sign::positive: return 1; + } +} +``` + +would be written as: + +```lean +inductive Sign where + | negative + | zero + | positive + +def signFactor (s : Sign) : Int := + match s with + | .negative => -1 + | .zero => 0 + | .positive => 1 +``` + +## Type classes + +A type class declares an operation that many types can support. An `instance` +implements it for one concrete type, like overloading a function for that type +in C++. The compiler picks the right instance from the argument types at +compile time, the same way C++ picks an overload. + +```cpp +std::string toText(Sign s) // the "instance" for Sign +{ + switch (s) + { + case Sign::negative: return "-"; + case Sign::zero: return "0"; + case Sign::positive: return "+"; + } +} +``` + +would become: + +```lean +class ToText (T : Type) where + toText : T → String -- a function from T to String + +instance : ToText Sign where -- Sign can now be turned into text + toText + | .negative => "-" + | .zero => "0" + | .positive => "+" +``` + +## FFI + +`@[export name]` gives a function a C symbol, so the C++ code can declare it +`extern "C"` and call it. + +```lean +@[export lean_number_lt] -- exported as the C symbol "lean_number_lt" +def lean_number_lt (neg1 : UInt8) (mant1 : UInt64) (exp1 : Int64) ... +``` + +```cpp +// the matching declaration on the C++ side +extern "C" uint8_t +lean_number_lt(uint8_t, uint64_t, uint64_t, uint8_t, uint64_t, uint64_t); +``` + +## Where next? + +For a crash course beyond this document, we recommend the learning platform [lean4.dev](https://lean4.dev/). + +If you care about functional programming in Lean 4, we recommend the excellent book [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) by David Thrane Christiansen. + +If you want to dabble in theorems and proofs, we recommend [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/). + diff --git a/formal_verification/README.md b/formal_verification/README.md index 12465b79066..ac2d2e1845e 100644 --- a/formal_verification/README.md +++ b/formal_verification/README.md @@ -33,236 +33,3 @@ lake build `lake build` is the proof check: it passes only if every file elaborates with no `sorry` and standard axioms. -## Lean 4 introduction - -Lean 4 is a functional programming language and a theorem prover. The -same compiler builds the code and checks the proofs. Each Lean snippet below is -paired with the closest C++. - -### Pure functions - -`def` defines a constant or a function. Every function is pure: it takes values -in, returns a value, and does nothing else. It cannot change its arguments or -any outside state, and the same arguments always give the same result. -The body is a single expression, so `if` yields one of two values, like the -C++ conditional operator `?:`. `let` introduces a local name for an -intermediate result, like a `const` local variable in C++, and it cannot be -reassigned. - -```lean -def maxRep : UInt64 := 9223372036854775807 - -def Number.toRat (n : Number) : ℚ := - let sign : Int := if n.negative then -1 else 1 - ... -``` - -```cpp -constexpr uint64_t maxRep = 9223372036854775807; - -double toRat(Number const& n) -{ - int const sign = n.negative_ ? -1 : 1; // the ternary mirrors Lean's if - ... -} -``` - -`abbrev` is an alias, like C++ `using`. - -### Do notation - -Pure code has no assignment and no loops. When an algorithm is easier to write -with them, `do` gives the C++ style back: `let mut` declares a variable that -can be updated, `for` loops over a collection, and `return` exits early. The -compiler translates the block into pure code, so nothing changes for the -caller. - -```lean -def sumOfSquares (xs : List Nat) : Nat := Id.run do -- run the block as pure code - let mut total := 0 - for x in xs do - total := total + x * x - return total -``` - -```cpp -uint64_t sumOfSquares(std::vector const& xs) -{ - uint64_t total = 0; - for (auto x : xs) - total += x * x; - return total; -} -``` - -### Numbers - -- `UInt64` is a 64-bit unsigned integer, the same as `uint64_t`. Arithmetic - that goes past the maximum wraps around, `UInt64` max + 1 gives 0. -- `Int` and `Nat` (integers and naturals) are arbitrary precision and never - overflow. -- `ℚ` is a rational number: an exact fraction of two integers. - -The model mirrors the C++ fields with `UInt64`/`Int`. The specification -`Number.toRat` maps them into `ℚ`, where arithmetic is exact. - -### Structures - -A `structure` is the Lean version of a C++ struct: named fields, a generated -constructor, and dot access like `n.mantissa`. The `deriving` line asks the -compiler to write boilerplate for the type. `DecidableEq` generates `==`, like -`operator== = default` in C++. `Repr` generates debug printing. - -```lean -structure Number where - negative : Bool - mantissa : UInt64 - exponent : Int - deriving DecidableEq, Repr -``` - -```cpp -struct Number -{ - bool negative_; - std::uint64_t mantissa_; - int exponent_; - friend bool operator==(Number const&, Number const&) = default; // ~ deriving -}; -``` - -A field can also require a proof. In the structure below, `hrange` is not -data, it is a claim about `min` and `max` that must be proven when a value is -created. A range that violates the claim does not compile, so an invalid -`MantissaRange` can never exist: - -```lean -structure MantissaRange where - min : UInt64 - max : UInt64 - hrange : max.toNat + 1 = 10 * min.toNat := by decide -- proof as a field -``` - -### Inductive types - -An `inductive` type declares a fixed set of options, like a C++ `enum class`. -An option can also carry data, and the type then works like `std::variant`: a -value holds exactly one of the listed options. A `structure` is the special -case with exactly one option. `Bool` itself is inductive, with constructors -`true` and `false`. `match` branches over the options, like a `switch` that -can also read the carried data. Proofs do the same case split with the tactic -`rcases`. - -```lean -inductive Sign where - | negative - | zero - | positive - -def signFactor (s : Sign) : Int := - match s with - | .negative => -1 - | .zero => 0 - | .positive => 1 -``` - -```cpp -enum class Sign { negative, zero, positive }; - -int signFactor(Sign s) -{ - switch (s) - { - case Sign::negative: return -1; - case Sign::zero: return 0; - case Sign::positive: return 1; - } -} -``` - -### Type classes - -A type class declares an operation that many types can support. An `instance` -implements it for one concrete type, like overloading a function for that type -in C++. The compiler picks the right instance from the argument types at -compile time, the same way C++ picks an overload. - -```lean -class ToText (T : Type) where - toText : T → String -- a function from T to String - -instance : ToText Sign where -- Sign can now be turned into text - toText - | .negative => "-" - | .zero => "0" - | .positive => "+" -``` - -```cpp -std::string toText(Sign s) // the "instance" for Sign -{ - switch (s) - { - case Sign::negative: return "-"; - case Sign::zero: return "0"; - case Sign::positive: return "+"; - } -} -``` - -### Bool vs Prop - -`Bool` is the ordinary `bool`: a value computed while the program runs. `Prop` -is a statement about values, like "the mantissa is within bounds". A `Prop` is -not computed but proven, once, at compile time, and it costs nothing at -runtime. The symbols read: `∧` and, `∨` or, `¬` not, `↔` if-and-only-if. - -```lean -def Number.isnormal (n : Number) : Prop := - n = Number.zero ∨ - (largeRange.min ≤ n.mantissa ∧ n.mantissa ≤ largeRange.max ∧ ...) -``` - -```cpp -bool isnormal() const; // the C++ version checks one value at runtime -``` - -The model never calls its `isnormal`. Theorems take it as an assumption, "for -every normalized number ...", and stating an assumption is a job for a `Prop`, -not a `Bool`. - -### Theorems, lemmas and proofs - -A theorem is written like a function: the arguments are its assumptions, the -return type is the statement it claims, and the body after `:=` is the proof. -The compiler checks that the body really proves the statement, the same way it -checks that a function returns its declared type. Nothing is run. If the file -compiles, the theorem holds. `lemma` means the same, used for small helpers. - -```lean -theorem operator_lt_iff (x y : Number) - (hx : x.isNormalized) (hy : y.isNormalized) : -- given these proofs - x.operator_lt y = true ↔ x.toRat < y.toRat := -- this statement holds - operator_lt_iff_proof x y hx hy -- the proof -``` - -### Namespaces - -`namespace X ... end X` works like C++. Naming a definition `Number.toRat` -enables the dot call `n.toRat`, like a member function. - -### FFI - -`@[export name]` gives a function a C symbol, so the C++ tests can declare it -`extern "C"` and call it. This is the only place Lean and C++ touch. - -```lean -@[export lean_number_lt] -- exported as the C symbol "lean_number_lt" -def lean_number_lt (neg1 : UInt8) (mant1 : UInt64) (exp1 : Int64) ... -``` - -```cpp -// the matching declaration on the C++ side -extern "C" uint8_t -lean_number_lt(uint8_t, uint64_t, uint64_t, uint8_t, uint64_t, uint64_t); -``` diff --git a/formal_verification/XRPL/Model/Protocol/Number.lean b/formal_verification/XRPL/Model/Protocol/Number.lean index a790cbb3896..d015afd9f17 100644 --- a/formal_verification/XRPL/Model/Protocol/Number.lean +++ b/formal_verification/XRPL/Model/Protocol/Number.lean @@ -1,20 +1,35 @@ import Mathlib.Tactic /-! -Lean model of rippled's `Number` (`include/xrpl/basics/Number.h`), a decimal floating point -type used for XRPL amount arithmetic. --/ +Lean model of xrpld's `Number`. + +For simplicity, and to demonstrate the approach, we model just one small function here: +`operator<`, along with the constants and the normalization check the proofs need. + +Names, constants, and the branching of the function bodies are kept relatively faithful +to C++ in this instance - as we wanted to make sure we capture every branch of the code. -set_option linter.style.nativeDecide false +`Number.operator_lt` is a named function, instead of Lean's overloaded `<`. We chose this +approach because for other operators (+, -, *, /), we also need the third parameter: +rounding mode. + +Constants are spelled out in full digits, never as expressions like `10^19 - 1`, because +proofs run faster without having to evaluate expressions. + +The one definition with no C++ counterpart is `toRat`, which gives the exact rational +value a `Number` represents. It exists only to state and prove properties. +-/ namespace XRPL.Model.Protocol -/-- Largest mantissa of an IOU `STAmount`, `10^16 - 1`. -/ +structure Number where + negative : Bool + mantissa : UInt64 + exponent : Int + deriving DecidableEq, Repr + def cMaxValue : UInt64 := 9999999999999999 -/-- Mantissa range of a normalized `Number`, mirroring the C++ `MantissaRange` where -every normalized mantissa has the same digit count. -The two proof fields make any instance a valid range by construction. -/ structure MantissaRange where min : UInt64 max : UInt64 @@ -23,56 +38,37 @@ structure MantissaRange where /-- The range can hold the largest IOU mantissa. -/ hfit : cMaxValue.toNat ≤ max.toNat := by decide -/-- The C++ `MantissaScale::Large` range, `[10^18, 10^19 - 1]`. The model and all proofs assume this scale. -/ +def Number.operator_lt (l r : Number) : Bool := + let lneg := l.negative + let rneg := r.negative + if lneg != rneg then lneg + else if l.mantissa == 0 then r.mantissa > 0 + else if r.mantissa == 0 then false + else if l.exponent > r.exponent then lneg + else if l.exponent < r.exponent then !lneg + else if lneg then l.mantissa > r.mantissa + else l.mantissa < r.mantissa + def largeRange : MantissaRange := { min := 1000000000000000000, max := 9999999999999999999 } -/-- Smallest exponent of a normalized `Number` (C++ `kMinExponent`). -/ def minExponent : Int := -32768 -/-- Largest exponent of a normalized `Number` (C++ `kMaxExponent`). -/ def maxExponent : Int := 32768 -/-- Largest mantissa the C++ signed 64-bit rep can hold, `2^63 - 1` (C++ `kMaxRep`). -/ def maxRep : UInt64 := 9223372036854775807 -/-- Mirror of the C++ `Number`. The value it represents is `(-1)^negative * mantissa * 10^exponent`. -Field names match the C++ members, without the C++ trailing underscore. -/ -structure Number where - negative : Bool - mantissa : UInt64 - exponent : Int - deriving DecidableEq, Repr - -/-- The canonical zero, what C++ `Number{}` default-constructs: positive, mantissa 0, and -the smallest `int` value as exponent. -/ def Number.zero : Number := { negative := false, mantissa := 0, exponent := -2147483648 } -/-- Constructs a `Number` from raw fields without normalizing, like the C++ `Unchecked` -constructor tag. This is how the FFI and the tests construct arbitrary numbers. -/ def Number.unchecked (negative : Bool) (mantissa : UInt64) (exponent : Int) : Number := { negative := negative, mantissa := mantissa, exponent := exponent } -/-- The C++ `isnormal()` check -/ -def Number.isnormal (n : Number) : Prop := +def Number.isNormalized (n : Number) : Prop := n = Number.zero ∨ (largeRange.min ≤ n.mantissa ∧ n.mantissa ≤ largeRange.max ∧ (n.mantissa ≤ maxRep ∨ n.mantissa.toNat % 10 = 0) ∧ minExponent ≤ n.exponent ∧ n.exponent ≤ maxExponent) -/-- Alias of `isnormal`, the spelling used in property statements. -/ -abbrev Number.isNormalized (n : Number) : Prop := n.isnormal - -/-- The exact value a `Number` stands for: `sign * mantissa * 10^exponent`, as a rational. - -`ℚ` is Lean's rational number type: a fraction of two integers, always exact. -Unlike a C++ double it represents `10^exponent` exactly even for negative exponents. - -`mkRat a b` builds the fraction `a / b`. An exponent `≥ 0` scales the mantissa up into a -whole number (denominator 1). An exponent `< 0` puts `10^(-exponent)` in the denominator. -The sign flag negates the result. - -This is a proof-only specification. The C++ has no equivalent for this. -/ def Number.toRat (n : Number) : ℚ := let sign : Int := if n.negative then -1 else 1 let m : Int := n.mantissa.toNat @@ -81,31 +77,4 @@ def Number.toRat (n : Number) : ℚ := else mkRat (sign * m) ((10 : Nat) ^ (-n.exponent).toNat) -/-- The C++ `operator<(Number, Number)`. - -Lean can overload `<` just like C++ does: - -```lean -instance : LT Number where - lt l r := -- `x < y` runs the body written here - if l.negative != r.negative then l.negative - else ... -``` - -We use a named function instead, for two reasons. An instance is locked to exactly two -arguments, and some C++ helpers we model need more, like an asset or a rounding mode, so -named functions keep all models uniform. And the C++ name tells a C++ developer exactly -which function is being modeled. -/ -def Number.operator_lt (l r : Number) : Bool := - let lneg := l.negative - let rneg := r.negative - if lneg != rneg then lneg - else if l.mantissa == 0 then r.mantissa > 0 - else if r.mantissa == 0 then false - else if l.exponent > r.exponent then lneg - else if l.exponent < r.exponent then !lneg - else if lneg then l.mantissa > r.mantissa - else l.mantissa < r.mantissa - - end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean index 25959747847..235f69907a4 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean @@ -4,8 +4,7 @@ import XRPL.Properties.Protocol.Number.Compare.Common.Proofs namespace XRPL.Model.Protocol /-- Top-level comparison theorem for normalized numbers. -`x.operator_lt y` is `true` exactly when the value of `x` is below the value of `y` as rationals. -In other words, the C++ comparison algorithm implements the true order on the values the numbers represent. -/ +`x.operator_lt y` is `true` exactly when the value of `x` is below the value of `y` as rationals. -/ theorem operator_lt_iff (x y : Number) (hx : x.isNormalized) (hy : y.isNormalized) : x.operator_lt y = true ↔ x.toRat < y.toRat := From 982cf92b275dc5d9680b2f48a7a0fa9d8789725e Mon Sep 17 00:00:00 2001 From: Dejan Cabrilo Date: Thu, 9 Jul 2026 21:51:45 +0200 Subject: [PATCH 6/9] Simplify proofs --- .../Protocol/Number/Common/Constants.lean | 6 + .../Protocol/Number/Common/ToRatLemmas.lean | 101 ++++++----------- .../Number/Compare/Common/Proofs.lean | 105 ++++++++---------- .../Protocol/Number/Compare/Compare.lean | 7 +- .../Protocol/Number/Signum/Common/Proofs.lean | 3 + 5 files changed, 97 insertions(+), 125 deletions(-) diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean b/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean index ebabe81d75f..833a96b5f9d 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Common/Constants.lean @@ -2,6 +2,12 @@ import Mathlib.Tactic import XRPL.Model.Protocol.Number +/-! +The `largeRange` mantissa bounds as explicit naturals. + +Kept in a leaf file of their own so that any proof file can import the +ground-truth values alone, without the lemmas built on top of them. +-/ namespace XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean b/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean index e38115f2fa1..cd021aaaa2e 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Common/ToRatLemmas.lean @@ -3,6 +3,10 @@ import Mathlib.Tactic import XRPL.Model.Protocol.Number import XRPL.Properties.Protocol.Number.Common.Constants +/-! +The base layer for reasoning about `Number.toRat`. Downstream proofs go through +these lemmas instead of unfolding `toRat` themselves. +-/ namespace XRPL.Model.Protocol @@ -15,96 +19,65 @@ lemma Number.isNormalized.mantissaBounds {n : Number} · exfalso; apply hne; rw [h_zero]; rfl · exact ⟨hmin, hmax⟩ -/-- The magnitude of the value is `mantissa * 10^exponent`, whatever the sign flag says. -Later proofs reason about magnitudes and reattach the sign at the end. -/ -lemma abs_toRat_eq (n : Number) : - |n.toRat| = (n.mantissa.toNat : ℚ) * 10 ^ n.exponent := by +/-- Closed form of `toRat`: the sign factor times `mantissa * 10^exponent`, as `ℚ`. -/ +lemma Number.toRat_eq (n : Number) : + n.toRat = (if n.negative = true then (-1 : ℚ) else 1) * (n.mantissa.toNat : ℚ) + * 10 ^ n.exponent := by unfold Number.toRat split_ifs with hneg hexp hexp · rw [Rat.mkRat_one] have h_to : n.exponent = (n.exponent.toNat : ℤ) := (Int.toNat_of_nonneg hexp).symm - have h_neg_val : ((-1 * (n.mantissa.toNat : Int) * (10 : Int) ^ n.exponent.toNat : Int) : ℚ) - = -((n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent) := by - push_cast - conv_rhs => rw [h_to]; rw [zpow_natCast] - ring - rw [h_neg_val, abs_neg] - rw [abs_of_nonneg (by positivity)] - · have hneg_exp : n.exponent < 0 := not_le.mp hexp - have h_pow : (0 : ℚ) < (10 : ℚ) ^ n.exponent := zpow_pos (by norm_num) _ - rw [Rat.mkRat_eq_div] push_cast + conv_rhs => rw [h_to, zpow_natCast] + · rw [Rat.mkRat_eq_div] have h_neg_exp : n.exponent = -((-n.exponent).toNat : ℤ) := by rw [Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ -n.exponent)]; ring - have h_val : (-1 * (n.mantissa.toNat : ℚ)) / (10 : ℚ) ^ (-n.exponent).toNat - = -((n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent) := by - conv_rhs => rw [h_neg_exp, zpow_neg, zpow_natCast] - field_simp - rw [h_val, abs_neg, abs_of_nonneg (by positivity)] + push_cast + conv_rhs => rw [h_neg_exp, zpow_neg, zpow_natCast] + rw [div_eq_mul_inv] · rw [Rat.mkRat_one] have h_to : n.exponent = (n.exponent.toNat : ℤ) := (Int.toNat_of_nonneg hexp).symm - have h_val : ((1 * (n.mantissa.toNat : Int) * (10 : Int) ^ n.exponent.toNat : Int) : ℚ) - = (n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent := by - push_cast - conv_rhs => rw [h_to]; rw [zpow_natCast] - ring - rw [h_val, abs_of_nonneg (by positivity)] - · have hneg_exp : n.exponent < 0 := not_le.mp hexp - rw [Rat.mkRat_eq_div] push_cast + conv_rhs => rw [h_to, zpow_natCast] + · rw [Rat.mkRat_eq_div] have h_neg_exp : n.exponent = -((-n.exponent).toNat : ℤ) := by rw [Int.toNat_of_nonneg (by omega : (0 : ℤ) ≤ -n.exponent)]; ring - have h_val : (1 * (n.mantissa.toNat : ℚ)) / (10 : ℚ) ^ (-n.exponent).toNat - = (n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent := by - conv_rhs => rw [h_neg_exp, zpow_neg, zpow_natCast] - field_simp - rw [h_val, abs_of_nonneg (by positivity)] + push_cast + conv_rhs => rw [h_neg_exp, zpow_neg, zpow_natCast] + rw [div_eq_mul_inv] + +/-- The magnitude of the value is `mantissa * 10^exponent`, whatever the sign flag says. +Later proofs reason about magnitudes and reattach the sign at the end. -/ +lemma abs_toRat_eq (n : Number) : + |n.toRat| = (n.mantissa.toNat : ℚ) * 10 ^ n.exponent := by + rw [Number.toRat_eq] + split_ifs + · rw [neg_one_mul, neg_mul, abs_neg, abs_of_nonneg (by positivity)] + · rw [one_mul, abs_of_nonneg (by positivity)] /-- With the negative flag set the value is at most 0. Only `≤`, since a zero mantissa still gives value 0. -/ lemma Number.toRat_nonpos_of_negative (n : Number) (hneg : n.negative = true) : n.toRat ≤ 0 := by - unfold Number.toRat - rw [hneg]; simp only [if_true] - split_ifs with hexp - · rw [Rat.mkRat_one]; push_cast - have : (0 : ℚ) ≤ (n.mantissa.toNat : ℚ) * (10 : ℚ) ^ n.exponent.toNat := by positivity - linarith - · rw [Rat.mkRat_eq_div]; push_cast - have h_m_nn : (0 : ℚ) ≤ (n.mantissa.toNat : ℚ) := Nat.cast_nonneg _ - have h_pow_pos : (0 : ℚ) < (10 : ℚ) ^ (-n.exponent).toNat := by positivity - have h_frac_nn : (0 : ℚ) ≤ (n.mantissa.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent).toNat := - div_nonneg h_m_nn (le_of_lt h_pow_pos) - have : -(1 : ℚ) * (n.mantissa.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent).toNat - = -((n.mantissa.toNat : ℚ) / (10 : ℚ) ^ (-n.exponent).toNat) := by - field_simp - rw [this]; linarith + rw [Number.toRat_eq, if_pos hneg, neg_one_mul, neg_mul] + exact neg_nonpos.mpr (by positivity) /-- With the negative flag clear the value is at least 0. -/ lemma Number.toRat_nonneg_of_nonnegative (n : Number) (hneg : n.negative = false) : 0 ≤ n.toRat := by - unfold Number.toRat - rw [hneg]; simp only [Bool.false_eq_true, if_false] - split_ifs - · rw [Rat.mkRat_one]; push_cast; positivity - · rw [Rat.mkRat_eq_div]; push_cast; positivity + rw [Number.toRat_eq, if_neg (by rw [hneg]; exact Bool.false_ne_true), one_mul] + positivity /-- The value is 0 exactly when the mantissa is 0. -/ lemma Number.toRat_eq_zero_iff {n : Number} : n.toRat = 0 ↔ n.mantissa = 0 := by + rw [← abs_eq_zero, abs_toRat_eq, mul_eq_zero] constructor + · rintro (hm | hpow) + · have hm' : n.mantissa.toNat = 0 := by exact_mod_cast hm + exact UInt64.ext hm' + · exact absurd hpow (zpow_ne_zero _ (by norm_num)) · intro h - have habs := abs_toRat_eq n - rw [h, abs_zero] at habs - have h10_pos : (0 : ℚ) < 10 ^ n.exponent := zpow_pos (by norm_num) _ - have hm_zero : (n.mantissa.toNat : ℚ) = 0 := by - nlinarith [Nat.cast_nonneg (α := ℚ) n.mantissa.toNat] - have : n.mantissa.toNat = 0 := by exact_mod_cast hm_zero - exact UInt64.ext this - · intro h - have hm : n.mantissa.toNat = 0 := by rw [h]; rfl - unfold Number.toRat - simp only [hm, Nat.cast_zero] - split_ifs <;> simp + exact Or.inl (Nat.cast_eq_zero.mpr (by rw [h]; rfl)) end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean index ce75cdbe66a..f4e8969f28b 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Common/Proofs.lean @@ -1,22 +1,36 @@ import XRPL.Properties.Protocol.Number.Common.ToRatLemmas import XRPL.Properties.Protocol.Number.Signum.Common.Proofs +/-! +The proof that `Number.operator_lt` is correct, together with the lemmas it is +built from. The headline theorem in `Compare.lean` delegates here. +-/ namespace XRPL.Model.Protocol +/-- Eliminates a `mantissa == 0` guard when the mantissa is zero. -/ +private lemma ite_mantissa_eq_zero {α : Sort*} {m : UInt64} (hm : m = 0) (a b : α) : + (if m == 0 then a else b) = a := + if_pos (beq_iff_eq.mpr hm) + +/-- Eliminates a `mantissa == 0` guard when the mantissa is nonzero. -/ +private lemma ite_mantissa_ne_zero {α : Sort*} {m : UInt64} (hm : m ≠ 0) (a b : α) : + (if m == 0 then a else b) = b := by + rw [beq_eq_false_iff_ne.mpr hm, if_neg Bool.false_ne_true] + /-- A non-negative number with a nonzero mantissa has a strictly positive value. -/ lemma Number.toRat_pos_of_not_negative (n : Number) (hneg : n.negative = false) (hm : n.mantissa ≠ 0) : 0 < n.toRat := by have h1 := Number.toRat_nonneg_of_nonnegative n hneg have h2 : n.toRat ≠ 0 := fun h => hm (Number.toRat_eq_zero_iff.mp h) - exact lt_of_le_of_ne h1 (Ne.symm h2) + exact h1.lt_of_ne' h2 /-- A negative number with a nonzero mantissa has a strictly negative value. -/ lemma Number.toRat_neg_of_negative' (n : Number) (hneg : n.negative = true) (hm : n.mantissa ≠ 0) : n.toRat < 0 := by have h1 := Number.toRat_nonpos_of_negative n hneg have h2 : n.toRat ≠ 0 := fun h => hm (Number.toRat_eq_zero_iff.mp h) - exact lt_of_le_of_ne h1 h2 + exact h1.lt_of_ne h2 /-- Exponent dominance: between normalized nonzero values, the smaller exponent always means the smaller magnitude. Normalization pins the mantissa inside one decade `[10^18, 10^19)`, @@ -42,7 +56,7 @@ lemma abs_toRat_lt_of_exp_lt (x y : Number) have hpow_y : (0 : ℚ) < 10 ^ y.exponent := zpow_pos (by norm_num) _ calc (x.mantissa.toNat : ℚ) * 10 ^ x.exponent ≤ 9999999999999999999 * 10 ^ x.exponent := - mul_le_mul_of_nonneg_right hxm_le (le_of_lt hpow_x) + mul_le_mul_of_nonneg_right hxm_le hpow_x.le _ < 1000000000000000000 * 10 ^ (x.exponent + 1) := by rw [zpow_add_one₀ (by norm_num : (10 : ℚ) ≠ 0), show (1000000000000000000 : ℚ) * (10 ^ x.exponent * 10) @@ -52,7 +66,7 @@ lemma abs_toRat_lt_of_exp_lt (x y : Number) apply mul_le_mul_of_nonneg_left _ (by norm_num) exact zpow_le_zpow_right₀ (by norm_num) (by omega) _ ≤ (y.mantissa.toNat : ℚ) * 10 ^ y.exponent := - mul_le_mul_of_nonneg_right hym_ge (le_of_lt hpow_y) + mul_le_mul_of_nonneg_right hym_ge hpow_y.le /-- With equal exponents, comparing magnitudes is exactly comparing mantissas. -/ lemma abs_toRat_lt_iff_of_exp_eq (x y : Number) @@ -60,15 +74,8 @@ lemma abs_toRat_lt_iff_of_exp_eq (x y : Number) |x.toRat| < |y.toRat| ↔ x.mantissa < y.mantissa := by rw [abs_toRat_eq, abs_toRat_eq, hexp] have hpow : (0 : ℚ) < 10 ^ y.exponent := zpow_pos (by norm_num) _ - constructor - · intro h - have := lt_of_mul_lt_mul_right h (le_of_lt hpow) - rw [UInt64.lt_iff_toNat_lt] - exact_mod_cast this - · intro h - have h' : (x.mantissa.toNat : ℚ) < y.mantissa.toNat := by - exact_mod_cast UInt64.lt_iff_toNat_lt.mp h - exact mul_lt_mul_of_pos_right h' hpow + rw [mul_lt_mul_iff_of_pos_right hpow, Nat.cast_lt] + exact UInt64.lt_iff_toNat_lt.symm /-- The signed value of a negative `Number` is the negated magnitude. -/ private lemma toRat_eq_neg_abs (n : Number) (hneg : n.negative = true) : @@ -81,9 +88,21 @@ private lemma toRat_eq_abs (n : Number) (hneg : n.negative = false) : n.toRat = |n.toRat| := by rw [abs_of_nonneg (Number.toRat_nonneg_of_nonnegative n hneg)] +/-- Between negative numbers, the smaller magnitude is the larger value. -/ +private lemma toRat_lt_of_abs_lt_of_neg {x y : Number} (hx : x.negative = true) + (hy : y.negative = true) (h : |y.toRat| < |x.toRat|) : x.toRat < y.toRat := by + rw [toRat_eq_neg_abs x hx, toRat_eq_neg_abs y hy] + exact neg_lt_neg h + +/-- Between non-negative numbers, the smaller magnitude is the smaller value. -/ +private lemma toRat_lt_of_abs_lt_of_nonneg {x y : Number} (hx : x.negative = false) + (hy : y.negative = false) (h : |x.toRat| < |y.toRat|) : x.toRat < y.toRat := by + rw [toRat_eq_abs x hx, toRat_eq_abs y hy] + exact h + /-- **Correctness of `operator_lt`**: on normalized values the comparison agrees with the -order of the exact rational values. The case split retraces the C++ branches: signs differ, -one side is zero, exponents differ, exponents equal. -/ +order of the exact rational values. The case split retraces the branches of `operator_lt`: +signs differ, one side is zero, exponents differ, exponents equal. -/ theorem operator_lt_iff_proof (x y : Number) (hx : x.isNormalized) (hy : y.isNormalized) : x.operator_lt y = true ↔ x.toRat < y.toRat := by @@ -97,36 +116,25 @@ theorem operator_lt_iff_proof (x y : Number) unfold Number.operator_lt rw [hsx, hsy] simp only [bne_self_eq_false, Bool.false_eq_true, if_false] - rw [show (x.mantissa == 0) = false from beq_eq_false_iff_ne.mpr hxm, - show (y.mantissa == 0) = false from beq_eq_false_iff_ne.mpr hym] - simp only [Bool.false_eq_true, if_false] + rw [ite_mantissa_ne_zero hxm, ite_mantissa_ne_zero hym] rcases lt_trichotomy x.exponent y.exponent with hexp | hexp | hexp · -- ex < ey: |x| < |y| so x > y; the operator returns !lneg = false. rw [if_neg (by omega : ¬ x.exponent > y.exponent), if_pos hexp, show (!(true : Bool)) = false from rfl] simp only [Bool.false_eq_true, false_iff, not_lt] have habs := abs_toRat_lt_of_exp_lt x y hx hy hxm hym hexp - rw [hxs, hys] - linarith + exact (toRat_lt_of_abs_lt_of_neg hsy hsx habs).le · -- ex = ey: sign-aware mantissa compare. rw [if_neg (by omega : ¬ x.exponent > y.exponent), if_neg (by omega : ¬ x.exponent < y.exponent), if_pos trivial, decide_eq_true_iff] - constructor - · intro h - have habs := (abs_toRat_lt_iff_of_exp_eq y x hexp.symm).mpr h - rw [hxs, hys] - linarith - · intro h - rw [hxs, hys] at h - exact (abs_toRat_lt_iff_of_exp_eq y x hexp.symm).mp (by linarith) + rw [hxs, hys, neg_lt_neg_iff, abs_toRat_lt_iff_of_exp_eq y x hexp.symm] · -- ex > ey: |x| > |y| so x < y; the operator returns lneg = true. rw [if_pos hexp] constructor · intro _ have habs := abs_toRat_lt_of_exp_lt y x hy hx hym hxm hexp - rw [hxs, hys] - linarith + exact toRat_lt_of_abs_lt_of_neg hsx hsy habs · intro _ rfl · -- x negative, y non-negative: x < y always. @@ -163,9 +171,7 @@ theorem operator_lt_iff_proof (x y : Number) simp only [bne_self_eq_false, Bool.false_eq_true, if_false] by_cases hxm : x.mantissa = 0 · -- x = 0: x < y iff y is nonzero. - rw [show (x.mantissa == 0) = true from beq_iff_eq.mpr hxm] - simp only [if_true] - rw [decide_eq_true_iff] + rw [ite_mantissa_eq_zero hxm, decide_eq_true_iff] have hx0 : x.toRat = 0 := Number.toRat_eq_zero_iff.mpr hxm rw [hx0] constructor @@ -178,52 +184,33 @@ theorem operator_lt_iff_proof (x y : Number) · intro h have hym : y.mantissa ≠ 0 := fun hc => absurd (Number.toRat_eq_zero_iff.mpr hc) (ne_of_gt h) - change (0 : UInt64) < y.mantissa - rw [UInt64.lt_iff_toNat_lt, show (0 : UInt64).toNat = 0 from rfl] - have hne : y.mantissa.toNat ≠ 0 := by - intro hc - apply hym - rw [← UInt64.toNat_inj, hc] - rfl - omega - · rw [show (x.mantissa == 0) = false from beq_eq_false_iff_ne.mpr hxm] - simp only [Bool.false_eq_true, if_false] + exact UInt64.pos_iff_ne_zero.mpr hym + · rw [ite_mantissa_ne_zero hxm] by_cases hym : y.mantissa = 0 · -- y = 0: a positive x is never below it. - rw [show (y.mantissa == 0) = true from beq_iff_eq.mpr hym] - simp only [if_true] + rw [ite_mantissa_eq_zero hym] have hy0 : y.toRat = 0 := Number.toRat_eq_zero_iff.mpr hym rw [hy0] simp only [Bool.false_eq_true, false_iff, not_lt] exact le_of_lt (Number.toRat_pos_of_not_negative x hsxf hxm) - · rw [show (y.mantissa == 0) = false from beq_eq_false_iff_ne.mpr hym] - simp only [Bool.false_eq_true, if_false] + · rw [ite_mantissa_ne_zero hym] rcases lt_trichotomy x.exponent y.exponent with hexp | hexp | hexp · -- ex < ey: |x| < |y| so x < y; the operator returns !lneg = true. rw [if_neg (by omega : ¬ x.exponent > y.exponent), if_pos hexp, show (!(false : Bool)) = true from rfl] simp only [true_iff] have habs := abs_toRat_lt_of_exp_lt x y hx hy hxm hym hexp - rw [hxs, hys] - linarith + exact toRat_lt_of_abs_lt_of_nonneg hsxf hsyf habs · -- ex = ey: mantissa compare. rw [if_neg (by omega : ¬ x.exponent > y.exponent), if_neg (by omega : ¬ x.exponent < y.exponent), decide_eq_true_iff] - constructor - · intro h - have habs := (abs_toRat_lt_iff_of_exp_eq x y hexp).mpr h - rw [hxs, hys] - linarith - · intro h - rw [hxs, hys] at h - exact (abs_toRat_lt_iff_of_exp_eq x y hexp).mp (by linarith) + rw [hxs, hys, abs_toRat_lt_iff_of_exp_eq x y hexp] · -- ex > ey: |x| > |y| so never x < y; the operator returns lneg = false. rw [if_pos hexp] simp only [Bool.false_eq_true, false_iff, not_lt] have habs := abs_toRat_lt_of_exp_lt y x hy hx hym hxm hexp - rw [hxs, hys] - linarith + exact (toRat_lt_of_abs_lt_of_nonneg hsyf hsxf habs).le end XRPL.Model.Protocol diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean index 235f69907a4..b7aea11f8a6 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean @@ -3,8 +3,11 @@ import XRPL.Properties.Protocol.Number.Compare.Common.Proofs namespace XRPL.Model.Protocol -/-- Top-level comparison theorem for normalized numbers. -`x.operator_lt y` is `true` exactly when the value of `x` is below the value of `y` as rationals. -/ +/-- `x.operator_lt y` is `true` if and only if the rational value of `x` is below the rational value of `y` + +We hide the actual proof in a helper file (Common/Proofs.lean), +so readers of this file can focus on theorems and not tactics and proofs. +-/ theorem operator_lt_iff (x y : Number) (hx : x.isNormalized) (hy : y.isNormalized) : x.operator_lt y = true ↔ x.toRat < y.toRat := diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean b/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean index 72dc0ffe929..0232f013f40 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Signum/Common/Proofs.lean @@ -1,5 +1,8 @@ import XRPL.Properties.Protocol.Number.Common.ToRatLemmas +/-! +What normalization implies about the sign flag and the mantissa. +-/ namespace XRPL.Model.Protocol From 4de336568aeae3d79432ef6c3c1715d4de29d2c9 Mon Sep 17 00:00:00 2001 From: Dejan Cabrilo Date: Thu, 9 Jul 2026 21:53:38 +0200 Subject: [PATCH 7/9] Fix style doc-strings should start with a single space or newline --- .../XRPL/Properties/Protocol/Number/Compare/Compare.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean index b7aea11f8a6..3662f501c48 100644 --- a/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean +++ b/formal_verification/XRPL/Properties/Protocol/Number/Compare/Compare.lean @@ -3,9 +3,9 @@ import XRPL.Properties.Protocol.Number.Compare.Common.Proofs namespace XRPL.Model.Protocol -/-- `x.operator_lt y` is `true` if and only if the rational value of `x` is below the rational value of `y` +/-- `x.operator_lt y` is `true` if and only if the rational value of `x` is below the rational value of `y`. -We hide the actual proof in a helper file (Common/Proofs.lean), +We hide the actual proof in a helper file (Common/Proofs.lean), so readers of this file can focus on theorems and not tactics and proofs. -/ theorem operator_lt_iff (x y : Number) From fef42c3008ad042c87e78aa48d64cdf2df03827d Mon Sep 17 00:00:00 2001 From: Dejan Cabrilo Date: Fri, 10 Jul 2026 08:47:18 +0200 Subject: [PATCH 8/9] Remove unused word --- cspell.config.yaml | 1 - 1 file changed, 1 deletion(-) diff --git a/cspell.config.yaml b/cspell.config.yaml index 7ea3fb0428d..db4926648dc 100644 --- a/cspell.config.yaml +++ b/cspell.config.yaml @@ -245,7 +245,6 @@ words: - qbsprofile - queuable - Raphson - - rcases - rcflags - replayer - rerandomize From db7f0f81cf7b22a40f79b3884af1721c082675ce Mon Sep 17 00:00:00 2001 From: Ivan Randjelovic Date: Fri, 10 Jul 2026 16:39:20 +0200 Subject: [PATCH 9/9] Minor style changes Signed-off-by: Ivan Randjelovic --- cspell.config.yaml | 1 + docs/formal-verification/README.md | 65 +++++++++++++------ docs/formal-verification/lean4.md | 4 +- formal_verification/README.md | 4 +- .../XRPL/Model/Protocol/Number.lean | 4 +- 5 files changed, 52 insertions(+), 26 deletions(-) diff --git a/cspell.config.yaml b/cspell.config.yaml index db4926648dc..29296052e15 100644 --- a/cspell.config.yaml +++ b/cspell.config.yaml @@ -304,6 +304,7 @@ words: - takergets - takerpays - ters + - Thrane - TMEndpointv2 - trixie - tx diff --git a/docs/formal-verification/README.md b/docs/formal-verification/README.md index 8e7ec07f7e6..a506170536c 100644 --- a/docs/formal-verification/README.md +++ b/docs/formal-verification/README.md @@ -36,10 +36,13 @@ us the model faithfully represents the C++. ## Overview - Lean4 models are in `formal_verification/XRPL/Model` under the root directory. -- C++ has unit tests in `src/test/formal_verification/` that compare Lean4 vs C++ implementation. +- C++ has unit tests in `src/test/formal_verification/` that compare Lean4 vs + C++ implementation. - For these test to work, Lean4 needs to expose its functions to C++. -- Lean4 is capable of compiling to C via FFI exports, which can then be called from C++. These exports are defined in `formal_verification/XRPL/FFI`. -- C++ side also needs FFI wrappers to abstract any complexities or memory management away from C++ developers. +- Lean4 is capable of compiling to C via FFI exports, which can then be called + from C++. These exports are defined in `formal_verification/XRPL/FFI`. +- C++ side also needs FFI wrappers to abstract any complexities or memory + management away from C++ developers. ```mermaid flowchart TD @@ -68,8 +71,12 @@ There are two use-cases of Lean4 models: As part of day-to-day development cycle, it is important that: -1. Theorems always compile in Lean4 (in Lean4, "it compiles" means "its verified"). For regular workflow of most developers, this can be left to CI/CD. -2. Cross-verification unit tests always pass (it means Lean4 models have not drifted from C++). This affects developers working on formally verified code or formal verification itself. +1. Theorems always compile in Lean4 (in Lean4, "it compiles" means "its + verified"). For regular workflow of most developers, this can be left to + CI/CD. +2. Cross-verification unit tests always pass (it means Lean4 models have not + drifted from C++). This affects developers working on formally verified code + or formal verification itself. Integration is done as following: @@ -114,7 +121,8 @@ cmake/XrplLean4.cmake Links the Lean4 libraries into xrpld ## The Lean4 model: translating C++ into code suitable for theorems and proofs -A model is a translation of the C++ code. For example, Number class data structure will look like: +A model is a translation of the C++ code. For example, Number class data +structure will look like: ```lean inductive rounding_mode where @@ -150,14 +158,16 @@ with no `sorry` and only standard axioms, the proofs are sound. Lean4 compiles to C, so each `@[export]` function is a C symbol that C++ can call. -Lean4 values live as heap-allocated `lean_object*` pointers in the C ABI, and C++ works with them through those handles. +Lean4 values live as heap-allocated `lean_object*` pointers in the C ABI, and +C++ works with them through those handles. Before any export can be called, the Lean4 runtime and the module's initializers must run. The base suite does this exactly once, behind a `std::once_flag`, and serializes all Lean4 calls behind a mutex because the Lean4 runtime is single-threaded. This is handled in `src/test/formal_verification/common/LeanSuite.h` -Note that we only compile and initialize the model, so that the tests are buildable and runnable even while the proofs are a work in progress. +Note that we only compile and initialize the model, so that the tests are +buildable and runnable even while the proofs are a work in progress. ### Memory management is hidden in a base class @@ -184,7 +194,8 @@ surrender it, and never calls `lean_inc` / `lean_dec` itself. A typed wrapper builds on this so a test sees only ordinary C++ values, which is what `NumberFFI::build` / `read` above do. -An operation's result structure isn't kept as a handle. A RAII guard `LeanObjOwner` frees it when the fields have been copied out: +An operation's result structure isn't kept as a handle. A RAII guard +`LeanObjOwner` frees it when the fields have been copied out: ```cpp struct LeanNumberResult : LeanNumber @@ -234,9 +245,11 @@ public: #### Running a function -A function export takes the operands' fields, calls the matching model function, and returns the result as a Lean4 structure. +A function export takes the operands' fields, calls the matching model +function, and returns the result as a Lean4 structure. -For example, `lean_number_mul` decodes its arguments into `Number` values, calls `Number.operator_mul`, and encodes the outcome: +For example, `lean_number_mul` decodes its arguments into `Number` values, +calls `Number.operator_mul`, and encodes the outcome: ```lean structure FFINumberResult where @@ -267,7 +280,9 @@ The returned structure is a `lean_object*`. ## The build process -The Lean4 side is heavy: it depends on `mathlib`, which contains thousands of files that are slow to compile. The strategy is to compile it **once** and keep it warm. +The Lean4 side is heavy: it depends on `mathlib`, which contains thousands of +files that are slow to compile. The strategy is to compile it **once** and keep +it warm. Our model is built **in-tree** by CMake when `formal_verification=ON`, while mathlib's native objects come prebuilt from the `lean4-deps` Conan package. @@ -277,7 +292,8 @@ what changed. ### Compile mathlib once, keep edits incremental -`lake exe cache get` downloads mathlib's _elaboration_ artifacts (`.olean`), so the objects are compiled locally. +`lake exe cache get` downloads mathlib's _elaboration_ artifacts (`.olean`), so +the objects are compiled locally. On first build, `lean4-deps` compiles mathlib's modules and caches them for reuse later. @@ -291,14 +307,18 @@ Two properties keep compilation after edit fast: We link the objects into a **shared** library, passing the ~8,000 object paths in a file instead of on the command line. -8,000 paths on one command line overflow the OS limit (`ARG_MAX`), which is why both `ar` and lake's own `:shared` facet fails on mathlib, so CMake links them itself. +8,000 paths on one command line overflow the OS limit (`ARG_MAX`), which is why +both `ar` and lake's own `:shared` facet fails on mathlib, so CMake links them +itself. The Lean4 build writes its artifacts into `formal_verification/.lake/` (gitignored). Building `xrpld` needs no separate Lean4 toolchain installed, Conan provides it. ### Wiring into xrpld -`formal_verification` is a Conan option (declared in `conanfile.py`) mirrored into a CMake option of the same name (declared in `cmake/XrplSettings.cmake`). Default is **OFF**, so a normal `xrpld` build is unaffected. +`formal_verification` is a Conan option (declared in `conanfile.py`) mirrored +into a CMake option of the same name (declared in `cmake/XrplSettings.cmake`). +Default is **OFF**, so a normal `xrpld` build is unaffected. When the option is on, a single `cmake --build .` builds the Lean4 library first, then links `xrpld` against it. @@ -336,7 +356,8 @@ cmake --build . --parallel N into the graph, and the matching `-Dformal_verification=ON` tells CMake to build and link the Lean4 side. -`--lockfile-partial` lets Conan add `lean4` and `lean4-deps`, which are opt-in and not pinned in `conan.lock`. +`--lockfile-partial` lets Conan add `lean4` and `lean4-deps`, which are opt-in +and not pinned in `conan.lock`. ## Testing Principles @@ -346,7 +367,9 @@ and link the Lean4 side. model. Each case runs the operation in both implementations and asserts they agree (`checkResult`). -The suite involves targeted fuzzing. Inputs are chosen to push the **result** onto those boundaries, to trigger coverage of every edge case, with a random pass to cover usual inputs as a backstop. +The suite involves targeted fuzzing. Inputs are chosen to push the **result** +onto those boundaries, to trigger coverage of every edge case, with a random +pass to cover usual inputs as a backstop. A `Number` is `mantissa × 10^exponent`, sign-magnitude, normalized into a fixed mantissa range. @@ -361,10 +384,12 @@ The backstop draws operands from `randomOperand`, which returns a boundary value about a third of the time and a uniform interior value otherwise, so random _pairs_ also mix a boundary operand with an interior one. -Its exponent range is `[STAmount::kMinOffset, kMaxOffset]` = `[-96, 80]`, the range real amounts occupy, since `Number` backs `STAmount`. +Its exponent range is `[STAmount::kMinOffset, kMaxOffset]` = `[-96, 80]`, the +range real amounts occupy, since `Number` backs `STAmount`. -Widening it to the full exponent range was measured to catch **fewer** bugs (random pairs land so far apart that additions stop cancelling); the extremes are -covered by the deterministic sweeps instead. +Widening it to the full exponent range was measured to catch **fewer** bugs +(random pairs land so far apart that additions stop cancelling); the extremes +are covered by the deterministic sweeps instead. #### Landing a result on a boundary diff --git a/docs/formal-verification/lean4.md b/docs/formal-verification/lean4.md index d60fee80383..f761d1fb17c 100644 --- a/docs/formal-verification/lean4.md +++ b/docs/formal-verification/lean4.md @@ -123,6 +123,7 @@ Among other things, `do` notation also supports `while` loops and mutable variab An `inductive` type declares a fixed set of alternatives, like a C++ `enum class`. (Its constructors can also carry data, which makes it closer to a `std::variant`, but the simple form is enough here.) For example, this C++ code: + ```cpp enum class Sign { negative, zero, positive }; @@ -187,7 +188,7 @@ instance : ToText Sign where -- Sign can now be turned into text ## FFI `@[export name]` gives a function a C symbol, so the C++ code can declare it -`extern "C"` and call it. +`extern "C"` and call it. ```lean @[export lean_number_lt] -- exported as the C symbol "lean_number_lt" @@ -207,4 +208,3 @@ For a crash course beyond this document, we recommend the learning platform [lea If you care about functional programming in Lean 4, we recommend the excellent book [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) by David Thrane Christiansen. If you want to dabble in theorems and proofs, we recommend [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/). - diff --git a/formal_verification/README.md b/formal_verification/README.md index ac2d2e1845e..d507719bb17 100644 --- a/formal_verification/README.md +++ b/formal_verification/README.md @@ -20,7 +20,8 @@ Conan package, so it needs no separate Lean or elan install. ## Working on the proofs directly -Only needed when editing the Lean model or proofs by hand. You can use lake binary in `.conan2` directory or install your own. +Only needed when editing the Lean model or proofs by hand. +You can use lake binary in `.conan2` directory or install your own. That requires [elan](https://github.com/leanprover/elan) (it provides the Lean version pinned in `lean-toolchain`): @@ -32,4 +33,3 @@ lake build `lake build` is the proof check: it passes only if every file elaborates with no `sorry` and standard axioms. - diff --git a/formal_verification/XRPL/Model/Protocol/Number.lean b/formal_verification/XRPL/Model/Protocol/Number.lean index d015afd9f17..aab20a6f029 100644 --- a/formal_verification/XRPL/Model/Protocol/Number.lean +++ b/formal_verification/XRPL/Model/Protocol/Number.lean @@ -6,11 +6,11 @@ Lean model of xrpld's `Number`. For simplicity, and to demonstrate the approach, we model just one small function here: `operator<`, along with the constants and the normalization check the proofs need. -Names, constants, and the branching of the function bodies are kept relatively faithful +Names, constants, and the branching of the function bodies are kept relatively faithful to C++ in this instance - as we wanted to make sure we capture every branch of the code. `Number.operator_lt` is a named function, instead of Lean's overloaded `<`. We chose this -approach because for other operators (+, -, *, /), we also need the third parameter: +approach because for other operators (+, -, *, /), we also need the third parameter: rounding mode. Constants are spelled out in full digits, never as expressions like `10^19 - 1`, because