solidity: std math library

[VoR0220]

I've included a lot of basic functions...binomial is one that I'm currently trying to figure out but not being able to utilize a 2D array makes this more difficult.

[chriseth]

Can you combine than with the other math library? And perhaps we could use this sqrt function:

contract c {
    uint bla;
    /// @why3 ensures { to_int result * to_int result <= to_int arg_x < (to_int result + 1) * (to_int result + 1) }
    function sqrt(uint x) returns (uint y) {
        if (x == 0) return 0;
        else if (x <= 3) return 1;
        uint z = (x + 1) / 2;
        y = x;
        while (z < y)
        /// @why3 invariant { to_int !_z = div ((div (to_int arg_x) (to_int !_y)) + (to_int !_y)) 2 }
        /// @why3 invariant { to_int arg_x < (to_int !_y + 1) * (to_int !_y + 1) }
        /// @why3 invariant { to_int arg_x < (to_int !_z + 1) * (to_int !_z + 1) }
        /// @why3 variant { to_int !_y }
        {
            y = z;
            z = (x / z + z) / 2;
        }
    }
}

[VoR0220]

I can absolutely change the sqrt function, but what do you mean by combine with the other math library?

[chriseth]

This does not really behave as "infinity". What about uint_max? (also applies to the others)

[VoR0220]

After taking some time to understand how Infinity works in other languages, I think I'd agree here. Perhaps this fits better trying to make a global object in Solidity itself? Just shooting out ideas. Either way, point taken and I will update accordingly.

[chriseth]

Right, we might allow access to constant public variables at some point.

[alexvandesande]

I would like to include an example on the homestead site that uses a square root and to do it properly I'd love to include it as an example of importing a library.

Can we merge and deploy this to the live net?

[alexvandesande]

Also I'm curious about how this can calculate a square root, it's fascinating..

while (z < y) {
y = z;
z = (x / z + z) / 2;
}

edit: Found it. This is awesome!

[michael-spengler]

    function sqrt(uint256 x) public pure returns (uint256 y) {
        uint256 z = (x + 1) / 2;
        y = x;
        while (z < y) {
            y = z;
            z = (x / z + z) / 2;
        }
        return y;
    }

https://ethereum.stackexchange.com/a/2913/65406