From d0848b3910dbcbb24dcd06302ef6674f0824ab09 Mon Sep 17 00:00:00 2001
From: Satyawan Singh <satyawansinghinuk@gmail.com>
Date: Fri, 28 Aug 2026 15:32:19 +0100
Subject: [PATCH] fix: align Lean justifiability overflow semantics

---
 crates/blockchain/state_transition/src/lib.rs |  4 +--
 formal/EthLambda/Justifiability.lean          | 10 +++++--
 formal/EthLambdaProofs/Justifiability.lean    |  1 +
 .../Justifiability/ImplEquivalence.lean       |  9 +++++-
 .../Justifiability/Regression.lean            | 28 +++++++++++++++++++
 5 files changed, 46 insertions(+), 6 deletions(-)
 create mode 100644 formal/EthLambdaProofs/Justifiability/Regression.lean

diff --git a/crates/blockchain/state_transition/src/lib.rs b/crates/blockchain/state_transition/src/lib.rs
index b4f85322..df4751cb 100644
--- a/crates/blockchain/state_transition/src/lib.rs
+++ b/crates/blockchain/state_transition/src/lib.rs
@@ -503,8 +503,8 @@ pub fn slot_is_justifiable_after(slot: u64, finalized_slot: u64) -> bool {
 /// funnel votes towards only some slots, increasing finalization chances.
 ///
 /// 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 natural numbers (see `formal/EthLambda/Justifiability/`).
+/// Lean4 implementation via FFI. Its equivalence theorem covers deltas below
+/// `2^62`, the range where the pronic discriminant fits in `u64`.
 ///
 /// Without the feature, uses the native Rust implementation.
 #[cfg(not(feature = "lean-ffi"))]
diff --git a/formal/EthLambda/Justifiability.lean b/formal/EthLambda/Justifiability.lean
index 962463ac..1f23544e 100644
--- a/formal/EthLambda/Justifiability.lean
+++ b/formal/EthLambda/Justifiability.lean
@@ -33,12 +33,16 @@ def isqrt (n : UInt64) : UInt64 :=
     -- r+1 ≤ n/(r+1)  ↔  (r+1)*(r+1) ≤ n  (when r+1 > 0)
     if r + 1 <= n / (r + 1) then r + 1 else r
 
-/-- Computable justifiability check mirroring the Rust implementation. -/
+/-- Computable justifiability check mirroring Rust's checked arithmetic.
+    The pronic discriminant is evaluated only when `4 * delta + 1` fits in
+    `UInt64`; otherwise that branch returns `false`. -/
 def justifiable (delta : UInt64) : Bool :=
   delta <= 5
     || isqrt delta ^ 2 == delta
-    || (let val := 4 * delta + 1
-        isqrt val ^ 2 == val && val % 2 == 1)
+    || if delta <= 4611686018427387903 then
+         let val := 4 * delta + 1
+         isqrt val ^ 2 == val && val % 2 == 1
+       else false
 
 /-- Full slot-level function matching the Rust `slot_is_justifiable_after` API. -/
 def slotIsJustifiableAfter (slot finalizedSlot : UInt64) : Bool :=
diff --git a/formal/EthLambdaProofs/Justifiability.lean b/formal/EthLambdaProofs/Justifiability.lean
index 1c0240af..ffd98844 100644
--- a/formal/EthLambdaProofs/Justifiability.lean
+++ b/formal/EthLambdaProofs/Justifiability.lean
@@ -5,3 +5,4 @@ import EthLambdaProofs.Justifiability.Classification
 import EthLambdaProofs.Justifiability.Infinite
 import EthLambdaProofs.Justifiability.Density
 import EthLambdaProofs.Justifiability.ImplEquivalence
+import EthLambdaProofs.Justifiability.Regression
diff --git a/formal/EthLambdaProofs/Justifiability/ImplEquivalence.lean b/formal/EthLambdaProofs/Justifiability/ImplEquivalence.lean
index 6f63b186..d0508f6e 100644
--- a/formal/EthLambdaProofs/Justifiability/ImplEquivalence.lean
+++ b/formal/EthLambdaProofs/Justifiability/ImplEquivalence.lean
@@ -401,6 +401,12 @@ private lemma uint64_sq_toNat (a : UInt64) (ha : a.toNat < 2 ^ 32) :
 theorem justifiable_equiv (d : UInt64) (h : d.toNat < 2 ^ 62) :
     justifiable d = true ↔ Justifiable d.toNat := by
   rw [justifiable_iff]
+  have hguard : d ≤ 4611686018427387903 := by
+    apply UInt64.le_iff_toNat_le_toNat.mpr
+    have hlimit : (4611686018427387903 : UInt64).toNat = 2 ^ 62 - 1 := by
+      decide
+    rw [hlimit]
+    omega
   -- Bounds for 4 * d + 1 not overflowing
   have hval_nat : (4 * d + 1).toNat = 4 * d.toNat + 1 := by
     have h4_eq : (4 : UInt64).toNat = 4 := by decide
@@ -427,7 +433,8 @@ theorem justifiable_equiv (d : UInt64) (h : d.toNat < 2 ^ 62) :
     simp [UInt64.toNat_one]
   -- Unfold justifiable and convert Bool to Prop
   unfold justifiable
-  simp only [Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq]
+  simp only [hguard, ↓reduceIte, Bool.or_eq_true, Bool.and_eq_true,
+    decide_eq_true_eq, beq_iff_eq]
   -- The let binding in justifiable introduces `val := 4 * d + 1`; after simp, it becomes
   -- direct UInt64 expressions that we can rewrite with our bridge lemmas
   constructor
diff --git a/formal/EthLambdaProofs/Justifiability/Regression.lean b/formal/EthLambdaProofs/Justifiability/Regression.lean
new file mode 100644
index 00000000..1e1e10da
--- /dev/null
+++ b/formal/EthLambdaProofs/Justifiability/Regression.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 ethlambda contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import EthLambda.Justifiability
+
+/-!
+# Fixed-Width Arithmetic Regression
+
+The pronic discriminant for this value overflows UInt64. Rust uses checked
+arithmetic, so the Lean FFI implementation must reject it as well.
+-/
+
+/-- `4 * delta + 1` would wrap to `9` under unchecked UInt64 arithmetic. -/
+example : justifiable 4611686018427387906 = false := by
+  decide
+
+/-- The largest delta whose pronic discriminant fits remains evaluable. -/
+example : justifiable 4611686018427387903 = false := by
+  decide
+
+/-- Perfect-square detection remains valid at the first overflowing-pronic delta. -/
+example : justifiable 4611686018427387904 = true := by
+  decide
+
+/-- Values above the checked-pronic range do not wrap into false positives. -/
+example : justifiable 18446744073709551615 = false := by
+  decide