Axis 1: Type system enrichment — newtypes, ADTs, pattern matching, Result types

[Th0rgal]

Goal

Enrich Verity's type system beyond Solidity's flat uint256-for-everything model by adding semantic newtypes, algebraic data types (ADTs) with exhaustive pattern matching, and a Call.Result type for external calls. These are the type-level features that prevent entire classes of bugs at compile time.

Parent issue: #1726 (Language design improvements)
Connects to: #1724 Waves 1, 4 (type widths, ABI features)

---

Feature 1: Semantic Newtypes (P0)

Problem

Everything in Solidity is `uint256`. Wei, token amounts, timestamps, slot indices, and percentages are all the same type. This caused the Parity multisig freeze (~$280M) and countless DeFi exploits from mixing up raw amounts vs. scaled amounts (WAD vs. RAY vs. raw).

Why Language-Level Change is Required

The `verity_contract` macro has a fixed grammar (defined in `Macro/Syntax.lean`) that only accepts: `storage`, `errors`, `constants`, `immutables`, `linked_externals`, `constructor`, special entrypoints, and `function` blocks. There is no slot for custom type definitions.

`ParamType` is a closed inductive with exactly 11 variants (`uint256`, `int256`, `uint8`, `address`, `bool`, `bytes32`, `string`, `tuple`, `array`, `fixedArray`, `bytes`). The parser `valueTypeFromSyntax` only recognizes those exact identifiers. You can define Lean structures outside the contract block, but you cannot use them as parameter/storage types.

Design

Add a `types` section to the `verity_contract` grammar:

```
verity_contract MyToken where
types
Wei : Uint256 -- newtype wrapper, zero-cost
Shares : Uint256
Timestamp : Uint256

storage
totalAssets : Wei := slot 0
totalShares : Shares := slot 1

function deposit (assets : Wei) : Unit := do
-- COMPILE ERROR: can't add Wei + Shares without explicit conversion
-- let wrong ← safeAdd assets totalShares
-- OK: explicit conversion required
let shares := Shares.wrap (Wei.unwrap assets)
...
```

Implementation Plan

1. Syntax (`Macro/Syntax.lean`): Add `types` section with `typeName : baseType` entries
2. ParamType (`CompilationModel/Types.lean`): Add `| newtypeOf (name : String) (base : ParamType)` constructor
3. valueTypeFromSyntax (`Macro/Translate.lean`): Resolve user-defined type names from the contract's `types` block
4. Macro elaboration (`Macro/Elaborate.lean`): Generate `structure Wei where val : Uint256` for each newtype, with `.wrap`/`.unwrap` accessors
5. Compilation (`CompilationModel/Compile.lean`): Erase newtypes — compile to the base type's Yul. Zero runtime overhead.
6. Validation: Reject operations between mismatched newtypes at macro elaboration time
7. ABI: Newtypes encode as their base type in the ABI JSON

Estimated effort: 2–3 weeks

---

Feature 2: Algebraic Data Types + Exhaustive Pattern Matching (P1)

Problem

Solidity has flat enums (just integers) and no sum types. This leads to forgotten enum cases (no exhaustiveness checking), boolean blindness, and no way to represent typed alternatives. 51.4% of Solidity developers want algebraic datatypes; 34% want pattern matching (Developer Survey 2024).

Design

Add an `inductive` section to the `verity_contract` grammar:

```
verity_contract Governance where
inductive ProposalState where
| Pending -- tag 0, no payload
| Active (forVotes : Uint256) (againstVotes : Uint256) -- tag 1, 2 words
| Executed -- tag 2, no payload
| Defeated -- tag 3, no payload

storage
proposalState : Uint256 → ProposalState := slot 5

function processProposal (id : Uint256) : Unit := do
let state ← getProposalState id
match state with
| .Pending => activateProposal id
| .Active forVotes againstVotes =>
if forVotes > againstVotes then executeProposal id
else defeatProposal id
| .Executed => revert "Already executed"
| .Defeated => revert "Already defeated"
-- Missing a case = Lean compile error (exhaustiveness is free)
```

Storage Encoding

ADT values stored as tagged unions in consecutive slots:

```
slot + 0: tag (uint8 value)
slot + 1: field_0 (if any)
slot + 2: field_1 (if any)
...
```

