Specialization and staging: executable records

These four corpora use the packaged Kappa v0.3.0 executable recorded above. They are working-tree additions based on repository commit 386282d29bd48303 2a4bcd5f6dacd6d2 c9a7fedf; the working tree has no configured origin, and that base commit does not contain the corpora. The accepted source digests below, rather than a nonexistent artifact commit, are therefore the reproducibility authority. They target /Users/wabbit/.local/bin/kappa, whose SHA-256 is 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. No unsafe flag, axiom, admitted lemma, unchecked positivity condition, or unchecked productivity condition is used. From each artifact directory run:

kappa check corpus.kp
kappa test corpus.kp
kappa run corpus.kp
kappa audit corpus.kp

The exact transcripts below include every command result.

Chapter 127: fuelled numeric specialization

Reproducibility record for exercise 127.6. The directory is artifacts/ch127-scheme0-fuelled-specializer/. Its accepted SHA-256 is

Its accepted transcript is

$ kappa check corpus.kp
[exit 0]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
power-3: (x * (x * (x * 1)))
dynamic-if: if0 x then 5 else y
fuel-zero: residual loop(0,x); retained loop(n;x)=loop(n+1;x)
fuel-two: entry loop_0(x); equations loop_0(x)=loop_1(x);
 loop_1(x)=loop(2,x); retained loop(n;x)=loop(n+1;x)
memo-hit: entry same_2(x); equation same_2(x)=same_2(x)
closure-check: computed closed
All 6 Chapter 127 corpus cases passed.
$ kappa audit corpus.kp
[]

Replacing the exact fragment Known (a + b) by Known a produces a typechecking mutant with SHA-256

and changes the dynamic-conditional output to contain then 2; the stdout test fails while audit remains []. The corpus is a bounded specializer and proves no self-applicability or Futamura equation. Removing the retained target loop produces the typechecking closure mutant

and changes the computed closure line to computed open; test fails and audit remains []. This mutation exercises the structured residual-call graph rather than a literal verdict.

The proof companion MixCore.agda was checked with Agda 2.8.0 by running agda MixCore.agda; it uses only Agda built-ins. Its source SHA-256 is

and its checked declarations include mix-sound, static-fold-instance, and dynamic-conditional-instance. It is a proof-carrying online specializer for arithmetic and zero tests: literal residuals are folded and dynamic tests retain both specialized branches. It has no call specialization, memoization, fuel control, or self-application.

The required Scheme0 self-application path is artifacts/ch127-scheme0-fuelled-specializer/ scheme0-self-application.sh. It pins the acquired Chapter 5 archive references/01-core/jones-gomard-sestoft-partial-evaluation/ artifacts/ch5-scheme-partial-evaluator.zip, whose SHA-256 is

and uses its unchanged scheme0.ss, spec.ss, annotate.ss, analyse.ss, and subject.ss. The recorded replay used Gambit Scheme 4.9.8 on arm64 macOS. It specializes the annotated Scheme0 specializer to the annotated power program and to itself, invokes the resulting compiler-generator on both annotated inputs, and obtains

scheme0-power-generator-self=pass
scheme0-cogen-self=pass
scheme0-cogen-definitions=60
All 3 Chapter 127 Scheme0 self-application checks passed.

The wrapper scheme0-self-application.scm has SHA-256

and asserts structural equality rather than a canned status string.

The independent flow-chart self-application path is artifacts/ch127-scheme0-fuelled-specializer/ native-self-application.sh. It pins the acquired Chapter 4 flow-chart archive references/01-core/jones-gomard-sestoft-partial-evaluation/ artifacts/ch4-prolog-partial-evaluator.tar.Z, whose SHA-256 is

and uses its unpacked mix.fc, mixmix.in, cogen.fc, and self.in. The replay used SWI-Prolog 10.0.2 on arm64 macOS with double-quoted strings read as code lists and label_num/1 declared dynamic; both are command-line compatibility settings, so the acquired source remains unchanged. Its stable observations are

native-mixmix=pass
native-cogen-self=pass
native-regenerated-self=fixed-point
native-regenerated-lines=120
All 4 Chapter 127 native self-application checks passed.

