Finite certificates for bounded persistent word interfaces

Working research note, 30 September 2026.

The question is how a finite amount of work now can keep the past usable by indefinitely many later operations. This note gives a sufficient certificate criterion for a restricted class of immutable constructor programs. Its three parts are shape preservation, bounded access and allocation, and exact word equations. Their combination yields a whole-execution guarantee.

The criterion is decidable for the specified rule format. It is not a characterization of all bounded persistent realizations, a procedure for discovering representations, or a new general verification principle. The contribution here is an explicit specialization that connects independently checkable algebraic rules to the reviewed simultaneous-record compiler. Novelty relative to the verification literature has not been established.

1. A small example and its limitation

Represent a word by immutable trees

$$E,\quad A,\quad B,\quad \operatorname{Cat}(x,y),$$

with meanings $\epsilon,a,b,\alpha(x)\alpha(y)$, respectively. Returning one new node $\operatorname{Cat}(x,y)$ implements concatenation without inspecting either old tree. Changing that rule to $\operatorname{Cat}(y,x)$ has exactly the same resource cost and preserves the same types, but fails the specification: $ab\ne ba$.

A less immediate correct rule is

$$\operatorname{Cat}(\operatorname{Cat}(x,y),z) \longmapsto \operatorname{Cat}(x,\operatorname{Cat}(y,z)).$$

Its input and output meanings independently normalize to $XYZ$. Two new nodes suffice; the old addresses copied have length at most two. Other input shapes can be left unchanged. The old tree remains usable.

Neither fact provides a constant-cost first-symbol operation on every such tree. Section 7 proves this for the unaugmented representation. Storing a word correctly and making a particular observation locally accessible are separate obligations. This distinction is the reason to certify an entire specified interface, rather than one attractive update.

2. Exact model

Fix a finite alphabet $\Gamma$, a finite set of sorts, and finitely many constructors. Each constructor has one result sort and a fixed ordered list of child sorts. Tags may refine a sort, but all such refinements must be finite and declared. A value is a finite acyclic constructor DAG satisfying these signatures. Sharing is allowed. Every child is an actual value; missing children, if wanted, must be represented by a declared constructor. The maximum arity is $q$.

For each sort $s$, choose a positive finite component count $m_s$. Its mathematical interpretation is a tuple in $(\Gamma^*)^{m_s}$. Each constructor component is specified by a finite concatenation of literal letters and child-component variables. Empty, duplicated and reordered components are allowed. Thus a constructor interpretation is an explicit tuple of monoid terms, not an arbitrary semantic oracle. Structural recursion defines $\alpha$ on every finite DAG, unfolding a shared child at each occurrence. Interpreted words are mathematical values; the runtime does not build or traverse them.

For example a context has two components $(L,R)$, acting on a word $u$ as $LuR$. Composition has components

$$(L_1,R_1)\circ(L_2,R_2)=(L_1L_2,R_2R_1).$$

This covers these one-hole contexts. General higher-order contexts, level-indexed dependent types and arbitrary semantic functions are outside the theorem as stated.

A public operation has finitely many input roots of declared sorts and finitely many rules. Finite request letters and finite control states may be expanded into separate operation cases. Each rule has:

1. A tuple of finite constructor patterns. Every frontier variable has a declared sort and occurs once in the pattern tuple. An inspected internal node may also have a distinct name.
2. An ordered list of fresh constructor slots. A field names a pattern-bound old node or an earlier fresh slot. The output roots name old nodes or fresh slots of the declared output sorts.
3. One finite output tag.

The pattern regions must be disjoint and cover all well-sorted input tuples. Pattern variables are syntactically distinct, but their actual values may alias or share descendants. Rules never test that fact. There is no mutation, pointer-identity test, unbounded scalar, recursive call, hidden traversal, suspension or external primitive.

Root depth is zero. Define $r$ as the maximum old address length appearing anywhere in a pattern, including frontier bindings that are copied without inspection. This conservative definition bounds both tag decisions and old targets. Define $A$ as the maximum number of listed fresh slots in a rule, including unused slots. Both are per-call worst-case bounds, independent of heap size, history length, word length and aliasing.