Layout uses max-width of all variants. `ProposalState` always occupies 3 slots (tag + 2 words) regardless of active variant, matching Rust's enum layout strategy.

New CompilationModel Constructs

ParamType:
```lean
| adt (name : String) (variants : List (String × List ParamType))
```

Expr (3 new constructors):
```lean
| adtConstruct (typeName : String) (variantIdx : Nat) (args : List Expr)
| adtTag (value : Expr) -- extracts tag byte
| adtField (value : Expr) (fieldIdx : Nat) -- extracts field at index
```

Stmt (1 new constructor):
```lean
| matchAdt (scrutinee : Expr) (arms : List (Nat × List String × List Stmt))
-- (variantIdx, bound variable names, body statements)
```

Yul Lowering

`matchAdt` compiles to `YulStmt.switch` (already exists in the Yul AST):

```yul
{
let __tag := sload(scrutinee_slot)
switch __tag
case 0 { // Pending
// body
}
case 1 { // Active
let forVotes := sload(add(scrutinee_slot, 1))
let againstVotes := sload(add(scrutinee_slot, 2))
// body
}
case 2 { /* Executed body / }
case 3 { / Defeated body */ }
default { revert(0, 0) } // invalid tag = corruption
}
```

`adtConstruct` compiles to sequential `sstore` calls:
```yul
sstore(slot, tag)
sstore(add(slot, 1), field_0)
sstore(add(slot, 2), field_1)
```

ABI Encoding

For function parameters/return values: `abi.encode(uint8 tag, type_0 field_0, type_1 field_1, ...)` using max-width encoding (all field positions present, unused ones zeroed).

Exhaustiveness

Lean's kernel already checks exhaustiveness. When the macro generates the `match` expression, the Lean elaborator rejects non-exhaustive matches before compilation. This is free — no extra implementation.

Implementation Plan

1. Syntax (`Macro/Syntax.lean`): Add `inductive` section
2. ParamType (`CompilationModel/Types.lean`): Add `adt` constructor
3. Expr/Stmt (`CompilationModel/Types.lean`): Add `adtConstruct`, `adtTag`, `adtField`, `matchAdt`
4. Translate (`Macro/Translate.lean`): Parse `match ... with` into `Stmt.matchAdt`
5. Compile (`CompilationModel/Compile.lean`): Lower `matchAdt` to `YulStmt.switch`, lower `adtConstruct` to sequential sstores
6. Validation (`CompilationModel/Validation.lean`): Validate tag range, field count per variant
7. SupportedSpec: Initially outside proven fragment; add incrementally

Estimated effort: 4–6 weeks

---

Feature 3: `Call.Result` Type (P1)

Problem

External calls return `(bool success, bytes memory data)` which developers routinely ignore. The Dexible hack ($2M) exploited unchecked return values.

Design

`Call.Result` is an ADT (builds on Feature 2):

```lean
inductive Call.Result where
| ok (data : Bytes)
| err (data : Bytes)
```

Usage in contracts:
```
function safeTransfer (token : Address, to : Address, amount : Uint256) : Unit := do
let result ← externalCall token "transfer(address,uint256)" [to, amount]
match result with
| .ok _ => pure ()
| .err e => revert (formatError e)

-- Or shorthand (bang operator = revert on failure):
externalCall! token "transfer(address,uint256)" [to, amount]
```

Implementation

• `Call.Result` is a built-in ADT (no user definition needed), available in every contract
• `externalCall` returns `Call.Result` instead of raw `Uint256` success flag
• The `!` sugar desugars to `match result with | .ok d => d | .err e => revertReturndata`
• Lint warning if `Call.Result` is bound but never matched

Estimated effort: 2–3 weeks (after ADTs are implemented)

---

Execution Order

1. Newtypes first (P0, standalone, 2–3 weeks)
2. ADTs + match second (P1, larger, 4–6 weeks)
3. Call.Result third (P1, builds on ADTs, 2–3 weeks)

Related Issues

• Language design improvements: fix Solidity's systemic flaws, inspired by Rust/Cairo/Move #1726 — Parent: language design improvements
• Solidity feature parity: close the gap between verity_contract EDSL and production Solidity #1724 — Solidity parity (Waves 1, 4)
• Extend proven fragment to cover the full CompilationModel language surface #1723 — Proven fragment extension (ADTs initially outside, added incrementally)