GKR with a Machine-Checked Core, and a Sparse Prover Made Faster with Byte-Identical Proofs
In briefGKR protocol with a machine-checked core and a faster sparse prover with identical proofs
SummaryThis post describes StateSync-GKR, which gives the first machine-checked soundness bound for GKR on general layered circuits, in Isabelle/HOL. The bound is applied to a soundness proof for sparse-Merkle updates. Release 1.2 of the sparse prover proves 2.41 to 2.71 times faster and produces byte-identical proofs.