The final oracle runs the generated compiler-generator on self.in a second time and requires byte-for-byte equality of the two generated files. The Scheme0 replay is the executable path corresponding to the chapter’s source-bounded theorem. The flow-chart replay is a separate historical cross-check. Neither is a semantic proof or a self-application claim for the Kappa corpus.

Chapter 128: recursive whistle decisions

Reproducibility record for exercise 128.5. The directory is artifacts/ch128-sc-cbv-whistle-visualizer/. Its accepted SHA-256 is

Its accepted transcript is

$ kappa check corpus.kp
[exit 0]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
driver-beta: contract:zero
driver-known-case: contract:zero
driver-open-case: refine:case-zero|case-succ(x)
process-tree: root->{zero,succ(x)}
residual-render: case x of zero=>zero | succ=>succ(x)
full-rule-ledger-1: R1,R2,R3,R4,R5,R6,R7,R8,R9,R10
full-rule-ledger-2: R11,R12,R13,R14,R15,R16,R17,R18,R19,R20
application-ledger: A1,A2,A3,A4a,A4b,A4c
fusion-oracle: one-traversal-equal
unsafe-fold: rejected-constructor-mismatch
variant: fold
growth: whistle
unrelated: drive
variable-base: valid
numeral-base: valid
nullary-coupling: valid
msg-witness: valid
All 17 Chapter 128 corpus cases passed.
$ kappa audit corpus.kp
[]

Replacing the homeomorphic-embedding guard he ancestor current by the variant guard same ancestor current produces a typechecking mutant with SHA-256

and prints growth: drive; the stdout test fails while audit remains []. Deleting the beta contraction produces mutant

and changes the first driver line to outside-projection; check and audit pass, while test fails. The program recursively checks finite homeomorphic embedding, executes the exact local driving projection, renders one process tree and residual case, and computes a finite fusion oracle; it is not the full SC-CBV transformer and proves no termination or improvement theorem.

The proof companion CoreLemmas.agda was checked with Agda 2.8.0 by running agda CoreLemmas.agda; it uses only Agda built-ins. Its source SHA-256 is

and declares the variable, numeral, diving, and coupling constructors of the embedding relation. It proves reflexivity, numeral-label collapse, and one finite witness. The constructors are not lemmas, the witness is not the chapter’s displayed growth pair, and the file contains no full SC-CBV termination proof.

The native comparison implementation is pinned at references/06-programming/klyuchnikov-romanenko-spsc/artifact-spsc/, commit f0016c59400195b28694075ec2517daa0becf10a. Its Haskell spsc-lite-haskell/Supercompiler.hs and companion tests provide an executable positive-supercompilation reference. It is not the exact SC-CBV calculus of the chapter, so no Jónsson–Nordlander theorem is transferred from that repository.

Chapter 129: modal code checking

Reproducibility record for exercise 129.8. The directory is artifacts/ch129-tstage-code-checker/. Its accepted SHA-256 is

Its accepted transcript is

$ kappa check corpus.kp
[exit 0]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
boxed-modal: accepted:Code Nat
boxed-ordinary: rejected
let-box: accepted:Nat
let-box-eval: 7
nested-substitution: accepted:Nat
modal-index-decrement: accepted:Nat
power-code: accepted:Code Nat
power-code-eval: 27
bta-static-fold: 5
bta-dynamic-residual: (2 + x)
All 10 Chapter 129 corpus cases passed.
$ kappa audit corpus.kp
[]

Replacing the box-body call’s empty ordinary-context argument Nil by the caller’s argument ordinary produces a typechecking mutant with SHA-256

and accepts boxed-ordinary; the stdout test fails while audit remains []. Replacing modal-index decrement by identity produces mutant SHA-256

and changes modal-index-decrement to rejected; check and audit pass, but the stdout test fails. The checker covers a finite typed fragment, its complete arithmetic binding-time card, and its generated code. A third typechecking mutant replaces static addition by its left operand; its SHA-256 is

