# Add a Contract (Spec → Proof → Compiler → Tests)

> **New to Verity?** Follow the [step-by-step First Contract tutorial](/first-contract) instead. It walks through building a TipJar contract from scratch with explanations at every step (2–3 hours).

This is the shortest reliable path to add a new contract end-to-end, anchored to SimpleStorage. It assumes familiarity with the Verity EDSL and proof patterns.

Porting from Solidity? Start with [Solidity to Verity Translation](/guides/solidity-to-verity). For production contracts with inheritance, modifiers, precompiles, linked externals, or protocol-specific cryptography, use [Production Solidity Patterns](/guides/production-solidity-patterns) before introducing new helpers.

## Quick Start: Scaffold Generator

Use the scaffold generator to create all boilerplate files at once:

```bash
# Simple contract with one uint256 field
python3 scripts/generate_contract.py MyContract

# Contract with typed fields
python3 scripts/generate_contract.py MyToken --fields "balances:mapping,totalSupply:uint256,owner:address"

# Contract with typed function signatures
python3 scripts/generate_contract.py MyToken --fields "balances:mapping" --functions "deposit(uint256),withdraw(uint256),getBalance(address)"

# Contract with uint256-keyed mapping
python3 scripts/generate_contract.py MyRegistry --fields "data:mapping(uint256)" --functions "store(uint256,uint256),get(uint256)"

# Preview without creating files
python3 scripts/generate_contract.py MyContract --dry-run
```

This creates 7 scaffold files (EDSL, Spec, Invariants, Proofs re-export shim, Basic proofs, Correctness proofs, Property tests) and prints follow-up steps for `All.lean` plus canonical contract registration.

`generate_contract.py` currently scaffolds scalar fields plus simple `mapping(address => uint256)` / `mapping(uint256 => uint256)` storage only. For `mappingStruct` / `mappingStruct2` layouts with packed members, use the native `verity_contract` storage forms `MappingStruct(...)` / `MappingStruct2(...)` and the corresponding `structMember` / `setStructMember` operations directly.

## Checklist

1. **Spec**
   - Define interface and storage in `Contracts/<Name>/Spec.lean`
   - Add invariants in `Contracts/<Name>/Invariants.lean` (optional)
   - Align function signatures with Solidity types and storage slots

2. **EDSL Implementation**
   - Implement contract logic in `Contracts/<Name>/<Name>.lean`
   - Reuse helper lemmas for storage updates and mapping reads

3. **Contract Specification Proofs**
   - Prove correctness in `Contracts/<Name>/Proofs/Basic.lean` and `Correctness.lean`
   - Each theorem states observable behavior (return values + storage deltas)

4. **Compiler Integration + Layer 2 Proofs**
   - Add canonical `verity_contract` declaration in `Contracts/<Name>/<Name>.lean`
   - Handwritten `Compiler.Specs.*Spec` definitions still exist but are not the canonical compile path
   - Compilation correctness is provided by the generic typed-IR theorem in `Compiler/TypedIRCompilerCorrectness.lean`
   - Layer 2 preservation is proved generically by `Compiler/Proofs/IRGeneration/Contract.lean`

5. **Differential Tests** (not generated by scaffold; copy from `DifferentialCounter.t.sol`)
   - Add harness in `test/Differential<Name>.t.sol`
   - Inherit `YulTestBase`, `DiffTestConfig`, and `DifferentialTestBase` (all three required)
   - Add edge-value tests using `_edgeUintValues()`

6. **Property Tests** (Proofs → Tests)
   - Add Foundry tests in `test/Property<Name>.t.sol`
   - Tag tests with `/// Property: theorem_name`
   - Verify with `python3 scripts/check_property_coverage.py`

## Expected File Layout

```
Contracts/<Name>/
  ├── Spec.lean        # Function specifications
  ├── Invariants.lean  # State invariants (optional)
  ├── Proofs.lean      # Re-export shim
  ├── <Name>.lean      # EDSL implementation
  └── Proofs/
        ├── Basic.lean       # Basic contract-spec correctness proofs
        └── Correctness.lean # Advanced correctness proofs
Compiler/TypedIRCompilerCorrectness.lean  # Generic compilation correctness (shared)
test/Differential<Name>.t.sol          # Differential tests
test/Property<Name>.t.sol              # Property tests
```

## Common Pitfalls

- **Storage slot mismatches** between spec, EDSL, and compiler
- **Missing canonical registration**:
  - Add the `verity_contract` declaration in `Contracts/<Name>/<Name>.lean`
  - Add `Contracts.<Name>.spec` to `Compiler.Specs.allSpecs` in `Compiler/Specs.lean`
- **Mapping conversions** not mirrored between spec and proofs
- **Property tag drift**: test tags must match lemma names exactly

## Validation Checklist

```bash
# 1. Lean code compiles
lake build

# 2. Differential tests pass
FOUNDRY_PROFILE=difftest forge test --match-contract Differential<Name>

# 3. Property tests pass
FOUNDRY_PROFILE=difftest forge test --match-contract Property<Name>

# 4. Regenerate property manifest and validate
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

# 5. Storage layout, selectors, and code hygiene
python3 scripts/check_storage_layout.py
python3 scripts/check_selectors.py
python3 scripts/check_contract_structure.py
python3 scripts/generate_verification_status.py --check
python3 scripts/check_axioms.py
python3 scripts/check_lean_hygiene.py
```

**Reference**: See [SimpleStorage](/examples#simplestorage) for a minimal end-to-end example.

**Need external libraries?** If your contract uses cryptographic primitives or other Yul functions, see [Linking External Libraries](/guides/linking-libraries) for the `--link` workflow. `CryptoHash` is a working end-to-end example.

## See also

- [Adding Your First Contract](/first-contract), step-by-step tutorial with TipJar
- [Solidity to Verity Translation](/guides/solidity-to-verity), direct mappings and translation workflow
- [Production Solidity Patterns](/guides/production-solidity-patterns), reusable surfaces and oracle/spec-boundary guidance
- [Linking External Libraries](/guides/linking-libraries), if your contract uses Yul library functions
- [Proof Debugging Handbook](/guides/debugging-proofs), when proofs get stuck