# Adding Your First Contract to Verity

**Time Required**: 2-3 hours for first contract
**Prerequisites**: Basic familiarity with Lean 4 syntax and smart contract concepts

> **New to Lean 4?** You'll need to understand `do` notation, `def`/`theorem`, and basic tactic proofs (`simp`, `intro`, `constructor`). Start with:
> - [Lean 4 Manual: Basics](https://lean-lang.org/lean4/doc/): language overview
> - [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/): chapters 1–5 cover everything needed here
> - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/): `do` notation and monads (chapter 4)

This tutorial walks you through creating a complete verified smart contract from scratch. We'll build a **TipJar** contract, a simple balance ledger where users can deposit tips and check balances.

> **Why TipJar?** It uses the core EDSL features (mappings, `msgSender`, `require`, arithmetic) while staying simple enough to prove fully on your first attempt.

---

## Overview: The Verity Workflow

Every contract follows this path:

```
Specification → Implementation → Proofs → Compilation → Testing
     (30m)          (45m)         (1-2h)      (auto)      (30m)
```

**What you'll learn**:
- How to write formal specifications
- How to implement contracts in the EDSL
- How to prove correctness properties
- How to compile and test against deployed bytecode

---

## Phase 1: Setup (15 minutes)

### 1.1 Use the Scaffold Generator

The easiest way to start is with the scaffold generator:

```bash
python3 scripts/generate_contract.py TipJar \
  --fields "tips:mapping" \
  --functions "tip(uint256),getBalance(address)"
```

This creates all required files:
- `Contracts/TipJar/Spec.lean`: formal specification
- `Contracts/TipJar/Invariants.lean`: state invariants
- `Contracts/TipJar/SpecProofs.lean`: compilation correctness proof re-export
- `Contracts/TipJar/TipJar.lean`: EDSL implementation
- `Contracts/TipJar/Proofs/Basic.lean`: basic correctness proofs (EDSL matches spec)
- `Contracts/TipJar/Proofs/Correctness.lean`: advanced correctness proofs
- `test/PropertyTipJar.t.sol`: Foundry tests

### 1.2 Or Create Files Manually

```bash
mkdir -p Contracts/TipJar/Proofs
touch Contracts/TipJar/Spec.lean
touch Contracts/TipJar/Invariants.lean
touch Contracts/TipJar/SpecProofs.lean
touch Contracts/TipJar/TipJar.lean
touch Contracts/TipJar/Proofs/Basic.lean
touch Contracts/TipJar/Proofs/Correctness.lean
touch test/PropertyTipJar.t.sol
```

### 1.3 Our Contract Goal

We want to build a contract where:
- Users can deposit a tip (adding to their balance) via `tip(uint256)`
- Anyone can check a balance via `getBalance(address) → uint256`
- Each address has an independent balance
- Balances use EVM modular arithmetic (wrapping on overflow). This matches EVM opcodes, not Solidity's default checked arithmetic

> **Tip**: For contracts that should match Solidity ^0.8 behavior, add `require` guards (see `SafeCounter` example).

---

## Phase 2: Write Specification (30 minutes)

Specifications describe **what** the contract should do, not **how** it does it.

### 2.1 Create the Spec File

Open `Contracts/TipJar/Spec.lean`:

```lean
/-
  TipJar: Formal Specification

  Specifies deposit and balance-check behavior for a simple tip ledger.
-/

import Verity.Specs.Common
import Verity.Macro
import Verity.EVM.Uint256

namespace Contracts.TipJar.Spec

open Verity
open Verity.EVM.Uint256

/-- tip: increases sender's balance by amount -/
def tip_spec (amount : Uint256) (s s' : ContractState) : Prop :=
  -- Sender's balance increases by amount (modular arithmetic)
  s'.storageMap 0 s.sender = add (s.storageMap 0 s.sender) amount ∧
  -- No other mapping entries change
  storageMapUnchangedExceptKeyAtSlot 0 s.sender s s' ∧
  -- Non-mapping storage and context are preserved
  sameStorageAddrContext s s'

/-- getBalance: returns balance at given address, no state change -/
def getBalance_spec (addr : Address) (result : Uint256) (s : ContractState) : Prop :=
  result = s.storageMap 0 addr

end Contracts.TipJar.Spec
```

