Files

T

Brummel eaa52ff64f docs(contracts): honesty-prose cleanup + ratifier integrity

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.

2026-06-02 11:27:53 +02:00

3.1 KiB

Raw Permalink Blame History

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) 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).

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.

3.1 KiB Raw Permalink Blame History

Tail calls

Explicit, verified tail calls

3.1 KiB

Raw Permalink Blame History