| -- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001 |
| -- Copyright (C) 2026 SNAPKITTYWEST / Sovereign Kernel Project |
| -- CLONE_GATE: sparse-router-formal::formal::route |
| -- |
| -- Formal model of raw_route. The three-phase structure: |
| -- Phase 1: region-owner fast path |
| -- Phase 2: sparse edge traversal (bounded fan-out) |
| -- Phase 3: least-loaded fallback |
|
|
| import SparseRouter.Types |
| import SparseRouter.Scoring |
|
|
| namespace SparseRouter.Route |
|
|
| open SparseRouter SparseRouter.Scoring |
|
|
| inductive RouteDecision where |
| | ownerFastPath (w : WorkerId) |
| | sparseEdgeBest (w : WorkerId) (score : Int) |
| | leastLoadedFallback (w : WorkerId) |
| deriving Repr |
|
|
| def routeDecisionWorker : RouteDecision → WorkerId |
| | .ownerFastPath w => w |
| | .sparseEdgeBest w _ => w |
| | .leastLoadedFallback w => w |
|
|
| def bestCandidate (workers : Fin MaxWorkers → Worker) (candidates : List WorkerId) |
| (t : Task) : Option (WorkerId × Int) := |
| candidates.foldl (fun acc wid => |
| let s := computeScore (workers wid) t |
| match acc with |
| | none => some (wid, s) |
| | some (_, bestScore) => if s > bestScore then some (wid, s) else acc |
| ) none |
|
|
| def selectLeastLoaded (workers : Fin MaxWorkers → Worker) |
| (n : Nat) (hn : n > 0) (hbound : n ≤ MaxWorkers) : WorkerId := |
| let candidates := List.range n |>.filterMap fun i => |
| if h : i < MaxWorkers then some ⟨i, h⟩ else none |
| match candidates with |
| | [] => ⟨0, by omega⟩ |
| | hd :: tl => |
| tl.foldl (fun best wid => |
| if (workers wid).deque.count < (workers best).deque.count |
| then wid else best |
| ) hd |
|
|
| def rawRoute (state : RouterState) (t : Task) |
| (hw : state.numWorkers > 0) : RouteDecision := |
| let r := t.memoryRegion |
| let entry := state.regionTable r |
| match entry.owner with |
| | some owner => .ownerFastPath owner |
| | none => |
| let edges := state.sparseEdges r |
| match bestCandidate state.workers edges.workers t with |
| | some (w, s) => .sparseEdgeBest w s |
| | none => .leastLoadedFallback |
| (selectLeastLoaded state.workers state.numWorkers hw state.inv_workers_bound) |
|
|
| theorem raw_route_always_returns_worker (state : RouterState) (t : Task) |
| (hw : state.numWorkers > 0) : |
| ∃ w, routeDecisionWorker (rawRoute state t hw) = w := by |
| exact ⟨_, rfl⟩ |
|
|
| theorem owner_fast_path_deterministic (state : RouterState) (t : Task) |
| (hw : state.numWorkers > 0) |
| (howner : (state.regionTable t.memoryRegion).owner = some w) : |
| rawRoute state t hw = .ownerFastPath w := by |
| simp [rawRoute, howner] |
|
|
| end SparseRouter.Route |
|
|
