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 W τ : Type) : Type

Slot accessor over a state of static shape S, writing into a pending-writes accumulator of type W.

Concretely a pair (read, update): read is a lens over the live Prod-chain state (unchanged from the original design); update stamps a new Signal into the slot's entry of the pending-writes accumulator W.

Why update targets W (a tuple of per-slot Signals), not Signal S

The original update : Signal τ → Signal S → Signal S rebuilt the FULL bundled next-state on every write — reading every other slot back out of the previous accumulator via lens chains. Composing k writes therefore built a k-deep chain in which each layer referenced the previous layer once per slot, and the closure evaluator (which has no sharing — the heap DAG is walked as a tree) paid ~k^k per cycle. That is the real mechanism behind issue #95: a 10-register pass-through chain hung near t≈20 through Signal.val, while hand-written bundleAll! FSMs (flat, single next-tuple) of 6+ registers were instant.

With W = SigList (one pending Signal per slot), a write is pure tuple surgery — no Signal nodes are created, nothing re-reads other slots — and runCircuitH bundles the accumulator ONCE into the register file. Evaluation cost per cycle is linear in the circuit size.

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

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

@[reducible]

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

Equations

• s.read = s.fst

@[reducible]

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

Equations

• s.update = s.snd

@[reducible]

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

Equations

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

@[reducible]

def Sparkle.Core.Reg (dom : Domain.DomainConfig) (S W τ : 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 W τ = (Sparkle.Core.Signal.Signal dom τ × Sparkle.Core.Circuit.Slot dom S W τ)

@[reducible]

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

Equations

• r.liveRead = r.fst

@[reducible]

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

Equations

• r.slot = r.snd

@[reducible]

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

Equations

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

@[implicit_reducible]

instance Sparkle.Core.instCoeHeadRegSignal {dom : Domain.DomainConfig} {S W τ : Type} : CoeHead (Reg dom S W τ) (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 W τ) => r.fst }

@[implicit_reducible]

instance Sparkle.Core.instCoeOutRegSignal {dom : Domain.DomainConfig} {S W τ : Type} : CoeOut (Reg dom S W τ) (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 W τ) => r.fst }

Reg-typed arithmetic / bitwise overloads.

`return a + b` (where `a b : Reg dom S W (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`. 

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• Sparkle.Core.instHXorRegBitVecSignal = { hXor := fun (a b : Sparkle.Core.Reg dom S W (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. 

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Sparkle.Core.instHAddRegBitVecSignal_3 {dom : Domain.DomainConfig} {S W : Type} {n : Nat} : HAdd (Reg dom S W (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 W (BitVec n)) (b : Sparkle.Core.Signal.Signal dom (BitVec n)) => a.fst + b }

@[implicit_reducible]

instance Sparkle.Core.instHAddSignalBitVecReg {dom : Domain.DomainConfig} {S W : Type} {n : Nat} : HAdd (Signal.Signal dom (BitVec n)) (Reg dom S W (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 W (BitVec n)) => a + b.fst }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• Sparkle.Core.instHXorRegBitVecSignal_2 = { hXor := fun (a : Sparkle.Core.Reg dom S W (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)

@[reducible]

def Sparkle.Core.Circuit.SigList (dom : Domain.DomainConfig) : List Type → Type

Pending-writes accumulator: one Signal per register slot.

This replaces the function-composition NextBuilder as the thing the Circuit monad threads. A write is a pure tuple update; runCircuitH bundles the final tuple into the register file once (flat, depth-1). See the Slot docstring for why the composed form was catastrophic for simulation (issue #95).

Equations

• Sparkle.Core.Circuit.SigList dom [] = Unit
• Sparkle.Core.Circuit.SigList dom (α :: αs) = (Sparkle.Core.Signal.Signal dom α × Sparkle.Core.Circuit.SigList dom αs)

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

The Circuit monad — state-passing over the pending-writes accumulator W (a Circuit.SigList at runCircuitH: one pending Signal per register slot; see Slot for why this replaced the function-composition NextBuilder, issue #95).

Equations

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

@[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 τ W : Type} (r : Reg dom S W τ) (sig : Signal.Signal dom τ) : Circuit dom W 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).

Note the accumulator parameter of Circuit here is the pending-writes tuple (a Circuit.SigList at runCircuitH), NOT the live-state shape: the write is pure tuple surgery and never touches the Signal graph.

Equations

• Sparkle.Core.Circuit.next r sig w = ((), r.slot.update sig w)

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 τ W α : Type} [AsSignal dom τ α] (r : Reg dom S W τ) (val : α) : Circuit dom W 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 τ W : Type} (r : Reg dom S W τ) : 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

@[implicit_reducible]

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 = { }

@[implicit_reducible]

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 1

• toLeaves : ρ → List (Option String × (τ : Type) × 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 W : 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 W [] = Unit
• Sparkle.Core.RegList dom S W (α :: αs) = (Sparkle.Core.Reg dom S W α × Sparkle.Core.RegList dom S W αs)

@[reducible]

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

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

Read lenses are pure Signal-level chains of Signal.map Prod.fst / Prod.snd — the same primitives Sparkle's IR elaborator already lowers.

Write "lenses" are pure tuple updates into the pending-writes accumulator: lift lifts an update on the local SigList suffix into an update on the full accumulator W. No Signal node is built on the write path — this flatness is the issue-#95 fix (see Slot).

Equations

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

@[reducible]

def Sparkle.Core.mkHolds {dom : Domain.DomainConfig} (αs : List Type) (live : Signal.Signal dom (HList αs)) : Circuit.SigList dom αs

The "everything holds" seed for the pending-writes accumulator: each slot's entry is its own live read. A slot that is never written keeps its value; a written slot's entry is replaced by Circuit.next.

Equations

• Sparkle.Core.mkHolds [] x_2 = ()
• Sparkle.Core.mkHolds (head :: αs') live = (Sparkle.Core.Signal.Signal.map Prod.fst live, Sparkle.Core.mkHolds αs' (Sparkle.Core.Signal.Signal.map Prod.snd live))

@[reducible, inline]

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

One Signal.register per slot, fed DIRECTLY by that slot's pending Signal — no projection of a bundled next-state, no reconstruction. Pack the register outputs back into a Signal dom (HList αs).

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

Equations

• Sparkle.Core.packRegister [] x_3 x_4 = Sparkle.Core.Signal.Signal.pure ()
• Sparkle.Core.packRegister (head :: αs') init writes = Sparkle.Core.Signal.bundle2 (Sparkle.Core.Signal.Signal.register init.fst writes.fst) (Sparkle.Core.packRegister αs' init.snd writes.snd)

@[reducible]

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) (Circuit.SigList dom αs) αs → Circuit dom (Circuit.SigList dom α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.

The Circuit accumulator is Circuit.SigList dom αs — the flat pending-writes tuple seeded by mkHolds — rather than the historical NextBuilder function composition. See Slot for why (issue #95).

[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.