5b4eb766c35b57891e73e3f756a4e938b4d8741e
923 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
 Brummel
|
5b4eb766c3 |
glossary: bootstrap AILang nomenclature ledger
Add design/glossary.md (25 entries) and wire it in via the paths.glossary profile slot, making it standing reading for every skill and agent role. Built by the glossary skill's bootstrap procedure: five read-only glossary-extractor agents swept the prose surface (design/contracts, design/models, design/INDEX.md, docs/PROSE_ROUNDTRIP.md, and the 60 docs/specs in three blocks), reporting recurring domain-concept terms and their competing synonyms with frequencies. docs/plans was excluded as a derived execution artefact that mirrors spec/contract vocabulary rather than originating it. Three apparently-contested clusters were resolved by record-reality against the authoritative current docs (CLAUDE.md + design/): the retired .ailx extension yields to .ail; Form-A wins over "Form A" (13:2); round-trip wins over roundtrip (15:10). The one genuine nomenclature choice -- the canonical term for the structured hashable form -- was decided by the user: JSON-AST is canonical, .ail.json is its on-disk file. The local conformance check caught and removed a Form-B / JSON-AST Avoid-list collision before write. |
||
|
Brummel
|
1a1a68df8b |
plan: mir.1b — codegen consumes MIR (the atomic switch)
Second half of spec iteration mir.1, planned against the landed mir.1a
infrastructure (
|
||
|
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
|
438a009b83 |
plan: mir.1a — typed-MIR infrastructure (additive half of spec mir.1)
First of two plans for spec iteration mir.1 (docs/specs/0060-typed-mir.md).
mir.1 is the project's largest iteration — a full codegen frontend
switch from walking &Term to walking &MTerm — and it does not fit one
bite-sized plan, because the switch is atomic: there is no compiling
intermediate between "all Term" and "all MTerm" (dual-path is
spec-forbidden). The MIR *producer* side, by contrast, compiles and
tests in isolation. So mir.1 is sequenced across two plans:
- mir.1a (this plan): the additive producer — new leaf crate
ailang-mir (MTerm/MArg/Callee/Mode/StrRep, structurally complete over
all 17 Term variants plus the Str split), ailang-check::lower_to_mir
(post-mono walk that calls canonical synth per node and maintains
locals/loop_stack exactly as synth does — no second type engine), and
ailang-check::elaborate_workspace (check → desugar+lift → mono →
lower_to_mir). Nothing consumes MIR yet; codegen untouched; whole
suite stays green; three ty-fill pins load the #51/#53/#49 witnesses
as fixtures and elaborate the full workspace (prelude included).
- mir.1b (next plan, against the landed types): flip codegen's walk to
&MTerm, delete synth_with_extras + synth_arg_type (9 call sites across
lib.rs/drop.rs/match_lower.rs), thread the 18 lower_workspace* callers,
switch the CLI build path to elaborate_workspace.
Both together satisfy the spec's mir.1 row. The split is plan
granularity, not a spec change — the spec's mir.1 deliverable is
unchanged.
Orchestrator design calls baked in (planner judgement, no user fork):
dedicated MTerm::Str{lit,rep} variant (Str-split installs the mir.4
hook at the #49 loop seed); emit_ir keeps &Module (builds MIR
internally — minimal blast radius); lower_to_mir scaffolding mirrors
mono.rs:771-816; Match-arm binding reuses synth's own type_check_pattern.
Recon (plan-recon) mapped the full deletion blast radius for mir.1b
(9 synth_arg_type sites, not the 3 the focus-hint assumed; 18
lower_workspace* callers). The two new witness fixtures
(new_rawbuf_size_only, new_counter_user_adt) were verified ail
check-clean during planning.
|
||
|
Brummel
|
8bc2972594 |
spec: typed-mir — place lower_to_mir post-mono, correct one-engine framing
plan-recon flagged that monomorphise_workspace runs between check and codegen, and codegen lowers the post-mono workspace. The first draft of this spec placed lower_to_mir as the final phase of check_workspace (pre-mono) and claimed "nothing re-walks the AST". That is wrong on both counts: - Built pre-mono, MIR would not carry the monomorphic specialisations monomorphise_workspace appends — exactly the post-mono bodies codegen emits today — reintroducing the check↔codegen gap this milestone exists to close. - synth is a pure `&Term → Type` function and the authoring AST carries no node-ids, so MIR cannot be a side-table read off a check pass; it is built inline by a walk. The honest property is therefore not "no second walk" but "no second *engine*": codegen's synth_with_extras is a hand-copied mirror of synth that drifts (every raw-buf bug is a drift point). The milestone replaces the mirror with a single post-mono call to canonical synth, materialised as MIR. Corrections: architecture diagram and data flow now run check → lift → monomorphise → lower_to_mir; lower_to_mir is wrapped by a new front-end entry elaborate_workspace that subsumes the lift+mono orchestration the CLI does today; check_workspace stays for the diagnostics-only path (`ail check`). Node count fixed 27 → 17 Term variants (ast.rs:436). Re-dispatched grounding-check after the edit (post-PASS edit invalidates the prior report) — PASS, all load-bearing post-mono assumptions ratified against live code (main.rs build order, mono.rs synth use, 17-variant Term, no node-ids). |
||
|
Brummel
|
207c63649f |
spec: typed-mir check→codegen boundary contract
Open a new milestone introducing a typed mid-level IR (`ailang-mir`) as the single artefact crossing the check → codegen boundary, so codegen re-derives nothing. Root cause (architect drift review): the boundary today carries no typed artefact. `crates/ail/src/main.rs:2293` calls `check_workspace`, discards the result, and hands `lower_workspace` the raw `Workspace`. `CheckedModule` (ailang-check/src/lib.rs:1283) carries only top-level (Type, hash). Codegen therefore re-runs four independent derivations of what check already proved — type synthesis (`synth_with_extras`), callee resolution (`type_home_module` ×3 + `is_static_callee`), uniqueness/mode (`infer_module_with_cross`, second run), and Str representation (`!is_str` recur gate). Every raw-buf bug (#43/#46/#47/#49/#51/#53, all "check-clean, build-divergent") is a point where one of those re-derivations disagreed with check and got patched one leg at a time. Honest framing: this is removal of a re-derivation architecture, not a RED→GREEN of crashing programs. #51 and #53 build today (patched by |
||
|
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
|
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
|
43e3b21080 |
audit: raw-buf usability repair — cycle tidy (refs #7)
Close-out audit for the raw-buf usability repair (range 8e9f0f0..HEAD: B1 #46, B2 #47, B3 #48, B5 loop-result drop, docs). Architect drift review (against design/INDEX.md + the kernel-extensions model): all three lockstep-invariant pairs undisturbed (INTERCEPTS ↔ intrinsic markers, lower_app ↔ is_static_callee, Pattern::Lit ↔ pre_desugar_validation — none touched; the edits sit in linearity, synth_with_extras, and drop.rs). Every fix shipped a property-protecting RED test. B3 brings the diagnostic into conformance with the model's pre-existing §4 promise rather than opening a gap. One drift item raised and fixed here: the B4 ratification paragraph in design/models/0007 §RawBuf overstated the set non-enforcement as unconditional. Verified: a double-consume of an own-param RawBuf inside a fn with explicit modes fires [use-after-consume]; it slips through only where the linearity activation gate skips the fn (paramless main, or implicit-mode params). The paragraph now states the enforcement is gated, names the gate, and gives both the caught and the uncaught case. Regression (commands.regression, verbatim): - bench/check.py EXIT 0 — 34 metrics; 0 regressed, 34 stable - bench/compile_check.py EXIT 0 — 24 metrics; 0 regressed, 24 stable - bench/cross_lang.py EXIT 0 — 25 metrics; 0 regressed, 25 stable No baseline moved; carry-on. Two forward-queue items filed during the repair, both out of scope here: - #49 per-iteration leak of superseded heap loop-binder values across recur (a Str accumulator leaks; RawBuf does not — set is in-place). - #50 bare RawBuf not auto-imported in type-constructor positions (a RawBuf in a user ADT field needs the qualified raw_buf.RawBuf); the RawBuf-in-ADT substrate itself works (builds, runs, drop cascades leak-clean) with the qualified name. cycle raw-buf-usability tidy (clean). |
||
|
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
|
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
|
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
|
f37bd959d4 |
audit: raw-buf milestone close — tidy (clean) (refs #7)
Cycle-close drift review for the raw-buf milestone (raw-buf.1-.6 +
the #42/#43 drop-leak bug-fixes), range a163c8c..HEAD. raw-buf.6
(
|
||
|
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
|
fb0dd92a6c | plan: raw-buf.6 kernel-stub-retirement (refs #7) | ||
|
Brummel
|
c5eca7e91d |
bench: re-ratify compile_check baseline (closes #45)
Re-baseline bench/baseline_compile.json, last ratified 2026-05-15 ( |
||
|
Brummel
|
7321826c66 |
audit: cycle-close tidy for #44 — $-lexer-reservation (refs #44)
Cycle-close audit for the #44 Form-A `$`-reservation cycle (b151990..HEAD). One drift item fixed inline. Both regression scripts exited 1; investigated and attributed to machine load this session, NOT a code regression — baseline deliberately NOT updated. Architect drift review: - [fixed] design/models/0001-authoring-surface.md — the line "The only reserved tokens are `(`, `)`, and whitespace" was made stale by this cycle (the lexer now rejects any identifier token containing `$`). Corrected to distinguish token *delimiters* (`(`/`)`/whitespace) from the `$` *character reservation within a token*, scoped to the Form-A authoring surface, naming the enforcement site (`LexError::ReservedDollar`) and the intentional `.ail.json` non-guard. - [carry-on] honesty sweep otherwise clean: the only other `$`-mentions in the ledger (0008-memory-model.md, 0003-pipeline.md) describe synthetic mint names (buf$1, <hint>$lr_N) and remain correct. No over-broad "no Module can contain `$`" prose exists. The corrected fresh_binder doc-comment (feat commit) is Form-A-scoped and honest. - Decision: no new ledger *contract* added. 0015-language-constraints holds the four RC-soundness preconditions (strict eval, no recursive value bindings, no shared mutable refs, acyclic ADTs); a lexical character reservation is a different category and is documented in the authoring-surface model doc with its enforcement site, which is its natural home. Architect confirmed absence of `$`-contract prose is not itself drift. Lockstep pairs: none apply (architect walked each against the diff): - Pattern::Lit typecheck <-> pre_desugar_validation.rs — neither changed. - lower_app <-> is_static_callee — codegen unchanged. - INTERCEPTS <-> (intrinsic) markers — intercepts.rs + kernel sources unchanged. Regression scripts: - bench/cross_lang.py: EXIT 0. 25 metrics; 0 regressed, all stable. - bench/compile_check.py: EXIT 1; "12 regressed" — ALL are check_ms.* (type-check wall-clock), baseline ~1.8-3.3ms vs actual ~2.5-4.4ms, ~+0.8ms absolute and roughly UNIFORM across every fixture regardless of size (hello +39%, bench_list_sum +51%). All 12 build_O0_ms.* (the ~93ms LLVM portion of the same `ail build`) are within tolerance but also uniformly shifted +12-15%. Attribution: NOT this cycle's code. The guard adds one `raw.contains('$')` byte-scan per token; a tiny module is ~50 tokens, so the added cost is nanoseconds — physically cannot account for +0.8ms on a 2ms check. The uniform ~12-15% shift across the WHOLE `ail` invocation (check AND build) is a global machine-slowdown fingerprint (heavy concurrent subagent/cargo load this session); it crosses the 25% tolerance only on the tiny-baseline check_ms metrics. Localised by reasoning, not by the bencher (the effect is environmental, nothing to localise in code). - bench/check.py: EXIT 1; throughput metrics flipping run-to-run with identical code (rc_over_bump moved in/out of REGRESSION across four runs; bump_s swung -9.5/-11/-14/-15%). Same machine-load variance; rc_over_bump is a ratio of two independently-noisy wall-clock measurements, the noisiest metric in the set. Baseline NOT updated on either script: ratifying a machine-load delta would bake an under-load baseline in and mask a future real regression. OPEN VERIFICATION: re-run bench/compile_check.py and bench/check.py on a quiet machine to confirm green; tracked as the cycle's one open item. Cycle #44 closes (code + docs clean; regression gate pending a clean-machine confirmation, baseline untouched). |
||
|
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
|
559531806d |
plan: reserved-dollar-in-names — dollar-lexer-reservation (refs #44)
Executable plan for spec 0057 (committed
|
||
|
Brummel
|
c76057008e |
spec: reserve $ in the Form-A lexer (refs #44)
#44 asks to enforce-or-retract the `$`-in-authored-binder-names reservation that `fresh_binder` (ailang-core::desugar) relies on for collision-free shadow-rename mints. This spec chooses enforcement, and places it in the Form-A lexer rather than the check layer. The placement is the load-bearing design decision. An earlier draft put the reject in `pre_desugar_validation` (check layer), justified by "a client could construct `.ail.json` directly, bypassing the lexer". The user corrected the threat model: the client LLM author is forbidden from emitting canonical `.ail.json` — it writes Form A exclusively, and only the orchestrator hand-authors JSON in rare exceptions. So the entire hallucinating-client attack surface is Form-A source, which always flows through `tokenize`. That collapses the design: - `$` is a reserved character (like `(`/`)`) with no legitimate authored use in any position — verified: zero authored `$` idents exist in the checked-in `.ail` corpus; the six `$` occurrences are all in comments. No positional split, so no AST-aware walker is needed — unlike `.`/`/`, which DO have legitimate uses (`std_list.map`) and therefore live in the check layer (`InvalidDefName`). The issue's premise "lex.rs reserves only `.`" is false on two counts and is corrected in the spec. - The reject is a single new `LexError::ReservedDollar`, raised inline in the `tokenize` run-classification arm, surfaced through the existing `ParseError::Lex` -> `W::SurfaceParse` -> `surface-parse-error` channel. No new `CheckError`, no AST walker, no multi-entry-point wiring (the check layer has four entry points, only two of which currently run the pre-desugar pass — a trap the lexer placement sidesteps entirely). Documented non-goals (honesty rule): the `.ail.json` deserialization path stays unguarded (the orchestrator's self-responsible channel, scoped out by the user); the `fresh_binder` probe-body simplification (issue Q4) is not bundled — only its now-false doc-comment is corrected. grounding-check PASS on the final bytes: all six load-bearing assumptions ratified by green tests; all three Form-A example blocks parse-gate clean (exit 0 today, by design — the reject is new behaviour). String- and comment-internal `$` stay legal by scan order; no must-fail `$` fixture goes under examples/ (the round-trip test parses every fixture there). |
||
|
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
|
1990147467 |
plan: unique-binder-names — desugar alpha-rename for #43 A2b (refs #43)
Executable plan for spec 0056. Three tasks: - Task 1 (atomic compile unit): introduce a `Scope` struct threading two maps — `entries` keyed by each binder's effective (post-rename) name, `rename` mapping authored→effective for shadow detection and Term::Var resolution; add `fresh_binder` (<name>$<n>) and `rename_pattern_binders`; rewrite every binder site (Let, flat-Match pattern, Lam params, Loop binders) with rename-on-shadow, plus the LetRec arm and both def-boundary constructions, to the new API. - Task 2: correct the UniquenessTable doc-comment; verify the four RED tests go GREEN; full-suite regression gate. - Task 3: regression guard — a desugar unit test pinning that a shadowing let is alpha-renamed and that a letrec capturing the shadow-renamed binder still resolves (the entries-keyed-by-effective choice is what keeps capture detection correct under rename). Recon surfaced two facts the spec's sketch did not: the scope is a bare BTreeMap (so resolved_name/bind live on a new Scope type, not the map), and the LetRec capture-detection reads effective names from the desugared body — hence entries are keyed by effective name. Both stay internal to desugar.rs, preserving acceptance criterion 5 (no change to uniqueness.rs logic / codegen gates / linearity.rs). Both no-change consumers verified: match_lower.rs:795 keys by the emitted (renamed) pattern binder; linearity builds table and lookups from the same desugared tree. |
||
|
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
|
||
|
Brummel
|
b49f57d9c6 |
spec: raw-buf — re-carve drop ratification to raw-buf.5, retirement to .6 (refs #7)
raw-buf.4 (RawBuf payload + Term::New desugar) implemented and about to
land, but it surfaced that the drop ratification was mis-scoped: the
flat drop FUNCTION is emittable in .4, but the drop CALL needs a codegen
resolution mechanism the .4 plan did not scope. An owned RawBuf binder's
value is a cross-module type-scoped intrinsic call ((app RawBuf.set ..) :
own (RawBuf a)); codegen's is_rc_heap_allocated only marks an App binder
drop-trackable when synth_callee_ret_mode resolves the callee's Own mode,
but codegen synth_arg_type has no TypeDef-first / cross-module-mono
resolution ladder (unlike the checker's lib.rs:3465), so the binder is
non-trackable and no drop call is inserted. A second site
(uniqueness::infer_module's per-module globals) misses the cross-module
borrow mode too.
Re-carve (six iterations; .1-.4 done, .5/.6 remain):
raw-buf.4 — RawBuf payload + Term::New desugar + flat drop FUNCTION
(DONE). Worked program prints 60; Float/Bool/reject ship.
raw-buf.5 — owned cross-module type-scoped drop-call resolution: a
TypeDef-first + cross-module-mono arm in codegen
synth_arg_type feeding is_rc_heap_allocated /
synth_callee_ret_mode / drop_symbol_for_binder, plus
cross-module op visibility in uniqueness::infer_module.
Ratified by raw_buf_no_leak (live == 0).
raw-buf.6 — kernel_stub retirement (was .5).
Also documents the raw-buf.4 diagnostic-behaviour change: because the
Term::New desugar now runs before check, (new T ..) with a missing
new-op surfaces type-scoped-member-not-found (more precise) rather than
the prep.2 new-type-not-constructible it supersedes; new-arg-kind-mismatch
is obsoleted (the desugar drops the type-arg). Same rejection conditions,
preserved. And corrects the @ailang_rc_release spec slip to the real
symbol @ailang_rc_dec.
The drop-call resolution is its own iteration for the same reason
raw-buf.3 became a mechanism prep: it is a codegen-resolution mechanism
(parity with the checker's type-scoped/cross-module ladder), separable
from the RawBuf payload, and isolating it keeps the resolution change
off the .4 payload diff.
|
||
|
Brummel
|
9ff1f22d42 |
plan: raw-buf.4 RawBuf payload + Term::New desugar (refs #7)
Four tasks. Task 1: raw_buf manifest (source.ail + mod + lib re-export)
+ ailang-surface wiring (parse_raw_buf + injection) + round-trip +
workspace count 4->5 — checkable, no codegen (raw_buf not yet in the
bijection collector list, so its markers are uncollected, bijection
stays green). Task 2: the general Term::New -> (app T.new <values>)
desugar (runs before check, so the type-scoped callee flows through the
raw-buf.3 scope threading to RawBuf_new__T), drops the NewArg::Type
(element type inferred from use — no type-ascription term exists),
removes both codegen deferral arms; ratified by a (new StubT 42)
build-and-run. Task 3: the 12 scope-qualified RawBuf_op__T entries +
emit fns (alloc/gep/load/store over an @ailang_rc_alloc slab, Int emits
in full + Float/Bool by an exact element-type/width substitution table)
+ a flat intrinsic-storage drop + raw_buf added to the bijection
collector module list (marker<->entry lockstep closes here). Task 4:
the E2E (int -> 60, float, bool, param-in reject, drop leak).
plan-recon resolved both make-or-break risks favourably: (A) the
alloc/load/store emit has a clean mirror (emit_eq_str does
locals-by-position -> fresh_ssa -> gep -> call -> ret; @ailang_rc_alloc
returns the payload ptr with rc-header auto-prepended); (D) desugar runs
BEFORE check/synth/mono (prepare_workspace_for_check), so Term::New
becomes (app RawBuf.new ..) before synth's type-scoped resolution sets
scope=Some("RawBuf") -> reaches the raw-buf.3 RawBuf_new__Int mint. No
checker tweak needed.
Three orchestrator design calls (spec underspecified the codegen
detail): (1) drop discriminator = derived signal "the TypeDef's `new`
op is (intrinsic)-bodied" -> flat @ailang_rc_dec drop; correctly
separates RawBuf (intrinsic new) from StubT (real-body new), where a
param_in heuristic would misclassify StubT (also param_in). No schema
change, no hash-pin. (2) @ailang_rc_release does not exist -> the real
symbol is @ailang_rc_dec (spec slip corrected). (3) Bool = 1 byte per
spec; the 12 emits are per-element-specialised so each hardcodes its
width (Int/Float 8, Bool 1) + store type (i64/double/i1); the i1
store/load syntax is verify-first, raw_buf_bool_e2e is the catch.
Baseline after raw-buf.3 is 670; gates step 670->671 (round-trip)
->672 (StubT desugar) ->677 (5 RawBuf E2E). kernel_stub stays
(retirement is raw-buf.5).
|
||
|
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
|
8508182f84 |
plan: raw-buf.3 type-scoped polymorphic intrinsic mechanism (refs #7)
Two tasks. Task 1 threads a TypeDef scope through the free-fn mono path: a scope: Option<String> field on FreeFnCall + MonoTarget::FreeFn, populated Some(prefix) only on the type-scoped T.f resolution branch (lib.rs:3535, gated on type_home.is_some()), None everywhere else; consumed at the two mono-symbol mint sites via a scoped_base helper (both read the same MonoTarget → lockstep) and folded into mono_target_key. Result: StubT.peek @ Int mints StubT_peek__Int, not the colliding bare peek__Int; existing bare-resolved symbols unchanged (669-gate is the no-regression backstop). Task 2 adds the StubT.peek ratifier op to the stub source, extends the bijection collector to expand a polymorphic type-scoped intrinsic over its TypeDef's param-in set (building the same T_f__<elem> strings via mono_symbol_n on Type::Con elems, so collector and mint agree byte-for-byte), registers StubT_peek__Int/Float entries + emit fns, updates kernel_stub_module_round_trips, and adds a mono-symbol integration test (borrow-param calls, no Term::New, no codegen). plan-recon resolved the make-or-break unknown favourably: the TypeDef scope is discarded at lib.rs:3535 but fully available there (prefix + type_home live) — a clean thread-through, not a resolution re-architecture. Three orchestrator design calls folded in: peek's emit is a plausible signature-correct stub, unit-ratified only (never instantiated in .3, no Term::New to build a StubT; RawBuf's emits in .4 are the E2E-verified ones; peek retires in .5); the exact llvm_type(borrow StubT Int) string is an implementer verify-first step (eq__Unit precedent); scope-trigger is the call path (not signature, which would perturb bare-called fns like length), scope-value is the prefix, collector infers from signature — they agree by construction for single-TypeDef kernel modules, bijection + 669-gate backstop. peek Form-A verified to parse+check this session under a probe module (ok, 32 symbols / 3 modules). Final gate 670 (669 + 1 new mono test); .ll snapshots stay green (peek polymorphic → no instantiation without a call site). |
||
|
Brummel
|
d2885c7ae6 |
spec: raw-buf — re-carve .3/.4/.5, type-scoped polymorphic intrinsic prep (refs #7)
Second re-carve. Planning raw-buf.3 (via plan-recon) surfaced that
RawBuf's ops are a THIRD intrinsic shape the intrinsic-bodies mechanism
never handled: type-scoped polymorphic top-level intrinsics (forall a,
param-in {Int,Float,Bool}, called as RawBuf.get). The existing bijection
+ symbol story covers only monomorphic top-level intrinsics (answer,
float_*) and per-type class-method instances (eq__Int).
The gap (both confirmed in source by recon + grounding-check):
- mono_symbol_n mints <base>__<T> from the bare fn name, so RawBuf.get
@ Int → get__Int — the RawBuf scope never enters the symbol;
new/get/set/size @ Int would collide with any other poly free fn of
those (very common) names.
- the bijection collector's Def::Fn arm records the bare name "get" as
one marker, matching neither the per-type entries nor their symbols;
one polymorphic marker must map to N per-element entries, which the
1-marker-to-1-entry bijection cannot express.
So raw-buf.3 is no longer "add 12 table rows" — it is a new language
mechanism. Re-carve (3 remaining iterations):
raw-buf.3 — type-scoped polymorphic intrinsic mechanism: scope-
qualified mono symbols (RawBuf_get__Int) + bijection-
collector expansion over param-in. Built and ratified
standalone on the stub (a StubT.peek op + its 2 scoped
entries + mono/bijection unit tests), the prep pattern
prep.1/.2/.3 used. No RawBuf, no Term::New dependency.
raw-buf.4 — RawBuf payload (module + 12 scoped entries + drop) +
Term::New desugar ((new RawBuf ...) sugar, removes both
deferral arms). Pure consumer of .3. Worked program → 60.
raw-buf.5 — kernel_stub retirement (peek + answer + stub leave;
RawBuf carries all roles).
Decided design (Option A): scope-qualified symbols, not bare. Rationale
is semantic — the type-scoped call convention RawBuf.get should carry
through to a collision-free, IR-legible symbol; bare get__Int is a
latent collision landmine on the most-reused op names. Removing that
collision class is itself feature-acceptance criterion-3 evidence.
The raw_buf module Form-A in § Concrete code shapes is gate-verified
(ail check → ok, 35 symbols / 3 modules). Grounding-check PASS: all 10
current-behaviour assumptions ratified by named green tests; the
Term::New codegen-deferral (lib.rs ~2096 + ~3298) is the same
about-to-be-deleted prep.2 transient, reported-not-blocked (consistent
with the override logged on
|
||
|
Brummel
|
fbdbe740e6 |
iter raw-buf.2-kernel-rename (DONE 2/2): ailang-kernel-stub → ailang-kernel family-crate (refs #7)
Pure crate rename, zero behavioural change. ailang-kernel-stub becomes
the ailang-kernel family-crate: a re-export hub (src/lib.rs) plus one
submodule per kernel-tier module (today only kernel_stub:
src/kernel_stub/{mod.rs, source.ail}). raw-buf.3 plugs raw_buf in as a
sibling submodule; this iter only builds the home.
Task 1 (atomic — the rename breaks the build until every site is
threaded):
- git mv crates/ailang-kernel-stub → crates/ailang-kernel.
- Carved the STUB_AIL Form-A body verbatim (byte-identical, verified
via diff against HEAD's raw string) into src/kernel_stub/source.ail,
loaded by mod.rs via include_str!. The answer (intrinsic) fn is
byte-preserved — its INTERCEPTS bijection partner stays pinned.
- lib.rs is now the hub: `pub use kernel_stub::SOURCE as STUB_AIL;`.
The public symbol STUB_AIL is preserved, so ailang-surface and the
bijection test bind to it unchanged.
- 8 compile sites threaded across 6 files: Cargo package name,
workspace member + dep-alias, ailang-surface dep, loader.rs
use-paths (ailang_kernel_stub → ailang_kernel). Cargo.lock
auto-regenerated.
Task 2 (doc/ledger honesty, no build impact):
- design/INDEX.md, CLAUDE.md code-layout row + lockstep-pair row,
design/models/0007 ×2 — crate-path strings updated to the new
ailang-kernel/src/kernel_stub path.
- Scope note: the spec's raw-buf.2 Components row named only
design/INDEX.md + the CLAUDE.md code-layout row. plan-recon found two
more present-tense crate-path refs (CLAUDE.md:312 lockstep row,
model 0007:8/235). Folded them in per the honesty-rule — a rename
that leaves stale present-state paths is an incomplete rename.
Path-only; the retirement narrative stays for raw-buf.4.
The AILang module name kernel_stub (the Form-A string + parse_kernel_stub
fn) is deliberately unchanged — only the crate identifier moved.
Verification (orchestrator, this session): cargo build --workspace
clean; cargo test --workspace 669 passed / 0 failed / 2 ignored
(baseline held exactly — no test added/removed). Carve byte-identity
confirmed by diff; no stale ailang-kernel-stub / ailang_kernel_stub
refs remain in-tree (git grep, excl. history + lockfile). The four
rename-invisible ratifiers (kernel_stub_module_round_trips,
intercepts_bijection_with_intrinsic_markers, .ll snapshots,
workspace_pin) all green via the preserved re-export.
|
||
|
Brummel
|
395a40f3e7 |
plan: raw-buf.2-kernel-rename — atomic crate rename + family-crate reshape (refs #7)
Two tasks. Task 1 (atomic): git mv ailang-kernel-stub → ailang-kernel, carve the STUB_AIL Form-A body verbatim into src/kernel_stub/source.ail (incl. the answer (intrinsic) fn — a perturbed byte shifts the .ll snapshots + kernel_stub_module_round_trips), add mod.rs (include_str!) + lib.rs hub (pub use kernel_stub::SOURCE as STUB_AIL), thread all 8 compile sites across 6 files (Cargo package + workspace member + dep-alias + ailang-surface dep + loader.rs use-paths), end with cargo build + cargo test green. Task 2: doc/ledger crate-path honesty fixes (INDEX, CLAUDE.md code-layout + lockstep rows, model 0007) — path-only, retirement narrative left for raw-buf.4. Zero behavioural change; public symbol STUB_AIL preserved via the re-export so ailang-surface + the bijection test bind unchanged. NO raw_buf submodule (that is raw-buf.3). plan-recon mapped 8 compile-breaking sites + 5 doc sites (two beyond the spec's named row list — CLAUDE.md:312 lockstep + model 0007:8,235 — folded in per honesty-rule). Baseline measured this session: 669 passed / 0 failed / 2 ignored (not the stale 667 from the pre-recarve 0105 plan; intrinsic-bodies added 2 tests). |
||
|
Brummel
|
3ec406e687 |
spec: raw-buf — re-carve .2/.3/.4 post intrinsic-bodies (refs #7)
raw-buf.1 (intercept registry) shipped (
|
||
|
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
|
298fc2d36f |
plan: intrinsic-bodies.2-migration-lock — 4-task prelude migration + bijection pin (refs #9)
Decomposes intrinsic-bodies.2 (parent spec § Architecture points 6-8)
into 4 tasks + a final gate:
Task 1 — migrate the 13 authored prelude dummy bodies to (intrinsic):
7 Eq/Ord instance methods (inner (body false)/(body true)/
(body (term-ctor Ordering EQ)) → (intrinsic), Design X lambda-body
placement) + 6 float_* fns ((body false) → (intrinsic)). Gated by
round-trip + the 4 eq/compare/float E2E ratifiers staying green
(behaviour-preserving: the intercepts emit identical IR).
Task 2 — rebaseline the two moving hash pins: prelude_module_hash_pin
(prelude module hash) and mono_hash_stability's 6 eq/compare
def-hashes (capture-from-failure, replace the constant). The 4
show__* pins do NOT move.
Task 3 — replace the one-directional registry_contains_all_legacy_arms
pin with intercepts_bijection_with_intrinsic_markers: an in-source
test that walks prelude + kernel_stub pre-mono for Term::Intrinsic
markers, recovers mangled names (mono_symbol for instance methods,
fn name for top-level), and asserts the bijection over the
intrinsic-backed class (14) with the 5-name *__Int optimisation-only
allowlist. Both directions + a stale-allowlist guard.
Task 4 — confirm no codegen path lowers an intercepted body (already
true post-.1: intercept-by-name precedes lower_term), delete the
stale dummy-body comment at lib.rs:1310-1319, and conditionally edit
0007-honesty-rule.md ONLY if it names the dummies (recon: it does
not — a general rule; no forced edit).
Recon-driven plan decisions:
1. The bijection pin lives in intercepts.rs's in-source #[cfg(test)]
mod tests, NOT a crates/ail/tests integration test. Visibility
forces it: the pin needs INTERCEPTS (pub(crate) in codegen, in-source
only) AND the parse hops (ailang-surface dev-dep). Verified
ailang-surface does not dep ailang-codegen, so there is no
dev-dep cycle blocking the in-source test from calling parse_prelude
(the dev-dep-cycle hazard that bit pd.2.4/pd.3.1 does not apply
here — that was the ailang-core <-> ailang-surface edge).
2. The pin walks PRE-mono (parse_prelude/parse_kernel_stub) and
reconstructs mangled names via mono_symbol, rather than walking
post-mono. Post-mono only synthesises USED mono symbols, so a
post-mono walk would miss any instance method the pin's entry
fixture does not exercise (e.g. eq__Unit). Pre-mono + mono_symbol
sees all 14 markers unconditionally.
3. Task 2's hashes are capture-from-failure, not pre-computed — the new
prelude bytes determine them. The old->new values get recorded in
the iter commit body by the Boss.
All verification filter strings checked against the tree: the 4 E2E
ratifier fn names, the mono pin name, and the prelude pin target all
resolve to ≥1 real test. No ail/ail-json/ll fenced block in the plan
(the migrated-form snippets are scheme fragments — the (intrinsic) form
is already ratified by .1's kernel_intrinsic_smoke.ail), so the
parse-bytes gate is a documented no-op.
Handoff target: skills/implement on docs/plans/0107-intrinsic-bodies.2-migration-lock.md
|