Unchecked Multiplication checks performance bottleneck

[rajathkotyal]

Hello :)

I was solving the numeric primitive types challenge #59, For the multiplication harnesses (the unchecked_mul 128 bit) PR : #96 , the proofs are taking a long time and not fully completing. Based on my research, I feel this is because the state space for checking 128 bit integers is extremely large, i.e. there should be approx 2 ( 2 ^ 128 ) = 2 ^ 256 number of combinations that are valid for verification, which is practically not possible. Hence I have limited the ranges to search within. Do you think this is a feasible approach, or am I missing something?

Note : i32, u32, i64 and u64 could still be run. But it would at least take a couple hours to finish. Is that acceptable? Or do we have any performance constraints to adhere to. Do let me know.

Thank you!

[celinval]

Hi @rajathkotyal, I just wanted to make sure this answer in your PR has unblocked you. Thanks!

[rajathkotyal]

Hi @celinval . Yes it has. Thank you!

Closing this discussion.