该论文处理的是一个在可验证计算工程中常被忽视的信任缺口：GKR 协议的可靠性界只能保证『关于某个算术电路的输出声明是可信的』，却无法保证『该电路确实编码了应用所期望的状态转移』。作者以稀疏 Merkle 树（SMT）的成员证明、非成员证明与状态更新为具体应用载体，在 Isabelle/HOL 证明助手内对这条从状态转移到 GKR 验证的完整信任链进行机器检验。 方法上分为若干层次。首先是编译器模型：它建立了电路接受与状态转移有效性之间的双向关系（而非仅有单向的可靠性蕴含），从而同时覆盖可靠性与完整性两个方向。其次是可复用的协议模型：把层归约（layer reduction）、wiring predicate 扩展，以及从外部导入的 sumcheck 可靠性结论组装起来，形成一个针对某个显式『链事件』的界；其组合定理把语义上的无效性传递到该界上，且 witness 在挑战实验之前就已固定，避免了先看挑战再选证据的隐患。作者特别强调使用具体解释（concrete interpretations）与前提激活（premise activation）来暴露『空洞假设集』——即假设集合在逻辑上被满足但语义上无内容的情况，这是仅靠一次干净编译无法发现的。 进一步的工作构造了精确的四次 KoalaBear 扩域，把基域上的电路对象提升到扩域，并在其陈述的挑战假设下建立分母为 p^4 的装配界。论文还附带了一个可执行的 Rust prover，通过 Creusot/Why3 合约提供部分实现层面的连接，并给出一个条件性定理，把成功的验证者执行轨迹与模型事件关联起来——但该定理依赖一个未被消解的值对应（value-correspondence）前提。作者明确列出未完成的部分：既未建立转录中的在线挑战分布性质，也未建立多轮 Fiat–Shamir 归约。因此其核心贡献是：在单一证明助手内完成编译器正确性与 GKR 装配模型的组合，并显式、诚实地刻画了遗留的实现义务与密码学义务。 适合阅读的人群包括：形式化方法与证明助手研究者、zkVM / 可验证计算与状态承诺（SMT、Rollup 状态根）方向的协议设计者，以及需要对证明系统实现做独立评估的安全审计人员。