and it changes bta-static-fold: 5 to 2; test fails and audit remains []. The corpus proves no staging or tower theorem.

The proof companion TstageCore.agda was checked with Agda 2.8.0 using only built-ins. Its source SHA-256 is

It intrinsically separates ordinary and modal contexts, enforces an empty ordinary context at box introduction, implements both simultaneous substitutions, and checks beta and box beta. It contains no tower theorem.

The independent tagless-final replay used OCaml 5.4.1 and GHC 9.14.1 in references/06-programming/finally-tagless-partially-evaluated/course/. The accepted source SHA-256 values are

The replay was

$ ocaml final_obj.ml
[exit 0; Warning 8]
$ ocaml final_dic.ml
All done
[exit 0; Warning 8]
$ ghci -ignore-dot-ghci -v0 TTFdB_pe.hs \
  -e 'print main'
PE: adding 1 1
PE: adding 1 1
PE: adding 5 10
PE: adding 1 2
PE: adding 1 2
PE: adding 100 3
PE: adding 3 103
PE: adding 1 2
PE: adding 100 4
PE: adding 1 2
PE: adding 1 3
PE: adding 2 4
True
[exit 0]

In each OCaml run, Warning 8 identifies one deliberately partial object-language matcher. These are the acquired course’s evaluator/dictionary and de Bruijn partial-evaluation fixtures. They execute representations adjacent to the chapter’s small tagless-final algebra; they do not check $\mathsf{Tstage}$ or prove proposition 129.8, proposition 129.9.

An earlier independent MacoCaml replay used the source archive and published Docker image deposited with [XWNY23]. Their recorded SHA-256 values are, respectively,

The source archive remains in the reference dossier. The 573,006,275-byte Docker image was not retained, and neither were the five files extracted from it. Consequently the second digest and the following file digests are a historical replay record, not locally reproducible pins:

The retained artifact README documents the expected behavior of the missing examples: a typed power generator, generated code computing $3^5=243$, a phase error for the wrong leveled import, and a successful fresh-name example. Those statements are documentation supplied by the depositor, not output captured by this book. In particular, the repository contains neither the five example files nor Makefile targets named mpower-show-type, mpower-show-generated, mpower-run, apply-wrong, or apply; the readable unqualified multiplication expression in the README is an editorial paraphrase of its qualified compiler output. A bytecode-only build of the retained compiler source completed on an audit host before the historical documentation target failed, but the resulting binaries were not retained and no binary digest is promoted to a reproducible pin.

Consequently no MacoCaml example execution is claimed here. Reacquiring the 573,006,275-byte Docker image and its /examples directory, verifying the historical file digests, and replaying the documented targets with MacoCaml 4.04.0+dev9-2015-09-05 remain an unresolved reproducibility gap. The archive and README evidence neither prove theorem 129.10 nor test the Tstage rules.

The interpreter-tower comparison was inspected at paper-artifact commit 97ec4cce985528271bd1ac9c40f94a0f0e424d2b and at the later unlicensed Coq-scaffold commit d938bf9cdec5bcfd1f3bf8c1ac2431007da2afe1. The latter still contains the admitted correctness_of_interpretation_inner boundary described in the chapter; neither revision supplies a tower-collapse theorem used by this book.

The comparison artifacts are pinned separately and do not extend the Kappa corpus’s theorem boundary:

• BER MetaOCaml release N153 is archived at references/06-programming/ber-metaocaml/ ber-metaocaml-N153-ocaml-5.3.0.tar.gz, SHA-256 ccde02f992a93f24fced4f706daf03e3 be4ae8d58ea2d49875debb0fed4b4a52; its release test references are under release-source/ber-metaocaml-153/test/. The archive name and changelog describe the OCaml 5.3 port, but its internal README identifies N114 and its INSTALL requires an OCaml 4.14.1 source tree. The audit host has stock OCaml 5.4.1 and no matching patched compiler tree. Those mutually inconsistent build documents prevent an exact N153 replay; no MetaOCaml test output is claimed.

