Declaration processing, dependent copatterns, and erasure: executable records

The five corpora target Kappa v0.3.0 at /Users/wabbit/.local/bin/kappa, whose SHA-256 is 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. The recorded run used the local repository dtt-book, which has no configured remote, at worktree base commit 386282d29bd483032a4bcd5f6dacd6d2c9a7fedf. The five artifact directories were uncommitted additions at run time, so the per-corpus source digests below are the authoritative source identities for this record. No unsafe flag, axiom, admitted lemma, unchecked positivity, unchecked termination, or unchecked productivity declaration is used. Every diagnostic printed by these five programs is computed by the program: no verdict, path, frontier, or trace is a written-out constant. From each artifact directory, run kappa check corpus.kp, kappa test corpus.kp, kappa run corpus.kp, and kappa audit corpus.kp.

Chapter 122: signed strict positivity

Reproducibility record for exercise 122.5. The corpus is artifacts/ch122-datatype-block-positivity-checker/corpus.kp; accepted SHA-256 is ea27cac84308ea86001f7835ba687e5c02816bcdf5bf79d0a8bb925cf8330e17. 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
accepted: tree-forest
accepted: branching
branching hypotheses -,(y:Nat)->P(x y),P(fst x)*-,-
rejected: negative-bad at domain:negative
rejected: nested-bad at recursive-argument
rejected: double-negative at domain:blocked
rejected: former-bad at former-argument:List
All 7 Chapter 122 corpus cases passed.
$ kappa audit corpus.kp
[]

The third line is the hypothesis type of definition 122.8, computed for each binder of the accepted block. Three mutations are recorded. Treating a function domain as a codomain leaves a typechecking mutant with SHA-256

which accepts negative-bad and double-negative. Reversing the sign but leaving the ancestry flag open leaves a typechecking mutant with SHA-256

which still rejects negative-bad and accepts double-negative; that fixture is what shows the flag is not redundant. Returning the trivial hypothesis at a function field leaves a typechecking mutant with SHA-256

whose every verdict is unchanged: only the hypothesis line moves, from (y:Nat)->P(x y) to -, and the block is then accepted on the strength of an eliminator that cannot induct over that field. All three fail the exact stdout test. The corpus decides the finite regular grammar and computes the hypothesis types; it proves no positivity-model or normalization theorem.

Chapter 123: certified group descent

Reproducibility record for exercise 123.5. The corpus is artifacts/ch123-recursive-group-descent-checker/corpus.kp; accepted SHA-256 is 66c735aaeac10477594d6d9eb505374315465a34b2cbb45e9dca06cc7b702ca2. 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
accepted: even-odd
accepted: lex-reset
rejected: same-argument on odd->even
rejected: later-coordinate-only on loop->loop
All 4 Chapter 123 corpus cases passed.
$ kappa audit corpus.kp
[]

Changing the lexicographic scan to ignore an earlier increase leaves a typechecking mutant with SHA-256

which accepts later-coordinate-only. Dropping the component filter, so that every call site must descend, leaves a typechecking mutant with SHA-256

which rejects even-odd on its call to the auxiliary base outside the component. Both fail the exact stdout test. The corpus checks four finite call graphs and proves no termination theorem for arbitrary programs.

Chapter 124: finite stream observation

Reproducibility record for exercise 124.6. The corpus is artifacts/ch124-corecursive-group-observer/corpus.kp; accepted SHA-256 is 090be7630c7bca040b51de90e002430623e5979f472b5c8b5990fa1ea7307c04. 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
from-0=0,1,2,3
accepted: alternating ranks even=0,odd=0
accepted: alias-chain ranks f=2,g=1,h=0
alias-chain resolved heads f=0,g=0,h=0
rejected: head-loop zero-cycle f->g->f
All 5 Chapter 124 corpus cases passed.
$ kappa audit corpus.kp
[]

Relaxing the rank table once instead of once per vertex leaves a typechecking mutant with SHA-256 d34f7a58b2ac9ae506b59e894f8cb23815aa7337c39c5ea55b4e32f874801f61, which rejects the guarded alias chain. Dropping the strict rank decrease from the zero-edge certificate leaves a typechecking mutant with SHA-256 c4dc918ea7e0f78f17b27c8819ea5a93b8aeff718ee53a1f17f1eedaaebeef12, which accepts head-loop at equal ranks. Both fail the exact stdout test. Finite observations are witnesses, not a productivity or normalization proof.

Chapter 125: typed frontiers

Reproducibility record for exercise 125.5. The corpus is artifacts/ch125-dependent-copattern-case-tree/corpus.kp; accepted SHA-256 is f38a98d0e21cad679878de07d1258d3874e2975f14d7fc4bcb1b885afe87dd69. The exact transcript is

$ kappa check corpus.kp
[exit 0; no stdout]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
tree=corec(s){next=succ s;step=refl next;tail=s:=succ s}
frontiers=next:{};step:{next};tail:{next,step}
iterate-observations=1,2,3
rejected: step-before-next at field step missing next
rejected: uncovered-input at field next input zero
rejected: missing-field at field step
rejected: per-field-uncovered at field step input zero
rejected: ill-typed-term at field next expected successor of state
All 8 Chapter 125 corpus cases passed.
$ kappa audit corpus.kp
[]

The tree, frontiers, and trace are read from the compiled spine. The five typechecking mutation digests are

They expose, respectively, predecessor checking, constructor coverage, stored frontier advancement, per-field coverage, and finite right-side typing. Each passes kappa check, fails kappa test at its named oracle, and has empty audit. The program checks one finite record and proves no general copattern-elaboration theorem.

Chapter 126: untyped execution shapes

Reproducibility record for exercise 126.9. The corpus is artifacts/ch126-dependent-definition-erasure-runner/corpus.kp; accepted SHA-256 is

The exact transcript is

$ kappa check corpus.kp
[exit 0; no stdout]
$ kappa test corpus.kp
PASS corpus.kp
total 1: 1 passed, 0 failed, 0 unsupported, 0 harness errors
$ kappa run corpus.kp
append-two-singletons=vcons(a,vcons(b,vnil))
append-runtime-arity=2
from-0=0,1,2,3
sigma-projections=a,b
bool-elim=suc(zero)
J-erasure=a
J-alpha=lam(y',y)
branch-alpha=case(K(a,b)){K(x'',x')=>pair(x,x')}
refl-value=refl
retained-unused-branch=zero
rejected: erased-branch-use at inconsistent relevance annotation
rejected: unretained-branch-use at inadmissible branch relevance at hiddenbox
rejected: inconsistent-constructor-signature at inconsistent constructor signature
rejected: duplicate-case-tag at duplicate case tag
rejected: inconsistent-binder-relevance at inconsistent relevance annotation
rejected: standalone-erased-lambda at no runtime relevance derivation
rejected: erased-boolean-branch at erased scrutinee proof
erased-application=f
rejected: non-administrative erased application
All 19 Chapter 126 corpus cases passed.
$ kappa audit corpus.kp
[]

The first line is produced by the Texec evaluator of definition 126.1 applied to the erased $\mathsf{append}$ closure, not by a source-level list append; fuel is a checked budget and exhaustion would print out-of-fuel. The eight typechecking mutation digests, in the exercise’s order, are

They expose binder retention, erased-scrutinee rejection, branch arity, branch admissibility, freshening, binder lookup, constructor signatures, and tag distinctness. Each passes check, fails the exact stdout test, and has empty audit. The byte-authoritative recipes are mutants/A.patch through mutants/H.patch in the artifact directory; applying each patch to the accepted corpus produces exactly its listed digest. The runner exercises both simulations and proves neither.