logos-storage/plonky2
1
0
Fork 0
mirror of https://github.com/logos-storage/plonky2.git synced 2026-01-04 23:03:08 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #1192 from topos-protocol/misc_constraints

Browse Source
This commit is contained in:
Robin Salen 2023-08-21 14:58:34 -04:00 committed by GitHub
commit 74212a29ae
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 23 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
evm/src/arithmetic/byte.rs
View File

@ -318,8 +318,7 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
}
let t = F::Extension::from(F::from_canonical_u64(32));
let t = builder.constant_extension(t);
let idx0_hi = builder.mul_extension(idx_decomp[5], t);
let t = builder.add_extension(idx0_lo5, idx0_hi);
let t = builder.mul_add_extension(idx_decomp[5], t, idx0_lo5);
let t = builder.sub_extension(idx[0], t);
let t = builder.mul_extension(is_byte, t);
yield_constr.constraint(builder, t);

31
evm/src/cpu/decode.rs
View File

@ -118,39 +118,33 @@ pub fn eval_packed_generic<P: PackedField>(
lv: &CpuColumnsView<P>,
yield_constr: &mut ConstraintConsumer<P>,
) {
let cycle_filter: P = COL_MAP.op.iter().map(|&col_i| lv[col_i]).sum();
// Ensure that the kernel flag is valid (either 0 or 1).
let kernel_mode = lv.is_kernel_mode;
yield_constr.constraint(cycle_filter * kernel_mode * (kernel_mode - P::ONES));
yield_constr.constraint(kernel_mode * (kernel_mode - P::ONES));
// Ensure that the opcode bits are valid: each has to be either 0 or 1.
for bit in lv.opcode_bits {
yield_constr.constraint(cycle_filter * bit * (bit - P::ONES));
yield_constr.constraint(bit * (bit - P::ONES));
}
// Check that the instruction flags are valid.
// First, check that they are all either 0 or 1.
for (_, _, _, flag_col) in OPCODES {
let flag = lv[flag_col];
yield_constr.constraint(cycle_filter * flag * (flag - P::ONES));
yield_constr.constraint(flag * (flag - P::ONES));
}
// Manually check the logic_op flag combining AND, OR and XOR.
// TODO: This would go away once cycle_filter is replaced by the sum
// of all CPU opcode flags.
let flag = lv.op.logic_op;
yield_constr.constraint(cycle_filter * flag * (flag - P::ONES));
yield_constr.constraint(flag * (flag - P::ONES));
// Now check that they sum to 0 or 1.
// Includes the logic_op flag encompassing AND, OR and XOR opcodes.
// TODO: This would go away once cycle_filter is replaced by the sum
// of all CPU opcode flags.
let flag_sum: P = OPCODES
.into_iter()
.map(|(_, _, _, flag_col)| lv[flag_col])
.sum::<P>()
+ lv.op.logic_op;
yield_constr.constraint(cycle_filter * flag_sum * (flag_sum - P::ONES));
yield_constr.constraint(flag_sum * (flag_sum - P::ONES));
// Finally, classify all opcodes, together with the kernel flag, into blocks
for (oc, block_length, kernel_only, col) in OPCODES {
@ -176,8 +170,7 @@ pub fn eval_packed_generic<P: PackedField>(
// If unavailable + opcode_mismatch is 0, then the opcode bits all match and we are in the
// correct mode.
let constr = lv[col] * (unavailable + opcode_mismatch);
yield_constr.constraint(cycle_filter * constr);
yield_constr.constraint(lv[col] * (unavailable + opcode_mismatch));
}
}
@ -188,20 +181,18 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
) {
let one = builder.one_extension();
let cycle_filter = builder.add_many_extension(COL_MAP.op.iter().map(|&col_i| lv[col_i]));
// Note: The constraints below do not need to be restricted to CPU cycles.
// Ensure that the kernel flag is valid (either 0 or 1).
let kernel_mode = lv.is_kernel_mode;
{
let constr = builder.mul_sub_extension(kernel_mode, kernel_mode, kernel_mode);
let constr = builder.mul_extension(cycle_filter, constr);
yield_constr.constraint(builder, constr);
}
// Ensure that the opcode bits are valid: each has to be either 0 or 1.
for bit in lv.opcode_bits {
let constr = builder.mul_sub_extension(bit, bit, bit);
let constr = builder.mul_extension(cycle_filter, constr);
yield_constr.constraint(builder, constr);
}
@ -210,21 +201,15 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
for (_, _, _, flag_col) in OPCODES {
let flag = lv[flag_col];
let constr = builder.mul_sub_extension(flag, flag, flag);
let constr = builder.mul_extension(cycle_filter, constr);
yield_constr.constraint(builder, constr);
}
// Manually check the logic_op flag combining AND, OR and XOR.
// TODO: This would go away once cycle_filter is replaced by the sum
// of all CPU opcode flags.
let flag = lv.op.logic_op;
let constr = builder.mul_sub_extension(flag, flag, flag);
let constr = builder.mul_extension(cycle_filter, constr);
yield_constr.constraint(builder, constr);
// Now check that they sum to 0 or 1.
// Includes the logic_op flag encompassing AND, OR and XOR opcodes.
// TODO: This would go away once cycle_filter is replaced by the sum
// of all CPU opcode flags.
{
let mut flag_sum = lv.op.logic_op;
for (_, _, _, flag_col) in OPCODES {
@ -232,7 +217,6 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
flag_sum = builder.add_extension(flag_sum, flag);
}
let constr = builder.mul_sub_extension(flag_sum, flag_sum, flag_sum);
let constr = builder.mul_extension(cycle_filter, constr);
yield_constr.constraint(builder, constr);
}
@ -263,7 +247,6 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
// correct mode.
let constr = builder.add_extension(unavailable, opcode_mismatch);
let constr = builder.mul_extension(lv[col], constr);
let constr = builder.mul_extension(cycle_filter, constr);
yield_constr.constraint(builder, constr);
}
}

