从漏例证书到可执行模式分派 ​

覆盖检查与模式编译路线最后交付三份互相校验的结果：遗漏值与逐行有用性，保留动作和绑定的决策树，带失败出口的回溯字节码。下载标准库核验器，普通和python -O均保留显式检查，只向标准输出写JSON。

一、固定源语言与观察结果 ​

类型为Bool = F | T与List = Nil | Cons(Bool,List)。值是已经求值的有限、不可变树；类型入口的默认见证分别是F和Nil。列表长度没有统一上限，但不接受无限/循环对象；不把空类型伪装成有默认值。

模式可以是通配、变量、构造子或左偏or。每个分支中的变量只出现一次，or两臂绑定相同名字且类型一致。源解释器从上向下选第一条结构匹配行，输出动作ID和完整绑定环境；没有行匹配输出None。动作体并未执行，失败不包含任意语言的异常或非终止行为。

共同核心没有guard。末尾的guard实验另用明确语义：结构匹配成功后只检查一次纯、全定义的guard，假则进下一源行，不重试本行or右臂。下载器实际只提供nonempty_xs，并拒绝把带guard矩阵交给共同核心的树编译器。

二、先交一份真正能执行的漏例 ​

初始有序矩阵如下：

逐行解释这两项诊断：第四行没有任何成为首匹配的输入；全表仍漏掉(Cons(F,Nil),F)。前者由第一行遮蔽第四行，后者需要首项为F的非空列表配F标记。不要用“有一条死行”代替另一个穷尽性问题的答案。

请写出见证重建过程：选Cons后矩阵只剩(T,_,F)和(_,_,T)；头列缺F，默认只保留后者的(_,T)；尾列移走通配符，标记列缺F。先得到标记F，再补默认尾Nil和头F，最后重建Cons。把这对值交给源解释器，结果确实为None。

现在在末尾Nil/T之前加入Cons(F,_),F → false-head。新表共有五行。有用性函数依次给出的见证为：

全通配符候选现在返回None，证明表已穷尽。候选自身若含or，要对展开后的每个候选行求见证；任一成功就有用，不是要求所有替代同时匹配。

迁移任务：把一个新的_,_ → early移到最前面。现在所有旧行都无用，且每个实际输入返回early。它没有引入遗漏，却改变全部动作选择，说明“覆盖相同”不足以证明编译语义相同。

三、交树与槽，不只交最终动作 ​

槽0保存列表，槽1保存标记，槽2保存列表头，槽3保存列表尾。只有确认槽0为Cons后，才能投影产生槽2、3。先选列表列的树为：

Switch slot0
  Nil  → Leaf empty, {}
  Cons → project head→slot2, tail→slot3
         Switch slot2
           T → Switch slot1
                 F → Leaf take-tail, {xs: slot3}
                 T → Leaf flagged, {}
           F → Switch slot1
                 F → Leaf false-head, {}
                 T → Leaf flagged, {}

这份IR有4个Switch、5个Leaf，共9节点。同一位置slot1在整棵树中有两个节点，但一次运行只会经过其中一个，没有违反“每条路径不重复测试同一位置”的保证。

执行三份记录：

下载器也生成每次选最右可检列的树。它仍有9节点，但第一行输入要查标记、列表两次；后两行是标记、列表、头三次。别用平均值掩盖某个输入变慢，也别把读槽和完整展开打印变量值混为同一成本。

四、核对全部23条字节码 ​

回溯编译器保留五行，按反向生成使所有跳转目标编号更小。下面TEST o tag children yes no在标签成功时先投影字段，再进入yes；ACCEPT后的最后编号是guard失败出口。无guard记为true。

 0 FAIL
 1 ACCEPT shadowed  []   true 0
 2 TEST 1 T    []    1 0
 3 TEST 0 Nil  []    2 0
 4 CLEAR 3
 5 ACCEPT false-head []  true 4
 6 TEST 1 F    []    5 4
 7 TEST 2 F    []    6 4
 8 TEST 0 Cons [2,3] 7 4
 9 CLEAR 8
