Object calculus checker and evaluator

Reproducibility record for exercise 25.17.

The pinned companion is artifacts/ch25-objects/corpus.kp. It is checked with Kappa commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the accepted source SHA-256 is 33ca277edaa2b99d423fb45d6018a372404024bd90714a2b2b0dde8a92c0ef90. Run

kappa check artifacts/ch25-objects/corpus.kp
kappa test  artifacts/ch25-objects/corpus.kp
kappa run   artifacts/ch25-objects/corpus.kp
kappa audit artifacts/ch25-objects/corpus.kp

The seven stable cases exercise late self across $p/q$, persistent override, missing-method rejection, runtime minimum reannotation, rejection of covariant components for update, a recursive fluent object, and the recursive-create trace against frozen self. The run ends with

All 7 Chapter 25 corpus cases passed.

The audit is empty. Three real mutations are recorded in the README: frozen self ff035f330eda9fec3693bbf8a6cb584abf0a93c072a3872d94b3cbfdf19a147c, apparent-supertype reannotation 3c655ec8c2c2cda241dc35a55db6534d86e0e991f10e4d3daca8438ceeeda056, and covariant shared components 46766c272846ad078df2e11b3ec023b1403cd2a56fd50e7ab137ded51d6ff88f; each makes its intended positive/negative assertion fail. The evaluator is a bounded executable model of the printed fragment. Passing it is evidence for the examples only, not a mechanized proof of the chapter’s metatheorems.

Chapter 26: corrected overwrite step

Reproducibility record for exercise 26.10.

The portable companion is artifacts/ch26-corrected-row-unifier/corpus.kp, accepted at SHA-256 aae9e62839d5a3c61762005e6b5b863b2c4162ce2be92653b04e7ce1f6cf2c90. It uses compiler source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested local compiler binary has SHA-256 476688a4b6078aaef4e7a23f46383a3879df40d391bca7d6878545197a002d01. Run

kappa check artifacts/ch26-corrected-row-unifier/corpus.kp
kappa test  artifacts/ch26-corrected-row-unifier/corpus.kp
kappa run   artifacts/ch26-corrected-row-unifier/corpus.kp
kappa audit artifacts/ch26-corrected-row-unifier/corpus.kp

The run prints six named PASS lines and ends with

All 6 Chapter 26 corpus cases passed.

The audit prints []. The solver constructs all four branches from a symbolic overwrite equation, identifies each concrete witness’s branch, compares the resulting updated two-label rows, and checks coverage of all four shapes. A separate row model over labels $a,b$ accepts the empty and $a$-only inputs for $W$ while rejecting inputs whose $b$-field survives update; the corpus does not claim that two shapes cover the full row universe. The shared-row input becomes an actual presence-obligation output. Length plus witness coverage makes omission of any one branch fail the frozen oracle. The program is finite regression evidence; it proves no solver termination, completeness, finite-complete-set, or nonprincipality theorem. No Kappa defect or conformance-suite change was required. The concatenation case inspects the selected origin, rather than only the length of the origin list, and the final success summary is conditional on all six case booleans.

Self types and matching: executable boundary

Reproducibility record for exercise 21.15.

The portable finite companion is artifacts/ch27-self-matching/corpus.kp. It represents positive-Self variance, reference invariance, record protocols, matching without subsumption, and packages as ordinary Kappa data. Introduction checks positivity and matching before sealing a payload with one hidden witness; opening checks that same witness in the payload and result positions. The accepted SHA-256 is 3008dea7235d8c9d58569da8954b204d95b25a6e2d2adac4eb5b522b5b034af3; it uses portable kappa-v1 at compiler source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. Run

kappa check artifacts/ch27-self-matching/corpus.kp
kappa test  artifacts/ch27-self-matching/corpus.kp
kappa run   artifacts/ch27-self-matching/corpus.kp
kappa audit artifacts/ch27-self-matching/corpus.kp

The run prints seven PASS lines and ends with All 7 self/matching corpus cases passed.; the audit prints []. The negative-control targets reverse arrow polarity incorrectly, admit $\mathsf{Ref}X$, and omit result-witness checking; each typechecks and fails the frozen stdout oracle. These runs check the finite examples, not matching soundness, preservation, progress, or the step-indexed fundamental theorem.

Finite operation trees, CBPV, and deep handlers

Reproducibility record for exercise 22.21.

The executable companion is in artifacts/ch28-effects-cbpv. It represents a finite first-order instance of the chapter’s operation trees, defunctionalized sequencing, state and exception folds, deep choice handling, and a fueled force/thunk-and-sequencing evaluator as object-language data. The chapter contains the mathematical proofs. The companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0, specification digest 84ca9ed0659956261853a9dace910ef0bd8edd8670ad3b346bdb387d9313ae1b, and conformance-ledger digest 41b1afa1a4e63f9492d637774544c81784e616d3d4a4af495ab0244de0304b94. The accepted corpus digest is 317cb9855c0e005675a7ec9a45146b9e56aa6be0181ebeb44735b5947aed8698.

From the repository root, run

kappa check \
  artifacts/ch28-effects-cbpv/corpus.kp
kappa test \
  artifacts/ch28-effects-cbpv/corpus.kp
kappa run \
  artifacts/ch28-effects-cbpv/corpus.kp
kappa audit \
  artifacts/ch28-effects-cbpv/corpus.kp

The check is silent, the inline harness passes one corpus, the run ends with

All 8 effects corpus cases passed.

and the audit prints []. The cases exercise CBPV force/thunk and sequencing, three tested monad equations, algebraicity, both orders of state and exception handling, forwarding, deep nested choice, and the choice-node handler/fold equation.

Three typechecking semantic mutations fail the frozen stdout oracle. Omitting recursive handling of the true choice branch exposes a nested request; retaining the old state at put erases the commit update; and replacing the get-forwarding constructor by its false branch discards a request. Restoring the accepted source restores all eight cases. The README records the exact pin, commands, output, and limitations. These executions are implementation evidence only: they do not prove the chapter’s monad, safety, simulation, agreement, quotient, or termination results, and they do not claim interpreter–native-backend parity.

Scoped substitution in Kappa

Reproducibility record for exercise 23.15. The executable companion is artifacts/ch29-scoped-operations/corpus.kp. It targets the Kappa compiler on PATH; no developer-cache path is part of the published contract. The pins used for the accepted run are

From the repository root, the required acceptance commands are

export LANG=C.UTF-8 LC_ALL=C.UTF-8
kappa check \
  artifacts/ch29-scoped-operations/corpus.kp
kappa test \
  artifacts/ch29-scoped-operations/corpus.kp
kappa run \
  artifacts/ch29-scoped-operations/corpus.kp
kappa audit \
  artifacts/ch29-scoped-operations/corpus.kp

All four exit successfully. The test command reports one passing test and no failures or harness errors; the audit prints []. The complete run output is

PASS ordinary substitution descends through ordinary branches
PASS scoped substitution preserves ordinary parameters
PASS scoped substitution leaves the scoped computation untouched
PASS scoped substitution composes only the continuation
PASS tested substitution equations and monad laws hold
PASS false algebraicity and all-fields traversal are distinguished
All 6 scoped-operations corpus cases passed.

The artifact represents continuations by a finite Kont datatype. Or stores ordinary recursive branches. Once stores a scoped computation and an explicit continuation. Local additionally stores the ordinary name and initial-state parameters. Thus one field-level mistake cannot masquerade as another.

The script artifacts/ch29-scoped-operations/run-mutations.sh creates temporary copies and checks three semantic mutations. Each mutated source passes kappa check, produces [] under kappa audit, and makes both kappa test and kappa run exit nonzero:

1. all-fields-traversal maps the post-computation through the Once body while retaining the composed outside continuation; the body-preservation and pairwise-distinction oracle lines fail;

2. corrupt-local-parameter increments the stored initial-state parameter during bind; the parameter-preservation oracle fails;

3. reverse-continuation composes the new continuation before the old one; continuation order and the tested associativity instance fail.

The accepted module uses @PrivateByDefault and exports only public main. The script then reruns check, test, run, and audit on the untouched accepted corpus and reports

PASS accepted corpus restored and rechecked

These executions illustrate a finite construction. They do not prove lemma 23.5, lemma 23.10, theorem 23.11, corollary 23.12; nor do they establish any handler-safety or operational theorem, since chapter 23 defines no operational handler language. Acceptance is interpreter-only; no native-backend parity claim is made.

Higher-order source bind and modular elaboration

Reproducibility record for exercise 24.17.

The executable companion is artifacts/ch30-hefty-elaboration/corpus.kp. It is a portable kappa-v1 finite model of result tags, higher-order source nodes, first-order target trees, source bind, catamorphic elaboration, disjoint component dispatch, state and throw handling, and empty-signature observation. The companion checks tags dynamically and does not claim the intrinsic Agda types of the chapter.

The Kappa source commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the specification and conformance-ledger digests are respectively 84ca9ed0659956261853a9dace910ef0bd8edd8670ad3b346bdb387d9313ae1b and 41b1afa1a4e63f9492d637774544c81784e616d3d4a4af495ab0244de0304b94. The repository-local compiler digest is 476688a4b6078aaef4e7a23f46383a3879df40d391bca7d6878545197a002d01. The accepted corpus digest is 899757b46ec93102abf15c5348ed7250b64a9463fc6b5a672d6d3887dd11329c, the README digest is f0e50b41ac8c63d7c31fd55159cd2cc032ff582e884d76d07c5d87a5bc0312c2, and the retained transcript digest is 0b1e0aeb2a22454af30053c858977c87a49f97d492a67b5c24ce85c6e6518bb3.

From the repository root, run

K=kappa
$K check artifacts/ch30-hefty-elaboration/corpus.kp
$K test  artifacts/ch30-hefty-elaboration/corpus.kp
$K run   artifacts/ch30-hefty-elaboration/corpus.kp
$K audit artifacts/ch30-hefty-elaboration/corpus.kp

The run ends with

PASS global transaction Just(2)
PASS alternative transaction Nothing
PASS correct bind state 1
PASS structural bind state 2
PASS mismatched catch rejected and operation dispatch unique
All 5 Chapter 30 corpus cases passed.

and the audit is [].

Four typechecking semantic mutations fail both the inline oracle and the program’s acceptance guard. Making the alternative catch globally has digest e2688f460b00362b06fb07a99ebb913ced32cfbc352f645ed5c0d7a5bbef5dbb and flips the alternative transaction. Recursing through the catch-owned branches during source bind has digest 6bb042c31539fd7e4e570027775837db4950c156579db0eb12a3fd8cc5f9a5b3 and flips the correct-bind count. Omitting the fallback tag check has digest 67f9ce08465455591ad39c24fb33fb16d6147c5e5540ae823e96bd46924765eb and accepts the mismatched catch. Making the throw component also own the catch tag has digest 25164a3b69200db649fe8389583a9a0f676b6408569713dbe2ea834cc81044a0 and violates unique dispatch. The accepted source was restored and all four commands passed again.

The primary artifact is references/06-programming/hefty-algebras/hefty-pop2023-artifact.zip, SHA-256 09dafad16f63bf2473c51988f312af8f3175c64dd1310b81c2fb1253540e3f4d, at commit 539a2a6bcdf1c3d9ad9a4e186c39302ea365b6ab. This archive is retained as historical primary evidence, not as a rebuild performed during this pass. The audit host had no Agda executable, the archive did not retain Git metadata with which to verify that commit, and its standard-library submodule content was not vendored. The claims below are therefore source-audit claims rather than a fresh Agda acceptance run. Its src/Law/Hefty/Catch.agda imports function extensionality from src/Postulate/Extensionality.agda; the reusable lawfulness interface is relative to that postulate. Its bind-throw field checks the homogeneous result-code instance; the chapter’s heterogeneous bind–throw equation is a separately proved local strengthening. The transaction observations in src/Example/Hefty/Catch+Throw+State.agda close by refl. The Kappa model is an independent finite observation model, not a replacement for this Agda evidence. Neither executable establishes monad laws, catamorphism uniqueness, modularity, simulation, inference, or progress.

Duplicate effect rows, unification, and handler traces

Reproducibility record for exercise 25.15.

The companion artifacts/ch31-effect-rows represents finite labels, duplicate-preserving open rows, substitutions, exposure/unification, one-layer handler frames, and two Algorithm-W row traces as object-language data. Chapter 25 supplies the mathematics; the companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0, specification digest 84ca9ed0659956261853a9dace910ef0bd8edd8670ad3b346bdb387d9313ae1b, and conformance-ledger digest 41b1afa1a4e63f9492d637774544c81784e616d3d4a4af495ab0244de0304b94. The accepted corpus digest is 95558200cecd4ab844eaf9c98e48866ceaadd398a678fe1f7850a02e2c204173.

From the repository root, run

K=kappa
$K check artifacts/ch31-effect-rows/corpus.kp
$K test artifacts/ch31-effect-rows/corpus.kp
$K run artifacts/ch31-effect-rows/corpus.kp
$K audit artifacts/ch31-effect-rows/corpus.kp

