docs: orphaned debt gets a queue — #14 and #50 enter gap_selfhost as T13/T14 #197

praghunathan · 2026-08-14T12:40:08+02:00

praghunathan commented

2026-08-14 12:40:08 +02:00

docs: orphaned debt gets a queue — #14 and #50 enter gap_selfhost as T13/T14

Along the way:

selfhost: the dead-side envelope claim becomes a cell — Law 3 pays its prose
selfhost: one declaration per number — the impl's agreeing copies die
selfhost: T13 falls the other way — the clauses stay, and a gate now reads them
selfhost: T14 falsified — a String crosses a match arm, take_if retires
selfhost: the machine gets its encoders — Emit lays bytes, Elf grows a second segment
selfhost: the skip learns the input idiom's spellings; Recognize halts before the body
selfhost: INPUT — Eval's law splits, and the plex is the Σ the compiler computes

Touches 22 files: src/cklang/compiler/Elf.ck, src/cklang/compiler/Elf.ckh, src/cklang/compiler/Emit.ck, src/cklang/compiler/Emit.ckh, src/cklang/compiler/Eval.ck, src/cklang/compiler/Eval.ckh and 16 more.

docs: orphaned debt gets a queue — #14 and #50 enter gap_selfhost as T13/T14 Along the way: - selfhost: the dead-side envelope claim becomes a cell — Law 3 pays its prose - selfhost: one declaration per number — the impl's agreeing copies die - selfhost: T13 falls the other way — the clauses stay, and a gate now reads them - selfhost: T14 falsified — a String crosses a match arm, take_if retires - selfhost: the machine gets its encoders — Emit lays bytes, Elf grows a second segment - selfhost: the skip learns the input idiom's spellings; Recognize halts before the body - selfhost: INPUT — Eval's law splits, and the plex is the Σ the compiler computes Touches 22 files: `src/cklang/compiler/Elf.ck`, `src/cklang/compiler/Elf.ckh`, `src/cklang/compiler/Emit.ck`, `src/cklang/compiler/Emit.ckh`, `src/cklang/compiler/Eval.ck`, `src/cklang/compiler/Eval.ckh` and 16 more.

hkowalski approved these changes

2026-08-15 14:28:15 +02:00

hkowalski left a comment

Approving. I would have split src/rust/crates/ck_driver/tests/stdlib_composes_silence.rs differently, but not enough to hold this up.

Approving. I would have split `src/rust/crates/ck_driver/tests/stdlib_composes_silence.rs` differently, but not enough to hold this up.

