# Examples Gallery

A small set of contracts, each introducing a new pattern. They build on each other: SimpleStorage uses one slot, Counter adds arithmetic, Owned adds access control, SimpleToken combines all three.

Each contract is verified end-to-end against the generic whole-contract Layer 2 theorem in `Compiler/Proofs/IRGeneration/Contract.lean` for the current supported fragment, there are no per-contract bridge axioms.

For the *file layout* and authoring steps these examples follow, see [Add a Contract](/guides/add-contract). For a guided walkthrough that builds one from scratch, see [Your First Contract](/first-contract).

## SimpleStorage

Single storage slot with get/set.

```verity
verity_contract SimpleStorage where
  storage
    storedData : Uint256 := slot 0

  function store (value : Uint256) : Unit := do
    setStorage storedData value

  function retrieve () : Uint256 := do
    return (← getStorage storedData)
```

Proofs cover store/retrieve roundtrip and state isolation.

## Counter

Read-modify-write with increment and decrement.

```verity
verity_contract Counter where
  storage
    count : Uint256 := slot 0

  function increment () : Unit := do
    let current ← getStorage count
    setStorage count (add current 1)

  function decrement () : Unit := do
    let current ← getStorage count
    setStorage count (sub current 1)
```

Proofs cover arithmetic, composition (two increments add 2), and decrement-at-zero wraparound behavior.

## SafeCounter

Same as Counter but uses checked arithmetic from `Stdlib.Math`.

```verity
verity_contract SafeCounter where
  storage
    count : Uint256 := slot 0

  function increment () : Unit := do
    let current ← getStorage count
    let newCount ← requireSomeUint (safeAdd current 1) "Overflow"
    setStorage count newCount
```

Proofs cover overflow/underflow revert and bounds preservation.

## Owned

Access control with an owner address and a `require` guard. `onlyOwner` is a same-contract helper that any function can call directly.

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

  constructor (initialOwner : Address) := do
    setStorageAddr owner initialOwner

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

  function transferOwnership (newOwner : Address) : Unit := do
    onlyOwner
    setStorageAddr owner newOwner
```

Proofs cover access-control enforcement and the full lifecycle (create, transfer, locked-out old owner).

## OwnedCounter

Composes Owned and Counter. Increment/decrement require ownership.

```verity
verity_contract OwnedCounter where
  storage
    owner : Address := slot 0
    count : Uint256 := slot 1

  function increment () : Unit := do
    onlyOwner
    let current ← getStorage count
    setStorage count (add current 1)
```

Proofs cover cross-pattern composition, ownership transfer locking out old owner, and counter value surviving ownership transfer.

## Ledger

Mapping storage for per-address balances with deposit, withdraw, and transfer.

```verity
verity_contract Ledger where
  storage
    balances : Address → Uint256 := slot 0

  function deposit (amount : Uint256) : Unit := do
    let sender         ← msgSender
    let currentBalance ← getMapping balances sender
    setMapping balances sender (add currentBalance amount)   -- EVM modular arithmetic

  function transfer (to : Address) (amount : Uint256) : Unit := do
    let sender        ← msgSender
    let senderBalance ← getMapping balances sender
    require (senderBalance >= amount) "Insufficient balance"
    if sender == to then
      pure ()
    else
      let recipientBalance    ← getMapping balances to
      let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow"
      setMapping balances sender (sub senderBalance amount)
      setMapping balances to newRecipientBalance
```

Proofs cover balance guards, deposit/withdraw/transfer sum equations, and deposit-withdraw cancellation.

## SimpleToken

Composes Owned and Ledger. Adds owner-controlled minting and supply tracking.

```verity
verity_contract SimpleToken where
  storage
    owner       : Address := slot 0
    balances    : Address → Uint256 := slot 1
    totalSupply : Uint256 := slot 2

  constructor (initialOwner : Address) := do
    setStorageAddr owner initialOwner
    setStorage totalSupply 0

  function mint (to : Address) (amount : Uint256) : Unit := do
    onlyOwner
    let currentBalance ← getMapping balances to
    let newBalance     ← requireSomeUint (safeAdd currentBalance amount) "Balance overflow"
    let currentSupply  ← getStorage totalSupply
    let newSupply      ← requireSomeUint (safeAdd currentSupply amount) "Supply overflow"
    setMapping balances to newBalance
    setStorage totalSupply newSupply

  function transfer (to : Address) (amount : Uint256) : Unit := do
    let sender        ← msgSender
    let senderBalance ← getMapping balances sender
    require (senderBalance >= amount) "Insufficient balance"
    if sender == to then
      pure ()
    else
      let recipientBalance    ← getMapping balances to
      let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow"
      setMapping balances sender (sub senderBalance amount)
      setMapping balances to newRecipientBalance
