ch:typed-metaprogramming: scoped macro expansion

Problem and invariant. Expand a binder-introducing twice macro without capturing caller syntax, and check the finite staged core. Keep source entries $\beta \mapsto o_s$ distinct from scoped entries $\beta \mapsto (a,S,o_h)$. Maintain a bijection $\rho (o_s)=o_h$, extend the origin environment beneath every constructed binder, choose introduction stamps outside the used and input-stamp sets, keep constructed origins distinct from caller and exported origins, and use a variable only at its recorded phase.

Representation and first result. Represent a scoped identifier by an atom and a finite stamp list. Lists make subset and mutation traces readable, although a bit set would make membership faster after assigning stamps dense indices. Implement same-atom comparison, subset, strict subset, candidate collection, and deletion of every dominated candidate. The minimal end-to-end version constructs twice(x) and already prints caller-reference-preserved: the copied argument keeps its caller scopes, while the binder and references written by the transformer receive the introduction stamp.

Origin renaming and provenance. Use different datatypes for source and scoped environment entries. Check that both token maps are injective, that the scoped origins are distinct, and that lookup by each source token returns $\rho$ of its source origin. Represent provenance syntax by references, applications, and lambdas. At a lambda, recurse under the binding consed onto the origin environment. The nested test contains two constructed binders; its inner reference resolves to the inner origin and its second reference resolves to the outer constructed origin. Checking the body under the unextended environment is the deliberately wrong version and prints constructed-binder-unresolved.

Staged core and substitution. Implement phase-indexed lookup and inference for naturals, Booleans, arrows, quotation, splicing, generation, and analytical matching. Check $d:\mathsf{Code}(\mathbb{N})@1$ in $\mathsf{quote}(\mathsf{quote}(\mathsf{splice}(d)))$: lookup occurs at phase one, splice concludes at phase two, and the quotations conclude at phases one and zero with final type $\mathsf{Code}(\mathsf{Code}(\mathbb{N}))$. The evaluator reduces generated addition and the analytical Boolean branch. Capture-avoiding substitution renames a colliding lambda binder before descending.

Observable result and mutations. The exact run is

caller-reference-preserved
introduced-reference-local
rejected: ambiguous-binding
origin-renaming-preserved
constructed-binder-provenance
nested-quotation-typed
generated-normal-form
analytical-true-branch
rejected: ill-staged
beta-capture-avoided
absent-target-alpha-preserved
All 11 Chapter 116 corpus cases passed.

Seven mutants still check and must fail the stdout oracle: collapse the two origin images; omit the provenance-environment extension; ignore the phase in variable lookup; descend below a colliding binder without alpha-renaming; omit the substitution target from the alpha-renaming freshness bound; add the introduction stamp to copied caller syntax; and return false from the true analytical branch. Their changed lines, in the same order, are

Acceptance and boundary. Require a silent check, one passing test, the exact run, an empty audit, and the restored source record in Appendix E. The finite program illustrates origin compatibility, provenance, phase typing, and capture avoidance. It proves neither production hygiene nor the calculus-wide progress and preservation theorems.