def Cryptlib.Util.Nat.Nat.toUInt32Words (words val : Nat) (out : Array UInt32 := #[]) : Array UInt32

Equations

• Cryptlib.Util.Nat.Nat.toUInt32Words 0 val out = out
• Cryptlib.Util.Nat.Nat.toUInt32Words words_2.succ val out = Cryptlib.Util.Nat.Nat.toUInt32Words words_2 (val >>> 32) (out.push (UInt32.ofNat val))

@[irreducible]

def Cryptlib.Util.Nat.Nat.fromUInt32Words (x : Subarray UInt32) (i out : Nat := 0) : Nat

Equations

• Cryptlib.Util.Nat.Nat.fromUInt32Words x i out = if i < Std.Slice.size x then Cryptlib.Util.Nat.Nat.fromUInt32Words x (i + 1) (out <<< 32 ||| x[Std.Slice.size x - i - 1]!.toNat) else out

def Cryptlib.Util.Nat.Nat.toUInt64Words (words val : Nat) (out : Array UInt64 := #[]) : Array UInt64

Equations

• Cryptlib.Util.Nat.Nat.toUInt64Words 0 val out = out
• Cryptlib.Util.Nat.Nat.toUInt64Words words_2.succ val out = Cryptlib.Util.Nat.Nat.toUInt64Words words_2 (val >>> 64) (out.push (UInt64.ofNat val))

@[irreducible]

def Cryptlib.Util.Nat.Nat.fromUInt64Words (x : Subarray UInt64) (i out : Nat := 0) : Nat

Equations

• Cryptlib.Util.Nat.Nat.fromUInt64Words x i out = if i < Std.Slice.size x then Cryptlib.Util.Nat.Nat.fromUInt64Words x (i + 1) (out <<< 64 ||| x[Std.Slice.size x - i - 1]!.toNat) else out

partial def Cryptlib.Util.Nat.Nat.log2_ceil (value : Nat) (result : Nat := 0) : Nat

partial def Cryptlib.Util.Nat.Nat.log2_floor (value : Nat) (result : Nat := 0) : Nat