fix is_small_add #989
fix is_small_add #989
Conversation
59cbc54 to
592a940
Compare
There was a problem hiding this comment.
Reviewed 1 of 2 files at r1, all commit messages.
Reviewable status: 1 of 2 files reviewed, 5 unresolved discussions (waiting on @DavidLevitGurevich)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 17 at r2 (raw file):
// Small add operands are 27 bits. const SMALL_ADD_MAX_VALUE: u128 = 2_u128.pow(27) - 1;
u128 probably shouldnt appear anywhere in this context
the bounds should either be defined by [u32;8], or be projected to a range (טווח) that makes sense - in the small add case that is i32
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 700 at r2 (raw file):
fn is_small_add(dst: MemoryValue, op0: MemoryValue, op_1: MemoryValue) -> bool { [dst, op0, op_1].iter().all(|val| { match val {
I think you should delegate this to a function and test it specifically
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 707 at r2 (raw file):
let val = limbs_to_u128(felt252[0..4].try_into().unwrap()); val <= SMALL_ADD_MAX_VALUE }
I think you can delete, the 3rd case should cover every possible value
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 712 at r2 (raw file):
let val_be = val.iter().rev(); let p_min_1_be = P_MIN_1.iter().rev(); let p_min_2_to_27_be = P_MIN_2_TO_27.iter().rev();
iterate in reverse?
Code quote:
let val_be = val.iter().rev();
let p_min_1_be = P_MIN_1.iter().rev();
let p_min_2_to_27_be = P_MIN_2_TO_27.iter().rev();stwo_cairo_prover/crates/adapter/src/opcodes.rs line 718 at r2 (raw file):
val_be.clone().cmp(p_min_2_to_27_be), Ordering::Greater | Ordering::Equal ) && matches!(val_be.cmp(p_min_1_be), Ordering::Less | Ordering::Equal)
name the two variables
Code quote:
// For small negative we check that operands are in the range [P-2^27, P-1].
matches!(
val_be.clone().cmp(p_min_2_to_27_be),
Ordering::Greater | Ordering::Equal
) && matches!(val_be.cmp(p_min_1_be), Ordering::Less | Ordering::Equal)stwo_cairo_prover/crates/adapter/src/opcodes.rs line 1072 at r2 (raw file):
let casm_states_by_opcode = CasmStatesByOpcode::from_iter([trace_entry].into_iter(), &memory_builder); assert_eq!(casm_states_by_opcode.add_opcode_small.len(), 1);
Suggestion:
memory_builder.set(fp, MemoryValue::F252(P_MIN_1));
memory_builder.set(fp + 2, MemoryValue::F252(P_MIN_2));
let trace_entry = relocated_trace_entry!(ap as usize, fp as usize, pc as usize);
let casm_states_by_opcode =
CasmStatesByOpcode::from_iter([trace_entry].into_iter(), &memory_builder);
assert_eq!(casm_states_by_opcode.add_opcode_small.len(), 1);|
Previously, ohad-agadi (Ohad) wrote…
I take that back |
592a940 to
ab90194
Compare
There was a problem hiding this comment.
Reviewable status: 1 of 4 files reviewed, 4 unresolved discussions (waiting on @DavidLevitGurevich and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 17 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
u128 probably shouldnt appear anywhere in this context
the bounds should either be defined by [u32;8], or be projected to a range (טווח) that makes sense - in the small add case that is i32
But small values are defined as u128, I want to put a bound that speaks the same language. Why to have an extra casting?
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 700 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
I think you should delegate this to a function and test it specifically
what do you mean? It is already a separate function. added tests
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 707 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
I think you can delete, the 3rd case should cover every possible value
If small values can be stored in F252 (as you said can happen), it won't catch it (for example, zero).
If you promise that small values are in MemoryValue::Small, it can be deleted.
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 718 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
name the two variables
which ? val_be.clone().cmp(p_min_2_to_27_be) ? this ? How?
There was a problem hiding this comment.
Reviewable status: 1 of 4 files reviewed, 4 unresolved discussions (waiting on @anatgstarkware, @DavidLevitGurevich, and @Stavbe)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 17 at r2 (raw file):
Previously, Stavbe wrote…
But small values are defined as u128, I want to put a bound that speaks the same language. Why to have an extra casting?
because the u128 is implementation and not API
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 700 at r2 (raw file):
Previously, Stavbe wrote…
what do you mean? It is already a separate function. added tests
you're testing the sorting, I want to specifically check values
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 707 at r2 (raw file):
Previously, Stavbe wrote…
If small values can be stored in F252 (as you said can happen), it won't catch it (for example, zero).
If you promise that small values are in MemoryValue::Small, it can be deleted.
can you give an example?
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 718 at r2 (raw file):
Previously, Stavbe wrote…
which ? val_be.clone().cmp(p_min_2_to_27_be) ? this ? How?
yes
There was a problem hiding this comment.
Reviewable status: 1 of 4 files reviewed, 4 unresolved discussions (waiting on @anatgstarkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 17 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
because the u128 is implementation and not API
This const is also an implementation and not an API. It will add to the code about 20 "as u128".
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 700 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
you're testing the sorting, I want to specifically check values
I added test, please take a look
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 707 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
can you give an example?
for example, zero.
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 718 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
yes
I don't have a good idea how to call it, so please suggest
There was a problem hiding this comment.
Reviewable status: 1 of 4 files reviewed, 2 unresolved discussions (waiting on @anatgstarkware, @DavidLevitGurevich, and @Stavbe)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 17 at r2 (raw file):
Previously, Stavbe wrote…
This const is also an implementation and not an API. It will add to the code about 20 "as u128".
can you define it above the is_small_add function?
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 707 at r2 (raw file):
Previously, Stavbe wrote…
for example, zero.
your test pass on zero
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 718 at r2 (raw file):
Previously, Stavbe wrote…
I don't have a good idea how to call it, so please suggest
ok
ab90194 to
5a13821
Compare
There was a problem hiding this comment.
Reviewable status: 1 of 4 files reviewed, 2 unresolved discussions (waiting on @anatgstarkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 17 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
can you define it above the is_small_add function?
Done.
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 707 at r2 (raw file):
Previously, ohad-agadi (Ohad) wrote…
your test pass on zero
Done.
5a13821 to
2d64b05
Compare
There was a problem hiding this comment.
Reviewable status: 1 of 4 files reviewed, 1 unresolved discussion (waiting on @anatgstarkware, @az-starkware, and @DavidLevitGurevich)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 703 at r4 (raw file):
match felt252[4..8] { // If the value is small, it can only fit in the positive range. [0, 0, 0, 0] => limbs_to_u128(felt252[0..4].try_into().unwrap()) <= SMALL_ADD_MAX_VALUE,
im not sure this is correct
what happens when there are 5 limbs?
ebf0af6 to
b24bcc0
Compare
There was a problem hiding this comment.
Reviewable status: 1 of 6 files reviewed, 1 unresolved discussion (waiting on @anatgstarkware, @az-starkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 703 at r4 (raw file):
Previously, ohad-agadi (Ohad) wrote…
im not sure this is correct
what happens when there are 5 limbs?
If it's positive, it is for sure not less than 2**27-1
If it's negative, go to the other match
Anyway, changed for more clear implementation
There was a problem hiding this comment.
Reviewable status: 1 of 6 files reviewed, 3 unresolved discussions (waiting on @anatgstarkware, @az-starkware, and @DavidLevitGurevich)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 703 at r4 (raw file):
Previously, Stavbe wrote…
If it's positive, it is for sure not less than 2**27-1
If it's negative, go to the other matchAnyway, changed for more clear implementation
alright
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 699 at r6 (raw file):
.flat_map(|&x| x.to_le_bytes()) .collect::<Vec<_>>(), )
that's a malloc for every value , n_add_steps * 3 :(
try using bytemuck::cast if the unsafe scares u
Suggestion:
U256::from_little_endian(
unsafe{transmute(arr.map(u32::to_le_bytes))}
)stwo_cairo_prover/crates/adapter/src/opcodes.rs line 707 at r6 (raw file):
let value = u256_from_le_array(val.as_u256()); let postive_upper_bound = U256::from(2_u128.pow(27) - 1); let negative_upper_bound = u256_from_le_array(P_MIN_1);
can these be consts? sorry not checking myself bad reception in train
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 772 at r6 (raw file):
#[test] fn test_is_small_add() { let postive_upper_bound = 2_u128.pow(27) - 1;
can you add tests for values in [0, positive_upper_bound) that are F252
I know it's trivial it works because you call to_u256 but implementation might change
There was a problem hiding this comment.
Reviewable status: 1 of 6 files reviewed, 3 unresolved discussions (waiting on @anatgstarkware, @az-starkware, @DavidLevitGurevich, and @Stavbe)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 699 at r6 (raw file):
Previously, ohad-agadi (Ohad) wrote…
that's a malloc for every value , n_add_steps * 3 :(
try using bytemuck::cast if the unsafe scares u
but it really is safe so consider using that favorably
4caecbe to
79f781c
Compare
There was a problem hiding this comment.
Reviewable status: 1 of 6 files reviewed, 3 unresolved discussions (waiting on @anatgstarkware, @az-starkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 699 at r6 (raw file):
Previously, ohad-agadi (Ohad) wrote…
but it really is safe so consider using that favorably
no malloc + safe
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 707 at r6 (raw file):
Previously, ohad-agadi (Ohad) wrote…
can these be consts? sorry not checking myself bad reception in train
Done.
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 772 at r6 (raw file):
Previously, ohad-agadi (Ohad) wrote…
can you add tests for values in [0, positive_upper_bound) that are F252
I know it's trivial it works because you call to_u256 but implementation might change
Done.
|
Previously, Stavbe wrote…
I meant the U256 |
There was a problem hiding this comment.
Maybe we shouldn't introduce primitive_types::U256, starknet-ff uses crypto_bigint::U256.
We can do this without going to u256 at all, work only with the reduced form (like we do in the air).
If you want starknet-ff functionality, please see impl From<Felt252> for FieldElement in cpu.rs and the comment above it.
Please consult @dancarmoz
Reviewable status: 1 of 6 files reviewed, 2 unresolved discussions (waiting on @az-starkware, @DavidLevitGurevich, and @ohad-agadi)
79f781c to
5852b3b
Compare
c58d1eb to
f7ff8d5
Compare
There was a problem hiding this comment.
Reviewed 2 of 3 files at r8, all commit messages.
Reviewable status: 5 of 7 files reviewed, 1 unresolved discussion (waiting on @az-starkware and @DavidLevitGurevich)
stwo_cairo_verifier/asdf-vm line 1 at r10 (raw file):
Subproject commit d536803b6f20b8d031e5e9173f6fdc82380ba5c1
?
f7ff8d5 to
36e1f67
Compare
There was a problem hiding this comment.
Reviewable status: 5 of 7 files reviewed, 1 unresolved discussion (waiting on @az-starkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_verifier/asdf-vm line 1 at r10 (raw file):
Previously, ohad-agadi (Ohad) wrote…
?
Done.
|
Don't we need parentheses? Suggestion: (value >= SMALL_ADD_NEGATIVE_LOWER_BOUND && value <= SMALL_ADD_NEGATIVE_UPPER_BOUND) |
There was a problem hiding this comment.
Reviewable status: 5 of 7 files reviewed, 1 unresolved discussion (waiting on @anatgstarkware, @az-starkware, and @DavidLevitGurevich)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 725 at r11 (raw file):
Previously, anatgstarkware (anatg) wrote…
Don't we need parentheses?
I believe anat is correct, can we have a test for this (not the entire is_small_add_function)?
and test a value in every range and also the boundaries
36e1f67 to
96346d5
Compare
There was a problem hiding this comment.
Reviewable status: 5 of 7 files reviewed, 1 unresolved discussion (waiting on @anatgstarkware, @az-starkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 725 at r11 (raw file):
Previously, ohad-agadi (Ohad) wrote…
I believe anat is correct, can we have a test for this (not the entire is_small_add_function)?
and test a value in every range and also the boundaries
No need, but added for clarity.
There are already tests for all the cases.
Actually, the checking: value <= SMALL_ADD_NEGATIVE_UPPER_BOUND, checks that we are in the reduced form, but the AIR allows values that are not reduced. So maybe I need to relax it and change upper bound = P + 2**27 -1, WDYT?
There was a problem hiding this comment.
Reviewable status: 5 of 7 files reviewed, 1 unresolved discussion (waiting on @anatgstarkware, @az-starkware, @DavidLevitGurevich, and @Stavbe)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 725 at r11 (raw file):
Previously, Stavbe wrote…
No need, but added for clarity.
There are already tests for all the cases.Actually, the checking: value <= SMALL_ADD_NEGATIVE_UPPER_BOUND, checks that we are in the reduced form, but the AIR allows values that are not reduced. So maybe I need to relax it and change upper bound = P + 2**27 -1, WDYT?
so you need to add something like:
|| (value >= SMALL_ADD_NEGATIVE_LOWER_BOUND + P && value <= SMALL_ADD_NEGATIVE_UPPER_BOUND + P)?
There was a problem hiding this comment.
Reviewable status: 5 of 7 files reviewed, 1 unresolved discussion (waiting on @anatgstarkware, @az-starkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 725 at r11 (raw file):
Previously, ohad-agadi (Ohad) wrote…
so you need to add something like:
|| (value >= SMALL_ADD_NEGATIVE_LOWER_BOUND + P && value <= SMALL_ADD_NEGATIVE_UPPER_BOUND + P)?
No. It's not linear. The lower bound is the same. The upper bound will be changed from P-1 to P + 2**27 + 1, but I am not sure it is needed since the honest prover assumed to fill the trace with the reduced form.
There was a problem hiding this comment.
Reviewable status: 5 of 7 files reviewed, 1 unresolved discussion (waiting on @az-starkware and @DavidLevitGurevich)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 725 at r11 (raw file):
Previously, Stavbe wrote…
No. It's not linear. The lower bound is the same. The upper bound will be changed from P-1 to P + 2**27 + 1, but I am not sure it is needed since the honest prover assumed to fill the trace with the reduced form.
|
Previously, ohad-agadi (Ohad) wrote…This is a completeness issue. It is fine to increase the upper bound as Stav suggested |
There was a problem hiding this comment.
Reviewable status: 5 of 7 files reviewed, 3 unresolved discussions (waiting on @az-starkware and @DavidLevitGurevich)
stwo_cairo_prover/crates/adapter/src/memory.rs line 11 at r12 (raw file):
/// P-2**27 in F252 format. pub const P_MIN_2_TO_27: [u32; 8] = [
Can we move to the tests?
Code quote:
P_MIN_2_TO_27stwo_cairo_prover/crates/adapter/src/opcodes.rs line 702 at r12 (raw file):
} // 2^27
Suggestion:
// 2^27 - 1|
Please separate this test into the three ranges |
There was a problem hiding this comment.
Reviewable status: 5 of 7 files reviewed, 3 unresolved discussions (waiting on @az-starkware, @DavidLevitGurevich, and @Stavbe)
2663321 to
9d243ed
Compare
There was a problem hiding this comment.
Reviewable status: 4 of 7 files reviewed, 1 unresolved discussion (waiting on @anatgstarkware, @az-starkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/opcodes.rs line 785 at r12 (raw file):
Previously, anatgstarkware (anatg) wrote…
Please separate this test into the three ranges
Done.
There was a problem hiding this comment.
Reviewable status: 4 of 7 files reviewed, 1 unresolved discussion (waiting on @az-starkware, @DavidLevitGurevich, and @ohad-agadi)
stwo_cairo_prover/crates/adapter/src/memory.rs line 10 at r13 (raw file):
use tracing::{span, Level}; /// Prime 2^251 + 17 * 2^192 + 1 in little endian.
Why was that deleted?
There was a problem hiding this comment.
Reviewed 2 of 3 files at r3, 2 of 3 files at r8, 1 of 1 files at r11, 2 of 2 files at r13, all commit messages.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @DavidLevitGurevich and @Stavbe)
9d243ed to
cf2120d
Compare
There was a problem hiding this comment.
Reviewable status: 6 of 7 files reviewed, 1 unresolved discussion (waiting on @az-starkware and @DavidLevitGurevich)
stwo_cairo_prover/crates/adapter/src/memory.rs line 10 at r14 (raw file):
use tracing::{span, Level}; /// Prime 2^251 + 17 * 2^192 in little endian.
Suggestion:
Prime minus one 2^251 + 17 * 2^192 in little endian|
same below |
|
Previously, anatgstarkware (anatg) wrote…
Please keep the line between constants |
cf2120d to
83e5720
Compare
There was a problem hiding this comment.
Reviewable status: 6 of 7 files reviewed, all discussions resolved (waiting on @az-starkware and @DavidLevitGurevich)
stwo_cairo_prover/crates/adapter/src/memory.rs line 10 at r13 (raw file):
Previously, anatgstarkware (anatg) wrote…
Why was that deleted?
because it was not true. Fixed.
There was a problem hiding this comment.
Reviewable status: 6 of 7 files reviewed, all discussions resolved (waiting on @az-starkware and @DavidLevitGurevich)
There was a problem hiding this comment.
Reviewed 1 of 1 files at r15, all commit messages.
Reviewable status:complete! all files reviewed, all discussions resolved (waiting on @DavidLevitGurevich)
This change is