ch:control-operators: ch:control-operators

Problem and result. Implement a finite stack machine together with a represented CPS spine. The four discriminatory cases check whole-spine capture, throw-time stack replacement, persistent reuse, and the two-stage LEM observation. The remaining direct/CPS, declared-cost, and DNE equalities are smoke outputs, not independent evidence.

Representation. Use an explicit list of frames for the live stack and a persistent copy for a captured continuation. Maintain the invariant that this copy contains the complete ordered list, that throw replaces the caller’s list with it, and that the copy remains available to later callers. Give the represented CPS spine one constructor per frame. Host-language functions would be shorter, but would hide equality of saved continuations and prevent finite structural comparison.

First complete version. Implement ordinary arithmetic frames, then capture the entire current list. Throw discards the caller’s list and installs the saved list before evaluation continues. Print the direct/CPS comparison as a smoke check; in this corpus its helper duplicates the stack interpreter and therefore supplies no independent oracle.

Remaining cases. Reuse one saved continuation from two callers to expose persistence. Print the declared capture/throw costs and the reflexive DNE constructor equality only as smoke outputs. Finally encode both stages of the LEM change-of-mind example.

A failing version. Save only the top frame at capture. The module still typechecks and audits cleanly, but complete-spine restoration fails and the LEM observation loses the injection frame.

Acceptance test. Run the four Appendix E commands and require the exact eight cases, the final summary, mutation rejection, and audit output [].

Mathematical boundary. The finite machine illustrates the printed capture, throw, and CPS clauses. It proves neither machine safety nor CPS typing, simulation, normalization, or any classical consistency result.