FPRD LabShare an approach

Two-sided boundary certificates for catenation

Working research note, 30 September 2026.

Understand when future computational behavior admits a representation maintained by finite rules with bounded local access and bounded allocation, and what structural obstructions prevent such a representation.

This note tests the finite-boundary method on semi_concat. It closes the indexed shape and composition obligations of this prefix-repair dependency, under explicit buffer contracts. The earlier concat note already gave the word argument. Here the extra work is to expose the bounded fallback, justify the level and occupancy transitions, and state a reusable interface.

Contents

1. Bounded fallback catenation lemma

Fix a set of entries E, an arbitrary interpretation w:E -> Gamma, and immutable representations C with interpretation alpha:C -> Gamma. Fix a natural constant h. Suppose there are total normalizers on admitted inputs

left: C -> Vector(E, <=h) + L
right: C -> Vector(E, <=h) + R.

Each preserves the represented word, using concatenated entry meanings for vectors and declared meanings lambda and rho for L and R. Suppose also:

  • push(e,c) represents w(e) alpha(c), and inject(c,e) represents alpha(c) w(e);
  • join(l,r) represents lambda(l) rho(r) and returns an admitted C;
  • all three operations and both normalizers preserve their declared shapes, have finite bounded rules, and preserve old versions.

Define cat(x,y) by three branches:

  1. If left(x) is vector v, right-fold push over v into the original y.
  2. Otherwise, if right(y) is vector v, left-fold inject over v into the original x.
  3. Otherwise return join(left-view,right-view).

Lemma. For every admitted x,y, including overlapping persistent inputs, the result represents alpha(x) alpha(y), preserves old versions, and has uniform bounded local access and allocation.

Proof. A right-fold of push over e1,…,em has word w(e1)…w(em) alpha(y), by induction on m. A left-fold of inject has word alpha(x) w(e1)…w(em). Substitute the normalizer equations in the first two branches and the join equation in the third. Persistence follows by composition. Since m<=h, unfold each fold into finitely many calls. The maximum over these finite paths bounds old access and allocation. No bound on the lengths of w(ei) is used. This proves the assertion for arbitrary word substitutions and every legal finite history by induction over calls.

Initialization is any fixed finite admitted graph with a declared meaning. Runtime tags, record arities and root registers are finite; values are immutable finite acyclic DAGs. No pointer-identity tests, mutation, lazy evaluation or amortized charges are included. Mathematical proof indices may be unbounded if erased from the finite runtime rules.

This is a sufficient interface theorem. Its hypotheses can be checked by separate branch coverage, typing, word equations and resource certificates for each normalizer and operation. They do not assume correctness of cat. It is neither a characterization nor an optimum bound.

2. Exact source and primitive obligations

Use the companion repository, commit 503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0. The inspected files are lib/cadeque_core.ml and theory/Cadeque/{Types,Models,Core}.v; hashes are in the recorded evidence.

Fix an arbitrary payload set A and natural level l. Put E_l=stored A l. All quantifiers range over finite values satisfying the displayed indexed types, with arbitrary sharing, not just values reached by a selected test. An E_l entry can represent a long word. Interpret Small(p) by the word of p and Big(p,c,s) by the word of p, followed by c, followed by s.

Assume the ordered, level-preserving sequence and occupancy contracts of Buffer.push, inject, single, pair, pop2, eject2, push2, inject2, has7p and has7s. The two classifiers return either all entries in a vector of length at most six or an ordered split into a two-entry boundary and a buffer of at least five. Each primitive must independently have uniform finite-record resource bounds. The original scalar size tests are not silently accepted as finite tags; the earlier bounded-threshold replacement remains the route for supplying these resource contracts.

The preceding single-chain note supplies word-preserving triple/chain conversions for all colors. The following derivation supplies the remaining normalizer obligations without assuming semi_concat.

3. Endpoint insertion is local

