Erasure, dependent protocols, effects, specifications, and partiality: executable records

The five corpora are working-tree additions based on repository commit 8b1c2dee7be41fac33d6de1146fab4061a1b2a61. 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 101: guarded finite extraction

Reproducibility record for exercise 101.5. The corpus is artifacts/ch101-graded-erasure-trace-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 erased-index suc zero
PASS retained-argument argument retained
PASS open-erased-match rejected: erased match in open context
PASS inferred-use rejects dishonest zero grade
PASS closed-erased-match is accepted
PASS shadowed same-name use does not retain outer binder
All 6 Chapter 101 corpus cases passed.
$ kappa audit corpus.kp
[]

Deleting the retained argument at an inferred grade-one application leaves a typechecking mutant, but its named oracle fails. Treating every variable as unused and descending under a shadowing binder separately fail the dishonest zero-grade and shadowing oracles. These runs check finite extraction decisions, not logical-relation soundness or heap-access accounting. The replayed grade-one-deletion mutant has SHA-256

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

Chapter 102: indexed protocol traces

Reproducibility record for exercise 102.8. The corpus is artifacts/ch102-dependent-session-trace-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 vector-2 accepted: end
PASS vector-length-mismatch rejected: expected Vec 2
PASS duplicate-endpoint rejected: endpoint reused
PASS payload substitution changes continuation index
PASS array-3 accepted: end
PASS array-3-short rejected: expected Vec 1
All 6 Chapter 102 corpus cases passed.
$ kappa audit corpus.kp
[]

Replacing the length transition’s stored state by None makes the vector, mismatch, and substitution oracles fail. Stopping unfoldRepeat one element early separately fails both array oracles. Bypassing the endpoint-generation comparison in SendVector accepts the replayed endpoint and fails its named oracle. The replayed payload-substitution mutant has SHA-256

It passes kappa check; kappa test exits nonzero because the vector, mismatch, and substitution records change to FAIL. The run checks finite traces, not preservation, closed global progress, or the ATS static sort.

Chapter 42: dependent sequencing

Reproducibility record for exercise 103.5. The corpus is artifacts/ch103-dcbpv-dependent-sequencing-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 return-vector-2 accepted: Vec 2
PASS raw-effect-in-type rejected: computation in value position
PASS force-neutral neutral computation
PASS readto-classifier accepted: thunked
PASS global read is not thunkable; inclusion required
PASS dependent bind substitutes returned value
PASS force-thunk evaluates its computation
PASS unknown thunk dependency rejected
All 8 Chapter 103 corpus cases passed.
$ kappa audit corpus.kp
[]

Accepting the raw-computation fallback in inferClassifierIndex leaves a typechecking mutant, but the raw-effect oracle fails. Replacing ThunkedRead lo hi by ThunkedRead lo lo fails both read oracles. Classifying GlobalReadEffect as thunkable fails only the equality-versus-inclusion oracle. Disabling force/thunk computation and accepting an unknown thunk dependency fail their named oracles. The corpus illustrates a finite rule delta; it proves neither the Fire Triangle nor subject reduction. The replayed raw-computation-fallback mutant has SHA-256

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

Chapter 104: finite verification conditions

Reproducibility record for exercise 104.5. The corpus is artifacts/ch104-dijkstra-vc-generator/ 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 increment vc valid
PASS negative-raise exception post valid
PASS bad-advertised-post vc rejected
PASS bind threads updated state
PASS catch handles the raised computation
PASS put changes the state seen by get
All 6 Chapter 104 corpus cases passed.
$ kappa audit corpus.kp
[]

Passing the original rather than updated state through bind leaves a typechecking mutant, but the increment, state-threading, and direct put/get oracles fail. Propagating a caught failure instead of running its handler separately fails the catch oracle. The corpus decides finite postconditions; it proves no normalization, WP-soundness, or external-solver theorem. The replayed non-threading-bind mutant has SHA-256

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

Chapter 43: fuel-bounded observation

Reproducibility record for exercise 105.6. The corpus is artifacts/ch105-partiality-fuel-observer/ 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 gcd-6-4-20 done 2
PASS search-even-from-3-4 done 4
PASS search-never-12 later
PASS one fuel removes at most one step
PASS partial bind preserves its source step
PASS delayed continuation contributes one step
PASS return is observable without fuel
All 7 Chapter 105 corpus cases passed.
$ kappa audit corpus.kp
[]

Removing a residual step at zero fuel, dropping a bind continuation, and adding an early-equality exit to the printed Gcd machine each leave a typechecking mutant but fail the residual-machine, bind, and three-delay Gcd oracles respectively. The run witnesses finite convergence only; later is not a divergence proof. The replayed zero-fuel mutant has SHA-256

It passes kappa check; kappa test exits nonzero because the one-step fuel record changes to FAIL.