Proof levels need not be runtime counters

Working research note, 30 September 2026.

Overview

An immutable program can use the same finite constructors at every nesting depth even when its correctness proof labels values by an unbounded level $n$. For example, three level-$n$ entries may be packed into one level-$n+1$ entry. The executable code needs only the constructor tags; the proof needs to know that the three input levels agree. Treating that proof index as a runtime counter would impose storage the program does not use.

This distinction matters when certifying bounded persistent work. The earlier certificate theorem uses finitely many constructor sorts to check shape, word meaning, access and allocation. Here we show that exact agreement of arbitrary nesting levels is not recognizable by any such finite sort system. This is a limit of the certificate format, not an impossibility result for the program.

The positive result is a uniform lifting rule: proof indices may remain in the typing argument if the erased runtime cases, word equations and resource bounds are finite and independent of those indices. Applying that rule checks the deque’s red-to-green prefix repair under explicit module contracts. The word order, level changes and constant resource bounds are established; the pop_green helper remains an unresolved predecessor obligation. The repair itself is imported from Viennot, Wendling, Gueneau and Pottier, so this note does not claim a new deque algorithm or an unconditional certificate for their implementation.

1. The same word can have different structural roles

Let $E_n$ be the type of elements at nesting level $n$. At level zero, an element is a payload letter. At higher levels, a stored value has one of the forms

$$\operatorname{Small}(p),\qquad \operatorname{Big}(p,c,s),$$

where $p,s$ contain at least three elements of $E_n$, while $c$ is a chain of elements of $E_{n+1}$. Both constructors produce an element of $E_{n+1}$. These are mutually inductive types on finite acyclic values, as in the companion source.

Write $\phi_n:E_n\to\Gamma^*$ for flattening to payload words, and $\Phi$ for the extension to buffers and chains by concatenation. For instance, nine payloads $a$ at level zero and three stored triples $\operatorname{Small}(a,a,a)$ at level one both flatten to $a^9$. Their flattened word alone does not describe their structural role.

Two measures must remain separate:

• Occupancy: the number of entries in a buffer at its current level.
• Fringe: the word obtained by flattening those entries to payloads.

Moving three entries always adds three to occupancy. At a higher level, those entries can stand for long words. A proof that treats them as three payload letters would silently lose the required quantifier.

2. Exact level agreement is not a finite-sort invariant

Consider the abstract three-entry fragment, with ranked signature $g$ (nullary) and $S$ (ternary). Its indexed typing rules are

$$g:E_0,\qquad \frac{x:E_n\quad y:E_n\quad z:E_n}{S(x,y,z):E_{n+1}}.$$

This models a Small value with a fixed three-entry buffer. It concerns this abstract constructor signature, not a claim that every concrete buffer implementation has been translated to it.

Proposition. The set of trees typable at some level is not a regular tree language. Consequently no finite ordinary constructor-sort system, even allowing finitely many local annotations and then erasing them, exactly recognizes this invariant.

Proof. Put $t_0=g$ and $t_{n+1}=S(t_n,t_n,t_n)$. With only one ground symbol, the typable trees are precisely the $t_n$. Suppose a deterministic bottom-up tree automaton recognizes them. Finitely many states imply that two trees $t_i,t_j$, $i<j$, receive the same state. The automaton must then give $S(t_j,t_i,t_i)$ the same state as the accepted $t_{i+1}$. But its three children have unequal levels, so it is not typable. This is a contradiction.

A nondeterministic finite tree automaton can be determinized by assigning each subtree the set of its possible states. Ordinary finite constructor sorts are such a finite-state system. Finitely annotated versions remain finite-state after existentially choosing annotations. The contradiction therefore applies to them as well. $\square$

The limitation is exact recognition of this invariant over all input trees. For any fixed maximum level, finitely many sorts suffice. A coarser finite grammar can admit mixed-level trees. A program may also preserve the precise invariant from initialization without being able to recognize it on arbitrary input graphs. None of this proves that a deque needs runtime level counters, that no adequate coarser invariant exists, or that another representation cannot support the same interface.

There is a sharp positive control. Initialize one record $g$, then repeatedly return one fresh record $S(t,t,t)$, sharing the old root in all three fields. This generates exactly the unfoldings $t_n$, with $q=3,r=0,A=1$, and retains every earlier version. Its exact reachable unfolding language is nonregular despite constant work per step. Thus finite runtime rules do not force a regular reachable-shape invariant. The earlier finite-sort certificate can still verify word tripling using a coarser grammar that admits mixed-level trees; exact level recognition and sufficient semantic verification are different demands.

This is a standard finite-state indistinguishability argument applied to the shape obligation in our certificate format. It is not a new general nonregularity method.

3. A sufficient uniform lifting lemma

Here is a conservative extension of the previous certificate principle. Use finitely many constructor and operation schemata, with natural-number indices in their typing judgments, but erase all indices from execution. Values remain finite acyclic immutable DAGs with finite tags and bounded arity. Their word interpretations are fixed constructor expressions that do not depend on the index.

For each finite operation case, require:

