# 槽200、原始RBP与处理器0的条件连接

固定自产3.11 Demo2835 Ultra目标SHA256为`5f9c1b6fcb019366f835d8f02d9ec3b2957fe619e039410d07f288a9c73f63f0`。目标只作为数据，完整CPU、原生可达性、精确3.8及保护业务恢复未证明。

沿用S=原入口RSP、F=(S-648)&~15、先前76初始字节及完整窗口/映像/上下文条件。208快路之后，虚拟栈[S-8]=S、RBP=S-8、RSP=F、RSI=VIP+52。处理器136的10条前缀读取这个S，按字节索引200写到F+200，RBP恢复为S；22条完整路径继续派发到处理器0/0x140052281。

新增VIP+52处200、VIP+53处0及表项0的四字节，共6个新事实，76→82。新槽200与原19槽逐字节不相交，并保持原671字节窗口。槽200保存S；它不同于槽120：槽120从原入口保存的是原始RBP。不能将当前虚拟栈指针RBP=S替换为原始入口RBP，也不能只因寄存器名称相同而等同两个状态。

处理器0的14条检查路径先读取VIP字节索引，再读取当前内存[RSP+索引]到R9，RBP减8后写[RBP]=R9。RDX为索引，RSI加1，R8=RSP+384，条件为无符号RBP>R8；RBX保持。BSR R9W,R15W的目的与状态均在后继实际覆盖，原完整指令保留，沿用已有有限死效果规则。完整26条快路保留派发器和完整搬栈互补出口，早期栈写不被最终guard抹掉。

新增VIP+54处120、VIP+55处78；表项78四字节已在旧事实中，复用不重复计数，82→84。在已证明槽120及前序保存条件下，0读取原始入口RBP并压入S-8，下一目标为78/0x14005242b。末态R9=原始入口RBP、RDX=120、RBX=S、RBP=S-8、RSI=VIP+56、RAX=78、R8=目标、RSP=F，其他GPR按前序精确状态保持。槽200=S和原19槽都保留，共20槽。检查false范围仍恰为8<=S<264，先前快路成立蕴含本次快路成立；先前guard=false的编码末态不作为真实后继输入。

公开五层transition-chain为208检查、派发、136完整路径、0检查、派发；90个精确绑定、6条有序STORE和4个完整互补出口。202节点/677引用。全部原预算保持，未增加公开跨报告摘要或手工状态接口。

`prove_context200_join.py`的30查询为23UNSAT/7SAT，含4项未切割局部完整状态方程、5层全状态及2个动态目标互补分区、源字方程、条件接点、原始内存/窗口/槽位保持和反例。接点中的源字cut分别有未切割原LOAD方程；派发内存cut对应原第一STORE的afterMemory。负例必须恢复这个STORE的内存定义，不能用自由cut声称真实反例。源DAG在切割前完整校验。不是单项未切割整链或整VM证明。

独立`verify_context200_join.py`重读原字节、完整DAG、全部查询、90绑定、所有cut和反例恢复定义，以及76→82→84的事实计数。原19槽与新200的1216个字节对归纳结合先前覆盖任意0..255槽起点的栈写非别名证书，保留20槽及独立入口64位/ADD映像59位未知。

数值检查复用1004个自由上下文0状态与880个连接状态：64个不满足映像分离跳过，256个前序分支停止，560个条件下到达下一78。检查全16GPR、整内存、6写、4出口和20槽；两部署复用同批，不累计为新覆盖。首版动态目标混合状态查询、第二版连接数组查询各2秒unknown保留；通过分开互补目标和原源字方程的明确归纳解决，不提高预算。