Skip to content

Commit 070a21c

Browse files
jeswrclaude
andauthored
feat(zk): Noir mirror of the DualLeafV2 no-value sentinel, pinned to the host constant (#7103)
* feat(zk): Noir mirror of the DualLeafV2 no-value sentinel (host-pinned) Adds `zk/dual-leaf-v2`, a dependency-free Noir library carrying the `DualLeafV2` reserved no-value sentinel and the scale-free value-lane constants as `global`s, re-checking the sentinel's band exclusion in Noir, and exporting the two assertions a dual-leaf leaf recompute would call (`assert_handle_not_value_none`, `assert_handle_in_band`). `crates/sparq-zk/tests/dual_leaf_v2_noir_pin.rs` pins every Noir literal to its host derivation in `dual_leaf_v2` (include_str!, so a moved file is a compile error), and re-asserts the band exclusion on the value parsed out of the Noir file. A SEPARATE Nargo package on purpose: every `*.nr` under `zk/compose` is sha256-pinned by the `bench/zk-compose` measurement evidence, whose verifier requires the measured inventory to equal that tree exactly, so a new file there would invalidate a measurement only dedicated hardware can redo. Scope, honestly: ENFORCEMENT is still open. No member in `zk/compose` imports the library, so no shipped circuit asserts the band exclusion on a witnessed hook, and no proof that verifies today changes. The in-circuit leaf recompute does not exist in Noir. The docs that said the in-circuit half had not shipped at all are corrected to say the mirror has, the enforcement has not. CI: the zk-toolchain lane runs `nargo test` on the new package (and its paths filter now covers it); the host pin rides the existing `sparq-zk (dual-leaf)` feature-matrix leg, so the leg-name golden is untouched. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015CB7XiW3NDsggNCuDcuJJo * fix(ci): attribute the DualLeafV2 Noir mirror to sparq-zk in the ownership map `docs-quality quick-gates` failed on the first push: `tests/dual_leaf_v2_noir_pin.rs` `include_str!`s `zk/dual-leaf-v2/src/lib.nr`, which is an out-of-crate repo-level input, and the path-ownership audit (scripts/ci_audit_inputs.py, self-tested by scripts/tests/test_path_ownership.py) requires every such read to be attributed in ci/path-ownership.toml or the change-based selector cannot know a literal edit there must re-run sparq-zk. Adds the `[[map]]` entry. `python3 scripts/tests/test_path_ownership.py` now passes (30 tests) and `scripts/ci_audit_inputs.py` reports the file as covered. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015CB7XiW3NDsggNCuDcuJJo --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent e3a619b commit 070a21c

12 files changed

Lines changed: 421 additions & 19 deletions

File tree

‎.github/feature-matrix.d/sparq-zk.yml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,12 @@
1919

2020
# Exercise the default-OFF dual-leaf identity/desynchronisation
2121
# regression guard in an explicit opt-in matrix leg.
22+
# It also carries `tests/dual_leaf_v2_noir_pin.rs` (same `dual-leaf` feature):
23+
# the host/circuit pin tying every `global` in zk/dual-leaf-v2/src/lib.nr to its
24+
# `dual_leaf_v2` host derivation. The Noir half of that mirror runs as `nargo test`
25+
# in `.github/workflows/zk-toolchain.yml`; this leg is where the HOST half runs, so
26+
# the two cannot drift apart unnoticed. The leg NAME is unchanged, so
27+
# scripts/tests/feature-matrix-legnames.golden.txt is untouched.
2228
- name: "sparq-zk (dual-leaf — identity/desync regression guard)"
2329
crate: "sparq-zk"
2430
features: "dual-leaf"

‎.github/workflows/zk-toolchain.yml‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,12 @@ on:
6666
# sq-5reoy: narrowed from zk/** to zk/compose/** — the zk/ieee754 and
6767
# zk/xpath trees were externalized to the sparq-org/noir_IEEE754 and
6868
# sparq-org/noir_XPath face repos (#1599), whose own CI covers their nargo tests
69-
# and the ieee754 differential oracle. zk/compose is the only in-tree Noir tree left.
69+
# and the ieee754 differential oracle. zk/compose is the only in-tree Noir tree that
70+
# PROVES anything; zk/dual-leaf-v2 (the DualLeafV2 sentinel/constants mirror, no deps,
71+
# imported by no member) is the one other in-tree Noir package and runs its nargo tests
72+
# in this lane too.
7073
- "zk/compose/**"
74+
- "zk/dual-leaf-v2/**"
7175
- "bench/zk-compose/campaigns/**"
7276
- "bench/zk-bindings/**"
7377
- "crates/sparq-conformance/examples/proof_corpus.rs"
@@ -88,6 +92,7 @@ on:
8892
# sq-5reoy: narrowed from zk/** to zk/compose/** (see the pull_request
8993
# paths note above — the ieee754/xpath trees moved to their face repos, #1599).
9094
- "zk/compose/**"
95+
- "zk/dual-leaf-v2/**"
9196
- "bench/zk-compose/campaigns/**"
9297
- "bench/zk-bindings/**"
9398
- "crates/sparq-conformance/examples/proof_corpus.rs"
@@ -391,6 +396,17 @@ jobs:
391396
working-directory: zk/compose
392397
run: nargo test --package sparq_zk_compose_core
393398

399+
# The DualLeafV2 sentinel/constants mirror (zk/dual-leaf-v2). A separate Nargo
400+
# package on purpose: every *.nr under zk/compose is sha256-pinned by the
401+
# bench/zk-compose measurement evidence, whose verifier requires the measured
402+
# inventory to equal the tree EXACTLY (verify_result_evidence.py), so a new file
403+
# there would invalidate a measurement that only dedicated hardware can redo.
404+
# Dependency-free, imported by no member: compile + execute only, seconds.
405+
- name: Run the DualLeafV2 constants-mirror Noir tests (nargo test)
406+
if: steps.changes.outputs.zk == 'true'
407+
working-directory: zk/dual-leaf-v2
408+
run: nargo test
409+
394410
# The load-bearing step: run EVERY `#[ignore]`d test in the ZK crates. With the
395411
# toolchain on PATH the forge tests do a REAL bb prove and assert every forgery is
396412
# REJECTED (and the positive controls verify); the empirical bb anchors re-validate

‎AGENTS.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,7 @@ A `zk/compose/` **member** is a `bin`-type Noir package directory under `zk/comp
189189
2. **Run the Rust gate locally:** `cargo nextest run -p sparq-zk-compose` (NOT just `nargo test`). `snapshot_covers_every_member` runs WITHOUT the `nargo`/`bb` toolchain — it only reads the `zk/compose/` directory names against the snapshot — so this step catches a missing baseline even on a box without the ZK toolchain. The `gate_count_regression` bloat check additionally needs `nargo`+`bb` (it skips cleanly when absent).
190190

191191
This is **Gate G5** territory for top-level `zk/` `bin` circuits (`snapshot_covers_top_level_circuits`); the `zk/compose/`-family coverage is enforced by `snapshot_covers_every_member` in the same test file.
192-
**Externalized Noir dependencies (sq-5reoy / #1599).** The former in-tree `zk/ieee754` and `zk/xpath` trees were split out to the [`sparq-org/noir_IEEE754`](https://github.com/sparq-org/noir_IEEE754) and [`sparq-org/noir_XPath`](https://github.com/sparq-org/noir_XPath) face repos and removed from this repo. Their latest releases are **`v0.11.0`** (noir_IEEE754) and **`v0.3.0`** (noir_XPath, cut 2026-07-06 — see `research/zk-audit-readiness-dossier.md` §1.3). Those are the face repos' own release trains and are NOT automatically what this repo consumes: `zk/compose` pins `sparq_ieee754 @ v0.11.0`, and the XPath differential harness pins `XPATH_TAG: "v0.3.0"` (`.github/workflows/xpath-differential.yml`, `zk/xpath/scripts/run_differential_harness.sh` — bumped off v0.2.0 by #5456, so that lane's evidence is now about the current release) — read the pin, not this note, when you need to know what a lane actually verifies. `zk/compose` is the only in-tree Noir tree left; `zk/compose/compose_core/Nargo.toml` now consumes `sparq_ieee754` as a **pinned Nargo git dependency** (`{ git = "…/noir_IEEE754", tag = "v0.11.0" }`), exactly like its existing `poseidon` git dep. Two consequences for agents: (1) any `nargo compile` of `zk/compose` (the forge suite, `bench/zk-compose/scripts/gate_counts.sh`, the `sparq-zk-compose` test estate) now **fetches that git dep from GitHub** — a cold `~/.nargo` cache needs network access; a network-restricted runner must warm `~/.nargo` first. (2) **Toolchain-pin drift:** the `NARGO_VERSION`/`BB_VERSION` pins in `zk-toolchain.yml` and the face repos' pins are now maintained independently — when you bump the Noir toolchain here, confirm the released `sparq_ieee754` tag was cut on a compatible `nargo` (and re-run the forge suite, which compiles the git dep). Their nargo tests + the ieee754 differential oracle now run in the face repos' own CI, not in `zk-toolchain.yml`.
192+
**Externalized Noir dependencies (sq-5reoy / #1599).** The former in-tree `zk/ieee754` and `zk/xpath` trees were split out to the [`sparq-org/noir_IEEE754`](https://github.com/sparq-org/noir_IEEE754) and [`sparq-org/noir_XPath`](https://github.com/sparq-org/noir_XPath) face repos and removed from this repo. Their latest releases are **`v0.11.0`** (noir_IEEE754) and **`v0.3.0`** (noir_XPath, cut 2026-07-06 — see `research/zk-audit-readiness-dossier.md` §1.3). Those are the face repos' own release trains and are NOT automatically what this repo consumes: `zk/compose` pins `sparq_ieee754 @ v0.11.0`, and the XPath differential harness pins `XPATH_TAG: "v0.3.0"` (`.github/workflows/xpath-differential.yml`, `zk/xpath/scripts/run_differential_harness.sh` — bumped off v0.2.0 by #5456, so that lane's evidence is now about the current release) — read the pin, not this note, when you need to know what a lane actually verifies. `zk/compose` is the only in-tree Noir tree that PROVES anything (the one other in-tree Noir package, `zk/dual-leaf-v2`, is a dependency-free constants + assertions library mirroring the `DualLeafV2` host sentinel, run by `nargo test` in the same lane and imported by no member); `zk/compose/compose_core/Nargo.toml` now consumes `sparq_ieee754` as a **pinned Nargo git dependency** (`{ git = "…/noir_IEEE754", tag = "v0.11.0" }`), exactly like its existing `poseidon` git dep. Two consequences for agents: (1) any `nargo compile` of `zk/compose` (the forge suite, `bench/zk-compose/scripts/gate_counts.sh`, the `sparq-zk-compose` test estate) now **fetches that git dep from GitHub** — a cold `~/.nargo` cache needs network access; a network-restricted runner must warm `~/.nargo` first. (2) **Toolchain-pin drift:** the `NARGO_VERSION`/`BB_VERSION` pins in `zk-toolchain.yml` and the face repos' pins are now maintained independently — when you bump the Noir toolchain here, confirm the released `sparq_ieee754` tag was cut on a compatible `nargo` (and re-run the forge suite, which compiles the git dep). Their nargo tests + the ieee754 differential oracle now run in the face repos' own CI, not in `zk-toolchain.yml`.
193193

194194
### New-parser correctness checklist — shipping a hand-written parser
195195
A hand-written parser (replacing or bypassing a reference implementation) ships only with **ALL** of (design record: [`research/testing-strategy-assessment-2026-07.md`](research/testing-strategy-assessment-2026-07.md), section 8):

‎CHANGELOG.md‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -115,8 +115,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
115115
left in the plain mode, and a `value_none()` re-derived until it falls outside the reachable
116116
value-handle band, which `is_in_handle_band` decides and a test asserts — the checkable invariant
117117
`research/zk-field-native-encoding.md` §14.1 asks for, discharging that reserved-tag requirement on
118-
the HOST side. The in-circuit half stays open: no Noir global or assert names the sentinel, so a
119-
member refuses it only because its `u64` range decomposition cannot represent it. V1's constants, vectors and public API are
118+
the HOST side. The in-circuit half stays open: the `zk/dual-leaf-v2` Noir library mirrors the
119+
sentinel and its band check, but no proving member imports it, so a member refuses the sentinel
120+
only because its `u64` range decomposition cannot represent it. V1's constants, vectors and public API are
120121
unchanged and V1 stays recognised and verifiable, but it is no longer production-selectable. The
121122
§14.1 `LANG_NONE` separation is asserted on the host side only (see the hardening entry below). Both versions carry the same #769-accepted INV-VL
122123
downgrade; not externally audited (CR-G8 / sq-qhy4).

‎ci/path-ownership.toml‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,16 @@ crates = ["sparq-reason"]
192192
pattern = "bench/zk-compose/**"
193193
crates = ["sparq-zk-compose"]
194194

195+
# The DualLeafV2 sentinel/constants Noir mirror, include_str!'d by sparq-zk's
196+
# tests/dual_leaf_v2_noir_pin.rs (the host/circuit pin: every `global` in that
197+
# .nr must equal its dual_leaf_v2 host derivation). A literal edit there is
198+
# exactly a change that must re-run sparq-zk, so the file is attributed to it.
199+
# It sits OUTSIDE zk/compose on purpose — every *.nr under zk/compose is
200+
# sha256-pinned by the bench/zk-compose measurement evidence.
201+
[[map]]
202+
pattern = "zk/dual-leaf-v2/**"
203+
crates = ["sparq-zk"]
204+
195205
# [FABLE-5] sq-0iqzw: the ADJUDICATED cross-engine divergence allowlist, read at
196206
# runtime by the sparq-bench differential fuzzer (crates/sparq-bench/src/fuzz.rs
197207
# DivergenceAllowlist, via an env!("CARGO_MANIFEST_DIR")-relative path) AND by its

0 commit comments

Comments
 (0)