Rocq 内核修复：嵌套互余 cofixpoint 仅允许主分支递归调用外层 cofixpoint

形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载本文围绕 RocqCoq 继任者内核的一处守卫条件guard condition修复展开当互余 cofixpoint 嵌套在另一个 cofixpoint 之中时只有内层互余块的主分支main branch of the mutual允许对外层 cofixpoint 发起递归调用其余分支的此类调用将被内核拒绝。读完本文你将理解余归纳定义的守卫检查机制、本次修复在kernel/inductive.ml中的具体实现以及如何在测试套件中复现与验证这类修复。背景余归纳定义与 cofixpoint 的守卫条件Rocq 通过CoInductive定义余归纳类型coinductive types并通过CoFixpoint构造余递归定义。与Fix类似内核在类型检查时会校验 cofixpoint 的每个递归调用是否满足守卫条件递归调用必须出现在某个构造函数参数内部更精确地说出现在共域余归纳类型的严格子项路径上否则定义会被判定为非法。从源码看cofixpoint 在项表示中对应CoFix构造子接口在 kernel/constr.mli(* If [funnames [|f1,.....fn|]] [typarray [|t1,...tn|]] [bodies [b1,.....bn]] then [mkCoFix (i, (funnames, typarray, bodies))] constructs the ith function of the block [CoFixpoint f1 b1 with f2 b2 ... with fn bn.] *) type cofixpoint (constr, types, Sorts.relevance) pcofixpoint val mkCoFix : cofixpoint - constr一个互余块mutual block由若干分支组成语法上写作cofix f : ... with g : ... for f其中for f指定该块被展开时选取的分支也就是主分支。守卫条件的必要性在于保证内核的一致性consistency若允许未受守卫的余递归调用就可能构造出无穷下降序列进而在余归纳类型上导出悖论。历史上与此相关的守卫检查漏洞多次被修复例如doc/sphinx/changes.rst的 9.1.0 内核变更记录中就列有guard checking forgot to check non principal arguments of a fixpoint for unguarded uses of the fixpoint leading to an inconsistencydoc/sphinx/changes.rst等多项修复。问题本质嵌套互余 cofixpoint 中的递归调用许可changelog 文档doc/changelog/01-kernel/22392-no-nested-mutual-cofix-Fixed.rst记录的内容如下Fixed:On mutual cofixpoints nested in another, only the main branch of the mutual may do a recursive call of the outer cofixpointPR #22392修复 issue #22389by Yann Leray。即在修复前守卫检查对嵌套互余场景存在疏漏。所谓嵌套互余指在一个互余 cofixpoint 的定义体中又出现另一个互余 cofixpoint 块例如示意结构CoFixpoint outer : (cofix f : ... outer ... with g : ... outer ... for f)修复前内层互余块的非主分支如上述g即使递归调用了外层 cofixpoint也可能被守卫检查放过。由于非主分支并不参与该块的展开路径允许它绕过守卫地引用外层余递归定义会破坏每个递归调用都必须被构造函数包裹的封闭性理论上可被利用来构造不一致性。修复实现check_one_cofix对CoFix分支的新约束本次修复的核心位于内核守卫检查函数check_one_cofix中kernel/inductive.ml。它通过局部递归函数check_rec_call env alreadygrd n tree t遍历定义体其中alreadygrd记录当前是否已处于受保护位置n与nbfix标识当前外部互余块的递归变量范围tree描述共域余归纳类型的子项路径。当遍历遇到嵌套的CoFix时kernel/inductive.ml 的处理逻辑为| CoFix (i, (_, varit, vdefs as recdef)) - let () if not (List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env, UnguardedRecursiveCall c)) in let () if not (Array.for_all (noccur_with_meta n nbfix) varit) then raise (CoFixGuardError (env, RecCallInTypeOfDef c)) in let nbfixinner Array.length vdefs in let env push_rec_types recdef env in let () if not (Array.for_all_i (fun j c - Int.equal i j || noccur_with_meta (n nbfixinner) nbfix c) 0 vdefs) then raise (CoFixGuardError (env, RecCallInNonMainMutual c)) in check_rec_call env alreadygrd (n nbfixinner) tree vdefs.(i)这段代码依次施加四重约束内层 cofixpoint 块自身的应用参数args中不得出现外层 cofixpoint 的递归调用否则报UnguardedRecursiveCall内层互余块的所有类型varit中不得出现外层 cofixpoint 的递归调用否则报RecCallInTypeOfDef遍历内层互余块的全部定义体vdefs对于索引j不是主分支i的定义体若其中出现外层 cofixpoint 的递归调用即noccur_with_meta (n nbfixinner) nbfix c为假直接抛出RecCallInNonMainMutual错误——这正是本次修复新增的约束主分支vdefs.(i)则继续递归进入check_rec_call只要递归调用受守卫位于构造函数参数内就仍然允许。需要特别说明的是上述约束针对的是外层 cofixpoint 的递归调用。检查进行到第 3 步时环境已通过push_rec_types recdef推入内层互余块因此外层 cofixpoint 的递归变量位于n nbfixinner之后的索引区间noccur_with_meta (n nbfixinner) nbfix c正是用来探测该定义体中是否引用了外层 cofixpoint。完整检查流程与错误报告check_rec_call的入口调用为check_rec_call env false 1 vlra defkernel/inductive.mlalreadygrd初始为false——定义体顶层位置直接调用自身不被视为受守卫。整块检查由check_cofix驱动kernel/inductive.mllet check_cofix ?evars env (_bodynum,(names,types,bodies as recdef)) let flags Environ.typing_flags env in if flags.check_guarded then let nbfix Array.length bodies in for i 0 to nbfix-1 do let fixenv push_rec_types recdef env in try let ((mind, _),_) codomain_is_coind ?evars env types.(i) in let vlra WfPaths.lookup_subterms env mind in check_one_cofix ?evars fixenv nbfix bodies.(i) vlra with CoFixGuardError (errenv,err) - error_ill_formed_rec_body errenv (Type_errors.CoFixGuardError err) names i fixenv (judgment_of_fixpoint recdef) done else ()要点如下每个分支的类型必须先满足codomain_is_coind即共域必须是余归纳类型否则报CodomainNotInductiveType整块检查受环境 typing flags 的check_guarded控制可关闭对应 kernel/environ.ml 中的deactivated_guard关闭时守卫检查整体跳过任何守卫违规包括新增的RecCallInNonMainMutual都会包装为CoFixGuardError最终经error_ill_formed_rec_body转为IllFormedRecBody类型的类型错误拒绝该定义。check_cofix的入口在类型检查器 kernel/typeops.ml 的CoFix (i,recdef)分支被调用与check_fix平行。全部 cofix 守卫错误类型集中在 kernel/type_errors.mli 的pcofix_guard_error中错误构造子含义CodomainNotInductiveType共域不是余归纳类型UnguardedRecursiveCall递归调用未受守卫NestedRecursiveOccurrences递归调用的参数中嵌套出现本块递归变量RecCallInTypeOfAbstraction递归调用出现在 λ 抽象的类型中RecCallInNonRecArgOfConstructor递归调用出现在构造函数的非递归参数中RecCallInTypeOfDef内层互余块的类型中引用外层递归变量RecCallInNonMainMutual内层互余块的非主分支体中引用外层递归变量本次修复新增RecCallInCaseFun/RecCallInCaseArg/RecCallInCasePred递归调用出现在 match 的返回函数、被匹配项或谓词中NotGuardedForm/ReturnPredicateNotCoInductive其他未受守卫形式测试与同类修复脉络仓库的失败测试 test-suite/failure/cofixpoint.v 专门覆盖嵌套 cofixpoint 的守卫检查其用例可追溯到 2014 年 Maxime Dénès 在 coqdev 上报告的问题CoInductive CoFalse : . CoInductive CoTrue : I. Fail CoFixpoint loop : CoFalse : (cofix f : loop with g : loop for f). Fail CoFixpoint loop : CoFalse : (cofix f : I with g : loop for g). Fail CoFixpoint loop : CoFalse : (cofix f : loop with g : I for f).这些用例验证了无论主分支还是非主分支未受守卫的外部 cofixpoint 递归调用如直接以loop为体都必须被拒绝。本次 #22392 修复在此基础上进一步收紧即使递归调用出现在受保护位置只要它位于内层互余块的非主分支体中同样必须被拒绝。test-suite/failure/目录下的失败测试全部以Fail标注预期被拒绝的定义回归测试时由测试框架确认这些定义确实无法通过内核检查。同类修复在 changelog 中并不孤立。doc/sphinx/changes.rst的 9.1.0 内核条目还记录了守卫检查对非主参数漏检#20415、嵌套 match 检查不完整#20457、跨 fixpoint 错误归约#20648等多项漏洞修复doc/sphinx/changes.rst可见守卫检查是内核一致性的长期关注点本次修复与之一脉相承。对使用者的影响对于普通用户本次修复的直观影响是在互余定义中嵌套另一个互余块时非主分支不再被允许调用外层 cofixpoint。此前可能碰巧通过检查的此类定义在新版内核中将得到类型错误报错源自RecCallInNonMainMutual。如果你在代码中确实需要在嵌套互余块的非主分支中使用外部余递归函数正确的做法是把该调用移到主分支体内或将其作为显式参数传入内层块从而让递归调用发生在受守卫且许可的位置。内核层面不做任何推测性放行——守卫条件必须由用户定义的结构显式满足。需要说明的是check_guarded这一 typing flag 的存在意味着守卫检查可以在某些实验性设置下被整体关闭见 kernel/environ.ml但关闭守卫检查会破坏内核的一致性保证只适用于专门的内核调试场景不应在正常开发中使用。小结本次修复PR #22392修复 issue #22389约束了嵌套互余 cofixpoint 的守卫检查只有内层互余块的主分支可以对外层 cofixpoint 做递归调用核心实现位于 kernel/inductive.ml通过RecCallInNonMainMutual错误拒绝非主分支中的外部递归调用检查流程完整链路为typeops.ml入口 →check_cofix→check_one_cofix→check_rec_call错误经CoFixGuardError/IllFormedRecBody上报相关回归测试见 test-suite/failure/cofixpoint.v此类守卫检查修复的演进脉络可查阅 doc/sphinx/changes.rst。赞分享形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载相关推荐GitHub Markdown与文档渲染技巧大全GitHub Markdown与文档渲染技巧大全 本文全面介绍了GitHub Markdown的高级使用技巧包括语法高亮与代码块优化、表情符号与图片嵌入技巧、教程文档CPython 修复深层嵌套 GenericAlias 的 __parameters__ 递归崩溃问题gh-issue-154275CPython 修复深层嵌套 GenericAlias 的 __parameters__ 递归崩溃问题gh issue 154275 导读 本文围绕 CPy编程语言语言运行时解释器标准库企业微信推送消息到微信免费方案Wecom酱搭建与使用全攻略企业微信推送消息到微信免费方案Wecom酱搭建与使用全攻略 你是不是也遇到过这样的场景服务器报警只能发邮件、监控通知要装一堆 App、想给自己微信发条定时提后端即时通讯Serverless上一篇YCBlogs Android WebView 问题实战手册从内核进化、性能优化到安全漏洞与 JS 交互的 16 个坑位全解下一篇智慧树自动刷课插件3分钟配置实现全自动学习体验创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考