**Key Concepts**:
- `s` is the initial state, `s'` is the final state after the operation
- `storageMap 0` refers to the mapping at storage slot 0
- `storageMapUnchangedExceptKeyAtSlot` says only one key changed at one slot
- `sameStorageAddrContext` says uint256 storage, address storage, and context are preserved
- `add` is EVM modular addition (wraps at 2^256)

### 2.2 Create Invariants File

Open `Contracts/TipJar/Invariants.lean`:

```lean
/-
  TipJar: State Invariants

  Properties that hold across all operations.
-/

import Verity.Specs.Common

namespace Contracts.TipJar.Invariants

open Verity

-- Tip operations don't affect regular storage slots
def uint_storage_unchanged (s s' : ContractState) : Prop :=
  s'.storage = s.storage

-- Tip operations don't affect address storage
def addr_storage_unchanged (s s' : ContractState) : Prop :=
  s'.storageAddr = s.storageAddr

end Contracts.TipJar.Invariants
```

---

## Phase 3: Implement in EDSL (45 minutes)

Now we implement the contract using the EDSL. Every function in the EDSL is a `Contract`, a state-transforming computation that can succeed or revert.

### 3.1 Create EDSL Implementation

Open `Contracts/TipJar/TipJar.lean`:

```lean
/-
  TipJar: Deposit tips and check balances

  Demonstrates:
  - Mapping storage (Address → Uint256)
  - Sender identification via msgSender
  - EVM modular arithmetic

  Pattern: Simple balance ledger
-/

import Contracts.Common

namespace Contracts.TipJar

open Verity hiding pure bind
open Verity.EVM.Uint256

-- Storage layout: tips mapping at slot 0
def tips : StorageSlot (Address → Uint256) := ⟨0⟩

-- Deposit a tip: add amount to sender's balance
def tip (amount : Uint256) : Contract Unit := do
  let sender ← msgSender
  let currentBalance ← getMapping tips sender
  setMapping tips sender (add currentBalance amount)

-- Look up balance for any address
def getBalance (addr : Address) : Contract Uint256 := do
  getMapping tips addr

-- Example: Alice tips 100, then we check her balance
def exampleUsage : Contract Uint256 := do
  tip 100
  getBalance "0xAlice"

#eval (exampleUsage.run { defaultState with
  sender := "0xAlice",
  thisAddress := "0xTipJar"
}).getValue?
-- Expected output: some 100

end Contracts.TipJar
```

**EDSL API reference** (from `Verity/Core.lean`):

| Function | Type | Description |
|----------|------|-------------|
| `msgSender` | `Contract Address` | Get transaction sender |
| `msgValue` | `Contract Uint256` | Get ETH value sent with call |
| `blockTimestamp` | `Contract Uint256` | Get current block timestamp |
| `getStorage s` | `Contract Uint256` | Read uint256 slot |
| `setStorage s val` | `Contract Unit` | Write uint256 slot |
| `getMapping s key` | `Contract Uint256` | Read mapping entry |
| `setMapping s key val` | `Contract Unit` | Write mapping entry |
| `getStorageAddr s` | `Contract Address` | Read address slot |
| `setStorageAddr s val` | `Contract Unit` | Write address slot |
| `require cond msg` | `Contract Unit` | Revert if condition is false |

> **Tip**: Use `defaultState` to create a zero-initialized state for testing:
> ```lean
> #eval (myContract.run { defaultState with sender := "0xAlice" }).getValue?
> ```
> This avoids spelling out every field and stays valid when new fields are added.

### 3.2 Test the EDSL Implementation

