A local-view certificate for single-chain pop

Working research note, 30 September 2026.

The broader goal is to determine when completed work can remain available to future computation through finite rules, bounded local access and bounded allocation. This note asks a narrow but decisive question: can the real single-chain branch of pop_green be certified without assuming the very pop contract needed by the preceding prefix-repair proof?

Yes. The route factors through a temporary triple view:

$$\mathsf{SingleChain}\xrightarrow{\mathsf{triple\_of\_chain}} \mathsf{Triple}\xrightarrow{\mathsf{pop\_only\_green}} E_l\times(\mathsf{Zero}+\mathsf{Triple}) \xrightarrow{\mathsf{chain\_of\_triple}} E_l\times\mathsf{SemiChain}.$$

The first and last maps preserve the flattened word. The middle map removes exactly its first stored entry. Type inversion gives a finite exhaustive list of middle cases at every nesting level. Composing the three commuting word equations proves the single-chain pop contract. This discharges one actual predecessor of ensure_green_prefix; the pair-chain route remains open.

The deque algorithm and its existing Rocq theorem are due to Viennot, Wendling, Gueneau and Pottier; the inspected companion source is pinned to one commit. The result here is an independent certificate argument for one source route and a reusable local-view principle. It is not a new deque algorithm and it is not a new proof of their full pop_green theorem.

1. Model, quantifiers and observation

Fix a payload type (A) and an arbitrary nesting level (lN). Let (E_l= A l). Every value is a finite immutable acyclic value admitted by the mutually indexed constructors in the pinned source. Sharing between inputs and 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 exactly as in theory/Cadeque/Models.v. A stored entry is an arbitrary word block. At positive levels it need not denote one payload letter.

The input class in this note is exactly

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

Thus the chain has arity one and its two exposed colors are green. The source then selects the Single arm of pop_green; no reachability hypothesis or fixed maximum level is added.

The observation is the flattened sequence only. The preservation statement does not identify stored graphs, allocation histories, pointer identities or behavior under an arbitrary future scaffold context. It supports future calls whose observations factor through the certified deque interface. For a fixed controller, exact interface traces follow once every operation it can call is certified. This note alone does not provide that whole-interface premise.

Initialization is likewise separate: a compiled controller starts from any fixed finite well-typed initial graph with the declared abstract sequence. This one-operation theorem preserves the invariant for the returned root and leaves every old version unchanged.

2. The theorem

Assume the buffer operation used by the source has the following contract. For every nonempty buffer (p) of (E_l), Buffer.pop p returns (x,p’) with

