用反合一（anti-unification）对形式化策略做语义 diff

审查代码时，你会从 diff 开始。你不会靠肉眼比较两个 3000 行的文件并指望找出每一处改动。形式化策略（policy）的比较可能更难，因为文本 diff 常常突出那些不影响语义的句法改动。交换两个合取项的顺序、交换等式两边、或使用等价的谓词，文件的大部分看起来都像是被改动了。而真正的行为变化，比如需求写着 and 的地方却出现了 Or，可能淹没在这些噪音中。

语义 diff 会展示两个策略的相同之处和不同之处。本文所用的开源引擎使用反统一来计算这种 diff，它为两个表达式找到最特化的公共模式。Plotkin 的1970 年论文给出了经典表述。该引擎在 e-graph 上工作，e-graph 会记录已知相等的表达式。我们提供支撑这些等式的代数定律和领域规则，例如把外部目的地与“非内部”的目的地等同起来。结果会把相同部分只展示一次，并为每个不同部分保留两个版本供审查。如果没有剩余差异，则在这些定律和规则下两个策略等价。当规则或搜索不完整时，剩余差异可能反映的是引擎尚未发现的等价关系。

一个应用场景是自动形式化。自动形式化是把自然语言翻译成形式语言。假设你想把需求转化为 SMT-LIB——这是 Z3 和 cvc5 等 SMT（可满足性模理论）求解器的标准输入语言——或者转化为 Cedar 或 Dogwood，以控制软件系统中的授权。大型语言模型（LLM）会根据散文式文本生成形式化产物。模型负责撰写产物，但不参与计算 diff。运行模型两次，它可能生成两种不同的形式化结果，而且没有真值可以判断哪一个是正确的。语义 diff 可以显示它们在哪里一致、哪里不同。通过改变模型、提示词或采样温度生成更多候选结果，比较它们就能看出哪些部分保持不变、哪些部分有变化。先审查有变化的部分。

需求也可以转化为OpenShell 沙箱策略或 通用表达式语言（CEL）表达式。OpenShell 使用 YAML 来描述智能体的文件系统和网络访问权限。CEL 嵌入在应用中用于求值表达式，包括策略条件。这些语言和格式所能表达的内容各不相同，但对它们的任何翻译都可能在条件、作用域或事件上出现分歧。下表给出了一些示例性的分歧：

在每个已完成的示例中,我们都在同一策略背景下比较同一需求的不同翻译。我们将相关语法编码为项,并声明比较中用到的等式。引擎读取这些编码。它并不导入来自那四种格式的原生策略。

这个想法是 Farquhar 等人在《自然》(Nature, 2024) 中描述的 语义熵 的形式化方法版本。该方法采样多个自然语言答案,把相互蕴含的答案聚类,并报告一个单一的数字。对于形式化输出,反合一能保留更多信息。它不是只返回一个分数,而是识别出共享结构和每一处分歧。

反例有助于解释分歧的后果。SMT 求解器可以找到一个具体赋值,它满足其中一个公式却违反另一个。审查者随后可以追踪该赋值在公式中的传播,以理解相互冲突的决策。反合一器提供了另一种视角:它组织共享结构和相异的片段,而无需发起 SMT 查询。求解器或策略校验器可以帮助解决这些片段。我们假设你能阅读 S 表达式语法,如 SMT-LIB 中的语法,并知道什么是授权策略。E 图和反合一会在出现时加以解释。

当多个翻译在需求的某一部分上达成一致时,diff 只显示该部分一次。在有分歧的地方,它保留各备选项以便审查。

语义 diffing 如何表示分歧

假设一个策略生成管线为这条需求交给你两个候选规则:发送到外部目的地的敏感数据必须加密。

这两个规则是否相同并不明显。条件被重新排序了,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)添加一行 function。其中 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,运行到饱和(直到没有规则再产生新的等式),然后再次进行 diff:

