import { Callout } from 'nextra/components'

# Capabilities & Limits

This page is the honest map of what you can write in `verity_contract` today: what is **fully expressible and machine-checked**, what is **partially modeled**, and what **compiles but sits on an explicit trust boundary**. It is the curated companion to the per-constructor [Interpreter Feature Matrix](https://github.com/lfglabs-dev/verity/blob/main/docs/INTERPRETER_FEATURE_MATRIX.md) and [`artifacts/feature_ownership.json`](https://github.com/lfglabs-dev/verity/blob/main/artifacts/feature_ownership.json); when the docs and artifacts disagree, the artifacts win.

For *why* some features are trusted rather than proved, see the [Trust Model](/trust-model) — the Layer 1/2/3 framing lives there. For the live theorem inventory, see [Verification Status](/verification).

<Callout type="info">
Everything below — proved, partial, or trust-boundary — is additionally exercised by 70,000+ differential test vectors against real EVM execution. "Not modeled in proofs" means the proof interpreters do not yet cover it, not that it is untested.
</Callout>

## Fully expressible and verified

Modeled end-to-end in the current supported fragment and carrying machine-checked preservation proofs.

**Storage**
- Scalar fields (`Uint256`, `Address`, `Bool`, `Bytes32`) at explicit slots.
- Mappings: single, double (`mapping2`), `Uint256`-keyed, plus word-offset and packed-word variants.
- Structs and nested storage structs; struct-valued mappings (`MappingStruct` / `MappingStruct2`), including fixed-array members expanded into stable names such as `roots[1]` and `proof[1][1]`.
- ERC-7201 namespaced storage roots (`storage_namespace`).

**Computation**
- Checked arithmetic via `safeAdd` / `safeSub` / `safeMul` / `safeDiv` + `requireSomeUint`; wrapping `add` / `sub` / `mul` / `div` / `mod` / `pow`.
- Bitwise (`and` / `or` / `xor` / `shl` / `shr`), comparison (`eq` / `lt` / `gt` / `le` / `ge`), logical (`logicalAnd` / `logicalOr` / `logicalNot`).
- Fixed-point helpers (`mulDivDown` / `mulDivUp`, `wMulDown` / `wDivUp`, `min` / `max`).

**Control & I/O**
- `if` / `ite` branching; `require` / string-message revert control flow. Custom-error control-flow forms exist, while richer typed ABI error payload mechanics remain a partial proof-boundary surface.
- Returns: single, multi (`returnValues`), array, bytes, and storage words.
- Context reads: `msgSender` (`caller`), `msg.value`, `block.timestamp`.

**Builtins**: all 36 EVM builtins carry proved agreement between the Verity evaluator and the EVMYulLean reference semantics.

## Partially modeled

Compiler-supported and differential-tested, but only partially covered by the proof interpreters.

| Feature | Status | Issue |
|---|---|---|
| Source-level internal helpers | compiler-supported and hidden from selector dispatch / ABI JSON; helper-summary reuse exists in source-semantics lemmas, but the generic body/IR theorem still gates helper-positive callers behind the helper-excluding supported statement fragment | [#1630](https://github.com/lfglabs-dev/verity/issues/1630) |
| Higher-order internal calls | function-pointer parameters are monomorphized at compile time, so downstream compiler/proof layers see first-order helper calls; remaining proof coverage follows the internal-helper boundary above | [#1747](https://github.com/lfglabs-dev/verity/issues/1747) |
| `forEach` loops | zero-bound and empty-body literal-bound loops proved; positive non-empty loop bodies are future work | — |
| Constructors, fallback, and receive | compiler-supported entrypoint surfaces; outside the generic Layer 2 proof fragment | — |
| Events / logs and typed errors | source-level event and custom-error forms compile; ABI log/error payload mechanics and raw logs remain partial or trust-boundary surfaces | — |
| Richer storage layout features | many scalar, mapping, struct, packed-word, and ERC-7201 forms are covered; additional layout compatibility and richer dynamic layouts are compiler-supported or trust-reported rather than generically proof-modeled | — |
| Single-word linear memory (`mload` / `mstore`) | single-word support in the IR interpreter; full coverage needs EVMYulLean integration | [#1411](https://github.com/lfglabs-dev/verity/issues/1411) |
| Runtime introspection (`block.number`, `address(this)`, `tx.origin`, `chainid`, `blobbasefee`) | compiler-supported and source-executable; outside the generic proof fragment | — |
| `selfbalance()` / `address(this).balance` | source-executable with differential coverage; not yet in the proof fragment | — |
| Low-level `try/catch` | lowers to a raw call + success-word `ite`; first-class catch over higher-level helpers and payload decoding are unsupported | [#1161](https://github.com/lfglabs-dev/verity/issues/1161) |

## Compiles, but on a trust boundary

These lower to intended Yul and are differential-tested, but their runtime semantics are **not fully modeled by the proof interpreters**. Treat each use as an explicit trust-boundary assumption and archive `--trust-report`.

- **`keccak256`** — compiles through the typed intrinsic and uses the in-tree Keccak implementation on the executable source path, but the proof stack still treats dynamic memory hashing as an explicit primitive assumption (`keccak256_memory_slice_matches_evm`) rather than a fully modeled operation. Enforce exclusion with `--deny-axiomatized-primitives`.
- **ECMs, typed interface calls, external calls, and low-level mechanics** — `call` / `staticcall` / `delegatecall`, returndata plumbing, `externalCallBind`, typed Solidity interface dot-calls, linked Yul libraries such as Poseidon, CREATE2, SSTORE2-style `extcodecopy`, and ECMs (`callWithValue`, `bubblingValueCall`, no-output adapters/routers, SafeTransferLib-style optional-return helpers, callback helpers, CREATE2/SSTORE2 helpers, and the precompile ECMs `ecrecover` / `sha256` / BN254). Enforce with `--deny-low-level-mechanics` or `--deny-assumed-dependencies` depending on the surface; each precompile carries its own `evm_*_precompile` trust-report assumption, while CREATE2/SSTORE2 carry layout/address assumptions (see [`docs/EXTERNAL_CALL_MODULES.md`](https://github.com/lfglabs-dev/verity/blob/main/docs/EXTERNAL_CALL_MODULES.md) and [`AXIOMS.md`](https://github.com/lfglabs-dev/verity/blob/main/AXIOMS.md)).
- **`delegatecall` / proxy upgradeability** — additionally a dedicated proxy boundary. Enforce with `--deny-proxy-upgradeability` ([#1420](https://github.com/lfglabs-dev/verity/issues/1420)).
- **Raw payload plumbing, local obligations, and proxy-specific refinements** — `calldatacopy`, `returndataCopy`, `revertReturndata`, `rawLog`, `local_obligations`, `unsafe "reason" do` blocks, and delegatecall/proxy refinements. Enforce raw-event exclusion with `--deny-event-emission`, local-obligation exclusion with `--deny-local-obligations`, unsafe-block exclusion with `--deny-unsafe`, and low-level mechanics with `--deny-low-level-mechanics`.
- **Nested dynamic ABI decoding** — `arrayElementDynamicWord` / `paramDynamicHeadWord` read checked static leaf words from dynamic-shaped calldata; the decoded words are not modeled in proofs ([#1832](https://github.com/lfglabs-dev/verity/issues/1832)).

## Not supported in `verity_contract` today

- **String storage and layout** — ABI-level `String` works for calldata flow, `returnBytes`, event/custom-error payloads, and direct parameter `==` / `!=`. String *storage*, dynamic linked externals, dynamic local aliases, and word-style operators over `String` are unsupported; prefer numeric / address / bytes logic ([#1159](https://github.com/lfglabs-dev/verity/issues/1159)).
- **Solidity-style first-class `try/catch`** over high-level external calls (see the partial note above, [#1161](https://github.com/lfglabs-dev/verity/issues/1161)).
- **Whole-mapping reads or function-shaped writes** — operate per key with `getMapping` / `setMapping`.
- **Inheritance and modifiers as language constructs** — model them by explicit composition and guard helpers (see [Solidity → Verity](/guides/solidity-to-verity#2-patterns-that-need-restructuring)).
- **Dynamic dispatch on function pointers** — a function-pointer argument that is a runtime value, an expression, or a non-helper name has no statically-known target to monomorphize and fails fast with an issue-linked diagnostic ([#1747](https://github.com/lfglabs-dev/verity/issues/1747)). Pass an explicit mode/enum and dispatch to direct helper calls instead.

## Staying inside the proved subset

The compiler can fail the build when a contract leaves the verified envelope. Pass the relevant `--deny-*` flag(s) and archive `--trust-report <path>` for the JSON trust surface:

| Flag | Rejects |
|---|---|
| `--deny-axiomatized-primitives` | `keccak256` and other axiomatized primitives |
| `--deny-local-obligations` | explicit `local_obligations [...]` refinements |
| `--deny-linear-memory-mechanics` | partially modeled `mload` / `mstore` / copy mechanics |
| `--deny-runtime-introspection` | `block.number`, `address(this)`, `chainid`, … |
| `--deny-low-level-mechanics` | `call` / `staticcall` / `delegatecall`, ECMs, returndata plumbing |
| `--deny-proxy-upgradeability` | `delegatecall`-style proxy / upgradeability |
| `--deny-event-emission` | raw `rawLog` event emission |
| `--deny-unchecked-dependencies` | dependencies marked `unchecked` |
| `--deny-assumed-dependencies` | any `assumed` or `unchecked` foreign surface |
| `--deny-layout-incompatibility` | candidate storage layout breaks a baseline layout report |
| `--deny-unsafe` | catch-all for unsafe blocks and all deny-gated trust surfaces |

See [Compiler & CLI](/compiler) for the full flag list and the [Trust Model](/trust-model) for how these map to Layer 1/2/3.