fix(ssa): Check cast bit size when fetching the max num bits for a value #4699
Conversation
Changes to circuit sizes
🧾 Summary (10% most significant diffs)
Full diff report 👇
|
| @@ -178,7 +178,7 @@ impl Binary { | |||
| let non_constant = if lhs.is_some() { self.rhs } else { self.lhs }; | |||
| if let Some(constant) = constant { | |||
| let max_possible_value = | |||
| 2u128.pow(dfg.get_value_max_num_bits(non_constant)) - 1; | |||
| 2u128.pow(dfg.type_of_value(non_constant).bit_size()) - 1; | |||
There was a problem hiding this comment.
There is actually two issues. The Cast logic was incorrect and also that in #4691 we should be checking against the bit_size of the variable's type. According to the comments for get_value_max_num_bits it is attempting to the following, which is not what we want:
Returns the maximum possible number of bits that `value` can potentially be
There was a problem hiding this comment.
I'll pull this out into its own fix and we can wait for @TomAFrench to take a look at the Cast fix as those are his changes.
There was a problem hiding this comment.
Can you explain why we should make this change? The motivation for the current implementation is that get_value_max_num_bits will return the max number of bits which value can take, i.e. non_constant < 2^max_bits. This allows us to reason how about when the constant is greater than this upper bound then it's impossible for the equality to hold.
This relies on casts up from a smaller type as otherwise the constant will always be less than the max potential value of the variable.
There was a problem hiding this comment.
This relies on casts up from a smaller type as otherwise the constant will always be less than the max potential value of the variable.
Ok I understand thank you for elaborating. I was thinking that using get_value_max_num_bits was a typo due to the comments above about variable types. I can update those to discuss that we want to check how for casts from a lower type as well as bringing usage back of get_value_max_num_bits.
…formation (#4700) # Description ## Problem\* No issue as this was found by @jfecher while testing in debug mode where we get overflow errors after #4691 Resolves #4699 (comment) ## Summary\* ## Additional Context ## Documentation\* Check one: - [ ] No documentation needed. - [ ] Documentation included in this PR. - [ ] **[For Experimental Features]** Documentation to be submitted in a separate PR. # PR Checklist\* - [ ] I have tested the changes locally. - [ ] I have formatted the changes with [Prettier](https://prettier.io/) and/or `cargo fmt` on default settings. --------- Co-authored-by: Tom French <tom@tomfren.ch>
…formation (#4700) # Description ## Problem\* No issue as this was found by @jfecher while testing in debug mode where we get overflow errors after #4691 Resolves #4699 (comment) ## Summary\* ## Additional Context ## Documentation\* Check one: - [ ] No documentation needed. - [ ] Documentation included in this PR. - [ ] **[For Experimental Features]** Documentation to be submitted in a separate PR. # PR Checklist\* - [ ] I have tested the changes locally. - [ ] I have formatted the changes with [Prettier](https://prettier.io/) and/or `cargo fmt` on default settings. --------- Co-authored-by: Tom French <tom@tomfren.ch>
Description
Problem*
No issue as this was found by @jfecher while testing in debug mode so pushed a quick fix
Summary*
We check for
Castinstructions inget_value_max_num_bitsas per this PR (#4039) in order to determine a more restrictive upper bound on values. However, if we cast from a larger data type we are returning the larger bit size.Additional Context
Documentation*
Check one:
PR Checklist*
cargo fmton default settings.