Datalog：不动点引擎

purrdf-datalog 是确定性的、wasm32-clean 的 Datalog 求值：一个列式关系存储、一个会选择索引的规划器，以及一个半朴素不动点，不带任何环境 I/O、挂钟时间或随机数生成器。

它的存在使规则集成为_数据_，而不是手写的循环。purrdf-entail 把 RDF、RDFS、OWL 2 RL 与 D 演算声明为 DL 子句程序并在此求值，正因如此，推理报告才能携带实际运行的那个确切程序的契约哈希，而不是一句关于本应运行哪些规则的声明。

purrdf-datalog 由总括 crate purrdf 重新导出为 purrdf::datalog 模块——蕴涵接口携带它的类型（ReasoningReport 会交出一个 datalog::cache::ContractHash 与一个 datalog::seminaive::BudgetReport），因此对这些类型做匹配的使用方不需要再额外依赖 purrdf-datalog。只有当只需要不动点本身、构建中不含其他任何 purrdf 接口时，才直接依赖该 crate（purrdf-datalog = "…"）。

唯一的规则 IR：DL 子句

每条规则都具有如下形态

U₁ ∧ … ∧ Uₙ  →  ∃ȳ. (C₁ ∨ … ∨ Cₘ)

其中每个析取项 Cᵢ 本身是头部原子的合取。这一种形态就容纳了全部五种头部形式——原子式（普通的 Datalog 规则）、存在式、析取式、合取式以及空（false）——因此，像 A ⊑ ∃r.C 这样降为带一个_共享_见证的 ∃y. (r(x, y) ∧ C(y)) 的公理，是一条规则，而不是两条互不相关的规则。

半朴素求值器执行原子头和不含存在量词的合取头。多个头共享一次体求值；每条记录的推导都标明原始子句索引和头序号。递归、因子投影与分层否定使用同一个求值器。谓词须等到所有生成规则完成后才算完备，即使共享规则提前产生了较高层的头。独立证明检查所选的头序号；第 2 版编码显式携带这一序号。

存在式头、析取头和假头会被点名拒绝。存在形式并不会因这一拒绝而丢失：受限 chase 会消费它，生成按前沿寻址的 Skolem 见证，四个存在式 RDF/RDFS 模式正是由此触发，规则清单也因此显示为完整。永远不会发生的是替代项泄漏到答案中——上层的蕴涵层会在物化边界处扣留每一个提及见证的结论，并报告这一扣留，而不是凭空编造调用方并未要求的答案。

确定性

使用 Guard::not_equal("?left", "?right") 可进行原生项不等比较，无需回调。它精确比较已绑定项的身份，不进行数值强制转换。调用方定义的 Guard::filter("!=", ...) 仍是回调：决定原生行为并参与子句摘要的是操作种类，而不是名称。独立证明检查器根据已检查的前提重新求值原生顶层过滤器。

• 每个键下的行保持插入顺序；arrangement（排布）是已排序的；任何映射的迭代顺序都不会到达输出路径。
• 计划以一个 BLAKE3 摘要进行内容寻址，该摘要涵盖规划器版本、调用方的契约哈希以及子句程序的规范摘要。缓存由调用方持有，绝不是进程级全局变量——全局缓存会使答案依赖于求值历史。
• 凡是并行化的工作，都使用按源顺序归约的带索引 par_iter/par_chunks，从不使用 par_sort 或 par_bridge，并在 wasm32-unknown-unknown 上退化为内联顺序执行。

相同的输入在每个目标上都产生逐字节相同的输出。

上限只会拒绝，从不截断

三个上限约束每一次运行所持有与枚举的内容。调用方通过 EvalOptions 选择所有上限，每项都有明确的默认值：

EvalOptions::without_term_arena_limit 移除词法形式字节数的逻辑上限。实际存储准入仍然适用。预算报告提供有效上限，该值也参与契约哈希。

存储事实准入在改变存储前检查每一次唯一插入。拒绝时，BudgetReport::stored_facts 报告已准入的数量，observed_stored_facts 报告第一次被拒绝的插入，恰好多一个。重复候选不再消耗存储事实额度。

存储事实的默认值之所以不同，是因为存储所在的内存不同：wasm32 上的求值与页面的其余部分共享同一块线性内存，其默认值就是此前该上限尚为固定值时所有目标平台共用的那个值。原生进程能够持有大得多的最小模型，而一个按浏览器确定的上限曾在那里拒绝普通的、会终止的规则集——仅仅是一条把 70,000 条 ex:p 三元组逐条复制到 ex:q 的规则。默认值在编译时依据目标架构选定，绝不经由 Cargo feature。

