feat: formalize slot_is_justifiable_after in Lean4#269
feat: formalize slot_is_justifiable_after in Lean4#269MegaRedHand wants to merge 19 commits intomainfrom
slot_is_justifiable_after in Lean4#269Conversation
🤖 Kimi Code ReviewThis PR integrates formally verified Lean4 code for the 3SF-mini justifiability check via FFI. The implementation is mathematically sound and the Rust integration follows safe patterns, though there are minor build system and documentation improvements needed. Critical/Security FindingsNone. The consensus logic is mathematically proven (zero axioms/sorrys in the proof tree) and the FFI boundary uses scalar types ( Code Correctness & Safety
Build System & Maintenance
Rust Best Practices
TestingThe unit tests in
Recommendations
Automated review by Kimi (Moonshot AI) · kimi-k2.5 · custom prompt |
🤖 Claude Code ReviewNow I have enough context. Let me compile the review. PR Review:
|
| Item | Severity |
|---|---|
justifiable overflow for delta >= 2^62 (no guard in Rust layer) |
Medium — correctness gap vs. documented proof precondition |
Stale formal/ffi/LeanFFI/Justifiability.lean path in doc |
Low |
Missing rerun-if-changed for EthLambda.lean and config files |
Low — causes stale incremental builds |
lake build failure gives no stderr |
Low — DX issue |
gmp static linking may fail on some Linux distros |
Low — portability |
| No equivalence test between Lean and Rust implementations | Low — regression safety |
Linter suppression in Bridge.lean |
Nit |
Automated review by Claude (Anthropic) · sonnet · custom prompt
🤖 Codex Code Review
I could not run a full Automated review by OpenAI Codex · gpt-5.4 · custom prompt |
The Lean runtime is compiled with Clang/libc++ (std::__1:: ABI), so linking libstdc++ on Linux leaves C++ stdlib symbols unresolved. - build.rs: use -lc++ on all platforms (matching leanc behavior), add Lean's bundled libc++ search path (<prefix>/lib/libc/) - CI: install libc++-dev as system fallback for the FFI test job
🤖 Kimi Code ReviewThis is a substantial and well-structured PR integrating formally verified Lean 4 code into the Rust consensus client. The mathematical proofs and FFI boundaries appear correct, but there are build system fragilities and CI efficiency issues to address. Critical IssuesBuild System Fragility let lean_project = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("../../formal");This breaks if the crate is moved or vendored. Use CI Efficiency & Correctness Also, Python 3.14 (line 184) is still pre-release. Use Missing Error Handling in Build Script .expect("Failed to run `lean --print-prefix`")For better UX, detect missing Lean and emit a descriptive error with installation instructions rather than a raw panic. Consensus & SecurityFFI Initialization Safety fn init_lean() {
INIT.call_once(|| unsafe {
lean_initialize_runtime_module();
let res = initialize_EthLambda_EthLambda(1);
lean_ffi_dec_ref(res);
lean_io_mark_end_initialization();
});
}Lean initialization can fail (e.g., memory exhaustion). While unlikely in practice, consider documenting that panics here are fatal and unrecoverable. Consensus-Critical Equivalence pub fn justifiable(delta: u64) -> bool {
init_lean();
unsafe { lean_justifiable(delta) != 0 }
}While the Lean debug_assert!(delta < (1 << 62), "justifiable: delta >= 2^62, theorem precondition violated");PerformanceRedundant Lake Builds FFI Call Overhead Code QualityLean 4 Idioms Rust Feature Propagation C Glue Code Recommendations
The formal verification work (classification, pronic detection, infinite liveness, density bounds) is mathematically rigorous and the FFI boundary is minimal and safe. The separation of Automated review by Kimi (Moonshot AI) · kimi-k2.5 · custom prompt |
🤖 Codex Code Review
I did not find other obvious runtime issues in the non-FFI changes. I could not run the Lean build/tests locally because Automated review by OpenAI Codex · gpt-5.4 · custom prompt |
🤖 Claude Code ReviewNow I have a comprehensive view of the PR. Let me write the review. PR Review: feat: formalize
|
Greptile SummaryThis PR introduces a Lean4 formal verification framework for the Confidence Score: 5/5Safe to merge; all findings are documentation and hardening suggestions with no impact on production correctness. All findings are P2: an overstated doc-comment, a theoretical UInt64 overflow requiring delta >= 2^62 (billions of years of slots), a grep word-boundary nit, and a missing rerun-if-changed entry. The core Newton's-method correctness proof, FFI wiring, and CI structure are solid. No P0/P1 issues found. formal/EthLambda/Justifiability.lean (overflow note on pronic check) and crates/blockchain/state_transition/src/lib.rs (doc comment accuracy)
|
| Filename | Overview |
|---|---|
| formal/EthLambda/Justifiability.lean | Computable UInt64 implementation of justifiability check with FFI exports; the pronic detection via 4 * delta + 1 can overflow for delta >= 2^62, a gap not covered by the published proofs. |
| formal/EthLambdaProofs/Justifiability/ImplEquivalence.lean | Thorough Newton's-method correctness proof bridging UInt64 isqrt to Nat.sqrt; justifiable_equiv correctly scoped to d < 2^62. |
| formal/lean-ffi/build.rs | Builds Lean C IR and links Lean runtime; rerun-if-changed only covers EthLambda sources, so changes to lakefile.toml or lean-toolchain won't trigger a rebuild. |
| formal/lean-ffi/src/lib.rs | Clean FFI bindings with Once-guarded runtime init; doc comment references incorrect path for the proofs directory. |
| crates/blockchain/state_transition/src/lib.rs | Feature-gates slot_is_justifiable_after correctly; doc comment claims proven correct for all natural numbers but proof only holds for delta < 2^62, and references wrong directory path. |
| .github/workflows/ci.yml | Adds lean-build and lean-ffi-test jobs; sorry grep check uses a plain string match that could produce false positives. |
| formal/EthLambdaProofs/Justifiability/Density.lean | Proves O(sqrt(N)) density bound for justifiable deltas via Finset cardinality bounds — clean and well-structured. |
| formal/lean-ffi/src/lean_glue.c | Minimal glue wrapping the static inline lean_dec_ref into a real symbol for Rust FFI — correct. |
Flowchart
%%{init: {'theme': 'neutral'}}%%
flowchart TD
A["Rust: slot_is_justifiable_after"] --> B{lean-ffi feature?}
B -- Yes --> C["ethlambda_lean_ffi crate"]
B -- No --> D["Native Rust implementation"]
C --> E["init_lean - once-guarded runtime init"]
E --> F["FFI: lean_slot_is_justifiable_after"]
F --> G["Lean: slotIsJustifiableAfter / justifiable delta"]
G --> H{delta le 5?}
H -- Yes --> OK["return true"]
H -- No --> I{isqrt squared equals delta?}
I -- Yes --> OK
I -- No --> J["4*delta+1 odd perfect square? WARN: overflows for delta ge 2^62"]
J -- Yes --> OK
J -- No --> NOK["return false"]
subgraph Lean Proofs
K["isqrt_correct: UInt64 isqrt = Nat.sqrt"]
L["justifiable_equiv: d lt 2^62"]
M["justifiable_unbounded: liveness"]
N["justifiable_density: O-sqrt-N"]
end
Prompt To Fix All With AI
This is a comment left during a code review.
Path: crates/blockchain/state_transition/src/lib.rs
Line: 506-507
Comment:
**Inaccurate doc comment: wrong path and overstated coverage**
The comment says "proven correct for all natural numbers (see `formal/EthLambda/Justifiability/`)" — both claims are wrong. The proofs live in `formal/EthLambdaProofs/Justifiability/`, not in the implementation lib. More importantly, `justifiable_equiv` only holds for `d.toNat < 2^62`; for larger deltas the `4 * delta + 1` term overflows UInt64 and the pronic check can misfire (e.g., delta = 2^62 wraps to give `val = 1`, which passes both the square and odd checks, falsely returning pronic).
```suggestion
/// When the `lean-ffi` feature is enabled, this calls the formally verified
/// Lean4 implementation via FFI. The Lean implementation has been proven correct
/// for all inputs with delta < 2^62 (see `formal/EthLambdaProofs/Justifiability/`).
/// For deltas >= 2^62 (unreachable in practice) the UInt64 pronic check may overflow.
///
/// Without the feature, uses the native Rust implementation.
```
How can I resolve this? If you propose a fix, please make it concise.
---
This is a comment left during a code review.
Path: formal/EthLambda/Justifiability.lean
Line: 40-41
Comment:
**UInt64 overflow in pronic check for delta >= 2^62**
When `delta >= 2^62`, the expression `4 * delta + 1` overflows UInt64 (wraps mod 2^64). For example, `delta = 2^62` gives `val = 1`, which satisfies both `isqrt(1)^2 = 1` and `1 % 2 = 1`, so the pronic arm returns `true` even though 2^62 is not pronic. The theorem `justifiable_equiv` correctly scopes its guarantee to `d < 2^62`, but the exported `leanJustifiable` and `leanSlotIsJustifiableAfter` functions apply the unchecked algorithm to all UInt64 values.
In practice slot differences will never reach 2^62, and the `ImplEquivalence` comments acknowledge this bound, so this is informational — but worth a guard comment on the FFI exports clarifying the domain:
```lean
-- Note: correctness of the pronic check is proven only for delta < 2^62.
-- Slot differences in practice are bounded well below this limit.
@[export lean_justifiable]
def leanJustifiable (delta : UInt64) : UInt8 :=
if justifiable delta then 1 else 0
```
How can I resolve this? If you propose a fix, please make it concise.
---
This is a comment left during a code review.
Path: .github/workflows/ci.yml
Line: 155-160
Comment:
**`sorry` grep may produce false positives**
`grep -rn "sorry"` matches the substring anywhere — inside identifiers like `not_sorry`, in comments (`-- no sorry used here`), or in string literals. A false positive would block CI without any real sorry in the proof tree. Scoping to a word-boundary regex avoids this:
```suggestion
if grep -rn "\bsorry\b" EthLambda/ EthLambdaProofs/ --include="*.lean"; then
```
How can I resolve this? If you propose a fix, please make it concise.
---
This is a comment left during a code review.
Path: formal/lean-ffi/build.rs
Line: 65-66
Comment:
**`rerun-if-changed` doesn't cover build-system files**
Changes to `formal/lean-toolchain` or `formal/lakefile.toml` change what the `lake build` step produces, but they don't live under `../EthLambda`, so Cargo won't re-run this build script when they're modified. Consider adding them:
```rust
println!("cargo:rerun-if-changed=../EthLambda");
println!("cargo:rerun-if-changed=../../formal/lakefile.toml");
println!("cargo:rerun-if-changed=../../formal/lean-toolchain");
println!("cargo:rerun-if-changed=src/lean_glue.c");
```
How can I resolve this? If you propose a fix, please make it concise.Reviews (1): Last reviewed commit: "Merge branch 'main' into lean-formalizat..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| /// Lean4 implementation via FFI. The Lean implementation has been proven correct | ||
| /// for all natural numbers (see `formal/EthLambda/Justifiability/`). |
There was a problem hiding this comment.
The comment says "proven correct for all natural numbers (see formal/EthLambda/Justifiability/)" — both claims are wrong. The proofs live in formal/EthLambdaProofs/Justifiability/, not in the implementation lib. More importantly, justifiable_equiv only holds for d.toNat < 2^62; for larger deltas the 4 * delta + 1 term overflows UInt64 and the pronic check can misfire (e.g., delta = 2^62 wraps to give val = 1, which passes both the square and odd checks, falsely returning pronic).
| /// Lean4 implementation via FFI. The Lean implementation has been proven correct | |
| /// for all natural numbers (see `formal/EthLambda/Justifiability/`). | |
| /// When the `lean-ffi` feature is enabled, this calls the formally verified | |
| /// Lean4 implementation via FFI. The Lean implementation has been proven correct | |
| /// for all inputs with delta < 2^62 (see `formal/EthLambdaProofs/Justifiability/`). | |
| /// For deltas >= 2^62 (unreachable in practice) the UInt64 pronic check may overflow. | |
| /// | |
| /// Without the feature, uses the native Rust implementation. |
Prompt To Fix With AI
This is a comment left during a code review.
Path: crates/blockchain/state_transition/src/lib.rs
Line: 506-507
Comment:
**Inaccurate doc comment: wrong path and overstated coverage**
The comment says "proven correct for all natural numbers (see `formal/EthLambda/Justifiability/`)" — both claims are wrong. The proofs live in `formal/EthLambdaProofs/Justifiability/`, not in the implementation lib. More importantly, `justifiable_equiv` only holds for `d.toNat < 2^62`; for larger deltas the `4 * delta + 1` term overflows UInt64 and the pronic check can misfire (e.g., delta = 2^62 wraps to give `val = 1`, which passes both the square and odd checks, falsely returning pronic).
```suggestion
/// When the `lean-ffi` feature is enabled, this calls the formally verified
/// Lean4 implementation via FFI. The Lean implementation has been proven correct
/// for all inputs with delta < 2^62 (see `formal/EthLambdaProofs/Justifiability/`).
/// For deltas >= 2^62 (unreachable in practice) the UInt64 pronic check may overflow.
///
/// Without the feature, uses the native Rust implementation.
```
How can I resolve this? If you propose a fix, please make it concise.| || (let val := 4 * delta + 1 | ||
| isqrt val ^ 2 == val && val % 2 == 1) |
There was a problem hiding this comment.
When delta >= 2^62, the expression 4 * delta + 1 overflows UInt64 (wraps mod 2^64). For example, delta = 2^62 gives val = 1, which satisfies both isqrt(1)^2 = 1 and 1 % 2 = 1, so the pronic arm returns true even though 2^62 is not pronic. The theorem justifiable_equiv correctly scopes its guarantee to d < 2^62, but the exported leanJustifiable and leanSlotIsJustifiableAfter functions apply the unchecked algorithm to all UInt64 values.
In practice slot differences will never reach 2^62, and the ImplEquivalence comments acknowledge this bound, so this is informational — but worth a guard comment on the FFI exports clarifying the domain:
-- Note: correctness of the pronic check is proven only for delta < 2^62.
-- Slot differences in practice are bounded well below this limit.
@[export lean_justifiable]
def leanJustifiable (delta : UInt64) : UInt8 :=
if justifiable delta then 1 else 0Prompt To Fix With AI
This is a comment left during a code review.
Path: formal/EthLambda/Justifiability.lean
Line: 40-41
Comment:
**UInt64 overflow in pronic check for delta >= 2^62**
When `delta >= 2^62`, the expression `4 * delta + 1` overflows UInt64 (wraps mod 2^64). For example, `delta = 2^62` gives `val = 1`, which satisfies both `isqrt(1)^2 = 1` and `1 % 2 = 1`, so the pronic arm returns `true` even though 2^62 is not pronic. The theorem `justifiable_equiv` correctly scopes its guarantee to `d < 2^62`, but the exported `leanJustifiable` and `leanSlotIsJustifiableAfter` functions apply the unchecked algorithm to all UInt64 values.
In practice slot differences will never reach 2^62, and the `ImplEquivalence` comments acknowledge this bound, so this is informational — but worth a guard comment on the FFI exports clarifying the domain:
```lean
-- Note: correctness of the pronic check is proven only for delta < 2^62.
-- Slot differences in practice are bounded well below this limit.
@[export lean_justifiable]
def leanJustifiable (delta : UInt64) : UInt8 :=
if justifiable delta then 1 else 0
```
How can I resolve this? If you propose a fix, please make it concise.|
|
||
| - name: Verify zero sorries | ||
| working-directory: formal | ||
| run: | | ||
| if grep -rn "sorry" EthLambda/ EthLambdaProofs/ --include="*.lean"; then | ||
| echo "::error::Found sorry in Lean sources" |
There was a problem hiding this comment.
sorry grep may produce false positives
grep -rn "sorry" matches the substring anywhere — inside identifiers like not_sorry, in comments (-- no sorry used here), or in string literals. A false positive would block CI without any real sorry in the proof tree. Scoping to a word-boundary regex avoids this:
| - name: Verify zero sorries | |
| working-directory: formal | |
| run: | | |
| if grep -rn "sorry" EthLambda/ EthLambdaProofs/ --include="*.lean"; then | |
| echo "::error::Found sorry in Lean sources" | |
| if grep -rn "\bsorry\b" EthLambda/ EthLambdaProofs/ --include="*.lean"; then |
Prompt To Fix With AI
This is a comment left during a code review.
Path: .github/workflows/ci.yml
Line: 155-160
Comment:
**`sorry` grep may produce false positives**
`grep -rn "sorry"` matches the substring anywhere — inside identifiers like `not_sorry`, in comments (`-- no sorry used here`), or in string literals. A false positive would block CI without any real sorry in the proof tree. Scoping to a word-boundary regex avoids this:
```suggestion
if grep -rn "\bsorry\b" EthLambda/ EthLambdaProofs/ --include="*.lean"; then
```
How can I resolve this? If you propose a fix, please make it concise.| println!("cargo:rerun-if-changed=../EthLambda"); | ||
| println!("cargo:rerun-if-changed=src/lean_glue.c"); |
There was a problem hiding this comment.
rerun-if-changed doesn't cover build-system files
Changes to formal/lean-toolchain or formal/lakefile.toml change what the lake build step produces, but they don't live under ../EthLambda, so Cargo won't re-run this build script when they're modified. Consider adding them:
println!("cargo:rerun-if-changed=../EthLambda");
println!("cargo:rerun-if-changed=../../formal/lakefile.toml");
println!("cargo:rerun-if-changed=../../formal/lean-toolchain");
println!("cargo:rerun-if-changed=src/lean_glue.c");Prompt To Fix With AI
This is a comment left during a code review.
Path: formal/lean-ffi/build.rs
Line: 65-66
Comment:
**`rerun-if-changed` doesn't cover build-system files**
Changes to `formal/lean-toolchain` or `formal/lakefile.toml` change what the `lake build` step produces, but they don't live under `../EthLambda`, so Cargo won't re-run this build script when they're modified. Consider adding them:
```rust
println!("cargo:rerun-if-changed=../EthLambda");
println!("cargo:rerun-if-changed=../../formal/lakefile.toml");
println!("cargo:rerun-if-changed=../../formal/lean-toolchain");
println!("cargo:rerun-if-changed=src/lean_glue.c");
```
How can I resolve this? If you propose a fix, please make it concise.
| /// Check if `delta` is justifiable under 3SF-mini rules. | ||
| /// | ||
| /// Calls the formally verified Lean4 implementation via FFI. | ||
| pub fn justifiable(delta: u64) -> bool { | ||
| init_lean(); | ||
| unsafe { lean_justifiable(delta) != 0 } | ||
| } |
There was a problem hiding this comment.
Not sure we need this
1 participant
Introduction
This PR introduces a Lean4 package under
formal/, formalizingslot_is_justifiable_afterand proving some properties like "there's always another justifiable slot" and "the distance between justifiable slots increases as the delta increases".First step of #272
Lean4 package structure
The new Lean4 package has two libraries:
EthLambdaandEthLambdaProofs. The first one contains the actual implementations called from Rust, using bounded types likeUInt64.EthLambdaProofs, on the other hand, contains theorems proving some properties of the implementation.Apart from those two, there's an additional directory with a Rust crate wrapping the Lean FFI glue.