Rewriting and dependent resource systems: executable records

All four corpora target the installed Kappa v0.3.0 executable with SHA-256 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. For each path below, run kappa check corpus.kp, kappa test corpus.kp, kappa run corpus.kp, and kappa audit corpus.kp from its artifact directory. Every accepted audit returns [].

Chapter 39: finite rewrite certificates

Reproducibility record for exercise 97.6. The corpus is artifacts/ch97-lambda-pi-modulo-certificate-checker/corpus.kp; accepted SHA-256 is 96d2ca1e211dac85f3fe02684d6e5ec135542dc9b8347c529b4c7c9f9c7f714e. The run prints eight named passes and ends All 8 Chapter 97 corpus cases passed. Certificates store endpoint terms, infer both endpoint types, traverse every supplied overlap, and compute joins at fuel 12. The accepted MoreOverlaps fixture reaches its later dishonest pair. Changing the inferred type of $\mathsf{Truth}$ to $\mathsf{Nat}$ leaves a typechecking mutant but fails the endpoint-inference oracle. Replacing the recursive MoreOverlaps branch by True also typechecks and fails the later-dishonest-pair oracle. Structural decrease is supplied evidence, not a computed termination proof. The corpus is not a dependent typechecker, termination prover, confluence prover, or mechanization of subject reduction.

The retained implementation pins used for static comparison are Dedukti 2.7 at commit d73a00d04766a7b0ed44f8c00834eb908662a50e and Lambdapi 3.0.0 at f73c64dbeebf850ecc3384d64f0dbf93a1ea6acd. These provenance hashes do not enlarge the Kappa artifact’s theorem boundary.

Chapter 40: shape and state usage

Reproducibility record for exercise 98.8. The corpus is artifacts/ch98-linear-dependent-state-checker/corpus.kp; accepted SHA-256 is 5efa395f1a67e56ede4fb69877ff4cb5c0fdbcb42ee6eef7bff8b373f23486d7. The run prints seven named passes and ends All 7 Chapter 98 corpus cases passed. A term/context traversal computes uses, a separate type traversal rejects raw state indices, and every state type has unit shape; the observable result type remains separate. Changing the shape of $\mathsf{CellState}(w)$ to expose $w$ leaves a typechecking mutant but fails the state-shape oracle. The finite checker proves neither simultaneous substitution nor categorical soundness.

Chapter 41: semiring demand

Reproducibility record for exercise 99.7. The corpus is artifacts/ch99-quantitative-demand-calculator/corpus.kp; accepted SHA-256 is 78a116185410d08abdd176fc2389cf6a44abf43ec80269fcafabdb0e8312bc9b. The run prints eight named passes and ends All 8 Chapter 99 corpus cases passed. Natural-number and zero–one–many contexts both preserve and compare their named spines; a term traversal infers duplicate use as Many, so a promised One is rejected. Omitting zero–one–many multiplication during scaling leaves a typechecking mutant but fails the named substitution oracle. Making natural-context spine comparison constantly true separately fails the named mismatched-spine oracle. The calculation is not an admissibility or erasure theorem.

Chapter 100: three-component grades

Reproducibility record for exercise 100.8. The corpus is artifacts/ch100-graded-modal-vector-calculator/corpus.kp; accepted SHA-256 is 211395e7ca559e10e8d2fdc02bfdcefcdf6067c46a0b6c4737f3b4d1fe2cd9ec. The run prints eight named passes and ends All 8 Chapter 100 corpus cases passed. Recursive grade rows and a recursive row list implement position-indexed discard, column choice, scaling, and insertion. The nonzero fixture computes $3+2\cdot 4=11$. Failing to increment the expected row length, or dropping the retained $3$ summand, leaves a typechecking mutant but fails its named oracle. Copying the subject vector into the subject-type field separately fails the named separation oracle. The corpus is neither a GrTT typechecker nor a proof of preservation, strong normalization, or operational erasure.