# Proof Debugging Handbook

**Purpose**: Get unstuck when proofs fail with practical solutions, not theory.

**Who this is for**: Developers writing proofs in Verity, from beginners to experts encountering unfamiliar errors.

---

## Quick Reference

### Most Common Issues

| Symptom | Quick Fix | Section |
|---------|-----------|---------|
| "simp made no progress" | Pass definitions to `simp`: `simp [myDef]` | [Tactic Failures](#common-tactic-failures) |
| "omega failed" | Use `by_cases` to split constraints | [Tactic Failures](#common-tactic-failures) |
| "unknown identifier" | Check imports, spelling | [Import Errors](#import-errors) |
| "type mismatch" | Use `#check` to compare types | [Type Errors](#type-errors) |
| Proof too slow | Cache intermediate lemmas with `have` | [Performance](#proof-performance) |
| "motive is not type correct" | Use `generalize` before `induction` | [Induction Errors](#induction-errors) |

---

## Diagnostic Tools

Before debugging, know your tools:

### Type Inspection

```lean
-- Show the type of an expression
#check myTerm                    -- Output: myTerm : Type

-- Show all implicit arguments
#check @myFunction              -- Shows hidden type parameters

-- Print full definition
#print MyTheorem                -- Shows complete proof/definition

-- Show type and value
#reduce myComplexExpression     -- Normalizes and evaluates
```

### Goal Inspection

```lean
-- In a proof, inspect current state
theorem my_theorem : ... := by
  trace "{goal}"                -- Print current goal
  trace "Variable x: {x}"       -- Print specific variable
  sorry                         -- Skip temporarily to see what's needed
```

### Evaluation

```lean
-- Test functions
#eval myFunction arg1 arg2      -- Runs the function

-- Check equivalence
example : expr1 = expr2 := rfl  -- Definitional equality
```

---

## Common Tactic Failures

### "simp made no progress"

**Diagnosis**: `simp` doesn't know how to simplify your goal.

**Cause**: Definition not unfolded, or no simp lemmas apply.

**Solution 1**: Unfold before simping
```lean
-- ❌ DOESN'T WORK
theorem getValue_correct : ... := by
  simp [getStorage]  -- Error: simp made no progress

-- ✅ WORKS
theorem getValue_correct : ... := by
  unfold getValue     -- First unfold the definition
  simp [getStorage]   -- Now simp can make progress
```

**Solution 2**: Add simp attribute
```lean
-- Mark lemma for automatic simplification
@[simp] theorem my_helper_lemma : a + 0 = a := ...

-- Now simp will use it automatically
theorem uses_helper : ... := by
  simp  -- Automatically applies my_helper_lemma
```

**Solution 3**: Add specific lemmas to simp
```lean
-- Be explicit about what to simplify
simp [myDefinition, myLemma1, myLemma2]
```

### "omega failed to solve goal"

**Diagnosis**: Constraint is not linear arithmetic, or omega needs help.

**Cause**: Non-linear terms, dependent types, or complex constraints.

**Solution 1**: Split into linear cases
```lean
-- ❌ DOESN'T WORK (non-linear)
theorem complex_bound : a * b ≤ MAX := by
  omega  -- Error: not linear arithmetic

-- ✅ WORKS (split cases)
theorem complex_bound : a * b ≤ MAX := by
  by_cases ha : a = 0
  · simp [ha]     -- a = 0 case is trivial
  · by_cases hb : b = 0
    · simp [hb]   -- b = 0 case is trivial
    · omega       -- Now linear constraints only
```

**Solution 2**: Add intermediate lemmas
```lean
-- Help omega with explicit steps
theorem with_helper : a + b < MAX := by
  have h1 : a < MAX / 2 := by assumption
  have h2 : b < MAX / 2 := by assumption
  omega  -- Now has enough context
```

**Solution 3**: Convert inequalities
```lean
-- omega prefers ≤ over <
have h : a + b ≤ MAX := by omega
have h' : a + b < MAX + 1 := by omega
```

### "failed to synthesize instance"

**Diagnosis**: Lean can't find required typeclass instance.

**Cause**: Missing import, or instance doesn't exist.

**Solution 1**: Add missing import
```lean
-- ❌ DOESN'T WORK
#check (5 : Uint256)  -- Error: failed to synthesize OfNat

-- ✅ WORKS
import Verity.EVM.Uint256
#check (5 : Uint256)  -- Now works
```

**Solution 2**: Provide instance explicitly
```lean
-- If instance exists but isn't found automatically
example : MyClass MyType := inferInstance  -- Try to find it
example : MyClass MyType := by assumption  -- Use from context
```

### "motive is not type correct"

**Diagnosis**: Dependent type mismatch during induction.

**Cause**: Goal depends on the term being inducted on.

**Solution**: Generalize the motive
```lean
-- ❌ DOESN'T WORK
theorem bad_induction (xs : List α) : xs.length = n := by
  induction xs  -- Error: motive not type correct

-- ✅ WORKS
theorem good_induction (xs : List α) : xs.length = n := by
  generalize hlen : xs.length = m  -- Generalize first
  rw [hlen] in *
  induction xs
  · simp  -- Base case
  · simp [*]  -- Inductive case
```

---

## Type Errors

### "type mismatch"

**Diagnosis**: Expression has wrong type for context.

**Cause**: Incorrect type annotation, coercion needed, or logic error.

**Solution 1**: Check types
```lean
-- Use #check to debug
#check myValue      -- Expected: Uint256, Got: Nat

-- Add explicit coercion
example : Uint256 := ofNat myNatValue  -- ✅
```

**Solution 2**: Check expected vs actual
```lean
-- Error message shows:
-- Expected: a.val + b.val ≤ MAX_UINT256
-- Got:      a + b ≤ MAX_UINT256

-- Fix: Extract .val explicitly
have h : a.val + b.val ≤ MAX_UINT256 := by assumption
```

**Solution 3**: Rewrite to match types
```lean
-- Use rw to convert types
rw [theorem_that_converts_type]
exact my_proof
```

---

## Arithmetic & Overflow Proofs

### SafeAdd/SafeSub Failures

**Pattern 1**: Proving safeAdd returns Some
```lean
-- Goal: safeAdd a b = some c
theorem safeAdd_proof (h : a.val + b.val ≤ MAX_UINT256) :
    safeAdd a b = some ⟨a.val + b.val, by omega⟩ := by
  unfold safeAdd
  simp [willAddOverflow_eq_false h]
  -- Now prove the value is correct
  rfl
```

**Pattern 2**: Proving addition doesn't overflow
```lean
-- Common pattern for increment proofs
theorem increment_no_overflow (h : count.val < MAX_UINT256) :
    willAddOverflow count 1 = false := by
  unfold willAddOverflow
  simp
  omega  -- Uses h to show count.val + 1 ≤ MAX_UINT256
```

**Pattern 3**: Bounded arithmetic
```lean
-- Prove result stays in bounds
theorem bounded_add (h1 : a.val ≤ bound) (h2 : b.val ≤ bound) :
    (safeAdd a b).isSome → (safeAdd a b).get!.val ≤ 2 * bound := by
  intro hsome
  have hval : (safeAdd a b).get! = ⟨a.val + b.val, _⟩ := by
    simp [safeAdd] at hsome ⊢
    omega
  simp [hval]
  omega  -- Uses h1, h2
```

---

## Contract Execution: `.run`, `.fst`, `.snd`

Verity contracts are functions `ContractState → ContractResult α`. Use these to extract results:

| Expression | Returns | Type | When to use |
|------------|---------|------|-------------|
| `(op).run s` | Full result | `ContractResult α` | Matching on success/revert |
| `((op).run s).fst` | Return value | `α` | Proving what a getter returns |
| `((op).run s).snd` | Output state | `ContractState` | Proving how state changes |

**Common patterns in actual proofs:**

```lean
-- Proving a getter returns the right value
theorem retrieve_meets_spec (s : ContractState) :
  let result := ((retrieve).run s).fst      -- extract return value
  retrieve_spec result s := by ...

-- Proving a setter modifies state correctly
theorem store_meets_spec (s : ContractState) (value : Uint256) :
  let s' := ((store value).run s).snd       -- extract output state
  store_spec value s s' := by ...

-- Proving a guarded operation succeeds
theorem increment_unfold (s : ContractState) (h : ...) :
  (increment).run s = ContractResult.success ()  -- match full result
    { storage := ..., ... } := by ...
```

**Important caveat**: `.fst` returns `default` on revert. If the operation might revert, either:
- Add a guard hypothesis (e.g., `h_no_overflow : ...`) to ensure success
- Match on the full `ContractResult` instead

Avoid `Contract.runState` and `Contract.runValue` in new proofs — use `((op).run s).snd` and `((op).run s).fst` directly. The `run` + projection pattern is used by all existing proofs and works better with `simp`.

---

## Storage State Reasoning

### Function Extensionality

**Problem**: Prove two storage functions are equal.

**Pattern**: Use `ext` tactic
```lean
-- Goal: state1.storage = state2.storage
theorem storage_equal : state1.storage = state2.storage := by
  ext slot  -- For all slots
  by_cases h : slot = targetSlot
  · simp [h]  -- Show target slot is equal
  · simp [h]  -- Show other slots unchanged
```

### Storage Unchanged Except

**Pattern**: Common in contract proofs
```lean
-- Goal: Only slot k changed
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

**Problem**: Multiple storage updates in sequence.

**Pattern**: Use `have` to chain `_meets_spec` lemmas (see Counter proofs)
```lean
-- Actual pattern from Counter/Basic.lean
theorem increment_twice_adds_two (s : ContractState) :
  let s' := ((increment).run s).snd
  let s'' := ((increment).run s').snd
  s''.storage 0 = EVM.Uint256.add (EVM.Uint256.add (s.storage 0) 1) 1 := by
  have h1 := increment_adds_one s                         -- First op
  have h2 := increment_adds_one (((increment).run s).snd) -- Second op
  calc ... = ... := h2
    _ = ... := by rw [h1]
```

For low-level multi-update proofs, unfold bind directly:
```lean
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]
```

---

## Proof Pattern Library

### Authorization Checks

```lean
-- Pattern: Operation succeeds when authorized
theorem authorized_succeeds (state : ContractState) (sender : Address)
    (h : state.storageAddr owner.slot = sender) :
    ((operation sender).run state).isSuccess = true := by
  unfold operation onlyOwner require
  simp [h]  -- Simplifies sender = owner check
  -- Prove rest of operation
```

### Induction on Nat

```lean
-- Pattern: Structural induction
theorem by_nat_induction : ∀ n : Nat, P n := by
  intro n
  induction n with
  | zero =>
      -- Base case: P 0
      constructor
      simp
  | succ k ih =>
      -- Inductive case: P k → P (k+1)
      constructor
      simp [ih]  -- Use inductive hypothesis
```

### Induction on Lists

```lean
-- Pattern: List induction
theorem by_list_induction (xs : List α) : Q xs := by
  induction xs with
  | nil =>
      -- Base case: Q []
      simp [Q]
  | cons head tail ih =>
      -- Inductive case: Q tail → Q (head :: tail)
      simp [Q, ih]
```

### Case Analysis

```lean
-- Pattern: Boolean case split
theorem by_bool_cases (b : Bool) : R b := by
  cases b
  · -- Case: b = false
    simp [R]
  · -- Case: b = true
    simp [R]
```

### Option Handling

```lean
-- Pattern: Option.isSome vs Option.get?
theorem option_proof (opt : Option α) (h : opt.isSome) :
    opt.get! = value := by
  cases opt
  · contradiction  -- opt = none contradicts h
  · simp            -- opt = some x, prove x = value
```

---

## Tactic Ordering

**Preferred (Verity standard)**:
```lean
-- ✅ BEST: Pass all definitions to simp in one call
theorem retrieve_meets_spec (s : ContractState) :
  let result := ((retrieve).run s).fst
  retrieve_spec result s := by
  simp [retrieve, storedData, retrieve_spec]  -- One shot
```

**Alternative when simp can't unfold**:
```lean
-- ✅ OK: unfold first, then simp
theorem good_order : getValue state = value := by
  unfold getValue     -- Expose the definition
  simp [getStorage]   -- Now simp can work with it
```

**General rule**: Pass definitions directly to `simp` (e.g. `simp [myDef, mySlot]`). Use `unfold` only when `simp` can't unfold a definition on its own (e.g., mutually recursive definitions).

---

## Common Error Messages

### Import Errors

| Error | Cause | Fix |
|-------|-------|-----|
| "unknown identifier 'Uint256'" | Missing import | `import Verity.EVM.Uint256` |
| "unknown identifier 'Contract'" | Missing import | `import Verity.Core` and `open Verity` |
| "unknown identifier 'ContractState'" | Missing import | `import Verity.Core` and `open Verity` |
| "ambiguous identifier" | Multiple imports | Use fully qualified name |

### Type Class Errors

| Error | Cause | Fix |
|-------|-------|-----|
| "failed to synthesize OfNat" | Missing numeric instance | Check type has OfNat instance |
| "failed to synthesize Inhabited" | No default value | Provide explicit value |
| "failed to synthesize DecidableEq" | Can't decide equality | Use `= true` or `= false` explicitly |

### Proof Errors

| Error | Cause | Fix |
|-------|-------|-----|
| "unsolved goals" | Proof incomplete | Add sorry to see remaining goals |
| "maximum recursion depth" | Infinite tactic loop | Add fuel or use different tactic |
| "kernel type mismatch" | Proof term invalid | Check proof type matches theorem |
| "deterministic timeout" | Proof too expensive | Simplify or add intermediate lemmas |

---

## Proof Performance

### Slow Proofs (>10 seconds)

**Problem**: Proof takes too long.

**Diagnosis**: Expensive tactics on large terms.

**Solution 1**: Cache intermediate results
```lean
-- ❌ SLOW: Recomputes expensive_lemma multiple times
theorem slow_proof : ... := by
  simp [expensive_lemma args]
  rw [expensive_lemma args]
  exact expensive_lemma args

-- ✅ FAST: Compute once, reuse
theorem fast_proof : ... := by
  have h := expensive_lemma args  -- Compute once
  simp [h]
  rw [h]
  exact h
```

**Solution 2**: Split into smaller lemmas
```lean
-- Instead of one giant proof
theorem giant_proof : A ∧ B ∧ C ∧ D := by
  constructor; [proof of A]
  constructor; [proof of B]
  constructor; [proof of C]
  [proof of D]

-- Split into pieces
theorem prove_A : A := by [proof]
theorem prove_B : B := by [proof]
theorem prove_C : C := by [proof]
theorem prove_D : D := by [proof]

-- Combine quickly
theorem fast_proof : A ∧ B ∧ C ∧ D := ⟨prove_A, prove_B, prove_C, prove_D⟩
```

**Solution 3**: Use rfl instead of simp
```lean
-- ❌ SLOW: simp does lots of work
example : (a + 0) = a := by simp

-- ✅ FAST: rfl is instant for definitional equality
example : (a + 0) = a := rfl  -- Works if definitionally equal
```

---

## Debugging Workflows

### Workflow 1: Unknown Error

1. **Read error message carefully** - Often points to exact issue
2. **Use #check** on terms mentioned in error
3. **Simplify** - Remove parts of proof until it works
4. **Add sorry** - See remaining goals after partial proof
5. **Search codebase** - Find similar proofs that worked

### Workflow 2: Stuck on Goal

1. **Inspect goal** - `trace "{goal}"` to see full state
2. **Try tactics** systematically:
   - `simp` (simplify)
   - `unfold` (expand definitions)
   - `rw` (rewrite with lemma)
   - `omega` (arithmetic)
3. **Split cases** - `by_cases` or `cases` to reduce complexity
4. **Add assumptions** - Use `have` for intermediate steps

### Workflow 3: Type Mismatch

1. **Check both types** - `#check expected` and `#check actual`
2. **Look for coercions** - May need `ofNat`, `.val`, etc.
3. **Rewrite** - Use `rw [lemma]` to transform type
4. **Convert** - Add explicit conversion functions

---

## Real Examples from Verity

Verity proofs follow the **`_meets_spec` pattern**: each EDSL operation has a corresponding `_spec` predicate, and the proof shows the operation satisfies it. This is the dominant pattern across all verified contracts.

### Example 1: SimpleStorage retrieve (spec-based proof)

**Goal**: Prove `retrieve` returns the stored value.

```lean
-- The spec predicate (defined in Specs/SimpleStorage/Spec.lean)
def retrieve_spec (result : Uint256) (s : ContractState) : Prop :=
  result = s.storage storedData.slot

-- The proof (from Proofs/SimpleStorage/Basic.lean)
theorem retrieve_meets_spec (s : ContractState) :
  let result := ((retrieve).run s).fst
  retrieve_spec result s := by
  simp [retrieve, storedData, retrieve_spec]
```

**Key insights**:
- Theorem states the operation's result satisfies a named `_spec` predicate
- Single `simp` with the operation, slot name, and spec definition — no `unfold` needed
- `((op).run s).fst` extracts the return value; `.snd` extracts the output state

### Example 2: Counter increment (multi-conjunct spec)

**Goal**: Prove `increment` updates count and preserves everything else.

```lean
-- The spec is a conjunction: correct value ∧ other slots preserved ∧ context preserved
theorem increment_meets_spec (s : ContractState) :
  let s' := ((increment).run s).snd
  increment_spec s s' := by
  refine ⟨?_, ?_, ?_⟩                -- Split the conjunction into 3 goals
  · rfl                               -- Goal 1: s'.storage 0 = add (s.storage 0) 1
  · intro slot h_neq                  -- Goal 2: other slots unchanged
    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, ...]  -- Goal 3: context preserved
```

**Key insights**:
- `refine ⟨?_, ?_, ?_⟩` splits a conjunction into separate goals
- Each conjunct is proved independently (value correctness, isolation, context preservation)
- When `simp` alone doesn't close a goal, use `split` for `if`-expressions and `exact absurd` for contradictions

### Example 3: Owned transferOwnership (require-guarded proof)

**Goal**: Prove ownership transfer works when the caller is the current owner.

```lean
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
  -- Unfold the full chain: transferOwnership → onlyOwner → isOwner → require → setStorageAddr
  simp only [transferOwnership, onlyOwner, isOwner, owner,
    msgSender, getStorageAddr, setStorageAddr,
    Verity.require, Verity.pure, Verity.bind, Bind.bind, Pure.pure,
    Contract.run, ContractResult.snd, ContractResult.fst,
    transferOwnership_spec]
  -- After unfolding, the guard is (s.sender == s.storageAddr 0)
  -- h_is_owner resolves it, so execution proceeds to setStorageAddr
  simp [h_is_owner, Specs.sameStorageMapContext, ...]
  intro slot h_neq
  simp [beq_iff_eq, h_neq]
```

**Key insights**:
- `require`/`onlyOwner` guards add a hypothesis like `h_is_owner : s.sender = s.storageAddr 0`
- Pass the guard hypothesis to `simp` so it can resolve the boolean check
- After the guard resolves, the proof proceeds like an unguarded operation

### Example 4: Ledger sum preservation (conservation proof)

**Goal**: Total balance unchanged by transfer (accounts for duplicate addresses).

```lean
-- Uses countOcc to handle addresses appearing multiple times in the list
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
  -- Strategy: use point_update_sum_eq for sender (subtract) and recipient (add)
  have h_sender := point_update_sum_eq ...
  have h_recipient := point_update_sum_eq ...
  -- Combine with omega for final arithmetic
  omega
```

**Key insights**:
- Conservation proofs use `countOcc` to account for duplicate addresses in the sum
- Helper lemma `point_update_sum_eq` relates storage point-updates to sum changes
- `omega` handles the final linear arithmetic after `have` statements set up equations

### Pattern summary

| Pattern | When to use | Example |
|---------|-------------|---------|
| `simp [op, slot, spec]` | Simple read-only operations | `retrieve_meets_spec` |
| `refine ⟨?_, ?_, ?_⟩` | Multi-conjunct specs | `increment_meets_spec` |
| `simp only [... chain ...]` + `simp [h_guard]` | Guarded operations with `require` | `transferOwnership_meets_spec_when_owner` |
| `have h := helper ...` + `omega` | Conservation / arithmetic properties | `transfer_sum_preservation` |

---

## Getting Help

### When to Ask for Help

Try these first:
1. ✅ Read this guide
2. ✅ Search codebase for similar proofs
3. ✅ Use diagnostic tools (#check, trace)
4. ✅ Simplify to minimal failing example

If still stuck:
- **GitHub Discussions**: Post minimal example
- **Issues**: If you found a bug or missing documentation
- **Lean Zulip**: For general Lean questions

### Minimal Example Template

```lean
-- Minimal failing example for help requests
import Verity.Core

-- Context
def myDefinition : Type := ...

-- What I'm trying to prove
theorem my_theorem : myProperty := by
  unfold myDefinition
  simp
  -- ERROR: simp made no progress
  sorry

-- What I expected: ...
-- What I got: ...
```

---

## Advanced Debugging

### Proof Term Inspection

```lean
-- See the proof term Lean generates
#print my_theorem  -- Shows proof term

-- Check if proof is what you expect
example : ... := proof_term  -- Manually write proof term
```

### Tactic Tracing

```lean
-- Enable tactic tracing
set_option trace.Meta.Tactic.simp true

theorem my_theorem : ... := by
  simp  -- Will show all simplification steps
```

### Goal State Logging

```lean
-- Log intermediate states
theorem complex_proof : ... := by
  trace "Initial goal: {goal}"
  unfold definition1
  trace "After unfold: {goal}"
  simp
  trace "After simp: {goal}"
  omega
```

---

## Summary: Quick Decision Tree

**Proof fails?**
→ Read error message

**"unknown identifier"?**
→ Check imports, spelling

**"type mismatch"?**
→ Use #check, add coercion

**"simp made no progress"?**
→ Add unfold first

**"omega failed"?**
→ Split cases with by_cases

**Proof too slow?**
→ Cache intermediate results with have

**Still stuck?**
→ Search for similar proofs, ask for help

---

## Additional Resources

- **First Contract Tutorial**: [/guides/first-contract](/guides/first-contract) - Start here if new
- **Code Comment Conventions**: [CONTRIBUTING.md](https://github.com/Th0rgal/verity/blob/main/CONTRIBUTING.md) - Style guide
- **Proof Structure**: [Compiler/Proofs/README.md](https://github.com/Th0rgal/verity/blob/main/Compiler/Proofs/README.md) - Architecture
- **Lean 4 Manual**: [https://lean-lang.org/lean4/doc/](https://lean-lang.org/lean4/doc/) - Language reference
- **Lean Zulip**: [https://leanprover.zulipchat.com/](https://leanprover.zulipchat.com/) - Community chat

---

**Happy Proving! 🎉**

Remember: Every expert was once stuck on "simp made no progress". You've got this!