Dependent subtyping, object paths, and classical control: executable records

The four corpora are working-tree additions based on repository commit 386282d29bd483032a4bcd5f6dacd6d2c9a7fedf. They target Kappa v0.3.0 at /Users/wabbit/.local/bin/kappa. Its SHA-256 is 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. No unsafe flag, axiom, admitted lemma, unchecked positivity, or unchecked productivity condition is used. From each artifact directory, run kappa check corpus.kp, kappa test corpus.kp, kappa run corpus.kp, and kappa audit corpus.kp.

Chapter 44: three isolated ledgers

Reproducibility record for exercise 106.8. The corpus is artifacts/ch106-dependent-boundary-ledger/ corpus.kp; accepted SHA-256 is

The exact transcript is

$ kappa check corpus.kp
[exit 0]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
PASS dependent function comparison accepted
PASS reversed function domain rejected
PASS certified index zero accepted
PASS index three rejected
PASS negative cycle certificate accepted
PASS nonnegative cycle rejected
PASS nil round trip returns nil
PASS cons-to-zero cast returns error
PASS cross-ledger routing rejected
PASS forged path weight rejected
PASS disconnected certificate rejected
All 11 Chapter 106 corpus cases passed.
$ kappa audit corpus.kp
[]

Routing a refinement payload through the gradual ledger leaves a typechecking mutant, but the cross-ledger oracle fails. Its SHA-256 is

It passes kappa check; kappa test exits nonzero because the cross-ledger record changes to FAIL.

Trusting a certificate’s claimed path weight instead of recomputing its edge sum leaves a typechecking mutant, but the forged-weight oracle fails. The run checks eleven finite tagged requests; it proves no dependent-subtyping, refinement-soundness, graduality, or interoperability theorem. The replayed forged-weight mutant has SHA-256

It passes kappa check; kappa test exits nonzero because the forged-weight record changes to FAIL.

Chapter 45: inert selection

Reproducibility record for exercise 107.8. The corpus is artifacts/ch107-dot-inert-selection-checker/ corpus.kp; accepted SHA-256 is

The exact transcript is

$ kappa check corpus.kp
[exit 0]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
PASS cell context accepted
PASS bad bounds rejected
PASS duplicate label rejected
PASS lower tight selection printed
PASS upper tight selection printed
PASS unequal-bound mutation rejected
PASS missing member lookup rejected
PASS function entry has no member selection
All 8 Chapter 107 corpus cases passed.
$ kappa audit corpus.kp
[]

Ignoring equalBounds in the recursive-entry branch leaves a typechecking mutant, but the bad-bounds and unequal-bound oracles print FAIL. The corpus checks finite inertness certificates and tight selection chains. It is not a DOT typechecker and proves no canonical-form, preservation, progress, or decidability theorem. The replayed unequal-bound mutant has SHA-256

It passes kappa check; kappa test exits nonzero with the two named records changed to FAIL.

Chapter 46: stable lookup

Reproducibility record for exercise 108.9. The corpus is artifacts/ch108-pdot-stable-path-lookup/ corpus.kp; accepted SHA-256 is

The exact transcript is

$ kappa check corpus.kp
[exit 0]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
PASS x.a.c reaches a lambda
PASS alias replacement changes two occurrences
PASS missing target prefix rejected
PASS retained suffix formation enforced
PASS mutually recursive aliases report a cycle
PASS deleted-prefix mutation detected
PASS undeclared selected field rejected
PASS insufficient lookup fuel reported
All 8 Chapter 108 corpus cases passed.
$ kappa audit corpus.kp
[]

Deleting the declaredUse conjunct while retaining the declared-root gate leaves a typechecking mutant with SHA-256

Its test exits nonzero because retained suffix formation enforced becomes FAIL; the final summary is absent. The bounded interpreter reports cycles rather than proving termination. It proves no singleton-replacement, preservation, lookup, or pDOT safety theorem.

Chapter 47: finite NEF classification

Reproducibility record for exercise 109.8. The corpus is artifacts/ch109-dependent-control-nef-checker/ corpus.kp; accepted SHA-256 is

The exact transcript is

$ kappa check corpus.kp
[exit 0]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
PASS variable accepted in dependency
PASS lambda-pair accepted in dependency
PASS mu-alpha rejected in dependency
PASS mu-tp accepted in dependency
PASS application-spine rejected in dependency
PASS prf-pair nef but not normal
PASS normal mu-alpha is not nef
PASS mu-star rejects ordinary context
PASS control remains legal outside dependency
PASS dependent product prints visible result family
PASS p0 witness-proof mismatch exposed by mutation
PASS nondependent equality has no proof occurrence
All 12 Chapter 109 corpus cases passed.
$ kappa audit corpus.kp
[]

Changing the MuAlpha branch of nef to True leaves a typechecking mutant, but the ordinary-$\mu$ rejection, normal-but-not-NEF, and witness/proof-mismatch oracles print FAIL. The accepted MuStar fixture separately checks that its command uses only NStar or a NEF binder, rejecting an ordinary context. The program is a finite grammar and formula walk. It implements neither Miquey’s stores and commands nor CPS, preservation, normalization, or consistency. The replayed NEF-boundary mutant has SHA-256

It passes kappa check; kappa test exits nonzero with the three named records changed to FAIL.