```bash
lake build Contracts.TipJar
```

If successful, the `#eval` block evaluates and prints `some 100`.

---

## Phase 4: Prove Correctness (1-2 hours)

This is where formal verification happens. We prove that our implementation matches our specification.

### 4.1 Write Contract Specification Proofs

Open `Contracts/TipJar/Proofs/Basic.lean`:

```lean
/-
  TipJar: Basic Correctness Proofs

  Prove that the EDSL implementation matches the formal specification.
-/

import Contracts.TipJar.Spec
import Contracts.TipJar.Invariants
import Verity.Proofs.Stdlib.Automation

namespace Contracts.TipJar.Proofs

open Verity
open Verity.EVM.Uint256
open Contracts.TipJar
open Contracts.TipJar.Spec

-- tip: implementation matches spec
theorem tip_meets_spec (s : ContractState) (amount : Uint256) :
    tip_spec amount s (((tip amount).run s).snd) := by
  simp [tip, tip_spec, tips, msgSender, getMapping, setMapping, bind,
        Specs.storageMapUnchangedExceptKeyAtSlot,
        Specs.storageMapUnchangedExceptKey, Specs.storageMapUnchangedExceptSlot,
        Specs.sameStorageAddrContext, Specs.sameStorage, Specs.sameStorageAddr,
        Specs.sameContext]
  constructor
  · simp [Contract.run]
  · constructor
    · constructor
      · intro other hne; simp [*]
      · intro other hne addr; simp [*]
    · simp

-- getBalance: returns the correct value
theorem getBalance_correct (s : ContractState) (addr : Address) :
    getBalance_spec addr (((getBalance addr).run s).fst) s := by
  simp [getBalance, getBalance_spec, tips, getMapping]

-- getBalance doesn't modify state
theorem getBalance_preserves_state (s : ContractState) (addr : Address) :
    ((getBalance addr).run s).snd = s := by
  simp [getBalance, tips, getMapping]

-- Roundtrip: tip then getBalance returns updated balance
theorem tip_getBalance_roundtrip (amount : Uint256) (s : ContractState) :
    let s' := ((tip amount).run s).snd
    ((getBalance s.sender).run s').fst = add (s.storageMap 0 s.sender) amount := by
  simp [tip, getBalance, tips, msgSender, getMapping, setMapping, bind]

end Contracts.TipJar.Proofs
```

### 4.2 Common Proof Patterns

Here are the tactics you'll use most often:

**Pattern 1: Simple proofs with simp**
```lean
theorem simple_property : ... := by
  simp [functionName, helperFunctions]
```

**Pattern 2: Proofs with case splits**
```lean
theorem conditional_property : ... := by
  unfold functionName
  split
  · -- Case 1: condition true
    simp [...]
  · -- Case 2: condition false
    simp [...]
```

**Pattern 3: Proofs requiring intermediate lemmas**
```lean
theorem main_property : ... := by
  have h1 := helper_lemma_1
  have h2 := helper_lemma_2
  simp [h1, h2, ...]
```

See [Proof Debugging Handbook](/guides/debugging-proofs) for common errors and fixes.

### 4.3 Build and Check Proofs

```bash
# Build all proofs
lake build

# Check for incomplete proofs
grep -r "sorry" Contracts/TipJar/
```

**Goal**: Zero `sorry` statements before moving to testing.

---

## Phase 5: Add to Compiler (15 minutes)

### 5.1 Add Canonical Compiler Declaration

Add your contract in `Contracts/<Name>/<Name>.lean` with `verity_contract`.
Then register `Contracts.<Name>.spec` in `Compiler/Specs.lean` under `allSpecs`:

```lean
verity_contract TipJar where
  storage
    tips : Address -> Uint256 := slot 0

  function tip (amount : Uint256) : Unit := do
    let sender <- msgSender
    let current ← getMapping tips sender
    setMapping tips sender (add current amount)

  function getBalance (addr : Address) : Uint256 := do
    return (← getMapping tips addr)
```

