From b9338136b951805de739e522bd5656af36e4a9e2 Mon Sep 17 00:00:00 2001 From: Jay Kim Date: Mon, 9 Nov 2026 19:49:57 +0900 Subject: [PATCH 1/2] Update the formal paper entry and the OIP documentation link The StateSync-GKR formal verification paper at arXiv:2610.05335 is now titled Soundness of the GKR Protocol for Sparse-Merkle Updates, with a Machine-Checked Core. Update its Published research entry to that title and to the current abstract, and link the Ethereum Research post that presents both StateSync-GKR papers as one argument. Point the protocol row in SUPPORT.md at the OIP v0.6 documentation. --- SUPPORT.md | 2 +- profile/README.md | 24 +++++++++++++++--------- 2 files changed, 16 insertions(+), 10 deletions(-) diff --git a/SUPPORT.md b/SUPPORT.md index 341a31d..6c5b9ef 100644 --- a/SUPPORT.md +++ b/SUPPORT.md @@ -11,7 +11,7 @@ recovery, incident response, legal advice, or a response-time agreement. | --- | --- | | Organization profile or public-link defect | Issue form in `Oraclizer/.github` | | Repository-specific bug, proof, or documentation question | The affected repository's issue forms and `CONTRIBUTING.md` | -| Protocol semantics and conformance scope | [OIP documentation](https://docs.oraclizer.io/oip-v05/oip-overview/) | +| Protocol semantics and conformance scope | [OIP documentation](https://docs.oraclizer.io/oip-v06/oip-overview/) | | Research paper or artifact | [Research index](https://research.oraclizer.io) and the linked repository | | Sensitive vulnerability | Private path in the affected repository's `SECURITY.md` | | General or research inquiry | `jay@oraclizer.io` | diff --git a/profile/README.md b/profile/README.md index fd470d0..c81d581 100644 --- a/profile/README.md +++ b/profile/README.md @@ -154,20 +154,26 @@ from serving capacity, and each result from its comparison conditions. ### StateSync-GKR formal verification -**Jinwook Kim.** *StateSync-GKR: Machine-Checking the Trust Chain from -Sparse-Merkle State Transitions to GKR Verification.* +**Jinwook Kim.** *Soundness of the GKR Protocol for Sparse-Merkle Updates, +with a Machine-Checked Core.* [arXiv:2610.05335](https://arxiv.org/abs/2610.05335) · [Software DOI](https://doi.org/10.5281/zenodo.23280552) · [Repository](https://github.com/Oraclizer/statesync-gkr) -The paper machine-checks, in Isabelle/HOL, the sparse-Merkle semantics, a -model of the circuit compiler, the GKR and sumcheck reduction, and their -composition, including the exact degree-four KoalaBear extension field that -the implementation uses. A conditional forward acceptance theorem and -recorded proofs for selected Rust contracts relate the model to the shipped -verifier. The exact statements and premises are documented in the -repository's formal-verification guide. +The paper proves per-input soundness for membership, non-membership and +update claims on sparse Merkle trees of every depth, covering cube gates for +the Poseidon2 S-box and challenges from KoalaBear's quartic extension. +Isabelle/HOL also checks a layer-chain bound, the exactness of the verifier's +checks on encoded witnesses in a constraint-level model and, over one field, +their composition for claims with no valid witness. In the repository, a +conditional, mechanized forward acceptance theorem and recorded proofs for +selected Rust contracts relate the model to the shipped verifier; its +formal-verification guide states the exact premises. + +Both StateSync-GKR papers are presented as one argument in the Ethereum +Research post +[GKR with a Machine-Checked Core, and a Sparse Prover Made Faster with Byte-Identical Proofs](https://ethresear.ch/t/gkr-with-a-machine-checked-core-and-a-sparse-prover-made-faster-with-byte-identical-proofs/26226). More protocol, proof, RWA, and economic research is indexed at [research.oraclizer.io](https://research.oraclizer.io). From e58fbf60aaf770491f2f07fd445ca4bae341f51c Mon Sep 17 00:00:00 2001 From: Jay Kim Date: Mon, 9 Nov 2026 19:56:51 +0900 Subject: [PATCH 2/2] Show OIP v0.6 in the organization system map The OIP box in the desktop and mobile system map images still labeled v0.5 as the published version. Change the label to v0.6. Only the label text changes; positions, sizes and the rest of both images are unchanged. --- profile/assets/oraclizer-system-map-mobile.svg | 2 +- profile/assets/oraclizer-system-map.svg | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/profile/assets/oraclizer-system-map-mobile.svg b/profile/assets/oraclizer-system-map-mobile.svg index bd5c2d8..af29e10 100644 --- a/profile/assets/oraclizer-system-map-mobile.svg +++ b/profile/assets/oraclizer-system-map-mobile.svg @@ -38,7 +38,7 @@ ORACLE STATE MACHINE Bidirectional coordination of state transitions - OIP v0.5 · PUBLISHED + OIP v0.6 · PUBLISHED OSS · IN DEVELOPMENT BIND → VERIFY → COMMIT diff --git a/profile/assets/oraclizer-system-map.svg b/profile/assets/oraclizer-system-map.svg index e003885..917e20d 100644 --- a/profile/assets/oraclizer-system-map.svg +++ b/profile/assets/oraclizer-system-map.svg @@ -64,7 +64,7 @@ ORACLE STATE MACHINE Bidirectional coordination of state transitions - OIP v0.5 · PUBLISHED + OIP v0.6 · PUBLISHED OSS · IN DEVELOPMENT BIND → VERIFY → COMMIT