The check is silent, the inline harness passes one corpus, the run ends with

All 8 Chapter 31 corpus cases passed.

and the audit prints []. The cases cover row exchange without contraction, one-occurrence cancellation, exposure and open-row MGU calculation, the shared-tail guard, the transaction’s three W equations, one-layer forwarding, rethrow followed by outer fallback, and the reader handler’s output-tail equation.

Three typechecking semantic mutations fail the frozen stdout oracle. Recursing on the unmodified row rather than the cancellation residual has digest cbe00a3d13527b5083d97143d2ce7dac23402890175f1afa90f1897b6135f985; replacing the distinguished shared-tail guard result by a generic unification failure has digest 46757ebd87355b72c73e73ace0515bc5a9ec12ba6cdf4701d5018c3d3589e4e0; and treating a forwarding frame as an immediate return has digest 7dc7845176e9569d9d7b9320c5af3b34476e727093e66c05a61d22fa40c0b372. Each mutant passes check and audit but makes both test and run exit unsuccessfully. Restoring the accepted source makes all four commands pass. The README records their exact output, compiler identity, mutation failures, and limitations.

This bounded first-order execution is implementation evidence only. It does not prove row-equivalence completeness, cancellation, unifier termination or factorization, Algorithm-W soundness or principality, preservation, progress, the source calculus’s restricted typing translation, or any theorem about Kappa.

Finite authority, label, translation, and tunnelling model

Reproducibility record for exercise 32.16. The portable kappa-v1 companion is artifacts/ch32-effect-capabilities-tunnelling/corpus.kp. It represents operation names, handler identities, runtime labels, authorities, closure classes, validated handler stacks, a finite Effekt source, and a finite System-$\mathsf{Xi}$ target as ordinary Kappa data. Kappa’s own effect facilities are not used as an oracle.

Acceptance used the interpreter built from clean Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the compiler executable SHA-256 is

The specification and conformance-ledger SHA-256 values are respectively

and

The accepted corpus SHA-256 is

Place the pinned compiler on PATH. From the archive root run

export LANG=C.UTF-8 LC_ALL=C.UTF-8
kappa check artifacts/ch32-effect-capabilities-tunnelling/corpus.kp
kappa test  artifacts/ch32-effect-capabilities-tunnelling/corpus.kp
kappa run   artifacts/ch32-effect-capabilities-tunnelling/corpus.kp
kappa audit artifacts/ch32-effect-capabilities-tunnelling/corpus.kp

The check is silent, the harness reports one passing corpus, the audit prints [], and the run is

PASS authorized request reaches the outer handler
PASS dynamic lookup captures the nearer same-operation handler
PASS equal operation names do not identify equal handlers
PASS closure crossing an abstraction boundary retains outer authority
PASS second-class closure escape is rejected
PASS capability use outside its label scope is rejected
PASS Effekt-to-Xi translation retains the required capability label
PASS tunneled request crosses the intervening same-operation handler
PASS duplicate active identities or labels are rejected
PASS duplicate source identities or labels are rejected by translation
All 10 Chapter 32 corpus cases passed.

Five one-site semantic mutations were applied separately. Each passes kappa check, leaves an empty audit, and makes the unchanged kappa test and kappa run oracles exit unsuccessfully:

The exact full hashes, edits, statuses, and output are retained in MUTATIONS.md and TRANSCRIPT.txt. Restoring the accepted digest makes all four acceptance commands pass again.

The translation preserves identities and labels supplied by a validated source term; it does not allocate fresh ones. Stack validation separately rejects identity reuse and label reuse by a distinct identity. Translation validation tests the same two failures for source bindings. These finite checks are implementation evidence only. They do not prove System-$\mathsf{Xi}$ progress or preservation, the Effekt translation theorem, effect safety, tunnelling parametricity, logical soundness, or any theorem about Kappa. Acceptance used the interpreter only; no native-backend parity claim is made.

Finite modal actions and source translations

Reproducibility record for exercise 33.13. The portable kappa-v1 companion is artifacts/ch33-modal-effect-types/corpus.kp. It represents labels, effect lists, absolute and extension modalities, a duplicate-bearing row arrow, a capability block, and their finite translations as object-language data. Kappa’s own effect system is not used as an oracle. The accepted corpus SHA-256 is

From the repository root, run

kappa check artifacts/ch33-modal-effect-types/corpus.kp
kappa test  artifacts/ch33-modal-effect-types/corpus.kp
kappa run   artifacts/ch33-modal-effect-types/corpus.kp
kappa audit artifacts/ch33-modal-effect-types/corpus.kp

The checker is silent, the inline harness reports one passing corpus, and the audit prints []. The run is

PASS absolute modality replaces the ambient effects
PASS extension modality retains the ambient effects
PASS modality composition is left to right
PASS row translation preserves duplicate labels
PASS row arrows translate to absolute boxes
PASS capability blocks bind an explicit effect variable
PASS capability calls instantiate the formal effect
PASS modal elimination rejects the wrong ambient context
All 8 Chapter 33 corpus cases passed.

Three one-site semantic mutations were replayed separately. Making absolute action prepend rather than replace, returning a singleton from the duplicate row translation, and returning the empty effect list from capability instantiation each leaves check successful and audit empty, but makes both test and run exit unsuccessfully against the unchanged oracle. Restoring the accepted source makes all four commands pass.

This artifact observes eight finite distinctions only. It proves neither Met progress nor subject reduction, neither source type-preservation theorem, neither operational-preservation theorem, and no property of the Kappa compiler. The retained METL artifact is independent implementation evidence for its surface checker, interpreter, and examples; it implements neither source translation.

Lexical lookup, resumptions, and hopper traces

Reproducibility record for exercise 34.13. The portable kappa-v1 companion is artifacts/ch34-lexical-handlers/corpus.kp. It represents handler frames, exchanger addresses, one-shot cells, clues, and instruction classes as object-language data. It implements none of Lexa, Salt, SL, or TL. The accepted corpus SHA-256 is

From the repository root, run

kappa check artifacts/ch34-lexical-handlers/corpus.kp
kappa test  artifacts/ch34-lexical-handlers/corpus.kp
kappa run   artifacts/ch34-lexical-handlers/corpus.kp
kappa audit artifacts/ch34-lexical-handlers/corpus.kp

The accepted run is

PASS nearest-name search selects the inner handler
PASS identity search selects the lexical outer handler
PASS identity search skips a nearer same-name handler
PASS direct exchanger lookup selects the lexical handler
PASS resumption use invalidates its cell
PASS a consumed resumption is rejected
PASS two hoppers preserve lexical provenance
PASS mainline code has no search while raise code does
All 8 Chapter 34 corpus cases passed.

The checker is silent, the inline harness reports one passing corpus, and audit prints [].

Two one-site semantic mutations were replayed. Replacing identity comparison by effect-name comparison leaves check and audit successful but makes both identity oracles fail. Returning a fresh resumption cell after successful resume likewise remains well typed but makes the invalidation oracle fail. For each mutant, test and run exit unsuccessfully. Restoring the accepted digest makes all four commands pass.

The corpus is finite execution evidence. It proves neither 2024 Lexa-to-Salt behavior preservation nor 2025 SL-to-TL simulation, and its instruction list is not a cost model or a benchmark reproduction.

Pinned native-artifact audit.

The exact 2024 archive references/06-programming/lexical-effect-handlers-direct/artifact-2024/lexa.tar has SHA-256 d23ca439dd6be214 10371a494b94a2c2 dfbf85d6a5a361b7 5ab1560f3f587bc7. Its README supports only x86-64 and uses Nix; its formal translation test also uses Racket. The exact 2025 archive references/06-programming/zero-overhead-lexical-handlers/artifact-2025/lexa_oopsla25.tar.gz has SHA-256 . Its README requires x86-64 Linux, 32 GB, four cores, and privileged Docker access to CPU performance counters. The maintained checkout is pinned at 1117dfbf7837ffa3c858674e10ae2fa00e21ad6d.

The audit host is arm64 Darwin and its Docker server is arm64 Linux; neither Nix nor Racket is installed. The platform therefore cannot execute either pinned native workflow at its stated architecture, and an emulated run would not reproduce trustworthy performance measurements. No native compiler or benchmark command is claimed to have passed. The paper’s reported numbers are cited engineering evidence only; the four Kappa commands above are the separate executable record accepted for this chapter.

Control stacks and their CPS spines

Reproducibility record for exercise 35.14.

The executable companion is in artifacts/ch35-control. It represents whole stacks, persistent captured continuations, throw-time stack replacement, and finite LEM observations as object-language data. Its additional direct/CPS, declared-cost, and DNE equalities are smoke outputs, not independent evidence. Chapter 17 supplies the mathematics.

Kappa has no raw call/cc, letcc, throw, shift0, or control0 primitive. The artifact does not claim otherwise. It targets portable kappa-v1 and pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0, specification digest 84ca9ed0659956261853a9dace910ef0bd8edd8670ad3b346bdb387d9313ae1b, and conformance-ledger digest 41b1afa1a4e63f9492d637774544c81784e616d3d4a4af495ab0244de0304b94. The accepted corpus digest is 342dee3007dc79072af9127e600dd2b9621ef2c557ac37fe6eaecac4cbf5af04.

From the repository root, run

kappa check \
  artifacts/ch35-control/corpus.kp
kappa test \
  artifacts/ch35-control/corpus.kp
kappa run \
  artifacts/ch35-control/corpus.kp
kappa audit \
  artifacts/ch35-control/corpus.kp

The check is silent, the inline harness passes one corpus, and the run ends with

All 8 Chapter 35 corpus cases passed.

The audit prints []. Four discriminatory cases cover complete-spine capture, current-stack replacement, two uses of one saved continuation, and the two-stage LEM change of mind. The other four outputs are smoke checks: cpsApply duplicates the stack interpreter, the reported costs are declared constants, and the DNE case compares one encoded constructor with itself. They must not be counted as independent corroboration.

Three typechecking semantic mutations fail the frozen stdout oracle. Capturing only the top frame has digest 040382d1b54b9616b90d15b447c999c7f8fb8c89bd82203bd856bf4feb0a7f46; using the current rather than saved stack in throw has digest a62fedbb24c816141b57ebdc01fcd7dccf6fb86d4efda95f36e54162fdd15dce; omitting the injection frame from the LEM continuation has digest b699fd72f3ab247cf957954a0c315c35ba33db4dc18621985967d33fb9728b63. They respectively fail complete capture/LEM, stack replacement/persistence, and LEM alone. Restoring the accepted digest restores all eight cases and the empty audit.

The unchanged Piróg–Polesiuk–Sieczkowski Coq supplement is efftrans-coq.zip in the archived typed-handler-control-equivalence source directory, digest e0327217478dc80679f4e084af9c8c11e55c8ca05668bb5ea2bf6a97cb564f55. ZIP validation succeeds. The supplement identifies Coq 8.8.2; the retained source note records the modern Rocq 9.1.1 compatibility failure in Binding/Core.v. This is an honest toolchain boundary, not a failure of the published theorem and not a substitute for the chapter’s printed proof.

These executions are finite implementation evidence only. They do not execute raw control; prove stack typing, preservation, progress, CPS typing, simulation, or normalization; establish Curry–Howard consistency; prove the four PPS correspondences; or mechanize the dependent inconsistency.

Linear checking and file-token evaluation

Reproducibility record for exercise 36.18.

The executable companion is in artifacts/ch36-linear-affine. It represents the chapter’s types, terms, two contexts, live tokens, checker, and evaluator as object-language data; chapter 18 supplies the mathematical proofs. The companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The accepted corpus SHA-256 is b5a1380bab2bf176480f1f0983851b039779440bfe9a572d08b580fb97b80548. Its README records the specification, conformance-ledger, and compiler digests, GHC 9.14.1, arm64 macOS 26.3.1, exact commands, accepted-output summary, mutation checks, and evidence boundary. From the repository root run

kappa check \
  artifacts/ch36-linear-affine/corpus.kp
kappa test \
  artifacts/ch36-linear-affine/corpus.kp
kappa run \
  artifacts/ch36-linear-affine/corpus.kp
kappa audit \
  artifacts/ch36-linear-affine/corpus.kp

The check is silent, the inline harness passes one corpus, the trace ends with

All 9 Chapter 36 corpus cases passed.

and the audit prints []. The positive cases cover tensor swap, sum residual sharing, local bang copying, and read-close cleanup. The negative cases reject duplication, discard, unequal case residuals, a dropped returned file, and effectful promotion. Mutations that pass the original context to the second tensor premise, ignore branch-residual equality, or admit applications as promoted values each make the inline test fail. No compiler or conformance-suite change was required. These executions do not prove the chapter’s substitution, safety, ownership, or cut results, and they do not claim native backend parity.

Evaluation-translation inspector

Reproducibility record for exercise 37.8.

