# CVL Property Generator

This repository contains a set of Python scripts that automatically generate CVL (Certora Verification Language) specifications for Solidity smart contracts. The tool analyzes smart contracts and automatically generates formal verification properties and corresponding CVL rules.

## Requirements

- Python 3.11+
- Solidity compiler (`solc`)
- Python dependencies (see `requirements.txt`)
- Claude API key (saved to an environment variable named `ANTHROPIC_API_KEY`)

## Installation

1. Install Python dependencies:

    ```bash
    pip install -r requirements.txt
    ```

## Overview

The CVL Generator consists of three main scripts:

1. **`scripts/auto_generate_cvl.py`** - Main orchestrator script that coordinates the entire process
2. **`scripts/auto_generate_properties.py`** - Generates natural language properties for contracts and functions
3. **`scripts/properties_to_cvl.py`** - Converts natural language properties into formal CVL specifications

## Quick Start

To generate CVL specifications for your smart contract:

```bash
./scripts/auto_generate_cvl.py \
  --contract-file MyContract.sol \
  --contract MyContract \
  --solc solc \
  --out verification.spec
```

## Script Details

### `scripts/auto_generate_cvl.py` (Main Script)

The primary script that orchestrates the entire CVL generation process. It automatically calls the other two scripts in sequence.

**Usage:**

```bash
./scripts/auto_generate_cvl.py [OPTIONS]
```

**Required Arguments:**

- `--contract-file PATH` - Path to the Solidity contract file
- `--contract STRING` - Name of the contract to analyze

**Optional Arguments:**

- `--solc STRING` - Path to the Solidity compiler (default: "solc")
- `--remappings STRING [STRING ...]` - Solidity import remappings (e.g., "@openzeppelin/=lib/openzeppelin/")
  - Note that if a `remappings.txt` file exists in the cwd, it will be used automatically
- `--via-ir` - Enable compilation via IR (intermediate representation)
- `--n-concurrent INT` - Number of concurrent property generation requests (default: 5)
- `--cvl-imports STRING [STRING ...]` - CVL files to import in the generated specification
- `--out PATH` - Output file for the generated CVL specification (default: "nat.spec")
- `--properties-dir PATH` - Directory to store intermediate property files (default: auto-generated timestamp)
- `--methods METHOD [METHOD ...]` - List of methods such that properties will be generated only for them. If empty then properties will be generated for all methods in the contracts
- `--generate-invariants` - Generate (also) contract-level invariants
- `--extra_info PATH [PATH ...]` - List of files with additional information about the contract/methods (e.g. design docs)
- `--no-validate` - Disable self-validation of the properties (whether they can be translated to CVL).

**Token Optimization Flags:**

- `--optimizations OPT1,OPT2,...` - Comma-separated list of token optimizations to enable
  - Available optimizations: `exclude-libs`, `compact`, `summarize`
  - Default: `exclude-libs,compact,summarize` (all enabled)
  - Use `none` to disable all optimizations
  - Examples:
    - `--optimizations compact,summarize` - Enable only compact and summarize
    - `--optimizations exclude-libs` - Enable only exclude-libs
    - `--optimizations none` - Disable all optimizations
- `--summary-file PATH` - Load pre-generated summaries from file instead of generating them

**Optimization descriptions:**
- `exclude-libs`: Filter out library code (lib/, node_modules/, etc.) from analysis
- `compact`: Remove interfaces, internal libraries, and verbose NatSpec comments
- `summarize`: Generate AI-powered function summaries and use declarations-only contract (enables prompt caching)

**Example:**

```bash
./scripts/auto_generate_cvl.py \
  --contract-file contracts/Token.sol \
  --contract ERC20Token \
  --solc /usr/local/bin/solc \
  --n-concurrent 3 \
  --cvl-imports "base.spec" "helpers.spec" \
  --out token_verification.spec \
  --methods transfer transferFrom
```

### `scripts/auto_generate_properties.py`

Analyzes smart contracts and generates natural language properties that describe expected behaviors for both individual functions and the contract as a whole.

**Usage:**

```bash
./scripts/auto_generate_properties.py [OPTIONS]
```

**Key Features:**

