Single-slot abstraction over a Prod-chain state.

Each register slot is identified by a *getter/setter* lens
into the HList.  We don't expose `Fin n` indexing — the lens
pair is what the macro-style allocator would produce, and
the elaborator can reduce a lens that's a chain of `.1`/`.2`
accesses into a plain bit slice. 

@[reducible]

def Sparkle.Core.Circuit.Slot (dom : Domain.DomainConfig) (S τ : Type) : Type

Slot accessor over a state of static shape S.

Concretely a pair (read, update) of lens functions over the Prod-chain state. Defined as a plain Prod alias rather than a structure so the elaborator's existing Prod / Prod.fst / Prod.snd recognition lowers field access without needing a separate struct-projection rule.

Equations

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

@[reducible]

def Sparkle.Core.Circuit.Slot.read {dom : Domain.DomainConfig} {S τ : Type} (s : Slot dom S τ) : Signal.Signal dom S → Signal.Signal dom τ

Equations

• s.read = s.fst

@[reducible]

def Sparkle.Core.Circuit.Slot.update {dom : Domain.DomainConfig} {S τ : Type} (s : Slot dom S τ) : Signal.Signal dom τ → Signal.Signal dom S → Signal.Signal dom S

Equations

• s.update = s.snd

@[reducible]

def Sparkle.Core.Circuit.Slot.mk {dom : Domain.DomainConfig} {S τ : Type} (read : Signal.Signal dom S → Signal.Signal dom τ) (update : Signal.Signal dom τ → Signal.Signal dom S → Signal.Signal dom S) : Slot dom S τ

Equations

• Sparkle.Core.Circuit.Slot.mk read update = (read, update)

@[reducible]

def Sparkle.Core.Reg (dom : Domain.DomainConfig) (S τ : Type) : Type

Register handle = (liveRead, slot) Prod.

Same rationale as Slot — a Prod alias rather than a structure, so accesses through .1 / .2 ride on the existing elaborator rules.

Equations

• Sparkle.Core.Reg dom S τ = (Sparkle.Core.Signal.Signal dom τ × Sparkle.Core.Circuit.Slot dom S τ)

@[reducible]

def Sparkle.Core.Reg.liveRead {dom : Domain.DomainConfig} {S τ : Type} (r : Reg dom S τ) : Signal.Signal dom τ

Equations

• r.liveRead = r.fst

@[reducible]

def Sparkle.Core.Reg.slot {dom : Domain.DomainConfig} {S τ : Type} (r : Reg dom S τ) : Circuit.Slot dom S τ

Equations

• r.slot = r.snd

@[reducible]

def Sparkle.Core.Reg.mk {dom : Domain.DomainConfig} {S τ : Type} (liveRead : Signal.Signal dom τ) (slot : Circuit.Slot dom S τ) : Reg dom S τ

Equations

• Sparkle.Core.Reg.mk liveRead slot = (liveRead, slot)

instance Sparkle.Core.instCoeHeadRegSignal {dom : Domain.DomainConfig} {S τ : Type} : CoeHead (Reg dom S τ) (Signal.Signal dom τ)

A Reg dom S τ coerces to its live Signal dom τ read. Lets user code use cnt directly anywhere a Signal dom τ is expected (e.g. as the rhs of Circuit.next or Signal.mux), without needing an explicit Circuit.read or .1.

Equations

• Sparkle.Core.instCoeHeadRegSignal = { coe := fun (r : Sparkle.Core.Reg dom S τ) => r.fst }

instance Sparkle.Core.instCoeOutRegSignal {dom : Domain.DomainConfig} {S τ : Type} : CoeOut (Reg dom S τ) (Signal.Signal dom τ)

CoeOut: lets Lean coerce a Reg to a Signal even when the expected type isn't fully known (e.g. when both arguments to Signal.mux need coercion and neither side pins down the α first). CoeOut is checked when going from a concrete known type, not to one, so it triggers on a Reg lhs regardless of whether the target Signal's τ is yet determined.

