Skip to content

Latest commit

 

History

History
378 lines (213 loc) · 7.99 KB

Math.md

File metadata and controls

378 lines (213 loc) · 7.99 KB
Raw

Module 0x1::Math

The module provide some improved math calculations.

use 0x1::Vector;

Constants

const U128_MAX: u128 = 340282366920938463463374607431768211455;


const U64_MAX: u64 = 18446744073709551615;

Function u64_max

u64::MAX

public fun u64_max(): u64
Implementation 
public fun u64_max(): u64 {
    U64_MAX
}

Function u128_max

u128::MAX

public fun u128_max(): u128
Implementation 
public fun u128_max(): u128 {
    U128_MAX
}

Function sqrt

babylonian method (https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Babylonian_method)

public fun sqrt(y: u128): u64
Implementation 
public fun sqrt(y: u128): u64 {
    if (y < 4) {
        if (y == 0) {
            0u64
        } else {
            1u64
        }
    } else {
        let z = y;
        let x = y / 2 + 1;
        while (x < z) {
            z = x;
            x = (y / x + x) / 2;
        };
        (z as u64)
    }
}
Specification 
pragma opaque = true;
pragma verify = false;
aborts_if [abstract] false;
ensures [abstract] result == spec_sqrt();

We use an uninterpreted function to represent the result of sqrt. The actual value does not matter for the verification of callers.

fun spec_sqrt(): u128;

Function pow

calculate the y pow of x.

public fun pow(x: u64, y: u64): u128
Implementation 
public fun pow(x: u64, y: u64): u128 {
    let result = 1u128;
    let z = y;
    let u = (x as u128);
    while (z > 0) {
        if (z % 2 == 1) {
            result = (u * result as u128);
        };
        u = (u * u as u128);
        z = z / 2;
    };
    result
}
Specification 
pragma opaque = true;
pragma verify = false;
aborts_if [abstract] false;
ensures [abstract] result == spec_pow();

We use an uninterpreted function to represent the result of pow. The actual value does not matter for the verification of callers.

fun spec_pow(): u128;

Function mul_div

https://medium.com/coinmonks/math-in-solidity-part-3-percents-and-proportions-4db014e080b1 calculate x * y /z with as little loss of precision as possible and avoid overflow

public fun mul_div(x: u128, y: u128, z: u128): u128
Implementation 
public fun mul_div(x: u128, y: u128, z: u128): u128 {
    if (y == z) {
        return x
    };
    if (x == z) {
        return y
    };
    let a = x / z;
    let b = x % z;
    //x = a * z + b;
    let c = y / z;
    let d = y % z;
    //y = c * z + d;
    a * c * z + a * d + b * c + b * d / z
}
Specification 
pragma opaque = true;
include MulDivAbortsIf;
aborts_if [abstract] false;
ensures [abstract] result == spec_mul_div();


schema MulDivAbortsIf {
    x: u128;
    y: u128;
    z: u128;
    aborts_if y != z && x > z && z == 0;
    aborts_if y != z && x > z && z!=0 && x/z*y > MAX_U128;
    aborts_if y != z && x <= z && z == 0;
    aborts_if y != z && x <= z && x / z * (x % z) > MAX_U128;
    aborts_if y != z && x <= z && x / z * (x % z) * z > MAX_U128;
    aborts_if y != z && x <= z && x / z * (y % z) > MAX_U128;
    aborts_if y != z && x <= z && x / z * (x % z) * z + x / z * (y % z) > MAX_U128;
    aborts_if y != z && x <= z && x % z * (y / z) > MAX_U128;
    aborts_if y != z && x <= z && x % z * (y % z) > MAX_U128;
    aborts_if y != z && x <= z && x % z * (y % z) / z > MAX_U128;
    aborts_if y != z && x <= z && x / z * (x % z) * z + x / z * (y % z) + x % z * (y / z) > MAX_U128;
    aborts_if y != z && x <= z && x / z * (x % z) * z + x / z * (y % z) + x % z * (y / z) + x % z * (y % z) / z > MAX_U128;
}


fun spec_mul_div(): u128;

Function sum

calculate sum of nums

public fun sum(nums: &vector<u128>): u128
Implementation 
public fun sum(nums: &vector<u128>): u128 {
    let len = Vector::length(nums);
    let i = 0;
    let sum = 0;
    while (i < len){
        sum = sum + *Vector::borrow(nums, i);
        i = i + 1;
    };
    sum
}

Function avg

calculate average of nums

public fun avg(nums: &vector<u128>): u128
Implementation 
public fun avg(nums: &vector<u128>): u128{
    let len = Vector::length(nums);
    let sum = sum(nums);
    sum/(len as u128)
}

Module Specification

pragma verify = false;
pragma aborts_if_is_strict;