- Generates properties for each public/external function
- Creates contract-level invariants
- Analyzes storage variables and their relationships
- Outputs properties in JSON format with explanations

**Arguments:**

- `--contract-file STRING` - Path to the Solidity contract file
- `--contract STRING` - Name of the contract to analyze
- `--solc STRING` - Path to the Solidity compiler
- `--remappings STRING [STRING ...]` - Solidity import remappings (e.g., "@openzeppelin/=lib/openzeppelin/")
  - Note that if a `remappings.txt` file exists in the cwd, it will be used automatically
- `--via-ir` - Enable compilation via IR (intermediate representation)
- `--n-concurrent INT` - Number of concurrent requests
- `--properties-dir PATH` - Directory to store property files
- `--out STRING` - Output JSON file for properties
- `--methods METHOD [METHOD ...]` - List of methods such that properties will be generated only for them. If empty then properties will be generated for all methods in the contracts
- `--generate-invariants` - Generate (also) contract-level invariants
- `--extra_info PATH [PATH ...]` - List of files with additional information about the contract/methods (e.g. design docs)
- `--no-validate` - Disable self-validation of the properties (whether they can be translated to CVL).

### `scripts/properties_to_cvl.py`

Converts natural language properties into formal CVL (Certora Verification Language) specifications. This script can be used standalone if you already have properties generated.

**Usage:**

```bash
./scripts/properties_to_cvl.py [OPTIONS]
```

**Key Features:**

- Parses natural language properties using a custom grammar
- Generates type-safe CVL rules
- Handles complex Solidity types (structs, mappings, arrays)
- Supports both function-level and contract-level properties
- Automatically handles variable declarations and type inference

**Arguments:**

- `--properties-file PATH` - JSON file containing properties
- `--contract-file STRING` - Original Solidity contract file
- `--contract STRING` - Contract name
- `--solc STRING` - Solidity compiler path
- `--remappings STRING [STRING ...]` - Solidity import remappings (e.g., "@openzeppelin/=lib/openzeppelin/")
  - Note that if a `remappings.txt` file exists in the cwd, it will be used automatically
- `--via-ir` - Enable compilation via IR (intermediate representation)
- `--out STRING` - Output CVL specification file
- `--cvl-imports STRING [STRING ...]` - CVL imports to include
- `--properties-dir PATH` - Directory containing property reasoning files
- `--property PROPERTY_NAME` - only parse and translate this property. Useful for debugging

## Output Files

### Generated Properties (`properties.json`)

```json
{
  "transfer-a9059cbb": {
    "transfer amount positive": "amount > 0",
    "sender balance decrease": "msg.sender.balance@after == msg.sender.balance@before - amount"
  },
  "MyContract": {
    "monotonic nonce": "nonces[n]@before <= nonces[n]@after"
  }
}
```

### Generated CVL Specification (`.spec` file)

```cvl
import "base.spec";

/*
 * amount > 0
 *
 * What it means: The amount parameter in transfer function must be greater than zero
 * Why it should hold: Prevents meaningless zero-value transfers
 * Possible consequences: Could allow gas-wasting operations
 */
rule transfer_transfer_amount_positive_1(env e) {
    // Declare variables
    uint256 amount;
    address to;

    // call function under test
    transfer(e, to, amount);

    // verify integrity
    assert (amount > 0);
}
```

### Property Reasoning Files

For each function/contract, reasoning files (`*-reason.json`) are generated containing detailed explanations of why each property should hold and what consequences violations might have. These explanations are then embedded into the documentation of each rule.

## Advanced Usage

### Manual Property Generation

You can run the property generation step separately:

```bash
./scripts/auto_generate_properties.py \
  --contract-file MyContract.sol \
  --contract MyContract \
  --out properties.json
```

### Manual CVL Generation

If you have existing properties, generate CVL directly:

```bash
./scripts/properties_to_cvl.py \
  --properties-file properties.json \
  --contract-file MyContract.sol \
  --contract MyContract \
  --out verification.spec
```

## Error Handling

The tool provides detailed error messages for:

- Solidity compilation errors
- Type inference failures
- Property parsing errors
- CVL generation issues

Failed rules are reported separately, allowing partial specification generation even when some properties cannot be converted.