1. Coverage without inspecting indices. The runtime rule is selected by finitely many constructor tags. A finite erased-pattern partition covers the admitted inputs. Its symbolic typing premises are obtained by unfolding the declared constructor typing schemes, so every typed match is included. No extra convenient premise may be silently imposed.
2. Indexed typing certificate. Annotate all returned and fresh values. After substituting the input constructor equations, every required index equality becomes an identity. Required lower bounds follow from the declared nonnegative parameters, for example $5+p+3\geq8$, $3+r\geq3$.
3. Fringe certificate. Independently derive the input and output word expressions and compare their normal forms, treating each frontier element’s fringe as an arbitrary word, not necessarily one letter.
4. Uniform resource certificate. The erased rule has a fixed finite allocation list and fixed old-address bounds. Its code contains no operation on a proof index. Any called module must have its own uniform shape, semantic and resource contract.

A concrete sufficient arithmetic check is substitution of explicitly given affine expressions, coefficient comparison for identities, and checking that a required nonnegative difference has nonnegative constant and coefficients in natural parameters. This is finite and sound but incomplete. This note does not implement a general indexed-type inference or coverage algorithm. For the source instance below, the four cases and their typing constraints are explicit.

Lemma (uniform lifting). For any finite set of such certified rules without unresolved module calls, any fixed finite typed initial graph, and every finite legal sequence of calls, indexed well-typedness, the certified word relations and the uniform per-call resource bounds are preserved. Earlier versions remain valid. If the abstract relations specify deterministic operations, their observable interface traces are preserved. With unresolved module calls, the same conclusion is conditional on their stated contracts.

Proof. Fix any assignment of natural numbers satisfying the input typing premises. The index identities and inequalities prove that each constructed value has its declared type. The word-expression substitution lemma from the preceding theorem proves the operation relation; it works for arbitrary word substitutions, including large nested elements.

The erased rule is independent of the chosen numbers, so its maximum allocation and old-access bounds apply to every assignment. Old fields remain unchanged. Induct over calls, retaining the typing witnesses for earlier versions as well as the current roots. Deterministic abstract specifications give exact trace agreement by uniqueness. A module call uses its contract at the appropriate point in this induction; an unproved contract remains a premise. $\square$

The finite runtime implementation, rather than a finite set of proof indices, is what the simultaneous-record compiler needs. For a fixed finite controller with $s$ registered roots and uniform bounds $q,r,A$, it still gives $d=\max(1,s+Aq)$, $k=r+1$. Its fixed finite initial graph uses virtual initialization. It preserves decoded records and the certified controller observations, not arbitrary raw scaffold-context observations. An accepting scaffold for $L$ still transfers to a PEG for $L^R$.

4. Exact contracts for the prefix repair

Fix any finite payload alphabet $\Gamma$ and any $n\geq0$. Let $p$ be a buffer of $E_n$ entries with occupancy at least five. Let $c$ be a nonempty green chain of $E_{n+1}$ entries. The source routine is

stored, child = pop_green(c)
p2, child = extract_prefix(stored, child)
return make_green_prefix(p, p2, child)

The following premises are explicit and do not follow merely from matching helper names in OCaml and Rocq:

Buffer occupancy contracts count $E_n$ entries. Semantic contracts use their flattened words. A scalar-free threshold implementation can supply has3p via the earlier bounded-probing construction; this note does not discharge its buffer implementation or the pop_green premise. All calls are strict and persistent; no memoization or amortized-cost assumption is substituted for a uniform bound.

The source code for extraction has two cases:

Small(p2):                 return p2, D
Big(p2, T, s):
    D1 = semi_push(Small(s), D)
    D2 = semi_concat(T, D1)
    return p2, D2

In the Big case, $s$ has level $n$ and at least three entries. Consequently Small(s) has level $n+1$, exactly the level expected by $D$ and $T$. Its fringe is $\Phi(s)$. Thus extraction returns a prefix and child whose combined fringe is the old stored head followed by $D$, in the correct order.

Next split $p_2$ into a three-entry buffer $u$ and remainder. If the remainder $v$ has fewer than three entries, append both $u$ and $v$ to $p$. Otherwise append $u$ to $p$, and prepend Small(remainder) to the child. The latter constructor is legal precisely because the remainder has at least three entries.

5. Conditional repair theorem

Theorem. Under exactly the contracts in Section 4, ensure_green_prefix returns a buffer $p'$ of $E_n$ entries with occupancy at least eight, and a semi-regular chain $c'$ of $E_{n+1}$ entries, satisfying

$$\Phi(p')\Phi(c')=\Phi(p)\Phi(c).$$

This holds for every nesting level, every admissible finite input value, and every sharing pattern between the retained inputs.

Proof. Write capitals for the fringes of the corresponding buffers and chains. The four families of cases are:

The input column comes from the stored constructor and pop contract. The two output columns come from the executed extraction and repair clauses. Their concatenation equals the input in each case. In particular, the Big case must place $T$ before $S D$.

