Constrain new top to loaded value in MLOAD_GENERAL (#1434)

This commit is contained in:
Hamy Ratoanina 2023-12-19 03:57:20 -05:00 committed by GitHub
parent 18e08f4f61
commit 096c7456bb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -43,6 +43,15 @@ fn eval_packed_load<P: PackedField>(
yield_constr.constraint(filter * (load_channel.addr_segment - addr_segment));
yield_constr.constraint(filter * (load_channel.addr_virtual - addr_virtual));
// Constrain the new top of the stack.
for (&limb_loaded, &limb_new_top) in load_channel
.value
.iter()
.zip(nv.mem_channels[0].value.iter())
{
yield_constr.constraint(filter * (limb_loaded - limb_new_top));
}
// Disable remaining memory channels, if any.
for &channel in &lv.mem_channels[4..NUM_GP_CHANNELS] {
yield_constr.constraint(filter * channel.used);
@ -95,6 +104,17 @@ fn eval_ext_circuit_load<F: RichField + Extendable<D>, const D: usize>(
yield_constr.constraint(builder, constr);
}
// Constrain the new top of the stack.
for (&limb_loaded, &limb_new_top) in load_channel
.value
.iter()
.zip(nv.mem_channels[0].value.iter())
{
let diff = builder.sub_extension(limb_loaded, limb_new_top);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}
// Disable remaining memory channels, if any.
for &channel in &lv.mem_channels[4..] {
let constr = builder.mul_extension(filter, channel.used);