On 20/08/25 11:45, Harishankar Vishwanathan wrote:
This is nice work on improving the precision of the tnum_mul algorithm Nandakumar. I had a few questions and comments (below).
Thanks a lot for going through this seriously.
If I understand the idea correctly, when the multiplier's (i.e. tnum a) bit is unknown, it can either be 0 or 1. If it is 0, then we add nothing to accumulator, i.e. TNUM(0, 0). If it is 1, we can add b to the accumulator (appropriately shifted). The main idea is to take the union of these two possible partial products, and add that to the accumulator. If so, could we also do the following? acc = tnum_add(acc, tnum_union(TNUM(0, 0), b));
But tnum_union(TNUM(0, 0), b) would introduce a concrete 0 to the set, right?
The comments in your algorithm seem different from what the code implements: I believe the comment should read: /* acc = tnum_union(acc_0, acc_1), where acc_0 and ... */
Yes, thanks a lot for pointing out! Will fix in v3.
Finally, what is the guarantee that this algorithm is sound? It will be useful to have a proof to ensure that we are maintaining correctness.
Been working on it. Thank you, -- Nandakumar Edamana
