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
8 changes: 0 additions & 8 deletions ceno_recursion_v2/src/circuit/inner/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,18 +29,14 @@ pub use trace::*;
pub struct InnerCircuit<S: AggregationSubCircuit> {
pub verifier_circuit: Arc<S>,
pub def_hook_commit: Option<CommitBytes>,
pub has_fixed_commit: bool,
pub has_fixed_no_omc_init_commit: bool,
pub instance_public_value_indices: Arc<Vec<Vec<usize>>>,
}

impl<SC: StarkProtocolConfig<F = F>, S: AggregationSubCircuit> Circuit<SC> for InnerCircuit<S> {
fn airs(&self) -> Vec<AirRef<SC>> {
let bus_inventory = self.verifier_circuit.bus_inventory();
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,14 +59,10 @@ impl<SC: StarkProtocolConfig<F = F>, S: AggregationSubCircuit> Circuit<SC> for I
}) as AirRef<SC>;

let vm_pvs_air = Arc::new(vm_pvs::VmPvsAir {
transcript_bus,
public_values_bus,
cached_commit_bus,
lookup_challenge_bus,
pvs_air_consistency_bus,
deferral_enabled,
has_fixed_commit: self.has_fixed_commit,
has_fixed_no_omc_init_commit: self.has_fixed_no_omc_init_commit,
instance_public_value_indices: self.instance_public_value_indices.clone(),
}) as AirRef<SC>;

Expand Down
6 changes: 0 additions & 6 deletions ceno_recursion_v2/src/circuit/inner/trace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -89,12 +89,6 @@ impl InnerTraceGen<CpuBackend<BabyBearPoseidon2Config>> for InnerTraceGenImpl {
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);
let num_lookup_challenge_consumers = proof.chip_proofs.len();
preflight.vm_pvs.lookup_challenge_alpha_lookup_count =
num_lookup_challenge_consumers;
preflight.vm_pvs.lookup_challenge_beta_lookup_count =
num_lookup_challenge_consumers;
(preflight, sponge)
})
.unzip();
Expand Down
191 changes: 8 additions & 183 deletions ceno_recursion_v2/src/circuit/inner/vm_pvs/air.rs
Original file line number Diff line number Diff line change
@@ -1,34 +1,24 @@
use std::{borrow::Borrow, sync::Arc};

