bits

machine.Bits.half

def Bits.half (width : Nat) : Nat

Half the number of values of a width: 2^(width - 1), the magnitude of the most negative signed value.

machine.Bits.minSigned

def Bits.minSigned (width : Nat) : Int

The least signed value of a width: -2^(width - 1).

machine.Bits.maxSigned

def Bits.maxSigned (width : Nat) : Int

The greatest signed value of a width: 2^(width - 1) - 1.

machine.Bits.maxUnsigned

def Bits.maxUnsigned (width : Nat) : Int

The greatest unsigned value of a width: 2^width - 1.

machine.Bits.unsignedOf

def Bits.unsignedOf (width : Nat) (v : Int) : Nat

The unsigned representation of v in a width: v modulo 2^width.

machine.Bits.wrapUnsigned

def Bits.wrapUnsigned (width : Nat) (v : Int) : Int

Wraps v into the unsigned range of a width.

machine.Bits.wrapSigned

def Bits.wrapSigned (width : Nat) (v : Int) : Int

Wraps v into the signed range of a width (two’s complement).

machine.Bits.and

def Bits.and (width : Nat) (x : Int) (y : Int) : Nat

Bitwise and of x and y in a width, as an unsigned representation.

machine.Bits.or

def Bits.or (width : Nat) (x : Int) (y : Int) : Nat

Bitwise or of x and y in a width, as an unsigned representation.

machine.Bits.xor

def Bits.xor (width : Nat) (x : Int) (y : Int) : Nat

Bitwise exclusive or of x and y in a width, as an unsigned representation.

machine.Bits.not

def Bits.not (width : Nat) (x : Int) : Nat

Bitwise complement of x in a width, as an unsigned representation: x exclusive or all ones.

machine.Bits.shiftLeft

def Bits.shiftLeft (x : Int) (k : Nat) : Int

Shifts left by k: x * 2^k (wrapping is the language’s choice).

machine.Bits.shiftRight

def Bits.shiftRight (x : Int) (k : Nat) : Int

Shifts x right by k bits, rounding toward negative infinity (an arithmetic shift).

machine.Bits.wrapUnsignedInRange

def Bits.wrapUnsignedInRange (width : Nat) (v : Int) : Bool.and (Int.ble (pos 0) (Bits.wrapUnsigned width v)) (Int.ble (Bits.wrapUnsigned width v) (Bits.maxUnsigned width)) = true

Wrapping v into the unsigned range of width lands in it: 0 <= wrapUnsigned width v <= 2^width - 1.

machine.Bits.wrapSignedInRange

def Bits.wrapSignedInRange (width : Nat) (v : Int) : Bool.and (Int.ble (Bits.minSigned width) (Bits.wrapSigned width v)) (Int.ble (Bits.wrapSigned width v) (Bits.maxSigned width)) = true

Wrapping v into the signed range of width lands in it: -2^(width-1) <= wrapSigned width v <= 2^(width-1) - 1.