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: 5 additions & 3 deletions bin/cli/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1237,16 +1237,18 @@ mod tests {
#[test]
fn accel_counts_sizes_dma_calls() {
let mut counts = AccelCounts::default();
// (bytes, rows) as the executor derives them at each ecall.
for (bytes, rows) in [(256, 33), (256, 33), (8, 2), (3, 4), (0, 1)] {
// Rows as the executor derives them at each ecall.
for bytes in [256, 256, 8, 3, 0] {
let rows =
executor::vm::instruction::execution::copy_trace_rows(0x1000, 0x2000, bytes, false);
counts.tally(Accelerator::Dma, bytes, rows);
}

assert_eq!(counts.dma, 5, "every DMA ecall counts as one call");
assert_eq!(counts.dma_bytes, 523);
// The rows are the executor's, derived where src, dst and count are all known;
// the report only sums them.
assert_eq!(counts.dma_rows, 73);
assert_eq!(counts.dma_rows, 32 + 32 + 1 + 3 + 1);

// The other accelerators must leave the DMA size lines alone.
let mut others = AccelCounts::default();
Expand Down
5 changes: 3 additions & 2 deletions executor/programs/rust/dma_memset_min/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,9 @@ unsafe extern "C" {
}

pub fn main() {
// 43 bytes = five eight-byte rows plus a three-byte tail, so one call yields
// a first row, wide intermediate rows, tail rows and a terminal row.
// 43 bytes: the stub seeds the first 8 with stores and hands the chip the other
// 35, which it moves as four eight-byte rows and three one-byte rows. The chain
// ends on the row that moves the last byte; there is no terminal row.
let mut buffer = [0u8; 43];
let count = core::hint::black_box(buffer.len());

Expand Down
10 changes: 5 additions & 5 deletions executor/src/vm/logs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,11 @@
/// DMA memcpy and DMA memset: byte count. 0 for every other syscall, Keccak
/// included.
///
/// The row count is carried rather than recomputed downstream because it is not a
/// function of the byte count: a row is eight bytes or one, and the schedule reads
/// `src % 8` and `dst % 8` to decide. The executor is the only place that holds
/// `src`, `dst` and `count` at once, so it derives the count there and the CLI's
/// accelerator report just sums it.
/// The row count is carried rather than recomputed downstream so that trace sizing
/// and the CLI's accelerator report share one formula, `copy_trace_rows`, which the
/// executor evaluates where `src`, `dst` and `count` are all known. Today a row's
/// width follows from the remaining count alone (eight bytes, or one for the last
/// seven), so the CLI report just sums the carried counts.
#[derive(Debug, Clone)]
pub struct Log {
/// PC before instruction execution (use this to look up the instruction)
Expand Down
8 changes: 4 additions & 4 deletions executor/src/vm/memory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ impl BuildHasher for U64BuildHasher {
pub type U64HashMap<V> = HashMap<u64, V, U64BuildHasher>;

/// Total cap on public output bytes across all `commit_public_output` calls.
/// The COMMIT AIR concatenates calls via the running `x254` index, so this
/// The COPY chip's commit rows concatenate calls via the running `x254` index, so this
/// is enforced as a running-total budget rather than a per-call limit.
pub const MAX_PUBLIC_OUTPUT_TOTAL_SIZE: u64 = 1024 * 1024;
/// Maximum size of the private input memory region (in bytes). 512 MiB so a
Expand All @@ -60,7 +60,7 @@ pub const PRIVATE_INPUT_LENGTH_PREFIX_BYTES: usize = size_of::<u32>();
pub struct Memory {
cells: U64HashMap<[u8; 4]>,
/// Bytes committed to public output via `commit_public_output`. The
/// COMMIT AIR doesn't write to a fixed memory region (it streams bytes
/// COPY chip's commit rows don't write to a fixed memory region (it streams bytes
/// onto the Commit bus by `index`), so this buffer is purely the
/// executor's view used by `read_return_value` and CLI display.
public_output: Vec<u8>,
Expand Down Expand Up @@ -202,8 +202,8 @@ impl Memory {
}

/// Append `length` bytes from guest memory starting at `address` to the
/// public output. The COMMIT AIR concatenates calls via the running
/// `x254` index, and the trace builder accumulates `commit_ops` into
/// public output. The COPY chip's commit rows concatenate calls via the
/// running `x254` index, and the trace builder collects their bytes into
/// `VmProof.public_output`; this method maintains the executor's view
/// of the same byte stream so `read_return_value` matches.
pub fn commit_public_output(&mut self, address: u64, length: u64) -> Result<(), MemoryError> {
Expand Down
2 changes: 1 addition & 1 deletion executor/tests/rust.rs
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,7 @@ fn test_commit() {
fn test_ef_io_demo_concatenates_writes() {
// Demo guest reads its private input via EF `read_input`, then emits it
// back as the public output via TWO `write_output` calls (split in halves).
// The COMMIT AIR concatenates the two calls; the executor's
// The COPY chip's commit rows concatenate the two calls; the executor's
// `commit_public_output` appends in the same order.
let input: Vec<u8> = b"hello world!".to_vec();
run_program_and_check_public_output(
Expand Down
2 changes: 1 addition & 1 deletion prover/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ pub struct RuntimePageRange {
pub const FIXED_TABLE_COUNT: usize = 6;

/// How many sub-proofs each counted table contributes. Chunked chips report
/// their chunk count; the six accelerators are not chunked and report 0 or 1
/// their chunk count; the five accelerators are not chunked and report 0 or 1
/// (see `validate`). The verifier needs this to reconstruct matching AIRs.
#[derive(Debug, Clone, rkyv::Archive, rkyv::Serialize, rkyv::Deserialize)]
pub struct TableCounts {
Expand Down
2 changes: 1 addition & 1 deletion prover/src/tables/copy.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
//! COPY table — one streaming copy primitive for `memcpy`/`memmove`, `memset`
//! and the `write` syscall.
//!
//! Replaces the COMMIT table, and the DMA/DMA_SET pair that preceded it. A row copies `1` or `8`
//! Replaces the COMMIT table. A row copies `1` or `8`
//! bytes from `src` to `dst` and chains through [`BusId::CopyNext`] until the row
//! where `count == step`.
//!
Expand Down
2 changes: 1 addition & 1 deletion prover/src/tables/cpu.rs
Original file line number Diff line number Diff line change
Expand Up @@ -976,7 +976,7 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
}

// -------------------------------------------------------------------------
// ECALL: system-call bus (HALT/COMMIT/KECCAK receive). mult = ECALL.
// ECALL: system-call bus (HALT/COPY/KECCAK/ECSM/HINT receive). mult = ECALL.
// ECALL[timestamp, rv1].
// -------------------------------------------------------------------------
interactions.push(BusInteraction::sender(
Expand Down
2 changes: 1 addition & 1 deletion prover/src/tables/hint.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@
//! sound and avoids the mixed-timestamp bookkeeping of a partial-buffer read.
//!
//! `mu` is constrained to a bit (`IS_BIT`, the table's only algebraic constraint) —
//! the same guard every other multiplicity-column table carries (ECSM/ECDAS/COMMIT/
//! the same guard every other multiplicity-column table carries (ECSM/ECDAS/COPY/
//! STORE/MEMW_R). The `Ecall` bus alone does not establish it: its tuple carries the
//! timestamp, a free column, so the LogUp identity pins only the *sum* of `mu` over
//! the rows sharing a `(ts, syscall)` tuple to the CPU's send — it does not rule out
Expand Down
2 changes: 1 addition & 1 deletion prover/src/tables/keccak.rs
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ pub fn bus_interactions() -> Vec<BusInteraction> {

// 1. ECALL receiver (shared bus, per spec keccak:c:output)
// Payload: [ts_lo, ts_hi, syscall_lo32, syscall_hi32] in DWordWL [lo, hi]
// ordering, matching the CPU ECALL sender shared with HALT/COMMIT.
// ordering, matching the CPU ECALL sender shared with HALT/COPY/ECSM/HINT.
interactions.push(BusInteraction::receiver(
BusId::Ecall,
Multiplicity::Column(cols::MU),
Expand Down
4 changes: 2 additions & 2 deletions prover/src/tables/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -307,11 +307,11 @@ pub enum BusId {
// =========================================================================
/// Instruction decode lookup
Decode = 18,
/// System call handling (CPU → HALT/COMMIT for all ECALLs)
/// System call handling (CPU → HALT/COPY/KECCAK/ECSM/HINT for all ECALLs)
Ecall = 19,
// ID 20 is reserved for the removed CommitNextByte bus: COMMIT's per-byte
// recursion moved to COPY, which chains over [`BusId::CopyNext`].
/// COMMIT output bus: verifier computes the receiver contribution externally
/// Commit output bus (sent by COPY's commit rows): verifier computes the receiver contribution externally
/// from `VmProof.public_output` using the shared LogUp challenges
Commit = 21,
/// Keccak core ↔ round chip: (timestamp, round, state[200 bytes])
Expand Down
9 changes: 4 additions & 5 deletions prover/src/tests/count_table_lengths_drift_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,11 +101,10 @@ fn count_table_lengths_matches_traces() {
}

/// Runs one Rust DMA guest and asserts the sizing pass matches the built traces.
/// Each ecall has two hand-maintained replays — `collect_dma_*_ops` for
/// generation and `replay_dma_*_for_sizing` for counting — and they must agree,
/// so the fixtures cover a single chunk plus the multi-chunk / overlapping /
/// near-`MAX_DATA_ROWS` cases of `dma_memcpy_cases`, and the same schedule
/// driven through the memset table.
/// Sizing replays each ecall through `replay_copy_for_sizing`, which delegates to
/// the same `collect_copy_ops` trace generation uses; the fixtures cover a single
/// chunk plus the multi-chunk and overlapping cases of `dma_memcpy_cases`, and the
/// same schedule driven through memset.
fn assert_dma_fixture_counts(elf_name: &str, syscall_number: u64) {
let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
.parent()
Expand Down
1 change: 0 additions & 1 deletion prover/src/tests/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ pub mod branch_constraints_tests;
#[cfg(test)]
pub mod bytewise_tests;
#[cfg(test)]
#[cfg(test)]
pub mod compute_commit_bus_offset_tests;
#[cfg(test)]
pub mod constraint_emit_tests;
Expand Down
2 changes: 1 addition & 1 deletion prover/src/tests/prove_elfs_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3692,7 +3692,7 @@ fn test_prove_private_input_different_values() {

/// End-to-end: EF zkVM IO interface — demo guest reads its private input via
/// `read_input` and emits it back through TWO `write_output` calls. The
/// COMMIT AIR's running `x254` index concatenates them; the resulting proof's
/// running `x254` index of COPY's commit rows concatenates them; the resulting proof's
/// `public_output` must equal the original input.
#[test]
fn test_prove_ef_io_demo_concatenates() {
Expand Down
8 changes: 4 additions & 4 deletions prover/src/tests/skip_empty_tables_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,7 @@ fn validate_still_requires_cpu_and_the_register_file() {
}

/// The counts ride in the proof, so they are the prover's to choose, and the
/// sub-proof cross-check constrains only their *sum*. The six accelerators are
/// sub-proof cross-check constrains only their *sum*. The five accelerators are
/// not chunked — `generate_optional` emits one table or none — so any count
/// above 1 describes a table set no prover can build, and the sum alone does not
/// catch it: lower another count by the same amount and the total still matches.
Expand Down Expand Up @@ -577,7 +577,7 @@ fn an_accelerator_count_above_one_is_rejected() {
);
}

// The chunked chips keep taking any count: this is a cap on the six, not a
// The chunked chips keep taking any count: this is a cap on the five, not a
// cap on chunking.
let mut many_mul = honest.clone();
many_mul.mul = 7;
Expand Down Expand Up @@ -615,9 +615,9 @@ fn counts_that_wrap_have_no_total() {

/// The accelerators are the ones a run most often never reaches, and each cost a
/// four-row sub-proof regardless. A program with no keccak, no EC and no hint
/// ecall now carries none of the six.
/// ecall now carries none of the five.
#[test]
fn a_run_without_accelerators_omits_all_six() {
fn a_run_without_accelerators_omits_all_five() {
let (elf, logs, _instructions) = run_asm_elf("xori");
let mut traces =
Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
Expand Down
2 changes: 1 addition & 1 deletion syscalls/src/allocator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ use riscv as _;

const MAX_MEMORY_SIZE: usize = 0xC000_0000;

/// The accelerated `memset` depends on this.
/// Kept for the accelerated `memset`, though its soundness no longer depends on it.
///
/// COPY pins `dst = src + 8` with one 64-bit `ADD`, so a range crossing the 2^32 limb
/// boundary is perfectly provable and neither the chip nor the executor refuses it
Expand Down
Loading