acorn-prover
使用 Acorn 定理证明器验证并编写数学和密码形式化证明。在使用 Acorn 证明文件 (.ac)、验证定理、形式化数学或加密协议或用 Acorn 语言编写证明时使用。触发条件：(1) 创建或编辑 .ac 文件，(2) 运行 acorn verify 命令，(3) 形式化数学或加密证明，(4) 有关 Acorn 语法或标准库的问题。
安装 / 下载方式
TotalClaw CLI推荐
totalclaw skills install shop:totalclaw:totalclaw~flyingnobita-acorn-provercURL直接下载，无需登录
curl -fsSL https://skills.taituai.com/api/skills/totalclaw%3Atotalclaw~flyingnobita-acorn-prover/file -o flyingnobita-acorn-prover.md# 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
---
## 中文说明
# Acorn Prover
## 设置（首次运行时必须执行）
如果技能目录中不存在 `config.env`：
1. **询问用户**以下路径：
- `ACORN_LIB` - acornlib 的路径（例如 `/path/to/acornprover/acornlib`）
- `ACORN_PROJECT` - 用于 `.ac` 文件的项目目录路径（例如 `/path/to/acorn-playground`）
2. **使用 `list_dir` 或等效命令验证**路径是否存在。如果路径无效，请告知用户并再次询问。
3. **使用已验证的路径运行 setup.sh**：
```bash
bash skills/acorn-prover/scripts/setup.sh "<ACORN_LIB>" "<ACORN_PROJECT>"
```
4. **加载配置（source）**以获取 `ACORN_LIB`、`ACORN_PROJECT` 和 `USE_MISE` 变量：
```bash
source skills/acorn-prover/config.env
```
如果上述任何项为空 / 未设置，请告知用户手动设置该变量。
如果上述任何项发生更改，请向用户询问新路径并重新运行设置。
## 配置
配置值存储在 `skills/acorn-prover/config.env` 中：
| Variable | 说明 |
| --------------- | ------------------------------- |
| `ACORN_LIB` | acornlib 的路径 |
| `ACORN_PROJECT` | .ac 文件的项目目录 |
| `USE_MISE` | 如果 mise 可用则为 `true` |
## 验证证明
如果 `USE_MISE=true`：
```bash
mise run acorn verify <filename>.ac
```
否则，使用直接 CLI：
```bash
acorn --lib "$ACORN_LIB" verify <filename>.ac
```
## 重新验证证明 (CI/CD)
检查所有证明是否已缓存且无需 AI 搜索：
```bash
# With mise
mise run acorn reverify
# Or direct CLI
acorn --lib "$ACORN_LIB" reverify
```
用于 CI 流水线，以确保所有证明都已完成。
## 训练数据生成
为 AI 模型开发生成训练数据（问题-证明对）：
```bash
# With mise
mise run acorn training ./training_data
# Or direct CLI
acorn --lib "$ACORN_LIB" training ./training_data
```
参数：`DIR` - 输出训练数据的目录。
## 文档生成
生成库参考文档：
```bash
# With mise
mise run acorn docs ./docs/library
# Or direct CLI
acorn --lib "$ACORN_LIB" docs ./docs/library
```
参数：`DIR` - 输出文档的目录。
## 工作流程
1. 加载配置：`source skills/acorn-prover/config.env`
2. 在 `$ACORN_PROJECT/` 中编写证明文件
3. 运行相应的命令（verify、reverify、training、docs）
4. **始终向用户显示完整的命令输出**（无论成功还是出错）
5. 使用 [references/syntax.md](references/syntax.md) 中的常见错误表来调试错误
6. 迭代直到验证通过
## 快速语法概览
```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 }
```
要点：
- 内置逻辑关键字（`not`、`and`、`or`、`implies`、`iff`、`true`、`false`）是保留字 - 不要重新定义
- 构造器名称必须为小写
- 类型类公理使用命名块，而非 `axiom` 关键字
## 标准库 (`acornlib`)
`$ACORN_LIB/src` 中的关键模块：
| Module | 内容 |
| ------------------- | ------------------------------------------ |
| `nat/` | 自然数公理、归纳法、加法 |
| `add_group.ac` | 带 `a + -a = A.0` 的 `AddGroup` |
| `add_comm_group.ac` | 阿贝尔群（`AddCommGroup`） |
## 参考资料
- **完整语法、错误表、示例**：参见 [references/syntax.md](references/syntax.md)
- **Context7 文档**：使用 `context7` MCP 配合 `/acornprover/acorn` 或 `/acornprover/acornlib` 获取最新文档