两年前我第一次接触操作系统形式化验证时导师递给我一个任务验证一个迷你调度器的就绪队列性质。我当时的反应和大多数人一样——队列不就是个列表嘛往里塞任务再取出来这个有什么好证的结果真上手才发现光是把“加入任务后再拿出任务队列能恢复原样”写成定理就够我折腾大半天。问题全出在列表和集合这些最底层的数据结构上递归归纳的边界、空与非空的分支、去重与顺序之间的微妙关系每一条都在考验你对逻辑表达式的掌控力。这个系列的第二篇我决定把HOL列表与集合的玩法从头到尾认真捋一遍把我踩过的坑、验证过的套路和可直接照抄的证明模式都放出来。无论你是正在学HOL4的学生还是想给系统代码加一层形式化保障的工程师这篇文章都能帮你少走弯路。1. 为什么操作系统验证绕不开列表和集合1.1 从“就绪队列验证”这个需求说起说到操作系统内核里的数据结构列表和集合几乎无处不在。就绪队列是列表进程集合是集合页框分配状态是集合设备链表是列表打开文件表可能是列表加集合的组合。形式化验证要做的第一步就是把运行时的数据结构“翻译”成定理证明器里的逻辑对象然后对这个对象证明不变量。以就绪队列为例。一个最朴素的需求是把一个进程加入就绪队列它就应该出现在队列的末尾把它从队首取出来调度其余进程的相对顺序不能变。用HOL的列表建模时“进程在队列里”这个命题天然对应列表的成员关系而“调度后队列恢复现场”则对应列表在入队和出队操作下的等式关系。这种建模方式直接、自然但真正动手证明时你会发现列表的每个操作都对应一堆归纳情况和case分析普通程序里一个循环就搞定的事在定理证明器里可能要拆分出三四个子目标。集合在操作系统验证中的角色同样关键。比如页框分配器要维护“已分配页框集合”和“空闲页框集合”这两者必须是不相交的且它们的并集等于全部可用页框。如果你用列表模拟集合就得额外处理重复元素和顺序问题白白增加证明负担。HOL里集合的本质是谓词x IN s本质上就是s x集合的运算也被翻译成逻辑连接词。这个设计让“两个集合相等”变成了“两个谓词等价”证起来比列表的等式更干净。所以结论很直接列表负责“有顺序的排列”集合负责“无顺序的归属”。操作系统里两类需求都有两种数据结构都要会。这就是这个系列教程选了HOL列表与集合作为第二篇的原因。1.2 HOL里的列表和集合与普通语言有什么不同第一次用HOL的人特别容易栽在一个思维惯性上把普通编程语言里的“列表”和“集合”概念原封不动搬进来。这在思想的起点上就走偏了。普通语言里列表就是一个运行时数据结构你关心的是它的内存布局和操作复杂度。HOL里的列表是一种归纳定义的代数数据类型你的任务不是“调用它的方法”而是“证明它的性质”。普通语言里集合通常是一个哈希表或者树你关心的是插入和查找的速度。HOL里的集合是逻辑谓词你操作的是逻辑蕴含、合取、析取。换句话说HOL列表与集合不是给你“用的工具”而是给你“证明的对象”。这种差异最直接的影响体现在证明风格上。普通代码出bug你会调试、打日志、看堆栈HOL证明出问题你会展开定义、选择归纳变量、构造存在性实例然后看着子目标一层层化简。刚开始可能很不习惯但你适应了之后会发现恰恰是这种“一切都可展开、一切都可检查”的机制给了你在普通测试里拿不到的信心——当一条定理在HOL4里证明通过它就不只是在几个测试用例上成立而是在所有可能的输入上都成立。2. HOL中列表的定义与常用武器2.1 列表的递归构造Nil 与 ConsHOL里列表的定义非常经典本质就是两个构造子的递归数据类型datatype a list [] | :: (a, a list)注意这里的[]是空列表构造子::是中缀形式的“头部加尾部”构造子。[1;2;3]实际上就是1 :: 2 :: 3 :: []的语法糖。我刚开始用的时候总觉得这个定义简单到不值得关注但后来才意识到这个递归结构是列表所有性质的根源。因为列表是递归定义的你定义在列表上的函数几乎全都是递归函数。比如求长度LENGTH(LENGTH [] 0) ∧ (LENGTH (h :: t) 1 LENGTH t)比如拼接APPENDHOL里也写作(APPEND [] l l) ∧ (APPEND (h :: t) l h :: APPEND t l)这些定义遵循同一种模式先给空列表的情况再给非空列表的情况而非空情况中递归调用作用在尾部t上。只要你能写出这种递归定义HOL就会自动为你生成对应的归纳定理这就是我接下来要说的核心武器。2.2 必背的高频列表定理用HOL证明关于列表的性质绕不开下面这几个定理。我把它们整理成一张表按频率从高到低排列每个都标注了典型使用场景定理名称定理内容简化表述典型场景LIST_INDUCT对尾部归纳P []且P t P (h::t)几乎所有列表性质证明的起点LENGTH_NILLENGTH l 0 l []判空、边界条件化简LENGTH_APPENDLENGTH (APPEND l1 l2) LENGTH l1 LENGTH l2拼接操作的长度分析MEM_APPENDx MEM (APPEND l1 l2) x MEM l1 ∨ x MEM l2元素归属性的拆分MAP_APPENDMAP f (APPEND l1 l2) APPEND (MAP f l1) (MAP f l2)映射与拼接的交换律FILTER_APPENDFILTER P (APPEND l1 l2) APPEND (FILTER P l1) (FILTER P l2)过滤与拼接的交换律APPEND_EQ_NILAPPEND l1 l2 [] l1 [] ∧ l2 []判断拼接结果为空这几个定理不是我瞎列的而是我在证明调度器、文件系统元数据时反复用到的“基础弹药”。它们的共同特点是把复杂操作拆成简单操作的组合把关于结构的情报转化为关于逻辑的情报。特别提一下MEM——它表示“元素出现在列表中”。在操作系统的场景里x MEM run_queue可以读作“进程x在就绪队列中”这个命题再配合列表操作就能描述几乎所有队列不变量的基础形式。2.3 列表归纳法实操证明 LENGTH_APPEND理论说再多不如实际手推一遍。我现在带你亲手证明LENGTH_APPEND这是列表证明的“Hello World”但里面包含的技法可以复用到大多数场景。要证的定理是∀ l1 l2. LENGTH (APPEND l1 l2) LENGTH l1 LENGTH l2第一次看到这个定理很容易想当然地对l2做归纳或者对两个参数同时归纳。正确做法是对l1归纳因为APPEND的递归定义是围绕第一个参数展开的。方法如下第一步对l1使用LIST_INDUCT归纳会分成两个子目标。空列表子目标LENGTH (APPEND [] l2) LENGTH [] LENGTH l2用APPEND的定义直接把左边化成LENGTH l2再用LENGTH的空列表定义把右边的LENGTH []化成0最后用算术化简收掉。这里我习惯用simp [APPEND, LENGTH]一条命令搞定但新手建议先用rewrite或fs逐条展开看清每一步发生了什么。非空列表子目标是整个证明的关键LENGTH t 1 ? 假设 LENGTH (APPEND t l2) LENGTH t LENGTH l2具体展开后左边会用APPEND的h::t分支变成LENGTH (h :: APPEND t l2)再用LENGTH的定义变成1 LENGTH (APPEND t l2)。此时必须代入归纳假设LENGTH (APPEND t l2) LENGTH t LENGTH l2右边LENGTH (h::t) LENGTH l2变成1 LENGTH t LENGTH l2。两边一化简等式平凡成立。这里有个很多新手栽过的坑如果你对l2做归纳APPEND的定义不会自动拆开第一个参数的 head 和 tail整个证明会卡死在“APPEND t l2”这种无法化简的形式上。所以记住一条经验归纳变量必须选递归定义中参与递归的那个参数。3. HOL中的集合本质与推理套路3.1 集合的本质是谓词HOL里的集合本质上就是一个返回布尔值的函数。s是一个集合x IN s在底层就是s x。整个集合理论建立在这个简单的洞察上一个集合就是描述“哪些元素属于它”的谓词。这个设计带来两个直接好处。第一集合的运算可以直接用逻辑连接词定义。比如并集s1 ∪ s2 λx. x IN s1 ∨ x IN s2交集s1 ∩ s2 λx. x IN s1 ∧ x IN s2第二证明集合相等用的不再是“两个容器内容一样”这种运行时直觉而是外延性公理两个集合相等当且仅当它们的每一个元素归属都等价。换句话说你要证s1 s2只需证∀x. x IN s1 ⇔ x IN s2。这个套路在HOL中有一个专门的引理我用SET_EQ或者EXTENSION来触发它。3.2 常用集合运算与推理套路集合推理在HOL里很少需要你从零开始大部分工作就是“展开定义再加上逻辑推理”。我按使用频率整理一下常用武器UNION_COMM / UNION_ASSOC并集的交换律和结合律在处理多个集合合并时是主力。INTER_COMM / INTER_ASSOC交集的交换律和结合律。SUBSET_ANTISYM两个方向都有子集关系就得到集合相等是证明集合相等的常规路线。IN_UNIONx IN s1 ∪ s2 ⇔ x IN s1 ∨ x IN s2遇到member命题第一时间展开它。DELETE_INSERT、INSERT_DELETE集合的插入和删除操作之间的关系在建模页框分配这类场景时特别常用。实际证明中的套路一般是先做集合外延展开得到∀x. x IN A ⇔ x IN B然后用EQ_TAC把双向蕴含拆成两个方向每个方向再根据具体的IN定义做逻辑推理。以并集结合律为例证明s1 ∪ (s2 ∪ s3) (s1 ∪ s2) ∪ s3时外延展开之后你面对的是纯命题逻辑的等价式子。这种证明完全可以用metis_tac或者其他自动化策略暴力收官但为了锻炼手感我建议新手手动走一遍先展开三次IN_UNION把IN的析取结构全部暴露出来再用命题逻辑的结合律合并。手工走通之后你会发现集合证明的套路就这么简单——集合运算是壳逻辑运算才是核。3.3 FINITE 与无穷集合的边界集合推理里有一个操作系统验证绕不开的概念有限性。因为内核里的集合几乎都是有限集合而很多证明技巧需要“集合有限”作为前提。HOL对FINITE的定义是归纳式的空集有限往有限集里插入一个新元素得到的集合仍然有限。这条定义链得到了一个重要结论任何有限集都可以被转换成一个列表。实际使用中FINITE_LIST_TO_SET保证任何列表转成的集合都有限反过来SET_TO_LIST可以从有限集中构造出一个列表。我做文件系统链接计数验证时就吃过“忘记证明有限性”的亏。当时想对一个已分配页框集合做遍历求和直接调用一个依赖列表表示的工具函数结果证明卡住。后来才发现那个工具函数的前提条件里要求集合必须是FINITE的而我完全没提供这个前提。从那以后我养成了一个习惯建模阶段就提前确认每个集合操作的有限性要求能证明的在定义时就当附带给出来。4. 列表与集合联合作战一个系统验证小案例4.1 建模模拟调度器与页框分配集合前面铺了这么多现在来看一个综合案例。我基于模拟项目X做了一套极简内核模型核心是两个部分就绪队列用列表建模已分配页框用集合建模。先看数据结构定义(* 就绪队列进程ID列表 *) Definition run_queue_def: run_queue [] : num list End (* 入队把任务追加到队尾 *) Definition enqueue_def: enqueue q task APPEND q [task] End (* 出队取队首返回原队列去掉队首 *) Definition dequeue_def: dequeue [] NONE ∧ dequeue (h::t) SOME (h, t) End (* 从队列提取进程集合 *) Definition process_set_def: process_set q LIST_TO_SET q End (* 已分配页框集合 *) Definition alloc_def: allocated_frames : num set {} End注意process_set_def这一条它把列表和集合连接了起来。LIST_TO_SET会把列表里的元素收集成集合自动去重。这正是操作系统场景所需要的队列里进程出现两次可能是个bug但集合视角下你关心的只是“这个进程是否在某处存在”。4.2 验证“入队后进程集合恰好扩张一个元素”我要验证的第一个核心性质是把一个进程加入就绪队列后进程集合等于原集合与“新进程”的并集。定理陈述如下∀q task. process_set (enqueue q task) process_set q ∪ {task}这个定理听起来很直观但证明过程能体现列表和集合配合的标准套路。我用rw [enqueue_def, process_set_def]把定义全部展开目标变成LIST_TO_SET (APPEND q [task]) LIST_TO_SET q ∪ {task}接着调用列表与集合互转的核心引理LIST_TO_SET_APPENDLIST_TO_SET (APPEND q [task]) LIST_TO_SET q ∪ LIST_TO_SET [task]右边化为LIST_TO_SET q ∪ {task}正好为目标。整个证明最微妙的地方在于LIST_TO_SET的去重行为如果task已经在q里左边的集合并不会多出一个元素右边的并集同样不会多出元素。这个“去重一致性”在逻辑上自动成立不需要单独证明。我第一次推到这里还有点半信半疑后来专门验证了一遍task已在列表中的情况确认两边的确都等于原集合这才放心。第二个要验证的性质跟出队相关出队不会把任何进程从集合中凭空变出来。具体来说如果dequeue q SOME (h, t)那么process_set t ⊆ process_set q。这个定理的价值在于它保证了调度器取出队首后剩下的进程仍然属于原有进程集合不会出现“进程消失”这种不变量破坏。证明方法是对q做Cases_on分空和非空两种情况然后展开dequeue_def和process_set_def用列表的MEM与集合归属的转换关系收尾。4.3 这个案例对操作系统验证的扩展思路我在模拟项目X里验证完这两个性质后最大的感受是列表与集合的组合是系统验证的基本功它们能覆盖的远不止调度器。你可以把run_queue换成“打开文件表”把process_set换成“已打开文件描述符集合”模式完全一样。更关键的是这套建模思路可以往上叠加不变量。比如“所有在就绪队列里的进程都处于就绪状态”这需要集合ready_state_set与process_set q的子集关系比如“已分配页框集合与空闲页框集合互不相交”这需要交集为空的集合论证。而这些不变量最后都会化约为本文前面讲的列表和集合的基础定理。基础不牢上层根本走不动。5. 常见问题与排查实录5.1 最常翻车的五个点我在HOL列表与集合的实践中见过太多人包括我自己反复踩同样几个坑。这里挑五个最典型的每一个都附上现场描述和解决思路。第一个坑归纳变量选错。证明关于APPEND的性质时选了第二个列表做归纳导致递归定义无法展开整个证明卡死在原地。解决方法前面说过观察递归定义里哪个参数在递归就选哪个参数做归纳。还有个通用判断标准如果归纳到一半发现子目标里的结构无法用定义化简多半是归纳变量选错了。第二个坑集合外延展开后方向搞反。用SET_EQ展开集合相等后两个方向的蕴含有时会让人觉得两边长得一样但如果你在展开之前没有正确定义集合运算的优先级很容易出现x ∈ A ∨ x ∈ B和x ∈ B ∨ x ∈ A这种表面上看起来不同、实际上等价的式子。解决方法是先fs []把集合运算全部展开成逻辑公式再用taut_tac或者prove_tac做纯命题逻辑的收尾。第三个坑FULL_SIMP_TAC把公式炸了。有些集合定义展开后会产生大量连接词如果直接full_simp_tac轻则目标变成一坨不可读的命题逻辑公式重则证明器内存暴涨。我的习惯是分步化简先用simp []只展开必要的定义再用较小的规则集合做定点化简最后才考虑用全量简化。第四个坑EXISTS_TAC找错存在性实例。集合证明里经常需要“构造一个元素证明属于某个集合”这时如果选错了 witness后续子目标可能根本走不通。比如证明∃x. x ∈ s直接挑s里的任意元素不一定行因为你还得先证明它有某个性质。实践经验是在选 witness 之前先把目标化简到最简形式看清到底需要什么类型的元素。第五个坑忽略有限性前提。前面已经讲过当目标要求遍历集合时哪怕只差一个FINITE s前提证明也会卡住。我现在的做法是在建模阶段就给每个集合加上有限性引理并尽量把“有限性”放进不变量里一起证明。5.2 调试技巧速查HOL列表与集合的调试核心是“看清楚证明器在做的事”。我给你几个亲测有效的速查技巧症状常用排查方法推荐策略目标卡在中间化简不了用-配合simp定向展开指定定义检查递归定义参数选择是否正确证明器运行太久不退出查看当前目标是否变成巨大命题公式避免过早全量展开用控定义展开定理在最后一步过不去用print_tac xxx标记位置打印中间目标定位具体是哪个子目标失败集合相等证不出来检查是否漏了FINITE前提先单独证明有限性再合并进主定理想套用某个现成引理却用不上用db搜索相关引理名搜索可用的引理库另外一个我特别想分享的心得HOL4的证明脚本不要一次性写很长。我用g开目标用e逐条执行策略每执行完一步就停下来看看当前目标变成了什么。这样虽然看起来慢但能防止大方向走偏后整个脚本全部报废。等到每一步都确认无误再把这些e串成完整的prove或store_thm效率反而高出一大截。调试时还有一个容易被忽略的工具类型打印。如果目标里出现大幅变量分不清哪个是列表的h、哪个是集合的s可以在脚本开头开启类型显示让所有变量带上类型注解。这个习惯帮我省了不少脑力。最后分享一个小技巧证明列表与集合结合的性质时提前把LIST_TO_SET_APPEND、MEM_LIST_TO_SET这类桥梁引理准备好。它们会在证明中反复出现与其每次都现场展开一遍不如先作为本地引理prove好放一边后面用fs一个接一个用。我在模拟项目X里几乎每三个证明就会用到一次这类桥梁引理。现在一看到LIST_TO_SET出现在目标里我第一反应不是展开它而是搜索有没有现成的互转定理可以直接用。这个思路的转变是HOL列表与集合从入门到上手的真正的分水岭。