# Example Contracts

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, and SimpleToken combines all three.

## How to organize a contract

- **Spec**: `Verity/Specs/<Name>/Spec.lean`
- **Invariants**: `Verity/Specs/<Name>/Invariants.lean`
- **Implementation**: `Verity/Examples/<Name>.lean`
- **Basic proofs**: `Verity/Proofs/<Name>/Basic.lean`
- **Advanced proofs**: `Verity/Proofs/<Name>/Correctness.lean`
- **Compilation correctness**: `Compiler/TypedIRCompilerCorrectness.lean` + `Compiler/Proofs/IRGeneration/Contract.lean` for the current supported fragment.
- **Reusable proof infra**: `Verity/Proofs/Stdlib/`

Example (SimpleStorage):
- Spec: `Contracts/SimpleStorage/Spec.lean`
- Implementation: `Contracts/SimpleStorage/SimpleStorage.lean`
- Basic proofs: `Contracts/SimpleStorage/Proofs/Basic.lean`
- Correctness proofs: `Contracts/SimpleStorage/Proofs/Correctness.lean`

## Authoring checklist

1. Define behavior in `Contracts/<Name>/Spec.lean`.
2. Add invariants in `Contracts/<Name>/Invariants.lean` if needed.
3. Implement the EDSL contract in `Contracts/<Name>/<Name>.lean`.
4. Prove spec adherence in `Contracts/<Name>/Proofs/Basic.lean` using `Verity/Proofs/Stdlib/` helpers.

## SimpleStorage

Single storage slot with get/set.

```lean
def storedData : StorageSlot Uint256 := ⟨0⟩

def store (value : Uint256) : Contract Unit := do
  setStorage storedData value

def retrieve : Contract Uint256 := do
  getStorage storedData
```

Proofs cover store/retrieve roundtrip and state isolation.

## Counter

Read-modify-write with increment and decrement.

```lean
def count : StorageSlot Uint256 := ⟨0⟩

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

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

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

## SafeCounter

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

```lean
def increment : Contract 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.

```lean
def owner : StorageSlot Address := ⟨0⟩

def isOwner : Contract Bool := do
  let sender ← msgSender
  let currentOwner ← getStorageAddr owner
  return sender == currentOwner

def onlyOwner : Contract Unit := do
  let ownerCheck ← isOwner
  require ownerCheck "Caller is not the owner"
```

Proofs cover access control enforcement and ownership transfer.

## OwnedCounter

Composes Owned and Counter. Increment/decrement require ownership.

```lean
def owner : StorageSlot Address := ⟨0⟩
def count : StorageSlot Uint256 := ⟨1⟩

def increment : Contract 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.

```lean
def balances : StorageSlot (Address → Uint256) := ⟨0⟩

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

def transfer (to : Address) (amount : Uint256) : Contract 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.

```lean
def owner : StorageSlot Address := ⟨0⟩
def balances : StorageSlot (Address → Uint256) := ⟨1⟩
def totalSupply : StorageSlot Uint256 := ⟨2⟩

def mint (to : Address) (amount : Uint256) : Contract 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

def transfer (to : Address) (amount : Uint256) : Contract 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.

## ReentrancyExample

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

```lean
-- 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 Libraries](/guides/linking-libraries) guide for a walkthrough.

```lean
-- 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/Th0rgal/verity/blob/main/Contracts/CryptoHash/Contract.lean)

## ERC20 (Foundation Scaffold)

Baseline-verified ERC20 foundation scaffold with executable logic (`mint`, `transfer`, `approve`, `transferFrom`) and formal spec/invariant modules.

Source:
- Implementation: [`Contracts/ERC20/ERC20.lean`](https://github.com/Th0rgal/verity/blob/main/Contracts/ERC20/ERC20.lean)
- Spec: [`Contracts/ERC20/Spec.lean`](https://github.com/Th0rgal/verity/blob/main/Contracts/ERC20/Spec.lean)
- Invariants: [`Contracts/ERC20/Invariants.lean`](https://github.com/Th0rgal/verity/blob/main/Contracts/ERC20/Invariants.lean)

## Pattern progression

1. **SimpleStorage**: single slot
2. **Counter**: arithmetic
3. **SafeCounter**: stdlib integration
4. **Owned**: access control
5. **OwnedCounter**: composition (Owned + Counter)
6. **Ledger**: mapping storage
7. **SimpleToken**: full composition (Owned + Ledger + supply tracking)
8. **ReentrancyExample**: vulnerability modeling and safety proofs
9. **CryptoHash**: external library linking (unverified)
10. **ERC20**: standards-oriented token scaffold with baseline proofs and specs/invariants

## Source

All contracts are in [`Contracts/`](https://github.com/Th0rgal/verity/tree/main/Contracts).