# Solidity-to-Verity Translation Guide

This guide is the practical path for converting a Solidity contract into the
`verity_contract` surface. Add proofs once the source shape and generated model
are stable.

It focuses on:

1. Direct syntax and semantic mappings.
2. Patterns that require restructuring.
3. A worked translation walkthrough.
4. Common pitfalls that cause incorrect translations.

For production contracts with inheritance, modifiers, external protocols, packed
hashes, precompiles, and ZK boundaries, pair this page with
[Production Solidity Patterns](/guides/production-solidity-patterns). That guide
is the agent-facing checklist for reusing Verity's existing surfaces instead of
inventing parallel helpers.

## 1. Direct Mappings

Use this table as your first-pass conversion checklist.

| Solidity | Verity EDSL |
|---|---|
| `uint256 public x;` | `x : Uint256 := slot 0` inside `storage` |
| `mapping(address => uint256) balances;` | `balances : Address -> Uint256 := slot 1` |
| `mapping(bytes32 => Circuit) circuits;` | `circuits : MappingStruct(Uint256,[...]) := slot n` |
| ERC-7201 storage root | `storage_namespace erc7201 "package.storage.Name"` before that root's fields |
| nested storage struct | `state : StorageStruct [...] := slot n` |
| `bytes calldata data` | `data : Bytes` |
| `Transaction[] calldata txs` | `txs : Array Transaction` |
| `msg.sender` | `msgSender` |
| `require(cond, "msg")` | `require cond "msg"` |
| `revert CustomError(...)` | `revertError CustomError(...)` |
| `x = y + z` (checked) | `let sum <- requireSomeUint (safeAdd y z) "overflow"` then `setStorage xSlot sum` |
| `x = y - z` (checked) | `let d <- requireSomeUint (safeSub y z) "underflow"` then `setStorage xSlot d` |
| `x = y * z` (checked) | `let p <- requireSomeUint (safeMul y z) "overflow"` then `setStorage xSlot p` |
| `x = y / z` (checked) | `let q <- requireSomeUint (safeDiv y z) "division by zero"` then `setStorage xSlot q` |
| `balances[a]` | `let v ← getMapping balances a` |
| `balances[a] = v` | `setMapping balances a v` |
| `allowances[a][b]` | `let v ← getMapping2 allowances a b` |
| `tokenOwners[id]` (address-valued uint-keyed) | `let owner ← getMappingUintAddr tokenOwners id` |
| `emit Transfer(from, to, amount)` | `emitEvent "Transfer" [amount] [addressToWord from, addressToWord to]` |
| `return v;` | `pure v` (or `return v` inside `verity_contract`) |

## 2. Patterns That Need Restructuring

Some Solidity features are not 1:1 in the current EDSL/compiler pipeline.

### Inheritance -> Explicit Composition

- Solidity: `contract Child is Ownable, ERC20 { ... }`
- Verity: compose the inherited storage roots, guards, and helpers explicitly.
- Use `storage_namespace erc7201 "..."` for each inherited ERC-7201 root when
  the source uses namespaced storage.
- Put shared checks in reusable EDSL helpers (for example `onlyOwner`).

### Modifiers -> Guard Helpers

Solidity:

```solidity
modifier onlyOwner() {
    require(msg.sender == owner, "not owner");
    _;
}
```

Verity pattern:

```verity
verity_contract OwnedExample where
  storage
    owner : Address := slot 0

  function onlyOwner () : Unit := do
    let currentOwner ← getStorageAddr owner
    let sender ← msgSender
    require (sender == currentOwner) "not owner"

  function restricted () : Unit := do
    onlyOwner
    -- restricted body
```

Call helpers directly by name. `internalCall` and `internalCallAssign` are the lowered compilation-model nodes for helper calls, not the source syntax to write in `verity_contract`.

### try/catch

Partial support exists today via low-level `tryCatch` sugar in `verity_contract`:

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

This lowers to a low-level call result check plus an `ite` on the returned success word, so it works for raw `call` / `staticcall` / `delegatecall`-style expressions that already return `0` on failure.

What is still missing under issue `#1161`:

- Solidity-style first-class `try/catch` over higher-level external-call helpers / ECMs
- catch-payload decoding on the compilation-model path; the handler binder must currently be ignored (`_`) and returndata must be read explicitly if needed

