Import verified Lean4EVM primitives

[Vilin97]

What this adds

Import the public mrLSD/Lean4EVM MIT-licensed formalization as LeanPool.Lean4EVM. It provides reusable fixed-width unsigned integer and fixed-size byte primitives for Ethereum semantics, with proved wrapping arithmetic, shifts, signed operations, ADDMOD/MULMOD, byte extraction, sign extension, and checked width conversions.

Provenance and selection

• Upstream: https://github.com/mrLSD/Lean4EVM
• Exact imported commit: 0109646545bc1f29c719c1268bad7c561d2035f8
• MIT license; author: mrLSD; no AI disclosure or co-authored AI commit found
• Repository created 2026-09-05 and completed primitive API commit 2026-09-07, inside the run window
• Discovery evidence included authenticated Lean Zulip, X cache, GitHub repository/commit search, Reservoir, arXiv, and public web search

Scope and porting

Only the coherent proof-bearing primitive closure is imported (11 Lean modules, 3,538 lines); upstream test/audit harnesses and package tooling are excluded. Imports are namespaced under LeanPool.Lean4EVM, standard pool headers are retained, and the project card plus generated root entry are registered.

The port targets Lean Pool’s exact leanprover/lean4:v4.34.0-rc1 and pinned Mathlib. Three deprecated if_pos rewrites were replaced with ite_eq_left; zero-modulus branches in signed remainder, ADDMOD, and MULMOD were repaired for the current API. No theorem was weakened.

Trust and validation

• No sorry, admit, custom axioms, unsafe, partial, opaque, native decisions, diagnostics, broad imports, or option overrides in imported content
• Public headline declarations audit to the standard Lean axioms only
• lake build LeanPool.Lean4EVM passes warning-free
• lake exe mk_all --check, targeted runLinter, targeted lint-style, and forbidden-token scans pass
• Full lake build LeanPool completed successfully on the shared cached environment
• Repository quality audit is running against the final tree; its result will be added before merge

Compile measurements

Controlled candidate closure on the shared pool environment:

Build	Jobs	Wall	Peak RSS
Baseline before cleanup	917	12.56s	1,787,372 KB
After cleanup	917	6.8s	not separately sampled

The cleanup removes deprecated rewrites and repairs current-toolchain elaboration; no broad import or dependency fan-out was introduced.

[Vilin97]

Independent thorough review — approve

I reviewed the final diff, the upstream README/source at commit 0109646545bc1f29c719c1268bad7c561d2035f8, the MIT license, and the selected declarations.

• Faithfulness: the card names fixed-width arithmetic and byte primitives; the listed toNat_add, toNat_mul, toNat_addmod, toNat_mulmod, and toNat_byteAt_of_lt declarations prove exactly those contracts. No full-EVM or transaction-execution claim is made.
• Novelty and fit: this is a standalone, reusable pure-Lean EVM primitive layer, suitable for verified blockchain semantics and cslib-style reuse; it is not present in the pool or Mathlib.
• Significance: nominal U64/U128/U256 and H160/H256/Bytes32/Address types plus proved wrapping, signed, modular, shift, conversion, and byte laws provide a useful base for later EVM verification.
• Sources/license: public upstream URL, exact commit, MIT license, author, and human provenance are recorded. The eligible-window completion evidence is the repository creation (2026-09-05) and primitive API commit (2026-09-07).
• Engineering/trust: 11 proof-bearing modules (3,538 lines) are imported; tests/tooling are excluded. The port builds on the pool toolchain, has no forbidden constructs or option overrides, passes targeted linter/style and generated-index checks, and the measured cleanup reduced candidate closure wall time from 12.56s to 6.8s.

Verdict: approve. I found no material faithfulness, source, significance, or maintainability defect.

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 23.86 s (= 0.40 min) — user 25.93 s, sys 7.88 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 2,720 maxHeartbeats units across 12 files (3,566 added LOC).

Sum of lean --profile: 21052.8 ms (= 21.05 s). Import-excluded time: 10700.8 ms (= 10.70 s).

