在形式化验证这块很多人一上来就被各种抽象符号劝退。但实际做操作系统内核的验证时你会发现真正每天都在打交道的其实是最朴素的列表和集合。上一篇文章我们把证明环境跑通梳理了HOL里的函数定义和基本推理规则这一篇就来啃这两块最基础也最关键的地基材料。不是说它们简单而是说它们的使用频率极高——从进程队列到资源分配从内存映射到中断状态几乎所有内核模型的抽象表达最后都会落到列表和集合的运算上。这篇文章的内容不会只停留在列表是什么、集合是什么这种入门层面。我会把HOL中列表和集合的底层表示方式、核心定理的证明套路、以及在操作系统建模场景里的具体用法串起来讲。比较合适的读者对象是已经跑通HOL环境、能写基本函数定义但对着list_ind、SIMP_CONV、集合外延性这些概念还犯迷糊的实践者。1. 为什么形式化验证绕不开列表与集合从内核建模讲到数据结构选型做操作系统形式化验证和写普通业务代码有一个很大的区别——你不是在编程而是在描述一个系统然后用逻辑工具去证明这个系统的某些性质。这时候数据结构的角色就有点不一样了。1.1 内核里的列表和集合比你想的更无处不在先随便想想一个简化内核里会出现哪些结构。就绪队列是一个进程控制块的列表锁的等待队列是个列表页表项的管理在某些抽象层上是个映射而中断在当前CPU上是否被屏蔽、某一组资源是否已经被分配出去这些状态天然的抽象就是集合。以最经典的就绪队列为例。在严苛的验证工作中我们不会直接拿队列的有序性、去重性这些特性开刀而是先问一个问题队列本身在逻辑语言里怎么定义对比一下如果用普通的命令式语言你可以把队列直接塞进数组、链表甚至是一个简单的向量上。但在HOL这种高阶逻辑框架里我们能选的方式很有限——因为语言本身是纯函数式的且一切皆函数。这就引出了列表和集合在验证中的真正价值它们是操作系统验证里几乎所有有限状态结构的统一载体。还有一点值得提前说HOL里的集合和我们数学课上学的集合有一点微妙的出入。数学里的集合通常被理解为一堆元素的整体但在HOL里集合本质上是一个谓词——一个从元素类型到布尔值的函数。这种谓词表示法既有好处也有坑后面专门展开。1.2 列表承担有序状态集合承担无序归属那么选型逻辑就很清楚了凡是需要体现顺序、先后、排列的都用列表。凡是只关心某个东西在不在里面、不关心顺序的都用集合。举个例子你要描述当前CPU上正在执行哪个进程用一个进程ID的变量就够了但如果你要描述就绪进程有哪些且按优先级排列这就是一个列表而如果你要描述当前系统中哪些中断是被屏蔽的集合是最自然的选择——因为中断号之间没有天然的先后语义你只是想在某个逻辑时刻断言某个中断号元素是否属于这个屏蔽集合。这听起来像常识但在实际建模时我见过不少人把顺序无关的状态误用成列表或者在需要顺序保证的场景里用了集合结果在证明过程中额外背上大量不必要的证明义务。选型错了后面的定理证明就会痛苦得多。1.3 HOL里的列表和集合不是拿来操作的而是拿来断言的还有一点要转变思维。在C/Rust里你操作列表是增删改查关心的是性能。在HOL里列表和集合更多时候是出现在性质断言里。比如queue_ok q这个谓词可能是对队列里的每个进程块做一些不变量检查irq_masked s可能是判断某个集合是否覆盖了某些关键中断号。你写的是定义和定理而不是指令序列。这种思维转换是第一道坎但跨过去之后你会发现验证工作其实比写业务逻辑更静态、更从容。2. HOL列表的类型内核与递归定义纯函数式基因带来的设计差异HOL中的列表定义和ML里高度相似——这并不奇怪因为HOL很多就是内嵌在Standard ML里的。但要注意HOL里的列表不是运行时数据结构而是完全的逻辑对象所有运算都在类型层面、定义层面和定理层面发生。2.1 从list类型的基本构造说起HOL里列表类型的标准定义大概是这样的val list_INDUCT Define list_INDUCT (P: a list - bool) P [] /\ (!h t. P t P (h::t)) !l. P l;这段定义看着绕其实是归纳原理的表述。你可以这样理解如果想要证明某个性质对所有列表成立只需要证明它对空列表成立并且假设它对尾部列表成立时能推出对头部加尾部的情况成立即可。实际在HOL4的bossLib里列表的构造子就是[]空列表和::cons操作。h::t表示在尾部t前面加上头部h。基本的模式匹配、递归函数定义和你在ML里习惯的写法几乎一模一样。举个例子val APPEND_def Define (APPEND [] l l) /\ (APPEND (h::t) l h::(APPEND t l));这个就是运算符的底层定义。第一个等式是空列表的情况第二个等式把问题缩减到尾部本质上是一个递归定义。在HOL里APPEND [] l l这样的等式本身就是一条定理可以直接被重写规则使用。2.2 为什么不可变是形式化验证的福星很多做C/Rust的朋友看到纯函数式列表第一反应是这不浪费内存吗每次append都得复制整条链表这在普通的软件工程语境下是对的但在验证语境下不可变性恰恰是最珍贵的性质。正因为列表不可变在HOL里我们才有大量漂亮的等式定理比如APPEND (APPEND a b) c APPEND a (APPEND b c)。如果是可变数据结构这个等式需要各种时序逻辑、指针别名分析才能描述复杂度立刻爆表。HOL里的列表不需要考虑谁还在引用它所有表达式都是无副作用的定理重写时可以把任意子表达式替换成等价的另一个表达式这大大简化了证明。提示如果在HOL里看到某个列表表达式的化简不出结果第一反应不要怀疑底层数据结构有问题而是看看自己的递归定义是不是漏了某个构造子case或者化简时没有正确使用对应的重写定理。2.3 柯里化、递归与终止性问题HOL是定义在类型论之上的高阶逻辑所以一切函数本质上都是一元的那些多参数的函数都是柯里化的。这一点和ML一致。比如APPEND在类型系统里大概是a list - a list - a list传入第一个列表后返回一个函数再传入第二个列表才得到结果。在定义递归函数时HOL要求你提供明确的终止性理由。好在列表上的递归基本都是结构递归——每次递归调用都在处理尾部的子列表长度严格递减。对于这种递归HOL的Define命令通常能自动判断终止。如果你自定义了一个奇怪的递归比如基于取一半之类的非结构递归就需要手动提供终止证明这往往是初学者比较郁闷的地方。我的建议是初期尽量把函数定义成对列表直接做结构递归的形态能给后续证明省下大量麻烦。3. 列表上的核心定理与证明套路从MAP、APPEND到归纳法实战有了类型和递归定义就可以开始证明定理了。这一节我们直接上手几个常见定理走一遍完整的证明过程顺便把归纳法的选择策略讲透。3.1MAP_APPEND的证明几乎每个验证项目都会遇到MAP是列表上最常用的高阶函数之一作用是把一个函数应用到列表每个元素上得到新列表。我们要证明的第一个定理是MAP f (APPEND l1 l2) APPEND (MAP f l1) (MAP f l2)直观理解就是先拼接再映射等于先映射再拼接。这个定理有多常用呢在操作系统验证里但凡涉及对队列里的所有进程做某个操作或把新进程追加到队列后统一更新状态的场景大概率都会用到。证明过程是这样的我对l1做归纳 e (Induct_on l1) OK. 2 subgoals: ...第一个子目标是对空列表的。因为MAP f (APPEND [] l2)可以化简为MAP f l2而APPEND (MAP f []) l2也会化简为MAP f l2所以两边相同reflexivity即可解决。这里要清楚为什么能化简——MAP_def和APPEND_def的第一条等式直接给出结果。用SIMPS或者REWRITE_TAC [MAP_def, APPEND_def]就能处理。第二个子目标是h::t的情况。归纳假设告诉我们MAP f (APPEND t l2) APPEND (MAP f t) l2成立。那么左边MAP f (APPEND (h::t) l2)可以化简为MAP f (h::(APPEND t l2))再化简为f h :: MAP f (APPEND t l2)右边化简为f h :: APPEND (MAP f t) l2。于是问题归结为归纳假设本身asm_rewrite一下即可。完整脚本往往就两行 e (Induct_on l1 REWRITE_TAC [MAP_def, APPEND_def] - DECIDE_TAC) e (RW_TAC list_ss [] METIS_TAC [MAP_def, APPEND_def])RW_TAC list_ss []里的list_ss是HOL4里专为列表配好的化简集里面已经展开了绝大多数列表函数的基本定义。正因为它存在上面的证明比手写快得多。3.2FOLDR和FOLDL左折叠还是右折叠折叠函数FOLDR和FOLDL在验证里是真正的老黄牛。FOLDR f a [x1; x2]等于f x1 (f x2 a)从右往左FOLDL f a [x1; x2]等于f (f a x1) x2从左往右。两者的定义如下val FOLDR_def Define (FOLDR f a [] a) /\ (FOLDR f a (h::t) f h (FOLDR f a t));一个很常见的定理是如果f满足某种结合性和单位元条件那么FOLDR和FOLDL结果相同。典型的用处在操作系统建模中比如对进程列表的每一项累加内存占用无论从左还是从右计算总内存不变。证明FOLDR和FOLDL等价时不能直接对列表归纳往往要引入一个更强的引理推广辅助参数。因为FOLDL的累加器天然往前传而FOLDR是往后累积直接证同一是做不动的。这里有个经验看到需要推广辅助参数的迹象时别硬着头皮证原始定理赶紧让归纳假设更强——具体来说把辅助变量连带着放到归纳假设里。这几乎是所有归纳证明中的核心技巧。3.3LENGTH、MEM、FILTER的经典不等式列表的LENGTH、MEM成员关系、FILTER过滤也常用。下面这个定理在验证调度正确性时特别有用MEM x (FILTER P l) MEM x l /\ P x意思是x在过滤后的列表里当且仅当x在原列表里且满足条件P。证明同样是结构归纳加化简核心在于FILTER_def里的分支需要cases处理P x的真假。(* 这是HOL4里的写法 *) e (Induct_on l REWRITE_TAC [MEM_def, FILTER_def] REPEAT STRIP_TAC METIS_TAC [])这类定理看似不起眼但后面做移除已调度进程后集合不变这类论证时几乎每步都离不开。3.4 归纳法选择的三个决定性问题列表归纳法不是无脑套的。我有几个判断标准供参考若定理结论对列表的尾部递归结构敏感优先对那个在递归位置变化的列表做归纳。如果两边都有列表比如MAP f (APPEND l1 l2) ...这种通常对最左边递归展开的列表做归纳。如果遇到折叠相关先想想要不要推广累加器大概率需要。经验补充能直接用induction傻瓜式完成固然好但在项目中期定理之间的依赖关系会很复杂发现某条定理证不过去时先怀疑归纳变量选错了再怀疑重写规则没喂全。4. 集合的经典编码谓词表示法与重写驱动的集合化简接下来是集合。HOL里集合的定义方式对刚接触的人来说有点诡异但一旦接受它就非常优雅。4.1 集合就是谓词a - bool在HOL中类型a set本质上是a - bool的别名。集合A的根本操作是元素归属x IN A。由于集合被表示为函数x IN A在定义层面其实就是A x。也就是说一个集合只是一个返回布尔值的函数。这个编码方式带来一个直接推论没有集合实例这样的实体集合完全由它的特征函数决定。两个集合相等的定义就是外延相等!x. x IN A x IN B这在HOL里通常用SET_EQ之类的定理来处理即A B可以拆分为两个方向的子集关系。4.2 基本集合运算的定义与化简空集在HOL里写作{}多数实现为\x. F全集UNIV是\x. T插入x INSERT A表示在集合A上加上元素x删除x DELETE A表示从A中去掉x交集A INTER B对应\x. A x /\ B x并集A UNION B对应\x. A x \/ B x。熟悉这套定义之后绝大多数集合化简题就是布尔代数题。HOL4里专门有一个set_ss或pred_set_ss不同版本名字略有区别化简集把IN和运算的定义展开成布尔逻辑之后用METIS_TAC或者DECIDE_TAC往往能一路推平。举个例子证明x IN (A UNION B) x IN A \/ x IN B这基本是UNION_def的直接展开没有任何难度。但真正在验证项目里集合表达式并不会这么干净。经常会出现嵌套多重集合表达式、受限集合{x | P x}、以及大并集BIGUNION这时就要靠重写把集合层面降维到逻辑层面。4.3 受限集合与BIGUNION的实际应用受限集合{x | P x}在操作系统建模里用处很大。比如定义所有被锁占用的资源ID集合可以写成{r | locked r}定义所有已注册中断处理函数的中断号集合可以写成{irq | registered irq}。BIGUNION是集合的集合的并集。如果有一个中断集合的集合里面每个元素是一组中断号那么所有中断号的并集就是BIGUNION。这个操作在验证资源分类、按组分配资源时常用。它的基本定理是x IN BIGUNION s ?t. t IN s /\ x IN t这个定义本身几乎就是一条重写定理。4.4 集合外延性的坑与SET_EQ的妙用做集合相等证明时必须时刻想着外延性三个字。很多刚入门的人试图直接化简A B结果发现A和B在表达式上完全不同根本没法直接跑。这时候应该做的是 e (SET_EQ_TAC) ...SET_EQ_TAC把A B转化为!x. x IN A x IN B之后再按元素逐个击破。这个转换用得非常频繁建议形成习惯——别看题目里只是简单集合直接上外延套路往往比强行化简快十倍。另外要留意集合没有顺序、没有重复{x; x; y}在HOL里和{x; y}是相等的但化简起来可能需要额外的规则。这些细节说多了没用多写几个证明就能记住。5. 操作系统建模实战用列表就绪队列、用集合描述中断与资源状态这一节把前面的抽象概念拉到真实建模场景里直接看两个能跑通的实际例子。声明一下下面代码只是演示性质的简化内核模型不代表任何特定工业项目。5.1 案例一用列表建模就绪队列并证明入队操作的尾部追加性质我们定义一个非常简化的进程ID类型和就绪队列type_abbrev (pid, :num) val enqueue_def Define (enqueue (p:pid) [] [p]) /\ (enqueue p (h::t) h :: enqueue p t);这里的enqueue把新进程追加到队尾。现在要证明一个性质新进程入队后队列长度恰好加一val ENQUEUE_LENGTH prove( !p l. LENGTH (enqueue p l) LENGTH l 1, REPEAT GEN_TAC Induct_on l - REWRITE_TAC [enqueue_def, LENGTH_def] - ASM_REWRITE_TAC [enqueue_def, LENGTH_def]);这个证明非常简单但它揭示了一个验证日常先定义后证明结构性性质。真正的调度验证当然比这复杂但核心流程是一样的——把队列的追加定义为递归函数然后围绕它构建不变量定理。稍微实际一些的变体是描述去重队列enqueue_unique只有在进程ID不在队列中时才追加。这时需要证明的就不是单纯的长度了而是不变量保持如果原队列无重复元素新队列也无重复元素。这就必须引入MEM和FILTER相关定理正好用上前面第三节的内容。5.2 案例二用布尔集合记录CPU中断屏蔽状态现在用集合建模中断屏蔽。假设系统里有三个中断号1、2、3关键中断号是1和2。屏蔽一个中断就是把它加入一个集合val mask_irq_def Define mask_irq (n:num) (s:num set) n INSERT s;我们要证明的定理是如果一开始所有关键中断都已屏蔽往里面加任何中断号关键中断仍然是屏蔽的val MASK_PRESERVES_KEY_IRQS prove( !n s. key_irqs SUBSET s key_irqs SUBSET (mask_irq n s), REPEAT STRIP_TAC REWRITE_TAC [mask_irq_def] key_irqs SUBSET (n INSERT s) by METIS_TAC [SUBSET_INSERT, SUBSET_TRANS] ACCEPT_TAC ());这里的key_irqs是一个受限集合{1; 2}。看似平淡无奇但这种设置某状态后关键状态仍然保持的定理正是操作系统验证里最常写的命题——它们合起来才支撑起即使在高中断频率下关键资源也不会缺失的整体结论。5.3 从简化模型到真实验证工作流的扩展路径你会说这两个案例也太玩具了。没错真实操作系统的验证比如进程调度正确性、虚拟内存映射一致性、文件系统崩溃一致性都要复杂得多。但从方法论上它们几乎都是从这种小块定理拼起来的先把某个状态表示成列表或集合然后证明每个操作都维持一组不变量最后把这些定理组合起来得到顶层正确性。真实项目里经常出现的情况是数据结构远不止一层而是列表的元素本身含有嵌套集合集合的元素又是一组列表。这时前面所有关于列表和集合的基本定理就变得更加珍贵。没有扎实的底子嵌套起来很快就会乱套。6. 验证实践中的常见陷阱与个人心得这一节分享一些我在实际验证过程中踩过的坑以及几次醍醐灌顶的经验。如果你在某个证明上卡了两小时大概率命中了下面的某一条。6.1 陷阱一重写器展开过头把定理证明变成无从下手的怪物REWRITE_TAC [某个定义]是所有定义都会无条件展开。有时候你只想展开它出现在特定位置的那一次结果它把其他你不希望动的东西也展开了目标变得面目全非。遇到这种情况别硬撑着化简改用ONCE_REWRITE_TAC、RW_TAC或者手动ASSUME后用fs控制展开。6.2 陷阱二归纳变量选择错误导致归纳假设太弱第二类常见问题是定理里有两个列表你归纳了错误的那个。通常规则是选择递归定义中真正递归的位置对应的变量。如果你把APPEND l1 l2性质的归纳放到l2上归纳假设往往会非常弱证到第二步就停住了。这时赶紧换成另一个列表试试。6.3 陷阱三集合相等死磕化简忘了外延性如果你在一个A B的目标前疯狂REWRITE_TAC大概率陷入死胡同。正确的第一招永远是SET_EQ_TAC或者你手动拆两边子集关系把集合等式变成纯逻辑命题。再提醒一次集合就是谓词集合相等就是谓词间的双蕴含别把它们当成两个盒子来比较。6.4 技巧一定义得越规范证明越省力在HOL里定义一个操作时多想想如果我要证明它的性质最自然的等式形式是哪几条。尽量让定义在递归结构上线性展开每个构造子给一条干净的等式。我在实践中发现定义写得好后面定理的REWRITE_TAC [func_def]几乎是一击即中定义写砸了后面全是各种cases和剥壳。6.5 技巧二常用定理清单要自己攒HOL4自带了很多列表和集合定理但真正常用的也就是那么十几个APPEND_assoc、MAP_APPEND、FOLDR_APPEND、MEM_APPEND、FILTER_APPEND、SUBSET_INSERT、IN_UNION、SET_EQ等等。建议大家把自己项目里反复出现的定理单独建一个库——不是说要重新实现什么而是把自己的证明脚本整理成模块让新定理能顺着已有定理快速证明。这套流程越早建立后期效率越高。6.6 技巧三别放着METIS_TAC不用但别只会METIS_TACMETIS_TAC非常强大能在几十秒内自动找到很多中等难度的一阶逻辑证明。但在大型项目里它偶尔会把证明时间拉得很长或者因为目标里带有大量无关假设而性能滑坡。我的做法是小目标无脑METIS_TAC收掉复杂目标先手动拆分到足够小的规模再让METIS_TAC做临门一脚。这样既省力又不至于让证明变成黑盒。结尾与下一步如果这一篇的列表和集合你能够熟练掌握操作系统验证的基础就算打下了一半。接下来值得啃的内容是关系与函数的一些高阶抽象、以及更深层的归纳原理与定义原理——比如如何定义一组进程之间的依赖关系如何对树形结构做递归和证明。这些在后续的教程里我会继续写。最后分享一个我的习惯每学一个新的数据结构或新的证明模式不要只读一定要在HOL里亲手敲一遍定义、手动走一遍归纳证明。不夸张地说我自己的感悟有七成来自踩坑只有三成来自看文档。形式化验证这门手艺听着高大上实际上靠的是大量重复训练形成的证明直觉。列表和集合只是起点但起点的地基打不牢后面整个体系都会跟着晃。把这一篇里的代码全部自己跑通一遍再去追后面的内容你会觉得顺畅很多。