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

For the isolated BBS+/BLS12-381 and Circom/LegoGroth16 composition experiment, see
[`zk/native-composition/README.md`](../../zk/native-composition/README.md). Its dedicated
CI runs real proof tests. The native-only [Ark tracing patch](../../zk/native-composition/vendor-support/README.md)
has separate provenance and compatibility checks; it does not certify upstream
constraint arithmetic. Its optional `native-rdf` feature adds a separately
versioned [public RDF support API](references/native-rdf.md): `issue_rdf`,
`prove_public_bgp`, and `verify_public_bgp` authenticate reconstructed public BGP
triples against verifier-owned issuer/status policy. Public signed-slot indices
and status references are disclosed. Support selection covers all accepted roles
when a matching allocation exists. Signed epoch labels must match exactly;
status bytes use the native least-significant-bit-first convention documented in
the reference. It provides no hidden RDF predicate or Noir
linkage and remains unaudited. The original tuple executable stays separate.

`prepare_public_bgp` exposes the honest prover's support preparation
without a proof or authentication verdict. The separate `native-binding` feature
enables the [finite binding-job adapter](references/native-binding-tests.md),
which reports native preparation, admission refusals and actual proof verification
as distinct outcomes. Its `rdf::binding_tests` helper constructs genuine weaker
statements for synthetic fixture controls; these must fail the required verifier.
The mandatory malicious-proof library suite remains separate.
The native CI lane also requires the complete shared finite binding replay;
see the [native CI profile](../../bench/zk-bindings/README.md#native-finite-ci-replay)
for its fixed domain, actual-verifier negative requirements and evidence limits.
CI matches the retained Cargo package/target executable record to the supplied
binary; manual calls without those records explicitly retain no build attestation.

The native [dependency policy record](../../research/native-dependency-policy/README.md)
separates inherited trust records, exact-version licenses and candidate-owned
metadata checks. Native audit-coverage and maintenance failures remain open;
passing the proof tests does not satisfy these dependency gates.

The [VC query protocol draft](../../research/vc-query-protocol.md) and its
[method registry](../../research/vc-query-methods.json) propose separating credential suites
from pluggable query proof methods, and map the selected-result, exact-evaluator and native
paths from source. They are design records: no JSON signature mode or cross-method linking
exists, a registry label shows no support, and none is externally audited. Only
`method:risc0-exact` version 3 has `adapter_available: true`, for exactly the six tuples of the
exact V3 adapter below; every other entry and version stays `false`.

The experimental, unpublished, dependency-free `sparq-query-protocol` crate adds a
first executable layer of that draft. It provides typed descriptors, whole capability tuples,
obligation enforcers, `admit` negotiation that rejects wildcards, fallbacks and downgrades, and
a `QueryMethod` trait with opaque witnesses and typed claims. It also validates a stored request
subset (`StoredRequest`: query text, original `Challenge32`, audience, validity window, form,
shape-checked base IRI, DESCRIBE policy), encodes it and descriptors under the LOCAL structural
profile `local-struct-v1`, and defines a shared `ChallengeStore` contract that consumes the
original challenge once. It has no backend, interoperable wire encoding, transport, parser,
hash or other cryptography, ships no production challenge store, proves no cryptographic claim,
and registers no method. See [query-method contracts](references/query-method-contracts.md).

The detached exact-evaluator host crate's optional `vcq` feature (off by default) adds
the first `QueryMethod` adapter, `sparq_proved_evaluator::vcq::Risc0ExactV3`, over the V3 relation:
bag SELECT, boolean ASK and CONSTRUCT graphs under holder-declared or verifier-agreed authority,
with the fixed default V3 policy. It binds the stored request through a derived nonce and consumes
the original challenge once, after every other check. It authenticates no credential and checks no
status or holder key. The ignored `host/tests/vcq_genuine.rs` prove and verify-only row-bound modes
take an explicit `SPARQ_VCQ_PROOF_JOB`. One run at source `872c219ca` was independently certified
(seven genuine Succinct receipts, one rejected as `capacity`; public synthetic fixture, not a full
gate, no benchmark). See [vcq exact adapter](references/vcq-exact-adapter.md) for tuples and caveats.

For the opt-in synthetic selected-support measurement adapter, its strict
experiment manifest, timing boundaries and unavailable stages, see
[experiment instructions](../../bench/zk-compose/experiments/README.md). Driver
measurements are explicitly enabled by `with_stage_metrics()` and drained by
`take_stage_metrics()`; they remain local diagnostics outside presentations. Local
measurements are NONcanonical and do not establish external security assurance.

Use the [binding corpus and replay harness](../../bench/zk-bindings/README.md) to retain original goldens and separate native, actual constraint, and genuine proof coverage. Imported negative cases require their declared rejection category and phase; an ambiguous evaluation/budget error cannot certify capacity rejection. Explicit version-specific positive goldens preserve the original V1 rejections and unchanged inputs. The [existing engine/storage replay](../../bench/zk-bindings/engine-replay.md) preserves seed/query/dataset identity; normalized oracle agreement never authorizes proof reuse. The experimental [engine proof replay bridge](../../bench/zk-bindings/engine-proof-replay.md) (`sparq_proved_evaluator_model::replay` plus the `engine_replay_proof` host example) prepares one retained cell for exact V3 evaluation and can prove and independently verify it; it authenticates no source credential. The Turtle conversion and original-file hash checks are host checks, not proved by the guest. Only a verifier-agreed anchor that the verifier prepared from the originals binds the converted N-Quads to them. For synthetic experiments, `engine_replay_setup synthetic REPLAY_DIR PROFILE EXPECTED.json RUN_ID NEW_OUTPUT_DIR` writes `holder.json`, `holder-declared.json`, `verifier-agreed.json`, a byte-exact `expected.json` and `setup.json`. Before writing, it checks both authorities natively against the independently supplied expectation. It creates no proof. Its `RUN_ID`-derived nonces are test challenges, never a production challenge source. The host computes its agreed anchor from the original `data.ttl` while also acting as holder, so that anchor is test-setup trust input, not source authentication. The ignored `real_engine_replay_omission_is_an_observed_guest_abort` test (`SPARQ_ENGINE_REPLAY_OMISSION_JOB`) creates no proof. It requires the exact SDK guest-abort message for an omitted statement under the agreed anchor. That is an observed execution rejection, not a negative cryptographic proof.

## 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, None, None)
    .expect("filter inputs render");
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` (RECOGNISED and verifiable, but NOT production-selectable — it records the in-band no-value sentinel `research/zk-field-native-encoding.md` §14.1 asks to be out of band; see `dual_leaf_v2::*`) · `DualLeafV2` (scheme IRI `registry::ZK_SCHEME_POSEIDON2_DUALLEAF_V2` — the dual-leaf method selectable for NEW issuance) · `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, and `checked_for_issuance() -> Result<Self, MethodNotSelectable>` / `checked_for(MethodUse) -> Result<Self, MethodNotSelectable>` turn that posture into a REFUSAL a new-issuance path cannot skip (`MethodUse::{NewIssuance, LegacyAlreadyIssued}` — `NewIssuance` is the `Default` and refuses a superseded version or a research dial; `LegacyAlreadyIssued` is the written-down opt-in for re-deriving or re-verifying an ALREADY-ISSUED commitment, which accepts every recognised method; `MethodNotSelectable::{method, scheme_iri}` names what was refused). `RegistryEntry::method() -> Option<CommitmentMethod>` reads the selection; The method is set only at CONSTRUCTION and the `scheme` field is private (read it with `RegistryEntry::scheme()`): `RegistryEntry::new_already_issued(doc, c, salt, m)` records a method AS-IS (what DECODING and ALREADY-ISSUED entries need, so it still accepts `DualLeafV1`), and `RegistryEntry::new_for_issuance(doc, c, salt, m)` / the signed `RegistryEntry::issued(doc, c, salt, m, sk)` / `issued_with_status(doc, c, salt, m, status_list, index, version, status, sk)` return `Result<Self, MethodNotSelectable>` and refuse a non-selectable method. The issuer signature covers the recorded method for EVERY method, `string-canonical` included: issuance signs `sig::commitment_message_with_scheme` / `commitment_message_with_status_and_scheme` over `sig::scheme_iri_to_field(scheme)`, and `verify_commitment_signature{,_with_status}` recompute it from the recorded scheme, so changing an entry's `zk:scheme` after signing fails verification and an unrecognised scheme fails closed. A registry entry is never verified over the method-independent `commitment_message_with_salt` / `commitment_message_with_status` message, so a registry signature made before the method binding does not verify (none shipped: `sparq-zk` is unpublished and no released artifact calls registry issuance). The manifest verifier's attestation message is a separate path and is unchanged. Recording is NOT retirement: an existing entry keeps its method and retiring one in a deployed registry stays the operator's choice. These host entry points take the same `MethodUse` argument and fail closed on `NewIssuance`: `dual_leaf::{commit_triples_dual, commit_graph_dual}(…, MethodUse)` (new `DualCommitError::MethodNotSelectable`), `dispatch::resolve_circuit_for_use(method, id, MethodUse)` (new `DispatchError::MethodNotSelectableForIssuance`; plain `resolve_circuit` stays the VERIFICATION view and is unchanged) and compose's `driver::CircuitProver::prove_value_lane(method, MethodUse, challenge, &ValueLaneProof, out_dir, tag)` (refuses before any `nargo`/`bb` subprocess, `DriverError::Dispatch`). Compose's V1 value-lane builders, renderers and constants are reachable only by name under `legacy_v1::*` (see the dual-leaf value-lane entry below); the ordinary names produce V2 only. **`LegacyAlreadyIssued` is a caller assertion**, not evidence of issuance history: nothing on these paths reads a signature, a registry entry or a timestamp to confirm it. Per-term encoders (`dual_leaf::encode_literal`, `dual_leaf_boolean::encode_boolean`, `dual_leaf_datetime::{encode_datetime, encode_date}`, …) stay UNGATED building blocks — they produce components, not a commitment, a recorded entry, a rendered `Prover.toml` or a proof. **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 (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; 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 (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). `degenerate_value_component(datatype, language) -> Result<Fr, DualLeafError>` is **fail-closed on the `LANG_NONE` separation**: a language tag whose constant equals `LANG_NONE` is refused with `DualLeafError::ReservedLanguageConstant` rather than encoded (`checked_lang_const(language) -> Result<Fr, DualLeafError>` is the gate; `lang_const` stays the raw derivation). `lang_const` is a 248-bit truncated BLAKE3 digest and `LANG_NONE` is the field element `1`, so the refusal fires only on a fixed-target preimage; it changes no committed value. This is the HOST half of the §14.1 assert; no Noir member asserts it. 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)` (sq-hh7a4) and `dual_leaf_datetime::{encode_datetime, encode_date}(&Literal)` (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 `dual_leaf_boolean::boolean_datatype_const()` (= BLAKE3 key derivation over the `xsd:boolean` IRI under the context `dual_leaf_boolean::BOOLEAN_LANE_CONTEXT`, a hash domain separate from the plain `blake3(datatype IRI)` a string-lane leaf folds, for every byte string, so no such leaf can be opened on the boolean FILTER, whose member range-checks the hook to `u64`) 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 -->
- `dual_leaf_v2::*` (behind the SAME OFF-by-default `dual-leaf` feature — the `DualLeafV2` host scheme, added ALONGSIDE V1 with V1's constants, vectors and public API byte-unchanged): the V1 leaf SHAPE is kept and only the CONSTANTS are re-derived. `lane_const(datatype, params) -> Fr` derives a value-lane `DATATYPE_CONST` in BLAKE3's KEY-DERIVATION mode under the public context `LANE_CONTEXT` over the LENGTH-FRAMED pair `u32_be(len iri) ‖ iri ‖ u32_be(len params) ‖ params`, with the named lanes `integer_lane_const()` / `double_lane_const()` / `decimal_lane_const(fd)` / `boolean_lane_const()` (params `LANE_PARAMS_BOOLEAN = "bit"`) / `datetime_lane_const()` / `date_lane_const()`; `lang_const(language)` moves into its own `LANG_CONTEXT` domain; `degenerate_datatype_const(datatype)` is deliberately the PLAIN fold a string-lane leaf carries. The framing makes a lane constant injective in `(datatype, params)` jointly for ARBITRARY BYTE STRINGS (so the argument does not rest on the datatype being a valid IRI), and the two BLAKE3 modes put a lane constant and the plain fold in separate hash domains — both PROPERTIES under BLAKE3's mode domain separation and, after the 248-bit field reduction, its collision/preimage resistance, NOT unconditional facts. `value_none()` is derived under `VALUE_NONE_CONTEXT` and re-derived with a `u32` counter until it falls OUTSIDE the reachable handle band, which `is_in_handle_band(&Fr)` decides and a host test asserts — that asserted exclusion discharges the §14.1 reserved-tag requirement FOR V2 **on the HOST side** (the in-circuit MIRROR has shipped as the `zk/dual-leaf-v2` Noir library — `VALUE_NONE_V2`, `LANG_NONE` and the scale-free lane constants as `global`s, the band exclusion re-checked by `nargo test`, and `assert_handle_not_value_none` / `assert_handle_in_band` exported for a future leaf recompute, each literal pinned to its host derivation by `crates/sparq-zk/tests/dual_leaf_v2_noir_pin.rs`; ENFORCEMENT is still open — no `zk/compose` member imports that library, so a member rejects the sentinel only because its `u64` range decomposition cannot represent it) (V1's `VALUE_NONE = 2` sits inside the band and stays as shipped); `no_value()` mirrors it unfolded for IRI / blank-node leaves. The lane encoders `encode_integer` / `encode_double` / `encode_decimal` / `encode_boolean` / `encode_datetime` / `encode_date` return the SAME `DualLeafComponents` under the SAME fail-closed same-leaf co-binding and the SAME handles as V1 (only the constants differ), and `encode_literal` / `degenerate_value_component` / `encode_term` / `encode_triple` / `commit_triples` / `commit_graph` / `is_hookable_datatype` mirror the V1 whole-graph builder — SAME RDFC10 canonicalization, SAME canonical leaf order, SAME flat sponge, but V2 routes ALL SIX value lanes — `is_hookable_datatype` and `encode_literal` route `xsd:boolean` / `xsd:dateTime` / `xsd:date` as well as `xsd:integer` / `xsd:decimal` / `xsd:double`, so a V2-committed graph carries a real value hook under that datatype's own lane constant for every literal on them. Two deliberate consequences: the three newly routed lanes inherit the §6 FAIL-CLOSED rule, so an XSD-legal but NON-canonical lexical on them (`"1"^^xsd:boolean`, a bare or non-`Z` `xsd:dateTime`, a `24:00:00` instant) now fails the WHOLE commitment instead of taking the degenerate string lane; and a V2 commitment over a graph CONTAINING such a literal is RE-BASED. Every leaf on the three already-routed lanes, every degenerate string-lane leaf, every IRI / blank-node leaf and the whole-graph commitment over a graph of only those are BYTE-UNCHANGED (a fixed vector captured before the routing change pins both halves). `DualLeafV1`'s routing is unchanged, so an already-issued V1 graph is unaffected. The no-language slot still folds V1's `LANG_NONE = 1`; V2's `degenerate_value_component` returns `Result` and refuses a tag whose V2 `lang_const` equals it through the same gate as V1 (`dual_leaf_v2::checked_lang_const`, `DualLeafError::ReservedLanguageConstant`). NOT discharged by V2: the in-circuit half of that `LANG_NONE` separation (no Noir member asserts it) and the ENFORCEMENT of the band check inside a proving member (no shipped member takes a degenerate component as an operand, and none imports the `zk/dual-leaf-v2` library; wiring it belongs with the scan/join leaf recompute). V2 carries the SAME #769-accepted INV-VL downgrade as V1 and asserts NO soundness or privacy property; the estate is NOT externally audited (CR-G8 / sq-qhy4). <!-- privacy-claims-allow: opt-in versioned host encoder; the separation statements are framed as properties under BLAKE3 domain separation / collision resistance, the INV-VL downgrade and the undischarged LANG_NONE assumption as OPEN audit obligations; 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) -->.
- `verify::fragment_typed_filters(&str) -> Result<Vec<TypedQueryFilter>, VerifyError>` — the DATATYPE-GENERAL sibling of `fragment_filters`, for a relying party that needs a FILTER constant's datatype and lexical form rather than a `u64`. `TypedQueryFilter { variable, op: FilterCmp, constant: oxrdf::Literal }` keeps the literal VERBATIM (a non-canonical lexical form is returned as spelled — refusing it belongs to whatever consumes the filter, where the refusal can name which encoder rejected it). Same independent `spargebra` parse, same walk order, same `SELECT`/`ASK`-only + no-dataset-clause admission, and the same flip of a `const op ?var` comparison. It widens the DATATYPE axis ONLY: `?var op <literal>` is still the sole admitted conjunct, so `?a op ?b`, arithmetic, IRI operands, disjunction, `EXISTS` and a `Not` over a non-equality all remain `UnsupportedFragment`. `fragment_filters` now shares one private walker with it and is otherwise UNCHANGED — behaviour and error strings alike (a regression test asserts the three messages verbatim).
- `commit::CommitmentMethod::recognised() -> &'static [CommitmentMethod]` — every method THIS BUILD recognises, the enumeration counterpart of `from_scheme_iri`. A verifier that must authenticate a commitment method builds one candidate signed message per entry (see `sparq_zk_compose::method_auth`); the `value-only` dial is absent unless its feature is on. Being listed says the method is recognised and decodable — not that any policy ADMITS it (`DualLeafV1` is listed and not production-selectable).
- The METHOD-BOUND **PRESENTATION** messages, each under its own domain tag: `sig::presentation_message_with_status_and_scheme(&Fr c, &Fr salt, &Fr status_ref, &Fr scheme_digest)` (`ZKSIG_M5`) for a bearer attestation, and `sig::commitment_message_with_holder_and_scheme(&Fr c, &Fr salt, &Fr status_ref, &Fr holder_pk_digest, &Fr scheme_digest)` (`ZKSIG_M4`) — the ONE shape that binds a holder key AND a commitment method into a single signed object. Sign with `SecretKey::{sign_presentation_with_status_and_scheme, sign_commitment_with_holder_and_scheme}`, passing `scheme_digest = sig::scheme_iri_to_field(method.scheme_iri())`. Purely additive (new domain tags; every existing signature verifies over the message it was made against). **`ZKSIG_M5` is NOT the registry's `ZKSIG_M3`** `commitment_message_with_status_and_scheme`, which has the same preimage shape under a different tag: recording a commitment in an issuer's registry is a separate statement from authorising its presentation, so a registry signature never verifies as a presentation attestation (and an issuer that holder-bound a credential has not thereby made it presentable as a bearer one).
- `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)>` (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, &HolderRegistry, &HolderBindingPolicy, &EntailmentPolicy, &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), with_method_policy(MethodPolicy), method_policy()}`, `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).
- **Authenticated commitment method** (`method_auth`, always compiled): the verifier does NOT read a commitment method from the manifest and does not assume one — it RECOVERS it from the issuer signature. `method_auth::candidate_messages(&CommitmentMessageInputs { commitment, salt, status_ref, holder_digest })` builds the METHOD-BOUND PRESENTATION message (`sig::presentation_message_with_status_and_scheme`, the `ZKSIG_M5` tag; or `sig::commitment_message_with_holder_and_scheme`, `ZKSIG_M4`, when the attestation is holder-bound) of every `CommitmentMethod::recognised()` method, plus the method-UNBOUND message (`ZKSIG_C3`/`ZKSIG_C4`) the verifier used before. A registry entry's `ZKSIG_M3` signature is NOT a candidate. `method_auth::classify(&candidates, verifies)` is a PURE function of the candidate set and a "does this message verify" predicate: exactly one BOUND candidate verifying gives `AuthenticatedMethod::Bound(m)`, none-bound-but-unbound gives `AuthenticatedMethod::Unbound`, more than one bound is `MethodAuthError::AmbiguousMethod` (refused, not resolved), nothing verifying is `MethodAuthError::NoCandidateVerified`. `method_auth::authenticate(..)` is `candidate_messages` + `classify` + the policy in one call, and `method_auth::authenticated_message(.., authenticated)` is the message a later recompute must use — for `Unbound` it is byte-identical to what the verifier computed before, which is the back-compatibility property. `AuthenticatedMethod::method() -> Option<CommitmentMethod>` names the absent case; `Unbound` means NO method was attested and must never be read as a default one. **The relying party's policy** is `MethodPolicy::{current(), admit_legacy_dual_leaf_v1(), require_method_bound(), accepts_unbound(), admits_method(m), admit(authenticated)}`, set on the EXTERNAL trust anchor with `KeySet::with_method_policy` (never read from the manifest). `current()` is the default and ACCEPTS a method-unbound attestation, so every already-issued credential verifies exactly as before; `require_method_bound()` refuses one (`CheckError::MethodNotAuthenticated`); an attested `DualLeafV1` is refused (`CheckError::MethodNotAdmitted`) unless `admit_legacy_dual_leaf_v1()` is written down, and the `value-only` research dial is admitted by no policy. For a HIDDEN-ONLY commitment (no clear attestation) the method is selected by the hidden entry's declared `message`, which must EQUAL one of the candidates: a value matching none of them is refused with `CheckError::HiddenIssuerMessageMismatch`, and the policy applies to the method the bb hidden-issuer proof is then required to BIND (so that entry of the method map is only meaningful after the bb stage). EVERY entry declared over that commitment is checked, and all of them must select the SAME candidate, so the message check does not depend on the order the prover listed them in. The SALT that a hidden-only commitment's message is recomputed from is resolved the same order-independent way: every hidden-issuer entry over that commitment must carry a salt, each must decode to a field element, and all must decode to the SAME one (the hex spelling may differ — agreement is compared on the decoded element); if any is absent or malformed, or two disagree, the salt does not resolve and the commitment is refused as unreferenced (fail-closed). That refuses strictly more than the earlier first-entry-wins resolution, which let entry order decide; a clear attestation's salt is still preferred when one exists. Issuer side: `SecretKey::{sign_presentation_with_status_and_scheme, sign_commitment_with_holder_and_scheme}(.., &scheme_digest)` where `scheme_digest = sig::scheme_iri_to_field(method.scheme_iri())`. **Back-compatible with ONE qualification, about the declared `message` of hidden-issuer entries, and it opens no gate:** a hidden-issuer entry's declared `message` was previously not read at all, and over a hidden-only commitment it is now required to equal a verifier-built candidate (for every entry over that commitment), so a hidden-only manifest whose declared message is empty, not decodable as a field element, or unmatched is now refused with `CheckError::HiddenIssuerMessageMismatch` — and a refusal of a malformed hidden-only manifest may be reported earlier, in the pre-filter, than it was before. The hidden-issuer stage likewise requires EVERY entry's declared `message`, including one over a commitment that also has a clear attestation, to equal the message its proof is checked against, and that check may now be reported ahead of an entry's depth or proof refusal. Otherwise every manifest that verified before still verifies under the default policy; the newly accepted manifests are only those carrying an issuer signature over a method-bound presentation message (`ZKSIG_M5`/`ZKSIG_M4`). Not externally audited (sq-qhy4).
- **Pinned value-lane inputs** (`value_pin`, behind the OFF-by-default `dual-leaf` feature) — **⚠️ THE VALUE-LANE VERIFIER GATES ARE CLOSED; these functions decide nothing.** `verifier::prefilter_manifest_structure` still refuses EVERY value-lane sub-proof at stage 0 with `CheckError::ValueLaneSubProofNotAccepted`, before it reads a sub-proof for anything else; the stage-2 binding-edge operand match still admits only the `filter_int` family and `filter_edge_true` is untouched. A manifest every one of whose pins holds is still refused. What `value_pin` provides is the INPUT a future gate needs: `expected_value_lane(AuthenticatedMethod, FilterCmp, &oxrdf::Literal) -> Result<ExpectedLane, PinError>` routes the constant's datatype to its member and lane constant and encodes the bound with the lane's own V2 encoder (`ExpectedLane { member, lane_const: ExpectedLaneConst::{Fixed(Fr), DecimalAtAdmittedScale}, op, bound: ExpectedBound::{U64, Bits, Signed, Decimal} }`); `check_value_lane_pin(method, &TypedQueryFilter, &ProofInputs)` checks all five equalities — member, canonically-spelled lane constant (for the decimal lane, `decimal_lane_const(fd)` at an `ADMITTED_FRACTION_DIGITS` = `1..=19` scale, with the query constant rescaled to it EXACTLY, never rounded), op code after the `const op ?var` flip, bound, and verdict `true` — each failing closed with its own `PinError::{MethodNotBound, MethodHasNoValueLane, LegacyMethodValueLane, MixedScanMethods, UnsupportedConstantDatatype, ConstantNotEncodable, LaneNotRouted, MemberMismatch, LaneConstMismatch, ScaleNotAdmitted, OpMismatch, BoundMismatch, VerdictNotTrue, NotAValueLaneSubProof}`. `scan_method(&ProofManifest, &AuthenticatedMethods)` requires EVERY commitment a scan draws from to have authenticated the SAME method (mixed is refused), and `check_lane_routed(datatype)` reads `dual_leaf_v2::is_hookable_datatype`, which now routes ALL SIX value lanes — so `xsd:boolean`, `xsd:dateTime` and `xsd:date` pass it, and what it still refuses (`PinError::LaneNotRouted`) is any OTHER datatype a direct caller passes. Only `AuthenticatedMethod::Bound(DualLeafV2)` proceeds; `Unbound` is `MethodNotBound` (a pin is never computed against an assumed method), `StringCanonicalV1` has no value lane, `DualLeafV1` is `LegacyMethodValueLane`. Numeric promotion is NOT supported (an `xsd:integer` constant does not route to the decimal member — it fails closed as a member mismatch). Research-grade, not externally audited (sq-qhy4); the value lanes carry the #769-accepted INV-VL downgrade (CR-G8).
- 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 + 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 (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 — `legacy_v1::boolean_datatype_const() -> FieldHex` (= `dual_leaf_boolean::boolean_datatype_const()`, the constant the host encoder `sparq_zk::dual_leaf_boolean::encode_boolean` folds into the committed leaf, sq-hh7a4). `legacy_v1::build_filter_value_dl_boolean(&Literal, FilterOp, bound: bool) -> Result<BuiltFilterValueDlBoolean, BuildValueDlV1Error>` 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. **`DualLeafV2` `xsd:boolean` lane — its OWN bit-constrained member:** `CircuitId::FilterValueDlBool` + `ProofInputs::FilterValueDlBool { operand_enc, op, bound, datatype_const, expected }` is the `filter_value_dl_bool` member, whose PUBLIC layout is field-for-field the integer member's (so the host serialisation and the verifier's public-input reconstruction are the integer lane's) and which ADDITIONALLY constrains BOTH the witnessed `VALUE_HOOK` and the public `bound` to the bit domain `{0, 1}` in-circuit (`v * (v - 1) == 0`) — so a handle of `2`, which the shared integer member's `u64` range decomposition admits, is refused by the RELATION rather than only by the host encoder. It is a SEPARATE member because the integer lane legitimately uses the whole `u64` domain and adding constraints there would move that member's gate count and its measured evidence. `manifest::boolean_lane_const_v2() -> FieldHex` is the V2 lane constant (`sparq_zk::dual_leaf_v2::boolean_lane_const()`), `build::build_filter_value_dl_bool(&Literal, FilterOp, bound: bool) -> Result<BuiltFilterValueDlBool, DualLeafError>` builds the public inputs + the two private witnesses from a canonical `"true"`/`"false"` literal (fail-closed otherwise) disclosing the HONEST `build::boolean_verdict(...)`, and `toml::filter_value_dl_bool_prover_toml(...)` renders its `Prover.toml` with that constant PINNED. The `DualLeafV1` boolean lane keeps sharing the integer member and is unchanged. **V2 compose coverage, exactly:** ALL SIX lanes now have V2 `build` helpers. Beside the `_bool` / `_datetime` / `_date` entries, `build::build_filter_value_dl_{int, f64, decimal}(&Literal, FilterOp, bound: &Literal) -> Result<BuiltFilterValueDlNumeric, BuildValueDlV2Error>` build the integer, double and decimal lanes from TYPED operands over ONE shared assembly: both operands go through the lane's own `dual_leaf_v2` encoder (so the disclosed bound is the field the committer would have folded, by the same code, and a non-canonical or wrong-datatyped operand on EITHER side is the encoder's `Err`), the COMMITTED literal's lane constant is carried, and the verdict is COMPUTED — `build::integer_verdict(u64, FilterOp, u64)`, `build::double_bits_verdict(u64, FilterOp, u64)` (IEEE semantics over the two canonical bit patterns, the member's `f64_verdict`) and the shared `build::signed_epoch_verdict(...)` for decimal — never taken from the caller. The decimal lane rescales the bound to the COMMITTED literal's scale EXACTLY (that scale is the one folded into its lane constant, which is what the member works at), refusing a bound that would need rounding or would overflow a `u64` with `BuildValueDlV2Error::DecimalScaleNotRepresentable`, through the same two functions `value_pin` pins with — so the builder's scale and the pin's cannot disagree. `BuiltFilterValueDlNumeric { inputs, witness }` carries the member's `value_lane::LaneWitness`, and `.lane_proof()` hands it to the checked typed prove entry, so the `Prover.toml` is rendered from validated typed fields and never from caller TOML. Tested as a composition: every one of the six lanes' builder output satisfies `value_pin::check_value_lane_pin` for the matching typed FILTER, and changing any single pinned field of it is refused with that field's own `PinError`. The verifier gates are UNCHANGED — a manifest assembled from these builders is still refused with `CheckError::ValueLaneSubProofNotAccepted`, per lane. **V1 by name only:** every V1 value-lane constant, builder and renderer lives under `legacy_v1::*` (`boolean_datatype_const`, `datetime_datatype_const`, `date_datatype_const`, `build_filter_value_dl_{boolean,datetime,date}`, `filter_value_dl{,_boolean,_f64,_decimal,_datetime}_prover_toml`), each admitting V1 constants only (`DispatchError::NotALegacyV1LaneConst`); the ordinary `build` / `toml` names refuse a V1 constant. Verification-side V1 support is unchanged (raw `bb` verification, `resolve_circuit`, the verifier's id derivation and the `LegacyAlreadyIssued` pairing view); the manifest pre-filter still refuses every value-lane sub-proof, V1 or V2. **Lane↔member pairing:** `dispatch::check_lane_member_pairing(&ProofInputs) -> Result<(), DispatchError>` refuses a `ProofInputs::FilterValueDl` carrying `manifest::boolean_lane_const_v2()` (`DispatchError::LaneMemberMismatch`) — the V2 boolean lane constant may only ride `FilterValueDlBool`, because `datatype_const` is a public input no member pins and the shared integer member range-decomposes its handle over the whole `u64` domain. `verifier::prefilter_manifest_structure` runs the same check per sub-proof before it reads them for anything else (`CheckError::LaneMemberMismatch`). PRECONDITION, not a claim: this is a HOST/structural boundary. The value-lane verifier gates (`verifier.rs`'s stage-2 binding edges and `filter_edge_true`) stay CLOSED until the verifier authenticates the commitment method and pins member, lane, scale and bound itself (sq-j506) — the pairing check does not make a V2 value-lane proof verifier-enforced. Same INV-VL downgrade + CR-G8 / sq-qhy4; NOT externally audited; no soundness/privacy claim. **`xsd:dateTime` / `xsd:date` lane (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 — the V1 constants are `legacy_v1::datetime_datatype_const()` / `legacy_v1::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), and the V2 ones are the `dual_leaf_v2` dateTime/date lane constants. 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>` (V2; the V1 forms are `legacy_v1::*`) 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_bool_prover_toml(...)` / `filter_value_dl_datetime_prover_toml(...)` emit each member's V2 `Prover.toml` (their private witnesses are field elements — `value_hook` (+ `value_neg` for decimal/dateTime) + `lexical_component`; the boolean renderers are the integer layout with their lane constant PINNED and `bound: bool` mapped to its hook). Each returns `Result<String, DispatchError>`: the `(member, datatype_const)` pairing and the canonical spelling of EVERY `FieldHex` it writes are checked BEFORE any text is rendered, so a refused input produces no `Prover.toml` at all. **The checked prove entry** is `driver::CircuitProver::prove_value_lane(method, MethodUse, challenge, &value_lane::ValueLaneProof, out_dir, tag)`: it takes no circuit id and no TOML. A `ValueLaneProof` has one typed variant per lane (built by `ValueLaneProof::from_inputs(&ProofInputs, LaneWitness)` or a builder's `lane_proof()`); the member comes from `ValueLane::member` (through `ValueLaneProof::circuit_id`), the table `value_lane::derive_value_lane_member` and the verifier's id derivation also read; and the `Prover.toml` is rendered inside the entry by `ValueLaneProof::checked_prover_toml` after the `(method, member, use)` dispatch, the canonical check of every written field, the lane↔member allow-list and the method/constant version agreement (`DispatchError::MethodLaneVersionMismatch`: a `DualLeafV1` method needs a V1 constant, a `DualLeafV2` method a V2 one). **`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. **The LANE↔MEMBER allow-list** is the same module's `dispatch::check_lane_const_for_member(&CircuitId, &FieldHex, MethodUse)` and `check_lane_member_pairing{,_for_use}(&ProofInputs[, MethodUse])`, shared by the value-lane builders, the renderers, `prove_value_lane` and the verifier's structural pre-filter (stage 0 of `prefilter_manifest_structure`) — and deliberately NOT by the raw `CircuitProver::{prove, prove_in, gen_witness*}` entries, which take a `CircuitId` plus TOML bytes and stay UNGATED (documented as such), so a caller rendering its own TOML is outside this boundary. It is AFFIRMATIVE and decided on DECODED field elements: a `datatype_const` is legal on a member iff a shipped lane derives it FOR that member (V1 integer/boolean → the shared integer member, V1/V2 double → `f64`, V1/V2 decimal at any encodable scale `fd ∈ 1..=19` → `decimal`, V1/V2 dateTime/date → `datetime`, V2 integer → the integer member, V2 boolean → `filter_value_dl_bool` and nothing else), a V1 constant only under `MethodUse::LegacyAlreadyIssued`, and the text must be the CANONICAL rendering of the element it decodes to (`field_from_hex_str` also accepts uppercase, `0x`-less, short and at-or-above-modulus spellings, which a text comparison would let through) — `DispatchError::{LaneMemberMismatch, UnknownLaneConst, LegacyLaneConstForIssuance, NonCanonicalFieldHex}`. **Exactly what the canonicality rule covers:** `datatype_const` at `check_lane_const_for_member`, `operand_enc` plus `datatype_const` at the `ProofInputs`-level `check_lane_member_pairing{,_for_use}`, and every `FieldHex` a value-lane renderer or `prove_value_lane` writes (same decoder) — no non-value-lane variant's public inputs. The `ProofInputs`-level check also requires the VARIANT and the declared `id` to name the same member (`DispatchError::ValueLaneVariantIdMismatch`), deriving the member from the variant with `value_lane::derive_value_lane_member`; a `ValueLaneProof` carries no separate id, so the checked prove entry cannot be given a crossed pair. `prove_value_lane` renders the TOML itself, from typed fields that each pass the canonical check, so no caller text reaches `nargo` through it. `check_lane_member_pairing_for_use` alone does not cross-check the method version against the constant version under `MethodUse::LegacyAlreadyIssued`; `prove_value_lane` does. The use flag is a CALLER ASSERTION: nothing reads a signature, registry entry or timestamp. The pre-filter refuses EVERY value-lane sub-proof (`CheckError::ValueLaneSubProofNotAccepted`) — unconditionally, inspecting no edge, because `filter_edge_true` discharges a query FILTER only through a `filter_int` edge, so such a sub-proof would otherwise be verified while discharging nothing; **behaviour change:** such a manifest used to be accepted. **These are HOST-side and structural-pre-filter refusals; the value-lane verifier GATES (stage-2 binding edges, `filter_edge_true`) stay closed until the verifier authenticates the method and pins member, lane, scale and bound itself (sq-j506).** **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}`.
- Status Merkle roots and witnesses require the entire byte-sized snapshot to fit `2^depth` bits; oversized snapshots return `None` before hashing. Nonempty snapshots therefore require depth at least three. Missing trailing status bits remain revoked padding. This admission also protects legacy accepted-policy anchors and successful-result policies; the successful-result verifier derives depth 10/17/20 from its complete accepted policy.
- **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.

<!-- zkp-3: host planner, never a proof verification shortcut. -->
The `sparq_zk_compose::planner` API admits strict SELECT DISTINCT / true ASK,
selects successful per-result witnesses, and derives public disclosure versus
remaining proof obligations. Its credential/leaf references and metrics are
PRIVATE planning data; authentication remains required for public triples and
FILTER operands. See [disclosure planning](references/disclosure-planner.md) for
the API, bounds, result contract, and limitations. Host planning is not
cryptographic verification; this surface is not externally audited.
`planner::signed::SignedDisclosureQuery` and its signed planning/optimization
functions separately admit canonical `i64` FILTERs. They preserve committed RDF
terms and do not extend the existing unsigned proof verifier. See the signed
admission section in the disclosure-planning reference.

## Common recipes

<!-- zkp-10.1: separate exact-dataset contract, not a selected-result upgrade. -->
The opt-in detached [exact evaluator](references/exact-evaluator.md) proves bounded default-graph evaluation with explicit verifier-agreed or holder-declared scope. It is experimental and not externally audited; its first adapter carries no issuer-signature or credential-status claim.
The separately versioned [complete named-dataset API](references/exact-datasets-v2.md) adds a committed catalog including empty named graphs, GRAPH and local snapshot FROM/FROM NAMED selection. V1 requests and commitments retain their meaning.
The opt-in [V3 graph-result API](references/graph-results-v3.md) adds blank-node identity, canonical tables and bounded graph forms through typed host/guest APIs; consult artifact-bound evidence for actual execution status.
Issuer-authenticated RDF (V5): every feature is off by default and experimental, and each layer keeps its own evidence level (native model tests, native host tests, direct guest execution, adapter native tests, one genuine adapter case; the low-level driver has no receipt):

- **Model** (model feature `authenticated-rdf`): the [native V5 model](references/authenticated-rdf-model.md) checks W3C `eddsa-rdfc-2022` credentials against a verifier-pinned key table, then reuses V3 evaluation.
- **Guest** (host feature `authenticated-rdf`): a [separately pinned V5 guest and low-level host API](references/authenticated-rdf-guest.md) with a committed guest lock. An independently audited scoped gate at `42d13fed` passed its native tests and executed the guest directly, without proving. Its ignored genuine-proof driver proves only the one to six case IDs a v2 job declares; a subset run claims nothing about undeclared cases.
- **Adapter** (host feature `vcq-authenticated` = `vcq` + `authenticated-rdf`): the generic [V5 vcq adapter](references/vcq-authenticated-rdf-adapter.md) `vcq_authenticated::Risc0AuthenticatedRdfV5` declares six tuples (bag SELECT, ASK, CONSTRUCT; `IssuerAuthenticated`; both authorities). An independently verified scoped native gate at `7fe88955` passed its tests and Clippy without proving. Separately, at that frozen source, one independently audited genuine receipt of the approved V5 guest proved one public synthetic case, `select-bag-verifier-agreed`, with 28 controls. The other five tuples and the row-bound case have not run, so the registry keeps its `adapter_available` false.

None processes JSON-LD or full Data Integrity or checks status, holder binding, validity against a clock or wallet/world completeness. The campaign's V5 and vcq commands have not run as a full campaign. Not externally audited (`sq-qhy4`). <!-- privacy-claims-allow: native tests, direct execution and one synthetic adapter receipt; not audited -->
The [campaign evidence guide](references/evaluator-evidence.md) explains exact artifact export, actual receipt evidence and source/HAL provenance.
The [exact-evaluator experiment adapter](../../zk/sparql-evaluator/experiments/README.md) runs fixed synthetic V2 contracts against an independently accepted caller artifact and pin, with real local receipts, typed tamper controls and scoped measurement.

The [query-coverage corpus](references/evaluator-conformance.md) separates executed host semantics, explicit unsupported features, and guest proof evidence. Its opt-in NPS comparison recipe records other engines' observations without installing dependencies or treating their output as a conformance oracle.

### 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::clear(index, version)),
    holder: None,                                       // bearer; see HolderBindingPolicy
};
```

### 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, &[], None, None).unwrap();
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, None, None).unwrap();
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,
    derivation_steps: vec![],                               // Simple regime: no inference steps
    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 }],
    join_edges: vec![],
    hidden_revocation: None,
    fully_hidden_revocation: None,
    hidden_issuer_attestations: vec![],
    holder_pok_proofs: vec![],
    holder_set_proofs: 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, EntailmentPolicy, FileSeenNonces, HolderBindingPolicy, HolderRegistry, KeySet,
    RevocationPolicy, VerifierNonce,
};
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,
                      &HolderRegistry::empty(),            // Challenge binding: no holder PoP in use
                      &HolderBindingPolicy::allow_bearer(), // or ::require_binding()
                      &EntailmentPolicy::simple_only(),     // reject RDFS/OWL manifests
                      &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.
// 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
// The issuer signs a HIDING index commitment; the circuit recomputes it from index + blinding.
let index_commitment = sparq_zk::sig::status_index_commitment(3, &blinding); // blinding: per-credential, OS-random
let toml = revoke_prover_toml(&nonce_field, &root, &index_commitment, 3, &blinding, &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)

- **Commitment method: AUTHENTICATED. Value-lane gates: CLOSED.** The verifier recovers a committed graph's commitment method from the issuer signature (`method_auth`, above) and can compute exactly what a value-lane sub-proof's public inputs would have to be for a given typed query FILTER (`value_pin`, above). Neither opens a gate. `verifier::prefilter_manifest_structure` still refuses EVERY value-lane sub-proof unconditionally at stage 0 (`CheckError::ValueLaneSubProofNotAccepted`), before it reads a sub-proof for anything else; the stage-2 binding-edge operand match still admits only the `filter_int` family, and `filter_edge_true` is untouched. A manifest every one of whose pins HOLDS is still refused — a test asserts exactly that. **Nothing ties a pin to an obligation:** there is no edge from a value-lane sub-proof to a query FILTER in this verifier, so nothing establishes that a sub-proof whose pin holds is the one answering that FILTER. Creating that edge, adding the stage-2 arms, routing the typed filters by the scan's authenticated method, and making the pattern-slot encoding method-aware are the remaining sq-j506 wiring. Also not supported: **numeric promotion** (an `xsd:integer` FILTER constant does not route to the decimal member — it fails closed), and the decimal **scale is public** via the lane constant, which was already true of every decimal value-lane proof.

- **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).
- **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).
- **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 (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`. **But full verification discharges a query `FILTER` only through a true-verdict `FilterInt` sub-proof** (`verifier::filter_edge_true`), so a manifest that relies on the `filter_f64`, signed, decimal or dual-leaf lanes for a query FILTER is rejected (`UnboundFilter`, or `EdgeKindMismatch` for a value-lane edge); those lanes await query-binding integration (`site/specs/zksparql.typ`). 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 (#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 (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 (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. The prover side refuses it too: `ZkDataset::query_traced` returns `TraceError::Query` with that reason before evaluating, instead of tracing an empty answer over the default-graph-only union. (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** (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** (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` (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` (sq-wz99x — ONE member for BOTH the `xsd:dateTime` and `xsd:date` classes, which are separated by the public lane constant alone) + `filter_value_dl_bool` (the `DualLeafV2` `xsd:boolean` lane's dedicated BIT-DOMAIN member — the integer member's public layout plus `{0, 1}` constraints on the witnessed handle and the public bound). 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 — 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; 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`** (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`** (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** (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 (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). The scheme is also **versioned**: `DualLeafV2` (`sparq_zk::dual_leaf_v2`) keeps V1's leaf shapes and re-derives the constants — length-framed lane constants in BLAKE3's key-derivation mode and a `value_none()` asserted outside the reachable handle band, which discharges §14.1's reserved-tag requirement for V2 on the HOST side (the in-circuit MIRROR has shipped as the `zk/dual-leaf-v2` Noir library, host-pinned and `nargo test`-checked; its ENFORCEMENT inside a proving member has not) — and adds the DEDICATED bit-constrained `filter_value_dl_bool` member for its boolean lane; V1 stays byte-unchanged and verifiable but is no longer production-selectable, and V2's whole-graph builder ROUTES the boolean/dateTime/date lanes that V1 leaves unrouted (narrowing what a V2 graph may contain to those lanes' §13.2 value domain — `Z`-only instants with at most three fraction digits, so an untimezoned or non-`Z` date/dateTime fails the V2 commitment, and re-basing a V2 commitment over a graph that contains one; the already-routed lanes' leaves and commitments are byte-unchanged). Both versions assert the §14.1 `LANG_NONE` separation on the HOST side (a language tag whose constant equals `LANG_NONE` is refused, never encoded); the in-circuit half is still open. 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. <!-- 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):** 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):** `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:19047` + the `avg_over_empty_is_integer_zero_one_row` test at `:19121`), 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:1427`, reached from `GraphPattern::Group` and the `Extend`-over-`Group` shape at `:1410`/`:1417`), 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`).
- **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. <!-- 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). <!-- 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 -->
- [`site/specs/zksparql.typ`](../../site/specs/zksparql.typ) — the zkSPARQL specification, rewritten from this code (#6652); it states which FILTER lanes are wired into full query verification.
- `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.

## Private successful-result experiment

With `sparq-zk-compose/successful-results`, use
`result::prepare_result(query, credentials, rows, policy, nonce)`, then
`PreparedResult::prove(driver, output_dir, unique_tag)`. The relying party calls
`result::verify_result(expected_query, presentation, policy, nonce, seen, driver,
work_dir)` with independently chosen request/trust/status/freshness inputs.
Successful verification returns released mappings. The new contract is separate
from `verify_manifest`: only nonempty positive `SELECT DISTINCT` answers, selected
IRIs/literals, and private canonical nonnegative `xsd:integer` predicates through
`u64::MAX` are admitted. `ResultOptions::integer_capacity` selects the default
smallest range bucket or explicit `IntegerCapacityPolicy::HideInU64`; actual
decimal length stays private. Status capacities are independently derived at
depth 10/17/20 from all freshness-accepted snapshots.
Public predicates run in the verifier and select the member without numeric
circuitry. Roots/salts/status indices and intermediate encodings are private;
issuer slots/capacities/result size remain public. See the [successful-result contract](references/successful-results.md)
for exact scope. Before proving or verifying, it requires the exact
pinned version field (`nargo version = 1.0.0-beta.21` as the first line; trimmed
`bb` output `5.0.0-nightly.20260324`); substrings, diagnostics and non-UTF-8
output are rejected. This is a pin guard, not binary attestation (no hash check).
Research-stage, not externally
audited: no complete-answer, absence, wallet-size or holder-identity guarantee.

`planner::plan_disclosure_admitted` additionally accepts a predicate
`Fn(pattern_index, MembershipRef, &Triple) -> bool` that excludes ineligible
backend candidates while retaining all query checks. It preserves original
wallet/leaf indices and is private preparation, never a verifier trust decision.

Result preparation filters issuer/status/backend eligibility before
selecting witnesses. Each proof uses an internally unique private witness directory;
canonical-key generation and verification also isolate concurrent scratch files.
Caller tags are descriptive and cannot cause private-result input collisions.
All witness/proving entry points validate tags before I/O: ASCII letters,
digits, underscores, hyphens and dots are accepted; `.`/`..`, separators and other
characters reject. Legacy untagged APIs retain the empty tag; successful-result
proofs require a nonempty label. Dots are injectively encoded as `%2E` internally
and every filename has a fixed prefix; literal percent signs reject. Input
writes reject final-component symlinks on
Unix. Workspaces and their parent directories must be controlled by the caller.

Successful-result proofs now select a one- or two-credential circuit
bucket, so removing a credential also removes its in-circuit signature check.
The default `CredentialCapacity::Smallest` reveals the selected capacity; choose
`prepare_result_with_options(..., ResultOptions { credential_capacity:
CredentialCapacity::HideInTwo, ..ResultOptions::default() })` to keep the fixed two-slot policy. The verifier
checks the bounded issuer-slot shape and derives the member independently.

Explicit `planner::optimize_disclosure[_admitted]` jointly minimizes
credential authentication count and then shared membership count for fixed
released rows. Its bounded report distinguishes `Optimal`, `Infeasible`, and
`BudgetExhausted`; an exhausted feasible plan never implies optimality. Backend
admission and credential-capacity limits remain enforced. This is structural host
selection, not a calibrated speed claim or cryptographic assurance; see
[disclosure planning](references/disclosure-planner.md).

`prepare_result` defaults to joint `WitnessSelection::Optimize` with the
backend's credential bound. Set `ResultOptions.witness_selection` to `FirstSuccess`
for the baseline, and `max_search_steps` to bound candidate attempts. Inspect
`PreparedResult::work().optimization`: an exhausted feasible incumbent is usable
but has no established optimum; exhaustion without a feasible plan returns
`ResultError::SearchExhausted`. Neither diagnostics nor private attributions enter
the public presentation, and the independent verifier is unchanged.

`CircuitProver::compile` returns an immutable content-addressed snapshot
under the ignored target cache. Driver compile/execute calls share a Unix advisory
workspace lock, and proof/key jobs consume their own ACIR copies. Concurrent driver
processes may share a local workspace; do not run external nargo writes or remove
the cache during those jobs. Unique legacy prover tags remain required for legacy
witness APIs. Lock failures reject; the existing Unix platform and Rust 1.88
minimum are preserved.

Both planner selection paths enforce `MAX_DISCLOSURE_CREDENTIALS` on the
supplied slice before traversing credentials; empty and ineligible graphs count.
This input bound is independent of candidate-triple search fuel.

Successful-result preparation also checks `MAX_DISCLOSURE_CREDENTIALS`
before its authentication prepass. Its graph contract is string-canonical only;
the generated gate matrix records dual-leaf and value-only pairs as unsupported.

[Exact temporal keys and enforced year capacity](references/exact-temporals.md)
cover the shared evaluator and separate native/actual-guest regression evidence.

The exact-dataset evaluator applies the [aggregate operand boundary](references/aggregate-profile.md) in both native admission and guest evaluation. Non-COUNT aggregate operands must be constants or variables proven bound by the inner algebra; expression operands and nullable bindings are outside this initial profile. This is a restriction, not complete aggregate conformance.

## Exact-evaluator SDK dependencies

The separate [exact evaluator](../../zk/sparql-evaluator/README.md) uses
detached workspaces. Its [SDK patch record](../../vendor/zk-sdk/README.md) preserves
upstream source/license identity and documents discovery-only dependency selection
and derive-macro, server-profiler and kernel-binary feature boundaries, with
executable patch reconstruction, explicit lockfile patch-selection corruption
controls, and the native `edge_matrix.py` feature compiler. The kernel's default
binary dependency activation and embedded ELF remain unchanged; the patch record
separately documents an upstream real-target binary compilation limitation.
Synthetic dependency checks remain separate from actual guest proof evidence.
The exact evaluator enables the [numeric capacity guard](references/numeric-capacity.md). Valid values beyond the finite arithmetic lane can be returned directly; integer/decimal EBV uses exact zero classification. Unsupported arithmetic/comparison consumption fails the entire evaluation. Native default budgets leave this option off.

The SDK provenance checks bind both workspace patch tables and resolved
feature-matrix package manifests to the exact inventoried vendor directories.
The [SDK reference](../../vendor/zk-sdk/README.md) distinguishes direct Cargo
kernel defaults from the embedding helper's explicit feature requirement, and
records library-only Clippy scope separately from kernel or guest execution.

The exact evaluator admits the [bounded nullable alternative/inverse profile](references/nullable-paths.md). Bag duplicates and concrete absent endpoints are retained; nullable sequences, nested nullable quantifiers and residual paths in EXISTS remain excluded. Actual guest evidence must bind the updated admission artifact.

The exact model's `evaluate_detailed`, `v2::evaluate_detailed` and
`v3::evaluate_detailed` evaluate their same versioned requests and emit
the same journal as `evaluate`, while returning `EvaluationError` with distinct
`Budget`, `Capacity`, `Execution` and existing `Rejected` cases; their
`BudgetExceeded` and `EvaluationCapacity` enums are re-exported by the model. Execution causes
come from actual engine emitters; private engine diagnostics are discarded. The
legacy `evaluate` APIs keep their original execution rejections, including V3's
separate query and graph diagnostics. This error
API is outside request/journal encoding and adds no receipt evidence by itself.

The [shared original-corpus controller](../../bench/zk-bindings/README.md)
retains native versus actual-proof counters and independently pinned goldens.
Row-only goldens keep the caller's default `--variables`, except
where a hash-pinned reviewed projection override matches the exact source file
and fixture. Imported SELECT goldens whose row width differs from the
projection width are rejected, not replayed.

Original successful-result v1 circuit, ABI and verification-key bytes are
preserved under the pinned toolchain and checked against independent baseline
keys in the toolchain suite. Expanded v2 tiny and predicate-free profiles have
representative genuine-proof checks in addition to wrapper execution coverage;
see the successful-result reference for evidence and scope.

Opt-in `result::prepare_result_public_pattern` (unchanged
`ResultOptions`) emits version 4 (`PUBLIC_PATTERN_VERSION`): the first
all-constant-or-projected pattern is checked against a verifier-derived public
triple table instead of private typed openings. `verify_result` recognizes it;
default dispatch is unchanged. The pattern moves to index zero identically in
prover and verifier, and the `public_triples` table is appended last to the
`result_v4_k{1,2}_n16_p3_r4_f0_d10` public ABI. Signatures, hidden roots, salts,
status references, policy paths and leaf membership stay in-circuit. Remaining
patterns keep the generic typed and shared-variable checks. The verifier
rebuilds the pattern, table, package and byte order from its query, released rows,
issuer-slot count and policy. Public subjects and predicates must be IRIs, and
objects must be IRIs or literals. Dispatch never uses the witness choice or count.
Only F0 (no FILTER on a hidden variable), status depth 10 and K1/K2 are
supported; no public pattern or any other profile rejects without fallback. It
proves support for the selected rows only, not completeness. Research-grade, not
externally audited; no runtime saving is claimed.
Checked-in static evidence for both members, from one independent
non-canonical Linux x86_64 work-box run at source `14d426bd`: `bb gates` circuit
sizes in the [gate snapshot](../../crates/sparq-zk-compose/tests/gate_count_snapshot.json),
plus ACIR, ABI and source-bound tool provenance in
[`result_public_gates.json`](../../bench/zk-compose/result_public_gates.json).
`bench/zk-compose/scripts/verify_result_evidence.py` checks these records
against the snapshots and the shared Noir source inventory. The refreshed legacy
inventories stay value-identical, and legacy keys are compared byte-for-byte by
test with no key files retained. Static counts are not a runtime or security
audit. In that run the ignored toolchain tests
`result_real_public_pattern_k1_k2_proofs_and_verifier_controls` (one genuine K1
and one K2 proof, each with typed verifier-rejection controls) and
`result_relation_public_pattern_rejects_tampered_retained_witnesses` passed. Their
proof outputs are not retained in the repository (that run's evidence bundle has
SHA-256 `a1944e1c49692b360155fc725ad8800b33ebe7a5ef09de8afdfd68ae63b81fbb`), so
future CI replays are still required.
The [binding corpus](../../bench/zk-bindings/README.md) registers an
explicit `noir_public_pattern` backend over its existing finite domain; it never
substitutes version 1 or signed members. A separate non-canonical EC2 run at
corpus source `2e0f4a9dba47d537835b4745c66147f097c68e43` executed all 576 native cells (72 accepted, 468 support
refusals, 36 empty-graph refusals) and all 46 real cells (4 genuine K1 proofs,
32 absent-binding and 10 private-witness-attack constraint failures). That run is
distinct from the `14d426bd` measurements above, is not a hosted CI run, and makes
no gate, runtime or security claim; see the corpus README for its controls and hashes.

The `result_experiment` example also accepts a separately versioned
schema-3 manifest for a paired `baseline_v1` versus `public_pattern_v4` ablation
over K1 and K2 synthetic wallets. Both arms use one eligible query, the same
released rows, signed inputs, policy and realized issuer-slot count, and one
acceptance digest per profile. Relation version, package and proof stay
separately visible, and transcripts are not claimed byte-identical. The legacy
selected-support query is not version-four eligible and stays unchanged. The
adapter reports raw per-sample timings only. No schema-3 manifest file is
committed; the
[experiment instructions](../../bench/zk-compose/experiments/README.md) carry an
inline sample to save outside the checkout, plus the round options, schedule,
controls and limits. No measured outcome is recorded in this skill.

`result::signed` exposes separately versioned canonical signed-integer
preparation and verification, with a fixed capacity and no public sign/length
selector. See the [signed result contract](references/signed-results.md) for its
API, lexical limits and evidence boundary, and
[signed admission](references/disclosure-planner.md#canonical-signed-integer-admission)
for the independent planner. Native/core checks do not constitute genuine signed
result-proof evidence.

Default host checks validate the legacy compatibility evidence's source
hashes and byte lengths. The ZK toolchain lane independently rebuilds the fixed
foundation keys in addition to checking current keys. Only v1 byte stability is
promised; unchanged v2 circuit sizes do not establish key compatibility.

The selected-support and exact-evaluator examples also admit separately
versioned materialized synthetic profiles: bounded wallet candidates and named
organization counts. Each generated manifest runs one ordinary sample and preserves
the existing authentication, authority, replay and typed rejection contracts.

The [bounded workload campaign](../../bench/zk-compose/campaigns/README.md)
materializes wallet candidate and named-organization fixtures before measurement,
then interleaves real adapter subprocesses. It preserves per-sample failures,
unsupported combinations, exact inputs, authority/authentication identities and
raw reports. Paired planner acceptance contracts retain visibly different public
capacities; exact authority modes and selected support are separate contracts.