| -- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001 |
| -- Copyright (C) 2026 SNAPKITTYWEST / Sovereign Kernel Project |
| -- CLONE_GATE: sparse-router-formal::formal::deque |
|
|
| import SparseRouter.Types |
|
|
| namespace SparseRouter.Deque |
|
|
| open SparseRouter |
|
|
| def push (d : WorkDeque) (t : Task) (h : d.count < DequeCapacity) : WorkDeque := |
| { tasks := d.tasks ++ [t] |
| count := d.count + 1 |
| inv_count := by simp [List.length_append]; omega |
| inv_cap := by omega } |
|
|
| def pop (d : WorkDeque) (h : d.count > 0) : Task × WorkDeque := |
| let last := d.tasks.getLast (by intro hempty; simp [hempty] at h; exact absurd d.inv_count (by omega)) |
| let rest := d.tasks.dropLast |
| (last, |
| { tasks := rest |
| count := d.count - 1 |
| inv_count := by |
| simp [List.length_dropLast, d.inv_count]; omega |
| inv_cap := by omega }) |
|
|
| theorem push_increases_count (d : WorkDeque) (t : Task) (h : d.count < DequeCapacity) : |
| (push d t h).count = d.count + 1 := by |
| simp [push] |
|
|
| theorem pop_decreases_count (d : WorkDeque) (h : d.count > 0) : |
| (pop d h).2.count = d.count - 1 := by |
| simp [pop] |
|
|
| theorem push_pop_identity (d : WorkDeque) (t : Task) |
| (hcap : d.count < DequeCapacity) : |
| let d' := push d t hcap |
| let hpos : d'.count > 0 := by simp [push]; omega |
| (pop d' hpos).1 = t := by |
| simp [push, pop, List.getLast_append] |
|
|
| end SparseRouter.Deque |
| |
