操作式证明工程

前几节介绍了两种证明方式：前向证明从已有定理构造新定理，而后向证明通过目标树分解给定的待证目标。两者的基本思路都是声明式的：用户先给出目标，如一条定理或一个后置状态，再论证这一目标成立。

本部分将介绍第三种风格：操作式证明。这也是 C* 证明在日常验证中最常用的风格。

两种风格有相同的基础：每一次状态变化最终都有经内核检查的蕴含定理作为依据。区别在于用户需要写什么：声明式步骤要写出完整的结果，未改变的内容也要全部重复写出；操作式步骤只需说明意图（如“展开 pp 处的链表”），由证明库实例化结果、保留未改动的框架，并构造定理。

有证明的视图转换介绍本部分的基础：同一块具体内存可以有多个分离逻辑视图，每一次视图变化都有蕴含定理作为依据，而声明式与操作式风格的区别只在于目标视图的来源。该节还介绍提升机制与证明库提供的通用状态变换函数。通过提升机制，小足迹蕴含可以作用于完整的符号状态。

操作的声明与应用介绍操作框架本身：如何用消耗/产出模式声明一个可复用的操作，并在声明时卸除其证明义务；模式如何从当前状态中选择资源；一次操作应用又如何生成一条关于完整状态的定理，并将其提交到状态中。该节以链表原地反转为例，展示一个完全采用操作式风格的证明。

证明-规约-实现胶囊展示操作式风格为证明工程带来的好处。该节介绍如何将一个实现片段、它的规约以及连接二者的证明封装为一个可复用、经独立验证的 C 函数，并说明这种方式为何比那些仍须信任内部实现的封装准则提供更强的保证。