Checking one finite indexed construction language

Working certificate note, 1 October 2026.

This completes an executable check requested by the preceding stored-word study. It is supporting verification work. The automata boundary states the larger semantic question and an exact operation-interface theorem.

Model and finite syntax

The runtime is a finite straight-line immutable construction plan. Every instruction names supplied roots or earlier results. Levels and occupancies are proof expressions, erased from runtime; they have form $c+a_n n+a_p p+a_r r+a_s s$ with integer coefficients. Each listed parameter ranges independently over all natural numbers. There are no remaining inequality guards or correlations. The finite split alternatives have been reparameterized as short occupancy 0,1,2 or long occupancy 3+r.

The checker supports the following fragment of the pinned Rocq types:

Chain endpoint colors range over all 16 combinations of the four binary hues in Color/GYOR.v. Kinds are only,left,right. An inhabited chain has arity 0,1,2, by its Empty,Single,Pair outer constructor. The checker does not construct or infer all node/body/packet witnesses: opaque Chain roots come with their actual source type as a premise. Semi existentially hides arity and colors while preserving the only kind and level.

Empty does not inherit a maximum rank from its allocations. It can be instantiated at any declared natural level. Two separately typed uses may instantiate the same erased empty constant differently. The implementation uses explicit annotated Empty instructions; it is not an inference algorithm for implicit polymorphism. Ground is the Rocq indexed constructor: no claim is made that OCaml allocates a corresponding Ground wrapper.

Arithmetic decision and soundness

For an affine f over independent natural parameters,

$$\forall u\in\mathbb N^4:f(u)=0 \iff \text{every coefficient, including the constant, is zero},$$

and

$$\forall u\in\mathbb N^4:f(u)\ge0 \iff \text{every coefficient, including the constant, is nonnegative}.$$

For necessity in the second statement, set every parameter to zero to test the constant, then send a variable with a negative coefficient arbitrarily large while holding the others at zero. Sufficiency follows by summing nonnegative terms. The first statement follows by the same specializations.

Therefore coefficient comparison exactly decides the affine obligations within this domain. Natural levels/occupancies, level agreement, occupancy lower bounds and output refinements are finite checks. Finite index symbols are checked separately. Under a correlation such as u>=v, the test is not complete: u-v may be nonnegative despite a negative coefficient. Such premises are outside the declared syntax, not silently rejected languages.

Soundness proposition. For every accepted finite plan, every assignment of its independent parameters, and every finite acyclic tuple of supplied values having the declared types and word meanings, executing the plan returns the checked types and word equation, preserves old values, and has the recorded constructor/module-call counts, conditional on the named primitive contracts.

Proof: induct over the ordered instruction list. The arithmetic check supplies the constructor premises at every parameter assignment. Each constructor’s type and word equations determine the next result. A module instruction uses its explicit contract. split3 introduces fresh word variables and its decomposition equation; recursive substitution transports that equation to later values. Literal equality of the normalized output and target gives the word guarantee. No old instruction mutates a field. Finally check the finite output annotations. This is an unbounded written induction, not proof-assistant verification of the Python checker.

It checks supplied annotated plans. A fixed allocation budget alone does not make all annotations finite: Empty can have arbitrarily many level annotations. No complete plan enumeration, representation discovery, source-refinement or general indexed typing theorem is claimed.

Source instance and resources

The model follows VerifiedCatenableDeque commit 503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0. The constructors and routines belong to Viennot, Wendling, Gueneau and Pottier. The current file hashes pin Types.v, Models.v and cadeque_core.ml. Core.v’s make_green_prefix and extract_prefix statements, and GYOR.v’s hue definitions, were inspected. No upstream Rocq development was rerun.

The finite source control is Small/Big followed by the split alternatives 0,1,2,3+r, giving eight plans. The input prefix has occupancy 5+p at level n; the stored head has level n+1; its exposed buffers have level n; the residual child is Semi(n+1). In the Big branch its exposed child has only kind and level n+1. Every admitted head at positive successor level is Small or Big; every >=3-entry buffer has exactly one of the four occupancy cases. This establishes this case coverage, without inferring arbitrary source patterns.

The checker admits all eight plans and derives an output prefix of occupancy at least eight and a child of type Semi(n+1). It derives their word equations from the generic instructions. It does not repeat or replace the preceding helper semantic proofs, or certify the implementations of split/injection, semi_push or semi_concat.

Let each named module call have uniform record-arity bound q0, allocation bound A0 and radius r0. The radius must bound both observations and returned old handles relative to its named argument roots, with no hidden input pointers. Let c be the recorded call count, o the explicit fresh-record count, and d the separately justified input-view address depth. Then

$$q\le\max(3,q_0),\qquad A\le cA_0+o,\qquad r\le d+cr_0+o.$$

The checked fragment has c<=5,o<=3,d=1. These are conservative bounds for this explicit contract-plan model. Output handles are a pair of roots; extra implementation packaging, matching or module wrappers must be charged separately if present. Input path depths are declared view-contract premises, not automatically extracted address proofs. No numerical resource theorem for the whole OCaml library is claimed.

Useful failures and the exact closure boundary

In the short-two case let P have 5+p entries, U three, V two, all at n, and D be Semi(n+1). Returning inject3(P,U) and semi_push(Small(V),D) has the intended formal word PUVD and matching levels. It fails the occupancy premise: Small(V) requires at least three entries. For n=0, P=a^5,U=a3,V=b^2,D=Empty gives the concrete word a^8 b^2. Omitting Small in the long case is a separate sort failure. Wrong Empty kind or level in Big is also rejected even though its empty word cannot reveal the error.

Nor does one-call typing supply iteration of the same view. The input to ensure_green_prefix has a nonempty green child. Take a singleton child holding Small(U) with exactly three n-level entries. The source pop_only_green/Only_end singleton branch returns Empty; pop_green packages it as Semi Empty. extract_prefix exposes U, and short-zero repair leaves Empty unchanged. The output child is therefore outside the original nonempty-green-child input view. This is a written source witness, not a Python execution of the OCaml routine. It disproves closure of that narrow view, not the full deque algorithm, a wider interface, or all realizations.

Reproduction and verification scope

check_indexed_plans.py checks its built-in plans, or one supplied JSON plan with –plan. The Big/long example is a complete input to that interface. Recorded output lists accepted plans, rejected modifications and exact scope. –source PATH checks the three source hashes.

The finite samples corroborate arithmetic and Empty specialization, and the mutation checks test that the checker can reject concrete mistakes. They do not prove the Python checker correct, every source branch correct, primitive costs, or a closed whole deque representation. The affine method, indexed source ingredients and inductive soundness method are established ingredients; novelty is unestablished.