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). 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