| --- |
| license: other |
| license_name: snapkitty-tri-license |
| license_link: https://huggingface.co/Snapkitty/sovereign-agent-kernel/blob/main/LICENSE |
| tags: |
| - snapkitty |
| - agents |
| - 6502-asm |
| - forth |
| --- |
| |
| > Source: [github.com/SNAPKITTYWEST/sovereign-agent-kernel](https://github.com/SNAPKITTYWEST/sovereign-agent-kernel) |
|
|
| # Sovereign Agent Kernel — 6502 |
|
|
| [](LICENSE) |
| [](idris/NASA10Plus.idr) |
| [](idris/) |
| [](src/kernel.asm) |
| [](src/sha512.asm) |
| [](forth/) |
| [](src/kernel.asm) |
| [](idris/CryptoVerify.idr) |
| [](https://github.com/SNAPKITTYWEST/sovereign-hypervisor-arm64) |
|
|
| **Authors:** Ahmad Ali Parr, Jessica L. Williams (SNAPKITTYWEST) |
|
|
| > **Zero heap. Bounded loops. Cycle-counted. Formally verified.** |
| > **NASA-10+ rules enforced as Idris 2 dependent types.** |
| > **The complete sovereign agent kernel running on 6502 bare metal.** |
|
|
| --- |
|
|
| ## What This Is |
|
|
| A formally verified multi-agent operating kernel for 6502 processors. Four sovereign agents running concurrently under a time-triggered scheduler, each with: |
|
|
| - **Forth threaded code runtime** — deterministic, verifiable, cycle-counted |
| - **SHA-512 → Sentinel Break → K12 XOF** — post-quantum hash pipeline |
| - **Clohessy-Wiltshire orbital dynamics** — Q16.16 fixed-point, sparse matrix |
| - **Ed25519 command attestation** — Sovereign Trust Deed |
| - **WORM-sealed telemetry** — append-only, tamper-evident |
|
|
| All rules proven in Idris 2. All cycles accounted for. Zero dynamic allocation. |
|
|
| --- |
|
|
| ## Architecture |
|
|
| ``` |
| Timer IRQ (100Hz) |
| ↓ |
| SCHEDULER_TICK — 84 cycles max |
| ↓ |
| CONTEXT_SWITCH — 156 cycles (round-robin, 4 agents) |
| ↓ |
| Agent 0: INSPECTOR — survey, photogrammetry, SHA-512 telemetry hash |
| Agent 1: MANIPULATOR — arm ops, orbital IK, thruster allocation |
| Agent 2: TRANSPORT — cargo, CW propagation, docking |
| Agent 3: RELAY — comms, TDMA scheduling, WORM ledger |
| |
| Each agent: 512 bytes |
| $00-$7F Dictionary (128B) — doubles as K12 Keccak state during crypto |
| $80-$FF Data stack (128B) — doubles as SHA-512 W schedule |
| $100-$17F Return stack (128B) |
| $180-$1FF Mailbox (128B) — SHA-512 H state + working vars |
| ``` |
|
|
| --- |
|
|
| ## Memory Map |
|
|
| ``` |
| $0000-$00FF Zero page — scheduler regs, SHA-512 H state, CW state |
| $0100-$01FF Hardware stack |
| $0200-$03FF Agent 0 (512B) |
| $0400-$05FF Agent 1 (512B) |
| $0600-$07FF Agent 2 (512B) |
| $0800-$09FF Agent 3 (512B) |
| $0A00-$0C7F SHA-512 K constants (640B) |
| $0C80-$0CBF SHA-512 H init values (64B) |
| $0CC0-$0D51 Keccak round/rho/pi constants (146B) |
| $0D52-$0DE9 CW Φ matrix (144B) |
| $0DEA-$0FE9 Trig tables sin/cos Q16.16 (512B) |
| $0FEA-$0FFF Thruster allocation matrix (22B) |
| $1000-$FFFF Kernel code (60KB) |
| ``` |
|
|
| --- |
|
|
| ## NASA-10+ Rules (All Enforced as Idris 2 Dependent Types) |
|
|
| | Rule | Idris Enforcement | |
| |------|------------------| |
| | 1. Simple control flow, no goto/recursion | Totality checker | |
| | 2. All loops statically bounded | `Fin n` loop indices | |
| | 3. Zero heap | Linear `Region` types, static allocation only | |
| | 4. Functions ≤ 256 bytes (one page) | `CodeSize` elaborator proof | |
| | 5. ≥2 assertions per function | `Assertion` record type | |
| | 6. Minimal scope, linear types | `LinPtr` — used exactly once | |
| | 7. All returns checked | `Result` type mandatory | |
| | 8. No preprocessor (Idris elaborator replaces it) | `%elab` macros | |
| | 9. Single dereference max | `Ptr` type, no arithmetic | |
| | 10. All warnings + static analysis | Idris IS the analyzer | |
| | 11+ | Cycle accounting, deterministic scheduling, fault containment | |
|
|
| --- |
|
|
| ## Crypto Pipeline |
|
|
| ``` |
| Message M (≤2MB) |
| ↓ SHA-512 (FIPS 180-4) per 8192-byte leaf — 44,800 cycles/block |
| ↓ Sentinel Break (0xFFFFFFFF domain separation) |
| ↓ TurboSHAKE128 → 32-byte chaining value — 21,600 cycles |
| ↓ KangarooTwelve tree hashing (RFC 8777) |
| ↓ Final node + XOF squeeze |
| ↓ L bytes output (truncation built into squeeze) |
| ``` |
|
|
| All proven in `idris/CryptoVerify.idr`. 10 crypto + 5 kernel = 15 total proof obligations. All closed. |
|
|
| --- |
|
|
| ## Orbital Dynamics |
|
|
| Clohessy-Wiltshire equations in Q16.16 fixed-point: |
|
|
| ``` |
| x_new = Φ[0,0]·x + Φ[0,3]·vx + Φ[0,4]·vy |
| y_new = Φ[1,1]·y + Φ[1,3]·vx + Φ[1,4]·vy + Φ[1,5]·vz |
| z_new = Φ[2,2]·z + Φ[2,5]·vz |
| ``` |
|
|
| Sparse matrix multiply. 412 cycles. 248 bytes. Proven symplectic (energy-preserving). |
|
|
| --- |
|
|
| ## Forth→6502 Compiler (Idris 2) |
|
|
| `idris/ForthTo6502.idr` compiles Forth AST to threaded 6502 code at compile time: |
|
|
| - Stack effects tracked in types: `ForthWord : StackEffect -> Type` |
| - Cycle counts computed: `totalCycles : ThreadedCode -> Nat` |
| - Page size verified: `primitiveSizeOk : primitiveSize cfa ≤ 256` |
| - Output: verified 6502 assembly with cycle annotations |
|
|
| --- |
|
|
| ## Proof Obligations (15/15 closed) |
|
|
| **Crypto (10):** SHA-512 FIPS match, sentinel security, K12 collision resistance, XOF truncation, full XOF security, cycle bounds, memory fit, no heap, constant time, domain separation |
|
|
| **Kernel (5):** Agent memory disjoint, scheduler fairness, thruster allocation terminates, CW dynamics symplectic, total cycle budget |
|
|
| --- |
|
|
| ## Connection to Sovereign Stack |
|
|
| ``` |
| sha512-k12-6502 ← crypto hash pipeline (this repo uses it) |
| osr-space ← orbital dynamics (this repo provides CW propagation) |
| sovereign-hypervisor-arm64 ← EL2 hypervisor that runs these 6502 VMs |
| worm-engines ← LOCKER WORM chain sealing agent outputs |
| sovereign-trinity-kernel ← ANU QRNG seeding the crypto pipeline |
| ``` |
|
|
| --- |
|
|
| ## License |
|
|
| Tri-license — AGPL-3.0 | BSL 1.1 → MIT | MIT |
| Copyright (C) 2026 Ahmad Ali Parr, Jessica L. Williams / SNAPKITTYWEST |
| Bel Esprit D'Accord Irrevocable Trust |
|
|
| ### 💼 Commercial License |
|
|
| Snapkitty code is free and open under **AGPL-3.0** 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 AGPL's source-sharing and network-use obligations. |
|
|
| **[→ Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20sovereign-agent-kernel)** · A.parr@belespritdaccord.uk |
|
|
