# EDSL API Reference

Canonical reference for primitives used to write Verity contracts.

```verity
import Verity
open Verity
open Verity.EVM.Uint256
open Verity.Stdlib.Math
```

Every primitive is a `Contract α = ContractState → ContractResult α`. Read-only primitives never revert; write primitives return `success ()`; only `require` and `requireSomeUint` (and `revertError`) may emit `ContractResult.revert`. Proof lemmas for every primitive live in `Verity/Core.lean` (one `_run` lemma per primitive) and `Verity/Proofs/Stdlib/Automation.lean` / `Verity/Proofs/Stdlib/MappingAutomation.lean` (`_runState` / `_runValue` mirrors). See [Core Architecture](/core) for the model.

## Storage

| Function | Type |
|----------|------|
| `getStorage` / `setStorage` | `StorageSlot Uint256 → …` |
| `getStorageAddr` / `setStorageAddr` | `StorageSlot Address → …` |
| `getMapping` / `setMapping` | `StorageSlot (Address → Uint256) → Address → …` |
| `getMappingAddr` / `setMappingAddr` | Address-keyed mapping with address values (`wordToAddress` under the hood) |
| `getMappingUint` / `setMappingUint` | `StorageSlot (Uint256 → Uint256) → Uint256 → …` |
| `getMappingUintAddr` / `setMappingUintAddr` | Uint-keyed mapping with address values |
| `getMapping2` / `setMapping2` | `StorageSlot (Address → Address → Uint256) → Address → Address → …` |
| `getStorageArrayLength` / `getStorageArrayElement` / `setStorageArrayElement` | Dynamic in-storage arrays with `[StorageArrayElem α]` typeclass |
| `pushStorageArray` / `popStorageArray` | Append / remove tail element of an in-storage array |

```verity
let bal   <- getMapping balances msgSenderAddr
let owner <- getMappingUintAddr tokenOwners tokenId
setMapping balances msgSenderAddr (bal - amount)

let allow <- getMapping2 allowances owner spender
setMapping2 allowances owner spender (allow - amount)
```

The `addressToWord` / `wordToAddress` helpers convert between the two representations; the `*Addr` mapping variants apply them automatically.

## Control flow

```verity
def require (condition : Bool) (message : String) : Contract Unit
def bind {α β : Type} (ma : Contract α) (f : α → Contract β) : Contract β
```

`require false msg` is the only revert primitive. Use it in place of an explicit `revert`. `bind` short-circuits on revert and powers do-notation.

```verity
require (amount > 0) "amount must be nonzero"
let x <- getStorage counterSlot
setStorage counterSlot (x + 1)
```

### `Contract.tryCatch`

```verity
def Contract.tryCatch {α : Type} (attempt : Contract α) (handler : String → Contract Unit) : Contract α
```

If `attempt` reverts with message `msg`, `tryCatch` runs `handler msg` on the state *before* the revert and returns whatever `handler` returns (or the original revert if `handler` itself reverts). Useful for fallback paths inside a contract. See `Verity/Core.lean` for the exact semantics.

### `forEach`

Bounded iteration in the compilation-model surface (`Stmt.forEach`). Accumulator-style loops use `Stmt.assignVar` inside `Stmt.forEach`; the macro path currently rejects mutating `let mut` locals from nested `forEach` bodies, so macro-authored contracts should use explicit memory scratch space for accumulators.

```verity
forEach "i" count (do
  -- body
)
```

## Events

```verity
def emitEvent (name : String) (args : List Uint256) (indexedArgs : List Uint256 := []) : Contract Unit

emitEvent "Transfer" [amount] [fromAddr, toAddr]
```

## Arithmetic

### Wrapping (`Uint256`)

`add`, `sub`, `mul`, `pow`, `div`, `mod`, EVM modular arithmetic. `pow a b` / `a ^ b` compiles to Yul `exp(a, b)`.

```verity
let z : Uint256 := add x y
let scale : Uint256 := pow 10 decimals
```

### Checked (`Stdlib.Math`)

```verity
def safeAdd (a b : Uint256) : Option Uint256
def safeSub (a b : Uint256) : Option Uint256
def safeMul (a b : Uint256) : Option Uint256
def safeDiv (a b : Uint256) : Option Uint256

def requireSomeUint (opt : Option Uint256) (message : String) : Contract Uint256

let sum     <- requireSomeUint (safeAdd a b) "overflow"
let product <- requireSomeUint (safeMul a b) "overflow"
let quot    <- requireSomeUint (safeDiv a b) "division by zero"
```