### 5.2 Legacy Note

Handwritten `Compiler.Specs.*Spec` definitions are retained for proof-migration and
special workflows only; they are not the canonical CLI compile path.

Function selectors (the first 4 bytes of `keccak256("functionName(paramTypes)")`) are computed automatically by `computeSelectors` during compilation.

> **Tip**: Run `python3 scripts/check_selectors.py` to verify that the auto-computed selectors match `solc --hashes` output. You can also compute selectors manually with `python3 scripts/keccak256.py "tip(uint256)" "getBalance(address)"`.

### 5.3 Compilation Correctness

When you define a contract using the `verity_contract` macro in `Contracts/<Name>/<Name>.lean`, the framework provides the frontend typed-IR correctness path in `Compiler/TypedIRCompilerCorrectness.lean`. For the current explicit supported fragment, the compiler-level `CompilationModel -> IR` result now lives in `Compiler/Proofs/IRGeneration/Contract.lean` as a generic whole-contract theorem rooted at successful `CompilationModel.compile`.

The compiler proves Layer 2 preservation automatically for the supported fragment, with no manual per-contract bridge proofs needed. All three compiler layers are fully proved with 0 sorry and 0 axioms. The remaining trusted boundary is `solc` (Yul to bytecode). See `AXIOMS.md` for details.

> **Tip**: Study `Compiler/TypedIRCompilerCorrectness.lean` to see the supported statement fragment grammar and bridge theorem examples for Counter, SimpleStorage, ERC20, and ERC721.

### 5.4 Generate Yul Code

```bash
lake build verity-compiler
lake exe verity-compiler

# Check output
ls artifacts/yul/TipJar.yul
```

### 5.5 Verify Compilation

```bash
python3 scripts/check_yul.py
```

---

## Phase 6: Testing (30 minutes)

### 6.1 Create Property Tests

Open `test/PropertyTipJar.t.sol`. This is a complete, working test file you can copy-paste:

