Skip to content

VERIFICATION_STATUS.md

Latest commit

 

History

History
282 lines (219 loc) · 45.2 KB

VERIFICATION_STATUS.md

File metadata and controls

282 lines (219 loc) · 45.2 KB
Raw

Verification Status

For the full documentation, see veritylang.com/verification.

Architecture

Verity implements a three-layer verification stack proving smart contracts correct from specification to Yul bytecode:

EDSL contracts (Lean)
    ↓ Layer 1: EDSL ≡ CompilationModel [PROVEN FOR CURRENT CONTRACTS; GENERIC CORE, CONTRACT BRIDGES]
CompilationModel (declarative compiler-facing model)
    ↓ Layer 2: CompilationModel → IR [GENERIC WHOLE-CONTRACT THEOREM]
Intermediate Representation (IR)
    ↓ Layer 3: IR → Yul [GENERIC SURFACE, EXPLICIT BRIDGE HYPOTHESIS]
Yul (EVM Assembly)
    ↓ (Trusted: solc compiler)
EVM Bytecode

Layer 1: EDSL ≡ CompilationModel, PROVEN FOR CURRENT CONTRACTS

What it proves today: The EDSL Contract monad execution is equivalent to CompilationModel interpretation for the current supported contract set. This is the frontend semantic bridge. The proof stack has a generic typed-IR core, but the active bridge theorems are still instantiated per contract. Separate per-contract proofs under Contracts/<Name>/Proofs/ then show these contracts satisfy their human-readable specifications; those specification theorems are downstream contract proofs, not the definition of Layer 1 itself.

Verified Contracts

Contract Properties Status Location
SimpleStorage 20 Complete Contracts/SimpleStorage/Proofs/
Counter 31 Complete Contracts/Counter/Proofs/
SafeCounter 25 Complete Contracts/SafeCounter/Proofs/
Owned 23 Complete Contracts/Owned/Proofs/
Ownable 6 Complete Contracts/Ownable/Proofs/
OwnedCounter 63 Complete Contracts/OwnedCounter/Proofs/
OwnedCounterComposed 6 Complete Contracts/OwnedCounterComposed/Proofs/
Ledger 33 Complete Contracts/Ledger/Proofs/
LocalObligationMacroSmoke 4 Baseline Contracts/LocalObligationMacroSmoke/Proofs/
SimpleToken 61 Complete Contracts/SimpleToken/Proofs/
ERC20 22 Baseline Contracts/ERC20/Proofs/
ERC721 11 Baseline Contracts/ERC721/Proofs/
Vault 9 Baseline Contracts/Vault/Proofs/
ReentrancyExample 5 Complete Contracts/ReentrancyExample/Contract.lean
ReentrancyRelyGuarantee 10 Semantic Contracts/ReentrancyRelyGuarantee/Contract.lean
CryptoHash 0 No specs Contracts/CryptoHash/Contract.lean
Total 329 ✅ 100% —

Note: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (329 total properties).

