Skip to content
Open
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
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
#### Bug Fixes

- Fixed debug-only underflow in memory range-check trace generation when the first memory access is at `clk = 0` ([#2976](https://github.com/0xMiden/miden-vm/pull/2976)).
- Aligned replay stack word access bounds with `StackInterface`, allowing the maximum valid start index for word reads and writes ([#3014](https://github.com/0xMiden/miden-vm/pull/3014)).
- Replaced unsound `ptr::read` with safe unbox in panic recovery, removing UB from potential double-drop ([#2934](https://github.com/0xMiden/miden-vm/pull/2934)).
- Reverted `InvokeKind::ProcRef` back to `InvokeKind::Exec` in `visit_mut_procref` and added an explanatory comment (#2893).
- Fixed the release dry-run publish cycle between `miden-air` and `miden-ace-codegen`, and preserved leaf-only DAG imports with explicit snapshots ([#2931](https://github.com/0xMiden/miden-vm/pull/2931)).
Expand Down
46 changes: 44 additions & 2 deletions processor/src/trace/parallel/processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,7 @@ impl StackInterface for ReplayProcessor {
}

fn get_word(&self, start_idx: usize) -> Word {
debug_assert!(start_idx < MIN_STACK_DEPTH - 4);
debug_assert!(start_idx <= MIN_STACK_DEPTH - WORD_SIZE);
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would it be clearer to write this as debug_assert!(start_idx + WORD_SIZE <= MIN_STACK_DEPTH)? That states the full-word-fit invariant directly, which makes the later offset math easier to check at a glance.


let word_start_idx = MIN_STACK_DEPTH - start_idx - 4;
let mut result: [Felt; WORD_SIZE] =
Expand All @@ -274,7 +274,7 @@ impl StackInterface for ReplayProcessor {
}

fn set_word(&mut self, start_idx: usize, word: &Word) {
debug_assert!(start_idx < MIN_STACK_DEPTH - 4);
debug_assert!(start_idx <= MIN_STACK_DEPTH - WORD_SIZE);
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Related to this bound, would it help to switch the next line to MIN_STACK_DEPTH - start_idx - WORD_SIZE instead of - 4? Using WORD_SIZE in both places makes the offset formula much easier to audit.

let word_start_idx = MIN_STACK_DEPTH - start_idx - 4;

// Reverse so word[0] ends up at the top of stack (highest internal index)
Expand Down Expand Up @@ -506,3 +506,45 @@ impl Stopper for ReplayStopper {
}
}
}

#[cfg(test)]
mod tests {
use super::*;
use crate::trace::trace_state::{
AdviceReplay, ExecutionContextReplay, HasherResponseReplay, MastForestResolutionReplay,
MemoryReadsReplay, StackOverflowReplay, StackState, SystemState,
};

fn build_replay_processor() -> ReplayProcessor {
let system = SystemState {
clk: 0_u32.into(),
ctx: ContextId::root(),
fn_hash: Word::default(),
pc_transcript_state: Word::default(),
};
let stack = StackState::new([ZERO; MIN_STACK_DEPTH], MIN_STACK_DEPTH, ZERO);

ReplayProcessor::new(
system,
stack,
StackOverflowReplay::default(),
ExecutionContextReplay::default(),
AdviceReplay::default(),
MemoryReadsReplay::default(),
HasherResponseReplay::default(),
MastForestResolutionReplay::default(),
1_u32.into(),
)
}

#[test]
fn stack_set_word_allows_max_start_idx() {
let mut processor = build_replay_processor();
let start_idx = MIN_STACK_DEPTH - WORD_SIZE;
let word = [Felt::new(1), Felt::new(2), Felt::new(3), Felt::new(4)].into();
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since this test is about the WORD_SIZE boundary, would it make sense to build the sample word from WORD_SIZE too instead of a 4-element literal? That keeps the test aligned with the same constant the implementation is checking.


processor.set_word(start_idx, &word);

assert_eq!(processor.get_word(start_idx), word);
}
}
Loading