Skip to content

Commit fde3c23

Browse files
committed
conditional
1 parent 882f8c7 commit fde3c23

1 file changed

Lines changed: 4 additions & 2 deletions

File tree

src/memory/nebula.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -281,12 +281,14 @@ impl<F: ArkPrimeField> MemBuilder<F> {
281281
}
282282

283283
// don't record this operation
284-
pub fn nondet_read(&self, addr: usize, tag: usize) -> Vec<F> {
284+
pub fn cond_nondet_read(&self, cond: bool, addr: usize, tag: usize) -> Vec<F> {
285285
let ty = self.mem_spaces.get(&tag).unwrap();
286286
assert!(!ty.is_stack());
287287
let sr = ty.tag();
288288

289-
let read_elem = if self.mem.contains_key(&(addr, sr)) {
289+
let read_elem = if !cond {
290+
MemElem::padding(addr, ty.elem_len())
291+
} else if self.mem.contains_key(&(addr, sr)) {
290292
let re = self.mem.get(&(addr, sr)).unwrap().clone();
291293
assert_eq!(re.addr, F::from(addr as u64));
292294
re

0 commit comments

Comments
 (0)