Proof production, metaprogramming, and universe engineering: executable records

The seven corpora use packaged Kappa v0.3.0. The tested executable SHA-256 is

In each directory run, in order, kappa check corpus.kp, kappa test corpus.kp, kappa run corpus.kp, and kappa audit corpus.kp. Every accepted check is silent, every test reports one passing corpus, and every audit is [].

Chapter 114: proof-producing tactic replay

Reproducibility record for exercise 114.4. The directory is artifacts/ch114-proof-producing-tactic-replayer/. Its accepted SHA-256 is

Its run is

accepted: lambda-lambda-var
accepted: pair-var-var
rejected: missing-validation-argument
All 3 Chapter 114 corpus cases passed.

The replayed mutation returns after the first generated goal. It still checks, but the third line becomes accepted: invalid-drop and the test exits nonzero. This is finite validation bookkeeping, not a proof of tactic soundness or kernel soundness.

Chapter 115: reflected monoid equality

Reproducibility record for exercise 115.4. The directory is artifacts/ch115-commutative-monoid-simplifier/. Its accepted SHA-256 is

Its run is

equal
equal
not-equal
dependent-respectful
All 4 Chapter 115 corpus cases passed.

Discarding the right summand during normalization still checks but changes the first two lines to not-equal; the test fails. Replacing the heterogeneous $\mathsf{Small}/\mathsf{Large}$ fiber relation by a same-fiber test changes the fourth line to dependent-respectful-failed; that test also fails. The corpus checks finite multiplicity maps and one finite model of dependent respectfulness. It proves no reflection, termination, or generalized-rewriting theorem.

Chapter 116: scoped macro expansion

Reproducibility record for exercise 116.4. The directory is artifacts/ch116-scoped-hygienic-macro-expander/. Its accepted SHA-256 is

Its run is

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

Seven semantic mutants still check and fail the stdout oracle. Collapsing the origin renaming changes the fourth line to origin-renaming-collapsed. Omitting the constructed-binder environment extension changes the fifth to constructed-binder-unresolved. Ignoring a variable’s phase changes the ninth to accepted: ill-staged. Omitting alpha-renaming changes the tenth to beta-capture-detected. Omitting the substitution target from the alpha-renaming freshness bound changes the eleventh to absent-target-corrupted. Adding the introduction stamp to copied caller syntax changes the first to caller-reference-captured. Reversing the analytical true branch changes the eighth to analytical-failed. Restore the accepted source and require a silent check, one passing test, the exact run, and an empty audit. These are finite hygiene, origin-renaming, provenance, source-typing, staging, substitution, and computation oracles, not a theorem for a production macro expander.

Chapter 117: level normalization

Reproducibility record for exercise 117.6. The directory is artifacts/ch117-first-class-level-normalizer/. Its accepted SHA-256 is

Its run is

equal
equal
not-below
All 3 Chapter 117 corpus cases passed.

Combining successor exponents by minimum still checks but changes the final decision to below; the test fails. The program decides only the finite level algebra, not type conversion or typing.

Chapter 118: bounded sort constraints

Reproducibility record for exercise 118.7. The directory is artifacts/ch118-bounded-sort-constraint-solver/. Its accepted SHA-256 is

Its run is

accepted
accepted
rejected: elimination
All 3 Chapter 118 corpus cases passed.

Treating the elimination table as complete still checks but changes the third line to accepted; the test fails. This finite table solver proves no SortPoly or bounded-calculus metatheorem.

Chapter 119: coherent path comparison

Reproducibility record for exercise 119.6. The directory is artifacts/ch119-coherent-coercion-path-checker/. Its accepted SHA-256 is

Its run is

unique
coherent
rejected: parallel-casts
All 3 Chapter 119 corpus cases passed.

Comparing normalized programs only by length still checks but reports the bad diamond coherent; the test fails. The finite graph does not prove coherence or completion for an arbitrary coercion signature.

Chapter 120: positive actions

Reproducibility record for exercise 120.4. The directory is artifacts/ch120-positive-description-action-checker/. Its accepted SHA-256 is

Its run is

identity
composition
dependent-sigma
rejected: negative-occurrence
All 4 Chapter 120 corpus cases passed.

Returning the original right product component still checks but changes the first line to identity-failed; always selecting the zero Sigma fiber changes dependent-sigma to dependent-sigma-failed. Both tests fail. The interpreter covers the finite description language, not the normalization and checking theorem.

Chapter 121: five finite clause outcomes

Reproducibility record for exercise 121.9. artifacts/ ch121-dependent-clause-compiler/ contains the structured finite Kappa row-specialization model for the chapter’s five closed acceptance groups. Accepted source SHA-256: aa2eb1f7600dd519 867747b8327caacc 13e7a66a27f09481 b8b06a2c568ffb83. It uses the same installed Kappa v0.3.0 executable and digest as the preceding record.

From the repository root run

cd artifacts/ch121-dependent-clause-compiler
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The exact run output is

append-123=ok:[1,2,3]
overlap-bool=ok:true->0,false->1,shadowed-wildcard=true
missing-false=reject:uncovered:path=false
bad-dot=reject:inaccessible:forced=suc(k),written=k
absurd-bool=reject:reachable:true,false
All 5 Chapter 121 corpus cases passed.

The last record aggregates both positive Boolean branches as a finite artifact-only observation. The mathematical compiler of definition 121.12 instead returns its single declaration-order result $\mathsf{badAbsurd}(1,\mathsf{tt},(\mathsf{tt}))$. Changing buildMissing to return the accepted Boolean tree makes the third record fail; restore the rejection before release. Audit returns []. The model traverses structured finite patterns, preserves the frontier/row-width invariant after single-use selected specialization and zero-width forced-image matching, derives generic split trees and actual assignment lists from branch specialization, evaluates append by interpreting the derived tree, checks whole-term selected successor dots, and computes wildcard shadowing by ordered priority. It does not type arbitrary dependent matrices, implement branch-local restricted unification, or prove the compiler theorems.