`verity_contract` lowers `requireSomeUint` over `safeAdd`/`Sub`/`Mul`/`Div` to explicit compiled `require` guards. Bare `add`/`sub`/`mul`/`div` stay wrapping.

### Fixed-point helpers

In `Stdlib.Math`: `mulDivDown`, `mulDivUp`, `wMulDown`, `wDivUp`, `SNARK_SCALAR_FIELD`, `modField`. Full-precision proof helpers: `mulDiv512Down?`, `mulDiv512Up?` (return `Option Uint256`; `none` on zero divisor or quotient overflow). First-class compiler lowering for a 512-bit division primitive is tracked separately.

## Context accessors

```verity
def msgSender       : Contract Address
def contractAddress : Contract Address
def msgValue        : Contract Uint256
def blockTimestamp  : Contract Uint256
def blockNumber     : Contract Uint256
def blobbasefee     : Contract Uint256
```

## `verity_contract` authoring surface

### Local obligations

```verity
function unsafeEdge ()
  local_obligations [manual_delegatecall_refinement := assumed "Caller proves the handwritten assembly path."]
  : Unit := do
  pure ()
```

Each entry lowers into `localObligations`, surfaces in `--trust-report`, and participates in `--deny-local-obligations`. Direct assembly-shaped primitives (raw low-level calls, returndata forwarding, manual memory/calldata) without a local obligation fail closed.

### Same-contract helpers

Call helpers with ordinary function-call syntax, do not write `internalCall` directly (those are post-lowering IR nodes).

```verity
storeBump x
let y ← bump x
let (assets, shares) ← preview seed
```

The macro lowers effect-only calls to `Stmt.internalCall`, result bindings to `Stmt.internalCallAssign`, expression-position calls to `Expr.internalCall`. Supports scalar parameters, static tuples/structs, direct `Bytes`/dynamic-array forwarding from caller ABI. Dynamic returns use explicit return surfaces only.

### Tuple sugar

```verity
let (first, second) := pair
let (_, second) := pair
let (assets, shares) ← preview seed
let (supply, borrow, delegate_) := structMembers positions user [supplyShares, borrowShares, delegate]
return (first, second)
```

Tuple-typed parameters stay shape-preserved as right-nested Lean products; ABI-flattened aliases (`pair_0`, `pair_1`, …) are injected so you can use them directly. `_` binders are accepted and discarded hygienically.

### Stateless contracts and payable / initializer constructors

```verity
verity_contract Stateless where
  storage   -- empty block is allowed

  function whoAmI () : Address := do
    let sender ← msgSender
    return sender
```

```verity
constructor (seedOwner : Address) payable := do
  setStorageAddr owner seedOwner
```

`payable` removes the `callvalue` guard and emits `stateMutability: "payable"` in the ABI.

```verity
function initOwner (seedOwner : Address) initializer(initializedVersion) : Unit := ...
function upgradeToV2 ()                 reinitializer(initializedVersion, 2) : Unit := ...
```

`initializer(slot)` prepends `require(slot == 0, ...)` then stores `1`. `reinitializer(slot, n)` requires the tracked version `< n`, then stores `n`. Guard slots must be user-declared `Uint256` fields.

### Constants and immutables

```verity
constants
  basisPoints : Uint256 := 10000
  mintFeeBps  : Uint256 := 30
  treasury    : Address := (wordToAddress 42)

immutables
  seededSupply : Uint256 := add seed offset
  treasury     : Address := ownerSeed
  paused       : Bool    := true
  feeBps       : Uint8   := 7
  domainTag    : Bytes32 := 42
```

Constants inline into `Expr` trees at compile time; constant bodies cannot reference runtime builtins (`blockTimestamp`, calldata reads, low-level opcodes, etc.), those are rejected at elaboration. Immutables lower to read-only `__immutable_<name>` slots seeded in the constructor. Supported immutable types: `Uint256`, `Uint8`, `Address`, `Bytes32`, `Bool`.

Storage, constants, immutables, and functions share one namespace; duplicate or cross-kind reuse is rejected with explicit diagnostics. Generated names (`spec`, `<name>_modelBody`, `<name>_model`, `<name>_bridge`, `<name>_semantic_preservation`) are reserved.

### Linked externals

```verity
linked_externals
  external echo(Uint256) -> (Uint256)

function storeQuote (value : Uint256) : Unit := do
  let quoted := externalCall "echo" [value]
  setStorage lastQuote quoted
```

