Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 0 additions & 29 deletions ceno_recursion/src/transcript/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,32 +53,3 @@ pub fn transcript_check_pow_witness<C: Config>(
builder.assert_eq::<Var<C::N>>(bit, Usize::from(0));
});
}

pub fn clone_challenger_state<C: Config>(
builder: &mut Builder<C>,
src: &DuplexChallengerVariable<C>,
) -> DuplexChallengerVariable<C> {
let dst = DuplexChallengerVariable::new(builder);
builder
.range(0, dst.sponge_state.len())
.for_each(|idx_vec, builder| {
let value = builder.get(&src.sponge_state, idx_vec[0]);
builder.set(&dst.sponge_state, idx_vec[0], value);
});

let input_offset = src.input_ptr - src.io_empty_ptr;
builder.assign(&dst.input_ptr, input_offset + dst.io_empty_ptr);

let output_offset = src.output_ptr - src.io_empty_ptr;
builder.assign(&dst.output_ptr, output_offset + dst.io_empty_ptr);
dst
}

pub fn challenger_add_forked_index<C: Config>(
builder: &mut Builder<C>,
challenger: &mut DuplexChallengerVariable<C>,
index: &Usize<C::N>,
) {
let felt = builder.unsafe_cast_var_to_felt(index.get_var());
challenger.observe(builder, felt);
}
34 changes: 14 additions & 20 deletions ceno_recursion/src/zkvm_verifier/verifier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ use crate::{
use ceno_zkvm::structs::{ComposedConstrainSystem, VerifyingKey, ZKVMVerifyingKey};
use ff_ext::BabyBearExt4;

use crate::transcript::{challenger_add_forked_index, clone_challenger_state};
use gkr_iop::{
evaluation::EvalExpression,
gkr::{
Expand Down Expand Up @@ -167,22 +166,6 @@ pub fn verify_zkvm_proof<C: Config<F = F>>(
);
challenger.observe(builder, log2_max_codeword_size_felt);

iter_zip!(builder, zkvm_proof_input.chip_proofs).for_each(|ptr_vec, builder| {
let chip_proofs = builder.iter_ptr_get(&zkvm_proof_input.chip_proofs, ptr_vec[0]);
let chip_idx = builder.get(&chip_proofs, 0).idx_felt;
challenger.observe(builder, chip_idx);

iter_zip!(builder, chip_proofs).for_each(|ptr_vec, builder| {
let chip_proof = builder.iter_ptr_get(&chip_proofs, ptr_vec[0]);

iter_zip!(builder, chip_proof.num_instances).for_each(|ptr_vec, builder| {
let num_instance = builder.iter_ptr_get(&chip_proof.num_instances, ptr_vec[0]);
let num_instance = builder.unsafe_cast_var_to_felt(num_instance);
challenger.observe(builder, num_instance);
});
});
});

let alpha = challenger.sample_ext(builder);
let beta = challenger.sample_ext(builder);

Expand Down Expand Up @@ -253,9 +236,15 @@ pub fn verify_zkvm_proof<C: Config<F = F>>(

iter_zip!(builder, chip_proofs).for_each(|ptr_vec, builder| {
let chip_proof = builder.iter_ptr_get(&chip_proofs, ptr_vec[0]);
// fork transcript to support chip concurrently proved
let mut chip_challenger = clone_challenger_state(builder, &challenger);
challenger_add_forked_index(builder, &mut chip_challenger, &forked_sample_index);
// Fork chip transcript independently and bind challenges/metadata in verifier order.
let mut chip_challenger = DuplexChallengerVariable::new(builder);
transcript_observe_label(builder, &mut chip_challenger, b"fork");
let alpha_felts = builder.ext2felt(alpha);
chip_challenger.observe_slice(builder, alpha_felts);
let beta_felts = builder.ext2felt(beta);
chip_challenger.observe_slice(builder, beta_felts);
let fork_id_felt = builder.unsafe_cast_var_to_felt(forked_sample_index.get_var());
chip_challenger.observe(builder, fork_id_felt);
builder.assert_usize_eq(
chip_proof.rw_out_evals.length.clone(),
Usize::from(
Expand All @@ -267,6 +256,11 @@ pub fn verify_zkvm_proof<C: Config<F = F>>(
Usize::from(circuit_vk.get_cs().num_lks() * 4),
);
chip_challenger.observe(builder, chip_proof.idx_felt);
iter_zip!(builder, chip_proof.num_instances).for_each(|ptr_vec, builder| {
let num_instance = builder.iter_ptr_get(&chip_proof.num_instances, ptr_vec[0]);
let num_instance = builder.unsafe_cast_var_to_felt(num_instance);
chip_challenger.observe(builder, num_instance);
});

// getting the number of dummy padding item that we used in this opcode circuit
let num_lks: Var<C::N> =
Expand Down
44 changes: 0 additions & 44 deletions ceno_recursion_v2/skills/ceno-recursion-principles/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -72,50 +72,6 @@ When forking, keep:
- Keep target regression test command handy:
- `RUST_MIN_STACK=33554432 RUST_BACKTRACE=1 cargo test -p ceno_recursion_v2 leaf_app_proof_round_trip_placeholder -- --nocapture`

## AIR Refactor Execution Protocol (Reusable)

Use this protocol for any AIR/module refactor (not tied to a specific module such as vm_pvs).

### A. Diff-First Task Intake
- Start from user edits, not assumptions: inspect `git diff` (staged + unstaged).
- Extract added comments/TODOs and convert them into a condensed checklist with:
- behavior to implement,
- exact file/symbol target,
- acceptance condition.
- Keep comments short and actionable; remove or resolve implementation TODOs during the patch.

### B. Source-of-Truth and Pattern References
- For transcript/order semantics and real data filling, use:
- `../ceno_zkvm/src/scheme/verifier.rs` (`verify_proof_validity`).
- For constraint/bus message skeleton patterns, refer to upstream OpenVM continuation/recursion crates and mirror local style.
- Prefer adapting existing local AIR/bus patterns over inventing new message shapes.

### C. Transcript and Bus Invariants
- Preserve transcript-visible operation order before challenge sampling (`alpha`, `beta`) exactly.
- Keep producer/consumer bus keys aligned (`proof_idx`, `air_idx`, `pv_idx`, `tidx`, gating flags).
- If preflight ownership moves across modules, ensure order is preserved via explicit orchestrator steps.
- Do not silently change AIR count/order: `airs()` ordering must match proving-context ordering.

### D. Refactor Steps (Generic)
1. Read `git diff` and publish condensed implementation plan.
2. Implement real data population from source-of-truth fields (avoid placeholder drift).
3. Wire constraints/bus message skeletons using upstream-compatible patterns.
4. Reconcile preflight/transcript ordering with verifier semantics.
5. Remove stale comments and dead wiring introduced by prior placeholders.

### E. Required Validation Gate
Run both commands before declaring completion:

```bash
cargo fmt --all
RUST_LOG=debug RUST_MIN_STACK=33554432 RUST_BACKTRACE=1 cargo test --release -p ceno_recursion_v2 leaf_app_proof_round_trip_placeholder -- --nocapture
```

Acceptance criteria:
- Both commands pass.
- No order mismatch against source-of-truth transcript sequence.
- No unresolved implementation TODOs from the task diff.

## Acceptance Checklist for Migration PRs

Before continuing to next module, verify:
Expand Down
31 changes: 17 additions & 14 deletions ceno_recursion_v2/skills/recursion-v2-git-diff-driven-task/SKILL.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
---
name: recursion-v2-git-diff-driven-task
description: Diff-driven execution protocol for ceno_recursion_v2 tasks. Harvest newly added code comments from git diff, condense into an implementation checklist, implement against upstream OpenVM skeleton patterns, and fill real data from ceno_zkvm verifier source-of-truth.
description: Diff-driven execution protocol for ceno_recursion_v2 tasks. Harvest TODO/task comments from current git diff, align strictly with the user's change request, implement against upstream OpenVM skeleton patterns, and fill real data from ceno_zkvm verifier source-of-truth.
---

# Recursion V2 Git Diff Driven Task
Expand All @@ -10,7 +10,8 @@ description: Diff-driven execution protocol for ceno_recursion_v2 tasks. Harvest
Use this skill when task intent is written into newly added source comments and implementation should be driven directly by `git diff`.

This protocol enforces:
- comment-first task intake from staged and unstaged diffs,
- TODO/comment-first task intake from staged and unstaged diffs,
- explicit alignment to the user's current change request,
- condensed, reviewable implementation plans,
- upstream-compatible constraint/bus skeleton wiring,
- source-of-truth data fill from the verifier path,
Expand All @@ -27,21 +28,22 @@ Use this skill when any of the following applies:
## Diff Intake Protocol (Required)

1. Read `git diff` from both unstaged and staged changes.
2. Extract only newly added task comments that describe behavior changes.
3. Convert comments into a condensed checklist item format:
2. Extract only newly added TODO/task comments that describe behavior changes.
3. Restate the explicit user change request and filter out out-of-scope TODOs/comments.
4. Convert in-scope items into a condensed checklist format:
- `target`: file and symbol,
- `behavior`: what must be implemented,
- `acceptance`: concrete condition proving completion.
4. Remove duplicate or ambiguous items and keep only executable work items.
5. Present the condensed plan for review before editing logic.
5. Remove duplicate or ambiguous items and keep only executable work items.
6. Present the condensed plan for review before editing logic.

## Implementation Protocol (Required)

1. Implement checklist items in priority order.
2. Keep implementation scoped to the comment-defined behavior.
3. Resolve temporary task comments by either:
- replacing them with finished code, or
- retaining a minimal explicit TODO with ownership if blocked.
2. Keep implementation scoped to the user-approved request and in-scope diff TODOs.
3. Resolve every in-scope diff TODO by either:
- replacing it with finished code, or
- retaining a minimal explicit TODO with ownership and blocker rationale.
4. Preserve existing AIR ordering and bus key invariants unless checklist items explicitly request changes.

## Reference Hierarchy
Expand All @@ -59,7 +61,7 @@ Use references in this order:
## Plan Quality Bar

A valid plan must:
- map every actionable diff comment to exactly one checklist item,
- map every actionable in-scope diff TODO/comment to exactly one checklist item,
- state file/symbol targets explicitly,
- include acceptance conditions that can be verified by code reading or test execution,
- and call out any blocker assumptions before implementation starts.
Expand All @@ -77,6 +79,7 @@ cargo fmt --all

Task is done only when all are true:
- All condensed checklist items are implemented or explicitly marked blocked with rationale.
- All in-scope TODOs introduced by the current `git diff` are resolved or explicitly owned/blocked.
- No unresolved implementation comments remain from the task diff without ownership.
- Constraint/bus skeleton usage follows upstream-compatible patterns.
- Real data fill aligns with `ceno_zkvm/src/scheme/verifier.rs` semantics.
Expand All @@ -85,12 +88,12 @@ Task is done only when all are true:
## Quick Reusable Checklist Template

```markdown
- [ ] Collect unstaged + staged git diff comments
- [ ] Collect unstaged + staged git diff TODO/task comments
- [ ] Restate user request and mark in-scope items only
- [ ] Condense into target/behavior/acceptance checklist
- [ ] Share plan and get implementation go-ahead
- [ ] Implement using upstream continuation/recursion skeleton patterns
- [ ] Fill real data per ceno_zkvm verifier source-of-truth
- [ ] Remove or resolve task comments/TODOs introduced in this diff
- [ ] Resolve in-scope TODOs introduced in this diff
- [ ] Run required completion gate commands
```

Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
interface:
display_name: "Recursion V2 Diff-Driven Task"
short_description: "Implement recursion-v2 work from newly added git-diff comments with upstream skeleton and verifier-truth alignment"
default_prompt: "Follow recursion-v2-git-diff-driven-task: harvest staged+unstaged diff comments, condense into target/behavior/acceptance checklist, use upstream openvm continuation/recursion constraint-bus skeletons, fill real data per ceno_zkvm/src/scheme/verifier.rs, then run required completion gate commands in order."

short_description: "Implement recursion-v2 work from current git-diff TODO/task comments while strictly honoring explicit user scope"
default_prompt: "Follow recursion-v2-git-diff-driven-task: read staged+unstaged git diff, extract newly added TODO/task comments, restate and enforce explicit user request scope, condense in-scope work into target/behavior/acceptance checklist, implement against upstream openvm continuation/recursion constraint-bus skeletons, fill real data per ceno_zkvm/src/scheme/verifier.rs, resolve all in-scope diff TODOs (or mark owner+blocker), then run required completion gate commands in order."
33 changes: 29 additions & 4 deletions ceno_recursion_v2/src/bus.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
use openvm_poseidon2_air::POSEIDON2_WIDTH;
use openvm_stark_sdk::config::baby_bear_poseidon2::D_EF;
use recursion_circuit::{bus as upstream, define_typed_per_proof_permutation_bus};
use recursion_circuit::{
bus as upstream, define_typed_per_proof_lookup_bus, define_typed_per_proof_permutation_bus,
};
pub use upstream::{
AirPresenceBus, AirPresenceBusMessage, AirShapeBus, AirShapeBusMessage, CachedCommitBus,
CachedCommitBusMessage, ColumnClaimsBus, ColumnClaimsMessage, ExpressionClaimNMaxBus,
Expand All @@ -11,16 +13,16 @@ pub use upstream::{
};

// ── Forked transcript bus ─────────────────────────────────────────────────────
// Carries per-chip fork transcript state, addressed by (fork_id, fork_tidx)
// Carries per-chip fork transcript state, addressed by (fork_id, tidx)
// instead of the absolute tidx used by the trunk TranscriptBus.

#[repr(C)]
#[derive(stark_recursion_circuit_derive::AlignedBorrow, Debug, Clone, Copy)]
pub struct ForkedTranscriptBusMessage<T> {
/// Fork identifier (1-based). Matches TranscriptAir's fork_id column.
pub fork_id: T,
/// Position within the fork state (0-based).
pub fork_tidx: T,
/// Position within the fork transcript namespace.
pub tidx: T,
/// Sponge state element being communicated.
pub value: T,
/// 1 if this is a sample operation, 0 if observe.
Expand All @@ -29,6 +31,29 @@ pub struct ForkedTranscriptBusMessage<T> {

define_typed_per_proof_permutation_bus!(ForkedTranscriptBus, ForkedTranscriptBusMessage);

#[repr(u8)]
#[derive(Debug, Clone, Copy)]
pub enum LookupChallengeKind {
Alpha = 0,
Beta = 1,
}

impl LookupChallengeKind {
pub const fn as_usize(self) -> usize {
self as usize
}
}

#[repr(C)]
#[derive(stark_recursion_circuit_derive::AlignedBorrow, Debug, Clone, Copy)]
pub struct LookupChallengeMessage<T> {
pub kind: T,
pub word_idx: T,
pub value: T,
}

define_typed_per_proof_lookup_bus!(LookupChallengeBus, LookupChallengeMessage);

#[repr(C)]
#[derive(stark_recursion_circuit_derive::AlignedBorrow, Debug, Clone, Copy)]
pub struct TowerModuleMessage<T> {
Expand Down
2 changes: 2 additions & 0 deletions ceno_recursion_v2/src/circuit/inner/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ impl<SC: StarkProtocolConfig<F = F>, S: AggregationSubCircuit> Circuit<SC> for I
let transcript_bus = bus_inventory.transcript_bus;
let public_values_bus = bus_inventory.public_values_bus;
let cached_commit_bus = bus_inventory.cached_commit_bus;
let lookup_challenge_bus = bus_inventory.lookup_challenge_bus;
let poseidon2_compress_bus = bus_inventory.poseidon2_compress_bus;
let pvs_air_consistency_bus =
PvsAirConsistencyBus::new(self.verifier_circuit.next_bus_idx());
Expand All @@ -63,6 +64,7 @@ impl<SC: StarkProtocolConfig<F = F>, S: AggregationSubCircuit> Circuit<SC> for I
transcript_bus,
public_values_bus,
cached_commit_bus,
lookup_challenge_bus,
pvs_air_consistency_bus,
deferral_enabled,
instance_public_value_indices: self.instance_public_value_indices.clone(),
Expand Down
22 changes: 11 additions & 11 deletions ceno_recursion_v2/src/circuit/inner/trace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -83,9 +83,20 @@ impl InnerTraceGen<CpuBackend<BabyBearPoseidon2Config>> for InnerTraceGenImpl {
child_dag_commit,
self.deferral_enabled,
);
let (preflights, per_proof_initial_transcripts): (Vec<Preflight>, Vec<TS>) = proofs
.iter()
.map(|proof| {
let mut sponge = initial_transcript.clone();
let mut preflight = Preflight::default();
super::verifier::run_preflight(child_vk, proof, &mut preflight, &mut sponge);
super::vm_pvs::run_preflight(child_vk, proof, &mut preflight, &mut sponge);
(preflight, sponge)
})
.unzip();
let vm_ctx = super::vm_pvs::generate_proving_ctx(
child_vk,
proofs,
&preflights,
proofs_type,
child_is_app,
self.deferral_enabled,
Expand All @@ -105,17 +116,6 @@ impl InnerTraceGen<CpuBackend<BabyBearPoseidon2Config>> for InnerTraceGenImpl {
super::unset::generate_proving_ctx(&[], child_is_app)
};

let per_proof_initial_transcripts = proofs
.iter()
.map(|proof| {
let mut sponge = initial_transcript.clone();
let mut preflight = Preflight::default();
super::verifier::run_preflight(child_vk, proof, &mut preflight, &mut sponge);
super::vm_pvs::run_preflight(child_vk, proof, &mut preflight, &mut sponge);
sponge
})
.collect();

(
vec![verifier_ctx, vm_ctx, idx2_ctx],
poseidon2_inputs,
Expand Down
Loading
Loading