Narrow the two bare import Mathlib to the modules actually used

YulSemantics/Adequacy.lean

@@ -1,3 +1,4 @@
+import Mathlib.Data.Nat.Basic
 import YulSemantics.BigStep
 import YulSemantics.Interp
 import YulSemantics.Dialect.EVM

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

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

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 :=

YulSemantics/FibExample.lean

@@ -1,3 +1,4 @@
+import Mathlib.Data.Nat.Fib.Basic
 import YulSemantics.Interp
 import YulSemantics.Syntax
 import YulSemantics.BigStep

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))

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

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