Narrow the two bare import Mathlib to the modules actually used

[leonardoalt]

Summary

YulSemantics/Dialect/EVM.lean and YulSemantics/Basic.lean each had a bare import Mathlib. Every Lean module's initialize_<Module> calls the initializer of each module it imports, and that is a real symbol reference the linker cannot discard, so one bare import Mathlib anywhere in a downstream executable's import closure keeps all ~8,200 Mathlib object files alive at link time.

Dialect.EVM is in the import closure of the yulc executable in powdr-labs/yul-compiler, so it alone accounted for the entire drag. Measured there with this change plus the companion downstream PR (ordinary runnable link, no --unresolved-symbols games):

	bytes	objects in yulc.rsp
before	165,277,392	8,724
after	134,841,520	1,112
delta	-30,435,872 (-29.0 MiB, -18.4%)	-7,612

This library's own lake build graph drops from 8,578 jobs to 884.

Changes

• Dialect/EVM.lean: import Mathlib -> import Mathlib.Tactic.SplitIfs, the only Mathlib entry point the metatheory needs after the earlier EVMOp/EVMExec split. The set_option linter.unnecessarySeqFocus false in on effects_sound_withExternal is no longer needed and is dropped.
• Basic.lean: import Mathlib -> import Std.Tactic.BVDecide. bv_decide is a Std tactic; nothing in the file needed Mathlib.
• 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₂.

Why the (D := evm) annotations are needed

Step and EquivArgs take [DecidableEq D.Value], and these proof terms are elaborated before the expected type fixes D. With Mathlib in scope, DecidableEq (Dialect.Value ?D) was inconclusive rather than failing: LinearOrder.toDecidableEq and the long chain below it leave 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. The proof terms themselves are unchanged.

One statement change, called out explicitly

EvmState.selfdestructs : List (U256 × Bool), so in the finishSelfdestruct test fixture in EVM.lean the expected [0x10] was elaborating through Mathlib's boolean-ring NatCast Bool into [(16, false)]. It is now written [(0x10, false)] directly. This was verified equal to the old elaboration (([0x10] : List (U256 × Bool)) = [(16, false)] closes by decide) before the import was removed. No tactic block, definition or proof term changed anywhere in this PR.

Testing

• lake build: passes (8,578 jobs -> 884).
• lake lint (the batteries/runLinter driver CI uses): passes.
• Integrated against powdr-labs/yul-compiler in the companion draft PR Point yul-semantics at the Mathlib-narrowed rev; 29 MB off yulc yul-compiler#138, with this exact commit as the pinned rev: full lake build, lake build yulc, the axiom check (Checks.lean), the spec-closure check (SpecClosure.lean), the YulIR round-trip, and the four Solidity corpora (syntax / interpreter / optimizer / object-compiler / EVM-code-transform) all pass, with no change in pass or known-failure counts.

Notes

Downstream consumers that were getting Mathlib lemmas and tactics transitively through YulSemantics.Dialect.EVM will need to add narrow imports of their own; powdr-labs/yul-compiler#138 is the worked example.

🤖 Generated with Claude Code