appendix sectiontutorials

ch:amortized-resource-analysis: heap-trace checker

Problem and invariant. Execute two finite chapter reconstructions and compare their emitted heap-cell events with the two paper bounds. For pairs, every event is emitted by an actual pair or cons constructor. For startBreadth, every event names one site in the chapter’s explicit accounting schedule; the unavailable 2010 source program is not claimed as the trace source.

Two representations. One can interpret the whole first-order RAML syntax. The companion instead implements attach, spine-copying append, and pairs directly, then a compact-tree traversal and a named allocation schedule over a two-list queue. The two representations are intentionally distinguished.

First complete version. Implement the reconstructed programs and event counter first. Implement $(\binom{n}{2})$ by structural recursion, then check both monomial/binomial identities and bounds at each of the eight inputs. Freeze the chapter table only after the program runs produce it.

A failing version. Delete $28 n$ from the breadth bound. The reconstructed programs still check, but the bound is zero at $n = 1$ while the trace is $16$ , so the inline oracle fails.

Acceptance test and boundary. Run the four appendix E commands and require the exact trace, a passing inline test, and audit []. This proves the finite arithmetic assertions, not AARA soundness or agreement with any RAML release.