# Core Architecture

The core is intentionally small. It provides types for contract state, storage operations, a `require` guard, and `@[simp]` lemmas for proof automation.

## Types

```verity
abbrev Address := String
abbrev Uint256 := Verity.Core.Uint256

structure StorageSlot (α : Type) where
  slot : Nat
```

`StorageSlot` is parameterized by type, so `StorageSlot Uint256`, `StorageSlot Address`, and `StorageSlot (Address -> Uint256)` are all distinct. This prevents mixing storage types at compile time.

`Uint256` is a dedicated 256-bit modular integer type, so `+`, `-`, `*`, `/`, and `%` wrap exactly like the EVM.

> **Note**: This matches EVM wrapping semantics, not Solidity's default checked arithmetic (^0.8). Use `require` guards to match Solidity behavior. See [TRUST_ASSUMPTIONS.md](https://github.com/lfglabs-dev/verity/blob/main/TRUST_ASSUMPTIONS.md#8-arithmetic-semantics-wrapping-vs-checked) for details.

## ContractState

```verity
structure ContractState where
  -- Persistent storage spaces, indexed by slot
  storage         : Nat → Uint256                          -- uint256 slots
  storageAddr     : Nat → Address                          -- address slots
  storageMap      : Nat → Address → Uint256                -- address-keyed mapping
  storageMapUint  : Nat → Uint256 → Uint256                -- uint-keyed mapping
  storageMap2     : Nat → Address → Address → Uint256      -- double mapping
  storageArray    : Nat → List Uint256                     -- dynamic in-storage arrays
  -- EIP-1153 transient storage
  transientStorage : Nat → Uint256
  -- EVM context
  sender, thisAddress : Address
  msgValue, selfBalance : Uint256
  blockTimestamp, blockNumber, chainId, blobBaseFee : Uint256
  -- Calldata and memory
  calldataSize : Uint256
  calldata : List Nat
  memory   : Nat → Uint256
  -- Bookkeeping
  knownAddresses : Nat → FiniteAddressSet                  -- tracked per slot, for conservation
  events         : List Event                              -- append-only log
```

Six persistent storage spaces plus transient storage. `storage` for Uint256 values, `storageAddr` for addresses, `storageMap` / `storageMapUint` / `storageMap2` for the three mapping shapes, `storageArray` for dynamic arrays. Each is indexed by a natural number (the slot).

`knownAddresses` tracks which addresses have been seen per slot and is used by conservation proofs. EVM context fields (`msgValue`, `blockTimestamp`, `blockNumber`, `chainId`, `blobBaseFee`, `selfBalance`) and calldata/memory are modeled so EDSL proofs can reason about them; the `verity_contract` macro routes context accessors and `tstore`/`tload` through these fields.

## ContractResult

```verity
inductive ContractResult (α : Type) where
  | success : α → ContractState → ContractResult α
  | revert : String → ContractState → ContractResult α
```

Every contract operation returns either `success` with a value and updated state, or `revert` with an error message and the state at the point of failure.

