Isabelle/STARK：Isabelle/HOL 中 zk-STARK 的形式化
Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL
AI总结：
该研究在 Isabelle/HOL 中完成了 STARK 风格透明证明协议的形式化，构建了含证明者/验证者可执行模型等内容的开发成果，为相关领域提供了形式化方法层面的支撑。
AI中文摘要：
本报告描述了 Isabelle/HOL 中对 STARK 风格透明证明协议的形式化。该开发包含证明者与验证者的可执行模型、带最弱前置条件演算的有限概率状态单子、零失败诚实完备性定理，以及带有显式概率界的分阶段可靠性定理。报告面向具备形式化方法背景的读者，提供了足够的密码学背景以解释该协议，但其重点在于形式模型、证明的分解，以及主要定义和定理的 Isabelle 源代码位置。
英文摘要：
This report presents mechanized query-bounded soundness for a STARK-style protocol in Isabelle/HOL. An acceptance-preserving embedding connects adaptive, privately randomized Fiat-Shamir transcript producers to an established staged adversary experiment and the original probabilistic verifier. The proof combines FRI correlated-agreement reasoning, Merkle authentication, exact modulo-sampler accounting and weighted-path amplification. Event-sensitive accounting refines the complete error bound without changing the verifier or treating repeated oracle calls as free. For a certified 192-bit prime field, trace length 1024 and 640 query repetitions, the concrete theorem bounds false-endpoint acceptance by $2^{-137}$ for every modeled producer satisfying the uniform syntactic oracle-call bound fs_query_bound $(2^{20})$ P. A separate honest-completeness theorem gives acceptance one for the correct square-sequence endpoint in the same final verifier. These are fixed-statement results in a classical, field-valued random-oracle model with terminating finite-support computation, not an unrestricted 137-bit work-factor guarantee. The development does not prove zero knowledge, knowledge extraction, quantum-query security or correctness of a deployed bit-hash implementation. This report retains earlier proof routes as research history; the accompanying current-results overview and checked theorem manifest identify the principal claims and their assumptions.
