File size: 2,537 Bytes
29f097e 32b4893 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 | -- 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
|