use ceno_emul::{FullTracer as Tracer, WORD_SIZE};
use ceno_zkvm::{
instructions::riscv::constants::{
END_CYCLE_IDX, END_PC_IDX, EXIT_CODE_IDX, HEAP_LENGTH_IDX, HEAP_START_ADDR_IDX,
HINT_LENGTH_IDX, HINT_START_ADDR_IDX, INIT_CYCLE_IDX, INIT_PC_IDX, PUBIO_DIGEST_IDX,
PUBIO_DIGEST_U16_LIMBS, SHARD_ID_IDX, SHARD_RW_SUM_IDX,
},
structs::VK_DIGEST_LEN,
use ceno_zkvm::instructions::riscv::constants::{
END_CYCLE_IDX, END_PC_IDX, EXIT_CODE_IDX, HEAP_LENGTH_IDX, HEAP_START_ADDR_IDX,
HINT_LENGTH_IDX, HINT_START_ADDR_IDX, INIT_CYCLE_IDX, INIT_PC_IDX, PUBIO_DIGEST_IDX,
PUBIO_DIGEST_U16_LIMBS, SHARD_ID_IDX, SHARD_RW_SUM_IDX,
};
use openvm_circuit_primitives::utils::{and, assert_array_eq, not};
use openvm_stark_backend::{
BaseAirWithPublicValues, PartitionedBaseAir, interaction::InteractionBuilder,
};
use openvm_stark_sdk::config::baby_bear_poseidon2::{D_EF, DIGEST_SIZE};
use p3_air::{Air, AirBuilder, AirBuilderWithPublicValues, BaseAir};
use p3_field::PrimeCharacteristicRing;
use p3_matrix::Matrix;
use recursion_circuit::bus::{
CachedCommitBus, PublicValuesBus, PublicValuesBusMessage, TranscriptBus, TranscriptBusMessage,
};
use recursion_circuit::bus::{CachedCommitBus, PublicValuesBus, PublicValuesBusMessage};
use stark_recursion_circuit_derive::AlignedBorrow;

use crate::{
bus::{LookupChallengeBus, LookupChallengeKind, LookupChallengeMessage},
circuit::inner::{
bus::{PvsAirConsistencyBus, PvsAirConsistencyMessage},
vm_pvs::VmPvs,
},
utils::TranscriptLabel,
use crate::circuit::inner::{
bus::{PvsAirConsistencyBus, PvsAirConsistencyMessage},
vm_pvs::VmPvs,
};

#[repr(C)]
Expand All @@ -38,26 +28,14 @@ pub struct VmPvsCols<F> {
pub is_valid: F,
pub is_last: F,
pub has_verifier_pvs: F,
pub vk_digest: [[F; D_EF]; VK_DIGEST_LEN],
pub lookup_challenge_alpha: [F; D_EF],
pub lookup_challenge_beta: [F; D_EF],
pub lookup_challenge_alpha_lookup_count: F,
pub lookup_challenge_beta_lookup_count: F,
pub fixed_commit_log2_max_codeword_size: F,
pub fixed_no_omc_init_commit_log2_max_codeword_size: F,
pub witness_commit_log2_max_codeword_size: F,
pub child_pvs: VmPvs<F>,
}

pub struct VmPvsAir {
pub transcript_bus: TranscriptBus,
pub public_values_bus: PublicValuesBus,
pub cached_commit_bus: CachedCommitBus,
pub lookup_challenge_bus: LookupChallengeBus,
pub pvs_air_consistency_bus: PvsAirConsistencyBus,
pub deferral_enabled: bool,
pub has_fixed_commit: bool,
pub has_fixed_no_omc_init_commit: bool,
pub instance_public_value_indices: Arc<Vec<Vec<usize>>>,
}

Expand Down Expand Up @@ -198,159 +176,6 @@ impl<AB: AirBuilder + InteractionBuilder + AirBuilderWithPublicValues> Air<AB> f
// local.is_valid * is_leaf,
// );

// Mirror the native verifier transcript prefix exactly:
// vk digest, transcript-visible public values, commitments with size
// fields, then lookup challenge samples.
for (tidx, value) in [(0usize, 1668508018u32), (1usize, 118u32)] {
self.transcript_bus.receive(
builder,
local.proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(tidx),
value: AB::Expr::from_u32(value),
is_sample: AB::Expr::ZERO,
},
local.is_valid,
);
}

let mut transcript_tidx = TranscriptLabel::Riscv.field_len();
for digest in local.vk_digest {
self.transcript_bus.observe_ext(
builder,
local.proof_idx,
AB::Expr::from_usize(transcript_tidx),
digest,
local.is_valid,
);
transcript_tidx += D_EF;
}

for instance_indices in self.instance_public_value_indices.iter() {
for global_pv_idx in instance_indices {
self.transcript_bus.receive(
builder,
local.proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(transcript_tidx),
value: vm_public_value_by_index::<AB>(local, *global_pv_idx),
is_sample: AB::Expr::ZERO,
},
local.is_valid,
);
transcript_tidx += 1;
}
}

if self.has_fixed_commit {
for (didx, value) in local.child_pvs.fixed_commit.iter().enumerate() {
self.transcript_bus.receive(
builder,
local.proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(transcript_tidx + didx),
value: (*value).into(),
is_sample: AB::Expr::ZERO,
},
local.is_valid,
);
}
transcript_tidx += DIGEST_SIZE;
self.transcript_bus.observe(
builder,
local.proof_idx,
AB::Expr::from_usize(transcript_tidx),
local.fixed_commit_log2_max_codeword_size,
local.is_valid,
);
transcript_tidx += 1;
}

if self.has_fixed_no_omc_init_commit {
for (didx, value) in local.child_pvs.fixed_no_omc_init_commit.iter().enumerate() {
self.transcript_bus.receive(
builder,
local.proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(transcript_tidx + didx),
value: (*value).into(),
is_sample: AB::Expr::ZERO,
},
local.is_valid,
);
}
transcript_tidx += DIGEST_SIZE;
self.transcript_bus.observe(
builder,
local.proof_idx,
AB::Expr::from_usize(transcript_tidx),
local.fixed_no_omc_init_commit_log2_max_codeword_size,
local.is_valid,
);
transcript_tidx += 1;
}

for (didx, value) in local.child_pvs.witness_commit.iter().enumerate() {
self.transcript_bus.receive(
builder,
local.proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(transcript_tidx + didx),
value: (*value).into(),
is_sample: AB::Expr::ZERO,
},
local.is_valid,
);
}
transcript_tidx += DIGEST_SIZE;
self.transcript_bus.observe(
builder,
local.proof_idx,
AB::Expr::from_usize(transcript_tidx),
local.witness_commit_log2_max_codeword_size,
local.is_valid,
);
transcript_tidx += 1;

