本终点从同一带事件循环产生三个真实目标：不变分支外提、带余数尾段的计数展开，以及先外提再展开。需交出的证据包括实际IR、完整事件迹、返回元组和控制测试数，不能只说“优化后结果没变”。
路线入口见从重复选择到连续迭代组。模型是数学整数、纯总表达式、进入时一次捕获的非负次数和有限无内层循环的体；只有emit和返回是外部观察。break、continue、异常和调用不在参考语法中。
运行准备
下载标准库参考器，保存在当前目录，使用Python3.10或更新版本。它不访问网络或输入文件，只输出JSON。
python foundation-counted-loop-transform-check.py > result.json
python -O foundation-counted-loop-transform-check.py > optimized.json
cmp result.json optimized.json两个输出逐字节相同，status应为PASS，inputs为1000。代码中的检查使用显式异常，不依赖-O会关闭的assert。随机输入只是实现回归；对所有合法循环的论证见两页的体替换归纳与商余数实例双射。
语句格式为('set',变量,表达式)、('emit',标签,表达式)、('if',条件,真体,假体)、('repeat',次数,体)；块用tuple表示。表达式为整数、变量名或(op,left,right)。unswitch(p,path)选择一个源if；路径按“语句位置、分支槽2或3、语句位置……”编码。unroll(p,k)返回真实复制过的目标；没有在解释器内用“优化模式”伪装改写。
任务一：四个程序，同一条事件迹
取n=10、mode=1、seed=1、start=2。每轮先记录i，按mode更新s，再记录s，最后递增i。依次打印源、外提、展开、组合的观察和计数。
PYTHONDONTWRITEBYTECODE=1 python - <<'PY'
import runpy
m=runpy.run_path('foundation-counted-loop-transform-check.py')
p=m['example'](); x={'n':10,'mode':1,'seed':1,'start':2}
u=m['unswitch'](p,(1,))['program']
a=m['unroll'](p,4)['program']; b=m['unroll'](u,4)['program']
for label,q in zip(('source','unswitch','unroll','combined'),(p,u,a,b)):
r=m['execute'](q,x)
print(label,'code',q['code'])
print('result',r['result'],'events',r['events'])
print('nodes',m['statement_count'](q['code']),'counts',r['counts'])
PY四者均返回(4083,12)，事件完整序列为
(before,2), (after,4), (before,3), (after,11),
(before,4), (after,26), (before,5), (after,57),
(before,6), (after,120), (before,7), (after,247),
(before,8), (after,502), (before,9), (after,1013),
(before,10), (after,2036), (before,11), (after,4083)按同一顺序，code语句节点为7/12/33/48，循环测试为11/11/6/6，if测试为10/1/10/1。初始化也计入运行赋值数，故assignments为22/23/23/24；新增捕获不会被误说成零成本。四者都产生20项事件，加法20次、乘法10次；展开额外各算一次商和余数，组合只在被选中的那支计算它们。
解释33个节点：捕获1个、两个repeat2个、原6节点体的5份副本共30个。解释48个节点：外提捕获与外层if共2个，每个分支展开后为3+5×4=23个，故2+23+23=48。未执行的分支也占静态代码空间。
任务二：换分支、零轮与空尾段
把mode改成0，负分支的s为−1、−4、−8、−13、−19、−26、−34、−43、−53、−64，四者均返回(−64,12)。这次没有乘法，不能复用任务一的运算数当作所有输入的开销。
对N/k取(0,4)、(3,8)、(8,4)、(10,1)，逐项核验源与展开后的循环测试。下面不依赖外提，避免把两类控制混在一起。
PYTHONDONTWRITEBYTECODE=1 python - <<'PY'
import runpy
m=runpy.run_path('foundation-counted-loop-transform-check.py'); p=m['example']()
for n,k in ((0,4),(3,8),(8,4),(10,1)):
x={'n':n,'mode':1,'seed':1,'start':2}
a=m['execute'](p,x); b=m['execute'](m['unroll'](p,k)['program'],x)
print(n,k,'result',a['result'],b['result'],'tests',a['counts'].get('loop_tests',0),b['counts'].get('loop_tests',0),'events',len(b['events']))
u=m['unswitch'](p,(1,))['program']; x={'n':0,'mode':1,'seed':1,'start':2}
print('zero unswitch',m['execute'](u,x)['counts'])
print('negative branch',m['execute'](p,{'n':10,'mode':0,'seed':1,'start':2})['result'])
PY四组测试数分别为1对2、4对5、9对4、11对12；返回分别为(1,2)、(26,5)、(1013,10)、(4083,12)。事件数为0、6、16、20。零轮外提仍做一次if测试，但不产生事件，返回(1,2)。
请推导一般减少量q(k−1)−1，而不是猜“因子越大一定越好”。对N=3、k=8，整组一次也不执行，却仍有一次失败测试；尾段又完整执行源三轮，因此控制反而更多。代码体积与实际耗时还需另作判断。
任务三：让错误目标自己暴露
本任务真正改写目标语法再执行，不给解释器传入“请失败”的标志。先删去尾段，再将第一份副本的i更新移到前面。最后构造一个会改变mode的源，手工冻结错误分支。
PYTHONDONTWRITEBYTECODE=1 python - <<'PY'
import runpy
from copy import deepcopy
m=runpy.run_path('foundation-counted-loop-transform-check.py'); p=m['example']()
x={'n':10,'mode':1,'seed':1,'start':2}; good=m['unroll'](p,4)['program']
missing=deepcopy(good); missing['code']=missing['code'][:-1]
print('missing cleanup',m['execute'](missing,x)['result'],len(m['execute'](missing,x)['events']))
phase=deepcopy(good); capture,group,tail=phase['code']; body=group[2]
phase['code']=(capture,('repeat',group[1],(body[3],)+body[:3]+body[4:]),tail)
print('early update first events',m['execute'](phase,x)['events'][:2])
changing=deepcopy(p)
changing['code']=(('repeat','n',p['code'][0][2]+(('set','mode',('sub','mode',1)),)),)
print('safe refusal',m['unswitch'](changing,(1,)))
frozen=deepcopy(changing); body=list(frozen['code'][0][2]); body[1]=body[1][2][0]
frozen['code']=(('repeat','n',tuple(body)),)
y={**x,'n':3,'mode':2}
print('changing vs frozen',m['execute'](changing,y)['result'],m['execute'](frozen,y)['result'])
PY删除尾段得到(1013,10)和16项事件。提前更新的前两项是(before,3)、(after,5)，而正确是(before,2)、(after,4)。会改变mode的源三轮条件真、真、假，返回(7,5)；冻结真支返回(26,5)。合法外提器应拒绝它，reason指出条件读取体内被写的变量，program为null。
不能以“体每轮都相同”推出条件每轮同值。也不能以“每个表达式最终都算过”推出事件保序。请在提交中各写出失效前提，不只粘贴三个错误数字。
任务四：次数捕获、嵌套选择与新鲜名字
把每轮最后改成n:=0。源仍执行进入时确定的十轮。正确展开的尾段读取新鲜捕获变量，错误版本故意改成读取当前n。
PYTHONDONTWRITEBYTECODE=1 python - <<'PY'
import runpy
from copy import deepcopy
m=runpy.run_path('foundation-counted-loop-transform-check.py'); p=m['example']()
x={'n':10,'mode':1,'seed':1,'start':2}
p['code']=(('repeat','n',p['code'][0][2]+(('set','n',0),)),)
good=m['unroll'](p,4); bad=deepcopy(good['program']); code=list(bad['code'])
code[-1]=('repeat',('rem','n',4),code[-1][2]); bad['code']=tuple(code)
print('capture',good['captured_counts'])
print('source good bad',[m['execute'](q,x)['result'] for q in (p,good['program'],bad)])
nested={'params':('n','mode'),'init':(('set','i',0),('set','s',0)),
'code':(('repeat','n',(('if',('lt','i',3),(('if',('gt','mode',0),(('set','s',('add','s',1)),),(('set','s',('sub','s',1)),)),),()),('set','i',('add','i',1)))),),
'returns':('s','i')}
q=m['unswitch'](nested,(0,2,0))['program']
print('nested',[m['execute'](z,{'n':5,'mode':1})['result'] for z in (nested,q)])
collision=m['example'](); collision['params']+=('__trip_0','__trip_1')
collision['returns']+=('__trip_0','__trip_1')
z=m['unroll'](collision,4)
print('fresh',z['captured_counts'],m['execute'](z['program'],{**x,'__trip_0':77,'__trip_1':88})['result'])
print('size limit',m['unroll'](m['example'](),10**9,max_statements=10000))
PYsource与good返回(4083,12)，bad返回(1013,10)。嵌套例仍保留i<3，所以两者返回(3,5)，不是(5,5)。名字碰撞例应选__trip_2，保留源观察77、88，返回(4083,12,77,88)。不能把所有以某前缀开头的变量都从比较中隐藏。
巨大因子例在复制前给出size_limit，needed为6000000009，program为null。这是输出规模政策，不是“因子十亿破坏了数学正确性”。若体为空，生成器只输出捕获和两个空repeat，不实际做十亿次空复制。
任务五：提交对全部输入的证据和拒绝边界
先用两段文字分别完成证明。外提需要入口条件的读取在整个体中不变，再对选中if的语法位置和每轮状态归纳；零轮新增条件求值依靠纯总且无事件的前提。展开需要t=gk+j与尾段t=qk+j给出覆盖双射和原次序，随后用完整体F的N次复合说明环境与事件迹一致。两份证明不能互相替代。
然后自行运行以下拒绝：因子0、负数和True；含break或内层repeat的源；返回仅在可能零轮的体中定义的变量；选中条件读取体内先定义但入口未定义的t。前三类是模型或因子检查失败；最后一类可有良构源，但外提条件不满足，不能把两种失败写成同一语义反例。
最后明确更宽语言的边界。N=0、条件1/d>0、d=0时，直接提前求值会新增异常；若条件本身发事件，外提会改变事件次数。即使补N>0护卫，条件前的源emit与随后异常的先后仍可能改变。参考器不支持这些表达式，所以这部分提交应是边界推理，不能声称本脚本实际模拟了设备或异常语义。
执行预算是另一个独立限制。把budget设为0会报告budget_exhausted、没有返回值；它不是证明程序发散，更不是与另一个耗尽程序相等的证书。该模型本身已由有限次数和有限体保证终止，预算只是测试工具的停机政策。