10 ACCEPT flagged []    true 9
11 TEST 1 T    []   10 9
12 TEST 0 Cons [2,3]11 9
13 CLEAR 12
14 ACCEPT take-tail [xs] true 13
15 TEST 1 F    []   14 13
16 BIND xs 3 15
17 TEST 2 T    []   16 13
18 TEST 0 Cons [2,3]17 13
19 CLEAR 18
20 ACCEPT empty []      true 19
21 TEST 0 Nil  []   20 19
22 CLEAR 21                 # 总入口

(Cons(T,Nil),F)走22→21→19→18→17→16→15→14，8条指令，标签测试4次，字段投影2次。21尝试Nil失败，18才确认Cons；它们测试的是同一个根槽的两个不同标签。

(Cons(F,Nil),F)走22→21→19→18→17→13→12→11→9→8→7→6→5，13条指令，标签测试8次，字段投影6次。它与树都返回false-head，但重试后行产生了真实重复工作。

结构计数也应复算：m=5，构造子出现C=11，变量出现V=1，所以1+2m+C+V=23。这里保留了不可达的第五行动作块；覆盖诊断可以支持删除它，但本次计数不能在不改IR的情况下假装已经做了优化。

五、用不同结构检验时间和体积 ​

改用三列Bool和四行：(T,_,T)→a、(_,_,F)→b、(F,T,T)→c、(_,_,_)→d。生成两种选列结果：

左选静态树11节点、总测试20次；右选9节点、总测试16次。右选改善总和却使T,F,T和T,T,T从2次变3次。两种策略都不是最优性证明，只是保持语义后可测量的不同布局。

再取一行n列，每列都是F|T，动作yes。本页未做or化简或DAG共享：展开有2ⁿ行，无共享树2ⁿ⁺¹−1节点；共享成功标签的回溯代码只有2n+3条指令。n=0也合法：树只有一个Leaf，代码为FAIL、ACCEPT、CLEAR三条，输入空向量仍返回yes。

若先把Bool的F|T化成_，当然能进一步缩小；若共享相同续树，节点计数也改变。请把这些变换作为新的IR重新计数，而不是把优化后结果算进上表的未优化实现。

六、guard提交点的结构迁移 ​

输入改回一列List。第一行为(Cons(_,xs)|xs) when nonempty(xs) → first，第二行为_ → fallback。单元素列表首先匹配左臂，xs=Nil，guard失败，于是返回fallback；两元素列表的尾非空，所以返回first。

请对照两个错误做法：

1. 在guard失败时回到or右臂，会把xs改绑为整个列表，让单元素输入错误地返回first
2. 把两臂变成两条各自有guard的独立源行，会产生同一个错误

正确字节码把左、右臂都接到同一ACCEPT，而该ACCEPT失败出口直接是下一源行CLEAR。对单元素，入口标签7→6→5→3→2→1；它不会经过右臂标签4。每次结构成功最多执行一次该行guard。

再用Cons(h,Cons(_,xs)) | Cons(h,xs)测试失败临时绑定：单元素输入在左臂写h后失败，右臂须重新给出完整h/xs。两臂绑定集合不同或同一普通分支重复变量，均应在编译入口拒绝。

七、验收边界与成本账本 ​

主JSON包含真实树、槽父表、完整字节码、入口编号、漏例与诊断、三条主轨迹、选列8输入表、n=0…8的体积表和guard反例。它比较31个长度不超过4的Bool列表乘2个标记，共62输入；左树/右树/回溯的标签测试总数分别182/154/347。or族的各维全部输入共511个，另核长度不超过6的127个guard输入及5个非法入口。

这些有限对照用来找实现错误，不代替任意有限深度上的正确性。覆盖递归的终止量是显式构造子总数与列数的字典序；树靠候选矩阵和槽值不变量；字节码靠模式成功/失败出口归纳及严格下降的标签。递归类型本身不会要求枚举无限多个列表。

成本分别报告输入良构校验、or展开、候选矩阵工作、静态输出和单次执行。字节码主体线性体积不表示透明入口校验也线性；树没有重复标签测试，不表示字段投影、输入验证、绑定输出和日志免费。打印一个深尾值要按实际字符量付费，保存它的引用则不必重新遍历尾部。

最终交付应能回答：漏例为什么真的未覆盖；被遮蔽行为什么没有首匹配；每个Leaf/BIND取哪个输入子项；每条失败边跳到哪一候选；guard失败是否越过整行；两种成本表统计的究竟是哪一种操作。