# Getting Started

This guide walks you through setting up a development environment for Verity, building the project, and running your first verification.

## Prerequisites

| Tool | Purpose | Required for |
|------|---------|-------------|
| [elan](https://github.com/leanprover/elan) | Lean toolchain manager | Building everything |
| [Foundry](https://book.getfoundry.sh/getting-started/installation) | Solidity testing framework | Running property tests |
| Python 3.8+ | Scripts | Scaffold generator, CI scripts |
| [`solc`](https://docs.soliditylang.org/en/latest/installing-solidity.html) 0.8.33+ | Solidity compiler | Differential tests only |

> **Installing `solc`**: Foundry does not ship `solc`. Install it separately via [`solc-select`](https://github.com/crytic/solc-select):
> ```bash
> pip3 install solc-select
> solc-select install 0.8.33
> solc-select use 0.8.33
> solc --version
> ```
> On macOS you can also use `brew install solidity`. The project requires version 0.8.33+.

## 1. Install Lean 4

[elan](https://github.com/leanprover/elan) manages Lean toolchains (like `rustup` for Rust). The project pins its toolchain in `lean-toolchain`.

```bash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
```

Follow the prompts, then **reload your shell**:

```bash
source ~/.elan/env    # or open a new terminal
lean --version        # should print leanprover/lean4:v4.15.0 (or whatever lean-toolchain pins)
```

> **Tip**: If `source ~/.elan/env` does not work, check `~/.profile` or `~/.bashrc` for the elan path entry.

## 2. Install Foundry

[Foundry](https://book.getfoundry.sh/) provides `forge` for compiling and testing Solidity contracts. The project uses it for property-based differential tests.

```bash
curl -L https://foundry.paradigm.xyz | bash
foundryup
forge --version
```

## 3. Clone and build

```bash
git clone https://github.com/lfglabs-dev/verity.git
cd verity
lake build                # Downloads dependencies and verifies the current proof set
```

The first build downloads Mathlib and compiles everything, expect **20–45 minutes** on first run (Mathlib is large). Subsequent builds are incremental and much faster (seconds to minutes).

## Explore a proof

Once the build completes, the core loop is **write a contract in Lean → prove it correct → compile it to EVM bytecode**:

```bash
lake build Contracts.SimpleStorage.Proofs.Basic    # verifies theorems in seconds
lake exe verity-compiler                            # writes artifacts/yul/SimpleStorage.yul
```

Three directories to keep in mind:

1. `Contracts/<Name>/<Name>.lean`, EDSL implementation, executable Lean code.
2. `Contracts/<Name>/Spec.lean`, `Invariants.lean`, `Proofs/`, logical specs (`Prop`) and proofs.
3. `Compiler/Specs.lean`, `CompilationModel` values that generate IR/Yul.

## 4. Run the test suite

```bash
# All tests (property tests deploy Yul via vm.ffi, so FFI is required)
FOUNDRY_PROFILE=difftest forge test

# Unit tests only (no FFI needed)
forge test --no-match-path "test/Property*" --no-match-path "test/Differential*" --no-match-path "test/CallValue*" --no-match-path "test/CalldataSize*" --no-match-path "test/yul/*"
```

The `difftest` profile enables `vm.ffi()` calls needed by property tests (to invoke `solc` for Yul compilation), differential tests (to invoke the Lean-based interpreter), and Yul end-to-end tests. This requires `lake build` to have completed successfully.

## 5. Generate your first contract

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

This writes EDSL implementation, specs, invariants, proofs, and a Foundry property test under `Contracts/TipJar/` and `test/`. Follow the printed instructions to register the contract in `Compiler/Specs.lean`, then see the [First Contract tutorial](/first-contract) for the full walkthrough.

## 6. Compile to Yul/EVM

```bash
lake build verity-compiler
lake exe verity-compiler          # Output in artifacts/yul/
```

For contracts that use external libraries (e.g., Poseidon hash):

```bash
lake exe verity-compiler --link examples/external-libs/PoseidonT3.yul -o artifacts/yul
```

See the [Linking Libraries guide](/guides/linking-libraries) for details.

## What to read next

1. **[Example Contracts](/examples)**, Progressive examples from single-slot storage to token transfers
2. **[Core Architecture](/core)**, The Contract monad, state model, and design decisions
3. **[First Contract tutorial](/first-contract)**, Hands-on guide building a TipJar from scratch
4. **[Compiler reference](/compiler)**, Full CompilationModel DSL documentation