# Architecture Overview

Verity is a Lean-4 embedded DSL for writing smart contracts that compile to EVM
bytecode and come with machine-checked correctness proofs. Each layer of the
system has a specific responsibility: the **EDSL** is where humans write
contracts and theorems; the **CompilationModel** is the declarative typed
specification the compiler consumes; the **IR** is the intermediate form the
proofs target; **Yul** is the textual EVM dialect emitted to disk; and the
deployable **EVM** bytecode is produced by `solc` from Yul. Every transition is
either proved in Lean or recorded as an explicit assumption in the trust report.

## Pipeline

```
EDSL  -->  CompilationModel  -->  IR  -->  Yul  -->  EVM
```

**EDSL.** The source layer. Contracts are written using `verity_contract` (or
the lower-level `Contract` monad) against `Verity/Core.lean`. Specs, invariants,
and proofs live next to the implementation in `Contracts/<Name>/`. Read by the
human author; consumed by the elaborator to build a `CompilationModel`. Layer 1
proves the EDSL implementation refines its `CompilationModel`.

**CompilationModel.** The declarative typed-IR layer (`Compiler/CompilationModel.lean`).
A `CompilationModel` carries fields, events, errors, the constructor, function
bodies as `Expr`/`Stmt`, externals, and local obligations. Written by the
compiler (or by hand for legacy specs); read by the IR generator. Layer 2
proves that the IR generated from any `CompilationModel` in the supported
fragment preserves its semantics.

**IR.** The typed intermediate representation that sits between
`CompilationModel` and Yul (`Compiler/Proofs/IRGeneration/`). Generated
automatically; read by the Yul code generator and by the Layer 2 / Layer 3
proofs. The end-to-end correctness theorem is stated at this level.

**Yul.** The textual EVM dialect emitted by `Compiler/Codegen.lean` and the Yul
pretty-printer in `Compiler/Yul/*.lean`. Written to `artifacts/yul/*.yul`; read
by `solc --strict-assembly`. Layer 3 proves IR-to-Yul preservation.

**EVM.** The final deployable bytecode. Produced by `solc` from Yul; deployed by
`forge create` or any standard toolchain. Not in the proof envelope: `solc`,
the EVM spec, and the deployment pipeline are explicit trust assumptions.

## Layer responsibilities

When a Solidity-facing feature is added, the first question is which layer should
own it. Verity works best when features enter as typed source or
`CompilationModel` constructs and the later layers only lower those constructs.

| Feature kind | Owner | Examples |
|---|---|---|
| Source syntax | `verity_contract` macro | Source-level `internal` helpers, storage declarations, function parameters |
| Storage layout | Macro lowering plus `CompilationModel` fields | `MappingStruct`, `MappingStruct2`, fixed-array struct members like `roots[1]` |
| Reusable call mechanics | External Call Modules | ERC-20 wrappers, callbacks, CREATE2, SSTORE2, precompiles |
| Low-level primitives | `CompilationModel` mechanics and trust reports | `call`, `staticcall`, `create2`, `extcodecopy`, `codecopy` |
| Proof widening | Supported-fragment witnesses and theorem interfaces | Moving a feature from tested/trusted into the proved subset |

That split matters because many production ports need Solidity mechanisms that
are useful but not yet fully modeled in the proof interpreters. Verity should
still compile them directly, but it must also surface the remaining assumption in
`--trust-report` and let proof-strict users reject it with a `--deny-*` flag.

## Source-to-model boundary

The `verity_contract` macro emits both executable Lean code and a
`CompilationModel`. The model is the compiler-facing artifact; selector dispatch,
ABI output, storage layout, trust reporting, and later proofs all consume it.

Source-level `internal` functions become internal `FunctionSpec`s. They are
callable by other functions, but they are excluded from external selector
dispatch and ABI JSON. Entry points with special EVM meaning, such as `receive`
and `fallback`, should stay external because their names control dispatcher
behavior.

