def sqrt_iter {n : Nat} (i : Nat) (x w : BitVec n) : BitVec (n + 1)

Implementation of integer square root. Remainder bit appended to the end of the result.

Equations

• One or more equations did not get rendered due to their size.

def bit_sqrt {n : Nat} (x : BitVec n) : BitVec (n + 1)

Equations

• bit_sqrt x = sqrt_iter ((n - 1) / 2) x 0

def sqrt_impl {e s : Nat} (x : PackedFloat e s) (m : RoundingMode) : PackedFloat e s

Equations

• One or more equations did not get rendered due to their size.

def sqrt {e s : Nat} (x : PackedFloat e s) (m : RoundingMode) : PackedFloat e s

Equations

• sqrt x m = if x.isZero = true then x else if (x.sign || x.isNaN) = true then PackedFloat.getNaN e s else if x.isInfinite = true then PackedFloat.getInfinity e s false else sqrt_impl x m

theorem square_sqrt_is_id (x : BitVec 5) : bit_sqrt (BitVec.setWidth 10 x * BitVec.setWidth 10 x) = BitVec.setWidth (10 + 1) x <<< 1