How Spike Star Works
====================

This page traces the verifier from input set to robustness certificate, following
the formulation used in the paper. The implementation lives in
``src/snn_decomp/`` (``sets/star.py``, ``EffectiveSynapses.py``,
``sets/ftf_star_rep.py``).

1. The generalized star set
---------------------------

The input set is a **generalized star** :math:`\Theta = \langle \mathbf{c}, V, P\rangle`,
representing

.. math::

   \llbracket\Theta\rrbracket = \Bigl\{\, \mathbf{x} = \mathbf{c} + \textstyle\sum_{i=1}^{m}
   \alpha_i \mathbf{v}_i \;\;\text{s.t.}\;\; P(\boldsymbol{\alpha}):\; C\boldsymbol{\alpha}\le \mathbf{d} \,\Bigr\},

with center :math:`\mathbf{c}`, basis vectors :math:`V=\{\mathbf{v}_1,\dots,\mathbf{v}_m\}`,
and a conjunction of linear predicates :math:`P`. This one representation
**generalizes hyperrectangles (boxes), zonotopes, and convex polytopes** through the
choice of :math:`V` and :math:`P` — a box is :math:`V=\mathrm{diag}(\epsilon)` with
:math:`\boldsymbol{\alpha}\in[-1,1]^m`; a zonotope keeps the box predicate but allows
non-axis-aligned :math:`V`.

2. F2F encoding and decoding
----------------------------

First-to-fire latency encoding maps a normalized input :math:`x\in[0,1]` to a single
spike time

.. math::

   \mathcal{L}(x) = \mathrm{round}\bigl((T-1)(1-x)\bigr) + 1 \;\;(x>0), \qquad
   \mathcal{L}(0) = \infty,

so brighter inputs fire earlier (:math:`x=1` at :math:`t=1`) and a zero input never
fires. Decoding scores each class by its first output spike time
:math:`t_c^{\mathrm{out}}`:

.. math::

   y_c = \begin{cases} T+1-t_c^{\mathrm{out}}, & t_c^{\mathrm{out}}<\infty,\\ 0, & \text{otherwise,}\end{cases}

so an **earlier output spike yields a larger score**, and the predicted class is
:math:`\arg\max_c y_c`.

3. LIF dynamics
---------------

Each LIF neuron integrates synaptic current with a leak and a **subtract reset**:

.. math::

   V_{ij}[t] = \beta_i V_{ij}[t-1] + \textstyle\sum_k W_{ijk}\,s_{i-1,k}[t] + b_{ij}
   - V_{\mathrm{th}}\,s_{ij}[t-1], \qquad
   s_{ij}[t] = \mathbf{1}\{V_{ij}[t]\ge V_{\mathrm{th}}\}.

Under F2F encoding every neuron fires **at most once** (a has-fired mask prevents
re-firing), so the spatiotemporal firing activity is a sparse binary table.

4. Spike patterns and effective synapses
-----------------------------------------

Stacking the per-timestep spike vectors gives the layer spike train
:math:`\mathbf{S}_i\in\{0,1\}^{T\times N_i}`; collecting them across layers gives the
**spike pattern** :math:`\boldsymbol{\sigma}=(\mathbf{S}_1,\dots,\mathbf{S}_L)`. Because
:math:`\mathbf{s}_{i-1}[t]` is binary, the synaptic current is a column-masked weight —
the **effective synapses**

.. math::

   \mathbf{W}_i^{\mathrm{eff}}[t] = \mathbf{W}_i \odot \mathbf{s}_{i-1}[t]^\top .

Once the encoded input spikes and the spike pattern :math:`\boldsymbol{\sigma}` are
fixed, every effective weight is determined and each finite-horizon update is
**affine in the star predicate variables**. This is the piecewise-affine structure
star sets exploit.

5. The spiking star set
-----------------------

Different inputs in the star may produce different spike patterns, partitioning the
predicate space into finitely many cells. The **spiking star set**
:math:`\mathcal{S}=\langle \mathbf{c}, V, P, \Sigma\rangle` augments the star with the
set :math:`\Sigma` of reachable patterns and represents the output as a **union**

.. math::

   \llbracket\mathcal{S}\rrbracket = \bigcup_{\boldsymbol{\sigma}\in\Sigma}
   \bigl\{ f_{\boldsymbol{\sigma}}(\mathbf{x}) \;:\; \mathbf{x}\in\llbracket\Theta\rrbracket
   \text{ refined to } \boldsymbol{\sigma} \bigr\},

where :math:`f_{\boldsymbol{\sigma}}` is the affine map on that pattern's cell. (No
Minkowski sum over time — the temporal recurrence is folded into each affine
:math:`f_{\boldsymbol{\sigma}}`, and the reachable set is the union across cells.)

6. Spiking affine propagation
-----------------------------

On a cell with fixed pattern, :math:`f_{\boldsymbol{\sigma}}(\mathbf{x})=A_{\boldsymbol{\sigma}}\mathbf{x}+\mathbf{b}_{\boldsymbol{\sigma}}`,
and the star image is exact with the predicate unchanged:

.. math::

   f_{\boldsymbol{\sigma}}(\Theta) = \bigl\langle\, A_{\boldsymbol{\sigma}}\mathbf{c}+\mathbf{b}_{\boldsymbol{\sigma}},\;
   \{A_{\boldsymbol{\sigma}}\mathbf{v}_1,\dots,A_{\boldsymbol{\sigma}}\mathbf{v}_m\},\; P \,\bigr\rangle .

Applying the same affine image over a *larger* predicate region yields a sound
enclosure of that component.

7. Enclosure and robustness
---------------------------

The verifier produces a **box enclosure** of the reachable scores,
:math:`\widehat{\mathcal{R}} = \prod_c [\underline y_c, \overline y_c]`, by bounding
each class score (one bound and one margin LP per competing class). The input set is
**certified robust** for class :math:`c^*` when

.. math::

   \underline y_{c^*} > \overline y_c \quad \text{for all } c\neq c^*

(a strict margin; exact ties are not certified).

8. Symbolic relaxation and adaptive latency splitting
-----------------------------------------------------

Enumerating :math:`\Sigma` is exponential, so the verifier never builds it. It starts
with **one symbolic relaxation** over the full input set — relaxing each ambiguous
hidden spike decision to a continuous predicate variable with a step-hull
over-approximation — and refines only when the relaxation cannot certify the pairwise
margins. Refinement **splits input F2F latency cells** adaptively: no split is purely
symbolic; fixing all perturbed-input latencies recovers **exact latency-level
analysis**. The split order affects runtime but not soundness.

.. note::
   The :doc:`playground` runs this pipeline live on a 2-input toy with a star (box or
   zonotope) input, showing the latency cells, the per-class score enclosure, the
   membrane envelopes, and the spike-train ranges, with a sound margin verdict.