Bounded-threshold erasure in a real-time catenable deque

30 September 2026. Source-to-model resource audit and a general structural replacement lemma. This note removes the unbounded-scalar objection to the efficient catenable-deque presentation used by the segmented filtering construction. It does not yet prove that the hand-written OCaml source has the same sequence semantics as the separately verified Rocq implementation.

1. Exact question and source snapshot

The preceding segmented-transport theorem reduces every request in the forward repeated-filtering controller to at most three operations on a strict, fully persistent catenable sequence. The missing hypothesis requires one root into immutable, finite-labelled records of fixed arity, fixed old-access radius, and bounded fresh allocation per operation. Mutation, memoization, pointer identity, scans, amortized work, and unbounded scalar fields are forbidden.

This audit considers only empty, rear insertion inject, front removal pop, and concat. It deliberately excludes length, random access, folds, iteration, bulk construction, and reversal.

The source is the companion repository for Viennot, Wendling, Gueneau, and Pottier’s Verified Purely Functional Catenable Real-Time Deques. The v3 paper was posted on 3 July 2026. The last repository commit before that posting is

3516131f0dae5e557c20b75aace7dee5a5084757.

At that commit:

• lib/deque_core.ml has SHA-256 e76266335ba922f9d871f25677f7f9b18d9f6f4188e6ac896ef8026ec427ef76;
• lib/cadeque_core.ml has SHA-256 003bddf1c77dc13b64de882ea1d04a9229d688a1b9ad78ee4b5ab06fbc4034e7.

The repository head inspected on 30 September 2026 was 503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0. Between the v3 snapshot and that head, the only change under lib/ makes five phantom marker types private. It does not change an operation or a runtime branch.

2. A general bounded-threshold erasure lemma

Let D be a fully persistent deque. From every retained version, pop returns either None or an element and another persistent version. Suppose one pop has record arity at most q_D, old-access radius at most r_D, and fresh allocation at most A_D.

For a fixed natural number K, define the observation

$$\operatorname{cut}_K(d)= \begin{cases} |d|,&|d|<K,\\ \mathsf{AtLeast}(K),&|d|\geq K. \end{cases}$$

Theorem 1 (bounded-threshold erasure). cut_K can be computed without a stored length, mutation, restoration, or traversal. Starting from d_0=d, perform at most K successive calls to pop. If the call on d_i returns None, report i. If all K calls succeed, report AtLeast(K). Retain any intermediate root or extracted element required by the client.

The construction is fully persistent and has the conservative bounds

$$q\leq q_D,\qquad r\leq K r_D,\qquad A\leq K A_D. \tag{1}$$

The symmetric claim holds with eject. If the client already knows a fixed lower bound, probes below it may be omitted.

Proof

After i successful calls, d_i represents the original sequence with its first i elements removed. This is an induction on i from deque semantics. The next call fails exactly when the original length is i. If the first K calls all succeed, the original length is at least K. Persistence leaves d_0 and every retained intermediate version unchanged, so no restoration is needed. Sequential composition of at most K bounded transition plans gives (1). The same induction from the rear proves the eject version. $\square$

The fixed cutoff is essential. This lemma does not recover an exact unbounded length and does not cover a data-dependent threshold. A saturated finite counter is not a substitute: after enough removals, it cannot tell when a long sequence crosses the threshold. The theorem works because it asks the persistent structure a bounded number of local questions at the moment the answer is needed.

The hypothesis is syntactically checkable: list every length observation and show that each compares with a constant bounded by one global K. No realization conclusion is assumed by this check.

3. Where the integers occur

There are two length layers in the hand-written OCaml distribution.

1. lib/cadeque.ml is a public convenience wrapper with an exact integer length. The required interface can bypass it and call Cadeque_core directly. The core already returns None on an empty pop.
2. Cadeque_core.Buffer uses Deque.t, whose wrapper also carries an integer length. Inside the required slice, the integer is observed only by four occurrences of Deque.length, in has3, has7s, has7p, and has8.