> **Important**: On revert, the returned state may include mutations from operations that executed *before* the revert. This differs from EVM semantics where REVERT discards all state changes. Contracts must follow the **checks-before-effects pattern**, all `require` guards before any `setStorage`/`setMapping` calls, to ensure the revert state equals the original input state. See [TRUST_ASSUMPTIONS.md](https://github.com/lfglabs-dev/verity/blob/main/TRUST_ASSUMPTIONS.md) and [#254](https://github.com/lfglabs-dev/verity/issues/254) for details.

## Contract monad

```verity
abbrev Contract (α : Type) := ContractState → ContractResult α
```

A contract is a function from state to result. The custom `bind` short-circuits on revert:

```verity
def bind (ma : Contract α) (f : α → Contract β) : Contract β :=
  fun s => match ma s with
  | ContractResult.success a s' => f a s'
  | ContractResult.revert msg s' => ContractResult.revert msg s'
```

This gives do-notation with automatic failure propagation. A failed `require` stops the whole chain.

## Primitives

The core types above are operated on by a small surface of EDSL primitives, storage get/set, mapping get/set, context accessors (`msgSender`, `msgValue`, `blockTimestamp`, `contractAddress`), event emission, and the `require` guard. Those are documented in the [EDSL API Reference](/edsl-api-reference); the prose here only covers the *type layer* and the monad, not the operation catalogue.

The shape of every primitive is the same: it's a `Contract α` value, which is `ContractState → ContractResult α`. Read-only primitives like `msgSender` and `getStorage` always emit `ContractResult.success`; write primitives like `setStorage` return `success ()` with a modified `ContractState`. `require` is the one operation that may emit `ContractResult.revert`, preserving the original state.

> `setMapping` (and its keyed variants) also inserts the key into `knownAddresses` for that slot, enabling conservation proofs that sum over all balances.

## Simp lemmas

Every storage operation, context accessor, and event function has a full-result `@[simp]` lemma:

```verity
-- Full-result form (preferred for new proofs):
@[simp] theorem getStorage_run (s : StorageSlot Uint256) (state : ContractState) :
  (getStorage s).run state = ContractResult.success (state.storage s.slot) state := rfl

@[simp] theorem require_true (msg : String) (s : ContractState) :
  (require true msg).run s = ContractResult.success () s := rfl

@[simp] theorem require_false (msg : String) (s : ContractState) :
  (require false msg).run s = ContractResult.revert msg s := rfl
```

Older `_fst`/`_snd` projection lemmas also exist, but the full-result forms above are preferred, they prove success, value, and state in one shot. Most simple properties can be proven by `simp only [...]` with the right set of definitions.

## Why ContractResult instead of StateM

A plain `StateM ContractState α` monad cannot model `require` failures, proofs would have to assume guards pass (introducing axioms). `ContractResult` makes success/failure explicit, so proofs reason about both paths with no axioms. The cost is a small amount of extra infrastructure (the `ContractResult` type, custom `bind`, and simp lemmas).

## Type safety

The `StorageSlot α` type parameter prevents mixing storage types:

```verity
def owner : StorageSlot Address := ⟨0⟩
def count : StorageSlot Uint256 := ⟨1⟩
def balances : StorageSlot (Address → Uint256) := ⟨2⟩
def prices : StorageSlot (Uint256 → Uint256) := ⟨3⟩
def allowances : StorageSlot (Address → Address → Uint256) := ⟨4⟩

-- These compile:
let value ← getStorage count              -- Uint256
let addr ← getStorageAddr owner           -- Address
let bal ← getMapping balances "0xAlice"   -- Uint256
let price ← getMappingUint prices tokenId -- Uint256
let allow ← getMapping2 allowances owner spender -- Uint256

-- This doesn't:
let wrong ← getStorage owner  -- Type error: owner is Address, not Uint256
```

## Spec helpers

Specs express what a function **did not change**. `Verity/Specs/Common.lean` provides named predicates so specs don't repeat field-by-field equality. Import with `import Verity.Specs.Common` and `open Verity.Specs`.

Three layers, narrowest first:

- **Atomic**, one field at a time: `sameStorage`, `sameStorageAddr`, `sameStorageMap`, `sameStorageMapUint`, `sameStorageMap2`, `sameContext`.
- **Mixed** (most common in practice), two storage checks + `sameContext`:
  - `sameAddrMapContext`, use when only `setStorage` (uint256 slot) writes.
  - `sameStorageMapContext`, use when only `setStorageAddr` writes.
  - `sameStorageAddrContext`, use when only `setMapping` writes.
- **Composite** (strictest), everything except one storage type: `sameExceptStorage`, `sameExceptStorageAddr`, `sameExceptStorageMap`, `sameExceptStorageMapUint`, `sameExceptStorageMap2`. `sameAllStorage` covers context-only writes. All composites include `sameContext`.
- **Fine-grained**, for single-entry mapping updates: `storageUnchangedExcept slot`, `storageAddrUnchangedExcept slot`, `storageMapUnchangedExceptKeyAtSlot slot addr`, `storageMapUnchangedExceptKeysAtSlot slot a1 a2` (transfers), `storageMapUintUnchangedExceptSlot`, `storageMapUintUnchangedExceptKey`, `storageMap2UnchangedExceptSlot`.

A counter's `increment` writes only the uint256 count slot, so the unchanged-state predicate is `sameAddrMapContext`. An ERC20 `transfer` (two mapping keys) uses `storageMapUnchangedExceptKeysAtSlot balances.slot from to`.

## Source

[`Verity/Core.lean`](https://github.com/lfglabs-dev/verity/blob/main/Verity/Core.lean) · [`Verity/Specs/Common.lean`](https://github.com/lfglabs-dev/verity/blob/main/Verity/Specs/Common.lean)