20
evm/src/cpu/membus.rs
View File

@ -49,11 +49,11 @@ pub fn eval_packed<P: PackedField>(
lv: &CpuColumnsView<P>,
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_cpu_cycle: P = COL_MAP.op.iter().map(|&col_i| lv[col_i]).sum();
// Validate `lv.code_context`. It should be 0 if in kernel mode and `lv.context` if in user
// mode.
yield_constr
.constraint(is_cpu_cycle * (lv.code_context - (P::ONES - lv.is_kernel_mode) * lv.context));
// Validate `lv.code_context`.
// It should be 0 if in kernel mode and `lv.context` if in user mode.
// Note: This doesn't need to be filtered to CPU cycles, as this should also be satisfied
// during Kernel bootstrapping.
yield_constr.constraint(lv.code_context - (P::ONES - lv.is_kernel_mode) * lv.context);
// Validate `channel.used`. It should be binary.
for channel in lv.mem_channels {
@ -66,13 +66,13 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
lv: &CpuColumnsView<ExtensionTarget<D>>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
// Validate `lv.code_context`. It should be 0 if in kernel mode and `lv.context` if in user
// mode.
// Validate `lv.code_context`.
// It should be 0 if in kernel mode and `lv.context` if in user mode.
// Note: This doesn't need to be filtered to CPU cycles, as this should also be satisfied
// during Kernel bootstrapping.
let diff = builder.sub_extension(lv.context, lv.code_context);
let constr = builder.mul_sub_extension(lv.is_kernel_mode, lv.context, diff);
let is_cpu_cycle = builder.add_many_extension(COL_MAP.op.iter().map(|&col_i| lv[col_i]));
let filtered_constr = builder.mul_extension(is_cpu_cycle, constr);
yield_constr.constraint(builder, filtered_constr);
yield_constr.constraint(builder, constr);
// Validate `channel.used`. It should be binary.
for channel in lv.mem_channels {

5
evm/src/cross_table_lookup.rs
View File

@ -399,7 +399,7 @@ pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, S, const D: usize, const
consumer.constraint_first_row(*local_z - select(local_filter, combine(vars.local_values)));
// Check `Z(gw) = combination * Z(w)`
consumer.constraint_transition(
*next_z - *local_z * select(next_filter, combine(vars.next_values)),
*local_z * select(next_filter, combine(vars.next_values)) - *next_z,
);
}
}
@ -524,8 +524,7 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
.collect::<Vec<_>>();
let combined_next = challenges.combine_circuit(builder, &next_columns_eval);
let selected_next = select(builder, next_filter, combined_next);
let mut transition = builder.mul_extension(*local_z, selected_next);
transition = builder.sub_extension(*next_z, transition);
let transition = builder.mul_sub_extension(*local_z, selected_next, *next_z);
consumer.constraint_transition(builder, transition);
}
}

5
evm/src/memory/memory_stark.rs
View File

@ -408,7 +408,6 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
let diff = builder.sub_extension(next_addr_context, addr_context);
builder.sub_extension(diff, one)
};
let context_range_check = builder.mul_extension(context_first_change, context_diff);
let segment_diff = {
let diff = builder.sub_extension(next_addr_segment, addr_segment);
builder.sub_extension(diff, one)
@ -423,7 +422,9 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
let timestamp_range_check = builder.mul_extension(address_unchanged, timestamp_diff);
let computed_range_check = {
let mut sum = builder.add_extension(context_range_check, segment_range_check);
// context_range_check = context_first_change * context_diff
let mut sum =
builder.mul_add_extension(context_first_change, context_diff, segment_range_check);
sum = builder.add_extension(sum, virtual_range_check);
builder.add_extension(sum, timestamp_range_check)
};