```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.33;

import "./yul/YulTestBase.sol";

/**
 * @title PropertyTipJarTest
 * @notice Property tests matching Lean theorems from Contracts/TipJar/Proofs/Basic.lean
 *
 * Tests 4 proven theorems:
 * 1. tip_meets_spec - Tip increases sender balance by amount
 * 2. getBalance_correct - getBalance returns correct value
 * 3. getBalance_preserves_state - getBalance is read-only
 * 4. tip_getBalance_roundtrip - Tip then getBalance returns updated balance
 */
contract PropertyTipJarTest is YulTestBase {
    address tipjar;
    address alice = address(0x1111);
    address bob = address(0x2222);

    function setUp() public {
        tipjar = deployYul("TipJar");
        require(tipjar != address(0), "Deploy failed");
    }

    //═══════════════════════════════════════════════════════════════════════
    // Property 1: tip_meets_spec (fuzz test)
    // Theorem: Tip increases sender's balance by the given amount
    //═══════════════════════════════════════════════════════════════════════

    /// Property: tip_meets_spec
    function testProperty_Tip_MeetsSpec(address sender, uint256 amount) public {
        // Constrain to avoid overflow in our assertion
        vm.assume(amount > 0 && amount <= type(uint256).max / 2);
        uint256 before = getBalanceFromStorage(sender);
        vm.assume(before + amount <= type(uint256).max);

        // Call tip(uint256) as sender
        vm.prank(sender);
        (bool success,) = tipjar.call(abi.encodeWithSignature("tip(uint256)", amount));
        require(success, "tip failed");

        // Assert: sender's balance increased by exactly `amount`
        assertEq(
            getBalanceFromStorage(sender),
            before + amount,
            "tip_meets_spec: balance should increase by amount"
        );
    }

    //═══════════════════════════════════════════════════════════════════════
    // Property 2: getBalance_correct (fuzz test)
    // Theorem: getBalance returns the stored value
    //═══════════════════════════════════════════════════════════════════════

    /// Property: getBalance_correct
    function testProperty_GetBalance_Correct(address addr, uint256 amount) public {
        // Set a known balance directly in storage
        setBalance(addr, amount);

        // Call getBalance(address)
        (bool success, bytes memory data) = tipjar.call(
            abi.encodeWithSignature("getBalance(address)", addr)
        );
        require(success, "getBalance failed");
        uint256 result = abi.decode(data, (uint256));

        // Assert: returned value matches storage
        assertEq(result, amount, "getBalance_correct: should return stored balance");
    }

    //═══════════════════════════════════════════════════════════════════════
    // Property 3: getBalance_preserves_state
    // Theorem: getBalance doesn't modify storage
    //═══════════════════════════════════════════════════════════════════════

    /// Property: getBalance_preserves_state
    function testProperty_GetBalance_PreservesState(address addr) public {
        // Set up some state
        setBalance(addr, 42);
        uint256 balanceBefore = getBalanceFromStorage(addr);

        // Call getBalance, should be read-only
        (bool success,) = tipjar.call(
            abi.encodeWithSignature("getBalance(address)", addr)
        );
        require(success, "getBalance failed");

        // Assert: storage unchanged
        assertEq(
            getBalanceFromStorage(addr),
            balanceBefore,
            "getBalance_preserves_state: storage should not change"
        );
    }

    //═══════════════════════════════════════════════════════════════════════
    // Property 4: tip_getBalance_roundtrip (fuzz test)
    // Theorem: Tip then getBalance returns the updated balance
    //═══════════════════════════════════════════════════════════════════════

    /// Property: tip_getBalance_roundtrip
    function testProperty_Tip_GetBalance_Roundtrip(uint256 amount) public {
        vm.assume(amount <= type(uint256).max / 2);

        uint256 before = getBalanceFromStorage(alice);

        // Tip as alice
        vm.prank(alice);
        (bool success1,) = tipjar.call(abi.encodeWithSignature("tip(uint256)", amount));
        require(success1, "tip failed");

        // Read back via getBalance
        (bool success2, bytes memory data) = tipjar.call(
            abi.encodeWithSignature("getBalance(address)", alice)
        );
        require(success2, "getBalance failed");
        uint256 result = abi.decode(data, (uint256));

        // Assert: roundtrip gives before + amount
        assertEq(
            result,
            before + amount,
            "tip_getBalance_roundtrip: should return before + amount"
        );
    }

    //═══════════════════════════════════════════════════════════════════════
    // Utility functions (reusable pattern for mapping-based contracts)
    //═══════════════════════════════════════════════════════════════════════

    /// @notice Read a mapping(address => uint256) entry directly from storage
    /// @dev TipJar uses slot 0 for the tips mapping.
    ///      Solidity/Yul mapping layout: keccak256(abi.encode(key, baseSlot))
    function getBalanceFromStorage(address addr) internal view returns (uint256) {
        bytes32 slot = keccak256(abi.encode(addr, uint256(0)));
        return uint256(vm.load(tipjar, slot));
    }

    /// @notice Write a mapping entry directly (for test setup)
    function setBalance(address addr, uint256 amount) internal {
        bytes32 slot = keccak256(abi.encode(addr, uint256(0)));
        vm.store(tipjar, slot, bytes32(amount));
    }
}
```

**Key patterns to understand**:
- `deployYul("TipJar")` deploys your pre-generated `artifacts/yul/TipJar.yul` contract (via `solc` assembly through `vm.ffi`)
- `vm.prank(sender)` sets `msg.sender` for the next call (Foundry cheatcode)
- `vm.load`/`vm.store` read/write raw storage slots (for assertions and test setup)
- Mapping slot formula: `keccak256(abi.encode(key, baseSlot))` (the standard Solidity storage layout)
- `vm.assume(...)` constrains fuzz inputs to avoid false failures (e.g., overflow)

