191 Commits

Author SHA1 Message Date
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 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 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 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 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 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 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 19757480b7 audit(0064/cutover): record shipped drop machinery + retire dead desugar arm
Cycle-close tidy for the #55 cutover (its audit drift-resolution).
Architect drift review found the design ledger out of step with the
codegen that the cutover shipped, plus two debt items; regression green
(733 passed / 0 failed across the workspace).

design/contracts/0008-memory-model.md — the Codegen contract described
the drop-emission *gates* but not the drop machinery the cutover landed.
Added three subsections recording the present state (honesty rule):
- Per-monomorph drop fns for polymorphic ADTs (crates/ailang-codegen/
  src/dropmono.rs: collect_drop_monos / DropAdtMeta, the suffix scheme,
  value-field-skip on the substituted field type). Ratified by
  alloc_rc_value_type_field_is_not_rc_dec_dropped.
- String-literal rep promotion at owned drop sites (StrRep::Static→Heap
  on a Str literal flowing into an Own slot the callee drops; gated
  strictly on Own). Ratified by own_str_literal_arg_is_dropped_exactly_once.
- Same-constructor arm grouping in match desugar (build_chain /
  build_ctor_group bind ctor fields once). Ratified by
  lit_pat_ctor_tail_drop_single_drop + lit_pat_nil_scrutinee_single_drop.

crates/ailang-core/src/desugar.rs — build_chain routes every Ctor-head
arm (including a length-1 run) through build_ctor_group, so
desugar_one_arm's Pattern::Ctor arm was unreachable dead code
duplicating the bind-once lowering. Replaced it with unreachable! naming
the invariant, and corrected two stale doc comments (the module-header
step 4 and the desugar_one_arm doc still described it as handling ctor
arms, and mislabeled the Lit lowering as Term::Match — it is Term::If).
Full workspace stayed green, confirming the arm was dead.

crates/ailang-check/src/linearity.rs — renamed test implicit_fn_is_exempt
→ own_param_consumed_once_is_clean. Post-0062 there is no Implicit and no
exemption; the test pins the ordinary single-Own-consume clean path.

