Brummel
eaa52ff64f
Second tranche of the contracts-against-code audit. Two threads, both applied conservatively under the over-correction guards in docs_honesty_pin.rs (the self-labelled tiebreaker in 0008 and the Diverge-reserved anchor in 0010 are deliberate honest content and were left untouched; design rationale that explains a present-state design principle — semantic-locality, the reuse-as-wrapper reasons — was also preserved). Honesty-rule (0007): demote clear change/deletion narration to present tense. - 0008: drop "they were promoted from ... to ... Recorded here so"; strip the "Iter A"/"Iter B" iteration labels (the descriptive titles carry the meaning); drop "(no longer a carve-out)". - 0001: "were rewired to use ... was deleted at the same time" -> present tense. (The substance was already correct: `pretty.rs` holds only the diagnostic helpers; an audit agent had misread the line as "pretty.rs was deleted" — the file exists, the printer code does not.) - 0012: drop "Per the tail-call survey of existing fixtures" and "Migration of existing fixtures is partial" -> present-state description of which corpus fixtures carry the tail marker. Ratifier integrity: a contract that names a test which does not ratify it is itself a form of the dishonesty this ledger forbids. - 0014 named `bench/architect_sweeps.sh`, which sweeps honesty-anchors and ratifies none of the six verification mechanisms; and claim 5 cited `tests/expected/`, which never existed (git log empty). Point claim 5 at the real golden mechanism (`crates/ail/tests/snapshots/` via `ir_snapshot.rs`) and the footer at each mechanism's actual test. - 0015's four constraints are guaranteed by absence (no thunk/`ref`/ `IORef` node, non-recursive `let`); the named uniqueness in-source tests only count RC consumes, never the constraints. State the by-construction guarantee and point the ratifier at `ast.rs` (the single source of truth for which nodes exist). - INDEX ratifying-test column updated for both to match. All ledger pins green (docs_honesty_pin, design_index_pin incl. every_contract_names_a_resolvable_ratifying_test, effect_doc_honesty_pin, carve_out_inventory); architect honesty sweep clean. Deferred, recommend-only: 0016-method-dispatch carries no invariant absent from 0013 (merge candidate), but a contract-file merge touches INDEX, the retired-counter convention, and cross-refs — a structural call left for explicit direction. Minor history phrasing in 0008's Type::Con.name hash-shift paragraph (§"FnDef.suppress") also left.
66 lines
3.1 KiB
Markdown
66 lines
3.1 KiB
Markdown
# Tail calls
|
|
|
|
## Explicit, verified tail calls
|
|
|
|
For an LLM author, recursion is the natural iteration form
|
|
(`\n. if n == 0 then () else loop(n-1)` is what I reach for, not
|
|
a `for`-loop). Without a tail-call guarantee, every recursive
|
|
program has a silent stack-depth ceiling that no compile-time
|
|
diagnostic warns about. That is exactly the class of correctness
|
|
hazard the language exists to eliminate.
|
|
|
|
Solution: explicit, verified tail calls.
|
|
|
|
- **AST.** `Term::App { fn, args, tail: bool }` and
|
|
`Term::Do { op, args, tail: bool }` (see
|
|
[Data model](0002-data-model.md)) gain a `tail` flag,
|
|
serde-defaulting to `false` so existing fixtures load with
|
|
`tail: false` and their hashes stay bit-identical.
|
|
- **Typecheck.** A new pass `verify_tail_positions(fn_body)`
|
|
runs after the main type-check. It walks the body with an
|
|
`is_tail_context: bool` threaded down. The flag is `true` at
|
|
the start and propagates to every sub-term that is the value of
|
|
the whole expression: the body of every `Term::Match` arm, both
|
|
branches of `Term::If`, the right operand of `Term::Seq`, the
|
|
body of `Term::Let` and the in-clause of `Term::LetRec`, and the
|
|
body of `Term::Lam` (each Lam opens its own tail scope); the
|
|
identity nodes `Term::Clone` / `Term::ReuseAs` and a `Term::Loop`
|
|
body propagate the enclosing flag unchanged. The flag is `false`
|
|
for every argument position: args of any
|
|
`App`/`Do`/`Ctor`/`Recur`/`New`, the scrutinee of `Match`, the
|
|
condition of `If`, the left operand of `Seq`, and the value of a
|
|
`Let`/`LetRec` binding. When the walker
|
|
visits an `App { tail: true }` or `Do { tail: true }`, the
|
|
flag must be `true` at that visit; otherwise emit diagnostic
|
|
`tail-call-not-in-tail-position`.
|
|
- **Codegen.** Emit `musttail call` (LLVM IR) for marked calls
|
|
instead of plain `call`. LLVM rejects at IR-verification
|
|
time if the call cannot physically be a tail call (calling
|
|
convention mismatch, signature divergence, etc.). The reject
|
|
surfaces as a hard build error, not a silent runtime
|
|
surprise.
|
|
- **Form (A).** Two new keywords: `tail-app`, `tail-do`.
|
|
Productions are positional analogues of `app`/`do` with
|
|
`tail: true` set on the resulting term. EBNF gains 2 lines;
|
|
total production count goes from ~28 to ~30, still inside
|
|
the constraint-1 budget (see
|
|
[authoring surface](0001-authoring-surface.md)).
|
|
|
|
**What this does NOT promise.** Many recursive calls are *not* in
|
|
tail position because they are arguments to constructor calls (e.g.
|
|
`Cons (f h) (map f t)`). The current pipeline adds annotation + verification;
|
|
it does **not** add a CPS transform or accumulator-form
|
|
rewrite. Programs whose recursion is constructor-blocked
|
|
will continue to be stack-bounded by recursion depth. The
|
|
canonical authoring pattern in such cases is to write the
|
|
accumulator-form variant (`map_acc`, `fold_left`, etc.)
|
|
explicitly. The stdlib ships both forms where
|
|
relevant.
|
|
|
|
In the corpus, only terminal recursions (`print_list`-style)
|
|
carry the tail marker; the constructor-blocked recursions in
|
|
`map`, `sort`, `insert` are unmarked — they cannot benefit from
|
|
`musttail` without a source-level rewrite.
|
|
|
|
Ratified by: `crates/ailang-check/src/lib.rs`.
|