definitionroutine

Controller allowance and clock certificate

Defines allowance and clock certificate: allowance drops at each call
contract checked locally at every call boundary
Definition·def:ctrl-allowance·§11.2 Program states and record bounds

Statement (paper)

A raw controller is the caller's own selection, arithmetic, scoring or terminal-path record, excluding the working states of a query it calls. In a terminal program graph an explicit chain contains only its terminal-path controllers and, in a scoring program, its score suffix or completed score word. The interiors of cap traversals, inverse score ranks, numerical digit queries and paired motions are opaque queries; they are never explicitly pushed working graphs in this chain. A raw controller has an integer allowance w≥1w\ge1 and a numerical clock t≥0t\ge0. Fixed raw constants a0,b0,a′>0a_0,b_0,a'>0 give the following certificate at a call to a lower query or an explicitly pushed raw terminal controller at (w′,j)(w',j): w′<w,j−t≤a′(w−w′),ℓ≤a0(w−w′)+b0(t−j). w'<w,\qquad j-t\le a'(w-w'),\qquad \ell\le a_0(w-w')+b_0(t-j). Here ℓ\ell counts only the suspended caller record, including its delimiters, return modes and pending data. It does not count the callee's physical working space. Without a pending call its own raw records have length at most a0w+b0ta_0w+b_0t. A structural operation has a canonical starting clock zero; numerical queries used by its finite-margin tests are included in this certificate.

In plain English

A raw controller is the caller's own record, excluding the working states of any query it calls. It carries an integer allowance w≥1w\ge1 and a clock t≥0t\ge0, and at each call to a lower query or pushed terminal controller at (w′,j)(w',j) it must satisfy w′<ww'<w, j−t≤a′(w−w′)j-t\le a'(w-w') and ℓ≤a0(w−w′)+b0(t−j)\ell\le a_0(w-w')+b_0(t-j), where ℓ\ell is the length of the suspended caller record. Without a pending call its records have length at most a0w+b0ta_0w+b_0t.

Why it's here

This is the bookkeeping contract that lets the controller realization argue that suspended caller records stay within a space bound, while cap traversals, rank queries, digit queries and paired motions are treated as opaque calls. Because the allowance strictly drops across each call and the clock can rise only in proportion to that drop, the realization theorem and the guarded local graph lemma can check one local inequality at every boundary instead of tracking the whole call chain.
Classified routine:
A bookkeeping definition in the spirit of standard potential-function space accounting for recursive logspace composition, where each call's suspended record is charged against a strictly decreasing budget; it sets up the paper's own controller framework rather than introducing a new idea.

Uses

Nothing else in the paper

Used by

thmController interfaces have restoring O(B)-space implementationslemGuarded local graph for terminal recipesclaimAllowance strictly drops at every boundaryclaimClock invariant bounds shared facilitiesclaimGuarded deterministic finite graph keeps designated pathsclaimProbe copies fit enlarged A,D bound

Sources

PaperOpen
Section
§11.2 Program states and record bounds
Page
—
Label
def:ctrl-allowance
Line
sections/implementation.tex:199
Leannot aligned

Phase 2 aligns this node to a Lean declaration.