A finite first-order program with an acyclic helper-call graph and fixed bounded loops can be expanded to this format when all its primitives are these constructor operations. Inline calls, unroll the loops, enumerate the finite branches, and substitute known fresh constructors through subsequent tests. The expansion may be very large. This statement does not cover recursive helpers, general OCaml features, or unverified library calls. No extraction of the existing catenable implementation is claimed here.

3. What the certificate checks

An operation specification is given independently of its rule bodies. For each output tag it gives finitely many equations in input components, output components and literal letters. These equations define a relation $R$ on abstract input, abstract output and tag.

For example concatenation has $v=xy$. Stack pop has three tags:

$$\begin{array}{c|c} \mathsf{empty}&x=\epsilon,\ v=\epsilon\\ \mathsf a&x=av\\ \mathsf b&x=bv. \end{array}$$

Together these define a unique pop result for each binary word. In general, equations need not define a function. The certificate theorem first guarantees the stated relation; the exact-interface corollary separately requires a deterministic abstract specification. That requirement is not silently delegated to the checker.

Shape check. Check constructor and root sorts, distinct pattern names, fresh-slot order, and input-pattern coverage and disjointness. Sort productivity is the finite least fixed point starting with nullary constructors. To check coverage, truncate productive input trees at the maximum constructor-pattern height. There are finitely many such truncated tuples. Each must match exactly one rule. Every truncated cell has a finite ground completion, and all its completions select the same patterns. This decides coverage. No semantic reachability invariant is assumed.

Resource check. Compute $q,r,A$ directly from the signatures and rule syntax, then compare them with the proposed budgets. This is not an asymptotic running-time argument. A copied but uninspected tail counts toward the access radius.

Equation check. Assign an independent formal word variable $X_{x,j}$ to component $j$ of each frontier value $x$. Evaluate constructor interpretations on the input patterns. Evaluate the fresh slots in their listed order, using the resulting old-node expressions. Substitute these two independently derived tuples into each specification equation. Flatten concatenations and delete empty terms. Accept only if the two resulting strings of letters and formal variables are literally equal.

All three procedures terminate on the finite certificate. They require no assumption that the proposed implementation already realizes its specification. Finding the sorts, interpretation and rules can be difficult; verification of the supplied certificate is the decidable part.

4. Certificate theorem and proof

Theorem (restricted certificate soundness). Fix the finite data in Sections 2 and 3. Suppose every operation passes the three checks. Start from any fixed finite well-sorted acyclic initial graph with specified roots and abstract interpretation. Then every finite legal history of operations, including calls on retained earlier versions, has the following properties:

• Every call selects exactly one rule, returns roots of the specified sorts and satisfies its abstract relation $R$.
• Every call inspects and copies old targets only within radius $r$ and allocates at most $A$ fresh records of arity at most $q$, using the maximum bounds over the finite operation set.
• All old values and their interpretations remain unchanged. Returned roots can be used in any later well-sorted call.

Here a client must already possess each supplied root handle. The theorem does not give free lookup of an arbitrary historical version.

Proof. First establish a substitution lemma. For a matched input pattern, substitute the actual interpreted frontier components for its formal variables. Induction up the finite pattern shows that each symbolic node expression becomes the interpretation of the corresponding actual old node. If frontier values alias, the substitution simply assigns correlated words to some distinct variables; the induction does not require independent actual values.

Next induct over the fresh-slot list. Its fields have already been assigned either old values or earlier fresh values. Constructor typing makes each new value well-sorted, and the constructor interpretation commutes with the same substitution. Consequently every symbolic output expression instantiates to the actual output interpretation.

An accepted equation has identical normalized sides. Any substitution of words therefore gives equality in $\Gamma^*$. Applying the two preceding inductions proves every required specification equation. The reported tag selects exactly the relation whose equations were checked.

Productivity and the finite coverage check ensure exactly one applicable rule for every well-sorted input tuple. Fresh references point only to old nodes or earlier fresh nodes, so the extended graph remains acyclic. The resource bounds follow from the listed addresses and slots. No rule changes an old field or tag, so interpretations of old roots are unchanged.

Finally induct over the number of executed calls. The fixed initial graph supplies the base case; the one-call argument preserves all premises for every subsequently selected tuple of retained roots. This proves the statement for arbitrarily long finite histories, including branching persistent use. An infinite sequence, when considered, has the same guarantee on each finite prefix. $\square$

