Function vstd::arithmetic::logarithm::log

source · 
pub open spec fn log(base: int, pow: int) -> int
Expand description
recommends
base > 1,
pow >= 0,
{
    if pow < base || pow / base >= pow || pow / base < 0 {
        0
    } else {
        1 + log(base, pow / base)
    }
}

This function recursively defines the integer logarithm. It’s only meaningful when the base of the logarithm base is greater than 1, and when the value whose logarithm is taken, pow, is non-negative.