# 固定上下文写入链的条件证书

本轮修复 `opaque-status` 的宿主校验：架构未定义和固定解码器未建模可以同时描述同一个标志位，例如 `SHR DX,0x82` 和 `SHR DH,0x96` 的 OF。两类共同阻断传播；defined/preserved 仍不能与它们交叠，每类不得重复、六种标志必须完整覆盖。后续 ADD 重新定义的五位可以进入保存映像，直接观察此前 SHR 的 OF 仍拒绝。两份完整原始解码夹具和正反回归保留。

公开接口、原始运行时 pins、40 工具、13 审批门和全部预算保持原值。`test_status_chain_runtime.mjs` 可验 project 或 compose；真实解码只读自产 PE 数据，不执行目标。源码/安装/配置模型分别留回执，不能用本页代替其中任何一层。

研究对象仍是 SHA256 `5f9c1b6fcb019366f835d8f02d9ec3b2957fe619e039410d07f288a9c73f63f0` 的官方 3.11 Demo 自产样本，并非精确 3.8。入口新模式的整个 DAG 和全部普通语义字段与旧上下文证书一致；入口保存映像 knownMask=0、有效未知64位。它与后续 ADD 保存映像独立，后者仅 CF/PF/ZF/SF/OF 已知，有效未知59位，AF仍自由。

令 S 为原始 RSP，F=`(S-648)&~15`（全部按 uint64 回绕），VIP=`0x1400846c4`，TABLE=`0x140056098`。沿用原671字节窗口、64→10位桥接、映像分离、全部内存保持引理，以及立即数/137快路条件；不能把 guard=false 的末态当下一段输入。前250证书已经给出67个初始字节前提、两个虚拟栈操作数为零和 next136。

| 处理器 | 新增前提 | 复用前提 | 条件结果 |
| --- | --- | --- | --- |
| 136，22条 | VIP+47=176、VIP+48=78 | TABLE+4*78 的4字节 | F+176保存新FlagsImage；RBP=S-8、RSI=VIP+49；next78=`0x14005242b` |
| 78，27条 | VIP+49=192、VIP+50=208、TABLE+4*208的4字节 | 无新增重复计数 | F+192保存零；RBP=S、RSI=VIP+51；next208=`0x1400556d4` |

初始字节总数依次67→69→75。FlagsImage 仅满足 `image & 0x8c5 == 0x44`，不能改写成完整标志字0x44。136通过RBX保存读取值，78通过RDI保存读取值且R10=索引；最后RBX=FlagsImage、RDI=0、R10=192。其他寄存器按完整摘要继承，不能冒称都等于原始输入。

`prove_context_write_join.py` 给出四份局部全16GPR/整字节内存/全部有序写入/末控制方程，两个公开层的精确18状态绑定摘要，以及136目标选择与完整互补出口。公开250前缀103节点、整层和边界与前证书完全相同，复用其完整标志映像方程和层摘要。没有公开跨报告摘要注入接口。

后八写的地址类依次为 F-8、S-8、S-16、F-8、F+176、F-8、F+192、F-8。所有起点仍在原窗口；旧17槽与新176/192逐字节不相交，前3地址类用旧137全称引理，新2类用新增全称引理，再明确实例化8704个字节对及单字节保持引理。三项通用数组查询分别确认250后、136后、78后的虚拟栈/新上下文字。派发表的内存 cut 始终指向已证明的上下文写后内存，原DAG即使在cut后也完整检查。不同节点ID不作为地址不别名证据。

源码证书22查询=16 UNSAT+6 SAT，包含缺失虚拟字、索引、派发字节的反例及75前提一致性。早期合并状态/守卫查询在原2秒内unknown，原始文件保留；最终将完整状态与纯目标分区分开证明，未提高预算或把unknown当UNSAT。每查询≤2秒/512MiB，整体45秒、创建时单进程2GiB/50秒Job；确认真实退出后才读取日志。

1264个普通状态数值场景中1200满足分离，64跳过；256在原立即数分支停止，944继续250→136→78。核对完整16GPR/整内存/八次写入/互补guard、旧17槽及新176/192；入口自由映像与新250自由输入独立变化。安装重跑使用同批场景，不增加独立覆盖数。该检查不是第二个CPU解释器，也不是全称证明。

`verify_context_write_join.py` 独立验读原字节、报告/查询SHA、进程与预算、特定案例的typed cuts、完整状态绑定、窗口依赖和有限归纳，不重新求解或执行CPU。结果属于组件全称证明加明确条件归纳，**没有单项未切割整链SMT证明**。原生可达性、加载字节/重定位、故障语义、完整RFLAGS、后继208及剩余VM ISA、精确3.8、Ultra/Enigma完整业务和稳定覆盖仍未通过。

维护入口：`test:context-join-proof` / `test:context-join-audit`，参数必须使用封存的绝对路径和SHA；目录必须新建，失败原件不可覆盖。实际部署/模型审计见本轮独立checkpoint，不从源码证书推断模型调用成功。