Equations

• Sparkle.Core.instCoeOutRegSignal = { coe := fun (r : Sparkle.Core.Reg dom S τ) => r.fst }

Reg-typed arithmetic / bitwise overloads.

`return a + b` (where `a b : Reg dom S (BitVec n)`) goes
through the `CoeHead Reg → Signal` instance, which then
drives Lean's `HAdd` resolution via the Signal overload's
`(· + ·) <$> a <*> b` Applicative lift.  Under the
ρ-generic `runCircuitH`, the Applicative path leaks the
Stream's `t : Nat` binder into wire translation (the same
failure mode this whole edge case keeps hitting).

The fix is to short-circuit the coerce: provide a Reg-Reg
overload that lowers straight to the Signal-Signal HAdd
instance, skipping the typeclass projection.  Lean prefers
the more specific Reg overload, so `a + b` resolves here
instead of going through `CoeHead`. 

instance Sparkle.Core.instHAddRegBitVecSignal {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HAdd (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHAddRegBitVecSignal = { hAdd := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst + b.fst }

instance Sparkle.Core.instHSubRegBitVecSignal {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HSub (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHSubRegBitVecSignal = { hSub := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst - b.fst }

instance Sparkle.Core.instHMulRegBitVecSignal {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HMul (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHMulRegBitVecSignal = { hMul := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst * b.fst }

instance Sparkle.Core.instHAndRegBitVecSignal {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HAnd (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHAndRegBitVecSignal = { hAnd := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst &&& b.fst }

instance Sparkle.Core.instHOrRegBitVecSignal {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HOr (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHOrRegBitVecSignal = { hOr := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst ||| b.fst }

instance Sparkle.Core.instHXorRegBitVecSignal {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HXor (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHXorRegBitVecSignal = { hXor := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst ^^^ b.fst }

Operator instances lifting Reg to Signal.

`cnt + 1#8` doesn't trigger the `CoeHead` above because Lean
resolves `HAdd cnt 1#8` by looking up `HAdd` with the lhs
type `Reg …`, not by coercing first.  We provide the mixed
`HAdd (Reg …) (BitVec n) (Signal …)` instances explicitly,
mirroring the existing `Signal × BitVec` instances. 

instance Sparkle.Core.instHAddRegBitVecSignal_1 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HAdd (Reg dom S (BitVec n)) (BitVec n) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHAddRegBitVecSignal_1 = { hAdd := fun (a : Sparkle.Core.Reg dom S (BitVec n)) (b : BitVec n) => a.fst + Sparkle.Core.Signal.Signal.pure b }

instance Sparkle.Core.instHSubRegBitVecSignal_1 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HSub (Reg dom S (BitVec n)) (BitVec n) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHSubRegBitVecSignal_1 = { hSub := fun (a : Sparkle.Core.Reg dom S (BitVec n)) (b : BitVec n) => a.fst - Sparkle.Core.Signal.Signal.pure b }

instance Sparkle.Core.instHMulRegBitVecSignal_1 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HMul (Reg dom S (BitVec n)) (BitVec n) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHMulRegBitVecSignal_1 = { hMul := fun (a : Sparkle.Core.Reg dom S (BitVec n)) (b : BitVec n) => a.fst * Sparkle.Core.Signal.Signal.pure b }

instance Sparkle.Core.instHAddRegBitVecSignal_2 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HAdd (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHAddRegBitVecSignal_2 = { hAdd := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst + b.fst }

instance Sparkle.Core.instHSubRegBitVecSignal_2 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HSub (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHSubRegBitVecSignal_2 = { hSub := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst - b.fst }

instance Sparkle.Core.instHMulRegBitVecSignal_2 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HMul (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHMulRegBitVecSignal_2 = { hMul := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst * b.fst }

instance Sparkle.Core.instHAddRegBitVecSignal_3 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HAdd (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHAddRegBitVecSignal_3 = { hAdd := fun (a : Sparkle.Core.Reg dom S (BitVec n)) (b : Sparkle.Core.Signal.Signal dom (BitVec n)) => a.fst + b }

instance Sparkle.Core.instHAddSignalBitVecReg {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HAdd (Signal.Signal dom (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHAddSignalBitVecReg = { hAdd := fun (a : Sparkle.Core.Signal.Signal dom (BitVec n)) (b : Sparkle.Core.Reg dom S (BitVec n)) => a + b.fst }

instance Sparkle.Core.instHXorRegBitVecSignal_1 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HXor (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHXorRegBitVecSignal_1 = { hXor := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst ^^^ b.fst }

instance Sparkle.Core.instHAndRegBitVecSignal_1 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HAnd (Reg dom S (BitVec n)) (BitVec n) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHAndRegBitVecSignal_1 = { hAnd := fun (a : Sparkle.Core.Reg dom S (BitVec n)) (b : BitVec n) => a.fst &&& Sparkle.Core.Signal.Signal.pure b }

instance Sparkle.Core.instHAndRegBitVecSignal_2 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HAnd (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHAndRegBitVecSignal_2 = { hAnd := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst &&& b.fst }

instance Sparkle.Core.instHOrRegBitVecSignal_1 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HOr (Reg dom S (BitVec n)) (BitVec n) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHOrRegBitVecSignal_1 = { hOr := fun (a : Sparkle.Core.Reg dom S (BitVec n)) (b : BitVec n) => a.fst ||| Sparkle.Core.Signal.Signal.pure b }

instance Sparkle.Core.instHOrRegBitVecSignal_2 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HOr (Reg dom S (BitVec n)) (Reg dom S (BitVec n)) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHOrRegBitVecSignal_2 = { hOr := fun (a b : Sparkle.Core.Reg dom S (BitVec n)) => a.fst ||| b.fst }

instance Sparkle.Core.instHXorRegBitVecSignal_2 {dom : Domain.DomainConfig} {S : Type} {n : Nat} : HXor (Reg dom S (BitVec n)) (BitVec n) (Signal.Signal dom (BitVec n))

Equations

• Sparkle.Core.instHXorRegBitVecSignal_2 = { hXor := fun (a : Sparkle.Core.Reg dom S (BitVec n)) (b : BitVec n) => a.fst ^^^ Sparkle.Core.Signal.Signal.pure b }

def Sparkle.Core.Circuit.NextBuilder (dom : Domain.DomainConfig) (S : Type) : Type

Pending next-cycle writes accumulated by the body.

nextOf live returns the closed next-state Signal — we build it by chaining slot updates over the user's <~ calls in source order, starting from live as the "everything holds" baseline.

Equations

• Sparkle.Core.Circuit.NextBuilder dom S = (Sparkle.Core.Signal.Signal dom S → Sparkle.Core.Signal.Signal dom S)

def Sparkle.Core.Circuit (dom : Domain.DomainConfig) (S α : Type) : Type

The Circuit monad — state-passing over the pending writes accumulator Circuit.NextBuilder dom S.

S is the static HList shape of the register state. The macro / allocator chooses S at runCircuit time and the type stays fixed across the body.

Equations

• Sparkle.Core.Circuit dom S α = (Sparkle.Core.Circuit.NextBuilder dom S → α × Sparkle.Core.Circuit.NextBuilder dom S)

@[reducible, inline]

def Sparkle.Core.Circuit.pure' {dom : Domain.DomainConfig} {S α : Type} (a : α) : Circuit dom S α

Equations

• Sparkle.Core.Circuit.pure' a b = (a, b)

@[reducible, inline]

def Sparkle.Core.Circuit.bind {dom : Domain.DomainConfig} {S α β : Type} (m : Circuit dom S α) (k : α → Circuit dom S β) : Circuit dom S β

Equations

• m.bind k b = k (m b).fst (m b).snd

@[reducible]

instance Sparkle.Core.Circuit.instMonad {dom : Domain.DomainConfig} {S : Type} : Monad (Circuit dom S)

Equations

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

@[reducible, inline]

def Sparkle.Core.Circuit.next {dom : Domain.DomainConfig} {S τ : Type} [Inhabited S] (r : Reg dom S τ) (sig : Signal.Signal dom τ) : Circuit dom S Unit

Record a next-cycle Signal for one register slot. Repeat writes overwrite earlier ones via Slot.update's "stamp into the slot" semantics (last write wins, matching the macro).

Equations

• Sparkle.Core.Circuit.next r sig b = ((), fun (live : Sparkle.Core.Signal.Signal dom S) => r.slot.update sig (b live))

class Sparkle.Core.Circuit.AsSignal (dom : Domain.DomainConfig) (τ α : Type) : Type

Type class capturing "things that can be the rhs of a register write" — a Signal dom τ directly, or a bare element value (e.g. BitVec n, Bool) that we wrap in Signal.pure.

Lets circuit do lower state <~ 0#2 (BitVec rhs) and cnt <~ cnt + 1#8 (Signal rhs) through the same Circuit.next shape without per-case syntax tracking.

• toSignal : α → Signal.Signal dom τ

@[reducible]

instance Sparkle.Core.Circuit.instAsSignalSignal {dom : Domain.DomainConfig} {τ : Type} : AsSignal dom τ (Signal.Signal dom τ)

Equations

• Sparkle.Core.Circuit.instAsSignalSignal = { toSignal := fun (s : Sparkle.Core.Signal.Signal dom τ) => s }

@[reducible]

instance Sparkle.Core.Circuit.instAsSignalBitVec {dom : Domain.DomainConfig} {n : Nat} : AsSignal dom (BitVec n) (BitVec n)

Equations

• Sparkle.Core.Circuit.instAsSignalBitVec = { toSignal := fun (v : BitVec n) => Sparkle.Core.Signal.Signal.pure v }

@[reducible]

instance Sparkle.Core.Circuit.instAsSignalBool {dom : Domain.DomainConfig} : AsSignal dom Bool Bool

Equations

• Sparkle.Core.Circuit.instAsSignalBool = { toSignal := fun (v : Bool) => Sparkle.Core.Signal.Signal.pure v }

@[reducible, inline]

def Sparkle.Core.Circuit.nextAny {dom : Domain.DomainConfig} {S τ : Type} [Inhabited S] {α : Type} [AsSignal dom τ α] (r : Reg dom S τ) (val : α) : Circuit dom S Unit

Polymorphic register-write: accepts either a Signal dom τ or a bare τ value (lifted via AsSignal). Replaces next at the user-visible API; next remains as the raw Signal-only form used internally.

Equations

• Sparkle.Core.Circuit.nextAny r val = Sparkle.Core.Circuit.next r (Sparkle.Core.Circuit.AsSignal.toSignal val)

@[reducible, inline]

def Sparkle.Core.Circuit.read {dom : Domain.DomainConfig} {S τ : Type} (r : Reg dom S τ) : Signal.Signal dom τ

Read the live current-cycle Signal of a register handle. Just a projection — there for symmetry with next.

Equations

• Sparkle.Core.Circuit.read r = r.liveRead

HasDomain ρ dom — outParam-style typeclass that walks

a return type ρ and reports the unique `DomainConfig` of
every `Signal` leaf it contains.

`runCircuitH`'s ρ-generalisation (single Signal / tuple of
Signals / user record packing several Signals) lets the body
return any Lean value, but the surrounding `Signal.loop`
needs `dom` to be a specific `DomainConfig` value, not a
metavariable.  Without this class, type inference can pull
`dom` out of `ρ` only when `ρ` is *literally* `Signal dom τ`
— a Prod or record wrapping Signal leaves it inaccessible to
the elaborator.

`dom` is `outParam` so it's inferred from `ρ`; one instance
per shape walks the type structurally.  User-defined records
can pick up a `HasDomain` instance via a one-line manual
`instance : HasDomain MyOut dom := ⟨⟩` (any single-`dom`
record qualifies; the instance is empty because the class
carries no methods — it's purely an inference hint). 

class Sparkle.Core.HasDomain (ρ : Type) (dom : outParam Domain.DomainConfig) : Type

instance Sparkle.Core.instHasDomainSignal {dom : Domain.DomainConfig} {τ : Type} : HasDomain (Signal.Signal dom τ) dom

Base case: a single Signal dom τ carries dom.

Equations

• Sparkle.Core.instHasDomainSignal = { }

instance Sparkle.Core.instHasDomainProd {α β : Type} {dom : Domain.DomainConfig} [HasDomain α dom] [HasDomain β dom] : HasDomain (α × β) dom

Recursive case: a Prod of two values whose HasDomain instances agree on dom carries the same dom. If the two sides disagree, instance search fails with a clear error rather than silently picking one.

Equations

• Sparkle.Core.instHasDomainProd = { }

SignalLeaves — flatten ρ into a list of its Signal

leaves so the wire-translation compiler can emit one output
port per leaf.

Companion of `HasDomain`.  `toLeaves r` walks the value
structurally and produces a `(name, Σ τ, Signal dom τ)`
triple for every Signal slot in `r`.  The compiler's
`synthesizeCombinational` reads the list and registers each
leaf as its own Verilog wire, so
`circuit do { … return ⟨a, b, c⟩ }` (or its record-literal
equivalent) yields three real `output` ports rather than
one bundled `bundle2` blob.

The class is `outParam ρ` — driven by the user value;
`dom` is `outParam` so instance search can resolve from
`ρ`.  Base instances handle `Signal dom τ`, `Prod α β`,
`Unit`, and `PUnit`.  User records pick up a derived
instance via `deriving SignalLeaves`. 

class Sparkle.Core.SignalLeaves (ρ : Type) (dom : outParam Domain.DomainConfig) : Type (u_1 + 1)

• toLeaves : ρ → List (Option String × (τ : Type u_1) × Signal.Signal dom τ)

  Walk r and emit one (label, τ, signal) record per Signal dom τ leaf. The label is intended for output- port naming on the Verilog side; for unlabelled leaves (Signal dom τ at the top level, Prod's sides) we pass none and the compiler invents a positional name.

@[reducible]

instance Sparkle.Core.instSignalLeavesSignal {dom : Domain.DomainConfig} {τ : Type} : SignalLeaves (Signal.Signal dom τ) dom

Base case: a single Signal dom τ is one anonymous leaf.

Equations

• Sparkle.Core.instSignalLeavesSignal = { toLeaves := fun (s : Sparkle.Core.Signal.Signal dom τ) => [(none, ⟨τ, s⟩)] }

@[reducible]

instance Sparkle.Core.instSignalLeavesProd {dom : Domain.DomainConfig} {α β : Type} [SignalLeaves α dom] [SignalLeaves β dom] : SignalLeaves (α × β) dom

Prod: concatenate the two sides' leaves, left first.

Equations

• Sparkle.Core.instSignalLeavesProd = { toLeaves := fun (p : α × β) => Sparkle.Core.SignalLeaves.toLeaves p.fst ++ Sparkle.Core.SignalLeaves.toLeaves p.snd }

Arbitrary-arity runCircuitH via HList state.

The generalisation of `runCircuit{1,2,3,4}` to any list of
register types.  Constraint `[HListWireable αs]` ensures
every slot type is synth-friendly; without it a user could
drop e.g. `Option Nat` into the list and hit a synth
failure deep inside the elaborator.

Three pieces:

  1. `RegList dom S αs` — heterogeneous list of register
     handles, one per slot, sharing one outer state shape S.
  2. `mkRegList` — builds the `RegList` from a live state
     Signal by composing `Prod.fst` / `Prod.snd` accessors
     (the slot lenses are constructed once, recursively).
  3. `runCircuitH` — closes the body with `Signal.loop` and
     a chain of `Signal.register`s, one per slot.

Each piece is `@[reducible, inline]` so the IR elaborator
can unfold through them at synth time. 

@[reducible]

def Sparkle.Core.RegList (dom : Domain.DomainConfig) (S : Type) : List Type → Type

RegList dom S αs — a tuple of register handles for slots αs, all carrying the same outer state shape S. Defined structurally on αs so a RegList dom S (α :: αs') decomposes into Reg dom S α × RegList dom S αs'. S is fixed across the whole list — it doesn't shrink as we recurse, which is the key to keeping the slot lenses typed against the original outer state.

Equations

• Sparkle.Core.RegList dom S [] = Unit
• Sparkle.Core.RegList dom S (α :: αs) = (Sparkle.Core.Reg dom S α × Sparkle.Core.RegList dom S αs)

@[reducible]

def Sparkle.Core.mkRegList {dom : Domain.DomainConfig} {S : Type} (liveOuter : Signal.Signal dom S) (αs : List Type) (readSig : Signal.Signal dom S → Signal.Signal dom (HList αs)) (writeSig : Signal.Signal dom (HList αs) → Signal.Signal dom S → Signal.Signal dom S) : RegList dom S αs

Build a RegList dom S αs by walking down αs.

Constructed slot lenses are pure Signal-level chains of Signal.map Prod.fst / Prod.snd and bundle2 — the same primitives Sparkle's IR elaborator already lowers. No value-level Signal.map closures over arbitrary functions.

The slot read/update lenses are passed in as Signal-level operations (rather than pure-value functions) so the chained Prod.fst/Prod.snd calls stay visible to the elaborator at every recursion depth.

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.Core.mkRegList liveOuter [] x_3 x_4 = ()

@[reducible, inline]

def Sparkle.Core.packRegister {dom : Domain.DomainConfig} (αs : List Type) : HList αs → Signal.Signal dom (HList αs) → Signal.Signal dom (HList αs)

For each slot of αs, take the corresponding init and a slice of nextState, and emit a Signal.register. Pack the results back into a Signal dom (HList αs).

Reducible so the synth elaborator unfolds through it to the underlying Signal.register / bundle2 chain.

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.Core.packRegister [] x_3 x_4 = Sparkle.Core.Signal.Signal.pure ()

@[reducible, inline]

def Sparkle.Core.runCircuitH {dom : Domain.DomainConfig} {αs : List Type} {ρ : Type} [HasDomain ρ dom] [HListWireable αs] [Inhabited (HList αs)] (inits : HList αs) (body : RegList dom (HList αs) αs → Circuit dom (HList αs) ρ) : ρ

Generic runCircuit taking any HList of initial values. The body receives a matching RegList of register handles and returns an arbitrary ρ.

ρ is unconstrained: it can be a single Signal dom τ, a tuple (Signal dom τ₁, Signal dom τ₂), a user-defined record packing several Signals (e.g. an Ethernet RxOut), or any combination. The synthesis elaborator (Sparkle/Compiler/Elab.lean) walks ρ structurally and emits one Verilog wire per Signal leaf, so multi-output blocks come out of circuit do { … return ⟨a, b, c⟩ } naturally without a bundle2-shaped contortion.

Historically this signature required body : … → Circuit … (Signal dom ρ), which made multi-output blocks expressible only via tupling at the Signal level. Dropping that constraint is the monad-friendly story: the user's body builds whatever Lean value they want and returns it; the Circuit monad just threads the register-update slot map alongside.

[HListWireable αs] requires every slot type to be Wireable, gating non-synthesisable types at the call site instead of the synth elaborator.

Equations

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