src/rust/crates/ck_driver/tests/stdlib_composes_silence.rs

					
				@ -0,0 +122,4 @@

				/// and it must have none: this is the machine behind Types.ck's "the SELF-ROOT

				/// check vouches for this line".

				#[test]

				fn the_live_stdlib_checks_clean_as_its_own_root() {

the_live_stdlib_checks_clean_as_its_own_root reads, decides and writes in one function. The deciding part is the piece I would want to test on its own. Worth splitting?

`the_live_stdlib_checks_clean_as_its_own_root` reads, decides and writes in one function. The deciding part is the piece I would want to test on its own. Worth splitting?

praghunathan commented

2026-08-16 06:30:00 +02:00

Split. The decision in the_live_stdlib_checks_clean_as_its_own_root is a pure function now, with its own tests in src/rust/crates/ck_driver/tests/stdlib_composes_silence.rs.

Split. The decision in `the_live_stdlib_checks_clean_as_its_own_root` is a pure function now, with its own tests in `src/rust/crates/ck_driver/tests/stdlib_composes_silence.rs`.

praghunathan added 8 commits

2026-08-17 14:23:20 +02:00

docs: orphaned debt gets a queue — #14 and #50 enter gap_selfhost as T13/T14 ff644a9322

A debt number pointing at the deleted register is untracked debt (§3a).
The composes-Equals silence (Types.ck, declared ≠ actual) and the
String-across-match detour behind take_if (Prelude) now sit in the Tier-2
queue with their retirement conditions; every citation site names its
entry. #33 stays a bare historical citation — it marks a RULED law that
landed, not open debt.

Law-watchdog finding 2, tracked. Comment-only in the stdlib; check clean.

selfhost: the dead-side envelope claim becomes a cell — Law 3 pays its prose 0e9d7eb359

The comment at skip_verdict declared the dead side measures its OWN
envelope from depth 0; the code did it in four places and no test
observed it. Now one does, both directions and both dead positions: a
dead branch 8 deep inside a live context already 5 deep is accepted (the
fresh envelope — a shared counter would refuse it), a 9th dead nesting is
err 8, and a settled || carries the same pair at its skipped operand.

Law-watchdog finding on b4ef0376, paid. Suite 146/146.

selfhost: one declaration per number — the impl's agreeing copies die d5d9a5f616

Probed both directions: a module reads its own header's consts (check
clean with the impl copy deleted), and a header and impl DISAGREEING
still check clean — the header's spelling folds, the impl's is dead
text. So an agreeing copy is drift waiting, bound by nothing; the
FILE_SIZE pair 10d26a70 introduced, Lexer's MAX_SOURCE pair, and Eval's
three cap pairs all retire — the header is THE declaration. The silent
acceptance is pinned by header_and_impl_const_may_disagree_silently
(runs: 42, the header's number), which moves the day the contract is
enforced. CELL_COUNT 390 → 391.

Also: "#33" drops the debt label — it cites a settled ruling, and a
false status word poisons every debt grep.

Law-watchdog findings. Suite 146/146; capability 391 green.

selfhost: T13 falls the other way — the clauses stay, and a gate now reads them 179bf16fe4

Probed both positions. T13's premise ("unqualified root-trait names
don't resolve from mod Types") is false: the composes probe is the
compilation-global trait roster — a Prelude trait binds bare from any
module, an unknown name refuses (E0753), and a qualified spelling never
reaches the resolver (E0013: the clause grammar takes bare identifiers
only, the parser reports the `::`). What LOOKED like silence is an
ATTRIBUTION boundary, not a missing pass: a dependency unit's
diagnostics are dropped at the app boundary, so no app check ever
vouched for a stdlib page's clause — `composes NoSuchTrait` spliced into
String checks clean under a trivial app, and the same bytes refuse when
the stdlib is its own root.

So the lawful fix is the opposite of the queued deletion: the
behaviour-trait entries (Equals/Ord/Show/Concat) stay, spelled exactly
as the root spec authors them, and the machine that reads them is the
SELF-ROOT check (app == stdlib), gated in
ck_driver/tests/stdlib_composes_silence.rs — the silence pinned with
doctored bytes and two contrast arms, and the live stdlib asserted clean
as its own root. The falsified SILENT prose is deleted from both stdlib
copies; Types.ck cites the pins instead. T13 leaves gap_selfhost.md
paid: falsified, its truth in cells.

Five new cells: an_unknown_composes_trait_name_refuses (E0753),
a_qualified_composes_trait_name_is_a_grammar_gap (E0013),
composes_resolves_a_prelude_trait_unqualified,
composes_resolves_a_sibling_module_trait,
composes_trait_args_are_not_arity_checked (the live hole: 3 args on a
1-param trait pass clean). CELL_COUNT 391 → 396.

Also: Prelude.ck "#31" drops the debt label — same fix as #33 in
e064bca0.

Check clean · suite 146/146 · capability 396 green · stdlib self-root
gate green. Corpus oracle skipped: the corpus stdlib edit is
comment-only, folding untouched.

selfhost: T14 falsified — a String crosses a match arm, take_if retires ab560f5a74

Probed before building (the T13 lesson, taken literally). T14's premise
("a String may not cross a match arm") is false in every shape the
Prelude formats need: a region-typed PARAM as an arm result, param vs
empty-literal arms across two regions, and the exact corpus group-site
shape (newtype-ctor round-trip in the true arm) all check clean and exit
42. The law was already paid by the merge-slot fix
`match_string_arm_result` pins — a merge slot is a BINDING and takes the
value's whole word list, the `(position, len)` descriptor for a String
(docs/values.md:147) — and nothing in that law is literal-only. The
queue entry was stale at queue time.

The derivation, from the docs and not from emission: a match is typed to
the union of its arm bodies; every value is a `(position, len)`
descriptor into the fenced region (docs/values.md:147); a merge binds
whichever arm's descriptor jumped in, exactly as a `let` of either value
would — region identity rides in the position word, so arms need not
share a region. No new region law exists to add: the binding law already
covers the merge, which is why the fix is deletion, not construction.

So `take_if` — the len-0-same-region detour that existed only because
the merge once took a single word — retires from BOTH trees. The live
src/cklang/stdlib had no callers (the show engines are excised): the fn
and its header row are deleted, and the self-root gate
(stdlib_composes_silence) holds. The corpus tree's five call sites in
`span_text` (Types.ck) become what they always meant: a `match` on the
magnitude with the String in the arms — the group when nonzero, the
empty literal when zero. Same widths, same narrowing round-trips, same
rendered text (`timespan_show_omits_zero_groups` still pins `2m13s`).

Two new cells hold the probes: `string_param_as_match_arm_result` (the
detoured shape, runs 42) and `string_param_and_empty_literal_match_arms`
(two source regions merging, runs 42). CELL_COUNT 396 → 398. T14 leaves
gap_selfhost.md paid: falsified, its truth in cells — the watchdog queue
(T13, T14) is empty.

Check clean · suite 146/146 · capability 398 green · self-root gate
green · corpus oracle 45/45 (the corpus stdlib changed; the oracle run
is the proof the emitted images agree).

selfhost: the machine gets its encoders — Emit lays bytes, Elf grows a second segment c1e1feb816

Emit.ck is the closed set of fixed-length x86-64 encodings the input
vertical emits — loads, stores and immediates over absolute addresses,
the register algebra, cmp/setcc, the jumps, the call, and the two
composed sequences (read, exit) whose sizes are sums of their parts.
Every encoding was executed on the machine before it was transcribed;
every size is one public const, declared == actual, one declaration per
number (SZ_LOAD/SZ_LOAD2/SZ_STORE would be three names for the number 8,
so ABS_SIZE is the one name).

Elf.ck learns the two-segment input image: emit_input_headers writes the
same ELF64 header law through the one put_ehdr both emitters now share
(entry and phnum are the only two fields that ever differed), phdr 1
covers the file R+X as today, phdr 2 reserves the plex at DATA_VADDR —
filesz 0, memsz the Σ the generator computed, zero-filled by the loader.
The pure 132-byte exit image is untouched, byte for byte, and its tests
prove it. SYS_EXIT now lives once, in Emit.

selfhost: the skip learns the input idiom's spellings; Recognize halts before the body ba1e6995d0

The grammatical skip — declared a syntactic superset — now walks the
qualified call, the Region literal, the usize ascription tail and the one
release statement between the lets and the tail, all under the same
nesting guard (the turn bounds are unmoved and restated where they live).
Eval's fold refuses every one of them as a value, err 1, and the split is
pinned from both sides: the shape is accepted, the number does not exist
until a generator computes what can be computed and emits what cannot.

Recognize::prepare is the pipeline before main's body — shape, Eof, the
entry, the duplicate law, every const folded — stopped exactly where the
fold and the emitter part ways; recognize() is prepare plus the body fold
plus the exit range, verdict-identical to before, refusal order preserved
verbatim. The internals Gen walks with (the checked arithmetic, the
comparison table, the scans, the frame, the callee fold, the dead-side
skips, the declaration stepper) become public declarations in the
headers — one spelling each, moved not copied.

selfhost: INPUT — Eval's law splits, and the plex is the Σ the compiler computes c8a85002ce

The vertical the totality was waiting for: with the carve idiom in main
(Floor::mmap folded to a constant — the runtime never allocates, the
loader reserves; Region over it; Floor::read_bytes(0, …) as the one
input; Bytes::at widened to the exit word; munmap folded to the release
the exit already is), a program holds ONE value the compiler cannot
compute, and Gen.ck splits Eval's law exactly there: everything
computable from source still folds — the fold is the proof, dead sides
emit no bytes — and what depends on input is emitted as 1:1 machine code
over absolute addresses, with ZERO runtime checks: exit range, overflow,
divisor and index are proven over compiler-computed intervals (a simple
branch refines both arms) or the program is refused. Err 15, driver 78:
the region law, both directions.

The plex is the Σ law's fourth reading — the program is a record,
instances are fields: carve + Σ 8·(params + runtime lets + temps) over
main and every fn reached by a runtime call (the reach query rides the
check walk), frames at prefix-sum offsets from DATA_VADDR, every slot an
address in the emitted bytes. Count and write are one walk under a flag,
so declared size IS emitted size; the callee is checked per site and
emitted once, because instruction choice reads foldedness alone, never
an interval. The text envelope C_TEXT is a theorem with its densest
witness named, and the ELF carve follows the emitter through it.

Main.ck now compiles through Gen; the pure program still folds to the
fixed 132-byte image, the degenerate resident of the same field.

hkowalski manually merged commit 2a4ae4838a into master

2026-08-17 14:23:20 +02:00

hkowalski referenced this pull request from a commit

2026-08-17 14:23:20 +02:00

Merge pull request #197 from northgale/feat/197-docs-orphaned-debt-gets-a-queue-14-and-50-ente

Sign in to join this conversation.

No reviewers

No labels

No milestone

No project

No assignees

2 participants

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

northgale/cklang-bootstrap!197

Rows
Columns