Trust reduction: eliminate the keccak256 selector axiom via kernel-computable Keccak-256

[Th0rgal]

Summary

Verity currently has 2 Lean axioms. This issue proposes a concrete path to eliminate axiom #1 (keccak256_first_4_bytes) and evaluate options for axiom #2 (solidityMappingSlot_lt_evmModulus).

---

Current axioms

Axiom 1: keccak256_first_4_bytes (Selectors.lean:41)

axiom keccak256_first_4_bytes (sig : String) : Nat

Purpose: Computes bytes4(keccak256(signature)) for ABI function dispatch.

Current mitigation: CI cross-checks against solc --hashes and selector fixtures. Low risk, but it is still an axiom in the proof kernel.

Axiom 2: solidityMappingSlot_lt_evmModulus (MappingSlot.lean:125)

axiom solidityMappingSlot_lt_evmModulus (baseSlot key : Nat) :
    solidityMappingSlot baseSlot key < Compiler.Constants.evmModulus

Purpose: Asserts keccak256 output fits in 256 bits. Mathematically trivially true (keccak256 produces exactly 32 bytes) but unprovable because the FFI call is opaque.

---

Proposed elimination path for axiom 1

Hi Thomas,

I was looking into Verity's architecture and noticed the need for a project-specific axiom to model Keccak-256 function selectors.
I actually just built a solution that might let you eliminate it: https://github.com/AlexeyMilovanov/lean-keccak-unrolled

It's a kernel-computable Keccak-256 engine. By unrolling the permutation into a static circuit, it completely bypasses
the Lean elaborator's memory limits, allowing you to compute and prove EVM selectors at compile-time.
The architectural approach builds upon the elaborator limitations discussed over at https://github.com/gdncc/Cryptography.

By the way, out of curiosity --- who's that in your avatar?
Best,
Alexey.

Integration approach

If lean-keccak-unrolled works as described, the integration would be:

1. Add as a Lake dependency — import the Keccak namespace
2. Replace the axiom with a def — compute keccak256_first_4_bytes as a kernel-computable function rather than an axiom
3. Prove selector values at compile time — each function selector becomes a native_decide or decide proof rather than an axiom-backed constant
4. Remove CI cross-check dependency — selector validation becomes a proof obligation, not a CI script. The CI scripts can remain as belt-and-suspenders but are no longer load-bearing.

Validation steps before integration

• Verify lean-keccak-unrolled compiles against the same Lean toolchain (check lean-toolchain compatibility)
• Benchmark: confirm selector computation stays under reasonable elaboration time (the unrolled circuit approach should be fast, but verify on Verity's actual selector set)
• Confirm output matches solc --hashes for all current contract selectors
• Confirm no new axioms are introduced by the dependency

---

Options for axiom 2

Axiom 2 is harder because it's about the FFI keccak256 output bound, not selector computation. Options:

Approach	Effort	Outcome
A. Use lean-keccak-unrolled for mapping slots too	Medium	If keccak256 is kernel-computable, solidityMappingSlot can be a def and the bound is provable from the output type
B. Wrap the FFI call with a length check	Low	Replace axiom with a runtime assertion + if guard. Not a proof, but removes the axiom.
C. Accept as permanent	None	Document as "same trust class as Solidity/EVM" — the axiom states something that is trivially true about 32-byte hash outputs

Recommendation: Try approach A first. If lean-keccak-unrolled can compute arbitrary keccak256 (not just 4-byte selectors), both axioms can be eliminated in one integration.

---

Impact

Eliminating both axioms would make Verity's proof stack axiom-free (modulo the Lean kernel itself), which is a significant trust reduction milestone. The AXIOMS.md file would become a historical document rather than an active trust surface.