Verifiable Credentials let an issuer sign attribute claims about a holder, and selective-disclosure schemes let the holder reveal subsets of those claims; but no peer-reviewed system lets the holder prove that a SPARQL query — any non-trivial algebra over multiple credentials — was evaluated correctly against the holder's wallet without revealing more than the query result entails. We close that gap with a circuit-level encoding of a non-trivial fragment of the SPARQL 1.1 algebra (BGP, Join, Filter, OPTIONAL, UNION, bounded property paths, EXISTS, NOT EXISTS, and MINUS) over Merkle-committed signed RDF, modular across both commitment shape (sorted-leaf Merkle and prefix tree) and signature suite (Schnorr, BBS+, SD-JWT-VC, ed25519, ECDSA, with ML-DSA / lattice-BBS as the post-quantum migration target). The encoding is realised as a Noir circuit library; its soundness and completeness are stated against the Pérez–Arenas–Gutiérrez algebra and mechanised in Lean 4 over a Lampe-extracted Noir operational semantics, with a worked numeric primitive (IEEE 754 add_f32) closed end-to-end and the SPARQL-fragment proofs reported with explicitly enumerated open obligations. A disclose-and-verify-externally discipline keeps any deterministic function of the disclosed multiset (DISTINCT, ORDER BY, LIMIT, COUNT, SUM) outside the circuit, so the prover pays no constraints for properties the verifier can re-check on the released bindings. We report empirical results for the sparql_noir implementation against the W3C SPARQL 1.1 evaluation suite and the new zkSPARQL-bench axial benchmark over partitioned LUBM and BSBM, qualifying the prior zkVM baseline's sub-second-prover commitment for queries over up to 10^3 committed triples. A draft W3C-style specification for SPARQL-as-default-VC-query-interface ships as a companion artefact.
The current draft is rebuilt from main on every push.
Four sub-vocabularies back the paper's security analysis. IRIs under https://w3id.org/zkp-sparql/ are placeholders pending the public-release decision.
| Vocabulary | Scope | Serialisation |
|---|---|---|
sec-prop |
Eight security properties (unlinkability, PQ forgery / snooping, leakage) — paper §7.7. | Turtle · JSON-LD |
sig-impl |
Signature scheme implementations (BBS+, SD-JWT-VC, ed25519, ECDSA) and how each realises or fails the eight security properties. | Turtle · JSON-LD |
sec-req |
Regulatory requirement frameworks (eIDAS 2.0, NIST PQC, UK DVS) that pull on `sec-prop` properties. | Turtle · JSON-LD |
prov-ext |
Minimal extensions to `prov-o` for BibTeX-amenable provenance, used only where `bibo:` does not cover a need. | Turtle · JSON-LD |
| Repository | Description |
|---|---|
zkp-sparql-workspace |
Master workspace: paper, Lean proofs, shared tooling. |
sparql_noir |
Noir circuits for the SPARQL fragment (BGP, Join, Filter, OPTIONAL, UNION, property paths, EXISTS, MINUS). |
noir_IEEE754 |
IEEE 754 float primitives in Noir, plus matching Lean equivalence proofs. |
noir_XPath |
XPath primitives in Noir, used by SPARQL FILTER on string-valued literals. |
sparql-zkp-ontologies |
Source vocabularies (yaml-ld) for the four ontologies hosted above. |