def Cryptlib.Util.UInt32.UInt32.test_bit (bit : Nat) (x : UInt32) : Bool

Equations

• Cryptlib.Util.UInt32.UInt32.test_bit bit x = ((1 <<< bit).toUInt32 &&& x != 0)

def Cryptlib.Util.UInt32.UInt32.swap_endian (x : UInt32) : UInt32

Equations

• Cryptlib.Util.UInt32.UInt32.swap_endian x = x >>> (8 * 3) &&& 255 ||| (x >>> (8 * 2) &&& 255) <<< (8 * 1) ||| (x >>> (8 * 1) &&& 255) <<< (8 * 2) ||| (x &&& 255) <<< (8 * 3)

def Cryptlib.Util.UInt32.UInt32.ror (x : UInt32) (n : Nat) : UInt32

Equations

• Cryptlib.Util.UInt32.UInt32.ror x n = x >>> UInt32.ofNat n ||| x <<< UInt32.ofNat (32 - n)

def Cryptlib.Util.UInt32.UInt32.of_be32 (b3 b2 b1 b0 : UInt8) : UInt32

Equations

• Cryptlib.Util.UInt32.UInt32.of_be32 b3 b2 b1 b0 = UInt32.ofNat b3.toNat <<< (8 * 3) ||| UInt32.ofNat b2.toNat <<< (8 * 2) ||| UInt32.ofNat b1.toNat <<< (8 * 1) ||| UInt32.ofNat b0.toNat

def Cryptlib.Util.UInt32.UInt32.to_le (x : UInt32) : ByteArray

Equations

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

def Cryptlib.Util.UInt32.UInt32.to_be (x : UInt32) : ByteArray

Equations

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