9b0eb58cd91648846072ad080f7ac9a4a16627ec
396 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
 Brummel
|
9b0eb58cd9 |
refactor(surface): share the copy-pasted parser sub-productions
Round-trip-preserving — the byte-isomorphic Form-A ↔ JSON-AST tests, the hash pins, and the full fixture-corpus parse are all green; error strings passed through verbatim, not homogenised. - The Int/Float/Str/true/false literal-token match was inlined in three parsers; extracted try_parse_literal_token and routed parse_pat_lit and the parse_term fallthrough through it. - parse_doc and parse_export were identical but for the keyword; both now go through one parse_string_attr, and the previously doc/export-bypassed expect_string helper is back on the shared path. - parse_effects_clause and parse_forall_constraints_clause shared the expect-keyword / collect / reject-empty / expect-rparen shape; unified under parse_repeating_clause, with each clause's empty-error message passed in. parse_intrinsic_attr was left inline-able-but-not-inlined: it has two call sites, so inlining would re-duplicate a documented helper. |
||
|
Brummel
|
e5534d1532 |
refactor: clear clippy code lints across the workspace
Machine-applicable clippy fixes plus three by-hand cleanups; all semantics-preserving (full workspace test suite green). Auto-applied (cargo clippy --fix): - dropped `.clone()` on the Copy type ParamMode (ret_mode/param_mode) - map_or(false, p) -> is_some_and(p) - removed redundant closures and an explicit .into_iter() - useless format!, a needless deref, an as_bytes-after-slice By hand: - ailang-codegen: named the loop-frame tuple types (LoopFrame / LoopBinderSlot) instead of the bare nested Vec<(String, Vec<(String, String, String, Type)>)>, clearing the type-complexity lint and documenting what each slot holds. - ailang-check: collapsed the two identical pass-through arms of the Type-Con qualifier (already-dotted / primitive) into one `||` guard. - ailang-core: converted a stale `///` block (it described a test that was relocated, documenting nothing) back to a plain `//` comment. Remaining clippy output is 16 markdown list-indentation nits in prose doc comments — doc formatting, not code, left for a docs pass. |
||
|
Brummel
|
d5e69148c6 |
refactor(check): unify the two Type-Con qualifiers over an is-local predicate
qualify_local_types and qualify_workspace_types were two ~55-line recursive Type rewriters identical in every arm (Con skip-guards for already-dotted and primitive names; Fn/Var/Forall recursion) except the bare-name decision: the local form rewrites iff the name is in local_types; the workspace form leaves names own to the module bare and otherwise searches module_types for the defining module. Factor the recursion into one rewrite_type_cons that takes the bare- name decision as a `&dyn Fn(&str) -> Option<String>` (Some = rewrite to this qualified name, None = leave bare). The two public functions are now thin wrappers passing their respective closure. Recursion order and Con-arm check order are preserved exactly; cross-module qualification tests green. |
||
|
Brummel
|
7d9ab4d29d |
refactor(codegen): parameterise the copy-pasted IR-emission families
Emitted IR is byte-identical for every case — proven by the IR-pin
suites (eq_primitives_pin, ord_int_intercept_ir_pin, the raw_buf_*
and drop/leak pins) and the full e2e suite, all green.
intercepts.rs:
- The twelve emit_rawbuf_{new,get,set,size}_{int,float,bool} functions
were copy-paste across three element types, differing only in the
element width (8/8/1) and the LLVM load/store type (i64/double/i1).
Collapsed to four parameterised cores; the element variants are thin
call sites passing the (width, type) pair.
- Replaced the repeated, off-by-one-prone parameter-SSA extraction
idiom (`locals[n-2]`, `locals[n-1]`) with an Emitter::last_param_ssas
helper.
- Factored the shared IR-Str bytes GEP out of emit_eq_str /
emit_compare_str into emit_str_bytes_gep.
drop.rs:
- The three emit_*_drop_fn_for_type methods shared one wrapping shape
(monomorphic short-circuit, else loop over instantiations dispatching
to a *_for_instantiation helper); hoisted into emit_drop_fn_wrapper
taking the per-instantiation emitter as a fn pointer.
- emit_flat_intrinsic_drop_fn / _partial_drop_fn differed only in the
symbol prefix and an ignored mask param; merged into one inner
emitter.
No INTERCEPTS-registry or (intrinsic)-marker changes.
|
||
|
Brummel
|
7ae92d3e60 |
refactor(test): hoist duplicated test helpers into ailang-test-support
closes #60 The fixture-corpus filter (NON_PARSEABLE_FIXTURES + list_ail_fixtures) was copy-pasted across three test crates and drifted out of sync as new reject fixtures landed; the examples_dir / workspace_root path walk was reimplemented ~30 more times across the suite, under two spellings (workspace_root / ws_root). Introduce crates/ailang-test-support — a zero-dependency, dev-only leaf crate — as the single home for these helpers: - NON_PARSEABLE_FIXTURES, list_ail_fixtures - workspace_root, examples_dir - canonical_workspace_root (symlink-resolved variant, for the tsan/ race tests that feed the root into native build steps) All integration-test copies across ailang-core, ailang-surface, ailang-prose, ailang-check, and ail now import from the shared crate; the local definitions and their now-orphaned path imports are removed. Path helpers resolve via the support crate's own CARGO_MANIFEST_DIR, so they return the correct absolute paths from any caller. ail_bin helpers are intentionally left in place: they depend on env!("CARGO_BIN_EXE_ail"), which Cargo only defines when compiling the ail crate's own integration tests, so they cannot move to a shared crate. Behaviour-identical: same paths, same fixture lists; full workspace test suite green. Net -177 LOC. |
||
|
Brummel
|
ac9171ebf0 |
refactor: collapse duplicated helpers and drop dead code across check/core/codegen
Pure simplification pass, no behaviour change — hashes, canonical forms, diagnostic codes, and emitted IR are byte-identical (hash-pin and IR-pin tests unchanged and green). ailang-check: - strip_forall and collect_pattern_binders were triplicated verbatim across linearity.rs / reuse_shape.rs / uniqueness.rs; hoisted each to a single pub(crate) fn in lib.rs. - mono.rs::pattern_binders was a fourth copy of collect_pattern_binders (iterative style, same result for every Pattern shape); deleted, now calls the shared fn. - maybe_instantiate and expect_eq were single-call wrappers; inlined at their sole call sites and removed. ailang-core: - collect_used_in_pattern was a verbatim duplicate of pattern_binds; deleted, call site repointed. pattern_binds made private (no external callers; the doc-comment's lift_letrecs claim was stale). - is_false serde helper replaced by std::ops::Not::not at the four skip_serializing_if sites (all plain-bool fields); helper removed. - test-only any_nested_ctor / any_let_rec folded into one generic any_term(t, &pred) walker. - removed dead test helpers tmp_dir / examples_dir, orphaned when their tests relocated to tests/workspace_pin.rs. ailang-codegen: - removed the write-only Emitter::types field, its populating loop, and the now-unused CtorInfo struct it fed. - adt_drop_symbol / adt_partial_drop_symbol differed only in a prefix literal; folded into one adt_symbol(prefix, ...). Symbol strings unchanged. Net -180 LOC. |
||
|
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
|
19757480b7 |
audit(0064/cutover): record shipped drop machinery + retire dead desugar arm
Cycle-close tidy for the #55 cutover (its audit drift-resolution). Architect drift review found the design ledger out of step with the codegen that the cutover shipped, plus two debt items; regression green (733 passed / 0 failed across the workspace). design/contracts/0008-memory-model.md — the Codegen contract described the drop-emission *gates* but not the drop machinery the cutover landed. Added three subsections recording the present state (honesty rule): - Per-monomorph drop fns for polymorphic ADTs (crates/ailang-codegen/ src/dropmono.rs: collect_drop_monos / DropAdtMeta, the suffix scheme, value-field-skip on the substituted field type). Ratified by alloc_rc_value_type_field_is_not_rc_dec_dropped. - String-literal rep promotion at owned drop sites (StrRep::Static→Heap on a Str literal flowing into an Own slot the callee drops; gated strictly on Own). Ratified by own_str_literal_arg_is_dropped_exactly_once. - Same-constructor arm grouping in match desugar (build_chain / build_ctor_group bind ctor fields once). Ratified by lit_pat_ctor_tail_drop_single_drop + lit_pat_nil_scrutinee_single_drop. crates/ailang-core/src/desugar.rs — build_chain routes every Ctor-head arm (including a length-1 run) through build_ctor_group, so desugar_one_arm's Pattern::Ctor arm was unreachable dead code duplicating the bind-once lowering. Replaced it with unreachable! naming the invariant, and corrected two stale doc comments (the module-header step 4 and the desugar_one_arm doc still described it as handling ctor arms, and mislabeled the Lit lowering as Term::Match — it is Term::If). Full workspace stayed green, confirming the arm was dead. crates/ailang-check/src/linearity.rs — renamed test implicit_fn_is_exempt → own_param_consumed_once_is_clean. Post-0062 there is no Implicit and no exemption; the test pins the ordinary single-Own-consume clean path. Did the desugar + linearity edits inline rather than via an agent: I had already loaded build_chain/build_ctor_group/desugar_one_arm to prove the arm dead, and a sub-agent would have redone the same reading. |
||
|
Brummel
|
b129af1363 |
fix(check): inherit borrow on heap sub-binders of a borrowed scrutinee (#58)
The strict linearity check accepted consuming a heap-typed pattern sub-binder extracted from a `(borrow)`-mode match scrutinee. The sub-binder aliases the caller-owned interior, so moving it into an `(own)` slot double-frees at runtime (SIGSEGV) — `ail check` returned exit 0, `ail build`+run crashed. A pre-existing hole the corpus never exercised; the #55 cutover's universal activation of the strict check exposed it (sibling to the #57 / spec 0064 class-2 let-alias-of-borrow hardening — this is the pattern-sub-binder analog). Root: `walk_arm` seeded every pattern sub-binder with `borrow_count = 0` (freely consumable), bypassing the `Borrow`-param seeding in `check_fn` that starts a borrowed param at `borrow_count = 1`. The whole-param consume was caught (cut55_2d, correctly rejected); the moved-out heap sub-binder was not. Fix: in `Term::Match`, resolve the scrutinee through `resolve_alias` and record whether it is a borrowed binder; thread that into `walk_arm`, which now seeds a heap-typed (`!is_value`) sub-binder of a borrowed scrutinee with `borrow_count = 1`. Value-typed sub-binders (e.g. the `Int` head) stay at `0` — copied out, no heap alias. Nested matches fall out for free: the inner match re-derives borrowed status from the borrow-carrying sub-binder. Rejected alternative: forcing fieldtest fixture cut55_2b to also reject. 2b is a clean borrow-traversal — `bump`'s recursive param is `(borrow)`, so the tail `t` is only borrowed, never consumed into an `(own)` slot. Distorting the fix to reject it would be unsound (false positive on legitimate borrow-rebuild). The fixture's own comment misdescribed its recursive param as `(own)`; the code says `(borrow)`. Verification: - RED test linearity::tests::consume_heap_sub_binder_of_borrow_scrutinee_is_rejected: was left:0 right:1 (check returned []), now green. - Full workspace: 732 passed / 0 failed (was 731; +1 the new test). No committed corpus newly rejected by the sharper check. - fieldtest repro cut55_2c: exit 0 (wrongly accepted) -> exit 1 (consume-while-borrowed on `t`). closes #58 |
||
|
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
|
d8be95dd44 |
fix(check): render restricted-set diagnostic in AILang set syntax (#52)
The `param-not-in-restricted-set` diagnostic rendered its allowed
element set with `{allowed:?}` — a Rust `{:?}` debug print of the
`Vec<String>`, producing `["Bool", "Float", "Int"]` with quotes,
brackets, and Rust list shape. AILang's audience is an LLM author, so a
language-level diagnostic leaking Rust formatting into its surface is a
quality defect.
Fix: render the set as `{Bool, Float, Int}` via a thiserror trailing-arg
`.allowed.join(", ")` wrapped in literal braces. The set is alphabetical
and stable (unchanged — the source is a sorted BTreeSet projection).
Design decision (set notation, not a union): the allowed set is a
membership set ("one of"), and AILang has no union-type surface syntax,
so brace set-notation `{A, B, C}` reads naturally without implying a
type-level union the language does not have. The structured JSON detail
(CheckError::detail, the `allowed` array) is left untouched — it is
machine-readable and correctly an array, not the cosmetic surface.
RED-first, inline: the bug is a one-line Display-string change at a
single site (lib.rs ~760). The exact lines were already loaded while
assessing the /boss queue, so a debugger subagent would only redo the
same reading (CLAUDE.md "When NOT to delegate: context already loaded").
TDD discipline is preserved by the new RED test
`param_in_reject_message_renders_allowed_set_in_ailang_syntax`, which
asserts the AILang set form and the absence of Rust quotes/brackets;
it failed RED on the old `{allowed:?}` and passes GREEN on the fix. The
pre-existing pin `param_in_reject_message_names_allowed_set` only
asserted substring presence, so it did not pin (or block) the format.
Verification: full ailang-check suite green (121 lib tests + integration
suites); live CLI repro from the issue now renders
`(allowed: one of {Bool, Float, Int})`.
closes #52
|
||
|
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
|
39b674c1ec |
chore: throwaway mode-migration tool for the Implicit cutover (#55, 0121 task 3)
Adds `ail migrate-modes <file>` (a throwaway CLI subcommand) and the AST walker `ailang_core::ast::for_each_fn_type_mut` it drives: parse a .ail, map every bare/Implicit fn-type slot to Own, preserve explicit Own/Borrow, print back. Semantically invisible today (PartialEq treats Implicit == Own), but it materialises the modes so the post-cutover parser — which will reject bare slots — accepts the migrated corpus. Both are throwaway: removed in task 4 once ParamMode::Implicit is deleted (the closure references Implicit and would not compile). RED-first: migrate_modes.rs failed to compile (missing walker) before for_each_fn_type_mut was added. Additive; full workspace suite green. refs #55 |
||
|
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
|
a378dad0aa |
docs(design): ratify the check→codegen boundary (mir.5, typed-MIR close)
mir.5 is the typed-MIR milestone's closing iteration. Its CODE half had
already converged before the iteration began, so mir.5 ships no code —
it ratifies into the design/ ledger the boundary the code already holds.
Verified at iteration entry (empirically, not from the spec sketch):
- all four named re-derivers grep-clean in codegen: synth_with_extras,
synth_arg_type, type_home_module, the second infer_module_with_cross;
- lower_workspace takes &MirWorkspace (codegen consumes MIR);
- MTerm::New is unreachable!() — raw-buf.4 desugars Term::New to
(app T.new …) before codegen, so there is no element-type
re-derivation left to relocate;
- #51 / #53 (the element-type / new-T codegen crashes) are closed;
their residue was fixed by
|
||
|
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
|
eba1be8d9d |
feat(codegen): fill MArg.mode for App args, read the anon-temp drop gate off it, delete module_def_ail_types (mir.3b)
Second of two iterations delivering spec 0060's mir.3 row (plan docs/plans/0118-mir.3b-marg-mode-and-table-delete.md). lower_to_mir's Term::App arm fills each MArg.mode from the resolved callee's param_modes (the sig = synth_pure(callee) it already holds); codegen's emit_call anon-temp borrow-slot drop gate reads arg.mode instead of re-looking-up the callee's param_modes from the module_def_ail_types table; and — since that gate was the table's only reader — the module_def_ail_types field plus all its construction and threading are deleted. Two refinements to the spec's mir.3b sketch, settled in planning from a focused recon and recorded in spec 0060: 1. module_def_ail_types is deleted in mir.3b, not mir.5. A grep proved self.module_def_ail_types had exactly ONE reader (the anon-temp gate); the own-param drop reads param_modes from the def's own f.ty, not this table. Once the gate moves onto MArg.mode the table is dead, so it is removed now rather than carried as dead code to mir.5. The mir.5 row's "last re-derivation residue" shrinks to the element-type / Term::New (New.elem) work. 2. MArg.mode is filled for App args only; MTerm::Let.mode is not filled. Only App args have a real per-arg mode source (the callee Type::Fn.param_modes). Do args (EffectOpSig has no param modes), Ctor args (no per-field mode), and Recur args (loop binders carry no mode) stay Mode::Owned. Let.mode has no source (ast::Term::Let has no mode field) and no consumer (the let-drop gate reads consume, not Let.mode), so it stays Owned — filling it would invent a value nobody reads. Safety property held: MArg.mode is filled from the same callee fn-type the gate read from the table, so the drop fires identically. For (app RawBuf.get (app RawBuf.set …) 0), RawBuf.get's param 0 is borrow, so args[0].mode = Borrow — exactly the value module_def_ail_types yielded. Confirmed by the anon-temp witness staying green. ParamMode -> Mode conversion: Borrow -> Mode::Borrow; Own and Implicit (the Implicit ≡ Own contract) -> Mode::Owned. The own-param drop keeps reading ParamMode off f.ty (Type/ParamMode imports retained, live readers at lib.rs:1356/1507). Also retires three now-stale doc comments that named the deleted module_def_ail_types field (ailang-check/src/lib.rs, uniqueness.rs, and the codegen_import_map_fallback_pin test doc) — a direct consequence of the deletion, reworded to the current architecture. Verification (orchestrator, post-implement inspect): diff matches the plan (App-arg m_args built before m_callee consumes sig — the benign borrow-order deviation the plan's note flagged); module_def_ail_types grep-clean across all of crates/; cargo build --workspace clean (no unused/dead_code); cargo test --workspace 702 passed / 0 failed / 3 ignored (+1 = the new producer pin app_arg_carries_callee_borrow_mode; no #[ignore] added). The anon-temp drop-correctness witness raw_buf_owned_drop_balances_rc_stats stays live=0, now driven by MArg.mode; the other RC-stats leak pins green; #49 stays #[ignore] (mir.4); #51/#53 build guards green. mir.3 is now complete (3a relocated consume_count + deleted the second uniqueness run; 3b filled the mode annotation + deleted module_def_ail_types). Remaining: mir.4 (#49 StrRep RED->GREEN), mir.5 (element-type/Term::New + ledger). |
||
|
Brummel
|
6bc0b501cb |
feat(codegen): relocate per-binder consume_count into MIR; delete codegen's second uniqueness run (mir.3a)
First of two iterations delivering spec 0060's mir.3 row (plan docs/plans/0117-mir.3a-consume-count-relocation.md). The per-binder consume_count — the only thing codegen read from its second infer_module_with_cross run — now lives on a new binder-keyed MirDef.consume: BTreeMap<String,u32>, filled once by lower_to_mir on the post-mono body. Codegen builds its existing (def,binder)->consume_count lookup from those maps and the three scope-close drop sites (own-param, let-binder, match-arm) read it; the codegen uniqueness run, its UniquenessTable field, and the import are deleted. mir.3 is split into two iterations (recorded in spec 0060): the named deletion depends ONLY on consume_count. All three drop sites read consume_count from self.uniqueness, while the modes they also gate on (param_modes for the own-param dec, scrutinee_is_owned for the match dec) come from the type, not the uniqueness pass (UniquenessInfo carries no mode). So mir.3a relocates consume_count and ships the deletion; mir.3b (next) fills MArg.mode/MTerm::Let.mode and switches emit_call's anon-temp gate onto MArg.mode. The split halves the change at the codebase's highest-risk surface (RC/drop correctness, the raw-buf leak saga) and makes each half independently verifiable against the live=0 leak pins. Design: consume_count lands on MirDef (binder-keyed), NOT on MArg. The drop sites key by (def, binder_name) — a per-binder aggregate — while the spec-sketched MArg.consume_count is per-arg-position and never reaches them; the per-def map matches the UniquenessTable's own keying and all three binder kinds (param/let/pattern) uniformly. MArg.consume_count stays a mir.1 default. Source = run check's infer_module_with_cross inside lower_to_mir post-mono (the synth_pure single-engine-re-walked pattern); retaining a check-time result is blocked (check's uniqueness is pre-mono and runs on-demand-from-codegen, never in check_workspace, so it would miss the mono specialisations). cross_module_types (= codegen's module_def_ail_types) is rebuilt in elaborate_workspace from the post-mono workspace. Safety property held: this is a PURE RELOCATION of an identical computation — infer_module_with_cross ran on the post-mono module in codegen and now runs on the same post-mono module in lower_to_mir, so drop placement is byte-identical. cross_module_types matches module_def_ail_types exactly (both insert f.name->f.ty over post-mono Def::Fn), confirmed by the leak pins staying green. Verification (orchestrator, post-implement inspect): diff matches the plan; codegen grep-clean for infer_module_with_cross + UniquenessTable (now ailang-check-internal); cargo build --workspace clean (no errors, no unused warnings — module_def_ail_types survives for emit_call's anon-temp param_modes gate); cargo test --workspace 701 passed / 0 failed / 3 ignored (+1 = the new producer pin mirdef_consume_is_populated_for_let_binder; no #[ignore] added). The live=0 drop-correctness witnesses all green: alloc_rc_loop_valued_rawbuf_binder_drops_at_scope_close (#43/#47), alloc_rc_heap_loop_binder_replaced_by_recur_does_not_leak, alloc_rc_print_int_does_not_leak_show_result_str. #49 stays #[ignore] (mir.4); #51/#53 build guards green. |
||
|
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
|
895ba846e8 |
feat(codegen): switch the lowering walk from &Term to typed &MTerm (mir.1b)
Atomic completion of spec iteration mir.1 (docs/specs/0060-typed-mir.md): codegen now consumes the typed MIR produced by `lower_to_mir` instead of re-deriving types from the bare `ast::Term`. Every codegen helper that took `&Term` (lower_term, lower_app, drop.rs, match_lower.rs) takes `&MTerm` and reads each node's checker-proved type off `MTerm::ty()`. The build path is `Workspace -> elaborate_workspace -> MirWorkspace -> lower_workspace`; the public `lower_workspace*` entry points and their 18 call sites thread `&MirWorkspace`. The codegen-side type re-derivers `synth_with_extras` + `synth_arg_type` (and the `builtin_ail_type` / `builtin_effect_op_ret` mirror tables) are deleted — grep-clean. The three re-derivers the spec keeps until mir.2/mir.3 (`type_home_module`, `is_static_callee`, the second `infer_module_with_cross`) stay. The mechanical Term->MTerm match-arm conversion was straightforward and compiler-enforced. The substance was a set of producer-side correctness gaps that only surface once codegen reads `MTerm::ty()` and once the build path re-synthesises the post-mono AST through the canonical `synth` (which, unlike the old codegen, fully re-unifies). Each was root-caused against a failing e2e fixture: 1. `qualify_local_types` stripped fn-type modes (rebuilt `Type::Fn` with empty `param_modes` / `Implicit` `ret_mode`), so a monomorphised polymorphic intrinsic (`RawBuf.set`) lost its `Own` ret-mode and the owned temporary leaked at the call site. Made mode-preserving, like its sister `qualify_workspace_types` and `Subst::apply` ( |
||
|
Brummel
|
449df13c9c |
fix(check): preserve fn-type modes through Subst::apply
`Subst::apply` rebuilt every `Type::Fn` with `param_modes: vec![]` and `ret_mode: Implicit`, discarding the modes the surrounding type carried. That was harmless while nothing downstream of inference read fn-type modes — but it is a latent under-specification: substitution is meant to be type-preserving, and a fn type's modes are part of its identity (an `(own T) -> (own U)` contract is not the same contract as its borrow-returning sibling). Modes are positional over `params`, and substitution remaps each param type element-wise without changing the arity, so the mode lists stay aligned — preserving them is a clone, not a re-derivation. The typed-MIR boundary (milestone 0060) makes this load-bearing: a node type synthesised by `lower_to_mir::synth_pure` ends with `subst.apply`, and the codegen drop path reads `ret_mode == Own` off a call's callee node to decide RC trackability. With the modes stripped here, an Own-returning call read back `Implicit`, nothing was trackable, and a heap-allocated binder leaked at scope close. Preserving the modes restores that signal at the source rather than re-deriving it in codegen (which is exactly the re-derivation the milestone exists to delete). Safe by construction: `unify`'s Fn arm destructures modes with `..` and compares only params/ret/effects, so carrying modes through `apply` cannot change unification; and `Type`'s custom `PartialEq` already treats `Implicit` and `Own` as interchangeable (only `Borrow` is distinct), so equality outcomes are unaffected except where preserving a `Borrow` is the more correct answer anyway. Whole `ailang-check` suite stays green. RED pin: crates/ailang-check/tests/subst_preserves_modes.rs. |
||
|
Brummel
|
600565d356 |
fix(check): localize own-ADT type-args in free-fn mono; complete the lower_to_mir producer
Additive producer-side work for the typed-MIR milestone (spec
docs/specs/0060-typed-mir.md), surfaced while building the mir.1b
codegen-consumption switch. Nothing here consumes MIR — codegen is
untouched; the whole existing suite stays green and one new RED pin
goes green. The mir.1b codegen switch itself stays in the working tree.
Headline fix — own-ADT type-arg localization in free-fn mono:
monomorphise_workspace's free-fn arm normalises every observed
type-arg through Registry::normalize_type_for_lookup. That
normalisation is load-bearing for cross-module dedup and a stable
specialisation symbol name, but it qualifies a *defining-module-own*
ADT to `<module>.<T>`. synthesise_mono_fn_for_free_fn then substitutes
those qualified type-args into the polymorphic source signature and
body, which are in the module's own *bare* convention (the qualify
pre-pass deliberately leaves own-module type-cons bare — lib.rs:4358,
"the current module sees its own types bare"). The result is a
self-inconsistent specialisation: e.g. fold_left specialised with
accumulator b := List<Int> minted
((std_list.List<Int>, Int) -> std_list.List<Int>,
std_list.List<Int>, List<Int>) -> std_list.List<Int>
— a qualified accumulator parameter against a bare list argument and a
bare Lam body. check_workspace never hits this (it synths the pre-mono
bodies, bare throughout); the old codegen tolerated it via the
now-deleted synth_arg_type's loose type-tracking. The post-mono synth
re-entry in lower_to_mir does full unification and correctly rejects
it: `expected std_list.List<Int>, got List<Int>`.
Fix: localize_own_types (mono.rs) strips the `<defining_module>.`
prefix back to bare for the module's own ADTs, applied to the type-args
before they are substituted, so the synthesised signature and body stay
uniformly bare-own. The *stored* type_args remain normalised, so the
symbol name and the Phase-3 rewrite-cursor key on the same canonical
form — the byte-identity invariant between synthesis and rewrite is
untouched. The ClassMethod arm needs no analogue: it already
substitutes the un-normalised target.type_ (mono.rs:841).
Alternatives rejected: (a) drop the normalisation in the shared
apply_subst_and_normalize helper — breaks cross-module dedup, mints
duplicate specialisations under divergent names. (b) Make
lower_to_mir's synth treat `<owner>.T` and bare `T` as equal during
unification — papers over the producer inconsistency in the consumer
and contradicts the established own-types-stay-bare invariant the rest
of check relies on. (c) Qualify the whole synthesised def own->qualified
— fights lib.rs:4358 and would require the lower path to also flip,
cascading the convention change through synth.
Producer completeness (additive, mirrors existing guards):
- lower_module skips Type::Forall defs (lower_to_mir.rs), mirroring
emit_module's guard. Polymorphic defs are stale source kept for
round-trip; their bodies carry mono-rewritten call names for
specialisations that were never synthesised, so a synth re-entry
would hit UnknownIdentifier.
- lower_module lowers non-literal const bodies to typed MTerm, carried
in MirModule.consts (+ MirConst in ailang-mir). A non-literal const
(e.g. a List ctor expression) needs a typed body once the consumer
walk takes &MTerm; literal consts emit a global and need no body.
- MirModule gains `ast: Module`, populated by lower_module — forward
scaffolding the mir.1b codegen consumption reads for module
structure. Populated here, consumed by the in-tree switch.
Verification: full `cargo test --workspace` green (697 passed, 0 failed)
with the codegen-consumption switch stashed out, including the new pin
crates/ailang-check/tests/lower_to_mir_ty.rs::poly_free_fn_accumulating_into_own_adt_elaborates
(RED before the localize fix with the exact mismatch above, GREEN after)
and the full e2e corpus (the own-ADT-poly demos elaborate clean and run
through the old codegen). This proves the producer fix is
regression-free and the remaining 22 e2e reds in the working tree are
codegen-consumption defects, not producer defects.
|
||
|
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
|
02775b58ca |
test(codegen): mark the #49 Str-leg RED pin #[ignore] pending the representation spec
The Str-leg pin (committed |
||
|
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
|
420703d321 |
fix(codegen): resolve the dotted T.new user-ADT callee, symmetric to check
A monomorphic `(new Counter 42)` over a user-defined ADT that declares a `new` fn passed `ail check` but crashed `ail build --alloc=rc` with `unknown variable: Counter.new` (RED-pinned in |
||
|
Brummel
|
1eff055a0e |
test(codegen): RED-pin #53 — monomorphic (new T args) over a user ADT must build
A monomorphic `(new Counter 42)` over a user-defined ADT that declares a
`new` fn passes `ail check` but crashes `ail build --alloc=rc` with
`unknown variable: Counter.new`. Distinct root from #51 (the polymorphic
type-arg drop, fixed by
|
||
|
Brummel
|
ee4107c721 |
fix(check): honour the written element type-arg on polymorphic (new T …)
A `(new RawBuf (con Int) 3)` whose buffer is never observed by a later
get/set passed `ail check` but crashed `ail build` with
`RawBuf_new__Unit has no registered intercept`, and a forbidden
`(new RawBuf (con Unit) 3)` was wrongly accepted at check. Both legs
share one root: the `Term::New` desugar discarded the author's written
`NewArg::Type` before anything could use it.
This was never an inference problem. The element type is EXPLICITLY
known — the author wrote `(con Int)`. The defect was that the desugar
threw that known type away and relied on re-discovering it from
downstream use; with no use (size-only), `RawBuf.new`'s result-only
forall var stayed unpinned, mono Unit-defaulted it, and codegen aborted
on the unregistered `RawBuf_new__Unit` intercept. The fix USES the
written type instead of inferring it.
Mechanism:
- desugar.rs: a polymorphic `(new T <elem> …)` (carrying a written
`NewArg::Type`) now SURVIVES into check instead of being lowered to
`(app T.new …)`. A monomorphic `(new Counter 42)` (no type-arg) keeps
the raw-buf.4 app-lowering unchanged.
- lib.rs synth `Term::New` arm: (a) validates the written element type
against the constructed type's `param_in` set via
`check_type_well_formed`, firing `ParamNotInRestrictedSet` naming the
forbidden element (leg 2) — synth is the correct site because it has
Env/registry access, unlike `pre_desugar_validation`; (b) binds the
result-only forall var DIRECTLY to the written type (`?a := Int`, a
trivial binding, no inference channel) by pushing a `FreeFnCall` whose
metas are the written concrete types, so mono mints
`RawBuf_new__<elem>` and never `__Unit`.
- mono.rs: `rewrite_mono_calls` and `interleave_slots` gain matching
`Term::New` arms that each consume exactly one free-fn slot at a
type-arg-bearing `Term::New` (mirroring synth's single observation,
pushed before the value-args), and `rewrite_mono_calls` reduces the
node to `(app <mangled> <value-args>)` so codegen never sees
`Term::New` and the lib.rs:2200 `unreachable!` stays valid. The two
walkers stay in lockstep.
The Unit-default policy in mono stays correct for genuinely-unobservable
vars (`is_empty(Nil)` etc.); only the case with a written `NewArg::Type`
is changed.
Alternatives rejected: an additive `type_args` field on `Term::App`
(~100 construction sites across 7 crates — a detour that builds a new
transport slot only to copy the already-known type into it); a runtime
type-witness parameter on `RawBuf.new` (invents a runtime value for a
pure type property); an identity-lambda wrapper carrying the element in
its param-type (hides a semantic property in a runtime construct). The
written type belongs where the author put it, carried to the one point
that consumes it.
Verification: both RED legs (committed
|
||
|
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
|
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
|
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
|
75109f171d |
fix(check): param-not-in-restricted-set names the allowed set (closes #48)
The ParamNotInRestrictedSet diagnostic named the offending type, the
type-variable and the home type, but not the allowed set {Int, Float,
Bool} that design/models/0007 §4 promises it names. A downstream author
was told what is wrong but not what is right, and the kernel source that
carries the set is not available to a downstream consumer.
The allowed set already travels on the error struct (it flows into the
JSON `details.allowed`); only the human-readable `#[error]` render
dropped it. Append it to the Display string. JSON details unchanged.
Surfaced by the raw-buf fieldtest (finding B3, docs/specs/0058).
RED-first: param_in_reject_message_names_allowed_set pins the message
content before the one-line render fix.
|
||
|
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
|
11e4c4624d |
feat: reserve $ in the Form-A lexer (closes #44)
Enforces the `$`-in-authored-names reservation that fresh_binder (ailang-core::desugar) silently relied on. `fresh_binder` mints shadow-rename binders as <base>$<n>; its collision probe could not see an authored binder literally named <base>$<n> that binds later under the same (def, name) uniqueness key — the exact collapse class #43 closed. The `$`-for-synthetic convention (`$mp_N`, <hint>$lr_N, <base>$<n>) was held by discipline only. This makes it a lexer-enforced invariant: no Form-A identifier token may contain `$`. A one-line guard in tokenize rejects any token run containing `$` before int/float/ident classification, raising the new LexError::ReservedDollar { token, start }. It surfaces through the existing ParseError::Lex -> W::SurfaceParse -> surface-parse-error channel with zero new wiring — no new CheckError, no AST walker, no entry-point threading. Placement rationale (the load-bearing call): the threat vector is Form-A source only. The client LLM author is forbidden from emitting canonical .ail.json directly — it writes Form A exclusively; only the orchestrator hand-authors JSON in rare exceptions. So every authored identifier a hallucinating client could produce flows through the lexer. `$` is a reserved character (like parens) with no legitimate authored use in any position — unlike `.`/`/`, which DO have legitimate uses (std_list.map) and therefore live in the check layer (InvalidDefName) with AST-aware positional logic. No positional split for `$` means no walker; the lexer is the right boundary. An earlier draft put the reject in pre_desugar_validation justified by "a client could build .ail.json directly" — false under the authoring contract, so the simpler lexer reservation replaced it. Exemptions by scan order, not special-case: `$` inside string literals and comments stays legal because both are consumed by earlier branches of the scan loop, before a run is ever sliced. The six checked-in example files mentioning loop$lr_0 in comments keep parsing. Documented non-goals (honesty rule): the .ail.json deserialization path stays unguarded (the orchestrator's self-responsible channel); the fresh_binder probe-body simplification (issue Q4) is not bundled — only its now-false doc-comment is corrected to state the enforced invariant, scoped to Form-A authored identifiers. Verification (all run, all green): - 3 in-source lexer tests: reject on x$1, exemption for $ in string, exemption for $ in comment. RED confirmed pre-guard (tokenize("x$1") returned Ok([Ident]), expect_err panicked); GREEN after. - 2 integration tests (reserved_dollar_pin.rs): the reject reaches the public parse entry as ParseError::Lex(ReservedDollar); string exemption survives at parse level. - cargo test --workspace: green, 0 failed. - CLI: check on the comment-$ example (exit 0) and on the #43 shadow idiom raw_buf_int.ail (exit 0, buf->buf$1 rename minted post-parse, never re-lexed); a fresh $-binder source now rejected with the surface-parse-error diagnostic naming the token and byte offset. Spec: docs/specs/0057-reserved-dollar-in-names.md (grounding-check PASS). Plan: docs/plans/0112-reserved-dollar-in-names.md. |
||
|
Brummel
|
b151990028 |
audit: raw-buf close-fixes — honesty + ledger for the binder-rename (refs #43)
Architect drift review at raw-buf milestone close (after
|
||
|
Brummel
|
55d76ae4a1 |
fix: alpha-rename shadowing binders at desugar — A2b leg (closes #43)
The last open leg of the RawBuf owned-heap drop-leak cluster #43: the UniquenessTable shadow-name collapse. The side-table keys by (def_name, binder_name); a fn that shadows a binder name — the shipped `(let buf (new…) (let buf (set buf…) … (get buf)))` idiom — collapses every shadow onto one key. The outermost binding records last (on pop) and overwrites the inner ones, so codegen's scope-close drop gates read the collapsed consume_count for the innermost binding, misjudge its ownership, and suppress its drop. The owned slab leaked (live==1). Fix: desugar now alpha-renames any binder whose authored name shadows an enclosing binding to a fresh `<name>$<n>`, making the (def, name) key injective per fn. The rename is on-shadow-only and uniform across binder kinds (Let, flat-Match pattern-binders, Lam params, Loop binders); non-shadowing binders keep their authored name, so every existing fixture's desugared output is byte-identical (evidenced by the full pre-existing desugar suite passing unchanged). IR-neutral: codegen names heap by fresh SSA, never by the source binder name. No consumer of the uniqueness table changes — they all key by name, and the name is now a per-fn injective identity (acceptance criterion 5). The fix is entirely internal to ailang-core::desugar; uniqueness.rs gets only a doc-comment correction (its old text was wrong on two counts: "last = innermost by pop-order" was backwards, and "every shipping fixture has unique binder names" was false). Mechanism (vs. the spec's sketch): the threaded lexical scope became a `Scope` struct carrying `entries` keyed by each binder's EFFECTIVE (post-rename) name and `rename` mapping authored→effective. Keying entries by effective name is load-bearing, not cosmetic: the LetRec capture-detection reads `free_vars_in_term` of the desugared body (effective names) and filters by `scope.contains_key` — had entries stayed keyed by authored name, renaming an enclosing let would have made a captured shadowed binder invisible to capture detection (UnknownVar in the lifted fn). `insert_fixed` records identity renames for never-renamed binders (fn-params, LetRec name/params) so an inner renamable binder that shadows them is still detected. Alternatives rejected: (A) an AST id field and (B) a derived binding-path — both solve the deeper, SEPARATE problem of persistent AST provenance back to the authored form, which is certain to be needed eventually but is not required here; conflating the internal naming collision with provenance is a category error. C′ (this) reuses the existing fresh-name machinery and touches one pass. Verification: the three shipped Let-shadow tests (raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats) reach live==0 (were RED at live==1); the flat-pattern differential (flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed) reaches its alpha-renamed control's live count (was 5 vs 3); a new desugar unit test (shadowing_let_is_alpha_renamed) pins the rename + reference resolution; full workspace suite green, no fixture output drift. Both no-change consumers re-verified by hand: match_lower.rs keys by the emitted (renamed) pattern binder, linearity builds table and lookups from the same desugared tree. Spec: docs/specs/0056-unique-binder-names.md. Plan: docs/plans/0111-unique-binder-names.md. |
||
|
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
|
0f6108e428 |
fix: resolve cross-module borrow modes in the uniqueness pass (refs #43)
A2a leg of the owned-RawBuf drop-leak. Prerequisite: regression-free
and independently correct, but does NOT alone close the leak — the
three shadow_rebind RED tests (
|
||
|
Brummel
|
f7f4c3b237 |
test: RED shadow-rebind RawBuf drop-leak on shipped fixtures (refs #43)
raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats guard
the three shipped milestone fixtures (the LLM-natural shadow-rebind
idiom `(let buf (new...) (let buf (set buf...) ...(get buf)))`) with a
live==0 RC-stats assertion alongside their existing stdout check.
This is a SECOND, distinct leak mechanism (A2), separate from the
anonymous-temp path fixed in
|
||
|
Brummel
|
62cd4b4ee7 |
fix: drop owned temp passed to a borrow slot at the call site (closes #43)
GREEN side of the owned-RawBuf drop-leak. RED test
raw_buf_owned_drop_balances_rc_stats (
|
||
|
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
|