这份终点要求交付能执行的启动表，而不是只画几条看起来平行的箭头。先完成有限图上的列表调度，再保留原迭代距离，构造跨轮周期表。每一项都要分清合法性、数值语义、性能与搜索是否有结论。
下载标准库参考程序，执行 python foundation-instruction-scheduling-check.py 和 python -O foundation-instruction-scheduling-check.py。输出 JSON 应完全相同，status 为 PASS。程序只写标准输出，不写文件；所有实际检查使用显式 require，不依赖被 -O 删除的 assert。需要保存时可以自行重定向输出。
任务一：交出六拍表，再证明五拍表
输入 x，六条操作 A=x·x、B=x+1、C=x−1、D=2C、E=A+D、F=D+3，结果全部保留。A 至 F 的延迟为 (4,3,1,1,1,1)，资源为 (M,M,M,A,M,M)，两个类别每拍容量1。直接边为 C→D、A→E、D→E、D→F。资源字母只是本例端口名字。
先逆拓扑计算高度 (5,3,3,2,1,1)，逐拍列出就绪表、选中的操作及被容量挡住的操作。相同高度按 A 至 F 的声明次序选择。应得到启动 (0,1,2,3,4,5)，最后完成时刻6。说明为什么 B 尚未完成时 M 仍能接受 C，以及为什么 D 不能只因 C 已启动就立即启动。
另交启动 (0,2,1,2,4,3)，逐边核对松弛量，逐时刻核对两个端口。最后完成时刻5。给出“主口五次启动，最后启动至少在4，延迟至少1”的下界，证明这一份确实最优。不要将这个结论推广成关键路径优先总能最优。
读取 list_counterexample.greedy_execution 和 better_execution，两份实际执行在 x=4 时都应得到 A=16、B=5、C=3、D=6、E=22、F=9。参考器还比较 x=−50,…,50 的两份输出。检查器把同一时间边界的完成放在启动前；因此 D 在2启动、在3完成后，F 就能在同一边界3启动；A 在4完成后，E 也能在同一边界4启动。
构造一个只有 u→v 的反例：u 延迟4，v 延迟1，两个不同类别容量各1；提交 s(u)=0、s(v)=1。要求检查器报告 dependence，slack=−3，而不能因“u 排在 v 前面”接受。
任务二：单轮合法，跨轮为什么碰撞
前缀和循环的 A 读 X[i]，B 乘因子 k，C 加上一轮累加值，D 写 Y[i]。延迟 (2,3,1,1)，资源 (MEM,MUL,ALU,MEM)，各容量1。边为 A→B、B→C、C→D，距离均0，另有 C→C、距离1。X、Y 完全不重叠且下标不越界，c₋₁ 为初始累加值。
先检查单轮表 (0,2,5,6)，完成于7。再重复间隔 II=2，给出第一次可以直接看到的 MEM 冲突：D₀ 与 A₃ 都在6启动。JSON 的 first_iteration_collides_later 在余数0中同时列出 A、D。不要把它改成“延迟2的加载连续占用两拍 MEM”；模型只限制启动数。
把 D 改到7。列出四条边的松弛量 (0,0,1,1)，以及模表：MEM 的0槽为 A、1槽为 D；MUL 的0槽为 B；ALU 的1槽为 C。完整偏移为 (0,2,5,7)。这份证书可以复用到任意有限 N，但不证明每个 N 都比单轮串行更快。
任务三：把有限启动和排空真正执行完
取 X=[1,2,3,4]、k=2、初值0。提交全部16个具名操作的启动与完成时间，而不是只给中间的重复部分。逐个加载应读1、2、3、4；逐个累加应得到2、6、12、20；存储在8、10、12、14完成。periodic_execution.trace 按事件边界记录每个实际读取或计算、何时交付及每次写入的下标和值。
在 t=6，A₂ 完成，同时 A₃ 与 B₂ 启动；在 t=7，C₁ 与 D₀ 启动；在 t=8，A₃ 和 C₁ 等先前操作的完成先处理，D₀ 写 Y[0]=2，随后 B₃ 启动。逐项核对值来自哪一个轮号，不能把多个轮的 B 或 C 放进同一虚拟结果槽而覆盖。
核对周期表四轮耗时14，串行表以 II=7 重复则耗时28。再看 one_trip：X=[3] 时输出 [6]，周期表最后在8完成，比单轮的7更慢。zero_trips 必须没有事件、没有存储、输出空数组、最后时刻0。initial_edges 只给 C[-1]→C[0] 的外部初值要求，不意味着执行负轮号指令。
下面的短命令可在不改脚本的情况下换输入。X=[−2,5,0]、k=3、初值4 应得到 [−2,13,13]，最后在12完成。
python -c 'import runpy; m=runpy.run_path("foundation-instruction-scheduling-check.py"); print(m["execute_prefix"]({"A":0,"B":2,"C":5,"D":7},2,[-2,5,0],3,4))'任务四：四种搜索结果各自证明什么
主例固定 II=2、H=7、默认试放预算，得到 feasible，18次试放，偏移 (0,2,5,7)。将 H 缩到6，得到 no_schedule_in_window，189次试放：它只排除了此窗口。保留 H=7 而把预算改成1，得到 search_limit，只有1次试放，不交付时间表。
把 II 改成1，不论把窗口放到20多大，资源下界2已经构成证书，所以在0次试放后返回 infeasible_by_bound。保存每个结果的 starts：只有 feasible 有完整映射，其余为 None。程序的预算计数只包含试放，前面的简单环枚举不在此预算内。
再把累加 C 的延迟改为3，先写出原距离1自环的约束：下一次累加至少隔3拍。II=2 被 recurrence_bound=3 否决；II=3、H=8 得到 (0,2,5,8)，四轮数值仍相同。证明这里的瓶颈是结果依赖，不是 ALU 每拍接单能力消失。
最后处理两个节点 P、Q：都延迟2、都用容量1的 R；P→Q 距离0，Q→P 距离2。两种下界都是2。mii_not_sufficient.ii_two_window 只报告 H=8 内无表；你还需另交全局证明：II=2 的两条依赖迫使 Q−P=2，两者同余而争用 R。II=3 的 P=0、Q=2 通过。这说明下界并非总可达到，也说明应把数学证书与有限搜索状态分开报告。
任务五：破坏别名合同，并修复依赖
用共享数组 [1,2,3,4,0]，把 X[i] 解释成第 i 格，把 Y[i] 解释成第 i+1 格。逐轮串行执行，源输出应为 [2,6,18,54]：第1轮写出的6成为第2轮读入，第2轮写出的18成为第3轮读入。
故意沿用无别名的周期表，输出却为 [2,6,12,20]。指出哪两次加载过早：A₂ 在4读到了原3，而源应等 D₁ 写出6；A₃ 在6读到了原4，而源应等 D₂ 写出18。参考器的私有 fault 分支专为这项反例构造重叠内存，公开 execute_prefix 总是分开输入和输出。
修复图时新增 D→A、距离1。沿 A→B→C→D→A 相加，延迟和7、距离和1，因此 II≥7；原 II=2 表在新增边上失败。不要只修改 expected 数组掩盖差异，也不要随意更改循环距离以迁就已排好的表。
交付清单与可重复检查
最终提交两份六操作表及数值结果、主例完整周期证书与16操作事件表、四种搜索结果、改变累加延迟后的新表、两个节点的下界不充分证明，以及重叠内存反例和新增边。说明有限寄存器分配、复杂预约表、异常与提前退出都没有被此模型解决。
参考器除上述确定例子，还执行420组随机前缀和输入（含零轮、负因子、非零初值）、1000张随机 DAG，以及180张三节点图在完整小窗口中的穷举对照。最后一项验证有限搜索的剪枝不会丢失窗口内解，不证明大图搜索实用；独立的全局不可行结论仍需要资源、递推或额外数学证书。
验收时可故意把 D 偏移改回6，或删掉“完成先于读取”的检查，确认错误能被边或容量证据定位。一次 status=PASS 不能替代解释它究竟覆盖了哪一种机器、哪些依赖和哪些实际读取。