# 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

```lean
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/Th0rgal/verity/blob/main/TRUST_ASSUMPTIONS.md#8-arithmetic-semantics-wrapping-vs-checked) for details.

## ContractState

```lean
structure ContractState where
  storage : Nat → Uint256                         -- Uint256 storage
  storageAddr : Nat → Address                      -- Address storage
  storageMap : Nat → Address → Uint256            -- Mapping storage (address-keyed)
  storageMapUint : Nat → Uint256 → Uint256        -- Mapping storage (uint256-keyed)
  storageMap2 : Nat → Address → Address → Uint256 -- Double mapping storage
  sender : Address
  thisAddress : Address
  msgValue : Uint256
  blockTimestamp : Uint256
  knownAddresses : Nat → FiniteAddressSet          -- Tracked addresses per slot
  events : List Event := []                        -- Emitted events (append-only)
```

Five independent storage spaces: `storage` for Uint256 values, `storageAddr` for addresses, `storageMap` for address-keyed mappings (e.g., `balances[owner]`), `storageMapUint` for uint256-keyed mappings, and `storageMap2` for double mappings (e.g., `allowances[owner][spender]`). Each is indexed by a natural number (the slot).

The state also carries: the `sender` address, the contract's own `thisAddress`, EVM context fields (`msgValue`, `blockTimestamp`), `knownAddresses` for tracking which addresses have been seen per slot (used in conservation proofs), and an append-only `events` log.

## ContractResult

```lean
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/Th0rgal/verity/blob/main/TRUST_ASSUMPTIONS.md) and [#254](https://github.com/Th0rgal/verity/issues/254) for details.

## Contract monad

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

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

```lean
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.

## Storage operations

Five pairs of get/set functions, one per storage type:

| Storage type | Get | Set | Slot type |
|---|---|---|---|
| Uint256 | `getStorage` | `setStorage` | `StorageSlot Uint256` |
| Address | `getStorageAddr` | `setStorageAddr` | `StorageSlot Address` |
| Mapping (address-keyed) | `getMapping` | `setMapping` | `StorageSlot (Address → Uint256)` |
| Mapping (uint256-keyed) | `getMappingUint` | `setMappingUint` | `StorageSlot (Uint256 → Uint256)` |
| Double mapping | `getMapping2` | `setMapping2` | `StorageSlot (Address → Address → Uint256)` |

All follow the same pattern — read from or write to the corresponding `ContractState` field:

```lean
def getStorage (s : StorageSlot Uint256) : Contract Uint256 :=
  fun state => ContractResult.success (state.storage s.slot) state

def setStorage (s : StorageSlot Uint256) (value : Uint256) : Contract Unit :=
  fun state => ContractResult.success ()
    { state with storage := fun slot =>
        if slot == s.slot then value else state.storage slot }
```

Mapping operations take key arguments:

```lean
-- Address-keyed mapping (e.g., balances[owner])
let bal ← getMapping balances owner
setMapping balances owner newBal

-- Uint256-keyed mapping
let val ← getMappingUint prices tokenId
setMappingUint prices tokenId newPrice

-- Double mapping (e.g., allowances[owner][spender])
let allow ← getMapping2 allowances owner spender
setMapping2 allowances owner spender newAllow
```

> `setMapping` also inserts the key into `knownAddresses` for that slot, enabling conservation proofs that sum over all balances.

## Context accessors

Read-only functions for accessing transaction context:

```lean
let sender ← msgSender           -- Transaction sender address
let self ← contractAddress        -- This contract's address
let value ← msgValue             -- ETH value sent with call
let time ← blockTimestamp         -- Current block timestamp
```

These return values from `ContractState` without modifying state.

## Event emission

```lean
emitEvent "Transfer" [amount] [senderBal, recipientBal]
```

`emitEvent name args indexedArgs` appends to the `events` log. The `indexedArgs` parameter is optional (defaults to `[]`).

## Require guard

```lean
def require (condition : Bool) (message : String) : Contract Unit :=
  fun s => if condition
           then ContractResult.success () s
           else ContractResult.revert message s
```

Returns `success` when the condition holds, `revert` with the message when it doesn't.

## Simp lemmas

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

```lean
-- 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:

```lean
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 (`Verity/Specs/Common.lean`)

Specs express what a function **did not change**. `Common.lean` provides named predicates so specs don't repeat field-by-field equality.

Import with `import Verity.Specs.Common` and `open Verity.Specs`.

### Atomic helpers (single field)

| Helper | Asserts |
|--------|---------|
| `sameStorage s s'` | `s'.storage = s.storage` |
| `sameStorageAddr s s'` | `s'.storageAddr = s.storageAddr` |
| `sameStorageMap s s'` | `s'.storageMap = s.storageMap` |
| `sameStorageMapUint s s'` | `s'.storageMapUint = s.storageMapUint` |
| `sameStorageMap2 s s'` | `s'.storageMap2 = s.storageMap2` |
| `sameContext s s'` | sender, thisAddress, msgValue, blockTimestamp unchanged |

### Composite helpers

Use these instead of conjunctions of atomics:

| Helper | Meaning | Use when operation only writes... |
|--------|---------|-----------------------------------|
| `sameAllStorage s s'` | All 5 storage types unchanged | Context fields only |
| `sameExceptStorage s s'` | Everything except `storage` unchanged | `setStorage` |
| `sameExceptStorageAddr s s'` | Everything except `storageAddr` unchanged | `setStorageAddr` |
| `sameExceptStorageMap s s'` | Everything except `storageMap` unchanged | `setMapping` |
| `sameExceptStorageMapUint s s'` | Everything except `storageMapUint` unchanged | `setMappingUint` |
| `sameExceptStorageMap2 s s'` | Everything except `storageMap2` unchanged | `setMapping2` |

All composites include `sameContext`.

### Mixed storage+context helpers

These combine two atomic storage checks with `sameContext`. They are the most commonly used helpers in practice — appearing in nearly every spec:

| Helper | Meaning | Use when operation only writes... |
|--------|---------|-----------------------------------|
| `sameAddrMapContext s s'` | `sameStorageAddr ∧ sameStorageMap ∧ sameContext` | `setStorage` (uint256 slot only) |
| `sameStorageMapContext s s'` | `sameStorage ∧ sameStorageMap ∧ sameContext` | `setStorageAddr` (address slot only) |
| `sameStorageAddrContext s s'` | `sameStorage ∧ sameStorageAddr ∧ sameContext` | `setMapping` (mapping only) |

**Example**: A counter's `increment` spec modifies a uint256 storage slot, so the unchanged-state predicate is `sameAddrMapContext` (address storage, mapping storage, and context are all unchanged).

### Fine-grained helpers (specific slot or key)

For operations that modify a single entry in a mapping:

| Helper | Asserts |
|--------|---------|
| `storageUnchangedExcept slot s s'` | All uint256 slots except `slot` unchanged |
| `storageAddrUnchangedExcept slot s s'` | All address slots except `slot` unchanged |
| `storageMapUnchangedExceptKeyAtSlot slot addr s s'` | Mapping unchanged except `slot`/`addr` |
| `storageMapUnchangedExceptKeysAtSlot slot a1 a2 s s'` | Mapping unchanged except `slot`/`a1`/`a2` (transfers) |
| `storageMapUintUnchangedExceptSlot slot s s'` | Uint256-keyed mapping unchanged except `slot` |
| `storageMapUintUnchangedExceptKey slot key s s'` | Uint256-keyed mapping at `slot` unchanged except `key` |
| `storageMap2UnchangedExceptSlot slot s s'` | Double mapping unchanged except `slot` |

### Choosing the right helper

| Operation | Mixed (most common) | Composite (strictest) | Fine-grained |
|-----------|---------------------|----------------------|--------------|
| `setStorage count v` | `sameAddrMapContext` | `sameExceptStorage` | `storageUnchangedExcept count.slot` |
| `setStorageAddr owner v` | `sameStorageMapContext` | `sameExceptStorageAddr` | `storageAddrUnchangedExcept owner.slot` |
| `setMapping balances addr v` | `sameStorageAddrContext` | `sameExceptStorageMap` | `storageMapUnchangedExceptKeyAtSlot balances.slot addr` |
| ERC20 transfer (two keys) | `sameStorageAddrContext` | `sameExceptStorageMap` | `storageMapUnchangedExceptKeysAtSlot balances.slot from to` |
| `setMappingUint prices id v` | — | `sameExceptStorageMapUint` | `storageMapUintUnchangedExceptKey prices.slot id` |
| Read-only (`getStorage`, etc.) | — | `sameAllStorage ∧ sameContext` | — |

## Source

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