Snapkitty/sovereign-agent-kernel

Sovereign Agent Kernel — 6502

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