C*：开发与证明一体化

用 cstar_mcp 进行 AI 辅助验证

EN | 中文

前两节把证明的两半自动化了：策略负责匹配并消去空间资源，SMT 求解器负责解决剩下的纯目标。 它们决定不了的，是第一个证明块之前的一切——数据的逻辑模型、谓词族、循环不变式、填补缺口的那条引理。 在本教程中，这些判断一直出自在 VSCode 里阅读符号状态的人。 cstar_mcpcstar_mcp 把同一条回路交给 AI 助手。 它通过 MCP（Model Context Protocol，即 AI 助手调用外部工具所用的接口）开放验证器，让助手能够查看某一行的符号状态、搜索定理数据库、编辑证明块，再重新查验。

配置

服务器随工具链一起发布，位于 ~/.cstar/bin/cstar_mcp~/.cstar/bin/cstar_mcp。 无论使用哪种助手，都按下面这些参数在 MCP 客户端中注册它：

  • 传输方式：标准输入输出（由客户端启动的本地进程）；
  • 命令：二进制文件的绝对路径 /Users/you/.cstar/bin/cstar_mcp/Users/you/.cstar/bin/cstar_mcp，因为配置不经 shell 读取，~~ 不会被展开；
  • 参数：无；
  • 环境变量：不需要；CSTAR_MCP_MAX_STACKSCSTAR_MCP_MAX_STACKS 可以提高常驻文件的数量（默认三个）。

工具

连接到服务器的助手可以看到六个工具。

工具 作用
cstar_showlspcstar_showlsp {path, line}{path, line}：某一源码行处的验证状态，即该行执行之后的状态。在函数内部，回复带有 symbolic_statesymbolic_state 与作用域内的幽灵变量；在文件作用域（从函数的右花括号起），回复带有截至该行累积的 vcvc。lines: [...]lines: [...] 一次查询同一文件的多行，scopesscopes 则裁剪幽灵变量的转储。
search_theoremssearch_theorems {pattern, limit?}{pattern, limit?}：对具名 HOL Light 定理（含定理语句）做正则搜索；名字完全匹配的排在最前
search_conversionssearch_conversions {pattern, limit?}{pattern, limit?}：对具名变换做同样的搜索
cstar_helpcstar_help {topic?}{topic?}：证明工作流指南，或其中的某个参考主题（syntaxsyntax、contractscontracts、memorymemory、predicatespredicates、loopsloops、bitopsbitops、aritharith、projectproject、techniquetechnique、operationsoperations、apiapi、errorserrors）
cstar_killlspcstar_killlsp {path?}{path?}：在内部故障之后，拆除某个文件的证明器与常驻守护进程，或全部拆除
cstar_interruptcstar_interrupt {}{}：中止一个挂起的证明器请求；证明器本身继续存活

cstar_showlspcstar_showlsp 即 Show Symbolic StateShow Symbolic State 的 MCP 形态，寻址规则与 VSCode 命令相同：函数内的行显示该行之后的状态，文件作用域的行携带截至该处收集到的验证报告，所以只有在文件真正的最后一行查询、且 verification_conditionsverification_conditions、axiomsaxioms 与 strategiesstrategies 都为空时，文件才算通过验证。 对一个文件的第一次查询比较慢，因为要启动该文件的证明器并构建常驻守护进程；之后对同一文件的查询很快返回，守护进程也会自动跟进修改。 默认最多三个文件同时保持常驻（环境变量 CSTAR_MCP_MAX_STACKSCSTAR_MCP_MAX_STACKS 可以提高上限），各有各的证明器，因此在文件之间切换没有代价；查询第四个文件时会淘汰最久未用的那个，回复中会以 notenote 说明。

助手所执行的回路

cstar_helpcstar_help 提供的指南写明了一套工作流，也正是本教程一路手工执行的那一套：

  1. 先做设计——数据的逻辑模型、谓词族、把递归的界写进后置条件的诚实契约、折叠与展开引理——然后才写代码与证明块；
  2. 每写完一个函数就查询它的右花括号，逐个验证；
  3. 失败时，查询证明块前后的可执行行，阅读状态；
  4. 在定理与变换数据库中搜索能填补缺口的东西；
  5. 编辑证明块，再次查询，这时已经是热态；
  6. 最后在文件的最后一行查询，三个列表都必须为空。

