From a06f9701ea2299e465ece245b43204e94185c8dc Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 29 Jul 2026 19:26:58 +0200 Subject: [PATCH] Narrow the two bare `import Mathlib` to the modules actually used MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Every Lean module's `initialize_` function calls the initializer of each module it imports. That call is a genuine symbol reference, so the linker cannot discard it: a single bare `import Mathlib` anywhere in a downstream executable's import closure keeps *all* ~8,200 Mathlib object files alive at link time, even though almost none of their code is reachable. A solc statically linked against the Yul compiler's C API was 340 MB, of which 62 MB was Mathlib pulled in this way. This library had two bare imports, and `YulSemantics.Dialect.EVM` is in the import closure of the downstream `yulc` executable, so it alone accounted for the whole 8,200-module drag. * `YulSemantics/Dialect/EVM.lean` — after the EVMOp/EVMExec split this file is metatheory only, and the single Mathlib entry point it needs is the `split_ifs` tactic (`Mathlib.Tactic.SplitIfs`). The `set_option linter.unnecessarySeqFocus false in` on `effects_sound_withExternal` is no longer needed either. * `YulSemantics/Basic.lean` — `bv_decide` is a Std tactic (`Std.Tactic.BVDecide`); nothing here needed Mathlib at all. Fixing the cascade in the modules that were getting Mathlib transitively through `Dialect.EVM`: * `Adequacy.lean` — `Mathlib.Data.Nat.Basic` (`le_rfl` at `Nat`'s `LinearOrder`). * `FibExample.lean` — `Mathlib.Data.Nat.Fib.Basic` (`Nat.fib`). * `Observation.lean`, `ObjectRun.lean`, `Examples.lean`, `Rewrites.lean` — explicit `(D := evm)` on four `Step.block` terms and one `EquivArgs.of_forall₂`. `Step`/`EquivArgs` take `[DecidableEq D.Value]`, and these proof terms are elaborated before the expected type fixes `D`. With Mathlib present, `DecidableEq (Dialect.Value ?D)` was *inconclusive* rather than failing — Mathlib's order hierarchy offers `LinearOrder.toDecidableEq` and a long chain below it, which leaves the search stuck on metavariables — so Lean postponed it until `?D` was known. Without Mathlib there are no candidate instances at all, so it is a hard failure. Naming the dialect makes elaboration independent of which instances happen to be in scope. No tactic block, definition or proof term changed. The only statement change is in an `EVM.lean` test fixture: `EvmState.selfdestructs : List (U256 × Bool)`, so the expected `[0x10]` was elaborating through Mathlib's boolean-ring `NatCast Bool` to `[(16, false)]`. That is now written `[(0x10, false)]` directly — verified equal to the old elaboration before the import was removed. `lake build` goes from 8,578 jobs to 884; `lake lint` still passes. Co-Authored-By: Claude Opus 5 (1M context) --- YulSemantics/Adequacy.lean | 1 + YulSemantics/Basic.lean | 10 ++++++++-- YulSemantics/Dialect/EVM.lean | 13 ++++++++++--- YulSemantics/Examples.lean | 2 +- YulSemantics/FibExample.lean | 1 + YulSemantics/ObjectRun.lean | 2 +- YulSemantics/Observation.lean | 6 +++--- YulSemantics/Rewrites.lean | 2 +- 8 files changed, 26 insertions(+), 11 deletions(-) diff --git a/YulSemantics/Adequacy.lean b/YulSemantics/Adequacy.lean index 985d1e0..6ae46ca 100644 --- a/YulSemantics/Adequacy.lean +++ b/YulSemantics/Adequacy.lean @@ -1,3 +1,4 @@ +import Mathlib.Data.Nat.Basic import YulSemantics.BigStep import YulSemantics.Interp import YulSemantics.Dialect.EVM diff --git a/YulSemantics/Basic.lean b/YulSemantics/Basic.lean index a124e6e..cef6945 100644 --- a/YulSemantics/Basic.lean +++ b/YulSemantics/Basic.lean @@ -1,11 +1,17 @@ -import Mathlib +import Std.Tactic.BVDecide /-! # YulSemantics.Basic -Confirms the toolchain and Mathlib are wired up, and that the EVM word type `BitVec 256` +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. + Module map: * `YulSemantics.Ast` — AST + control-flow `Outcome` * `YulSemantics.Dialect` — abstract `Dialect` + EVM dialect instance diff --git a/YulSemantics/Dialect/EVM.lean b/YulSemantics/Dialect/EVM.lean index 8e63b01..c0daac1 100644 --- a/YulSemantics/Dialect/EVM.lean +++ b/YulSemantics/Dialect/EVM.lean @@ -1,4 +1,4 @@ -import Mathlib +import Mathlib.Tactic.SplitIfs import YulSemantics.Dialect.EVMExec /-! @@ -9,6 +9,14 @@ lawfulness, `@[simp]` state-helper lemmas, and worked examples). The Mathlib-fre 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. -/ namespace YulSemantics.EVM @@ -130,7 +138,6 @@ theorem effects_sound : evm.EffectsSound := by _ | ⟨a, _ | ⟨b, _ | ⟨c, _ | ⟨d, _ | ⟨e, _ | ⟨f, _ | ⟨g, args⟩⟩⟩⟩⟩⟩⟩ <;> simp_all [stepOp, un, bin, ter, rd0, rd1] <;> subst r <;> rfl -set_option linter.unnecessarySeqFocus false in /-- The effect classification remains sound for every external call/create relation. External operations carry no determinism, non-writing, or non-halting promise (the call/create family is now marked `halts := true` to cover static-context write protection), so only the non-halting @@ -218,7 +225,7 @@ example : let st := finishSelfdestruct (selfdestructTestState false) 0x20 (st.env.selfBalance, st.env.balanceOf 0x10, st.env.balanceOf 0x20, st.selfdestructs, st.halted) = - (0, 0, 12, [0x10], some (.selfdestruct, [])) := by rfl + (0, 0, 12, [(0x10, false)], some (.selfdestruct, [])) := by rfl example : let st := finishSelfdestruct (selfdestructTestState false) 0x10 diff --git a/YulSemantics/Examples.lean b/YulSemantics/Examples.lean index 2c9de93..56c0fc8 100644 --- a/YulSemantics/Examples.lean +++ b/YulSemantics/Examples.lean @@ -18,7 +18,7 @@ open YulSemantics EVM /-- The empty program runs to a normal outcome, leaving the state and (empty) environment. -/ example : Run evm [] EvmState.init [] EvmState.init .normal := - Step.block Step.seqNil + Step.block (D := evm) Step.seqNil /-- `{ stop() }` halts. (Exercises the halt-propagation path through `exprStmt`/built-in.) -/ example : ∃ V' st' o, Run evm [Stmt.exprStmt (Expr.builtin .stop [])] EvmState.init V' st' o := diff --git a/YulSemantics/FibExample.lean b/YulSemantics/FibExample.lean index f419589..cd03ae7 100644 --- a/YulSemantics/FibExample.lean +++ b/YulSemantics/FibExample.lean @@ -1,3 +1,4 @@ +import Mathlib.Data.Nat.Fib.Basic import YulSemantics.Interp import YulSemantics.Syntax import YulSemantics.BigStep diff --git a/YulSemantics/ObjectRun.lean b/YulSemantics/ObjectRun.lean index 90583d9..ec32bce 100644 --- a/YulSemantics/ObjectRun.lean +++ b/YulSemantics/ObjectRun.lean @@ -121,7 +121,7 @@ theorem constructorCode_returns (L : Layout) (n : Ident) (d : Data) (hlt : d.size < 2 ^ 256) : ∃ V st, Run evm (constructorCode n) L.initState V st .halt ∧ st.halted = some (.ret, d.bytes) := by - refine ⟨[], _, Step.block (Step.seqCons + refine ⟨[], _, Step.block (D := evm) (Step.seqCons (Step.exprStmt (Step.builtinOk (Step.argsCons (Step.argsCons (Step.argsCons Step.argsNil (eval_datasize _ _ _ _)) (eval_dataoffset _ _ _ _)) Step.lit) rfl)) diff --git a/YulSemantics/Observation.lean b/YulSemantics/Observation.lean index 6b6fb1b..e4e0f54 100644 --- a/YulSemantics/Observation.lean +++ b/YulSemantics/Observation.lean @@ -79,7 +79,7 @@ private theorem run_dead (st0 : EvmState) (hstatic : st0.env.static = false) : show stepOp .sstore _ st0 = some _ simp [stepOp, guardStatic, hstatic] have hrun : Run EVM.evm deadStoreRevert st0 [] _ .halt := - Step.block (Step.seqCons + Step.block (D := EVM.evm) (Step.seqCons (Step.exprStmt (Step.builtinOk (Step.argsCons (Step.argsCons Step.argsNil Step.lit) Step.lit) hss)) (Step.seqStop @@ -93,7 +93,7 @@ private theorem run_bare (st0 : EvmState) : ∃ st', Run EVM.evm bareRevert st0 [] st' .halt ∧ committedState st0 st' = { st0 with halted := some (.revert, []) } := by have hrun : Run EVM.evm bareRevert st0 [] _ .halt := - Step.block (Step.seqStop + Step.block (D := EVM.evm) (Step.seqStop (Step.exprStmtHalt (Step.builtinHalt (Step.argsCons (Step.argsCons Step.argsNil Step.lit) Step.lit) rfl)) (by decide)) @@ -143,7 +143,7 @@ example : st'.storage 0 = 1 ∧ (committedState EvmState.init st').storage 0 = 0 := by have hrun : Run EVM.evm deadStoreRevert EvmState.init [] _ .halt := - Step.block (Step.seqCons + Step.block (D := EVM.evm) (Step.seqCons (Step.exprStmt (Step.builtinOk (Step.argsCons (Step.argsCons Step.argsNil Step.lit) Step.lit) rfl)) (Step.seqStop diff --git a/YulSemantics/Rewrites.lean b/YulSemantics/Rewrites.lean index c88e888..32dc6e1 100644 --- a/YulSemantics/Rewrites.lean +++ b/YulSemantics/Rewrites.lean @@ -135,7 +135,7 @@ theorem sstore_add_zero (x : Ident) : (.exprStmt (.builtin .sstore [.lit (.number 0), .var x])) := EquivStmt.exprStmt_congr (EquivExpr.builtin_congr EVM.Op.sstore - (EquivArgs.of_forall₂ (.cons (EquivExpr.refl _) (.cons (add_zero x) .nil)))) + (EquivArgs.of_forall₂ (D := EVM.evm) (.cons (EquivExpr.refl _) (.cons (add_zero x) .nil)))) /-- The same rewrite at the whole-program level, written in concrete syntax (the `x` here is the Yul identifier `"x"`). The `hoist` side condition is `rfl` — the rewrite touches no function