Manuscript X-K-ST@1 · X-K-ST.tex · proposition · 93c39c0f
Proposition: Resource soundness
Occupancy, storage, and no enlargement › Cut-by-cut ledgers · lines 989–1008 · proof included or linked
X-K-ST@1#prop:resource
The maxima in (eq:peak) are finite. A legal execution obeys the stated peak and storage bounds when every allocation, communication buffer, release, and returned output is included in its cut specification.
Proof. There are finitely many branches and finitely many cuts, each with finitely many finite registers. Their specified indicator sums are therefore finite.
Each allowed instruction changes the live-name and ownership lists by its declared input/output rule. Induction over an execution identifies the actual lists with the certificate lists at every cut. Their maxima are the asserted bounds.