Skip to content

evm proof checker updates #174

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
nomeata merged 7 commits into from
Aug 29, 2026
Merged

evm proof checker updates #174

Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
a8e2318
feat:proof checker in solidity
FawadHa1der Jun 17, 2026
4de0197
chore: resolve conflict on ecmlean.yaml
FawadHa1der Aug 14, 2026
838442a
evm proof chcker updates to include nested inductives
FawadHa1der Aug 14, 2026
03177e0
Merge branch 'master' of github.com:leanprover/lean-kernel-arena
FawadHa1der Aug 18, 2026
3af9ddb
fix: more kernel arena test coverage
FawadHa1der Aug 18, 2026
fe5c869
more test coverage for evm rpoof checker
FawadHa1der Aug 28, 2026
860491e
Merge branch 'master' of github.com:leanprover/lean-kernel-arena
FawadHa1der Aug 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions checkers/evmlean.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,21 +23,21 @@
description: |
A Lean 4 kernel implemented in Solidity and executed on the Ethereum
Virtual Machine. Accepting a proof is a metered EVM execution; the same
call can be replayed on any EVM chain (61.5KB deployed — over today's
call can be replayed on any EVM chain (61.6KB deployed — over today's
EIP-170 limit, sized for the 64KiB raise on the Glamsterdam track, so it
needs a devnet/L2 with a raised code-size limit to deploy for real).

Checks inductive families including multi-type mutual groups and nested
inductives, projections, quotients, Nat and String literals. Gets all ten of the Arena's
static tests right: the eight adversarial ones are rejected at the
inductives, projections, quotients, Nat and String literals. Gets all twelve of the Arena's
static tests right: the ten adversarial ones are rejected at the
offending declaration, and the two that are actually valid
(level-index-out-of-order, sparse-name-index) are accepted. Declines unsafe/partial declarations and any export beyond
its resource budget; resource exhaustion is reported as a decline rather
than as a wrong verdict or a checker fault.
version: "0.3.0"
version: "0.4.0"
url: https://github.com/FawadHa1der/evm_proof_checker
ref: main
rev: 47368a1541bb96dc8ed10059ed82fbfb55e52d7b
rev: 1cb438894e50abf9b5293d33da5e0a2001519c06
build: npm install --no-audit --no-fund && node tools/build.js
run: node bin/evmlean.js $IN
# Module-scale exports exceed the per-run gas budget by orders of magnitude —
Expand Down