Populates `spec.externals` with assumed foreign signatures. Single-word argument/return types only (`Uint256`, `Uint8`, `Address`, `Bytes32`, `Bool`); at most one return. Dynamic and tuple-shaped linked externals are rejected at elaboration.

### Raw log surface

```verity
rawLog [topic0, add topic1 1] dataOffset dataSize
```

Lowers to `Stmt.rawLog`. Supports 0–4 topics (`log0`–`log4`). Classified as not-modeled event emission in the trust report, use `--deny-event-emission` for proof-strict runs.

### Transient storage (EIP-1153)

```verity
tstore slot value
let warmed := tload slot
```

Lowers to `Stmt.tstore` / `Expr.tload`. The executable path keeps a separate `ContractState.transientStorage` map. Classified under `lowLevelMechanics` in the trust report.

### Dynamic arrays

```verity
let count := arrayLength recipients
let first := arrayElement recipients 0
returnArray amounts
```

`arrayElement` is bounds-checked (compiled path reverts on out-of-range; executable fallback mirrors). Supports scalar arrays and ABI-decodable static/nested struct arrays. Dynamic-element arrays (`Array Bytes`, `Array String`) support `arrayLength` only; indexed reads and `returnArray` are rejected for those until offset-aware lowering lands.

`String`/`Bytes` support ABI transport (`returnBytes`, custom-error/event payloads, parameter flow) and direct `==`/`!=` checks. Other word-level operators (`<`, `add`, `logicalAnd`) on `String`/`Bytes` are rejected, applies to function bodies, constructor bodies, constants, and immutable initializers.

### Modifiers, structs, ADTs, and namespaced storage