$$\Phi(p)=\phi_l(x)\Phi(p'),$$

and decreases occupancy by exactly one. Buffer.has1 distinguishes zero occupancy from positive occupancy without changing the buffer. Both operations are strict, persistent and have uniform local-access and allocation bounds independent of (l), occupancy and history.

Theorem (single-chain pop_green). For every (A,l) and every input

$$c:\mathsf{chain}\ A\ l\ 1\ \mathsf{only}\ \mathsf{green}\ \mathsf{green},$$

the Single source route returns (x:E_l) and a semi-cadeque (d) over (E_l) such that

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

The result is well indexed at the same element level (l), all returned colors and arities are admitted by their constructors, and all old values remain unchanged.

This is a sufficient source-route theorem, not a characterization of every bounded pop representation. It gives a construction bound conditional on the buffer bounds; no optimality is claimed.

3. View conversion preserves the exact fringe

The source routine triple_of_chain has seven clauses. They are exhaustive for a nonempty arity-one chain by inversion on Single, its packet body and the regularity witness. In each clause, chain_seq and triple_seq normalize to the same word.

The two cases where order could be lost are illustrative. Write (H[-]) for the one-hole word context of the extracted head node, (B[-]) for the remaining body, (T[-]) for the tail node, and (R,L,Q) for the corresponding child-chain words. Then

$$\begin{aligned} \mathsf{Pair\_yellow}:&\quad H[B[T[R]]\,Q],\\ \mathsf{Pair\_orange}:&\quad H[L\,B[T[R]]]. \end{aligned}$$

The returned triple has child chain Pair(Single(...), rc) in the first case and Pair(lc, Single(...)) in the second, giving exactly these two normal forms. The hole and single-child clauses are direct context reassociations. No equation assumes that any frontier entry is a singleton word.

Conversely, chain_of_triple has six clauses and preserves triple_seq exactly. It rebuilds the packet body around the child chain. Its yellow-pair and orange-pair clauses use the same two asymmetric orders above. Inverse graph identity is neither needed nor claimed: both conversions need only commute with the sequence observation.

These are finite symbolic equalities over word blocks. They hold for every substitution of finite words, hence for arbitrary nesting depth and sharing.

4. Typed closure of the pop view

The key coverage step is inversion on

$$t:\mathsf{triple}\ A\ l\ \mathsf{only}\ \mathsf{green}.$$

There are exactly five top-level source combinations. Splitting the orange_tc call on child arity yields seven semantic subcases:

The first row has two result subcases because the residual end buffer may be empty or nonempty. No RT input is possible because RT produces a red triple. OST has arity one and therefore a Single child. OPT has arity two and therefore a Pair child. These are consequences of the declared indices, not assumptions about reachable values.

The occupancy transitions explain the colors. Removing one entry changes

$$8+q\mapsto7+q,\qquad 7+q\mapsto6+q,\qquad 6+q\mapsto5+q,$$

which are precisely the minimum prefix sizes for GN to YN, YN to ON, and ON to RN. An unchanged suffix has at least one unit of spare occupancy for the next color. The child stays at level (l+1) and its arity is unchanged. orange_tc merely selects OST or OPT from that arity.

For every row, write the popped entry word as (X), the remaining prefix as (P), the child word as (C), and the suffix as (S). The non-end cases all have the independent normalization

$$XPCS=X\,(PCS).$$

For Only_end, the same equation is (XP=X(P)), with (P=) in the zero-result branch. The buffer contract supplies the only removal step. The color transitions are semantically invisible but required for well-typed reuse.

5. Composition proof

Let (t=(c)). Section 3 gives

$$\mathsf{chain\_seq}(c)=\mathsf{triple\_seq}(t).$$

By the exhaustive inversion in Section 4, pop_only_green(t) returns (x) and either zero or a triple (t’), with

$$\mathsf{triple\_seq}(t)= \phi_l(x)\,\mathsf{pt\_triple\_seq}(t').$$

If the result is zero, pop_green returns the empty chain and the equation is done. Otherwise let (c’=(t’)). Section 3 gives

$$\mathsf{chain\_seq}(c')=\mathsf{triple\_seq}(t').$$

Substitution proves

$$\mathsf{chain\_seq}(c)=\phi_l(x)\,\mathsf{chain\_seq}(c').$$

Wrapping (c’) as a semi-cadeque changes no sequence. Every operation only constructs fresh immutable wrappers around old fields, so retained inputs are unchanged. This proves the theorem. $\square$

The proof has the shape of a small commuting triangle: move to a view in which the requested observation is local, perform the bounded operation, and move back through another observation-preserving map. Requiring an inverse on physical representations would be stronger than necessary.

6. Resource bounds and compiler consequence

Count explicit algebraic constructor blocks in the pinned OCaml route, including returned pair/option/semi wrappers but excluding primitive buffer internals. triple_of_chain allocates at most four, pop_only_green at most three, chain_of_triple at most three, and the outer pop_green result at most two. Thus the wrapper skeleton allocates at most twelve fresh blocks of arity at most three.

Suppose Buffer.pop and Buffer.has1 have maximum arity (q_B), old-access radius (r_B), and together allocate at most (A_B) fresh blocks. A conservative inlining bound for this route is

$$q\leq\max(3,q_B),\qquad A\leq A_B+12,\qquad r\leq r_B+5.$$

The additive radius covers the chain, packet, body/head-node and buffer path outside the primitive. These are construction bounds for this route, not measurements of an optimizing compiler and not optima. The existing Rocq contract proves sequence correctness of its buffer call; this certificate still treats the primitive’s finite-record resource bound as a separate module obligation.

For a fixed finite controller with (s) registered roots whose other called operations also have certificates, take the maximum route bounds (q,r,A). The simultaneous-record compiler then uses

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

This preserves decoded records and the controller’s certified interface observations from its fixed finite initialization. It does not preserve literal target-node identity or arbitrary future scaffold tests. If such a controller recognizes (L), the resulting scaffold recognizes (L), and the scaffold-to-PEG transfer gives a PEG for (L^R), not for (L) without the reversal.

7. Checks, examples and limitations

The symbolic checker pins the four relevant source files at commit 503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0. It checks seven triple_of_chain word cases, six chain_of_triple word cases, all seven typed pop subcases and the composed equation. Formal word blocks are used, including a two-token block for one stored head, so the test does not collapse structural occupancy into payload length.

Positive edge cases include a one-entry Only_end, which returns the head and an empty chain, and every green-node color degradation above. Negative controls reject retaining the popped head, swapping child and suffix, reversing the yellow pair, and keeping GN after its prefix drops below eight entries. The last mutation preserves the word but violates shape, confirming that the word and type certificates are independent obligations.

The recorded output states the exact verification scope. The checker is a handwritten symbolic model, not an OCaml parser, source-to-source refinement proof, general dependent-type checker or proof-assistant formalization. Hashes establish provenance, not a semantic source relation. The written branch comparison supplies that relation for this route.

The full source already has a stronger machine-checked theorem for pop_green, including the pair branch. Our additional contribution is the finite local-view certificate decomposition, explicit level-uniform coverage, resource interface and connection to the persistent-record compiler. Whether this exact combination is novel remains unestablished.

8. Next obligation

The single route removes the circular pop_green premise from one real path through ensure_green_prefix. It does not justify the pair input to pop_green. The next decisive question is whether pop_pair_green admits the same local-view factorization without introducing an unresolved semantic primitive:

1. certify pop_left_green, including its six-element boundary result;
2. certify only_of_right and both conversions;
3. compose the two result branches with exact order and indexed colors;
4. retain the same arbitrary-word-block quantifier.

If that closes with finite source cases and the same buffer contract, the entire pop_green premise used by prefix repair is discharged. If it does not, the missing invariant should be isolated before expanding the agenda.