Commit Graph

1014 Commits

Author SHA1 Message Date
Brummel 7fe08139fb experiment(cma): M-expressions tested — middle of the pack; sharpens the finding (refs #68)
Tested McCarthy's head[a; b] notation (user request). Explicit structure
(brackets + semicolons) in the function-call shape LLMs know cold. Result
4-5/8 (model variance over two runs): below plain parens, above bracket-free.

Two watch-out catches kept it honest: (1) a trailing ';' before ']' — a normal
trailing separator Qwen wrote — was rejected by my too-strict parser; fixed to
tolerate it, round-trip preserved (without this M-expr looked unfairly bad).
(2) L4 then failed with 43 '[' vs 42 ']', a genuine Qwen bracket imbalance (not
truncation), the same depth-tracking failure as plain parens.

Why worse than plain parens despite being explicit: swapping () for [] does
nothing for the balance burden, and the semicolons ADD a second consistency
requirement Qwen does not reliably meet.

This sharpens the overall finding across five formats (annotated-parens 7/8 >
plain parens 6/8 > M-expr 4-5/8 > indent 3/8 > YAML 2/8): the discriminator is
not "explicit vs implicit" but REDUNDANT CUE vs EXTRA BURDEN. Depth-annotated
parens carry nesting redundantly so the model can't lose its place (best);
indentation moves tracking to an implicit channel (worst); M-expr semicolons
add bookkeeping on top of bracket balance (middle). Lever for an LLM-authored
language: redundant self-checking structure, not a lighter or more familiar
surface that carries extra bookkeeping. Synthesis in format-findings.md.
2026-06-02 19:11:18 +02:00
Brummel 525112e32e experiment(cma): bracket-free formats tested — they make Qwen WORSE, not better (refs #68)
Tested the user's bracket-free ideas (indent, YAML) against the annotated-paren
result. Hypothesis was that removing the closing token removes the repetition
tail. The opposite held.

Instrument note (the watch-out paid off twice): a real YAML library auto-quotes
and gives *,-,true special meaning, which collides with the AILang operators —
Qwen wrote `- *` (multiply), a YAML alias marker, and the library crashed. That
is a measurement bug, not a model failure. Rebuilt with a hand-written literal
indent parser (atoms verbatim, no quoting); `- *` then round-trips fine.

With the instrument fixed, the result is monotone across four formats:
  format 4 annotated parens 7/8 > plain Form-A parens 6/8 > yamlish indent 3/8
  > YAML library 2/8.
More explicit structure marking helps this model; less hurts. Qwen's weakness
is structure-tracking at depth, and indentation makes it track the nesting
itself — as error-prone as matching parens but without the redundant cue. The
bracket-free surfaces fail EARLIER (L3/L4), before the L7 repetition ceiling is
even reached.

Lever for an LLM-authored language: redundant explicit structure (depth-
annotated brackets), not a lighter surface. Synthesis in format-findings.md;
raw ladders qwen-yaml.md (PyYAML, discarded) and qwen-yamlish.md (own parser).
2026-06-02 18:49:35 +02:00
Brummel 682b935ba3 experiment(cma): annotated-paren format helps Qwen — cracks the bracket wall (refs #68)
Tests the user's hypothesis: if no human reads the surface, lift the paren-
counting burden. Format 4 = annotated parens, every paren carries its nesting
depth. Discipline: the format has no ail parser, so the converter is round-trip
verified (parse-identity on known-good demos) before judging any model output.

Result: it helps. Plain Form-A 6/8 -> format 4 7/8 on the same ablation ladder.
The depth annotation cracks the bracket-balance wall that broke L4. At the
hardest level (L7 SMA) Qwen produced perfectly balanced brackets through the
deepest nesting AND correct SMA logic; the only remaining issue was a construct
quirk (it treats seq as variadic, but AILang seq is binary). Proof the blocks
were right: Qwen's exact logic with a manual binary-seq fix runs and emits the
exact expected SMA output.

Pushing further (format 4 + explicit seq-binary hint) fixed the seq nesting but
L7 still failed on two MODEL-behaviour limits, not encoding: it simplified the
logic, and fell into a closing-token repetition tail (hundreds of #0) ). The
tail is paren-driven, so the natural next test is a bracket-free format
(indent / keyword-delimited) with no closing token to loop on — a deliberate
next step needing its own verified converter. Synthesis in format-findings.md.
2026-06-02 18:30:24 +02:00
Brummel da99ebaba8 experiment(cma): ablation finds WHY Qwen fails at Form-A — two distinct walls (refs #68)
Try-and-error ablation, minimal few-shot context, single shot per level, a
ladder L0 (fn returns 42) to L7 (full SMA). Two ladders: base few-shot that
only destructures, then one that also constructs (term-ctor).

Finding: Qwen is NOT generally incapable. With minimal correct context it
writes 6/8 tasks green, including ADTs, match, recursive fns, and Series use.
The failures are two specific walls:

- Wall 1 (cheap): unfamiliar constructs. It built lists with (app Cons ...) —
  calling the ctor like a function — because it had only seen match, never
  term-ctor. Adding ONE term-ctor example flipped L3 and L5 to green and
  removed the Cons error. The model generalises a construct from one example.

- Wall 2 (hard): paren/nesting discipline at depth. The two that stay red
  (L4, L7) fail purely on bracketing, not knowledge. In L4 the recursive
  function is flawless; main closes a 4x-nested term-ctor value one paren
  early so the let body slides inside it — total paren count is BALANCED
  (43/43), the parens are just misplaced. Green/red tracks nesting depth, not
  feature. Examples do not fix it. This is the same weakness the full-SMA
  probes hit (run 2 had correct logic, died on brackets; run 3's long context
  tipped it into a seq-repetition loop).

Takeaway: the bottleneck is the fully-parenthesised surface at depth, not the
semantics. Natural next test: the .ail.json authoring form, which removes
human paren-counting. Driver qwen_ablation.py; ladders in qwen-ablation-min.md
and qwen-ablation-ctor.md; synthesis in qwen-ablation.md.
2026-06-02 18:09:31 +02:00
Brummel 8b7e683cc9 experiment(cma): SMA probe run 3 — full grammar+spec+lib makes Qwen degenerate (refs #68)
Third run of the SMA authoring probe, this time with Qwen fully equipped: a
distilled complete Form-A construct grammar (with explicit arity/paren rules),
the mini-spec, and the verbatim Series library source. Hypothesis: the formal
grammar clears the bracket failures of runs 1-2. It did the opposite.

With ~80k prompt tokens the model degenerated into an identical pathological
(seq (seq (seq ...))) tower every turn (321 open parens vs 10 close,
byte-identical across all 6 turns, indentation exploding). Doubling max_tokens
to confirm it was not mere truncation produced HTTP 413 (request too large) —
more budget yields an even larger degenerate output, confirming degeneration.

Verdict (n=1 model): Qwen3-Coder-Next wrote no working SMA in any of three
configurations; more reference material made it WORSE, not better (the lean
run 2 got the algorithm right, the fully-equipped run 3 looped); it never
converged from ail-check feedback in any run; all failures are Form-A
bracket-shape errors, never semantics. Driver + raw logs updated.
2026-06-02 17:49:23 +02:00
Brummel 577bb6be43 experiment(cma): SMA authoring probe against Qwen3-Coder-Next (refs #68)
Probe whether a foreign model can write the Series SMA worked example in
AILang Form-A from the mini-spec + Series API alone. Two live runs, neither
reached green, but a clean progression:

- Run 1 (stock API doc): 6 byte-identical turns, blocked on (app new ...) —
  Qwen treats the  term head as an ordinary function.
- Run 2 (new clarified as a term head): clears that; ownership threading
  comes out idiomatically right (nested let s = Series.push s v), but
  S-expression bracketing breaks (push sees 4 args, not 2).

Cross-cutting: Qwen clears a hurdle only with per-quirk guidance and never
converges from the ail check diagnostic (same failure repeated all 6 turns
in both runs); the failures are Form-A bracket-shape errors, not semantic.
n=1 model, single session. Driver: sma_probe.py; raw logs sma-probe-run{1,2}.md.
Live IONOS run, with consent.
2026-06-02 17:31:35 +02:00
Brummel 29625e7262 feat(cma): revive cross-model harness corpus to current language (refs #68)
The cma authoring-form harness corpus had gone dead against the language
as it evolved since May. The plan modelled it as merely schema-dead
(missing param_modes/ret_mode); it was also drift-dead in the example
BODIES. Fixed in place, with `ail check` + both test suites as the oracle:

- Schema: param_modes/ret_mode completed on every fn type; existing
  borrow annotations preserved (data_with_match's borrow over List).
- Symbol drift: `<`/`==` -> `lt`/`eq` (operator-routing); the removed
  `io/print_int` op -> print_str(int_to_str n) followed by a newline
  print, preserving the trailing newline the references' expected_stdout
  needs.
- Ownership/ADT restructures: data_simple's reuse-as now wraps the
  source in a match arm (ctor must be statically visible);
  data_with_match's count_via_letrec + local go switched borrow->own
  (consume-while-borrowed under the tightened ownership analysis;
  head_or_zero still exercises borrow over the boxed List).
- param_modes_all rewritten to own (Int) + borrow over a boxed ADT --
  (borrow Int) is now a borrow-over-value error.
- Two new author-facing examples (loop_sum: Loop/Recur; new_rawbuf: New)
  cover the Term variants that landed since May.
- spec_completeness.rs: drop the deleted ParamMode::Implicit; cover
  Loop/Recur/New; allowlist the non-authorable Term::Intrinsic out.
- spec.md section 4 rewritten to own/borrow (mandatory, no implicit)
  with the borrow-over-value rule; rendered/ regenerated.
- mock_full_run fixture's t3 turn-2 program migrated so the harness
  score assertions hold; usage fields untouched.

Both render/ and harness/ cargo test suites green in mock mode; no live
IONOS call. Run the harness budget/reference tests with AIL_BIN pointing
at target/debug/ail (ail is not on PATH in the test env).
2026-06-02 17:08:30 +02:00
Brummel 72d2d9c806 test: prune duplicate tests, re-sight two blind coverage guards
Follow-up to a fan-out audit of the whole test suite (742 tests, 21
read-only assessors + synthesis). Two clusters of the audit were
actioned here; the #66 hashing-removal cohort it surfaced is left for
the #66 scope, and the RED-first doc-rot sweep is deferred.

§2 — true duplicates removed (each kept test is a strict superset or
identical fixture+assertions of the deleted one):
- ailang-check param_in_reject_message_names_allowed_set (kept the
  _renders_allowed_set_in_ailang_syntax superset)
- ailang-check cross_module_pat_ctor_typedriven_resolves (kept ct2_;
  shared cross_module_ws helper retained, 2 other callers)
- ailang-core mq1_qualified_instancedef_class_accepted (kept ct1_)
- ail e2e bool_to_str_emits_true_branch (kept the rc-stats superset)
- ail loop_recur_str adt-leg guard (the standalone heap pin owns it;
  dropped the dangling header reference too)
- ailang-check over_strict_mode_silent_when_param_is_borrow (its
  assertion is subsumed by explicit_fn_with_no_uses_is_clean; its own
  doc claimed a "borrowing body" the Lit body never provided)

§4 — meta-guards that had gone partially blind re-sighted:
- spec_drift::spec_mentions_every_def_kind now pushes Class/Instance
  exemplars and asserts their `(class `/`(instance` anchors; the
  "wait for 22b.4" exclusion was stale (anchors shipped in e809f45).
- schema_coverage now tracks Term::New (VariantTag + EXPECTED +
  visitor insert); the new_*/raw_buf_* fixtures already exercise it,
  so the "no fixture emits new" exclusion was stale.
- prose doc_wrap_widow_control_skips_when_combined_too_long was
  tautological: its 32/32/42-char words gave combined=75<=80, so
  widow control actually fired. Rebuilt the fixture (short head + two
  40-char words → combined=81>80) so it hits the real skip branch,
  and added the missing "last line stays 1 word" assertion. The
  obvious 2-word fixture does NOT work — it skips via the
  prev_words<2 branch, not the combined-over-budget branch.

ailang-check 124->121, ailang-core 55->54, e2e 102->101,
loop_recur_str 4->3; spec_drift 8 green, schema_coverage green,
prose lib 63 green.
2026-06-02 16:59:43 +02:00
Brummel 426ce88d2a plan: cma-revival.1 cross-model harness corpus revival (refs #68)
Bite-sized plan for spec 0069. Six tasks: complete schema fields across the
13 examples + 4 references (own default, existing borrow preserved); rewrite
param_modes_all + spec.md section 4 (own Int / borrow boxed-ADT, value/boxed
rule); add loop_sum + new_rawbuf examples; spec_completeness variant coverage
+ Intrinsic allowlist; regenerate rendered + green render suite; migrate
mock_full_run fixture + green harness suite.

All verbatim .ail/.ail.json bodies parse-gate verified this session. The gate
caught a real language drift the spec had to absorb: borrow over an unboxed
value type (Int) is now a borrow-over-value error, so param_modes_all borrows
over a boxed ADT instead.
2026-06-02 16:32:31 +02:00
Brummel 74849160b7 spec: cross-model harness corpus revival (refs #68)
The cma authoring-form harness (experiments/2026-05-12-cross-model-authoring)
is milestone-complete but its corpus went schema-dead: the implicit-cutover
made param_modes/ret_mode mandatory, so today's ail check rejects 100% of the
master examples + reference solutions and the renderer crashes on load. This
spec revives the corpus to the current language and gets a mock run green.

Scope (corpus-first, method-form-later per #68): minimal field-completion
preserving existing modes; two new author-facing examples (loop/recur, new);
spec.md section 4 rewritten to own/borrow with the borrow-over-value rule
surfaced under the parse-gate; spec_completeness allowlists the non-authorable
Term::Intrinsic out; mock fixture migrated so harness score assertions hold.
No live IONOS call. Old specs 0017/0018 left intact as closed-milestone
history.
2026-06-02 16:32:31 +02:00
Brummel 54d8f0c660 docs(contracts): record the leak-class branch-param drop gate (#63)
Audit of the #63 leg-3 cycle flagged ledger drift: 0008-memory-model.md
enumerated the Own-param drop gates as a closed set, but the leak-class
branch-param fall-through drop now ships in codegen with no home in the
contract. Per the honesty-rule (a contract describes the actual present
state), reconcile it.

Adds the fourth gate with its three soundness guards — disjointness from
the fn-return dec (partition by aggregate: ==0 vs >=1), no-use-after-free
(the use-after-consume rejection makes an aggregate>=1 param dead past
the construct), and the heap-RC-ADT type precondition (field_drop_call !=
ailang_rc_dec; closure/static-Str/Var params are skipped to avoid a
static-constant underflow). Notes that the pre-tail-call Own-param dec
now shares the per-branch model (gate-source = MArm.consume) and updates
the binder-name-injectivity precondition to cover the per-branch consume
maps carried on MArm / MTerm::If and correlated by the traversal-order
cursor.

The accepted heap-capturing-closure-in-leak-class leak (soundness over
completeness) is recorded in the backlog as Brummel/AILang#67.

refs #63
2026-06-02 15:51:35 +02:00
Brummel d72fe0c2e6 fix(codegen): drop branch-consume-split owned params (#63 leg 3)
The last leg of the #63 drop-soundness cluster: an (own ...) heap param
consumed on one match-arm / if-branch but live on a sibling was never
dropped on the live path, leaking one slab per call. This was the
residual live=2 leak in series_sma that kept the series headline from
being leak-clean.

Root: the per-fn aggregate consume_count (the worst-case max over all
branches from uniqueness::merge_states) was codegen's only consume
signal, and every owned-param drop site gated on it. A param consumed
on SOME branch makes the aggregate >= 1, so every site skipped it —
including the branch where it stays live. match and if share this root
(if is first-class MTerm::If, not desugared to match).

Mechanism (spec 0068):
- CAPTURE: uniqueness retains the per-branch consume snapshots it
  already computes per branch and discarded at the max merge — new
  BranchConsume + infer_module_with_cross_branches (the aggregate-only
  infer_module_with_cross now delegates and drops the channel).
- CARRY: additive MArm.consume / MTerm::If.{then,else}_consume, attached
  by lower_to_mir via a traversal-order cursor (post-order pop, kind- and
  exhaustion-asserts make a desync a loud panic; neutral for const bodies
  which uniqueness does not walk). The AST carries no node id, so the
  correspondence is the structural pre-order both walks share — pinned by
  branch_consume_maps_attach_to_matching_arms.
- GATE: emit_leakclass_branch_param_drops fires a fall-through drop only
  for the leak class (branch_consume==0 AND aggregate>=1), in match arms
  + both if branches; the pre-tail-call dec switches its gate source from
  the aggregate to per-arm. The fn-return dec and arm-close pattern-binder
  dec are UNCHANGED.

Safety:
- Double-free: the drop sites partition by aggregate (==0 -> existing
  fn-return/pre-tail-call; >=1 -> new per-branch). Disjoint, so no param
  is dropped twice — no fn-return disable, no tail-position analysis.
- Use-after-free: the checker rejects use-after-consume, so an
  aggregate>=1 param is provably dead past the construct (path-terminal
  drop, tail position irrelevant).
- Type eligibility (found by the full-suite gate during implement; spec
  0068 refined): the new agg>=1 site is the FIRST drop site that can
  reach a STATIC closure-pair param (a top-level fn ref like inc in
  Either.either, consumed on one arm, live on the other) — a .rodata
  constant with no rc-header. field_drop_call routes Type::Fn / static-Str
  / Type::Var to the bare ailang_rc_dec, which underflowed on it. The
  helper now drops only params with a real per-type heap-ADT drop fn
  (field_drop_call != "ailang_rc_dec"). Sound (no underflow) and
  leak-correct (a static closure/Str allocates nothing). Witnessed green
  by std_either_demo / std_list_demo / poly_rec_capture_demo.

Verification: full workspace suite green (116 binaries); both new leak
pins (if + match) and series_sma_no_leak_pin green at live=0; legs 1/2
pins still green; INTERCEPTS<->(intrinsic) bijection intact; no
Pattern::Lit reject path added.

The leg-3 helper's type precondition was applied inline by the
orchestrator (a narrowing guard clause in an already-reviewed Task-4
helper, full context loaded) after the implement-orchestrator correctly
surfaced the spec gap rather than papering over the regression.

This clears the series_sma leak tail; the series milestone (#61) close
stays a separate deliberate step (its end-to-end milestone fieldtest).

closes #63
2026-06-02 15:47:01 +02:00
Brummel 3447ac8039 plan: branch-consume-split drop soundness (#63 leg 3)
Five-task plan for spec 0068, decomposed RED-first:
1. RED — new if-branch fixture + pin, un-ignore the committed match pin.
2. CAPTURE — retain per-branch consume snapshots in uniqueness (new
   BranchConsume + infer_module_with_cross_branches; old API delegates).
3. CARRY — additive MArm.consume / MTerm::If.{then,else}_consume,
   attached by a traversal-order cursor in lower_to_mir (post-order pop,
   exhaustion assert, neutral for const bodies) + lock-step test.
4. GATE — emit_leakclass_branch_param_drops helper + :823 gate-source
   switch to per-arm; fall-through drops in match arms + if branches.
   Disjoint-by-aggregate from the unchanged fn-return dec.
5. VERIFY — series_sma live=0 pin, full workspace suite, lockspair check.

All inlined code lifted from the live source bodies (uniqueness.rs,
lower_to_mir.rs, match_lower.rs, lib.rs) read this session, not from
memory. The one new surface fixture (if-branch) parse-checks clean; the
correspondence test reuses the existing match fixture via the
lower_to_mir_ty.rs elaborate_fixture/body helpers (verified present).

refs #63
2026-06-02 15:25:58 +02:00
Brummel f7226cfba5 spec: branch-consume-split drop soundness (#63 leg 3)
Design spec for the last open leg of bug #63: an (own ...) heap
param consumed on one branch of a match/if but live on a sibling
branch is never dropped on the live branch, leaking one slab per
call. This is the residual live=2 leak in series_sma that keeps
the series milestone #61 from closing.

The leak is general (match AND if, not Series-specific): the
per-fn aggregate consume_count — the worst-case max over all
branches from uniqueness::merge_states — is codegen's only consume
signal, and every owned-param drop site gates on it. A param
consumed on some branch makes the aggregate >= 1, so every drop
site skips it, including the branch where it stays live.

Approach A (chosen, scope = the whole branch-consume-split class):
retain the per-branch consume snapshots the uniqueness walker
already computes and currently discards at the max merge; carry
them additively on MArm.consume and MTerm::If.{then,else}_consume
(attached by lower_to_mir in structural traversal-order lock-step,
since Term/Match/If/Arm carry no node id); codegen reads them at
the branch drop sites. The check pass stays the sole consume
authority (the mir.3a direction).

Mechanism (refined during planning recon, simpler + provably safe
than the first draft's fn-return-disable): the drop sites PARTITION
by aggregate consume, so the per-branch map only ever ADDS drops
for the leak class and never collides with an existing site:

  - fn-return dec (lib.rs) and arm-close pattern-binder dec: UNCHANGED.
    They keep firing for aggregate == 0 (live on every path).
  - pre-tail-call dec (match_lower.rs): gate source switches from the
    per-fn aggregate to the per-arm map. Identical decision for legs
    1/2 (aggregate 0 => per-arm 0 on every arm); additionally drops a
    param live on this tail-call arm but consumed on a sibling.
  - NEW fall-through drop (match arms + if branches), before the br to
    the join: fires ONLY for the leak class — branch_consume == 0 AND
    aggregate >= 1.

Double-free safety is disjointness by aggregate: the new drop needs
aggregate >= 1, fn-return needs aggregate == 0 — mutually exclusive,
so no fn-return disable and no tail-position analysis are needed.
Use-after-free safety: the checker REJECTS using an owned value
after it was consumed on any branch (use-after-consume), pinned green
by use_after_consume_on_own_param_is_reported and
harden_ownership_heap_double_consume_still_errors — so an aggregate>=1
param is provably never live past the construct, making the per-branch
drop path-terminal regardless of tail position.

grounding-check PASS (all load-bearing assumptions ratified by green
tests / structural fact, incl. the disjointness and use-after-consume
claims). Two RED repros carried: the already-committed ignored match
pin and a new if-branch pin.

refs #63
2026-06-02 15:18:08 +02:00
Brummel d565ed87a3 feat(cli): resolve canonical type-scoped describe form
`ail describe <Type>.<op>` is the canonical form for a type-associated
operation (model 0007 §1), but resolve_describe_name only ever looked
up the left segment as a workspace module, so `Series.push` errored
`no module \`Series\`` even though `series.push` and bare `push`
resolved fine.

The dotted branch now falls through on a module miss: if no module is
named by the left segment, scan the workspace for the `Def::Type` named
by it and resolve `<op>` through that type's home module — returning the
identical `Def` the module-scoped and bare forms return (verified: same
hash d5278789db5f267a for `Series.push` / `series.push`). A literal
module still wins (precedence preserved); the bare-name and
ambiguous-name paths are untouched. The genuinely-unknown-prefix
diagnostic is tightened to `no module or type \`X\` in workspace`, and a
type-found-but-op-missing case reports `no def \`op\` in module \`home\`
(home of type \`Type\`)`.

Fix is CLI-local (crates/ail/src/main.rs); ailang-check untouched (a
direct ws.modules scan sufficed, no env.module_types needed). Full
workspace suite green (738); the RED pin describe_resolves_type_scoped_op
(8d58c83) is now GREEN.

closes #64
2026-06-02 14:17:34 +02:00
Brummel 8d58c8310b test(cli): RED pin for type-scoped describe resolution
`ail describe <Type>.<op>` is the canonical form (model 0007 §1) but
currently errors `no module \`Series\` in workspace` because
resolve_describe_name (crates/ail/src/main.rs) only looks up the left
segment as a MODULE, never as a known TYPE. The module-scoped
`series.push` and bare `push` forms already resolve fine.

RED pin: describe_resolves_type_scoped_op asserts
`ail describe --workspace examples/series_sma.ail Series.push` exits 0
and prints the `series.push` def. Fails today on the exit-0 assertion
(feature absent), not on scaffolding. GREEN side follows.

refs #64
2026-06-02 14:14:08 +02:00
Brummel a35878154b docs(examples): correct rbx_1 ctor-field qualification note
The field-test note on the `Window` ctor claimed that bare
`(con RawBuf (con Float))` in a user ADT ctor field gives a
type-mismatch and that "the only form that checks is the
fully-qualified `raw_buf.RawBuf`". Verified against the current
tool (release at HEAD), that claim is false in every form I could
construct:

- bare `(con RawBuf a)` (type-variable element) in a non-kernel
  module: checks ok
- bare `(con RawBuf (con Float))` (concrete element): checks ok
- a `(new RawBuf ...)` value stored via `term-ctor` into a
  bare-declared field: checks ok
- the full rbx_1 program with the field switched to bare RawBuf:
  checks ok

A ctor field is plain type position, and model 0007 §3
("kernel-module types are accessible bare in type position") already
covers it — the auto-import that makes bare `Series` work at a call
site equally makes bare `RawBuf` resolve in a user ctor field. The
only genuine constraint is that a ctor field carries no mode:
`(own (RawBuf a))` is a surface-parse-error, which model 0007 line
458 already documents.

So there is no qualification asymmetry to add to the ledger; the
ledger is correct as-is. The drift was in this checked-in comment
(a guessed rule recorded as fact), now rewritten to the verified
reality. The qualified spelling is kept in the code as the explicit
form. No ledger change.

closes #65
2026-06-02 14:09:48 +02:00
Brummel a2808a6938 test(codegen): ignored RED pin for match-arm consume-split leak (#63 leg 3)
The third and final identified leg of #63: an owned heap param consumed
on one match arm but live on a sibling fall-through arm is never
dropped, because both codegen drop sites (the fn-return Own-param dec in
lib.rs and the pre-tail-call dec in match_lower.rs) gate on the per-fn
AGGREGATE consume_count. When the param is consumed on one arm
(aggregate >= 1) but live on another, the gate skips the drop on the
live arm too. This is the residual that keeps examples/series_sma.ail at
live=2 after legs 1 and 2.

Series-free minimal repro (a `Box` consumed on the `On` arm, live on the
`Off` fall-through arm; main takes the `Off` path): `live=1` today.

Committed #[ignore]: unlike legs 1 and 2, this is NOT a contained fix.
The per-arm/per-path consume information is destroyed by the worst-case
`max` merge in uniqueness.rs (`merge_states`) before MIR — MArm carries
only {pat, body}, MirDef.consume is the per-fn aggregate — so codegen
has no per-arm liveness to gate a fall-through drop on. Closing it needs
a memory-model change (retain per-arm consume, surface it to codegen,
emit the drop only on the live arm, never at the post-match join or the
consuming arm — a live double-free hazard) and a fresh brainstorm cycle.
The pin is committed ignored so the precise symptom and minimal repro
are durable; un-ignore when the fix ships. The assertion is a correct
symptom pin (live == 0); only the fix mechanism is undecided.

refs #63
2026-06-02 13:59:09 +02:00
Brummel e3a9065aa7 fix(codegen): drop owned values on let/seq-wrapped tail-call arms (#63 leg 2)
After leg 1, a tail call wrapped in a trailing `(let ...)` / `(seq ...)`
still leaked: `arm_body_is_tail_call` matched only a direct
App/Do{tail:true} arm body, so for an MTerm::Let/Seq body the gate was
false and both pre-tail-call drops (the scrutinee-husk shallow-dec and
the leg-1 owned-param dec) were skipped — while lower_term still
descended through the wrapper and emitted the inner call as musttail.

The fix replaces the one-level match with a local recursive
`tail_position_is_tail_call` that peels through a trailing Let-body /
Seq-rhs chain to its tail-position sub-term. This is a contained fix:
the predicate feeds only the two drop-emission gates, never the
musttail-emission decision (which is independent, in lower_term off
App{tail:true}), so widening it restores the drops without changing
which calls are tail calls. The let-bound value's scope-close drop is
gated on `!block_terminated` and stays correctly skipped, so the
forwarded let binding is not double-freed.

Verified: the leg-2 pin goes green (live=0, was live=4); the leg-1 pin
stays green; full `cargo test --workspace` 0 failures, no double-free /
underflow / IR-snapshot delta; lockstep pairs untouched.
examples/series_sma.ail drops from live=8 to live=2 with unchanged
stdout (3.0 / 5.33333 / 5.66667 / 5.33333).

Not yet leak-clean: the residual live=2 is a THIRD, distinct leg — an
(own) heap param consumed on one match arm but live on a sibling
base-case (non-tail fall-through) arm is not dropped there, because the
fn-return Own-param dec gates on the per-fn AGGREGATE consume_count
(>=1 here, from the recursive arm) rather than per-arm liveness. Routed
as its own RED-first bugfix.

refs #63
2026-06-02 13:53:14 +02:00
Brummel 2488d9d345 test(codegen): RED pin for let-wrapped tail-call leak (#63 leg 2)
After the leg-1 fix (68f500c), a tail call wrapped in a trailing
`(let ...)` (or `seq`) still leaks: the arm body is an MTerm::Let, not
a direct App{tail:true}, so `arm_body_is_tail_call` (match_lower.rs
~717) is false and both the scrutinee-husk shallow-dec and the leg-1
owned-param dec are skipped — while lower_term still descends through
the Let body and emits the inner call as musttail. The scrutinee husk
and the non-forwarded owned param each leak one slab per recursion
step.

Series-free minimal repro (a plain `Box` whose replacement is
let-bound before the tail call), asserting live == 0 under
AILANG_RC_STATS=1. RED today: `allocs=6 frees=2 live=4`. This is the
leg that keeps examples/series_sma.ail at live=8 (its canonical
`(let s_new (push …) (seq … (tail-app …)))` body).

The debugger confirmed the fix is contained, not a design fork:
`arm_body_is_tail_call` feeds only the two drop-emission gates, never
the musttail-emission decision (which lives independently in
lower_term off App{tail:true}), so peeling the detection through a
trailing Let/Seq chain ending in a tail call is safe. The let
scope-close drop is gated on `!block_terminated` and so is correctly
skipped, avoiding a double-free of the let binding.

refs #63
2026-06-02 13:46:06 +02:00
Brummel 68f500c4b0 fix(codegen): drop owned params on tail-call-terminated match arms (#63 leg 1)
An owned heap ADT param that a tail-recursive match arm neither
forwards into the tail call nor consumes had no drop site: the
fn-return Own-param dec in lib.rs is gated behind `!block_terminated`
and so fires only on the fall-through `ret` path, while the per-arm
drop in match_lower.rs handled only pattern binders. A
`musttail call`-terminated arm therefore leaked one slab per
recursion step (#63, leg 1).

match_lower.rs now emits a pre-tail-call Own-param dec, gated exactly
like the fn-return path: Rc strategy, `arm_body_is_tail_call`,
ParamMode::Own, ptr-typed, and uniqueness `consume_count == 0`. For an
Own param consume_count==0 also implies "not forwarded into the tail
call" — a forwarded Own arg is walked Position::Consume and carries
consume_count>=1 — so the gate cannot drop a param the callee took
ownership of. The drop routes through the same per-type /
partial-drop machinery (honouring moved_slots) as the fn-return path.

The match scrutinee param is explicitly skipped: its ownership is
already discharged by the pre-tail-call scrutinee-husk shallow-dec
plus the moved-out field binders, so dropping it here would dec the
same outer cell twice (a double-handling the first cut of this fix
introduced and the quality review caught — the pin read live=0 but
the IR showed two decs on the scrutinee cell).

Verified: the committed RED pin is green (live=0, allocs==frees);
full `cargo test --workspace` 0 failures; the fix introduces no
under-free (loop_recur_heap_binder / loop_recur_str_binder /
loop_str_recur_literal / rc_pin_recurse_implicit /
lit_pat_ctor_tail_drop all stay live=0, no underflow to depth 5).
No INTERCEPTS/(intrinsic) or pre_desugar_validation change; no IR
snapshot refresh needed.

Leg 1 only. Leg 2 — a `let`/`seq`-wrapped tail call makes the arm
body an MTerm::Let so `arm_body_is_tail_call` is false, skipping both
the husk-dec and this new param-dec — still leaks (examples/series_sma.ail
stays live=8). It gets its own RED pin and fix next.

refs #63
2026-06-02 13:41:57 +02:00
Brummel 1be6e49b4f test(codegen): RED pin for owned-param leak in tail-recursion (#63)
An owned heap ADT param threaded through a tail-recursive fn whose
base-case arm neither forwards nor consumes it is never RC-dec'd, so
it leaks one slab per recursion step. Series-free minimal repro
(a plain `Box` ADT, no Series/RawBuf), so the pin guards the GENERAL
memory-model invariant rather than the Series surface that first
surfaced it (examples/series_sma.ail, live=8).

The pin builds the fixture with --alloc=rc, runs it under
AILANG_RC_STATS=1, and asserts live == 0 (allocs == frees). RED today:
`allocs=6 frees=4 live=2`. The fixture passes the replacement ctor
directly into the tail call (not let-bound) to isolate leg 1 — the
owned-param drop omission — from the second, distinct leg the
debugger found (a `let`-wrapped tail call also defeats the
scrutinee-husk shallow-dec gate; that leg is what pushes box_ctrl to
live=4 and series_sma to live=8, and gets its own pin once leg 1 is
green).

Cause (debugger, for the GREEN side): the fn-return Own-param dec in
crates/ailang-codegen/src/lib.rs (~1444) is gated behind
`!block_terminated`, so it fires only on the fall-through ret path;
crates/ailang-codegen/src/match_lower.rs (~805) drops only pattern
binders, never the fn's owned params. A tail-call-terminated match arm
thus has no drop site for an owned param with consume_count==0 that is
not forwarded into the tail call.

refs #63
2026-06-02 13:31:54 +02:00
Brummel 3b3c8c4f07 fieldtest(series-step1): 5 examples, 5 findings (1 bug, 1 friction, 1 spec-gap)
Post-ship field test of the shipped `series` library extension as a
downstream Form-A author working from the public surface only. Five
fixtures under examples/fieldtest/ across the construction/auto-import,
ring-buffer/financial-indexing, len/total_count bookkeeping, param-in
error-quality, and operator-naming axes; spec at
docs/specs/0067-fieldtest-series-step1.md.

Wins (carry-on): auto-import works with no `(import series)`; the
financial index (0 = newest) maps directly onto the bounded-buffer
mental model and stays correct after multiple wraps; the param-in
diagnostic for a disallowed element type names the type, the
type-variable, the qualified type, and the allowed set.

Findings routed:
- [bug] An owned ADT threaded through tail-recursion whose base case
  neither returns nor consumes it is never dropped — a general
  drop-soundness leak (a plain `Box` control with no Series/RawBuf
  also leaks). Series surfaces it heavily on the whitepaper's headline
  streaming pattern, and the committed reference examples/series_sma.ail
  itself leaks (live=8). Minimal repro: series-step1_5 (live=4).
- [friction] `ail describe ... Series.push` (the canonical type-scoped
  form) reports module-not-found; only `series.push` / bare `push`
  resolve, and no command lists a type's op set.
- [spec_gap] referencing a kernel base type (`RawBuf`) from a user ADT
  ctor field requires full qualification (`raw_buf.RawBuf`) while bare
  `Series` works in type-position via auto-import — the asymmetry is
  undocumented.

The fixtures that leak still produce correct output; the leak is a
separate observable under AILANG_RC_STATS and an orthogonal,
pre-existing bug, not a Series defect.

refs #61
2026-06-02 13:22:30 +02:00
Brummel 73fbb240be docs(model): reconcile 0007 Series with the shipped step-1 reality
The `series` library extension shipped (35a9bc6); model 0007's
Series section was an aspirational sketch with systematic defects
that no longer match the live tool. Bring it to present-state per
the honesty-rule:

- STATUS: the library-extension milestone now reads step-1 shipped
  (primitive Series over {Int, Float}, Bool deferred), with SoA
  step-2 (#62) still pending. INDEX.md row updated to match.
- The `series` code listing is replaced with the shipped source
  (crates/ailang-kernel/src/series/source.ail, doc-strings elided),
  cited as the source of truth. Every defect the sketch carried is
  corrected in the shipped form it now shows: param-in (a Int Float)
  not (... Bool); `(new RawBuf lookback)` with no type-arg; bare `a`
  for the element type variable (not `(con a)`); forall-bound op
  signatures; `lt` not `<`; and the at-index formula with the
  correct sign on i — which already matched the section's own prose
  (`head - 1 - i + 2*lookback`), so the sketch was internally
  inconsistent and the prose was right.
- The SMA worked example uses `ge` (not the non-existent `>=`) and
  emits each average followed by a newline, matching the committed
  pin fixture so the doc and the test agree.
- The "four constructs not in today's AILang" framing is now
  present-state: the mechanisms shipped via raw_buf, Series itself
  via the step-1 library extension.

Both edited module blocks parse against the live tool.

refs #61
2026-06-02 13:12:01 +02:00
Brummel 35a9bc67b1 feat(series): ship the kernel-tier Series library extension (#61)
Series a is a bounded ring buffer with financial-style indexing
(index 0 = newest), shipped as a PURE AILang library extension over
RawBuf — zero Rust codegen, zero intercepts, zero (intrinsic)
markers. It is the first kernel-tier module that depends on another
kernel-tier module (raw_buf). This turns the committed SMA headline
pin (6b7ee45) green and closes the step-1 scope of #61.

The module lives at crates/ailang-kernel/src/series/{source.ail,
mod.rs} and is auto-injected by the loader exactly like raw_buf
(parse_series + injection in ailang-surface/src/loader.rs, re-export
in lib.rs). Five real-bodied ops: new / push / at / len /
total_count, all built on RawBuf.{new,set,get}.

The source is the model-0007 sketch with every defect corrected and
each correction verified against the live tool:
- param-in narrowed to (a Int Float); Bool deferred per #61.
- inner alloc is `(new RawBuf lookback)` with no element type-arg —
  the element is solved from the `(con RawBuf a)` ctor-field context,
  which the base-tier mono fix (b11a6d9) carries through to the
  caller's concrete type. This is the capability that lets Series be
  pure AILang.
- element-typed params/rets are bare `a`, not `(con a)` (a type
  variable, not a nullary ctor).
- op signatures bind `a` via `(forall (vars a) ...)`.
- comparison uses the named helper `lt`, not the non-existent `<`.
- the at-index formula is `(head - 1 - i + 2*lookback) mod lookback`
  (0007 had the sign on i wrong, walking the wrong direction).

Cross-kernel-module visibility — the flagged risk — needed ZERO
mechanism change: the loader derives its implicit-import set from
every kernel module, so series's body resolves `RawBuf.*` and
`(con RawBuf a)` via the existing kernel auto-visibility.

Both CLAUDE.md lockstep pairs stay intact:
- INTERCEPTS <-> (intrinsic) markers: unchanged. Series is
  pure-AILang, adds neither; intercepts_bijection_with_intrinsic_
  markers still green.
- Term::New typecheck/reject <-> pre_desugar_validation.rs:
  untouched; the new/Series construction exercises existing paths.

Test-surface ripple, all verified:
- workspace module-count pins 4 -> 5 (e2e.rs, workspace_pin.rs),
  with a `series` membership assertion added — the kernel set grew
  by one deliberate module.
- two mono-identity tests (typeclass_22b3.rs) now skip `prelude`
  and `series`: series is the first auto-imported real-bodied
  consumer of the prelude polyfns `lt`/`compare` over Int, so mono
  legitimately materialises `lt__Int`/`compare__Int` into prelude
  for every workspace. That is a concrete call site, not gratuitous
  mutation; the tests' real invariant (mono leaves work-free modules
  untouched) still holds for every other module.
- five IR snapshots refreshed; the deltas are strictly additive
  (zero IR deletions) — the same series-driven Int specialisations.

Verified: full `cargo test --workspace` green; SMA binary built via
`ail build --alloc=rc` prints `3.0 / 5.33333 / 5.66667 / 5.33333`.

refs #61
2026-06-02 13:09:17 +02:00
Brummel 6b7ee45e49 test(series): RED pin for the SMA worked example (#61 headline)
The headline acceptance of #61: the simple-moving-average worked
example from design/models/0007-kernel-extensions.md must build via
`ail build --alloc=rc`, run, and print the correct moving averages.
Green ⇒ the kernel-tier `Series` library extension works end to end
(ring-buffer push, financial-style indexing at index 0 = newest,
count/total bookkeeping).

The fixture is the 0007 worked example with two corrections applied,
both verified against the live tool this session:

- `>=` is not a surface symbol; the polymorphic Ord helper is `ge`
  (here on Int operands: total_count vs window size).
- `print` on Float emits no trailing newline, so the four averages
  would concatenate into an unreadable blob. The emit branch now
  prints the average followed by `io/print_str "\n"`, so each
  average lands on its own line and the output is deterministic and
  assertable. (This legibility fix is also queued to be carried back
  into model 0007.)

RED reason (right-for-the-right-reason): `ail check` rejects with
[bare-cross-module-type-ref] on `Series` — the kernel-tier module
does not exist yet. The fixture itself parses and is otherwise valid.

Expected stdout was derived by probing the live %g float formatter
independently (the SMA averages are 9/3, 16/3, 17/3, 16/3 over the
stream 1,5,3,8,6,2 with window 3): `3.0\n5.33333\n5.66667\n5.33333`.

GREEN side (the `series` kernel module + the five ops) is the next
mini-mode iteration.
2026-06-02 12:59:34 +02:00
Brummel b11a6d9883 fix(mono): thread declared return type into mono synth re-entry
GREEN for the series-step-1 base-tier RED (e035eff). A polymorphic fn
that allocates `(new RawBuf n)` with no explicit type-arg — element var
solved purely from the enclosing ctor-field type `(con RawBuf a)` —
checked clean but failed `ail build --alloc=rc` with the unregistered
`RawBuf_new__Unit`.

Root cause (verified, and it diverges from the handoff's diagnosis
pointer): the no-type-arg `(new RawBuf n)` desugars to an ordinary
`(app RawBuf.new n)` free-fn call, NOT a surviving `Term::New` — so the
`lower_to_mir.rs:501 elem: None` site the pointer named is never reached
for this case. The real gap is in mono's synth re-entry.
`RawBuf.new : forall a. (Int) -> RawBuf a` has a result-only forall var
`a` that no argument pins. `collect_mono_targets` and
`collect_residuals_ordered` re-`synth` the body but never unified the
synthesised body type against the declared return type, so `a`'s metavar
stayed unbound through the walk and the free-fn arm Unit-defaulted it.
This is the typed-MIR re-synth strictness family again: a mono synth
re-entry that did not replicate a step `check_fn` performs.

Fix (one file, mono.rs): both re-entries now call a shared
`unify_body_against_declared_ret` that mirrors `check_fn`'s closing
`unify(&ret_ty, &body_ty, …)` (lib.rs:2498), threading the return-type
solution into the same `subst` the FreeFnCall metas read. For
`mk : (Int) -> Box Float` this pins `a := Float` from the ctor-field
context `(con RawBuf a)`, so the buffer specialises to the registered
`RawBuf_new__Float`. Safe by construction: mono runs on already-checked
code, so this unify can only re-derive the solution check already
proved — it cannot introduce a new failure. The shared helper keeps the
two passes resolving identical `type_args`, so the minted symbol matches
the Phase-3 rewrite target.

Verification: full `cargo test --workspace` green (0 failed across all
suites); new pin green; `intercepts_bijection_with_intrinsic_markers`
green (no intercept/marker change — `RawBuf_new__Float` already
registered); `pre_desugar_validation.rs` untouched. Both CLAUDE.md
lockstep pairs intact. End-to-end: a polymorphic `Series a` over RawBuf
now builds and runs with the model-0007 `(new Series (con Float) n)`
caller surface — the precondition for Series as a pure library
extension.

refs #61
2026-06-02 12:44:51 +02:00
Brummel e035eff8df test(series): RED pin for polymorphic RawBuf element-var forwarding
Base-tier enabling RED for the `series` milestone step 1 (#61). A
polymorphic fn that allocates `(new RawBuf n)` with no explicit
type-arg — element var solved purely from the enclosing ctor-field
type `(con RawBuf a)`, never from a value argument — checks clean but
fails `ail build --alloc=rc`: mono drops the check-phase solution for
`a`, defaults it to Unit, and codegen mints the unregistered
`RawBuf_new__Unit`. The fixture reads the element back via `RawBuf.get`
so a wrong specialisation is observable (the program must print the
stored `1.0`).

This is the precondition the user picked (option B) so Series can ship
as a pure AILang library extension over RawBuf while keeping the
model-0007 `(new Series (con Float) 3)` caller surface. The #51 fix
carried a WRITTEN `(con Int)` type-arg through mono; the
variable-via-expected-type case is the untouched gap.

RED: `ail check` exits 0; `ail build --alloc=rc` aborts with
`RawBuf_new__Unit has no registered intercept`. GREEN target: builds,
runs, prints `1.0`. The mono fix must not break the INTERCEPTS↔
(intrinsic) bijection or the Term::New↔pre_desugar_validation lockstep.

refs #61
2026-06-02 12:36:01 +02:00
Brummel c747cdf932 docs(ledger): fix two coherence gaps surfaced by the project skim
A read-only coherence skim across the project (the contract edits
themselves verified code-true, INDEX bijection exact, all pins green)
surfaced two pre-existing drifts — both predating this audit, neither
from the contract pass. Fixed in the same conservative style.

1. Model 0008 (ownership-totality) §1+§2 narrated the `Implicit`
   leak in the PRESENT tense, contradicting the file's own STATUS
   header (Implicit deleted via #55, 76b21c0), contract 0008 ("There
   is no `Implicit`"), and the live fixture. §1 claimed "This is
   documented intentional behaviour today ... the fixture asserts
   `live = 1`"; the `rc_let_implicit_returning_app.ail` fixture now
   asserts `live = 0` (its own comment marks the `live = 1` lane as
   "Pre-0062"). §2 claimed "the typechecker already treats
   `Implicit ≡ Own` (`ParamMode::mode_eq`)"; that variant and fn no
   longer exist. Rewrote both to past tense (the leak the cutover
   fixed). The STATUS header had been updated at cutover; these two
   bodies had not. The design argument (§2-§8) is untouched — the
   header frames it as the whitepaper's reasoning and points readers
   to the contract for current state.

2. Contract 0010 (scope-boundaries) referenced 18 example fixtures as
   `examples/*.ail.json` — files that exist only as `.ail` since the
   form-A-default migration (JSON is derived in-process; only the
   twelve carve-outs remain `.ail.json` on disk). All 18 → `.ail`
   (every target verified present). Same single stale file-path ref in
   model 0001 §3 (`list_map_poly`) corrected; model 0001's other two
   `.ail.json` mentions are intentional references to the canonical
   JSON *form* (the whitepaper's subject) and were left.

Honesty sweep clean; design_index_pin / docs_honesty_pin /
effect_doc_honesty_pin green; no dangling example path remains.
2026-06-02 11:57:51 +02:00
Brummel 4ec8f90b19 docs(contracts): finish the honesty pass (0003, 0008, 0013, 0017)
Third tranche, completing the honesty-rule sweep across the remaining
contracts. Same conservative bar: cut unbacked-verification claims,
change/deletion history, and forward-intent; keep present-state design
rationale.

- 0003: drop "sanitiser-verified" — no TSan/sanitiser test exists in
  the tree, so the claim asserts a verification that does not happen.
  The data-race-freedom property (argued from the non-atomic-but-never-
  shared hot path + atomic-relaxed shared counter) stays.
- 0008: the `Type::Con.name` hash paragraph ("the tightening shifted
  the hashes ... The new pins ... re-asserts the pre-tightening hashes")
  -> present-state: which fixtures carry which hash shape and which test
  pins each.
- 0013: drop "the former codegen-side fallback (at ..., and the
  now-deleted `synth_with_extras`) is retracted" (deletion history; the
  present fact is that codegen does not re-resolve, per the boundary);
  "A future refactor that loosens any one of the four breaks ..." ->
  present-tense statement that the four are load-bearing and each pinned.
- 0017: drop "a real cost surfaced by the `bench_closure_chain`
  regression at the operator-routing-eq-ord milestone" (history) and
  "the symmetric extensions are mechanical when the first such workload
  appears" (forward-intent); keep the present-state allocation cost, the
  pin, and the Int-only-asymmetry rationale.

All 18 contracts now reviewed against the code. Ledger pins green;
honesty sweep clean.
2026-06-02 11:30:46 +02:00
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
Brummel 56e076b2ca docs(contracts): make 0012 tail-context list code-exhaustive
The §Typecheck enumeration in 0012-tail-calls.md presented the
tail-position rule as exhaustive ("The flag is `false` for: ...") but
omitted `Term::If` entirely — even though `verify_tail_positions`
propagates `is_tail` into both `If` branches (ailang-check/src/lib.rs),
and 0012's own motivating example (`if n == 0 then () else loop(n-1)`)
relies on the `else` branch being a tail position.

Restate the rule by principle (a sub-term is in tail position iff it is
the value of the whole expression) and enumerate the actual checker's
arms: `If` branches, `Match` arms, `Seq` right, `Let`/`LetRec`
in-clause, `Lam` body, and the identity/`Loop` propagators; every
argument position (incl. `If` condition, `Recur`/`New` args) is
non-tail. Matches the present `verify_tail_positions` walker.
2026-06-02 11:16:49 +02:00
Brummel 625fe849be docs(contracts): reconcile contracts + honesty-pin with shipped reality
First tranche of a contracts-against-code audit (the inverse of the
usual direction: testing the ledger's claims against the code). Each
fix here is a verified factual divergence between a contract and the
code; the direction of the fix follows which side actually drifted.

Code drifted from the stated goal -> fix the code:

- 0014's claim 6 ("`cargo doc --no-deps` runs warning-free") was the
  design goal; reality had 6 warnings. Demote the offending intra-doc
  links to plain code spans so the docs match the goal:
  - ailang-core: `[`load_workspace`]` cannot resolve from core (the
    fn lives in ailang-surface, which core may not depend on) — three
    sites in workspace.rs.
  - ailang-check: three public-item docs linked the `pub(crate)`
    helpers `qualify_local_types` / `qualify_workspace_types`.
  `cargo doc --no-deps --workspace` is now warning-free.

Contract stale, code legitimately advanced -> fix the contract:

- 0011 stated `float_to_str` "codegen is reserved and not yet
  shipped". It is shipped: lowers to `@ailang_float_to_str(double)`,
  green under the codegen `float_to_str_no_longer_errors_internal`
  unit test and the e2e `float_to_str_smoke`. The docs_honesty_pin
  anchor that protected the stale "reserved" wording moved in lockstep
  to assert the present-tense lowering instead — the pin had been
  guarding a claim the code already falsified.
- 0013 named the diagnostic `ConstraintReferencesUnboundTypeVar`; the
  variant is `UnboundConstraintTypeVar` (workspace.rs), and its scope
  is a class-method signature whose constraint mentions a tyvar bound
  neither by the method's `forall` nor by the class `param`.
- 0017 called the primitive Eq/Ord bodies "placeholder lambdas"; they
  carry the `(intrinsic)` marker — the lockstep partner to the
  INTERCEPTS registry, not a placeholder.
- 0009 said "seven" `.ail.json` carve-outs and described the inventory
  test as pinning seven; the test pins twelve (7 subject-matter + 4
  recur + 1 loop-binder, per carve_out_inventory.rs).

Verified separately: 0001's "pretty-printer code in pretty.rs was
deleted, leaving only diagnostic helpers" is factually correct (an
audit agent misread it as "pretty.rs was deleted"); its only issue is
history phrasing, deferred to the honesty-prose tranche.

Deferred to later tranches: honesty-rule prose (history/rationale that
is not a protected honest-reserved/tiebreaker anchor), stale/mislinked
ratifying-tests (0014's `architect_sweeps.sh`, 0015's uniqueness
in-source tests), 0014's never-existent `tests/expected/`, 0012's
non-exhaustive tail-context list, and the 0016<->0013 redundancy.
2026-06-02 11:14:01 +02:00
Brummel 69e738d6e6 docs(design): close the sma_demo module paren in models/0007 (refs #7)
Verifying the previous commit's surface-syntax fix with `ail parse`
(the whitepaper's code blocks are unfenced/untagged, so no spec
validation ever parsed them) surfaced a fourth, pre-existing drift the
line-by-line signature fix had missed: the §sma_demo `(module …)` was
short one closing paren and never balanced — it could not have parsed
as written, independent of the mode/con-wrapper drift. Added the
missing `)`.

With it, both worked-example modules now parse clean:
- §sma_demo  → `ail parse` ok (4.4 KB JSON)
- §series    → `ail parse` ok

`ail parse` resolves no names, so this verifies surface syntax only,
which is the intended scope. The §series listing still leans on
kernel-tier polymorphism that `ail check` rejects today; its full
compile-verification stays with the pending Series milestone per
spec 0059, exactly as the prior commit stated.
2026-06-02 11:12:22 +02:00
Brummel 5e5b0e1484 docs(design): bring models/0007 worked examples onto the shipped surface (refs #7)
The raw-buf milestone fieldtest (spec 0066) surfaced a spec_gap: the
kernel-extensions whitepaper teaches RawBuf surface syntax through its
§Series worked examples, but those examples were written before three
downstream surface decisions landed and never caught up — so an LLM
author who pattern-matches them writes programs that fail to parse.
Three drift classes, all verified against the HEAD parser:

- fn-type slots carried no mode. Post-#55 every value slot needs an
  explicit `(own …)` / `(borrow …)` (the bare_slot_reject contract).
- `(new RawBuf lookback)` omitted the element type. Post-#51 the form
  is `(new RawBuf (con T) <size>)`; the whitepaper's own spec line
  (§"allocates") already documents `(new RawBuf (con T) (size: Int))`.
- parametrised kernel types were spelled bare `(Series a)` /
  `(Series (con Float))`, contradicting the whitepaper's OWN prose
  (`(con Series (con Float))` at the §mechanisms section). Wrapped in
  `(con …)` to match the documented canonical form.
- `len` / `total_count` carried no `(type …)` at all; completed from
  the obvious neighbour signatures (`borrow (con Series a) → own Int`).

Scope is deliberately surface-syntax only. The §Series listing stays a
forward-looking sketch of the still-pending library-extension milestone
(STATUS header; "not in today's AILang" at the sma_demo block). Its
full cross-module compile-verification remains assigned to the Series
milestone per spec 0059 — these edits do not claim it compiles today
(it leans on kernel-tier polymorphism that is not yet authorable), only
that its surface syntax now matches what RawBuf authors must actually
write.
2026-06-02 10:56:01 +02:00
Brummel 9545257333 fieldtest: raw-buf milestone — 4 examples, 3 findings (refs #7)
Milestone-close fieldtest for the raw-buf milestone, milestone-scope
variant: four end-to-end scenarios derived top-down from the milestone
promise (construct via (new RawBuf <elem> <size>), fill/read via
set/get, size-only buffers, element variety across {Int,Float,Bool},
forbidden-element reject at check, buffer threading under own/borrow).

Result confirms the milestone-promise hypothesis — RawBuf is clean
end to end, zero bugs:
- mrb_1 Int fill/read loop: check ok, run + native build both print 70
- mrb_2 Float own->own threading + borrow read: prints 3.5
- mrb_3 size-only Bool buffer (#51 legitimate-but-unobserved case): prints 8
- mrb_4 Unit element: rejected at check with a precise
  param-not-in-restricted-set diagnostic; build stops at the same
  error, codegen never reached (the #51 fix)

Two [working] findings (carry-on) and one [spec_gap]: the
kernel-extensions whitepaper (design/models/0007) teaches bare-mode
fn-type slots that the post-#55 parser rejects. Verified and triaged
separately; the ledger fix follows in its own commit.
2026-06-02 10:46:16 +02:00
Brummel 2ca483dbfd docs(design): reconcile models 0008/0009 STATUS with the shipped #55 cutover
The 0008 totality core shipped via #55 (spec 0062, 76b21c0), but both
model whitepapers still claimed "nothing here is shipped" — drift the
architect would flag.

- 0008: STATUS now "partially realised". Records what landed (binary
  ParamMode, value-type trivial-own, no mode-polymorphism, the hash
  reset) and points at the contract ledger for current-state facts.
  Marks §3.4/Q3 naming as resolved (verbal own/borrow kept, user
  decision); leaves the return-side escape axis (§5.1-5.2), multi-return
  (§5.3), and Q2/Q4 as the genuine remainder. escape.rs is named as the
  opt-only stack-promotion pass, not the §5.2 reachability check.
- 0009: STATUS stays "nothing shipped" (true), but the runtime-axis-dual
  paragraph now notes 0008's annotation axis landed, so 0009's
  precondition is met rather than hypothetical; the §8-Q3 coupling to
  0008's unshipped return-escape pass is flagged as still ahead.

Contract 0008-memory-model.md needed no change — already current.
2026-06-02 10:12:30 +02:00
Brummel d8d148224c refactor(test): slice the bytes, not the str (sliced_string_as_bytes)
`line[..s].as_bytes()` re-walks UTF-8 boundaries to slice the &str
first; `&line.as_bytes()[..s]` slices the byte view directly. `s` is a
byte offset from `str::find`, so the two are equivalent here. Clears
the last clippy warning in the workspace.
2026-06-02 02:35:17 +02:00
Brummel 1be2c1f145 docs: fix doc_lazy_continuation across the workspace
Eighteen markdown list items in module- and item-doc comments had
continuation lines that were not indented to align under the item
text, so rustdoc rendered them as separate paragraphs and broke the
list. Corrected the indentation (and, at two sites where a general
wrap-up sentence followed a sublist, separated it with a blank doc
line so it does not mis-attach to the last item). Doc whitespace only;
no prose reworded, no code changed.

Workspace clippy is now warning-clean.
2026-06-02 02:34:40 +02:00
Brummel b5799640f8 refactor(core): demote orphaned doc comments in the workspace test module
Two `///` blocks in the in-source test module described tests that were
relocated to tests/workspace_pin.rs, leaving doc comments attached to
nothing (clippy: empty-lines-after-doc). Converted them to plain `//`
notes, matching the already-`//` relocation marker next to them.
2026-06-02 02:30:08 +02:00
Brummel 5cd2a964e3 refactor(surface): collapse the optional-clause duplicate-check onto set_once
Every definition parser repeated the same triplet per optional
attribute — `if slot.is_some() { return duplicate_clause_err(...) }
slot = Some(parse_X()?)`. Factor the check-then-assign into one
helper, set_once(slot, production, subject, clause, value), invoked as
`set_once(&mut doc, prod, subj, "doc", self.parse_doc()?)?`. The match
on peek_head_ident() and the per-clause production/subject/clause
arguments are unchanged, so every duplicate-clause error string stays
byte-identical (the *_rejects_duplicate_*_clause tests pin them).

The helper checks is_some() before the parser runs, so a duplicate
clause still reports at the offending clause's position. Arms that do
more than a plain check+assign (the bool flags drop-iterative/kernel,
the param-in nested map, the suppress/method Vec pushes) are left
inline.
2026-06-02 02:29:10 +02:00
Brummel 72503c40fe refactor(cli): collapse duplicated handler helpers in main.rs
CLI contract (stdout/stderr/exit codes/JSON field order) unchanged —
the e2e diff/manifest/describe cases plus the staticlib/emit-ir/
roundtrip CLI tests are green.

- locate_bump_runtime / locate_rc_runtime / locate_str_runtime were
  three copies of the same upward runtime/<file> walk; folded into
  locate_runtime_file(filename, err_msg) with each error string passed
  through verbatim.
- describe built the same single-def Module wrapper in both branches;
  hoisted into wrap_single_def.
- manifest built the same per-symbol JSON object in two branches
  (workspace adds a leading "module" field); hoisted into
  manifest_def_json(def, Option<module>), field insertion order
  preserved (serde_json preserve_order).

Left duplicated by design: the build_to/build_staticlib elaborate-or-
exit blocks (a shared helper would have to name a MIR type from a crate
ail does not depend on) and the Diff handler's two-report branches (a
generic output router was out of scope and no cleaner).
2026-06-02 02:24:34 +02:00
Brummel 10da23304e refactor(prose): fold the five copies of effects-clause rendering into one helper
The " with <e1>, <e2>" effects clause was rendered by five verbatim
blocks across the fn / class-method / instance-method / type writers.
Hoisted into write_effects_clause(out, effects); all five sites now
call it. Output is byte-identical — the snapshot/round-trip tests
confirm no drift.

The two forall<...> blocks were left alone: they diverge in the
trailing token (one ends `>`, the other `> ` before a where-clause),
so a shared helper would be awkward rather than cleaner.
2026-06-02 02:19:35 +02:00
Brummel 9b0eb58cd9 refactor(surface): share the copy-pasted parser sub-productions
Round-trip-preserving — the byte-isomorphic Form-A ↔ JSON-AST tests,
the hash pins, and the full fixture-corpus parse are all green; error
strings passed through verbatim, not homogenised.

- The Int/Float/Str/true/false literal-token match was inlined in three
  parsers; extracted try_parse_literal_token and routed parse_pat_lit
  and the parse_term fallthrough through it.
- parse_doc and parse_export were identical but for the keyword; both
  now go through one parse_string_attr, and the previously
  doc/export-bypassed expect_string helper is back on the shared path.
- parse_effects_clause and parse_forall_constraints_clause shared the
  expect-keyword / collect / reject-empty / expect-rparen shape;
  unified under parse_repeating_clause, with each clause's empty-error
  message passed in.

parse_intrinsic_attr was left inline-able-but-not-inlined: it has two
call sites, so inlining would re-duplicate a documented helper.
2026-06-02 02:17:51 +02:00
Brummel e5534d1532 refactor: clear clippy code lints across the workspace
Machine-applicable clippy fixes plus three by-hand cleanups; all
semantics-preserving (full workspace test suite green).

Auto-applied (cargo clippy --fix):
- dropped `.clone()` on the Copy type ParamMode (ret_mode/param_mode)
- map_or(false, p) -> is_some_and(p)
- removed redundant closures and an explicit .into_iter()
- useless format!, a needless deref, an as_bytes-after-slice

By hand:
- ailang-codegen: named the loop-frame tuple types (LoopFrame /
  LoopBinderSlot) instead of the bare nested
  Vec<(String, Vec<(String, String, String, Type)>)>, clearing the
  type-complexity lint and documenting what each slot holds.
- ailang-check: collapsed the two identical pass-through arms of the
  Type-Con qualifier (already-dotted / primitive) into one `||` guard.
- ailang-core: converted a stale `///` block (it described a test that
  was relocated, documenting nothing) back to a plain `//` comment.

Remaining clippy output is 16 markdown list-indentation nits in prose
doc comments — doc formatting, not code, left for a docs pass.
2026-06-02 02:14:15 +02:00
Brummel d5e69148c6 refactor(check): unify the two Type-Con qualifiers over an is-local predicate
qualify_local_types and qualify_workspace_types were two ~55-line
recursive Type rewriters identical in every arm (Con skip-guards for
already-dotted and primitive names; Fn/Var/Forall recursion) except
the bare-name decision: the local form rewrites iff the name is in
local_types; the workspace form leaves names own to the module bare
and otherwise searches module_types for the defining module.

Factor the recursion into one rewrite_type_cons that takes the bare-
name decision as a `&dyn Fn(&str) -> Option<String>` (Some = rewrite to
this qualified name, None = leave bare). The two public functions are
now thin wrappers passing their respective closure. Recursion order
and Con-arm check order are preserved exactly; cross-module
qualification tests green.
2026-06-02 02:05:57 +02:00
Brummel 7d9ab4d29d refactor(codegen): parameterise the copy-pasted IR-emission families
Emitted IR is byte-identical for every case — proven by the IR-pin
suites (eq_primitives_pin, ord_int_intercept_ir_pin, the raw_buf_*
and drop/leak pins) and the full e2e suite, all green.

intercepts.rs:
- The twelve emit_rawbuf_{new,get,set,size}_{int,float,bool} functions
  were copy-paste across three element types, differing only in the
  element width (8/8/1) and the LLVM load/store type (i64/double/i1).
  Collapsed to four parameterised cores; the element variants are thin
  call sites passing the (width, type) pair.
- Replaced the repeated, off-by-one-prone parameter-SSA extraction
  idiom (`locals[n-2]`, `locals[n-1]`) with an Emitter::last_param_ssas
  helper.
- Factored the shared IR-Str bytes GEP out of emit_eq_str /
  emit_compare_str into emit_str_bytes_gep.

drop.rs:
- The three emit_*_drop_fn_for_type methods shared one wrapping shape
  (monomorphic short-circuit, else loop over instantiations dispatching
  to a *_for_instantiation helper); hoisted into emit_drop_fn_wrapper
  taking the per-instantiation emitter as a fn pointer.
- emit_flat_intrinsic_drop_fn / _partial_drop_fn differed only in the
  symbol prefix and an ignored mask param; merged into one inner
  emitter.

No INTERCEPTS-registry or (intrinsic)-marker changes.
2026-06-02 02:02:17 +02:00
Brummel 7ae92d3e60 refactor(test): hoist duplicated test helpers into ailang-test-support
closes #60

The fixture-corpus filter (NON_PARSEABLE_FIXTURES + list_ail_fixtures)
was copy-pasted across three test crates and drifted out of sync as
new reject fixtures landed; the examples_dir / workspace_root path
walk was reimplemented ~30 more times across the suite, under two
spellings (workspace_root / ws_root).

Introduce crates/ailang-test-support — a zero-dependency, dev-only
leaf crate — as the single home for these helpers:
- NON_PARSEABLE_FIXTURES, list_ail_fixtures
- workspace_root, examples_dir
- canonical_workspace_root (symlink-resolved variant, for the tsan/
  race tests that feed the root into native build steps)

All integration-test copies across ailang-core, ailang-surface,
ailang-prose, ailang-check, and ail now import from the shared crate;
the local definitions and their now-orphaned path imports are removed.
Path helpers resolve via the support crate's own CARGO_MANIFEST_DIR,
so they return the correct absolute paths from any caller.

ail_bin helpers are intentionally left in place: they depend on
env!("CARGO_BIN_EXE_ail"), which Cargo only defines when compiling the
ail crate's own integration tests, so they cannot move to a shared
crate.

Behaviour-identical: same paths, same fixture lists; full workspace
test suite green. Net -177 LOC.
2026-06-02 01:54:37 +02:00
Brummel ac9171ebf0 refactor: collapse duplicated helpers and drop dead code across check/core/codegen
Pure simplification pass, no behaviour change — hashes, canonical
forms, diagnostic codes, and emitted IR are byte-identical (hash-pin
and IR-pin tests unchanged and green).

ailang-check:
- strip_forall and collect_pattern_binders were triplicated verbatim
  across linearity.rs / reuse_shape.rs / uniqueness.rs; hoisted each to
  a single pub(crate) fn in lib.rs.
- mono.rs::pattern_binders was a fourth copy of collect_pattern_binders
  (iterative style, same result for every Pattern shape); deleted, now
  calls the shared fn.
- maybe_instantiate and expect_eq were single-call wrappers; inlined
  at their sole call sites and removed.

ailang-core:
- collect_used_in_pattern was a verbatim duplicate of pattern_binds;
  deleted, call site repointed. pattern_binds made private (no external
  callers; the doc-comment's lift_letrecs claim was stale).
- is_false serde helper replaced by std::ops::Not::not at the four
  skip_serializing_if sites (all plain-bool fields); helper removed.
- test-only any_nested_ctor / any_let_rec folded into one generic
  any_term(t, &pred) walker.
- removed dead test helpers tmp_dir / examples_dir, orphaned when their
  tests relocated to tests/workspace_pin.rs.

ailang-codegen:
- removed the write-only Emitter::types field, its populating loop, and
  the now-unused CtorInfo struct it fed.
- adt_drop_symbol / adt_partial_drop_symbol differed only in a prefix
  literal; folded into one adt_symbol(prefix, ...). Symbol strings
  unchanged.

Net -180 LOC.
2026-06-02 01:39:35 +02:00
Brummel e25580e3a3 test(cutover): live accept/reject corpus for the #55 ownership surface
Wires the #55-cutover fieldtest into a durable regression net. The
fieldtest exercised the post-cutover ParamMode={Own,Borrow} surface as a
downstream LLM author would and produced 12 fixtures + a report; left as
loose files they would be dead fixtures that drift. This commits them as
a protected property.

crates/ail/tests/cut55_cutover_surface.rs — one table-driven test running
each fixture through `ail check` and asserting accept (exit 0) or reject
at the right pipeline stage. Reject rows key on the bracketed diagnostic
CODE (consume-while-borrowed, borrow-over-value, borrow-return-not-permitted,
surface-parse-error), NOT message text, so the test is decoupled from the
diagnostic-wording improvement tracked separately.

examples/fieldtest/cut55_*.ail — the corpus. cut55_2c is the #58 repro
(now correctly rejected). cut55_2b was misanalysed by the fieldtest as a
consume-while-borrowed reject; in fact bump's recursive param is
(borrow List) so the tail is only borrowed, never consumed into an own
slot — `ail check` correctly accepts it. Renamed to
cut55_2b_borrow_traversal_clean and recast as the #58 false-positive
guard (a borrow-position use of a heap sub-binder must stay accepted).
cut55_1b similarly does not fire over-strict-mode (its recursive call
consumes the tail, so the lint's consume_count==0 premise fails) — comment
corrected; it is a plain accept. cut55_1c is the genuine over-strict-mode
example (accepts exit 0, emits the warning).

docs/specs/0065-eliminate-implicit-mode fieldtest report — moved 2c to
the reject set, added the 2b false-positive-guard section, marked the
double-free spec_gap RESOLVED (it shipped as the #58 fix).

Relates to #55.
2026-06-02 00:45:21 +02:00