`verity_contract` also supports Solidity-style **modifiers** (`modifier onlyRelayer := do ...` then `with onlyRelayer`), **struct declarations** (including packed storage structs via `@word N packed(byteOffset, byteWidth)`), **algebraic data types**, **newtype wrappers**, **storage namespaces** (`storage_namespace erc7201 "myapp.storage.X"`), and **mapping-of-struct** sugar (`MappingStruct`, `MappingStruct2`). The full grammar lives in [`Verity/Macro/Syntax.lean`](https://github.com/lfglabs-dev/verity/blob/main/Verity/Macro/Syntax.lean); concrete usage shapes are in the [production Solidity patterns guide](/guides/production-solidity-patterns).

### Custom errors

```verity
errors
  error NonPositive(Uint256)
  error AmountTooLarge(Uint256, Uint256)

function requirePositive (amount : Uint256) : Unit := do
  requireError (amount != 0) NonPositive(amount)

function rejectLarge (amount : Uint256) : Unit := do
  if amount > 100 then
    revert AmountTooLarge(amount, 100)
```

Populates `CompilationModel.errors`; guarded and unconditional custom-error exits lower to `Stmt.requireError` / `Stmt.revertError`.

## External Calls (ECM)

External calls are modeled as **Externally Callable Modules** (ECMs), statement constructors that ABI-encode arguments, perform a `call` / `staticcall`, validate the return shape, and bind the result word. They carry explicit trust-report metadata; module-level `axioms` apply rather than pure `simp`-style contract lemmas.

### ERC-20 helpers

Inside `verity_contract` bodies, the standard names lower directly:

```verity
safeTransfer token to amount
safeTransferFrom token fromAddr to amount
safeApprove token spender amount

let balance <- balanceOf token owner
let current <- allowance token owner spender
let supply  <- totalSupply token
```

These compile to `Compiler.Modules.ERC20.*Module` ECMs. If the contract defines a same-named function with matching arity, the helper form is rejected to avoid ambiguity.

### ERC-4626 vault helpers

Twelve ECMs share one template: ABI-encode the selector + static args, `staticcall` (or `call` for state-changing), expect one 32-byte return word, bind it.

```verity
Compiler.Modules.ERC4626.previewDeposit  (resultVar : String) (vault assets   : Expr) : Stmt
Compiler.Modules.ERC4626.previewMint     (resultVar : String) (vault shares   : Expr) : Stmt
Compiler.Modules.ERC4626.previewWithdraw (resultVar : String) (vault assets   : Expr) : Stmt
Compiler.Modules.ERC4626.previewRedeem   (resultVar : String) (vault shares   : Expr) : Stmt
Compiler.Modules.ERC4626.convertToAssets (resultVar : String) (vault shares   : Expr) : Stmt
Compiler.Modules.ERC4626.convertToShares (resultVar : String) (vault assets   : Expr) : Stmt
Compiler.Modules.ERC4626.totalAssets     (resultVar : String) (vault          : Expr) : Stmt
Compiler.Modules.ERC4626.asset           (resultVar : String) (vault          : Expr) : Stmt
Compiler.Modules.ERC4626.maxDeposit      (resultVar : String) (vault receiver : Expr) : Stmt
Compiler.Modules.ERC4626.maxMint         (resultVar : String) (vault receiver : Expr) : Stmt
Compiler.Modules.ERC4626.maxWithdraw     (resultVar : String) (vault owner    : Expr) : Stmt
Compiler.Modules.ERC4626.maxRedeem       (resultVar : String) (vault owner    : Expr) : Stmt
Compiler.Modules.ERC4626.deposit         (resultVar : String) (vault assets receiver : Expr) : Stmt
```

`asset` masks the returned word to 160 bits. `deposit` uses `call` (state-changing). Each module records a corresponding `erc4626_<name>_interface` assumption in the trust report.

### Precompiles and hashing

```verity
Compiler.Modules.Precompiles.ecrecover        -- `let signer <- ecrecover digest v r s` in macro surface
Compiler.Modules.Precompiles.sha256Memory     -- aliased as `sha256`
Compiler.Modules.Hashing.abiEncodePackedWords -- contiguous-word keccak256
Compiler.Modules.Hashing.sha256PackedWords    -- contiguous-word SHA-256 via 0x02
Compiler.Modules.Hashing.abiEncodePackedStaticSegments  -- mixed widths, 1–32 bytes each
Compiler.Modules.Hashing.sha256PackedStaticSegments
```

```verity
Compiler.Modules.Hashing.abiEncodePackedWords "digest"
  [Expr.param "root", Expr.param "contextHash", Expr.param "nullifier"]
```

Segment widths in 1–32 bytes; sub-word values are left-aligned. Dynamic `bytes`/`string` packed encoding stays outside this core surface. Trust report records `evm_ecrecover_precompile`, `evm_sha256_precompile`, etc.

### Oracle and generic calls

```verity
Compiler.Modules.Oracle.oracleReadUint256
  (resultVar : String) (target : Expr) (selector : Nat) (staticArgs : List Expr) : Stmt

Compiler.Modules.Calls.withReturn
  (resultVar : String) (target : Expr) (selector : Nat) (args : List Expr) (isStatic : Bool := false) : Stmt

Compiler.Modules.Calls.bubblingValueCall
  (target value inputOffset inputSize outputOffset outputSize : Expr) : Stmt
```

`Oracle.oracleReadUint256` is the standard read-only oracle case; trust-report assumption `oracle_read_uint256_interface`.

### `keccak256` primitive

```verity
let digest := keccak256 offset size
```

Elaborates to `Expr.keccak256`; lowers to Yul `keccak256(offset, size)`. The machine-readable trust report records the explicit primitive assumption `keccak256_memory_slice_matches_evm`.

`Expr.keccak256` also remains an explicit proof boundary today: the compiler supports it directly, but the current proof stack still treats it as an axiomatized primitive instead of a fully modeled operation. When it appears, archive `--trust-report` and use `--deny-axiomatized-primitives` for proof-strict runs (see issue `#1411`).

### `tryCatch`

```verity
tryCatch (call gas target value inOffset inSize outOffset outSize) (do
  setStorage lastFailure 1)
```

Lowers to a synthetic `letVar` + `ite` entering the catch block when the result word is `0`. Low-level call-like expressions only; catch-payload decoding is not modeled yet.

### Low-level `call` / `staticcall` / `delegatecall`

First-class forms exist in the compilation model (`Expr.call`, `Expr.staticcall`, `Expr.delegatecall`). They are not yet modeled by the current proof interpreters. In the machine-readable interpreter feature matrix, low-level call plumbing and returndata behavior remain a compiler-and-testing trust boundary rather than a proved semantic feature today.

When the low-level form is `delegatecall`, the trust report now also isolates it as a dedicated proxy / upgradeability boundary; archive `--trust-report` and use `--deny-proxy-upgradeability` for proof-strict runs (see issue `#1420`).

First-class linear-memory forms (`Expr.mload`, `Stmt.mstore`, `Stmt.calldatacopy`, `Stmt.returndataCopy`, `Expr.returndataOptionalBoolAt`) also compile today, but they are still only partially modeled by the current proof interpreters. When they appear, treat them as an explicit memory/ABI trust boundary, archive `--trust-report`, and use `--deny-linear-memory-mechanics` for proof-strict runs (see issue `#1411`).

Prefer ECM wrappers when they fit. For the remaining unavoidable cases, attach a `localObligations` entry at the usage site and discharge it before shipping.