The executable companion is in artifacts/ch37-evaluation-translation. It represents finite named source and target syntax, implements the name, value, and need term translations, and executes the principal name and need target traces used in the chapter. The companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The accepted corpus SHA-256 is e63a09a4a37446bb2fa5e757f8a17a2fab4dcc8c8b1f01e9eee4eb75587ea0df. Its README records the specification, conformance-ledger, compiler digest, GHC 9.14.1, arm64 macOS 26.3.1, commands, mutations, and evidence boundary. From the repository root run

kappa check \
  artifacts/ch37-evaluation-translation/corpus.kp
kappa test \
  artifacts/ch37-evaluation-translation/corpus.kp
kappa run \
  artifacts/ch37-evaluation-translation/corpus.kp
kappa audit \
  artifacts/ch37-evaluation-translation/corpus.kp

The check is silent, the inline harness passes one corpus, the trace ends with

All 5 Chapter 37 corpus cases passed.

and the audit prints []. The five cases execute the Lin-Beta/Lin-Bang name image, check rejection and acceptance at the value restriction, execute need garbage collection by Aff-Weak, and distinguish the application boxing clauses. Deleting the name argument box, accepting applications as values, or ignoring free occurrence each makes the matching inline oracle fail. No compiler or conformance-suite change was required.

These runs inspect finite translations and classifiers. They do not prove substitution, typing or reduction preservation, reduction reflection, conservativity, observational equivalence, confluence, cost, or any theorem about Kappa.

Ordered Lambek proof search

Reproducibility record for exercise 38.11.

The executable companion is in artifacts/ch38-ordered-lambek. It represents formulas, ordered context words, and deterministic backward rule enumeration as object-language data; chapter 38 supplies the mathematical proofs. The companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The accepted corpus SHA-256 is 21eb1844b6ca44941611b21b9cc0acad0195f4d27dcd834015b1e43cde3380f8. Its README records the specification, conformance-ledger, and compiler digests, GHC 9.14.1, arm64 macOS 26.3.1, exact commands, accepted-output summary, mutation checks, and evidence boundary. From the repository root run

kappa check \
  artifacts/ch38-ordered-lambek/corpus.kp
kappa test \
  artifacts/ch38-ordered-lambek/corpus.kp
kappa run \
  artifacts/ch38-ordered-lambek/corpus.kp
kappa audit \
  artifacts/ch38-ordered-lambek/corpus.kp

The check is silent, the inline harness passes one corpus, the trace ends with

All 6 Chapter 38 corpus cases passed.

and the audit prints []. The cases cover product association, illegal exchange, one residuation instance, the residual chain, the distinct-category sentence, and all of its single adjacent swaps. Mutations that reverse the product-right blocks, remove backslash-left search, or collapse distinct atoms each make the same inline test fail. No compiler or conformance-suite change was required. The explicit fuel is an implementation totality witness, not the chapter’s mathematical termination proof. These executions do not prove cut elimination, residuation, search exactness, complexity, linguistic adequacy, or any theorem about Kappa.

Focused rule graphs and finite saturation

Reproducibility record for exercise 39.13.

The executable companion is in artifacts/ch39-focusing. It represents polarized formulas, persistent contexts, ordered inversion queues, and the three sequent forms. Duplicate-free list representations of persistent contexts are compared by mutual membership, so insertion order does not create a distinct finite-set search state. From a suspension-normal root, it records as object-language data every primitive focused-rule instance reached by search. The graph builder deduplicates candidates while closing under bottom-up rule premises. A second pass computes the least fixed point of conclusions whose premises are already known. The fuel parameters expose a broken finiteness invariant; exhaustion is not interpreted as underivability.

The companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The accepted corpus SHA-256 is 9bde43d0ab7cd7f73a322525103d08b4bbde8d5fadc682245c8e8b1055518da6. Its README records the specification and conformance-ledger digests, GHC 9.14.1, arm64 macOS 26.3.1, exact commands, accepted-output summary, mutation checks, and evidence boundary. From the repository root run

kappa check \
  artifacts/ch39-focusing/corpus.kp
kappa test \
  artifacts/ch39-focusing/corpus.kp
kappa run \
  artifacts/ch39-focusing/corpus.kp
kappa audit \
  artifacts/ch39-focusing/corpus.kp

The check is silent, the inline harness passes one corpus, the trace ends with

All 7 Chapter 39 corpus cases passed.

and the audit prints []. The cases expose a forced inversion prefix, both right-disjunction injections, both negative-conjunction projections, a cyclic implication graph stopped by candidate deduplication, and an underivable atom. Removing deduplication exhausts the cyclic case’s fuel; replacing either second-choice rule by the first makes the corresponding choice case fail. Each mutation makes the inline test exit unsuccessfully. No compiler or conformance-suite change was required. These executions do not prove de-focalization, cut, identity expansion, focalization, finite candidate closure, saturation exactness, complexity, or any theorem about Kappa, and they do not claim native-backend parity.

Direct proof-net switching and reverse sequentialization

Reproducibility record for exercise 40.11.

The executable companion is in artifacts/ch40-proof-nets. It gives every formula occurrence a stable natural-number identifier, stores axiom and tensor edges as fixed edges, and stores the two premise choices of every par separately. It enumerates bit vectors in lexicographic left-before-right order. Parent-recording undirected depth-first search reports a nonparent revisit as a cycle and an unvisited vertex as disconnection. A second routine removes conclusion pars, searches for a splitting conclusion tensor, computes its two correction-graph components, and recursively reconstructs a sequent derivation.

The companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The accepted corpus SHA-256 is da5f9686ce82e4c9fbc94a8d72a4e5b5ebc1e95ac0b7d8eae342639d3d48f912. Its README records the specification and conformance-ledger digests, GHC 9.14.1, arm64 macOS 26.3.1, the repository-local compiler digest, exact commands, output, input invariant, mutation checks, and evidence boundary. From the repository root run

kappa check \
  artifacts/ch40-proof-nets/corpus.kp
kappa test \
  artifacts/ch40-proof-nets/corpus.kp
kappa run \
  artifacts/ch40-proof-nets/corpus.kp
kappa audit \
  artifacts/ch40-proof-nets/corpus.kp

The check is silent, the inline harness passes one corpus, the audit prints [], and the run is

PASS PN-CORRECT-2 accepted 2 switchings; sequentialization has 4 rules
PASS PN-CYCLIC-1 rejected switching 1: cycle
PASS PN-DISCONNECTED-4 rejected switching 1: disconnected
PASS PN-FOUR-PAR-16 accepted 16 switchings; sequentialization has 13 rules
PASS PN-LAST-CYCLE-16 rejected switching 16: cycle
All 5 Chapter 40 corpus cases passed.

The final negative is a well-formed four-par structure. Every bit vector containing a left choice yields a tree. Vector 1111, enumerated sixteenth, disconnects the central tensor component and closes a cycle among the four outer components; cycle detection fires first. The README gives the stable-ID construction.

Three accepted-source mutations were run separately against the inline oracle. Miswiring one axiom endpoint in PN-CORRECT-2, replacing the fourth right premise of the final negative by its left premise, and deleting a splitting tensor without removing its fixed incident edges each made kappa test exit unsuccessfully. Restoring the frozen source restored all five cases. No compiler or conformance-suite change was required.

The implementation is exactly the direct enumerator of definition 40.18; its claim is $O(2^{k}n)$, not Guerrini’s $O(n)$ bound. It does not implement sequential unification. Explicit fuel exposes an implementation totality failure and is not interpreted as logical rejection. These executions check the represented structures, switching order, rejection reasons, and reconstructed rule counts. They do not prove soundness, sequentialization, normalization, confluence, either complexity theorem, or any theorem about Kappa, and they do not claim native-backend parity.

Interaction-net arithmetic and scheduling

Reproducibility record for exercise 41.18.

The executable companion is in artifacts/ch41-interaction-nets. It represents unary-addition states, a pair of disjoint active computations, unordered rule keys, boundary arities, and the pinned HVM2 paper-rule/dispatcher mapping as object-language data. It also represents two independent pinned-HVM2 VOID candidates, their two finite schedules, ideal frontier span, and root readback. Chapter 41 supplies the mathematical proofs.

The companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The accepted corpus SHA-256 is 0444fdae89471503fd842041a99b40380a7310f6e7d207f737863eddc7801d49. Its README records the specification and conformance-ledger digests, GHC 9.14.1, arm64 macOS 26.3.1, compiler digest, exact commands, output, mutation checks, and evidence boundary. From the repository root run

kappa check \
  artifacts/ch41-interaction-nets/corpus.kp
kappa test \
  artifacts/ch41-interaction-nets/corpus.kp
kappa run \
  artifacts/ch41-interaction-nets/corpus.kp
kappa audit \
  artifacts/ch41-interaction-nets/corpus.kp

The check is silent, the inline harness passes one corpus, the audit prints [], and the run ends with

All 8 Chapter 41 corpus cases passed.

The eight cases cover $3+2$ in four unary interactions, a one-step diamond, agreement of two normalization schedules, constructor-tree erasure and duplication by agent count, uniqueness of unordered rule keys, boundary preservation, the ten-to-eight HVM2 count mapping, and the two VOID schedules with work two, ideal span one, and numeric-zero readback.

Five mutations were run separately against the inline oracle. Removing the successor from the addition accumulator, giving a nullary tree zero erasure interactions, treating unordered symbol pairs as ordered, and mapping Operate2 to the switch dispatcher each made kappa test exit unsuccessfully. A fifth mutation changed the HVM2 microbenchmark’s expected readback root from zero to one and failed its inline oracle. Restoring the accepted source restored all eight cases. No compiler or conformance-suite change was required.

These executions are finite implementation evidence. They do not prove strong confluence, general development independence, divergence, lambda simulation, universality, optimality, HVM2 correctness or speed, or any theorem about Kappa; they do not claim native-backend parity.

Optimal-sharing graph contraction and certificate auditor

Reproducibility record for exercise 42.8.

The portable Kappa companion is in artifacts/ch42-optimal-sharing. It constructs the one-node labeled term graph of definition 42.1, contracts its stored beta redex, and checks the preserved node, label, and readback calculation of proposition 42.2. It then checks supplied finite traces of claimed rightmost-fan contractions. Each entry records distinct endpoint identifiers with opposite rightmost tags, a claimed family label, and a list of finite lambda terms. The checker validates each adjacent path pair by root capture-avoiding beta contraction or compatible congruence modulo alpha-equivalence and maintains uniqueness of family labels. Its invariant is that every accepted entry has distinct endpoints, opposite rightmost tags, a nonempty verified beta path, and a label absent from the accepted prefix. The opening graph is a finite fragment; the certificate checker cannot validate facing incidence or propagation in a general sharing graph.

The accepted corpus SHA-256 is d864169187e42efc19f372a6b24a9122338954727ae075494d8e3cd04c735f5f. The language profile is portable kappa-v1, and the tested compiler source commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The tested executable’s SHA-256 is 476688a4b6078aaef4e7a23f46383a3879df40d391bca7d6878545197a002d01. Place that executable first on PATH; from the repository root run

kappa check artifacts/ch42-optimal-sharing/corpus.kp
kappa test artifacts/ch42-optimal-sharing/corpus.kp
kappa run artifacts/ch42-optimal-sharing/corpus.kp
kappa audit artifacts/ch42-optimal-sharing/corpus.kp

The check succeeds silently, the test reports one passing corpus, and the audit prints []. The run ends with

All 6 Chapter 42 corpus cases passed.

The four stored mutations independently corrupt the retained opening-graph label and disable pair, adjacent-beta-step, and label-repeat validation. Their SHA-256 values are, respectively, c72839eee24bee9bae77162e29bf9d537c585a294285f08abeb760b407304e72, 7138aa3d5ebcf11271271aea8b51adfd78046e8e84803dda4dd312e8a2cbbb96, bee5ad6fbc523d1b892174027f1d53507d65d17eeca298b941ca7f453c8f0d90, and 6ff0aaf958727dd9af7567462171c3d107b2c3b0103c6db77b391de656ec61d8. Each remains typechecking and audit-clean but fails its isolated negative oracle. The capsule constructs and checks the displayed one-node graph. For general supplied certificates it does not synthesize a path, connect the fields to a sharing-graph step, prove Lévy optimality, or establish a runtime cost bound.

Chapter 43: finite BI bunches and resource forcing

Reproducibility record for exercise 43.16. The executable companion is artifacts/ch43-bi-resource-semantics/corpus.kp. It represents BI formulas, distinct additive and multiplicative bunches, one-hole contexts, selected rule trees, separate ACU comparison, and three finite resource models as object-language Kappa data. Kappa’s own contexts and type checker are not used as a BI derivability or forcing oracle.

The portable kappa-v1 corpus was accepted with the interpreter built from Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The compiler executable SHA-256 is

The specification and conformance-ledger SHA-256 values are respectively

and

The accepted corpus SHA-256 is

Place the pinned compiler on PATH. From the archive root run

