File size: 1,823 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 | -- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001
-- Copyright (C) 2026 SNAPKITTYWEST / Sovereign Kernel Project
-- CLONE_GATE: sparse-router-formal::formal::invariants
--
-- Core safety invariants for the sparse router:
-- INV-1: Every routed task lands on exactly one worker deque
-- INV-2: Region ownership is well-formed (owner < numWorkers)
-- INV-3: Sparse edge sets reference valid workers
-- INV-4: Deque capacity is never exceeded
import SparseRouter.Types
import SparseRouter.Route
namespace SparseRouter.Invariants
open SparseRouter SparseRouter.Route
def RegionOwnerValid (state : RouterState) : Prop :=
∀ r : Fin MaxRegions,
match (state.regionTable r).owner with
| some w => w.val < state.numWorkers
| none => True
def SparseEdgesValid (state : RouterState) : Prop :=
∀ r : Fin MaxRegions,
∀ w ∈ (state.sparseEdges r).workers,
w.val < state.numWorkers
def DequeCapacityRespected (state : RouterState) : Prop :=
∀ i : Fin MaxWorkers,
(state.workers i).deque.count ≤ DequeCapacity
def TaskCountConserved (state : RouterState) (totalTasks : Nat) : Prop :=
(Finset.univ.sum fun i : Fin MaxWorkers => (state.workers i).deque.count) = totalTasks
structure WellFormedRouter (state : RouterState) : Prop where
owner_valid : RegionOwnerValid state
edges_valid : SparseEdgesValid state
deque_cap : DequeCapacityRespected state
workers_pos : state.numWorkers > 0
theorem route_preserves_uniqueness (state : RouterState) (t : Task)
(hw : state.numWorkers > 0) :
∃! w : WorkerId, routeDecisionWorker (rawRoute state t hw) = w := by
exact ⟨_, rfl, fun _ h => h.symm⟩
theorem sparse_traversal_bounded (edges : SparseEdgeSet) :
edges.count ≤ MaxSparseEdges :=
edges.inv_bounded
end SparseRouter.Invariants
|