Skip to content

Commit 6b53ac7

Browse files
committed
Merge main into fix/halt-final-pc-token
Brings in #984 (COPY replaces COMMIT, x254 becomes two words) and #1016. Conflicts: - lib.rs: keep the pinned REGISTER commitment and add main's COPY AIR. - register.rs: keep the single OFFSET/INIT/FINI/IS_PC commitment; x254 is at 508-509 now. - trace_builder.rs: drop the COMMIT aux count; REGISTER takes final_pc_ts. - constraint-program tests: CPU with ts_base 0 plus main's COPY check. Changes the merge needs without a textual conflict: - cpu_start: COPY is a fixed table ahead of REGISTER and COMMIT is gone, so the first CPU sub-proof is at 5 + HALT + the five accelerators. The air_refs debug check and cpu_proof_start_matches_air_refs_layout (now 32 masks) follow. - collect_epoch_from_cpu_ops returns Result: main made collect_ops_from_cpu fallible. - multiplicity_forgery_poc: VmAirs::new takes the CPU heights and the REGISTER commitment; the prover commits to its own trace.
2 parents e774e15 + 8e413a3 commit 6b53ac7

104 files changed

Lines changed: 11185 additions & 2039 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Cargo.lock‎

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎bin/cli/README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ cargo run -p cli --release -- execute <PROGRAM.elf> [--private-input <FILE>] [--
4141
|---|---|
4242
| `--private-input <FILE>` | Pass private input bytes to the guest (read via `get_private_input()`). |
4343
| `--flamegraph <FILE>` | Generate folded-stack flamegraph output. See [Guest Program Flamegraphs](#guest-program-flamegraphs). |
44-
| `--cycles` | Count instructions during execution and print the dynamic instruction count. Also reports `Keccak calls` / `Ecsm calls` (accelerator syscall invocations). Combined with `--flamegraph`, the accelerator lines are omitted (the flamegraph path exposes no per-log data). |
44+
| `--cycles` | Count instructions during execution and print the dynamic instruction count. Also reports `Keccak calls` / `Ecsm calls` / `Dma calls` (accelerator syscall invocations), plus `Dma bytes` copied and the `Dma rows` those copies add to the trace before its power-of-two padding. One guest `memcpy` is chunked into several DMA ecalls, so the byte and row lines, not the call count, are what the copies cost. The lines cover `memcpy`, `memmove` and `memset`, which share one ecall path and one table; the commit byte loop lives in that same table but is not tallied here. Combined with `--flamegraph`, the accelerator lines are omitted (the flamegraph path exposes no per-log data). |
4545

4646
### Prove
4747

‎bin/cli/src/main.rs‎

Lines changed: 163 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -191,9 +191,12 @@ enum Commands {
191191
cycle_budget: Option<u64>,
192192

193193
/// Print the dynamic instruction (cycle) count, plus `Keccak calls` /
194-
/// `Ecsm calls` (accelerator syscall invocations). The accelerator lines
195-
/// are omitted when combined with --flamegraph (that path has no per-log
196-
/// data).
194+
/// `Ecsm calls` / `Dma calls` (accelerator syscall invocations), and for
195+
/// DMA the `Dma bytes` copied and the `Dma rows` those copies add to the
196+
/// trace before its power-of-two padding. One `memcpy` is chunked into
197+
/// several DMA ecalls, so the byte and row lines, not the call count, are
198+
/// what the copies cost. The accelerator lines are omitted when combined
199+
/// with --flamegraph (that path has no per-log data).
197200
#[arg(long)]
198201
cycles: bool,
199202
},
@@ -408,6 +411,41 @@ struct FlamegraphCliOptions {
408411
checkpoint_cycles: Option<u64>,
409412
}
410413

414+
/// One tally per [`Accelerator`] variant, printed by `execute --cycles`.
415+
#[derive(Default)]
416+
struct AccelCounts {
417+
keccak: u64,
418+
ecsm: u64,
419+
dma: u64,
420+
/// Bytes copied and DMA table rows those copies consume. Keccak and ECSM
421+
/// cost the same per call, so DMA is the only accelerator whose report needs
422+
/// a size next to its count: one `memcpy` becomes as many ecalls as the
423+
/// guest stub chunks it into, which makes `dma` alone a poor cost proxy.
424+
dma_bytes: u64,
425+
dma_rows: u64,
426+
}
427+
428+
impl AccelCounts {
429+
/// Exhaustive `match`: a new `Accelerator` variant is a compile error here,
430+
/// so it cannot be executed without also being reported. `dst_val` is the
431+
/// ECALL's logged operands: `dst_val` is the chunk's byte count for DMA and
432+
/// unused for the others; `rows` is the COPY row count the executor derived
433+
/// at the ecall. The width follows from `count` alone today, so the row count is
434+
/// recoverable from it; the slot is kept because the AIR permits a schedule that
435+
/// reads both ends' residues and a future one may.
436+
fn tally(&mut self, accelerator: Accelerator, dst_val: u64, rows: u64) {
437+
match accelerator {
438+
Accelerator::Keccak => self.keccak += 1,
439+
Accelerator::Ecsm => self.ecsm += 1,
440+
Accelerator::Dma => {
441+
self.dma += 1;
442+
self.dma_bytes += dst_val;
443+
self.dma_rows += rows;
444+
}
445+
}
446+
}
447+
}
448+
411449
/// Classifies one executed instruction as an accelerator syscall invocation.
412450
///
413451
/// Delegates to the executor's canonical `SyscallNumbers::accelerator()` so the
@@ -461,7 +499,7 @@ fn cmd_execute(
461499
// below (the flamegraph path drives execution inside the executor and does
462500
// not expose per-log data). `None` means "not counted", so the accel lines
463501
// are omitted rather than printed as misleading zeros.
464-
let mut accel_counts: Option<(u64, u64)> = None;
502+
let mut accel_counts: Option<AccelCounts> = None;
465503

466504
let cycle_count = if let Some(ref output_path) = flamegraph.path {
467505
// Shared execute+flamegraph path (executor::flamegraph) instead of
@@ -527,14 +565,13 @@ fn cmd_execute(
527565
};
528566

529567
let mut cycle_count: u64 = 0;
530-
let mut keccak_calls: u64 = 0;
531-
let mut ecsm_calls: u64 = 0;
532-
// Reused per chunk: `(current_pc, a7)` for logs whose a7 matches an
533-
// accelerator syscall number. This is a cheap superset — a non-ECALL
568+
let mut counts = AccelCounts::default();
569+
// Reused per chunk: `(current_pc, a7, dst_val)` for logs whose a7 matches
570+
// an accelerator syscall number. This is a cheap superset — a non-ECALL
534571
// instruction can hold the same value in src1 — that `accelerator_of`
535572
// confirms below, once the chunk's `&Log` borrow (tied to the executor's
536573
// `&mut`) is released so the instruction cache can be read again.
537-
let mut accel_candidates: Vec<(u64, u64)> = Vec::new();
574+
let mut accel_candidates: Vec<(u64, u64, u64, u64)> = Vec::new();
538575
loop {
539576
let logs = match executor.resume_budgeted(cycle_count, cycle_budget) {
540577
Ok(logs) => logs,
@@ -551,17 +588,20 @@ fn cmd_execute(
551588
.map(|s| s.accelerator().is_some())
552589
.unwrap_or(false)
553590
{
554-
accel_candidates.push((log.current_pc, log.src1_val));
591+
accel_candidates.push((
592+
log.current_pc,
593+
log.src1_val,
594+
log.dst_val,
595+
log.src2_val,
596+
));
555597
}
556598
}
557599
}
558600
// `logs` is no longer used, so the executor's `&mut` borrow is free
559601
// and the instruction cache can be read to confirm each candidate.
560-
for (pc, a7) in accel_candidates.drain(..) {
561-
match accelerator_of(executor.instructions.get(pc), a7) {
562-
Some(Accelerator::Keccak) => keccak_calls += 1,
563-
Some(Accelerator::Ecsm) => ecsm_calls += 1,
564-
None => {}
602+
for (pc, a7, dst_val, rows) in accel_candidates.drain(..) {
603+
if let Some(accelerator) = accelerator_of(executor.instructions.get(pc), a7) {
604+
counts.tally(accelerator, dst_val, rows);
565605
}
566606
}
567607
if cycle_budget.is_some_and(|budget| cycle_count >= budget) {
@@ -575,16 +615,19 @@ fn cmd_execute(
575615
}
576616

577617
if cycles {
578-
accel_counts = Some((keccak_calls, ecsm_calls));
618+
accel_counts = Some(counts);
579619
}
580620
cycle_count
581621
};
582622

583623
if cycles {
584624
println!("Cycles: {}", cycle_count);
585-
if let Some((keccak_calls, ecsm_calls)) = accel_counts {
586-
println!("Keccak calls: {}", keccak_calls);
587-
println!("Ecsm calls: {}", ecsm_calls);
625+
if let Some(counts) = accel_counts {
626+
println!("Keccak calls: {}", counts.keccak);
627+
println!("Ecsm calls: {}", counts.ecsm);
628+
println!("Dma calls: {}", counts.dma);
629+
println!("Dma bytes: {}", counts.dma_bytes);
630+
println!("Dma rows: {}", counts.dma_rows);
588631
}
589632
}
590633

@@ -1163,43 +1206,115 @@ mod tests {
11631206
assert_eq!(continuation_epoch_size(20).unwrap(), 1 << 20);
11641207
}
11651208

1209+
/// The chip each syscall must drive, written out here rather than read back
1210+
/// from `SyscallNumbers::accelerator()`. Comparing the CLI against the
1211+
/// executor alone would pass if both agreed on the wrong answer — a chip
1212+
/// demoted to `None` has to fail somewhere, and this is that somewhere.
1213+
///
1214+
/// Cross-checked row by row against `SyscallNumbers::ALL`, which the
1215+
/// executor's macro generates from the enum, so a new syscall fails the test
1216+
/// until it gets a row here.
1217+
const EXPECTED_ACCELERATORS: &[(SyscallNumbers, Option<Accelerator>)] = &[
1218+
(SyscallNumbers::KeccakPermute, Some(Accelerator::Keccak)),
1219+
(SyscallNumbers::Ecsm, Some(Accelerator::Ecsm)),
1220+
(SyscallNumbers::DmaMemcpy, Some(Accelerator::Dma)),
1221+
(SyscallNumbers::DmaMemset, Some(Accelerator::Dma)),
1222+
(SyscallNumbers::Print, None),
1223+
(SyscallNumbers::Panic, None),
1224+
(SyscallNumbers::Commit, None),
1225+
(SyscallNumbers::Halt, None),
1226+
// `hint` drives its own HINT table, but the executor maps it to no
1227+
// `Accelerator`: the ecall adds no correctness constraint, so there is no
1228+
// accelerated work to attribute. `execute --cycles` reports no hint line.
1229+
(SyscallNumbers::Hint, None),
1230+
];
1231+
11661232
// `accelerator_of` must match the prover's `CpuOperation::from_log`: count an
11671233
// invocation only when the instruction is an ECALL AND a7 is the accelerator
1168-
// syscall number. Covers both accelerators, the non-accelerator syscalls, a
1169-
// non-ECALL whose src1 collides with an accelerator number, and a cache miss.
1234+
// syscall number.
11701235
#[test]
11711236
fn accelerator_of_mirrors_prover_classification() {
1172-
use executor::vm::instruction::execution::{ECSM_SYSCALL_NUMBER, KECCAK_SYSCALL_NUMBER};
1173-
11741237
let ecall = Instruction::EcallEbreak;
11751238

1176-
assert_eq!(
1177-
accelerator_of(Some(&ecall), KECCAK_SYSCALL_NUMBER),
1178-
Some(Accelerator::Keccak)
1179-
);
1180-
assert_eq!(
1181-
accelerator_of(Some(&ecall), ECSM_SYSCALL_NUMBER),
1182-
Some(Accelerator::Ecsm)
1183-
);
1239+
for &syscall in SyscallNumbers::ALL {
1240+
let rows = EXPECTED_ACCELERATORS
1241+
.iter()
1242+
.filter(|(listed, _)| *listed == syscall)
1243+
.count();
1244+
assert_eq!(
1245+
rows, 1,
1246+
"{syscall:?} needs exactly one row in EXPECTED_ACCELERATORS"
1247+
);
1248+
}
11841249

1185-
// Non-accelerator syscalls (Commit=64, Halt=93) count as neither.
1186-
assert_eq!(
1187-
accelerator_of(Some(&ecall), SyscallNumbers::Commit as u64),
1188-
None
1189-
);
1190-
assert_eq!(
1191-
accelerator_of(Some(&ecall), SyscallNumbers::Halt as u64),
1192-
None
1193-
);
1250+
for &(syscall, expected) in EXPECTED_ACCELERATORS {
1251+
assert_eq!(
1252+
accelerator_of(Some(&ecall), syscall.raw()),
1253+
expected,
1254+
"ECALL with a7 of {syscall:?} must classify as {expected:?}"
1255+
);
1256+
// A non-ECALL instruction whose src1 happens to equal a syscall a7
1257+
// must not count — this is the `f.ecall &&` guard the prover applies.
1258+
assert_eq!(
1259+
accelerator_of(Some(&Instruction::Fence), syscall.raw()),
1260+
None,
1261+
"non-ECALL with a7 of {syscall:?} must not count"
1262+
);
1263+
// No decoded instruction at the pc (cache miss) counts as neither.
1264+
assert_eq!(accelerator_of(None, syscall.raw()), None);
1265+
}
1266+
}
11941267

1195-
// A non-ECALL instruction whose src1 happens to equal an accelerator a7
1196-
// must not count — this is the `f.ecall &&` guard the prover applies.
1197-
assert_eq!(
1198-
accelerator_of(Some(&Instruction::Fence), KECCAK_SYSCALL_NUMBER),
1199-
None
1200-
);
1268+
// Every tallied accelerator gets its own counter: no two variants may share
1269+
// a field, and each must land in the one the report prints.
1270+
#[test]
1271+
fn accel_counts_tallies_each_accelerator_separately() {
1272+
for &(_, expected_accelerator) in EXPECTED_ACCELERATORS {
1273+
let Some(accelerator) = expected_accelerator else {
1274+
continue;
1275+
};
1276+
let mut counts = AccelCounts::default();
1277+
counts.tally(accelerator, 0, 0);
1278+
assert_eq!(
1279+
counts.keccak + counts.ecsm + counts.dma,
1280+
1,
1281+
"{accelerator:?} must increment exactly one counter"
1282+
);
1283+
let expected = match accelerator {
1284+
Accelerator::Keccak => counts.keccak,
1285+
Accelerator::Ecsm => counts.ecsm,
1286+
Accelerator::Dma => counts.dma,
1287+
};
1288+
assert_eq!(
1289+
expected, 1,
1290+
"{accelerator:?} must increment its own counter"
1291+
);
1292+
}
1293+
}
1294+
1295+
// The byte and row lines are what make the DMA report a cost figure rather
1296+
// than a call count, so they must accumulate across chunked ecalls and use
1297+
// the executor's row formula — the same one trace generation sizes with.
1298+
#[test]
1299+
fn accel_counts_sizes_dma_calls() {
1300+
let mut counts = AccelCounts::default();
1301+
// Rows as the executor derives them at each ecall.
1302+
for bytes in [256, 256, 8, 3, 0] {
1303+
let rows =
1304+
executor::vm::instruction::execution::copy_trace_rows(0x1000, 0x2000, bytes, false);
1305+
counts.tally(Accelerator::Dma, bytes, rows);
1306+
}
12011307

1202-
// No decoded instruction at the pc (cache miss) counts as neither.
1203-
assert_eq!(accelerator_of(None, KECCAK_SYSCALL_NUMBER), None);
1308+
assert_eq!(counts.dma, 5, "every DMA ecall counts as one call");
1309+
assert_eq!(counts.dma_bytes, 523);
1310+
// The rows are the executor's, derived where src, dst and count are all known;
1311+
// the report only sums them.
1312+
assert_eq!(counts.dma_rows, 32 + 32 + 1 + 3 + 1);
1313+
1314+
// The other accelerators must leave the DMA size lines alone.
1315+
let mut others = AccelCounts::default();
1316+
others.tally(Accelerator::Keccak, 200, 0);
1317+
others.tally(Accelerator::Ecsm, 32, 0);
1318+
assert_eq!((others.dma, others.dma_bytes, others.dma_rows), (0, 0, 0));
12041319
}
12051320
}

‎docs/continuations_design.md‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -321,7 +321,8 @@ attack and why X blocks it.
321321
### Design X
322322

323323
`MU` gates **every** L2G interaction (matches the standard table pattern —
324-
LT/MUL/MEMW each gate all their interactions with one multiplicity column).
324+
LT/MUL/MEMW gate their lookups with their multiplicity columns or sums of them; the
325+
only constant-1 sends are the `ARE_BYTES` checks that bound LT's and MUL's own μ).
325326

326327
The crucial consequence — which we first mistook for redundancy — is that gating
327328
the **Memory bus bookend** with `MU` forces `MU = 1` on every *touched* cell:
@@ -444,7 +445,7 @@ dropped the "chain is complete" property both rely on.
444445

445446
Registers must also carry across epochs: epoch *i+1* must start from epoch *i*'s
446447
final register file. Unlike memory, the register file is **small and fixed** (34
447-
registers / 67 word-addresses, all present every epoch), so it needs no L2G /
448+
registers / 68 word-addresses, all present every epoch), so it needs no L2G /
448449
global telescoping — we bind the whole snapshot directly.
449450

450451
**Mechanism (no new bus).** The REGISTER table is the register analog of PAGE — it
@@ -491,13 +492,13 @@ chain ends on are verifier-known.
491492

492493
### Commit index (x254)
493494

494-
The COMMIT chip's running output index lives in a synthetic single-word register
495-
**x254** (word-address 508), so it rides the **same** register binding above —
495+
The COPY chip's running output index lives in the synthetic register **x254**
496+
(word-addresses 508-509), so it rides the **same** register binding above —
496497
epoch *i*'s `FINI[x254]` becomes epoch *i+1*'s `INIT[x254]`, pinned by the two
497498
locks like any register. Each epoch therefore indexes its committed bytes from the
498499
*carried* value, not from `0`:
499500

500-
- the COMMIT trace seeds `current_commit_index` from x254
501+
- the COPY trace seeds `current_commit_index` from x254
501502
(`register_state.read_index()` in `trace_builder.rs`), with a debug-assert
502503
pinning the two in sync every step;
503504
- the verifier's commit-bus offset (`compute_commit_bus_offset`'s `start_index`)

0 commit comments

Comments
 (0)