Finite-boundary splicing closes green pop

Working research note, 30 September 2026.

The broader goal is to understand when past computation can remain usable through finite rules, bounded local access and bounded allocation. The specific question here is whether the remaining pair-chain branch of the catenable deque’s pop_green operation admits the same local-view factorization as the single-chain branch.

It does. The left view either retains a valid residual view or underflows to a fixed boundary of exactly six stored entries. In the first case, the residual left chain is paired with the unchanged right chain. In the second, those six entries are spliced in front of the right view and converted back to one only chain. Both paths preserve the exact order of arbitrary stored-word blocks.

This proves the complete pop_green sequence contract for the inspected source algebra, under explicit buffer contracts. Combined with the preceding single-chain certificate, pop_green is no longer an assumed semantic predecessor of the prefix-repair theorem. The buffer implementation and the other prefix-repair helpers retain their separately stated obligations.

The deque algorithm and its stronger existing Rocq theorem belong to Viennot, Wendling, Gueneau and Pottier. The inspected companion source is pinned to one commit. The additional result is our finite-boundary certificate decomposition and its connection to bounded persistent-record compilation. Novelty of this exact formulation remains unestablished.

1. A reusable finite-boundary lemma

Let $L,R,C,B,X$ be sets with word interpretations $\lambda,\rho,\gamma,\beta,\chi$ into a free monoid $\Gamma^*$. Suppose:

1. A pair representation has meaning $\lambda(l)\rho(r)$.

