| --- |
| license: other |
| license_name: sovereign-leviathan-sl-agpl3-001 |
| license_link: https://huggingface.co/Snapkitty/sparse-router-formal/blob/main/LICENSE |
| tags: |
| - snapkitty |
| - october-2026-drop |
| - rust |
| - pascal |
| - lean4 |
| - c |
| - kani |
| - work-stealing |
| - scheduler |
| - formal-verification |
| --- |
| |
| > Mirrored from [https://github.com/SNAPKITTYWEST/sparse-router-formal](https://github.com/SNAPKITTYWEST/sparse-router-formal) at commit `5e292ee`. Part of the **SnapKitty October 2026 main drop**. |
|
|
| # Sparse Router β Formally Verified Locality-Aware Work-Stealing Scheduler |
|
|
| **License**: Sovereign Leviathan covenant (`LicenseRef-Sovereign-Leviathan-SL-AGPL3-001`), AGPL-3.0 based |
|
|
| ## Architecture |
|
|
| ``` |
| sparse-router-formal/ |
| βββ rust/tensor-hw/ # Production Rust: tensor core + RAW_ROUTE + Kani proofs |
| β βββ src/ # 10 modules: buffer, ownership, memory, view, governance... |
| β βββ ffi/ # sparse_router.rs, kani proofs, C ABI, FFI bridge |
| βββ pascal/ # Reference implementation (independent conformance oracle) |
| βββ formal/ # Lean 4 formal proofs (convergence, invariants, scoring) |
| βββ c-reference/ # Standalone C reference (header-only, benchmarkable) |
| βββ tests/conformance/ # 52 cross-language conformance tests (7 categories) |
| βββ spec/ # Normative specifications (contract, state machine, memory model) |
| βββ src/pascal/ # Pascal transformer sources |
| βββ scripts/ # Clone-gate verification |
| ``` |
|
|
| ## Novel Method: RAW_ROUTE |
| |
| Three-phase routing with O(K) sparse-edge traversal (K β€ 16), not O(N) worker scan: |
| |
| ``` |
| score(w, t) = locality(w,t) + memory_affinity(w,t) + queue_pressure(w) |
| + stealability(w) - migration_cost(w,t) |
| ``` |
| |
| | Phase | Path | Complexity | |
| |-------|------|-----------| |
| | 1 | Region-owner fast path | O(1) | |
| | 2 | Sparse edge traversal | O(K) | |
| | 3 | Least-loaded fallback | O(N) | |
| |
| ## Formal Verification |
| |
| ### Lean 4 Proofs (`formal/`) |
| - **Convergence**: potential function Ξ¦ = |unowned regions| strictly decreases β stable in β€ MAX_REGIONS steps |
| - **Uniqueness**: every routed task lands on exactly one worker deque |
| - **Bounded traversal**: sparse edge fan-out β€ MAX_SPARSE_EDGES |
| - **Scoring properties**: locality bonus, empty-queue bonus, zero migration cost for local tasks |
| - **Deque correctness**: push/pop identity, count invariants |
| |
| ### Kani Proofs (`rust/tensor-hw/ffi/sparse_router_kani.rs`) |
| - All tasks routed (progress guaranteed) |
| - Region owner consistency |
| - Locality over balance |
| - Migration cost avoidance |
| - Fallback coverage |
| - Route decision stability |
| - Score bounds (all weights finite) |
| - No deadlock (acyclic region ownership) |
| |
| ### Cross-Language Conformance (`tests/conformance/`) |
| 52 tests across 7 categories β Rust and Pascal must agree: |
| - Buffer lifetime, ownership transitions, views, materialization |
| - Generation validation, governance, routing |
| |
| ## Build |
| |
| ```bash |
| make test # C reference tests (7 tests) |
| make bench # C benchmarks (~100M routes/sec) |
| make test-rust # Rust test suite (49 tests) |
| make verify # Lean 4 proofs (requires lake) |
| make clone-gate-check # Verify all markers present, no MIT |
| ``` |
| |
| ## Clone Gate |
| |
| All source files contain `CLONE_GATE` markers. See `CLONE_GATE.md` for terms. |
| No MIT or Apache licensing permitted. See `LICENSE`. |
| |
| ## Deliverables Summary |
| |
| | Component | LOC | Status | |
| |-----------|-----|--------| |
| | Specifications | ~3,600 | 7 normative documents | |
| | Rust Core | ~2,670 | 10 modules + 49 tests | |
| | Pascal Reference | ~2,450 | 10 modules + 10 tests | |
| | Lean 4 Proofs | ~350 | 6 modules, convergence theorem | |
| | C Reference | ~450 | Header-only + benchmarks | |
| | Conformance Tests | ~2,800 | 52 tests + oracle | |
| | Kani Proofs | ~400 | 8 formal proofs | |
| | **Total** | **~12,700** | **Production ready** | |
| |
| --- |
| |
| ### πΌ Commercial License |
| |
| SnapKitty code is free and open under the **Sovereign Leviathan covenant (AGPL-3.0 based)** for open-source use. Building a commercial product or service? A **proprietary commercial license** from Snapkitty Collective LLC lets you ship this code without the covenant's source-sharing and network-use obligations. |
| |
| **[β Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20sparse-router-formal)** Β· A.parr@belespritdaccord.uk |
| |
