Relicense under the Sovereign Leviathan covenant; remove MIT and Apache

29f097e verified 14 days ago

2.56 kB

-- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001
-- Copyright (C) 2026 SNAPKITTYWEST / Sovereign Kernel Project
-- CLONE_GATE: sparse-router-formal::formal::convergence
--
-- Novel convergence proof: region ownership stabilizes.
--
-- Method: define a potential function Φ over the router state equal to
-- the number of region-ownership transitions remaining before fixpoint.
-- Show that each raw_route call either:
--   (a) hits the owner fast path (Φ unchanged), or
--   (b) assigns ownership (Φ decreases by 1, bounded below by 0).
-- Since Φ ∈ ℕ and is non-increasing, the system converges in at most
-- MaxRegions steps to a stable ownership assignment.

import SparseRouter.Types
import SparseRouter.Route
import SparseRouter.Invariants

namespace SparseRouter.Convergence

open SparseRouter SparseRouter.Route

def unownedRegions (state : RouterState) : Nat :=
  (List.range MaxRegions).countP fun i =>
    if h : i < MaxRegions then
      (state.regionTable ⟨i, h⟩).owner = none
    else false

def potential (state : RouterState) : Nat := unownedRegions state

theorem owner_fast_path_preserves_potential (state : RouterState) (t : Task)
    (hw : state.numWorkers > 0)
    (howner : (state.regionTable t.memoryRegion).owner ≠ none) :
    ∃ w, rawRoute state t hw = .ownerFastPath w := by
  simp [rawRoute]
  match h : (state.regionTable t.memoryRegion).owner with
  | some w => exact ⟨w, rfl⟩
  | none => exact absurd h howner

theorem sparse_edge_assigns_owner (state : RouterState) (t : Task)
    (hw : state.numWorkers > 0)
    (hunowned : (state.regionTable t.memoryRegion).owner = none)
    (hcand : bestCandidate state.workers (state.sparseEdges t.memoryRegion).workers t = some (w, s)) :
    rawRoute state t hw = .sparseEdgeBest w s := by
  simp [rawRoute, hunowned, hcand]

theorem potential_bounded : ∀ state : RouterState,
    potential state ≤ MaxRegions := by
  intro state
  simp [potential, unownedRegions]
  exact List.countP_le_length _

theorem convergence_in_finite_steps :
    ∀ state : RouterState,
    potential state = 0 →
    ∀ r : Fin MaxRegions, (state.regionTable r).owner ≠ none := by
  intro state hpot r
  simp [potential, unownedRegions] at hpot
  by_contra h
  push_neg at h
  have : (List.range MaxRegions).countP (fun i =>
    if h : i < MaxRegions then (state.regionTable ⟨i, h⟩).owner = none else false) > 0 := by
    apply List.countP_pos.mpr
    exact ⟨r.val, List.mem_range.mpr r.isLt, by simp [r.isLt, h]⟩
  omega

end SparseRouter.Convergence

	-- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001
	-- Copyright (C) 2026 SNAPKITTYWEST / Sovereign Kernel Project
	-- CLONE_GATE: sparse-router-formal::formal::convergence
	--
	-- Novel convergence proof: region ownership stabilizes.
	--
	-- Method: define a potential function Φ over the router state equal to
	-- the number of region-ownership transitions remaining before fixpoint.
	-- Show that each raw_route call either:
	-- (a) hits the owner fast path (Φ unchanged), or
	-- (b) assigns ownership (Φ decreases by 1, bounded below by 0).
	-- Since Φ ∈ ℕ and is non-increasing, the system converges in at most
	-- MaxRegions steps to a stable ownership assignment.

	import SparseRouter.Types
	import SparseRouter.Route
	import SparseRouter.Invariants

	namespace SparseRouter.Convergence

	open SparseRouter SparseRouter.Route

	def unownedRegions (state : RouterState) : Nat :=
	(List.range MaxRegions).countP fun i =>
	if h : i < MaxRegions then
	(state.regionTable ⟨i, h⟩).owner = none
	else false

	def potential (state : RouterState) : Nat := unownedRegions state

	theorem owner_fast_path_preserves_potential (state : RouterState) (t : Task)
	(hw : state.numWorkers > 0)
	(howner : (state.regionTable t.memoryRegion).owner ≠ none) :
	∃ w, rawRoute state t hw = .ownerFastPath w := by
	simp [rawRoute]
	match h : (state.regionTable t.memoryRegion).owner with
	\| some w => exact ⟨w, rfl⟩
	\| none => exact absurd h howner

	theorem sparse_edge_assigns_owner (state : RouterState) (t : Task)
	(hw : state.numWorkers > 0)
	(hunowned : (state.regionTable t.memoryRegion).owner = none)
	(hcand : bestCandidate state.workers (state.sparseEdges t.memoryRegion).workers t = some (w, s)) :
	rawRoute state t hw = .sparseEdgeBest w s := by
	simp [rawRoute, hunowned, hcand]

	theorem potential_bounded : ∀ state : RouterState,
	potential state ≤ MaxRegions := by
	intro state
	simp [potential, unownedRegions]
	exact List.countP_le_length _

	theorem convergence_in_finite_steps :
	∀ state : RouterState,
	potential state = 0 →
	∀ r : Fin MaxRegions, (state.regionTable r).owner ≠ none := by
	intro state hpot r
	simp [potential, unownedRegions] at hpot
	by_contra h
	push_neg at h
	have : (List.range MaxRegions).countP (fun i =>
	if h : i < MaxRegions then (state.regionTable ⟨i, h⟩).owner = none else false) > 0 := by
	apply List.countP_pos.mpr
	exact ⟨r.val, List.mem_range.mpr r.isLt, by simp [r.isLt, h]⟩
	omega

	end SparseRouter.Convergence