export LANG=C.UTF-8 LC_ALL=C.UTF-8
kappa check artifacts/ch43-bi-resource-semantics/corpus.kp
kappa test  artifacts/ch43-bi-resource-semantics/corpus.kp
kappa run   artifacts/ch43-bi-resource-semantics/corpus.kp
kappa audit artifacts/ch43-bi-resource-semantics/corpus.kp

The check is silent, the harness reports one passing corpus, the run ends with

All 13 Chapter 43 corpus cases passed.

and the audit prints []. Acceptance used the interpreter only; no native-backend parity claim is made.

The thirteen named cases cover a purely additive proof, nested weakening and contraction below a comma, rejection of multiplicative weakening and contraction, a valid multiplicative split, rejected interchange, the running mixed derivation, both conjunction semantics, both implication semantics, and a finite weakening countermodel. Three separately typechecking mutations have SHA-256 values

Each mutant passes kappa check, fails the unchanged stdout oracle, and exits unsuccessfully under kappa run. The exact full hashes and transcripts are retained in README.md, MUTATIONS.md, and TRANSCRIPT.txt inside the companion directory. These three mutations flip deliberately exposed Boolean decision points in the model; they are reproducible semantic negative controls, not a claim that an unconstrained mutation tool discovered the faults.

The internal fuel value 240 is validated only for the fixed named corpus. Exhausting it is not evidence of noncongruence or nonforcing, and the program is not a total decision procedure for arbitrary external formulas, bunches, or models. These executions do not prove identity expansion, cut elimination, soundness, completeness, or decidability of full BI. In particular, the finite artifact does not encode Moore closure, the universal BI algebra, algebraic soundness, reflection, or the semantic cut route of section 43.5.

Finite heaps and footprint checks

Reproducibility record for exercise 44.12.

The executable companion is in the directory artifacts/ch44-separation-logic. It represents the finite heap commands and assertion checks as object-language data; chapter 44 supplies their proofs. The companion targets portable kappa-v1. It pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The accepted corpus SHA-256 is c1644c10e83c59441341ba90d55150b8e79391a6c486f688d08b6a358a0887c8. Its README records the specification, conformance-ledger, and compiler digests, GHC 9.14.1, arm64 macOS 26.3.1, the exact commands, and the evidence boundary. From the repository root run

kappa check \
  artifacts/ch44-separation-logic/corpus.kp
kappa test \
  artifacts/ch44-separation-logic/corpus.kp
kappa run \
  artifacts/ch44-separation-logic/corpus.kp
kappa audit \
  artifacts/ch44-separation-logic/corpus.kp

The check is silent, the inline harness passes one corpus, the trace ends with

All 5 Chapter 44 corpus cases passed.

and the audit prints []. The cases cover framed update, allocation followed by deallocation, exact-chain push/pop, a use-after-free fault, and alias rejection. Mutations that turn a missing load into null, reuse an allocated location, or remove the aliasing footprint checks each make the same inline test fail. Their respective SHA-256 values are 8b7eb3283aebeec42abc758daeb8a4544aea76712d0a730e311be4f2809413b4, 957a7a86f0b93529d914fe1661425567a911bc9a58e5999db274326fa9a4ec05, and 909c00eae739e7a06c2098b714219966203f064ceae2775067ea7b0ef63e2a72. Every mutant passes check and audit, and fails the unchanged inline oracle; MUTATIONS.md, TRANSCRIPT.txt, and accepted-output.txt retain the exact patches and outcomes. No compiler or conformance-suite change was required. These executions are not proofs of locality, the frame theorem, Hoare soundness, leak freedom, race freedom, or any theorem about Kappa.

The independent SLF comparison evidence is read-only source replay at the pinned DeepSpec revision recorded in appendix D: the exercise checks the declared small-footprint signatures and the MList unfolding against the book statements. No local Rocq execution is claimed, and that comparison does not extend the Kappa artifact’s acceptance boundary.

Physical CAS and abstract-commit traces

Reproducibility record for exercise 45.11.

The executable companion is in artifacts/ch45-iris-increment. The Kappa program records each thread as ready, loaded, or returned; a world also carries the physical counter and an abstract commit count. Load changes only a control state. Successful CAS increments both counters and returns the old value. Failed CAS changes neither counter and restores the ready state.

The portable compiler profile is pinned to Kappa commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. The accepted source SHA-256 is ; the tested compiler binary SHA-256 is . From the repository root, the four commands are kappa check, kappa test, kappa run, and kappa audit on artifacts/ch45-iris-increment/corpus.kp. Check is silent, test reports one passing file, run ends

All 8 Chapter 45 corpus cases passed.

and audit prints [].

The replayed mutation makes a failed right-thread CAS increment the physical and abstract counters. The mutant has SHA-256 4dd8e54b517463a9 73c980896725d7ea c93311eff4610a68 a0c6cd1a2f2c2c1e; it passes check and audit but fails the unchanged test oracle. The artifact README and transcript record exact commands and outcomes. These runs check finite branch calculations. They do not implement Iris or prove invariant soundness, logical atomicity, adequacy, progress under fairness, or any linearizability theorem.

Finite ownership-protocol traces

Reproducibility record for exercise 46.13.

The executable companion is in artifacts/ch46-ownership-borrowing. It represents the chapter’s finite mode machine as Kappa data and checks seven traces: nested shared borrowing, exclusive reborrowing, owner reuse after scope exit, rejection of use after move, rejection of sharing during exclusive access, and rejection of ending an outer exclusive lifetime first, plus rejection of ending a foreign shared lifetime. It targets portable kappa-v1. The accepted source SHA-256 is 9023a6a229744e84b4cdffca7007b92efd578efc4ba3f291e2ee42b1ac2823e0. The pinned compiler source commit is 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested packaged binary has SHA-256 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6 on arm64 macOS 26.3.1. From the repository root run

kappa check artifacts/ch46-ownership-borrowing/corpus.kp
kappa test  artifacts/ch46-ownership-borrowing/corpus.kp
kappa run   artifacts/ch46-ownership-borrowing/corpus.kp
kappa audit artifacts/ch46-ownership-borrowing/corpus.kp

The check is silent, the harness passes its one corpus, the run ends with

All 7 Chapter 46 corpus cases passed.

and audit prints []. Permitting sharing from an exclusive state, omitting the top-lifetime test, or permitting reads from the unavailable state is a typechecking finite-model mutation that falsifies a permanent case. The program does not model payload updates, histories, association, or a scheduler. It does not prove protocol preservation, Affe soundness, Pure Borrow leak freedom, any open conjecture, or any theorem about Kappa.

Archived Pure Borrow implementation evidence.

The final evaluated record is Zenodo 19622061. Its source agrees, apart from repository-only development and CI files, with the annotated pldi26-artifact tag at commit c12a933cca63f2db8083254b33994c5a006ca580. The first record, Zenodo 18902181, retains both the original artifact pinned through commit e5b027fb84663d2fc2b92956bbc32a09dfeda272 and the repaired source/image pair. Zenodo 19511795 and the final record contain the repair. The upstream snapshot 24fabd7b5d3921a478733d17dcd3edae3119559b postdates evaluation and is not used as artifact evidence.

All retained Zenodo files matched their record MD5 values, every archive passed a full table-of-contents read, and each Git snapshot was clean and passed git fsck --connectivity-only. The OCI images were validated as archives but were not loaded or executed in this acceptance pass. The several-hour benchmark was not rerun. Consequently the archive supports implementability and preserves the reported version-one bug/fixed history; this book imports published measurements only as cited engineering evidence and makes no local performance or scheduler-correctness claim.

Chapter 47: finite update eligibility

Reproducibility record for exercise 47.9. artifacts/ch47-uniqueness-eligibility/ contains the portable Kappa attribute and update-eligibility checker. Its accepted source SHA-256 is

The tested packaged Kappa v0.3.0 executable has SHA-256

Run kappa check, kappa test, kappa run, and kappa audit on artifacts/ch47-uniqueness-eligibility/corpus.kp. The run prints six named PASS lines and ends with

audit returns []. The replayed mutation reverses the arguments of leqAttr in the constructor constraint. It remains typechecking and audit-clean but fails the forbidden-inequality oracle. This finite checker does not implement graph denotation, graph rewriting, inference, preservation, or quicksort.

Chapter 48: finite place and loan checking

Reproducibility record for exercise 48.9. artifacts/ch48-place-loan-checker/ contains the portable Kappa projection-path, partial-move, loan, collection, and rank checker. Its accepted source SHA-256 is

The tested packaged Kappa v0.3.0 executable has SHA-256

Run kappa check, kappa test, kappa run, and kappa audit on artifacts/ch48-place-loan-checker/corpus.kp. The run prints seven named PASS lines and ends with

audit returns []. The replayed mutation replaces prefix overlap by exact path equality. It remains typechecking and audit-clean but fails the root–descendant oracle. This finite checker implements neither Featherweight Rust nor Oxide and proves none of their progress, preservation, safety, or termination results.

Chapter 49: finite access-overlap checking

Reproducibility record for exercise 49.7. artifacts/ch49-swiftlet-access/ contains the portable Kappa path auditor. A single verdict-producing traversal determines both acceptance and the printed reason. Accepted source SHA-256: . The tested packaged Kappa v0.3.0 executable has SHA-256 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. Run kappa check, kappa test, kappa run, and kappa audit on artifacts/ch49-swiftlet-access/corpus.kp. The exact run is

PASS distinct fields
PASS distinct constant indices
PASS equal paths rejected [end/end]
PASS root and descendant rejected [end/field]
PASS nested unknown indices rejected [unknown/unknown]
PASS different roots with unknown indices rejected [unstable/path]
All 6 Chapter 49 corpus cases passed.

Audit returns []. The replayed mutation changes the unknown-index stability branch from false to true. Its SHA-256 is f5e504a7bf3af952 55371aba578d692d 13633b69bac38f0e 25e6186561980566. It remains typechecking and audit-clean but fails the different-root unknown-index oracle. The artifact decides only the book’s finite conflict relation; it does not prove Swiftlet progress, preservation, independence, or compiler correctness.

Chapter 50: region-authority traces

Reproducibility record for exercise 50.7. artifacts/ch50-region-capability/ contains the portable Kappa trace auditor. Accepted source SHA-256: 826db44ac6261017 b92818db21273781 666f8b8bf7aa79fa 0f151fd0579fd0c1. The tested packaged Kappa v0.3.0 executable has SHA-256 5b9b64cac3cd2b43 f381d085b46d2489 24bcc3a5e65cb5a9 87d44e7d5833c6b6. Run kappa check, kappa test, kappa run, and kappa audit on artifacts/ch50-region-capability/corpus.kp. The exact run is

PASS allocate access free
PASS access after free rejected
PASS free shared rejected
PASS double free rejected
PASS live halt rejected
All 5 Chapter 50 corpus cases passed.

Audit returns []. The replayed mutation lets shared authority take the free transition. It has SHA-256 ad3c64e2ef0cc648 2ad7a4fbd6bc581a a6f5ff6d68c5b593 cbd24062d9dc8f7b. It remains typechecking and audit-clean but fails the shared-free negative oracle. This finite state machine does not implement inference or prove memory safety, complete collection, or translation correctness.

Chapter 51: finite subcapturing

Reproducibility record for exercise 51.7. artifacts/ch51-capture-set/ contains the portable Kappa work-list checker. Accepted source SHA-256: c6b22552820f82f7866c8e8ff2b1425f0762ab0f8fe8211d92d0c89f0c999c6f. Run kappa check, kappa test, kappa run, and kappa audit on artifacts/ch51-capture-set/corpus.kp. The run is

PASS universal target
PASS direct capture
PASS indirect capture
PASS pure binding elimination
PASS reversed edge rejected
PASS declared universal escape rejected
All 6 capture-set corpus cases passed.

Audit returns []. The symmetric-edge mutation has SHA-256 4b0d73081cba7312e607c2f0f490ff57d3b3097fbf033ce70208c833a461101d and fails the reversed-edge oracle while check and audit remain clean. The directory’s MUTATIONS.md, accepted-output.txt, and TRANSCRIPT.txt make both accepted and mutated gates reproducible.

Chapter 52: file-protocol traces

Reproducibility record for exercise 52.7. artifacts/ch52-typestate-protocol/ contains the portable Kappa state machine. Accepted source SHA-256: ad855e98c6bce94dba3e22c5da4981f0a07a823dfe73e688321a8acc9ebd7055. Run the four commands above on artifacts/ch52-typestate-protocol/corpus.kp. The run is

PASS complete file trace
PASS read after eof rejected
PASS double close rejected
PASS read after close rejected
PASS unequal branch join rejected
All 5 typestate corpus cases passed.

Audit returns []. The mutation that leaves read-eof in open state has SHA-256 892e8cfe4712eb8de4441d961abdebb6875d92e45902554eb7318578b5ed7396 and fails only the read-after-eof oracle. The directory records the exact edit, accepted output, and gate transcript.

Chapter 53: flat and structural demands