连接步数的默认值在所有目标平台上相同。求值器在展开候选项之前，从轮次共享的预算池中预留该候选项的额度；额度耗尽时停止继续展开。这个工作量上限与保留存储分开：提高它可能允许更大的中间缓冲区，但不会提高存储事实或项存储区的上限。程序若需要更多候选工作量，调用方必须显式声明该额度（命令行上为 --max-join-steps）。

阻止发散规则的并不是连接步数上限。一条每轮生成一个新焦点节点的 SHACL 形状规则，只会针对输入发生变化的焦点节点重新执行，而不是针对此前的每一个焦点节点。项生成有独立的防护：新项长度有界时，由生成新项的轮数上限约束；保留的词法形式增长时，由项存储区上限约束。

上限只能拒绝。在上限之内的运行返回程序的最小模型，在任何允许它完成的上限下都是同一个模型。只提供完整结果的调用越过上限时会返回拒绝。保留状态的 EvaluationSession 通过单独的 PartialModel 提供经认证的事实。每个传入相同选项的调用方都会得到相同的答案或相同的拒绝；生效的上限被纳入结果的契约哈希，因此在一组上限下、或在某个目标平台的默认值下计算出的推理闭包，绝不会冒用另一组的身份。连接步数还取决于求值器的计划，因此针对某个版本收得过紧的上限，可能会在下一个版本中拒绝；留有余量的上限则不会改变一个已完成的答案。

Datalog 求值器不读取时钟。宿主可以将基于挂钟时间的截止期限或取消标志适配为与答案无关的 StopSignal 接口。信号在会话入口和轮次边界处被轮询。已停止的会话可以使用新的信号继续执行；新旧信号都不会改变完成后的模型。

模型输出、证明与工作量计数

普通求值默认使用 DerivationMode::ModelOnly。需要导出推导时，设置 EvalOptions::with_derivation_mode(DerivationMode::Record)。禁用记录时，Evaluation::derivations 返回 None；启用记录但没有推导出任何内容时，返回 Some([])。证明构造以 ProofError::DerivationsNotRecorded 拒绝仅有模型的结果。记录不会改变最小模型、内部规范见证的优先选择或候选计数。

Evaluation::work 将唯一输入事实和已提交的事实插入与物理候选准入分开计数。对于普通且已完成的分层运行，事实计数与连接计划无关。候选计数可能随规划器变化；报告给出规划器版本，调用方可以比较每个已提交事实对应的候选数。调度撤回可能导致稍后再次提交同一事实，因此产生另一次提交事件。

EvalOptions::with_round_execution(RoundExecution::Sequential) 为一次调用选择直接执行路径，不改变全局线程池。两种调度策略使用同一个求值器、按程序顺序归并并排序提交，保持相同的模型和已记录推导。

evaluate_guarded 等只提供完整结果的入口在拒绝时不返回模型。错误会点名该上限、观测到的与允许的数值，以及用于提高该上限的参数；蕴涵层通过 EntailError::Evaluate 或 EntailError::Chase 报告这些错误。

经认证的部分模型与续体（continuation）

EvaluationSession::new 接管输入存储的所有权，并借用不可变程序和 guard（守卫）求值器。它的 SessionContext 要求调用方提供规范的快照、守卫语义和证据机制身份标识。会话还会纳入所编写程序的规范身份标识。保留其 binding() 值，并将该绑定原样传给 resume，同时提供累计上限和可选的停止信号。调度方式可以变化；推导记录模式保持不变。任一绑定坐标发生变化时，续算会在执行前被拒绝。原始词典在每次公开读取和续算的边界处检查其绑定源是否仍然有效。

ResumeProgress::Paused 携带原始的资源或停止拒绝。partial_model() 借用初始事实和经证明已发布的事实、实际已完成的工作量、可选推导，以及每一层的 Complete、SoundLowerBound 或 Withheld 状态。前面的层全部完成之前，执行不会进入后续层，因此否定不会观察到尚未完整的下层关系扩展。后续依赖这些层的结论暂不提供。部分结果的身份标识在单独的哈希域中纳入原始规范绑定、governor（执行调控器）和消耗量。运行时的项句柄和行句柄绝不参与该身份标识。

提高上限或提供新的停止信号，即可继续执行已保留的连接、守卫、规则／轮次工作、排序后的事实发布以及当前增量。已完成的工作只计数一次；在相同的已拒绝额度下重试，不会增加已完成的工作量或守卫调用次数。EvaluationProofs::of_partial 为已记录且已发布的推导构造证明，并由完整模型所使用的同一个独立检查器校验。源和守卫失败仍是硬失败，并阻止进一步续算。

只有 ResumeProgress::Complete 才允许 take_complete() 返回 Evaluation。尚未完成时提出该请求，不会改变会话状态。完成后的模型、推导和成功的连接步数，与在最终选项下不间断运行的结果相同；其演算身份标识使用普通的 contract_hash_with 配方。续体是在进程内持有状态的所有者，没有序列化令牌形式。