queryCore computes the sum of Lemma 28 from the encodings and the trie of a tile (pruned encodings)

Let $P$ be a program of the light language whose procedure number $53$ is the body of queryCore, and in which the routines nineFirst, nineNext, scatter, horner and lookup meet their specifications for the limits $\mathrm{lim}$. Then queryCore meets its specification for $\mathrm{lim}$:

consider the encodings $\mathrm{enc}_A,\mathrm{enc}_B$ of a tile at $a_A,a_B$ ($10^L$ cells each), a trie array $T$ at $\mathit{tr}$ with the root $\mathit{root}$ of the tile's trie, an output string $\eta$ of $L$ symbols with exactly $m$ inner levels whose digits are stored at $\mathit{wd}$, and scratch areas $\mathit{ss}$ ($m$ cells) and $\mathit{box}$ ($L$ cells). Assume the standing assumptions on the limits, $t\le m$, that every box the query reads is found in the trie, that every partial sum of the query and every product $\mathrm{enc}_A(\tau)\,\mathrm{enc}_B(\tau)$ at a leaf $\tau$ with at most $m$ nines fits in a word, $10^L\le\mathrm{word}$, and that the scratch areas are disjoint from each other and from the data, all within memory. Then for every depth $d$ with $d+1\le\mathrm{depth}$, the call $\mathrm{queryCore}(a_A,a_B,\mathit{tr},\mathit{root},\mathit{wd},\mathit{ss},\mathit{box},L,m,t)$ ends within

steps, where $\ell$ is the number of leaves of order below $t$ and $k$ the number of boxes that the query reads, and returns

the products at the leaves of $\eta$ of order below $t$ plus the values the trie holds for the boxes of $\eta$; only the two scratch areas change. When the trie holds the true box values this is the sum of Lemma 28, i.e. the entry of the product for the query.

All leaves read have at most $m$ nines, so the routine is correct on pruned encodings.

“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.

Formalization Note The statement is P[Proc.queryCore]? = some queryCoreBody → Light.Sec4.Query.Callees lim P → QueryCoreSpecP lim P, where Callees bundles the specifications of the five routines; the returned value is trieQuery m t (arrT encA) (arrT encB) T root (digitsO η).