Proofs of authenticated-data-structure updates built on the Goldwasser-Kalai-Rothblum (GKR) protocol are sound only if three arguments hold together: the soundness of the protocol, the exactness of the arithmetization that turns an update into a circuit, and the binding of the hash commitments. For GKR, the mechanizations we know of stop at the sumcheck subprotocol. For sparse-Merkle membership, non-membership and update as compiled by the StateSync-GKR prover, we machine-check in Isabelle/HOL the first two arguments, their composition, and the leaf side of the third. For layered circuits with linear, product and cube gates, the cube gate serving the $x^3$ S-box of Poseidon2, we prove that for a false output claim, the event that some layer's sumcheck accepts a false sum while all earlier carried claims are false has probability at most $(s_{\mathrm{out}} + \sum_i (2 s_i d_i + 1))/|\mathbb{F}|$, where layer $i$ has $2^{s_i}$ wires and $d_i$ bounds the degree of its sumcheck polynomial. We instantiate the bound over the exact quartic extension of the 31-bit KoalaBear field from which small-field provers draw challenges, so that the denominator is $p^4 \approx 2^{124}$, and lift base-field layers and false outputs into it. In a constraint-level model of the compiler, with the hash sub-circuits as abstract functions, the verifier model accepts exactly the valid transitions, and leaf-commitment collisions reduce to sponge collisions. Their composition is mechanized for claims that no witness makes valid, and from the mechanized theorems it follows on paper that the bad event has probability at most this bound for every input that does not encode a valid transition. All bounds concern the interactive public-coin protocol with uniform challenges; the Fiat-Shamir transformation, knowledge soundness and zero knowledge are outside the model.
Authenticated state transitions need proof engines that conserve memory, avoid repeated setup, keep every result bound to its request under parallel execution and return complete proofs at service rates. We present StateSync-GKR, a reusable Rust sumcheck/GKR core with a sparse-Merkle frontend, and evaluate release 1.2.0 against release 1.1 measured on the same day on the same instance types, request corpus and latency budgets. Sparse layer reduction keeps additional requested allocation 3,242-fold and peak process memory about 89-fold below the engine's dense reference at width 4,096. Release 1.2 changes two parts of the software while proof bytes and verifier acceptance stay fixed: reorganized round arithmetic raises prepared proving throughput 2.4 to 2.7-fold on a 192-core bare-metal host, and a new serving path starts each job as soon as a worker is free, bounds queued work and buffered replies, and returns proofs in completion order bound to request identifiers. On a 192-core VM at 1,000 requests/s, 99th-percentile latency to verified acceptance falls from 440 to 34 ms. One connection carries 3,300 requests/s with every request inside one second, confirmed in three 60-second runs and a 30-minute run of 5.94 million requests without a latency or queue trend; at 3,400 requests/s reply traffic reaches the provider's documented 5-Gbit/s single-flow limit, and two connections passed 5,000 requests/s in 15-second screens. In single 15-second screens on 48 cores, the highest passing rate rose from 500 to 2,000/s. Offered 1.5 times its highest screened one-connection rate under a memory limit, with excess offers held back by the client, the worker held its resident memory near a fifth of that limit and left no submitted request unresolved. For an integrating service, fewer servers deliver the same proof rate with bounded tail latency, and existing verifiers accept the GKR proofs unchanged.