Those low-level call mechanics compile, but they are still outside the current proof-interpreter semantics; treat them as an explicit trust boundary for now (see issue `#1332`). Treat `delegatecall` even more strictly: it is also tracked as a dedicated proxy / upgradeability boundary, so archive `--trust-report` and use `--deny-proxy-upgradeability` when proxy semantics must remain outside the verified subset (see issue `#1420`).

### Manual ABI / memory plumbing

Manual ABI or memory plumbing (`mload` / `mstore` / copy-based payload handling) compiles, but it is still outside the fully proved interpreter semantics today. Treat that path as an explicit trust boundary, prefer higher-level helpers when available, and use `--deny-linear-memory-mechanics` if the translated contract must stay inside the proved subset (see issue `#1411`).

Raw `keccak256` hashing also compiles through the typed intrinsic surface, but it still relies on an explicit axiom in the current proof stack. Treat it as a separate trust boundary, archive `--trust-report`, and use `--deny-axiomatized-primitives` when the translated contract must stay inside the proved subset (see issue `#1411`).

### Reentrancy guard primitive

Use `nonreentrant(lockSlot)` on the external entrypoint when the Solidity source
uses `nonReentrant`. The lock must be a scalar `Uint256` storage field.

```verity
function nonreentrant(reentrancyLockSlot) deposit (...) with onlyRelayer : Unit := do
  ...
```

### String-heavy logic

ABI-level `String` support exists today for macro parsing, calldata flow, `returnBytes`, event payloads, custom-error payloads, and direct parameter `==` / `!=` checks (see issue `#1159`).
String storage/layout, dynamic linked externals, dynamic local aliases, and broader word-style operators over `String` remain unsupported, so prefer numeric/address/bytes-based logic unless you only need ABI transport or a direct parameter equality check.

### Internal helpers with dynamic calldata-shaped parameters

Preserve Solidity helper boundaries when Verity accepts the parameter shape.
For example, a Solidity helper such as:

```solidity
function _transferWithBalanceCheck(
  PermitTransferFrom calldata permit,
  address depositor,
  bytes calldata signature,
  uint256 totalAmount,
  bytes32 witness
) internal { ... }
```

translates as a same-contract helper:

```verity
function transferWithBalanceCheck
    (permit : PermitTransferFrom, depositor : Address, signature : Bytes,
     totalAmount : Uint256, witness : Bytes32) : Unit := do
  ...
```

Call it directly from the entrypoint (`transferWithBalanceCheck permit depositor
signature totalAmount witness`). Do not inline it only to work around helper
lowering unless the concrete source type is still unsupported.

### Namespaced and structured storage

Use one `storage_namespace` item per source root. Subsequent storage declarations
belong to that root until another `storage_namespace` item switches the active
namespace.

```verity
storage
  storage_namespace erc7201 "unlink.storage.State"
  state : StorageStruct [
    nextLeafIndex : Uint256 @word 0,
    merkleTree : StorageStruct [
      root : Uint256 @word 0,
      depth : Uint256 @word 1
    ] @word 1,
    verifierRouter : Address @word 10
  ] := slot 0

  storage_namespace erc7201 "unlink.storage.UnlinkPoolRelayers"
  relayersSlot : Address -> Uint256 := slot 0
```

For Solidity `mapping(K => Struct)` and nested mappings to structs, prefer
`MappingStruct(...)` / `MappingStruct2(...)` and named member access through
`structMember`, `structMembers`, `setStructMember`, and their `2` variants.

## 3. Worked Walkthrough: Minimal ERC20 Transfer Path

This is a focused translation of common ERC20 state + transfer logic.

### Solidity source fragment

```solidity
mapping(address => uint256) balances;
uint256 totalSupply;

function transfer(address to, uint256 amount) external returns (bool) {
    require(balances[msg.sender] >= amount, "insufficient");
    balances[msg.sender] -= amount;
    balances[to] += amount;
    emit Transfer(msg.sender, to, amount);
    return true;
}
```

### Step A: Define slots

```verity
def balances : StorageSlot (Address → Uint256) := ⟨0⟩
def totalSupply : StorageSlot Uint256 := ⟨1⟩
```

### Step B: Translate the function body