Count-heartbeats wall-clock total: 33.13 s. Repeated import cost inside lean --profile: 10352.0 ms (= 10.35 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/Lean4EVM/Primitives/UInt/Core.lean	950	1,264	3.73	3.76	2.94	0.82	159	0
LeanPool/Lean4EVM/Primitives/FixedBytes/Core.lean	397	311	3.28	2.30	1.42	0.88	62	0
LeanPool/Lean4EVM/Primitives/UInt/U256.lean	619	230	3.12	2.32	1.49	0.82	110	0
LeanPool/Lean4EVM/Primitives/FixedBytes/H256.lean	386	224	3.25	2.14	1.24	0.90	66	0
LeanPool/Lean4EVM/Primitives/FixedBytes/Bytes32.lean	303	206	2.46	1.69	0.78	0.91	57	0
LeanPool/Lean4EVM/Primitives/FixedBytes/H160.lean	244	182	2.60	1.54	0.66	0.87	45	0
LeanPool/Lean4EVM/Primitives/FixedBytes/Address.lean	269	135	2.55	1.59	0.71	0.88	49	0
LeanPool/Lean4EVM/Primitives/UInt/U128.lean	189	90	2.55	1.38	0.56	0.82	45	0
LeanPool/Lean4EVM/Primitives/UInt/U64.lean	146	78	2.20	1.26	0.43	0.83	39	0
LeanPool/Lean4EVM.lean	28	0	2.26	1.06	0.17	0.89	0	0
LeanPool/Lean4EVM/Primitives/FixedBytes.lean	20	0	2.62	1.05	0.15	0.90	0	0
LeanPool/Lean4EVM/Primitives/UInt.lean	15	0	2.51	0.96	0.14	0.83	0	0
Total	3,566	2,720	33.13	21.05	10.70	10.35	632	0

Aggregate phase totals

Phase	Time
import	10352.0 ms (= 10.35 s)
interpretation	3724.0 ms (= 3.72 s)
simp	1224.1 ms (= 1.22 s)
elaboration	1124.1 ms (= 1.12 s)
typeclass inference	972.9 ms (= 0.97 s)
tactic execution	957.7 ms (= 0.96 s)
tacticAnalysis	543.5 ms (= 0.54 s)
initialization	395.2 ms (= 0.40 s)
type checking	336.9 ms (= 0.34 s)
parsing	257.9 ms (= 0.26 s)
linting	255.1 ms (= 0.26 s)
compilation (LCNF base)	160.1 ms (= 0.16 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.Lean4EVM.Primitives.UInt.Core	6.10 s
LeanPool.Lean4EVM.Primitives.FixedBytes.Core	5.20 s
LeanPool.Lean4EVM.Primitives.FixedBytes.H256	2.30 s
LeanPool.Lean4EVM.Primitives.FixedBytes.Address	2.10 s
LeanPool.Lean4EVM.Primitives.UInt.U256	1.70 s
LeanPool.Lean4EVM.Primitives.FixedBytes.H160	1.60 s
LeanPool.Lean4EVM.Primitives.FixedBytes.Bytes32	1.40 s
LeanPool.Lean4EVM.Primitives.UInt.U64	1.30 s
LeanPool.Lean4EVM.Primitives.UInt.U128	1.20 s
LeanPool.Lean4EVM.Primitives.UInt	1.20 s
LeanPool.Lean4EVM.Primitives.FixedBytes	1.10 s
LeanPool.Lean4EVM	1.10 s

Per-file `lean --profile` output

LeanPool/Lean4EVM.lean

import took 889ms
cumulative profiling times:
	elaboration 0.278ms
	import 889ms
	initialization 34.5ms
	interpretation 129ms
	linting 0.473ms
	module linting 0.00109ms
	overlappingInstancesLinter 0.329ms
	parsing 0.0479ms
	tacticAnalysis 2.53ms
real 1.62
user 0.90
sys 0.75

LeanPool/Lean4EVM/Primitives/FixedBytes.lean

import took 897ms
cumulative profiling times:
	elaboration 0.169ms
	import 897ms
	initialization 35.8ms
	interpretation 117ms
	linting 0.304ms
	module linting 0.00135ms
	overlappingInstancesLinter 0.222ms
	parsing 0.0298ms
	tacticAnalysis 1.26ms
real 1.64
user 0.92
sys 0.74

LeanPool/Lean4EVM/Primitives/FixedBytes/Address.lean

import took 880ms
cumulative profiling times:
	attribute application 5.25ms
	blocked (unaccounted) 4.49ms
	compilation (IR) 0.775ms
	compilation (LCNF base) 12.3ms
	compilation (LCNF impure) 4.11ms
	compilation (LCNF mono) 8.36ms
	congr simp thm 2.01ms
	elaboration 71.9ms
	fix level params 0.405ms
	import 880ms
	initialization 34.7ms
	instantiate metavars 0.595ms
	interpretation 295ms
	let-to-have transformation 0.265ms
	linting 16.6ms
	module linting 0.00139ms
	overlappingInstancesLinter 8.28ms
	parsing 18.7ms
	process pre-definitions 7.88ms
	share common exprs 1.8ms
	simp 68.2ms
	tactic execution 42.6ms
	tacticAnalysis 37.6ms
	type checking 15.3ms
	typeclass inference 57.3ms
real 1.77
user 1.41
sys 0.77

LeanPool/Lean4EVM/Primitives/FixedBytes/Bytes32.lean

import took 909ms
cumulative profiling times:
	attribute application 9.06ms
	blocked (unaccounted) 0.65ms
	compilation (IR) 0.928ms
	compilation (LCNF base) 14.3ms
	compilation (LCNF impure) 4.51ms
	compilation (LCNF mono) 7.1ms
	congr simp thm 1.77ms
	elaboration 96.1ms
	fix level params 0.408ms
	import 909ms
	initialization 29.8ms
	instantiate metavars 0.682ms
	interpretation 334ms
	let-to-have transformation 0.263ms
	linting 19.7ms
	module linting 0.00122ms
	overlappingInstancesLinter 10.4ms
	parsing 22.2ms
	process pre-definitions 8.57ms
	share common exprs 2ms
	simp 71ms
	tactic execution 33.3ms
	tacticAnalysis 42.7ms
	type checking 14.6ms
	typeclass inference 54.9ms
real 1.85
user 1.48
sys 0.78

LeanPool/Lean4EVM/Primitives/FixedBytes/Core.lean

import took 883ms
cumulative profiling times:
	attribute application 7.41ms
	blocked (unaccounted) 12.7ms
	compilation (IR) 1.18ms
	compilation (LCNF base) 19.2ms
	compilation (LCNF impure) 6.05ms
	compilation (LCNF mono) 10.2ms
	congr simp thm 6.03ms
	elaboration 137ms
	fix level params 0.847ms
	import 883ms
	initialization 39.1ms
	instantiate metavars 1.45ms
	interpretation 382ms
	let-to-have transformation 0.422ms
	linting 29.4ms
	module linting 0.00133ms
	overlappingInstancesLinter 11ms
	parsing 30.3ms
	process pre-definitions 16.9ms
	share common exprs 4.47ms
	simp 331ms
	tactic execution 139ms
	tacticAnalysis 67.3ms
	type checking 32.3ms
	typeclass inference 136ms
real 1.99
user 2.12
sys 0.77

LeanPool/Lean4EVM/Primitives/FixedBytes/H160.lean

import took 874ms
cumulative profiling times:
	attribute application 5.98ms
	blocked (unaccounted) 0.806ms
	compilation (IR) 0.738ms
	compilation (LCNF base) 12.8ms
	compilation (LCNF impure) 3.54ms
	compilation (LCNF mono) 5.71ms
	congr simp thm 1.91ms
	elaboration 70.3ms
	fix level params 0.352ms
	import 874ms
	initialization 35.7ms
	instantiate metavars 0.526ms
	interpretation 293ms
	let-to-have transformation 0.209ms
	linting 16.9ms
	module linting 0.00135ms
	overlappingInstancesLinter 8.11ms
	parsing 14.5ms
	process pre-definitions 7.92ms
	share common exprs 1.46ms
	simp 52.2ms
	tactic execution 33.2ms
	tacticAnalysis 35.9ms
	type checking 12.7ms
	typeclass inference 48.3ms
real 1.77
user 1.38
sys 0.74

LeanPool/Lean4EVM/Primitives/FixedBytes/H256.lean

import took 899ms
cumulative profiling times:
	attribute application 8.81ms
	blocked (unaccounted) 0.853ms
	compilation (IR) 0.728ms
	compilation (LCNF base) 14ms
	compilation (LCNF impure) 4.43ms
	compilation (LCNF mono) 6.99ms
	congr simp thm 2.79ms
	elaboration 108ms
	fix level params 0.66ms
	import 899ms
	initialization 30.1ms
	instantiate metavars 1.1ms
	interpretation 379ms
	let-to-have transformation 0.393ms
	linting 25.9ms
	module linting 0.00162ms
	overlappingInstancesLinter 10ms
	parsing 27.5ms
	process pre-definitions 12.2ms
	share common exprs 3.61ms
	simp 69.2ms
	tactic execution 183ms
	tacticAnalysis 56.4ms
	type checking 118ms
	typeclass inference 176ms
real 1.99
user 1.94
sys 0.79

LeanPool/Lean4EVM/Primitives/UInt.lean

import took 826ms
cumulative profiling times:
	elaboration 0.145ms
	import 826ms
	initialization 29.4ms
	interpretation 104ms
	linting 0.293ms
	module linting 0.00166ms
	overlappingInstancesLinter 0.764ms
	parsing 0.03ms
	tacticAnalysis 0.78ms
real 1.54
user 0.87
sys 0.68

LeanPool/Lean4EVM/Primitives/UInt/Core.lean

import took 820ms
cumulative profiling times:
	attribute application 33.2ms
	blocked (unaccounted) 124ms
	compilation (IR) 3.44ms
	compilation (LCNF base) 36ms
	compilation (LCNF impure) 19.5ms
	compilation (LCNF mono) 40.5ms
	congr simp thm 10.2ms
	elaboration 419ms
	fix level params 2.34ms
	import 820ms
	initialization 28.7ms
	instantiate metavars 2.5ms
	interpretation 709ms
	let-to-have transformation 1.22ms
	linting 75.6ms
	module linting 0.00173ms
	overlappingInstancesLinter 59.4ms
	parsing 69.8ms
	process pre-definitions 33.6ms
	share common exprs 11.3ms
	simp 477ms
	tactic execution 227ms
	tacticAnalysis 156ms
	type checking 94.9ms
	typeclass inference 310ms
real 2.36
user 3.50
sys 0.79

LeanPool/Lean4EVM/Primitives/UInt/U128.lean

import took 825ms
cumulative profiling times:
	attribute application 2.98ms
	blocked (unaccounted) 6.44ms
	compilation (IR) 0.848ms
	compilation (LCNF base) 10.8ms
	compilation (LCNF impure) 3.94ms
	compilation (LCNF mono) 6.1ms
	congr simp thm 1.12ms
	elaboration 43.3ms
	fix level params 0.289ms
	import 825ms
	initialization 38.3ms
	instantiate metavars 0.466ms
	interpretation 255ms
	let-to-have transformation 0.167ms
	linting 14.6ms
	module linting 0.00151ms
	overlappingInstancesLinter 7.98ms
	parsing 15.1ms
	process pre-definitions 6.95ms
	share common exprs 1.23ms
	simp 29.4ms
	tactic execution 46.5ms
	tacticAnalysis 29.9ms
	type checking 8.22ms
	typeclass inference 27.4ms
real 1.69
user 1.26
sys 0.73

LeanPool/Lean4EVM/Primitives/UInt/U256.lean

import took 822ms
cumulative profiling times:
	attribute application 9.24ms
	blocked (unaccounted) 0.383ms
	compilation (IR) 1.64ms
	compilation (LCNF base) 31.6ms
	compilation (LCNF impure) 7.76ms
	compilation (LCNF mono) 13.7ms
	congr simp thm 3.74ms
	elaboration 140ms
	fix level params 1.17ms
	import 822ms
	initialization 30.3ms
	instantiate metavars 1.65ms
	interpretation 499ms
	let-to-have transformation 0.606ms
	linting 44.1ms
	module linting 0.00132ms
	overlappingInstancesLinter 15.8ms
	parsing 47.5ms
	process pre-definitions 20ms
	share common exprs 6.17ms
	simp 117ms
	tactic execution 239ms
	tacticAnalysis 85.6ms
	type checking 36.3ms
	typeclass inference 141ms
real 1.95
user 2.19
sys 0.75

LeanPool/Lean4EVM/Primitives/UInt/U64.lean

import took 828ms
cumulative profiling times:
	attribute application 2.31ms
	compilation (IR) 0.799ms
	compilation (LCNF base) 9.12ms
	compilation (LCNF impure) 3.8ms
	compilation (LCNF mono) 5.91ms
	congr simp thm 0.349ms
	elaboration 37.9ms
	fix level params 0.216ms
	import 828ms
	initialization 28.8ms
	instantiate metavars 0.331ms
	interpretation 228ms
	let-to-have transformation 0.14ms
	linting 11.2ms
	module linting 0.00132ms
	overlappingInstancesLinter 7.12ms
	parsing 12.2ms
	process pre-definitions 5.45ms
	share common exprs 0.959ms
	simp 9.13ms
	tactic execution 14.1ms
	tacticAnalysis 27.5ms
	type checking 4.59ms
	typeclass inference 22ms
real 1.64
user 1.12
sys 0.74

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

The PR appears safe to merge; no outstanding correctness, catalog, provenance, security, or repository-rule issue was identified.

Summary

This PR imports a selected, proof-bearing portion of Lean4EVM containing fixed-width unsigned integers and nominal fixed-size byte types.

• Adds wrapping arithmetic, shifts, signed operations, modular arithmetic, byte extraction, sign extension, serialization, and checked conversions.
• Registers LeanPool.Lean4EVM as the project boundary and adds it to the aggregate import surface.
• Aligns the project card’s headline results with their exact Lean declarations.
• Preserves explicit source revision, authorship, license, and selected-import scope.

_{Reviews (41) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

Changes requested by automated review

Reviewed exact head 4c0edbd8dd84e0f8280c5ddfda1954174a8037cb.

1. Project card misstates the BYTE theorem. Lean4EVM.U256.toNat_byteAt_of_lt proves the exact big-endian extraction formula; the < 256 bound is proved by Lean4EVM.U256.byteAt_toNat_lt. Update the main_results informal in LeanPool/projects.yml to describe the exact extraction formula (and, if desired, mention the separate bound theorem).
2. Required quality gate fails at this head. The CI Build pool/Build project run reports axiom audit produced no result for declarations whose names contain ? (for example Address.ofByteArray?_toByteArray and U128.toU64?) and reports the project card out of date. Make the exact-head repository quality audit pass without changing or weakening its gates, then rerun the protected checks.

The project remains changes requested until both blockers are resolved.

[Vilin97]

Changes requested by automated review

Reviewed exact current head d8cbed919e7910b32b79a79283ff676e025f3f44 after the automatic branch refresh.

1. Card still overclaims the BYTE theorem. Lean4EVM.U256.toNat_byteAt_of_lt proves the exact big-endian extraction formula; the < 256 bound is Lean4EVM.U256.byteAt_toNat_lt. Update the main_results informal to state the extraction formula (and optionally mention the separate bound theorem).
2. Protected validation is incomplete. Build pool and documentation checks are pending at this head. Keep the PR in changes-requested status until the card is corrected and the exact-head required checks finish green.

The prior quality-audit blocker appears resolved in the rebased tree, but it must be confirmed by the pending build.

[Vilin97]

Automated review: repairs pushed; needs-maintainer for review access

Reviewed final head 3fff8ca01bf63d9e13b026b9a71efbf837e4f572. The previous author-actionable blockers are repaired:

• Optional conversions and their theorem families now consistently use Opt names. The old parser truncated names at ?, leaving 37 unresolved axiom queries and silently auditing wrapping conversions for some other optional names. All 557 public declaration closures now resolve and pass the existing axiom audit; the compiled environment/backdoor audit passes. No audit or linter implementation was changed.
• The BYTE result now states the exact big-endian extraction formula. The generated card selects ADDMOD/MULMOD as its two headline links to satisfy the existing card format and line limit; all five advertised results remain in main_results, are preserved, and resolve successfully.
• Both safe main refreshes were merged into the isolated repair worktree. The implementation diff reverses byte-for-byte to the original source by the six name substitutions alone, establishing that this repair did not change executable definitions, hypotheses or proof bodies.

Validation: warning-free lake --wfail build LeanPool.Lean4EVM (917 jobs), project environment linters, generated-index check, project card/metadata and all five result declarations, 557 axiom closures and compiled trust audit. Baseline/repaired full project recompilation was 14.29/7.50 s with warm dependencies and similar peak RSS (~1.79 GB); different filesystem cache warmth means this is not a claimed performance improvement. The broad local metadata check could not resolve 191 unrelated projects whose oleans were not built in this isolated worktree; full repository CI remains the final gate.

Independent review: faithful, nonvacuous fixed-width/byte/EVM arithmetic endpoints; reusable shared BitVec representation and serialization proofs; substantial primitives library without claiming a complete EVM verifier. The existing generic proof factoring and width-specific modules are maintainable; this review finds no remaining concrete quality defect (4/5 assessment). The upstream scope and attribution are retained.

A fresh configured LLM review was requested, but GitHub returned HTTP 422: Cannot trigger a 'workflow_dispatch' on a disabled workflow. No fresh configured review ran. Final-head protected CI and Greptile are pending, and repository auto-merge is disabled. Apply needs-maintainer for restoring the existing review route and completing protected merge after the final-head checks; the old change-request blockers are superseded by these repairs. No workflow, policy, protection, resource limit or linter configuration was altered.

[Vilin97]

Daily maintainer cycle: repaired the upstream MIT attribution at 6d6129a5cc6ff1ed9806b54f8c1eb8597f97dd67.

The pinned upstream LICENSE names Copyright (c) 2026 Evgeny Ukhanov. That original notice was absent from both the imported project and this head's root NOTICE. Commit 6d6129a5c preserves the complete upstream copyright, permission and disclaimer verbatim in LeanPool/Lean4EVM.lean, without mixing infrastructure into this content PR.

Validation: warning-free lake --wfail build LeanPool.Lean4EVM (917 jobs), mk_all --check, project style, metadata/card and advertised declaration checks, all 557 public axiom closures, compiled trust audit, and git diff --check passed. Comment-stripped code tokens are identical. I re-reviewed the pushed commit and verified the remote head.

Retain needs-maintainer for the existing configured-review access boundary: LLM Review is still disabled_manually. Restore that route or explicitly decide how to satisfy the review requirement; all three protected checks have now passed on this repaired head. The attribution defect is fixed; no gate or protection was changed.

2026-09-17 exact-head reconciliation: Reviewed eed43b39ad2cb480aa7cfdb2b0f1e317349418ab. The complete old-to-new diff contains only the six polynomial restricted-sum files already reviewed and merged in #441; every refreshed file matches main at 7027ddb4a01421f61ac44811e6ca55a0bf020e4e. The submitted project/proofs, parsed metadata, and relevant tooling are unchanged. The substantive findings and needs-maintainer disposition above therefore persist at this SHA. New protected CI is pending; previous-head successes are not current-head approval. The meaningful quality repairs already recorded remain intact; the configured five-rubric workflow is still disabled manually, so review-access/remaining quality judgment needs a maintainer.

[Vilin97]

Automated cycle 2026-09-17: precise maintainer decision at eed43b39ad2cb480aa7cfdb2b0f1e317349418ab

The review-access boundary recorded above is no longer the reason to hold this PR: since the configured LLM review workflow was disabled on 2026-09-13, the repository has merged on thorough agentic review (#431, #434), and other labeled imports were merged on that basis this cycle. What remains here is one significance/fit decision that an independent exact-head verification this cycle surfaced, and which a maintainer should settle rather than automation:

• The import is a fixed-width integer and byte-string wrapper library over BitVec (316 theorems, 233 definitions, 55 proofs closed by bare rfl), and it has no headline theorem in the significance rubric's sense. Three of the five advertised results unfold definitions already written in Nat arithmetic: U256.lean:189 def addmod a b modulus := if modulus = 0 then 0 else ofNat ((a.toNat + b.toNat) % modulus.toNat) against U256.lean:544 toNat_addmod : (addmod a b modulus).toNat = if modulus = 0 then 0 else (a.toNat + b.toNat) % modulus.toNat (likewise mulmod, byteAt); the other two, FixedUInt.toNat_add/toNat_mul, are one-line transports of BitVec.toNat_add/toNat_mul through a one-field newtype.
• The upstream tree at the imported commit (2026-09-06, repository created 2026-09-05) contains only Primitives/; no interpreter, opcode semantics, state, or gas model exists, so the card's title "Verified Ethereum Virtual Machine primitives" is accurate but its branch: verified systems and blockchain semantics overstates the content.
• Faithfulness, attribution (MIT, Evgeny Ukhanov, notice retained), provenance: human, forbidden-construct scan, and duplicate search are all clean; candidates/CRITERIA.txt admits data-structure libraries and the project clears the 250-line floor at 3,538 lines. The question is purely whether a BitVec newtype API without a theorem meets the pool's "serious formalization" bar.

If the maintainer accepts the library on the data-structure clause, the only change requested is the branch wording; if not, the PR should be closed with the same explanation. Retaining needs-maintainer for that decision.

Disposition: needs-maintainer — independently reviewed c14616a17b46c35f218d221a7e6835de73e6f443.

Genuine borderline fit: criteria admit data-structure libraries, but this is a BitVec wrapper API without an independent headline theorem. ADDMOD/MULMOD and byteAt statements match their explicit Nat definitions; other arithmetic claims transport BitVec results through a one-field wrapper. No interpreter, state, gas or transaction semantics in the imported closure. MIT/Evgeny Ukhanov notice and human provenance checked. Overlap with Mathlib BitVec is substantive; no separate prior import found.

Prior audit-name and MIT-notice repairs remain. All initial-head required CI/trust gates pass. Maintainer must accept under the data-structure clause or decline for insufficient independent substance; if accepted, narrow branch metadata from blockchain semantics to fixed-width primitives. No new concrete proof defect established.

Absolute advisory build 23.86 s; serial profile 21.05 s. Prior controlled cleanup 12.56 → 6.8 s; not remeasured here.

Final-head reconciliation: the main refresh contains the already-reviewed Komlós import/Burkholder refactor and generated metadata. This PR’s own proof/tooling files are unchanged by that refresh. Fresh checks on refreshed heads remain the required gate; earlier successful runs are historical evidence, not an approval of pending CI. Repository auto-merge remains disabled. The linked disposition is the final action; no protection or workflow setting was changed.

2026-09-20 reconciliation: needs-maintainer at 390e3fe0f2687872c68c190e6c7b8436b7e5ecea.

The metadata is now accurately narrowed to fixed-width primitives and byte representations. Prior name-audit and MIT-attribution repairs remain; initial full CI/trust passes. Human decision remains: accept under the data-structure-library clause or decline for insufficient independent substance. No interpreter/state/gas/transaction verification is claimed. Quality 4/5 does not resolve this significance question.

Primitive infrastructure only, not a completed EVM verification. Significance does not transfer from Ethereum; acceptance remains explicitly undecided.

The current own-project/tooling files were compared with the reviewed content; later main-only refreshes do not change the conclusion. Current required CI and final head are recorded separately from historical green runs.

[Vilin97]

2026-09-18 exact-head reconciliation: Reviewed 7caca7c7a4 (auto-rebase merge of main). LeanPool/Lean4EVM/** and the parsed registry card are byte-identical to the last reviewed head eed43b39ad; the only differences are main's new imports, generated index/metadata, and the v4.34.0 toolchain bump, under which Build project, separation, and documentation preflight are green on the synced head. Nothing in the diff changes the open question, so needs-maintainer persists with the same decision: accept a BitVec newtype API without a headline theorem under the data-structure clause of candidates/CRITERIA.txt (then only the branch wording changes), or close.

Needs-maintainer resolution job, 2026-09-18 ~18:00 UTC (head b2b2013e, auto-rebase after #432/#433/#450): LeanPool/Lean4EVM/** and the parsed card are still byte-identical to eed43b39; the only differences are main's new cards, generated index/metadata, and the CI workflow changes from #450. The required checks are re-running on the synced head (Greptile already green). Nothing in the diff changes the open question, so needs-maintainer persists with the same decision: accept a BitVec newtype API without a headline theorem under the data-structure clause of candidates/CRITERIA.txt (then only the branch wording changes), or close.

[Vilin97]

Needs-maintainer cycle: reviewed fd55f0b2e61c4ebd002150a82cda083d9b10d51e after the fast-forward repair.

fd55f0b2e corrects the remaining scope overclaim in LeanPool/projects.yml and regenerates LeanPool/Lean4EVM.lean: the branch and tag now describe fixed-width arithmetic and byte representations; the entry documentation explicitly distinguishes that primitive API from an interpreter, machine state, gas accounting or transaction semantics. The pinned upstream tree and the actual FixedUInt/U256 definitions support this narrower description. All comment-stripped Lean tokens and theorem statements are unchanged; the upstream MIT notice is retained.

Validation in an isolated worktree: warning-free 923-job project build, generated-index check, Mathlib/style linters, scoped static and registry/card checks, all 557 public axiom closures and the compiled option/backdoor audit pass. Fresh remote CI is pending; earlier-head CI is not approval of this commit.

Retain needs-maintainer solely for the existing fit decision: does this substantial BitVec wrapper/byte API qualify under the data-structure clause despite lacking an independent headline theorem? The metadata repair is complete and need not wait for that decision. This review does not decide acceptance or authorize a gate bypass.

[Vilin97]

Daily needs-maintainer cycle: reviewed repaired head d8fe28b704dc80206bfd24b596834c1e4154f679.

Pushed a fast-forward repair in Primitives/UInt/Core.lean and Primitives/UInt/U256.lean: FixedUInt.toNat_ofNat_mod now supplies the shared residue-range proof used by ADDMOD and MULMOD. The operation definitions and zero-modulus branches are unchanged. The new helper derives positivity from word injectivity and bounds the residue by the word width; neither caller gains an assumption.

Validation at this head: warning-free project build; generated-index check; Mathlib and style linters over all project modules; scoped repository quality checks; axiom audit of all 558 public declarations and option-backdoor audit. Comparison against the previous head found identical types, universes, and safety settings for all 557 existing public declarations. Remote CI for this new commit must still complete; earlier green checks belong to the previous head.

needs-maintainer remains: the outstanding decision is whether this verified fixed-width data-structure/primitive API satisfies the repository's significance and inclusion criteria. The narrowed metadata and MIT attribution remain accurate, but the proof factoring does not supply a new independent headline result. Maintainer acceptance or rejection of that fit is still needed; this is a comment review, not approval.

[Vilin97]

Recommend closing for insufficient independent mathematical or verification content. Reviewed commit d8fe28b704dc80206bfd24b596834c1e4154f679.

The current scope and proofs are honest, and the previous BYTE wording, optional-name audit and MIT-attribution defects are repaired. Build project, separation and documentation preflight passed on the reviewed pre-refresh head. The remaining issue is the project's fit with the significance rubric.

The five advertised results are primitive API laws. FixedUInt.toNat_add and toNat_mul (Primitives/UInt/Core.lean:528,549) unfold the wrapper and finish by rfl after toBitVec_ofBitVec. U256.addmod and mulmod (Primitives/UInt/U256.lean:189,193) are defined by the exact natural-number residue formulas that toNat_addmod and toNat_mulmod restate; the additional proof is that the residue fits the word width. byteAt similarly implements the extraction formula directly. These are useful interface contracts, but they do not supply a substantive independent headline result.

I also checked the material beyond the card: FixedUInt.toBitVec_pow proves a basic binary-exponentiation recurrence, and FixedBytes proves bounds, injectivity and round trips for an elementary base-256 codec. Those complete the primitive library but do not change its significance level. The data-structure domain listed in the candidate criteria makes the subject eligible; it does not remove the review rubric's requirement for a significant completed result. This conclusion concerns the present import, not the quality or potential usefulness of the upstream library.

A later submission with a substantial verified algorithm, executable semantics refinement, or program-level correctness theorem would give the project an appropriate headline. Reaching that point is more than a small pre-merge edit, so I recommend closing this PR rather than continuing a metadata-only repair cycle.

Final reconciliation: the current head 68395a5cca7d7ffac08c38fe3e62aae298abf3d9 preserves the reviewed Lean4EVM files byte-for-byte. I am closing this PR on the significance finding above; the later main refresh does not change that finding. GitHub receives this as a comment review because the authenticated account authored the PR.