Zk Query Proofs

---
name: zk-query-proofs
description: Prove and verify a SPARQL query result over committed RDF Verifiable Credentials in zero knowledge with sparq-zk + sparq-zk-compose — per-graph Poseidon2 commitments, BGP scan + integer FILTER Noir proofs, issuer Schnorr attestation (incl. hidden-key set membership), status-list revocation (clear- or hidden-index), verifier nonces / single-use replay defence, and the ProofManifest/circuit family. Use when building or driving the zk-query-proofs surface (proving a query answer, verifying a manifest, attesting an issuer, checking revocation). Requires the Noir toolchain (nargo + bb).
---

# sparq-zk-query-proofs

Zero-knowledge proofs that a SPARQL query result is correct over RDF held in named-graph Verifiable Credentials. **`sparq-zk`** (stage 1) canonicalizes (RDFC10) and commits each named graph to a Poseidon2-BN254 commitment `C(G)`, encodes terms, and signs commitments with a Schnorr-over-Baby-JubJub issuer key. **`sparq-zk-compose`** (stage 2) builds per-property Noir circuit inputs (BGP **scan** + hidden-operand integer **FILTER**), drives `nargo`/`bb` to produce/verify proofs, and bundles everything into a serializable `ProofManifest` that a relying party verifies against its own trust anchors (issuer key-set, status list, fresh nonce).