Corollary (exact interface behavior). If the specified relations give deterministic total abstract operations on the relevant component tuples, and the initial interpretation equals the required initial abstract state, every legal interface trace produces exactly its specified abstract values and finite observable tags.

Proof. The theorem puts each concrete step in the abstract relation. Uniqueness identifies it with the specified abstract step. Induct on the trace. Initial equality starts the induction. $\square$

Uniqueness is evident for the stack specification above and for the stated concat, rotation and context operations. An arbitrary equation system might not have it. The checker makes no claim to decide totality or uniqueness for general abstract specifications.

The future quantifier is over the certified interface. In particular, two values with equal interpretations give equal future interface observations under the deterministic specification, even if their physical graphs differ. This is not equivalence under arbitrary future scaffold contexts. A controller that inspects additional unproved structure has left the certified interface.

5. Compilation with explicit bounds

Now fix a finite controller with $s$ registered roots, a finite request alphabet, and only certified constructor operations. A step has one specified root-wiring plan; unchanged registers are copied. Pad unused registers by missing roots in the compiler interface. Inputs must already be in the registered roots, rather than supplied through an unbounded external version-selection facility. Bound any finite in-step composition by expanding it before computing $r,A$.

The rule decisions factor through the radius-$r$ labelled unfolding. They do not observe pointer identity. Fresh slots form a special acyclic case of the reviewed simultaneous-record batches. Therefore the bounded simultaneous-record compiler applies with

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

The finite initial graph is represented in the compiler’s virtual decoder; it consumes no input symbol and imposes no exceptional first-step allocation. Its interpretation and initial finite control must be specified and checked separately. A finite ground construction, such as the stack initialization in the artifact, provides such an initial graph.

The compiler preserves decoded records, copied aliases, registered roots, control and prefix acceptance. Combined with the theorem, it preserves the certified abstract interface behavior. Physical target nodes use a different vocabulary, so equality of raw stored graphs is not asserted. These are construction bounds, not optima. The extra native layer in $k=r+1$ retains the reviewed base-versus-missing convention.

If an accepting controller recognizes $L$, the scaffold recognizes the same $L$, and the Loff-Moreira-Reis transfer gives a PEG for $L^R$. This note establishes no generalized pumping theorem and no language lower bound.

6. Positive, negative and incomplete instances

The supplied rule corpus and checker contain these examples:

The last row is a constructor-algebra model of one move used in the concat argument: form $\operatorname{Small}(s)$, append that to $c$, and form the left node with prefix $p$ and boundary pair $(y,z)$. Its four fresh IR nodes normalize to $PCSYZ$. This is an independently specified algebraic instance, not a translation or certificate for the OCaml buffer implementation. Its cost is the cost of this authored IR only.

Deliberately wrong variants reverse concat order, reverse context order, or retain a popped head. They fail the equation check. Missing or overlapping pop cases fail coverage; a cyclic fresh reference fails shape; understated allocation and radius fail resources. For reversed concat a concrete well-typed counterexample is $x=A,y=B$. For a retained popped head, use the one-element stack $\operatorname{ConsA}(\operatorname{Nil})$.

Rejection does not generally refute semantic correctness. For a sort with constructors $\operatorname{Zero}$ and $\operatorname{JoinZero}(x,y)$, interpreted by $\epsilon$ and $\alpha(x)\alpha(y)$, every finite value denotes $\epsilon$. Replacing any input by a new $\operatorname{Zero}$ preserves its meaning, by structural induction. Nevertheless its symbolic obligation is $X=\epsilon$, which this checker rejects. The checker forgets the restricted image of a frontier sort. Additional verified invariants could strengthen the certificate system, but are not built into this theorem.

Thus the criterion is sufficient and intentionally incomplete, even within the constructor format. Failure of one certificate says nothing by itself about other representations of the same abstract data or language.

7. A locality obstruction for the bare rope representation

Proposition. There is no uniform finite radius for a root-only operation that returns the first letter of every nonempty bare rope in Section 1. The operation may use finite rules and bounded fresh allocation, but its output tag must depend only on the supplied root’s bounded old unfolding and a common fixed control state. There is no additional cached summary.

Proof. Let $r$ be any proposed old-observation radius. Put $T_0^a=A$, $T_0^b=B$, and

$$T_{n+1}^x=\operatorname{Cat}(E,T_n^x).$$

