# Proof Debugging Handbook

When proofs fail. Patterns and fixes, no theory.

## Quick reference

| Symptom | Fix |
|---------|-----|
| "simp made no progress" | Pass definitions to `simp`: `simp [myDef]`, or `unfold` first |
| "omega failed" | Split with `by_cases`; omega is linear-only |
| "unknown identifier" | Check imports and `open` |
| "type mismatch" | Use `#check` on both sides; add `.val` or `ofNat` |
| "motive is not type correct" | `generalize` before `induction` |
| "failed to synthesize OfNat" | Add `import Verity.EVM.Uint256` |
| Proof too slow | Cache with `have h := ...`; prefer `rfl` over `simp` |

## Diagnostic tools

```verity
#check myTerm                    -- show type
#check @myFunction               -- show implicit args
#print MyTheorem                 -- show full definition
#reduce expr                     -- normalize and evaluate
#eval myFunction arg1 arg2       -- run it

-- In a proof
theorem t : ... := by
  trace "goal: {goal}"
  sorry                          -- skip to see remaining goals
```

## Tactic failures

### `simp made no progress`

`simp` doesn't know how to simplify your goal. Either unfold first or pass the right lemmas:

```verity
-- Doesn't work
theorem getValue_correct : ... := by
  simp [getStorage]

-- Works
theorem getValue_correct : ... := by
  unfold getValue
  simp [getStorage]
```

If a helper applies often, mark it `@[simp]` once so you don't have to thread it everywhere.

### `omega failed`

`omega` solves *linear* integer arithmetic. Non-linear terms (`a * b`), dependent types, or quantifiers will defeat it. Split into linear cases:

```verity
theorem complex_bound : a * b ≤ MAX := by
  by_cases ha : a = 0
  · simp [ha]
  · by_cases hb : b = 0
    · simp [hb]
    · omega
```

Or stage with `have` so omega has concrete bounds in context.

### `motive is not type correct`

The goal depends on the term you're inducting on. Generalize the dependency first:

```verity
theorem good_induction (xs : List α) : xs.length = n := by
  generalize hlen : xs.length = m
  rw [hlen] in *
  induction xs <;> simp [*]
```

## Type errors

`#check` is the fastest debugger. The error message usually shows expected vs got, read both sides carefully. For `Uint256`/`Nat` mismatches, extract `.val` or coerce with `ofNat`.

## `.run`, `.fst`, `.snd`

Verity contracts are `ContractState → ContractResult α`. Three projection patterns dominate:

| Expression | Returns | Use for |
|------------|---------|---------|
| `(op).run s` | Full `ContractResult α` | Match on success/revert |
| `((op).run s).fst` | Return value `α` | Prove what a getter returns |
| `((op).run s).snd` | Output state | Prove how state changes |

`.fst` returns `default` on revert, if the operation might revert, add a guard hypothesis or match the full result. Avoid `Contract.runState`/`Contract.runValue` in new proofs.

## Storage reasoning

**Function extensionality.** Two storage functions equal? Use `ext slot` and split:

```verity
theorem only_slot_k_changed :
    ∀ slot, slot ≠ k → state'.storage slot = state.storage slot := by
  intro slot hneq
  unfold updateOperation
  simp [setStorage, hneq]
```

**Sequential operations.** Chain `_meets_spec` lemmas with `have`, or unfold `bind` for low-level reasoning:

```verity
theorem two_updates (s : ContractState) :
  let s' := ((do setStorage slot1 val1; setStorage slot2 val2).run s).snd
  s'.storage slot2.slot = val2 := by
  simp [bind, Bind.bind, setStorage, Contract.run, ContractResult.snd]
```

## Real examples

Verity proofs follow the **`_meets_spec` pattern**: each EDSL operation has a `_spec` predicate, and the proof shows the operation satisfies it.

### Read-only (SimpleStorage)

```verity
theorem retrieve_meets_spec (s : ContractState) :
  let result := ((retrieve).run s).fst
  retrieve_spec result s := by
  simp [retrieve, storedData, retrieve_spec]
```

Single `simp` with operation + slot + spec, no `unfold` needed.

### Multi-conjunct spec (Counter)

```verity
theorem increment_meets_spec (s : ContractState) :
  let s' := ((increment).run s).snd
  increment_spec s s' := by
  refine ⟨?_, ?_, ?_⟩
  · rfl
  · intro slot h_neq
    simp only [increment, count, getStorage, setStorage,
      bind, Contract.run, Bind.bind, ContractResult.snd]
    split
    · next h => exact absurd (by simp [beq_iff_eq] at h; exact h) h_neq
    · rfl
  · simp [Specs.sameAddrMapContext]
```

`refine ⟨?_, ?_, ?_⟩` splits a conjunction; prove each conjunct independently.

### `require`-guarded (Owned)

```verity
theorem transferOwnership_meets_spec_when_owner (s : ContractState) (newOwner : Address)
  (h_is_owner : s.sender = s.storageAddr 0) :
  let s' := ((transferOwnership newOwner).run s).snd
  transferOwnership_spec newOwner s s' := by
  simp only [transferOwnership, onlyOwner, isOwner, owner,
    msgSender, getStorageAddr, setStorageAddr,
    Verity.require, Verity.pure, Verity.bind, Bind.bind, Pure.pure,
    Contract.run, ContractResult.snd, transferOwnership_spec]
  simp [h_is_owner, Specs.sameStorageMapContext]
  intro slot h_neq
  simp [beq_iff_eq, h_neq]
```

Pass the guard hypothesis to `simp` so it can resolve the boolean check.

### Conservation (Ledger)

```verity
theorem transfer_sum_preservation (s : ContractState) (to : Address) (amount : Uint256)
  (addrs : List Address) (h_guard : ...) :
  let s' := ((transfer to amount).run s).snd
  balanceSum s' addrs + countOccU s.sender addrs * amount
    = balanceSum s addrs + countOccU to addrs * amount := by
  have h_sender := point_update_sum_eq ...
  have h_recipient := point_update_sum_eq ...
  omega
```

Conservation uses `countOcc` for duplicate-safe sums; helper lemmas stage the equation, omega finishes.

### Pattern summary

| Pattern | When |
|---------|------|
| `simp [op, slot, spec]` | Simple read-only |
| `refine ⟨?_, ?_, ?_⟩` | Multi-conjunct specs |
| `simp only [...]` then `simp [h_guard]` | Guarded operations |
| `have h := helper ...` then `omega` | Conservation / arithmetic |

## Tactic ordering

Prefer one-shot `simp [def, slot, spec]`. Use `unfold` only when `simp` can't expose a definition on its own (e.g., mutually recursive). Don't sprinkle `unfold`s when one `simp` would do.

## See also

- [First Contract](/first-contract), the full workflow this guide drops into.
- [Core Architecture](/core), types and the `Contract` monad.
- [EDSL API Reference](/edsl-api-reference), every primitive with its simp lemma.