• The acquired LMS checkout is references/06-programming/rompf-odersky-lightweight-modular-staging/ artifact-lms-core/ at commit 361a806f674cd12d9d31655bd0f30664a451ad9f. Its project/build.properties pins sbt 0.13.15 and build.sbt pins Scala-Virtualized 2.11.2 with the continuations plugin. No retained replay has that exact dependency closure, so the official sbt test example supplies no executable evidence here. A separate comparison run used modern sbt 1.11.7; it does not satisfy the historical pin and does not close this gap.

• The Tan–Wei Lean artifact archive is references/05-metatheory/ tan-wei-semantics-preserving-staging/ staging-oopsla26-artifact.zip, SHA-256

  646ae5f4bd82ad5d15bfa4fe43a62a6c
  69d87953ade3cebc0e28ebd303ef92fa

  Its README pins Lean 4.29.0-rc2 and mathlib commit

  abc669d11b88e163aed1c05b352b5b16889c4ad8

  On the ARM64 audit host, the archive was rebuilt with the pinned Lean release and dependency revision:

  $ lean --version
  Lean (version 4.29.0-rc2,
    arm64-apple-darwin24.6.0,
    commit 83e54b65b65d1d3ce31d99d820a7bd5f3e219295,
    Release)
  $ lake build \
      Instar.TwoLevelBasic.Defs \
      Instar.TwoLevelRec.Defs \
      Instar.TwoLevelMut.Defs \
      Instar.TwoLevelFinal.Defs
  Build completed successfully (575 jobs).
  [exit 0]

  No sorry, admit, or axiom command occurs in the archived Instar Lean sources. This replay checks the artifact’s own theorem declarations, including the pure TwoLevelRec and reference TwoLevelFinal semantics_preservation.stepn.rep declarations; it does not prove a theorem for $\mathsf{Tstage}$ or the Scala evaluator below.

• The optimizing-evaluator artifact is references/06-programming/ wei-tan-zhong-let-it-be-optimized/ let-it-be-optimized-artifact.zip, SHA-256 a8e59f581a9eacc136c55117479b8bb72 b328ca97376a8acb910e9da44ae23df. The unmodified archive was run with Temurin JDK 17.0.20.1, sbt 1.11.7, and the archive’s pinned Scala 3.8.0:

  $ sbt -batch test
  [info] Passed: Total 67, Failed 0, Errors 0, Passed 67
  [success] Total time: 14 s
  [exit 0]

  Compilation issued 68 exhaustivity or narrowing warnings for deliberately partial host-language matches; no warning was treated as a passed test. The 67 tests exercise the five definitional evaluators, the CEKM machine, CSE, constant folding, dead-code elimination, inlining, intensional analysis, partially-static data, lambda hoisting, and the Section 12 extensions indexed by ARTIFACT-README.md. They verify the artifact’s expected generated strings, not contextual equivalence or compiler correctness.

• The tower repository and its incomplete proof scaffold are the two revisions recorded above. Their successful examples are execution evidence; the admitted Coq lemma prevents a proof claim.

These pins make acquisition and replay boundaries exact. The Lean and optimizing-evaluator replays above succeeded at their pinned toolchains; MetaOCaml and LMS remain unresolved for the exact mismatches printed above.

Chapter 130: dependent stage checking

Reproducibility record for exercise 130.6. The directory is artifacts/ch130-dependent-stage-checker/. Its accepted SHA-256 is

Its accepted transcript is

$ kappa check corpus.kp
[exit 0]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
vector-index: Vec(1)
quote-dependent: Code(Vec(1))
escape-beta: Vec(1)
csp-shift: Nat
raw-crossing: rejected
All 5 Chapter 130 corpus cases passed.
$ kappa audit corpus.kp
[]

Replacing the zero-index lookup result’s stage-equality conditional by unconditional Some ty produces a typechecking mutant with SHA-256

and accepts raw-crossing; the stdout test fails while audit remains []. The one-name finite witness checker and evaluator do not represent distinct stage names or stage abstraction and application and do not mechanize preservation, confluence, normalization, or progress. The proof companion SubstitutionCore.agda was checked with Agda 2.8.0 by running agda SubstitutionCore.agda; it uses only Agda built-ins. Its source SHA-256 is