Reproducibility record for exercise 53.7. artifacts/ch53-coeffect-context/ contains the portable Kappa demand analyzer. Accepted source SHA-256: a7441090c1d6b06f4632eff997334af99ac4a0a41ea2e0642042fc2654f3698b. Run the four commands above on artifacts/ch53-coeffect-context/corpus.kp. The run is

PASS constant has no implicit demand
PASS width access demanded
PASS implicit demands unioned
PASS structural counts x=3 y=1
PASS substitution grade 2*2=4
All 5 coeffect corpus cases passed.

Audit returns []. The max-instead-of-addition mutation has SHA-256 977bac9b17b87543f2657b6970584fe523097a14c2827f8bac02884e835b9c15 and fails only the repeated-use oracle. The directory records the exact edit, accepted output, and gate transcript.

All three artifacts use the packaged Kappa v0.3.0 executable with SHA-256 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. They are executable finite analyses, not mechanized metatheory.

Evidence snapshot.

The repository identifier is dtt-book. This checkout has no configured remote; the evidence below was replayed in the worktree based on commit 495120a69931ac6ac3d4db5b4ce14a6818979e0a. Each source hash below pins the uncommitted artifact content independently of that base commit. The Kappa toolchain is packaged Kappa v0.3.0, portable kappa-v1; its compiler binary has SHA-256 5b9b64ca c3cd2b43 f381d085 b46d2489 24bcc3a5 e65cb5a9 87d44e7d 5833c6b6.

Chapter 20: finite grade correspondence

Reproducibility record for exercise 54.12. artifacts/ch54-grade-correspondence/ contains a portable Kappa calculator for context scaling and addition, with a distinct boxed Linear Base shadow. Accepted source SHA-256: bede0991 0aa7d657 ccbf072a e9cb5c78 ce9c8154 4f795cdd 6e7d9777 f4fd6f69. The exact commands are

kappa check artifacts/ch54-grade-correspondence/corpus.kp
kappa test artifacts/ch54-grade-correspondence/corpus.kp
kappa run artifacts/ch54-grade-correspondence/corpus.kp
kappa audit artifacts/ch54-grade-correspondence/corpus.kp

The run is

PASS nested application grades
PASS direct translation preserves grades
PASS Boolean grade interpretation
PASS failed direct converse witness
All 4 Chapter 54 corpus cases passed.

Audit returns []. The multiplication-to-addition mutation fails the nested-grade oracle; omitting the translated argument box independently fails the translation oracle.

The optional fractional-ownership route was separately replayed with the authors’ preserved amd64 granule-repl Docker image. Its exact pins are listed in continuation rows:

The exact replay was

granule_root=references/04-modern-designs
granule_artifact=$granule_root/functional-ownership-\
fractional-uniqueness/zenodo-artifact
granule_image=ghcr.io/raehik/granule-repl:\
c35c265da06a442d3d3bbb419f43dfc8ff08a6af
docker load -i "$granule_artifact/artefact.tar.gz"
docker run --rm --platform linux/amd64 -i \
  -v "$PWD/$granule_artifact:/host:ro" \
  "$granule_image" <<'GRANULE'
:l /host/examples.gr
:t exampleBorrow
:q
GRANULE
docker run --rm --platform linux/amd64 -i \
  -v "$PWD/$granule_artifact:/host:ro" \
  "$granule_image" <<'GRANULE'
:l /host/parsum.gr
:t sumFromTo
:t parSum
main
:q
GRANULE

Granule 0.9.5.0 accepted exampleBorrow, inferred *Colour -> *Colour, accepted the fractional sumFromTo/unique parSum program, and evaluated main to 100.0. The files examples.gr and parsum.gr have SHA-256 respectively c1eb4bc1 ba548fde ac7b02d9 c4f5ec39 5d6b3a5e 35d1620f 3123ce85 c9f5ca7a and 3df3d38e 71f8a1bc ea010300 03aab291 73e5de22 fc008879 976f38a6 1c3b380d. This run is language-implementation evidence, not proof of the imported safety package.

Chapter 55: finite reactive trace

Reproducibility record for exercise 55.10. artifacts/ch55-simply-ratt-stream/ contains a running-sum trace and finite root-count oracle. Accepted source SHA-256: 8f212bac 3f345c7d 922f7a42 7c24df40 63f47bd9 8c1f4f22 0469cb32 310481dc. The exact commands are

kappa check artifacts/ch55-simply-ratt-stream/corpus.kp
kappa test artifacts/ch55-simply-ratt-stream/corpus.kp
kappa run artifacts/ch55-simply-ratt-stream/corpus.kp
kappa audit artifacts/ch55-simply-ratt-stream/corpus.kp

The run is

PASS running sum trace
PASS current output uses current input
PASS bounded machine roots
PASS history mutation detected
All 4 Chapter 55 corpus cases passed.

Audit returns []. The history-retaining mutation fails the root-bound oracle.

Chapter 56: finite SLL weight

Reproducibility record for exercise 56.11. artifacts/ch56-sll-weight/ implements the three displayed weight equations on a finite net syntax. Accepted source SHA-256: 1bd34833 b0e0bcbd f2af8577 af0ccd73 946c52da 3afb0737 77ce43a2 4b807e69. The exact commands are

kappa check artifacts/ch56-sll-weight/corpus.kp
kappa test artifacts/ch56-sll-weight/corpus.kp
kappa run artifacts/ch56-sll-weight/corpus.kp
kappa audit artifacts/ch56-sll-weight/corpus.kp

The run is

PASS nested-box weight
PASS external reduction decreases
PASS degree records box depth
PASS omitted-rank mutation detected
All 4 Chapter 56 corpus cases passed.

Audit returns []. Omitting rank multiplication at boxes makes the rank-three exponential reduction fail to decrease.

They are finite executable witnesses, not mechanized proofs of the chapter theorems.

Chapter 57: heap-cell traces

Reproducibility record for exercise 57.7. artifacts/ch57-aara-heap-traces/ checks the exact $0\dots 7$ traces and the paper’s two binomial-basis heap bounds. The breadth trace is the chapter’s explicit accounting schedule, not the unavailable 2010 source program. Accepted source SHA-256: ac7ab4b2e9edd95f4c839c48513e6edc7435d03467219e9f06de04bf14570cc9. The run is

TRACE pairs 0,0,3,9,18,30,45,63
TRACE startBreadth 0,16,42,80,130,192,266,352
PASS program traces and bounds for n=0..7
All 3 Chapter 57 corpus cases passed.

Audit returns []. Dropping the linear contribution from the breadth bound gives mutant SHA-256 c1014fa1750fb6ba3c3d1af58ee641ca55f0d898b6ad63dca1471f89cb56036a and fails the unchanged bound oracle at $n=1$.

Chapter 21: finite binary traces

Reproducibility record for exercise 58.8. artifacts/ch58-session-protocols/ checks six finite provider/client traces. Accepted source SHA-256: 01c6a82ccf1f1612ec3ccc0ed256dc391dcc4e06118cd5a08ee9bb4e9d509f82. The run is

PASS empty-trace termination
PASS tensor channel transfer
PASS internal left choice
PASS external right choice
PASS pre-unrolled request-answer trace
PASS mismatched endpoints rejected
All 6 Chapter 58 corpus cases passed.

Audit returns []. Reversing left selection to a right offer gives mutant SHA-256 2e803f480bd111a6ac9323a79bc348e156d3ab78433b3619d1bccf05a11880a3 and fails the unchanged left-choice oracle.

Chapter 59: MPST and choreography checks

Reproducibility record for exercise 59.7. artifacts/ch59-mpst-choreography/ executes finite global and choreography AST projection, the sender-tagged sale queue trace, a distinct-address linearity check, endpoint regeneration, and partial merge. Accepted source SHA-256: 32977201198d77b2785c7235cd917a52af445a99122d8f3976c721915b0a146f. The run is

PASS plain-merge sale projects to all three endpoints
PASS accepting sale trace replays FIFO queue transitions
PASS distinct-address sale satisfies linearity premise vacuously
PASS uninformed MPST branch rejected by plain projection
PASS changed choreography regenerates all endpoints
PASS hand-written endpoint mutation rejected
PASS missing Pirouette branch knowledge rejected
All 7 Chapter 59 corpus cases passed.

Audit returns []. Deleting equality of branch-specific send expressions from control merge gives mutant SHA-256 249ef69cdc08be9b6baa4b09b7c2f14bf846d1ab6f0955e7ed37a31d3d4bdadb and fails the unchanged endpoint-mutation and missing-branch-knowledge oracles.

All three companions use portable kappa-v1 and packaged Kappa SHA-256 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. Their README.md, TRANSCRIPT.txt, and MUTATIONS.md files record exact commands and evidence boundaries. They are finite checkers, not mechanizations of the chapters’ soundness, progress, subject-reduction, or projection theorems.

Shared Kappa provenance for Chapters 60–63. All four corpora were checked with the installed Kappa v0.3.0 distribution, embedded build kpp-hskll-0.3.0-1df6e4b1, on arm64 macOS 26.3.1. The distribution exposes no compiler source commit or implementation toolchain, so neither is claimed. Its compiler binary, bundled specification, and compliance-ledger SHA-256 values are, in order,

Each adjacent pair of lines concatenates to one hash. The separate wabbit-corp/kappa commit 216f913ee9d94519cccb3d9e16f6f9d3652188fe is a specification-only snapshot. Its standalone Spec.md has SHA-256

The two lines concatenate; it is not compiler provenance.

Chapter 22: finite cube-triple checking

Reproducibility record for exercise 60.9. artifacts/ch60-pts-cube-checker/ contains the portable Kappa corpus for the finite lambda-cube checker, its one-redex conversion stage, generated binder traces, and first-missing-triple reporting. Accepted source SHA-256:

The two lines concatenate. The tested distribution and its hashes are recorded in the shared provenance block above. From the repository root run

cd artifacts/ch60-pts-cube-checker
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

Check is silent, test passes one case, and audit is []. The exact run is

PASS polymorphic identity in lambda2: [(*,*,*); (Box,*,*)]
PASS lambda-arrow rejection: missing (Box,*,*)
PASS higher-order polymorphic product in lambda-2-omega:
  [(Box,Box,Box); (*,*,*); (Box,*,*); (Box,*,*)]
PASS term-indexed family rejection: missing (*,Box,Box)
PASS one-redex type conversion
All 5 Chapter 60 corpus cases passed.

Changing the polymorphic membership branch to return True unconditionally produces mutant SHA-256

The two lines concatenate. It leaves the corpus type-correct and audit-clean but changes the second line to FAIL. This finite run does not prove any PTS structural or normalization theorem.

Chapter 23: canonical-head inversion

Reproducibility record for exercise 61.8. artifacts/ch61-lf-adequacy-checker/ contains the portable Kappa corpus for the bounded intrinsic STLC signature’s canonical checker and decoder. Accepted source SHA-256:

The two lines concatenate. The tested distribution and its hashes are recorded in the shared provenance block above. Run

cd artifacts/ch61-lf-adequacy-checker
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The exact run is

