这份终点把魔集查询改写和删除与重推接在同一个可执行例子上。你要解释的不只是最后四个或两个答案，还包括请求怎样产生、错误支持怎样消失、替代证明怎样恢复，以及每一个中间集合为什么属于当前阶段。
下载标准库参考器，在文件所在目录运行：
python3 foundation-magic-dred-check.py > magic-dred.json
python3 -O foundation-magic-dred-check.py > magic-dred-optimized.json
cmp magic-dred.json magic-dred-optimized.json成功输出的 status 为 PASS，最后的 regressions 为4个绑定边界、720次查询比较、900批增量更新。cmp 不应输出差异。参考器不使用会被 -O 移除的 assert，也不在 dred 中调用全量求值；用于比对的有限地面枚举器只由测试层调用。程序只向标准输出写 JSON，不改你的输入文件。
本文以 R 表示原可达关系，Q 表示 @a:R:bf，M 表示 @m:R:bf。源程序是正长度可达性，因此只有存在非空环的节点才有 R(x,x)，不会无条件补一条自反边。所有关系都是集合，规则与查询在更新期间固定。
任务一：把查询需求真的编译成规则
使用源规则 R(X,Y)←E(X,Y) 与 R(X,Z)←R(X,Y),R(Y,Z)，查询 R(a,Y)。输入边完整列为 a→b、b→c、c→b、c→d、a→e、e→d、u→v、v→w、w→u。交出 magic_rules 和 adornment_trace，并把第二条源规则中的两个调用分别标明：调用前已经绑定哪些变量，绑定值来自哪个前缀。
验收规则恰为四条：M(a)←；Q(X,Y)←M(X),E(X,Y)；M(Y)←M(X),Q(X,Y)；Q(X,Z)←M(X),Q(X,Y),Q(Y,Z)。第一递归调用的 M(X)←M(X) 可以省略；第二调用的需求绑定变量是 Y。不能把查询常量 a 直接复制给每个递归调用，否则会漏掉从中间点继续的路径。
交出同步求值每一轮新出现的事实。参考器先读旧集合，再把本轮候选一并加入，因此不能把同一轮刚出现的事实提前用于其他规则：
- M(a)
- Q(a,b)、Q(a,e)
- M(b)、M(e)
- Q(b,c)、Q(e,d)
- Q(a,c)、Q(a,d)、M(c)、M(d)
- Q(c,b)、Q(c,d)
- Q(b,b)、Q(b,d)、Q(c,c)
- 空集，停止
原程序共有20条 R，改写程序有11条 Q 加5条 M。解释为何 M(d) 存在却没有 Q(d,y)，为何 u、v、w 的九条可达事实没有对应 Q，以及为何仍不能声称从未读取这一分量的输入。最终只选择 Q 的 a 行，得到 (a,b)、(a,c)、(a,d)、(a,e)。
成本证据也要分开。原程序852次 row_tests，改写程序811次；两者都使用同一简单同步匹配器。这个计数不含每次匹配重建、排序关系索引及集合和 JSON 工作，不能据此宣布通用加速比例。
任务二：让参数交换与空绑定暴露错误
在下载文件旁保存下面的短驱动，或直接从终端执行。它通过公开函数处理另一个真正不同的绑定方向，而不是检查主例的常量答案。
python3 - <<'PY'
import importlib.util
s = importlib.util.spec_from_file_location('md', 'foundation-magic-dred-check.py')
m = importlib.util.module_from_spec(s); s.loader.exec_module(m)
a = m.atom
rules = (
(a('P','?X','?Z'), (a('E','?X','?Y'), a('Q','?Z','?Y'))),
(a('Q','?U','?V'), (a('F','?U','?V'),)),
)
base = {a('E','a','b'), a('F','c','b'), a('F','d','z')}
g = m.magic_rewrite(rules, {'E':2,'F':2}, 'P', 'bf', ('a',))
for rule in g['rules']: print(m.show_rule(rule))
j = m.materialize(g['rules'], {'E':2,'F':2}, base)['idb']
print('adornments', g['adornments'])
print('answers', sorted(m.select_answers(j, g['answer_predicate'], 'bf', ('a',))))
PY验收必须出现 ('Q','fb')，答案为 [('a','c')]。E 匹配后 Y 已知而 Z 未知，所以 Q(Z,Y) 的第二列绑定。若错误地按 bf 请求第一列为 b，给定 F 没有这一行，便会漏掉正确的 c。
再把主例查询改为 ff，绑定值传空元组 ()。需求种子是 M()，不是不存在。正常结果应为完整20条 R 的对应答案；然后把生成程序中那个空体需求种子替换为 M()←M()，保留其他规则，重算应得空答案。自环只保留谓词声明，不会从空集合产生事实；若直接删掉唯一的 M 定义，参考器会按未定义体谓词拒绝程序。这是一个能击穿“无绑定就不必放种子”的反例。
最后执行 Ready()← 的零元查询，模式为空字符串、绑定值为 ()，EDB 为空。输出仍应含 Ready() 对应答案。另用 P(a)← 查询 P(z)，应为空；用 P(X,X)←E(X,Y) 与 E(a,b) 查询 P(a,Y)，应只返回 (a,a)。交付时解释这三例分别检查零元真值、常量守卫和重复变量相等，不能把它们合并为一个“空输入测试”。
任务三：删除输入事实，再恢复替代证明
读取 ordinary_delete。删除的是 E(a,b)，旧物化仍是原程序全部20条 R。过删前沿必须依次为 {E(a,b)}、{R(a,b)}、{R(a,c),R(a,d)}。交出这三批的规则见证，例如第三批的 R(a,c) 来自已受影响的 R(a,b) 与旧 R(b,c)。过删阶段必须还能访问完整旧事实，不能用已经删空的关系重新找旧依赖。
重推时的当前集合没有 R(a,b)、R(a,c)、R(a,d)，但仍有 R(a,e)、R(e,d)。因此先恢复 R(a,d)，下一轮无变化。最终18条 R 中，a 行只剩 d、e。说明为什么 R(a,d) 原本有好证明也仍进入过删，以及为什么这不会损害最终正确性。
再读取 wrong_peeling_extra，必须恰为 R(a,b)、R(a,c)。错误版本从旧结论出发，只反复去掉没有任何局部支持的事实；留下来的两个错误事实互相支持。写出两条支持实例，并指出它们的有限证明树缺少哪条输入边。不能仅说“有环所以错”：b、c 的真实可达环仍然正确，错误的是从 a 进入该环的依据已消失。
旧成功实例数为55，重推实际体成员测试为14。把这些数与过删3条、重推1条、净删除2条分别列出；它们测量不同对象，不能相互替代。
任务四：需求撤回与重插入必须可逆地解释
读取 magic_delete，交出以下完整过删前沿，不要只过滤 Q 的 a 行：
- E(a,b)
- Q(a,b)
- Q(a,c)、Q(a,d)、M(b)
- Q(b,b)、Q(b,c)、Q(b,d)、M(c)、M(d)
- Q(c,b)、Q(c,c)、Q(c,d)
第一批为 EDB，后四批共12条 IDB。删除完暂时只有 M(a)、M(e)、Q(a,e)、Q(e,d) 幸存。下一阶段同一轮恢复 Q(a,d) 与 M(d)：前者由 Q(a,e)、Q(e,d) 支持，后者由 M(e)、Q(e,d) 支持。因此不需要等 Q(a,d) 新加入后才提出 M(d)。下一轮为空，整个新物化是6条 IDB。
对照原查询全量重算，答案仍为 (a,d)、(a,e)；再对生成程序全量重算，全部6条 IDB 也必须相等。解释为什么只做第一项比较不足以发现冻结旧需求表的错误。
现在把 E(a,b) 插回。reinsertion 的每批新增 IDB 依次为 Q(a,b)；M(b)；Q(b,c)；Q(a,c)、M(c)；Q(c,b)、Q(c,d)；Q(b,b)、Q(b,d)、Q(c,c)；最后空集。M(d) 与 Q(a,d) 在删除后的状态中已经存在，所以不应再次列为新增。结束时恢复最初的16条 IDB，且查询答案恢复四个。
任务五：验证批次语义，而不是只测一条删除
cancelled_update 把同一个旧 E(a,b) 同时列入删除和插入。按先删后插的接口，实际删除与实际新增均为空，旧20条 IDB 原样保留，old_instances 为0。这只表明无需枚举旧成功实例；输入检查、集合规范化与返回值复制仍有工作。
new_values_batch 则真正删除 E(a,b)，并插入 E(d,fresh)、E(fresh,a)。先得到任务三的18条删除后物化，再开始新增。新常量 fresh 以前不在活跃域中，不能靠旧成功实例枚举出相关新结论。最终原程序有37条 R，其中 a 能到 a、d、e、fresh，却仍不能到 b 或 c。
独立验证这37条的结构：a、d、e、fresh 构成四节点强连通分量，给出16条内部可达；b、c 仍互相可达，二者各能到自身与对方及上述四节点，共12条；u、v、w 分量仍给出9条，总数为16+12+9。这里的自达由非空环证明，不是额外加入的自反闭包。
交付至少一个你新写的固定程序与连续混合更新序列，覆盖相互递归、替代 EDB 支持、重复体原子或零元关系。每一批都把新状态与从新 EDB 开始的有限地面全量重算比较。不得把任意 IDB 结论作为删除参数，也不得把已经错误的旧状态传入，再宣称算法应自动修复它。
交付清单与可重复检查
提交生成规则、逐调用绑定来源、原始与生成程序的每轮求值、实际 EDB 变化、完整过删与重推前沿、净结果、两种全量对照，以及故意错误版本的具体多答。结果为集合，序列只用于展示算法轮次；同一批内部的显示顺序没有声明语义。
参考器的主算法与地面枚举对照器采用不同匹配路线，但有限回归不能代替证明。验收还应检查公式与代码的同一前置条件：固定正安全程序、集合 EDB、精确旧最小物化、固定查询，以及新增时允许新常量。若把条件改成否定、聚合、袋计数或删除规则，必须重新设计接口，不能沿用这里的 PASS。