一次关于 twicetwice 的会话

取C* 中的前向证明里的 twicetwice 函数，存为一个独立项目中的 twice.ctwice.c；第 12 行是 int r = a + b;int r = a + b;，第 27 行是函数的右花括号。 下面是三次调用，助手发出的请求与服务器的回复（长值已截短；路径用绝对路径，或者相对于服务器启动时所在的目录）：

cstar_showlsp {"path": "twice.c", "line": 12, "scopes": "none"}
{
  "flag": true,
  "lsp": {
    "function": "twice",
    "line": 12,
    "symbolic_state": "fact (0i <= n__pre) ** fact (n__pre <= 100i) **
      data_at r__addr Tint ((n__pre + 1i) + n__pre - 1i) **
      data_at b__addr Tint (n__pre - 1i) **
      data_at a__addr Tint (n__pre + 1i) **
      data_at n__addr Tint n__pre",
    …
  }
}
cstar_showlsp {"path": "twice.c", "line": 12, "scopes": "none"}
{
  "flag": true,
  "lsp": {
    "function": "twice",
    "line": 12,
    "symbolic_state": "fact (0i <= n__pre) ** fact (n__pre <= 100i) **
      data_at r__addr Tint ((n__pre + 1i) + n__pre - 1i) **
      data_at b__addr Tint (n__pre - 1i) **
      data_at a__addr Tint (n__pre + 1i) **
      data_at n__addr Tint n__pre",
    …
  }
}

这正是 VSCode 面板在该行显示的状态，rr 单元里放着尚未化简的和。 在最后一行查询，返回的则是验证报告；因为两个证明块都已就位，三个列表都为空：

cstar_showlsp {"path": "twice.c", "line": 27, "scopes": "none"}
{
  "flag": true,
  "lsp": {
    "line": 27,
    "vc": { "axioms": [], "strategies": [], "verification_conditions": [] },
    …
  }
}
cstar_showlsp {"path": "twice.c", "line": 27, "scopes": "none"}
{
  "flag": true,
  "lsp": {
    "line": 27,
    "vc": { "axioms": [], "strategies": [], "verification_conditions": [] },
    …
  }
}

搜索返回名字与定理语句，采用打印器的记号：

search_theorems {"pattern": "REVERSE_APPEND", "limit": 2}
[
  {
    "name": "REVERSE_APPEND",
    "statement": "|- forall l m. REVERSE (l ++ m) == REVERSE m ++ REVERSE l"
  }
]
search_theorems {"pattern": "REVERSE_APPEND", "limit": 2}
[
  {
    "name": "REVERSE_APPEND",
    "statement": "|- forall l m. REVERSE (l ++ m) == REVERSE m ++ REVERSE l"
  }
]

查询失败时，回复带有 flag: falseflag: false 和一个 diagnosticsdiagnostics 数组，每个栈帧一项——文件、行、列，以及编译器或引擎的消息（含失败的语句，以及符号状态，如果有的话）——与人在 VSCode 面板里读到的报告相同。

小结

  • cstar_mcpcstar_mcp 通过 MCP 把验证器开放给 AI 助手：它随 ~/.cstar/bin~/.cstar/bin 发布，以标准输入输出服务器的形式、用绝对路径且不带参数在客户端注册，并为每个文件各自启动一个证明器。
  • 六个工具：cstar_showlspcstar_showlsp（某一行的符号状态，或文件作用域处的验证报告）、search_theoremssearch_theorems 与 search_conversionssearch_conversions、cstar_helpcstar_help（指南及其主题），以及用于恢复的 cstar_killlspcstar_killlsp 与 cstar_interruptcstar_interrupt。
  • 工作流就是本教程的工作流——先做设计、查询右花括号、阅读失败前后的状态、搜索、编辑、再查询——而“通过验证”指的是在文件真正的最后一行 verification_conditionsverification_conditions、axiomsaxioms 与 strategiesstrategies 都为空。