PASS decoded represented identity:
  (lam Atom. #0) : (Atom -> Atom)
PASS decoded represented application:
  ((lam Atom. #0) #0) : Atom
PASS rejected underapplied lam head
PASS rejected exotic inspect result head
All 4 Chapter 61 corpus cases passed.

Check is silent and audit is []. A decoder branch that returns the argument of InspectHead changes the fourth line to FAIL. This run illustrates one finite head inversion and proves no LF normalization or adequacy theorem.

Chapter 62: finite nominal substitution

Reproducibility record for exercise 62.6. artifacts/ch62-nominal-substitution-checker/ contains the portable Kappa corpus for finite permutations, support, and capture-avoiding substitution over four atoms. Accepted source SHA-256:

The two lines concatenate. The tested distribution and its hashes are recorded in the shared provenance block above. Run

cd artifacts/ch62-nominal-substitution-checker
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The exact run is

PASS abstraction support removes its binder
PASS finite permutation transports support
PASS substitution renames a capturing binder
PASS substitution leaves a shadowed occurrence bound
All 4 Chapter 62 corpus cases passed.

Check is silent and audit is []. Forcing substitution to descend through a binder whose atom equals the target leaves the corpus type-correct but changes the fourth line to FAIL. Replacing alpha-equivalence by binder-sensitive equality remains type-correct and changes the first two lines to FAIL. The four-atom run returns an explicit exhaustion result if no fresh atom remains. Alpha-equivalence is decided by paired binder stacks; the support probes check all transposition generators fixing each claimed singleton and a moving witness. The run proves no nominal-set or substitution theorem.

Optional route.

none.

Chapter 63: Beluga scope preflight $\star$

Reproducibility record for exercise 63.5. artifacts/ch63-beluga-context-scope/ contains the portable Kappa model of the paired schema-block projections. Accepted source SHA-256:

The two lines concatenate. It was checked with the same installed Kappa distribution and compiler executable as the preceding records. Run

cd artifacts/ch63-beluga-context-scope
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The exact run is

PASS schema block pairs its term with matching typing evidence
PASS same-context recursive call is in scope
PASS lambda recursive call supplies both matching projections
PASS altered call rejected: expected [g,b |- hastype b.x _]
All 4 Chapter 63 corpus cases passed.

Check is silent and audit is []. A type-correct mutation that accepts typing evidence for the wrong projected term changes the fourth line to FAIL. The pinned checkout is under references/06-programming/ in beluga-contextual-metaprogramming/source/; the input relative to it is examples/literate_beluga/0Beginner/Type_Uniqueness.bel. Its commit is

Its SHA-256, again concatenating the two lines, is

The schema and lambda-case source spans are inspected to justify the finite Kappa representation. No Beluga executable or locked opam environment is installed in this workspace, so the acceptance test makes no implementation-success or implementation-error claim.

Evidence snapshot.

The following portable kappa-v1 companions were replayed from base commit

495120a69931ac6ac3d4db5b4ce14a6818979e0a.

The packaged Kappa binary has SHA-256 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6.

Chapter 64: nominal restriction

Reproducibility record for exercise 64.6. The source at artifacts/ch64-nominal-restriction-checker/corpus.kp has SHA-256 0549242d30a19219c25951f13e79af24751bc43207d6ad99003c6c6d3cc728ec. Its run checks restriction, later-variable rejection, alpha-renaming, and the bound/free-name distinction, ending with All 6 Chapter 64 corpus cases passed.

Chapter 24: HOL kernel trace

Reproducibility record for exercise 65.7. The source at artifacts/ch65-hol-kernel-trace-checker/corpus.kp has SHA-256 040362d58fb92b3a97006fa77d3883b6a3a884591f9a2a0818c500c3c25ba9d1. Its run checks reflexivity, derived symmetry, and both outcomes of the ABS freshness test, ending with All 4 Chapter 65 corpus cases passed.

Chapter 66: extracted witness

Reproducibility record for exercise 66.7. The source at artifacts/ch66-system-t-witness-evaluator/corpus.kp has SHA-256 6e310c5cd4d8f4f7e1e2618c9cff0f8beaa240d8e7a9f4c6627d80820aee3df4. Its run checks both recursor equations, calculates the triangular witness at three, and detects the predecessor-index mutation, ending with All 4 Chapter 66 corpus cases passed.

For each source the exact commands are kappa check, kappa test, kappa run, and kappa audit; every command succeeds and every audit prints []. These are finite executable models, not mechanizations of DNTT decidability, HOL soundness, or Dialectica soundness.

Chapter 67: finite selection and controlled replay

Reproducibility record for exercise 67.9. The source at artifacts/ch67-bar-choice-replay/corpus.kp has SHA-256 12c97b8e47f9701d46ea017ce2b1cccbaddfc87091e37f8311dbd5bbefff67e2. It was replayed from base commit 495120a69931ac6ac3d4db5b4ce14a6818979e0a with packaged Kappa SHA-256 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. The exact commands are

kappa check artifacts/ch67-bar-choice-replay/corpus.kp
kappa test artifacts/ch67-bar-choice-replay/corpus.kp
kappa run artifacts/ch67-bar-choice-replay/corpus.kp
kappa audit artifacts/ch67-bar-choice-replay/corpus.kp

Check is silent, the inline test passes, audit prints [], and the run is

PASS binary product: maximize then minimize gives (1, 0)
PASS three-stage product: [1, 0, 1] with score 5
PASS strict controlled product unfolds equality: [1, 0, 1, 0]
PASS non-strict stopping mutant changes the bounded branch: [0, 0, 0, 0]
All 4 Chapter 67 corpus cases passed.

Changing only the strict branch from control < depth to control < depth || control == depth gives mutant SHA-256 f43c5511f7f1bfbb7c6af902eec2fc129d34760828db621335c0c7c34fbd04b3. The unchanged strict-output oracle fails. The finite fuel is explicit; this run is not an implementation or totality proof for infinite SBR or EPS.

The supplemental Agda source is pinned at references/06-programming/escardo-classical-choice-agda/source/. Examples.agda has SHA-256 6acf3c10ec98f04e3c859a9701de832da68f89f4f0aac99983128772b343eeff, and PigeonProgram.agda has SHA-256 096c06d32716deb618e4eef4d1bfbb9d33db9c0aa45f7e84df92afe2a60fb47b. No compatible Agda executable is installed, so this edition records source inspection and a hole scan, not a fresh typecheck or normalization transcript.

Chapter 25: finite analyzer calculations

Reproducibility record for exercise 68.14. The source at artifacts/ch68-verified-analyzer/corpus.kp has SHA-256 e08a991394d22624ac447d5d9362cf4b5747a4428a18f92d9ab23d9f2a2c1d58. The exact commands are

kappa check artifacts/ch68-verified-analyzer/corpus.kp
kappa test artifacts/ch68-verified-analyzer/corpus.kp
kappa run artifacts/ch68-verified-analyzer/corpus.kp
kappa audit artifacts/ch68-verified-analyzer/corpus.kp

Check is silent, the inline test passes, audit prints [], and the run is

PASS concrete countdown trace
PASS interval contains every reachable value
PASS widening and checked narrowing
PASS relational invariant x <= y
PASS unsound subtraction mutant rejected
All 5 Chapter 68 corpus cases passed.

The source, commands, and evidence boundary are repeated in artifacts/ch68-verified-analyzer/README.md; the captured run is in artifacts/ch68-verified-analyzer/TRANSCRIPT.txt. The embedded mutant is a false concrete nonnegativity predicate, not an interval transformer. The corpus is a finite calculation replay and does not mechanize the chapter’s analyzer, DBM closure, fixed-point theorems, or imported developments.

Chapter 69: SymImp-DL certificates and replay

Reproducibility record for exercise 69.5. artifacts/ch69-symimp-dl/ implements the finite command/path AST, a fuel-bounded symbolic work-list explorer, concrete replay, path-model check, certificate-edge incidence and strict negative-cycle checks, retained unknown, and concolic branch reversal. Accepted Kappa SHA-256: 491c9bb6a503630cac053c5910cb2d45c6bb2ffac84fa5baff9110bc00cbec74. The exact commands are

kappa check artifacts/ch69-symimp-dl/corpus.kp
kappa test artifacts/ch69-symimp-dl/corpus.kp
kappa run artifacts/ch69-symimp-dl/corpus.kp
kappa audit artifacts/ch69-symimp-dl/corpus.kp

The run ends with nine named PASS lines and All 9 SymImp-DL corpus cases passed.; audit returns []. Changing strict negative weight to nonpositive weight makes the zero-cycle oracle fail.

Representation.agda, SHA-256 aee7182e34797bedb6872f16d66049ce218e8d8ce047ba953110b2d3bcf0b3ed, states the symbolic/concrete store relation and proves expression correspondence for copy-plus-constant terms, assuming associativity of the abstract integer addition. No Agda executable is installed in the acceptance environment, so this edition records the source and hole scan but does not claim a fresh typecheck. The Agda file does not mechanize path coverage or certificate soundness.

Chapter 70: two-run checker and DCC fixture

Reproducibility record for exercise 70.5. artifacts/ch70-tini-checker/ implements the two-point lattice, explicit pc checker, finite evaluator, and two-run oracles. Accepted source SHA-256: 27dd124befef300026213fa43fce1aedca4d0cbbeb23c6076f7cfbb3e02f0555. Its four Kappa commands have the same forms as above with artifacts/ch70-tini-checker/corpus.kp; the run ends with six named PASS lines and All 6 imperative TINI corpus cases passed.; audit returns []. The pc-erased mutation accepts the leak and fails the independent two-run oracle.

The DCC comparison pins commit fe5eab69ce024ca1c1c6868a3d52513f9ce4ed8f under references/05-metatheory/simple-noninterference-parametricity/agda-artifact/. The accepted hashes are

Definitions.agda

a9571dfe7ea5e82d835805b34ed24d54

937571c67f5a4aabc8035d4e5c9b0100.

Translation.agda

eae5780581b34ae5d2d6815f2fde6491

069fc787cf256318adb8d7a6878c1452.

Formalisation.agda

f2fbe6c10e1d78e5748ec6d31a880b3f

43b5110253254d5d85533fd051f6da2b.

The three files contain no Agda holes. The two question marks reported by a text search are occurrences of the declared decision operation _$⊑$?_, not metas. The fixture also contains named postulates for lattice structure, extensionality, strong normalization, the observer construction, and shallow noninterference. Because Agda is not installed locally, the intended command

agda Definitions.agda Translation.agda Formalisation.agda

was not rerun and is not presented as passing evidence.

Both Kappa companions are finite executable witnesses, not mechanizations of the chapters’ general simulation or noninterference theorems.

Chapter 26: capture and free-variable audit

Reproducibility record for exercise 71.20. artifacts/ch71-dtt-substitution-auditor/ contains the portable Kappa corpus for named substitution. Accepted source SHA-256: 4cba1e53f9cc7351 f75634f2671f53a4 3ef1a4e29681a98d 0b6eab3b6cdc00ac. The tested packaged binary, specification, and conformance-ledger hashes are recorded in the artifact README; no compiler source commit is claimed. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 71 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Invert the capture guard; the formerly rejected binder is accepted. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 27: finite premise checking

Reproducibility record for exercise 72.23. artifacts/ch72-pisigma-rule-checker/ contains the portable Kappa corpus for dependent product and sum rules. Accepted source SHA-256: fcaafcaebb8ed046 99254ca9da625ad5 666a3cc910fa86a9 b55e57a194728376. 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 72 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Accept every second projection without comparing its family index. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 28: polarity traversal

Reproducibility record for exercise 73.30. artifacts/ch73-inductive-positivity-checker/ contains the portable Kappa corpus for strict positivity. Accepted source SHA-256: 025cf0c6cf858de6 54bbc1c84f6546cf a067ccc20de88ec6 ba088db9e96c4c7d. 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 73 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Preserve rather than reverse the sign in an arrow domain. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 29: finite max/successor constraints

Reproducibility record for exercise 74.15. artifacts/ch74-universe-level-solver/ contains the portable Kappa corpus for concrete universe constraints. Accepted source SHA-256: . 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 5 Chapter 74 corpus cases passed.; audit returns []. The replayed typechecking mutation removes successor from level evaluation. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 75: code decoding and scope

Reproducibility record for exercise 75.6. artifacts/ch75-tarski-universe-decoder/ contains the portable Kappa corpus for a finite de Bruijn code language. Accepted source SHA-256: f66fc6d139f48851 db62c6eca364ee65 6843a362044908ac 13218a08a2857749. Run the same four commands on corpus.kp. The run ends All 5 Chapter 75 corpus cases passed.; audit returns []. Checking a product body at the unextended depth is the replayed mutation. This corpus does not prove the chapter’s comparison theorem.

Chapter 76: assumption-use ledger

Reproducibility record for exercise 76.5. artifacts/ch76-hurkens-assumption-ledger/ contains the portable Kappa dependency certificate. Accepted source SHA-256: . Run the same four commands on corpus.kp. The run ends All 8 Chapter 76 corpus cases passed.; audit returns []. Ignoring the required large-beta flag is the replayed mutation. The corpus checks the finite assumption ledger; it is not a parser or proof checker for the diagonal terms.

Chapter 30: J-premise checking

Reproducibility record for exercise 77.17. artifacts/ch77-identity-eliminator-checker/ contains the portable Kappa corpus for identity elimination. The two lines below concatenate to its accepted source SHA-256:

The tested packaged binary, specification, and conformance-ledger hashes are recorded in the artifact README; no compiler source commit is claimed. The four repository-root commands are kappa check, kappa test, kappa run, and kappa audit on corpus.kp. The run ends All 4 Chapter 77 corpus cases passed.; audit returns []. The replayed mutation skips reflexive-branch substitution. It still checks, but kappa test exits nonzero. This is boundary evidence, not a metatheorem proof.

Shared Kappa provenance for Chapters 78–80. All three corpora were checked on arm64 macOS 26.3.1 with installed Kappa v0.3.0, whose executable contains build identifier kpp-hskll-0.3.0-1df6e4b1. The distribution does not expose its compiler source commit or implementation toolchain, so neither is claimed. The executable was kappa resolved by PATH. Its SHA-256, followed by the hashes of its bundled Spec.md and SPEC_COMPLIANCE.md, is recorded below; each adjacent pair concatenates to one hash:

For distinction, the separate specification-only repository wabbit-corp/kappa was inspected at commit

Its standalone Spec.md SHA-256 is the concatenation

that snapshot is not compiler provenance. Each record below gives its artifact directory and invokes, in order, the exact commands kappa check corpus.kp, kappa test corpus.kp, kappa run corpus.kp, and kappa audit corpus.kp; every occurrence of kappa resolved to the packaged executable described above.

Chapter 31: format-indexed parsing

Reproducibility record for exercise 78.8. The corpus is in artifacts/ch78-indexed-format-parser/. Its accepted source SHA-256 is the concatenation

The compiler distribution and executable are identified by the shared provenance record above. Run from the artifact directory:

cd artifacts/ch78-indexed-format-parser
kappa check corpus.kp
kappa test corpus.kp
kappa run corpus.kp
kappa audit corpus.kp

Check is silent, audit is [], and the run prints

PASS parse [2,1,3] produces [42,7,105]
PASS print preserves 427105
PASS final field rejected: expected width 3; actual width 2
All 3 Chapter 78 corpus cases passed.

Changing the short-field branch to accept an empty suffix remains typechecking and audit-clean, but test exits one because the final field is no longer rejected. The corpus imports graphemes from std.unicode, converts its Query Grapheme result to a list, rejects every non-decimal grapheme, and supplies only that checked digit stream to the width-indexed parser. KAPPA-ISSUES.md records the closed artifact error that originally omitted this required import. The corpus does not prove vector elimination, dependent-pattern compilation, coverage, or the no-K theorem.

Chapter 79: telescope-order checking

Reproducibility record for exercise 79.6. The corpus is in artifacts/ch79-dependent-record-checker/. Its accepted source SHA-256 is the concatenation

The compiler distribution and executable are identified by the shared provenance record above. Run from the artifact directory:

cd artifacts/ch79-dependent-record-checker
kappa check corpus.kp
kappa test corpus.kp
kappa run corpus.kp
kappa audit corpus.kp

The run is

PASS PointedLoop record accepted
PASS point projection computes to zero
PASS mismatched loop endpoint rejected: expected Id Nat 0 0; actual Id Nat 1 1
PASS field order is dependency sensitive
PASS duplicate label rejected
All 5 Chapter 79 corpus cases passed.

Check is silent and audit is []. Removing endpoint equality remains typechecking and audit-clean, but test exits one. The duplicate-label oracle records that the executable implements the chapter’s fresh-label projection fragment, not Pollack’s full repeated-label calculus. The corpus does not prove substitution, the Pollack-to-CPT correspondence, normalization, canonicity, or Sigma conservativity.

Chapter 80: one interpreted Tree code

Reproducibility record for exercise 80.9. The corpus is in artifacts/ch80-generic-description-interpreter/. Its accepted source SHA-256 is the concatenation

The compiler distribution and executable are identified by the shared provenance record above. Run from the artifact directory:

cd artifacts/ch80-generic-description-interpreter
kappa check corpus.kp
kappa test corpus.kp
kappa run corpus.kp
kappa audit corpus.kp

The run is

PASS Tree declaration elaborates through treeCode
PASS generic map transforms both recursive children
PASS generic fold size produces 3
PASS generic traversal produces leaves [1,2]
PASS dependent Sigma tag selects distinct payload codes
PASS negative recursive occurrence rejected
All 6 Chapter 80 corpus cases passed.

Check is silent and audit is []. Failing to reverse polarity in an arrow domain remains typechecking and audit-clean, but test exits one. The dependent-Sigma case also rejects both crossed payload shapes and an unknown tag. It implements only the finite regular normal form, not the whole MAG ISPT/SPF universe. The corpus does not prove indexed formation, description induction, the equality theorem, elaboration soundness, fold fusion, or the binding laws.

Optional route.

Chapter 81: finite container and ornament calculations $\star$

Reproducibility record for exercise 81.12. The directory artifacts/ch81-container-ornament-calculator/ contains the portable Kappa corpus. Its accepted source SHA-256 is 112855f3e5383c1 a8b1a03538098ed2 8777694d47322ed0 1bc2328ee73979132.

It was checked with packaged Kappa v0.3.0; the compiler binary SHA-256 is 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6.

From that artifact directory, run

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

The exact run output is

PASS container shape 3 matches three contents
PASS reverse morphism produces [8,4,2]
PASS one-hole plug produces [2,5,8]
PASS vector forget preserves [2,4,8]
REJECT declared length 2 with three contents: shape-content-mismatch
All 5 Chapter 81 corpus cases passed.

Check is silent, test reports one passed case, and audit returns []. The mutation is rejected by the same declared-shape check as the accepted vector. The finite corpus does not prove naturality, initiality, derivative laws, or the ornament representation theorem.

Chapter 32: checked Euclidean descent

Reproducibility record for exercise 82.7. The directory artifacts/ch82-well-founded-call-checker/ contains a Kappa implementation of the natural-measure calls in example 82.21. It targets the packaged Kappa v0.3.0 compiler. The accepted corpus SHA-256 is 07a66f22 39029915 49447833 e39a266d 5d910db1 ea8e729b 82aeab43 75aa8296. The tested compiler binary SHA-256 is 5b9b64ca c3cd2b43 f381d085 b46d2489 24bcc3a5 e65cb5a9 87d44e7d 5833c6b6; its packaged specification and compliance-ledger digests are recorded in the README. The run used arm64 macOS 26.3.1.

From that artifact directory, run

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

The exact run output is

PASS Euclid trace 18,12,6,0 is strictly decreasing
PASS gcd(48,18) = 6
PASS gcd(1071,462) = 21
PASS mutation gcd(48,18) -> gcd(18,48) rejected: 48 not<18
All 4 Chapter 82 corpus cases passed.

Each accepted Euclidean edge carries its old and new measure. The mutation $\mathsf{gcd}(a,b)\mapsto \mathsf{gcd}(b,a)$ proposes the first call $(48,18)\mapsto (18,48)$ and obtains Nondecreasing 18 48 independently of the driver’s fuel. kappa audit returns []; no compiler defect, unsafe feature, admission, or unchecked termination escape was used. The corpus checks four finite calculations. It does not prove accessibility induction, the well-founded recursor, certificate independence, or checker completeness.

Optional route.

Chapter 83: size-change matrices $\star$

Reproducibility record for exercise 83.8. The directory artifacts/ch83-size-change-checker/ contains the Kappa implementation of the selected two-parameter matrix closure and idempotent-cycle test. The corpus SHA-256 is feac8490ad15516a db75b4a642b7ddcc 1f0496329aac3d37 ddd1aba804e1b566; it uses the compiler and platform recorded in the preceding entry.

From that artifact directory, run

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

The exact output is

ACCEPT closure contains saturated [[strict,?],[strict,?]]
REJECT mutation [[weak,?],[strict,?]]: no-strict-diagonal
All 2 Chapter 83 corpus cases passed.

The audit result is []. The program decides the supplied finite matrices; the cited size-change theorem proves the infinite-descent consequence for safe call graphs.

Optional route.

Chapter 84: capture-free nested terms $\star$

Reproducibility record for exercise 84.10. The directory artifacts/ch84-mendler-nested-terms/ contains the portable Kappa corpus. Its accepted source SHA-256 is . It uses packaged Kappa v0.3.0 and the compiler binary digest recorded in the Chapter 81 entry.

From that artifact directory, run

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

The exact output is

PASS substitution prints lam(app(zeroV,sucV(7)))
PASS renaming identity
PASS renaming fusion 0 -> 2 -> 5
REJECT unshifted substitution under lambda: capture-detected
All 4 Chapter 84 corpus cases passed.

Check is silent, test reports one passed case, and audit is []. The executable flattens the nested family to cutoff-aware de Bruijn naturals; it does not implement rank-polymorphic Mendler iteration or prove parametricity, normalization, fusion, or substitution composition.

Chapter 33: guarded Fibonacci observation

Reproducibility record for exercise 85.8. The directory artifacts/ch85-guarded-stream-observer/ contains a Kappa finite-state observer for the pair transition used by the chapter’s Fibonacci stream. The accepted corpus SHA-256 is 09ffb0af92e57b32 b42aa243ab429825 061fa870b766ec37 59c491c38cb49d39.

The run used packaged Kappa v0.3.0 on arm64 macOS 26.3.1. The executable was kappa resolved by PATH. Its binary SHA-256 was 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6.

For the packaged Spec.md, the SHA-256 was 84ca9ed0 65995626 1853a9da ce910ef0 bd8edd86 70ad3b34 6bdb387d 9313ae1b.

For the packaged SPEC_COMPLIANCE.md, it was 41b1afa1 a4e63f94 92d63777 4544c817 84e616d3 d4a4af49 5ab0244d e0304b94.

From that artifact directory, run

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

The exact run output is

TRACE Fibonacci 0,1,1,2,3,5,8,13,21,34
PASS depth nine performs nine transitions
TRACE mutation 0,0
PASS mutated transition is rejected
All 4 Chapter 85 corpus cases passed.

The observer returns the value together with a counter incremented exactly once per successor depth; the depth-nine oracle checks both $34$ and $9$. The mutation replaces $(a,b)\mapsto (b,a+b)$ by $(a,b)\mapsto (a,a+b)$ and is detected at the second observation. kappa audit returns []; no compiler defect, unsafe feature, admission, or unchecked corecursion was used. Structural recursion on a finite depth checks the observations but does not prove guarded productivity, bisimulation soundness, or coinduction.

Chapter 86: recursive-effect observation

Reproducibility record for exercise 86.7. The directory artifacts/ch86-recursive-effect-interpreter/ contains the portable Kappa corpus for the successor server. Its accepted SHA-256 is f9caf842c1a24245 2235ce8c099ba7ab 7ff7fd1a89e64d5b beb8094d77537209.

The run used packaged Kappa v0.3.0 on arm64 macOS 26.3.1. The executable SHA-256 was 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6; the packaged Spec.md and SPEC_COMPLIANCE.md hashes are recorded in the preceding Kappa entry.

From that artifact directory, run

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

The exact run output is

TRACE server read 2; write 3; read 4; write 5
PASS one Tau preserves visible prefix
TRACE divergence silent-prefix
PASS successor mutation rejected
All 4 Chapter 86 corpus cases passed.

Audit returns []. The corpus computes a finite recursive-tree observer and mutation; it does not replay the source’s Rocq development or prove weak-bisimulation laws.

Chapter 87: bounded LTS fixtures

Reproducibility record for exercise 87.7. The directory artifacts/ch87-compositional-lts-checker/ contains the portable Kappa corpus for the four named finite fixtures. Its accepted SHA-256 is f1574a7f3123e686 0f16faa884b9251a 80b89d90f57c3159 57bf3956163437ab. From that artifact directory, run

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

The exact run output is

atomic-counter: PASS depth=6 (bounded)
atomic-exchanger: FAIL trace=call(0,exch2);call(1,exch4);ret(0,4);ret(1,2) depth=4
exchanger-vs-paired-set: PASS depth=4 (bounded)
two-counter-horizontal: PASS depth=6 (bounded)
MUTATION reversed-thread-tie-order: detected
All 5 Chapter 87 corpus cases passed.

Audit returns []. The corpus breadth-first computes the fixture traces and checks completed traces against their finite specifications; every PASS remains bounded testing. The corpus proves neither general refinement nor the locality and composition theorems.

Chapter 88: possibility exploration

Reproducibility record for exercise 88.7. The directory artifacts/ch88-lhl-possibility-explorer/ contains the self-contained Kappa queue explorer. Its accepted SHA-256 is a9c1c0aff113540d a498e86fd17ff86d 40acbd8bcb8f7d10 82ac7354378a9999. From that artifact directory, run

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

The exact run output is

TRACE enqueues {[1,2],[2,1]}
TRACE deq=1 {[2]}
TRACE forced [2,1] no-compatible-possibility
PASS exchanger remains singleton
PASS successor nonempty and stability
MUTATION incompatible possibility retained: detected
All 6 Chapter 88 corpus cases passed.

Audit returns []. The finite explorer is not a proof of LHL soundness, completeness, or a theorem about the native Rocq artifact.

Chapter 34: declaration summaries

Reproducibility record for exercise 89.8. The directory artifacts/ch89-pcuic-declaration-trace/ contains a Kappa checker for the chapter’s finite declaration-summary fragment. It checks family sorts and universe levels, exact constructor conclusions, uniform parameters, nested negative occurrences, constructor count and field sorts, and requested elimination families. The accepted corpus SHA-256 is 1df21fbeaecde136 3e651ac3b3340722 2edfc72ccffdfe9d 1f7e27311bed45f7. It uses the same packaged Kappa v0.3.0 compiler binary and platform as the preceding records.

From that artifact directory, run

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

The exact six-line report is

ACCEPT Vector
ACCEPT Equality
REJECT Bad at constructor-arg/domain
REJECT Exists: Prop-witness-blocks-Type-elimination
REJECT Or: Prop-not-singleton-for-Type-elimination
All 5 Chapter 89 corpus cases passed.

The replayed mutation ignores negative paths and therefore accepts Bad; the inline test rejects that result. kappa audit returns []; no compiler defect, unsafe feature, admission, or unchecked recursion was used. This nominal checker is not the historical PCUIC safe checker and supplies no proof of normalization, canonicity, consistency, or checker correctness.

Chapter 35: evidence-directed endpoint checking

Reproducibility record for exercise 90.20. artifacts/ch90-ett-evidence-checker/ contains the portable Kappa corpus for equality reflection. Accepted source SHA-256: a434967cd08b6607381c959eb6a5200533dcfe1215a0dffa6ffbb0495eb0da66. The tested packaged Kappa v0.3.0 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 90 corpus cases passed.; audit returns []. The replayed typechecking mutation was: Reflect evidence whose endpoints have different types. It makes kappa test exit nonzero. This is executable boundary evidence, not a proof of a metatheorem.

Chapter 36: PER decisions

Reproducibility record for exercise 91.11. The companion directory

contains the finite Kappa decision model for the chapter’s named lazy-evaluation and PER cases. Its accepted source SHA-256 is The tested installed Kappa v0.3.0 executable has SHA-256 This packaged distribution, also used for the Chapter 112 and 121 records below, has embedded build identifier kpp-hskll-0.3.0-1df6e4b1 on arm64 macOS 26.3.1. It exposes no compiler source commit or implementation toolchain, so neither is claimed. Its bundled Spec.md and SPEC_COMPLIANCE.md SHA-256 values are, respectively, 84ca9ed0659956261853a9dace910ef0bd8edd8670ad3b346bdb387d9313ae1b and 41b1afa1a4e63f9492d637774544c81784e616d3d4a4af495ab0244de0304b94. The separate specification repository at commit 216f913ee9d94519cccb3d9e16f6f9d3652188fe is not compiler provenance.

From that artifact directory, run

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

The exact run output is

eval-opening=3
int-eq-opening-3=true
nat-member-minus1=false
nat-member-opening=true
inc-spec-2=true
parity-eq-2-4=true
parity-eq-2-3=false
All 7 Chapter 91 corpus cases passed.

Changing the Diverge evaluator clause to a known zero value makes the first record fail; restore the clause before release. Audit returns []. The model decides only the named finite PER tags and neither constructs the Nuprl universe nor proves PER functionality, canonicity, consistency, or quotient soundness.

Chapter 48: independent annotation rechecking

Reproducibility record for exercise 110.10. artifacts/ch110-bidirectional-kernel-recheck/ contains a portable Kappa implementation of raw and core syntax, de Bruijn contexts, mutually recursive bidirectional checking, an independent core rechecker, and capture-avoiding core substitution. Accepted source SHA-256: $$\begin{array}{c}\mathtt{\text{9f3d4687965ca2b7}}\mathtt{\text{18d1860161631a1c}}\\ \mathtt{\text{e5357c953db11d8e}}\mathtt{\text{aa101be0bc162d6d}}.\end{array}$$ It uses the installed Kappa v0.3.0 executable with SHA-256 $$\begin{array}{c}\mathtt{\text{5b9b64cac3cd2b43}}\mathtt{\text{f381d085b46d2489}}\\ \mathtt{\text{24bcc3a5e65cb5a9}}\mathtt{\text{87d44e7d5833c6b6}}.\end{array}$$ The distribution exposes neither its compiler source commit nor its implementation toolchain, so neither is claimed.

From the repository root run

cd artifacts/ch110-bidirectional-kernel-recheck
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The exact run output is

identity=accept:Nat->Nat
successor=accept:Nat->Nat
application=accept:Nat
beta-substitution=accept:zero
nat-elim=accept:Nat
j-certificate=accept:Bool
wrong-step=reject:motive
wrong-ascription=reject:annotation
wrong-j-base=reject:motive
tampered-core=reject:recheck
tampered-j-proof=reject:recheck
All 11 Chapter 110 corpus cases passed.

Changing the CAnn rechecker arm to return its claimed type without checking its body gives mutant SHA-256 c1063e0da40c0973 4e7a3f51ca2529b1 d79719737a0795a5 e7170b5b5f36821c. The mutant passes kappa check, but the tampered-core oracle fails and kappa test exits nonzero. Independently, replace the complete CIdElim motive base equalityProof rechecker arm by

CIdElim motive _ _ ->
  Some (motiveResult motive)

The resulting mutant has SHA-256 $$\begin{array}{c}\mathtt{\text{7ca4f929e99bcb29}}\mathtt{\text{3c2d84a7cf2f550a}}\\ \mathtt{\text{31079b6796aaddee}}\mathtt{\text{66ff2ec14d85d8ad}}.\end{array}$$ It passes checking, but the tampered-j-proof oracle and aggregate fail, so the exact-output test exits nonzero. The accepted source was restored after each mutation. Audit returns [].

The model implements structural type equality, application, a constant-motive natural eliminator, and one finite identity-elimination certificate. It therefore tests the stated trust boundary but does not prove kernel soundness or completeness for the chapter’s full dependent theory.

Chapter 49: finite full-signature readback

Reproducibility record for exercise 111.17. artifacts/ch111-nbe-pi-bool/ contains a portable Kappa normalizer for the kernel signature $T_{\mathsf{impl}}$. It implements the value domain, evaluation, semantic application, projection and the four eliminators, semantic lifting, reflection, type-indexed eta-long reification, type quotation, code quotation, neutral readback, conversion by normal-form comparison, head inversion, a normal-form shape rechecker, and an idempotence check. Accepted source SHA-256:

It uses the installed Kappa v0.3.0 executable with SHA-256

The distribution exposes neither its compiler source commit nor its implementation toolchain, so neither is claimed.

Run

kappa check artifacts/ch111-nbe-pi-bool/corpus.kp
kappa test  artifacts/ch111-nbe-pi-bool/corpus.kp
kappa run   artifacts/ch111-nbe-pi-bool/corpus.kp
kappa audit artifacts/ch111-nbe-pi-bool/corpus.kp

The exact run output is

pi-eta=lamer(#2).(#2 er #0)
unit-eta=star
meta-kept=Pii0(#2).#3
meta-conv=reject
sigma-eta=<p1(#0),p2(#0)>
bool-stuck=if[Bool](tt,ff,#2)
nat-stuck=rec[Nat](0,lamer(Nat).lamer(Nat).S#0,#3)
id-stuck=J(Nat;#3;#3;Nat;#0;#0)
vec-stuck=vind[Nat](0,S#0,#3,#1)
bool-comp=ff
nat-comp=SS0
id-comp=0
vec-comp=S0
lift-vec-type=Vec(#1,#0)
vec-lift-type=Vec(L0(#1),#0)
lift-vec-code=L0(Vec(#1,#0))
vec-lift-code=Vec(L0(#1),#0)
lift-bool-code=Bool
lift-type-conv=accept
lift-code-conv=reject
level-conv=reject
level-normal=Umax(u0+1,u1)
level-schema-eq=accept
level-schema-permute=accept
level-schema-no=reject
symbolic-lift=Lu0(#0)
conv-accept=accept
conv-reject=reject
unPiMeta:i0:Bool
unUniv:max(u0+1,u1)
unUniv:none
wrong-readback=FAIL
normal-shape=True
idempotent-pi=accept
idempotent-vind=accept
All 35 Chapter 111 corpus cases passed.

Five semantic mutants are recorded in MUTATIONS.md; each passes kappa check, fails a named oracle and the computed aggregate, and is then replaced by the accepted source:

The fourth mutant collapses symbolic parameters to zero; its false acceptance of level-schema-no is the decisive witness that the accepted program compares schemas rather than one numeric assignment. Audit returns [].

The program is a normalizer and a partial rechecker over a fuel-bounded finite slice. It is not a type checker: the semantic type at which a term is read back is supplied by the corpus, and the rechecker verifies only the normal-form shape of the output and the idempotence of normalization. It neither infers semantic types nor checks universe formation. Execution tests the displayed evaluator, readback, conversion, and inversion cases; it does not prove theorem 111.76, theorem 49.18, or corollary 49.20.

Chapter 50: first-order contextual solver slice

Reproducibility record for exercise 112.14. artifacts/ch112-timpl-elaborator/ contains a Kappa first-order equation solver with arbitrary-arity rigid trees, ordered substitutions, and contextual flex–rigid assignment over finite list-valued declaration telescopes. It checks occurrence, scope, declaration arity, and distinct-variable spines; it decomposes equal rigid heads and reports rigid clash. A separate finite difference-constraint graph procedure detects positive-weight cycles of arbitrary length. The six named elaboration records traverse these reusable procedures. The accepted append and level-explicit vnil : Vec[0](Nat, zero) cores are reconstructed from actual solver assignments and checked by the independent finite kernel. Accepted source SHA-256: $$\begin{array}{c}\mathtt{\text{dac31334535acc64}}\\ \mathtt{\text{8d9c76e056d07110}}\\ \mathtt{\text{3889a0b3231709c8}}\\ \mathtt{\text{f133358c2e4deb11}}.\end{array}$$ It uses the installed Kappa v0.3.0 executable with SHA-256 $$\begin{array}{c}\mathtt{\text{5b9b64cac3cd2b43}}\\ \mathtt{\text{f381d085b46d2489}}\\ \mathtt{\text{24bcc3a5e65cb5a9}}\\ \mathtt{\text{87d44e7d5833c6b6}}.\end{array}$$

Run

kappa check artifacts/ch112-timpl-elaborator/corpus.kp
kappa test  artifacts/ch112-timpl-elaborator/corpus.kp
kappa run   artifacts/ch112-timpl-elaborator/corpus.kp
kappa audit artifacts/ch112-timpl-elaborator/corpus.kp

The exact run output is

append-ok=ok:append[u]{A}{m}{n} xs ys:Vec(A,n+m)
vnil-annotated-ok=ok:vnil[0]{Nat}:Vec(Nat,zero)
vnil-ambiguous=reject:unsolved-meta
occurs-bad=reject:occurs
scope-bad=reject:scope
level-cycle-bad=reject:level-cycle
All 6 Chapter 112 corpus cases passed.

Disabling the scope check in flex–rigid assignment lets the scope input produce a substitution. Its escaped core then reaches the finite kernel, which changes the fifth record from scope to kernel; the owner summary also reports failure. Restore the guard before release. Audit returns [].

Non-public guards check substitution after rigid decomposition, contextual abstraction and instantiation at a three-variable telescope, rigid clash, repeated-spine rejection, a three-node positive cycle, an acyclic graph, and a zero-weight cycle. Replacing the append-core kernel arm by unconditional acceptance leaves the public records fixed but makes a hidden malformed-core guard change the owner summary to failure.

The implemented boundary is first-order syntactic rigid/flex–rigid solving for distinct-variable spines and positive-cycle detection on finite integer-weighted graphs. It excludes flex–flex intersection, binders in term syntax, dependent typing, definitional equality, normalization, postponement, search, surface constraint generation, and a general Timpl kernel. It illustrates the chapter’s success conditions and trust boundary; it does not prove solver soundness, completeness, or a metatheorem about full Timpl.

Chapter 113: compact triangular unifier

Reproducibility record for exercise 113.8. artifacts/ch113-shared-dag-unifier/ contains a Kappa first-order worklist solver and a separate checker for its compact triangular bindings. Accepted source SHA-256: $$\begin{array}{c}\mathtt{\text{3a82337822726cfd}}\mathtt{\text{74c3d2531ce9072b}}\\ \mathtt{\text{0ceb21e304c2ecd4}}\mathtt{\text{ee146780102851de}}.\end{array}$$ It uses the installed Kappa v0.3.0 executable with SHA-256 $$\begin{array}{c}\mathtt{\text{5b9b64cac3cd2b43}}\\ \mathtt{\text{f381d085b46d2489}}\\ \mathtt{\text{24bcc3a5e65cb5a9}}\\ \mathtt{\text{87d44e7d5833c6b6}}.\end{array}$$

Run

kappa check artifacts/ch113-shared-dag-unifier/corpus.kp
kappa test  artifacts/ch113-shared-dag-unifier/corpus.kp
kappa run   artifacts/ch113-shared-dag-unifier/corpus.kp
kappa audit artifacts/ch113-shared-dag-unifier/corpus.kp

The exact run output is printed below. Its fifth logical line is wrapped after the first comma; concatenating the two centered fragments recovers the byte-for-byte stdout line.

shared-example=ok:x->G(y),y->G(a)
head-clash=reject:clash
occurs-self=reject:cycle
occurs-three=reject:cycle

All 5 Chapter 113 corpus cases passed.

Replacing the flexible-variable branch of occurs by False gives mutant SHA-256 6ecb04e96a22975b 7e5a210f0c79a913 12e7b3c0c8937ada e9888146c00640da. Checking and audit remain successful, but both cycle records become FAIL; the exact-output test exits nonzero. Independently replacing Symbol 4 by Symbol 3 in triangleRightHandSide gives mutant SHA-256 15123ab4a89cf014 174814d47eb89ed5 53fb2646b7dcdabb 5039fc3ef28e3ebe; only the compact-eight oracle and aggregate fail. The accepted source was restored after each mutation. Audit returns [].

The implementation represents first-order terms directly and preserves sharing by storing each triangular binding recipe once. It checks successful answers by applying those bindings to the original equations. It does not implement mutable term DAGs, union–find, parent lists, monotone graph cursors, or the Paterson–Wegman schedule. Its execution witnesses the finite semantic boundary cases and the exponential readback gap, but does not prove the chapter’s most-generality or linear-time theorems.