### 6.2 Run Tests

```bash
FOUNDRY_PROFILE=difftest forge test --match-contract TipJar -vv
```

### 6.3 Verify Property Coverage

```bash
python3 scripts/extract_property_manifest.py  # regenerate manifest with new theorems
python3 scripts/check_property_manifest.py
python3 scripts/report_property_coverage.py --format=markdown
```

---

## Phase 7: Integration & Validation (15 minutes)

### 7.1 Final Checklist

```bash
# 1. All Lean code compiles (including proofs)
lake build

# 2. No incomplete proofs
grep -r "sorry" Contracts/TipJar/

# 3. Yul generates and compiles
lake build verity-compiler
lake exe verity-compiler
python3 scripts/check_yul.py

# 4. Tests pass
FOUNDRY_PROFILE=difftest forge test --match-contract TipJar

# 5. All CI checks pass
python3 scripts/check_selectors.py
python3 scripts/extract_property_manifest.py
python3 scripts/check_property_manifest.py
python3 scripts/check_property_manifest_sync.py
python3 scripts/check_property_coverage.py
python3 scripts/check_contract_structure.py
python3 scripts/check_storage_layout.py
python3 scripts/generate_verification_status.py --check
```

### 7.2 Add to Module Exports

Register your contract in the build by adding imports to the appropriate `All.lean` or lakefile target:
```lean
import Contracts.TipJar.Spec
import Contracts.TipJar.Invariants
import Contracts.TipJar.TipJar
import Contracts.TipJar.Proofs.Basic
import Contracts.TipJar.Proofs.Correctness
```

> **Tip**: The scaffold generator prints these exact lines when you run it. Copy them directly.

> **Tip**: Focus on the supported `CompilationModel` (`CompilationModel`) path for compiler-facing work. The scaffold and CI checks in this repository are aligned to that single path.

---

## Common Troubleshooting

### "Unknown identifier" in proofs

**Problem**: Lean can't find a function or type.

**Solution**: Check your imports and `open` statements:
```lean
import Contracts.TipJar.Spec
import Contracts.TipJar.TipJar

open Verity
open Verity.EVM.Uint256
```

### "Type mismatch" errors

**Problem**: Wrong return type.

**Solution**: Check the function signature matches what you return:
```lean
def tip (amount : Uint256) : Contract Unit := do  -- Returns nothing
  ...

def getBalance (addr : Address) : Contract Uint256 := do  -- Returns Uint256
  ...
```

### Proofs don't close with `simp`

**Problem**: `simp` can't solve the goal.

**Solution**: Try `unfold` first to expose definitions, then `simp`:
```lean
theorem my_thm : ... := by
  unfold myFunction bind
  simp [getMapping, setMapping, msgSender, tips]
```

See [Proof Debugging Handbook](/guides/debugging-proofs) for more patterns.

### Tests fail with "selector not found"

**Problem**: Function selector mismatch between Lean and Solidity.

**Solution**:
```bash
python3 scripts/check_selectors.py
```

---

## Next Steps

1. **Add more properties**: Think of edge cases (zero amount, same sender/receiver)
2. **Add access control**: Look at `Contracts/OwnedCounter/OwnedCounter.lean` for the `require` + owner pattern
3. **Add more functions**: Try adding a `withdraw` with balance checks (see `Contracts/Ledger/Ledger.lean`)
4. **Study existing contracts**: `SimpleStorage` (simplest), `Counter` (arithmetic), `Ledger` (mappings), `OwnedCounter` (composition)

### Learning Resources

- [Core Architecture](/core): the full EDSL API reference
- [Compiler](/compiler): how the compilation pipeline works
- [Proof Debugging Handbook](/guides/debugging-proofs): common tactic failures and fixes
- [Lean 4 Manual](https://lean-lang.org/lean4/doc/): language reference
- [Foundry Book](https://book.getfoundry.sh/): testing framework