This document describes the feature coverage of Verity's reference interpreters, the EVMYulLean builtin bridge, and their proof status.
Machine-readable version: artifacts/interpreter_feature_matrix.json.
| Interpreter | File | Entry Point | Purpose |
|---|---|---|---|
| IRInterpreter | Compiler/Proofs/IRGeneration/IRInterpreter.lean |
execIRStmts |
Layer-2 preservation proofs |
| EVMYulLean bridge | Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean |
evalBuiltinCallViaEvmYulLean |
Pure builtin evaluation via EVMYulLean UInt256 |
The old YulSemantics fuel-based executor was removed as part of the EVMYulLean transition (DoD-5); the native EvmYulLean dispatcher is now the sole runtime authority.
The old SpecInterpreter module has been removed. Source semantics now live in
Verity/Core.lean, with the supported whole-contract Layer-2 source-side model
assembled in Compiler/Proofs/IRGeneration/SourceSemantics.lean. This matrix
keeps the legacy Spec (basic) / Spec (fuel) column names, and the
machine-readable artifact keeps SpecInterpreter_* keys, for compatibility
with the existing sync scripts and boundary checks.
| Feature | Constructor | Spec (basic) | Spec (fuel) | IR | EVMYulLean | Proof |
|---|---|---|---|---|---|---|
| Literals | Expr.literal |
ok | ok | ok | -- | proved |
| Parameters | Expr.param |
ok | ok | -- | -- | proved |
| Constructor args | Expr.constructorArg |
ok | ok | -- | -- | proved |
| Storage read | Expr.storage |
ok | ok | ok | -- | proved |
| Mapping read | Expr.mapping |
ok | ok | ok | -- | proved |
| Mapping + word offset | Expr.mappingWord |
ok | ok | -- | -- | proved |
| Packed mapping | Expr.mappingPackedWord |
ok | ok | -- | -- | proved |
| Double mapping | Expr.mapping2 |
ok | ok | -- | -- | proved |
| Double mapping + word | Expr.mapping2Word |
ok | ok | -- | -- | proved |
| Uint256-keyed mapping | Expr.mappingUint |
ok | ok | -- | -- | proved |
| Struct member (single) | Expr.structMember |
ok | ok | -- | -- | proved |
| Struct member (double) | Expr.structMember2 |
ok | ok | -- | -- | proved |
caller |
Expr.caller |
ok | ok | ok | ok | proved |
msg.value |
Expr.msgValue |
ok | ok | ok | -- | proved |
address(this).balance / selfbalance() |
Expr.selfBalance |
ok | ok | -- | -- | partial |
block.timestamp |
Expr.blockTimestamp |
ok | ok | ok | -- | proved |
block.number |
Expr.blockNumber |
0 | 0 | ok | -- | partial |
address(this) |
Expr.contractAddress |
0 | 0 | ok | ok | partial |
chainid |
Expr.chainid |
0 | 0 | ok | -- | partial |
mload |
Expr.mload |
0 | 0 | ok | -- | partial |
returndataOptionalBoolAt |
Expr.returndataOptionalBoolAt |
0 | 0 | -- | -- | partial |
keccak256 |
Expr.keccak256 |
0 | 0 | -- | -- | n/m |
call |
Expr.call |
0 | 0 | -- | -- | n/m |
staticcall |
Expr.staticcall |
0 | 0 | -- | -- | n/m |
delegatecall |
Expr.delegatecall |
0 | 0 | -- | -- | n/m |
| Arithmetic | add/sub/mul/pow/div/mod |
ok | ok | ok | ok | proved |
| Bitwise | and/or/xor/shl/shr |
ok | ok | ok | ok | proved |
| Bitwise | not |
ok | ok | ok | ok | partial |
| Comparison | eq/lt/gt/le/ge |
ok | ok | ok | ok | proved |
| Logical | logicalAnd/Or/Not |
ok | ok | -- | -- | proved |
| Fixed-point math | mulDivDown/Up, wMulDown/wDivUp, min/max |
ok | ok | -- | -- | proved |
| Full-precision mulDiv modeling | mulDiv512Down?/Up? |
-- | -- | -- | -- | EDSL/proof helper |
| Internal call (expr) | Expr.internalCall |
0 | ok | -- | -- | proved |
| Local variable | Expr.localVar |
ok | ok | ok | -- | proved |
| External call (linked) | Expr.externalCall |
ok | ok | -- | -- | assumed |
| Array length | Expr.arrayLength |
ok | ok | -- | -- | proved |
| Array element | Expr.arrayElement |
ok | ok | -- | -- | proved |
| Dynamic struct-array head word | Expr.arrayElementDynamicWord |
0 | 0 | -- | -- | n/m |
| Direct dynamic-struct param head word | Expr.paramDynamicHeadWord |
0 | 0 | -- | -- | n/m |
Legend: ok = supported, 0 = returns 0 (not modeled), del = delegated to Verity path, -- = not applicable at this layer, n/m = not modeled in proofs.
| Feature | Constructor | Spec (basic) | Spec (fuel) | IR | Proof |
|---|---|---|---|---|---|
| Let binding | Stmt.letVar |
ok | ok | ok | proved |
| Assignment | Stmt.assignVar |
ok | ok | ok | proved |
| Storage write | Stmt.setStorage |
ok | ok | ok | proved |
| Mapping write | Stmt.setMapping |
ok | ok | ok | proved |
| Mapping + word write | Stmt.setMappingWord |
ok | ok | -- | proved |
| Packed mapping write | Stmt.setMappingPackedWord |
ok | ok | -- | proved |
| Double mapping write | Stmt.setMapping2 |
ok | ok | -- | proved |
| Double mapping + word | Stmt.setMapping2Word |
ok | ok | -- | proved |
| Uint256-keyed write | Stmt.setMappingUint |
ok | ok | -- | proved |
| Struct member write | Stmt.setStructMember |
ok | ok | -- | proved |
| Struct member 2 write | Stmt.setStructMember2 |
ok | ok | -- | proved |
| Require | Stmt.require |
ok | ok | ok | proved |
| Require (custom error) | Stmt.requireError |
ok | ok | -- | proved |
| Revert (custom error) | Stmt.revertError |
ok | ok | -- | proved |
| Return (single) | Stmt.return |
ok | ok | ok | proved |
| Return (multi) | Stmt.returnValues |
ok | ok | -- | proved |
| Return (array) | Stmt.returnArray |
ok | ok | -- | proved |
| Return (bytes) | Stmt.returnBytes |
ok | ok | -- | proved |
| Return (storage words) | Stmt.returnStorageWords |
ok | ok | -- | proved |
| Stop | Stmt.stop |
ok | ok | ok | proved |
| If/else | Stmt.ite |
ok | ok | ok | proved |
| For-each loop | Stmt.forEach |
rev | ok | ok | partial |
| Event emission | Stmt.emit |
ok | ok | -- | proved |
| Internal call (stmt) | Stmt.internalCall |
rev | ok | -- | proved |
| Internal call assign | Stmt.internalCallAssign |
rev | ok | -- | proved |
| Manual full-word storage write | Stmt.setStorageWord |
ok | ok | -- | n/m |
| Memory store | Stmt.mstore |
rev | rev | ok | partial |
| Calldatacopy | Stmt.calldatacopy |
nop | nop | -- | n/m |
| Returndatacopy | Stmt.returndataCopy |
rev | rev | -- | n/m |
| Revert returndata | Stmt.revertReturndata |
rev | rev | -- | n/m |
| Raw log | Stmt.rawLog |
rev | rev | -- | n/m |
| External call bind | Stmt.externalCallBind |
rev | rev | -- | n/m |
ECM (callWithValue / callWithValueBytes included) |
Stmt.ecm |
rev | rev | -- | n/m |
Legend: ok = supported, rev = reverts (not modeled), nop = no-op (codegen concern), -- = not applicable, n/m = not modeled.
Stmt.forEach proof coverage is intentionally partial: zero-bound loops with
supported bodies are proved, arbitrary literal-bound empty-body loops are
proved, and positive literal loops with non-empty bodies remain future work.
This is the current IR-generation proof boundary, not a claim about arbitrary
non-empty loop-body preservation.
ECMs include standard Verity-core modules for generic external-call mechanics,
including Compiler.Modules.Calls.bubblingValueCall, which lowers
Solidity-style call{value: v}(data) wrappers to Yul call and forwards exact
revert returndata on failure. bubblingValueCallNoOutputModule exposes the
same no-output adapter/router shape directly to verity_contract ecmDo call
sites. These mechanics remain explicit trust-report surfaces: Verity models the
generic call choreography, while package-specific callee behavior and protocol
assumptions belong in dependent packages.
The standard ECM library also includes static-word packed hashing helpers:
Compiler.Modules.Hashing.abiEncodePackedWords and
Compiler.Modules.Hashing.sha256PackedWords. These model contiguous 32-byte
word preimages. For static mixed-width preimages, such as an address-sized
segment followed by a 32-byte value, use
Compiler.Modules.Hashing.abiEncodePackedStaticSegments or
Compiler.Modules.Hashing.sha256PackedStaticSegments with explicit 1- to
32-byte widths. Dynamic bytes / string packed encoding remains outside the
current core surface.
One-off raw instruction surfaces should not be added to this statement table by
default. Use Stmt.unsafeYul with a small UnsafeYulFragment helper, such as
UnsafeYulFragment.rawRevert, when the feature is just an explicit Yul escape
hatch. Keep common typed primitives such as Stmt.mstore and
Stmt.calldatacopy first-class when they have stable Verity semantics and are
useful for proofs.
| Builtin | Verity | EVMYulLean | Agreement Proved |
|---|---|---|---|
add |
ok | ok | yes |
sub |
ok | ok | yes |
mul |
ok | ok | yes |
div |
ok | ok | yes |
mod |
ok | ok | yes |
addmod |
ok | ok | yes |
mulmod |
ok | ok | yes |
lt |
ok | ok | yes |
gt |
ok | ok | yes |
slt |
ok | ok | yes |
sgt |
ok | ok | yes |
eq |
ok | ok | yes |
iszero |
ok | ok | yes |
and |
ok | ok | yes |
or |
ok | ok | yes |
xor |
ok | ok | yes |
not |
ok | ok | yes |
shl |
ok | ok | yes |
shr |
ok | ok | yes |
byte |
ok | ok | yes |
exp |
ok | ok | yes |
sdiv |
ok | ok | yes |
smod |
ok | ok | yes |
sar |
ok | ok | yes |
signextend |
ok | ok | yes |
sload |
ok | ok | yes |
caller |
ok | ok | yes |
address |
ok | ok | yes |
callvalue |
ok | ok | yes |
calldataload |
ok | ok | yes |
timestamp |
ok | ok | yes |
chainid |
ok | ok | yes |
calldatasize |
ok | ok | yes |
number |
ok | ok | yes |
blobbasefee |
ok | ok | yes |
mappingSlot |
ok | ok | yes |
Legend: ok = native evaluation.
36/36 builtins have universal bridge agreement proofs between Verity and EVMYulLean evaluation paths. 36 are discharged by universal symbolic lemmas in Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean. Of those, 25 are discharged by universal symbolic lemmas for the pure fragment, and none still require concrete-only regression coverage. No builtin remains delegated to the Verity-only evaluation path.
| Category | Proved | Assumed | Partial | Not Modeled |
|---|---|---|---|---|
| Expression features | 24 | 1 (externalCall) |
6 | 6 (keccak256, call, staticcall, delegatecall, arrayElementDynamicWord, paramDynamicHeadWord) |
| Statement features | 24 | 0 | 2 (forEach, mstore) |
6 (calldatacopy, returndataCopy, revertReturndata, rawLog, externalCallBind, ecm) |
| Builtins (agreement) | 36 | 0 | 0 | 0 (delegated) |
Proof-boundary features split across two buckets. Partially modeled features currently include runtime introspection (blockNumber, contractAddress, chainid) and single-word linear-memory forms (mload, mstore, returndataOptionalBoolAt). selfBalance is also partially modeled: it is compiler-supported and source-executable, but not yet included in the generic proof interpreter fragment. Fully not-modeled features currently include keccak256, low-level call / returndata plumbing (call, staticcall, delegatecall, calldatacopy, returndataCopy, revertReturndata), event emission (rawLog), and external call modules (externalCallBind, ecm). Dynamic struct-array head-word decoding (arrayElementDynamicWord) and direct dynamic-struct parameter head-word decoding (paramDynamicHeadWord) are also not modeled by proof interpreters yet. These features are still compiler-supported and are validated by differential testing (70,000+ test vectors against actual EVM execution).
-
Nested dynamic ABI decoding: The compiler can read checked static leaf words from calldata arrays whose tuple/struct elements contain nested dynamic members via
Expr.arrayElementDynamicWord, and from direct struct parameters whose ABI encoding is dynamic viaExpr.paramDynamicHeadWord(#1832). These are compilation-level ABI decoder surfaces for Unlink-style transaction arrays and theTransaction/WithdrawalTransaction/AdapterTransactiondirect-parameter shapes; proof interpreters do not model those decoded words yet. -
Runtime environment reads:
address(this).balancelowers to Yulselfbalance()and runs againstContractState.selfBalanceon the executable source path, with Foundry differential coverage against Solidity. The current generic proof interpreters do not model this balance read yet. -
Linear memory: The IRInterpreter has single-word memory support.
mload,mstore,calldatacopy,returndataCopy, andreturndataOptionalBoolAttherefore remain only partially modeled or not modeled in the proof interpreters today. Full linear memory coverage requires EVMYulLean semantic integration. -
Low-level calls:
call/staticcall/delegatecallandexternalCallBind/ecmare compiler-only features validated by Foundry testing, not modeled in proof interpreters. The standardCalls.callWithValue,Calls.callWithValueBytes,Calls.bubblingValueCall, andCalls.bubblingValueCallNoOutputECMs are part of this compiler-only surface for genericcall{value:v}adapter/router flows and are surfaced as assumed ECMs in trust reports. ERC-20 optional-return helpers, including the OpenZeppelin-style and Solmate SafeTransferLib variants, also live in this ECM bucket. The EVM precompile ECMs (Precompiles.ecrecover0x01,Precompiles.sha256Memory/sha2560x02, and the BN254 curve precompilesPrecompiles.bn256Add0x06,Precompiles.bn256ScalarMul0x07,Precompiles.bn256Pairing0x08) also fall in this compiler-only ECM bucket; each precompile carries its ownevm_*_precompiletrust assumption documented indocs/EXTERNAL_CALL_MODULES.mdandAXIOMS.md.delegatecalladditionally remains a dedicated proxy / upgradeability trust boundary; use--trust-report/--deny-proxy-upgradeabilitywhen those semantics must stay outside the selected verification envelope (issue #1420). -
Internal helper compositional proofs:
Stmt.internalCall/Expr.internalCall/Stmt.internalCallAssignexecute in the fuel-based interpreter path. Helper-level summary reuse is now surfaced as a first-class proof interface:SupportedSpecHelperProofs.helperCallSummarySounddelivers a helper's proved summary (from the sharedhProofscatalog) at any call site of a selector-dispatched function, and the three call-shape corollariesevalInternalCallObeysSummary/execInternalCallObeysSummary/execInternalCallAssignObeysSummaryland that summary's postcondition directly on the interpreter result for the expression, void-statement, and assigning-statement shapes respectively. Theverity_contractuser surface for these remains ordinary direct function-name calls;internalCall/internalCallAssignare the lower-level compilation-model constructors. Broader Layer 2 completeness work continues under #1630, with the interface/boundary refactor in #1633.
Last Updated: 2026-06-02
Machine-readable artifact: artifacts/interpreter_feature_matrix.json