A counter-free real-time persistent queue

30 September 2026. Written construction and invariant proof with finite executable exploration. This note supplies a strict transport primitive for the persistent-filtering program. It does not yet realize the filtering interface.

1. Why this queue matters

The abstract filtering scheduler processes a deep carry while future filtering requests consume completed level states from the shallow end. A natural implementation therefore needs a persistent first-in, first-out transport with worst-case bounded work. An amortized two-list queue is not enough: branching from an old version can repeat its entire reversal.

Hood and Melville gave a purely functional real-time queue by distributing each reversal across later operations. Standard presentations use unbounded natural-number fields for front length, rear length, and rotation progress. Those fields are not legal finite labels in the present record model.

The result below removes those scalar fields. It thereby gives a direct, checkable application of the bounded simultaneous-record compiler beyond the palindrome construction.

2. Exact interface and target model

Let Gamma be a fixed finite payload alphabet. The abstract state is a FIFO word over Gamma. Operations are enqueue(x) for x in Gamma and promised legal dequeue. The observations are empty and, when nonempty, front. Every finite operation trace and every branch from an earlier version count.

The target has one root, immutable records, finite tags and payloads, fixed arity, a fixed old-access radius, and a bounded fresh batch per operation. There is no mutation, memo table, address arithmetic, pointer-identity test, scan, or unbounded integer. Empty lists and the idle status are fixed virtual records in the pointer-closed initialization.

Theorem 1 (counter-free strict queue). The FIFO interface above has a fully persistent record realization with record arity at most 6, old-access radius at most 3, and at most 12 fresh records per operation.

These are conservative construction bounds, not optima. Dequeue legality is promised. The realization preserves the abstract FIFO sequence and therefore all future empty and front observations under the queue interface. It does not preserve a canonical graph shape or physical record identity.

3. Finite record vocabulary

The construction uses these finite record kinds:

• List(x,next) for a payload list;
• Token(next) for a unary rotation-progress witness;
• Idle, Rev, App, and Done status records;
• one queue root containing pointers to the front list, rear list, status, and two balance-certificate lists.

The Rev status stores a token stack and four list pointers: the unprocessed front, reversed-front accumulator, unprocessed rear, and reversed-rear accumulator. App stores a token stack and two list pointers. All tags and payloads are finite because Gamma is fixed.

One exec microstep has the following structural cases:

1. Rev with nonempty front and rear moves one node from each source to its accumulator and pushes one token.
2. Rev with empty front and singleton rear changes to App.
3. App with a token moves one front-accumulator node to the result and pops one token.
4. App with no token changes to Done.

Each public queue operation performs two exec microsteps. A dequeue also invalidates one token when a rotation is in progress. These are the classical Hood-Melville status transitions, with the numerical ok field replaced by the token stack.

4. Eliminating the length comparison

The remaining numerical test in the usual presentation asks whether the rear has become longer than the front. Let

$$d=|F|-|R|.$$

While no new rotation is required, every enqueue or dequeue lowers d by exactly one. Instead of storing d, store two immutable list cursors whose remaining total number of nodes is d. A public operation removes one cursor node. Testing whether the certificate is empty is a finite tag test.

When the certificate is already empty, the just-performed operation makes the rear one node longer than the front and starts a rotation. The rear is cleared from the public queue state. The new logical front has length equal to the old front plus the old rear, so the new balance certificate is simply the pair of old list heads. Their nodes are reused as tokens; no traversal or copying is performed.

This is why two certificate pointers suffice. Their order is irrelevant because only their combined remaining length is used. Popping first from one and then from the other maintains the invariant

$$\text{remaining certificate nodes}=|F|-|R|. \tag{1}$$

The previous rotation has reached Idle before this certificate can be exhausted. Two exec steps per public operation are exactly the classical real-time schedule that establishes this deadline.

5. Correctness and resources

Erase the shapes of the balance-certificate lists and replace their combined remaining length by d. Replace the token stack by its length ok. Under this projection, every structural transition is the corresponding length-based Hood-Melville transition:

• pushing or popping a token is ok+1 or saturated ok-1;
• consuming a certificate node is d-1;
• resetting the two certificate cursors sets d to the new front length;
• the four exec cases and dequeue invalidation are unchanged.

Induction on the operation trace proves (1), equality between token count and ok, and equality of the projected queue with the abstract FIFO word. The classical queue invariant then gives exact front, empty, enqueue, and promised dequeue behavior. Because every transition allocates a new root and never changes an old record, the same induction applies independently to every branch from every earlier version.

For the resource bound, the second exec step can inspect one successor of a list node exposed by the first. Radius 3 from the old queue root therefore suffices to select a finite combined transition plan. An exec step creates at most two payload-list nodes, one token, and one status record. Two steps, one public enqueue node, and the new queue root fit within 12 records. Fresh records may point to other records in the same simultaneous batch. The reviewed compiler therefore gives a scaffold construction of distance at most 4 and degree at most max(1,s+12q) for its fixed root count s and arity bound q<=6. This is a construction bound, not an optimum.

The scaffold simulates this queue controller on the same operation words. A later scaffold-to-PEG transfer would introduce exactly one reversal. No such language claim is needed for the filtering work here.

6. Verification scope

The checker implements only the structural token and two-cursor algorithm. It never consults a length in its transition function. Lengths are used separately in the audit to check (1). It explores branching versions, compares every legal transition with a raw FIFO word, and records conservative conceptual allocation counts.

This finite exploration corroborates the induction but does not prove it. The resource count is an audit of the stated constructor plan, not a compiler or proof-assistant result.

7. What this does not solve

A single FIFO does not yet implement the filter tower. Carries from one append produce completed levels in increasing-depth order, but a later append can create a newer shallow cascade that supersedes only a prefix of those levels. For example, an older job may have completed levels 1, 2, and 3; a newer job may then replace levels 1 and 2 but terminate before level 3. The correct depth order is then

$$\text{new }1,\quad \text{new }2,\quad \text{old }3,$$

not either FIFO production order. Thus the queue theorem settles strict persistent transport, but not prefix-overlay alignment.

The next exact primitive is a persistent nested-prefix transport supporting:

1. start a new overlay at logical depth 1;
2. extend the active overlay by one deeper state;
3. expose the newest state at depth 1; and
4. shift all logical depths down by one when P is applied.

Its operations must have finite tags, bounded local access, and bounded fresh allocation. A stack of overlay lists is not enough because shifting would have to advance every hidden layer or retain a lazily checkable common offset. That alignment problem, not FIFO reversal or an integer counter, is now the remaining forward-fragment bottleneck.

8. Relation to primary and verified sources

Hood and Melville’s Real Time Queue Operations in Pure LISP introduced the distributed-reversal queue. Okasaki’s Purely Functional Data Structures separates ordinary amortization from persistent scheduling and presents both real-time queue and global-rebuilding techniques. The Archive of Formal Proofs contains a Hood-Melville Queue formalization of the standard length-based presentation.

Those sources establish the queue design and its conventional correctness. The additional argument here is the structural elimination of every unbounded scalar needed for this bounded-record model, followed by the exact compiler resource accounting. Novelty of that adaptation has not been established.