安全多重执行

公开副本从未拿到真实秘密 ​

动态监测看到秘密后，设法阻止它经数据或控制流进入低结果。多重执行换了一个位置处理问题：负责公开答案的那份程序一开始只拿到固定替代值。它可以任意分支和计算，但没有真实秘密可供区别。

代价是答案可能改变。原程序若确实想把秘密写到公开结果，低副本会写出默认值相关的答案。安全性不表示保留所有不安全程序的行为；有用的透明性条件必须另写。

同一个秘密分支，公开值来自哪一份 ​

执行if h then out:=1 else out:=0，默认d=0。真实h=0时，高副本输出0；真实h=1时，高副本输出1。低副本在两种真实输入下都看到h=0，所以两次公开值均为0。若选择高副本的“更真实答案”补回公开接口，就立即恢复原泄漏。

对于if h then out:=0 else out:=0，原程序的低结果已经独立于秘密。两份都正常终止，低副本输出0，保持了原结果。它无需像语法类型系统那样因为高条件中的低写入而拒绝这段代码。

不等待高副本是一项执行要求 ​

while 0 < h do h := h - 1
out := 0

默认d=0。每次守卫测试、赋值或skip算一步，seq容器不另计步。真实h分别为0、1、3时，高副本分别需要2、4、8步；低副本始终2步。两份总工作分别4、6、10步，但低侧都可以在低副本2步完成时收到0。

若实现先跑高副本，再启动或发布低副本，低结果到达前的语义工作分别变成4、6、10步，秘密进入等待时间。若低结果已发布，但又把“全部副本完成”通知公开，同样新添了高侧观察。保护的是规定的低接口，不能顺便公开总工作日志。

默认值让原本结束的运行不结束 ​

把循环改成while h==0 do skip; out:=0。真实h=1时两步完成，默认h=0时循环永远不改状态，故数学语义中发散。这段程序满足TINI：所有正常结束的运行都输出0；然而SME低接口无法为本次真实输入交出结果。

预算20的下载检查会给真实运行OK、低运行UNKNOWN。UNKNOWN只是“20步内未完成”，上述发散结论要另用不变的真守卫证明。此例正好说明为什么透明性必须写投影终止，不能以TINI自动代替。

一步相同推广到整条低轨迹 ​

低投影相等以后，归纳对象是一份完整的低副本状态，包括待执行命令、变量值和解释栈。确定性保证相同状态选择相同下一条规则，算出相同新状态。有限前缀因此逐步相同；若某侧第T步结束，另一侧也在同一步结束。若永远不结束，另一侧也持续相同执行。

证明没有读取高副本状态，也没有让它决定低副本何时前进。只要两份共享可写计数器、资源失败或不受约束的等待，就需重新验证这个前提。本模型的相同步数不是硬件常数时间认证，缓存、调度与机器故障都未建模。

计算实际工作，不猜倍数 ​

若两份都结束，令其语义命令步数为$T_L,T_H$，包含seq容器的实际命令栈分派次数为$K_L,K_H$，表达式访问数为$E_L,E_H$。输入复制与验证后，单位代价整数模型的总工作为$O(A+v+K_L+K_H+E_L+E_H)$；两个私有状态用$O(v)$空间，解释栈另按语法大小A计。若同时保存两份完整日志，还应加上两份事件记录空间。

语义步数便于比较算法轨迹；实际解释器还处理可能反复进入的seq容器，成本必须计K。$T_L$与$T_H$可能差很多，甚至一份不结束，所以“两个副本”不推出“原真实执行的固定两倍”。对于上一节递减循环，真实h=0、1、3已有不同总账。高副本迟迟不结束也不应阻止一个已就绪的低答案；下载接口将sme_low单独暴露，函数内根本不运行高副本。

结构迁移 ​

从while h==0 do skip; out:=0开始，把默认值改为1。现在低副本两步结束，即使真实h=0的高副本不结束也能公开0。低接口仍独立于真实秘密，但相对于原程序的终止行为再次改变。请分别填写真实执行、默认执行和低接口三列，不能用“程序终止”一个词同时指代它们。

再把对外接口改成“等待两副本都完成才返回”。真实h=0和h=1便有不同返回行为。该迁移改变的是发布依赖，不是投影公式；只有同时检查输入屏蔽和输出发布路径，原来的证明才能覆盖实现。完整比较见终点任务。