<!-- sq-im8u: the `scaffold-caveat` anchor is single-sourced into
     book/src/getting-started/capabilities.md via mdBook {{#include}}. Load-bearing honesty
     caveat; keep the anchored line link-portable (bead refs + inline code only, no
     repo-relative links) so it renders under both mounts. Keep the ANCHOR markers
     one-per-line — mdBook excludes only the exact marker line. [OPUS-4.8] -->
<!-- ANCHOR: scaffold-caveat -->
> **Research-stage / experimental — NOT-yet-sound.** The composition verifier's soundness is the subject of an open audit (sq-qhy4 / sq-9hrn; remediation epic sq-1s2): a passing proof is NOT a guarantee the SPARQL statement holds under an adversarial prover. Read the "Honest scope" section before relying on a guarantee — only `Simple` entailment is proved; circuit members are fixed buckets. The query fragment covers BGP scans, integer FILTER (and the integer-valued `xsd:double` fragment), and a single-prover hidden cross-credential JOIN — the JOIN restricted to credentials sharing ONE issuer-signed revocation slot (sq-cuvmj; see "Honest scope").
<!-- ANCHOR_END: scaffold-caveat -->

## Prerequisites

- **Noir toolchain on `PATH`** (the only way to prove/verify): `nargo` **1.0.0-beta.21** and Barretenberg `bb` **5.0.0-nightly.20260324** (bb target `noir-recursive`). Other versions may change the bb public-input byte layout the verifier reconstructs against. If `nargo`/`bb` are absent, the structural pre-filter and all host-side helpers still work, but `verify_manifest` / `CircuitProver` cannot.
- **Compiled circuit family** lives at `zk/compose/` in the repo (a Nargo workspace, NOT linked — driven by subprocess). `CircuitProver::from_crate_root()` locates it as `../../zk/compose` relative to the crate.
- **Cargo deps** (both crates are `publish = false`, non-default workspace members — nothing else in sparq depends on them, and there is **no `zk` cargo feature on these crates** to enable; just add them as path/git deps):
  ```toml
  sparq-zk = { path = "crates/sparq-zk" }
  sparq-zk-compose = { path = "crates/sparq-zk-compose" }
  ```

## Quickstart

A self-contained integer-FILTER proof (`5 < 10`) and full verify. Compiles and runs against the current API when `nargo`+`bb` are present (else `prove_in`/`verify` error).

```rust
use sparq_zk_compose::build::{build_filter_int, encode_int_literal};
use sparq_zk_compose::driver::CircuitProver;
use sparq_zk_compose::toml::prover_toml_for;
use sparq_zk_compose::manifest::{CircuitId, FieldHex, FilterOp};

// 1. Build inputs: prove the hidden operand 5 satisfies `?v < 10`, verdict true.
let operand_enc = encode_int_literal(5);                       // term encoding of "5"^^xsd:integer
let (inputs, digits) =
    build_filter_int(operand_enc, /*value*/ 5, FilterOp::Lt, /*bound*/ 10, /*expected*/ true)
        .expect("a compiled filter_int member fits");

// 2. Render the Prover.toml (challenge = the verifier's nonce; 0x2a here).
let challenge = FieldHex("0x2a".into());
let (id, toml) = prover_toml_for(&inputs, &challenge, &[], &[], &digits);
assert_eq!(id, CircuitId::FilterInt { d: 1 });

// 3. Prove + verify via nargo/bb subprocesses (tag isolates concurrent provers).
let prover = CircuitProver::from_crate_root();
let out = std::env::temp_dir().join("sparq_zk_quickstart");
let art = prover.prove_in(&id, &toml, &out, "quickstart").expect("prove");
assert!(prover.verify(&art, &out.join("verify")).expect("verify runs"));
```

## Key APIs

Stage 1 (`sparq-zk`):
- `encode::salt_from_bytes(&[u8;32]) -> Fr` — a per-graph bnode salt. In trusted ingest use `ingest::IngestedDataset` instead (mints a fresh globally-unique salt per graph).
- `commit::commit_triples(triples: &[Triple], salt: Fr) -> Result<GraphCommitment, CommitError>` and `commit::commit_graph_content(&sparq_core::Graph, salt) -> Result<GraphCommitment, _>`. `GraphCommitment { canonical, leaves, commitment: Fr, salt: Fr }`.
- `commit::CommitmentMethod` (sq-zzxt, config-only — selects HOW a graph was committed over the `zk:scheme` slot): `StringCanonicalV1` (the byte-unchanged `DEFAULT`/back-compat anchor) · `DualLeafV1` · `ValueOnlyV1` (only under the OFF-by-default `commitment-value-only` feature — a **benchmark/research dial, never a production default**). A **closed, fail-closed enum**: `from_scheme_iri(iri) -> Option<Self>` returns `None` on an unknown/unselectable IRI (never a default). `scheme_iri()`/`scheme_node()` serialize it; `removes_inv_vl()` / `is_production_selectable()` report the honest per-method posture. `RegistryEntry::method() -> Option<CommitmentMethod>` / `RegistryEntry::with_method(m)` read + record the selection on a registry entry. **Config plumbing only — no circuit, no leaf-shape change** (the dual-leaf/value-only encodings + the per-method circuit dispatch are separate audit-gated beads); selecting `dual-leaf` records the #769-accepted INV-VL downgrade (value↔lexical agreement rests on trusted-issuer honesty), an open external-audit obligation (CR-G8 / sq-qhy4), and asserts NO soundness/privacy property. <!-- privacy-claims-allow: opt-in config plumbing only; dual-leaf INV-VL downgrade framed as an OPEN audit obligation; asserts no soundness/privacy property; sq-qhy4 / CR-G8 -->
- `dual_leaf::*` (sq-xojl, behind the OFF-by-default `dual-leaf` feature — the host mirror of the `filter_value_dl_int` circuit member): `encode_literal(&Literal) -> Result<DualLeafComponents, DualLeafError>` encodes a NON-NEGATIVE `xsd:integer` under the dual-leaf shape `Enc = h3(h3(VALUE_HOOK, DATATYPE_CONST, LANG_NONE), lexical_component, TYPE_CODE_LITERAL)` with **fail-closed same-leaf co-binding** (derives the value handle and the lexical hash from the SAME parse; a non-canonical / signed / overflowing form is rejected, so sparq's own ingest cannot self-desync); `DualLeafComponents { value_hook, datatype_const, lexical_component }` exposes `.value_component()` / `.leaf()` so the verifier/circuit cross-check reconstructs the committed `operand_enc`; `lexical_component` is byte-identical to the string-canonical `h_s` (identity ops unchanged). Selecting dual-leaf carries the #769-accepted **INV-VL downgrade** (value↔lexical agreement on the value-FILTER lane is trusted-issuer-honesty, NOT machine-enforced), an open external-audit obligation (CR-G8 / sq-qhy4); it asserts NO soundness/privacy property (estate NOT externally audited). Datatype classes ([OPUS-4.8] sq-2ezsx adds double + decimal): `encode_literal` (integer, sq-xojl), `encode_double` (`xsd:double` — accepts canonical scientific notation plus `INF`/`-INF`/`NaN`, rejecting Rust-parser extensions such as lowercase `e`, leading `+`, and redundant zeros; value handle = the SPARQL-numeric CANONICAL IEEE bits via `canonical_f64_bits`, so `-0.0`/`+0.0` and all NaN payloads collapse to ONE handle; [GPT-5.6] sq-vh829), `encode_decimal` (`xsd:decimal` — value handle = the SIGNED scaled magnitude at the lexical's canonical fraction scale, with the scale folded into `datatype_const` via `decimal_datatype_const(fd)` so `"5.0"`/`"5.00"` get distinct handles). Both are fail-closed co-binding (a non-canonical form is rejected). **Whole-graph HOST commitment builder ([OPUS-5] sq-vvfte — the §11 bead-2 host slice):** `encode_term_dual(&Term, &Fr) -> Result<Option<Fr>, DualLeafError>` / `encode_triple_dual(&Triple, &Fr)` / `commit_triples_dual(&[Triple], Fr) -> Result<DualGraphCommitment, DualCommitError>` / `commit_graph_dual(&sparq_core::Graph, Fr)` are the `DualLeafV1` mirror of `encode.rs`/`commit.rs` — SAME RDFC10 canonicalization, SAME canonical leaf order (index = leaf index), SAME single flat Poseidon2 sponge; only the per-term leaf SHAPE changes to the design §3.2 value-first tuples: IRI `h3(NO_VALUE, blake3(iri), TYPE_CODE_IRI)`, blank node `h3(NO_VALUE, h2(salt_G, blake3(label)), TYPE_CODE_BLANK_NODE)` (Q6 salt-scoped inner retained), a hookable literal its lane encoder's `.leaf()`, and `xsd:string`/`rdf:langString`/opaque literals the DATATYPE-FOLDED degenerate `h3(h3(VALUE_NONE, blake3(datatype IRI), LANG_CONST), h_s, TYPE_CODE_LITERAL)` (design Q1's leaf-SHAPE choice resolved proceed-and-document, epic-owner sq-1s2.1; `LANG_CONST` = `lang_const(lang)` for `rdf:langString`, `LANG_NONE` otherwise). What separates a degenerate `value_component` from a real one **in this build** is the datatype-folded tuple plus the ROUTING discipline — slot 1 (`DATATYPE_CONST`), not slot 0: every hookable datatype is routed to its lane encoder by `encode_literal_dual` (so a hookable `DATATYPE_CONST` never carries a degenerate `value_component`), and no real `VALUE_HOOK` is ever emitted under a non-hookable one (`xsd:string`, `rdf:langString`, an opaque datatype). That routing argument is what the scoped test pins, and it does **NOT** retire the design's reserved-tag invariant: `research/zk-field-native-encoding.md` §14.1 additionally REQUIRES `VALUE_NONE` to be a domain-separated `blake3_field` constant ASSERTED outside the whole reachable handle band `[0, 2^64) ∪ (p − 2^64, p)`, host-side and in Noir — precisely because the routing argument stops holding the moment any lane degrades instead of rejecting. The shipped `VALUE_NONE = 2` sits INSIDE that band, so that invariant is **NOT discharged**: it stays an OPEN external-audit obligation (§14.3, CR-G8 / sq-qhy4), and the test proves only current routing plus `VALUE_NONE ∉ {0,1}` for the two unrouted boolean hooks — not the cross-lane reserved-tag exclusion. IRI / blank-node leaves instead take the FLAT slot-0 `NO_VALUE` sentinel (the same reserved tag, unfolded — they have neither a datatype nor a language to fold), and are separated from literals by the `TYPE_CODE` in slot 2 regardless. The slot-1 lexical component is byte-identical to the string-canonical `h_s` for EVERY term class, so term identity is unchanged. **Fail-closed ingest:** a literal on a HOOKABLE lane (`is_hookable_datatype`) whose lexical the lane encoder rejects fails the WHOLE commitment (`DualCommitError::Leaf`) — NEVER a silent string-lane downgrade (that downgrade is the §6 desync); an RDF-1.2 triple term yields `Ok(None)` → `DualCommitError::UncommittableTerm`. The `xsd:boolean` and `xsd:dateTime`/`xsd:date` lanes are a documented, tested SEAM (not yet routed; their degenerate/real value components still cannot collide — `VALUE_NONE ∉ {0,1}` and the dateTime/date `datatype_const`s are scale-folded). HOST slice ONLY — no circuit/verifier change (the scan/join leaf recompute, `reconstruct_public_inputs`, and the cross-vectors are the paired follow-on), and the DEFAULT `string-canonical` pipeline is byte-unchanged. <!-- privacy-claims-allow: opt-in dual-leaf host encoder; INV-VL downgrade framed as an OPEN audit obligation; fail-closed co-binding is a host mitigation, not a guarantee; asserts no soundness/privacy property; sq-qhy4 / CR-G8 -->
- `dual_leaf_boolean::encode_boolean(&Literal)` ([FABLE-5] sq-hh7a4) and `dual_leaf_datetime::{encode_datetime, encode_date}(&Literal)` ([FABLE-5] sq-we9vs) — the remaining **dual-leaf value lanes**, behind the SAME OFF-by-default `dual-leaf` feature, returning the SAME `DualLeafComponents` under the SAME fail-closed same-leaf co-binding as `dual_leaf`. The full lane set is therefore **integer · decimal · double · boolean · dateTime · date**. **`xsd:boolean` (design §3.3):** `VALUE_HOOK` = `0` (false) / `1` (true) under `datatype_const(XSD_BOOLEAN)` with the `LANG_NONE` sentinel; ONLY the canonical lexicals `"true"`/`"false"` are accepted — the XSD-legal but NON-canonical spellings `"1"`/`"0"` (and any other lexical form or datatype) are REJECTED with a `DualLeafError`, never silently canonicalised, so sparq's own commitments cannot self-desync. The handle is injective on the two boolean VALUES but MANY-TO-ONE on the TERM (reject-list (v): `"true"` and `"1"` denote one value), which is exactly why `lexical_component` stays EXACTLY the string-canonical `h_s = blake3_field(literal.to_string())` — identity ops (`sameTerm`/`DISTINCT`/`join`) keep term identity unchanged. **`xsd:dateTime` / `xsd:date` (design §13):** `VALUE_HOOK = sign(T) * |T|` where `T` = milliseconds from `1970-01-01T00:00:00Z` on the XSD proleptic-Gregorian `timeOnTimeline` (NO leap seconds — XSD's timeline has none), at the member-fixed sub-second scale `EPOCH_SCALE_FS = 3`; canonical lexicals with `1..=FS` fraction digits are scaled UP to `FS` exactly, NEVER rounded (rounding would break injectivity AND desync the §6 co-binding), the sign is folded by field negation (mirroring `encode_decimal`) and `-0` cannot arise. `FS` is folded into the lane constant exactly like the decimal `@scale=` bind (B4): `datetime_datatype_const()` = `blake3("<xsd:dateTime IRI>@epochscale=3")` and `date_datatype_const()` = `blake3("<xsd:date IRI>@epochscale=3")`, so a hook at one scale can never collide a hook at another and `xsd:date` is its OWN lane (its hook is the scaled epoch of the date's STARTING instant, midnight UTC — XSD orders dates by their starting moment), which is load-bearing because the two hooks collide NUMERICALLY (`"1970-01-02Z"` and `"1970-01-02T00:00:00Z"` both hook `86_400_000`). **The §13.2 timezone rule — hookable domain = timezoned `Z` ONLY:** accepted lexicals are strict XSD-canonical `Z`-timezoned forms; fail-closed REJECTED (a `DualLeafError`, never a silent desynced leaf, never an implicit timezone) are **bare / un-timezoned** lexicals (XSD order between an un-timezoned and a timezoned value is PARTIAL — indeterminate inside the ±14:00 window — and mapping both into one scalar domain would compare indeterminate pairs determinately, inconsistent with the engine's own residual partial order, sq-2k5py), **non-`Z` offsets including `+00:00`/`-00:00`** (offset-normalisation is the documented §13.6 widening, NOT this module), **`24:00:00`** (two lexicals for one value) and the **leap second `60`** (not an XSD lexical), non-canonical year zeros, fractions with more than `FS` digits or a trailing zero, and a scaled-epoch magnitude overflowing `u64` (far-proleptic years — rejected, never wrapped, mirroring the integer lane). Within that domain the hook is injective-on-value within the datatype and, in slice 1, injective on the TERM too (the `Z`-only canonical domain admits one lexical per value), so no new row joins the §3.3 many-to-one hazard table until the §13.6 offset widening lands; `lexical_component` again stays EXACTLY the string-canonical `h_s`. Both lanes are the HOST half ONLY (no circuit/verifier change lands with them) and both inherit the #769-accepted **INV-VL downgrade** — value↔lexical agreement on the value-FILTER lane rests on TRUSTED-ISSUER HONESTY, not machine enforcement, and the §6 co-binding binds honest sparq ingest ONLY, not a malicious external issuer. The §13 rule set is itself registered as an OPEN external-audit obligation (gap **CR-G8** / `sq-qhy4`). Neither asserts a soundness or privacy property; the estate is NOT externally audited. Note the SEAM: these two lanes are deliberately NOT yet joined to `dual_leaf::is_hookable_datatype`, so under the whole-graph builder such literals still take the DEGENERATE string lane (see the `dual_leaf::*` entry). <!-- privacy-claims-allow: opt-in host encoders for two dual-leaf value lanes; the INV-VL downgrade and the §13 rule set are framed as OPEN audit obligations; the fail-closed co-binding is described as a host mitigation binding honest ingest only, not a guarantee; asserts no soundness/privacy property; sq-qhy4 / CR-G8 -->
- `ingest::IngestedDataset::ingest(store: &Graph, names: &[NamedNode]) -> Result<Self, IngestError>` — per-named-graph commitments, each under a fresh OS-random salt; `.commitments()`, `.salts()`, `.names()`.
- `sig::SecretKey::{from_seed(u64) /*test/tooling only*/, public_key(), sign_commitment_with_status(&Fr c, &Fr salt, &Fr status_ref) -> String}`; free fns `commitment_message_with_status`, `status_ref_digest(&Fr list_id, index, version)`, `status_list_id_to_field(iri)`, `public_key_to_hex` / `public_key_from_hex`, `verify`, and `SignatureScheme::Poseidon2SchnorrV1`. **`PublicKey::is_prime_order()`** (sq-l15mi, audit H-1) gates a key as on-curve + prime-order-subgroup (`[L]·pk == O`) + non-identity: Baby-JubJub has cofactor 8, so a torsion/low-order key admits a no-secret Schnorr forgery on the hidden-issuer path. `public_key_from_hex`, `key_set_leaf`, and `in_circuit_witness` fail-closed unless prime-order (`PublicKey`'s inner field is `pub`, so a torsion point can be constructed directly); the in-circuit `issuer.nr::schnorr_verify` mirrors this with `assert_in_prime_order_subgroup` on `pk` and `R`. This closes ONE finding; the estate is still audit-gated (sq-qhy4). <!-- privacy-claims-allow: describes a soundness-hardening guard + its scope; explicitly states it closes one finding and the estate remains NOT externally audited (sq-qhy4) -->.
- `sig::IssuerSignatureScheme` (sq-1hsl, the **OFF-circuit signature seam** — an OPEN trait, distinct from the CLOSED in-circuit `CommitmentMethod` enum because signature verification is verifier-side): `cryptosuite_iri() -> &str`, `verify_message(pk_hex, &Fr m, sig_hex) -> bool` (fail-closed, never panics), `in_circuit() -> InCircuitVerifier::{None, Native{member_hint}}` (the honest discriminator: whether a scheme has a native in-circuit verifier). `SchnorrBjjScheme` is the first/default impl — byte-for-byte the existing `public_key_from_hex`+`signature_from_hex`+`verify` path (back-compat), reporting the `hidden_issuer` native member. `resolve_signature_scheme(cryptosuite_iri) -> Option<Box<dyn IssuerSignatureScheme>>` (fail-closed; in lock step with `SignatureScheme::from_cryptosuite_iri`) and `verify_commitment_with_scheme(cryptosuite_iri, pk_hex, &Fr m, sig_hex) -> bool` (resolve + verify; no default fallback) compose the seam — independent of the commitment-method axis. The trait is the additive extension point for a second verifier-side scheme (an EdDSA/ECDSA-over-a-VC ingest bridge); only the Schnorr scheme is implemented today, and the trait asserts **no** soundness/privacy property (estate NOT externally audited, sq-qhy4). <!-- privacy-claims-allow: open trait BOUNDARY + Schnorr impl moved behind it byte-unchanged; only the in-tree Schnorr scheme is implemented; explicitly asserts no soundness/privacy property; sq-qhy4 -->
- `secprop::*` (sq-bevd3, behind the OFF-by-default **`secprop-annotations`** feature — the machine-readable form of `research/zk-configurable-commitment-security.md` §4, the per-method security posture): a STATIC annotation graph (`ontologies/secprop-methods.ttl`) keyed on the `zk:scheme`/`zk:cryptosuite` IRIs the registry records, parsed to a typed model via `parse_annotations() -> BTreeMap<String, MethodAnnotations>`. Each `MethodAnnotations { method, assertions }` holds `PropertyAssertion { property, level, assurance: Assurance::{Proven, Claimed, Conjectured}, audit_status, assumption, scope: Scope::{QueryProofLayer, SourceLayerOnly} }`. The three over-claim GUARDS are public: `audit_overclaim_violations(&ann)` (guard 1 — no `Proven` on a positive property while `audit_qhy4_open()` is `true`; only settled NEGATIVES `PQForgeable`/`Replayable`/`SchemeRevealed` may be `Proven`), `completeness_violations(&ann, &production_method_iris())` (guard 3 — every production-selectable `zk:scheme` is annotated), and `source_layer_transfer_violations(&ann, &constraints)` + `MethodAnnotations::admits_query_proof_property(property, level)` (guard 2 — a `SourceLayerOnly` property NEVER satisfies a query-proof constraint; `zk:sourceCryptosuite` is provenance, design §5.3). It RECORDS claims + their epistemic basis — it is **NOT** a proof; the dual-leaf soundness assertion carries an explicit `secx:IssuerHonesty` assumption (the #769-accepted INV-VL downgrade) and stays `Claimed`; `value_only_posture()` returns the OFF-by-default research dial's prose posture (never a graph subject). The `secx:` vocabulary is single-sourced in the dependency-free `sparq-secprop-vocab` leaf crate ([#3705](https://github.com/sparq-org/sparq/issues/3705)), which owns the constants, the canonical `secprop-ext.ttl` and the one TTL drift test; this feature takes that (zero-dependency) edge, so the IRIs are imported, not redeclared. Before #3705 sparq-trust owned them and, because sparq-trust depends on sparq-zk, the reverse edge was a cycle — so they were copied here and pinned by a cross-package `include_str!` (which also broke `cargo package` for this crate). Both the copies and `LOCAL_SECX_IRIS` are gone; `SEC_PROP_NS` and `SECX_EXTERNAL_SIGN_OFF_PENDING` remain, re-exported from the leaf. Asserts NO soundness/privacy property (estate NOT externally audited, sq-qhy4); the assurance default is `Claimed` and no method is `Proven` on a positive property while sq-qhy4 is open. <!-- privacy-claims-allow: opt-in annotation graph that RECORDS claims + epistemic basis; the over-claim guards forbid Proven on a positive property while sq-qhy4 is open; explicitly asserts no soundness/privacy property; sq-qhy4 / CR-G8 -->
- `vc_bridge::*` (sq-9c5e, behind the OFF-by-default `vc-bridge` feature — the **OFF-circuit W3C VC ingest bridge**, design §5): brings a W3C Data-Integrity VC into the commitment pipeline. `VcCryptosuite::{EddsaRdfc2022, EcdsaRdfc2019}` + `from_token`/`token` (fail-closed; `bbs-2023`/`ecdsa-sd-2023` never resolve HERE — they belong to the DELEGATING `vc_bridge_sd` seam below). `ecdsa-rdfc-2019` carries TWO curve profiles under one token and the token does not name the curve, so it is resolved from the issuer key by `EcdsaProfile::from_sec1_key(&[u8]) -> Result<EcdsaProfile, VcBridgeError>` (SEC1 33B/65B -> `P256`/SHA-256; 49B/97B -> `P384`/SHA-384; 67B/133B P-521 -> `UnsupportedKeyCurve`; anything else -> `MalformedPublicKey`) BEFORE the hash is taken (sq-txg1y). `verify_source_proof(credential: &[Triple], proof_config: &[Triple], suite, issuer_pk: &[u8], signature: &[u8]) -> Result<(), VcBridgeError>` (and `verify_source_proof_by_token(.., cryptosuite_token: &str, ..)`, which resolves the W3C token fail-closed first) RDFC10-canonicalises the credential + proof-config, derives the suite's `hashData` (`proofConfigHash || documentHash`) via `hash_data_from_triples` (SHA-256, 64B — Ed25519 + ECDSA-P256) or `hash_data_from_triples_sha384` (SHA-384, 96B — ECDSA-P384), and verifies the source proof OFF-circuit with the REAL Ed25519 (`ed25519-dalek`) / ECDSA-P256 (`p256`) / ECDSA-P384 (`p384`) verify path — fail-closed (`VcBridgeError::{UnsupportedCryptosuite, UnsupportedKeyCurve, MalformedPublicKey, MalformedSignature, VerificationFailed, …}`) on a malformed/out-of-scope key/signature/cryptosuite or a non-verifying proof, never a panic. `ingest_verified_vc(document, credential, proof_config, suite, issuer_pk, signature, salt) -> Result<IngestedCredential, VcBridgeError>` verifies FIRST then re-commits (`commit_triples`); `IngestedCredential::registry_entry()` records `zk:sourceCryptosuite` (the verbatim source W3C suite token) alongside `C(G)`. **Provenance only — NOT a re-verifiable in-proof property** (§5.3): the query proof binds to sparq's `Poseidon2SchnorrV1` commitment signature and does NOT re-check the VC's Data-Integrity proof in-circuit. The RDF-native surface above takes triples; the ADDITIVE `vc_bridge_json::*` layer (same `vc-bridge` feature, sq-txg1y) adds the JSON-LD **envelope** entry points — `parse_vc_json(vc_json: &str, contexts: &[(&str, &str)]) -> Result<VcEnvelope, VcBridgeError>` splits a DI-secured VC into `VcEnvelope { credential, proof_config, cryptosuite, verification_method, signature }` (strip `proof`; proof config = proof − `proofValue` with the document's `@context` per DI §3.2.2; `z`/base58-btc multibase decode; expand both halves to RDF with `oxjsonld`), and `verify_vc_json(vc_json, contexts, issuer_pk) -> Result<VcEnvelope, VcBridgeError>` runs the SAME off-circuit check on the result. `contexts` IS the `@context` allowlist — NO network, an unlisted context URL is refused by name (`JsonLdExpansion`); named-graph expansion is refused, not flattened (`NamedGraphUnsupported`); a `proof` array (proof set/chain) is refused. No `did:` resolution anywhere (caller supplies resolved key bytes and must itself check `verification_method` names them). NOT externally audited (sq-qhy4); asserts no in-circuit / query-soundness property. <!-- privacy-claims-allow: opt-in OFF-circuit ingest-time DI verifier; explicitly provenance-only and NOT a re-verifiable in-proof property; asserts no in-circuit/query-soundness property; sq-qhy4 -->
- `vc_bridge_sd::*` (sq-u5y1f, same OFF-by-default `vc-bridge` feature — the **selective-disclosure ingest SEAM**, design §5.3): the DELEGATION boundary for `bbs-2023` / `ecdsa-sd-2023`. **sparq implements NO selective-disclosure verifier** — no BBS pairing check, no `ecdsa-sd-2023` base/derived-proof check, no proof that the disclosed subset really is a subset of an issuer-signed statement set — so the host plugs its own audited one in via the object-safe `trait SelectiveDisclosureVerifier { fn id(&self) -> &str; fn supports(&self, suite: SdCryptosuite) -> bool; fn verify_derived_proof(&self, p: &SdPresentation<'_>) -> Result<(), String> }` (the rejection reason is a plain `String`, so a delegated reject can never be mistaken for one of sparq's own in-repo outcomes). `SdCryptosuite::{Bbs2023, EcdsaSd2023}` + `from_token`/`token` is a DELIBERATELY SEPARATE type from `VcCryptosuite` and the two token spaces are disjoint in both directions (an SD token never reaches the in-repo Ed25519/ECDSA paths; an `rdfc` token never reaches a delegated one). `SdPresentation { suite, disclosed_credential: &[Triple], proof_config: &[Triple], derived_proof_value: &[u8], issuer_pk: &[u8] }` carries the derived (disclosed-subset) credential — `derived_proof_value`/`issuer_pk` are OPAQUE to sparq and forwarded byte-for-byte; `SdPresentation::canonical_nquads() -> Result<(String, String), VcBridgeError>` offers sparq's RDFC10 as `(proof_config, credential)` so a host verifier need not bring a second implementation. `verify_disclosed_proof(&SdPresentation, &dyn SelectiveDisclosureVerifier) -> Result<(), VcBridgeError>` gates on `supports` FIRST (an unsupported suite never reaches `verify_derived_proof`) then delegates; `ingest_disclosed_vc(document, &SdPresentation, &dyn SelectiveDisclosureVerifier, salt) -> Result<IngestedSdCredential, VcBridgeError>` rejects an empty disclosed subset (`EmptyCredential`) BEFORE delegating, delegates FIRST, and only then re-commits the DISCLOSED subset (byte-identical to `commit_triples` over the same triples — the seam changes *who verified*, never *what is committed*). `IngestedSdCredential { document, commitment, source_cryptosuite, verifier_id }::registry_entry()` records `zk:sourceCryptosuite` (provenance only, exactly as the `rdfc` path — NOT a re-verifiable in-proof property); `verifier_id` stays OUT of the registry graph. **FAIL-CLOSED DEFAULT:** the only in-repo impl is `UnavailableSdVerifier`, whose `supports` is `false` for every suite and whose `verify_derived_proof` always errors — so with no host verifier an SD credential CANNOT be ingested (`VcBridgeError::SelectiveDisclosureUnavailable(token)`; a host reject is `SelectiveDisclosureRejected(reason)`). Adds NO dependency (the BBS/SD crypto stays outside sparq). `vc_bridge_json` is UNCHANGED and still `z`/base58-btc only, so a real `u`/base64url derived-proof document does not round-trip through it yet. NOT externally audited (sq-qhy4); asserts NO selective-disclosure soundness, unlinkability, or in-circuit / query-soundness property — those belong to the host verifier. <!-- privacy-claims-allow: opt-in DELEGATION seam that implements no SD verifier and explicitly disclaims SD soundness/unlinkability; fail-closed without a host verifier; provenance-only; sq-qhy4 -->

Stage 2 (`sparq-zk-compose`):
- `build::{Pattern, Slot::{Const(Term), Var}, build_scan(&[GraphCommitment], &Pattern) -> Option<BuiltScan>, build_filter_int(operand_enc, value, op, bound, expected) -> Option<(ProofInputs, Vec<u8>)>, encode_int_literal(u64) -> FieldHex}`. `BuiltScan { inputs: ProofInputs, witness: ScanWitness { counts, enc } }`. Composable signed/decimal FILTERs: `build_filter_signed_int(operand_enc, value: i64, op, bound: i64, expected) -> Option<(ProofInputs, FilterSignedWitness)>`, `build_filter_decimal(operand_enc, neg, int_part: &str, frac: &str, op, bound_neg, bound_scaled: u64, expected) -> Option<(ProofInputs, FilterSignedWitness)>` ([OPUS-4.8] sq-7lrq); `FilterSignedWitness { neg, int_digits, frac_digits }` is the private sign+digits witness.
- `toml::prover_toml_for(&ProofInputs, &FieldHex challenge, scan_counts: &[u32], scan_enc: &[Vec<[FieldHex;3]>], filter_digits: &[u8], join_witness: Option<&JoinWitness>, filter_signed_witness: Option<&FilterSignedWitness>) -> Result<(CircuitId, String), ProverTomlError>`. A `JoinEq`/`FilterSignedInt`/`FilterDecimal` input without its witness returns `Err(ProverTomlError::{JoinEqMissingWitness, FilterSignedMissingWitness})` (recoverable, never a panic).
- `driver::CircuitProver::{from_crate_root(), compile(&CircuitId), prove_in(&CircuitId, toml: &str, out_dir: &Path, tag: &str) -> Result<ProofArtifacts, DriverError>, gen_witness_tagged, canonical_vk, verify_with, verify}`.
- `verifier::encode_artifacts(&ProofArtifacts) -> String` — the `proof_hex` blob (`len|proof|len|public_inputs|vk`) to put in a `SubProof`.
- `capture::{CapturedSubProof::from_artifacts(member, relation, &ProofArtifacts), CapturedCarHireManifest::{new(captured_at, sub_proofs), to_pretty_json}, public_inputs_to_hex(&[u8]) -> Result<Vec<String>, CaptureError>, CAR_HIRE_CAPTURE_NOTE}` — packages native per-circuit `ProofArtifacts` into the **browser-shippable captured manifest** the `/showcase/zk-car-hire` in-tab verify fallback consumes (sq-1s2.3 / FL1 follow-up): proof bytes as a `number[]`, bb's `public_inputs` blob split into `0x`-field-hex words, plus the honest baked note. Pure serialization (no toolchain); the vk is never bundled (audit #2). Browser re-verify needs the sub-proof proved under bb.js's `evm`/keccak flavour (a driver follow-up). Research-grade, NOT externally audited (sq-qhy4); an in-tab verify of a bundled sub-proof does NOT establish composition soundness. <!-- privacy-claims-allow: captured-manifest packaging only; asserts no soundness/privacy property, NOT externally audited; sq-qhy4 -->
- `verifier::verify_manifest(&ProofManifest, &CircuitProver, work_dir: &Path, &KeySet, &RevocationPolicy, &VerifierNonce, &dyn SeenNonces) -> Result<(), CheckError>` — **the full-binding entry point** (the only path that runs every gate; an internal re-audit finds it sound-as-landed under its stated threat model, but it is **pending external cryptographer sign-off — treat it as NOT-yet-sound for production**, see [SECURITY.md](../../SECURITY.md) / sq-qhy4). `prefilter_manifest_structure(&ProofManifest, &KeySet, &RevocationPolicy)` runs only the fast structural gate (no bb, binds nothing to a proof, enforces no freshness — **NOT a sound verifier on its own**). <!-- privacy-claims-allow: negative usage ("NOT a sound verifier on its own") + pending-external-audit caveat; sq-toze.35 -->
- Trust anchors / freshness: `KeySet::{empty, from_hex_keys(I), with_hidden_issuer_depth(u32)}`, `RevocationPolicy::{up_to(now, window), accept_version(v), with_snapshot(StatusListSnapshot), with_hidden_index_depth(u32), with_accepted_set_depth(u32), with_min_version(u64), accepted_entries(), accepted_set_root(), accepted_member_index(list, version), min_version()}`, `VerifierNonce::{from_hex, from_field}`, `FileSeenNonces::open(path)` (durable), `InMemorySeenNonces::new()` (test-only).
- Manifest model: `manifest::{ProofManifest, ProofInputs::{Scan, FilterInt, FilterF64, FilterSignedInt, FilterDecimal, JoinEq}, SubProof { inputs, proof_hex }, BindingEdge, BindingMode::Challenge { challenge }, CommitmentAttestation, AttestedStatusRef, RevocationStatus, StatusListSnapshot, EntailmentRegime::Simple, FilterOp, CircuitId::{Scan, FilterInt, FilterF64, FilterSignedInt{md}, FilterDecimal{id,fd}, …}, FieldHex}`. `ProofManifest::{to_json, from_json}` round-trip via serde.
- Dual-leaf value lane (sq-xojl + sq-cfmv + [OPUS-4.8] sq-2ezsx, behind the OFF-by-default `dual-leaf` feature): `CircuitId::FilterValueDl` + `ProofInputs::FilterValueDl { operand_enc, op, bound, datatype_const, expected }` are the integer value-lane FILTER member — it binds the operand to the dual-leaf commitment via two Poseidon2 permutations over the witnessed `VALUE_HOOK` with **NO in-circuit blake3** (the measured gate win, `gate_count_snapshot.json`), and is DIGIT-COUNT-FREE (one member per datatype class; no `ceil(log10(value))` member-selection leak). **Sibling datatype-class members (sq-2ezsx):** `CircuitId::FilterValueDlF64` + `ProofInputs::FilterValueDlF64 { operand_enc, op, b_bits, datatype_const, expected }` (`xsd:double` — the value handle is the IEEE bits, and the member instantiates B4 IN-CIRCUIT by CANONICALISING `-0.0`/`+0.0` and NaN payloads before the bind, since the term is many-to-one on the value) and `CircuitId::FilterValueDlDecimal` + `ProofInputs::FilterValueDlDecimal { operand_enc, op, bound_neg, bound_scaled, datatype_const, expected }` (`xsd:decimal` — value handle = the SIGNED scaled magnitude; B4 is the canonical-SCALE bind, with the scale folded into the public `datatype_const`, so ONE compiled member serves every scale). **`xsd:boolean` lane ([OPUS-5] sq-5xdlk) — NO new circuit member:** `filter_value_dl_int` already takes `datatype_const` as a PUBLIC input and its `u64` comparison domain covers the boolean value hooks `{0 = false, 1 = true}`, so the boolean lane REUSES `CircuitId::FilterValueDl` + `ProofInputs::FilterValueDl` (same wire tag, same compiled artifact, so bb gate counts are unchanged) and is selected purely by that constant — `manifest::boolean_datatype_const() -> FieldHex` (= `blake3(xsd:boolean IRI)`, the constant the host encoder `sparq_zk::dual_leaf_boolean::encode_boolean` folds into the committed leaf, sq-hh7a4). `build::build_filter_value_dl_boolean(&Literal, FilterOp, bound: bool) -> Result<BuiltFilterValueDlBoolean, DualLeafError>` builds the public inputs + the two private field witnesses from a canonical `"true"`/`"false"` literal (fail-closed on the non-canonical XSD-legal `"1"`/`"0"` and on any non-boolean datatype), disclosing the HONEST verdict computed by `build::boolean_verdict(value, op, bound)` — `EQ`/`NE` plus the DEGENERATE XPath orderings `false < true`, which is exactly the integer relation over the hooks. Lane separation is that public `datatype_const` and only that: it is folded into `value_component`, so an `"1"^^xsd:integer` leaf's honest witness rebinds to a DIFFERENT leaf under the boolean constant and fails the member's `assert_eq(leaf, operand_enc)` (and symmetrically) — a BINDING argument resting on Poseidon2 preimage resistance, NOT an audited soundness claim. Same INV-VL downgrade + CR-G8 / sq-qhy4; NOT externally audited; no soundness/privacy claim. **`xsd:dateTime` / `xsd:date` lane ([OPUS-5] sq-wz99x) — ONE new member serving BOTH lanes:** `CircuitId::FilterValueDlDateTime` + `ProofInputs::FilterValueDlDateTime { operand_enc, op, bound_neg, bound_scaled_epoch, datatype_const, expected }` is the `filter_value_dl_datetime` member — structurally `filter_value_dl_decimal` with a SIGNED SCALED EPOCH value handle (milliseconds from `1970-01-01T00:00:00Z` on the XSD proleptic-Gregorian `timeOnTimeline`, lane-fixed `FS = 3`), reusing that member's UNCHANGED signed fixed-point verdict, so it adds no new comparison machinery. `xsd:date` needs NO second Noir function: its hook is the scaled epoch of the date's STARTING instant (midnight UTC) and the lane is selected purely by the PUBLIC constant — `manifest::datetime_datatype_const()` / `manifest::date_datatype_const()` (= `blake3(IRI ‖ "@epochscale=3")`, exactly what the host encoders `sparq_zk::dual_leaf_datetime::{encode_datetime, encode_date}` (sq-we9vs) fold into the committed leaf). That separation is load-bearing here in a way it is not for the boolean lane, because the two hooks COLLIDE numerically (`"1970-01-02Z"` and `"1970-01-02T00:00:00Z"` both hook `86_400_000`): only the constant, folded into `value_component`, makes the two leaves differ — again a BINDING argument under Poseidon2 preimage resistance, NOT an audited soundness claim. `build::{build_filter_value_dl_datetime, build_filter_value_dl_date}(&Literal, FilterOp, bound: &Literal) -> Result<BuiltFilterValueDlDateTime, DualLeafError>` build the public inputs + the three private witnesses (`value_neg` + `value_hook_scaled` + `lexical_component`), putting BOTH operands through the same encoder so the hookable domain — strict XSD-canonical `Z`-timezoned lexicals ONLY; bare / non-`Z`-offset / `24:00:00` / leap-second / non-canonical-year / over-`FS`-fraction / `u64`-overflowing forms are REJECTED fail-closed, a bare operand for the §13.2 order-INDETERMINACY reason rather than as merely unbuilt — is enforced on the FILTER's constant too, and a cross-lane `date`-vs-`dateTime` comparison is structurally inexpressible through the API. The disclosed verdict is COMPUTED by `build::signed_epoch_verdict(...)`, never taken from the caller. Same INV-VL downgrade, and the whole §13 rule set (`research/zk-field-native-encoding.md`) is itself an OPEN external-audit obligation under CR-G8 / sq-qhy4; NOT externally audited; no soundness/privacy claim. `toml::filter_value_dl_prover_toml(...)` / `filter_value_dl_f64_prover_toml(...)` / `filter_value_dl_decimal_prover_toml(...)` / `filter_value_dl_boolean_prover_toml(...)` / `filter_value_dl_datetime_prover_toml(...)` emit each member's `Prover.toml` (their private witnesses are field elements — `value_hook` (+ `value_neg` for decimal/dateTime) + `lexical_component`; the boolean renderer is the integer one with the lane constant PINNED and `bound: bool` mapped to its hook). **`dispatch::resolve_circuit(CommitmentMethod, &CircuitId) -> Result<CircuitId, DispatchError>`** and `dispatch::resolve_circuit_for_scheme(scheme_iri, &CircuitId)` are the **fail-closed `(commitment-method × circuit)` dispatch matrix** (sq-cfmv): they REJECT a value-lane member against a method with no value handle (`string-canonical`), a string-lane/identity member against `value-only`, an identity op routed at the value lane (reject-list (v)), and an unknown method IRI — `DispatchError::{IllegalPair, IdentityOpAtValueLane, UnknownMethod}`, never a silent mis-dispatch or default. **Wiring the resolver into `verify_manifest` (so the verifier reads the recorded `zk:scheme` and gates each sub-proof) is design bead 6 (depends on the host encoding sq-j506) — the resolver is the self-contained, tested component that bead consumes.** The member + matrix carry the #769-accepted INV-VL downgrade (CR-G8 / sq-qhy4); NOT externally audited; no soundness/privacy claim. <!-- privacy-claims-allow: opt-in dual-leaf value lane + fail-closed dispatch matrix; INV-VL downgrade framed as an OPEN audit obligation; resolver enforces structural legality only and asserts no soundness/privacy property; sq-qhy4 / CR-G8 -->
- Privacy upgrades (opt-in): `issuer::{key_set_root, key_membership_witness, hidden_issuer_prover_toml, HiddenIssuerWitness}`, `holder::{holder_set_root, holder_set_membership_witness, holder_set_prover_toml, HolderSetWitness}` (hidden-holder-SET tier, sq-3c00), and `revocation::{merkle_root, merkle_witness, revoke_prover_toml, MerkleWitness, hidden_ref_witness, revoke_hidden_ref_prover_toml, HiddenRefWitness}`.
- **Fully-hidden revocation — status-list IRI + version HIDDEN (sq-kndw, the deferred remainder of sq-6qe; `research/zk-statuslist-hide-iri-version.md` §3 sub-option A):** the THIRD revocation disclosure mode, usable end-to-end. **Issuer:** sign `sig::status_ref_fully_committed_digest(ref_commitment, index_commitment)` via the existing `SecretKey::sign_commitment_with_status`, where `ref_commitment = sig::status_ref_commitment(H(list), version, ref_blinding)` and `index_commitment = sig::status_index_commitment(index, blinding)`; attach `AttestedStatusRef::fully_hidden(&rc, &ic)`. **Holder:** disclose `RevocationStatus::fully_hidden(&rc, &ic)` (`status_list`/`index`/`version` all absent) and attach a `FullyHiddenRevocation` proof of the `revoke_hidden_ref_d10_a4` member — build it with `revocation::hidden_ref_witness(&policy.accepted_entries()?, set_depth, &snapshot, depth, index)` + `revocation::revoke_hidden_ref_prover_toml(..)`, id `build::derive_revoke_hidden_ref_id(depth, set_depth)` (EXACT-match; only `(10, 4)` is compiled). **Relying party:** opt in with `RevocationPolicy::{with_hidden_index_depth, with_accepted_set_depth}` (+ optional `with_min_version` to pin the public epoch floor as a policy constant rather than a rolling window); `verifier::bind_fully_hidden_revocation` derives the accepted-set root + floor from its OWN freshness-curated snapshots, rebuilds the public inputs from them, and `bb verify`s. **Disclosure floor:** nothing holder-identifying — the statement reduces to "some accepted `(list, version)` at or above the RP's public floor has my hidden index unset". Residual disclosures are policy-side: the accepted-set root (the RP's own policy fingerprint), the public `min_version`, and the member depths `(D, A)` via the vk. **⚠️ Re-blinding is mandatory:** `(ref_commitment, index_commitment)` is a stable per-issuance pair, so reusing it across presentations reinstates full linkability — the issuer must re-blind and RE-SIGN per presentation. The verifier enforces single-use of the pair through the same durable `SeenNonces` store as the nonce defence (`FullyHiddenRevocationLinkageReplay`), but that only helps against an HONEST relying party; the real fix is upstream and is the design's residual operational gap. Fail-closed throughout: a fully-hidden reference without its proof is `FullyHiddenRevocationRequired`, a proof without the reference `FullyHiddenRevocationUnbound`, an unenabled policy `FullyHiddenRevocationNotEnabled`, a prover-chosen anchor `FullyHiddenRevocationAnchorMismatch`. The clear-index and committed-index paths are UNCHANGED. Research-grade; NOT externally audited (sq-qhy4) — no soundness/privacy property is asserted as achieved. <!-- privacy-claims-allow: describes the mode's disclosure floor with the re-blinding requirement and the honest limit of its enforcement stated inline; asserts no soundness/privacy property as achieved; NOT externally audited, sq-qhy4 -->
- Large-registry scaling (sq-8k3h, host-side only): `issuer::{key_set_root_sparse, key_membership_witness_sparse}` and `holder::{holder_set_root_sparse, holder_set_membership_witness_sparse}` build the BIT-IDENTICAL root + authentication path in `O(n·depth)` (no `2^depth` materialisation), so a very large issuer/holder registry commits at any depth. The in-circuit relation is depth-generic and UNCHANGED — these are a drop-in for the dense builders, asserting NO new soundness/privacy property.

## Common recipes

### 1. Commit a credential graph and attest it as an issuer
```rust
use sparq_zk::commit::commit_triples;
use sparq_zk::encode::salt_from_bytes;
use sparq_zk::sig::{SecretKey, status_list_id_to_field, status_ref_digest, public_key_to_hex, SignatureScheme};
use sparq_zk_compose::manifest::{AttestedStatusRef, CommitmentAttestation, FieldHex};

let salt = salt_from_bytes(&[7u8; 32]);                 // production: use IngestedDataset (OS-random)
let commit = commit_triples(&credential_triples, salt).unwrap();

let issuer = SecretKey::from_seed(1);                   // production: generate from OS entropy, NOT a seed
let (list, index, version) = ("http://ex/status/1", 3u64, 1u64);
let status_ref = status_ref_digest(&status_list_id_to_field(list), index, version);

// A scan-covering attestation MUST bind salt AND status reference (fail-closed otherwise).
let attestation = CommitmentAttestation {
    commitment: FieldHex::from_field(&commit.commitment),
    issuer_public_key: public_key_to_hex(&issuer.public_key()),
    signature: issuer.sign_commitment_with_status(&commit.commitment, &salt, &status_ref),
    cryptosuite: SignatureScheme::Poseidon2SchnorrV1.cryptosuite_iri().to_string(),
    salt: Some(FieldHex::from_field(&salt)),
    status: Some(AttestedStatusRef { index, version }),
};
```

### 2. Build a BGP scan proof for `{ ?s <http://ex/age> ?o }`
```rust
use oxrdf::{NamedNode, Term};
use sparq_zk_compose::build::{build_scan, Pattern, Slot};
use sparq_zk_compose::manifest::ProofInputs;

let pattern = Pattern {
    s: Slot::Var,
    p: Slot::Const(Term::NamedNode(NamedNode::new("http://ex/age").unwrap())),
    o: Slot::Var,
};
let scan = build_scan(&[commit /* GraphCommitment */], &pattern).expect("a compiled scan member fits");
// scan.inputs is ProofInputs::Scan { id, commitments, rows, attribution, .. };
// scan.witness has the private per-graph encodings prover_toml_for needs.
let operand_enc = match &scan.inputs {
    ProofInputs::Scan { rows, .. } => rows[0][2].clone(), // the object column to feed a FILTER
    _ => unreachable!(),
};
```

### 3. Assemble + prove a full manifest (scan + bound integer FILTER)
```rust
use sparq_zk_compose::build::build_filter_int;
use sparq_zk_compose::driver::CircuitProver;
use sparq_zk_compose::toml::prover_toml_for;
use sparq_zk_compose::verifier::encode_artifacts;
use sparq_zk_compose::manifest::*;

let challenge = FieldHex("0x2a".into());                 // == the verifier's nonce
let prover = CircuitProver::from_crate_root();
let out = std::env::temp_dir().join("sparq_zk_manifest");

// scan proof
let (scan_id, scan_toml) = prover_toml_for(&scan.inputs, &challenge,
    &scan.witness.counts, &scan.witness.enc, &[]);
let scan_art = prover.prove_in(&scan_id, &scan_toml, &out, "scan").unwrap();

// filter proof `?o >= 18`, verdict true
let (filter_inputs, digits) = build_filter_int(operand_enc, 25, FilterOp::Ge, 18, true).unwrap();
let (f_id, f_toml) = prover_toml_for(&filter_inputs, &challenge, &[], &[], &digits);
let filter_art = prover.prove_in(&f_id, &f_toml, &out, "filter").unwrap();

let manifest = ProofManifest {
    r#type: "urn:sparq:zk:ProofManifest".into(),
    query: "SELECT ?s ?o WHERE { ?s <http://ex/age> ?o FILTER(?o >= 18) }".into(),
    issuers: vec!["did:key:zIssuer".into()],
    key_set: vec![public_key_to_hex(&issuer.public_key())], // declared (narrowing) — NOT the trust anchor
    commitment_attestations: vec![attestation],
    attributions: vec![vec![0]],                            // one BGP pattern, from graph 0
    pattern_scans: vec![vec![0]],                           // recorded reading; carries NO verification weight
    join_obligations: vec![],
    entailment_regime: EntailmentRegime::Simple,
    binding: BindingMode::Challenge { challenge: FieldHex("0x2a".into()) },
    revocation: Some(RevocationStatus::clear("http://ex/status/1", 3, 1)),  // ::committed / ::fully_hidden for the hidden modes
    status_snapshots: vec![],                               // prover copy is only a tripwire; see recipe 4
    sub_proofs: vec![
        SubProof { inputs: scan.inputs,   proof_hex: encode_artifacts(&scan_art) },
        SubProof { inputs: filter_inputs, proof_hex: encode_artifacts(&filter_art) },
    ],
    binding_edges: vec![BindingEdge { from_proof: 0, from_row: 0, from_slot: 2, to_proof: 1 }],
    hidden_revocation: None,
    hidden_issuer_attestations: vec![],
};
let json = manifest.to_json(); // ships to the verifier
```

### 4. Verify a manifest as a relying party (the full-binding path)
```rust
use sparq_zk_compose::driver::CircuitProver;
use sparq_zk_compose::verifier::{verify_manifest, KeySet, RevocationPolicy, VerifierNonce, FileSeenNonces};
use sparq_zk_compose::manifest::{ProofManifest, StatusListSnapshot};
use sparq_zk::sig::public_key_to_hex;

let manifest = ProofManifest::from_json(&json).unwrap();

// External trust anchors — resolved + authenticated OUT OF BAND, never from the manifest:
let trusted = KeySet::from_hex_keys([public_key_to_hex(&issuer.public_key())]); // issuers you trust
let policy = RevocationPolicy::accept_version(1)        // freshness window; or ::up_to(now, window)
    .with_snapshot(StatusListSnapshot {                // AUTHORITATIVE bitstring (bit decision reads HERE)
        status_list: "http://ex/status/1".into(), version: 1, bits: vec![0u8] /* index 3 unset = active */,
    });

let nonce = VerifierNonce::from_hex("0x2a").unwrap();  // mint fresh per session, hand to prover BEFORE proving
let seen = FileSeenNonces::open("/var/lib/sparq/seen_nonces").unwrap(); // durable single-use store

let prover = CircuitProver::from_crate_root();
match verify_manifest(&manifest, &prover, std::path::Path::new("/tmp/verify"),
                      &trusted, &policy, &nonce, &seen) {
    Ok(())  => { /* result is correct, issuer-attested, live, fresh */ }
    Err(e)  => eprintln!("rejected: {e:?}"), // CheckError variant pinpoints the failed gate
}
```
The nonce is **burned on presentation** (consumed even if verification then fails) — a rejection is never a free retry; mint a new nonce for the next attempt.

### 5. Fast structural pre-check without the toolchain
```rust
use sparq_zk_compose::verifier::{prefilter_manifest_structure, KeySet, RevocationPolicy};
// Re-parses the query (Q6 cross-graph bnode-join guard + arity), re-derives circuit ids,
// checks binding edges + issuer/key-set + revocation reference. NO bb, NO freshness.
// [OPUS-4.8] sq-en5dx: the Q6 guard keys each pattern's attribution on committed-graph
// IDENTITY (the answering scan's commitments[g]), NOT the scan-LOCAL index — so a
// genuine cross-scan join over two DISTINCT committed graphs (e.g. two k=1 scans, the
// `[[0],[0]]` alias) requires its non-bnode `join_obligations` entry to be DECLARED,
// while two scans over the SAME graph stay obligation-free. Still under sq-qhy4: NOT sound.
// NOT a sound verifier on its own — always follow with verify_manifest. privacy-claims-allow: negative usage; sq-toze.35
let _required = prefilter_manifest_structure(&manifest, &KeySet::empty(), &RevocationPolicy::accept_version(1))?;
```

### 6. Hidden-index revocation proof (privacy upgrade — index never disclosed)
```rust
use sparq_zk_compose::revocation::{merkle_root, merkle_witness, revoke_prover_toml};
use sparq_zk_compose::manifest::{CircuitId, HiddenIndexRevocation, FieldHex};
use sparq_zk_compose::driver::CircuitProver;
use sparq_zk_compose::verifier::encode_artifacts;

let depth = 10;                                  // compiled member: revoke_unset_d10 (<= 1024 indices)
let root = merkle_root(&authoritative_snapshot, depth).unwrap();
let witness = merkle_witness(&authoritative_snapshot, depth, /*hidden index*/ 3).unwrap(); // witness.bit must be 0
let toml = revoke_prover_toml(&nonce_field, &root, 3, &witness);
let prover = CircuitProver::from_crate_root();
let art = prover.prove_in(&CircuitId::RevokeUnset { depth }, &toml, std::path::Path::new("/tmp/rev"), "rev").unwrap();
// attach to manifest.hidden_revocation; enable on the verifier with
// RevocationPolicy::...with_hidden_index_depth(depth). (Hidden-issuer attestations mirror this
// with sparq_zk_compose::issuer::* + KeySet::with_hidden_issuer_depth.)
```

## Honest scope (what is and isn't supported)

- **Entailment:** only `EntailmentRegime::Simple` is proved cryptographically. `Rdfs`/`Owl` are ENFORCED but NOT in-circuit: the relying party must opt in (`EntailmentPolicy::with_rdfs`/`with_owl`), and the verifier then structurally re-checks every `manifest.derivation_steps` entry against its rule shape and requires each antecedent to be grounded in a DISCLOSED scan row or an earlier derived triple, fail-closed (sq-314). That is a re-check over disclosed data — the antecedents are not hidden — not an in-circuit inference proof. **`owl:sameAs` is refused fail-closed on that path** (`CheckError::EqualityReasoningUnsupported`, sq-rsd3v.6): rule shapes are re-checked by term-encoding equality, which is a term IDENTITY test and therefore the wrong proxy once `owl:sameAs` quotients the term universe, so a step that introduces or consumes an equality is rejected rather than allowed to ride the fixed-shape path. Equality reasoning instead needs the SEPARATE in-circuit union-find canonicalisation gadget (`zk/compose/compose_core/src/sameas.nr`, host mirror + witness builder `sparq_zk_compose::sameas::{CanonTable, CanonEntry, CanonError, OWL_SAME_AS}`) — which has NO compiled circuit member, NO `bb gates` cost measurement, and NO `verify_manifest` dispatch, so nothing composes it yet and no cost or privacy property is claimed for it. Research-grade, NOT externally audited (sq-qhy4).
- **N3 dataset-supplied rules — witnessed rule shape, research-grade (`sq-rsd3v.3`):** RDFS/OWL-RL have a FIXED PUBLIC rule table, so `derivation.nr` hard-codes six shapes behind a tag. An N3 rule set is **dataset-supplied** (`{p1 . p2 …} => {c1 …}`), so `zk/compose/compose_core/src/n3.nr` (`n3_derivation_check`) generalises that member two ways: (a) the **rule author becomes an issuer** — the rule graph is committed to a PUBLIC `rules_root` the circuit recomputes from the witnessed shapes, so the proof says WHOSE rules and an invented rule has no witness (signing that root is the existing `sq-z9l` `issuer.nr` machinery, not this member); and (b) the **rule shape is itself a witness** — each slot is `(kind, konst, var)` and the conclusion must be the rule's conclusion pattern under a substitution that is consistent by construction (an array indexed by variable id). Leaves still anchor to committed-graph membership and join premises still chain to earlier conclusions, so antecedents stay HIDDEN. **SAFETY (every conclusion variable bound in the premise) is enforced in-circuit and is load-bearing, not stylistic:** the substitution is a private witness, so an unbound conclusion variable would let the prover choose the derived triple — `rule_subset_check` runs a binding schedule (join atoms bind their variable slots; arithmetic builtins require bound inputs and bind their output; comparisons bind nothing) and refuses the rule. The whitelisted `math:` builtins are fixed gadgets: the five comparisons reuse `filter_signed`'s `signed_verdict` + canonical-`xsd:integer` operand binding VERBATIM, and `sum`/`difference`/`product` are exact field equations (magnitudes `< 2^64` against a `~2^254` modulus) that fail CLOSED when a result leaves the representable range. Everything else is **rejected, never approximated** — existentials-in-conclusion, `log:notIncludes`/`log:collectAllIn` (a negative over the closure, deferred with completeness), `math:quotient`/`exponentiation`/floats, `string:`/`list:`/`time:`, `log:semantics`/`log:includes`. The refusal is structural: the host gate `sparq_zk_compose::n3::{N3RuleSet, N3Rule, N3Premise, N3Slot, N3Builtin, N3SubsetError}` runs `admit` BEFORE `commit` folds, so **an out-of-subset rule graph has no root** and cannot reach the circuit at all. NO compiled circuit member, NO `bb gates` cost measurement, NO `verify_manifest` dispatch, and no `ProofStep`→slot witness mapper — so nothing composes it yet and no cost or privacy property is claimed. Inherits every `sq-rsd3v.2` caveat; research-grade, NOT externally audited (sq-qhy4). [OPUS-5]
- **Completeness under entailment — UNBUILT, NOT claimed (`sq-rsd3v.7`):** two obligations must never be conflated. SOUNDNESS of derivation ("every disclosed derived triple IS entailed") is what the host-side `derivation_steps` re-check (`EntailmentPolicy` + the verifier's entailment gate, sq-314) and the in-circuit RDFS relation (`zk/compose/compose_core/src/derivation.nr`, sq-rsd3v.2) address — as scoped, and NOT externally audited (sq-qhy4). COMPLETENESS under entailment ("no entailed answer is MISSING", a negative over a fixpoint) is the OTHER obligation and is **not built**: it needs BOTH an in-circuit closure-sweep over the flat full graph AND a fixpoint-saturation proof (no rule fires producing a new triple), and the saturation half exists nowhere in sparq. So a relying party that needs it declares `EntailmentPolicy::require_completeness_under_entailment()` and is REFUSED fail-closed on every non-`Simple` regime (`CheckError::CompletenessUnderEntailmentUnavailable`, whose message names both missing halves) rather than being handed a derivation-only accept it could misread. Passing a `Simple` manifest under that dial is NOT a completeness assertion either, and a closure materialised OFF-circuit and presented as `Simple` is a distinct trust model (entailment trusted to the materialiser's signature) that the dial cannot detect — the relying party must evaluate it separately. Folding / zkVM re-execution — the only shape that natively gives completeness — was measured OUT at credential scale; the documented RE-ENTRY TRIGGER is a huge closure PLUS a verifier demanding full completeness (`research/zk-inference-and-credentials.md` §3.7, §3.6(c); `research/zkp-performance-landscape.md` §5). [OPUS-5]
- **Query fragment:** BGP triple-pattern **scan** (in-circuit per-graph Poseidon2 commitment recompute + row soundness + **scan completeness**) and hidden-operand numeric **FILTER over `xsd:integer`** (`filter_int`, non-negative). `xsd:double` FILTER (`filter_f64`) is composable for the integer-valued fragment (`filter_f64_d{d}`; general fractional/scientific forms deferred). **NEGATIVE `xsd:integer`** (`filter_signed_int`) and **`xsd:decimal`** (`filter_decimal`, fixed-point at a fixed fraction-digit count, host-prescaled bound) are MANIFEST-COMPOSABLE ([OPUS-4.8] sq-1q9h compiled members, sq-7lrq composability wiring): `CircuitId::FilterSignedInt{md}` / `FilterDecimal{id,fd}` + the matching `ProofInputs` variants + `derive_filter_signed_int_id` / `derive_filter_decimal_id` + `build_filter_signed_int` / `build_filter_decimal` + the verifier binding edge + public-input reconstruction, so a signed/decimal FILTER assembles into a `ProofManifest` with the same operand binding as `filter_int`. The GENERAL fractional/scientific `xsd:double` fragment (an in-circuit decimal→IEEE round-to-nearest-even parser over an arbitrary lexical form) remains DEFERRED (sq-7lrq part 2). A **hidden cross-credential JOIN** is proved in-circuit (`join_eq`, single-prover; the join term stays private) — distinct from the verifier-side disclosed-row join. **Scope constraint (sq-cuvmj):** `ProofManifest::revocation` is SCALAR, so every scan-covering commitment must resolve to ONE issuer-signed status reference; a presentation whose two credentials sit on DISTINCT `(list, index, version)` slots is refused fail-closed (`RevocationReferenceMismatch`) before `bind_joins` is reached. So what is validated today is a hidden join across the graphs of ONE credential, or across credentials sharing a status slot — NOT an arbitrary multi-credential join. This is an over-restriction, not a hole (a revoked second credential cannot be smuggled past the liveness check); the per-commitment obligations a future multi-reference migration owes are pre-registered on `ProofManifest::revocation`. **No aggregation.** The Q6 cross-graph bnode-join guard runs from `manifest.attributions` / `join_obligations`. **Within-pattern repeated variable ([OPUS-5] #5240):** a variable used at TWO slots of the SAME BGP pattern (`{ ?v <p> ?v }`) constrains those two disclosed columns to be EQUAL, and `bind_repeated_pattern_slots` enforces it per ACTIVE disclosed row of every scan that matches the pattern by constants (`RepeatedSlotMismatch`). No earlier gate covered it: `scan_matches_pattern` compares only per-slot const-ness and the constant encodings, the scan circuit binds only the CONSTANT slots to `pattern_const_enc`, and every shared-variable gate — `recheck` / `cross_graph_join_obligations` on the disclosed path, `bind_joins` on the hidden path — iterates pattern PAIRS over per-pattern variable SETS and so cannot see a within-pattern repeat. Confirmed empirically reachable before the fix (a manifest disclosing `(alice, knows, bob)` under `SELECT ?v WHERE { ?v <knows> ?v }` was ACCEPTED by `prefilter_manifest_structure`). Like the sq-q9r5e FILTER rule it runs over constant MEMBERSHIP, so a query mixing a repeated-variable and a distinct-variable pattern at the same constant layout is over-demanded and REJECTED fail-closed rather than accepted on the prover's declaration. The `extended-fragment` regime already covered this via `bind_fragment_scans` (its projected-solution and existential-coherence maps are keyed by variable NAME across slots). **Explicit pattern→scan mapping ([OPUS-5] sq-q9r5e follow-up) — RECORDED, NOT LOAD-BEARING:** `manifest.pattern_scans` records, per query BGP pattern (query order, exactly like `attributions`), which `sub_proofs` indices the prover says answer it. It carries NO verification weight. The verifier resolves pattern→scan by constant MEMBERSHIP for every obligation it derives — `bind_query_correctness` (the FILTER slot gate), `bind_attributions` (audit #8), `global_attributions` (Q6) and `bind_joins` all ignore the field — so a manifest carrying a declaration is never accepted where the same manifest without one is rejected; it can only fail additionally, on the well-formedness checks below. That means the sq-q9r5e / audit-L-1 rule stands unweakened: where two patterns share a constant layout (`{ ?x <age> ?v . ?x <age> ?c }` — both `(?, <age>, ?)`) the FILTER must be discharged at EVERY slot the filtered variable occupies across every pattern that scan matches, INCLUDING the over-demand that rejects an honest `(?x=alice, ?v=25, ?c=5)` because the disclosed `5` also matches pattern 0. **Why the declaration does not relax it:** SPARQL evaluates each pattern over every compatible committed row and the query text authorises no prover-chosen partition of the data, so narrowing to the declared mapping would let the prover drop a constant-compatible scan's rows out of a pattern's FILTER and attribution obligations by fiat. Narrowing needs a claimed result row bound to the selected scan rows with all shared-variable joins enforced — a witness the flat manifest cannot express today, and it is NOT built. What the field does buy is fail-closed well-formedness: `check_pattern_scans` rejects a mis-sized declaration (`PatternScanArityMismatch`), an unanswered pattern (`PatternScanUnbound`), a named sub-proof out of range / not a scan / whose bb-bound `pattern_is_const`/`pattern_const_enc` contradict the pattern's constants (`PatternScanMismatch`, audit #10), and a scan declared for NO pattern (`PatternScanUndeclared`) — ADDITIONAL rejections, never a relaxation. An EMPTY `pattern_scans` means "not declared" and skips those checks. NOT externally audited (sq-qhy4).
- **Wave-1 extended fragment gate (query-side, `sparq-zk`):** `sparq_zk::verify::fragment_query` re-derives the *monotone* fragment extensions of `research/zksparql-fragment-extension.md` §3–§4 from the query text — property-path rewrites (predicate/inverse/sequence with deterministic `!`-namespace intermediates), bounded `?`/`*`/`+` closures over an atomic step as `PathReach` obligations (the `path_reach_d{k}` statement family: `k` is a **manifest** public input, never query text; `p?` pins `k=1`), UNION branch lists (joins distribute; capped at `MAX_FRAGMENT_BRANCHES`), VALUES public rows (`UNDEF` = wildcard; triple terms rejected), and subqueries with inner-only variables renamed apart — failing closed on everything else (OPTIONAL / MINUS / (NOT) EXISTS / GRAPH / SERVICE / BIND / aggregates / ORDER BY / `FROM` / subquery LIMIT / non-atomic closures / negated property sets). `verify::branch_obligations` extends the Q6 coarse rule per-branch (path endpoints join like pattern variables; a multi-graph path attribution additionally flags `path_link_non_bnode`). The stage-1 entry points (`fragment_patterns`/`fragment_filters`/`recheck`) are unchanged and still reject the extensions. **Dataset clauses now fail closed on BOTH gates ([OPUS-5] sq-p2hci):** the stage-1 entry points (`fragment_patterns` / `fragment_filters` / `fragment_expr_trees` / `recheck`) previously *ignored* a `FROM` / `FROM NAMED` clause and accepted the query. That was a consumer-honesty defect, not a missing feature — the statement these gates certify is fixed ("these solutions are in the answer over the **committed union**", witnesses drawn from the manifest's public attributions), so a consumer reading `SELECT * FROM <g1> …` off the manifest read the verdict as scoped to `g1` while the proof admitted scans attributed to any committed graph; since the FROM-restricted answer is a *subset* of the union answer, a disclosed solution could be one the query as written does not produce. The clause is also unenforceable here (the graph set is private by design, plan §2.4), so every entry point now rejects it with the same reason `fragment_query` already used. (sq-3kd2g.3; ZK-soundness posture unchanged: internally re-checked, external audit pending — sq-qhy4.)
- **Query-side FILTER/BIND expression-tree extraction (`sparq-zk`, sq-3kd2g.8):** `sparq_zk::verify::fragment_expr_trees(&str) -> Result<Vec<ExprObligation>, VerifyError>` generalizes the single-comparison `fragment_filters` path to a full **typed expression tree** (`ExprTree` = `Var` / `Const` / static `Bound` / `Node{op: ExprOp, args}`) over the design record §5.1 IN-fragment operator set — logical `&&`/`||`/`!`, comparisons across datatype lanes, `sameTerm`, `IN`/`NOT IN` constant lists, `IF`/`COALESCE`, arithmetic, term accessors (`STR`/`LANG`/`DATATYPE`/`isIRI`/`isBlank`/`isLiteral`/`isNumeric`), string / numeric / date-component functions, and the **bounded** (literal + anchored only) `REGEX`/`REPLACE` subset — for both `FILTER` conditions (`ExprObligation::Filter`) and `BIND`/`Extend` targets (`ExprObligation::Bind{target, expr}`). `extract_expr(&Expression)` is the per-expression extractor and `expr_leaf_vars(&ExprTree)` extends the variable→(pattern,slot) map (`variable_slots`) to expression leaves. The tree is re-derived from the query text ALONE, is an EXACT structural image (`!=`/`NOT IN` stay `Not(Eq)`/`Not(In)`; operand order and literal lexical forms preserved), and is FAIL-CLOSED: EXISTS, non-deterministic builtins (`RAND`/`NOW`/`UUID`/`STRUUID`/`BNODE`), term constructors (`IRI`/`STRDT`/`STRLANG`), estate-gap functions (`langMatches`/`TZ`/hash digests, pending sq-3kd2g.4), a `REGEX` beyond the bounded subset, aggregates-in-expression, and every other form yield `UnsupportedFragment`. This is the QUERY side only — it emits the neutral tree the compose verifier (sq-3kd2g.9) will bind a node-per-operator sub-proof estate against (§5.2 Option C); rooting leaves to scan rows and binding nodes to circuits is downstream. The existing `fragment_filters`/`QueryFilter`/`FilterCmp` path is byte-unchanged. (ZK-soundness posture unchanged: no circuit yet, internally re-checked, external audit pending — sq-qhy4.)
- **Wave-1 compose schema + fail-closed dispatch (OFF-by-default `extended-fragment` feature, sq-3kd2g.6):** `sparq-zk-compose` gains, behind the opt-in `extended-fragment` cargo feature, the compose side of the wave-1 fragment: `CircuitId::PathReach{d,k,n}` + `ProofInputs::PathReach` (the `path_reach_d{d}_k{k}_n{n}` member family, sq-3kd2g.2 — `d` is the design record's normative depth bound, disclosed as the public `depth_bound` and re-derived by the verifier; `k` = graph count, `n` = slot bucket), `build::build_path_reach` + `build::derive_path_reach_id`/`smallest_path_reach_id` + `toml::path_reach_prover_toml` (the prover wiring, symmetric to `build_join`/`build_scan`), the public-input reconstruction + `derive_id` binding, the per-solution UNION branch-attribution + VALUES row-index disclosure schema (`manifest::BranchWitness`, carried by the `manifest::FragmentManifest` wrapper — a distinct type so the stage-1 `ProofManifest` schema is byte-unchanged), and the **fail-closed** routing gate `verifier::dispatch_fragment(&FragmentManifest)`: it re-derives the branches from the query text alone (`verify::fragment_query`), then REFUSES (structured `FragmentDispatchError`, never a silent fallback) anything outside the proven-sound fragment — an unknown/mismatched circuit id, a bounded path claimed without a bound `PathReach` sub-proof of the right member, a `k`/depth mismatch (the disclosed `depth_bound` must equal the member's compiled `d`, req 1), a `p+`/`p*` closure disagreement, a `p?` bound to a deeper member, a branch attribution pointing at a non-existent branch, or a VALUES row-index out of range. **End-to-end routing (sq-h732x):** `verifier::verify_fragment_manifest(&FragmentManifest, …)` (same external inputs as `verify_manifest`) now verifies an extended-fragment presentation END-TO-END: it runs `dispatch_fragment` FIRST (fail-closed, before the verifier nonce is burnt or any bb subprocess starts, mapped into `CheckError::FragmentDispatch`), then the SAME crypto stage as `verify_manifest` over the embedded manifest — the per-sub-proof public-input reconstruction + canonical-vk + `bb verify`, nonce single-use + challenge binding, issuer attestation, revocation, holder binding — with stage-1a's query-fragment ACCEPTANCE routed through `fragment_query` (so the extended query is no longer rejected at `recheck`). `verify_manifest` itself is UNCHANGED and still rejects every extended query at its flat stage-1 `recheck` (byte-identical, feature ON or OFF). **Disclosed-solution term binding (sq-1zf94):** `verify_fragment_manifest` now also runs `verifier::bind_fragment_solution` (before the nonce is burnt) — the composition analogue of the flat `bind_query_correctness`/`bind_joins` term binding. `manifest::BranchWitness` gains a `solution: Vec<SolutionBinding>` (disclosed var→`DisclosedTerm`, IRI/literal), and the gate RE-ENCODES each disclosed term itself (`encode_term`, salt-independent for IRIs/literals — never a prover-supplied encoding) and demands, fail-closed (`FragmentSolutionError` → `CheckError::FragmentSolution`): each bound `PathReach`'s `pred_enc` = the query-text predicate encoding; each `src_enc`/`dst_enc` = the query-CONSTANT endpoint's encoding, or the disclosed solution's binding for a PROJECTED endpoint variable (a projected endpoint omitted from the solution is refused); and each disclosed `VALUES` cell = the PROJECTED variable's disclosed binding (a `values_rows` index pointing at a row whose cell disagrees — the "wrong disclosed row" — is refused). Because those `PathReach` public inputs are byte-bound into the bb proof (audit #1 reconstruction), a solution that passes this gate AND the crypto stage has its disclosed endpoints/VALUES terms genuinely tied to the proofs. **BGP scan-slot binding (sq-qyfth):** `verify_fragment_manifest` then runs the sibling gate `verifier::bind_fragment_scans` (also before the nonce is burnt) — the composition analogue of the flat `bind_query_correctness` scan-const check + the disclosed-row/`bind_joins` slot binding, for the LARGEST unbound surface #1673 left (a disclosed solution variable that occurs ONLY in a BGP scan). `manifest::BranchWitness` gains a `scan_rows: Vec<usize>` (one selected disclosed-row index per BGP-scan obligation), and the gate demands, fail-closed (`FragmentScanError` → `CheckError::FragmentScan`): the scan answers the query BGP pattern (`scan_matches_pattern`); a scan pattern carrying a variable has a selected row within the scan's ACTIVE disclosed rows (a missing selection or out-of-range index is refused); each PROJECTED scan variable's selected-row slot = its disclosed-solution encoding (a projected scan var omitted from the solution, or a row whose slot disagrees — the "wrong supporting row" — is refused); and the rows selected for two SCAN atoms sharing an EXISTENTIAL variable agree on its slot value (join incoherence is refused). This closes the BGP-scan-slot residual #1673 named. **Per-branch cross-graph Q6 + scan↔path coherence (sq-ygk6x):** `verify_fragment_manifest` then runs `verifier::bind_fragment_join_coherence` (also before the nonce is burnt) — the branch-local analogue of the flat cross-graph non-bnode obligation (`verify::cross_graph_join_obligations`/`recheck`), extended to path-rewritten obligations. Per branch it (1) binds every existential variable shared between two atoms — INCLUDING a scan slot and a `PathReach` endpoint (`src_enc`/`dst_enc` are public `FieldHex`, directly comparable to a selected scan row slot) — to ONE value by encoding-equality (a path claiming a different node than its supporting scan row, or another path endpoint, supports is refused, both directions — `FragmentJoinError::Incoherent` → `CheckError::FragmentJoin`); (2) re-derives the branch's Q6 obligations with `verify::branch_obligations` over the PROOF-BOUND per-obligation attributions (interned to a per-branch committed-graph identity, the safe-coarser flat discipline) and requires every cross-graph join edge's variable covered by the disclosed data — combined with the ALWAYS-ACTIVE salt-uniqueness gate (audit #9) an equal encoding across a cross-graph edge cannot be a blank node, so the flat non-bnode obligation holds branch-locally for BGP scans; and (3) refuses a multi-graph path (proof-bound attribution admitting >1 committed graph) whose interior-chain non-bnode obligation the verifier cannot discharge from disclosed data (`FragmentJoinError::MultiGraphPath`). **Salt-uniqueness + attestation now cover PATH commitments (sq-nlulr):** `verifier::bind_issuer_attestations` extends the audit-#9 issuer-attestation + salt-uniqueness record to `PathReach`-referenced committed graphs — each path commitment now carries the SAME issuer-attestation requirement + distinct-salt record as a scan commitment (an unattested or salt-colliding path commitment is refused fail-closed, `CheckError::UnattestedCommitment`/`SaltReused`, before any bb sub-proof runs), so a cross-graph scan↔single-graph-path (and path↔single-graph-path) join's non-bnode corollary is discharged by the two graphs being distinctly salted, exactly as for a scan↔scan join. This CLOSED the #1684 residual. **Honest scope — remaining BY DESIGN (not a non-bnode gap):** an EXISTENTIAL (non-projected) path endpoint's value stays hidden (a privacy choice); a multi-graph path is refused fail-closed. So the extended regime now carries the SAME attestation + salt discipline as the flat path for scan↔scan / scan↔single-graph-path / path↔single-graph-path cross-graph joins — enumerated, not hidden. Default builds are byte-identical (feature OFF); no new dependency; ZK-soundness posture unchanged (internally re-audited, external audit pending — sq-qhy4). No soundness/privacy claim.
- **Fixed circuit members only** (build returns `None` for shapes outside these): scan `k∈{1,2}`, `n∈{16,64}`, `r∈{4,8}` — **all eight `(k,n,r)` combinations compiled** ([OPUS-4.8] sq-pzet); `filter_int_d∈{1,2,3,4}`; `filter_f64_d∈{1,2,3,4}`; `filter_signed_int_d∈{2,4}` + `filter_decimal_i3_f2` (compiled AND manifest-composable — sq-1q9h members, sq-7lrq wiring; `md`/`(id,fd)` are EXACT-match, an out-of-family shape returns `None`); `join_eq` `n_a,n_b∈{16,64}` — **all four `(n_a,n_b)` combinations compiled** ([OPUS-4.8] sq-pzet); `revoke_unset_d10` (≤1024 status indices); `revoke_hidden_ref_d10_a4` (fully-hidden revocation, sq-kndw — ≤1024 status indices, ≤16 accepted `(list, version)` pairs); `hidden_issuer_d4` (≤16 issuers); `holder_pok`; `holder_set_d4` (hidden-holder SET, ≤16 holders — sq-3c00). Behind the OFF-by-default `dual-leaf` feature: the DIGIT-COUNT-FREE value-lane members `filter_value_dl_int` (sq-xojl) + `filter_value_dl_f64` + `filter_value_dl_decimal` ([OPUS-4.8] sq-2ezsx — one per datatype class; the decimal member is even scale-agnostic, the scale lives in the public `datatype_const`) + `filter_value_dl_datetime` ([OPUS-5] sq-wz99x — ONE member for BOTH the `xsd:dateTime` and `xsd:date` classes, which are separated by the public lane constant alone). The buckets are derived from the data by the prover **and re-derived by the verifier** (a proof can only verify against the member its public inputs fit); an out-of-bucket shape returns `None` (a clean error, never a silently-unprovable wrong-bucket member).
- **Privacy defaults:** issuer attestation is checked in the **clear** (reveals which issuer signed) and `RevocationStatus.{index, status_list, version}` are **disclosed** (linkability channels) unless you opt into the additive privacy circuits — hidden-issuer, hidden-index (`revoke_unset_d10`: hides the index + liveness bit), or **fully-hidden** (`revoke_hidden_ref_d10_a4`, sq-kndw: hides the list IRI and version too, subject to the per-presentation re-blinding requirement). These are **additive** layers; the clear-path checks always still run.
- **Holder binding (`HolderPop`):** a presentation may bind the proof to a holder key, cross-checked against the issuer-attested `AttestedHolderBinding.holder_pk_digest` (the issuer signed `commitment_message_with_holder` under the external `K`), so it closes the trusted-holder gap (holder A cannot present holder B's credential). Two tiers: **B1 (clear-key, default)** discloses the holder key and the verifier recomputes its digest host-side (`verifier::bind_holder_pop` / `bind_holder_binding`, gated by `HolderBindingPolicy::require_binding()`); **B2 (hidden-key, opt-in — [OPUS-4.8] sq-c2ql)** carries a `HolderPokProof` (a `holder_pok` bb proof) so the holder proves possession **in zero knowledge without disclosing the key** — `verifier::bind_holder_pok` binds the proof's public digest to the issuer-attested digest (the binding edge), gated by `HolderBindingPolicy::require_in_circuit_pok()`. B2 is **NOT-yet-sound** (sq-qhy4) like the rest of the verifier; it is the additive hidden-holder layer over B1.
- **Trust anchors are external, never the prover's manifest:** the trusted issuer key-set (`KeySet`) and the authoritative status bitstring (`RevocationPolicy::with_snapshot`) come from the relying party. `manifest.key_set` is only accepted as a *subset* of the external `K`; the prover's `status_snapshots` is only a tamper tripwire, never the bit-decision source.
- **Proving is subprocess-only** (`nargo`/`bb`), no embedded prover. **Concurrency:** against the *same* compiled member, use the tagged entry points (`prove_in` / `gen_witness_tagged` with a unique `tag`) — the untagged `prove` / `gen_witness` share one `Prover.toml`/witness and are only safe single-threaded.
- **Replay/freshness:** use `FileSeenNonces` (durable: `flock` + `fsync`, single-host) in production. `InMemorySeenNonces` is non-durable, test-only (a restart reopens the replay window). For multi-host, back `SeenNonces` with a DB UNIQUE constraint / CAS store.
- **Toolchain pin:** `nargo 1.0.0-beta.21`, `bb 5.0.0-nightly.20260324`, bb target `noir-recursive`. Other versions may change the public-input byte layout the audit-#1 reconstruction byte-compares against.
- **Maturity:** v1, authored by Opus 4.8 while Fable was unavailable; flagged for ZK re-review. Treat as a research seam, not a hardened product.
- **Dual-leaf value lane (opt-in, research grade, PARTIAL):** a field-native value-hook (`VALUE_HOOK`) dual-leaf encoding (design: `research/zk-field-native-encoding.md`; #769 accepted) is now implemented at research grade behind the OFF-by-default `dual-leaf` feature: the value-FILTER circuit members **`filter_value_dl_int`** (sq-xojl) + **`filter_value_dl_f64`** + **`filter_value_dl_decimal`** ([OPUS-4.8] sq-2ezsx — the double + decimal datatype classes; both bind `VALUE_HOOK` + a `lexical_component` witness with NO in-circuit blake3 — the measured gate win — and, because their terms are MANY-TO-ONE on the value (`-0.0`/`+0.0`, NaN payloads; `"5.0"`/`"5.00"`), instantiate B4 IN-CIRCUIT: f64 canonicalises the IEEE bits before the bind, decimal folds the canonical scale into the public `datatype_const`), plus **`filter_value_dl_datetime`** ([OPUS-5] sq-wz99x — the `xsd:dateTime` + `xsd:date` classes on ONE member, value handle = the SIGNED SCALED EPOCH on the XSD `timeOnTimeline` at lane-fixed `FS = 3`, reusing the decimal member's signed verdict unchanged; §13.2's `Z`-only hookable domain is the host's fail-closed predicate, so a bare/offset operand is REJECTED rather than compared), and the **`xsd:boolean` lane** ([OPUS-5] sq-5xdlk — NO new member: `filter_value_dl_int` already takes `datatype_const` as a PUBLIC input and its `u64` domain covers the boolean hooks `{0, 1}`, so the lane reuses that compiled artifact and is selected purely by the lane constant), their **host encoders** — the six lanes **integer · decimal · double · boolean · dateTime · date**: `sparq_zk::dual_leaf::{encode_literal, encode_double, encode_decimal}` + `sparq_zk::dual_leaf_boolean::encode_boolean` (sq-hh7a4 — canonical `"true"`/`"false"` only; the XSD-legal `"1"`/`"0"` rejected) + `sparq_zk::dual_leaf_datetime::{encode_datetime, encode_date}` (sq-we9vs — signed scaled epoch at lane-fixed `FS = 3`, `Z`-timezoned canonical lexicals ONLY), all fail-closed same-leaf co-binding — and the **fail-closed `(method × circuit)` dispatch matrix** (`sparq_zk_compose::dispatch`; sq-cfmv — all four are value-lane members). The HOST half of the commit pipeline has landed as a PARALLEL builder ([OPUS-5] sq-vvfte — `dual_leaf::{encode_term_dual, encode_triple_dual, commit_triples_dual, commit_graph_dual}`, the §3.2 leaf shapes over `commit.rs`'s unchanged canonical ordering + flat sponge, fail-closed on a rejected hookable lexical), deliberately NOT a re-base of `encode.rs`/`commit.rs` — the default `string-canonical` pipeline stays byte-unchanged. STILL PARTIAL: the CIRCUIT-side leaf recompute (scan/join + `reconstruct_public_inputs` + the cross-vectors) is the paired follow-on, and wiring the dispatch resolver into `verify_manifest` (so the verifier reads the recorded `zk:scheme` and gates each sub-proof) is design bead 6 — both audit-gated; and the `xsd:boolean` / `xsd:dateTime` / `xsd:date` lanes are a documented, tested SEAM not yet ROUTED by the whole-graph builder's `is_hookable_datatype`, so under `DualLeafV1` those literals still take the datatype-folded DEGENERATE string lane (joining them narrows what a `DualLeafV1` graph may CONTAIN — e.g. the XSD-legal but non-canonical `"1"^^xsd:boolean` becomes uncommittable — and re-bases those leaves, so it is its own follow-on). It carries the **INV-VL downgrade** — value↔lexical agreement on the value-FILTER lane is trusted-issuer-honesty, NOT machine-enforced (an open external-audit obligation, gap-register **CR-G8** / `sq-qhy4`). It makes no soundness or privacy claim; the estate is NOT externally audited. [OPUS-4.8] <!-- privacy-claims-allow: opt-in, audit-gated dual-leaf value lane; INV-VL downgrade framed as an OPEN obligation; asserts no soundness/privacy property; sq-qhy4 / CR-G8 -->
- **Numeric type promotion in mixed integer/float comparisons (sq-3x7dl.5, [SONNET-4.6]):** the `noir_XPath` circuit layer (`xpath/src/numeric_types.nr` in the `sparq-org/noir_XPath` face repo — formerly the in-tree `zk/xpath/xpath/src/numeric_types.nr`, externalized by sq-5reoy / #1599) previously truncated the `xs:integer` operand to `i8` before converting to `xs:float`/`xs:double`, silently producing wrong comparison results for integers outside [-128, 127] (e.g. `256 == 0.0` was `true`). This was a soundness-flavoured flaw: an adversarial prover could satisfy a FILTER constraint with a wrong integer value that happens to match after i8-wrap. Fixed by using the generated `From<i64>` trait (`f64::from(n)` / `f32::from(n)`) for all 20 mixed comparison functions (eq/lt/le/gt/ge — 5 operators × 2 operand orders × 2 float types). XPath 2.0 F&O §6.2 / Appendix B.1 type promotion uses IEEE 754 round-to-nearest-even (exact for |n| <= 2^53 in f64, |n| <= 2^24 in f32; correctly rounded beyond). Also fixed: `get_common_type(float, decimal)` now returns `float` per spec rather than `double` (Bug B); `XsdDouble::from_float` now correctly converts denormal f32 values to f64 rather than mapping them to signed zero (Bug C). These are internal circuit corrections; no Rust public API surface changed.
- **`op:numeric-divide` vs `idiv` de-aliasing + `fn:number` interior whitespace (sq-3x7dl.4, [FABLE-5]):** `noir_XPath` previously wired BOTH `xpath_op::numeric_divide` and `xpath_op::numeric_integer_divide` to truncating i64 division, so `7 div 2` silently evaluated to `3` — and SPARQL 1.1 §17.4 maps `/` to `op:numeric-divide`, so any FILTER/BIND dividing integers could constrain against a wrong value (the qt3-generated corpus only records exact-quotient cases, so the truncation was never exercised). Per XPath F&O §4.2.6, two `xs:integer` operands yield the `xs:decimal` quotient (`7 div 2 = 3.5`); the module has no arbitrary-precision decimal type, so `numeric_divide_int_as_double` implements the documented approximation: `XsdDouble::from_i64` promotion (exact for |n| <= 2^53, RNE beyond) + correctly-rounded IEEE 754 double division, fail-closed `assert(b != 0)` (err:FOAR0001 — no Infinity escape for decimal operands). `numeric_divide_int` remains only as `op:numeric-integer-divide` (`idiv`, truncates toward zero) — a distinct code path, with tests pinning `div(7,2)=3.5` vs `idiv(7,2)=3` against an independent Python IEEE 754 oracle. Also fixed: `fn_number_from_string` now implements the xsd `whiteSpace="collapse"` rule it delegates to — leading/trailing whitespace accepted, but once trailing whitespace starts any non-whitespace byte is invalid, so `fn:number('1 2')` is NaN (previously folded to `12`). Internal circuit corrections; no Rust public API surface changed.
- **`fn:avg(())` — DECIDED conformance divergence: keep the fail-closed error (sq-jxh15):** XPath F&O §15.4.4 says `fn:avg(())` returns the **empty sequence**; `noir_XPath` instead **rejects** (fail-closed assert). The DECISION is to **keep the error and record it as a deliberate divergence**, not to implement empty-return. Rationale, in the order it matters: (1) the "SPARQL-aggregate reading" originally offered to justify the error is **factually wrong** and must not be cited — SPARQL 1.1 §18.5.1.5 defines `Avg({}) = "0"^^xsd:integer` (a BOUND zero; sparq's own evaluator implements exactly that, `crates/sparq-engine/src/exec.rs:17512` + the `avg_over_empty_is_integer_zero_one_row` test at `:17586`), so "error" matches NEITHER spec. (2) The right reason to keep it is representability + fail-closed conservatism: Noir functions are total and fixed-arity with no empty-sequence/`Option` inhabitant in the module's value model, so the only two encodings available are *refuse* or *return some in-band value*. Refusing can only ever make a witness unsatisfiable; coercing to an in-band `0` would make the FALSE proposition `fn:avg(()) = 0` satisfiable in-circuit — the same wrong-value-is-witnessable shape as the `sq-3x7dl.5` i8-wrap defect. A conservative refusal is the correct image of "no value"; a fabricated zero is not. (3) The divergence is **currently unreachable from sparq**: `zk/compose` does not consume `noir_XPath` at all (`research/zk-audit-readiness-dossier.md` §1.3), and every aggregate is already fail-closed out of the ZK query fragment (`sparq_zk::verify::aggregates_error`, `crates/sparq-zk/src/verify.rs:1400`, reached from `GraphPattern::Group` and the `Extend`-over-`Group` shape at `:1383`/`:1390`), so no sparq proof path can evaluate `fn:avg` on any input. **Revisit if and only if** `noir_XPath` grows a real empty-sequence representation (an `Option`-shaped return across the aggregate surface) — at that point F&O empty-return becomes representable and this entry expires. **Honesty caveat:** the "currently rejects" behaviour is inherited from the bead and is **NOT verified in this repo** — the source is out-of-tree (`sparq-org/noir_XPath`, externalized by sq-5reoy / #1599) and the in-tree differential corpus (`zk/xpath/differential`) is scalar-only, so it carries no aggregate/sequence coverage either way. Documentation-only decision; no in-tree code or Rust public API changed, and the ZK estate's posture is unchanged — research-grade, external cryptographer sign-off still pending (`sq-qhy4`). [OPUS-5]
- **Per-method security-property annotations (opt-in, `secprop-annotations`):** the `sparq_zk::secprop` module ships the machine-readable per-method posture (`ontologies/secprop-methods.ttl`, design §5a) keyed on the `zk:scheme`/`zk:cryptosuite` IRIs. It RECORDS claims + their epistemic basis — it is NOT a proof. Three over-claim GUARDS are enforced by test AND exposed as public functions: no `Proven` on a positive privacy/soundness property while sq-qhy4 is open (only settled negatives — `PQForgeable`/`Replayable`/`SchemeRevealed` — may be `Proven`); completeness (every production-selectable scheme is annotated); and source-layer non-transfer (`zk:sourceCryptosuite` provenance never satisfies a query-proof constraint). The default assurance is `Claimed`+`ExternalSignOffPending`; promoting any annotation to `Proven` is HARD-GATED on the external sign-off (`sq-qhy4`, Phase 7 `sq-8ac8l`), out of agent scope. Asserts no soundness/privacy property. [OPUS-4.8] <!-- privacy-claims-allow: opt-in annotation graph recording claims + epistemic basis; the guards forbid Proven on a positive property while sq-qhy4 is open; asserts no soundness/privacy property; sq-qhy4 -->
- **W3C VC ingest bridge (opt-in, OFF-circuit; `vc-bridge` feature, sq-9c5e + sq-txg1y):** brings a W3C Data-Integrity VC in by verifying its proof (`eddsa-rdfc-2022` / `ecdsa-rdfc-2019`, the latter in BOTH published curve profiles — P-256/SHA-256 and P-384/SHA-384) OFF-circuit AT INGEST ONLY (real Ed25519 / ECDSA-P256 / ECDSA-P384 verify over `proofConfigHash || documentHash`), then re-committing under the sparq pipeline and recording `zk:sourceCryptosuite` provenance. A JSON-LD VC document can enter through the additive `vc_bridge_json` envelope layer (expansion via `oxjsonld` against a caller-supplied `@context` allowlist, no network), which then runs the same off-circuit check. `bbs-2023` / `ecdsa-sd-2023` selective disclosure is NOT verified by sparq either: the `vc_bridge_sd` seam (sq-u5y1f) DELEGATES the derived-proof check to a host-supplied `SelectiveDisclosureVerifier` and fails closed without one, doing only the RDFC10 canonicalization + re-commitment of the disclosed subset + provenance. **NOT in scope:** in-circuit VC-proof verification (the query proof binds to `Poseidon2SchnorrV1`, not the VC's own proof — §5.3), any in-repo selective-disclosure (BBS / `ecdsa-sd-2023`) verifier or SD soundness/unlinkability claim, P-521 ECDSA, remote `@context` fetching, and `did:` resolution. `zk:sourceCryptosuite` is provenance/back-compat ONLY, not a re-verifiable in-proof property. NOT externally audited (sq-qhy4). [OPUS-4.8] <!-- privacy-claims-allow: opt-in OFF-circuit ingest-time DI verifier plus a delegating SD seam that implements no SD verifier; provenance-only, explicitly not a re-verifiable in-proof property; asserts no in-circuit/query-soundness or SD-soundness property; sq-qhy4 -->

## See also

- Internal soundness re-audits (single-model, PRECEDE the external sq-qhy4 sign-off, do not replace it): [`research/zk-verifier-reaudit.md`](../../research/zk-verifier-reaudit.md) (binding layer, sq-gbp4) + [`research/zk-membership-pok-reaudit.md`](../../research/zk-membership-pok-reaudit.md) (hidden-issuer / holder-pok / holder-set, sq-ru0yx — finds them sound-as-landed AFTER the M-1 issuer challenge-reduction no-wrap fix). <!-- privacy-claims-allow: links to internal re-audits that explicitly state they precede and do NOT replace the external sq-qhy4 sign-off; assert no production soundness/privacy property -->
- `verifiable-credentials-zk` — credential signature schemes, commitment choices, and the credential↔circuit public-input contract.
- `noir-circuit-patterns` / `noir-optimisation` — writing/sizing the Noir circuits this crate drives (`zk/compose/`).
- `sparql-formal-semantics` — the Pérez–Arenas–Gutiérrez fragment + blank-node scoping the Q6 guard and `verify::recheck` enforce.
- `mpc-protocols` — the multi-party layer that composes with this single-prover ZK estate.