8000 Verify and fix the `U256::mul_u64` method by tcharding · Pull Request #1496 · rust-bitcoin/rust-bitcoin · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Verify and fix the U256::mul_u64 method #1496

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Dec 30, 2022
Merged

Verify and fix the U256::mul_u64 method #1496

merged 1 commit into from
Dec 30, 2022

Conversation

tcharding
Copy link
Member
@tcharding tcharding commented Dec 21, 2022 •
edited
Loading

Add kani verification for U256::mul_u64, doing so uncovered a bug in the current implementation due to overflow. Re-write the mul_u64 method.

Fix: #1497

Note

This PR now only tests mul_u64, I will add testing div as a separate PR.

@tcharding tcharding mentioned this pull request Dec 21, 2022
Merged
@tcharding tcharding force-pushed the 22-12-pow-kani-mul-div branch from 5530402 to c1997a0 Compare December 21, 2022 21:44
@Kixunil
Copy link
Collaborator
Kixunil commented Dec 22, 2022

I think it'd be more useful if you also checked (x * y) / y == x

@Kixunil
Copy link
Collaborator
Kixunil commented Dec 22, 2022

Oh, it found a bug, that's kinda cool!

@Kixunil Kixunil mentioned this pull request Dec 22, 2022
Closed
@tcharding tcharding force-pushed the 22-12-pow-kani-mul-div branch 2 times, most recently from 0edb0d5 to 56bec1a Compare December 27, 2022 00:27
@tcharding
Copy link
Member Author

Please ignore all the pushes, I was on the wrong branch.

@tcharding tcharding force-pushed the 22-12-pow-kani-mul-div branch from 56bec1a to 73993c6 Compare December 27, 2022 04:03
@tcharding tcharding changed the title Add two basic kani tests to pow Add kani verification to the U256::mul_u64 method Dec 27, 2022
@tcharding tcharding changed the title Add kani verification to the U256::mul_u64 method Verify and fix the U256::mul_u64 method Dec 27, 2022
@tcharding
Copy link
Member Author

Force push is total re-write, PR description has been updated.

@tcharding tcharding force-pushed the 22-12-pow-kani-mul-div branch 2 times, most recently from cf0cb81 to 9dd9682 Compare December 27, 2022 04:14
@tcharding
Copy link
Member Author

I don't rekon we should be running kani on every PR - it takes too long.

@elichai
Copy link
Member
elichai commented Dec 27, 2022 •
edited
Loading

Can I propose this implementation instead? It's very straight forward:

fn mul_u64(self, rhs: u64) -> (U256, bool) {
    let mut carry: u128 = 0;
    let mut splitted_le = [self.1 as u64, (self.1 >> 64) as u64, self.0 as u64, (self.0 >> 64) as u64];
    for word in &mut splitted_le {
        // TODO: Use `carrying_mul` when stabilized: https://github.com/rust-lang/rust/issues/85532
        let n = carry + (rhs as u128) * (*word as u128);
        *word = n as u64;
        carry = (n >> 64) as u128;
    }
    let low = splitted_le[0] as u128 | (splitted_le[1] as u128) << 64;
    let high = splitted_le[2] as u128 | (splitted_le[3] as u128) << 64;
    (Self(high, low), carry != 0)
}

@Kixunil
Copy link
Collaborator
Kixunil commented Dec 27, 2022

Yeah, @elichai's impl looks better, ACK that one but I want all non-truncated casts to be changed to use u128::from() and add a comment that all truncating casts are intentional and correct. I've also manually iterated the algorithm for largest possible value to check that + doesn't overflow, so maybe add a comment about that too.

@elichai
Copy link
Member
elichai commented Dec 27, 2022

Yeah, @elichai's impl looks better, ACK that one but I want all non-truncated casts to be changed to use u128::from() and add a comment that all truncating casts are intentional and correct. I've also manually iterated the algorithm for largest possible value to check that + doesn't overflow, so maybe add a comment about that too.

It can't overflow because 2 bitwise multiplications of b bits can never reach 2^b-1. (for intuition, let's think of base 10, it's obvious there are no single-digit numbers that when multiplied can reach 99, you can also look at u3 where u3::MAX=7(0b111) and 7*7 = 49(0b110001) which is less than u6::MAX=63=0b111111))

@Kixunil
Copy link
Collaborator
Kixunil commented Dec 27, 2022

It can't overflow because 2 bitwise multiplications of b bits can never reach 2^b-1

I think you meant to say "2 bitwise multiplications of b bits can never reach 2^(2*b)-1", anyway this part was immediately obvious to me. The less obvious part is 2 multiplications with previous carry added not overflowing the same bound.

@elichai
Copy link
Member
elichai commented Dec 27, 2022 •
edited
Loading

