正文 · AI 翻译
审查代码时，你会先看差异。你不会凭肉眼比较两个各有 3,000 行的文件，还指望找出每一处改动。形式化策略可能更难比较，因为文本差异往往会突出不影响含义的语法变化。调整两个合取项的顺序、交换等式两边的参数，或使用等价谓词，都可能让文件的大部分内容看起来发生了变化。真正影响行为的改动，例如要求写的是 and 却用了 Or，可能淹没在这些干扰中。语义差异会显示两个策略的共同之处以及分歧所在。本文使用的开源引擎通过反合一计算这种差异；反合一会找出两个表达式最具体的共同模式。Plotkin 1970 年的论文给出了经典表述。该引擎基于 e-graph 工作，用它记录已知相等的表达式。我们提供能证明这些相等关系成立的代数定律和领域规则，例如将“外部目的地”等同于“非内部目的地”。结果只显示一次共同部分，并保留每个不同部分的两个版本，供审查。如果没有剩余差异，那么在这些定律和规则下，两个策略是等价的。如果规则或搜索不完整，剩余差异可能反映的是引擎尚未发现的等价关系。一个应用场景是自动形式化。自动形式化将自然语言转换为形式语言。假设你想把需求转换为 SMT-LIB，即 Z3 和 cvc5 等可满足性模理论（SMT）求解器的标准输入语言，或者转换为 Cedar 或 Dogwood，以控制软件系统中的授权。大语言模型（LLM）根据文字描述生成形式化产物。模型负责写出产物，不参与差异的计算。将模型运行两次，它可能生成两种不同的形式化结果，而你没有真实标准来确定哪一种正确。语义差异会显示它们在哪些地方一致、哪些地方不同。你可以通过改变模型、提示词或采样温度来生成更多候选结果。比较这些结果，可以看出哪些部分保持一致、哪些部分会变化。先审查变化的部分。需求也可以转化为 OpenShell 沙箱策略或通用表达式语言（CEL）表达式。OpenShell 使用 YAML 描述代理对文件系统和网络的访问权限。CEL 嵌入在应用程序中，用于求值表达式，包括策略条件。这些语言和格式能表达的内容各不相同，但转换到其中任何一种时，都可能在条件、范围或事件方面产生分歧。下表列出了一些示例性分歧：语言或格式；策略关注点；分歧示例。Cedar；谁能在什么条件下对资源执行某项操作；一种转换要求同时具备所有权和批准，另一种接受满足其中任一条件。Dogwood；涉及当前请求和近期事件历史的授权；一种转换检查先前成功的响应，另一种检查请求事件。OpenShell 策略；代理对文件系统和网络的访问权限，包括针对特定二进制程序的规则；一种转换允许限于代码仓库范围的 GET，另一种允许限于组织范围的 POST。CEL；对宿主应用程序提供的输入求值的条件；一种转换要求两个允许的端口都满足生产环境条件，另一种只对其中一个端口提出这一要求。在每个具体示例中，我们都在同一个策略上下文中比较同一项需求的不同转换结果。我们将相关语法编码为项，并声明比较时使用的等式。引擎读取这些编码；它不会从这 4 种格式导入原生策略。这一思路是 Farquhar 等人在《Nature》（2024 年）中描述的“语义熵”的形式化方法对应物。该方法会采样多个自然语言答案，将彼此蕴涵的答案归为一类，并报告一个数值。对于形式化输出，反合一能保留更多信息：它会找出共同结构和每一处分歧，而不只是返回一个分数。 反例有助于解释分歧的后果。SMT 求解器可以找到一个具体赋值，使一个公式成立而另一个公式不成立。审查者随后可以沿着公式追踪这个赋值，理解相互冲突的决策。反合一器提供了另一种视角：它组织共同的结构和不同的片段，而不发出 SMT 查询。求解器或策略验证器可以帮助解决这些片段。我们假定你能读懂 SMT-LIB 中的 S 表达式语法，并知道什么是授权策略。E-graph 和反合一会在出现时加以解释。当几个译法在需求的某一部分上一致时，差异对照只显示该部分一次；在它们不一致的地方，则保留各个备选表达供审查。语义差异对照如何表示分歧 假设一个策略生成流水线为以下需求提供了两条候选规则：发送到外部目的地的敏感数据必须加密。规则 A 规则 B sensitive(data) ∧ external(dst) → encrypted ¬internal(dst) ∧ sensitive(data) → audited 它们是否是同一条规则并不明显。条件的顺序不同，external 被间接表达为 not internal，结论也不一致。引擎为这些项计算一个最具体反合一项。在其输入语言中，这两条规则是 S 表达式。完整程序首先声明词汇：(sort Formula) (sort Data) (sort Dest) (function Lit (bool) Formula) (function And (Formula) Formula :assoc-comm-idem :identity (Lit true)) (function Implies (Formula Formula) Formula) (function Not (Formula) Formula) 然后，它为每个谓词（sensitive、external、internal）和常量（data、dst、encrypted、audited）各添加一行函数声明。这里，And 被声明为满足结合律、交换律和幂等律，下一节会对此作出解释：(let ruleA (Implies (And (sensitive (data)) (external (dst))) (encrypted))) (let ruleB (Implies (And (Not (internal (dst))) (sensitive (data))) (audited))) (antiunify ruleA ruleB :algorithm exact) 引擎返回一个项：(anti-unify :size 11 :cr 0.5000 :completion exact (Implies (And (sensitive data) (Variants (external dst) (Not (internal dst)))) (Variants encrypted audited))) 结果中没有体现顺序变化，因为 And 被声明为满足结合律、交换律和幂等律。仍有两个 Variants 节点，每个节点标记输入之间存在分歧的位置，而其中只有一个是含义上的差异。(external dst) 与 (Not (internal dst)) 之间的差异是用词上的差异。两者表达的是同一个领域事实。引擎无法仅凭语法推断出这一点。将这个领域事实写成重写规则，运行至饱和（直到没有规则再添加新的等价关系），然后再次进行差异对照：(rewrite (external d) (Not (internal d))) (run 2) (antiunify ruleA ruleB :algorithm exact) 饱和后，引擎返回：(anti-unify :size 8 :cr 0.1429 :completion exact (Implies (And (sensitive data) (external dst)) (Variants encrypted audited))) 还剩一个 Variants 节点：在需求要求加密的地方，规则 B 要求审计。教科书式的表述会在这个位置放一个新变量。引擎则写出 (Variants encrypted audited)：一个容纳两种解读的节点。选择每个 Variants 节点的第一个子节点，就能在所声明的代数性质和重写规则下重构规则 A。选择第二个子节点，就能得到规则 B。反合一项是两个项的无损合并：共同结构只出现一次，每一处真正的分歧都成为一个局部、可供审查的节点。三个字段描述结果：:size、:cr 和 :completion。:size 字段统计具体节点（Variants 标记本身不计入，但它的两个子节点都计入，因此不能把结构藏在一个节点里）。:cr 字段报告压缩比 (s - a) / b，其中 s 是结果大小，a 和 b 分别是两个输入中较小和较大的大小。对于每个输入，我们使用其在当前 e-graph 中已知的最小等价形式。 得分为 0 表示在已声明的等式下完全一致。经过前述重写后，两个输入各有 7 个节点，结果有 8 个节点，因此得分为 (8 - 7) / 7，约为 0.1429。如果将两份完整策略放在单个 Variants 节点中，则会用到 14 个节点，得分为 (14 - 7) / 7 = 1。这是完全不共享结构时的参考值。得分 1 是参考值，并非上限。搜索可能使用比已知最小输入形式更大的等价形式。因此，如果结果大于两个输入的节点数之和，得分就会超过 1。例如，如果两个输入的最小形式各有 10 个节点，而结果有 23 个节点，则比值为 (23 - 10) / 10 = 1.3。:completion 字段报告 exact，表示搜索空间已穷尽；报告 budget，则表示默认的随时可用搜索（一种蒙特卡罗搜索，见实现部分）在穷尽搜索空间之前达到了模拟运行次数上限。:cr 越低，表示输入在已声明的等式下共享的结构越多。这并不能证明正确性：两个候选项可能有相同的错误。熵得分用一个数字概括差异。完整的语义差异结果还会指出候选项在哪里存在分歧，并在 Variants 节点中保留两种备选形式。语义差异比较只忽略已声明等式所涵盖的差异。普通的语法反合一也会报告本例中的重新排序。接下来的 3 节将展示如何声明代数性质并添加领域恒等式。反合一会将共享结构只存储一次，并用 Variants 节点标记每处差异。选择每个节点的一侧，就能在已声明等式的意义下重构对应的输入。5 分钟内运行语义差异比较 从源代码构建该引擎只需要固定版本的 Rust 工具链。其形式化验证注解将在实现部分介绍；使用普通 rustc 编译时，这些注解不会保留。以下命令将版本固定为示例所用的修订版：git clone https://github.com/yaspar-org/semi-persistent.git cd semi-persistent git fetch origin 5a7969ae4ea88117a64faac4f42af5c358e213e2 git checkout --detach FETCH_HEAD cargo build --release ./target/release/semi-persistent doc/book/examples/12-first-au.egg 它会输出一个 (anti-unify ...) 项。命令行解释器读取一个 S 表达式文件（按惯例扩展名为 .egg）。你需要声明排序和运算符，用 let 定义两个项，可以选择添加重写规则并运行至饱和，然后执行 antiunify。有两种机制可告知引擎哪些语法变化不影响含义：一是为运算符指定结合律、交换律和幂等律等代数性质的注解，二是针对其他情况编写显式重写规则。以下是示例所用签名中的代数部分：(function Lit (bool) Formula) (function And (Formula) Formula :assoc-comm-idem :identity (Lit true)) (function Or (Formula) Formula :assoc-comm-idem :identity (Lit false)) (function Eq (Account Account) Formula :comm) And 和 Or 都是可变参数运算符，满足结合律、交换律和幂等律，且各有一个布尔中性元素。Eq 满足交换律。因此，合取项的任何重新排序、重新分组和重复都算作同一个项。除此之外不作任何假设：只有列出的规律成立，其他任何恒等式都必须写成显式重写规则。:identity 元素使差异比较能够对齐仅存在于一个输入中的合取项：缺失的合取项会与 (Lit true) 配对，而不会导致整个 And 表达式无法对齐。两个案例研究都依赖这种通过单位元进行的对齐。:assoc-comm-idem 使重新排序、重新分组和重复的操作数等价。:identity 使差异比较能够将缺失的操作数与运算符的中性元素对齐。包含两个策略错误的示例 贯穿全文的示例随代码仓库提供，路径为 egraph/examples/au_policy_divergence.egg。 考虑这样一条策略语句：仅当源存储桶已启用版本控制，且目标存储桶位于获准区域时，才允许跨区域复制请求。如果对象标记为机密，目标账户与源账户必须相同，并且必须启用使用客户管理密钥的服务器端加密。不超过分段上传阈值的对象直接复制。更大的对象需要分段复制。两个人，或者同一模型的两次独立运行，将其形式化（文件中的 formulaA 和 formulaB）：编码 A (Implies (permit) (And (versioningOn (src)) (approvedRegion (regionOf (dst))) (Implies (taggedConfidential (obj)) (And (Eq (accountOf (dst)) (accountOf (src))) (sseCmk))) (Ite (Lte (sizeOf (obj)) (multipartThreshold)) (directCopy) (multipartCopy)))) 编码 B (Implies (permit) (And (Ite (Lt (sizeOf (obj)) (multipartThreshold)) (directCopy) (multipartCopy)) (Implies (taggedConfidential (obj)) (Or (Eq (accountOf (src)) (accountOf (dst))) (sseCmk))) (Or (usEast1 (regionOf (dst))) (euWest1 (regionOf (dst)))) (versioningOn (src)))) 文本上有 5 处差异。其中 3 处属于表示方式的差异：合取项的顺序调整了，Eq 的参数交换了位置，approvedRegion 被显式展开为两个 AWS 区域（us-east-1 和 eu-west-1）。另有 2 处涉及运算符变化：机密对象子句中的 And 变成了 Or，大小阈值处的 Lte 变成了 Lt。对两个编码做统一差异比较，会将其 28 行中的 18 行标记为已更改（图 1，文本差异窗格），却无法指明这 5 处差异中哪些改变了含义。两个编码的精确反统一结果如下：(anti-unify :size 42 :cr 0.5862 :completion exact (Implies permit (And (Implies (taggedConfidential obj) (And (Or (Eq (accountOf dst) (accountOf src)) (Variants (Lit false) sseCmk)) (Variants sseCmk (Lit true)))) (Ite (Variants (Lte (sizeOf obj) multipartThreshold) (Lt (sizeOf obj) multipartThreshold)) directCopy multipartCopy) (versioningOn src) (Variants (approvedRegion (regionOf dst)) (Or (usEast1 (regionOf dst)) (euWest1 (regionOf dst))))))) 5 处差异中有 2 处消失了。由于 And 被声明为满足结合律、交换律和幂等律（ACI），合取项的顺序调整被吸收了。由于 :comm 将 Eq 的参数规范化，两种解读中的交换后参数具有相同的打印顺序。两者都不改变含义，因此都未被报告。机密对象子句在要求使用“与”的地方用了 Or。编码 A 要求同时满足同一账户检查和使用客户管理密钥的服务器端加密。编码 B 则接受其中任一条件。该引擎借助各自的单位元，将 A 的合取式与 B 的析取式对齐，因此这一分歧表现为两个相邻的 Variants 节点。在每个节点都选择第一个子节点，就能重建 A：Or 简化为单独的相等性判断，而 sseCmk 仍是必须满足的合取项。在每个节点都选择第二个子节点，就能重建 B：必须满足的 sseCmk 被弱化为 (Lit true)，并且只作为 Or 中的一个备选条件保留下来。这两个 Variants 节点共同表明，编码 B 接受仅有服务器端加密的情况，因而允许跨账户复制机密对象。你可能原本以为 sseCmk 会被共享，而不是重复出现。然而，一阶反统一器无法对连接词本身进行泛化，因此 And 与 Or 的差异迫使结果拆分为两处对齐。通过恒等元对齐，5 个节点组成的相等性判断仍只共享一次。精确求解器的穷举搜索没有找到更小的形式，而且打印出的结果比用单个 Variants 完整保留两个子句少 1 个节点。加入领域重写规则，再运行一次差异比较。区域对应的 Variants 节点不是错误。它反映的是领域知识的缺失：在此部署中，获准区域恰好就是这两个。 将其表述为一次重写，进行饱和处理，然后再次求差异：(rewrite (approvedRegion r) (Or (usEast1 r) (euWest1 r))) (run 3) (antiunify formulaA formulaB :algorithm exact) Region 差异进入共享骨架，:cr 从 0.5862 降至 0.4000。完整结果见图 1 的语义差异窗格。恰好还剩两处分歧：被弱化的机密性条款和阈值。B 的 Lt 是严格小于，因此大小恰好等于 multipartThreshold 的对象在 A 下直接复制，在 B 下则走分段复制路径。分歧仅限于 Ite 条件。两个分支都位于共享骨架中。剩余的两处差异都是真正的缺陷，必须由授权审核人员解决。代数规则和一条领域重写规则解释了其他差异。同一个文件还运行随时可用搜索：(antiunify formulaA formulaB :algorithm uct :playouts 3000)，返回相同的大小为 35 的项。整个程序在 Apple M3 Pro 笔记本电脑上远低于 100 毫秒即可完成（二进制程序预热后为 50–60 毫秒）。这包括解析、声明、饱和处理、五次反合一查询及其回归检查，以及进程启动。我们使用 Rust 1.97.1 的 release 构建，通过 shell 的 time 命令，对 ./target/release/semi-persistent egraph/examples/au_policy_divergence.egg 进行五次预热后的运行，测量了实际耗时。“入门”一节展示了同一条命令。文本差异：28 行中有 18 行被标记 (Implies (permit) (And - (versioningOn (src)) - (approvedRegion (regionOf (dst))) + (Ite + (Lt (sizeOf (obj)) (multipartThreshold)) + (directCopy) + (multipartCopy)) (Implies (taggedConfidential (obj)) - (And - (Eq (accountOf (dst)) (accountOf (src))) + (Or + (Eq (accountOf (src)) (accountOf (dst))) (sseCmk))) - (Ite - (Lte (sizeOf (obj)) (multipartThreshold)) - (directCopy) - (multipartCopy)))) + (Or + (usEast1 (regionOf (dst))) + (euWest1 (regionOf (dst)))) + (versioningOn (src)))) 语义差异：两处分歧，范围明确 (anti-unify :size 35 :cr 0.4000 :completion exact (Implies permit (And (Implies (taggedConfidential obj) (And (Or (Eq (accountOf dst) (accountOf src)) (Variants (Lit false) sseCmk)) (Variants sseCmk (Lit true)))) (Ite (Variants (Lte (sizeOf obj) multipartThreshold) (Lt (sizeOf obj) multipartThreshold)) directCopy multipartCopy) (versioningOn src) (approvedRegion (regionOf dst))))) 图 1：对同一对编码进行文本差异比较和反合一。左侧的文本差异标记了 28 行中的 18 行（删除、新增）。右侧，一条领域重写规则将共享结构移入灰色骨架，突出显示的 Variants 将剩余差异限定在被弱化的机密性条款和严格阈值。语义差异窗格将一长行换行以适应显示。应用已声明的代数规则和一条领域重写规则后，五处文本差异减少为两处语义分歧：被弱化的机密性条款和严格的大小阈值。Cedar 和 Dogwood 策略的语义差异比较。在授权策略中，缺失一项约束条件会扩大许可范围，并可能导致策略在故障时默认放行。Cedar 是 Amazon Verified Permissions 背后的开源授权策略语言。Dogwood 为 Cedar 授权策略扩展了时间条件，用于 AI 智能体的运行时验证。其时间子语言利用记录的事件历史来约束操作。该引擎不评估 Dogwood 策略，而是依据已声明的代数规则比较其抽象语法差异。验证（模式检查）和重放（根据记录的事件历史评估策略）仍由 Dogwood 负责。该引擎的用户指南有一章完整示例，对针对同一要求独立编写的两个 Dogwood 候选策略进行差异比较：仅当过去 15 分钟内已有一次健康检查返回 200 时，才允许智能体向 /deploy 发出 POST 请求。候选策略 A 保留了两个请求约束条件（方法和路径），但从请求事件中读取状态码，而这种事件类型并不包含该字段。 候选方案 B 使用了正确的响应事件，却漏掉了 /deploy 路径守卫。任何匹配的健康检查之后，B 还允许向 /admin/purge-all 发送 POST 请求。候选方案在呈现形式上另有 6 处差异，声明的代数或由 3 条规则组成的比较理论都能消除这些差异：呈现形式差异／消除方式：Cedar 条件顺序，eAnd :assoc-comm-idem；时间合取顺序，tAnd :assoc-comm-idem；谓词字段顺序，args :assoc-comm-idem；method == "POST" 与 "POST" == method，eEq :comm；15m 与 900s，单位重写加常量折叠；count >= 1 与 1 <= count，(birewrite (tLte a b) (tGte b a))。比较理论由 3 条可见的重写规则组成，并非隐藏的规范化过程：(rewrite (mins x) (secsTimes x 60)) (rewrite (secsTimes x y) (secs (IBig::* x y))) (birewrite (tLte a b) (tGte b a)) (run 4)。这两个候选方案的反统一结果（位于仓库的 doc/book/examples/20-dogwood-simple.egg）大小为 61，:cr 为 0.1864；在其余部分共用同一策略骨架的情况下，恰有 2 处分歧：(anti-unify :size 61 :cr 0.1864 :completion exact (rule permit (head anyPrincipal (actionEq aHttpRequest) anyResource) (eAnd (eEq (eCtx (fld fInput (fld fMethod fnil))) (eStr vPOST)) (temporal ... (pred aHttpRequest (Variants request response) ... (Variants (eEq (eCtx (fld fInput (fld fPath fnil))) (eStr vDeploy)) eTrue))))。对每处分歧使用最简单的可用检查。2 处二元分歧产生 4 种候选补全方案。Dogwood 验证无需人工审查便解决了第一处分歧：它拒绝了两个 request 补全方案（“谓词……提到了字段 output.status_code，但该事件并未声明此字段”）。第二处分歧涉及单位元对齐：候选方案 A 的路径守卫与 eTrue 配对，表明候选方案 B 漏掉了该守卫。需求解决了这处分歧（保留守卫）；覆盖 2 个决策点的重放显示了后果：健康检查之后，候选方案 B 允许了目标范围之外的 POST 请求，而修复后的策略拒绝了它。将 B 的事件类型与 A 的守卫结合，得到了一条两个候选方案都未写出的策略。如果只在两个候选方案之间选择，就会保留其中一个错误。交换律有一个附带条件，而引擎并不检查它。Cedar 的 && 会短路求值，因此只有在两个操作数都不会引发错误时，交换它们的顺序才是可靠的。因此，这种比较依赖验证来排除与顺序有关的错误，例如只有放在 has 守卫之后才安全的属性访问。引擎不会重新检查这个条件。规范化打印器可以消除呈现形式上的差异，却无法找回漏掉的守卫。规范化打印器加文本差异比较可以用更低的成本消除表中大部分差异，甚至可以说是全部 6 处差异。任何规范化器都无法在其他部分已匹配的项中，将包含 2 个合取项的条件与包含 3 个合取项的条件对齐。按单位元取模的匹配方式通过将漏掉的合取项与 eTrue 配对来完成对齐。在 permit 条件中，漏掉这个合取项会暴露出使策略在失败时放行的权限范围扩大问题。对于 Dogwood 的候选方案，代数和 3 条重写规则消除了 6 处呈现形式上的差异。剩余的分歧揭示出一个模式错误和一个漏掉的守卫。结合正确选项所得到的策略并非任何一个候选方案提供的策略。比较策略翻译：OpenShell 和 CEL。接下来的两个例子改编自 OpenShell 和 CEL 文章中的谓词。对于每个例子，我们都为同一需求构造候选翻译。这些是用于说明的编码，并非记录下来的 LLM 样本。OpenShell：方法与路径范围。OpenShell 的例子将网络权限建模为关于二进制程序、主机、端口、层、方法和路径的谓词。我们改编了该文章的简化版 SMT-LIB 模型，其中的路径条件是前缀测试。我们用这套术语表述以下需求：当方法为 GET，且路径以 /repos/NVIDIA/OpenShell/issues/ 开头时，允许 /usr/bin/gh 向 api.github.com 的 443 端口发出经过检查的 REST 请求。 拒绝所有其他请求。候选方案 A 要求使用 GET 方法，并要求路径具有该仓库的 issues 前缀。候选方案 B 使用 POST 方法和范围更广的 /repos/NVIDIA/ 前缀。其他检查的顺序也不同。在编码中，gh、github 和 https 分别表示前文所示的二进制文件、主机和端口。名称 issuePrefix 和 orgPrefix 标识这两个前缀。精确求解器返回：(anti-unify :size 21 :cr 0.1053 :completion exact (And (EqText binary gh) (EqText host github) (EqText layer rest) (EqText method (Variants GET POST)) (EqNumber port https) (Prefix (Variants issuePrefix orgPrefix) path))) 二进制文件、主机、端口和层的检查是共有的。由于 And 被声明为满足结合律、交换律和幂等律，它们的顺序差异消失了。两个 Variants 节点标明了两处相互冲突的解读：允许的操作和路径的范围。这里的需求确定了这两处选择。对于含糊的需求，同样的节点会向需求负责人提供两个具体的备选项，供其澄清。CEL：共享条件的适用范围。CEL 示例揭示了重构过程中丢失的一项生产环境检查。我们将这些表达式用作以下需求的候选翻译：仅当请求处于生产环境中，且其端口为 80 或 443 时，才允许该请求。// 候选方案 A (is_prod && port == 80) || (is_prod && port == 443) // 候选方案 B is_prod && port == 80 || port == 443 CEL 中 && 的优先级高于 ||，因此候选方案 B 只对端口 80 应用生产环境检查。我们用提供的布尔值和整数输入对表达式进行编码，以 isProd、port80 和 port443 表示相应的输入和字面量：(anti-unify :size 13 :cr 0.3636 :completion exact (Or (And (Eq port port443) (Variants isProd (Lit true))) (And isProd (Eq port port80)))) 端口 80 的分支是共有的。在端口 443 的分支中，(Variants isProd (Lit true)) 显示了缺失的生产环境条件。当 is_prod = false 且 port = 443 时，A 拒绝该请求，B 则允许该请求。差异将审查指向句子中的一个部分：“处于生产环境中”是否适用于两个备选条件。此示例假定 is_prod 作为布尔值提供，port 作为整数提供。在这些假设下，两个表达式都不会引发错误。该编码未对 CEL 错误或未知值建模，引擎也不会检查这些输入假设。CEL-Java 的验证框架可以借助 Z3 检查等价性和策略不变量。此类检查可以为解决分歧提供依据。反统一器本身不会判定哪种翻译符合需求，而两个候选方案共有的错误仍会表现为共有部分。实现与性能 该算法运行在 e-graph 上，这是一种存储一个项及所有已知与其相等的项的数据结构。E-graph（等价图）源于定理证明器中的同余闭包过程，并通过等式饱和技术在编译器优化领域得到推广，如 Willsey 等人在《egg: Fast and Extensible Equality Saturation》（POPL 2021）中所述。该引擎的 e-graph 增加了对满足结合律和交换律的运算符的原生规范化。对 e-graph 进行反统一也被 babble 用于抽象学习和程序压缩（Cao 等人，POPL 2023）。早期实现无法扩展到小型示例以外的规模。我们基于饱和技术的原型也在这一规模遇到了瓶颈。原生 AC 规范化、针对不同子节点的 AC 感知匹配以及直接搜索，使查询可以在不到一秒内完成。半持久化降低了重复查询的成本。原生 AC 规范化。在该引擎中，结合律、交换律和幂等律不是重写规则，而是数据结构的属性。满足结合律和交换律的（AC）运算符在插入时将其子节点存储为规范化的有序多重集（ACI 运算符则存储为规范化的有序集合）。因此，一个 e-node 就能表示一个项的所有重新结合形式和排列；对于幂等运算符，重复的子节点被视为一个。 在声明的定律下相等就是结构相等。基于重写的替代方法会在实际工作开始前，向 e-graph 中灌入指数级数量的等价副本。对不同子节点进行具备 AC 感知能力的匹配。针对多重集节点的模式匹配采用最大划分语义：它对节点中不同的子节点进行分支，而不是枚举重数的拆分方式，因此大量重复的参数不会导致组合爆炸。直接搜索，而非重写。反统一本身也没有被编码成重写规则。精确动态规划求解器（:algorithm exact）以最优方式求解联合分解问题。这里的“最优”是相对于其大小优先的目标、当前 e-graph 和配置的循环处理策略而言的。随时可用的蒙特卡洛图搜索（:algorithm uct，默认算法）可在任意模拟次数预算下返回迄今最好的答案。对于示例中的那一对输入，3,000 次模拟重现了精确最优解。两种算法都首先优化结果大小，然后在大小相同的答案中，偏好在共享骨架中保留更多结构的答案。半持久化。e-graph 支持 (push) 和 (pop) 快照，快照记录为稀疏差异，而非深拷贝。因此，恢复状态所需的工作量与快照后发生的改动量成正比，此外还需付出修复派生索引的成本。按改动量计费的恢复机制使引擎能够在同一张共享图上比较众多候选项。回溯搜索可以恢复到较早的状态，而无需复制整张图。经过验证的核心及其范围。e-graph 的底层容器层已通过 Rust 验证器 Verus 验证。得到验证的性质是：恢复操作会重现对应 (push) 时的状态（1,703 个验证条件，0 个错误）。反统一 crate 证明了其目标排序和下界引理，但完整求解器尚无端到端的精化证明。引擎可以为它推导出的每个等价关系记录一份论证（--proofs）。正如代码仓库所注明的，这些记录尚不是经过独立重放检查的证书。所有这些主张及其证据等级和撤回情况，都列在代码仓库的主张清单（doc/claims.md）中。原生规范化避免将等价的 AC 项实体化。针对不同子节点的匹配控制了重数，直接求解器避免将反统一编码为重写，而半持久化降低了重复查询的成本。在流水线中使用语义差异比较 同一种方法可以从两个候选项扩展到更大的样本。生成 N 个需求的候选形式化表达。将它们加载到同一张共享 e-graph 中，根据领域规则进行饱和处理，再通过成对相等性检查将它们聚类。在用户指南中规模更大的 Dogwood 研究里，五个样本归并为三个簇。仅在呈现形式上不同的候选项会在构建过程中进入同一个等价类。对各簇的代表项两两进行反统一。然后，在基于引擎输出构建的一层中，按照反复出现的 Variants 节点在共享骨架中的位置对它们分组。在该研究中，三个成对差异被归并为恰好两个待审核项。对每一项使用最简单的可用检查方式：模式验证、重放、输入输出示例对，或人工审核。借助 (push) 和 (pop) 快照，可以在不重建图的情况下测试提议的解决方案。暂时将 Variants 节点的一个分支断言为领域事实，再次运行差异比较，然后回滚。构建在该引擎之上的工具可以依据硬约束和软约束选择并修复一个完整候选项，例如使用针对变体空间的 MaxSMT 求解器。MaxSMT（模理论最大可满足性）寻找满足所有硬约束，同时满足尽可能多的软约束或使其总权重最大化的解。《Programming Z3》第 8 节介绍了这种优化形式。这项能力不属于当前引擎。图 2 总结了该流水线。 图 2：对候选形式化表达进行聚类、找出反复出现的分歧，并将每项分歧交由适当的检查方式处理的流程。聚类规模和审查项目数量来自用户指南中规模更大的 Dogwood 研究。在持续集成（CI）中使用语义差异预算。命令 (checkau A B :max_size N :algorithm exact) 在成功时不输出任何内容，并在反统一器超出预算时使程序失败。用户指南中打印出的每个结果都以这种方式固定，因此指南和引擎不会彼此偏离。同一命令也可用作回归检查关卡。为参考形式化表达和重新生成的形式化表达设置结果大小上限，并在反统一器超出上限时让流水线失败。该二进制程序遵循标准 shell 惯例：结果写入 stdout，诊断信息（ok --- N nodes）写入 stderr，任何检查失败时进程都以非零状态退出。差异结果还可以指导后续提示，或帮助向需求负责人提出问题。样本之间两两计算的 :cr 均值，为每项需求提供一个分歧分数。Variants 节点已经包含提出具体澄清问题所需的备选项，例如“你的意思是严格小于阈值，还是不大于阈值？”有多个候选结果时，对等价输出进行聚类，比较各聚类的代表结果，并通过验证、重放、示例或人工审查来解决反复出现的分歧。开始使用：构建本文所用修订版本的引擎，然后运行策略示例。以下命令选择包含拉取请求 103 中 OpenShell 和 CEL 示例的修订版本：git clone https://github.com/yaspar-org/semi-persistent.git cd semi-persistent git fetch origin 5a7969ae4ea88117a64faac4f42af5c358e213e2 git checkout --detach FETCH_HEAD cargo build --release # 工具链已自动固定；不需要 Verus # 本文的完整示例：./target/release/semi-persistent egraph/examples/au_policy_divergence.egg # Dogwood 策略差异示例：./target/release/semi-persistent doc/book/examples/20-dogwood-simple.egg # 构造的 OpenShell 和 CEL 翻译示例：./target/release/semi-persistent egraph/examples/au_openshell_policy.egg ./target/release/semi-persistent egraph/examples/au_cel_policy.egg # 你自己的公式：声明一个签名、两个项，并进行反统一：./target/release/semi-persistent MY_PROGRAM.egg 该引擎在 GitHub 上以 Apache-2.0 许可证发布。用户指南从基本项逐步讲到策略案例研究，测试套件直接从代码仓库运行其中的每个程序。附录 B 介绍了 antiunify 和 checkau 命令。如果你的工件语言有抽象语法树（AST）和等式理论，就可以比较其差异：声明代数，将领域恒等式表述为重写规则，然后求最具体的反统一器。如果你的策略使用 Cedar，无论是手写的还是为 Amazon Verified Permissions 生成的，同样的方法都适用。OpenShell 和 CEL 示例展示了如何编码其他策略构造，以及如何比较对一项需求的不同候选解读。关于作者 Ferhat Erata Ferhat 是 AWS AI Labs 的应用科学家。他将大型语言模型与形式推理相结合，以提高生成式和智能体 AI 的安全性与防护能力。他的工作包括自动形式化、经验证的代码生成，以及利用验证器反馈训练推理模型。他的进攻性安全研究包括从功耗轨迹逆向工程量子电路，以及检测后量子密码代码中的侧信道漏洞。在攻读博士学位之前，他已在业界工作 10 多年，期间联合创立了 UNIT Research & Development，领导开发了连接文本文档与形式模型的平台 ModelWriter，并协调了 EUREKA/ITEA 工业研究项目的国家级联合体。Ferhat 拥有耶鲁大学计算机科学博士学位。他的网站是 ferhat.ai。 Rémi Delmas Rémi 是 AWS 自动推理团队的一名首席应用科学家，常驻波士顿。他的工作涵盖 CBMC 和 Kani 等形式化验证工具，以及神经符号自动形式化和推理系统。加入 AWS 之前，他在巴黎的优步先进技术中心从事城市空中交通相关工作。再之前，他在法国航空航天研究机构 ONERA 工作了10年，开发并应用用于关键嵌入式系统设计与验证的形式化方法。在职业生涯早期，他曾在 Prover Technology 开发铁路控制系统的验证工具。他拥有图卢兹 ISAE-SUPAERO 的计算机科学博士学位。他的研究兴趣包括自动推理、神经符号推理系统、软件安全和优化。