Each output prefix contains at least $5+3=8$ entries. The short branch adds at most two more. In the long branch, Small(remainder) is legal and has level $n+1$. Every semi-chain operation therefore receives the required element level. Extraction’s Big branch was typed above; the Small branch is immediate. The contracts give semi-regular output shape, and immutability preserves all retained inputs. No argument uses the numerical value of $n$. $\square$

Red-left corollary. Let the input to green_of_red_left have a well-typed body $b$, red Left node with prefix $p$ and boundary entries $y,z:E_n$, and a nonempty green child $c$. The source’s regularity relation supplies the last premise. Under Section 4, its result is a green chain with the same fringe.

Proof. Apply the theorem. If the new child is Empty, the source chooses Left(EN); otherwise it chooses Left(GN). Occupancy at least eight is sufficient for GN. The outer G regularity constructor permits either color of the semi-regular child. In both cases the argument supplied to the unchanged body is $\Phi(p')\Phi(c')\phi_n(y)\phi_n(z)$, equal to the old argument. Applying the same body interpretation preserves that equality. The body’s head and tail levels and kinds are unchanged. $\square$

These statements certify this repair composition conditionally. They do not prove pop_green by assuming its own desired conclusion: its contract is an explicitly unresolved predecessor obligation.

6. Resources and counterexamples

Treat pop_green, has3p, inject3, inject_vector, semi_push and semi_concat as module calls. Each prefix-repair path uses at most six such calls: the Big extraction uses one push and one concat, and the final short/long alternatives each use one further call after inject3. There is no loop on the nesting level.

If all these modules have uniform bounds $q_0,r_0,A_0$, inline the fixed caller skeleton. Let $B$ bound its own constructor slots and pointer projections, including result wrappers. Then a conservative prefix-repair bound is

$$q\leq\max(q_0,3),\quad A\leq6A_0+B,\quad r\leq6r_0+B.$$

Here constructors and tuples are encoded by individual records and finite color tags. $B$ is a syntactic constant of this skeleton, independent of $n$ and heap size, not an unmeasured runtime quantity. To justify the radius sum, retain all fresh slots from earlier module calls in the current batch. A path that exits those slots into the pre-call heap can never return to them. Each successive module adds at most $r_0$ to the maximum original-old address; caller projections add at most $B$ in total. Allocation adds directly. The red-left wrapper adds only fixed projections, constructors and its root-tag emptiness test. These are conditional construction bounds, not measured bounds for the library or claims of optimality.

Two tempting wrong rules demonstrate the distinct obligations. Reversing the Big extraction’s concat gives the wrong long-case output $P\,U\,R\,S\,D\,T$ instead of $P\,U\,R\,T\,S\,D$. For a concrete level-zero witness, take $P=a^5$, $U=R=S=a^3$, $T=b^3$ represented by a chain containing Small(b,b,b), and $D$ empty. The correct word is $a^{11}b^3a^3$; the wrong one is $a^{14}b^3$. All the occupancy premises hold. Omitting Small in the long branch can preserve the flattened word while passing a level-$n$ buffer where a level-$n+1$ stored entry is required. Repackaging a two-entry remainder as Small similarly violates occupancy. Word equality alone detects neither typing failure.

7. Evidence, credit and next obligation

The symbolic checker derives output expressions by executing a handwritten model of the two helper bodies under their primitive contracts. It compares them with a separately assembled input fringe and checks ranks and occupancy. Short remainders of size zero, one and two are separate cases; the long remainder has symbolic size $3+r$, with arbitrary $r\geq0$. Rank annotations mean $n+\text{offset}$ for arbitrary $n$, and word blocks are symbolic. These are algebraic checks, not sampled executions at a few depths.

The recorded output includes three negative controls and hashes for the four inspected source files at commit 503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0: lib/cadeque_core.ml, theory/Cadeque/Types.v, theory/Cadeque/Models.v and theory/Cadeque/Core.v. Hashes pin the inspected source; they do not establish automatic translation. No Rocq proof was rerun, no OCaml refinement was formally checked, and no general indexed-certificate checker was implemented. The proposition, lifting lemma and conditional repair theorem have written proofs in this note.

The inspected Rocq Core already states the make_green_prefix, extract_prefix, ensure_green_prefix and green_of_red_left contracts used here. Credit for the representation, repair and existing formal development belongs to Viennot, Wendling, Gueneau and Pottier: author-hosted paper, companion repository. Nested datatypes are established territory; see Bird and Meertens, Nested Datatypes. The finite-sort limitation uses standard tree-automata reasoning as in Comon et al..

The added work is the explicit boundary of our previous certificate format, the uniform proof/runtime distinction, and the conditional source-to-obligation test with separate level and occupancy checks. Novelty is not established. Earlier comparisons with persistence, pointer machines, residual/bisimulation theory and resource certification remain in the preceding note. No new transducer-uniformization, visibly-pushdown, representation-independent lower-bound or pumping claim follows from this example.

The next obligation is to discharge a pop_green case with its indexed shape and fringe guarantees, rather than treating that contract as proved. The single-chain route through triple_of_chain and pop_only_green is the first concrete test. Its proof must preserve the same distinction between structural entry count and flattened word size.