2. A local left-pop operation returns $x:X$ and either a boundary $b:B$ or a residual left view $l':L$, satisfying respectively

   $$\lambda(l)=\chi(x)\beta(b),\qquad \lambda(l)=\chi(x)\lambda(l').$$

3. A boundary splice $f:B\times R\to C$ satisfies

   $$\gamma(f(b,r))=\beta(b)\rho(r).$$

4. Residual pairing represents $\lambda(l')\rho(r)$.

Lemma (finite-boundary splice). The operation that uses $f(b,r)$ in the boundary branch and pairs $(l',r)$ in the residual branch returns $x$ and a residual representation $c$ satisfying

$$\lambda(l)\rho(r)=\chi(x)\gamma(c).$$

Proof. In the boundary branch, substitute the left-pop equation and then the splice equation:

$$\lambda(l)\rho(r) =\chi(x)\beta(b)\rho(r) =\chi(x)\gamma(f(b,r)).$$

In the residual branch,

$$\lambda(l)\rho(r) =\chi(x)\lambda(l')\rho(r),$$

which is the meaning of the residual pair. These are all result branches. $\square$

This semantic lemma does not require $B$ to be finite as a set. For a bounded persistent implementation, its shape must have a fixed finite interface. If $B$ is a fixed product of $h$ element slots and each premise is certified by finitely many bounded rules, the composed operation is bounded. Its resource bounds are obtained by finite call composition. This is a sufficient construction principle, not a characterization or an optimality theorem.

The hypotheses are checkable without assuming the result: list the local-pop branches, normalize each input and output word independently, verify the fixed boundary arity, verify the splice equation, and check constructor types and primitive resource contracts.

2. Exact deque instance

Fix an arbitrary payload type $A$ and nesting level $l\in\mathbb N$. Put $E_l=\mathsf{stored}\ A\ l$. Every value is a finite immutable acyclic value admitted by the source’s indexed constructors. Sharing with retained earlier versions is arbitrary.

For $x:E_l$, let $\phi_l(x)\in A^*$ be its recursive stored sequence. Extend this interpretation by concatenation to buffers, nodes, triples, chains and semi-cadeques as in theory/Cadeque/Models.v. One $E_l$ entry denotes an arbitrary word block, not necessarily one payload letter.

The pair-route input is exactly

$$c:\mathsf{chain}\ A\ l\ 2\ \mathsf{only}\ \mathsf{green}\ \mathsf{green}.$$

Constructor inversion gives $c=\mathsf{Pair}(c_L,c_R)$, where $c_L$ is an arity-one left chain with green exposed colors and $c_R$ is an arity-one right chain with green exposed colors. No reachability restriction or maximum level is assumed.

The observation is sequence equality. The theorem does not equate physical graphs, sharing patterns, allocation histories or arbitrary future scaffold contexts. A fixed controller receives exact future trace preservation only when every operation it can call is covered by its certified interface.

Initialization remains a fixed finite well-typed graph with a declared abstract sequence. All operations here are strict and persistent, so old versions remain unchanged.

3. Explicit buffer hypotheses

At element level $l$, require the following contracts:

• Buffer.pop removes the first entry and preserves the remaining order.
• Buffer.has5, on a buffer known to contain at least four entries, distinguishes exactly four from at least five without changing its sequence.
• Buffer.pair, Buffer.push2 and Buffer.push6 prepend their supplied entries in the displayed order.
• Each helper preserves entry level and its indexed occupancy result.
• Each helper is strict, persistent and has a uniform finite arity, old-access radius and allocation bound independent of $l$, occupancy and history.

These contracts are independently stated module obligations. The source’s has5 is already structural: it removes four entries on temporary persistent versions and tests the residual root for emptiness. pair, push2 and push6 are fixed compositions of at most six pushes. The earlier bounded-threshold audit supplies a scalar-free finite-record route for the larger buffer module. This note does not rerun or formalize that audit.

4. Certifying pop_left_green

Convert $c_L$ to a left triple $t_L$ with triple_of_chain. The preceding certificate proves

$$\mathsf{chain\_seq}(c_L)=\mathsf{triple\_seq}(t_L)$$

for all seven conversion clauses.

Inverting

$$t_L:\mathsf{triple}\ A\ l\ \mathsf{left}\ \mathsf{green}$$

gives five top-level coloring combinations. Splitting the ending threshold and the yellow child arity gives seven semantic subcases:

An RT input is impossible because its result color is red. OST and OPT force child arities one and two. The positive-prefix transitions are the same $8\mapsto7$, $7\mapsto6$, and $6\mapsto5$ transitions certified for the single route.

The ending case is the new boundary. Write the input prefix as $XBCDE$, with boundary pair $(F,G)$. If the residual prefix has exactly four entries, the triple word is

$$XBCDEFG.$$

pop_left_green returns head $X$ and the fixed boundary $(B,C,D,E,F,G)$. A four-entry prefix cannot rebuild a Left node, whose minimum is five. Thus the six-entry result is forced by shape, not merely a convenient implementation choice.

If at least five prefix entries remain, or in every non-ending coloring, the result is a residual left triple $t_L'$ and

$$\mathsf{triple\_seq}(t_L) =\phi_l(x)\mathsf{triple\_seq}(t_L').$$

These equations quantify over arbitrary word substitutions for every stored entry.

5. Certifying only_of_right

Let the six boundary entries have word blocks $B,C,D,E,F,G$. Convert the unchanged right chain to $t_R$ with triple_of_chain, preserving its exact word.

There are two source branches.

1. If $t_R$ is GT / Right EN, its word is $HI S$, where $(H,I)$ is the right node’s boundary pair and $S$ is its suffix. push2 followed by push6 constructs one Only_end buffer with word

   $$BCDEFGHIS.$$

2. Otherwise the right triple has positive arity and word $HI R S$, where $R$ is the child-chain word. pair followed by push6 constructs an eight-entry prefix $BCDEFGHI$. The resulting Only node therefore has word

   $$BCDEFGHIRS.$$

In both branches,

$$\mathsf{triple\_seq}(\mathsf{only\_of\_right}(b,t_R)) =\beta(b)\mathsf{triple\_seq}(t_R).$$

The eight constructed prefix entries justify adapt_to_prefix for every positive node coloring. That function changes only phantom index evidence; it does not inspect or modify runtime data. Omitting it can preserve the word while failing to type for an arbitrary right-node prefix index.

Typed coverage consists of GT/EN, GT/GN, YT/YN with Single or Pair child, OST/ON, and OPT/ON. Converting the result with chain_of_triple preserves its word in each corresponding clause.

6. Pair-route and full-pop theorems

Theorem (pair-chain pop_green). Under the contracts in Section 3, for every pair-route input $c$, pop_pair_green(c) returns $x:E_l$ and a semi-cadeque $d$ over $E_l$ satisfying

$$\mathsf{chain\_seq}(c) =\phi_l(x)\mathsf{semi\_cadeque\_seq}(d).$$

All returned levels, arities and colors are admitted by the indexed constructors, and every old value is preserved.

Proof. Write $L=\mathsf{chain\_seq}(c_L)$ and $R=\mathsf{chain\_seq}(c_R)$. Then $\mathsf{chain\_seq}(c)=LR$.

In the six-entry branch, Section 4 gives $L=XU$, where $U$ is the six-entry boundary word. Section 5 and chain_of_triple give residual word $UR$. Hence $LR=XUR$.

In the residual-triple branch, Section 4 gives $L=XL'$. The certified chain_of_triple conversion gives a residual left chain of word $L'$, and the returned Pair has word $L'R$. Hence $LR=XL'R$. These are the two source result branches. $\square$

Corollary (complete green pop). Combine the pair theorem with the previous single-chain theorem. For every $n\geq0$ and every

$$c:\mathsf{chain}\ A\ l\ (n+1)\ \mathsf{only}\ \mathsf{green}\ \mathsf{green},$$

the source pop_green returns $x,d$ with

$$\mathsf{chain\_seq}(c) =\phi_l(x)\mathsf{semi\_cadeque\_seq}(d).$$

The source arity constructors restrict a nonempty chain to arity one or two, so the Single and Pair proofs are exhaustive. This is an exact sequence theorem for the inspected source algebra under the buffer contracts. It is not a claim of raw graph equivalence or a new proof of the upstream Rocq theorem.

7. Resource bound

Count explicit algebraic constructor blocks in the pinned pair route, including result wrappers and excluding buffer-helper internals. triple_of_chain is called at most twice and allocates at most four blocks per call. pop_left_green allocates at most three, only_of_right at most two, chain_of_triple at most three, and the outer result at most two. A conservative wrapper bound is therefore 18 fresh blocks. The six-entry boundary gives maximum explicit arity six.

Suppose each of the five listed buffer helpers has arity at most $q_B$, radius at most $r_B$, and allocation at most $A_B$. A pair route calls at most four helpers: pop, possibly has5, and one of pair or push2, followed by push6. Conservative composed bounds are

$$q\leq\max(6,q_B),\qquad A\leq4A_B+18,\qquad r\leq4r_B+8.$$

The additive radius covers the chain, packet, body or node and view-wrapper paths outside helper calls. The Single route is smaller, so these also bound full pop_green after taking a common helper maximum. They are construction bounds, not optima or measurements of an optimizing OCaml compiler.

For a fixed finite controller with $s$ registered roots, once all its called operations have such certificates, the simultaneous-record compiler uses

$$d=\max(1,s+Aq),\qquad k=r+1.$$

It preserves decoded records and certified controller observations from a fixed finite initialization. It does not make arbitrary historical roots free, reveal pointer identity, or preserve arbitrary scaffold-context observations. A scaffold recognizing $L$ transfers to a PEG for $L^R$.

8. Verification, examples and novelty

The symbolic checker pins the four source files and checks seven typed pop_left_green subcases, six typed only_of_right subcases, and both pop_pair_green result arms. It uses free word blocks. In particular, one stored head is represented by two formal tokens to prevent accidental identification with one payload letter.

Positive edge cases include the exact five-entry ending prefix, which must return a six-entry boundary, and the non-ending splice, which constructs an eight-entry prefix. Negative controls reject placing the right word before the boundary, reversing the six entries, swapping residual left and right chains, retaining the popped head, rebuilding an undersized Left node, and omitting required prefix-index adaptation.

The recorded output states the exact scope. The checker is a handwritten symbolic model, not an OCaml parser, a source-refinement compiler, a proof-assistant formalization or a verification of buffer internals. Source hashes establish provenance, not a semantic source relation. The written branch derivation supplies that relation for this route.

The finite-boundary splice lemma is elementary algebraic composition. The upstream Rocq development already proves the full deque theorem. No novelty is claimed for either ingredient. The potentially additional contribution is their use as a checkable, resource-explicit local certificate pattern that can feed the scaffolding compiler. A literature search has not established novelty of that combination.

9. Consequence and next question

The prefix-repair theorem previously assumed all of pop_green. That semantic assumption can now be replaced by the explicit buffer contracts and the two route certificates. The remaining local premises for that repair are semi_push, semi_concat, has3p, inject3 and bounded vector injection.

The next decisive question is whether the finite-boundary splice lemma is merely convenient terminology for this deque or a reusable certificate interface. Test it against one independent persistent operation with a different fixed boundary size. A positive instance should expose a bounded underflow boundary and a separately checkable neighbor-splice equation. A negative example should show why unbounded boundary information prevents this certificate, without claiming that every alternative representation is impossible.