Replace the buffer representation by Deque_core.deque, with the same empty, push, inject, pop, and eject operations. The reversal bit in the wrapper also disappears: buffer construction starts unreversed and the core never requests reversal.

The four size cases become structural probes:

In an At_least_7 branch, the result needs the original deque minus two end elements, not the deeply probed version. The algorithm retains the version after the second pop or eject and probes a descendant of it. This is exactly where full persistence matters.

has1 and has5 are already structural. The sole polymorphic equality in Deque_core, d = empty, is unnecessary: match the root against T (Ending B0) instead. The assertion in Buffer.two is outside the reachable slice. The folds and bulk make function are also unreachable and are omitted. The remaining assertions are impossible branches certified by the phantom lower-bound types; a total finite transition table may map those unreachable cases arbitrarily.

4. Exact reachable source slice

After the replacement above, the required public operations reach the following helpers. Functions separated by commas are distinct source bindings.

Finite vectors and structural buffers. vector_fold_right, vector_fold_left; empty, push, inject, pop, eject, single, pair, triple, pop2, eject2, has1, push2, inject2, push3, inject3, pop3, eject3, push6, inject6, has3, has3p, has3s, has5, has7s, has7p, pop5, has8, push_vector, inject_vector, has3p8, push5, inject5, push_5vector, inject_5vector, and inject8.

Non-catenable deque core. green_push, green_inject, green_pop, green_eject, yellow_push, yellow_inject, yellow_pop, yellow_eject, buffer_push, buffer_inject, buffer_pop, buffer_eject, prefix_rot, suffix_rot, prefix23, suffix23, suffix12, prefix_decompose, suffix_decompose, buffer_unsandwich, buffer_halve, to_yellow, to_red, green_prefix_concat, green_suffix_concat, prefix_concat, suffix_concat, make_small, green_of_red, ensure_green, make_yellow, make_red, empty, is_empty, push, inject, pop, and eject.

Catenable core. push_left_node, inject_right_node, push_only_node, inject_only_node, push_left_packet, inject_right_packet, push_only_packet, inject_only_packet, single_node, single_packet, single_chain, push_left_chain, inject_right_chain, push_ne_chain, inject_ne_chain, is_empty_chain, semi_push, semi_inject, to_triple_coloring, triple_of_chain, chain_of_triple, left_of_only, right_of_only, stored_of_right, stored_of_left, is_empty_node, left_of_pair, right_of_pair, make_left, make_right, semi_concat, orange_tc, pop_left_green, eject_right_green, pop_only_green, eject_only_green, sandwich_only_green, adapt_to_prefix, only_of_right, adapt_to_suffix, only_of_left, pop_pair_green, eject_pair_green, sandwich_pair_green, pop_green, eject_green, sandwich_green, make_green_prefix, make_green_suffix, extract_prefix, extract_suffix, ensure_green_prefix, ensure_green_suffix, green_of_red_left, green_of_red_right, make_green_only, green_of_red_only, ensure_green_single, ensure_green, regularize, empty, push, inject, pop, and concat.

The internal eject helpers remain reachable during front-pop regularization, even though public rear removal is not in the required interface.

The runtime sum constructors are also finite. In the deque core they are B0 through B5, Hole, Packet, G, Y, R, Ending, Chain, Underflow, Ok, Overflow, Alone, Sandwich, None, Some, and T. In the catenable core they are V0 through V6; the finite threshold-result constructors; EN, GN, YN, ON, RN; Only, Only_end, Left, Right; G, R; Small, Big; Hole, Single_child, Pair_yellow, Pair_orange; Packet; Empty, Single, Pair; Stored_buffer; GT, YT, OST, OPT, RT; Triple; Not_enough, Ok, End; Alone, Sandwich; S, T; Is_empty, Not_empty; None, and Some. Repeated constructor names live in distinct types but need only finitely many tags after disambiguation.

5. Record certificate and explicit conservative bounds

Encode every tuple and algebraic constructor by one finite-tagged immutable record. Nested element pairs use ordinary binary pair records. The largest source tuple has eight fields, so

$$q_C\leq 8. \tag{2}$$