(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 表示在既定等式下完全一致。

经过前述重写后，两个输入各有七个节点，结果有八个节点，得到 (8 - 7) / 7，约为 0.1429。若把两个完整策略保存在单个 Variants 节点中将使用十四个节点，得到 (14 - 7) / 7 = 1。这是无共享时的参考值。

得分为 1 是参考值，而非上限。搜索可能使用比已知最小输入形式更大的等价形式。因此，当结果大于两者大小之和时，得分会超过 1。例如，若两个最小输入形式各为十个节点而结果有二十三个节点，比值为 (23 - 10) / 10 = 1.3。

:completion 字段在搜索空间被穷尽时报告 exact，而在默认的 anytime 搜索（一种蒙特卡洛搜索，实现章节中有描述）在穷尽搜索空间之前达到其 playout 上限时报告 budget。

较低的 :cr 表示在既定等式下输入共享更多结构。它并不能证明正确性：两个候选可能共享同一个错误。熵分数用一个数字概括差异程度。完整的语义差异分析还能定位候选之间的分歧位置，并在 Variants 节点中保留两种备选。

语义差异分析只忽略被既定等式覆盖的差异。普通的语法反统一器在本例中也会报告这次重排。接下来三节将展示如何声明代数并添加领域恒等式。

反统一器将共享结构存储一次，并用 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-expression 文件（按惯例为 .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 元素正是让 diff 能够对齐一方有而另一方缺失的合取项的关键：缺失的合取项与 (Lit true) 配对，而不是导致整个 And 表达式无法对齐。两个案例研究都依赖这种恒等对齐。

:assoc-comm-idem 使重排、重组和重复的操作数等价。:identity 让 diff 将缺失的操作数与运算符的中性元素对齐。

两个策略缺陷的实例演算

这个贯穿全文的示例以 egraph/examples/au_policy_divergence.egg 的形式随代码库一起发布。考虑一条策略语句：

仅当源存储桶已启用版本控制且目标存储桶位于已批准的 Region 中时，跨 Region 复制请求才被允许。如果对象带有 confidential 标签，目标账户和源账户必须相同，并且必须使用客户管理的密钥进行服务器端加密。不超过分片上传阈值的对象直接复制。更大的对象需要进行分片复制。

两个人，或同一模型的两次独立运行，产生了它的两种形式化结果（文件中的 formulaA 和 formulaB）：

(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))))

(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))))

有五处文本差异。其中三处是表现形式的：合取项被重排了，Eq 的参数被交换了，并且 approvedRegion 被显式展开为两个 AWS Region（us-east-1 和 eu-west-1）。另两处涉及不同的运算符：在 confidential 子句中，一个 And 变成了 Or；在大小阈值处，Lte 变成了 Lt。两种编码的统一 diff 将其 28 行中的 18 行标记为已更改（图 1，textual-diff 面板），并且没有指明五处差异中的哪几处改变了含义。以下是两种编码的精确反统一器：

(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)))))))

五处差异中有两处消失了。合取项的重排被吸收，因为 And 被声明为可结合、可交换且幂等（ACI）。交换过的 Eq 参数在两种读法中打印顺序相同，因为 :comm 已将其规范化。两者都不改变含义，因此都不被报告。

confidential 子句使用了 Or，而需求说的是和。编码 A 要求同时满足相同账户检查和使用客户管理密钥的服务器端加密。编码 B 则接受任意一个。引擎通过它们的中性元素将 A 的合取与 B 的析取对齐，因此分歧以两个相邻的 Variants 节点的形式呈现出来。在每个节点选择第一个子节点即可重构 A：Or 折叠为普通等式，而 sseCmk 仍然是一个强制合取项。在每个节点选择第二个子节点即可重构 B：强制的 sseCmk 弱化为 (Lit true)，仅作为 Or 内的一个备选而存在。这两个 Variants 节点共同表明，编码 B 仅凭服务器端加密即可通过，因此允许对机密对象进行跨账户复制。

你或许会以为 sseCmk 是共享而非重复出现的。然而，一阶反合一无法对连接词本身进行泛化，因此 And 与 Or 的对比迫使拆分为两条对齐。恒等对齐仍然只共享一次那个五节点的等式。精确求解器的穷举搜索没有找到更小的形式，而打印出的结果比把两个子句完整放在同一个 Variants 中小一个节点。

添加域 rewrite 并再次运行 diff。Region 的 Variants 节点并不是 bug。它反映的是缺失的域知识：在这个部署中，被批准的 Region 恰好就是那两个。把它声明为一个 rewrite，进行饱和，然后再次 diff：

(rewrite (approvedRegion r) (Or (usEast1 r) (euWest1 r)))
(run 3)
(antiunify formulaA formulaB :algorithm exact)

