class Sparkle.Core.Wireable (α : Type) : Type

Asserts that α has a known hardware bit-width.

Instances are intentionally minimal — no toBits/fromBits. The IR elaborator recognises the structural shape of α (BitVec / Bool / Prod / HWVector) directly when wiring, so the typeclass only needs to expose the width for code that reasons about state size statically.

• width : Nat

instance Sparkle.Core.instWireableBool : Wireable Bool

Equations

• Sparkle.Core.instWireableBool = { width := 1 }

instance Sparkle.Core.instWireableBitVec (n : Nat) : Wireable (BitVec n)

Equations

• Sparkle.Core.instWireableBitVec n = { width := n }

@[reducible]

def Sparkle.Core.HList : List Type → Type

Right-nested heterogeneous product over a static type list.

HList [α, β, γ] = α × β × γ × Unit. Definitionally a Prod chain so Prod.fst / Prod.snd projections (which the IR elaborator already lowers to bit slices) reach individual slots without needing new wire rules.

Equations

• Sparkle.Core.HList [] = Unit
• Sparkle.Core.HList (α :: αs) = (α × Sparkle.Core.HList αs)

@[reducible]

def Sparkle.Core.HList.cons {α : Type} {αs : List Type} (x : α) (xs : HList αs) : HList (α :: αs)

Element-wise construction (the same shape α × HList αs of the inductive HList (α :: αs), just sugared).

Equations

• Sparkle.Core.HList.cons x xs = (x, xs)

@[reducible]

def Sparkle.Core.HList.nil : HList []

Equations

• Sparkle.Core.HList.nil = ()

@[reducible]

def Sparkle.Core.HList.head {α : Type} {αs : List Type} (h : HList (α :: αs)) : α

Head of a non-empty HList — definitionally Prod.fst.

Equations

• h.head = h.fst

@[reducible]

def Sparkle.Core.HList.tail {α : Type} {αs : List Type} (h : HList (α :: αs)) : HList αs

Tail of a non-empty HList — definitionally Prod.snd.

Equations

• h.tail = h.snd

instance Sparkle.Core.instWireableUnit : Wireable Unit

Empty HList wires to a zero-width slot. Matches the Prod chain's Unit terminator.

Equations

• Sparkle.Core.instWireableUnit = { width := 0 }

instance Sparkle.Core.instWireableProd {α β : Type} [Wα : Wireable α] [Wβ : Wireable β] : Wireable (α × β)

Prod of two Wireables is Wireable. Width is the sum, exactly what the elaborator's existing Prod wire rule does.

Equations

• Sparkle.Core.instWireableProd = { width := Sparkle.Core.Wireable.width α + Sparkle.Core.Wireable.width β }

class Sparkle.Core.HListWireable (αs : List Type) : Type

HListWireable αs asserts that every element type in αs has a Wireable instance. Used as a constraint on runCircuit so users can't accidentally place non- synthesisable types (e.g. Option Nat) into the register state list — the type check fires at the runCircuit call site, well before #synthesizeVerilog would.

The class is intentionally empty: its presence is the assertion. Instances are derived structurally on the list so any αs whose elements are individually Wireable automatically gets an instance.

Wireable (HList αs) follows by induction over the Prod chain α × HList αs, using the existing Wireable (α × β) instance above.

instance Sparkle.Core.instHListWireableNil : HListWireable []

Equations

• Sparkle.Core.instHListWireableNil = { }

instance Sparkle.Core.instHListWireableConsOfWireable {α : Type} {αs : List Type} [Wireable α] [HListWireable αs] : HListWireable (α :: αs)

Equations

• Sparkle.Core.instHListWireableConsOfWireable = { }

instance Sparkle.Core.instWireableHListNil : Wireable (HList [])

HList αs is Wireable whenever every element is. Induction over the list.

Equations

• Sparkle.Core.instWireableHListNil = { width := 0 }

instance Sparkle.Core.instWireableHListCons {α : Type} {αs : List Type} [Wireable α] [Wireable (HList αs)] : Wireable (HList (α :: αs))

Equations

• Sparkle.Core.instWireableHListCons = inferInstanceAs (Sparkle.Core.Wireable (α × Sparkle.Core.HList αs))