The rooted labelled unfoldings of $T_{r+1}^a$ and $T_{r+1}^b$ agree through depth $r$: the only distinct label lies down $r+1$ right edges. Their interpreted words are $a$ and $b$. The same local view and control state select the same output tag, which cannot be correct on both. Fresh allocation cannot supply an old distinction absent from the allowed view. This holds for every $r$. $\square$

The witness trees can be built from $E,A,B$ by the certified concat rule, but the proposition concerns a root-only query over all such presentations. A controller that separately retained their first letters is outside its hypotheses. Annotating every concat root with a maintained first-letter summary defeats this particular obstruction. No claim is made about every persistent representation, every scaffold controller, or every language presentation.

This proposition explains the practical test for the next construction: after proving algebraic preservation, ask whether every required observation has a local rule on the invariant class. The omitted step cannot be supplied by an equation for concat alone.

8. Relation to established work and the remaining source obligation

The soundness proof is the standard pattern of a simulation relation and an inductive invariant. Finite constructor shape systems and their closure checks are established tree-automata material; tuple-word interpretations use ordinary algebraic interpretation and substitution. See Comon et al., Tree Automata Techniques and Applications, Chapters 1, 2 and 6 (author-hosted text). The elementary truncated-pattern procedure here needs less than the full tree-automata machinery.

Proof-carrying code and translation validation already separate producing an implementation from checking evidence for a policy or source relation. See Necula’s Proof-Carrying Code (1997) and Translation Validation for an Optimizing Compiler (2000), available from his primary publication page. This note does not claim that finite local proof obligations implying global correctness is new. It specializes that idea to immutable records, with explicit copied-address bounds and an alias-blind scaffold compilation target.

Static resource certification also has a substantial history, including Hofmann and Jost, Static Prediction of Heap Space Usage for First-Order Functional Programs (2003; author publication record). Their linear heap-use objective is different from the fixed worst-case per-operation access and fresh-allocation bounds used here. Classical persistence, including Driscoll, Sarnak, Sleator and Tarjan (author-hosted paper), does not by itself provide these particular strict bounds or arbitrary context-preservation guarantees.

The residual/bisimulation distinction and pointer-machine assumptions remain those in the foundational contracts. A deterministic transducer is supplied here, rather than synthesized by uniformizing a relation. The stack instance overlaps established pushdown-interface constructions; no new visibly-pushdown expressiveness claim is intended. The rope limitation is a local indistinguishability argument for one presentation, not an imported general data-structure lower bound. These comparisons leave novelty of this exact combined criterion open.

The catenable concat note remains a written source argument conditional on its stated exact buffer contract. This note does not discharge that contract, certify all the source’s level-indexed types, or prove its pop repair cascade. Conditional pop reasoning may use the same buffer contract; proving actual buffer implementations is a separate task, not a reason that conditional reasoning is impossible. The first source questions remain

$$\operatorname{pop\_green}(c)=(x,s) \Longrightarrow C(c)=[x]F(s), \qquad F(\operatorname{ensure\_green}(s))=F(s),$$

with their proper shape premises. The substantive next question is whether a finite shape invariant and tuple interpretation can express those premises and certify the repairs, or whether an explicitly stronger, level-parametric certificate is necessary.

9. Verification status and correction

The theorem and rope proposition have written unbounded proofs above. Neither is formalized in a proof assistant. The executable checker validates the authored JSON rule format only. It derives rule meanings from constructor bodies and compares them with independently written interface equations. Its equation checks are exact symbolic comparisons, not experiments on a finite sample of words. The proof that those comparisons entail correctness is the substitution argument in Section 4.

The recorded output includes input and checker hashes, accepted normal forms, resource bounds and rejection stages. It records ten accepted operation certificates and nine expected rejections, one of which is the intentionally incomplete but semantically valid erasure example. This is regression and artifact evidence, not formal verification of the checker or a complete source compiler.

There is a material qualification to the earlier concat checker: several assertions compare expressions constructed identically on both sides, and its source checks establish names, hashes and selected statements rather than deriving semantics from function bodies. Its recorded count of 107,142 checks must not be read as independently checked source equations or as formal verification of the source refinement. The earlier files remain available as historical algebra sanity checks and source-alignment evidence. The stronger, separately derived normalization check in this note does not retroactively certify the catenable source.