EVM Intrinsics (evm::)
The evm:: namespace exposes EVM-specific primitives. It is always in scope on
the EVM target. Only the seven intrinsics below exist; any other evm:: name
is rejected. The Lean model covers just evm::keccak256Packed (1–4 arguments)
and evm::ecrecover. evm::sha256, evm::ripemd160, evm::balance, and
evm::blockhash are rejected when compiling for Lean, and evm::keccak256 is
EVM-only as well.
Pure intrinsics
Usable inside pure fn bodies as well as routes:
| Intrinsic | Returns | Lowers to |
|---|---|---|
evm::ecrecover(hash, v, r, s) | address | ecrecover(...) (address(0) on bad signature) |
evm::keccak256(x) | U256 | uint256(keccak256(abi.encode(x))) |
evm::keccak256Packed(a, b, ...) | U256 | uint256(keccak256(abi.encodePacked(a, b, ...))) |
evm::sha256(a, ...) | U256 | uint256(sha256(abi.encodePacked(a, ...))) |
evm::ripemd160(a, ...) | U256 | ripemd160(abi.encodePacked(a, ...)), widened to uint256 |
evm::keccak256 is not yet accepted inside a pure fn; call it from a route
or member transform.
Impure intrinsics
Read live account or block context — not allowed inside pure fn (V4):
| Intrinsic | Returns | Lowers to |
|---|---|---|
evm::balance(addr) | U256 | addr.balance |
evm::blockhash(n) | U256 | uint256(blockhash(n)) |
Example (signed permit)
entity Permits {
error Expired();
error BadSignature();
routes {
permit(owner: address, value: U256, deadline: U256, v: u8, r: bytes32, s: bytes32)
where sys::timestamp <= deadline : throw Expired()
&& evm::ecrecover(
evm::keccak256Packed(owner, value, deadline, m_nonces[owner]),
v, r, s
) == owner : throw BadSignature()
=> []
}
m_nonces: HashMap<address, U256> {
in permit(owner, _, _, _, _, _) => m_nonces.insert(owner, m_nonces[owner] + 1)
}
}
ecrecover accepts the U256 digest directly (it is cast to bytes32 in the
generated Solidity). A production permit would hash an EIP-712 domain and
struct; the shape of the check is the same.
Portable digests
For a digest that must mean the same thing on EVM and in the Lean model, use
evm::keccak256Packed. evm::keccak256, evm::sha256, and
std::crypto::sha256 are EVM-only.