Correctness and time of a query of the Theorem 30 data structure with pruned encodings (queryAt)

Let $P$ be a program of the light language whose procedure number $55$ is the body of queryAt, and in which the routines outDigits (number $52$) and queryCore (number $53$) meet their specifications for the limits $\mathrm{lim}$. Then queryAt meets its specification for $\mathrm{lim}$:

for all parameters $p=(L,m,N)$ with $m\le L$, $t\le m$, block address $b_0$, matrices $X,Y$ with $|X_{ik}|,|Y_{kj}|\le U$, limits satisfying $\mathrm{Lim30}(p,t,b_0,U)$, every memory $\mu$ that holds the data structure for $X,Y$ at $b_0$, every pair $I,J<N$ and every depth $d$ with $d+2\le\mathrm{depth}$, the call $\mathrm{queryAt}(I,J,b_0)$ ends within

steps, returns $(XY)_{IJ}$, the final memory still holds the data structure, and it differs from $\mu$ only in the $3L+m$ scratch cells from the address $\mathrm{WD}(b_0)$.

Setting. The data structure of Theorem 30 is built for parameters $p=(L,m,N)$ with $m\le L$ ($L$ levels, $m$ inner levels), integer matrices $X\in\mathbb Z^{N\times 4^m}$ and $Y\in\mathbb Z^{4^m\times N}$ with entries of absolute value at most $U$, and a threshold $t\le m$. It lives in a block of memory starting at an address $b_0$: the shared tables of Section 2 with the pruned encodings of the $n_B$ row bands of $X$ and column bands of $Y$ (only the leaves whose $L$ decimal digits contain at most $m$ nines are stored), the directory, the table of trie roots (one per tile) and the trie array (one trie per tile, holding the values of its boxes). The limits must satisfy the bounds $\mathrm{Lim30}$: the standing assumptions (an address fits in a word and $100\le\mathrm{word}$), the block fits in memory, and $10^m(7^LU)^2$, $7^{L+1}U$ and $10^{L+1}$ fit in a word.

The query finds the tile of $(I,J)$ from the bands of row $I$ and column $J$, writes the digits of its output string $\eta$, reads the root of the trie of the tile, and evaluates the sum of Lemma 28 from the two encodings and the trie. With pruned encodings the encodings are correct only at the leaves with at most $m$ nines, which are exactly the leaves the query reads.

“Procedure $p$ meets its specification within $T$ steps” means: called at any depth $d$ allowed by the hypothesis, with the given argument values and a memory $\mu$ satisfying the precondition, the body of $p$ terminates within $T$ steps without violating the limits, and the returned value and final memory satisfy the postcondition. Programs are those of the library's light language (procedures numbered by their position in a list $P$, local variables, a memory of integer cells $\mu:\mathbb N\to\mathbb Z$, calls with a nesting depth), which the library compiles to the word RAM; runs are checked against limits $\mathrm{lim}=(\mathrm{word},\mathrm{space},\mathrm{depth})$ on the absolute value of every word, the number of memory cells and the call depth.

Formalization Note The name carries a P because the platform already has Light.Sec4.queryAt_spec, the same lemma for the unpruned data structure of the foundation development. The statement is P[Proc.queryAt]? = some queryAtBody → OutDigitsSpec lim P → QueryCoreSpecP lim P → QueryAtSpecP lim P. The invariant "holds the data structure" is DSReadyP, built on Sec2.SharedReadyP (pruned encodings).