package ktdeque

A purely-functional, persistent double-ended queue with worst-case O(1) push, pop, inject and eject, plus worst-case O(1) catenation. The implementation is extracted from a Rocq (Coq 9.1) formalization whose keystone theorems are closed with zero admits: totality, sequence preservation, the regularity invariant, and a constant per-operation cost bound, for both the section-4 deque (deque_wc_o1_) and the section-6 catenable deque (cat_keystone_ + cat_wc_o1). The package exposes an idiomatic interface -- open Ktdeque and use the Deque module (push/inject/pop/eject) or Cadeque (the same, plus concat) -- over the extracted code (the raw extraction is available as the internal sub-library ktdeque.extracted). On the benchmark suite the extracted artifact is faster than Viennot et al.'s hand-written OCaml cadeque on every workload at n=1M.