操作式证明工程

前几节介绍了两种证明方式：前向证明从已有定理构造新定理，而后向证明通过目标树分解一个给定的待证目标。 两者在本质上都是声明式的：用户陈述目标——一条定理、一个后置状态——然后为其给出论证。

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

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

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

操作的声明与应用打开操作框架本身：可复用的操作如何声明为一份消耗/产出模式、其证明义务如何在声明时卸除，模式如何从当前状态中选择资源，一次应用又如何变为一条提交到状态的完整定理——并以完全操作式的链表原地反转证明作为演示。

证明-规约-实现胶囊是操作式风格在证明工程上的收益。 该节展示了如何将一个实现片段、其规约，以及连接二者的证明，打包成一个可复用、独立验证的 C 函数——以及为什么这比那些必须信任内部实现的封装准则提供更强的保证。