From 507d8f1cb30a9c0137de9c0c375f3723a6a295e1 Mon Sep 17 00:00:00 2001 From: anatg Date: Tue, 2 Jun 2026 14:05:48 +0300 Subject: [PATCH] circuit_unpacker: scaffold crate with API and docs --- Cargo.lock | 8 ++ Cargo.toml | 1 + crates/circuit_unpacker/Cargo.toml | 14 +++ crates/circuit_unpacker/src/lib.rs | 179 +++++++++++++++++++++++++++ crates/circuit_unpacker/src/tests.rs | 58 +++++++++ 5 files changed, 260 insertions(+) create mode 100644 crates/circuit_unpacker/Cargo.toml create mode 100644 crates/circuit_unpacker/src/lib.rs create mode 100644 crates/circuit_unpacker/src/tests.rs diff --git a/Cargo.lock b/Cargo.lock index fa7c43d2..18ad0e5c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1458,6 +1458,14 @@ dependencies = [ "stwo", ] +[[package]] +name = "circuit-unpacker" +version = "1.2.2" +dependencies = [ + "circuits", + "stwo", +] + [[package]] name = "circuit-verifier" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index 1e6e56a1..0a9bfc52 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,6 +6,7 @@ members = [ "crates/vm_runner", "crates/privacy_prove", "crates/privacy_circuit_verify", + "crates/circuit_unpacker", ] resolver = "2" diff --git a/crates/circuit_unpacker/Cargo.toml b/crates/circuit_unpacker/Cargo.toml new file mode 100644 index 00000000..51d8a133 --- /dev/null +++ b/crates/circuit_unpacker/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "circuit-unpacker" +version.workspace = true +edition.workspace = true +license.workspace = true +repository.workspace = true +description = "Unpacker for a perfect-binary-tree recursion of circuit_verifier proofs." + +[dependencies] +# stwo circuits +circuits = { git = "https://github.com/starkware-libs/stwo-circuits", rev = "618db0a" } + +# stwo +stwo = { version = "2.2.0" } diff --git a/crates/circuit_unpacker/src/lib.rs b/crates/circuit_unpacker/src/lib.rs new file mode 100644 index 00000000..f115af13 --- /dev/null +++ b/crates/circuit_unpacker/src/lib.rs @@ -0,0 +1,179 @@ +//! Circuit-DSL unpacker for a perfect-binary-tree recursion of stwo-circuits proofs. +//! +//! # What this crate does +//! +//! It is the circuits-DSL analogue of the Cairo unpacker bootloader +//! (`starkware/.../bootloader/run_bootloader.cairo`, `BLAKE_UNPACKING` mode). Where the Cairo +//! bootloader walks task outputs at runtime via `[size, program_hash, ...]` headers, this +//! crate's [`run_unpacker`] walks a *statically-shaped* tree of [`circuit_verifier`] proofs and +//! emits each real leaf's outputs to the caller (typically an aggregator circuit). +//! +//! # Tree shape +//! +//! The tree is a **complete perfect binary tree** of `N_total = next_power_of_2(N)` slots, where +//! `N` is the number of *real* leaves the caller provides via [`UnpackerHints::leaf_outputs`]. The +//! last `N_total - N` slots are *dummy* leaves with a canonical empty output (see +//! [`DUMMY_LEAF_OUTPUT`]). Tree height is `log2(N_total)`. Every internal node has exactly two +//! children. +//! +//! Because the shape is fully determined by `N`, this crate does *not* embed `n_subtasks` / `size` +//! headers in the preimage of each node (which the Cairo unpacker requires for runtime walking). +//! Every preimage is the minimal data needed for the Blake binding: +//! +//! ```text +//! internal node preimage: [ h_L.0, h_L.1, h_R.0, h_R.1 ] (4 QM31s) +//! leaf preimage: [ ...leaf_output ] (k_i QM31s) +//! ``` +//! +//! # Hash binding +//! +//! At every node, the unpacker emits a Blake binding that matches the construction in +//! [`circuit_verifier::verify`] exactly: +//! +//! ```text +//! computed = blake( pp_root.0 || pp_root.1 || ...preimage ) +//! assert computed == node_hash +//! ``` +//! +//! The `node_hash` for the root is supplied by the caller (it is the verifier output emitted by +//! the top-level [`circuit_verifier`] proof). The `node_hash` for an internal node is itself a +//! pair of `Var`s extracted from its parent's preimage at the recursion's known offsets. The +//! `node_hash` for a real leaf is computed in the same way (its hash is what the parent's +//! preimage embeds). +//! +//! # Dummy leaves +//! +//! Dummies are pinned to known constants throughout: [`DUMMY_LEAF_OUTPUT`] is a 1-QM31 marker +//! `0xDEAD`. The hash of each "all-dummy subtree at depth d" is precomputed off-circuit and +//! pinned in-circuit with `Eq` gates — there is no recursion into +//! dummy subtrees and no Blake gate spent on them. Mixed subtrees (one real child, one dummy) +//! recurse only on the real side. +//! +//! Dummy leaves are *not* emitted in the unpacker's output: the returned `Vec>` has +//! exactly `N` entries (one per real leaf, in tree position order). +//! +//! # Inputs the unpacker does *not* take +//! +//! - It does **not** take the leaf STWO proofs or compose `build_verification_circuit` itself. The +//! caller is responsible for already having verified each leaf and producing its `output_hash` (2 +//! QM31 wires). For the top-level [`run_unpacker`] call only the root's hash is passed in; +//! intermediate leaf hashes are extracted from preimages during recursion. +//! - It does **not** take a per-task `program_hash`: the verifier's `output_hash` already commits +//! to the inner circuit's `preprocessed_root` (via the verifier's hash construction). +//! +//! # Relation to the Cairo unpacker +//! +//! Both serve the same role — turn an opaque verifier output hash + a prover-supplied preimage +//! hint into the actual outputs, via a Blake hash binding. Differences: +//! +//! | Aspect | Cairo unpacker (`bootloader.cairo`) | This crate | +//! |---------------------------------|--------------------------------------|---------------------------------------------| +//! | Value type | `felt252` | `QM31` | +//! | Tree shape | Free (per-call, runtime-walked) | Complete perfect binary, fixed by `N` | +//! | Layout headers in preimage | `[n_subtasks, size, program_hash]` | None (positions are compile-time-known) | +//! | Walking | Dynamic (size headers in preimage) | Static (offsets known from `N` and `k_i`) | +//! | Dummies | Not applicable | Right-aligned, precomputed-constant hashes | + +#[cfg(test)] +mod tests; + +use circuits::blake::HashValue; +use circuits::context::{Context, Var}; +use circuits::ivalue::{IValue, qm31_from_u32s}; +use stwo::core::fields::qm31::QM31; + +/// Marker value for an unused (dummy) leaf slot. +/// +/// Padding required to round `N` up to `next_power_of_2(N)`. A dummy leaf's output is a single +/// QM31 holding `0xDEAD` in the first M31 limb. The exact value is soundness-irrelevant — it just +/// has to be a deterministic constant that the unpacker can pin via [`Eq`](circuits::ops::eq). +/// +/// Reading `0xDEAD` in a debug dump of a recursive proof's leaves identifies a padded slot. +pub const DUMMY_LEAF_MARKER: u32 = 0xDEAD; + +/// The full dummy leaf output: a single-QM31 sequence carrying the marker. +pub fn dummy_leaf_output() -> Vec { + vec![qm31_from_u32s(DUMMY_LEAF_MARKER, 0, 0, 0)] +} + +/// Prover-supplied hints required to unpack the recursion. +/// +/// Carries one entry per **real** leaf, in tree position order. The unpacker derives every other +/// piece of structural information (tree height, dummy positions, internal-node preimages, +/// per-level dummy hash constants) from `leaf_outputs.len()` alone. +/// +/// Each `leaf_outputs[i]` is the i-th leaf's output as the inner STWO-proven circuit emitted it +/// (i.e., `output_values` minus the trailing `u` value the verifier convention drops). Length +/// `k_i` is allowed to vary across leaves. +#[derive(Debug, Clone)] +pub struct UnpackerHints { + /// Per-leaf output values. Length = number of real leaves. + pub leaf_outputs: Vec>, +} + +impl UnpackerHints { + /// Returns the number of real leaves, `N`. + pub fn n_real_leaves(&self) -> usize { + self.leaf_outputs.len() + } + + /// Returns the number of slots in the perfect binary tree, `N_total = next_power_of_2(N)`. + pub fn n_total_leaves(&self) -> usize { + self.n_real_leaves().next_power_of_two().max(1) + } + + /// Returns the tree height (depth of the root above the leaves). 0 for a single-leaf tree. + pub fn tree_height(&self) -> u32 { + self.n_total_leaves().trailing_zeros() + } + + /// Returns the number of dummy leaves padding the tree to a power of two. + pub fn n_dummy_leaves(&self) -> usize { + self.n_total_leaves() - self.n_real_leaves() + } +} + +/// Top-level unpacker entry point. +/// +/// # Arguments +/// +/// * `ctx` — circuits-DSL build context. `Value` is typically `QM31` (witness-carrying build, the +/// resulting context can validate via `is_circuit_valid()`) or `NoValue` (topology-only). +/// * `root_hash` — the 2-QM31 hash digest emitted by the top-level [`circuit_verifier`] proof. +/// Bound to the rest of the recursion via the Blake construction above. +/// * `preprocessed_root` — `preprocessed_root` of the underlying AIR. Identical at every internal +/// node (recursive-tree case: same verifier AIR at every layer). +/// * `hints` — prover-supplied preimage hints. See [`UnpackerHints`]. +/// +/// # Returns +/// +/// One inner `Vec` per real leaf, in tree position order. Inner length is the leaf's `k_i`. +/// Dummy leaves are not represented in the output. +/// +/// # Soundness contract +/// +/// On `ctx.is_circuit_valid()` returning `Ok`, the returned `Vec>` is guaranteed to +/// equal the actual outputs the STWO-proven leaf circuits emitted, chained back to `root_hash` +/// via a continuous Blake hash binding. The prover cannot supply differing +/// `hints.leaf_outputs` without falsifying one of the Blake assertions. +/// +/// Dummy positions are pinned to precomputed constants via `Eq` gates and cannot be +/// substituted by the prover for real (potentially-malicious) subtrees. +pub fn run_unpacker( + _ctx: &mut Context, + _root_hash: HashValue, + _preprocessed_root: HashValue, + hints: &UnpackerHints, +) -> Vec> { + // TODO: implement the Blake-binding tree walk. The real implementation pads + // `hints.leaf_outputs` with `dummy_leaf_output()` up to `n_total_leaves()` (a perfect binary + // tree of height `tree_height()`, with `n_dummy_leaves()` right-aligned dummy slots), recurses + // to bind every node under `preprocessed_root`, and truncates back to the real leaves. For now + // we only derive the (witness-independent) tree shape and return one empty output slot per real + // leaf; the leaf Vars and Blake gates arrive with the implementation. + let n_real = hints.n_real_leaves(); + debug_assert_eq!(hints.n_total_leaves(), n_real + hints.n_dummy_leaves()); + debug_assert_eq!(hints.n_total_leaves(), 1usize << hints.tree_height()); + let _dummy_fill = dummy_leaf_output(); + vec![Vec::new(); n_real] +} diff --git a/crates/circuit_unpacker/src/tests.rs b/crates/circuit_unpacker/src/tests.rs new file mode 100644 index 00000000..04874120 --- /dev/null +++ b/crates/circuit_unpacker/src/tests.rs @@ -0,0 +1,58 @@ +use circuits::blake::HashValue; +use circuits::context::Context; +use circuits::ivalue::{IValue, qm31_from_u32s}; +use stwo::core::fields::qm31::QM31; + +use crate::{UnpackerHints, run_unpacker}; + +/// Builds the preimage `[pp_root.0, pp_root.1, ...payload]` and Blake-hashes it off-circuit. +/// Mirrors the in-circuit hash construction used by both `circuit_verifier::verify` and the +/// unpacker, so the two are guaranteed to agree. +fn hash_with_pp_root(pp_root: HashValue, payload: &[QM31]) -> HashValue { + let preimage: Vec = std::iter::once(pp_root.0) + .chain(std::iter::once(pp_root.1)) + .chain(payload.iter().copied()) + .collect(); + QM31::blake(&preimage, preimage.len() * 16) +} + +/// Test 1: `N = 2` real leaves, no dummies (`N` is already a power of two). +/// Tree height = 1; the root has two leaf children, each with a distinct output length. +/// +/// Builds the expected root hash off-circuit, runs the unpacker with that hash and the matching +/// `leaf_outputs` hints, and asserts: +/// 1. The resulting circuit is valid (every constraint holds for the chosen witness). +/// 2. The returned `Vec>` has one inner `Vec` per real leaf with the right length. +/// 3. The returned `Var`s carry the QM31 values from `leaf_outputs`. +#[test] +fn unpacker_n2_no_dummies() { + // Distinguishable test data — pp_root, two leaf outputs of differing length. + let pp_root: HashValue = + HashValue(qm31_from_u32s(1, 0, 0, 0), qm31_from_u32s(2, 0, 0, 0)); + let leaf_0_output: Vec = (10..13).map(|i| qm31_from_u32s(i, 0, 0, 0)).collect(); + let leaf_1_output: Vec = (20..22).map(|i| qm31_from_u32s(i, 0, 0, 0)).collect(); + + // Off-circuit reference hashes. + let leaf_0_hash = hash_with_pp_root(pp_root, &leaf_0_output); + let leaf_1_hash = hash_with_pp_root(pp_root, &leaf_1_output); + let root_payload = vec![leaf_0_hash.0, leaf_0_hash.1, leaf_1_hash.0, leaf_1_hash.1]; + let root_hash = hash_with_pp_root(pp_root, &root_payload); + + // Build the unpacker circuit with witness values, wire pp_root and root_hash as constant + // Vars, then invoke the unpacker. + let mut ctx: Context = Context::default(); + let pp_root_vars = HashValue(ctx.constant(pp_root.0), ctx.constant(pp_root.1)); + let root_hash_vars = HashValue(ctx.constant(root_hash.0), ctx.constant(root_hash.1)); + let hints = UnpackerHints { + leaf_outputs: vec![leaf_0_output.clone(), leaf_1_output.clone()], + }; + + let _result = run_unpacker(&mut ctx, root_hash_vars, pp_root_vars, &hints); + + // TODO: `run_unpacker` is not implemented yet, so the output-shape (2) and output-value (3) + // assertions land with the implementation. Only circuit validity is checked for now. + assert!( + ctx.is_circuit_valid(), + "circuit constraints failed for valid input" + ); +}