Remove Mathlib dependency to shrink the compiled binary

.github/workflows/lean_action_ci.yml

@@ -19,14 +19,13 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v4
 
-      # lean-action installs the toolchain pinned in `lean-toolchain`, fetches the prebuilt Mathlib
-      # olean cache (so Mathlib is not recompiled from source), and runs `lake build` — which also
-      # type-checks every `example`/`def` in the library, including the DSL round-trips and the
-      # big-step smoke tests.
-      - name: Build (fetch Mathlib cache + lake build)
+      # lean-action installs the toolchain pinned in `lean-toolchain` and runs `lake build` — which
+      # also type-checks every `example`/`def` in the library, including the DSL round-trips and the
+      # big-step smoke tests. The only dependency is Batteries (built from source; it is small).
+      - name: Build (lake build)
         uses: leanprover/lean-action@v1
         with:
-          use-mathlib-cache: "true"
+          use-mathlib-cache: "false"
           build: "true"
           test: "false"
           lint: "true"

DESIGN.md

@@ -389,4 +389,5 @@ for the equivalence/simulation results above.
 ## Dependencies
 
 - Lean toolchain: `leanprover/lean4:v4.31.0` (see `lean-toolchain`).
-- [Mathlib](https://github.com/leanprover-community/mathlib4), pinned to the matching tag.
+- [Batteries](https://github.com/leanprover-community/batteries), pinned to the matching tag
+  (only for the `lake lint` driver and the `nolint` attribute — no Mathlib).

README.md

@@ -25,7 +25,6 @@ Requires the Lean toolchain pinned in [`lean-toolchain`](./lean-toolchain) (mana
 [`elan`](https://github.com/leanprover/elan)).
 
 ```sh
-lake exe cache get   # fetch prebuilt Mathlib oleans
 lake build
 ```
 

YulSemantics/Adequacy.lean

@@ -1,4 +1,3 @@
-import Mathlib.Data.Nat.Basic
 import YulSemantics.BigStep
 import YulSemantics.Interp
 import YulSemantics.Dialect.EVM
@@ -743,7 +742,7 @@ theorem adequacy (hE : E.Lawful) {funs V st code res} :
   constructor
   · intro h
     obtain ⟨N, hN⟩ := complete hE h
-    exact ⟨N, hN N le_rfl⟩
+    exact ⟨N, hN N (Nat.le_refl N)⟩
   · rintro ⟨n, h⟩
     have S := sound_all hE n
     cases code with
@@ -776,7 +775,7 @@ theorem run_adequacy (hE : E.Lawful) {prog st0 V' st' o} :
   constructor
   · intro h
     obtain ⟨N, hN⟩ := complete hE h
-    have := hN N le_rfl
+    have := hN N (Nat.le_refl N)
     exact ⟨N, by simpa [InterpOk, Interp.run] using this⟩
   · rintro ⟨n, h⟩
     exact run_sound hE h

YulSemantics/Basic.lean

@@ -6,11 +6,11 @@ import Std.Tactic.BVDecide
 Confirms the toolchain is wired up and that the EVM word type `BitVec 256`
 (see `DESIGN.md` §4) is available with its bitvector automation.
 
-This module deliberately does **not** `import Mathlib`. Every Lean module's `initialize_*`
-calls the initializer of each module it imports, so a bare `import Mathlib` anywhere in a
-downstream executable's import closure is a genuine symbol reference that keeps all ~8200
-Mathlib object files alive at link time. `bv_decide` comes from `Std`, so nothing here needs
-Mathlib; the modules that really do use Mathlib import the specific files they need.
+This project does **not** depend on Mathlib. Every Lean module's `initialize_*` calls the
+initializer of each module it imports, so a bare `import Mathlib` anywhere in a downstream
+executable's import closure is a genuine symbol reference that keeps all ~8200 Mathlib object
+files alive at link time. `bv_decide` comes from `Std` (core); the only external dependency is
+Batteries, kept for the `lake lint` driver and the `nolint` attribute.
 
 Module map:
 * `YulSemantics.Ast`     — AST + control-flow `Outcome`

YulSemantics/Dialect/EVM.lean

@@ -1,22 +1,12 @@
-import Mathlib.Tactic.SplitIfs
 import YulSemantics.Dialect.EVMExec
 
 /-!
 # YulSemantics.Dialect.EVM
 
 The **metatheory** of the EVM dialect (effect-classification soundness, executable-dialect
-lawfulness, `@[simp]` state-helper lemmas, and worked examples). The Mathlib-free executable
+lawfulness, `@[simp]` state-helper lemmas, and worked examples). The dependency-free executable
 interpreter (`Op`, `stepOp`, the `evm` dialect instance, all state defs) lives in
-`YulSemantics.Dialect.EVMExec`; this module imports it and adds the proofs, keeping Mathlib off
-the import path of code that only needs to *run* the dialect.
-
-## Imports
-
-This module deliberately does **not** `import Mathlib`. Every Lean module's `initialize_*`
-function calls the initializer of each module it imports, and that is a genuine symbol
-reference the linker cannot discard — so a single bare `import Mathlib` anywhere in a
-downstream executable's import closure keeps all ~8200 Mathlib object files alive at link
-time. The only Mathlib entry point this file actually needs is the `split_ifs` tactic.
+`YulSemantics.Dialect.EVMExec`; this module imports it and adds the proofs.
 -/
 
 namespace YulSemantics.EVM
@@ -121,7 +111,7 @@ theorem effects_sound : evm.EffectsSound := by
       change stepOp _ args st2 = some (.ok rets2 st2') at h2
       rcases args with _ | ⟨a, _ | ⟨b, _ | ⟨c, _ | ⟨d, args⟩⟩⟩⟩ <;>
         simp_all [stepOp, un, bin, ter, rd0, rd1, guardStatic] <;>
-        split_ifs at h1 h2 <;> simp_all
+        repeat1' (first | split at h1 | split at h2) <;> simp_all
   · intro op hw
     cases op <;> simp [effects] at hw
     all_goals

YulSemantics/Equiv.lean

@@ -1,4 +1,3 @@
-import Mathlib.Data.List.Forall2
 import YulSemantics.BigStep
 
 /-!
@@ -41,6 +40,21 @@ For whole programs, equivalence of the top-level blocks gives identical `Run` re
 
 namespace YulSemantics
 
+/-- Pointwise lifting of a relation to lists: `Forall₂ R l₁ l₂` holds when `l₁` and `l₂` have the
+same length and `R` relates their elements position-wise. (A local stand-in for Mathlib's
+`List.Forall₂` — the congruence lemmas below need nothing more than the inductive and `imp`.) -/
+inductive Forall₂ (R : α → β → Prop) : List α → List β → Prop
+  /-- Two empty lists are pointwise related. -/
+  | nil : Forall₂ R [] []
+  /-- Related heads on pointwise-related tails give pointwise-related lists. -/
+  | cons : R a b → Forall₂ R l₁ l₂ → Forall₂ R (a :: l₁) (b :: l₂)
+
+/-- `Forall₂` is monotone in the relation. -/
+theorem Forall₂.imp {R S : α → β → Prop} (H : ∀ a b, R a b → S a b) :
+    ∀ {l₁ l₂}, Forall₂ R l₁ l₂ → Forall₂ S l₁ l₂
+  | _, _, .nil => .nil
+  | _, _, .cons h t => .cons (H _ _ h) (t.imp H)
+
 variable {D : Dialect} [DecidableEq D.Value]
 
 /-! ### The equivalences -/
@@ -124,7 +138,7 @@ theorem EquivBlock.run_iff {p₁ p₂ : Block D.Op} (h : EquivBlock D p₁ p₂)
 /-! ### Congruence: argument lists -/
 
 private theorem argsImp {es₁ es₂ : List (Expr D.Op)}
-    (h : List.Forall₂
+    (h : Forall₂
       (fun e₁ e₂ => ∀ funs V st r, EvalExpr D funs V st e₁ r → EvalExpr D funs V st e₂ r) es₁ es₂) :
     ∀ funs V st r, EvalArgs D funs V st es₁ r → EvalArgs D funs V st es₂ r := by
   induction h with
@@ -137,14 +151,14 @@ private theorem argsImp {es₁ es₂ : List (Expr D.Op)}
       | argsHeadHalt ha hh => exact Step.argsHeadHalt (ih _ _ _ _ ha) (he _ _ _ _ hh)
 
 private theorem forall₂_symm {α : Type _} {R : α → α → Prop} {l₁ l₂ : List α}
-    (hsym : ∀ {a b}, R a b → R b a) (h : List.Forall₂ R l₁ l₂) : List.Forall₂ R l₂ l₁ := by
+    (hsym : ∀ {a b}, R a b → R b a) (h : Forall₂ R l₁ l₂) : Forall₂ R l₂ l₁ := by
   induction h with
   | nil => exact .nil
   | cons hh _ ih => exact .cons (hsym hh) ih
 
 /-- Pairwise-equivalent argument lists are equivalent. -/
 theorem EquivArgs.of_forall₂ {es₁ es₂ : List (Expr D.Op)}
-    (h : List.Forall₂ (EquivExpr D) es₁ es₂) : EquivArgs D es₁ es₂ :=
+    (h : Forall₂ (EquivExpr D) es₁ es₂) : EquivArgs D es₁ es₂ :=
   fun _ _ _ _ =>
     ⟨argsImp (h.imp fun _ _ he funs V st r => (he funs V st r).mp) _ _ _ _,
      argsImp ((forall₂_symm (fun he => he.symm) h).imp
@@ -193,7 +207,7 @@ theorem EquivStmts.cons_congr {s₁ s₂ : Stmt D.Op} {ss₁ ss₂} (hs : EquivS
 
 /-- Pairwise-equivalent statement sequences are equivalent. -/
 theorem EquivStmts.of_forall₂ {ss₁ ss₂ : List (Stmt D.Op)}
-    (h : List.Forall₂ (EquivStmt D) ss₁ ss₂) : EquivStmts D ss₁ ss₂ := by
+    (h : Forall₂ (EquivStmt D) ss₁ ss₂) : EquivStmts D ss₁ ss₂ := by
   induction h with
   | nil => exact EquivStmts.refl []
   | cons hh _ ih => exact EquivStmts.cons_congr hh ih
@@ -214,7 +228,7 @@ theorem EquivBlock.of_stmts {b₁ b₂ : Block D.Op} (hss : EquivStmts D b₁ b
   fun _ _ _ _ _ _ => ⟨blockImp hss hh, blockImp hss.symm hh.symm⟩
 
 /-- Convenience: pairwise-equivalent bodies with equal hoisted scopes form equivalent blocks. -/
-theorem EquivBlock.of_forall₂ {b₁ b₂ : Block D.Op} (h : List.Forall₂ (EquivStmt D) b₁ b₂)
+theorem EquivBlock.of_forall₂ {b₁ b₂ : Block D.Op} (h : Forall₂ (EquivStmt D) b₁ b₂)
     (hh : hoist D b₁ = hoist D b₂) : EquivBlock D b₁ b₂ :=
   EquivBlock.of_stmts (EquivStmts.of_forall₂ h) hh
 
@@ -273,7 +287,7 @@ theorem EquivStmt.cond_congr {c₁ c₂ : Expr D.Op} {b₁ b₂ : Block D.Op} (h
 /-- `selectSwitch` respects pairwise-related cases: equal labels, equivalent blocks. -/
 private theorem selectSwitch_congr {cv : D.Value} {cs₁ cs₂ : List (Literal × Block D.Op)}
     {dflt₁ dflt₂ : Option (Block D.Op)}
-    (hcases : List.Forall₂ (fun p q => p.1 = q.1 ∧ EquivBlock D p.2 q.2) cs₁ cs₂)
+    (hcases : Forall₂ (fun p q => p.1 = q.1 ∧ EquivBlock D p.2 q.2) cs₁ cs₂)
     (hdflt : EquivBlock D (dflt₁.getD []) (dflt₂.getD [])) :
     EquivBlock D (selectSwitch D cv cs₁ dflt₁) (selectSwitch D cv cs₂ dflt₂) := by
   induction hcases with
@@ -306,7 +320,7 @@ private theorem switchImp {c₁ c₂ : Expr D.Op} {cs₁ cs₂ dflt₁ dflt₂}
 equivalent blocks), and equivalent defaults. -/
 theorem EquivStmt.switch_congr {c₁ c₂ : Expr D.Op} {cs₁ cs₂ : List (Literal × Block D.Op)}
     {dflt₁ dflt₂ : Option (Block D.Op)} (hc : EquivExpr D c₁ c₂)
-    (hcases : List.Forall₂ (fun p q => p.1 = q.1 ∧ EquivBlock D p.2 q.2) cs₁ cs₂)
+    (hcases : Forall₂ (fun p q => p.1 = q.1 ∧ EquivBlock D p.2 q.2) cs₁ cs₂)
     (hdflt : EquivBlock D (dflt₁.getD []) (dflt₂.getD [])) :
     EquivStmt D (.switch c₁ cs₁ dflt₁) (.switch c₂ cs₂ dflt₂) := by
   have hcases' := forall₂_symm

YulSemantics/FibExample.lean

@@ -1,4 +1,3 @@
-import Mathlib.Data.Nat.Fib.Basic
 import YulSemantics.Interp
 import YulSemantics.Syntax
 import YulSemantics.BigStep
@@ -10,7 +9,7 @@ An example Yul contract that reads a number `n` from calldata, computes the `n`-
 (mod `2^256`), writes it to memory, and returns it — together with proofs of its semantics:
 
 * **concrete** end-to-end runs via the interpreter (`native_decide`), for several inputs; and
-* a **general** theorem: for every input `n`, the contract halts returning `Nat.fib n` (as a word).
+* a **general** theorem: for every input `n`, the contract halts returning `fib n` (as a word).
 
 The general proof factors through a loop-invariant lemma (`fibLoop`) proven by induction on the
 number of remaining iterations, over the big-step judgment.
@@ -20,6 +19,16 @@ namespace YulSemantics.FibExample
 
 open YulSemantics EVM
 
+/-- The Fibonacci numbers (a local stand-in for Mathlib's `Nat.fib`; the naive double recursion is
+fine at the scale of the examples below). -/
+def fib : Nat → Nat
+  | 0 => 0
+  | 1 => 1
+  | n + 2 => fib n + fib (n + 1)
+
+/-- The defining recurrence, in rewrite-friendly form. -/
+theorem fib_add_two (n : Nat) : fib (n + 2) = fib n + fib (n + 1) := rfl
+
 /-- The Fibonacci contract, in concrete Yul syntax. `a`/`b` carry consecutive Fibonacci numbers;
 after `n` iterations `a = fib n`. -/
 def fibContract : Block EVM.Op := yul% {
@@ -45,22 +54,22 @@ def callWith (n : Nat) : EvmState :=
 /-- `fib 0 = 0`. -/
 example :
     (Interp.run EVM.exec 3000 fibContract (callWith 0)).map (fun r => loadWord r.2.1.memory 0)
-      = .ok (BitVec.ofNat 256 (Nat.fib 0)) := by native_decide
+      = .ok (BitVec.ofNat 256 (fib 0)) := by native_decide
 
 /-- `fib 1 = 1`. -/
 example :
     (Interp.run EVM.exec 3000 fibContract (callWith 1)).map (fun r => loadWord r.2.1.memory 0)
-      = .ok (BitVec.ofNat 256 (Nat.fib 1)) := by native_decide
+      = .ok (BitVec.ofNat 256 (fib 1)) := by native_decide
 
 /-- `fib 7 = 13`. -/
 example :
     (Interp.run EVM.exec 3000 fibContract (callWith 7)).map (fun r => loadWord r.2.1.memory 0)
-      = .ok (BitVec.ofNat 256 (Nat.fib 7)) := by native_decide
+      = .ok (BitVec.ofNat 256 (fib 7)) := by native_decide
 
 /-- `fib 10 = 55`, and the full return path: the contract halts returning the 32-byte word. -/
 example :
     (Interp.run EVM.exec 3000 fibContract (callWith 10)).map (fun r => r.2.1.halted)
-      = .ok (some (.ret, List.replicate 31 0 ++ [UInt8.ofNat (Nat.fib 10)])) := by native_decide
+      = .ok (some (.ret, List.replicate 31 0 ++ [UInt8.ofNat (fib 10)])) := by native_decide
 
 /-! ### The general theorem
 
@@ -124,11 +133,11 @@ is pure), so it threads through unchanged. -/
 theorem fibLoop (funs : FunEnv evm) (st : EvmState) (nv : U256) :
     ∀ (k I : Nat), I + k = nv.toNat →
       ExecLoop evm funs
-        [("i", BitVec.ofNat 256 I), ("b", BitVec.ofNat 256 (Nat.fib (I + 1))),
-         ("a", BitVec.ofNat 256 (Nat.fib I)), ("n", nv)] st
+        [("i", BitVec.ofNat 256 I), ("b", BitVec.ofNat 256 (fib (I + 1))),
+         ("a", BitVec.ofNat 256 (fib I)), ("n", nv)] st
         (.builtin .lt [.var "i", .var "n"]) fibPost fibBody
-        [("i", BitVec.ofNat 256 nv.toNat), ("b", BitVec.ofNat 256 (Nat.fib (nv.toNat + 1))),
-         ("a", BitVec.ofNat 256 (Nat.fib nv.toNat)), ("n", nv)] st .normal := by
+        [("i", BitVec.ofNat 256 nv.toNat), ("b", BitVec.ofNat 256 (fib (nv.toNat + 1))),
+         ("a", BitVec.ofNat 256 (fib nv.toNat)), ("n", nv)] st .normal := by
   intro k
   induction k with
   | zero =>
@@ -148,17 +157,17 @@ theorem fibLoop (funs : FunEnv evm) (st : EvmState) (nv : U256) :
     refine Step.loopStep
       (Step.builtinOk (Step.argsCons (Step.argsCons Step.argsNil (Step.var rfl)) (Step.var rfl)) rfl)
       ?_
-      (fib_body funs st (BitVec.ofNat 256 I) (BitVec.ofNat 256 (Nat.fib I))
-        (BitVec.ofNat 256 (Nat.fib (I + 1))) nv)
+      (fib_body funs st (BitVec.ofNat 256 I) (BitVec.ofNat 256 (fib I))
+        (BitVec.ofNat 256 (fib (I + 1))) nv)
       (Or.inl rfl)
-      (fib_post funs st (BitVec.ofNat 256 I) (BitVec.ofNat 256 (Nat.fib (I + 1)))
-        (BitVec.ofNat 256 (Nat.fib I) + BitVec.ofNat 256 (Nat.fib (I + 1))) nv)
+      (fib_post funs st (BitVec.ofNat 256 I) (BitVec.ofNat 256 (fib (I + 1)))
+        (BitVec.ofNat 256 (fib I) + BitVec.ofNat 256 (fib (I + 1))) nv)
       ?_
     · show b2w ((BitVec.ofNat 256 I).ult nv) ≠ evm.zero
       rw [hcond]; decide
     · have hi : BitVec.ofNat 256 I + BitVec.ofNat 256 1 = BitVec.ofNat 256 (I + 1) := ofNat_add I 1
-      have hb : BitVec.ofNat 256 (Nat.fib I) + BitVec.ofNat 256 (Nat.fib (I + 1))
-              = BitVec.ofNat 256 (Nat.fib (I + 2)) := by rw [ofNat_add, ← Nat.fib_add_two]
+      have hb : BitVec.ofNat 256 (fib I) + BitVec.ofNat 256 (fib (I + 1))
+              = BitVec.ofNat 256 (fib (I + 2)) := by rw [ofNat_add, ← fib_add_two]
       rw [hi, hb]
       exact ih (I + 1) (by omega)
 
@@ -185,18 +194,18 @@ slice into `wordBytes`). -/
 theorem fibContract_correct (st0 : EvmState) :
     ∃ st, Run evm fibContract st0 [] st .halt ∧
       st.halted = some (.ret,
-        wordBytes (BitVec.ofNat 256 (Nat.fib (wordFrom st0.env.calldata 0).toNat))) := by
+        wordBytes (BitVec.ofNat 256 (fib (wordFrom st0.env.calldata 0).toNat))) := by
   have hstmts : ExecStmts evm (hoist evm fibContract :: []) [] st0 fibContract
-      [("b", BitVec.ofNat 256 (Nat.fib ((wordFrom st0.env.calldata 0).toNat + 1))),
-       ("a", BitVec.ofNat 256 (Nat.fib (wordFrom st0.env.calldata 0).toNat)),
+      [("b", BitVec.ofNat 256 (fib ((wordFrom st0.env.calldata 0).toNat + 1))),
+       ("a", BitVec.ofNat 256 (fib (wordFrom st0.env.calldata 0).toNat)),
        ("n", wordFrom st0.env.calldata 0)]
       { touchMemory
           { touchMemory st0 0 32 with
             memory := storeWord st0.memory 0
-              (BitVec.ofNat 256 (Nat.fib (wordFrom st0.env.calldata 0).toNat)) }
+              (BitVec.ofNat 256 (fib (wordFrom st0.env.calldata 0).toNat)) }
           0 32 with
         halted := some (.ret, readBytes (storeWord st0.memory 0
-          (BitVec.ofNat 256 (Nat.fib (wordFrom st0.env.calldata 0).toNat))) 0 32) }
+          (BitVec.ofNat 256 (fib (wordFrom st0.env.calldata 0).toNat))) 0 32) }
       .halt := by
     -- let n := calldataload(0)
     refine Step.seqCons (Step.letVal (Step.builtinOk (Step.argsCons Step.argsNil Step.lit) rfl) rfl) ?_