Skip to content

Solidity feature parity: close the gap between verity_contract EDSL and production Solidity #1724

Open
Open
Solidity feature parity: close the gap between verity_contract EDSL and production Solidity#1724
@Th0rgal

Description

@Th0rgal
Th0rgal
opened on Apr 12, 2026

Goal

Bring the verity_contract EDSL and CompilationModel to feature parity with Solidity 0.8.x, so that any standard Solidity smart contract can be faithfully expressed, compiled, and verified through Verity's pipeline. This is not about supporting arbitrary Solidity syntax, but about ensuring every semantically meaningful Solidity pattern has a first-class Verity equivalent with correct compilation and (where applicable) formal verification.

Background

Verity's verity_contract macro currently supports a substantial subset of Solidity patterns, sufficient for standard DeFi contracts (ERC20, ERC721, governance, simple AMMs). However, several Solidity features that production contracts commonly use are either partially supported, missing, or have no proof coverage.

Current Solidity Interop Status (from ROADMAP.md, Issue #586)

Feature Current Status Detail
Custom errors + typed revert payloads Partial ABI encoding works for scalar + tuple/array/bytes payloads (direct param refs only); expression-arg composites fail fast
Low-level calls + returndata Partial call/staticcall/delegatecall + returndataSize/returndataCopy/revertReturndata/returndataOptionalBoolAt exist; proof coverage is zero
fallback/receive/payable modeling Partial isPayable flag exists on functions; no dedicated fallback/receive entrypoint support
Event ABI parity Supported Full indexed dynamic/tuple hashing; proof-covered
Storage layout controls Partial Packed fields, explicit slots, alias slots, reserved ranges, struct-valued mappings all exist; proof coverage is partial
ABI JSON generation Partial --abi-output emits per-contract ABI JSON; view/pure mutability markers included
String/bytes ABI support Partial ABI-level only; no storage-level string/bytes

Current Type System Coverage

Verity type Solidity equivalent Status
Uint256 uint256 Full
Int256 int256 Full
Uint8 uint8 Full
Address address Full
Bytes32 bytes32 Full
Bool bool Full
String string ABI-only (calldata/return/events); no storage
Bytes bytes ABI-only (calldata/return/events); no storage
Array T T[] Calldata arrays (read-only); storage dynamic arrays (dynamicArray) for uint256
Tuple [...] Solidity tuples ABI encoding; no first-class destructuring
— uint8–uint248 (other widths) Missing — only uint8 and uint256 exist
— int8–int248 (other widths) Missing — only int256 exists
— bytes1–bytes31 Missing — only bytes32 exists
— mapping(K => mapping(K2 => mapping(K3 => V))) Partial — mapping2 is 2-deep; mappingChain is arbitrary-depth but has no proof coverage
— struct (as storage root) Missing — only struct-valued mappings, not top-level storage structs
— enum Missing — encode as uint8 manually
— Fixed-point (ufixed/fixed) Missing — not widely used in practice

Current CompilationModel Construct Coverage

Expressions (44 constructors in CompilationModel.Expr):

  • 30+ constructors fully operational
  • Several (constructorArg, keccak256, external calls, array ops, dynamicBytesEq) operational but outside the proven fragment

Statements (31 constructors in CompilationModel.Stmt):

  • All 31 compile and execute correctly
  • ~15 are in the proven fragment; ~16 are outside (events, errors, returns, calls, array mutations)

Parity Gaps — Detailed Breakdown

P0: Missing Type Widths (Blocks Many Contracts)

Solidity contracts routinely use uint128, uint64, uint32, uint16, int128, bytes4, bytes20, etc. Currently Verity only supports uint8, uint256, int256, bytes32, address, and bool.

What to add:

  1. UintN for N ∈ {16, 32, 64, 128, 160, 224, 248} — at minimum the widths used by OpenZeppelin, Uniswap, and Morpho contracts. This requires:
    • ParamType.uintN constructor (or parameterized ParamType.uint width)
    • ABI encoding/decoding (left-pad to 32 bytes, mask on decode)
    • Storage packing support (already exists via PackedBits)
    • Arithmetic overflow checking for safe operations
  2. IntN for common signed widths — less common but needed for price feeds, time deltas
  3. BytesN for N < 32 — needed for function selectors (bytes4), short identifiers
  4. enum support — compile as bounded uint8/uint16 with range checks

P1: Storage Strings and Bytes

Currently string/bytes are ABI-only (calldata parameters, return values, events). Production contracts store strings (e.g., token name/symbol, URI storage in ERC721).

What to add:

  1. FieldType.string / FieldType.bytes storage fields
  2. Short-string optimization (≤31 bytes stored inline, matching Solidity's layout)
  3. Long-string storage (length + keccak-addressed slots)
  4. Expr.storageString / Stmt.setStorageString read/write operations
  5. String concatenation / length / comparison operations

P2: Inheritance and Interface Composition

Solidity's contract A is B, C pattern is the primary code organization mechanism. Currently, Verity contracts are flat — all functions must be defined in a single verity_contract block.

What to add:

  1. Composition model: Allow verity_contract to reference another contract's functions/storage layout as a base
  2. Virtual/override dispatch: Model Solidity's C3 linearization for virtual function resolution
  3. Interface declarations: Allow declaring expected external interfaces (for type-safe external calls)
  4. Abstract contracts: Contracts with unimplemented functions (for template patterns)

Alternative approach: Instead of full inheritance, support trait-like composition where base contract functionality is imported as a library of functions + storage layout declarations. This is simpler and arguably better for verification (explicit composition vs implicit linearization).

P3: Constructor Features

Current constructor support is basic: parameters + body. Missing:

  1. Inheritance constructor chaining: Base constructor calls
  2. Immutable initialization: Partially supported (immutables section exists for scalar types); missing: complex immutable initialization, immutable arrays/structs
  3. Constructor modifiers: payable constructor (flag exists but limited)
  4. CREATE2 / factory patterns: Constructor with salt for deterministic deployment

P4: Modifier Support

Solidity modifiers (modifier onlyOwner() { require(msg.sender == owner); _; }) are used in almost every production contract.

What to add:

  1. Modifier declarations: Named code blocks with a _ continuation point
  2. Modifier application: Function annotations that wrap the function body
  3. Modifier composition: Multiple modifiers on a single function (chained execution)
  4. Compilation: Inline modifier bodies around the function body at compile time (matching solc behavior)

Simpler alternative: Modifiers are syntactic sugar for require checks at function entry. A preconditions: [...] section in verity_contract functions could capture the same pattern without the complexity of _ continuation semantics.

P5: Advanced Control Flow

Feature Status What to add
if/else Supported —
for loops Supported (as forEach with bound) True for(init; cond; post) with arbitrary conditions
while loops Missing while(cond) { body } — desugar to for(; cond; ) { body }
do-while Missing do { body } while(cond)
break/continue Missing in EDSL Available at Yul level; need EDSL surface
try/catch Missing External call error handling (low-level call + returndata check pattern exists)
Early return Supported —
Multiple return values Partial returnValues exists; no destructuring assignment
Ternary operator Supported Expr.ite

P6: Memory and ABI Features

Feature Status What to add
abi.encode Missing as first-class Used implicitly in events/errors; no general-purpose abi.encode
abi.encodePacked Missing Needed for keccak256(abi.encodePacked(...)) patterns
abi.encodeWithSelector Missing Needed for low-level call construction
abi.decode Missing as first-class Used implicitly in return decoding
type(X).max / .min Missing Type introspection constants
block.prevrandao Missing Available as EVM opcode but no CompilationModel expression
gasleft() Missing Available as EVM opcode
address(this).balance Missing SELFBALANCE opcode
msg.sig Missing First 4 bytes of calldata
msg.data Missing Raw calldata access (beyond calldataload)

P7: Advanced Storage Patterns

Feature Status What to add
Storage structs (top-level) Missing Only struct-valued mappings exist
Nested mappings (3+ deep) Partial mappingChain exists but no proof coverage
Storage arrays of structs Missing Only uint256 dynamic arrays
Constant storage layout compatibility Partial Explicit slots + reserved ranges exist
Transient storage (tstore/tload) Supported First-class in CompilationModel
Storage packing Supported Via PackedBits
delete Missing Zero-out storage slot/mapping/array

P8: External Interaction Patterns

Feature Status What to add
call/staticcall/delegatecall Supported (first-class) Proof coverage needed
transfer/send Missing Deprecated but used in legacy contracts; model as call with 2300 gas
Re-entrancy guards Partial Can be manually built with transient storage; no first-class nonReentrant
Multicall patterns Missing delegatecall to self with encoded calldata
Proxy patterns (UUPS, transparent) Outside proof model delegatecall + storage slot patterns; tracked in #1420
CREATE/CREATE2 Missing Contract creation opcodes
selfdestruct N/A Deprecated in Solidity

Proposed Execution Order

Wave 1: Type System Completeness (4–6 weeks)

  1. Parameterized uint widths (UintN for common widths) — unblocks the most contracts
  2. Parameterized int widths (IntN)
  3. Parameterized bytesN — needed for selectors, short identifiers
  4. Enum support — compile as bounded uint

Wave 2: Control Flow and Modifiers (3–4 weeks)

  1. while loops — desugar to for
  2. break/continue — surface in EDSL, already available at Yul level
  3. Modifier support — either _ continuation or preconditions sugar
  4. Multiple return value destructuring

Wave 3: Storage Completeness (4–6 weeks)

  1. Storage strings/bytes — short-string optimization + long storage
  2. Top-level storage structs — named field access without mapping key
  3. delete semantics — zero-out patterns
  4. Storage arrays of arbitrary types — beyond uint256
  5. Deep nested mappings — proof coverage for mappingChain

Wave 4: ABI and Memory (3–4 weeks)

  1. First-class abi.encode/abi.encodePacked/abi.decode
  2. First-class abi.encodeWithSelector
  3. type(X).max/.min constants
  4. Missing environment reads (block.prevrandao, gasleft(), address(this).balance, msg.sig)

Wave 5: Composition and Inheritance (6–8 weeks)

  1. Contract composition model (base contracts / trait imports)
  2. Virtual/override dispatch (or explicit override declarations)
  3. Interface declarations
  4. Constructor chaining

Wave 6: Advanced Interactions (4–6 weeks)

  1. Re-entrancy guard as first-class primitive
  2. try/catch sugar over low-level call + returndata check
  3. CREATE/CREATE2 support
  4. Proxy pattern support (connects to Verification: proxy and upgradeability semantics on top of native delegatecall support #1420)

Beyond Parity: Language Design Improvements (#1726)

While this issue tracks reaching Solidity feature parity, #1726 tracks going beyond parity by fixing Solidity's systemic design flaws at the language level. The beyond-parity features integrate into this issue's waves:

Wave Parity Features (this issue) Beyond-Parity Features (#1726)
Wave 1: Type System uint/int/bytes widths, enum + Semantic newtypes (types section) — #1727
+ ADTs + exhaustive match — #1727
Wave 2: Control Flow & Safety while/break/modifiers + CEI enforcement with proof opt-out — #1728
+ @[requires Role] with auto-theorems — #1728
+ Effect annotations (@[view]/@[modifies]) with auto-theorem generation — #1729
Wave 3: Storage strings/bytes, structs, delete + Automatic EIP-7201 namespaced storage — #1730
Wave 4: ABI & Memory abi.encode, type introspection + Call.Result type with match + ! sugar — #1727
Wave 5: Composition inheritance, interfaces + Explicit unsafe blocks — #1728
Wave 6: Advanced Interactions try/catch, CREATE2 (no additions)

Axis Sub-Issues

Relationship to Other Issues

Success Criteria

Minimum Viable Parity (Waves 1–3)

  • All uint widths 8/16/32/64/128/160/224/256 supported
  • All int widths supported
  • bytesN for common widths supported
  • while loops, break/continue available in EDSL
  • Modifier or precondition support
  • Storage strings/bytes (short + long)
  • Top-level storage structs
  • An OpenZeppelin ERC20 can be expressed 1:1 in verity_contract
  • A Uniswap V2 Pair can be expressed in verity_contract (or documented gap list < 5 items)

Full Parity (Waves 1–6)

  • Every Solidity 0.8.x language feature has a verity_contract equivalent or a documented, justified exclusion
  • Contract composition/inheritance model exists
  • CREATE2 + factory patterns work
  • A Morpho Vault contract can be fully expressed
  • Feature parity matrix in ROADMAP.md shows "supported" for all P0–P2 items
  • verity-compiler diagnostics guide migration for any remaining unsupported patterns

Estimated Effort

  • Minimum Viable Parity (Waves 1–3): 3–4 months
  • Full Parity (all waves): 8–12 months

Waves 1 and 2 can be parallelized. Waves 3 and 4 can be parallelized.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions