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

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 #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

• #1727 — Axis 1: Type System Enrichment: Semantic newtypes, ADTs + pattern matching, Call.Result type
• #1728 — Axis 2: Compile-Time Safety Enforcement: CEI enforcement (proof-based opt-out), @[requires Role] (auto-theorems), unsafe blocks
• #1729 — Axis 3: Effect System & Auto-Theorem Generation: @[view]/@[modifies]/@[no_external_calls] verified annotations that generate frame condition theorems
• #1730 — Axis 4: Storage Safety: Automatic EIP-7201 namespaced storage from contract name

Relationship to Other Issues

• #1722 (EVMYulLean migration): Provides the semantic foundation — new Solidity features compile to Yul that is verified against EVMYulLean.
• #1723 (Proven fragment extension): Each new feature added here should ideally land inside the proven fragment. The two issues track different axes: #1723 is "prove what we already have", this issue is "add what we don't have yet". Axis 3 (#1729) directly accelerates #1723 via auto-generated frame theorems.
• #1726 (Language design improvements): Beyond-parity features that enrich this issue's waves with safety guarantees. See table above.
• #1727 (Type system enrichment): Newtypes, ADTs, Result types — enriches Waves 1 and 4.
• #1728 (Safety enforcement): CEI, access control, unsafe — enriches Waves 2 and 5.
• #1729 (Effect system): Auto-theorem generation from annotations — enriches Wave 2 and accelerates #1723.
• #1730 (Storage safety): EIP-7201 namespaces — enriches Wave 3.
• #586 (Solidity interop profile): This issue is the implementation plan for the features tracked in #586's matrix.
• #1680 (Language completeness): Overlapping scope — this issue is more detailed and Solidity-focused.
• #1569 (Constants/immutables): Already delivered; constants and immutable scalars are in the macro.

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.

Begin with ROADMAP.md and Issue #586, then inspect the verity_contract macro and CompilationModel.Expr/Stmt coverage. Pick one explicitly scoped parity gap, such as parameterized widths or while loops, trace its existing ABI, compiler, or Yul entry points, and define completion with implementation plus proof coverage where required.