Module KTDequeSource

KTDeque - Rocq-extracted persistent real-time deque

A purely functional deque extracted from the Rocq development of the Kaplan-Tarjan real-time design. Every value of type kChain is an immutable snapshot; an operation returns a new snapshot sharing structure with the old one, so you can fork the deque, mutate one branch, and the other branch is unaffected.

This module is the OCaml extraction of the Rocq formalisation, hosted at https://github.com/yurug/kaplan2. The public theorem bundle for the extracted kt4 operation family lives in rocq/KTDeque/DequePtr/PublicTheorems.v. It packages sequence correctness, regularity preservation, bounded green_of_red_k dispatch, sufficient no-Fail preconditions, and a numeric bridge from the dispatch bound to the packet one-repair constants. A closed counterexample shows the reusable totality-state predicate is not itself push-closed without level/future-repair closure; the theorem bundle now also exposes a level-aware public-state candidate for level-0 inputs. It also derives the Green-tail and nested red-packet repair witnesses from shape + levels. Preserving that candidate, deriving the remaining bottom repair witnesses, and completing the pure-to-imperative cost refinement remain release-gate obligations before making an unqualified mechanically verified WC O(1) claim. For *why* the algorithm is correct and elegant — why "no two reds adjacent" delivers worst-case O(1), why packets aggregate yellow runs into a single allocation — read kb/spec/why-bounded-cascade.md first.

Quick start

  open KTDeque

  let push_or_fail x q =
    match push_kt2 (Coq_E.base x) q with
    | Some q' -> q'
    | None    -> failwith "regularity violated"

  let q = empty_kchain
  let q = push_or_fail 1 q
  let q = push_or_fail 2 q
  (* q now holds [2; 1] *)

  let xs = kchain_to_list q  (* [2; 1] *)

See also the hello example in the project monorepo for a fully runnable program.

Public API: where to look

Use one of the two operation families and the helpers below. Everything else is an internal extraction artefact (see Internal: extraction prelude at the bottom of this file).

Operations:

• empty_kchain, push_kt2, pop_kt2, inject_kt2, eject_kt2, kchain_to_list — the kt2 family, option-returning, idiomatic with monadic let*.
• push_kt4, pop_kt4, inject_kt4, eject_kt4 — the kt4 family, returns flat sum types push_result and pop_result. Equivalent semantics to kt2 but saves one allocation per successful op. Prefer for hot paths.

Element wrapping:

• Coq_E.base — wrap a base value into the level-tagged element type Coq_E.t. Required because the extracted deque stores level-l elements (sub-trees of paired-up base elements) rather than naked \'a; level-0 elements are exactly base values.
• Coq_E.to_list — flatten a level-l element back to a list of base values.

Why are there so many push_* functions?

The Rocq development proves several variants of each operation so that some lemmas can be stated against the variant most convenient for that proof, then transported to the production variant via equivalence theorems. Specifically:

• push_chain / push_chain_naive: partial naive push (no overflow handling). Internal building block.
• push_chain_full / push_chain_rec: recursive cascade. O(log n) per call — these are *proof artefacts*, not for production use. See §5 of why-bounded-cascade.md.
• push_kt: an early version with implicit colours. Superseded.
• push_kt2: explicit-colour, non-recursive bounded-cascade family. This is the clarity-oriented public code path.
• push_kt3: push_kt2 with yellow_wrap inlined for the Yellow fast path; same semantics, smaller constant factor.
• push_kt4: push_kt3 with option (X * Y) return replaced by a flat 2-constructor sum type, saving one allocation per successful op.

Use push_kt2 for clarity, push_kt4 for performance. The public theorem bundle currently targets the extracted kt4 family. The other variants are not part of the supported public API.

A note for re-extraction

This .mli file is checked into git as a snapshot in the project monorepo. The body (every type and val declaration) is verbatim Coq extraction output; the surrounding (** ... *) documentation is hand-written. When regenerating, please preserve the literate headers and per-binding doc comments.

Internal: extraction prelude

Coq's extracted module needs a small prelude of type aliases and helpers. None of this is part of the user-facing API.

Element abstraction

The extracted deque stores \'a Coq_E.t values, not naked \'a. A \'a Coq_E.t is a *level-l element*: at level 0 it is just an \'a; at level 1 it is a pair of two \'as; at level l it is a balanced binary tree of 2^l base values. This is what makes the deque branch binarily as it descends through nested packets (see why-bounded-cascade.md §1 for the structural picture).

User code only needs three of these functions:

• Coq_E.base to wrap an \'a into a level-0 \'a Coq_E.t before calling push_kt2 / inject_kt2 / push_kt4 / inject_kt4;
• Coq_E.to_list to extract the underlying \'a values from whatever the deque returns at the top of pop / eject;
• Coq_E.level for diagnostics (the public ops are intended to return level-0 elements at the public surface, so Coq_E.level e = 0 is a reasonable assertion).

