GKR with a Machine-Checked Core, and a Sparse Prover Made Faster with Byte-Identical Proofs
説明機械検証済みの中核をもつ GKR と、バイト単位で同一の証明を出す高速なスパース証明器
要約本稿は StateSync-GKR の研究を紹介します。一般の層状回路に対する GKR プロトコルについて、Isabelle/HOL で機械検証された初の健全性上界を示し、それをスパース Merkle 木の更新の証明に適用しています。あわせて、バージョン 1.2 の証明器が、証明のハッシュを変えずに 2.41〜2.71 倍速く証明することを報告しています。