acorn-prover

# Acorn Prover

## Setup (MUST DO WHEN RUNNING FIRST TIME)

If `config.env` does not exist in the skill directory:

1. **Ask the user** for the following paths:
   - `ACORN_LIB` - Path to acornlib (e.g., `/path/to/acornprover/acornlib`)
   - `ACORN_PROJECT` - Path to project directory for `.ac` files (e.g., `/path/to/acorn-playground`)

2. **Verify** the paths exist using `list_dir` or equivalent. If a path is invalid, inform the user and ask again.

3. **Run setup.sh** with the validated paths:

```bash
bash skills/acorn-prover/scripts/setup.sh "<ACORN_LIB>" "<ACORN_PROJECT>"
```

4. **Source the config** to get `ACORN_LIB`, `ACORN_PROJECT`, and `USE_MISE` variables:

```bash
source skills/acorn-prover/config.env
```

If any of the above are blank / not set, inform the user to set the variable manually.
If any of the above are changed, ask the user for new paths and run setup again.

## Configuration

Config values are stored in `skills/acorn-prover/config.env`:

| Variable        | Description                     |
| --------------- | ------------------------------- |
| `ACORN_LIB`     | Path to acornlib                |
| `ACORN_PROJECT` | Project directory for .ac files |
| `USE_MISE`      | `true` if mise is available     |

## Verify Proofs

If `USE_MISE=true`:

```bash
mise run acorn verify <filename>.ac
```

Otherwise, use the direct CLI:

```bash
acorn --lib "$ACORN_LIB" verify <filename>.ac
```

## Reverify Proofs (CI/CD)

Check that all proofs are cached with no AI searches required:

```bash
# With mise
mise run acorn reverify

# Or direct CLI
acorn --lib "$ACORN_LIB" reverify
```

Use for CI pipelines to ensure all proofs are complete.

## Training Data Generation

Generate training data (problem-proof pairs) for AI model development:

```bash
# With mise
mise run acorn training ./training_data

# Or direct CLI
acorn --lib "$ACORN_LIB" training ./training_data
```

Argument: `DIR` - Directory to output training data.

## Documentation Generation

Genera...