Skip to content

Commit 5529dbd

Browse files
authored
Clean up continuation AIR setup (#733)
1 parent 9c3cb93 commit 5529dbd

3 files changed

Lines changed: 13 additions & 36 deletions

File tree

executor/programs/asm/test_ecsm_split.s

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,7 @@ main:
55
# are set at the very START and never rewritten before the ecall. With a small
66
# continuation epoch size the ecall lands in a LATER epoch than the one that set
77
# the pointers, so the per-epoch touched-cell pass must carry registers across
8-
# the boundary to compute the right addresses. (Regression for the
9-
# epoch_touched_cells fresh-register bug.)
8+
# the boundary to compute the right addresses.
109
addi sp, sp, -96
1110
addi a0, sp, 64
1211
addi a1, sp, 0

prover/src/continuation.rs

Lines changed: 8 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,6 @@ fn global_memory_configs_from_init_page_data(
226226
/// Per-epoch register state and label.
227227
struct EpochStart<'a> {
228228
register_init: &'a [u32],
229-
is_first: bool,
230229
/// This epoch's 1-based table label (the `fini_epoch` constant).
231230
label: u64,
232231
}
@@ -292,18 +291,15 @@ impl ContinuationProof {
292291
/// preprocessed to INIT = `register_init` and FINI = `reg_fini`. Continuation epochs
293292
/// use the L2G bookend, so PAGE is skipped and `page_configs` is empty. The
294293
/// epoch-local L2G air is built separately by the caller (it needs the `label`).
295-
#[allow(clippy::too_many_arguments)]
296294
fn build_epoch_airs(
297295
elf: &Elf,
298296
opts: &ProofOptions,
299297
page_configs: &[PageConfig],
300298
table_counts: &TableCounts,
301299
register_init: &[u32],
302300
reg_fini: &[u32],
303-
is_first: bool,
304301
is_final: bool,
305302
) -> VmAirs {
306-
let register_init_arg = if is_first { None } else { Some(register_init) };
307303
// Continuation epochs preprocess FINI = R_{i+1} too (not just INIT = R_i), so the
308304
// final register file is a verifier-known public value bound by the REG-C2
309305
// Memory-bus token; reusing the same R_{i+1} as the next epoch's INIT binds
@@ -320,7 +316,7 @@ fn build_epoch_airs(
320316
table_counts,
321317
None,
322318
is_final,
323-
register_init_arg,
319+
None,
324320
None,
325321
register_preprocessed,
326322
)
@@ -375,7 +371,6 @@ fn prove_epoch(
375371
&table_counts,
376372
start.register_init,
377373
&reg_fini,
378-
start.is_first,
379374
is_final,
380375
);
381376

@@ -429,19 +424,17 @@ fn prove_epoch(
429424

430425
/// Verify one epoch using ONLY the [`EpochProof`] bundle plus the verifier-derived
431426
/// `register_init` (epoch 0: from the ELF; epoch i>0: from the previous epoch's
432-
/// `reg_fini`), `is_first`, `is_final`, and `label`. Rebuilds the AIRs and transcript
427+
/// `reg_fini`), `is_final`, and `label`. Rebuilds the AIRs and transcript
433428
/// from the bundle's statement values and indexes commits from the carried x254
434429
/// (`register_init[X254_INDEX]`), never from the prover's memory. PAGE is skipped for
435430
/// continuation epochs, so the AIRs are built with no page configs (the bundle does
436431
/// not get to supply any). Returns `true` iff the proof verifies and its committed
437432
/// L2G root matches the claimed one.
438-
#[allow(clippy::too_many_arguments)]
439433
fn verify_epoch(
440434
elf: &Elf,
441435
elf_bytes: &[u8],
442436
epoch: &EpochProof,
443437
register_init: &[u32],
444-
is_first: bool,
445438
is_final: bool,
446439
label: u64,
447440
opts: &ProofOptions,
@@ -471,7 +464,6 @@ fn verify_epoch(
471464
&epoch.table_counts,
472465
register_init,
473466
&epoch.reg_fini,
474-
is_first,
475467
is_final,
476468
);
477469
let l2g_air = l2g_memory_air(opts, label);
@@ -719,7 +711,6 @@ pub fn prove_continuation(
719711

720712
let start = EpochStart {
721713
register_init: &register_init,
722-
is_first: index == 0,
723714
label,
724715
};
725716
let epoch = prove_epoch(&elf, elf_bytes, &start, traces, is_final, &boundary, opts)?;
@@ -803,7 +794,6 @@ pub fn verify_continuation(
803794
let mut public_output: Vec<u8> = Vec::new();
804795

805796
for (index, epoch) in bundle.epochs.iter().enumerate() {
806-
let is_first = index == 0;
807797
let is_final = index == n - 1;
808798
let label = local_to_global::epoch_label(index as u64);
809799

@@ -812,7 +802,6 @@ pub fn verify_continuation(
812802
elf_bytes,
813803
epoch,
814804
&register_init,
815-
is_first,
816805
is_final,
817806
label,
818807
opts,
@@ -949,15 +938,14 @@ mod tests {
949938
);
950939
}
951940

952-
// Regression for the `epoch_touched_cells` fresh-register bug. A syscall whose
953-
// operand pointers live in registers (ECSM reads a0/a1/a2) can have those
941+
// Regression for touched-cell prediction from carried registers. A syscall
942+
// whose operand pointers live in registers (ECSM reads a0/a1/a2) can have those
954943
// registers set in an EARLIER epoch than the call. `test_ecsm_split` sets
955944
// a0/a1/a2 at the very start and runs the ECSM ~46 cycles later;
956945
// `epoch_size_log2 = 5` (32 cycles) puts the pointer setup in epoch 0 and the
957-
// ecall in epoch 1. The per-epoch
958-
// touched-cell pass must carry registers across the boundary — otherwise it
959-
// reads the pointers as 0, mispredicts the touched cells (and the ECSM
960-
// operands), and the epoch cannot verify.
946+
// ecall in epoch 1. The per-epoch touched-cell pass must carry registers across
947+
// the boundary — otherwise it reads the pointers as 0, mispredicts the touched
948+
// cells (and the ECSM operands), and the epoch cannot verify.
961949
#[test]
962950
fn test_ecsm_across_epochs_verifies() {
963951
let _ = env_logger::builder().is_test(true).try_init();
@@ -1058,7 +1046,7 @@ mod tests {
10581046
}
10591047

10601048
// Negative: reordering epochs must be rejected — each epoch proof is bound to its
1061-
// 1-based label (and is_first/chain), so a swapped epoch fails to verify. Guards
1049+
// 1-based label (and register chain), so a swapped epoch fails to verify. Guards
10621050
// the trusted-enumeration ordering.
10631051
#[test]
10641052
fn test_split_verify_rejects_reordered_epochs() {

prover/src/tables/trace_builder.rs

Lines changed: 4 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1899,20 +1899,10 @@ pub(crate) fn build_initial_image_paged(elf: &Elf, private_input: &[u8]) -> Page
18991899
image
19001900
}
19011901

1902-
/// Return the memory cells (bytes) an epoch touched, as `(address, end_value,
1903-
/// end_timestamp)` — the per-epoch input for the local-to-global table.
1904-
///
1905-
/// The epoch's `MemoryState` is seeded from `initial_image` at timestamp 0, and
1906-
/// the epoch's accesses set real timestamps (which start at 4). So cells with a
1907-
/// non-zero timestamp are exactly the ones this epoch read or wrote. The register
1908-
/// file is seeded from `register_init` (the carried registers), matching the real
1909-
/// epoch trace pass: a syscall can read its operand pointers from registers (e.g.
1910-
/// ECSM reads a0/a1/a2), so with a fresh register file those pointers would be wrong
1911-
/// for any epoch after the first, mispredicting the touched cells.
1912-
///
1913-
/// Reuses the early phases of [`Traces::from_image_and_logs`] read-only; sharing
1914-
/// a single path with it is left to a later step.
1915-
pub fn epoch_touched_cells<I: ImageSource>(
1902+
/// Test helper for computing one epoch's local-to-global touched cells without
1903+
/// building every trace table.
1904+
#[cfg(test)]
1905+
pub(crate) fn epoch_touched_cells<I: ImageSource>(
19161906
elf: &Elf,
19171907
initial_image: &I,
19181908
register_init: &[u32],

0 commit comments

Comments
 (0)