```

Proofs cover mint/transfer correctness, supply conservation equations, and storage isolation across all three slot types.

## Vault (minimal ERC-4626)

A conservative ERC-4626-style vault with 1:1 asset/share accounting. Deposits mint shares equal to assets; withdrawals burn 1:1. The shape exercises the canonical vault surface without complicating the share-price math.

```verity
verity_contract Vault where
  storage
    totalAssetsSlot   : Uint256 := slot 0
    totalSupplySlot   : Uint256 := slot 1
    shareBalancesSlot : Address → Uint256 := slot 2

  constructor () := do
    setStorage totalAssetsSlot 0
    setStorage totalSupplySlot 0

  function deposit (assets : Uint256) : Unit := do
    let sender ← msgSender
    let currentShares ← getMapping shareBalancesSlot sender
    let newShares ← requireSomeUint (safeAdd currentShares assets) "Share balance overflow"
    let currentAssets ← getStorage totalAssetsSlot
    let newAssets ← requireSomeUint (safeAdd currentAssets assets) "Total assets overflow"
    let currentSupply ← getStorage totalSupplySlot
    let newSupply ← requireSomeUint (safeAdd currentSupply assets) "Total supply overflow"
    setMapping shareBalancesSlot sender newShares
    setStorage totalAssetsSlot newAssets
    setStorage totalSupplySlot newSupply
```

The spec layer (`deposit_spec`, `withdraw_spec`, isolation predicates) lives in `Contracts/Vault/Spec.lean`. Native IR-lowering proofs are checked in [`Contracts/Vault/Proofs/Native.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/Vault/Proofs/Native.lean); deeper Basic/Correctness/Conservation coverage is tracked under issue [#1163](https://github.com/lfglabs-dev/verity/issues/1163).

## ReentrancyExample

Two parallel bank contracts, one vulnerable, one safe, demonstrating that reentrancy is a *provable* property, not just a testing concern.

```verity
-- Vulnerable: external call before state update
-- Modeled by subtracting totalSupply twice, balance once
theorem vulnerable_attack_exists :
  ∃ (s : ContractState),
    s.storageMap balances.slot "attacker" = (Verity.EVM.MAX_UINT256 : Uint256) ∧
    s.storage totalSupply.slot = (Verity.EVM.MAX_UINT256 : Uint256) ∧
    supplyInvariant s ["attacker"] ∧
    let s' := (withdraw (Verity.EVM.MAX_UINT256 : Uint256)).runState s;
    ¬ supplyInvariant s' ["attacker"]

-- Safe: state update before external call
-- The supply invariant is universally provable
theorem withdraw_maintains_supply (amount : Uint256) :
  ∀ (s : ContractState),
    supplyInvariant s [s.sender] →
    s.storageMap balances.slot s.sender ≥ amount →
    supplyInvariant ((withdraw amount).runState s) [s.sender]
```

Proofs cover: existential attack witness (vulnerability is provably exploitable), universal safety proof (safe version preserves invariant), and deposit invariant preservation.

## CryptoHash

Unverified example demonstrating external library linking via the [Linker](/compiler#linker). Has no specs or proofs; it exists to show how external Yul helper functions integrate with compiled output. See the [Linking External Libraries](/guides/linking-libraries) guide for a walkthrough.

```verity
-- Placeholder hash for proofs (replaced with real Poseidon at compile time)
def hashTwo (a b : Uint256) : Contract Uint256 := do
  return add a b

-- Store hash of two values
def storeHashTwo (a b : Uint256) : Contract Unit := do
  let h ← hashTwo a b
  setStorage lastHash h
```

The EDSL uses a placeholder function (`add`) for the hash. At compile time, the [Linker](/guides/linking-libraries) replaces the compiled output with a call to the real Poseidon library via `Expr.externalCall` in the CompilationModel layer.

Source: [`Contracts/CryptoHash/Contract.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/CryptoHash/Contract.lean)

## ERC20

Baseline-verified ERC20 with `mint`, `transfer`, `approve`, `transferFrom` and formal spec/invariant modules. Source: [`Contracts/ERC20/`](https://github.com/lfglabs-dev/verity/tree/main/Contracts/ERC20).

## ERC721

Standards-shaped NFT contract demonstrating multi-mapping storage: uint-keyed `owners` and `tokenApprovals`, address-keyed `balances`, and double-mapping `operatorApprovals`. Exercises `getMappingUint`, `getMapping2`, `addressToWord`/`wordToAddress`, and constructor parameters.

```verity
verity_contract ERC721 where
  storage
    owner             : Address := slot 0
    totalSupply       : Uint256 := slot 1
    nextTokenId       : Uint256 := slot 2
    balances          : Address → Uint256 := slot 3
    owners            : Uint256 → Uint256 := slot 4
    tokenApprovals    : Uint256 → Uint256 := slot 5
    operatorApprovals : Address → Address → Uint256 := slot 6
```

Source: [`Contracts/ERC721/`](https://github.com/lfglabs-dev/verity/tree/main/Contracts/ERC721).

## Source

All contracts: [`Contracts/`](https://github.com/lfglabs-dev/verity/tree/main/Contracts).