File size: 1,370 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 | -- 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
|