It can't overflow because 2 bitwise multiplications of b bits can never reach 2^b-1

I think you meant to say "2 bitwise multiplications of b bits can never reach 2^(2*b)-1", anyway this part was immediately obvious to me. The less obvious part is 2 multiplications with previous carry added not overflowing the same bound.

Right, I'm sorry, I'll try again:

∀ a,c ∈ ℤ ∩ [0, 2^b - 1] : a*c ≤ (2^b-1)^2 = 2^{2b} - 2^{b+1} + 1
and because an integer with 2b bits is in the range ℤ ∩ [0, 2^{2b}-1] then we have 2^{2b}-1 - (2^{2b} - 2^{b+1} + 1) = 2^{b+1} - 2 free space, and ∀ b ∈ ℤ, b > 1 we get 2^b ≤ 2^{b+1} - 2 (this last statement can be easily proven via induction)

Which means we can safely add another 2^b integer into the 2^{2b} multiplication result

@Kixunil
Copy link
Collaborator
Kixunil commented Dec 27, 2022

OK, I guess a comment linking to your very nice proof is even better then. :) Thanks!

@elichai
Copy link
Member
elichai commented Dec 27, 2022

OK, I guess a comment linking to your very nice proof is even better then. :) Thanks!

Doing a math degree does come in handy here and there 😜

@tcharding tcharding force-pushed the 22-12-pow-kani-mul-div branch 2 times, most recently from 0034749 to fd35efd Compare December 27, 2022 23:50
@tcharding
Copy link
Member Author

Thanks @elichai, mad geek props to you!

@tcharding
Copy link
Member Author

Needs #1508 to pass CI.

elichai
elichai previously approved these changes Dec 28, 2022
View reviewed changes
Copy link
Member
@elichai elichai left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ACK

Kixunil
Kixunil previously approved these changes Dec 28, 2022
View reviewed changes
Copy link
Collaborator
@Kixunil Kixunil left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ACK fd35efd796a1452eabad6417d08ff766a92e2e5f

bitcoin/src/pow.rs
(upper, lower)
}
let mut carry: u128 = 0;
let mut split_le = [self.1 as u64, (self.1 >> 64) as u64, self.0 as u64, (self.0 >> 64) as u64];
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is missing a comment about intentional truncation but maybe it's obvious enough from variable name.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah I tried using buf as the name and adding a comment but I think its clean like it is.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I find split_le more clear than buf.

@tcharding tcharding dismissed stale reviews from Kixunil and elichai via b138218 December 29, 2022 00:30
@tcharding tcharding force-pushed the 22-12-pow-kani-mul-div branch from fd35efd to b138218 Compare December 29, 2022 00:30
@tcharding
Copy link
Member Author

Implemented kani::Arbitrary for U256 - there is some dark magic going on that I don't understand, implementing a type from a crate that we do not depend on. Does cargo kani modify the manifest before building?

@tcharding tcharding mentioned this pull request Dec 29, 2022
Merged
@tcharding
Copy link
Member Author

I don't know why kani is failing here?

@tcharding tcharding force-pushed the 22-12-pow-kani-mul-div branch 4 times, most recently from 4e677cb to 0e372c6 Compare December 29, 2022 22:39
@tcharding @elichai
Verify and fix mul_u64
cf9733d 
Add kani verification for `U256::mul_u64`, doing so uncovered a bug in
the current implementation due to overflow.

Re-write the `mul_u64` method.

Props to Elichai for the algorithm.

Co-authored-by: Elichai Turkel <elichai.turkel@gmail.com>
@tcharding tcharding force-pushed the 22-12-pow-kani-mul-div branch from 0e372c6 to cf9733d Compare December 29, 2022 22:39
@Kixunil
Copy link
Collaborator
Kixunil commented Dec 30, 2022

Does cargo kani modify the manifest before building?

Not sure if that or it calls rustc directly. But they do document that they inject the crate.

Kixunil
Kixunil approved these changes Dec 30, 2022
View reviewed changes
Copy link
Collaborator
@Kixunil Kixunil left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ACK cf9733d

apoelstra
apoelstra approved these changes Dec 30, 2022
View reviewed changes
Copy link
Member
@apoelstra apoelstra left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ACK cf9733d

@apoelstra apoelstra merged commit 2282027 into rust-bitcoin:master Dec 30, 2022
@tcharding tcharding deleted the 22-12-pow-kani-mul-div branch January 12, 2023 07:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Kixunil Kixunil Kixunil approved these changes

@apoelstra apoelstra apoelstra approved these changes

@elichai elichai elichai left review comments

Assignees
No one assigned
Labels
aggregate release notes mention Tests
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Overflow in pow::U256::mul_u64
4 participants
@tcharding @Kixunil @elichai @apoelstra
0