self.transcript_bus.sample_ext(
builder,
local.proof_idx,
AB::Expr::from_usize(transcript_tidx),
local.lookup_challenge_alpha,
local.is_valid,
);
transcript_tidx += D_EF;
self.transcript_bus.sample_ext(
builder,
local.proof_idx,
AB::Expr::from_usize(transcript_tidx),
local.lookup_challenge_beta,
local.is_valid,
);

for i in 0..D_EF {
self.lookup_challenge_bus.add_key_with_lookups(
builder,
local.proof_idx,
LookupChallengeMessage {
kind: AB::Expr::from_usize(LookupChallengeKind::Alpha.as_usize()),
word_idx: AB::Expr::from_usize(i),
value: local.lookup_challenge_alpha[i].into(),
},
local.is_valid * local.lookup_challenge_alpha_lookup_count,
);
self.lookup_challenge_bus.add_key_with_lookups(
builder,
local.proof_idx,
LookupChallengeMessage {
kind: AB::Expr::from_usize(LookupChallengeKind::Beta.as_usize()),
word_idx: AB::Expr::from_usize(i),
value: local.lookup_challenge_beta[i].into(),
},
local.is_valid * local.lookup_challenge_beta_lookup_count,
);
}

// We look up proof metadata from VerifierPvsAir here to ensure consistency on each row.
self.pvs_air_consistency_bus.lookup_key(
builder,
Expand Down
59 changes: 1 addition & 58 deletions ceno_recursion_v2/src/circuit/inner/vm_pvs/mod.rs
Original file line number Diff line number Diff line change
@@ -1,11 +1,7 @@
use ceno_zkvm::instructions::riscv::constants::PUBIO_DIGEST_U16_LIMBS;
use openvm_stark_backend::{FiatShamirTranscript, TranscriptHistory};
use openvm_stark_sdk::config::baby_bear_poseidon2::{BabyBearPoseidon2Config, DIGEST_SIZE, F};
use p3_field::PrimeCharacteristicRing;
use openvm_stark_sdk::config::baby_bear_poseidon2::DIGEST_SIZE;
use stark_recursion_circuit_derive::AlignedBorrow;

use crate::system::{Preflight, RecursionField, RecursionProof, RecursionVk};

mod air;
mod trace;

Expand Down Expand Up @@ -35,56 +31,3 @@ pub struct VmPvs<F> {

pub use air::*;
pub use trace::*;

#[tracing::instrument(level = "trace", skip_all)]
pub fn run_preflight<TS>(
child_vk: &RecursionVk,
proof: &RecursionProof,
preflight: &mut Preflight,
ts: &mut TS,
) where
TS: FiatShamirTranscript<BabyBearPoseidon2Config> + TranscriptHistory,
{
let vk_digest = child_vk.compute_digest();
for elem in vk_digest {
ts.observe_ext(elem);
}

// Observe public values in canonical circuit-instance order first.
for (_, circuit_vk) in child_vk.circuit_vks.iter() {
for instance_value in circuit_vk.get_cs().zkvm_v1_css.instance.iter() {
ts.observe(
proof
.public_values
.query_by_index::<RecursionField>(instance_value.0),
);
}
}

if let Some(fixed_commit) = child_vk.fixed_commit.as_ref() {
for elem in fixed_commit.commit.clone().into_iter() {
ts.observe(elem);
}
ts.observe(F::from_u64(fixed_commit.log2_max_codeword_size as u64));
}

if let Some(fixed_no_omc) = child_vk.fixed_no_omc_init_commit.as_ref() {
for elem in fixed_no_omc.commit.clone().into_iter() {
ts.observe(elem);
}
ts.observe(F::from_u64(fixed_no_omc.log2_max_codeword_size as u64));
}

let witin = &proof.witin_commit;
for elem in witin.commit.clone().into_iter() {
ts.observe(elem);
}
ts.observe(F::from_u64(witin.log2_max_codeword_size as u64));

let alpha_ext = ts.sample_ext();
let beta_ext = ts.sample_ext();
preflight.vm_pvs.lookup_challenge_alpha = alpha_ext;
preflight.vm_pvs.lookup_challenge_beta = beta_ext;
preflight.vm_pvs.lookup_challenge_alpha_lookup_count = 0;
preflight.vm_pvs.lookup_challenge_beta_lookup_count = 0;
}
Loading
Loading