For a nonempty chain, push_ne_chain selects its Single packet or the left chain of its Pair. A packet examines just its outer body constructor: Hole edits its tail node; Single_child, Pair_yellow and Pair_orange edit their exposed head node. The edit prepends to that node’s prefix. It does not traverse the nested body. The inject helpers symmetrically edit the exposed suffix, selecting the right chain of a Pair.

Every node interpretation puts its prefix before its child word and suffix after it. Thus these edits prepend or append the new entry to the entire chain word. Adding an entry preserves each required occupancy lower bound, node color, chain arity and exposed colors. At level l+1 the inserted entry must be E_(l+1), even if it flattens to the same word as an E_l buffer. The empty semi-chain branch uses single_chain, whose Only_end has one entry and an empty child. This proves semi_push and semi_inject, as well as their nonempty forms, under the buffer contracts. Each uses one buffer primitive and finitely many constructor blocks and projections.

4. Normalizing one only-chain

For an ending only triple, has7s/has7p supplies either a vector of at most six entries or a Left/Right ending node with a five-entry-or-larger buffer and a two-entry boundary. The empty chain gives V0 separately. Nonempty ending buffers give vectors of lengths one through six. The input word is unchanged in each case.

For a non-ending Only triple, write its word P C S. Its prefix and suffix have at least five entries. For left_of_only split S=S’ Y Z. Then S’ has at least three entries, so Small(S’) is a legal E_(l+1) entry. Inject it into the nonempty child, obtaining word C S’. The Left result has word P (C S’) Y Z = P C S. Its original prefix, node color, child arity and triple coloring remain valid.

For right_of_only split P=X Y P’. Push Small(P’) into the child and obtain X Y (P’ C) S = P C S. Again |P’|>=3, and the retained suffix satisfies the same node-color requirement. These two arguments cover every admitted non-ending triple coloring, including red. They require no green-only restriction.

5. Normalizing a pair

The stored helpers transfer a whole neighboring triple into one stored entry. Let a right triple have word A B R S’ Y Z and let U be a buffer with at least one E_l entry. stored_of_right constructs

