class Sparkle.Data.BitPack.BitPack (α : Type u) (n : Nat) : Type u

BitPack type class: Proves a type α can be converted to/from a BitVec of width n.

This is essential for hardware synthesis, as all values must ultimately be representable as bit patterns.

Laws (not enforced, but expected):

• toBitVec (fromBitVec bv) = bv (round-trip property)
• fromBitVec (toBitVec x) = x (round-trip property)

• toBitVec : α → BitVec n
• fromBitVec : BitVec n → α

@[inline]

def Sparkle.Data.BitPack.BitPack.pack {α : Type u} {n : Nat} [BitPack α n] (x : α) : BitVec n

Convert a value to its bit vector representation

Equations

• Sparkle.Data.BitPack.BitPack.pack x = Sparkle.Data.BitPack.BitPack.toBitVec x

@[inline]

def Sparkle.Data.BitPack.BitPack.unpack {α : Type u} {n : Nat} [BitPack α n] (bv : BitVec n) : α

Convert a bit vector to its value representation

Equations

• Sparkle.Data.BitPack.BitPack.unpack bv = Sparkle.Data.BitPack.BitPack.fromBitVec bv

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackBoolOfNatNat : BitPack Bool 1

BitPack instance for Bool (1 bit)

Equations

• Sparkle.Data.BitPack.instBitPackBoolOfNatNat = { toBitVec := fun (b : Bool) => if b = true then 1#1 else 0#1, fromBitVec := fun (bv : BitVec 1) => bv != 0#1 }

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackBitVec {n : Nat} : BitPack (BitVec n) n

BitPack instance for BitVec n (identity mapping)

Equations

• Sparkle.Data.BitPack.instBitPackBitVec = { toBitVec := fun (bv : BitVec n) => bv, fromBitVec := fun (bv : BitVec n) => bv }

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackUnitOfNatNat : BitPack Unit 0

BitPack instance for Unit (0 bits)

Equations

• Sparkle.Data.BitPack.instBitPackUnitOfNatNat = { toBitVec := fun (x : Unit) => 0#0, fromBitVec := fun (x : BitVec 0) => () }

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackUInt8OfNatNat : BitPack UInt8 8

BitPack instance for UInt8 (8 bits)

Equations

• Sparkle.Data.BitPack.instBitPackUInt8OfNatNat = { toBitVec := fun (n : UInt8) => BitVec.ofNat 8 n.toNat, fromBitVec := fun (bv : BitVec 8) => UInt8.ofNat bv.toNat }

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackUInt16OfNatNat : BitPack UInt16 16

BitPack instance for UInt16 (16 bits)

Equations

• Sparkle.Data.BitPack.instBitPackUInt16OfNatNat = { toBitVec := fun (n : UInt16) => BitVec.ofNat 16 n.toNat, fromBitVec := fun (bv : BitVec 16) => UInt16.ofNat bv.toNat }

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackUInt32OfNatNat : BitPack UInt32 32

BitPack instance for UInt32 (32 bits)

Equations

• Sparkle.Data.BitPack.instBitPackUInt32OfNatNat = { toBitVec := fun (n : UInt32) => BitVec.ofNat 32 n.toNat, fromBitVec := fun (bv : BitVec 32) => UInt32.ofNat bv.toNat }

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackUInt64OfNatNat : BitPack UInt64 64

BitPack instance for UInt64 (64 bits)

Equations

• Sparkle.Data.BitPack.instBitPackUInt64OfNatNat = { toBitVec := fun (n : UInt64) => BitVec.ofNat 64 n.toNat, fromBitVec := fun (bv : BitVec 64) => UInt64.ofNat bv.toNat }

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackProdHAddNat {α β : Type u} {n m : Nat} [BitPack α n] [BitPack β m] : BitPack (α × β) (n + m)

BitPack instance for pairs (concatenate bit vectors)

Equations

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

def Sparkle.Data.BitPack.bitWidth (α : Type u) (n : Nat) [BitPack α n] : Nat

Helper to get the bit width of a type with BitPack instance

Equations

• Sparkle.Data.BitPack.bitWidth α n = n

def Sparkle.Data.BitPack.testRoundTrip {α : Type u} {n : Nat} [BitPack α n] [BEq α] (x : α) : Bool

Test if a value round-trips correctly through BitPack

Equations

• Sparkle.Data.BitPack.testRoundTrip x = (x == Sparkle.Data.BitPack.BitPack.fromBitVec (Sparkle.Data.BitPack.BitPack.toBitVec x))

structure Sparkle.Data.BitPack.RGB : Type

Example: RGB structure for demonstration

• r : BitVec 8
• g : BitVec 8
• b : BitVec 8

@[implicit_reducible]

instance Sparkle.Data.BitPack.instReprRGB : Repr RGB

Equations

• Sparkle.Data.BitPack.instReprRGB = { reprPrec := Sparkle.Data.BitPack.instReprRGB.repr }

def Sparkle.Data.BitPack.instReprRGB.repr : RGB → Nat → Std.Format

Equations

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

def Sparkle.Data.BitPack.instBEqRGB.beq : RGB → RGB → Bool

Equations

• Sparkle.Data.BitPack.instBEqRGB.beq { r := a, g := a_1, b := a_2 } { r := b, g := b_1, b := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Sparkle.Data.BitPack.instBEqRGB.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBEqRGB : BEq RGB

Equations

• Sparkle.Data.BitPack.instBEqRGB = { beq := Sparkle.Data.BitPack.instBEqRGB.beq }

@[implicit_reducible]

instance Sparkle.Data.BitPack.instBitPackRGBOfNatNat : BitPack RGB 24

BitPack instance for RGB (24 bits total)

Equations

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

def Sparkle.Data.BitPack.exampleRGB : RGB

Example RGB value

Equations

• Sparkle.Data.BitPack.exampleRGB = { r := 255#8, g := 128#8, b := 0#8 }