Analyse .tmc completeness: what can a routine only say in prose?

[mellonis]

.tmc can declare a fair amount about a program — alphabets and tape typing, routine and graph signatures, writes/preserves contracts with footprint inference, volatile tapes, [deprecated], and, once the binding arc lands (#95, #118), state parameters as exits, noreturn, named maps and alphabet import. The question this issue asks is the one #95 deliberately did not: is that everything a library author and a large program need, or are there facts about a routine that the language can only state in prose? Like #95 this is an analysis, not a fix — verdicts per line, and a sketch for anything judged worth adding.

The starting evidence is again the standard library's own header, which says of its doc lines: "The ? lines on each entity are its normative contract, including where the head sits on entry and on exit." A normative contract that lives only in prose is the thing to look at first.

Lines of inquiry

1. Head position is part of every stdlib contract and is machine-invisible.

Every std routine documents where the head must be on entry and where it rests on exit ("On entry the head is on the number (any cell up to and including its '$'); on exit it rests on that '$'"). Nothing checks it: not the compiler, not a lint, and not the testing library #30 will become, because the fact has no representation. This is the failure mode of real library use — calling plusOne with the head one cell off — and the footprint engine already walks bodies for writes. Determine what a head clause would have to say to be checkable (entry precondition as a glyph set the head must be on; exit postcondition as a glyph set, or same/moved relative to entry; per tape), whether inference can confirm it the way it confirms writes (the same over-approximation caveat for substitution writes applies), and whether it belongs in the interface section and headers so a caller's footprint can use it.

2. A routine generic over its alphabet.

goToEnd-shaped behaviour depends on the blank and nothing else, yet a routine is typed by one concrete alphabet and reuse over another goes through a map. Index binding already gives de-facto duck typing, but there is no way to declare "this routine needs only the blank and these two symbols; anything else is opaque and passed through". Determine whether an alphabet parameter on a signature (routine r<A>(tape t: A) with a required-glyph constraint) is expressible on top of the composition engine — the callee's rows would be written against required symbols plus a wildcard for the rest — or whether index binding plus the item-4 warning from #95 is the honest limit.

3. Named glyph sets.

'0'..'9' is respelled in every pattern that needs it, in the stdlib and in rpnhex.tmc. A declaration (set digits = { '0'..'9' }) usable in pattern cells, write vectors and contract clauses would name the semantics once. Small; decide whether it earns its keyword, and how it interacts with ranges, as bindings and folds.

4. Trap behaviour as part of the interface.

noreturn states that a routine never executes ret; nothing states whether it can leave by a trap (UnmappedRead/UnmappedWrite/NoTransition). Today that is the compile-time lint state-may-trap, which a library consumer never sees. Determine whether "never traps" (or the set of traps a routine may raise) is a fact worth carrying as a clause and in the interface section, and whether the existing analysis behind state-may-trap can back it.

5. Representations.

"A number in the bare representation" is a convention described in a namespace comment; named maps and alphabet import (from #95) give half of it, the alphabet. The other half — the shape invariant of the tape — may belong to the testing library rather than to types. Settle which, so the question stops recurring.

Method

Not by argument. Three probe programs, each written against the current language plus the #95 design, each either written without friction or stopping at the missing word:

• a library over two representations whose head preconditions are checked rather than documented (line 1);
• one routine generic over its alphabet, used over three different alphabets (line 2);
• decimal arithmetic over a rich alphabet, where named sets are either needed or provably not (line 3).

The probes live under docs/superpowers/ while the analysis runs; whatever survives becomes an example or a stdlib routine.

What a good outcome looks like

A written verdict per line — inherent / worth adding / not worth adding — with the probe that decided it, and for anything judged worth adding, enough of a sketch to become its own issue. Line 1 is the one that changes what a contract is; lines 2–5 mostly need settling.

Docs that bound the current language: docs/tmt/language.md (contract clauses, substitution), docs/tmt/stdlib.md, the ? lines throughout crates/turing-machine/src/stdlib/std.tmc, and the binding-arc spec docs/superpowers/specs/2026-09-13-issue-95-binding-analysis.md for what the language will already have.

[mellonis]

Verdicts (2026-09-13)

Three probe programs, untracked under docs/superpowers/probes/2026-09-13-tmc-completeness/ (probe1-head, probe2-generic, probe3-sets, each with a NOTES.md carrying the exact commands and outputs), decided the five lines. Three of them fold into the #95/#118 arc; the design is in the arc's spec (docs/superpowers/specs/2026-09-13-issue-95-binding-analysis.md, section "Folded in from #121"). This issue closes with that arc.

1. Head position — worth adding, in the arc. The probe reproduced the predicted failure exactly: plusOne entered one cell left of '$' returns |^0011$| for |^1010$| with exit 0, indistinguishable from a correct run; a strict routine entered on a blank traps NoTransition at a bare code address inside the callee. Two clauses per tape parameter, enters { … } and leaves { … }, after writes/preserves (entry is reserved, exit collides with the exit count). Checked twice: statically on the callee — enters must be a subset of what the entry state accepts (enters-not-accepted), leaves where inference is exact (exit rows without a move) — and at runtime in debug builds, as synthesized check states at entry and before every way out that read the real cell after any move and raise a new trap kind #2 = contract, named by routine, tape, clause and glyph. Stripped by a new --strip-asserts (separate from --strip-debugger), which --release includes; manifest profiles gain strip-asserts (tmt.json project 0.2 → 0.3). The sets ride the interface section, .param and .tmh; every stdlib tape gets annotated from its ? lines, which stop being the only carrier of the contract. Static inference alone was rejected: it loses everything after a move and widens through one-way collapse maps (invertNumber's exit would infer as {'_','^','$'}). A static site warning can be added later over the same sets.

2. Alphabet-generic routines — worth adding, small, in the arc. skipRight over {'_','a','b','c','d'} through with map { 'a'->'a', 'b'->'b' } traps UnmappedRead on 'c' under all three mechanisms: a closed map holes the unlisted symbols. The machine already runs the wanted behaviour — a hand-written descriptor with the unlisted symbols mapped to the callee's cardinality passed on today's binary, under mono and frames, because * matches any index and - writes nothing. The language gets the word: * in a map (with map { 'a'->'a', 'b'->'b', * }, with map { * }) makes unlisted symbols opaque — one flag bit on the binding record, the linker stops holing them, no VM or descriptor change. Safety: the compiler infers per tape whether every reading state has a * cell, exports it as the opaque bit (.param … opaque), and the linker refuses an open binding into a tape without it. * as v is already an error, so an opaque symbol can never be copied through a substitution.

3. Named glyph sets — worth adding, in the arc. Decimal plusOne + stripLeadingZeros in 55 lines respell the digit set five times plus two subsets; rpnhex.tmc writes 0..15 22 times. set NAME { … } — literals, ranges, other sets; namespaced, exportable, in .tmh; legal in alphabet bodies, contract clauses and pattern cells (with as); not in write cells, never a tape type; expands before IR. One reserved word. Two rulings that came out of the probe: a range, set member or single glyph outside the tape's alphabet in a pattern or clause is now an error (the silent per-alternative drop and empty-expansion go; the corpus has no partial range), and char-arithmetic is fixed — foldability is decided by the symbol's label being numeric, not by the literal's quotes, since '0' and 0 are one symbol.

4. Trap behaviour as a clause — not worth adding. Only NoTransition is decidable at compile time, and only as "may"; unmapped reads/writes belong to the site's binding, ExitOutOfRange cannot happen with declarative exits. Every stdlib state the lint flags is deliberately partial — omitting the catch-all is the documented way to fault on bad input. With line 1, a NoTransition on bad input is either an enters violation (the assert names it) or a promise the body does not keep (enters-not-accepted). state-may-trap stays opt-in for authors.

5. Representations — nothing in the language; a #30 assertion. What a consumer can get wrong: the alphabet (alphabet import and the #95 link check), the head (enters), and the tape's shape — ^101 with no '$', on which goToEnd walks right forever. Shape is a runtime property of contents, a regular language over the band; a type cannot see it and a runtime check is itself a machine, i.e. a test. #30 gets a shape assertion over glyph labels (num ~ "^\^[01]+\$$") as a first-class observable. build-history.md had no prior ruling; this is the first.

Two side findings recorded for the arc: the compiler already dedups identical graft instances by (graph, composite, continuations) — so #95's 5b needs a hygiene lint, not a feature — and tmt lint reports "tape is never read, written, or moved" on a machine whose only rule is a transparent call, the same missing-interface root cause.