From 0862695935a1b6fffcad2ab456a07cc8cfc4d3fe Mon Sep 17 00:00:00 2001 From: adust09 Date: Fri, 3 Jul 2026 00:41:04 +0900 Subject: [PATCH] feat(cont): prove CONT-2 justifiable iff distance is window, square, or pronic Prove justifiable_iff: the executable Slot.isJustifiableAfter holds iff the slot distance from the finalized slot is at most 5, a perfect square, or a pronic number. The core is correctness of the hand-rolled isqrt (isqrt_le / isqrt_lt_succ by functional induction on the base-4 recursion, uniqueness via isqrt_eq), plus the square-expansion helpers sq_succ / odd_sq and the pronic discriminant identity 4k(k+1) + 1 = (2k+1)^2 that justifies the upstream odd-square trick. Axiom-free, no Mathlib. --- LeanSpec/Forks/Lstar/Slot.lean | 144 ++++++++++++++++++++++++++++++- docs/lean4-proof-propositions.md | 12 +-- 2 files changed, 149 insertions(+), 7 deletions(-) diff --git a/LeanSpec/Forks/Lstar/Slot.lean b/LeanSpec/Forks/Lstar/Slot.lean index ee5f0f4..4600fe0 100644 --- a/LeanSpec/Forks/Lstar/Slot.lean +++ b/LeanSpec/Forks/Lstar/Slot.lean @@ -16,8 +16,13 @@ uses the argument order `(finalized, target)`, adopted here. Python asserts subtraction truncates instead — callers guarantee the precondition, as upstream's assert documents. -Supports the ST-* and CONT-2 propositions from -`docs/lean4-proof-propositions.md` (no theorems in this file). +Proves CONT-2 from `docs/lean4-proof-propositions.md`: + - CONT-2: `Slot.isJustifiableAfter finalized target` holds iff the slot + distance is at most 5, a perfect square, or a pronic number + (`justifiable_iff`), via correctness of the hand-rolled `isqrt`. + +Also supports the ST-* propositions (the executable judgments are consumed +by `process_attestations`). -/ import LeanSpec.Aliases @@ -61,4 +66,139 @@ def justifiedIndexAfter (finalized target : Slot) : Option Nat := if target ≤ finalized then none else some (target.toNat - finalized.toNat - 1) +/-! ## CONT-2: characterization of justifiability -/ + +/-- Expand `(k + 1)²` so `omega` can reason with `k * k` as an atom. -/ +private theorem sq_succ (k : Nat) : (k + 1) * (k + 1) = k * k + 2 * k + 1 := by + rw [Nat.mul_succ, Nat.succ_mul] + omega + +/-- Expand an odd square: `(2m + 1)² = 4m² + 4m + 1`. -/ +private theorem odd_sq (m : Nat) : + (2 * m + 1) * (2 * m + 1) = 4 * (m * m) + 4 * m + 1 := by + rw [sq_succ (2 * m), Nat.mul_mul_mul_comm] + omega + +/-- `isqrt` lower bound: its square never exceeds the input. -/ +theorem isqrt_le (n : Nat) : isqrt n * isqrt n ≤ n := by + induction n using isqrt.induct with + | case1 n h => + rw [isqrt, if_pos h] + have h01 : n = 0 ∨ n = 1 := by omega + cases h01 with + | inl h0 => subst h0; exact Nat.le_refl _ + | inr h1 => subst h1; exact Nat.le_refl _ + | case2 n h small large hlarge ih => + rw [isqrt, if_neg h] + dsimp only + split + · next h2 => exact h2 + · next h2 => exact absurd hlarge h2 + | case3 n h small large hnlarge ih => + rw [isqrt, if_neg h] + dsimp only + split + · next h2 => exact absurd h2 hnlarge + · next h2 => + have hexp : (2 * isqrt (n / 4)) * (2 * isqrt (n / 4)) + = 4 * (isqrt (n / 4) * isqrt (n / 4)) := by + rw [Nat.mul_mul_mul_comm] + omega + +/-- `isqrt` upper bound: the next square is strictly above the input. -/ +theorem isqrt_lt_succ (n : Nat) : n < (isqrt n + 1) * (isqrt n + 1) := by + induction n using isqrt.induct with + | case1 n h => + rw [isqrt, if_pos h] + rw [sq_succ] + omega + | case2 n h small large hlarge ih => + rw [isqrt, if_neg h] + dsimp only + split + · rw [show 2 * isqrt (n / 4) + 1 + 1 = 2 * (isqrt (n / 4) + 1) from by omega, + Nat.mul_mul_mul_comm] + omega + · next h2 => exact absurd hlarge h2 + | case3 n h small large hnlarge ih => + rw [isqrt, if_neg h] + dsimp only + split + · next h2 => exact absurd h2 hnlarge + · next h2 => exact Nat.lt_of_not_le h2 + +/-- `isqrt` is the unique value between the bracketing squares. -/ +theorem isqrt_eq (k n : Nat) (h1 : k * k ≤ n) (h2 : n < (k + 1) * (k + 1)) : + isqrt n = k := by + have hle := isqrt_le n + have hlt := isqrt_lt_succ n + have h3 : ¬ isqrt n < k := fun hc => by + have hstep : (isqrt n + 1) * (isqrt n + 1) ≤ k * k := + Nat.mul_le_mul (Nat.succ_le_of_lt hc) (Nat.succ_le_of_lt hc) + omega + have h4 : ¬ k < isqrt n := fun hc => by + have hstep : (k + 1) * (k + 1) ≤ isqrt n * isqrt n := + Nat.mul_le_mul (Nat.succ_le_of_lt hc) (Nat.succ_le_of_lt hc) + omega + omega + +/-- The pronic discriminant identity: `4k(k+1) + 1 = (2k+1)²`. -/ +private theorem pronic_disc (k : Nat) : + 4 * (k * (k + 1)) + 1 = (2 * k + 1) * (2 * k + 1) := by + rw [Nat.mul_succ, odd_sq] + omega + +/-- The three-form characterization of `justifiableDelta`: the distance is +within the immediate window, a perfect square, or a pronic number. -/ +theorem justifiableDelta_iff (δ : Nat) : + justifiableDelta δ = true ↔ + δ ≤ 5 ∨ (∃ k, δ = k * k) ∨ (∃ k, δ = k * (k + 1)) := by + unfold justifiableDelta immediateJustificationWindow + simp only [Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq] + constructor + · intro h + match h with + | .inl (.inl h5) => exact .inl h5 + | .inl (.inr hsq) => exact .inr (.inl ⟨isqrt δ, hsq.symm⟩) + | .inr ⟨hsq, hodd⟩ => + refine .inr (.inr ?_) + have hm : isqrt (4 * δ + 1) = 2 * (isqrt (4 * δ + 1) / 2) + 1 := by + omega + refine ⟨isqrt (4 * δ + 1) / 2, ?_⟩ + rw [hm, odd_sq] at hsq + rw [Nat.mul_succ] + omega + · intro h + match h with + | .inl h5 => exact .inl (.inl h5) + | .inr (.inl ⟨k, hk⟩) => + refine .inl (.inr ?_) + subst hk + rw [isqrt_eq k (k * k) (Nat.le_refl _) (by rw [sq_succ k]; omega)] + | .inr (.inr ⟨k, hk⟩) => + refine .inr ?_ + subst hk + have hr : isqrt (4 * (k * (k + 1)) + 1) = 2 * k + 1 := by + rw [pronic_disc] + exact isqrt_eq (2 * k + 1) _ (Nat.le_refl _) (by + rw [odd_sq, show 2 * k + 1 + 1 = 2 * (k + 1) from by omega, + Nat.mul_mul_mul_comm, sq_succ k] + omega) + constructor + · rw [hr] + exact (pronic_disc k).symm + · rw [hr] + omega + +/-- CONT-2: `is_justifiable_after` holds iff the slot distance from the +finalized slot is at most 5, a perfect square, or a pronic number. The +`finalized ≤ target` hypothesis mirrors upstream's assert; the +characterization itself holds for the truncated distance regardless. -/ +theorem justifiable_iff + (finalized target : Slot) (_h : finalized ≤ target) : + isJustifiableAfter finalized target ↔ + (let δ := target.toNat - finalized.toNat + δ ≤ 5 ∨ (∃ k, δ = k * k) ∨ (∃ k, δ = k * (k + 1))) := + justifiableDelta_iff (target.toNat - finalized.toNat) + end LeanSpec.Slot diff --git a/docs/lean4-proof-propositions.md b/docs/lean4-proof-propositions.md index 667e842..e3e6753 100644 --- a/docs/lean4-proof-propositions.md +++ b/docs/lean4-proof-propositions.md @@ -1,6 +1,6 @@ --- title: leanSpec → Lean4 Theorem Proving Proposition Catalog -last_updated: 2026-07-02 +last_updated: 2026-07-03 tags: - lean4 - formal-verification @@ -69,14 +69,14 @@ Format: `-`. `DOMAIN` is the abbreviation of the owning area: | Domain | Proved | Open | Axiom | Total | |---|---:|---:|---:|---:| | SSZ | 6 | 0 | 1 | 7 | -| CONT | 0 | 2 | 0 | 2 | +| CONT | 1 | 1 | 0 | 2 | | ST | 6 | 0 | 0 | 6 | | FC | 0 | 5 | 0 | 5 | | VAL | 0 | 5 | 0 | 5 | | NET | 0 | 2 | 0 | 2 | | STOR | 0 | 2 | 0 | 2 | | SYNC | 0 | 2 | 0 | 2 | -| **Total** | **12** | **18** | **1** | **31** | +| **Total** | **13** | **17** | **1** | **31** | ## SSZ & primitive types @@ -179,9 +179,10 @@ A **Container** is a composite SSZ type — a struct with named fields (analogou c1 < c2 ↔ c1.slot < c2.slot := by sorry ``` -- [ ] **CONT-2: justifiable holds iff the slot distance is one of three forms** - - Source: `is_justifiable_after` +- [x] **CONT-2: justifiable holds iff the slot distance is one of three forms** + - Source: `is_justifiable_after` (`src/lean_spec/spec/forks/lstar/slot.py`) - Note: Decides whether the target slot is at a justifiable distance from the finalized-checkpoint slot (LMD-CASPER justification-candidate check). + - Proved at: `LeanSpec/Forks/Lstar/Slot.lean` (`Slot.justifiable_iff`, via correctness of the hand-rolled `isqrt`: `isqrt_le` / `isqrt_lt_succ` / `isqrt_eq`) - Sample code: ```lean @@ -190,6 +191,7 @@ A **Container** is a composite SSZ type — a struct with named fields (analogou Slot.isJustifiableAfter finalized target ↔ let δ := target.toNat - finalized.toNat δ ≤ 5 ∨ (∃ k, δ = k * k) ∨ (∃ k, δ = k * (k + 1)) := by sorry + -- ✅ proved in LeanSpec/Forks/Lstar/Slot.lean as `Slot.justifiable_iff` ``` ## State Transition