Storage declarations lower to typed fields. For Morpho-style mapping structs,
fixed-array members are expanded into stable word-addressed member names. A
declaration such as `roots : FixedArray Bytes32 2 @word 1` exposes
`roots[0]` and `roots[1]`; nested arrays expose names like `proof[1][1]`.
Those names are what `structMember` and `setStructMember` use, so generated Yul
remains layout-reviewable without post-processing.

## Source layer (EDSL)

The EDSL is intentionally small. `Verity/Core.lean` provides `ContractState`,
`ContractResult` (the success/revert algebra), the `Contract` monad with
short-circuiting `bind`, six persistent storage spaces (uint256, address,
address-keyed mapping, uint256-keyed mapping, double mapping, dynamic arrays)
plus EIP-1153 transient storage, `require`, and a curated set of `@[simp]`
lemmas for proof automation. The `verity_contract` macro lowers
human-friendly syntax to both an executable Lean definition and a
`CompilationModel`, keeping the two in sync. See [`/edsl-api-reference`](/edsl-api-reference)
for the full surface and [`/first-contract`](/first-contract) for a guided walkthrough.

## Pipeline (CompilationModel → Yul)

The compiler runs a fixed sequence per contract: storage-slot inference,
selector lookup, IR generation, Yul AST construction, and pretty-printing. The
same binary emits machine-readable audit artifacts: `--trust-report`,
`--assumption-report`, `--layout-report`, and `--layout-compat-report`. The
linker (`Compiler/Linker.lean`) splices external Yul libraries (`--link`) into
the runtime section after validating that every non-builtin call site is
satisfied. See [`/compiler`](/compiler) for the pipeline narrative and CLI reference.

## Extension surfaces

External Call Modules, or ECMs, are the standard extension point for reusable
low-level or protocol-shaped calls. An ECM packages argument count, result
bindings, mutability flags, Yul lowering, and named assumptions. Standard ECMs
ship for ERC-20 optional-return wrappers, ERC-4626 reads, callbacks, generic
value calls, precompiles, CREATE2 deployment, and SSTORE2-style code-as-data
reads.

The CREATE2/SSTORE2 helpers are a representative boundary:

- `create2Deploy` lowers `create2(value, offset, size, salt)` and records
  `create2_initcode_layout` plus `create2_address_derivation`.
- `sstore2ReadCode` lowers `extcodecopy(pointer, dest, codeOffset, size)` and
  records `sstore2_pointer_code_layout`.

The compiler owns the mechanics. The contract or protocol proof owns the meaning
of the initcode, derived address, pointer bytecode layout, and returned data.

## Verification layers (1 / 2 / 3)

The pipeline annotations above mark where each layer applies — Layer 1 (EDSL →
`CompilationModel`), Layer 2 (`CompilationModel` → IR), Layer 3 (IR → Yul). The
canonical breakdown of what is proved versus trusted at each layer lives on the
[Trust Model](/trust-model), and the live theorem inventory is on
[Verification Status](/verification).

## Contributor checklist

For a new production feature, check every row before relying on it:

| Area | Question |
|---|---|
| Source surface | Is there source syntax or a documented API, with validation errors for unsupported forms? |
| Model surface | Does it lower to typed `CompilationModel` data rather than patched generated Yul? |
| ABI and dispatch | Are external selectors, ABI output, internal helpers, `receive`, and `fallback` handled explicitly? |
| Storage layout | Are resolved names, offsets, packing, and aliases visible in the model and layout report? |
| Trust reporting | Do all unproved mechanics appear in `--trust-report`, with fail-closed deny flags when appropriate? |
| Tests | Is there source smoke coverage, lowering coverage, trust-report coverage, and generated property-test coverage where relevant? |
| Docs | Do the architecture, capabilities, and feature-specific docs describe both behavior and remaining trust boundary? |

## Where to next

- [Getting Started](/getting-started), local setup and your first verification run.
- [First Contract](/first-contract), guided spec-to-proof walkthrough.
- [Compiler & CLI](/compiler), the pipeline in detail, plus CLI flags.
- [Trust Model](/trust-model), what you trust when you trust a Verity contract.
- [EDSL API Reference](/edsl-api-reference), canonical primitive reference.