ch:lexical-effect-handlers: ch:lexical-effect-handlers

Problem, result, and invariants. Build a finite trace model that separates operation names from lexical handler identities, then add the direct exchanger, one-shot resumption, and zero-Lexa clue calculations. The required result is the eight-line report in subsubappendix E.3.9. Maintain two invariants: identity lookup never changes the requested identity, and successful resume changes a fresh cell to consumed before returning.

Frames and the first obstruction. Give every handler frame four fields: identity, effect name, clause result, and exchanger address. Use the stack $$(2,\mathsf{ask},9,200)::\mathsf{call}::(1,\mathsf{ask},7,100)::ϵ.$$ Implement name lookup and identity lookup as separate recursive functions. The former must return $9$; asking the latter for identity $1$ must return $7$. Insert identity $3$, also named $\mathsf{ask}$, before the outer handler and require identity lookup to skip it.

Direct address and one-shot cell. The finite direct model resolves exchanger address $100$ to the same outer handler. Represent a resumption as either fresh with an exchanger address or consumed. Resume on a fresh cell returns the finite witness $\mathit{exchanger}+\mathit{argument}$ and the consumed state; resume on a consumed cell is rejected. The arithmetic result is only an inspectable marker that the correct exchanger traveled through the function.

Hopper calculation. Represent a clue as a label index plus effect name or as a captured-effect clue. A label hopper replaces a specified input index with its caller index and retains the effect name. Check $$⟨\hat{0},\mathsf{ask}⟩\mapsto ⟨\hat{2},\mathsf{ask}⟩\mapsto ⟨\hat{1},\mathsf{ask}⟩.$$ This finite representation does not implement capability and capture-set well-formedness; those remain in the printed SL/TL card.

Mainline boundary. Classify instructions only as move, call, return, or search. Require a mainline list of moves, a call, and a return to contain no search. Require a raise path to contain search. This checks list membership, not elapsed time or the native compiler’s data-section layout.

Failing versions and acceptance. First replace identity comparison with effect-name comparison. The two identity oracles must fail. Restore the source, then return a fresh cell from successful resume; the invalidation oracle must fail. Restore the accepted digest after each mutation. Run all four commands in subsubappendix E.3.9; require eight named PASS lines, the final acceptance line, and audit output [].

Mathematical boundary. The model checks eight finite calculations and two mutation failures. It proves no abstract-machine invariant, simulation, semantic preservation, source type safety, whole-compiler correctness, or cost theorem.