Region 的差异被移入了共享主干，:cr 从 0.5862 降至 0.4000。完整结果就是图 1 的语义 diff 面板。恰好剩下两处分歧：被削弱的保密条款和阈值。B 的 Lt 是严格的，因此恰好位于 multipartThreshold 的对象在 A 下被直接复制，而在 B 下走多部分路径。分歧仅限于 Ite 条件。两个分支都位于共享主干中。剩下的两处差异都是真实存在的 bug，需要授权审查者来解决。代数和一次域重写解释了其他差异。同一个文件还运行了 anytime 搜索 (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 的墙钟时间。Get started 部分展示了相同的命令。

 (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：同一对编码在 diff 与反合一下的表现。左侧，文本 diff 标记了 28 行中的 18 行（删除、新增）。右侧，一次域重写将共享结构移入灰色主干，高亮的 Variants 把剩余差异限定在被削弱的保密条款和严格阈值上。语义 diff 面板为一行较长内容做了换行以适应显示

应用声明的代数和一次域重写后，五处文本差异缩减为两处语义分歧：被削弱的保密条款和严格的大小阈值。

Cedar 与 Dogwood 策略的语义 diff

在授权策略中，一个被删除的守卫会扩大允许的范围，可能导致策略 fail open（失败时放开）。Cedar 是 Amazon Verified Permissions 背后的开源授权策略语言。Dogwood 通过时间条件扩展了 Cedar 授权策略，用于对智能体进行运行时验证。其时间子语言使用记录的事件历史来守卫某个操作。该引擎并不求值 Dogwood 策略，而是在声明的代数下对它们的抽象语法做 diff。验证（schema 检查）和重放（用记录的事件历史对策略求值）仍是 Dogwood 的职责。引擎的用户指南中有一个完整章节，对一个需求 diff 了两个独立编写的 Dogwood 候选方案：

智能体可以向 /deploy 发送 POST，但仅当健康检查在过去 15 分钟内已返回 200。

候选 A 保留了两个请求守卫（方法和路径），却从请求事件中读取状态码，而那种事件类型根本没有这个字段。候选 B 使用了正确的响应事件，但丢掉了 /deploy 路径守卫。在任何匹配的健康检查之后，B 还允许从 POST 到 /admin/purge-all 的访问。候选之间还有六处表述上的差异，全部被声明的代数或一个三条规则的比较理论吸收：

比较理论由三条可见的重写组成，而非一个隐藏的规范化过程：

(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，并且在原本共享的策略主干中恰好有两处不一致：

(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))))

对每处不一致使用最简单可用的检查。两处二元不一致给出四个候选补全。Dogwood 验证通过拒绝两个请求补全（“谓词 …… 提及了字段 output.status_code，但该字段未在该事件上声明”）在无需人工审核的情况下解决了第一处。第二处不一致是同一性对齐：候选 A 的路径守卫与 eTrue 配对，表明候选 B 遗漏了该守卫。需求将其解决（保留守卫），并且一次覆盖两个决策点的重放显示了后果：在一次健康检查之后，候选 B 允许偏离目标的 POST，而修复后的策略则拒绝它。把 B 的事件类型与 A 的守卫结合，产生了一个两位候选都没有写出的策略。若只是在两个候选之间做选择，就会保留两个缺陷之一。

交换律带有侧条件，而引擎并不检查它。Cedar 的 && 会短路，因此只有在两个操作数都不会引发错误时，交换它才是可靠的。因此比较依赖于验证来排除依赖顺序的错误，例如只有在 has 守卫之后才安全的属性访问。引擎不会重新检查该条件。

规范化打印器可以消除表述差异，但无法找回被丢弃的守卫。一个规范化打印器加上文本 diff，可以以更低代价吸收上表中大部分——可以说全部——六处差异。没有任何规范化器能在一个本已匹配的项内部，把两合取条件与三合取条件对齐。按单位元做匹配则通过把被丢弃的合取项与 eTrue 配对来对齐它们。在一个 permit 条件中，被丢弃的合取项暴露出使策略失效开放（fail open）的扩大。

对于 Dogwood 候选，代数和三条重写消除了六处表述差异。剩余的不一致暴露出一个模式错误和一个被丢弃的守卫。把正确的选择结合起来，就得到一个两位候选都没有给出的策略。

比较策略翻译：OpenShell 与 CEL

接下来两个示例改编自 OpenShell 和 CEL 文章中的谓词。对每一个，我们都为同一需求构造候选翻译。这些是示意性的编码，并非记录下来的 LLM 样本。

OpenShell：方法与路径范围。OpenShell 示例将网络权限建模为基于二元、host、port、layer、method 和 path 的谓词。我们采用该文章简化后的 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 时，允许该请求。

// Candidate A
(is_prod && port == 80) || (is_prod && port == 443)

// Candidate 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 是一种存储一个项以及所有已知与其相等的项的数据结构。E-graph（等价图）来自定理证明器中的合一闭包（congruence-closure）过程，并通过等式饱和（equality saturation）在编译器优化中得到推广，如 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 以及配置的循环策略而言。一种 anytime 的蒙特卡洛图搜索（:algorithm uct，默认方式）对于任意 playout 预算都会返回其最佳答案。在示例中的那一对上，3,000 次 playout 就能重现精确最优解。两者都首先优化结果大小，其次在大小相同的答案中，优先选择在共享主干中保留更多结构的答案。