pair and unpair are internal — the deque uses them when cascading.

ElementTree is the canonical instance; the deque uses it via the alias Coq_E.

Buffer (Buf5) — internal storage at every level

A \'x buf5 holds 0 to 5 elements at one chain level. The buffer's *colour* is determined by its size:

• 0 or 5 elements: Red — next op underflows or overflows;
• 1 or 4 elements: Yellow — next op safe in at least one direction;
• 2 or 3 elements: Green — next op safe in both directions.

See why-bounded-cascade.md §2 for the regularity invariant that combines these colours. User code never sees buf5 directly.

Internal: buffer-level operations

Building blocks for the chain-level operations above. Not part of the public API.

Packet and Chain — the recursive shape

\'a packet is a *yellow run*: a nest of PNode pre inner suf layers terminated by Hole. In the C runtime, an entire packet is allocated as a single contiguous block — that aggregation is what keeps a chain repair O(1) instead of O(yellow-run-length).

\'a chain is the older "implicit colour" representation, kept for cross-checks. The kChain type below is the production representation with explicit colour tags. Use kChain for new code.

Internal: chain-level building blocks (Chain, not kChain)

These work on the older implicit-colour chain type. The _full / _rec families are *recursive* (O(log n) per call) — they are proof artefacts used as targets for some Rocq lemmas, NOT for end-user consumption. See why-bounded-cascade.md §5 for the proof-artefact-vs-production-code distinction.

For the production WC O(1) ops, use the kt2 or kt4 family above.

Colours and regularity tags

Coq_E is the deque's chosen ELEMENT instance — a transparent alias for ElementTree. All public deque ops accept and return \'a Coq_E.t; user code typically goes through Coq_E.base / Coq_E.to_list only. The implementation under Coq_E is the same as under ElementTree (both are extractions of the same Rocq module), but the verified ops reference Coq_E specifically, so use it for type-equality with the deque's API surface.

Internal: colour-dispatched buffer-level helpers

Used by the chain-level ops above. green_* are partial on Red-sized inputs; yellow_* tolerate one direction of Yellow.

Internal: small-buffer constructors and decomposers

Build B2/B3 buffers from optional plus-pair forms; case-split a buffer into "underflow / ok / overflow" branches. Used inside make_small and the concat helpers.

Internal: cross-buffer concat helpers

{green,}_prefix_concat (b1, b2) redistributes elements between two adjacent buffers so the result has acceptable colours. Used inside green_of_red Cases 2 and 3.

Internal: rebalance primitives

make_small (the depth-1 collapse), green_of_red (the three- case red-to-green fix), ensure_green (the fire-or-noop dispatch). These are the heart of the WC-O(1) bound — see why-bounded-cascade.md §2-§3. Public callers should use push_kt2 / push_kt4 etc., which compose these primitives correctly.

Internal: superseded kt family

An early version with implicit colours, kept for proof cross-checks. Use the kt2/kt4 families above instead.

Public API: kt2 family (option-returning, recommended)

The verified worst-case O(1) deque, with option return types that integrate with monadic let*. All four ops:

• return Some _ on success;
• return None only on a regularity-invariant violation (which, provably, cannot happen on a sequence of inputs starting from empty_kchain — but the option is exposed because the extracted ops are total functions over arbitrary kChain values, not only the ones reachable from empty).

Sequence semantics (proved in OpsKTSeq.v):

• push_kt2 x q = Some q' implies kchain_to_list q' = Coq_E.to_list x @ kchain_to_list q.
• inject_kt2 q x = Some q' implies kchain_to_list q' = kchain_to_list q @ Coq_E.to_list x.
• pop_kt2 q = Some (x, q') implies kchain_to_list q = Coq_E.to_list x @ kchain_to_list q'.
• eject_kt2 q = Some (q', x) implies kchain_to_list q = kchain_to_list q' @ Coq_E.to_list x.

Cost (proved in Footprint.v): each op runs in worst-case O(1) primitive heap operations.

Optimized variants: kt3 family

The kt3 variants are operationally equivalent to kt2 but inline yellow_wrap / ensure_green_k / make_red_k into the body of each op and special-case the common "tail is not Red" path. Same return types as kt2; same correctness theorems (proved by _kt3_seq equivalences in OpsKTSeq.v). Smaller constant factor in extracted OCaml code.

Public API: kt4 family (no-option, allocation-optimal)

The kt4 variants replace the nested option (X * Y) return with a flat 2-constructor sum type: push_result for push_kt4 / inject_kt4, pop_result for pop_kt4 / eject_kt4.

OCaml extracts option (X * Y) as a Some block holding a pointer to an (X, Y) tuple block — two allocations per successful op. A flat sum is one block. Hot loops that bench in the 25–80 ns/op range are allocation-bound; this saves one allocation and is the family used by the bench's headline numbers.

Same correctness as kt2: the _kt4 = _kt2 equivalence is proved at the bottom of OpsKTSeq.v.