Constrain uninitialized memory to 0 (#1318)

This commit is contained in:
Hamy Ratoanina 2023-11-03 19:52:12 -04:00 committed by GitHub
parent f71f227d3c
commit d2b549affc
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -324,10 +324,14 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
yield_constr.constraint_transition(range_check - computed_range_check);
// Enumerate purportedly-ordered log.
// We assume that memory is initialized with 0. This means that if the first operation of a new address
// is a read, then its value must be 0.
for i in 0..8 {
yield_constr.constraint_transition(
next_is_read * address_unchanged * (next_values_limbs[i] - value_limbs[i]),
);
yield_constr
.constraint_transition(next_is_read * not_address_unchanged * next_values_limbs[i]);
}
}
@ -445,11 +449,17 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
yield_constr.constraint_transition(builder, range_check_diff);
// Enumerate purportedly-ordered log.
// We assume that memory is initialized with 0. This means that if the first operation of a new address
// is a read, then its value must be 0.
for i in 0..8 {
let value_diff = builder.sub_extension(next_values_limbs[i], value_limbs[i]);
let zero_if_read = builder.mul_extension(address_unchanged, value_diff);
let read_constraint = builder.mul_extension(next_is_read, zero_if_read);
yield_constr.constraint_transition(builder, read_constraint);
let first_read_value =
builder.mul_extension(next_values_limbs[i], not_address_unchanged);
let first_read_constraint = builder.mul_extension(first_read_value, next_is_read);
yield_constr.constraint_transition(builder, first_read_constraint);
}
}