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

Generate library reference documentation:

```bash
# With mise
mise run acorn docs ./docs/library

# Or direct CLI
acorn --lib "$ACORN_LIB" docs ./docs/library
```

Argument: `DIR` - Directory to output documentation.

## Workflow

1. Source config: `source skills/acorn-prover/config.env`
2. Write proof file in `$ACORN_PROJECT/`
3. Run the appropriate command (verify, reverify, training, docs)
4. **Always show the full command output to the user** (success or error)
5. Debug errors using the common errors table in [references/syntax.md](references/syntax.md)
6. Iterate until verification passes

## Quick Syntax Overview

```acorn
from nat import Nat
from add_comm_group import AddCommGroup

// Theorems - auto-proved or with hints
theorem example(a: Nat, b: Nat) {
    a < b implies a != b
}

// Typeclasses - axioms are named blocks, no "axiom" keyword
typeclass A: AddGroup extends Zero, Neg, Add {
    inverse_right(a: A) { a + -a = A.0 }
}

// Structures
structure Pair[T, U] { first: T  second: U }

// Inductive types - constructors MUST be lowercase
inductive MyBool { tru fls }
```

Key points:

- Built-in logic keywords (`not`, `and`, `or`, `implies`, `iff`, `true`, `false`) are reserved - do not redefine
- Constructor names must be lowercase
- Typeclass axioms use named blocks, not the `axiom` keyword

## Standard Library (`acornlib`)

Key modules in `$ACORN_LIB/src`:

| Module              | Contents                                   |
| ------------------- | ------------------------------------------ |
| `nat/`              | Natural number axioms, induction, addition |
| `add_group.ac`      | `AddGroup` with `a + -a = A.0`             |
| `add_comm_group.ac` | Abelian groups (`AddCommGroup`)            |

## References

- **Full syntax, error table, examples**: See [references/syntax.md](references/syntax.md)
- **Context7 docs**: Use `context7` MCP with `/acornprover/acorn` or `/acornprover/acornlib` for latest documentation