Did the desugar + linearity edits inline rather than via an agent: I had
already loaded build_chain/build_ctor_group/desugar_one_arm to prove the
arm dead, and a sub-agent would have redone the same reading.
2026-06-02 00:45:06 +02:00
Brummel b129af1363 fix(check): inherit borrow on heap sub-binders of a borrowed scrutinee (#58)
The strict linearity check accepted consuming a heap-typed pattern
sub-binder extracted from a `(borrow)`-mode match scrutinee. The
sub-binder aliases the caller-owned interior, so moving it into an
`(own)` slot double-frees at runtime (SIGSEGV) — `ail check` returned
exit 0, `ail build`+run crashed. A pre-existing hole the corpus never
exercised; the #55 cutover's universal activation of the strict check
exposed it (sibling to the #57 / spec 0064 class-2 let-alias-of-borrow
hardening — this is the pattern-sub-binder analog).

Root: `walk_arm` seeded every pattern sub-binder with
`borrow_count = 0` (freely consumable), bypassing the `Borrow`-param
seeding in `check_fn` that starts a borrowed param at `borrow_count = 1`.
The whole-param consume was caught (cut55_2d, correctly rejected); the
moved-out heap sub-binder was not.

Fix: in `Term::Match`, resolve the scrutinee through `resolve_alias`
and record whether it is a borrowed binder; thread that into `walk_arm`,
which now seeds a heap-typed (`!is_value`) sub-binder of a borrowed
scrutinee with `borrow_count = 1`. Value-typed sub-binders (e.g. the
`Int` head) stay at `0` — copied out, no heap alias. Nested matches fall
out for free: the inner match re-derives borrowed status from the
borrow-carrying sub-binder.

Rejected alternative: forcing fieldtest fixture cut55_2b to also reject.
2b is a clean borrow-traversal — `bump`'s recursive param is `(borrow)`,
so the tail `t` is only borrowed, never consumed into an `(own)` slot.
Distorting the fix to reject it would be unsound (false positive on
legitimate borrow-rebuild). The fixture's own comment misdescribed its
recursive param as `(own)`; the code says `(borrow)`.

Verification:
- RED test linearity::tests::consume_heap_sub_binder_of_borrow_scrutinee_is_rejected:
  was left:0 right:1 (check returned []), now green.
- Full workspace: 732 passed / 0 failed (was 731; +1 the new test). No
  committed corpus newly rejected by the sharper check.
- fieldtest repro cut55_2c: exit 0 (wrongly accepted) -> exit 1
  (consume-while-borrowed on `t`).

closes #58
2026-06-02 00:32:58 +02:00
Brummel 76b21c00eb feat(lang): eliminate the Implicit ownership default — totality + the drop-soundness it demasks (#55)
Deletes `ParamMode::Implicit`. `ParamMode` is now `{Own, Borrow}`:
every fn-type slot on every signature carries an explicit `own` or
`borrow`, no defaulted position survives anywhere (model 0008 §2,
spec 0062). The parser rejects a bare fn-type slot; `borrow-return`
and `borrow-over-value` reject at the signature; the corpus is
migrated to minimal-ownership modes (consumed ⇒ own, read-only-heap
⇒ borrow, value ⇒ trivial-own). The documented `Implicit`-ret-mode
leak is fixed: an owned heap return now drops exactly once (live=0,
acceptance criterion 5).

This was the easy half. Removing the default ACTIVATED a family of
drop paths that `Implicit` had silently skipped — the pre-cutover
language was leaking (and in places mis-dropping) here rather than
crashing, because an Implicit scrutinee turned the drop off. Making
the modes explicit (Own) turned those paths on and exposed two
latent-bug clusters, all fixed RED-first as part of this cutover:

Drop-soundness family (four legs):
  A. lit-sub-pattern double-free — the desugar re-matched the same
     owned scrutinee in the lit fall-through; fixed by grouping
     consecutive same-ctor arms into one match (bind fields once),
     in ailang-core desugar.
  B. Cons-husk leak on non-tail arm bodies — the lit-sub-pattern
     desugar rebound the owned scrutinee via `Let $mp = xs`, which
     bumped consume_count and suppressed the existing fn-return
     partial_drop. Fixed by not rebinding a bare-Var scrutinee
     (one husk-freeing mechanism, not two).
  C. polymorphic `drop_<T>` rc_dec'd monomorphised value fields —
     the per-ADT drop fn was emitted once from the polymorphic
     TypeDef, defaulting type-var fields to ptr and rc_dec'ing
     inline Ints (segfault). Fixed with per-monomorph drop
     functions (new ailang-codegen::dropmono): the drop set is
     collected from the lowered MIR, value-type fields are skipped,
     heap fields still freed once; monomorphic-concrete ADTs keep
     their byte-identical un-suffixed drop symbol.
  D. static Str literal passed to an `(own Str)` param — the
     literal lowers to a header-less rodata constant; the callee's
     now-active rc_dec read its length field as a refcount and
     freed a static address (segfault). Fixed with the missing
     fourth StrRep::Static→Heap promotion in lower_to_mir's App arm,
     gated on Own mode (borrow args stay static, no regression).

over-strict-mode lint over-fired: it suggested `(borrow V)` for
value-typed params (which `borrow-over-value` rejects — own is the
only legal mode there) and fired on `(intrinsic)` bodies (whose
consumption the linearity walk cannot observe). Tightened to skip
both; contract 0008 updated to the narrowed firing scope.

Irreversible step — canonical-form hash reset (model 0008 §6,
acceptance criterion 6). Every signature now carries explicit modes,
so the hashable canonical JSON changed for every module. RATIFY:
the corpus-wide hash-pin reset (hash_pin, prelude_module_hash_pin,
mono_hash_stability, eq_ord_e2e, embed_export_hash_stable, the
ct4/iter*/loop_recur schema-extension pins) and the list ir_snapshot
golden were regenerated once, deliberately, as the intended one-time
consequence of removing the mode elision from the canonical form —
not a regression. Each regenerated hash verified deterministic across
two runs.

Also fixes a pre-existing latent failure surfaced by the verification
gate, unrelated to this cutover: the `every_contract_names_a_resolvable_
ratifying_test` resolver (design_index_pin) could not resolve the
" + " dual-link ratifying-test form (`uniqueness.rs + linearity.rs`)
that the #57 audit-close (dfdc65f) introduced — it shipped red on that
commit. Resolver taught the dual-link form, mirroring its sibling.

Verification: cargo test --workspace = 731 passed, 0 failed (twice,
stable); e2e 102 passed, no binary exits non-zero (corpus crash-free);
grep-clean for Implicit/fn_implicit/mode_eq across crates; every drop
fix confirmed via emitted IR + AILANG_RC_STATS balance on the head==K,
head!=K, and Nil paths. Three BLOCKEDs en route (the unsound first
husk-dec attempt, the over-strict derivation premise, the leg-B fix
direction) were each treated as a real design/spec gap and rediagnosed,
not patched over.

Supersedes #54 (return-position-only leak patch). Precondition #57
(linearity hardening) was already met. Spec docs/specs/0062, plan
docs/plans/0121.

closes #55
2026-06-02 00:03:46 +02:00
Brummel 05c3c018de fix(check): branch Float NoInstance addendum on method name (#25)
The Float-aware `NoInstance` addendum emitted the same hint for every
Eq/Ord method at Float: "use float_eq / float_lt (and siblings ...)".
For `eq`/`ne`/`lt`/`le`/`gt`/`ge` that is correct — each has a drop-in
boolean `float_*` sibling. For `compare` it is incomplete and misleading:
`compare` returns three-way `Ordering`, but no `float_compare` ships (a
deliberate non-ship, docs/specs/2026-05-20-operator-routing-eq-ord.md).
An LLM author who reached for `compare` to get three-way ordering was
pointed at boolean siblings as if a drop-in existed, and left guessing
whether to reconstruct it themselves.

Fix: branch the addendum on the called method. The boolean arm keeps the
existing wording; the `compare` arm instead names the deliberate
`float_compare` omission and points at building a three-way `Ordering`
from `float_lt` + `float_eq`. One added branch on the existing
`method` field (already carried by `CheckError::NoInstance`), no new
machinery; the structured `ctx` is untouched.

Out of scope (the issue's deliberate non-ship): shipping a
`float_compare` fn. The friction was that the diagnostic did not
acknowledge the omission — now it does.

RED-first, inline: a one-branch diagnostic-text change at a single site
whose surrounding code was already loaded while working the adjacent #52
fix this session (CLAUDE.md "context already loaded" carve-out). TDD
discipline preserved by the new RED test
`compare_at_float_names_deliberate_no_float_compare` over a new minimal
fixture `examples/compare_float_noinstance.ail` (`compare` at Float); it
failed RED on the old shared wording and passes GREEN on the branch. The
pre-existing `eq_at_float_fires_float_aware_noinstance` still passes (eq
arm unchanged).

Verification: full ailang-check lib suite (121) + full ail test suite
green; live CLI renders both arms correctly.

closes #25
2026-06-01 20:34:20 +02:00
Brummel d8be95dd44 fix(check): render restricted-set diagnostic in AILang set syntax (#52)
The `param-not-in-restricted-set` diagnostic rendered its allowed
element set with `{allowed:?}` — a Rust `{:?}` debug print of the
`Vec<String>`, producing `["Bool", "Float", "Int"]` with quotes,
brackets, and Rust list shape. AILang's audience is an LLM author, so a
language-level diagnostic leaking Rust formatting into its surface is a
quality defect.

Fix: render the set as `{Bool, Float, Int}` via a thiserror trailing-arg
`.allowed.join(", ")` wrapped in literal braces. The set is alphabetical
and stable (unchanged — the source is a sorted BTreeSet projection).

Design decision (set notation, not a union): the allowed set is a
membership set ("one of"), and AILang has no union-type surface syntax,
so brace set-notation `{A, B, C}` reads naturally without implying a
type-level union the language does not have. The structured JSON detail
(CheckError::detail, the `allowed` array) is left untouched — it is
machine-readable and correctly an array, not the cosmetic surface.

RED-first, inline: the bug is a one-line Display-string change at a
single site (lib.rs ~760). The exact lines were already loaded while
assessing the /boss queue, so a debugger subagent would only redo the
same reading (CLAUDE.md "When NOT to delegate: context already loaded").
TDD discipline is preserved by the new RED test
`param_in_reject_message_renders_allowed_set_in_ailang_syntax`, which
asserts the AILang set form and the absence of Rust quotes/brackets;
it failed RED on the old `{allowed:?}` and passes GREEN on the fix. The
pre-existing pin `param_in_reject_message_names_allowed_set` only
asserted substring presence, so it did not pin (or block) the format.

Verification: full ailang-check suite green (121 lib tests + integration
suites); live CLI repro from the issue now renders
`(allowed: one of {Bool, Float, Int})`.

closes #52
2026-06-01 20:29:00 +02:00
Brummel 2769e50a35 fix(examples): destructure partition_eithers result once (#57, 0064 iter 4)
Final iteration of spec 0064 (the #55-cutover hardening, #57). Closes
class 4, the one genuine corpus bug among the four (not a false
positive): std_either_list.partition_eithers projected both
(app Pair.fst rest) and (app Pair.snd rest) from one owned `rest`.
Pair.fst/snd are own-param projections that move a field out, so each
consumes `rest` -> a genuine double-consume that universal linearity
activation (#55) would correctly reject. The fix is a body rewrite
(destructure `rest` once via (match rest (case (pat-ctor MkPair ls rs)
…)) then dispatch on the head), NOT a check change -- the check is
right.

Latent until activation: partition_eithers' param is a bare (Implicit)
slot today, so the check is skipped on it -- no RED->GREEN flip on the
real fixture. The rewrite is a pre-emptive corpus fix. Its correctness
rests on the unchanged 2 3 2 3 E2E output (std_either_list_demo, a
semantically-identical partition) and on the new c4_double_consume
must-stay-RED fixture, which -- with explicit modes, so the check is
active today -- demonstrates the double-projection shape IS rejected.

- examples/std_either_list.ail: partition_eithers Cons arm rewritten;
  doc updated (destructure-once, no longer "projections").
- examples/c4_double_consume.ail: must-stay-RED pin (the rejected
  shape), folded into a generalised
  harden_ownership_heap_double_consume_still_errors loop over
  {real_consume, c4_double_consume}.
- examples/c4_rewrite.ail: stays-clean pin (the accepted
  destructure-once shape), added to
  harden_ownership_false_positives_are_clean.

No hash-pin on std_either_list (verified); the e2e 2 3 2 3 output pin
is the content pin and is preserved. No check/schema/codegen change.
Verified: std_either_list checks clean; demo 2 3 2 3; both harden
assertions green; cargo test --workspace green; bench/check.py 34/34,
compile_check.py 24/24 stable.

This is the last of the four #57 hardening classes. Spec 0064 is now
code-complete: classes 1 (local fn-param modes), 2 (let-alias redirect),
3 (value-typed let-binder), and 4 (this) all shipped. The cycle is ready
for audit; the #55 cutover precondition is met.

refs #57
2026-06-01 18:22:59 +02:00
Brummel be259f9d46 feat(check): let-alias borrow propagation via alias-redirect (#57, 0064 iter 3)
Third iteration of spec 0064 (the #55-cutover hardening, #57). Closes
false-positive class 2: Term::Let walked its value in Position::Consume,
so (let a t (match a …)) over a borrow-mode t consumed t at the binding
and tripped consume-while-borrowed -- a let-alias of a borrowed value
read in a borrow position is not a consume.

Fix: the Checker gains a scoped aliases: HashMap<String,String>. A
(let a t body) whose value is a bare Var resolving to a tracked binder
records a -> root(t) for the body scope and skips the consume walk of
the value. A new resolve_alias helper maps a name to its root,
preferring a real binder at each chain step -- so an inner binder named
`a` (nested let, pattern binder, lam param) automatically shadows the
alias with NO change to with_binder/walk_arm/Lam (the shadowing is
resolved centrally in the resolver, not at three scattered introduction
sites). Every binder-state lookup keyed by name resolves through the
map first: use_var, the App borrow bump + decrement (pushing the
resolved root to `lent` so the decrement matches), callee_arg_modes,
and the reuse-as source.

Design calls (orchestrator):
- Alias REDIRECT, not state clone (spec scope decision 3): consuming
  the alias marks the single root consumed, so a real double-consume
  through an alias is still caught. A clone would track two independent
  binders and miss it (unsound). Pinned by the new
  let_alias_of_owned_double_consume_still_errors unit test:
  (let a p0 (seq a p0)) over an own heap p0 still fires
  use-after-consume.
- resolve_alias prefers binders -> shadowing needs no edits to the
  binder-introduction sites. Lower-risk than clearing aliases at each.
- reuse-as source (linearity.rs:663) is resolved through aliases too:
  it is the 4th binder-state-reading site; the spec's Fix 3 named three
  illustratively. Without it, (reuse-as <alias> …) would mis-fire
  reuse-as-source-not-bare-var on what IS a Var. Faithful completion of
  Fix 3.

The diagnostic now reports the resolved root name (the actual consumed
resource), not the surface alias.

Closes the design/contracts/0008-memory-model.md let-alias carve-out
(was "has not shipped yet") and extends its Ratified-by trailer to name
linearity.rs, where the propagation now lives -- a contract change
riding with the feature that forces it.

RED-first: examples/c2_let_alias.ail added to
harden_ownership_false_positives_are_clean (RED: consume-while-borrowed
on count's t); GREEN after. Verified: c2 RED->GREEN; 120 linearity unit
tests green; the soundness test fires; harden false-positive + heap
double-consume guards green; cargo test --workspace green;
bench/check.py 34/34, compile_check.py 24/24 stable. Diagnostic-only;
no schema/type/codegen change.

Class 4 (partition_eithers body rewrite) remains for the final
iteration of spec 0064.

refs #57
2026-06-01 18:12:25 +02:00
Brummel cc5991eeb3 feat(check): resolve local function-typed binder modes (#57, 0064 iter 2)
Second iteration of spec 0064 (the #55-cutover hardening, #57). Closes
false-positive class 1: applying a local function-typed binder -- a HOF
predicate param like std_list.filter's `p` -- treated its arguments as
Consume because callee_arg_modes resolved only the global symbol table
(locals returned an empty mode vec). So `(app p h)` with `p` a local
(borrow ...) predicate consumed the heap element `h`, and reusing `h`
in the kept Cons false-fired use-after-consume.

Fix: BinderState gains fn_param_modes: Option<Vec<ParamMode>>, seeded
at all three function-typed binder introduction sites via a new
fn_modes_of helper (strip_forall + Type::Fn { param_modes }, None for
non-fn / empty-modes so the caller falls through to globals): params
and lam-params from their signature type (param_tys), let-binders from
the LetBinderTypes table built in iter 1. callee_arg_modes reads a
local Var callee's fn_param_modes before the global lookup (a local
binder shadows a global -- correct lexical scope); the existing App
arg-walk maps a Borrow mode to a borrow walk unchanged, so the fix is
confined to the seeding + the one local-precedence read.

Scope call (orchestrator): all three seeding sites, not just the param
path that unblocks filter -- the point of this hardening cycle is to
leave no latent class (the #57-from-0063-deferral lesson), and the
extraction is uniform with the table already built.

RED-first: examples/c1_local_hof.ail added to
harden_ownership_false_positives_are_clean (RED: use-after-consume on
filter_box's h) before the fix; GREEN after. Two in-source unit tests
pin both seeding paths (param via signature, let via a hand-built
table). Verified: c1 RED->GREEN; 119 linearity unit tests green;
harden_ownership_false_positives_are_clean green (now c1 + c3); the
heap-double-consume must-stay-RED guard still fires; cargo test
--workspace green; bench/check.py 34/34, compile_check.py 24/24 stable.
Diagnostic-only; no schema/type/codegen change.

The stale `// Locals never carry fn-types in 18c.2` comment in
callee_arg_modes (and the fn's doc header) is rewritten to the accurate
local-precedence behaviour -- it sat in the replaced lines and directly
contradicted the new path.

Classes 2 (let-alias redirect) and 4 (partition_eithers rewrite) remain
for later iterations of spec 0064.

refs #57
2026-06-01 17:57:40 +02:00
Brummel 47964abf7c feat(check): tee let-binder types, exempt value-typed let-binders (#57, 0064 iter 1)
First iteration of spec 0064 (the #55-cutover hardening, #57). Closes
false-positive class 3: a value-typed `let`-binder (e.g. a `Float`
result bound and read more than once) tripped `use-after-consume`
because the linearity walk installed every `let`-binder as a default
heap-tracked BinderState. Spec 0063 deferred exactly this class
("value-typed let-binders ... deferred until a corpus shape demands
it"); eqord_3_newton_sqrt.iterate's `(let xnew (app / …) …)` is that
shape.

Mechanism (the design call, user-delegated): the let-binder's type is
ALREADY computed at synth's Let arm and discarded. Stop discarding it.
synth gains a (def,binder)->Type out-param (LetBinderTypes, defined in
linearity.rs); the Let arm records `subst.apply(&v)`. The table is
allocated per-module in check_workspace, threaded through
check_in_workspace -> check_def -> check_fn/check_const/check_instance
-> synth, and passed (immutable) into check_module_with_visible ->
Checker. linearity's Term::Let seeds BinderState.is_value from the
table via the existing type_is_value predicate -- the same per-binder
flag #56 seeds at param/pattern/lam sites, now extended to the let
site. No schema change, no hash shift, no codegen change; the check
stays diagnostic-only.

Not a re-run of inference in the walk (ruled out by aaa70d4 / 0063):
the type is teed from the one pass that already knows it.

RED-first: examples/c3_value_let.ail added to
harden_ownership_false_positives_are_clean (RED: use-after-consume on
xnew) before the fix; GREEN after. Two in-source unit tests pin the
seeding (value-typed let clean via a hand-built Float table) and its
type-gating (heap-typed let still errors). Full ailang-check suite
green (117 linearity + 14 workspace); cargo test --workspace green;
the heap-double-consume must-stay-RED guard still fires.

Implementation notes (verified against the diff):
- The live call graph routes check_in_workspace through check_def, not
  directly to check_fn (the plan's fixed line numbers predated that);
  the table is threaded through check_def's three arms. Required to
  reach every synth, not an extra.
- Step-10 compiler enumeration surfaced 26 synth call sites: 22
  recursive (the plan's "~22") plus 4 post-typecheck re-synth
  re-entries (lift.rs, lower_to_mir.rs, mono.rs x2). The four are
  write-only re-synth callers that discard their side-channels and
  never query the table, so each got a throwaway table -- the typed-MIR
  re-synth path (it re-enters canonical synth), consistent with the
  plan's const-def/test-caller pattern.

Fixes 1 (local fn-param modes), 2 (let-alias redirect), 4
(partition_eithers rewrite) are later iterations of spec 0064.

refs #57
2026-06-01 17:44:40 +02:00
Brummel e1c908912b feat(check): reject borrow-returns at the signature (#55, 0121 task 1)
`(ret (borrow T))` is now a check error (CheckError::BorrowReturnNotPermitted,
code `borrow-return-not-permitted`), fired on the fn signature before
body dataflow. Borrow-returns are refcount-invisible and can outlive
their source; re-enabling them needs the escape/liveness axis, which is
out of scope (spec 0062). The diagnostic names that gap as an honest
"not yet".

The check_fn signature destructure now also binds `ret_mode` (param_modes
stays under `..`; the borrow-over-value reject that reads it is folded
into the cutover, task 4). RED-first: examples/borrow_return_reject.ail
checked clean (exit 0) before the reject landed, exits 1 after. New
CLI-boundary E2E pin crates/ail/tests/mode_signature_rejects.rs, modelled
on raw_buf_new_type_arg_pin.rs. Additive — ParamMode::Implicit still
present; full workspace suite green, bench/check.py 0 regressed.

refs #55
2026-06-01 16:41:21 +02:00
Brummel aaa70d4c35 feat(check): harden the ownership analysis for universal activation (0063)
The strict linearity check (use-after-consume / consume-while-borrowed,
linearity.rs) runs today only on the ~45 of 258 all-explicit-mode fns;
its activation gate skips any fn with a bare/Implicit param. Deleting
ParamMode::Implicit (#55) would turn it on universally and surface ~21%
false positives in two classes. This closes both, making the core
ownership analysis sharp across the whole codebase for the first time —
the precondition for #55. Diagnostic-only: no schema, no hash, no
codegen change; the two existing diagnostic codes simply fire on a
smaller, more correct set.

Fix 1 — value-type exemption. A new is_value_type predicate
(ailang-core::primitives) names the unboxed set {Int,Bool,Float,Unit};
BinderState gains an is_value flag seeded from the binder's locally
available type (param signatures, ctor field types for pattern binders,
lam typed-params), and use_var short-circuits the Consume arm for it. A
value type has no refcount and is never consumed, so multi-read is
always legal.

  Str is deliberately NOT in the value set, though is_primitive_name
  includes it: drop.rs:490-492 lowers only Int/Bool/Float/Unit to
  non-ptr; Str is a ptr, RC-dec'd, so a multi-consume of Str without
  clone is a real use-after-free. is_value_type is the Str-excluding
  subset of is_primitive_name, pinned by a unit test. is_heap_type and
  the over-strict-mode lint are left untouched (separate concern).

Fix 2 — application is a borrow. Term::App walks its callee in
Position::Borrow (was Consume). Applying a function value reads it; it
stays live for further applications. Global fn-refs are untracked
(no-op); a tracked function-typed binder (a HOF param) is no longer
consumed by application. This fixes both the own-f-param
use-after-consume and the borrow-f-param consume-while-borrowed in the
recursion-passing HOF shape (map_int f t). Passing a function value as
an arg is unchanged — it follows the callee param_modes.

Scope decision: value-typed let-binders stay conservatively tracked as
heap (their type is inferred, not annotated, and the linearity walk
does not re-run inference). This is soundness-safe — over-strict, never
unsound — and not a measured corpus shape; lifting it would need a full
binder->type table out of the type-checker.

Verification: all three false-positive classes reproduced today against
explicit-mode fns and shipped as RED->GREEN fixtures
(examples/fp_{value,hof,map}.ail); examples/real_consume.ail stays RED
(heap double-consume still fires) to prove the exemption is type-gated.
715 workspace tests green; bench/check.py 0/34 and bench/compile_check.py
0/24 regressed. merge_states carries is_value so the flag survives
branch merges. RED-first verified per task.

closes #56
2026-06-01 15:38:32 +02:00
Brummel c5fd16a4eb feat(codegen): StrRep loop-carried Str ⇒ Heap, close the #49 recur leak
mir.4 closes bug #49 (a heap-Str loop binder replaced across `recur`
leaks every superseded slab; the loop result leaks too) structurally,
by making every Str a loop binder holds OR a loop returns an owned heap
slab — then deleting the `!is_str` carve-out from BOTH codegen gates
that carried it. The leg-by-leg `!is_str` patches are gone.

Mechanism (the milestone thesis: representation in MIR, codegen reads
it). lower_to_mir sets rep = StrRep::Heap on every Str literal in a
loop-carried position; codegen's MTerm::Str arm promotes a Heap literal
via ailang_str_clone (a fresh ailang_rc_alloc slab, rc_header refcount
1). Three promotion positions, all in the Loop/Recur lowering:
  1. binder seed inits (is_str_ty on the binder type);
  2. recur args at Str-binder positions (read off the innermost
     loop_stack frame);
  3. exit-arm tail result literals (promote_tail_str_literals walks the
     loop body's tail positions when the loop returns Str).
With every loop-carried Str now owned-heap, both gates lose !is_str:
the recur superseded-value dec (lib.rs) frees each intermediate slab;
the loop-result trackability gate (drop.rs:493) lets the caller's
scope-close free the final slab.

Why both gates, and the planning-time error this corrects. The original
plan/spec scoped the deletion to the recur dec gate only, reasoning the
#49 loop result is "consumed by print". The implement-orchestrator
landed that scope (Tasks 1-2) clean and correctly BLOCKED: it took #49
from live=3 to live=1, the residual being the loop RESULT. I verified
the diagnosis empirically:
  - print BORROWS its arg (prelude: `(let s (show x) (do io/print_str
    s))`, the eob.1 heap-Str discipline), so `(print s)` does not free
    the loop result; the caller's let-binder does, via drop.rs:493.
    "consumed by print" != "freed by print" — that was the error.
  - Deleting drop.rs:493's !is_str takes #49 and the recur-literal
    fixture to live=0.
  - Deleting drop.rs:493 WITHOUT exit-arm promotion SIGSEGVs (exit 139)
    on a loop returning a static Str literal — hence the third
    promotion position and the static-exit witness.
The agent surfaced a real spec defect via an empirical BLOCK rather
than guessing; I corrected the spec refinement note (both gates, three
positions) and completed the loop-result leg inline, the context
already loaded from verifying the BLOCK (CLAUDE.md "already loaded
context" carve-out). drop.rs:493's Str carve-out is now sound to delete.

Boundary (asserted ill-typed, not constructible): a borrowed static-Str
Var seeded/recur'd into a consumed Str loop binder — rejected upstream
by uniqueness (a consumed binder position is owned).

Verification (orchestrator-run): all four leak fixtures reach live=0
under AILANG_RC_STATS — #49 (xyyy), recur-literal (reset), static-exit
(result), and the f488d31 boxed-ADT guard (2, no regression). The #49
#[ignore] is lifted. Full workspace: 708 passed / 0 failed / 2 ignored
(mir.3b baseline 702/0/3; +6 passed, -1 ignored = #49 lifted; the 2
remaining ignores are doctests). ir_snapshot: no drift (the Heap
promotion does not reach non-loop-carried literals — the
non_loop_str_literal_stays_static pin confirms at the unit level).
Neither CLAUDE.md lockstep pair touches Str representation.

New witness fixtures: examples/loop_str_recur_literal_no_leak_pin.ail
(recur-arg leg) and examples/loop_str_static_exit_no_leak_pin.ail
(loop-result leg / static-exit soundness). New pins: lower_to_mir_ty
exit-arm producer pin + the flipped seed/recur-arg pins; two runtime
leak pins alongside the lifted #49.

closes #49
2026-06-01 00:54:44 +02:00
Brummel eba1be8d9d feat(codegen): fill MArg.mode for App args, read the anon-temp drop gate off it, delete module_def_ail_types (mir.3b)
Second of two iterations delivering spec 0060's mir.3 row (plan
docs/plans/0118-mir.3b-marg-mode-and-table-delete.md). lower_to_mir's
Term::App arm fills each MArg.mode from the resolved callee's
param_modes (the sig = synth_pure(callee) it already holds); codegen's
emit_call anon-temp borrow-slot drop gate reads arg.mode instead of
re-looking-up the callee's param_modes from the module_def_ail_types
table; and — since that gate was the table's only reader — the
module_def_ail_types field plus all its construction and threading are
deleted.

Two refinements to the spec's mir.3b sketch, settled in planning from a
focused recon and recorded in spec 0060:

1. module_def_ail_types is deleted in mir.3b, not mir.5. A grep proved
   self.module_def_ail_types had exactly ONE reader (the anon-temp
   gate); the own-param drop reads param_modes from the def's own f.ty,
   not this table. Once the gate moves onto MArg.mode the table is dead,
   so it is removed now rather than carried as dead code to mir.5. The
   mir.5 row's "last re-derivation residue" shrinks to the
   element-type / Term::New (New.elem) work.

2. MArg.mode is filled for App args only; MTerm::Let.mode is not filled.
   Only App args have a real per-arg mode source (the callee
   Type::Fn.param_modes). Do args (EffectOpSig has no param modes), Ctor
   args (no per-field mode), and Recur args (loop binders carry no mode)
   stay Mode::Owned. Let.mode has no source (ast::Term::Let has no mode
   field) and no consumer (the let-drop gate reads consume, not
   Let.mode), so it stays Owned — filling it would invent a value
   nobody reads.

Safety property held: MArg.mode is filled from the same callee fn-type
the gate read from the table, so the drop fires identically. For
(app RawBuf.get (app RawBuf.set …) 0), RawBuf.get's param 0 is borrow,
so args[0].mode = Borrow — exactly the value module_def_ail_types
yielded. Confirmed by the anon-temp witness staying green.

ParamMode -> Mode conversion: Borrow -> Mode::Borrow; Own and Implicit
(the Implicit ≡ Own contract) -> Mode::Owned. The own-param drop keeps
reading ParamMode off f.ty (Type/ParamMode imports retained, live
readers at lib.rs:1356/1507).

Also retires three now-stale doc comments that named the deleted
module_def_ail_types field (ailang-check/src/lib.rs, uniqueness.rs, and
the codegen_import_map_fallback_pin test doc) — a direct consequence of
the deletion, reworded to the current architecture.

Verification (orchestrator, post-implement inspect): diff matches the
plan (App-arg m_args built before m_callee consumes sig — the benign
borrow-order deviation the plan's note flagged); module_def_ail_types
grep-clean across all of crates/; cargo build --workspace clean (no
unused/dead_code); cargo test --workspace 702 passed / 0 failed / 3
ignored (+1 = the new producer pin app_arg_carries_callee_borrow_mode;
no #[ignore] added). The anon-temp drop-correctness witness
raw_buf_owned_drop_balances_rc_stats stays live=0, now driven by
MArg.mode; the other RC-stats leak pins green; #49 stays #[ignore]
(mir.4); #51/#53 build guards green.

mir.3 is now complete (3a relocated consume_count + deleted the second
uniqueness run; 3b filled the mode annotation + deleted
module_def_ail_types). Remaining: mir.4 (#49 StrRep RED->GREEN),
mir.5 (element-type/Term::New + ledger).
2026-05-31 20:10:25 +02:00
Brummel 6bc0b501cb feat(codegen): relocate per-binder consume_count into MIR; delete codegen's second uniqueness run (mir.3a)
First of two iterations delivering spec 0060's mir.3 row (plan
docs/plans/0117-mir.3a-consume-count-relocation.md). The per-binder
consume_count — the only thing codegen read from its second
infer_module_with_cross run — now lives on a new binder-keyed
MirDef.consume: BTreeMap<String,u32>, filled once by lower_to_mir on the
post-mono body. Codegen builds its existing (def,binder)->consume_count
lookup from those maps and the three scope-close drop sites (own-param,
let-binder, match-arm) read it; the codegen uniqueness run, its
UniquenessTable field, and the import are deleted.

mir.3 is split into two iterations (recorded in spec 0060): the named
deletion depends ONLY on consume_count. All three drop sites read
consume_count from self.uniqueness, while the modes they also gate on
(param_modes for the own-param dec, scrutinee_is_owned for the match
dec) come from the type, not the uniqueness pass (UniquenessInfo carries
no mode). So mir.3a relocates consume_count and ships the deletion;
mir.3b (next) fills MArg.mode/MTerm::Let.mode and switches emit_call's
anon-temp gate onto MArg.mode. The split halves the change at the
codebase's highest-risk surface (RC/drop correctness, the raw-buf leak
saga) and makes each half independently verifiable against the live=0
leak pins.

Design: consume_count lands on MirDef (binder-keyed), NOT on MArg. The
drop sites key by (def, binder_name) — a per-binder aggregate — while the
spec-sketched MArg.consume_count is per-arg-position and never reaches
them; the per-def map matches the UniquenessTable's own keying and all
three binder kinds (param/let/pattern) uniformly. MArg.consume_count
stays a mir.1 default. Source = run check's infer_module_with_cross
inside lower_to_mir post-mono (the synth_pure single-engine-re-walked
pattern); retaining a check-time result is blocked (check's uniqueness
is pre-mono and runs on-demand-from-codegen, never in check_workspace,
so it would miss the mono specialisations). cross_module_types
(= codegen's module_def_ail_types) is rebuilt in elaborate_workspace
from the post-mono workspace.

Safety property held: this is a PURE RELOCATION of an identical
computation — infer_module_with_cross ran on the post-mono module in
codegen and now runs on the same post-mono module in lower_to_mir, so
drop placement is byte-identical. cross_module_types matches
module_def_ail_types exactly (both insert f.name->f.ty over post-mono
Def::Fn), confirmed by the leak pins staying green.

Verification (orchestrator, post-implement inspect): diff matches the
plan; codegen grep-clean for infer_module_with_cross + UniquenessTable
(now ailang-check-internal); cargo build --workspace clean (no errors,
no unused warnings — module_def_ail_types survives for emit_call's
anon-temp param_modes gate); cargo test --workspace 701 passed / 0
failed / 3 ignored (+1 = the new producer pin
mirdef_consume_is_populated_for_let_binder; no #[ignore] added). The
live=0 drop-correctness witnesses all green:
alloc_rc_loop_valued_rawbuf_binder_drops_at_scope_close (#43/#47),
alloc_rc_heap_loop_binder_replaced_by_recur_does_not_leak,
alloc_rc_print_int_does_not_leak_show_result_str. #49 stays #[ignore]
(mir.4); #51/#53 build guards green.
2026-05-31 19:48:57 +02:00
Brummel a6fd93adba feat(codegen): pre-resolve the App callee in MIR; delete is_static_callee + type_home_module (mir.2)
Second re-deriver removal of the typed-MIR milestone (spec
docs/specs/0060-typed-mir.md, plan docs/plans/0116-mir.2-callee-static.md).
Static-callee resolution moves out of codegen and into lower_to_mir:
every Term::App callee is classified once, mirroring check's own synth
Term::Var ladder (lib.rs:3409-3582), and emitted as a resolved Callee.
Codegen reads the callee identity off MIR and routes each kind to the
right lowering. The codegen re-derivers is_static_callee and
type_home_module are deleted, and the lower_app <-> is_static_callee
lockstep pair is struck from CLAUDE.md.

Callee reshape (beyond the spec's original {module, fn_name} sketch —
spec 0060's Concrete-code-shapes block is updated in this iteration):

  pub enum Callee {
      Static  { module, fn_name, sig: Type },  // user/prelude fn -> emit_call, module pre-resolved
      Builtin { name, sig: Type },             // operator/intrinsic -> inline opcode lowering
      Indirect(Box<MTerm>),                    // dynamic: fn-pointer / closure / shadowed name
  }

Two forced refinements, both settled in planning:

- sig:Type on each resolved variant. drop::synth_callee_ret_mode reads
  the callee ret_mode, today off Callee::Indirect(inner).ty(). A
  resolved callee has no sub-term, so the sig (= synth_pure(callee),
  mode-preserving) is the lossless replacement. This is NOT a mir.3
  pull-forward: the MArg param-mode / consume_count fields stay at their
  mir.1 defaults. Without it, every statically-resolved call would lose
  its drop signal and the RawBuf / int_to_str RC-stats pins mir.1b fixed
  would regress.

- Builtin variant. Operators and the str-num builtins (+, not,
  str_concat, ...) are lowered inline by name and have no module/fn_name;
  a separate variant is cleaner than a sentinel module. The classifier
  decides Builtin vs Static from CHECK'S OWN resolution (a name in
  env.globals with no owning module is a builtin), never a copy of
  codegen's old is_static_callee allowlist. The recon's divergence audit
  confirmed check's builtin set and codegen's inline-arm set match
  exactly, so the single-engine rule is mechanically satisfiable with no
  env threading gap.

type_home_module is fully deletable: a workspace-wide grep confirmed no
program references a type-scoped T.fn as a value, so its only other
consumer (resolve_top_level_fn) collapses to the module-name fallback
with no behaviour change. (The spec's "x3 mirrors" wording over-counted;
the live surface was the definition plus two call sites.)

Alternatives rejected during planning: sentinel module in Static
(ugly); builtins left as Indirect (breaks — no fn-pointer for an
operator); name-rewrite Static{name,sig} keeping lower_app's by-name
dispatch (blurs builtin/user and still needs sig). The mir.1b
re-synth-strictness trap (post-mono synth_pure re-unify surfacing
mode-strip / bare-vs-qualified / metavar leaks) did NOT fire under the
new producer path — qualify_local_types mode-preservation and the $u
wildcard normalisation from mir.1b held.

Verification (orchestrator, post-implement inspect): diff matches the
plan; grep-clean for is_static_callee + type_home_module across
ailang-codegen and ail; cargo build --workspace green; cargo test
--workspace 700 passed / 0 failed / 3 ignored (no #[ignore] added this
iteration — the 3 are the pre-existing #49 Str-leg pin + two doctests).
Acceptance witnesses green: #53 (mono_new_over_user_adt_builds_and_runs),
#51 (rawbuf_new_int_size_only_builds_and_runs still builds), show_print
cross-module (print_user_adt_runs_end_to_end), the new mir.2 pins
(mir2_resolved_callee_kinds_run_end_to_end, callee_classification_*,
strengthened new_over_user_adt_carries_node_types asserting Callee::Static).
#49 heap-Str loop binder stays #[ignore] (lifts at mir.4).

Two new examples/ fixtures back the new pins (classify_pin.ail for the
producer classification pin, mir2_callee_kinds.ail for the E2E),
ail-parse / round-trip clean.

Forward note (cycle-close architect): crates/ail/tests/codegen_import_map_fallback_pin.rs:14-15
doc prose names lower_app's cross-module arm and synth_with_extras as
failure-mode targets — both now deleted (mir.2 / mir.1b). The pin's
protected invariant is still valid and green; the prose is stale and
wants a doc-honesty reword, left out of this iteration's footprint.
2026-05-31 19:27:56 +02:00
Brummel 895ba846e8 feat(codegen): switch the lowering walk from &Term to typed &MTerm (mir.1b)
Atomic completion of spec iteration mir.1 (docs/specs/0060-typed-mir.md):
codegen now consumes the typed MIR produced by `lower_to_mir` instead of
re-deriving types from the bare `ast::Term`. Every codegen helper that
took `&Term` (lower_term, lower_app, drop.rs, match_lower.rs) takes
`&MTerm` and reads each node's checker-proved type off `MTerm::ty()`.
The build path is `Workspace -> elaborate_workspace -> MirWorkspace ->
lower_workspace`; the public `lower_workspace*` entry points and their 18
call sites thread `&MirWorkspace`. The codegen-side type re-derivers
`synth_with_extras` + `synth_arg_type` (and the `builtin_ail_type` /
`builtin_effect_op_ret` mirror tables) are deleted — grep-clean. The
three re-derivers the spec keeps until mir.2/mir.3 (`type_home_module`,
`is_static_callee`, the second `infer_module_with_cross`) stay.

The mechanical Term->MTerm match-arm conversion was straightforward and
compiler-enforced. The substance was a set of producer-side correctness
gaps that only surface once codegen reads `MTerm::ty()` and once the
build path re-synthesises the post-mono AST through the canonical
`synth` (which, unlike the old codegen, fully re-unifies). Each was
root-caused against a failing e2e fixture:

1. `qualify_local_types` stripped fn-type modes (rebuilt `Type::Fn` with
   empty `param_modes` / `Implicit` `ret_mode`), so a monomorphised
   polymorphic intrinsic (`RawBuf.set`) lost its `Own` ret-mode and the
   owned temporary leaked at the call site. Made mode-preserving, like
   its sister `qualify_workspace_types` and `Subst::apply` (449df13).

2. `lower_to_mir::synth_pure` synthesises each node in isolation, so a
   nullary polymorphic ctor (`Nil : List<a>`) left its element type an
   unbound `$m` metavar that the canonical synth never pins. Codegen's
   mono unifier (`unify_for_subst`) already has a wildcard for exactly
   this — `$u`, the spelling the now-deleted codegen synth used — so the
   typed-MIR boundary normalises every residual `$m` to `$u` once
   (`wildcard_residual_metavars`), rather than teaching each consumer to
   tolerate a raw metavar.

3. The class-method mono arm (`synthesise_mono_fn`) substituted the
   registry-canonical *qualified* instance type into a method appended to
   the instance's own module, minting a `show_user_adt.IntBox` param
   against a bare-`IntBox` body. Localised to bare before substitution,
   symmetric to the free-fn arm (600565d).

4. Monomorphisation synthesises *downward* class-dispatch references —
   prelude's `print__<IntBox>` names the instance module `show_user_adt`
   that prelude never imports. The post-mono re-synth in `lower_module`
   seeds every workspace module name as an identity import (excluding the
   current module, to keep own types bare) so the qualified-var path
   resolves these; the canonical `synth` used by `check_workspace` stays
   strict.

5. Post-mono, a cross-module callee can name the consumer's *own* ADT
   qualified (`show_user_adt.IntBox`) where the consumer synthesises it
   bare — a spelling split that cannot exist pre-mono (the param is
   polymorphic there). synth's App arm strips the current module's own
   qualifier from both sides before unifying (`strip_own_module_qual`),
   a no-op pre-mono.

Acceptance: whole workspace suite green (698 tests); `e2e` 98/98 and
`show_print_e2e` 3/3; `synth_with_extras`/`synth_arg_type` grep-clean in
codegen; #51/#53 fixtures build and run; lower_to_mir_ty pins green. The
#49 heap-Str loop-binder leak remains ignored (lifts at mir.4).

Builds on the standalone producer fix (600565d, free-fn own-ADT
localisation) and the two standalone mode-preservation fixes
(449df13 Subst::apply); those landed separately as they are
independently correct and inert on the old codegen.
2026-05-31 18:29:36 +02:00
Brummel 449df13c9c fix(check): preserve fn-type modes through Subst::apply
`Subst::apply` rebuilt every `Type::Fn` with `param_modes: vec![]`
and `ret_mode: Implicit`, discarding the modes the surrounding type
carried. That was harmless while nothing downstream of inference read
fn-type modes — but it is a latent under-specification: substitution
is meant to be type-preserving, and a fn type's modes are part of its
identity (an `(own T) -> (own U)` contract is not the same contract as
its borrow-returning sibling). Modes are positional over `params`, and
substitution remaps each param type element-wise without changing the
arity, so the mode lists stay aligned — preserving them is a clone, not
a re-derivation.

The typed-MIR boundary (milestone 0060) makes this load-bearing: a node
type synthesised by `lower_to_mir::synth_pure` ends with `subst.apply`,
and the codegen drop path reads `ret_mode == Own` off a call's callee
node to decide RC trackability. With the modes stripped here, an
Own-returning call read back `Implicit`, nothing was trackable, and a
heap-allocated binder leaked at scope close. Preserving the modes
restores that signal at the source rather than re-deriving it in codegen
(which is exactly the re-derivation the milestone exists to delete).

Safe by construction: `unify`'s Fn arm destructures modes with `..` and
compares only params/ret/effects, so carrying modes through `apply`
cannot change unification; and `Type`'s custom `PartialEq` already
treats `Implicit` and `Own` as interchangeable (only `Borrow` is
distinct), so equality outcomes are unaffected except where preserving
a `Borrow` is the more correct answer anyway. Whole `ailang-check`
suite stays green.

RED pin: crates/ailang-check/tests/subst_preserves_modes.rs.
2026-05-31 18:01:24 +02:00
Brummel 600565d356 fix(check): localize own-ADT type-args in free-fn mono; complete the lower_to_mir producer
Additive producer-side work for the typed-MIR milestone (spec
docs/specs/0060-typed-mir.md), surfaced while building the mir.1b
codegen-consumption switch. Nothing here consumes MIR — codegen is
untouched; the whole existing suite stays green and one new RED pin
goes green. The mir.1b codegen switch itself stays in the working tree.

Headline fix — own-ADT type-arg localization in free-fn mono:

  monomorphise_workspace's free-fn arm normalises every observed
  type-arg through Registry::normalize_type_for_lookup. That
  normalisation is load-bearing for cross-module dedup and a stable
  specialisation symbol name, but it qualifies a *defining-module-own*
  ADT to `<module>.<T>`. synthesise_mono_fn_for_free_fn then substitutes
  those qualified type-args into the polymorphic source signature and
  body, which are in the module's own *bare* convention (the qualify
  pre-pass deliberately leaves own-module type-cons bare — lib.rs:4358,
  "the current module sees its own types bare"). The result is a
  self-inconsistent specialisation: e.g. fold_left specialised with
  accumulator b := List<Int> minted
    ((std_list.List<Int>, Int) -> std_list.List<Int>,
     std_list.List<Int>, List<Int>) -> std_list.List<Int>
  — a qualified accumulator parameter against a bare list argument and a
  bare Lam body. check_workspace never hits this (it synths the pre-mono
  bodies, bare throughout); the old codegen tolerated it via the
  now-deleted synth_arg_type's loose type-tracking. The post-mono synth
  re-entry in lower_to_mir does full unification and correctly rejects
  it: `expected std_list.List<Int>, got List<Int>`.

  Fix: localize_own_types (mono.rs) strips the `<defining_module>.`
  prefix back to bare for the module's own ADTs, applied to the type-args
  before they are substituted, so the synthesised signature and body stay
  uniformly bare-own. The *stored* type_args remain normalised, so the
  symbol name and the Phase-3 rewrite-cursor key on the same canonical
  form — the byte-identity invariant between synthesis and rewrite is
  untouched. The ClassMethod arm needs no analogue: it already
  substitutes the un-normalised target.type_ (mono.rs:841).

  Alternatives rejected: (a) drop the normalisation in the shared
  apply_subst_and_normalize helper — breaks cross-module dedup, mints
  duplicate specialisations under divergent names. (b) Make
  lower_to_mir's synth treat `<owner>.T` and bare `T` as equal during
  unification — papers over the producer inconsistency in the consumer
  and contradicts the established own-types-stay-bare invariant the rest
  of check relies on. (c) Qualify the whole synthesised def own->qualified
  — fights lib.rs:4358 and would require the lower path to also flip,
  cascading the convention change through synth.

Producer completeness (additive, mirrors existing guards):

  - lower_module skips Type::Forall defs (lower_to_mir.rs), mirroring
    emit_module's guard. Polymorphic defs are stale source kept for
    round-trip; their bodies carry mono-rewritten call names for
    specialisations that were never synthesised, so a synth re-entry
    would hit UnknownIdentifier.
  - lower_module lowers non-literal const bodies to typed MTerm, carried
    in MirModule.consts (+ MirConst in ailang-mir). A non-literal const
    (e.g. a List ctor expression) needs a typed body once the consumer
    walk takes &MTerm; literal consts emit a global and need no body.
  - MirModule gains `ast: Module`, populated by lower_module — forward
    scaffolding the mir.1b codegen consumption reads for module
    structure. Populated here, consumed by the in-tree switch.

Verification: full `cargo test --workspace` green (697 passed, 0 failed)
with the codegen-consumption switch stashed out, including the new pin
crates/ailang-check/tests/lower_to_mir_ty.rs::poly_free_fn_accumulating_into_own_adt_elaborates
(RED before the localize fix with the exact mismatch above, GREEN after)
and the full e2e corpus (the own-ADT-poly demos elaborate clean and run
through the old codegen). This proves the producer fix is
regression-free and the remaining 22 e2e reds in the working tree are
codegen-consumption defects, not producer defects.
2026-05-31 17:41:05 +02:00
Brummel 135f4ceed7 feat(check): mir.1a — typed-MIR types + post-mono lower_to_mir + elaborate_workspace (additive)
First half of spec iteration mir.1 (docs/specs/0060-typed-mir.md,
plan docs/plans/0114-mir.1a-mir-infrastructure.md). Purely additive: a
new leaf crate plus a post-mono lowering walk plus the front-end entry.
Nothing consumes MIR yet — codegen and the CLI are untouched — so the
whole existing suite stays green (102 test-result-ok lines, 0 failed;
the one ignored is the #49 pin, which lifts at mir.4). mir.1b flips
codegen to consume MIR and deletes the synth_with_extras mirror.

What lands:
- `ailang-mir` (new leaf crate, depends only on ailang-core): MTerm /
  MArg / MArm / MLoopBinder / MNewArg / Callee / Mode / StrRep / MirDef
  / MirModule / MirWorkspace, structurally complete over all 17 Term
  variants plus the dedicated Str split (MTerm::Str{lit,rep}). Every
  later-iteration annotation field exists now at a mir.1 default
  (App.callee = Indirect, MArg.mode/consume_count = Owned/1, Str.rep =
  Static, New.elem = None); the struct shape will not change across
  mir.2–mir.5, only the values. MTerm::ty() reads the carried type.
- `ailang-check::lower_to_mir`: the post-mono walk. Carries no second
  type engine — it calls the canonical `synth` per node with fresh
  throwaway inference scaffolding (subst/counter/residuals/…), applies
  the substitution, and threads only the lexical locals/loop_stack,
  maintained by the same push/pop rules synth uses (Let, Loop, Lam,
  LetRec, and Match via synth's own type_check_pattern). This is the
  "one engine, not two" property the milestone buys, on the producer
  side.
- `ailang-check::elaborate_workspace`: the single front-end entry —
  check (diagnostics gate) → desugar+lift → monomorphise → lower_to_mir
  — transcribed from the CLI build path. check_workspace stays for the
  diagnostics-only callers.
- Three ty-fill pins (crates/ailang-check/tests/lower_to_mir_ty.rs)
  load the #51/#53/#49 witnesses as fixtures and elaborate the whole
  workspace, so lower_to_mir is exercised over the full prelude+kernel,
  not just the tiny witness. Two new witness fixtures
  (examples/new_{rawbuf_size_only,counter_user_adt}.ail); #49 reuses the
  existing loop_recur_str_binder_no_leak_pin.ail.

Deviations from the plan, all forced by ground truth and verified
against the live code before commit:
- FnDef.export is Option<String>, not bool — dropped from MirDef (the
  plan's note allowed this fallback). Codegen reads FnDef.export
  directly, unaffected.
- fn_param_types did not exist — lifted the param-type extraction into
  a shared pub(crate) fn and rewired both mono.rs sites
  (collect_mono_targets, collect_rewrite_targets) to it, so the
  param-type source cannot drift between mono and lower_to_mir. The
  helper unwraps a top-level Forall then reads Type::Fn.params —
  identical to the inner_ty extraction it replaces; the early-return
  non-fn guard is preserved at both sites. Behaviour-preserving (whole
  suite green; this is the only edit to existing mono behaviour).
- lower_module mirrors two more mono.rs scaffolding rules the plan
  under-transcribed: skip intrinsic-bodied fns (they are
  signature-only; lowering them would hit synth's Term::Intrinsic
  guard) and seed env.current_module + env.globals + env.imports per
  module so synth's Var lookup resolves post-mono specialisations
  (e.g. compare__Int) in the prelude.
- The #53 pin asserts the lowered (new Counter 42) init carries ty
  Counter, not that it is an MTerm::New: a monomorphic `new` over a
  user ADT is desugared to a dotted call `(app Counter.new 42)` before
  lower_to_mir runs (desugar.rs:1078-1098), so it lowers to MTerm::App.
  MTerm::New survives only for a polymorphic `new` carrying a written
  NewArg::Type (the #51 RawBuf path, covered by the rawbuf pin). The
  pin's intent — ty-fill correctness — is preserved; the structural
  variant is mir.2/mir.5 territory.
- ailang-mir uses workspace-inherited Cargo fields for consistency with
  the existing crates (added it to [workspace.dependencies]).

refs #49
2026-05-31 14:04:03 +02:00
Brummel ee4107c721 fix(check): honour the written element type-arg on polymorphic (new T …)
A `(new RawBuf (con Int) 3)` whose buffer is never observed by a later
get/set passed `ail check` but crashed `ail build` with
`RawBuf_new__Unit has no registered intercept`, and a forbidden
`(new RawBuf (con Unit) 3)` was wrongly accepted at check. Both legs
share one root: the `Term::New` desugar discarded the author's written
`NewArg::Type` before anything could use it.

This was never an inference problem. The element type is EXPLICITLY
known — the author wrote `(con Int)`. The defect was that the desugar
threw that known type away and relied on re-discovering it from
downstream use; with no use (size-only), `RawBuf.new`'s result-only
forall var stayed unpinned, mono Unit-defaulted it, and codegen aborted
on the unregistered `RawBuf_new__Unit` intercept. The fix USES the
written type instead of inferring it.

Mechanism:
- desugar.rs: a polymorphic `(new T <elem> …)` (carrying a written
  `NewArg::Type`) now SURVIVES into check instead of being lowered to
  `(app T.new …)`. A monomorphic `(new Counter 42)` (no type-arg) keeps
  the raw-buf.4 app-lowering unchanged.
- lib.rs synth `Term::New` arm: (a) validates the written element type
  against the constructed type's `param_in` set via
  `check_type_well_formed`, firing `ParamNotInRestrictedSet` naming the
  forbidden element (leg 2) — synth is the correct site because it has
  Env/registry access, unlike `pre_desugar_validation`; (b) binds the
  result-only forall var DIRECTLY to the written type (`?a := Int`, a
  trivial binding, no inference channel) by pushing a `FreeFnCall` whose
  metas are the written concrete types, so mono mints
  `RawBuf_new__<elem>` and never `__Unit`.
- mono.rs: `rewrite_mono_calls` and `interleave_slots` gain matching
  `Term::New` arms that each consume exactly one free-fn slot at a
  type-arg-bearing `Term::New` (mirroring synth's single observation,
  pushed before the value-args), and `rewrite_mono_calls` reduces the
  node to `(app <mangled> <value-args>)` so codegen never sees
  `Term::New` and the lib.rs:2200 `unreachable!` stays valid. The two
  walkers stay in lockstep.

The Unit-default policy in mono stays correct for genuinely-unobservable
vars (`is_empty(Nil)` etc.); only the case with a written `NewArg::Type`
is changed.

Alternatives rejected: an additive `type_args` field on `Term::App`
(~100 construction sites across 7 crates — a detour that builds a new
transport slot only to copy the already-known type into it); a runtime
type-witness parameter on `RawBuf.new` (invents a runtime value for a
pure type property); an identity-lambda wrapper carrying the element in
its param-type (hides a semantic property in a runtime construct). The
written type belongs where the author put it, carried to the one point
that consumes it.

Verification: both RED legs (committed 61b9d3f) now green; full
check/codegen/core/surface suites green; intercepts bijection and
hash-pin tests green; existing raw-buf int/float/bool fixtures still
build and run leak-clean (live=0).

Out of scope (pre-existing at HEAD, separate issue): a monomorphic
`(new Counter 42)` over a user ADT fails with `unknown variable:
Counter.new` — unrelated to the type-arg drop fixed here.

closes #51
2026-05-31 03:03:14 +02:00
Brummel a92bcaf969 fix(check): qualify cross-module kernel type-cons in user ADT fields
A consumer module's ADT field could reference a kernel-tier
auto-imported type by its bare name in op/value positions
(`(new RawBuf ...)`, `RawBuf.get`) but NOT in the type-constructor
position of the field declaration: `(con RawBuf (con Int))` stayed
the unqualified `RawBuf<Int>` and failed to unify with the
constructor argument's `raw_buf.RawBuf<Int>`, so a RawBuf could not
be stored in a user ADT field without spelling the qualified
`raw_buf.RawBuf`.

`qualify_workspace_module` skipped `Def::Type` entirely, and the
`Term::Ctor` arm only qualified field types of cross-module *owning*
types — a *local* type carrying a cross-module field was the
uncovered case. The fix qualifies each ctor field type in the
`Def::Type` arm via the existing `qualify_workspace_types`, which
upgrades only genuinely cross-module type-cons (skips
`own_local_types` and primitives), so a purely-local field is never
spuriously rewritten. This is a check-side workspace transform, not
the on-disk canonical form, so no module hash drifts (both hash-pin
tests stay green).

RED test `rawbuf_in_user_adt_field_resolves_bare_name` in
crates/ailang-check/tests/workspace.rs, with the bare-name fixture
(now checks/builds/runs -> 42, live=0, the ADT drop cascade frees
the buffer slab) and the qualified control twin.

This is the Series-substrate shape (a RawBuf wrapped in a user ADT),
so the inconsistency would have bitten the pending series milestone.

closes #50
2026-05-30 17:48:34 +02:00
Brummel 744ad41e47 fix(check): resolve type-scoped borrow-receiver ops in linearity (closes #46)
A function whose parameter is `borrow (RawBuf a)` and which calls
RawBuf.get or RawBuf.size on that parameter even once was rejected at
`ail check` with [consume-while-borrowed] — the exact borrow-receiver
use the ledger advertises for get/size. The diagnostic also misnamed the
cause: the receiver is read, not consumed.

Root cause: the linearity walk's callee_arg_modes looked up the callee
under its spelled name. A type-scoped polymorphic op is spelled
`RawBuf.get` at the call site, but check_module_with_visible registers
the kernel raw_buf ops under their bare def names (get/size). The lookup
missed, the receiver arg defaulted to Consume, and consuming a binder
whose borrow_count==1 (the Borrow param) fired the false positive. The
kernel signatures themselves are correct (receiver slot is `borrow`); the
only defect was the name-resolution gap in the linearity globals lookup.

Fix: on a direct-lookup miss, fall back to the bare method name via the
existing parse_method_qualifier + qualifier_is_class_shape resolvers,
gated on a class/type-shaped qualifier so lowercase cross-module-fn
qualifiers (std_list.length) are excluded. This is how the rest of the
checker already treats type-scoped polymorphic ops; the fix is general,
not RawBuf-specific.

This unblocks the natural borrow-helper decomposition (a shared
read-only buffer behind a helper fn) — the shape the downstream series
milestone's Series.at / Series.total_count need.

Surfaced by the raw-buf fieldtest (finding B1, docs/specs/0058).
RED-first: rawbuf_borrow_receiver_read_is_linearity_clean.
2026-05-30 17:13:56 +02:00
Brummel 75109f171d fix(check): param-not-in-restricted-set names the allowed set (closes #48)
The ParamNotInRestrictedSet diagnostic named the offending type, the
type-variable and the home type, but not the allowed set {Int, Float,
Bool} that design/models/0007 §4 promises it names. A downstream author
was told what is wrong but not what is right, and the kernel source that
carries the set is not available to a downstream consumer.

The allowed set already travels on the error struct (it flows into the
JSON `details.allowed`); only the human-readable `#[error]` render
dropped it. Append it to the Display string. JSON details unchanged.

Surfaced by the raw-buf fieldtest (finding B3, docs/specs/0058).
RED-first: param_in_reject_message_names_allowed_set pins the message
content before the one-line render fix.
2026-05-30 17:13:40 +02:00
Brummel 13e590cb46 iter raw-buf.6 kernel-stub-retirement (DONE 5/5): retire the stub, raw_buf is the sole base extension (refs #7)
Closes the raw-buf milestone. raw_buf (shipped raw-buf.1-.5; the
owned-drop resolution landed under bug #42/#43) has subsumed every
ratification role kernel_stub held -- Term::New end-to-end, the
param-in reject, kernel-tier auto-import, the monomorphic intrinsic
path, and the type-scoped polymorphic intrinsic mechanism (RawBuf's
four ops). The stub is now redundant; this iteration removes it.

Pure removal (-636/+49 across 22 files, 7 deleted):
- Rust surface: drop `mod kernel_stub` + `STUB_AIL` re-export
  (ailang-kernel), `parse_kernel_stub` + its workspace injection
  (ailang-surface), the `answer` + two `StubT_peek__{Int,Float}`
  INTERCEPTS entries + their three emit fns (ailang-codegen). The
  (intrinsic) markers leave with the deleted source, so the
  marker<->entry bijection holds in lockstep.
- Source + tests: delete crates/ailang-kernel/src/kernel_stub/,
  kernel_stub_module_round_trips, the two stub-consumer e2e tests,
  and mono_scoped_symbol.rs (its scope-qualified-mono mechanism is
  now pinned by RawBuf's ops + the intercepts bijection).
- Fixtures: delete kernel_answer.ail, new_stubt_smoke.ail,
  peek_mono_pin_smoke.ail, and fieldtest kem_3_stub_consumer.ail
  (referenced the deleted StubT; documented a since-fixed bug).
- Pins: re-baseline both workspace-count content-pins 5 -> 4
  (workspace_pin.rs + the e2e.rs twin) and regenerate all five IR
  snapshots (400 stub-IR lines removed; no user IR changed -- the
  stub auto-injected into every build).
- Ledger: design/INDEX.md + design/models/0007 to present-state
  (raw_buf is the live ratifier; raw-buf milestone shipped, series
  pending), plus architecture-comment sweep across workspace.rs,
  mono.rs, check/codegen lib.rs, workspace_kernel.rs.

Scope decisions (orchestrator, pre-plan): the self-contained inline
serde_json check-layer fixtures in ailang-check/src/lib.rs keep their
incidental StubT/kernel_stub sample names (they construct what they
reference; not stub-ratification) -- the one permitted residual.
kem_4 fieldtest kept (uses a user NumBox ADT, comment-only edit).
hash.rs `name: "answer"` left (generic serde doc example).

Plan-gap caught at implement: the planner's verbatim edit list
under-enumerated four honesty sites; one (mono.rs:562) carried a
literal `StubT_peek__Int` -- a hard-gate symbol the verbatim list
missed, which would have failed Task 4's removal gate. Filled
(comment-only, no behaviour). Confirms the planner self-review
filter-completeness risk; the implement gate caught it.

Verification: full workspace suite green (0 failed); hard symbol gate
(STUB_AIL|parse_kernel_stub|emit_answer|emit_stubt_peek|StubT_peek__)
zero matches across crates/ examples/ design/; soft gate residual only
the kept inline fixtures; kernel crate is lib.rs + raw_buf/ only.
Regression: compile_check 24/24 stable (exit 0; uniform downward
check_ms within tol -- stub no longer parsed per compile), cross_lang
25/25, check 34/34 stable (exit 0; an earlier exit-1 on
rc_over_bump was machine-load ratio noise -- denominator bump_s got
faster, rc_s also improved -- confirmed green on re-run, not
baselined).
2026-05-30 16:07:29 +02:00
Brummel 55d76ae4a1 fix: alpha-rename shadowing binders at desugar — A2b leg (closes #43)
The last open leg of the RawBuf owned-heap drop-leak cluster #43: the
UniquenessTable shadow-name collapse. The side-table keys by
(def_name, binder_name); a fn that shadows a binder name — the shipped
`(let buf (new…) (let buf (set buf…) … (get buf)))` idiom — collapses
every shadow onto one key. The outermost binding records last (on pop)
and overwrites the inner ones, so codegen's scope-close drop gates read
the collapsed consume_count for the innermost binding, misjudge its
ownership, and suppress its drop. The owned slab leaked (live==1).

Fix: desugar now alpha-renames any binder whose authored name shadows
an enclosing binding to a fresh `<name>$<n>`, making the (def, name)
key injective per fn. The rename is on-shadow-only and uniform across
binder kinds (Let, flat-Match pattern-binders, Lam params, Loop
binders); non-shadowing binders keep their authored name, so every
existing fixture's desugared output is byte-identical (evidenced by the
full pre-existing desugar suite passing unchanged). IR-neutral: codegen
names heap by fresh SSA, never by the source binder name.

No consumer of the uniqueness table changes — they all key by name, and
the name is now a per-fn injective identity (acceptance criterion 5).
The fix is entirely internal to ailang-core::desugar; uniqueness.rs gets
only a doc-comment correction (its old text was wrong on two counts:
"last = innermost by pop-order" was backwards, and "every shipping
fixture has unique binder names" was false).

Mechanism (vs. the spec's sketch): the threaded lexical scope became a
`Scope` struct carrying `entries` keyed by each binder's EFFECTIVE
(post-rename) name and `rename` mapping authored→effective. Keying
entries by effective name is load-bearing, not cosmetic: the LetRec
capture-detection reads `free_vars_in_term` of the desugared body
(effective names) and filters by `scope.contains_key` — had entries
stayed keyed by authored name, renaming an enclosing let would have made
a captured shadowed binder invisible to capture detection (UnknownVar in
the lifted fn). `insert_fixed` records identity renames for never-renamed
binders (fn-params, LetRec name/params) so an inner renamable binder that
shadows them is still detected.

Alternatives rejected: (A) an AST id field and (B) a derived
binding-path — both solve the deeper, SEPARATE problem of persistent AST
provenance back to the authored form, which is certain to be needed
eventually but is not required here; conflating the internal naming
collision with provenance is a category error. C′ (this) reuses the
existing fresh-name machinery and touches one pass.

Verification: the three shipped Let-shadow tests
(raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats) reach
live==0 (were RED at live==1); the flat-pattern differential
(flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed) reaches
its alpha-renamed control's live count (was 5 vs 3); a new desugar unit
test (shadowing_let_is_alpha_renamed) pins the rename + reference
resolution; full workspace suite green, no fixture output drift. Both
no-change consumers re-verified by hand: match_lower.rs keys by the
emitted (renamed) pattern binder, linearity builds table and lookups
from the same desugared tree.

Spec: docs/specs/0056-unique-binder-names.md.
Plan: docs/plans/0111-unique-binder-names.md.
2026-05-30 12:42:44 +02:00
Brummel 0f6108e428 fix: resolve cross-module borrow modes in the uniqueness pass (refs #43)
A2a leg of the owned-RawBuf drop-leak. Prerequisite: regression-free
and independently correct, but does NOT alone close the leak — the
three shadow_rebind RED tests (f7f4c3b) stay RED pending the A2b
shadow-collapse leg, which needs a UniquenessTable contract change and
its own spec.

The leg. The uniqueness pass infer_module runs strictly per module
(called per-Emitter from codegen lib.rs:993 with a single Module). The
module holding `main` registers only its own + builtin signatures in
`globals`; the monomorphised intrinsic signatures (RawBuf_get__Int with
param_modes=[Borrow,Implicit], etc.) live exclusively in the raw_buf
module's separate pass. So a qualified cross-module callee
`raw_buf.RawBuf_get__Int` missed `main`'s globals entirely, returned
vec![], and the walk defaulted every arg to Position::Consume —
mis-counting the borrowed `buf` arg as a consume and inflating the
binder's consume_count, which gates off the scope-close drop. This is a
latent over-conservative default affecting ANY cross-module borrow
callee, not just RawBuf.

The fix (additive, two files). infer_module is kept as a thin wrapper
over a new infer_module_with_cross(m, &cross_module_types) that threads
the workspace-flat module->def->Type table (the same module_def_ail_types
codegen already builds and the A1 emit_call rule already reads). On a
same-module globals miss, callee_arg_modes now falls back to
cross_module_callee_ty: split the callee on the last `.`, resolve
<mod>.<def> positionally against the cross-module table, and read its
Type::Fn.param_modes. Same-module + builtin lookup stays the first
resort; unqualified names and absent entries fall through to the
existing all-consume default unchanged. Modes are matched positionally,
so RawBuf.set's Own first param still counts as a consume (the
new/set-chain binders keep consume_count==1 and are not dropped —
correct, set is in-place, same slab).

Verified: full workspace green except the three intended-RED
shadow_rebind tests; ailang-check and ailang-codegen (incl.
intercepts_bijection_with_intrinsic_markers) green; A1's
raw_buf_owned_drop_balances_rc_stats still green. raw_buf_int.ail still
leaks (live=1) — that is the A2b leg, addressed next.
2026-05-30 11:19:49 +02:00
Brummel 8ac8756682 iter raw-buf.4 rawbuf-payload-termnew-desugar (DONE, drop-call deferred to .5): RawBuf works, prints 60 (refs #7)
Ships RawBuf end-to-end as a consumer of the raw-buf.3 scope-qualified
intrinsic mechanism, plus the general Term::New construction sugar.
Working subset committed; the drop-CALL ratification (no-leak) is
re-carved to raw-buf.5 (see b49f57d) — the flat drop FUNCTION ships here,
its call-insertion needs a codegen resolution mechanism.

What ships (all green):
- raw_buf kernel-tier submodule (crates/ailang-kernel/src/raw_buf/):
  RawBuf TypeDef (param-in {Int,Float,Bool}, ctor B a) + four
  (intrinsic) ops new/get/set/size. parse_raw_buf + workspace injection
  (kernel-tier auto-imported); workspace count 4 -> 5.
- 12 scope-qualified INTERCEPTS entries RawBuf_{new,get,set,size}__{Int,
  Float,Bool} + emit fns: new allocs an @ailang_rc_alloc slab
  (8-byte i64 size header + n*width element bytes), get/set
  getelementptr+load/store at offset 8 + i*width, size loads the header.
  Mechanical on the raw-buf.3 naming + bijection machinery; bijection
  green (4 markers -> 12 entries).
- Term::New desugar (crates/ailang-core/src/desugar.rs): (new T <types>
  <values>) -> (app T.new <values>), runs before check so the
  type-scoped callee flows through the raw-buf.3 scope threading to
  RawBuf_new__T; drops the NewArg::Type (element type inferred from
  use). Both codegen Term::New deferral arms removed (replaced with
  unreachable!). Ratified by new_stubt_builds_and_runs.
- Flat intrinsic-storage drop FUNCTION @drop_raw_buf_RawBuf (single
  @ailang_rc_dec on the slab), emitted for any TypeDef whose new op is
  (intrinsic)-bodied — distinguishes RawBuf (intrinsic new) from StubT
  (real-body new -> generic ADT drop).
- E2E: raw_buf_int (-> 60), raw_buf_float (-> 4.0), raw_buf_bool
  (-> 42), raw_buf_param_in_reject (param-not-in-restricted-set).

In-scope additions beyond the literal plan (both sound, ratified):
- qualify_workspace_term now normalises a monomorphic cross-module
  type-scoped callee (StubT.new) to <home>.f; without it
  new_stubt_builds_and_runs cannot build (StubT.new is monomorphic, so
  the raw-buf.3 poly-mono path mints no symbol). Same-module + polymorphic
  callees carved out.
- diagnostic-behaviour: (new T ..) missing-new-op now surfaces
  type-scoped-member-not-found (desugar runs before check, bypassing
  synth's Term::New arm); new-arg-kind-mismatch obsoleted. Two unit
  tests updated to the new behaviour. param-in reject unaffected.

The 5 .ll snapshots gained @drop_raw_buf_RawBuf (+ partial) — injecting
raw_buf emits its drop fn into every program; benign, regenerated to the
final IR. (The plan's "snapshots stay green" assumption was wrong.)

Verification (orchestrator, this session): cargo test --workspace 676
passed / 0 failed / 2 ignored. raw_buf_int_e2e prints 60; bijection,
round-trip, new_stubt, float/bool/reject all green. The raw_buf_no_leak
test is NOT in this commit — it moves to raw-buf.5 with the drop-call
resolution that makes it pass (the slab currently leaks at scope close;
tracked, fixed next iter; milestone not released until close).
2026-05-30 00:49:51 +02:00
Brummel fd37fa6489 iter raw-buf.3 typescoped-intrinsic-mechanism (DONE 2/2): scope-qualified mono symbols + bijection expansion (refs #7)
New language mechanism: a type-scoped polymorphic top-level (intrinsic)
op now mints a scope-qualified mono symbol (StubT_peek__Int, not the
colliding bare peek__Int), and the intrinsic<->intercept bijection
expresses one such polymorphic marker as its N per-param-in-element
entries. Ratified standalone on the stub via a new StubT.peek op; no
RawBuf, no Term::New, no codegen E2E this iteration (RawBuf consumes the
mechanism in raw-buf.4).

Task 1 — scope threading. Added scope: Option<String> to FreeFnCall +
MonoTarget::FreeFn + the synth free_fn_owner tuple. Populated Some(prefix)
ONLY on the type-scoped T.f resolution branch (lib.rs:3538, gated on
type_home.is_some()); None on every local / same-module / implicit-import
branch, so existing bare-resolved symbols stay byte-identical. Consumed
via a scoped_base helper at both mono-symbol mint sites (synthesise +
rewrite, which read the same MonoTarget → automatically in lockstep) and
folded into mono_target_key so a scoped op and a bare op of the same name
never dedup-collide.

Task 2 — ratifier + bijection. Added StubT.peek to the stub source;
extended workspace_intrinsic_markers with a type-scoped-poly arm that
finds the unique same-module TypeDef referenced in the fn signature and
expands over its param-in set, building the T_f__<elem> strings via the
SAME mono_symbol_n on Type::Con elems so collector and mint agree
byte-for-byte; registered StubT_peek__Int/Float entries + emit fns;
extended kernel_stub_module_round_trips to cover peek; added
mono_scoped_symbol integration test (own-param calls, no Term::New, no
codegen — asserts both scoped symbols minted and bare peek__Int absent).

Latent bug fixed inline (regression caught at the full-suite gate, RED via
the existing escape_local_demo E2E). kernel_stub is implicitly imported,
so poly_free_fn_names_for_module unconditionally added peek's bare name to
every consumer; a consumer with its OWN monomorphic peek then had its
local call mistreated as a poly-free-fn site, over-advancing the mono slot
cursor and misaligning a print target. Fix: suppress the bare
implicit-import name when the current module declares a same-name global,
mirroring synth's resolution ladder (same-module global beats
implicit-import). Applied in lockstep to both poly_free_fn name + and
constraint-count maps; dot-qualified / type-scoped spellings stay
unconditional. This was a pre-existing inconsistency between mono's
name-set and synth's resolution that peek (first implicitly-imported poly
free fn colliding with a fixture-local name) exposed.

Plan deviations (all sound): collect_con_heads omits Borrow/Own recursion
(no such Type variant — borrow/own are ParamMode on Type::Fn, verified
ast.rs:752); scope bound via the existing synthesise_mono_fn_for_free_fn
MonoTarget destructure rather than a new param; the mono-pin fixture uses
own params (borrow + peek-returns-a trips consume-while-borrowed; peek is
never instantiated so the mode is immaterial to the scope-symbol
ratification).

Verification (orchestrator, this session): cargo build --workspace clean;
cargo test --workspace 670 passed / 0 failed / 2 ignored (669 baseline +
the one new mono test). Bijection green (1 marker -> 2 entries),
round-trip green, escape_local_demo green. .ll snapshots unchanged (peek
polymorphic -> never instantiated without a call site). Existing eq__*/
compare__*/float_* symbols byte-identical (mono_hash_stability green).
2026-05-29 19:39:35 +02:00
Brummel 52ff8738b8 iter intrinsic-bodies.1-mechanism (DONE 8/8): Term::Intrinsic leaf + cross-crate wiring (refs #9)
First iteration of the intrinsic-bodies milestone. Introduces the
Form-A `(intrinsic)` body marker as a new leaf AST term and wires it
through surface, checker, codegen, and a kernel_stub ratifier. The
prelude migration + hard-lockstep pin + dead-path removal are .2.

What landed (8 tasks):

  Task 1 — Term::Intrinsic unit variant (ast.rs), tag "t":"intrinsic"
    via the enum's rename_all=lowercase. Additive: no existing fixture
    carries it, hashes bit-identical. In-core exhaustive-match arms
    (canonical/hash/visit/pretty/desugar/workspace) added as leaves.
  Task 2 — surface parse + print: (intrinsic) as a fn body-slot clause
    and a lambda positional body, mapped to/from Term::Intrinsic.
  Task 3 — cross-crate walker sweep (check/codegen/prose/ail-main):
    leaf no-op/identity arms at every no-wildcard Term match the
    compiler flagged.
  Task 4 — checker: new Env.current_module_kernel_tier flag (m.kernel
    || m.name=="prelude"), set alongside current_module. A def whose
    body is intrinsic (top-level fn OR instance-method lambda, via the
    shared is_intrinsic_body helper) is checked signature-only; an
    intrinsic body outside kernel-tier/prelude is rejected with
    intrinsic-outside-kernel-tier.
  Task 5 — codegen: an intrinsic-bodied fn routes through the existing
    try_emit_primitive_instance_body / intercepts::lookup path; if no
    intercept fired it is an internal error, never a lower_term
    fallthrough. lower_term and the synth walker get Term::Intrinsic
    internal-error arms (an intrinsic body reaching either is an
    escape bug).
  Task 6 — answer intercept (ret i64 42) registered in INTERCEPTS;
    the `answer : () -> Int` intrinsic added to STUB_AIL;
    examples/kernel_intrinsic_smoke.ail added so schema_coverage
    observes Term::Intrinsic in the examples/ corpus.
  Task 7 — E2E ratifier: examples/kernel_answer.ail calls
    kernel_stub.answer and prints 42; answer_intrinsic_builds_and_runs_printing_42
    asserts it end-to-end (source → native).
  Task 8 — design/contracts/0002-data-model.md gains the
    { "t": "intrinsic" } Term entry + fn/lam prose; form_a.md grammar
    note updated.

Verification:
  cargo test --workspace → 669 passed, 0 failed (baseline 667 +2:
    intrinsic_in_user_module_is_rejected, answer_intrinsic_builds_and_runs_printing_42).
  bench/check.py + bench/compile_check.py → 0 regressed.
  Reject E2E (subprocess ail check --json, exit 1, code
    intrinsic-outside-kernel-tier) GREEN.
  Round-trip + hash pins GREEN — Term::Intrinsic is additive, no
    existing fixture carries it, no hash moved.

Three implementation completions beyond the plan (all behaviour-
preserving, surfaced during execution):

1. The signature-only skip had to apply at the mono pass's two
   synth-on-body re-entry sites (collect_mono_targets,
   collect_residuals_ordered), not only check_fn — else an intrinsic
   body hits synth's Term::Intrinsic internal-error guard. Repaired by
   extracting the shared crate::is_intrinsic_body helper and applying
   it at all three synth-on-body paths. Not a representation surprise:
   the same signature-only treatment, more call sites.

2. The compiler-enumerated exhaustive-match set was broader than the
   plan's named grep set (the plan anticipated this and made the sweep
   compile-driven). Extra leaf arms in core desugar/workspace, check
   reuse-as + qualify_workspace_term, codegen synth_with_extras,
   ail/src/main.rs, and four test targets.

3. Fixture corrections: emit_answer needed the body-close
   (block terminator) the plan snippet omitted; kernel_answer.ail's
   main is (ret Unit)(effects IO) using (app print ...) since
   io/print_int does not exist (the plan flagged this for the
   implementer to resolve against real effect-op names).

IR snapshots (hello/sum/list/max3/ws_main.ll) refreshed: purely
additive @ail_kernel_stub_answer fn+adapter+closure, emitted into
every workspace exactly as the pre-existing @ail_kernel_stub_new
already was (kernel_stub is auto-injected; confirmed new was present
in the pre-iter hello.ll baseline). No user-fn IR changed.

The .2 iteration migrates the 18 prelude dummy bodies to (intrinsic),
upgrades registry_contains_all_legacy_arms to a source<->registry
bijection pin, and removes the dead body-lowering path.
2026-05-29 17:21:32 +02:00
Brummel a163c8c34a GREEN: pre-pass/resolver asymmetry — same-module bare + kernel-tier qualifier acceptance (closes F1, F3)
Two minimal edits in ailang-check that bring the resolver's
acceptance set into line with what prep.1's workspace pre-pass
(`prepare_workspace_for_check`) actually produces. The pre-pass
itself is unchanged — its qualification rules are correct per
spec § "Realisation mechanism — workspace pre-pass". RED tests
landed in 4d39fdc; both turn GREEN, both fieldtest fixtures
that surfaced the bugs now `ail check` clean.

F1 — same-module type-scoped call (kem_2b_min_repro.ail).
The dot-qualified `Term::Var` arm in `synth_term`
(`crates/ailang-check/src/lib.rs` ~line 3425) was
unconditionally rewriting the resolved fn signature via
`qualify_local_types`, so a call like `(app Counter.value c)`
from inside Counter's home module produced a return type
`<this>.Counter` — but the matching `Term::Ctor` arm
(~line 3644) and the pre-pass itself both leave own-module
type-names bare. The two halves of the resolver disagreed.

Fix: branch on `target_module == env.current_module` — when
true, skip the qualification (the raw type is already in the
form the rest of the resolver speaks); when false, qualify
as before. `owner_types` lookup moved inside the else-branch
since it's only consulted when qualification runs. A short
comment names the pre-pass and the sibling Term::Ctor arm so
a future reader sees the three-way symmetry.

F3 — kernel-tier qualifier acceptance (kem_3_stub_consumer.ail).
The env-builder paths `build_check_env` (~line 1653) and
`check_in_workspace` (~line 1807) force-injected only
`"prelude"` into `env.imports` / `env.module_imports`. The
loader meanwhile derives the implicit-imports list from
`modules.values().filter(|m| m.kernel)` (since prep.3) — so
`kernel_stub` flows into runtime resolution but not into
the checker's qualifier-validity check (~line 1968). Bare
`StubT` got qualified by the pre-pass to `kernel_stub.StubT`,
then bounced off the validity check as "unknown module
prefix".

Fix at both sites: keep the unconditional `"prelude"` literal
injection AND additively insert every workspace module with
`kernel: true` into the per-module import map (skip
self-injection). Idempotent for production (where prelude
also carries `kernel: true`) and preserves the
`bare_name_resolves_through_implicit_import_to_free_fn`
unit-test contract — that test deliberately constructs a
prelude module with `kernel: false` to pin the legacy
"prelude is always implicit" guarantee per se, independent
of the kernel flag. Mirrors the loader's kernel-flag filter,
making the env-builder and the loader speak the same set.

Sibling pin `crates/ailang-check/tests/env_construction_pin.rs`
(the frozen-reproduction copy of `build_check_env`'s
`module_imports` loop) updated in lockstep so it remains a
meaningful drift detector after the env-builder change. The
pin is intentionally designed to track legitimate behavioural
changes.

Verification:
  - tests::type_scoped_call_in_same_module_resolves      GREEN
  - tests::kernel_tier_module_qualifier_resolves_…       GREEN
  - examples/fieldtest/kem_2b_min_repro.ail              ail check ok
  - examples/fieldtest/kem_3_stub_consumer.ail           ail check ok
  - cargo test --workspace                               666 / 0
  (664 prior baseline + 2 RED→GREEN this iter)

Implementer notes: one re-loop on the F3 site after the first
edit replaced the legacy "prelude" literal injection wholesale
with the kernel-flag filter — that broke the unit-test contract
above. Restored the literal AND added the filter on top per the
"don't adapt tests to bugs" memory. No spec-review or
quality-review loops.

prep.1's pre-pass design (spec § "Realisation mechanism") was
correct as written — the symmetry between owner-side
`qualify_local_types` and consumer-side `prepare_workspace_for_check`
holds. What was missing was uniform resolver-side acceptance of
the qualifiers the pre-pass produces. With these two edits, the
following equivalences hold throughout the checker:

  bare T  ≡  <this-module>.T            (F1, same-module rule)
  bare T  ≡  <kernel-module>.T          (F3, kernel-tier rule)

via the loader-driven implicit-imports list that now drives
both the checker's import map and the type-validity check.
2026-05-28 19:36:36 +02:00
Brummel 4d39fdc9c0 RED: same-module type-scoped call + kernel-tier qualifier — pre-pass/resolver asymmetry (refs F1, F3)
Two failing in-source tests added to ailang-check, both pinning
the pre-pass / resolver mismatch surfaced by the fieldtest:

  tests::type_scoped_call_in_same_module_resolves
      F1: `(app Counter.value c)` from inside Counter's own home
      module must check clean. Currently fails with
      `[type-mismatch] main: type mismatch: expected
      <this>.Counter, got Counter` because the dot-qualified
      Term::Var arm at lib.rs ~3430 unconditionally calls
      qualify_local_types on the resolved fn signature even when
      target_module == env.current_module, while the matching
      local Term::Ctor branch (~3644) returns bare `Counter`.
      The two halves of the resolver disagree on whether
      `<this>.T` and bare `T` denote the same type.

  tests::kernel_tier_module_qualifier_resolves_without_explicit_import
      F3: `(con StubT (con Int))` in a consumer type signature
      must resolve without `(import kernel_stub)`. Currently
      fails with `[unknown-module] … unknown module prefix
      `kernel_stub` …` because env.imports / env.module_imports
      (built at ~1797 and ~1667) force-inject only `prelude` from
      the kernel-tier set; the pre-pass freely produces
      `kernel_stub.StubT` qualifiers that then bounce off the
      qualifier-validity check at ~1968.

Shared root: in both bugs the workspace pre-pass synthesises a
qualifier (`<this>.T` for F1, `<kernel_mod>.T` for F3) that some
downstream consumer of the resolver does not accept. The fix
surface is the resolver-acceptance side in both cases — the
pre-pass's qualification rules are correct per the spec's
§ "Realisation mechanism — workspace pre-pass". Implementation
will be two minimal edits to distinct files-and-functions
(no sweeping refactor).

GREEN side handed to implement mini-mode in the next dispatch.
2026-05-28 19:29:02 +02:00
Brummel 9339279181 iter prep.3-kernel-tier-modules (DONE 9/9): kernel-tier modules + param-in + stub crate — closes #33
Terminal iteration of the kernel-extension-mechanics milestone. Ships
the four language-level mechanisms named in the spec's § Goal:
Module.kernel + TypeDef.param-in schema, their Form-A surface,
flag-driven kernel-tier auto-injection, and generic param-in checker
enforcement with a new diagnostic.

Schema (Tasks 1+2). Module gains a `kernel: bool` field
(skip_serializing_if = is_false), TypeDef gains a
`param_in: BTreeMap<String, BTreeSet<String>>` field
(skip-if-empty, kebab-renamed to "param-in"). Both fields are
strictly additive — every pre-existing fixture's canonical-JSON hash
is bit-stable except `prelude.ail`, which intentionally gains
`(kernel)`. The struct-literal sweep covered ~104 Module sites and
~35 TypeDef sites across the workspace; the additive serde-default
covers JSON deserialise paths, only Rust struct literals broke.

Form-A surface (Tasks 3+4). `(kernel)` is a bare module-header
attribute; `(param-in (a Int Float) (b Str))` is one outer
TypeDef-body clause carrying one or more inner var-lists (OQ1
decision — mirrors `(ctors …)`, one parser arm, deterministic
BTreeMap iteration). Both round-trip Form-A → JSON → Form-A
bit-identical.

Workspace-load migration (Task 5). The hardcoded `&["prelude"]`
literal at loader.rs:108 became a `modules.values().filter(|m|
m.kernel)` derivation; `parse_prelude()` injection stays because
the prelude has no on-disk manifest in user workspaces. Prelude
now carries `(kernel)` in its source, so the new filter picks it
up automatically. Code-path migration only — observable behaviour
is identical (prelude_free_fns.rs stays green). prelude hash
re-pinned (af372f28c726f29f) with Honesty-Rule provenance comment.
WorkspaceLoadError::ReservedModuleName diagnostic prose
repurposed: any built-in kernel module name is reserved
(currently prelude + kernel_stub), not specifically prelude. CLI
mapping at main.rs updated in lockstep.

Stub crate (Task 6). New `crates/ailang-kernel-stub/` is a
zero-dependency leaf crate carrying only `pub const STUB_AIL:
&str` with the Form-A source of the kernel_stub module (one
parametric TypeDef with param-in, one ctor). The parse hop —
`parse_kernel_stub()` — lives in ailang-surface next to
parse_prelude, keeping the crate-dependency graph acyclic
(`ailang-surface → ailang-kernel-stub → ailang-core`, no
back-edge). The stub is injected unconditionally in all builds as
the ratifying fixture for the kernel-extension mechanism; future
base extensions may add more or retire the stub. Drift-pinned by
`kernel_stub_module_round_trips`.

Checker (Task 7). New `CheckError::ParamNotInRestrictedSet`
variant + code() + ctx() arms + enforcement in
`check_type_well_formed`'s Type::Con arm — generic, data-driven
from the TypeDef, mentions no specific extension type. Two
in-source tests pin both the rejection (`Str` outside `{Int,
Float}`) and the acceptance (`Int` inside) paths.

Workspace-load integration tests (Task 8). New
`workspace_kernel.rs` integration-test crate with three tests:
auto-import without explicit `(import …)` declaration, two
kernel-tier modules co-load, explicit-import-overrides-auto-
import precedence preserved. Loader is import-tree-only so the
auto-import tests use a bridge module that brings the kernel
module into the workspace via the import graph — docstring
captures the reachability nuance for future readers.

Doc-state transitions (Task 9). INDEX.md kernel-extensions row
annotation transitions from "design accepted 2026-05-28; impl in
progress" to "mechanisms milestone closed 2026-05-28; raw-buf and
series milestones pending". Whitepaper STATUS + auto-import +
param-in sections transitioned forward→present for shipped
mechanisms; forward-tense survives only in sections describing
the still-pending raw-buf/series milestones (per Honesty-Rule).
data-model contract gains anchor blocks for both new schema
fields.

Side-effect: every binary's IR snapshot now contains ~52 lines
for `drop_kernel_stub_StubT` because the stub is auto-injected
into every workspace load. Snapshots refreshed; e2e expects 4
modules per workspace (prelude + kernel_stub + entry + zero or
more user modules) instead of the previous 3.

Plan defects scrubbed in the implementation (folded back into
the planner template via the planner's self-review checklist
next time): Task 4 sample test src used fictional
`(ctors (MkT a))` list form (project grammar is per-`(ctor MkT
a)`); Task 6 original wiring would have created a cycle
ailang-surface → ailang-kernel-stub → ailang-surface (inverted —
stub crate is zero-dep, parse hop lives in surface); Task 7 in-
source tests referenced a fictional `check_type_in_module`
helper (used the existing Workspace + check_workspace
convention); Task 8 first integration test expected loader to
auto-load kernel modules from disk (loader is import-tree-only;
tests use a bridge module).

Concern-5 fix folded in pre-commit: workspace.rs ReservedModuleName
doc-prose initially said "in test/dev builds" for kernel_stub —
but stub is unconditionally injected in all builds. Doc copy
tightened to present-state per Honesty-Rule.

Stats: 0 spec-review-loops, 0 quality-review-loops, 2 sweep-script
retries on Task 2 (brace-depth bug on nested vec![Ctor{…}],
recovered via per-file checkout + rewritten anchor-on-existing-
field sweep), 1 e2e-snapshot refresh on Task 6.
2026-05-28 18:43:42 +02:00
Brummel 078c39a76a iter prep.2-term-new-construct (DONE 4/4): Term::New AST + Form-A surface + checker + drift — closes #32
Second iteration of the kernel-extension-mechanics milestone. Ships
the `new` Form-A keyword + `Term::New { type_name, args: Vec<NewArg> }`
AST variant + `NewArg::Type|Value` enum end-to-end through schema /
surface / checker, with two new diagnostics
(`NewTypeNotConstructible`, `NewArgKindMismatch`), a new arm in
prep.1's workspace-wide normalisation pre-pass `qualify_workspace_term`
that rewrites bare `Term::New.type_name` to qualified form
(symmetric to the existing `Term::Ctor` arm), and the data-model.md
+ form_a.md anchor additions. Codegen out of scope per spec; codegen
sites get `CodegenError::Internal` arms naming the raw-buf milestone
as the carrier.

Verification:

- `cargo test --workspace`: 654 tests passing, 0 failed.
- 3 new in-source checker tests pin the elaboration paths:
  `new_resolves_via_type_scope` (the spec's worked Counter example
  checks cleanly), `new_type_not_constructible` (missing `new` def
  in home module fires the new diagnostic), `new_arg_kind_mismatch_value_where_type`
  (kind-mismatch detection).
- 2 new schema-drift pins (`term_new_round_trips`,
  `term_new_type_arg_round_trips`) ratify the JSON byte shape:
  `{"t": "new", "type": "<TypeName>", "args": [{"kind": "type"|"value",
  "value": ...}]}`.
- 1 new surface round-trip pin exercises mixed-kind args through
  Form-A → JSON → Form-A.
- 44+ exhaustive Term-match sites across 24 files extended with
  `Term::New` arms — workspace-wide cargo build clean.

Concerns documented inline:

- `crates/ailang-core/tests/schema_coverage.rs` deliberately does
  NOT register `VariantTag::TermNew` in the `EXPECTED_VARIANTS`
  set. The coverage test asserts every declared variant is
  observed in the .ail fixture corpus; no .ail fixture in the
  current tree emits `"t": "new"` (codegen-runnable Term::New
  programs require the raw-buf milestone's plugin registry).
  Registering would fail the coverage check. The `visit_term` arm
  IS extended (compile-forced); only the enum registration is
  deferred. Inline rationale in the source. Future milestone that
  ships a Term::New fixture extends both sides.
- `crates/ailang-surface/src/print.rs` `write_term` Term::New arm
  was added in Task 1 (not Task 2 as planned), because without it
  ailang-core's tests fail to compile (the surface crate is in
  the dependency graph of ailang-core's test binaries). Task 2's
  round-trip pin verified the arm's correctness.
- Task 3 (synth elaboration) needed one implementer re-loop: the
  first attempt over-qualified within-module type-references via
  `qualify_local_types` on `new`'s signature when the home module
  was the calling module itself. Fixed by skipping qualification
  when `home_module == env.current_module`.

Architectural composition with prep.1: `Term::New` joins
`Term::Ctor` as a `type_name`-bearing site that goes through
`qualify_workspace_term`'s bare→qualified rewrite before the
checker sees it. The checker's `synth` arm for `Term::New`
therefore receives an already-qualified `type_name` (or a local
bare name for same-module construction).

Milestone status: kernel-extension-mechanics (Gitea #6) advances
2/3 iters. Next: prep.3 (kernel-tier modules + param-in), issue #33.
2026-05-28 15:31:13 +02:00
Brummel b586999e81 iter prep.1-type-scoped-namespacing (DONE 5/5): TypeDef-first resolution + workspace pre-pass — closes #31
First iteration of the kernel-extension-mechanics milestone. Ships
the type-scoped `<TypeName>.<member>` resolution path as the
canonical form for type-associated operations, narrows the
`BareCrossModuleTypeRef` / `BadCrossModuleTypeRef` diagnostics from
"bare = strictly local" to "bare = in-scope by any path", migrates
12 std-library example fixtures, and introduces a workspace-wide
normalisation pre-pass `prepare_workspace_for_check` shared between
`check_workspace` and `monomorphise_workspace`.

Architectural discovery during implementation: the plan covered the
`Term::Var` dot-qualified resolver layer plus the workspace
validator's bare-name acceptance, but the migration of bare-form
fixtures exposed five sites where bare vs. qualified type-names
needed symmetric treatment — `Term::Ctor` resolution, `Type::Con`
well-formedness, mono's poly-free-fn name/constraint-count
enumeration, codegen's `lookup_ctor_by_type` bare-name path, and
the upstream desugar-then-qualify composition. Rather than
scattering TypeDef-first ladders across each site, the implementer
centralised the work into one pre-pass that walks every consumer
module's `Type::Con.name` and `Term::Ctor.type_name`, rewriting
bare cross-module references to their qualified `<home>.<Type>`
form. This is symmetric to the pre-existing `qualify_local_types`
(owner-side); the new pre-pass is the consumer-side mirror.
Downstream passes see qualified Types regardless of authoring form.
The TypeDef-first ladder still lives in `synth`'s `Term::Var` arm
because `<TypeName>.<member>` is term-position-only — `Maybe.from_maybe`
is a Var, not a Type expression, and the pre-pass does not rewrite
Var names.

Alternatives considered:

(a) Add TypeDef-first ladder at every resolution site separately
    (the plan's implicit assumption). Rejected: O(N) extension
    sites, each carrying the same workspace-walking logic; the
    pre-pass version is O(1) — one pass, every downstream consumer
    benefits.
(b) BLOCKED + spec re-brainstorm. Rejected: the architecture
    extension is consistent with prep.1's thesis (bare type-name
    resolves to the workspace-wide TypeDef) and forward-compatible
    with prep.2 (Term::New.type_name falls under the same rewrite)
    and prep.3 (kernel-tier TypeDefs enter the workspace map
    automatically). No design regression to bounce back over.

Spec updated to document the realisation mechanism honestly: the
"Realisation mechanism — workspace pre-pass" subsection clarifies
that the resolver-level semantics described in "Implementation
shape" are the user-facing contract, and the actual code path is
the pre-pass.

Verification:

- `cargo test --workspace`: ALL GREEN. 87 e2e + every crate's unit
  + integration tests pass with no regressions.
- Three NEW in-source tests pin Task 1's resolver paths:
  `type_scoped_member_resolves`, `type_scoped_member_not_found`,
  `type_scoped_receiver_not_a_type`.
- One NEW workspace test pins the narrowed validator:
  `ct1_validator_accepts_bare_with_explicit_import`.
- One renamed-and-flipped existing test:
  `ct1_validator_rejects_bare_xmod_with_import_candidate` →
  `ct1_validator_accepts_bare_xmod_with_import_candidate` (the
  bare-with-import path is now ACCEPTED).
- One NEW companion test for the workspace-wide ctor lookup:
  `ct2_term_ctor_bare_cross_module_via_workspace_resolves`.
- Two pre-existing tests' assertions updated for the new error
  wording: `ct1_check_cli::check_human_mode_emits_actionable_message_to_stderr`
  and `crates/ailang-check/tests/workspace.rs::unknown_module_prefix_is_reported`.
- 12 migrated `.ail` fixtures verified via the existing e2e
  suite (each fixture is the test runner's target for an existing
  `build_and_run` assertion).
- Negative fixture `ct_2_bare_cross_module.ail` semantically
  preserved: dropped its `(import std_maybe)` so bare `Maybe` is
  out-of-scope under the narrowed rule and still fires
  `BareCrossModuleTypeRef`.

Concerns:

- The pre-pass introduces a new architectural layer (consumer-side
  qualification) that the spec did not originally anticipate. Spec
  amendment in this commit documents the layer. Future iterations
  reference `prepare_workspace_for_check` as established
  infrastructure.
- `examples/test_ct1_bare_xmod_rejected.ail.json` switched its
  offending name from bare `Ordering` (which under the prep.1
  semantics may now resolve via implicit prelude) to a still-
  unresolvable `Mystery_Type`. The CLI test's intent (assert that
  a human-mode `ail check` exits non-zero on a still-RED case) is
  preserved.

Milestone status: kernel-extension-mechanics (Gitea #6) advances
1/3 iters. Next: prep.2 (`Term::New` construct) issue #32.
2026-05-28 14:43:03 +02:00
Brummel 832375f2ac convention: counter-prefix file naming across docs/specs/, docs/plans/, design/contracts/, design/models/
All 176 files in the four accumulating directories now use a
zero-padded 4-digit counter prefix that reflects creation order
(`NNNN-slug.md`). The counter is assigned per directory in strict
git-log creation order; ties broken alphabetically by original name.
The old `YYYY-MM-DD-` prefix on docs/specs/ and docs/plans/ files is
dropped — the date is recoverable from git log and the counter
carries the ordering.

A file's counter is stable for the life of the file: never reassigned,
never reused, never compacted. Deleted files retire their counter;
subsequent files do not fill the gap. This is the property that lets
cross-references stay literal — refs use the full filename including
the counter (`design/contracts/0007-honesty-rule.md`) so they grep
cleanly and resolve directly without a glob step.

313 cross-references updated across .md/.rs/.toml/.c/.json files
(test pins, include_str! paths, design-INDEX entries, baseline notes,
runtime C comments, inter-contract markdown links incl. bare basename
and `../models/foo.md` forms).

CLAUDE.md gets a new "File-naming convention" section spelling out
the rule and rationale. skills/brainstorm/SKILL.md and
skills/planner/SKILL.md updated so new spec/plan creation produces
counter-prefixed names from the start.

The full test suite (cargo test --workspace) passes.
2026-05-28 13:31:31 +02:00
Brummel 4fc65ccb99 iter schema-camelcase-fix.1 (DONE 4/4): paramTypes/retType → param-types/ret-type — closes #30
`Term::Lam`'s two camelCase JSON tags become kebab-case, matching
the convention every other compound-key tag in the AST schema
already follows. After this iter the canonical JSON has zero
camelCase outliers.

## Schema swap (atomic, Task 2)

- `crates/ailang-core/src/ast.rs:492,494` — two
  `#[serde(rename)]` strings: `"paramTypes" → "param-types"`,
  `"retType" → "ret-type"`. Rust field names unchanged.
- `crates/ailang-core/src/workspace.rs:1925-1926` — in-source
  JSON literal in the `ct1_validator_walks_lam_embedded_types`
  test.
- `design/contracts/data-model.md:142-147` — fenced JSON block
  in the canonical data-model contract. Honesty-Rule touch-point:
  the contract document must describe the actual present-state
  schema.
- `examples/test_loop_binder_captured_by_lambda.ail.json` and
  `experiments/2026-05-12-cross-model-authoring/master/examples/fn_with_lambda.ail.json`
  — the two `.ail.json` fixtures whose canonical-JSON embeds
  the renamed tags.

The five files moved together within one task because `Term::Lam`
has no `#[serde(default)]` on `param_tys` / `ret_ty` — a
renamed-away key is a hard deserialise error. Splitting the swap
would have left the workspace untestable mid-step.

## RED → GREEN pin (Tasks 1, 2)

`crates/ailang-core/tests/design_schema_drift.rs` gains
`lam_serialises_with_kebab_keys`: pins that `serde_json::to_value(&Term::Lam{...})`
emits `"param-types"` / `"ret-type"` AND does not emit the old
camelCase keys. Companion: the existing
`design_md_anchors_every_term_variant` test now also asserts the
kebab anchors appear inside `data-model.md`'s `lam` fenced block.
Both confirmed RED on entry, GREEN after Task 2.

## Rustdoc honesty pass (Task 3)

Three pure-prose edits keep production rustdoc consistent with
the new schema vocabulary: `crates/ailang-core/src/ast.rs:8` (the
module-level rename enumeration), `crates/ailang-surface/src/parse.rs:81`
(prose mention of `lam`'s carry), `crates/ailang-check/src/lib.rs:1707`
(InstanceMethod routing helper rustdoc). No compile or test
consequence — Honesty-Rule maintenance.

## Plan-pseudo-vs-reality finding: under-audited hash blast radius

The brainstorm spec audited `crates/ailang-core/tests/hash_pin.rs`
exhaustively (5 pinned modules, zero `(lam ...)` occurrences,
"no hash refresh required"). It missed
`crates/ailang-surface/tests/prelude_module_hash_pin.rs` — a
separate hash-pin file in a different crate that pins `prelude.ail`,
which contains 11 `(lam ...)` forms. The prelude module hash
drifted (`6d0577ff0d4e50ac` → `562a03fc57e7e017`); the implementer
refreshed it with a Honesty-Rule provenance comment matching the
precedent set in commit `26fb345`. Form-A is unchanged — only the
canonical-JSON byte stream differs, which is exactly what the
rename targets. The spec-side learning is: schema-rename
brainstorms must walk *every* test crate for hash-pin files, not
just the home crate of the AST.

## Why this shape, and not the alternatives

- *`params-ty` / `ret-ty` (Rust-field-name vibe)* — rejected. The
  AST JSON schema follows its own kebab/single-word convention,
  not Rust field names. The other multi-word tag (`reuse-as`) is
  kebab; abbreviating `params-ty` mixes singular+plural and has
  no precedent.
- *Inline typed params as a sub-tag* (e.g. `params: [{name, type}, ...]`)
  — rejected. Stronger semantic locality, but it changes schema
  topology rather than tag spelling. Out of scope for a camelCase
  correction; would have re-pinned far more than this milestone.
- *Bundle with #27 (arith-rename)* — rejected. #27 carries four
  open brainstorm questions (mod vs rem, neg vs sub 0, Num class,
  deprecation window) and is structurally a separate milestone.
  Each gets one re-pin wave with its own rationale; no churn
  saving from bundling.

## Honest call on the feature-acceptance gate

Clause 1 (LLM author naturally uses the new form) is the weakest
of the three. Direct empirical evidence is absent — the 2026-05-21
naming-A/B run measured a different axis. The argument is
indirect: a future LLM author generalises from the rest of the
schema ("compound keys are kebab"), and the two camelCase
outliers are precisely the sites where that generalisation
diverged from reality. Clause 2 (redundancy reduction) and
Clause 3 (no semantic surface touched) are direct.

## Forbidden touches verified untouched

`docs/plans/*.md` historic plans (which embed old tag names in
example JSON), `experiments/2026-05-12-cross-model-authoring/master/spec.md`,
`experiments/.../rendered/*.md`, and `experiments/.../runs/**` —
all left as frozen historical artefacts per Honesty-Rule
analogue (describe state at time of writing, not present state).
Verified via `git diff --name-only HEAD` (Task 4 Step 4).

## Verification

- `cargo test --workspace`: all test groups OK, 0 failed,
  2 ignored (pre-existing).
- `cargo test -p ailang-surface --test round_trip`: GREEN
  (Form-A unchanged invariant).
- New schema-shape pin and the extended data-model anchor walk:
  GREEN after Task 2.
- Negative grep across `crates/`, `examples/`, `design/`,
  `runtime/`: the only remaining `paramTypes` / `retType`
  occurrences in checked-in code are the load-bearing
  negative-assertion strings inside the new pin (intentional —
  they are what makes the pin RED-able on regression).
- Stats: `bench/orchestrator-stats/2026-05-21-iter-schema-camelcase-fix.json`
  — 4/4 tasks DONE, no re-loops, no review-loops.

closes #30
2026-05-21 12:57:06 +02:00
Brummel 5170b6abd1 iter operator-routing-eq-ord.1 (DONE 13/13): drop comparator builtins, route through Eq/Ord
Closes Gitea #1. Realises the "P2 follow-up" called out in
examples/prelude.ail:9 — removes the surface comparator names
`==` / `!=` / `<` / `<=` / `>` / `>=` from the language entirely,
routes the LLM-author's `(app eq …)` / `(app compare …)` /
`(app ne|lt|le|gt|ge …)` through prelude.Eq / prelude.Ord class-
dispatch, ships six named Float-comparison fns
(`float_eq`/`float_ne`/`float_lt`/`float_le`/`float_gt`/`float_ge`)
so Float keeps comparability without an Eq/Ord instance, and emits
primitive instance bodies with `alwaysinline` so the -O0 IR shape
stays at one instruction per comparison.

Plan-task journal (13 tasks, single atomic iter per Approach A):

  Task 1 — Bootstrap: 4 new fixtures (eq_user_adt_smoke.ail,
    eq_float_must_fail.ail, float_compare_smoke.ail,
    operator_unbound_check.ail) + 5 new E2E/pin tests as RED
    starting state. All 5 confirmed RED at start: north-star
    fixed `NoInstance Eq Unit` (preserved by Unit-eq opening line
    intentionally added in plan-self-review); float_compare unknown
    `float_eq`; operator-name typechecked (== still polymorphic);
    must-fail diagnostic lacked `float_eq`; alwaysinline absent
    from IR.

  Task 2 — Codegen alwaysinline + intercept arms: introduced
    `intercept_emit_wants_alwaysinline` allowlist + appended
    ` alwaysinline` between `)` and `{` of the `define` line in
    `emit_fn`; added 9 new intercept arms to
    `try_emit_primitive_instance_body` — `eq__Int`/`eq__Bool`/
    `eq__Unit` + the six `float_*` arms.

  Task 3 — Prelude reshape: `instance Eq Unit` added; Eq Int/Bool
    bodies become placeholder-`false` (intercept overrides); six
    `float_*` free fns added; line-9 P2-follow-up comment removed.
    Lockstep hash re-pins: prelude_module_hash_pin (3abe0d3fa3c11c99
    → new), mono_hash_stability six body-hash literals
    (eq__Int/Bool/Str + compare__Int/Bool/Str all shifted because
    placeholder body changes the canonical hash). IR-snapshot
    regen (hello/list/max3/sum/ws_main) rolled forward into this
    task at orchestrator's pragmatic call — prelude shift forces
    the snapshots immediately.

  Task 4 — Fixture migration: 58 .ail fixtures rewritten
    (`(app == …)` → `(app eq …)`, etc.; Float-typed operand sites
    to `(app float_eq …)` / `(app float_lt …)`). eq_ord_user_adt.ail:21
    inner `==` → `eq` migration with lockstep eq_ord_e2e.rs:134
    body-hash re-pin (3c4cf040cb4e8bb2 → new). Two prose snapshots
    accepted; deps test + 5 hash_pin literals updated as cascading
    consequences.

  Task 5 — Test-scaffold migration: all 8 in-source
    `#[cfg(test)] mod tests` AST-literal sites threaded
    (desugar.rs:2414, check/lib.rs:5656/6092/6220, codegen/lib.rs
    sites). 7 obsolete in-source tests deleted (5 eq_typechecks +
    2 lower_eq ADT/Fn rejection — coverage moves to E2E
    eq_user_adt_smoke + eq_float_must_fail). 2 additional letrec
    tests deleted (single-module check env can't resolve eq/ge
    without prelude auto-import; covered by workspace E2E).

  Task 6 — Lit-pattern desugar: build_eq emits
    `Term::Var { name: "eq" }` instead of `"=="` at desugar.rs:1109;
    doc-comment rewritten to describe class-dispatch.

  Task 7 — Dead-machinery deletion sweep (compile-gated): typchecker
    builtins (install + list comparator entries deleted); codegen
    builtin_binop_typed (10 comparator arms deleted from synth.rs,
    table reduced to arithmetic core); lower_eq fn entirely
    deleted; `==` short-circuit in lower_app deleted;
    `is_static_callee` `==` clause deleted;
    `is_arithmetic_or_comparison_op` renamed to `is_arithmetic_op`
    + caller-update at codegen/lib.rs:2152 + :2529. Dead
    `poly_a_a_to_bool` helpers also removed. Workspace build green
    after compile gate — every caller of the deleted surface was
    migrated by Tasks 4-6.

  Task 8 — Float-aware NoInstance diagnostic: check/lib.rs:856-880
    addendum extended to name `float_eq` / `float_lt` as the
    explicit alternative for Eq/Ord at Float;
    eq_float_noinstance.rs:32-44 assertion extended.

  Task 9 — IR snapshot regen: subsumed by Task 3 (prelude shift
    forced immediate snapshot regen; deferring to Task 9 would
    have left the workspace red between tasks).

  Task 10 — Prose-projection cleanup: 6 comparator arms deleted
    from binop_info; 3 in-source mod-tests updated/deleted
    (comparator-infix rendering would be dishonest now that the
    operators are no longer language identifiers).

  Task 11 — Contract updates: 5 design files rewritten to the
    class-dispatch present —
      float-semantics.md (arithmetic guarantees retained on
        +/-/*/; comparison guarantees transferred from ==/!=/<
        to float_eq/float_ne/float_lt/etc.);
      prelude-classes.md (Eq Unit added to instance list;
        new paragraph on six float_* fns; Float-no-Eq/Ord clause
        gains `→ use float_eq` cross-reference);
      str-abi.md (clause "REMAIN primitive operators" rewritten
        to describe class-method dispatch);
      scope-boundaries.md (multiple operator-name and
        Pattern::Lit-desugar clauses rewritten);
      authoring-surface.md (==, <= dropped from operator-example
        list).

  Task 12 — Initial acceptance gate: workspace 638/0 GREEN;
    bench/compile_check + cross_lang 0 regressed; bench/check.py
    flagged 4 regressions on bench_closure_chain (+29% bump_s,
    +47% rc_s, +29% bump_rss_kb, +48% rc_rss_kb). Orchestrator
    initially classified as DONE-with-concerns; Boss reclassified
    as PARTIAL-via-acceptance-#8-fail after independent re-run,
    extended iter scope to Task 13.

  Task 13 — Direct icmp intercept arms (Boss-extension):
    try_emit_primitive_instance_body gains direct-icmp arms for
    lt__Int / le__Int / gt__Int / ge__Int / ne__Int, bypassing
    the compare__Int → Ordering → match indirection that allocated
    one Ordering ctor per call in tight loops. Each new arm
    inherits `alwaysinline` via the existing allowlist (extended
    accordingly). New IR pin test `ord_int_intercept_ir_pin.rs`
    + smoke fixture `ord_int_intercept_smoke.ail` ratify the
    optimization — opt -O2 -S confirms zero `call
    @ail_prelude_lt__Int` in optimized IR; the icmp folds directly
    at every use site. Bool variants (lt__Bool/etc.) deliberately
    NOT added — no bench/example calls Ord at Bool; spec-extension
    permits skipping if unreachable at bench level. Family can be
    extended symmetrically when first Bool-ordered perf workload
    appears.

Bench-gate post-Task-13: bench_closure_chain bump_s -6.05%,
rc_s -2.67%, bump_rss_kb -0.77%, rc_rss_kb +0.46% — all four
previously-regressed metrics back inside tolerance. Full bench
corpus: 36 metrics, 0 regressed, 0 improved beyond tolerance,
36 stable. bench/check.py exit 0 ✓; bench/compile_check.py exit
0 ✓; bench/cross_lang.py exit 0 ✓.

Workspace: 640 passed, 0 failed across all binaries (delta vs.
milestone start: +5 new E2E/pin tests added in Task 1 + 1 IR pin
added in Task 13 − 9 in-source mod tests deleted as obsolete net
≈ −3). The eq_user_adt_smoke fixture's Unit-opening line was
the deliberate RED-first device added in planner self-review so
the north-star wouldn't accidentally GREEN at start (user-ADT-Eq
on Point with hand-written instance was already operable today;
the milestone's actual delivery is operator-name death + Eq Unit
+ Float-named-fns + cleanup of the two-pathy primitive
comparator machinery).

Net delta: 96 files changed, 1760 insertions, 1101 deletions;
12 net-new files (6 new fixtures, 5 new E2E/pin tests, 1 stats
file). main passes-test-count: 640 (was 633 pre-iter, accounting
for the deletions).

Spec-vs-acceptance addendum: spec §Testing strategy anticipated
the bench-gate-regression case with two recovery paths
(`alwaysinline` investigation or "spec needs revisiting toward α").
Task 13 is the third path — direct intercept arms for `lt`/etc.
that bypass the compare→match path entirely. The spec's contingency
clause was thus generous enough to absorb Task 13 without spec
revision, but a future iter that hits a class-method primitive
where the body shape introduces a similar codegen cost (Ordering
allocation, RC tax, deferred-init) should expect a parallel
extension. The pattern is "primitive instance whose canonical body
indirects through other class methods that allocate" → add a
direct-emit intercept arm + alwaysinline + IR-shape pin.

Concerns absorbed:
  - Codegen lower_app / resolve_top_level_fn gained a
    prelude-fallback lookup so bare monomorphic prelude fns
    (`float_eq` etc.) resolve from non-prelude modules without
    explicit `prelude.float_eq` qualifier. Mirrors the
    typechecker's implicit prelude import — not in plan but
    necessary infra for the named-fn surface to be callable.
  - Recon's "≈10 fixtures" estimate was 6× too low — 58 actual.
    Mechanical migration; no design impact.
  - Recon caught 4 in-source AST-literal sites the spec missed
    (lib.rs:5656 `>=` site + three codegen/lib.rs sites);
    Task 5 covered all.
  - Recon caught 2 contract files outside the spec's update set
    that directly contradicted the milestone (str-abi.md +
    scope-boundaries.md "REMAIN primitive operators" /
    "Pattern::Lit desugar to ==" clauses); Task 11 covered all 5.

Stats file:
`bench/orchestrator-stats/2026-05-21-iter-operator-routing-eq-ord.1.json`.

closes #1
2026-05-21 01:16:21 +02:00
Brummel 99df14c792 workflow: scrub residual JOURNAL/journal refs missed in the first sweep
A re-grep found 15 live references (excluding docs/specs/ and
docs/plans/, which stay historical) the previous two commits
missed — all in source comments, doctests, bench helpers, and one
agent file.

Per-file:
- crates/ail/src/main.rs: typeclass-coherence diagnostic comment
  pointed at "the JOURNAL queue's wording" — points at
  design/contracts/typeclasses.md alone.
- crates/ailang-prose/src/lib.rs: `//!` header referred to
  docs/JOURNAL.md "Pinned: human-readable prose surface" —
  retargeted to design/contracts/authoring-surface.md.
- crates/ailang-check/src/lib.rs: bugfix tag + "see iter
  method-dispatch-refactor journal" prose collapsed to a clean
  rationale paragraph; the canonical shape is stated inline.
- crates/ailang-surface/tests/prelude_decouple_carve_out_pin.rs:
  "(d) record the rationale in a per-iter journal" →
  "(d) record the rationale in the commit body".
- crates/ailang-surface/tests/prelude_module_hash_pin.rs: header
  collapsed (pd.2/pd.3 milestone narrative dropped — the test's
  purpose is self-evident from its body); both "per-iter journal"
  drift-instructions point at the commit body.
- runtime/rc.c: "bench numbers in JOURNAL 18f.2" →
  "original profiling bench numbers".
- bench/run.sh: two "JOURNAL entry" comments → "commit body".
- bench/architect_sweeps.sh: header rewritten (cross-ref to the
  design-md-consolidation milestone commits, not a JOURNAL entry).
  Sweep-4 extended with two new anti-regrowth phrases
  ("see the per-iter journal", "in a per-iter journal") so journal
  prose can't grow back into design/contracts/ silently.
- skills/audit/agents/ailang-architect.md: "unlike a journal it
  lives on main" → "since it lives on main".
- ail-embed/src/bin/timeshard_runner.rs: "records it in the
  close-out journal" → "prints it to stderr".
- ail-embed/tests/timeshard.rs: two "journal-only friction timing"
  → "stderr-only friction timing".

Verification (after the edit):
- `grep -rin '\bjournal\b'` against live tree returns exactly two
  hits: the Sweep-4 regex itself (intentional — TABU phrases that
  prevent regrowth) and the PHRASES array in design_index_pin.rs
  (intentional — the same regrowth guard at test level). Both are
  load-bearing negative assertions.
- `bash bench/architect_sweeps.sh` exits 0 ("All five sweeps
  clean") — no design/-side regrowth.
- `cargo build --workspace` green; `cargo test --workspace` green.
2026-05-20 11:32:37 +02:00
Brummel 54f0ced148 workflow: delete docs/journals/ and docs/journal-archive.md
Strict application of the "Future-Use, not Verlauf" criterion to the
two remaining journal artefacts:

- `docs/journals/` (110 files): the per-iter and audit journals from
  2026-05-11 onward. Pure history; no live reader after the previous
  sweep. Entire directory removed.
- `docs/journals/2026-05-19-design-decision-records.md`: the one file
  that had live readers (`docs_honesty_pin.rs:108`, `parse.rs:80`,
  `duplicate_ctor_pin.rs:8`, three roadmap.md mentions) and was framed
  as a "relitigation guard". On re-examination its three asserted
  pinned phrases ("Regions were considered and rejected", the
  "demands annotations *because*" rationale, the prose-render
  placeholder statement) are rationale-prose, not load-bearing
  invariants — the test pinned itself, not a system property. Any
  Decision that still holds lives in the code, `design/contracts/`,
  or `design/models/`. Removed with the rest.
- `docs/journal-archive.md` (pre-2026-05-11 history): content-frozen
  long-tail history with no live reader. Removed; if anyone ever
  needs the pre-cutoff rationale they can `git log --before=2026-05-11
  --grep=<keyword>`.

Live-file consequences:
- `docs_honesty_pin.rs` `design_md_present_tense_anchors_present`:
  the three `records.*` assertions and the `read("docs/journals/…")`
  are dropped; the contract/model anchor pins remain.
- `duplicate_ctor_pin.rs`: the "why-two-overlays rationale lives in
  docs/journals/…" comment is replaced with the rationale inline.
- `parse.rs`: the "form-refinement rationale lives in docs/journals/…"
  comment is dropped (the rule body already states the refinement).
- `roadmap.md`: the decision-records mention in the DESIGN.md →
  design/ entry's body is dropped; the journal-archive.md `context:`
  pointers across ~12 closed entries are either rephrased to point
  at the relevant iter/audit (no path), or simplified to a one-line
  comment when the iter name alone carries the story.
- `CLAUDE.md` Roles section: the `docs/journal-archive.md` slot is
  removed; vocabulary note rephrased.
- `design/INDEX.md`: the Docs bullet drops `journal-archive.md`.
- `skills/README.md` bootstrap-rationale pointer rephrased.

`docs/specs/` and `docs/plans/` (per-milestone specs and per-iteration
plans) are unaffected — they remain the structured-design artefacts
they were before this sweep.

Workspace builds, full test suite green.
2026-05-20 11:25:15 +02:00
Brummel 8e586f493f workflow: replace per-iter journal system with git log + BLOCKED.md
The per-iter journal under docs/journals/ duplicated the iter commit
body's substance and accumulated as Verlauf-Doku with no Future-Use.
Sweep across all live control documents: CLAUDE.md, the 7 SKILL.md
files, the 11 agent files, design/INDEX.md and the contracts/models
that referenced journals, docs/roadmap.md, and the handful of source
comments + tests that pointed at journal files for rationale.

Mechanism changes:
- Standing-reading-lists in every agent now read `git log -N --format=full`
  for recent project state, never per-iter journal files. The architect
  reads `git log <prev-milestone-close>..HEAD --format=full` for audit
  scope.
- implement-orchestrator no longer writes a journal file. DONE outcomes
  emit just code + stats; the end-report is the per-task summary the
  Boss uses to write the commit body. PARTIAL/BLOCKED outcomes emit
  BLOCKED.md at the repo root — uncommitted by convention, Boss removes
  on repair or discard. New iron-law line + four-rationalisation row
  + red-flag bullet codify it.
- audit ratify mechanic: --update-baseline is now paired with an explicit
  ratify paragraph in the audit-close commit body, not a separate
  JOURNAL ratify entry.
- design/contracts/honesty-rule.md: "history and rationale lives in
  docs/journals/" → "lives in git log (iter and audit commit bodies)".
  Pinned phrase preserved verbatim.
- CLAUDE.md "Roles of …" section reframed: design/, git log,
  journal-archive.md (content-frozen), roadmap.md, specs/, plans/.
  No docs/journals/ slot anymore.
- roadmap.md context-lines that pointed at per-iter journals are
  dropped where the spec/commit already carries the rationale, or
  rephrased to "shipped in the <iter> iter commit" / "docs/journal-
  archive.md (<date> entry)" for pre-2026-05-11 references.

What stays (this commit):
- docs/journals/ directory and contents are NOT touched. Removing the
  contents is a separate follow-up.
- docs/journals/2026-05-19-design-decision-records.md still has live
  readers (docs_honesty_pin.rs Z 108 + parse.rs + duplicate_ctor_pin.rs
  + 3 roadmap mentions) — also follow-up.
- docs/journal-archive.md still exists; its self-pointer header has
  been updated to drop the "see docs/journals/INDEX.md" mention.

Workspace builds, full test suite green.
2026-05-20 11:21:37 +02:00
Brummel ac4d545570 source: scrub iter-code / Decision-N residue from inline comments
Follow-up to bcd4181: the remaining ~530 inline `//` and `///`
comments still carrying opaque shorthand are now reformulated to
their content phrases. The only surviving `iter-<code>` reference
in source is the literal filename
`docs/journals/2026-05-13-iter-mq.3.md` (a real journal file).

Sweep covered:
  - `// Iter X.Y: <text>` prefixes (Iter 13a / 14a / 14e / 15g-aux /
    16b.x / 16d / 16e / 18b / 18c.x / 18d.x / 18e / 18g.x / 19a /
    19a.1 / 19b / 20a / 20f / 22-floats.x / 22b.x / 22c / 23.x /
    24.1 / cli-diag-human / hs.x / str-concat / etc.) — fully
    removed; the descriptive text that followed each prefix stays.
  - `// (Decision N)` and `per Decision N` and `Decision N axis 3` —
    replaced with the content phrase plus the relevant contract
    file (`design/contracts/tail-calls.md` for Decision 8,
    `design/contracts/memory-model.md` for Decision 10,
    `design/contracts/typeclasses.md` and `design/models/typeclasses.md`
    for Decision 11, `design/contracts/authoring-surface.md` for
    Decision 6, "the transitional dual-allocator" for Decision 9,
    "Effect prose" for Decision 3).
  - `// mq.X / mq.X (Task N) / mq.X journal / mq.X invariant` ->
    "the canonical-class-form rule / Class-class repurpose /
    method-dispatch-refactor journal / canonical-class-form
    invariant".
  - `// ct.X / ct.X (canonical-type-names) / ct.1.5a + ctt.2 /
    ct.2 Task N` -> "the canonical-form rule for type references /
    the canonical-form normalisation step / canonical-type-lookup
    refactor".
  - `// eob.X` -> "heap-Str-ABI" / "the Str carve-out".
  - `// rpe.X` -> "the per-type-print-op retirement".
  - `// post-mq.X / Pre-ct.X / pre-mq.X` -> "post-canonical-class-form" /
    "Pre-canonical-type-form" etc.
  - `/// Iter X regression: / /// Iter X.Y: / /// Iter A arm-close /
    /// Iter ct.4 (...): / /// Iter rpe.1 ...` -> descriptive
    phrases.

The journal filename in `crates/ailang-core/src/workspace.rs:573`
stays verbatim because it points at an actual file under
`docs/journals/`.

Tests: full `cargo test --workspace` green (80/80 test-result blocks
clean, no FAILED line). design_index_pin 5/5 + docs_honesty_pin 5/5
gating tests pass.
2026-05-20 09:58:04 +02:00