The proof for Babylonian square root algorithm in audit report is wrong

[yonggewang]

The proof for Babylonian square root algorithm in audit report is wrong https://uniswap.org/audit.html

[moodysalem]

@yonggewang can you elaborate? does the code not match the proof?

[yonggewang]

mathematical claim in the audit report is wrong. the code may produce results not as claimed in the audit report

[moodysalem]

I'm not sure what is meant by 'wrong', can you be specific about what part of the proof is incorrect?

[yonggewang]

too complicated to describe details here. The last two lines of the proof has a wrong argument. after one shows that a >b.. the value of b is not necessarily the largest value below b. It can be anything below b

The last formula has typo in it. but that is not main issue there. In the last formula, you have an extra Z_{N-1} which is a ghost. I do not see where it comes from. But you can just drop that without any issue. So that is a typo only I assume

[zawy12]

Max N for y<=2^x for odd x appears to be N = (x+1)/2+ floor(log((x+1)/2)/log(2)) giving N=135 and 136 for x=255 and 257.

[moodysalem]

@livnev do these comments make sense to you?

[zawy12]

For my part, I'm only saying that I have an equation that may help derive the guess of N=135 that's in the proof as opposed to settling for N<255.

[yonggewang]

the best practice for Babylonian's algorithm is to have a few extra digits (or a few bits in binary case)... e.g., if we want the accuracy for all digits on the left hand side of the fractional point, it is better to have one extra digit on the right hand side of the fractional point during the iteration. This could be proved easily. But the "proof" in the audit report seems to be faulty and cannot prove this fact (even if we keep several extra bits during iteration).

So assume zawy12's comments are talking about the same thing (extra bits beyond required accuracy). thanks!