# Handler208 与完整搬栈循环

固定自产 VMP 3.11 Demo2835 Ultra 文件 SHA256：`5f9c1b6fcb019366f835d8f02d9ec3b2957fe619e039410d07f288a9c73f63f0`。目标只作为数据读取；这些结论不等于精确 VMP3.8、原生可达性、CPU/OS 等价或完整保护业务恢复。

处理器从0x1400556d4开始，12条检查路径保存旧RBP到[RBP-8]，随后令RBP-=8、RBX=旧RBP、R8=RSP+384，按无符号RBP>R8选择派发器0x140052124或搬栈入口0x140052162。其余GPR保持原值，写入在判断前已经发生。24条快路包含完整派发器，保留互补出口的全部16GPR/整内存和各条STORE自身的guard。

搬栈入口29条包含准备和第一次复制：D=(RBP-384)&~15，读取原RSP处8字节后写到D，令RSP=D、RDI=原RSP+8、R8=D+8、RBX=248、R10=读取字；其13条正文每次从当前内存读取[RDI]并写[R8]，两个指针各加8、RBX减8，JNZ回到0x1400521a6，退出0x1400521d5再回派发器。初始计数来自原机器码256，调用者不提供次数。

公开constant-loop自动推导首次复制后再执行31次正文，共32个八字节字/256字节，再派发：445逻辑指令、533访问字节、33 STORE、201节点/1849引用。显式transition-chain从208检查连接完整搬栈：34层、612状态绑定、34 STORE、33完整互补出口、987节点/4068引用；终态只在自己的pathGuard下有效。所有原预算保持；不能把重复地址展开冒充一次project。

复制使用每一步写后内存。源目标可能重叠，不能假设初始内存快照复制：固定源0x1008、D=0x1010时，第二次读取可与原始0x1010字不同，该差异为SAT。BSR/BSF等先前有限死效果规则、活初始flags拒绝保持。

`prove_handler208_semantics.py`的84项查询为79UNSAT/5SAT：5个未切割完整局部状态方程，34层全状态/有序写入/守卫/互补出口，32个复制步骤、原始目标地址方程和派发末写的明确内存归纳，以及75→76条件接点与负例。每个源DAG在生成切割方程前完整校验；内存cut只指向原始beforeMemory，D仅重命名另证原式的原首写地址，末R10仅重命名已证明的最后复制值。并非一项未切割整循环或整VM查询。独立`verify_handler208_semantics.py`重读字节、报告、查询、预算、全部绑定/cut及证书，不重复SMT或CPU执行。

448个普通内存状态/3136次报告计算覆盖全16GPR、整字节内存、所有写入和互补出口，包括回绕、335个搬栈守卫成立和113个快路守卫成立。源码/安装副本复用同一批状态，不累计为额外覆盖。

在先前75字节条件证书、S=原入口RSP、F=(S-648)&~15及原671字节窗口、64→10桥接、映像分离和保持引理下，208检查false范围恰为8<=S<264；先前立即数快路成立推出208快路成立。新两写S-8和F-8仍在原窗口，并逐字节保持原17槽及176/192共19槽，2432个明确有限字节对实例；入口未知64位和ADD映像未知59位保持自由。现在[S-8]=S。

仅增加VIP+51=0x1400846f7处字节136；原表项136四字节复用，不重复计数，合计76初始字节。派发后RAX=136、R8=0x1400545b6、RBX=S、RBP=S-8、RSI=VIP+52、RSP=F；其余来自前序已证明状态，不能全部当作最初GPR。目标只在完整条件成立时成立。其后136再次保存原RSP的槽位及下一后继尚需继续证明。

早期原生脚本误用strict schema、SMT首版2秒unknown和后续证明脚本开发错误均保留在独立产物目录；不冒充首次通过。原128查询、单项2秒512MiB、共享45秒、单进程2GiB50秒预算保持。