a35878154bf400c9cb2a72b51a5a0fc450ab5627
200 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
 Brummel
|
a35878154b |
docs(examples): correct rbx_1 ctor-field qualification note
The field-test note on the `Window` ctor claimed that bare
`(con RawBuf (con Float))` in a user ADT ctor field gives a
type-mismatch and that "the only form that checks is the
fully-qualified `raw_buf.RawBuf`". Verified against the current
tool (release at HEAD), that claim is false in every form I could
construct:
- bare `(con RawBuf a)` (type-variable element) in a non-kernel
module: checks ok
- bare `(con RawBuf (con Float))` (concrete element): checks ok
- a `(new RawBuf ...)` value stored via `term-ctor` into a
bare-declared field: checks ok
- the full rbx_1 program with the field switched to bare RawBuf:
checks ok
A ctor field is plain type position, and model 0007 §3
("kernel-module types are accessible bare in type position") already
covers it — the auto-import that makes bare `Series` work at a call
site equally makes bare `RawBuf` resolve in a user ctor field. The
only genuine constraint is that a ctor field carries no mode:
`(own (RawBuf a))` is a surface-parse-error, which model 0007 line
458 already documents.
So there is no qualification asymmetry to add to the ledger; the
ledger is correct as-is. The drift was in this checked-in comment
(a guessed rule recorded as fact), now rewritten to the verified
reality. The qualified spelling is kept in the code as the explicit
form. No ledger change.
closes #65
|
||
|
Brummel
|
a2808a6938 |
test(codegen): ignored RED pin for match-arm consume-split leak (#63 leg 3)
The third and final identified leg of #63: an owned heap param consumed on one match arm but live on a sibling fall-through arm is never dropped, because both codegen drop sites (the fn-return Own-param dec in lib.rs and the pre-tail-call dec in match_lower.rs) gate on the per-fn AGGREGATE consume_count. When the param is consumed on one arm (aggregate >= 1) but live on another, the gate skips the drop on the live arm too. This is the residual that keeps examples/series_sma.ail at live=2 after legs 1 and 2. Series-free minimal repro (a `Box` consumed on the `On` arm, live on the `Off` fall-through arm; main takes the `Off` path): `live=1` today. Committed #[ignore]: unlike legs 1 and 2, this is NOT a contained fix. The per-arm/per-path consume information is destroyed by the worst-case `max` merge in uniqueness.rs (`merge_states`) before MIR — MArm carries only {pat, body}, MirDef.consume is the per-fn aggregate — so codegen has no per-arm liveness to gate a fall-through drop on. Closing it needs a memory-model change (retain per-arm consume, surface it to codegen, emit the drop only on the live arm, never at the post-match join or the consuming arm — a live double-free hazard) and a fresh brainstorm cycle. The pin is committed ignored so the precise symptom and minimal repro are durable; un-ignore when the fix ships. The assertion is a correct symptom pin (live == 0); only the fix mechanism is undecided. refs #63 |
||
|
Brummel
|
2488d9d345 |
test(codegen): RED pin for let-wrapped tail-call leak (#63 leg 2)
After the leg-1 fix (
|
||
|
Brummel
|
1be6e49b4f |
test(codegen): RED pin for owned-param leak in tail-recursion (#63)
An owned heap ADT param threaded through a tail-recursive fn whose base-case arm neither forwards nor consumes it is never RC-dec'd, so it leaks one slab per recursion step. Series-free minimal repro (a plain `Box` ADT, no Series/RawBuf), so the pin guards the GENERAL memory-model invariant rather than the Series surface that first surfaced it (examples/series_sma.ail, live=8). The pin builds the fixture with --alloc=rc, runs it under AILANG_RC_STATS=1, and asserts live == 0 (allocs == frees). RED today: `allocs=6 frees=4 live=2`. The fixture passes the replacement ctor directly into the tail call (not let-bound) to isolate leg 1 — the owned-param drop omission — from the second, distinct leg the debugger found (a `let`-wrapped tail call also defeats the scrutinee-husk shallow-dec gate; that leg is what pushes box_ctrl to live=4 and series_sma to live=8, and gets its own pin once leg 1 is green). Cause (debugger, for the GREEN side): the fn-return Own-param dec in crates/ailang-codegen/src/lib.rs (~1444) is gated behind `!block_terminated`, so it fires only on the fall-through ret path; crates/ailang-codegen/src/match_lower.rs (~805) drops only pattern binders, never the fn's owned params. A tail-call-terminated match arm thus has no drop site for an owned param with consume_count==0 that is not forwarded into the tail call. refs #63 |
||
|
Brummel
|
3b3c8c4f07 |
fieldtest(series-step1): 5 examples, 5 findings (1 bug, 1 friction, 1 spec-gap)
Post-ship field test of the shipped `series` library extension as a downstream Form-A author working from the public surface only. Five fixtures under examples/fieldtest/ across the construction/auto-import, ring-buffer/financial-indexing, len/total_count bookkeeping, param-in error-quality, and operator-naming axes; spec at docs/specs/0067-fieldtest-series-step1.md. Wins (carry-on): auto-import works with no `(import series)`; the financial index (0 = newest) maps directly onto the bounded-buffer mental model and stays correct after multiple wraps; the param-in diagnostic for a disallowed element type names the type, the type-variable, the qualified type, and the allowed set. Findings routed: - [bug] An owned ADT threaded through tail-recursion whose base case neither returns nor consumes it is never dropped — a general drop-soundness leak (a plain `Box` control with no Series/RawBuf also leaks). Series surfaces it heavily on the whitepaper's headline streaming pattern, and the committed reference examples/series_sma.ail itself leaks (live=8). Minimal repro: series-step1_5 (live=4). - [friction] `ail describe ... Series.push` (the canonical type-scoped form) reports module-not-found; only `series.push` / bare `push` resolve, and no command lists a type's op set. - [spec_gap] referencing a kernel base type (`RawBuf`) from a user ADT ctor field requires full qualification (`raw_buf.RawBuf`) while bare `Series` works in type-position via auto-import — the asymmetry is undocumented. The fixtures that leak still produce correct output; the leak is a separate observable under AILANG_RC_STATS and an orthogonal, pre-existing bug, not a Series defect. refs #61 |
||
|
Brummel
|
6b7ee45e49 |
test(series): RED pin for the SMA worked example (#61 headline)
The headline acceptance of #61: the simple-moving-average worked example from design/models/0007-kernel-extensions.md must build via `ail build --alloc=rc`, run, and print the correct moving averages. Green ⇒ the kernel-tier `Series` library extension works end to end (ring-buffer push, financial-style indexing at index 0 = newest, count/total bookkeeping). The fixture is the 0007 worked example with two corrections applied, both verified against the live tool this session: - `>=` is not a surface symbol; the polymorphic Ord helper is `ge` (here on Int operands: total_count vs window size). - `print` on Float emits no trailing newline, so the four averages would concatenate into an unreadable blob. The emit branch now prints the average followed by `io/print_str "\n"`, so each average lands on its own line and the output is deterministic and assertable. (This legibility fix is also queued to be carried back into model 0007.) RED reason (right-for-the-right-reason): `ail check` rejects with [bare-cross-module-type-ref] on `Series` — the kernel-tier module does not exist yet. The fixture itself parses and is otherwise valid. Expected stdout was derived by probing the live %g float formatter independently (the SMA averages are 9/3, 16/3, 17/3, 16/3 over the stream 1,5,3,8,6,2 with window 3): `3.0\n5.33333\n5.66667\n5.33333`. GREEN side (the `series` kernel module + the five ops) is the next mini-mode iteration. |
||
|
Brummel
|
e035eff8df |
test(series): RED pin for polymorphic RawBuf element-var forwarding
Base-tier enabling RED for the `series` milestone step 1 (#61). A polymorphic fn that allocates `(new RawBuf n)` with no explicit type-arg — element var solved purely from the enclosing ctor-field type `(con RawBuf a)`, never from a value argument — checks clean but fails `ail build --alloc=rc`: mono drops the check-phase solution for `a`, defaults it to Unit, and codegen mints the unregistered `RawBuf_new__Unit`. The fixture reads the element back via `RawBuf.get` so a wrong specialisation is observable (the program must print the stored `1.0`). This is the precondition the user picked (option B) so Series can ship as a pure AILang library extension over RawBuf while keeping the model-0007 `(new Series (con Float) 3)` caller surface. The #51 fix carried a WRITTEN `(con Int)` type-arg through mono; the variable-via-expected-type case is the untouched gap. RED: `ail check` exits 0; `ail build --alloc=rc` aborts with `RawBuf_new__Unit has no registered intercept`. GREEN target: builds, runs, prints `1.0`. The mono fix must not break the INTERCEPTS↔ (intrinsic) bijection or the Term::New↔pre_desugar_validation lockstep. refs #61 |
||
|
Brummel
|
9545257333 |
fieldtest: raw-buf milestone — 4 examples, 3 findings (refs #7)
Milestone-close fieldtest for the raw-buf milestone, milestone-scope
variant: four end-to-end scenarios derived top-down from the milestone
promise (construct via (new RawBuf <elem> <size>), fill/read via
set/get, size-only buffers, element variety across {Int,Float,Bool},
forbidden-element reject at check, buffer threading under own/borrow).
Result confirms the milestone-promise hypothesis — RawBuf is clean
end to end, zero bugs:
- mrb_1 Int fill/read loop: check ok, run + native build both print 70
- mrb_2 Float own->own threading + borrow read: prints 3.5
- mrb_3 size-only Bool buffer (#51 legitimate-but-unobserved case): prints 8
- mrb_4 Unit element: rejected at check with a precise
param-not-in-restricted-set diagnostic; build stops at the same
error, codegen never reached (the #51 fix)
Two [working] findings (carry-on) and one [spec_gap]: the
kernel-extensions whitepaper (design/models/0007) teaches bare-mode
fn-type slots that the post-#55 parser rejects. Verified and triaged
separately; the ledger fix follows in its own commit.
|
||
|
Brummel
|
e25580e3a3 |
test(cutover): live accept/reject corpus for the #55 ownership surface
Wires the #55-cutover fieldtest into a durable regression net. The
fieldtest exercised the post-cutover ParamMode={Own,Borrow} surface as a
downstream LLM author would and produced 12 fixtures + a report; left as
loose files they would be dead fixtures that drift. This commits them as
a protected property.
crates/ail/tests/cut55_cutover_surface.rs — one table-driven test running
each fixture through `ail check` and asserting accept (exit 0) or reject
at the right pipeline stage. Reject rows key on the bracketed diagnostic
CODE (consume-while-borrowed, borrow-over-value, borrow-return-not-permitted,
surface-parse-error), NOT message text, so the test is decoupled from the
diagnostic-wording improvement tracked separately.
examples/fieldtest/cut55_*.ail — the corpus. cut55_2c is the #58 repro
(now correctly rejected). cut55_2b was misanalysed by the fieldtest as a
consume-while-borrowed reject; in fact bump's recursive param is
(borrow List) so the tail is only borrowed, never consumed into an own
slot — `ail check` correctly accepts it. Renamed to
cut55_2b_borrow_traversal_clean and recast as the #58 false-positive
guard (a borrow-position use of a heap sub-binder must stay accepted).
cut55_1b similarly does not fire over-strict-mode (its recursive call
consumes the tail, so the lint's consume_count==0 premise fails) — comment
corrected; it is a plain accept. cut55_1c is the genuine over-strict-mode
example (accepts exit 0, emits the warning).
docs/specs/0065-eliminate-implicit-mode fieldtest report — moved 2c to
the reject set, added the 2b false-positive-guard section, marked the
double-free spec_gap RESOLVED (it shipped as the #58 fix).
Relates to #55.
|
||
|
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 (
|
||
|
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 |
||
|
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 |
||
|
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 |
||
|
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 |
||
|
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
|
||
|
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 |
||
|
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 |
||
|
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
|
||
|
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.
|
||
|
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 |
||
|
Brummel
|
04f75c8b71 |
test(codegen): RED-pin #49 Str leg — heap-Str loop binder must not leak across recur
A heap-Str accumulator threaded through a `(loop …)`/`recur` as a loop binder leaks: each iteration's superseded `str_concat` slab is never RC-dec'd, even when the loop's final result is consumed. The fixture reports `allocs=4 frees=1 live=3` under AILANG_RC_STATS (stdout `xyyy` is correct). Root (data-flow traced): the `Term::Recur` arm in crates/ailang-codegen/src/lib.rs (~2131) gates its superseded-value dec behind `!is_str`. That exclusion exists because a `Str` loop seed may be a static-literal Str — a constexpr GEP into a packed-struct global with no rc_header (lib.rs:1612) — and `ailang_rc_dec` on a static pointer reads garbage at `payload-8` and aborts on underflow (rc.c:221, no runtime guard, per design/contracts/0011-str-abi.md). So the Str binder's prior heap slab is overwritten by a plain `store` with no dec. Distinct from the loop-RESULT scope-close drop ( |
||
|
Brummel
|
61b9d3f513 |
test(raw-buf): RED-pin #51 — (new T <elem> …) must honour the element type-arg
Two failing E2E tests pinning the two legs of the #51 codegen crash, both rooted in the `Term::New` desugar dropping `NewArg::Type` (crates/ailang-core/src/desugar.rs:1053): - Leg 1 (legitimate): `(new RawBuf (con Int) 3)` used only via `RawBuf.size` — never observed by get/set, so the dropped `(con Int)` is the sole element-type carrier. The unpinned forall var defaults to Unit in mono and `ail build --alloc=rc` aborts on the unregistered `RawBuf_new__Unit` intercept. Pins build+run printing `3`. - Leg 2 (forbidden): `(new RawBuf (con Unit) 3)` — Unit is outside the param-in set {Int, Float, Bool}, but the dropped type-arg never reaches param-in enforcement, so `ail check` wrongly passes. Pins a `param-not-in-restricted-set` rejection naming Unit at check time. Both RED at HEAD. GREEN side carries the explicit element type from Term::New through to monomorphisation (must not mint __Unit) and adds the leg-2 reject pre-desugar per the Term::New/desugar lockstep. refs #51 |
||
|
Brummel
|
1b2d23ec42 |
fieldtest: raw-buf comprehensive — 4 examples, 8 findings (refs #7)
Comprehensive usability re-test of the RawBuf kernel extension in natural LLM-author decompositions the prior field test (0058) did not exercise: a Float RawBuf in a user ADT read through two borrow helpers, a Bool flag buffer filled with a computed value, an Int fib buffer whose fill reads its own writes plus two composed borrow summaries, and a forbidden core-primitive element. All three working fixtures build, run to expected values, and report live=0 across Float/Bool/Int widths — the core RawBuf surface (borrow-helper composition, fill loops, RawBuf-in-ADT, element widths) genuinely holds together. Orchestrator triage corrected the fieldtester's run, which executed a stale target/release/ail (built before the #50 fix). Every outcome was re-verified against a fresh build: - F2 (bare RawBuf ADT field unresolved) — RETRACTED: a stale-binary false positive. On a fresh build the bare name resolves in every configuration (ctor name == or != type name; builds/runs live=0). The #50 fix is correct and general. - F7 (NEW, issue #51) — a `check`-clean program crashes `build`: a buffer whose element type is never observed by a later get/set defaults its element to Unit in monomorphisation and hits an unregistered `RawBuf_new__Unit` intercept. Affects a legitimate `RawBuf<Int>` used only for its size AND a forbidden locally- constructed element. Root: the `(new T ...)` desugar drops the explicit element annotation; honouring it reverses the milestone's § Term::New desugar decision, so it routes through brainstorm. - F8 (process) — the field test ran stale; the fieldtester agent now builds from the current tree before running (plugin fix). F1 (spec_gap) resolved here: the design ledger's §Series substrate ctor wrote the storage field `(own (RawBuf a))`, which does not parse (`own` is fn-param/ret only). Rewritten to the verified-authorable `(con RawBuf a)`. The rest of the §Series listing is illustrative and its element- less `(new RawBuf lookback)` construction is entangled with #51; a full compile-verification of that listing belongs with the Series-substrate work. F5 (param-in rejects a forbidden core primitive, message names the set) and F4/F3 (borrow composition; substrate composite) carry on. F6 (param-in set rendered as a Rust-debug list) filed as #52. refs #7 |
||
|
Brummel
|
f488d314e8 |
fix(codegen): dec superseded heap loop-binder values across recur (ADT leg)
A heap value threaded through a `(loop ...)`/`recur` as a loop binder
leaked: the `Term::Recur` arm stored each new arg into the binder's
loop-carried alloca with a plain `store` and never RC-dec'd the heap
value already in that slot, so every iteration's superseded value was
lost. The scope-close drop path (drop.rs, commit
|
||
|
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 |
||
|
Brummel
|
d5cc6e96b6 |
docs(raw-buf): refresh fixture outcomes; ratify set non-enforcement (refs #7)
- rawbuf_1_score_table / rawbuf_2_running_max: the header OUTCOME blocks described the pre-fix breakage (does-not-check / unknown-variable). Those defects are fixed (B1 #46, B2 #47, B5); update the comments to the current state — both check, build, run to their expected values and are leak-clean under AILANG_RC_STATS. The files now serve as positive regression examples, not bug repros. - design/models/0007 §RawBuf: ratify the fieldtest's B4 spec_gap. The `own -> own` signature of RawBuf.set is a threading discipline, not runtime-enforced single-use; a double-consume of the same owned buffer aliases one slab (consistent with every owned value in the language). State that single-use is the author's responsibility and full linear enforcement is Issue #22 territory. Surfaced by the raw-buf fieldtest (docs/specs/0058). |
||
|
Brummel
|
8bcdae1b53 |
fix(codegen): drop a let-bound owned loop result at scope close
An owned heap value whose `let`-binding value is a `(loop ...)` result, afterwards only borrow-read (or unused), was never dropped at scope close — a memory leak (AILANG_RC_STATS live=1). Newly observable once #47 made fill-loops build: rawbuf_2_running_max leaked one buffer per run. Root cause: is_rc_heap_allocated — the predicate the let-lowering uses to decide a scope-close `dec` — matched only Term::Ctor, Term::Lam and Own-returning Term::App. A Term::Loop-valued binder fell through to false, so it was never registered for drop. (Sibling of the #47 synth gap: the Term::Loop arm under-handled in yet another pass.) Fix: add a Term::Loop arm that tracks the binder iff the loop's static result type lowers to llvm `ptr` (boxed/heap) AND is not Str — and widen drop_symbol_for_binder's App arm to cover Term::Loop so it resolves the per-type drop symbol. Two load-bearing safety gates: - the `ptr` gate excludes unboxed primitives (Int/Bool/Float/Unit), so an Int-returning loop is not handed to a drop fn; - Str is excluded because a loop can return a *static* Str (a seed literal threaded unchanged) and ailang_rc_dec on a static-Str pointer is UB; an Own-App can never return a static Str, which is why the App arm may track Str but the Loop arm must not. The loop's seed binders are consumed (moved in), so nothing else tracks the result; linearity guarantees no alias, so the new drop is single. Verified leak-clean and double-free-free across the fieldtest RawBuf set, the consumed case, the Int-gate case, and the escape case (a fn returning a loop-built owned RawBuf to its caller). The separate per-iteration leak of superseded heap loop-binder values (e.g. a Str accumulator threaded through recur) is a distinct, broader pre-existing bug, filed separately — not addressed here. RED-first: raw_buf_loop_no_leak_pin. |
||
|
Brummel
|
db710b1a73 |
fix(codegen): replay loop binders in synth_with_extras (closes #47)
A `let`-bound `loop` whose body references one of its own loop binders on the non-recur exit passed `ail check` but failed `ail build` with `unknown variable`. The fieldtest surfaced this with an owned RawBuf loop binder, but the trigger is element-type-independent. Root cause: the Term::Loop arm of synth_with_extras (the type-replay walk the let-lowering runs via synth_arg_type on every let value) descended into the loop body WITHOUT adding the loop binders to `extras`, unlike the Term::Let arm which pushes its binder. A loop binder referenced on the non-recur exit then resolved to UnknownVar during the type replay. Fix: clone `extras`, push each loop binder's (name, ty), and thread the augmented extras into the recursive synth of the body — mirroring the Term::Let arm exactly. General fix; a plain Int let-bound loop that references its binder also builds now. This restores check<->codegen agreement for the natural fill-loop (thread an owned buffer of runtime length through a loop/recur, one RawBuf.set per iteration) — the way to populate a buffer whose length is not a fixed set of literal indices. Surfaced by the raw-buf fieldtest (finding B2, docs/specs/0058). RED-first: loop_let_bound_binder_reference_builds. |
||
|
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. |
||
|
Brummel
|
8e9f0f06a6 |
fieldtest: raw-buf — 4 examples, 6 findings (refs #7)
Downstream field test of the raw-buf surface as a consumer with only the public interface (design ledger + `ail` CLI; no crate source). Four fixtures under examples/fieldtest/, spec at docs/specs/0058-fieldtest-raw-buf.md. Every recorded outcome reproduced independently before commit. Findings (3 bug, 1 spec_gap, 2 working): - B1 [bug] `borrow (RawBuf a)` receiver is unusable. A fn taking `borrow (RawBuf Int)` that calls RawBuf.get/.size on the parameter even once is rejected `consume-while-borrowed` — the diagnostic names the wrong cause (the receiver is not consumed). The ledger advertises get/size as borrow-receiver ops, so the documented use is unreachable from any helper-function decomposition. This blocks Series (#8) — the milestone's own downstream raison d'être — whose at/total_count read through a `borrow (Series a)`. - B2 [bug] An owned RawBuf threaded through a `loop` binder passes check but panics codegen `unknown variable: b` at build. A plain Int loop binder builds fine, so the fault is specific to an owned RawBuf loop binder. Breaks the check↔codegen agreement. - B3 [bug] `param-not-in-restricted-set` omits the allowed set. design/models/0007 §4 promises the diagnostic "names the offending type and the allowed set"; the shipped message names the type, the type-var, and the home type but not `{Int, Float, Bool}`. A downstream author is told what is wrong but not what is right. - B4 [spec_gap] RawBuf.set receiver double-consume is not enforced; two set calls on the same owned buffer silently alias the slab. Not raw-buf-specific (owned Str/ADT behave identically) — a pre-existing linearity-non-enforcement property. Recorded because RawBuf's own→own mutation is the first place a silent alias yields a mutated-in-place surprise. Ratify in the ledger or open a backlog item for full linear enforcement. - W1 [working] `(new …)` sugar + inference-from-use across Int/Float/Bool builds and runs first try (sensor_pair prints 5.0); the Bool i1/i8 packing edge round-trips. The milestone's cleanest win. - W2 [working] param-in reject fires for both Str and a user TypeDef. Net: B1+B2 mean the only RawBuf programs that build today are straight-line owned let-threading with literal indices — the shipped-fixture shape. Helper decomposition (B1) and runtime-length loop fill (B2) both fail. fieldtest does not self-resolve; routing is the orchestrator's call. |
||
|
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).
|
||
|
Brummel
|
0015f3dad1 |
spec: unique binder names per fn — A2b leg of RawBuf drop-leak (refs #43)
The last open leg of the #43 owned-heap drop-leak cluster is the
UniquenessTable shadow-name collapse: the side-table keys by
(def_name, binder_name), so a fn that shadows a binder name collapses
every shadow onto one key. The outermost binding (records last, on pop)
overwrites the inner ones; codegen's scope-close drop gates then read
the collapsed consume_count for the innermost binding and suppress its
drop, leaking the owned slab.
Spec 0056 resolves this as a compiler-internal naming collision — NOT
the deeper, separate problem of persistent AST provenance back to the
authored form (certain to be needed eventually, deliberately deferred;
conflating the two is a category error). Fix: alpha-rename shadowing
binders during desugar (reusing the existing fresh-name machinery that
already mints $mp_N / $lr_N), making the (def, name) key injective
again. No consumer of the uniqueness table changes — they all key by
name, and the name becomes a per-fn injective identity. IR-neutral:
codegen names heap by fresh SSA, never by source binder name. The
pre-desugar hashed form is untouched, so module identity and hash-pin
tests are unaffected.
RED fixtures securing the binder-kind class (the user's gating
condition before proceeding to the uniform-across-kinds fix):
- Let-shadow: the three raw_buf_{int,float,bool}_shadow_rebind tests
(already in tree, committed
|
||
|
Brummel
|
47efbdb5c0 |
test: RED owned-RawBuf drop-leak repro (refs #43)
raw_buf_owned_drop_balances_rc_stats + examples/raw_buf_drop_min.ail: a single owned 1-slot Int RawBuf, written once and read once. Prints 10 correctly but under AILANG_RC_STATS shows allocs=2 frees=1 live=1 — the slab leaks. Asserts stdout=="10" (green) and live==0 (RED until the owned-temp drop call is emitted). Root cause (verified, supersedes #42's disproven diagnosis). The leaked value is the anonymous owned temporary produced by RawBuf.set (own-ret, in-place: intercepts.rs emit_rawbuf_set_int does `ret ptr %b`, same slab as its input), then passed to RawBuf.get whose RawBuf param is `borrow`. After get borrows and returns an i64 the temp is dead, but no one drops it: codegen's only two scope-close drop emitters cover Term::Let binders (lib.rs:1785-1822) and Own fn-params (lib.rs:1426-1502); the general call lowerer emit_call (lib.rs:2552) splices args without inspecting per-arg own/borrow modes and emits no post-call drop for an owned arg landing in a borrow slot. Binder-independent, contra #42: the fully inline form with no `let` at all produces byte-identical leaking IR (no Term::Let exists, so the 1785 gate is never reached). The defect is the drop-CALL-site emission raw-buf.4 deferred to raw-buf.5; uniqueness.rs is not implicated. |
||
|
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
|
||
|
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). |
||
|
Brummel
|
6ccc756c0f |
audit + close: intrinsic-bodies — honest prelude docs + lockstep table + stale-model fix (refs #9)
Milestone close for intrinsic-bodies (.1 mechanism |
||
|
Brummel
|
caa3618c3e |
iter intrinsic-bodies.2-migration-lock (DONE 4/4): prelude → (intrinsic) + bijection pin (refs #9)
Second and final iteration of the intrinsic-bodies milestone. Migrates
the 13 authored prelude dummy bodies to (intrinsic), rebaselines the two
hash pins that move, and locks the registry to the source with a
bijection. Behaviour-preserving: the codegen intercepts emit identical
IR; the prelude placeholder bodies were already dead (intercepted by
name before lower_term, since raw-buf.1).
What landed (4 tasks):
Task 1 — examples/prelude.ail: 13 authored dummy bodies → (intrinsic).
7 Eq/Ord instance methods (eq Int/Bool/Str/Unit, compare
Int/Bool/Str) keep their lambda shell (params/ret = the method's
local signature, Design X); the inner (body false)/(body true)/
(body (term-ctor Ordering EQ)) becomes (intrinsic). 6 float_* fns
((body false) → (intrinsic) in the fn body slot). The honesty-rule
infraction the milestone exists to fix is now closed: no prelude
body lies about what runs.
Task 2 — hash rebaselines (the prelude bytes changed):
prelude module hash af372f28c726f29f → 2ea61ef21ebc1913
eq__Int 86ed4988438924d3 → cc7b99b63d1e44ae
eq__Bool d62d4d8c51f433f8 → fd0412f127986512
eq__Str 3d32f377c66b03e0 → fa269285754a52da
compare__Int 6d6c20520766368b → 0a02bd9effc9746c
compare__Bool 02b64e8fadc913eb → d0dc108dacf4e543
compare__Str 9645929d53cd3cc9 → d1419595dc52a456
The 4 show__* mono pins did NOT move (Show bodies are real).
Task 3 — intercepts.rs: registry_contains_all_legacy_arms (one-
directional, hardcoded 18-name list) replaced by
intercepts_bijection_with_intrinsic_markers. The in-source test
walks prelude + kernel_stub pre-mono for Term::Intrinsic markers,
recovers each marker's codegen symbol (mono_symbol(method, type) for
instance methods; the fn name for top-level float_*/answer), and
asserts a bijection over the intrinsic-backed class: (A) every
marker resolves to an INTERCEPTS entry, (B) every INTERCEPTS entry
not on the optimisation-only allowlist has a marker, plus a guard
that the allowlist names are themselves registered. The allowlist is
the 5 *__Int icmp-family entries, which intercept the monomorphised
specialisation of the real-bodied polymorphic lt/le/gt/ge/ne — an
optimisation, not a compiler-supplied body, so no marker. The pin
passing independently confirms Task 1 missed no prelude site.
Task 4 — confirmed no codegen path lowers an intercepted body (already
true since raw-buf.1: try_emit_primitive_instance_body matches by
name before f.body is inspected). Refreshed the now-accurate comment
at lib.rs:1310-1319. design/contracts/0007-honesty-rule.md needed NO
edit — it is a general present-tense rule and does not name the
prelude dummies (confirmed by grep), so editing it would have been
invented work.
Verification:
cargo test --workspace → 669 passed, 0 failed (post-.1 baseline held;
one test replaced net-0).
Behaviour-preservation ratifiers GREEN (the safety net):
eq_primitives_smoke_compiles_and_runs,
compare_primitives_smoke_prints_1_2_3_thrice (e2e.rs);
float_compare_smoke_prints_true_true_false (float_compare_smoke_e2e.rs);
eq_ord_polymorphic_runs_end_to_end (eq_ord_e2e.rs).
Bijection pin GREEN. Both hash pins GREEN at the new baselines.
bench/check.py + compile_check.py → 0 regressed.
Plan-text imprecision (no outcome impact, noted for the record): Task 1
Step 5 wrote `--test e2e` for all four ratifiers, but
float_compare_smoke_prints_true_true_false and
eq_ord_polymorphic_runs_end_to_end live in their own test targets
(float_compare_smoke_e2e.rs, eq_ord_e2e.rs). The verification-filter
self-review checked that the fn names exist, not that they sit in the
named target — a sharper form of the filter-zero discipline. The
implementer ran each in its real target; all four green.
Milestone intrinsic-bodies is now feature-complete (.1 mechanism +
.2 migration+lock). Audit + close follow.
|
||
|
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.
|
||
|
Brummel
|
aa49a56d5a |
fieldtest: kernel-extension-mechanics — 6 examples, 9 findings (3 bugs, 1 friction, 1 spec_gap, 4 working)
Post-audit fieldtest for the kernel-extension-mechanics milestone. Fieldtester wrote 6 .ail consumer programs against the public interface only (design ledger + spec + ail CLI; no source crate reads), one per axis with two for the param-in pair (accept + reject). All artefacts in examples/fieldtest/ + the spec. **Working (4):** F5 NewTypeNotConstructible diagnostic is precise (names the home module + missing def in one sentence). F6 Term::New codegen-deferral diagnostic explicitly names the raw-buf milestone where support lands. F7 param-in accept-path is end-to-end (check + build + run prints 17). F8 ParamNotInRestrictedSet names type-arg + var + TypeDef. **Bugs (3, action: debug):** - F1 (axis 1) — Same-module type-scoped call `(app Type.member …)` rejected with phantom-qualified `expected <this>.T, got T`. Bare `(app member …)` from inside Type's home module works. Spec's "Canonical form decision" promises type-scoped works uniformly; the resolver appears to disagree with the workspace pre-pass on whether `<this-module>.T` equals bare `T`. Repro: examples/fieldtest/kem_2b_min_repro.ail. - F3 (axis 3) — Kernel-tier auto-import scopes the name but does not register the module as a resolvable qualifier prefix. Per the pre-pass, a bare `StubT` in a type slot is qualified to `kernel_stub.StubT`; the resolver then rejects `kernel_stub` as unknown. Asymmetric: prelude's free fns work (per prelude_free_fns.rs), but the stub's TypeDef is effectively unreachable from any consumer. Repro: examples/fieldtest/kem_3_stub_consumer.ail. - F4 (axis 3, spec/ship coherence) — The spec's prep.3 worked- consumer relies on `(new StubT 42)`, but the shipped STUB_AIL has only a TypeDef + ctor — the `(fn new ...)` the spec designed is missing from the implementation. The diagnostic the resolver does emit on the consumer (F5) is precise; the bug is the absent def itself. Resolution: re-add the `new` to STUB_AIL (the spec's design), refresh the drift pin. **Friction (1, action: plan-or-defer):** - F2 — Loader's sibling-only module resolution forces symlinks for any cross-module fixture sitting outside the canonical `examples/` directory. The kem_1 example required local symlinks for std_list.ail + std_maybe.ail. Secondary: the diagnostic message names only the .ail.json path even though .ail also resolves — actively misleading. Recommended: small tidy iter for loader workspace-search-path + diagnostic clarity. **Spec-gap (1, action: ratify):** - F9 — `design/models/0007-kernel-extensions.md:80` uses `unit` as a value literal of type Unit; the checker treats it as a Term::Var lookup and emits [unbound-var]. Either ratify `unit` as the canonical Unit-value literal in the language, or tighten the design model to use the existing idiom. The current model/ surface disagreement is a small but real LLM-author trap. **Symlinks committed** as evidence of the F2 workaround: examples/fieldtest/std_list.ail and std_maybe.ail are symlinks into ../. They are the fingerprint of the friction — removing them silently would erase the evidence. Per Iron Law, fieldtester did not work around bugs — they were all surfaced and recorded. The kem_2b_min_repro.ail fixture exists specifically because F1 surfaced mid-drafting and got minimised; kem_3_stub_consumer.ail also stays as the F3 RED-side fixture. Triage (next-step routing for /boss): F4 → small inline fix (add (fn new ...) to STUB_AIL + drift refresh) F9 → small inline ratify (whitepaper edit) F2 → backlog issue, deferred (single tidy iter someday) F1, F3 → debug skill dispatches, then implement mini-mode F5-F8 → carry-on, recorded as wins |
||
|
Brummel
|
de4399df37 |
audit + close: kernel-extension-mechanics — latency-arm restoration + p99 jitter-metric removal (ratify)
Audit Step 2 (regression scripts) blocked at exit 2 on bench/check.py
— the latency arms produced lines=0 because their fixtures rely on
`(app print N)` to deliver one newline per sample, but the
io/print_str byte-faithful change (commit
|
||
|
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.
|
||
|
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.
|
||
|
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. |
||
|
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
|
||
|
Brummel
|
26fb3459d8 |
GREEN: io/print_str byte-faithful via @fputs(@stdout) — closes #29
The runtime print path now writes exactly the bytes of its
argument with no implicit trailing newline. `io/print_str` is
byte-faithful; authors who want a newline emit `(do io/print_str
"\n")` themselves.
## Codegen
`crates/ailang-codegen/src/lib.rs`:
- Module preamble: `@puts(ptr)` → `@fputs(ptr, ptr)` plus
`@stdout = external global ptr` (libc's `FILE *stdout`).
- Effect-op lowering for `io/print_str`: emit
`getelementptr +8` then `load ptr, ptr @stdout` then
`call/tail call i32 @fputs(ptr bytes, ptr fp)`. Identical
bytes-pointer GEP, distinct sink.
- The pinned IR-shape test renames from
`print_str_calls_puts_with_bytes_pointer` to
`print_str_calls_fputs_with_bytes_pointer_and_stdout` and now
asserts: bytes-GEP present, stdout-load present, both module-
preamble declarations present, and no `@puts(` call anywhere
in the emitted IR.
## Why this shape, and not the alternatives
- *Rename `io/print_str` to `io/println_str` (issue #29 option 2)*
— kept the auto-newline, just relabelled it. AILang's design
bias is explicit-over-implicit (CLAUDE.md: implicit conversions
cut). Auto-newline is a hidden runtime augmentation; the rename
would have preserved it. Rejected.
- *Append `\n` inside the polymorphic `print` (Show-mediated)
function in `examples/prelude.ail`* — would have been a one-line
fix. Rejected: `print` is the Show-mediated formatter, not a
newline emitter; baking a newline into it would have re-imposed
the same implicit-augmentation problem one layer up, breaking
callers that legitimately want pure-bytes output.
## Fixture / test sweep
30 `.ail` fixtures whose owning tests asserted line-separated
stdout now emit explicit `(do io/print_str "\n")` after each
print. Tests that asserted on multi-line stdout (`show_print_e2e`,
`floats_e2e`, `str_concat_e2e`, `eq_ord_e2e`, several `print_*`
smoke tests) had their fixtures sweetened the same way; assertions
themselves remain the canonical observable output. Fixtures that
never relied on the newline (no test ever read the absence of one)
were left untouched.
## Migrated metadata
- `crates/ailang-core/tests/hash_pin.rs`: the `ordering_match::main`
canonical hash is refreshed (`b65a7f834703ffb4` →
`8ed47b4062ce00f5`). The comment now names both successive
corpus migrations honestly: the per-type-print-retirement (which
moved `(do io/print_int x)` to `(app print x)`) AND this
fputs swap (which wrapped that with `(seq ... (do io/print_str
"\n"))`).
- `design/contracts/str-abi.md`: the consumer-ABI table now lists
`@fputs` as the print sink. A prose paragraph documents the
byte-faithful semantics and references this issue.
- `examples/ordering_match.prose.txt`: regenerated from the
updated `ordering_match.ail`.
- `crates/ail/tests/snapshots/{hello,sum,max3,list,ws_main}.ll`:
IR snapshots regenerated via `UPDATE_SNAPSHOTS=1`.
- Stale `@puts` comments in `runtime/str.c`,
`crates/ail/tests/{e2e,show_print_e2e,print_no_leak_pin}.rs`
replaced with `@fputs`.
## Verification
- `cargo test -p ail --test print_str_no_auto_newline_e2e` — both
RED tests from commit
|
||
|
Brummel
|
c8ecfa39b9 |
RED: io/print_str must print exactly the bytes of its argument — refs #29
Two RED E2E tests that pin the byte-faithful-print property of io/print_str. Both fail today because the codegen at crates/ailang-codegen/src/lib.rs:2754 lowers the op to a C `@puts` call, which writes the string plus a trailing newline. - io_print_str_does_not_append_auto_newline: (seq (do io/print_str "a") (do io/print_str "b")) → stdout "ab" current: "a\nb\n" - io_print_str_does_not_double_embedded_newline: (do io/print_str "x\n") → stdout "x\n" current: "x\n\n" Assertions compare RAW stdout (no .trim()) — the byte-level property IS the assertion target. Empirically caught in the cross-model-authoring naming-A/B run on 2026-05-21 (experiments/2026-05-21-naming-ab/runs/r1/): Qwen3- Coder repeatedly wrote `(do io/print_str "text\n")` with explicit \n, expecting byte-faithful output, and got doubled newlines — failing every t3_main_prints stdout match across all three cohorts. GREEN side (codegen swap @puts → fputs(s, @stdout) + sweep of existing fixtures that implicitly relied on the auto-newline) is the next commit, via implement mini-mode. refs #29 |
||
|
Brummel
|
505eb8484e |
fieldtest: operator-routing-eq-ord — 5 examples, 6 findings (4 working, 1 friction, 1 spec_gap)
Post-audit field test of the operator-routing-eq-ord milestone (closed via |
||
|
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 |
||
|
Brummel
|
14a91f0ae5 |
iter boehm-retirement.1 (DONE 10/10): retire the transitional Boehm GC backend
Closes Gitea #4. Removes the Boehm-Demers-Weiser conservative GC backend wholesale across six layers in one atomic iteration. After this iter, `AllocStrategy` has two variants (`Rc`, `Bump`), `--alloc=gc` is rejected at CLI parse with `unknown --alloc value`, the libgc link arm is gone, and the design ledger describes RC (canonical) + bump (raw-alloc bench-floor) as the only allocators. Layer-by-layer summary: CLI surface — `crates/ail/src/main.rs`: `parse_alloc_strategy` arm `"gc" => Ok(AllocStrategy::Gc)` removed; error wording updated to `(expected `rc` or `bump`)`; clap-derive `value_parser = ["gc","bump","rc"]` allowlist on BOTH `Build` and `Run` subcommands DROPPED so that `parse_alloc_strategy` remains the sole gatekeeper for the unknown-value diagnostic (otherwise clap shadows the runtime diagnostic with `invalid value 'gc' for '--alloc'`, which would miss the milestone-pin's stderr substring check). The `default_value = "rc"` stays. Codegen — `crates/ailang-codegen/src/lib.rs`: `AllocStrategy::Gc` variant + `Default` derive removed (no caller of `AllocStrategy::default()` existed in the workspace, so the trait derivation was dead). `fn_name` (spec called it `runtime_alloc_fn` loosely; actual identifier is `fn_name`) drops the `Gc => "GC_malloc"` arm. `lower_workspace` and `lower_workspace_staticlib` defaults flip from `Gc` to `Rc`. In-source negative-complement codegen test (mod tests, lib.rs:3571ff) retargets from `AllocStrategy::Gc` to `AllocStrategy::Bump` (bump also doesn't emit per-type drop fns; the test's semantic "no drop fns under non-RC" is preserved). Link branch — `crates/ail/src/main.rs:2389ff`: The `match strategy { AllocStrategy::Gc => { ... cmd.arg("-lgc"); ... } }` arm and its libgc-link block are entirely gone. The surviving match exhausts on `Bump` and `Rc` (Rust's exhaustiveness check confirms; no `error[E0004]`). Staticlib-guard diagnostic rewritten to drop the "shared Boehm collector" phrasing while preserving the prefix `staticlib (swarm) artefact is RC-only` verbatim (the surviving `staticlib_bump_is_rejected` test depends on that substring). Test suite — 3 pure-differential e2e tests deleted (`gc_handles_recursive_list_construction`, `alloc_rc_produces_same_stdout_as_gc`, `alloc_rc_matches_gc_on_std_list_demo`); 9 RC-feature tests stripped of their `stdout_gc` build call and differential `assert_eq!(stdout_gc, stdout_rc, ...)` (absolute `assert_eq!(stdout_rc.trim(), "<n>")` pin retained as correctness oracle); `staticlib_gc_is_rejected` deleted; new milestone-pin `crates/ail/tests/boehm_retirement_pin.rs` asserts `ail build --alloc=gc` exits ≠ 0 with stderr containing `unknown --alloc value` and `\`gc\``; `examples/gc_stress.ail` fixture deleted (no remaining references). Implementer expansion (not in plan): `iter17a_local_box_alloca` (in `e2e.rs`) carried an IR-shape assertion against `@GC_malloc`-absence as the witness for non-escaping allocation. After the Task-2 codegen default flip, the witness shifts to `@ailang_rc_alloc`-absence in escape-targeted positions; assertion + doc-comment updated. Property protected ("no heap allocation in non-escaping contexts") is unchanged; only the named allocator shifts. Bench harness — `bench/run.sh` 9→6 column compaction (workload + bump(s) + rc(s) + rc/bump + bump RSS + rc RSS); gc-arm `bench_latency_implicit_gc` build call + harness invocation dropped from latency block; header comment reframed from "GC-overhead bench harness" to "RC-overhead bench harness"; "Decision 10's Boehm-retirement target (1.3x)" rewording to "RC-overhead-vs-bump bench-health regression gate". `bench/check.py:62` header-sentinel changes from `"gc(s)" in line` to `"bump(s)" in line`; column-count check at `:72` flips from `!= 9` to `!= 6`; per-workload field set drops `gc_s`/`gc_over_bump`/`gc_rss_kb`; `ARM_LABEL_TO_KEY` drops the `"implicit @ gc": "implicit_at_gc"` entry. `bench/baseline.json` regenerated via `--update-baseline`. Implementer note (planner-defect): `write_new_baseline` iterated over the *existing* baseline's metric list when emitting the regenerated file, so even after parser-level `gc_*` removal, the fallback emitted them back into the JSON. Scrubbed post-update; the cleaner fix (have `write_new_baseline` emit only keys present in `parsed_throughput[workload]`) is a follow-up if the script becomes load-bearing for further allocator changes. Design ledger — `design/models/rc-uniqueness.md` excises the `## Dual allocator — RC canonical, Boehm parity oracle` section and the `Boehm-Demers-Weiser conservative GC` choice block + rationale + trade-offs; the per-fn-alloca section generalises Boehm-specific language to allocator-agnostic; the memory-model section's `## Choice.` paragraph reframes the 1.3× target from "Boehm-retirement gate" to "bench-health regression gate". `design/models/pipeline.md` drops the `--alloc=gc → links libgc` arm of the pipeline diagram and replaces it with `--alloc=bump → links bump-floor`; the accompanying prose rewrites accordingly. `design/contracts/scope-boundaries.md` rewrites the "Memory management via Boehm conservative GC" bullet to describe RC + per-fn-arena present-tense; the dead reference to `examples/gc_stress.ail.json` (file never existed; the fixture only ever had a `.ail` form, deleted by this iter) is dropped along with the `examples/std_list_stress.ail.json` reference whose purpose was Boehm-only soak testing. `:67`'s `@printf` / `@GC_malloc` parenthetical updated. `design/contracts/memory-model.md:232` drops the "leaks like the pre-Boehm era" phrase; the RC inc/dec instrumentation is wired up, so the "until then" conditional that referenced pre-Boehm is closed. `design/contracts/embedding-abi.md:42-44` rewrites the staticlib-guard prose to drop the `--alloc=gc` clause (gc is now a CLI-parser-level unknown-value, not a staticlib-guard rejection) and reframe the swarm-safety justification around `--alloc=bump` (leak-only bench instrument) rather than the historical Boehm collector. Honesty pin — `crates/ailang-core/tests/docs_honesty_pin.rs` inverts the polarity: the present-tense Boehm-anchor assertion on `pipeline.md` (`:116-117`) is deleted, and four absence-pins are added to `design_md_has_no_wunschdenken` against the Boehm-zombie strings `transitional Boehm`, `parity oracle`, `GC_malloc`, `libgc`. The `design_corpus()` already includes `rc-uniqueness.md` so no path-list change was needed for the new pins to scan. `crates/ailang-core/tests/design_index_pin.rs:166` drops the `"pre-Boehm"` token from the protected-exception comment list (the phrase no longer appears in `memory-model.md` after this iter, so the exception is dead). Runtime docs — `runtime/bump.c`, `runtime/rc.c`, `runtime/str.c` header comments scrubbed of Boehm/`GC_malloc`/`libgc` references. `bump.c`'s function signature description still documents `void *bump_malloc(size_t)` as the bench-floor allocator interface, but no longer cross-references libgc. Example fixtures — `examples/bench_latency_implicit.ail`, `bench_latency_explicit.ail`, `escape_local_demo.ail`, `reuse_as_demo.ail`, `rc_pin_recurse_implicit.ail` doc-comment headers scrubbed of `--alloc=gc` / Boehm references. The `.ail` surface (AST) is untouched in every case; round-trip invariant holds (`cargo test -p ailang-surface --test round_trip` green). Skill / agent prompts — `skills/audit/agents/ailang-bencher.md` rewritten to use an RC-vs-bump worked example pattern for the hypothesis-driven bench tutorial, replacing the recurring "RC vs Boehm under heap pressure" example. `skills/implement/agents/ailang-implementer.md` Decision-10 / Boehm references replaced with present-tense RC-commitment framing. IR snapshots — the 5 checked-in snapshots (`crates/ail/tests/snapshots/{hello,list,max3,sum,ws_main}.ll`) regenerated via `UPDATE_SNAPSHOTS=1 cargo test -p ail --test ir_snapshot`. Each previously contained `declare ptr @GC_malloc(i64)` and (for `list.ll`) a `call ptr @GC_malloc(...)` invocation; post-flip the snapshots contain `declare ptr @ailang_rc_alloc(i64)` plus the rc inc/dec runtime declarations. Spec-vs-acceptance addendum (caught at orchestrator end-report, absorbed here rather than in a follow-up spec edit): spec §6 acceptance criteria said "Boehm-grep returns matches ONLY in docs_honesty_pin.rs". The plan itself prescribed historical Boehm references in 3 additional files: (a) the new milestone-pin `boehm_retirement_pin.rs` (must literally invoke `--alloc=gc` to assert its rejection), (b) `embed_staticlib_alloc_guard.rs` file doc-comment historical note ("`--alloc=gc` no longer exists as a CLI value"), (c) `embedding-abi.md:44-45` contract historical clause ("see the Boehm-retirement iter"). All three are prescribed; the spec's grep wording was too narrow. The four absence-pins in `docs_honesty_pin.rs` catch the actual zombies (Boehm-narrative re-emerging in the design ledger), which is the substantive intent the spec was aiming at — the four extra documented-by-design exceptions are the cost of having an explicit milestone-pin and contract-level historical anchors. Net delta: - 32 files modified, 2 new (boehm_retirement_pin.rs + stats), 1 deleted (gc_stress.ail); - workspace tests: every binary `0 failed`. Pass-count delta: -3 net (4 e2e tests deleted, 1 new milestone-pin test added); - boehm-grep state: hits only in the four by-design exceptions documented above; - `bench/check.py` exit 0 against regenerated baseline; - CLI must-fail fixture: `ail build --alloc=gc examples/hello.ail` exits non-zero with stderr containing `unknown --alloc value` and `\`gc\``; - design ledger present-tense honest (Boehm-narrative gone from `rc-uniqueness.md` + `pipeline.md`; the few historical references in `embedding-abi.md` / `boehm_retirement_pin.rs` / `embed_staticlib_alloc_guard.rs` are explicit milestone-pins or contract anchors, not silent ledger residue). Bench measurement variance noted: closure-chain and hof-pipeline are ±1-5% jittery between runs; one regeneration flagged 2 metrics as `regressed` before a second run returned 0. The captured baseline is within self-comparison range. Existing per-metric tolerances absorb the jitter. Stats file: `bench/orchestrator-stats/2026-05-20-iter-boehm-retirement.1.json`. closes #4 |
||
|
Brummel
|
7a42989b34 |
iter nullary-app.1 (DONE 5/5): accept (app f) as canonical zero-arg call
Resolves Gitea #12 — the design fork from the 2026-05-20 /boss session, surfaced independently by two prior fieldtests (mut-local F3 + loop-recur `run_forever`). Mechanics, layer by layer: Parser — `crates/ailang-surface/src/parse.rs:1322-1331` drops the 4-line `expected at least one argument` guard in `parse_app_body`. Grammar comments at file top change `term+` to `term*` on both `app-term` and `tail-app-term`; doc comment on `parse_app_body` changes `1+ args` to `0+ args`. Inline comment cites #12 and notes which layers below already accept empty args. Serde — `crates/ailang-core/src/ast.rs:419-425` annotates `Term::App.args` with `#[serde(default)]`, mirroring `Term::Ctor.args`'s *actual* attrs verbatim (no `skip_serializing_if`). Write behaviour unchanged — canonical JSON still emits `"args":[]` for nullary calls; only read behaviour gains tolerance for the `args` key being absent. Verified hash-impact-free at plan time: `grep -rn '"args":\[\]' examples/*.ail.json` returns zero matches, so no existing fixture's canonical bytes shift. Doc-honesty — `design/contracts/data-model.md`: (a) the `app` jsonc shape gains an explicit "args may be empty / read-tolerant" note; (b) the existing `ctor` comment claiming "args omitted when empty" was factually false (Ctor.args has no `skip_serializing_if`; a serde probe at plan time confirmed writes always emit `"args":[]`). Rewritten to describe the actual write/read asymmetry, with a cross-reference to the new `app` note. E2E pin — `crates/ail/tests/nullary_app_e2e.rs` + `examples/nullary_app_smoke.ail`. Defines `greet : fn() -> Unit !IO` and calls it as `(app greet)`; asserts stdout `"hello\n"`. RED→GREEN pin for the parser change AND the milestone-protecting E2E for nullary call surface going forward. Fixture literal is `"hello"` (no `\n`) because `io/print_str` lowers via `puts` which appends a newline — the plan body had a `"hello\n"` literal which would have yielded `"hello\n\n"`; the implementer caught and aligned to the canonical pattern in `examples/hello.ail` while writing the fixture, fix scoped to that single file. Layers below parser untouched: typechecker's arity check at `crates/ailang-check/src/lib.rs:3300` is `args.len() != params.len()` which is `0 != 0 → false` for nullary; codegen's `args.iter().zip(sig.params.iter())` at `crates/ailang-codegen/src/lib.rs:2410` is an empty loop; LLVM `call @ail_<mod>_<name>()` with empty arglist is valid; surface printer's arg-emit loop at `crates/ailang-surface/src/print.rs:430-434` writes nothing for empty args, producing exactly `(app f)`. Verification: full workspace `cargo test --workspace --quiet` green (0 failed across all crates); drift pins `design_index_pin 5/5` + `design_schema_drift 8/8`; round-trip `2/2`; new `nullary_app_e2e 1/1`. Stats file: `bench/orchestrator-stats/2026-05-20-iter-nullary-app.1.json`. closes #12 |