Skip to content

Commit aa5283d

Browse files
Add asserts for values length in MemPadder init APIs (#1053)
Enforce documented preconditions in MemPadder::new_mem_records and MemPadder::init_mem_records. Prevent silent truncation from zip when values exceeds capacity. Assert values.len() <= padded_len and padded_len <= address_range.iter_addresses().len() for new_mem_records. Assert values.len() <= records.len() for init_mem_records. Aligns runtime behavior with doc “Require:” clauses and project style of asserting invariants Co-authored-by: Ming <[email protected]>
1 parent 2b1f7a4 commit aa5283d

File tree

1 file changed

+19
-0
lines changed
  • ceno_zkvm/src/instructions/riscv/rv32im

1 file changed

+19
-0
lines changed

ceno_zkvm/src/instructions/riscv/rv32im/mmu.rs

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -156,6 +156,19 @@ impl MemPadder {
156156
padded_len: usize,
157157
values: &[Word],
158158
) -> Vec<MemInitRecord> {
159+
assert!(
160+
values.len() <= padded_len,
161+
"values.len() {} exceeds padded_len {}",
162+
values.len(),
163+
padded_len
164+
);
165+
let address_capacity = address_range.iter_addresses().len();
166+
assert!(
167+
padded_len <= address_capacity,
168+
"padded_len {} exceeds address_range capacity {}",
169+
padded_len,
170+
address_capacity
171+
);
159172
let mut records = Self::new_mem_records_uninit(address_range, padded_len);
160173
for (record, &value) in zip(&mut records, values) {
161174
record.value = value;
@@ -169,6 +182,12 @@ impl MemPadder {
169182
///
170183
/// See `new_mem_records` for more details.
171184
pub fn init_mem_records(records: &mut Vec<MemInitRecord>, values: &[Word]) {
185+
assert!(
186+
values.len() <= records.len(),
187+
"values.len() {} exceeds records.len() {}",
188+
values.len(),
189+
records.len()
190+
);
172191
for (record, &value) in zip(records, values) {
173192
record.value = value;
174193
}

0 commit comments

Comments
 (0)