and checks raw dependent index/type substitution beneath vector indices and dependent codomains, plus a natural-stage-depth intrinsic term core with length-indexed vectors, explicit persistence, simultaneous substitution, typed beta and quote–escape steps, and preservation by construction. The two layers do not form a full mutually intrinsic calculus and prove no theorem for arbitrary stage words, general dependent conversion, confluence, or normalization.

Chapter 52: the category of contexts

Reproducibility record for exercise 141.23. artifacts/ch141-ctx-category/ contains the portable Kappa corpus for the category $\mathbf{Ctx}$ of contexts and substitutions. Accepted source SHA-256: b9f905d938ba28d139d3293eb5b0ac72 17f16c6e6cb778189e4839b7391eda70. The tested compiler, SHA-256 efe8214b6f4fe41e6104c8a418920781 a8c1f9f8cf9d5139db3c009055b622a3, was built with GHC 9.14.1 from a clean source archive of Kappa commit f7012f81bb940648f53253b7dbefc798a33142b6. The specification and conformance-ledger digests coincide with the corresponding clean compiler pin and are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 11 Chapter 141 corpus cases passed.; audit returns []. Eleven cases replay the chapter’s named calculations and boundary conditions: the first composite, the associativity instance, the capture instance, both identity laws, the seminar binder composite, the two directions of the Yoneda bijection on the term $x\mathsf{tt}$, the canonical renaming of a context with its inverse, substitution through a conditional, rejection of a noncomposable pair, and a seventeen-name freshening boundary. The renamings compose to identities as proposition 141.48 requires. Two regenerable mutations are recorded in the artifact’s MUTATIONS.md: disabling binder freshening fails exactly the capture case, and composing in the wrong order is rejected in the first composite, associativity, the right identity, the seminar composite, and one direction of the equivalence. The corpus works around the compiler defect KAPPA-BOOK-001 (a three-operand conjunction inside a do-block let is rejected), recorded in the repository’s Kappa issue ledger with reproducers under issues/. This is executable behavior evidence for the substitution algebra on named inputs; it proves neither the action law nor the Yoneda lemma, which the chapter proves.

Chapter 54: fuelled rewrite normalization

Reproducibility record for exercise 116.21. artifacts/ch148-explicit-substitution-normalizer/ contains the portable Kappa corpus for explicit substitutions. Accepted source SHA-256: 5c6c2e2917f0d821 2cfd4ca652e49e56 aec03e31053bd5ba 842e5652ee2f76fa. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 148 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Treat an ill-scoped lift as a normal substitution. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 62: endpoint-preserving path operations

Reproducibility record for exercise 189.17. artifacts/ch189-path-groupoid-checker/ contains the portable Kappa corpus for path groupoid laws. Accepted source SHA-256: 6a398be488ba1562 f24d0e8aecb59684 84ad6acaa0bae885 2b00e8303765c42a. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 189 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Construct a composite even when its middle endpoints differ. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 65: two-element transport tables

Reproducibility record for exercise 193.17. artifacts/ch193-univalence-transport-simulator/ contains the portable Kappa corpus for transport along finite equivalences. Accepted source SHA-256: 4a0219421237ad12 40d5fc72c1bf3c74 6a554cfb616f83df 730e92f0b6f948f0. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 193 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Declare every two-row table bijective. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 66: finite level classification

Reproducibility record for exercise 195.28. artifacts/ch195-finite-truncation-auditor/ contains the portable Kappa corpus for finite truncation levels. Accepted source SHA-256: d525bfd2f7fced33 3cf2fd906ec2415c 0102b48afdeb81ff 1db7a2ab2acf256a. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 195 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Mark Boolean as a proposition. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 68: finite endpoint checking

Reproducibility record for exercise 198.26. artifacts/ch198-hit-boundary-checker/ contains the portable Kappa corpus for HIT constructor boundaries. Accepted source SHA-256: dd7489e9e27120b6 8c4083c39bb44c47 bc80ea3542714a6c 0dc266deb5678f6f. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 198 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Check only the target of a suspension meridian. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 69: adjacent-inverse cancellation