```verity
def transfer (to : Address) (amount : Uint256) : Contract Unit := do
  let sender    ← msgSender
  let senderBal ← getMapping balances sender
  require (senderBal >= amount) "insufficient"
  let newSender ← requireSomeUint (safeSub senderBal amount) "underflow"
  let toBal     ← getMapping balances to
  let newTo     ← requireSomeUint (safeAdd toBal amount) "overflow"
  setMapping balances sender newSender
  setMapping balances to newTo
  emitEvent "Transfer" [amount] [addressToWord sender, addressToWord to]
```

Use `getMapping` / `setMapping` for individual entries, there is no whole-mapping read or function-shaped write in the EDSL. Keep `require` guards before any `setMapping` mutation so the revert state equals the input state.

### Step C: Write the spec shape

For this transfer path, typical specs include:

1. Sender decreases by `amount` when preconditions hold.
2. Recipient increases by `amount` when preconditions hold.
3. Total supply is unchanged.
4. If guard fails, result is `revert` and state is preserved.

Specs are `Prop`-valued predicates over the pre/post `ContractState`, not records. The canonical shape (used across `Contracts/<Name>/Spec.lean`) is `<op>_spec args s s' : Prop`:

```verity
def transfer_spec (to : Address) (amount : Uint256) (s s' : ContractState) : Prop :=
  s'.storageMap balances.slot s.sender =
    sub (s.storageMap balances.slot s.sender) amount ∧
  s'.storageMap balances.slot to =
    add (s.storageMap balances.slot to) amount ∧
  storageMapUnchangedExceptKeysAtSlot balances.slot s.sender to s s' ∧
  sameStorageAddrContext s s'
```

Pick the right "unchanged" helper from [`Verity.Specs.Common`](/core#spec-helpers) for the actual write set. Conservation specs (`balanceSum` equations) go here too when the contract needs them.

### Step D: Prove with existing automation

Use the `_meets_spec` convention, single `simp` with the operation, slot names, spec definition, and any guard hypothesis:

```verity
theorem transfer_meets_spec (s : ContractState) (to : Address) (amount : Uint256)
    (h_funds : s.storageMap balances.slot s.sender >= amount) :
    let s' := ((transfer to amount).run s).snd
    transfer_spec to amount s s' := by
  simp [transfer, transfer_spec, balances, msgSender, getMapping, setMapping,
        bind, h_funds,
        Specs.storageMapUnchangedExceptKeysAtSlot,
        Specs.sameStorageAddrContext]
```

Real-world references: [`Contracts/SimpleToken/Proofs/Basic.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/SimpleToken/Proofs/Basic.lean) and [`Contracts/ERC20/Proofs/Basic.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/ERC20/Proofs/Basic.lean).

## 4. Common Pitfalls

### 1) Short-circuit assumptions

Do not assume Solidity-style expression short-circuiting unless explicitly encoded in control flow.
Model branching with explicit `if`/`ite` in EDSL statements.

### 2) Storage slot drift

Slot indices are manual and must remain stable across:

1. contract code
2. specs
3. proofs
4. generated tests/scaffolds

Changing slot numbers after writing proofs is a common source of silent mismatches.

### 3) Checked vs wrapping arithmetic

Solidity `^0.8` arithmetic is checked by default.
If you want Solidity-equivalent behavior, use `safeAdd` / `safeSub` / `safeMul` / `safeDiv` with `requireSomeUint`.

### 4) Revert ordering

Keep checks before effects. Put `require` guards before `setStorage`/`setMapping` mutations.

### 5) ABI/selector mismatch

When mapping Solidity functions to `CompilationModel`, verify selector/parameter ordering exactly.
A selector mismatch can make proofs pass while runtime dispatch is wrong.

## 5. Translation Workflow Checklist

1. Port storage layout first, including ERC-7201 namespace roots and struct-valued mappings.
2. Port one function at a time.
3. Add specs immediately for each function.
4. Prove basic safety/correctness properties before adding next function.
5. Run differential/property tests after each milestone.

If you are starting from zero, pair this with:

- [Adding Your First Contract](/first-contract)
- [Production Solidity Patterns](/guides/production-solidity-patterns)
- [Compiler & CLI](/compiler)
- [Verification Status](/verification)