feat: recursion (updated)

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+    "rust-analyzer.cargo.features": ["recursion", "backends", "cache", "parallel", "disk-persistence"]
+}

Cargo.toml

@@ -48,6 +48,7 @@ arkworks = [
 parallel = ["dep:rayon", "ark-ec?/parallel", "ark-ff?/parallel"]
 cache = ["arkworks", "dep:once_cell", "parallel"]
 disk-persistence = []
+recursion = ["arkworks"]
 
 [dependencies]
 thiserror = "2.0"
@@ -71,6 +72,7 @@ rayon = { version = "1.10", optional = true }
 [dev-dependencies]
 rand = "0.8"
 criterion = { version = "0.5", features = ["html_reports"] }
+tracing-subscriber = { version = "0.3", features = ["env-filter"] }
 
 [[example]]
 name = "basic_e2e"
@@ -84,6 +86,14 @@ required-features = ["backends"]
 name = "non_square"
 required-features = ["backends"]
 
+[[example]]
+name = "recursion"
+required-features = ["recursion"]
+
+[[example]]
+name = "print_ast"
+required-features = ["recursion"]
+
 [[example]]
 name = "homomorphic_mixed_sizes"
 required-features = ["backends"]

README.md

@@ -93,6 +93,41 @@ Com(r₁·P₁ + r₂·P₂ + ... + rₙ·Pₙ) = r₁·Com(P₁) + r₂·Com(P
 
 This property enables efficient proof aggregation and batch verification. See `examples/homomorphic.rs` for a demonstration.
 
+### Recursive Proof Composition
+
+The `recursion` feature enables *traced verification* for building recursive SNARKs that compose Dory. Verification is routed through a tracing backend controlled by a [`recursion::TraceContext`](src/recursion/context.rs):
+
+- **Witness generation mode** (`TraceContext::for_witness_gen()`): compute operations and record per-op witnesses (prover-side).
+- **Symbolic mode** (`TraceContext::for_symbolic()`): do not compute; build an `AstGraph` describing proof obligations (verifier recursion / circuit wiring).
+
+```rust
+use std::rc::Rc;
+use dory_pcs::{verify_recursive};
+use dory_pcs::recursion::TraceContext;
+
+// Witness generation (prover-side)
+let ctx = Rc::new(TraceContext::for_witness_gen());
+verify_recursive::<_, E, M1, M2, _, W, Gen>(
+    commitment, evaluation, &point, &proof, setup.clone(), &mut transcript, ctx.clone()
+)?;
+let witnesses = Rc::try_unwrap(ctx).ok().unwrap().finalize();
+
+// Symbolic mode (verifier recursion / circuit wiring)
+let ctx = Rc::new(TraceContext::for_symbolic());
+verify_recursive::<_, E, M1, M2, _, W, Gen>(
+    commitment, evaluation, &point, &proof, setup, &mut transcript, ctx.clone()
+)?;
+let ast = ctx.take_ast().unwrap();
+```
+
+To visualize the generated proof-obligation DAG, run:
+
+```bash
+cargo run --features recursion --example print_ast
+```
+
+See `examples/recursion.rs` for an end-to-end demonstration, and `examples/print_ast.rs` for the AST visualizer.
+
 ## Usage
 
 ```rust
@@ -170,6 +205,15 @@ The repository includes three comprehensive examples demonstrating different asp
    cargo run --example non_square --features backends
    ```
 
+4. **`recursion`** - Traced verification for witness generation and symbolic AST generation
+   ```bash
+   cargo run --example recursion --features recursion
+   ```
+5. **`print_ast`** - Pretty-print the verifier recursion AST/DAG for a small proof
+   ```bash
+   cargo run --example print_ast --features recursion
+   ```
+
 ## Development Setup
 
 After cloning the repository, install Git hooks to ensure code quality:
@@ -238,6 +282,7 @@ cargo bench --features backends,cache,parallel
 - `cache` - Enable prepared point caching for ~20-30% pairing speedup. Requires `arkworks` and `parallel`.
 - `parallel` - Enable parallelization using Rayon for MSMs and pairings. Works with both `arkworks` backend and enables parallel features in `ark-ec` and `ark-ff`.
 - `disk-persistence` - Enable automatic setup caching to disk. When enabled, `setup()` will load from OS-specific cache directories if available, avoiding regeneration.
+- `recursion` - Enable traced verification for recursive proof composition. Provides witness generation and hint-based verification modes.
 
 ## Project Structure
 
@@ -263,15 +308,30 @@ src/
 ├── reduce_and_fold.rs             # Inner product protocol
 ├── messages.rs                    # Protocol messages
 ├── proof.rs                       # Proof structure
-└── error.rs                       # Error types
-
+├── error.rs                       # Error types
+└── recursion/                     # Recursive verification support
+    ├── mod.rs                     # Module exports
+    ├── witness.rs                 # WitnessBackend, OpId, OpType traits/types
+    ├── context.rs                 # TraceContext for execution modes
+    ├── trace.rs                   # TraceG1, TraceG2, TraceGT wrappers
+    ├── backend.rs                 # TracingBackend implementing VerifierBackend
+    ├── ast/                       # AST/DAG representation (proof obligations)
+    │   ├── mod.rs                 # Public exports + tests
+    │   ├── core.rs                # Core DAG types + validation + builder
+    │   ├── wiring.rs              # Wiring obligations (slots/wires/op kinds)
+    │   └── analysis.rs            # Optional graph analysis helpers
+    ├── challenges.rs              # Challenge precomputation and wiring
+    ├── collection.rs              # WitnessCollection storage
+    ├── collector.rs               # WitnessCollector and generator traits
 tests/arkworks/
 ├── mod.rs                         # Test utilities
 ├── setup.rs                       # Setup tests
 ├── commitment.rs                  # Commitment tests
 ├── evaluation.rs                  # Evaluation tests
 ├── integration.rs                 # End-to-end tests
-└── soundness.rs                   # Soundness tests
+├── soundness.rs                   # Soundness tests
+├── recursion.rs                   # Trace and hint verification tests
+└── witness.rs                     # Witness generation tests
 ```
 
 ## Test Coverage
@@ -285,6 +345,7 @@ The implementation includes comprehensive tests covering:
 - Non-square matrix support (nu < sigma, nu = sigma - 1, and very rectangular cases)
 - Soundness (tampering resistance for all proof components across 20+ attack vectors)
 - Prepared point caching correctness
+- Recursive verification (witness generation and hint-based verification)
 
 ## Acknowledgments