Relicense under the Sovereign Leviathan covenant; remove MIT and Apache

29f097e verified 14 days ago

1.82 kB

-- 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

	-- 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