半持久化。该 e-graph 支持将 (push) 和 (pop) 快照记录为稀疏差异而非深拷贝。因此恢复一个状态的代价与实际变更量成正比，外加修复派生索引的开销。代价成正比的恢复让引擎可以在同一个共享图上比较众多候选方案。回溯式搜索可以恢复较早的状态，而无需复制整个图。

经过验证的核心及其范围。e-graph 的底层容器层在 Verus（一个 Rust 验证器）中经过验证。所验证的性质是：restore 能复现与相应 (push) 匹配的状态（1,703 个已验证条件，0 个错误）。反统一 crate 证明了其目标顺序和下界引理，但完整求解器尚未具备端到端的精化证明。引擎可以为其推导出的每一个等价关系记录一条论证（--proofs）。正如仓库所指出的，这些记录尚不是可独立重放校验的证书。所有这些声明，连同证据等级和撤回记录，都在仓库的声明清单中（doc/claims.md）。

原生规范化避免了等价 AC 项的具体化。去重子节点匹配控制了多重性，直接求解器避免了把反统一编码为重写，半持久化则降低了重复查询的代价。

在流水线中使用语义差分

同样的方法可以从两个候选扩展到更大的样本。生成 N 个需求的形式化候选。将它们加载到一个共享的 e-graph 中，在领域规则下进行饱和，并使用成对相等性检查对它们进行聚类。在用户指南规模更大的 Dogwood 研究中，五个样本坍缩为三个聚类。仅在表现形式上不同的候选会在构建期间加入相同的等价类。对聚类代表进行两两反统一。然后，在构建于引擎输出之上的一层中，按照 Variants 节点在共享主干中的位置对反复出现的节点进行分组。在该研究中，三个成对 diff 正好缩减为 两个 审查项。为每个审查项使用最简单的可用检查：模式验证、重放、示例 I/O 对，或人工审查。

利用 (push) 和 (pop) 快照，无需重建图即可测试提议的解决方案。临时将 Variants 节点的一个分支断言为领域事实，再次运行 diff，然后回滚。构建在引擎之上的工具可以根据硬约束和软约束选择并修复完整的候选，例如通过在变体空间上使用 MaxSMT 求解器。MaxSMT（maximum satisfiability modulo theories，带理论的最大可满足性）寻求一个满足所有硬约束、同时满足尽可能多的软约束（或最大化其总权重）的解。《Programming Z3》第 8 节描述了这种优化形式。该能力并不包含在当前引擎中。图 2 总结了整个流水线。

图 2：一个用于对候选形式化进行聚类、定位反复出现的分歧，并将每个分歧路由到适当检查的流水线。聚类大小和审查项数量来自用户指南规模更大的 Dogwood 研究

在持续集成（CI）中使用语义 diff 预算。命令 (checkau A B :max_size N :algorithm exact) 在成功时不输出任何内容，当反统一结果超出预算时使程序失败。用户指南中的每个打印结果都以这种方式固定，因此指南与引擎不会产生偏差。同一命令还可以作为回归门槛。为参考形式化和重新生成的形式化设置最大结果大小，当反统一结果超出时使流水线失败。该二进制程序遵循标准 shell 约定：结果输出到 stdout，诊断信息（ok --- N nodes）输出到 stderr，任何检查失败时进程以非零值退出。

diff 还可以用于引导后续的提示词或向需求负责人提出问题。跨样本的平均成对 :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        # toolchain auto-pinned; Verus not required

# The worked example from this post:
./target/release/semi-persistent egraph/examples/au_policy_divergence.egg

# The Dogwood policy-diff example:
./target/release/semi-persistent doc/book/examples/20-dogwood-simple.egg

# The constructed OpenShell and CEL translation examples:
./target/release/semi-persistent egraph/examples/au_openshell_policy.egg
./target/release/semi-persistent egraph/examples/au_cel_policy.egg

# Your own formulas: declare a signature, two terms, and antiunify:
./target/release/semi-persistent MY_PROGRAM.egg

该引擎已在 GitHub 上以 Apache-2.0 许可开源。用户指南从基础术语逐步深入到策略案例研究，测试套件可直接从仓库运行指南中的每个程序。附录 B 记录了 antiunify 和 checkau 命令。如果你的制品语言具有抽象语法树（AST）和等式理论，你可以对其进行 diff：声明代数结构，将域上的恒等式表述为重写规则，然后求出最具体的反统一器。如果你的策略是 Cedar——无论是手写的，还是为 Amazon Verified Permissions 生成的——同样的方法也适用。OpenShell 和 CEL 示例展示了如何编码其他策略结构，并比较对某个需求的不同候选解读。

关于作者