The two core files and color declarations occupy 67,018 source characters at the audited head. The displayed structural replacements keep the closed required slice below 80,000 characters. After defunctionalizing the two vector folds, every higher-order call has one of the finitely listed targets. The closed call graph has no cycle: neither core contains let rec, a loop, a mutable cell, or an iteration primitive on the required path.

For a completely explicit, deliberately enormous construction bound, inline the closed call graph and sum all branches. A directed acyclic call graph with fewer than 80,000 syntax symbols has fewer than $2^{100000}$ dynamic source-action occurrences in one inlined operation, even after multiplying by the number of syntax sites. One pointer read or one constructor allocation per occurrence is a safe overestimate. Thus the restricted source admits

$$r_C < 2^{100000},\qquad A_C < 2^{100000}. \tag{3}$$

These are source-certificate bounds, not useful estimates and certainly not optima. They exist to close the logical gap between “nonrecursive” and the FPRD model’s demand for named constants. A later mechanical inliner should replace (3) by small bounds.

Initialization is the fixed value T Empty for the catenable core and T (Ending B0) for every empty structural buffer. Every operation allocates new immutable records and reuses old pointers; no old record is modified. The structural probes allocate only the bounded temporary versions already counted in (3). Old versions remain valid on every branch.

Combining (2)-(3) with the segmented-transport construction gives formal but astronomical conditional controller bounds

$$q\leq 8,\qquad r<3\cdot2^{100000}+4,\qquad A<3\cdot2^{100000}+8,$$

before the simultaneous-record compiler adds one scaffold layer. These are construction bounds, not optimality claims.

6. What is proved, and what is not

The bounded-threshold lemma is a written unbounded proof. Its application to the source is a source-to-resource certificate: all exact integers and all recursive or iterative control have been removed from the required runtime slice, and explicit finite arity, radius, allocation, and initialization bounds have been supplied.

The companion checker compares the four length-based classifications with their structural-probe replacements on labelled sequences of lengths 0 through 64 and on branching persistent traces. It also records the pinned hashes and static source counts. These finite checks corroborate the source audit; they do not prove Theorem 1 or OCaml functional correctness.

One semantic obligation remains. The authors prove the Rocq implementation correct, but explicitly state that there is no formal connection between it and the efficient hand-written OCaml implementation. Their testing of the OCaml implementation is substantial evidence, not a theorem. The present argument proves that replacing the four size tests preserves the behavior of that OCaml source, assuming the standard deque semantics of its building block. It does not prove the approximately sixty-helper refinement from the modified OCaml core to abstract sequence concatenation.

Consequently the forward filtering controller is not yet unconditional. The resource-model obstruction has been removed; the decisive remaining question is semantic correspondence. The shortest credible route is a helper-by-helper simulation from the modified OCaml algebraic states to the verified Rocq model functions, or an independent fringe-preservation proof for the modified source. Failure of that proof would concern this presentation only, not every catenable sequence or every filtering representation.

The result preserves abstract sequence behavior, if that final refinement is established. It does not preserve physical graph identity or arbitrary future scaffold-context observations. It concerns one fixed forward controller and makes no language-recognition or PEG claim. Any later scaffold-to-PEG transfer introduces exactly one reversal.

7. Literature and contribution boundary

Kaplan and Tarjan established the purely functional real-time catenable-deque construction. Viennot, Wendling, Gueneau, and Pottier supplied the first executable OCaml presentation and a separately machine-checked Rocq development. Their paper emphasizes both the absence of recursive functions in the efficient implementation and the lack of a formal OCaml-to-Rocq link. It also explains that the buffer indices express only constant lower bounds.

The imported ingredients are their data structure, its invariants, and the verified Rocq semantics. The additional argument here is the general bounded-threshold erasure lemma, its exact application to all four size tests, and the resulting scalar-free bounded-record source certificate. Novelty of this observation has not been established by a comprehensive literature search.

Primary sources:

• Viennot, Wendling, Gueneau, and Pottier, arXiv v3
• Companion source repository
• Kaplan and Tarjan, Purely Functional, Real-Time Deques with Catenation