Big(U A B, R, S'), (Y,Z).

Its Big prefix has at least three entries; its suffix S’ has at least three because the original right suffix had at least five. Its child is already at level l+1. The returned word is U A B R S’ Y Z, exactly U followed by the original right word. Dually, stored_of_left on left word X Y P’ L A B and nonempty U returns (X,Y), Big(P’,L,A B U), with the same inequalities and concatenated word X Y P’ L A B U.

For left_of_pair, write the left word P L Y Z and the right word R. There are two branches:

  • Ending left: L is empty. Move Y into P, use U=[Z] in stored_of_right, and make its Big entry the singleton child. The new prefix has at least six entries, so an ON node is legal. The child is green, so OST gives a green exposed triple, as required by the original GT/EN input. If stored_of_right returns z,(B,C), its equation is w(z) B C=Z R. The output word is P Y w(z) B C=P Y Z R.
  • Non-ending left: use U=[Y,Z], inject the returned Big entry z into L, and retain P and its node coloring. The output is P L w(z) B C, equal to P L Y Z R. The nonempty insertion preserves child arity and both colors, so the original triple coloring remains valid.

For right_of_pair, write the right word A B R S and the left word L. In the ending case R is empty: move B into S, use U=[A] in stored_of_left, and give the resulting ON node a singleton green child and coloring OST. If the helper returns (X,Y),z, then X Y w(z)=L A, so the output X Y w(z) B S is L A B S. In the non-ending case use U=[A,B], push z into R, and retain S and its coloring. The output is X Y w(z) R S=L A B R S. The same level and minimum-size checks apply.

Consequently make_left and make_right cover Empty, Single and Pair inputs, preserve their words, and return either a bounded vector or an admitted side triple with the required exposed color. Physical inverse views are not needed. Temporary allocations discarded by a fallback still count.

6. The semi_concat contract and resources

Theorem. Under Section 2, for every l and semi-cadeques x,y at level l, semi_concat(x,y) returns a semi-cadeque at level l with word alpha(x)alpha(y) and preserves all retained inputs. Its erased implementation has uniform bounded access and allocation.

Proof. Apply Section 1 with h=6. Sections 3-5 provide the normalizers and insertion operations. For the large-large branch, chain_of_triple preserves each side’s word and returns an arity-one chain of the correct left or right kind. Pair accepts their independently colored sides at the same level, and Semi hides the resulting arity and colors. Its word is the left word followed by the right word. These are the three executed source branches. The conceptual small-small case is already handled by the first branch; the source never normalizes its right input there.

For each buffer primitive let common bounds be qB,rB,AB. Each normalizer makes at most five such calls: the ending pair branch uses one push/inject, one singleton, two stored-helper calls and one singleton for its child. Other branches use no more. At most two normalizers and six fallback insertions are executed. Therefore 16 is a conservative primitive-call bound (not a claim that one path uses all 16). Let B be the maximum number of constructor allocations and pointer projections outside these primitive calls after finite inlining of the displayed helper call graph and the seven vector alternatives. This is an effectively computable syntactic constant; no recursion over depth or level remains. A valid conditional bound is

q <= max(6,qB),  A <= 16 AB+B,  r <= 16 rB+B.

For radius, a path through fresh intermediate records is expanded into the prior calls that supplied its old targets; the sum bounds access in the original pre-call heap. This is a construction bound, not an optimum or a numerical certification of the buffer implementation.

For finite payload tags and a fixed controller with s roots, the reviewed compiler then uses d=max(1,s+Aq), k=r+1 and fixed virtual initialization. It preserves the certified interface’s observations. Sequence equality does not assert physical graph equality or equivalence under arbitrary future scaffold contexts. A scaffold for L gives a PEG for L reversed.

7. Examples, verification and what this adds

Positive boundary cases are empty input, a six-entry ending buffer, a seven-entry ending buffer that now forms a side node, and an ending pair whose five-entry buffer becomes six and hence orange. All entries may denote arbitrary word blocks. Two retained arguments may even share roots.

Wrong fold direction reverses a two-entry boundary before insertion: prepending A then B produces BA instead of AB. Swapping large sides also fails on distinct words. Omitting Small/Big wrappers can preserve a word while violating the level judgment. These failures distinguish semantic, shape and resource obligations.

A useful restricted negative example replaces Vector(E,<=6) by an unbounded immutable linked list and keeps this same entry-by-entry fold algorithm. On a boundary of length m it makes m insertion calls; no uniform call or allocation bound follows, and a push implementation allocating a fresh cons each time allocates m records. This refutes that fallback’s bounded-resource claim only. A rope can join the same words in one record, so no obstruction for every representation follows.

The checker tests the finite symbolic word and occupancy obligations, with recorded output. It pins source hashes, but is a handwritten model, not an OCaml parser, source-refinement proof, complete type checker or Rocq rerun. The written proof provides branch coverage and color reasoning. No buffer internals are verified by this checker.

The primary paper, Sections 1.3.1-1.3.2, explicitly describes finite nonrecursive OCaml operations and verified Rocq fringe equations, while distinguishing the unverified OCaml/Rocq connection and runtime index costs. The algorithms are Kaplan-Tarjan’s, implemented and verified by Viennot, Wendling, Gueneau and Pottier. The generic composition proof is elementary. We claim no new deque or novel verification principle. The useful additional artifact is the explicit certificate boundary and its resource/compiler interface.

The prefix repair can now replace both its semi_push and semi_concat semantic assumptions with these derivations and the buffer contracts. Together with the pop notes, its remaining module obligations lie in the buffer interface. This is meaningful completion of an application, but it does not by itself establish a new fundamental characterization. Further progress should test what the interface predicts for another representation or operation, rather than indefinitely expanding this helper inventory.