Reproducibility record for exercise 202.13. artifacts/ch202-van-kampen-word-reducer/ contains the portable Kappa corpus for free-group word reduction. Accepted source SHA-256: 8db216c37bace614 acb9e1e71d5110b2 10b8e3e5dc69de79 db755321b1454c6e. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 202 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Disable cancellation for one inverse pair. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 74: two-object isomorphism classification

Reproducibility record for exercise 207.15. artifacts/ch207-finite-rezk-skeleton/ contains the portable Kappa corpus for finite skeletonization. Accepted source SHA-256: fead7a0fc0e07d11 774567e0a3148df0 9377425595e761e8 8c2f5aef88cd7322. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 207 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Merge as soon as one arrow exists. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 76: finite cardinal-expression evaluation

Reproducibility record for exercise 210.5. artifacts/ch210-finite-cardinal-evaluator/ contains the portable Kappa corpus for finite cardinal expressions. Accepted source SHA-256: a2942bb2dca0edee8f094dd17c65cb02f1169ded7cf339ceba54658e9ab951b9. The tested distribution is installed Kappa v0.3.0, embedded build identifier kpp-hskll-0.3.0-1df6e4b1, on arm64 macOS. It exposes no compiler source commit or implementation toolchain, so neither is claimed. Its binary, bundled specification, and conformance-ledger hashes are recorded in the artifact README. The separate wabbit-corp/kappa commit recorded there is a specification-only snapshot, not compiler provenance. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on artifacts/ch210-finite-cardinal-evaluator/corpus.kp. The run ends All 4 Chapter 210 corpus cases passed.; audit returns []. Replacing the sum clause by its left operand makes kappa test exit nonzero and makes the run end Chapter 210 corpus failed. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 77: dyadic bracket refinement

Reproducibility record for exercise 211.4. artifacts/ch211-dedekind-bracket-refiner/ contains the portable Kappa corpus for dyadic brackets around $\sqrt{2}$. Accepted source SHA-256: e1706ef80041f2e3e2674e359fbef4ca78381567b01d110ab16514044e99b716. The tested distribution is installed Kappa v0.3.0, embedded build identifier kpp-hskll-0.3.0-1df6e4b1, on arm64 macOS. It exposes no compiler source commit or implementation toolchain, so neither is claimed. Its binary, bundled specification, and conformance-ledger hashes are recorded in the artifact README. The separate wabbit-corp/kappa commit recorded there is a specification-only snapshot, not compiler provenance. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on artifacts/ch211-dedekind-bracket-refiner/corpus.kp. The run ends All 4 Chapter 211 corpus cases passed.; audit returns []. Omitting the factor two in the midpoint-square comparison makes kappa test exit nonzero and makes the run end Chapter 211 corpus failed. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 79: recursive code/type checking

Reproducibility record for exercise 215.18. artifacts/ch215-observational-equality-normalizer/ contains the portable Kappa corpus for observational equality codes. Accepted source SHA-256: 80df7642189ca5b8 c69699631d24960e c9c5866ba9753b06 3cfe5b7f6f260004. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 215 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Accept a natural-number code at Boolean type. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 80: truth-table evaluation and overlap checking

Reproducibility record for exercise 217.22. artifacts/ch217-demorgan-face-normalizer/ contains the portable Kappa corpus for De Morgan face formulas. Accepted source SHA-256: b8e29d6908afec76 d0bfc1fc2ff0b9f1 9ff56d54e376d4de 3d9e450a3645ad22. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 217 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Interpret reversal as the identity. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 81: finite entailment and overlap checking

Reproducibility record for exercise 218.18. artifacts/ch218-cartesian-cofibration-checker/ contains the portable Kappa corpus for Cartesian cofibrations. Accepted source SHA-256: e32c580874ca37b6 4ae8d47e58166e09 65aba253cdea8780 080ce67da3607f43. The pinned compiler commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested binary, specification, and conformance-ledger hashes are recorded in the artifact README. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 218 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Erase the diagonal locus. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.