Layer 1 uses macro-generated EDSL-to-CompilationModel bridge theorems backed by a generic typed-IR compilation-correctness theorem (TypedIRCompilerCorrectness.lean). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in CompilationModel and trusted at that boundary. Higher-order internal helpers (function-pointer parameters, #1747) are eliminated by a compile-time monomorphization pre-pass that runs before any lowering, so the CompilationModel only ever contains first-order helpers: these calls are covered by the existing first-order proof path and introduce no new boundary trust.

Internal helper calls are supported operationally in CompilationModel and the fuel-based interpreter path. Helper-level compositional proof reuse across callers is now a first-class verified interface at the helper-aware source semantics: SupportedSpecHelperProofs carries a single global helper-summary proof catalog (SupportedHelperSummaryProofCatalog) in which each helper summary is proved sound exactly once, and SupportedSpecHelperProofs.helperCallSummarySound — together with the call-shape specializations evalInternalCallObeysSummary / execInternalCallObeysSummary / execInternalCallAssignObeysSummary in SourceSemantics.lean — threads that once-proved catalog through to every selector-dispatched caller and every syntactic call site, so a helper proved once is consumed at each call without re-discharging its summary. What remains under #1630 is consuming that source-level reuse interface through the body/IR composition lemmas into the generic whole-contract theorem (still gated by the helper-excluding SupportedBodyInterface.stmtList fragment); the current interface/boundary refactor landed in #1633.

Layer 2: CompilationModel → IR — GENERIC WHOLE-CONTRACT THEOREM

Tracking:

What is generic today:

  • a structural theorem for raw statement lists inside the explicit SupportedStmtList fragment witness in TypedIRCompilerCorrectness.lean, re-exported for the compiler-proof layer in SupportedFragment.lean
  • a whole-contract theorem surface, compile_preserves_semantics, quantified over arbitrary supported CompilationModels, selectors, a SupportedSpec witness, and successful CompilationModel.compile output; the source side is already expressed in the helper-aware semantics family using the canonical SupportedSpec.helperFuel bound
  • a syntactic frame-reasoning library for the IR interpreter in Frames.lean: execStmts_frame_rule proves any supported statement list preserves every resource disjoint from its declared write set (#1990 part 1); writeFootprint / execStmts_frame_rule_writeFootprint compute a syntactic write footprint and prove the frame rule against it (#1990 part 2); and the ExecutionSummary family (execStmt_setStorage_execution_summary, execStmtList_execution_summary_cons) gives composable per-statement storage-write summaries (#1994)
  • non-alias certificates for finite mapping slots in MappingSlot.lean: distinct keys / word offsets resolve to distinct storage slots (mappingSlotLocations_nonAlias_get, nestedMappingSlotLocations_nonAlias_get), supporting the write-set disjointness the frame rule consumes (#2001)
  • the ABI word specifications in AbiEncoding.lean are now connected to memory in AbiMemoryLayout.lean (#2082 slice 3): yulLogDataWords_abiBlockWrites reads a 32-byte-stride mstore block back as exactly the words written, and instantiating it gives abiEncodeScalarHeads_memory_layout / abiEncodeArgs_memory_layout plus the pointwise head and dynamic-tail-offset facts (abiEncodeScalarHeads_memory_head, abiEncodeArgs_memory_head, abiEncodeArgs_memory_dynamic_offset_points_at_tail)
  • AbiEventObservable.lean threads that layout through the LOG opcodes: scalarEmitPayload_log_observable proves the compiled scalar emit payload (the unindexed mstore block followed by logN) appends exactly one observable whose topics are topic0 followed by the ABI encoding of the indexed arguments and whose data is the ABI encoding of the unindexed arguments
  • AbiDynamicEventObservable.lean removes the one-word-per-argument restriction (#2082 slice 4): DynEmitArg describes an unindexed payload argument at the IR level (static scalar, bytes/string, or dynamic scalar array), dynEmitPayloadExprs lays the whole payload out as one 32-byte-stride word block, and dynamicEmitPayload_log_observable proves that running that block followed by logN appends exactly one observable whose topics are topic0 followed by the ABI encoding of the indexed arguments and whose data is the full slice-2 abiEncodeArgs encoding (static heads, dynamic head offsets, then tails). The head offsets are computed by dynEmitHeadExprs and proved equal to abiEncodeArgHeads (dynEmitHeadExprs_eval, dynEmitPayloadExprs_eval), so the ABI head/tail arithmetic is pinned at the IR level rather than assumed; eventLogStmt_exec_dataExpr generalizes the slice-3 log lemma so the size operand may be the dynamic lane's __evt_data_tail accumulator instead of a literal

What is not yet covered:

  • the supported whole-contract fragment is still intentionally narrower than the full CompilationModel surface; unsupported features remain documented at the boundary instead of being claimed as proved
  • the body-level supported-fragment witness is now decomposed into feature-local interfaces (core, state, calls, effects) in SupportedSpec.lean, and the calls interface is further split into helpers, foreign, and lowLevel; calls.helpers now inventories direct helper callees through positive summary witnesses carrying an InternalHelperSummaryContract plus a strictly decreasing helper-rank measure, and expression-position helper callees are tracked separately with an explicit world-preservation-on-success obligation because the current helper-aware expression semantics returns only values. SourceSemantics.lean exposes the helper-aware source execution target those future contracts will quantify over and now defines InternalHelperSummarySound / SupportedBodyHelperSummariesSound plus direct-call consumption lemmas for helper summaries. The feature-local state / calls / effects scans recurse through nested ite / forEach bodies, so these boundary witnesses are control-flow complete, but helper reuse, low-level calls, and richer observables are still outside the proved generic theorem until those interfaces are threaded through the body/IR composition lemmas
  • the helper-aware source semantics is now proved to be a conservative extension of the current helper-free source semantics on the existing SupportedSpec fragment, and the public theorem surface is already anchored to that helper-aware semantics via SupportedSpec.helperFuel, so future helper-summary composition can target the same source-level semantics family without another theorem-shape rewrite or trusted-boundary change; SourceSemantics.lean now also defines the helper-free collapse goal ExecStmtListWithHelpersConservativeExtensionGoal together with a reusable global helper-summary proof catalog (SupportedHelperSummaryProofCatalog) that feeds SupportedSpecHelperProofs. SupportedSpec.lean now separates the coarse current helper exclusion (stmtTouchesUnsupportedHelperSurface) from the narrower exact-seam predicate stmtTouchesInternalHelperSurface, further cuts that genuine-helper surface into direct statement-position heads, expression-position heads, and structural recursive heads, and introduces the compiled-side glue SupportedCompiledInternalHelperWitness / SupportedRuntimeHelperTableInterface; Contract.lean proves compile_ok_yields_supportedRuntimeHelperTableInterface, so future exact helper-step proofs can assume a generic source-helper-to-runtime-helper-table mapping instead of re-deriving it ad hoc from CompilationModel.compile. GenericInduction.lean now exposes the helper-aware induction interfaces CompiledStmtStepWithHelpers / StmtListGenericWithHelpers, the lifting lemmas CompiledStmtStep.withHelpers_of_helperSurfaceClosed / stmtListGenericWithHelpers_of_core_and_helperSurfaceClosed, the induction-level theorem supported_function_body_correct_from_exact_state_generic_helper_steps, the exact helper-aware compiled induction seam CompiledStmtStepWithHelpersAndHelperIR / StmtListGenericWithHelpersAndHelperIR, the strong helper-free compiled compatibility witness StmtListCompiledLegacyCompatible, the weaker future-proof exact-seam witnesses StmtListHelperFreeCompiledLegacyCompatible and StmtListHelperFreeStepInterface, the split exact helper-step interfaces StmtListInternalHelperSurfaceStepInterface / StmtListResidualHelperSurfaceStepInterface, the finer genuine-helper interfaces StmtListDirectInternalHelperCallStepInterface / StmtListDirectInternalHelperAssignStepInterface / StmtListDirectInternalHelperStepInterface / StmtListExprInternalHelperStepInterface / StmtListStructuralInternalHelperStepInterface, the exact-seam lifting lemmas CompiledStmtStepWithHelpers.withHelperIR_of_legacyCompatible / stmtListGenericWithHelpersAndHelperIR_of_withHelpers_and_compiledLegacyCompatible, the split bridges stmtListGenericWithHelpersAndHelperIR_of_helperFreeStepInterface_and_directInternalHelperCallStepInterface_and_directInternalHelperAssignStepInterface_and_exprInternalHelperStepInterface_and_structuralInternalHelperStepInterface_and_residualHelperSurfaceStepInterface_and_helperFreeCompiledLegacyCompatible / stmtListGenericWithHelpersAndHelperIR_of_core_directInternalHelperCallStepInterface_and_directInternalHelperAssignStepInterface_and_exprInternalHelperStepInterface_and_structuralInternalHelperStepInterface_and_residualHelperSurfaceStepInterface_and_helperFreeCompiledLegacyCompatible plus coarser compatibility wrappers over StmtListDirectInternalHelperStepInterface, the body-level finer split bridge supported_function_body_correct_from_exact_state_generic_finer_split_internal_helper_surface_steps_and_helper_ir, the compatibility wrapper supported_function_body_correct_from_exact_state_generic_split_internal_helper_surface_steps_and_helper_ir, the source-side derivation lemma stmtListHelperFreeStepInterface_of_core (the compile-derived compiled-side derivation lemmas are retired together with GenericInduction/LegacyCompatibility), the exact induction-level body theorem supported_function_body_correct_from_exact_state_generic_helper_steps_and_helper_ir, the hypothesis-passing exact-body wrapper supported_function_body_correct_from_exact_state_generic_with_helpers_and_helper_ir_callsDisjoint, the transitional legacy-compiled-body target SupportedFunctionBodyWithHelpersIRPreservationGoal, and the exact future helper-aware compiled-body target SupportedFunctionBodyWithHelpersAndHelperIRPreservationGoal; Function.lean exposes the matching function-level wrapper supported_function_correct_with_helper_proofs_body_goal, and the older goal wrappers (supported_function_body_correct_from_exact_state_generic_with_helpers_goal, supported_function_correct_with_helper_proofs_goal) are therefore now abstract helper-free discharge paths into the transitional target rather than the eventual helper-rich theorem target
  • the machine-readable boundary catalog now makes that blocker exact rather than implicit: callers still reach the body theorem through the helper-free SupportedStmtList witness, and that helper exclusion is now derived directly in Lean as SupportedStmtList.helperSurfaceClosed; the helper-aware body theorem does not yet consume helper-summary soundness/rank evidence end to end. More precisely, that evidence is not yet consumed through the exact helper-aware compiled induction seam CompiledStmtStepWithHelpersAndHelperIR / StmtListGenericWithHelpersAndHelperIR and then into a direct proof of SupportedFunctionBodyWithHelpersAndHelperIRPreservationGoal for the genuinely new internal-helper cases, even though IRInterpreter.lean now defines helper-aware compiled-side targets (execIRFunctionWithInternals, interpretIRWithInternals) that can resolve IRContract.internalFunctions and Function.lean / Dispatch.lean / Contract.lean now expose wrapper theorems that already target those helper-aware compiled semantics. GenericInduction.lean now also makes the interim compiled-side boundary explicit by proving that the older legacy-compiled-body goal SupportedFunctionBodyWithHelpersIRPreservationGoal lifts into SupportedFunctionBodyWithHelpersAndHelperIRPreservationGoal on LegacyCompatibleExternalStmtList bodies when IRContract.internalFunctions = [], and it now also splits the exact helper-rich reuse boundary on both sides: the compiled side is reduced to StmtListHelperFreeCompiledLegacyCompatible, the residual non-helper side is isolated in StmtListResidualHelperSurfaceStepInterface, and the genuine internal-helper side is further reduced to StmtListDirectInternalHelperCallStepInterface, StmtListDirectInternalHelperAssignStepInterface, StmtListExprInternalHelperStepInterface, and StmtListStructuralInternalHelperStepInterface, with StmtListDirectInternalHelperStepInterface retained only as a compatibility wrapper over the two direct statement-position proof shapes, while the source side is reduced to StmtListHelperFreeStepInterface, combined by stmtListGenericWithHelpersAndHelperIR_of_helperFreeStepInterface_and_directInternalHelperCallStepInterface_and_directInternalHelperAssignStepInterface_and_exprInternalHelperStepInterface_and_structuralInternalHelperStepInterface_and_residualHelperSurfaceStepInterface_and_helperFreeCompiledLegacyCompatible and the body-level bridge supported_function_body_correct_from_exact_state_generic_finer_split_internal_helper_surface_steps_and_helper_ir. The compile-derived compiled-side witness producers are retired together with GenericInduction/LegacyCompatibility; the weaker source witness is still derived from the existing helper-free generic library, and the hypothesis-passing wrapper supported_function_body_correct_from_exact_state_generic_with_helpers_and_helper_ir_callsDisjoint reaches the exact helper-aware compiled body goal from an explicit caller-supplied disjointness witness, without requiring future helper-rich bodies to satisfy StmtListGenericCore wholesale. The intended legacy-compatible external-body Yul subset is now formalized directly in IRInterpreter.lean as LegacyCompatibleExternalStmtList, the weaker external-body witness is split out as LegacyCompatibleExternalBodies, the helper-free runtime-contract shape is now packaged as LegacyCompatibleRuntimeContract, and the exact first retarget theorem is now encoded as InterpretIRWithInternalsZeroConservativeExtensionGoal; IRInterpreter.lean now also decomposes that theorem into the explicit expr / stmt / stmt-list / function proof surface InterpretIRWithInternalsZeroConservativeExtensionInterfaces, factors shared transaction setup through applyIRTransactionContext, and still exposes the selected-function cut InterpretIRWithInternalsZeroConservativeExtensionDispatchGoal with the bridge theorem interpretIRWithInternalsZeroConservativeExtensionGoal_of_dispatchGoal over LegacyCompatibleRuntimeDispatch. The helper-free conservative-extension goal is now closed on that subset, including interpretIRWithInternalsZeroConservativeExtensionStmtSubgoals_closed and culminating in interpretIRWithInternalsZeroConservativeExtensionGoal_closed; the supporting closed surfaces include InterpretIRWithInternalsZeroConservativeExtensionStmtSubgoals, interpretIRWithInternalsZeroConservativeExtensionInterfaces_of_stmtCompatibility, the interpretIRWithInternalsZeroConservativeExtensionInterfaces_of_stmtSubgoals wrapper, and the dedicated expr-statement builtin classifier exprStmtUsesDedicatedBuiltinSemantics, with direct helper-free lemmas for stop, mstore, revert, return, and mapping-slot sstore. Dispatch.runtimeContractOfFunctions now also has a runtimeContractOfFunctions_legacyCompatible bridge, and Contract.lean exposes the helper-aware _goal / _closed wrappers compile_preserves_semantics_with_helper_proofs_and_helper_ir_goal and compile_preserves_semantics_with_helper_proofs_and_helper_ir_closed. The compile-derived LegacyCompatibleRuntimeContract witness producers are retired along with GenericInduction/LegacyCompatibility; those helper-aware whole-contract wrappers now consume the legacy-compatible runtime witness as an explicit caller-supplied hypothesis. The helper-aware compiled target remains available through evalIRExprWithInternals as total fuel-indexed helper-aware IR semantics. The remaining blocker on today's theorem domain is therefore helper-summary soundness/rank consumption in the genuinely new internal-helper cases of the exact helper-aware compiled induction seam, now cut along the same direct-helper-call / direct-helper-assign / expression-helper / structural-recursion lines as the source-side helper lemmas, and then in a direct proof of SupportedFunctionBodyWithHelpersAndHelperIRPreservationGoal while widening or replacing the helper-excluding statement fragment and proving the exact helper step interface at those heads. A later widening step still needs a weaker retarget boundary that can tolerate helper tables once helper-rich features move inside the theorem domain; that later compiled-side blocker remains tracked in #1638

Intended end-state claim:

  • "whole EDSL" means the proof-complete macro-lowered image of verity_contract, not all arbitrary Lean-produced CompilationModel terms
  • the widening target is to prove the generic theorem for that frontend image, or for a CompilationModel subset that the frontend lowering is proved to land inside
  • the machine-readable companion for that claim and the current proof boundary is artifacts/layer2_boundary_catalog.json

What is not fully migrated yet

  • The generic theorem surface is in place, but the supported whole-contract fragment is still narrower than the full CompilationModel / EDSL surface.
  • The contract/body support witness is no longer one undifferentiated exclusion bit, and helper calls now have an explicit summary inventory boundary, a reusable semantic summary contract slot, a global proof catalog for reusing helper-summary soundness across callers, and a dedicated source-semantics target, but the remaining excluded surfaces are still real proof gaps until the corresponding feature-local interfaces are consumed by positive theorem interfaces. In particular, helper reuse is still held behind the explicit helper-excluding SupportedBodyInterface.stmtList gate recorded in artifacts/layer2_boundary_catalog.json.
  • Contracts and features outside SupportedSpec still rely on explicit trust-surface documentation, targeted testing, or future fragment-widening work rather than a claim of full generic compile-preservation.

Current boundary:

  • Generic: supported statement-list compilation and the whole-contract theorem itself

  • Proved generically: initial-state normalization between withTransactionContext and initialIRStateForTx, under explicit transaction-context normalization hypotheses

  • No Lean axioms remain in Layer 2; 0 sorry placeholders remain. The storageLookup_projectStorage proof (previously a sorry) is now complete, using Batteries.RBMap.find?_insert lemmas with an injectivity argument over in-range storage slots.

  • Stateful environment-reading builtins route through native EVMYulLean context construction: callvalue, timestamp, number, caller, address, and calldatasize.

  • Additional explicit precondition: the generic theorem surface now requires the observed transaction-context fields (sender, thisAddress, msgValue, blockTimestamp, blockNumber, chainId) to already fit the bounded source-side Address/Uint256 domains

  • Outside the current generic theorem or current proof model: nested event emissions inside structural statements (ite/forEach), proxy/delegatecall upgradeability, linked externals, local unsafe obligations, and other trust-surfaced features not captured by the current supported whole-contract fragment. Scalar event emissions are proved through a contract-level wrapper for top-level emit statements with scalar parameters and at most three indexed parameters; callers supply the scalar-event list-interface witnesses required by the function-level bridge.

  • TODO (#2082): Stmt.emit is still true in stmtTouchesUnsupportedEffectSurface itself, and so are typed reverts (Stmt.requireError / Stmt.revertError / Stmt.panicCode). Two narrowings now exist alongside that predicate:

    • Events-aware effect surface: stmtTouchesUnsupportedEffectSurfaceWithEvents admits exactly the emission heads eventEmissionProofSupported already proves, and stmtTouchesUnsupportedContractSurfaceWithEvents_eq_false_of_featureClosedWithEvents bridges the core/state/call/effect decomposition to the contract-surface gate with that component in its events-aware form. SupportedBodyInterfaceWithScalarEvents.ofEffectInterfaceWithEvents builds the scalar-event body interface from that decomposition, so an event-carrying body no longer has to supply contractSurfaceWithEvents directly. SupportedBodyEffectInterfaceWithEvents.ofEffectInterface proves the weakening direction, so emission-free bodies still reach the same interface.
    • Typed-revert observable: TypedRevertStep discharges the hrevertExec hypothesis of compiledStmtStep_requireError / compiledStmtStep_revertError for zero-parameter custom errors and for custom errors with a single static scalar parameter, via the NonEscaping / RevertsAlways machinery in CustomErrorPayloadIR. Parameters whose store routes through compileUnindexedAbiEncode remain out of reach for the partial def reason recorded below.

    Slice 4 (AbiDynamicEventObservable.dynamicEmitPayload_log_observable) removes the shape restriction that slice 3 imposed — a payload with a head/tail split is now in the proved domain — but it does not yet flip that effect-surface bit, because the theorem is stated over the payload word block (dynEmitUnindexedStores) rather than over CompilationModel.compileEmit's output. Three gaps remain, all unsupported today:

    • Concrete dynamic lane (bytes/string unindexed arguments): compileEmit materializes tail data with dynamicCopyData (a calldatacopy) and carries dynamic head offsets in the mutable __evt_data_tail accumulator rather than as literals. Missing lemmas: (a) a word-granular calldatacopy readback lemma, in the style of AbiMemoryLayout.yulLogDataWords_abiBlockWrites, proving the copied region reads back as the padded data words; and (b) an accumulator invariant for __evt_data_tail, since it is reassigned inside the store block and therefore violates the "values evaluated in the initial state" premise of IRGeneration.EventObservable.execIRStmts_mstore_ptr_expr_block. A further obstacle is that compileUnindexedAbiEncode and compileIndexedInPlaceEncoding are partial def and hence opaque to Lean proofs; connecting the slice-4 theorem to the concrete lane requires making them structurally recursive first.
    • Indexed dynamic arguments (bytes/string hashed into a topic): the compiler copies the value into scratch memory and takes keccak256 of it. The observable model has no lemma pinning that hash, so the indexed side of dynamicEmitPayload_log_observable stays scalar (scalarEventIndexedTopicParts). Missing lemma: a keccak256-over-copied-region evaluation result tying the emitted topic to the source value's hash.
    • Typed reverts with dynamic or composite parameters: the revert observable is now discharged for zero-parameter and single-static-scalar-parameter custom errors, but there is still no counterpart of the emit theorem tying the payload's memory image to the ABI encoding, even though AbiMemoryLayout.abiEncodeArgs_memory_layout already supplies the dynamic-block memory image that lane will need. adt, static tuple/fixedArray and multi-parameter errors emit a parameter-count-dependent store list; bytes / string / array / dynamic composites route through the partial def encoder.

Key files:

Layer 3: IR → Native EVMYulLean, GENERIC, WITH EXPLICIT AXIOM BOUNDARY

What it proves today: generated runtime Yul is lowered into EVMYulLean and executed through the native EvmYul.Yul.callDispatcher theorem stack. The public EndToEnd surface compares the projected native dispatcher result with IR/source semantics on the observable storage/log/result surface. The old fuel-parametric Verity-side Yul executor and preservation/equivalence files are no longer part of the checked-in proof tree.

Key files: EndToEnd.lean, EvmYulLeanNativeHarness.lean, EvmYulLeanBodyClosure.lean, EvmYulLeanBridgeLemmas.lean, AXIOMS.md

Phase 4: EVMYulLean Native Dispatcher (safe-body EndToEnd target)

The retargeting module that bridged the old .verity execution path to the .evmYulLean backend, together with the old preservation and equivalence scaffolding, was removed in DoD-5 of the EVMYulLean transition. The native EvmYulLean dispatcher is now the sole runtime authority; there is no longer a parallel private execution chain to keep in sync.

The retained content of Phase 4 is the body-closure layer that proves compiler-emitted runtime Yul satisfies BridgedStmts so that the public EndToEnd surface (which targets native EvmYul.Yul.callDispatcher execution through EvmYulLeanNativeHarness) can compose with those closures unconditionally for the supported fragment.

  • genParamLoads_scalar_bridged: scalar calldata parameter-loading prologues emitted by genParamLoads satisfy BridgedStmts
  • genStaticTypeLoads_calldataload_bridged: static scalar leaf-load helpers for fixed arrays/tuples satisfy BridgedStmts
  • genParamLoads_static_scalar_bridged: full calldata parameter-loading prologues for static scalar fixed arrays/tuples satisfy BridgedStmts
  • compileExpr_bridgedSource: arithmetic/comparison/bit-operation source expressions, parameter length identifiers, storage, storage-array length, and ADT tag/field reads whose compiler field lookup succeeds, singleton and nested mapping reads (mapping, mappingWord, mappingUint, mapping2, mapping2Word) through the abstract mappingSlot bridge, mapping struct-member reads (structMember, structMember2), the reserved exponentiation builtin surface, calldata/memory/transient reads, and syntactic keccak256(offset, size) source expressions in the BridgedSourceExpr fragment compile to BridgedExpr; mappingSlot remains the mapping-slot memory+keccak abstraction boundary, and keccak256 remains outside the full source-vs-IR semantic core until memory-slice hashing is modeled by the source evaluator
  • compileExpr_keccak256_bridgedSource_of_exprCompileCore: specialized native syntactic closure for Expr.keccak256 offset size when offset and size are compile-core expressions, without adding keccak256 to the source semantic core
  • compileExpr_mappingChain_bridgedSource: specialized native syntactic closure for Expr.mappingChain field keys when every key is in BridgedSourceExpr, through the abstract mappingSlot bridge
  • bridgedSafeStmts_letKeccak_of_exprCompileCore / bridgedSafeStmts_assignKeccak_of_exprCompileCore: singleton let/assign bindings of syntactic keccak256(offset, size) are native safe bodies when offset and size are compile-core expressions
  • bridgedSafeStmts_externalMstoreLetKeccak_of_exprCompileCore: external two-statement mstore(...); let name := keccak256(...) memory-preimage bodies are native safe bodies when all four subexpressions are compile-core
  • BridgedSourceStmt / compileStmt_bridgedSource_bridged / compileStmtList_bridgedSource_bridged: a single per-statement source whitelist inductive (indexed by internal/external position) with master closure theorems replacing the former per-fragment list-level lattice (binding-leaf, pure-binding, storage, terminator, require, mapping-write, mixed/structured/nested body fragment lists); each admitted statement form compiles to BridgedStmts and the list-level lift aggregates pointwise membership
  • compileStmtList_external_recursive_body_fragment_bridged: mixed external source-body fragments closed recursively under Stmt.ite compile to BridgedStmts
  • compileStmtList_internal_recursive_body_fragment_bridged: mixed internal source-body fragments closed recursively under Stmt.ite compile to BridgedStmts
  • compileStmt_internalCall_bridged / compileStmtList_internalCall_bridged: statement-position Stmt.internalCall and Stmt.internalCallAssign whose arguments are BridgedSourceExpr and whose compiled helper name resolves in an explicit BridgedFunctionTable compile to BridgedStmts
  • compileStmt_externalCallBind_bridged / compileStmtList_externalCallBind_bridged: Stmt.externalCallBind whose arguments are BridgedSourceExpr and whose target stub resolves in an explicit BridgedFunctionTable compiles to BridgedStmts
  • compileStmtList_always_bridged: universal aggregation theorem for BridgedSafeStmts, now including the table-resolved internalCall / internalCallAssign and externalCallBind families; opaque Stmt.ecm remains outside the whitelist until concrete modules provide bridgeable-output obligations

The backend-parameterized bridge has been deleted. Body closure now has a universal safe-body aggregation theorem for BridgedSafeStmts, while the public EndToEnd theorem family targets native dispatcher execution through interpretIRRuntimeNative. The call-family path now requires an explicit bridged function table witness for each admitted callee rather than trusting arbitrary runtime dispatch.

Native-runtime transition status: the public theorem target is native EVMYulLean dispatcher execution. The executable native EVMYulLean path lives in EvmYulLeanNativeHarness.lean. The public native EndToEnd surface is the native result comparison/composition surface, the generated call-dispatcher and dispatcher-exec theorem family, and the concrete SimpleStorage theorem; the fuel-indexed nativeIRRuntimeMatchesIR seams and positive dispatcher-exec match family are file-local instead of public theorem authority. The no-mapping and mapping generated-dispatcher wrappers consume concrete dispatcher lowering and construct full emitted-runtime native lowering internally, while the call-dispatcher variants expose the actual generated EvmYul.Yul.callDispatcher premise and derive the dispatcher-exec projection internally.

Trust boundary (public EndToEnd target): native EvmYul.Yul.callDispatcher execution is the public semantic target. The old builtin-comparison module has been removed; it is not a runtime authority for public compiler correctness.

Not yet proven in this module:

  • opaque ECM body closure beyond the current BridgedSafeStmts whitelist
  • full native EvmYul.Yul.callDispatcher preservation for emitted runtime Yul without the remaining concrete dispatcher-exec obligations

Remaining gaps for whole-program retargeting:

  • 0 sorry-backed core equivalences
  • connect the table-resolved BridgedSafeStmts call-family constructors to whole-program emitted helper/stub tables, and add bridgeable-output obligations for remaining opaque ECM modules

Example Contract Compilation Coverage

The repository contains several different kinds of contract examples. Their current compile-preservation status is not uniform.

Contracts covered by the generic Layer 2 theorem

All contracts within the SupportedSpec fragment are covered by the generic whole-contract theorem in Compiler/Proofs/IRGeneration/Contract.lean. No manual per-contract bridge proofs are needed.

Spec proofs exist, contract-level compile-preservation is generic

All current contracts with spec proofs benefit from the generic Layer 2 theorem if they fall within the supported fragment. Contracts outside the fragment (e.g., those using linked externals or unsupported features) rely on testing for compile-preservation confidence.

Semantic example, not a current verity_contract compilation example

  • ReentrancyExample

ReentrancyExample is proved as a semantic case study in Lean, but it is not a current verity_contract macro contract with a contract-level compilation-preservation theorem surface in this repo.

Intentionally outside the current proof-complete compilation subset

  • CryptoHash: linked external Yul libraries / external call oracle surface
  • RawLogTrustSurface: raw event emission trust surface
  • LocalObligationTrustSurface: explicit local unsafe/refinement obligation surface
  • ProxyUpgradeabilityMacroSmoke, ProxyUpgradeabilityLayoutCompatibleSmoke, ProxyUpgradeabilityLayoutIncompatibleSmoke: proxy / delegatecall / upgradeability semantics are outside the current proof model
  • StringSmoke, StringEventSmoke, StringErrorSmoke: smoke examples for string, error, and event surfaces rather than current end-to-end proof-complete examples

Also note that the macro-generated *_semantic_preservation theorems are not contract-to-Yul semantic-preservation theorems. They are body-alignment equalities between generated CompilationModel bodies and macro-generated body fixtures, not full execution-preservation proofs for compiled IR/Yul.

Property Test Coverage

Contract Coverage Exclusions
ERC20 86% (19/22) 3 proof-only
Vault 0% (0/9) 9 proof-only
ERC721 100% (11/11) 0
SafeCounter 100% (25/25) 0
ReentrancyExample 100% (5/5) 0
ReentrancyRelyGuarantee 0% (0/10) 10 proof-only
Ledger 100% (33/33) 0
LocalObligationMacroSmoke 100% (4/4) 0
SimpleStorage 95% (19/20) 1 proof-only
OwnedCounter 70% (44/63) 19 proof-only
Owned 87% (20/23) 3 proof-only
Ownable 0% (0/6) 6 proof-only
OwnedCounterComposed 0% (0/6) 6 proof-only
SimpleToken 85% (52/61) 9 proof-only
Counter 74% (23/31) 8 proof-only
Stdlib 0% (0/0) 0 proof-only

Status: 78% coverage (255/329), 74 remaining exclusions all proof-only

  • Total Properties: 329
  • Covered: 255
  • Excluded: 74 (all proof-only)

Proof-Only Properties (59 exclusions): Internal proof machinery that cannot be tested in Foundry.

0 sorry remaining across Compiler/**/*.lean and Verity/**/*.lean proof modules. 5266 theorems/lemmas (3645 public, 1621 private) verified by lake build PrintAxioms.

1 documented Lean axiom remains: solidityMappingSlot_injective (mapping-slot ABI preimage collision-resistance). The former mapping-slot range axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, the Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is tracked as an explicit theorem hypothesis rather than a Lean axiom. Layer 2 itself still has 0 axioms.

Differential Testing

Status: CI runs large sharded randomized differential suites against the current contract set, comparing EDSL interpreter output against Solidity-compiled EVM execution. The seed-42 shard set owns the Random10000 stress lane; the multi-seed lane skips that target so it can cover cheaper randomized/property tests across several seeds without serially repeating the slowest stress suite.

Solidity Interop Support Matrix (Issue #586)

This matrix tracks migration-critical Solidity interoperability features and current implementation status.

Status legend:

  • supported: usable end-to-end
  • partial: implemented with functional limits or incomplete proof/test coverage
  • unsupported: not implemented as a first-class feature
Feature Spec support Codegen support Proof status Test status Current status
Custom errors + typed revert payloads partial partial n/a partial partial
Low-level calls (call / staticcall / delegatecall) with returndata partial partial n/a partial partial
fallback / receive / payable entrypoint modeling partial partial n/a partial partial
Event ABI parity for indexed dynamic/tuple payloads supported supported supported supported supported
Storage layout controls (packing + explicit slots) partial partial partial partial partial
ABI JSON artifact generation partial partial n/a partial partial
Dynamic-array element slot derivation (keccak256(bytes32(slot)) + index) unsupported supported unsupported partial unsupported

The dynamic-array row records a model divergence, not a codegen gap. The source semantics (Compiler/Proofs/IRGeneration/SourceSemantics.lean:330-350, findDynamicArrayElementAtSlot) places element i of the array rooted at slot s at solidityMappingSlot s i = keccak256(abi.encode(i, s)) — the 64-byte mapping preimage — while the Yul layout (Compiler/Proofs/Storage/StructArrayStorage.lean:666-671, storageArrayBasePointer / storageArrayElementPointer) uses the real Solidity keccak256(bytes32(s)) + i. The missing feature is an array-element slot derivation of that second form in the source semantics. Nothing asserts the two equal; the global storage-coherence collapse returns none at dynamic-array roots instead (Compiler.Proofs.Storage.MappingCoherentGlobal.storageKeySlot_slot_dynamicArray).

Diagnostics policy for unsupported constructs:

  1. Report the exact unsupported construct at compile time.
  2. Suggest the nearest supported migration pattern.
  3. Link to the owning tracking issue.
  4. When low-level mechanics, raw rawLog event emission, axiomatized primitives (for example keccak256), local unsafe/refinement obligations, or external assumptions are in play, emit a machine-readable trust report via verity-compiler --trust-report <path>. The report groups foreign trust surfaces into explicit proofStatus.proved, proofStatus.assumed, and proofStatus.unchecked buckets, localizes them to constructor/function usageSites, surfaces localized localObligations, classifies ECM/linked-external/primitive/local-obligation entries with a stable boundaryClass (compilerIntrinsic, abiBoundary, externalCall, oracleSummary, tokenModel, callback, event, gate, or storageLayoutAssumption), and now separately lists notModeledEventEmission, notModeledProxyUpgradeability, partiallyModeledLinearMemoryMechanics, and partiallyModeledRuntimeIntrospection so the current event, proxy/upgradeability, memory/ABI, and runtime-context proof gaps are explicit in both contract-level and per-site audit output. In human-readable mode, --verbose now emits matching usage-site and contract-level summaries. For fail-closed verification runs, add --deny-unchecked-dependencies, which now reports the exact usage site that introduced each unchecked dependency. For proof-strict runs that reject any unproved foreign surface, use --deny-assumed-dependencies, which fails on both assumed and unchecked linked externals / ECM modules and reports the exact usage site. For primitive-proof-strict runs, add --deny-axiomatized-primitives, which fails on any remaining axiomatized primitive and reports the exact usage site. For local-obligation-proof-strict runs, add --deny-local-obligations, which fails on any remaining assumed or unchecked localized unsafe/refinement obligation and reports the exact usage site. For memory-proof-strict runs, add --deny-linear-memory-mechanics, which fails on any remaining partially modeled linear-memory mechanic and reports the exact usage site. For event-proof-strict runs, add --deny-event-emission, which fails on any remaining raw rawLog event emission and reports the exact usage site. For low-level-proof-strict runs, add --deny-low-level-mechanics, which fails on any remaining first-class low-level call / returndata mechanic and reports the exact usage site. For proxy-proof-strict runs, add --deny-proxy-upgradeability, which fails on any remaining delegatecall-based proxy / upgradeability mechanic and reports the exact usage site; the dedicated proxy semantics gap is tracked under issue #1420. For runtime-proof-strict runs, add --deny-runtime-introspection, which fails on any remaining partially modeled runtime-introspection primitive and reports the exact usage site.

Trust Assumptions

See TRUST_ASSUMPTIONS.md for the full trust model and AXIOMS.md for axiom documentation.

Last Updated: 2026-06-19