Files
digital-drosophila/models/male-cns-lif/deterministic-runtime-v2/candidate/MaleCNS-NumericalContract-v1.md
T

27 lines
1.9 KiB
Markdown

# MaleCNS-NumericalContract-v1
Status: immutable candidate contract for `MaleCNS-LIF-runtime-v2-deterministic-candidate`.
## Frozen tensors and arithmetic
- State (`V`, `g`, ring-buffer arrivals, effective edge weights): IEEE-754 binary32.
- CSR `indptr` and edge ids: int64; target indices: int32; refractory/counts: int32.
- Effective edge weights are the frozen Phase 4C signed float32 weights; raw synapse counts remain unchanged.
- Canonical contribution key: `['target_idx', 'source_idx', 'edge_id']`. Since global CSR edge ids are source-row ordered, stable `(target_idx, edge_id)` sorting is equivalent.
- Each target is owned by one thread and accumulated sequentially with round-to-nearest-even `__fadd_rn`. Scientific fan-out contains no atomic add.
## Per-timestep total order
1. Read and clear the current exact ring-buffer slot.
2. `g = float32(g * g_decay)`, then `g = float32(g + recurrent_arrival)`.
3. Decrement refractory by one; while refractory remains nonzero, hold `V = V_reset`.
4. For available neurons, forward Euler: `V = float32(V + alpha * (g - (V - V_rest)))`, with every elementary operation rounded to float32.
5. Detect spikes using the frozen comparison `V >= V_threshold`; reset and set exact refractory steps.
6. Apply same-step external forced-spike events in ascending target index; a neuron already spiking or refractory is not double-counted.
7. Enumerate spiking source indices in ascending neuron index. Expand each CSR row in edge-id order.
8. Stable-sort contributions by target only, preserving source/edge order, then perform fixed sequential segmented sums.
9. Add each segment once to the ring-buffer slot exactly 18 steps ahead.
10. Emit events in `(simulation_step, neuron_idx)` order. Simultaneous events never receive a hidden priority beyond neuron index.
No threshold epsilon, voltage rounding/snap, float64 model substitution, approximate delay, topology change, or parameter change is permitted.