main
191 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
|
|
72d2d9c806 |
test: prune duplicate tests, re-sight two blind coverage guards
Follow-up to a fan-out audit of the whole test suite (742 tests, 21
read-only assessors + synthesis). Two clusters of the audit were
actioned here; the #66 hashing-removal cohort it surfaced is left for
the #66 scope, and the RED-first doc-rot sweep is deferred.
§2 — true duplicates removed (each kept test is a strict superset or
identical fixture+assertions of the deleted one):
- ailang-check param_in_reject_message_names_allowed_set (kept the
_renders_allowed_set_in_ailang_syntax superset)
- ailang-check cross_module_pat_ctor_typedriven_resolves (kept ct2_;
shared cross_module_ws helper retained, 2 other callers)
- ailang-core mq1_qualified_instancedef_class_accepted (kept ct1_)
- ail e2e bool_to_str_emits_true_branch (kept the rc-stats superset)
- ail loop_recur_str adt-leg guard (the standalone heap pin owns it;
dropped the dangling header reference too)
- ailang-check over_strict_mode_silent_when_param_is_borrow (its
assertion is subsumed by explicit_fn_with_no_uses_is_clean; its own
doc claimed a "borrowing body" the Lit body never provided)
§4 — meta-guards that had gone partially blind re-sighted:
- spec_drift::spec_mentions_every_def_kind now pushes Class/Instance
exemplars and asserts their `(class `/`(instance` anchors; the
"wait for 22b.4" exclusion was stale (anchors shipped in
|
||
|
|
d72fe0c2e6 |
fix(codegen): drop branch-consume-split owned params (#63 leg 3)
The last leg of the #63 drop-soundness cluster: an (own ...) heap param consumed on one match-arm / if-branch but live on a sibling was never dropped on the live path, leaking one slab per call. This was the residual live=2 leak in series_sma that kept the series headline from being leak-clean. Root: the per-fn aggregate consume_count (the worst-case max over all branches from uniqueness::merge_states) was codegen's only consume signal, and every owned-param drop site gated on it. A param consumed on SOME branch makes the aggregate >= 1, so every site skipped it — including the branch where it stays live. match and if share this root (if is first-class MTerm::If, not desugared to match). Mechanism (spec 0068): - CAPTURE: uniqueness retains the per-branch consume snapshots it already computes per branch and discarded at the max merge — new BranchConsume + infer_module_with_cross_branches (the aggregate-only infer_module_with_cross now delegates and drops the channel). - CARRY: additive MArm.consume / MTerm::If.{then,else}_consume, attached by lower_to_mir via a traversal-order cursor (post-order pop, kind- and exhaustion-asserts make a desync a loud panic; neutral for const bodies which uniqueness does not walk). The AST carries no node id, so the correspondence is the structural pre-order both walks share — pinned by branch_consume_maps_attach_to_matching_arms. - GATE: emit_leakclass_branch_param_drops fires a fall-through drop only for the leak class (branch_consume==0 AND aggregate>=1), in match arms + both if branches; the pre-tail-call dec switches its gate source from the aggregate to per-arm. The fn-return dec and arm-close pattern-binder dec are UNCHANGED. Safety: - Double-free: the drop sites partition by aggregate (==0 -> existing fn-return/pre-tail-call; >=1 -> new per-branch). Disjoint, so no param is dropped twice — no fn-return disable, no tail-position analysis. - Use-after-free: the checker rejects use-after-consume, so an aggregate>=1 param is provably dead past the construct (path-terminal drop, tail position irrelevant). - Type eligibility (found by the full-suite gate during implement; spec 0068 refined): the new agg>=1 site is the FIRST drop site that can reach a STATIC closure-pair param (a top-level fn ref like inc in Either.either, consumed on one arm, live on the other) — a .rodata constant with no rc-header. field_drop_call routes Type::Fn / static-Str / Type::Var to the bare ailang_rc_dec, which underflowed on it. The helper now drops only params with a real per-type heap-ADT drop fn (field_drop_call != "ailang_rc_dec"). Sound (no underflow) and leak-correct (a static closure/Str allocates nothing). Witnessed green by std_either_demo / std_list_demo / poly_rec_capture_demo. Verification: full workspace suite green (116 binaries); both new leak pins (if + match) and series_sma_no_leak_pin green at live=0; legs 1/2 pins still green; INTERCEPTS<->(intrinsic) bijection intact; no Pattern::Lit reject path added. The leg-3 helper's type precondition was applied inline by the orchestrator (a narrowing guard clause in an already-reviewed Task-4 helper, full context loaded) after the implement-orchestrator correctly surfaced the spec gap rather than papering over the regression. This clears the series_sma leak tail; the series milestone (#61) close stays a separate deliberate step (its end-to-end milestone fieldtest). closes #63 |
||
|
|
b11a6d9883 |
fix(mono): thread declared return type into mono synth re-entry
GREEN for the series-step-1 base-tier RED (
|
||
|
|
625fe849be |
docs(contracts): reconcile contracts + honesty-pin with shipped reality
First tranche of a contracts-against-code audit (the inverse of the
usual direction: testing the ledger's claims against the code). Each
fix here is a verified factual divergence between a contract and the
code; the direction of the fix follows which side actually drifted.
Code drifted from the stated goal -> fix the code:
- 0014's claim 6 ("`cargo doc --no-deps` runs warning-free") was the
design goal; reality had 6 warnings. Demote the offending intra-doc
links to plain code spans so the docs match the goal:
- ailang-core: `[`load_workspace`]` cannot resolve from core (the
fn lives in ailang-surface, which core may not depend on) — three
sites in workspace.rs.
- ailang-check: three public-item docs linked the `pub(crate)`
helpers `qualify_local_types` / `qualify_workspace_types`.
`cargo doc --no-deps --workspace` is now warning-free.
Contract stale, code legitimately advanced -> fix the contract:
- 0011 stated `float_to_str` "codegen is reserved and not yet
shipped". It is shipped: lowers to `@ailang_float_to_str(double)`,
green under the codegen `float_to_str_no_longer_errors_internal`
unit test and the e2e `float_to_str_smoke`. The docs_honesty_pin
anchor that protected the stale "reserved" wording moved in lockstep
to assert the present-tense lowering instead — the pin had been
guarding a claim the code already falsified.
- 0013 named the diagnostic `ConstraintReferencesUnboundTypeVar`; the
variant is `UnboundConstraintTypeVar` (workspace.rs), and its scope
is a class-method signature whose constraint mentions a tyvar bound
neither by the method's `forall` nor by the class `param`.
- 0017 called the primitive Eq/Ord bodies "placeholder lambdas"; they
carry the `(intrinsic)` marker — the lockstep partner to the
INTERCEPTS registry, not a placeholder.
- 0009 said "seven" `.ail.json` carve-outs and described the inventory
test as pinning seven; the test pins twelve (7 subject-matter + 4
recur + 1 loop-binder, per carve_out_inventory.rs).
Verified separately: 0001's "pretty-printer code in pretty.rs was
deleted, leaving only diagnostic helpers" is factually correct (an
audit agent misread it as "pretty.rs was deleted"); its only issue is
history phrasing, deferred to the honesty-prose tranche.
Deferred to later tranches: honesty-rule prose (history/rationale that
is not a protected honest-reserved/tiebreaker anchor), stale/mislinked
ratifying-tests (0014's `architect_sweeps.sh`, 0015's uniqueness
in-source tests), 0014's never-existent `tests/expected/`, 0012's
non-exhaustive tail-context list, and the 0016<->0013 redundancy.
|
||
|
|
1be2c1f145 |
docs: fix doc_lazy_continuation across the workspace
Eighteen markdown list items in module- and item-doc comments had continuation lines that were not indented to align under the item text, so rustdoc rendered them as separate paragraphs and broke the list. Corrected the indentation (and, at two sites where a general wrap-up sentence followed a sublist, separated it with a blank doc line so it does not mis-attach to the last item). Doc whitespace only; no prose reworded, no code changed. Workspace clippy is now warning-clean. |
||
|
|
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. |
||
|
|
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. |
||
|
|
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. |
||
|
|
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. |
||
|
|
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. |
||
|
|
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 |
||
|
|
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 (
|
||
|
|
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 |
||
|
|
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
|
||
|
|
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 |
||
|
|
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 |
||
|
|
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 |
||
|
|
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
|
||
|
|
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 |
||
|
|
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 |
||
|
|
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
|
||
|
|
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). |
||
|
|
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. |
||
|
|
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.
|
||
|
|
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` ( |
||
|
|
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. |
||
|
|
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.
|
||
|
|
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 |
||
|
|
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
|
||
|
|
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 |
||
|
|
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. |
||
|
|
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.
|
||
|
|
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).
|
||
|
|
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. |
||
|
|
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 (
|
||
|
|
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
|
||
|
|
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). |
||
|
|
52ff8738b8 |
iter intrinsic-bodies.1-mechanism (DONE 8/8): Term::Intrinsic leaf + cross-crate wiring (refs #9)
First iteration of the intrinsic-bodies milestone. Introduces the
Form-A `(intrinsic)` body marker as a new leaf AST term and wires it
through surface, checker, codegen, and a kernel_stub ratifier. The
prelude migration + hard-lockstep pin + dead-path removal are .2.
What landed (8 tasks):
Task 1 — Term::Intrinsic unit variant (ast.rs), tag "t":"intrinsic"
via the enum's rename_all=lowercase. Additive: no existing fixture
carries it, hashes bit-identical. In-core exhaustive-match arms
(canonical/hash/visit/pretty/desugar/workspace) added as leaves.
Task 2 — surface parse + print: (intrinsic) as a fn body-slot clause
and a lambda positional body, mapped to/from Term::Intrinsic.
Task 3 — cross-crate walker sweep (check/codegen/prose/ail-main):
leaf no-op/identity arms at every no-wildcard Term match the
compiler flagged.
Task 4 — checker: new Env.current_module_kernel_tier flag (m.kernel
|| m.name=="prelude"), set alongside current_module. A def whose
body is intrinsic (top-level fn OR instance-method lambda, via the
shared is_intrinsic_body helper) is checked signature-only; an
intrinsic body outside kernel-tier/prelude is rejected with
intrinsic-outside-kernel-tier.
Task 5 — codegen: an intrinsic-bodied fn routes through the existing
try_emit_primitive_instance_body / intercepts::lookup path; if no
intercept fired it is an internal error, never a lower_term
fallthrough. lower_term and the synth walker get Term::Intrinsic
internal-error arms (an intrinsic body reaching either is an
escape bug).
Task 6 — answer intercept (ret i64 42) registered in INTERCEPTS;
the `answer : () -> Int` intrinsic added to STUB_AIL;
examples/kernel_intrinsic_smoke.ail added so schema_coverage
observes Term::Intrinsic in the examples/ corpus.
Task 7 — E2E ratifier: examples/kernel_answer.ail calls
kernel_stub.answer and prints 42; answer_intrinsic_builds_and_runs_printing_42
asserts it end-to-end (source → native).
Task 8 — design/contracts/0002-data-model.md gains the
{ "t": "intrinsic" } Term entry + fn/lam prose; form_a.md grammar
note updated.
Verification:
cargo test --workspace → 669 passed, 0 failed (baseline 667 +2:
intrinsic_in_user_module_is_rejected, answer_intrinsic_builds_and_runs_printing_42).
bench/check.py + bench/compile_check.py → 0 regressed.
Reject E2E (subprocess ail check --json, exit 1, code
intrinsic-outside-kernel-tier) GREEN.
Round-trip + hash pins GREEN — Term::Intrinsic is additive, no
existing fixture carries it, no hash moved.
Three implementation completions beyond the plan (all behaviour-
preserving, surfaced during execution):
1. The signature-only skip had to apply at the mono pass's two
synth-on-body re-entry sites (collect_mono_targets,
collect_residuals_ordered), not only check_fn — else an intrinsic
body hits synth's Term::Intrinsic internal-error guard. Repaired by
extracting the shared crate::is_intrinsic_body helper and applying
it at all three synth-on-body paths. Not a representation surprise:
the same signature-only treatment, more call sites.
2. The compiler-enumerated exhaustive-match set was broader than the
plan's named grep set (the plan anticipated this and made the sweep
compile-driven). Extra leaf arms in core desugar/workspace, check
reuse-as + qualify_workspace_term, codegen synth_with_extras,
ail/src/main.rs, and four test targets.
3. Fixture corrections: emit_answer needed the body-close
(block terminator) the plan snippet omitted; kernel_answer.ail's
main is (ret Unit)(effects IO) using (app print ...) since
io/print_int does not exist (the plan flagged this for the
implementer to resolve against real effect-op names).
IR snapshots (hello/sum/list/max3/ws_main.ll) refreshed: purely
additive @ail_kernel_stub_answer fn+adapter+closure, emitted into
every workspace exactly as the pre-existing @ail_kernel_stub_new
already was (kernel_stub is auto-injected; confirmed new was present
in the pre-iter hello.ll baseline). No user-fn IR changed.
The .2 iteration migrates the 18 prelude dummy bodies to (intrinsic),
upgrades registry_contains_all_legacy_arms to a source<->registry
bijection pin, and removes the dead body-lowering path.
|
||
|
|
a163c8c34a |
GREEN: pre-pass/resolver asymmetry — same-module bare + kernel-tier qualifier acceptance (closes F1, F3)
Two minimal edits in ailang-check that bring the resolver's acceptance set into line with what prep.1's workspace pre-pass (`prepare_workspace_for_check`) actually produces. The pre-pass itself is unchanged — its qualification rules are correct per spec § "Realisation mechanism — workspace pre-pass". RED tests landed in 4d39fdc; both turn GREEN, both fieldtest fixtures that surfaced the bugs now `ail check` clean. F1 — same-module type-scoped call (kem_2b_min_repro.ail). The dot-qualified `Term::Var` arm in `synth_term` (`crates/ailang-check/src/lib.rs` ~line 3425) was unconditionally rewriting the resolved fn signature via `qualify_local_types`, so a call like `(app Counter.value c)` from inside Counter's home module produced a return type `<this>.Counter` — but the matching `Term::Ctor` arm (~line 3644) and the pre-pass itself both leave own-module type-names bare. The two halves of the resolver disagreed. Fix: branch on `target_module == env.current_module` — when true, skip the qualification (the raw type is already in the form the rest of the resolver speaks); when false, qualify as before. `owner_types` lookup moved inside the else-branch since it's only consulted when qualification runs. A short comment names the pre-pass and the sibling Term::Ctor arm so a future reader sees the three-way symmetry. F3 — kernel-tier qualifier acceptance (kem_3_stub_consumer.ail). The env-builder paths `build_check_env` (~line 1653) and `check_in_workspace` (~line 1807) force-injected only `"prelude"` into `env.imports` / `env.module_imports`. The loader meanwhile derives the implicit-imports list from `modules.values().filter(|m| m.kernel)` (since prep.3) — so `kernel_stub` flows into runtime resolution but not into the checker's qualifier-validity check (~line 1968). Bare `StubT` got qualified by the pre-pass to `kernel_stub.StubT`, then bounced off the validity check as "unknown module prefix". Fix at both sites: keep the unconditional `"prelude"` literal injection AND additively insert every workspace module with `kernel: true` into the per-module import map (skip self-injection). Idempotent for production (where prelude also carries `kernel: true`) and preserves the `bare_name_resolves_through_implicit_import_to_free_fn` unit-test contract — that test deliberately constructs a prelude module with `kernel: false` to pin the legacy "prelude is always implicit" guarantee per se, independent of the kernel flag. Mirrors the loader's kernel-flag filter, making the env-builder and the loader speak the same set. Sibling pin `crates/ailang-check/tests/env_construction_pin.rs` (the frozen-reproduction copy of `build_check_env`'s `module_imports` loop) updated in lockstep so it remains a meaningful drift detector after the env-builder change. The pin is intentionally designed to track legitimate behavioural changes. Verification: - tests::type_scoped_call_in_same_module_resolves GREEN - tests::kernel_tier_module_qualifier_resolves_… GREEN - examples/fieldtest/kem_2b_min_repro.ail ail check ok - examples/fieldtest/kem_3_stub_consumer.ail ail check ok - cargo test --workspace 666 / 0 (664 prior baseline + 2 RED→GREEN this iter) Implementer notes: one re-loop on the F3 site after the first edit replaced the legacy "prelude" literal injection wholesale with the kernel-flag filter — that broke the unit-test contract above. Restored the literal AND added the filter on top per the "don't adapt tests to bugs" memory. No spec-review or quality-review loops. prep.1's pre-pass design (spec § "Realisation mechanism") was correct as written — the symmetry between owner-side `qualify_local_types` and consumer-side `prepare_workspace_for_check` holds. What was missing was uniform resolver-side acceptance of the qualifiers the pre-pass produces. With these two edits, the following equivalences hold throughout the checker: bare T ≡ <this-module>.T (F1, same-module rule) bare T ≡ <kernel-module>.T (F3, kernel-tier rule) via the loader-driven implicit-imports list that now drives both the checker's import map and the type-validity check. |
||
|
|
4d39fdc9c0 |
RED: same-module type-scoped call + kernel-tier qualifier — pre-pass/resolver asymmetry (refs F1, F3)
Two failing in-source tests added to ailang-check, both pinning
the pre-pass / resolver mismatch surfaced by the fieldtest:
tests::type_scoped_call_in_same_module_resolves
F1: `(app Counter.value c)` from inside Counter's own home
module must check clean. Currently fails with
`[type-mismatch] main: type mismatch: expected
<this>.Counter, got Counter` because the dot-qualified
Term::Var arm at lib.rs ~3430 unconditionally calls
qualify_local_types on the resolved fn signature even when
target_module == env.current_module, while the matching
local Term::Ctor branch (~3644) returns bare `Counter`.
The two halves of the resolver disagree on whether
`<this>.T` and bare `T` denote the same type.
tests::kernel_tier_module_qualifier_resolves_without_explicit_import
F3: `(con StubT (con Int))` in a consumer type signature
must resolve without `(import kernel_stub)`. Currently
fails with `[unknown-module] … unknown module prefix
`kernel_stub` …` because env.imports / env.module_imports
(built at ~1797 and ~1667) force-inject only `prelude` from
the kernel-tier set; the pre-pass freely produces
`kernel_stub.StubT` qualifiers that then bounce off the
qualifier-validity check at ~1968.
Shared root: in both bugs the workspace pre-pass synthesises a
qualifier (`<this>.T` for F1, `<kernel_mod>.T` for F3) that some
downstream consumer of the resolver does not accept. The fix
surface is the resolver-acceptance side in both cases — the
pre-pass's qualification rules are correct per the spec's
§ "Realisation mechanism — workspace pre-pass". Implementation
will be two minimal edits to distinct files-and-functions
(no sweeping refactor).
GREEN side handed to implement mini-mode in the next dispatch.
|
||
|
|
9339279181 |
iter prep.3-kernel-tier-modules (DONE 9/9): kernel-tier modules + param-in + stub crate — closes #33
Terminal iteration of the kernel-extension-mechanics milestone. Ships
the four language-level mechanisms named in the spec's § Goal:
Module.kernel + TypeDef.param-in schema, their Form-A surface,
flag-driven kernel-tier auto-injection, and generic param-in checker
enforcement with a new diagnostic.
Schema (Tasks 1+2). Module gains a `kernel: bool` field
(skip_serializing_if = is_false), TypeDef gains a
`param_in: BTreeMap<String, BTreeSet<String>>` field
(skip-if-empty, kebab-renamed to "param-in"). Both fields are
strictly additive — every pre-existing fixture's canonical-JSON hash
is bit-stable except `prelude.ail`, which intentionally gains
`(kernel)`. The struct-literal sweep covered ~104 Module sites and
~35 TypeDef sites across the workspace; the additive serde-default
covers JSON deserialise paths, only Rust struct literals broke.
Form-A surface (Tasks 3+4). `(kernel)` is a bare module-header
attribute; `(param-in (a Int Float) (b Str))` is one outer
TypeDef-body clause carrying one or more inner var-lists (OQ1
decision — mirrors `(ctors …)`, one parser arm, deterministic
BTreeMap iteration). Both round-trip Form-A → JSON → Form-A
bit-identical.
Workspace-load migration (Task 5). The hardcoded `&["prelude"]`
literal at loader.rs:108 became a `modules.values().filter(|m|
m.kernel)` derivation; `parse_prelude()` injection stays because
the prelude has no on-disk manifest in user workspaces. Prelude
now carries `(kernel)` in its source, so the new filter picks it
up automatically. Code-path migration only — observable behaviour
is identical (prelude_free_fns.rs stays green). prelude hash
re-pinned (af372f28c726f29f) with Honesty-Rule provenance comment.
WorkspaceLoadError::ReservedModuleName diagnostic prose
repurposed: any built-in kernel module name is reserved
(currently prelude + kernel_stub), not specifically prelude. CLI
mapping at main.rs updated in lockstep.
Stub crate (Task 6). New `crates/ailang-kernel-stub/` is a
zero-dependency leaf crate carrying only `pub const STUB_AIL:
&str` with the Form-A source of the kernel_stub module (one
parametric TypeDef with param-in, one ctor). The parse hop —
`parse_kernel_stub()` — lives in ailang-surface next to
parse_prelude, keeping the crate-dependency graph acyclic
(`ailang-surface → ailang-kernel-stub → ailang-core`, no
back-edge). The stub is injected unconditionally in all builds as
the ratifying fixture for the kernel-extension mechanism; future
base extensions may add more or retire the stub. Drift-pinned by
`kernel_stub_module_round_trips`.
Checker (Task 7). New `CheckError::ParamNotInRestrictedSet`
variant + code() + ctx() arms + enforcement in
`check_type_well_formed`'s Type::Con arm — generic, data-driven
from the TypeDef, mentions no specific extension type. Two
in-source tests pin both the rejection (`Str` outside `{Int,
Float}`) and the acceptance (`Int` inside) paths.
Workspace-load integration tests (Task 8). New
`workspace_kernel.rs` integration-test crate with three tests:
auto-import without explicit `(import …)` declaration, two
kernel-tier modules co-load, explicit-import-overrides-auto-
import precedence preserved. Loader is import-tree-only so the
auto-import tests use a bridge module that brings the kernel
module into the workspace via the import graph — docstring
captures the reachability nuance for future readers.
Doc-state transitions (Task 9). INDEX.md kernel-extensions row
annotation transitions from "design accepted 2026-05-28; impl in
progress" to "mechanisms milestone closed 2026-05-28; raw-buf and
series milestones pending". Whitepaper STATUS + auto-import +
param-in sections transitioned forward→present for shipped
mechanisms; forward-tense survives only in sections describing
the still-pending raw-buf/series milestones (per Honesty-Rule).
data-model contract gains anchor blocks for both new schema
fields.
Side-effect: every binary's IR snapshot now contains ~52 lines
for `drop_kernel_stub_StubT` because the stub is auto-injected
into every workspace load. Snapshots refreshed; e2e expects 4
modules per workspace (prelude + kernel_stub + entry + zero or
more user modules) instead of the previous 3.
Plan defects scrubbed in the implementation (folded back into
the planner template via the planner's self-review checklist
next time): Task 4 sample test src used fictional
`(ctors (MkT a))` list form (project grammar is per-`(ctor MkT
a)`); Task 6 original wiring would have created a cycle
ailang-surface → ailang-kernel-stub → ailang-surface (inverted —
stub crate is zero-dep, parse hop lives in surface); Task 7 in-
source tests referenced a fictional `check_type_in_module`
helper (used the existing Workspace + check_workspace
convention); Task 8 first integration test expected loader to
auto-load kernel modules from disk (loader is import-tree-only;
tests use a bridge module).
Concern-5 fix folded in pre-commit: workspace.rs ReservedModuleName
doc-prose initially said "in test/dev builds" for kernel_stub —
but stub is unconditionally injected in all builds. Doc copy
tightened to present-state per Honesty-Rule.
Stats: 0 spec-review-loops, 0 quality-review-loops, 2 sweep-script
retries on Task 2 (brace-depth bug on nested vec![Ctor{…}],
recovered via per-file checkout + rewritten anchor-on-existing-
field sweep), 1 e2e-snapshot refresh on Task 6.
|
||
|
|
078c39a76a |
iter prep.2-term-new-construct (DONE 4/4): Term::New AST + Form-A surface + checker + drift — closes #32
Second iteration of the kernel-extension-mechanics milestone. Ships
the `new` Form-A keyword + `Term::New { type_name, args: Vec<NewArg> }`
AST variant + `NewArg::Type|Value` enum end-to-end through schema /
surface / checker, with two new diagnostics
(`NewTypeNotConstructible`, `NewArgKindMismatch`), a new arm in
prep.1's workspace-wide normalisation pre-pass `qualify_workspace_term`
that rewrites bare `Term::New.type_name` to qualified form
(symmetric to the existing `Term::Ctor` arm), and the data-model.md
+ form_a.md anchor additions. Codegen out of scope per spec; codegen
sites get `CodegenError::Internal` arms naming the raw-buf milestone
as the carrier.
Verification:
- `cargo test --workspace`: 654 tests passing, 0 failed.
- 3 new in-source checker tests pin the elaboration paths:
`new_resolves_via_type_scope` (the spec's worked Counter example
checks cleanly), `new_type_not_constructible` (missing `new` def
in home module fires the new diagnostic), `new_arg_kind_mismatch_value_where_type`
(kind-mismatch detection).
- 2 new schema-drift pins (`term_new_round_trips`,
`term_new_type_arg_round_trips`) ratify the JSON byte shape:
`{"t": "new", "type": "<TypeName>", "args": [{"kind": "type"|"value",
"value": ...}]}`.
- 1 new surface round-trip pin exercises mixed-kind args through
Form-A → JSON → Form-A.
- 44+ exhaustive Term-match sites across 24 files extended with
`Term::New` arms — workspace-wide cargo build clean.
Concerns documented inline:
- `crates/ailang-core/tests/schema_coverage.rs` deliberately does
NOT register `VariantTag::TermNew` in the `EXPECTED_VARIANTS`
set. The coverage test asserts every declared variant is
observed in the .ail fixture corpus; no .ail fixture in the
current tree emits `"t": "new"` (codegen-runnable Term::New
programs require the raw-buf milestone's plugin registry).
Registering would fail the coverage check. The `visit_term` arm
IS extended (compile-forced); only the enum registration is
deferred. Inline rationale in the source. Future milestone that
ships a Term::New fixture extends both sides.
- `crates/ailang-surface/src/print.rs` `write_term` Term::New arm
was added in Task 1 (not Task 2 as planned), because without it
ailang-core's tests fail to compile (the surface crate is in
the dependency graph of ailang-core's test binaries). Task 2's
round-trip pin verified the arm's correctness.
- Task 3 (synth elaboration) needed one implementer re-loop: the
first attempt over-qualified within-module type-references via
`qualify_local_types` on `new`'s signature when the home module
was the calling module itself. Fixed by skipping qualification
when `home_module == env.current_module`.
Architectural composition with prep.1: `Term::New` joins
`Term::Ctor` as a `type_name`-bearing site that goes through
`qualify_workspace_term`'s bare→qualified rewrite before the
checker sees it. The checker's `synth` arm for `Term::New`
therefore receives an already-qualified `type_name` (or a local
bare name for same-module construction).
Milestone status: kernel-extension-mechanics (Gitea #6) advances
2/3 iters. Next: prep.3 (kernel-tier modules + param-in), issue #33.
|
||
|
|
b586999e81 |
iter prep.1-type-scoped-namespacing (DONE 5/5): TypeDef-first resolution + workspace pre-pass — closes #31
First iteration of the kernel-extension-mechanics milestone. Ships
the type-scoped `<TypeName>.<member>` resolution path as the
canonical form for type-associated operations, narrows the
`BareCrossModuleTypeRef` / `BadCrossModuleTypeRef` diagnostics from
"bare = strictly local" to "bare = in-scope by any path", migrates
12 std-library example fixtures, and introduces a workspace-wide
normalisation pre-pass `prepare_workspace_for_check` shared between
`check_workspace` and `monomorphise_workspace`.
Architectural discovery during implementation: the plan covered the
`Term::Var` dot-qualified resolver layer plus the workspace
validator's bare-name acceptance, but the migration of bare-form
fixtures exposed five sites where bare vs. qualified type-names
needed symmetric treatment — `Term::Ctor` resolution, `Type::Con`
well-formedness, mono's poly-free-fn name/constraint-count
enumeration, codegen's `lookup_ctor_by_type` bare-name path, and
the upstream desugar-then-qualify composition. Rather than
scattering TypeDef-first ladders across each site, the implementer
centralised the work into one pre-pass that walks every consumer
module's `Type::Con.name` and `Term::Ctor.type_name`, rewriting
bare cross-module references to their qualified `<home>.<Type>`
form. This is symmetric to the pre-existing `qualify_local_types`
(owner-side); the new pre-pass is the consumer-side mirror.
Downstream passes see qualified Types regardless of authoring form.
The TypeDef-first ladder still lives in `synth`'s `Term::Var` arm
because `<TypeName>.<member>` is term-position-only — `Maybe.from_maybe`
is a Var, not a Type expression, and the pre-pass does not rewrite
Var names.
Alternatives considered:
(a) Add TypeDef-first ladder at every resolution site separately
(the plan's implicit assumption). Rejected: O(N) extension
sites, each carrying the same workspace-walking logic; the
pre-pass version is O(1) — one pass, every downstream consumer
benefits.
(b) BLOCKED + spec re-brainstorm. Rejected: the architecture
extension is consistent with prep.1's thesis (bare type-name
resolves to the workspace-wide TypeDef) and forward-compatible
with prep.2 (Term::New.type_name falls under the same rewrite)
and prep.3 (kernel-tier TypeDefs enter the workspace map
automatically). No design regression to bounce back over.
Spec updated to document the realisation mechanism honestly: the
"Realisation mechanism — workspace pre-pass" subsection clarifies
that the resolver-level semantics described in "Implementation
shape" are the user-facing contract, and the actual code path is
the pre-pass.
Verification:
- `cargo test --workspace`: ALL GREEN. 87 e2e + every crate's unit
+ integration tests pass with no regressions.
- Three NEW in-source tests pin Task 1's resolver paths:
`type_scoped_member_resolves`, `type_scoped_member_not_found`,
`type_scoped_receiver_not_a_type`.
- One NEW workspace test pins the narrowed validator:
`ct1_validator_accepts_bare_with_explicit_import`.
- One renamed-and-flipped existing test:
`ct1_validator_rejects_bare_xmod_with_import_candidate` →
`ct1_validator_accepts_bare_xmod_with_import_candidate` (the
bare-with-import path is now ACCEPTED).
- One NEW companion test for the workspace-wide ctor lookup:
`ct2_term_ctor_bare_cross_module_via_workspace_resolves`.
- Two pre-existing tests' assertions updated for the new error
wording: `ct1_check_cli::check_human_mode_emits_actionable_message_to_stderr`
and `crates/ailang-check/tests/workspace.rs::unknown_module_prefix_is_reported`.
- 12 migrated `.ail` fixtures verified via the existing e2e
suite (each fixture is the test runner's target for an existing
`build_and_run` assertion).
- Negative fixture `ct_2_bare_cross_module.ail` semantically
preserved: dropped its `(import std_maybe)` so bare `Maybe` is
out-of-scope under the narrowed rule and still fires
`BareCrossModuleTypeRef`.
Concerns:
- The pre-pass introduces a new architectural layer (consumer-side
qualification) that the spec did not originally anticipate. Spec
amendment in this commit documents the layer. Future iterations
reference `prepare_workspace_for_check` as established
infrastructure.
- `examples/test_ct1_bare_xmod_rejected.ail.json` switched its
offending name from bare `Ordering` (which under the prep.1
semantics may now resolve via implicit prelude) to a still-
unresolvable `Mystery_Type`. The CLI test's intent (assert that
a human-mode `ail check` exits non-zero on a still-RED case) is
preserved.
Milestone status: kernel-extension-mechanics (Gitea #6) advances
1/3 iters. Next: prep.2 (`Term::New` construct) issue #32.
|
||
|
|
832375f2ac |
convention: counter-prefix file naming across docs/specs/, docs/plans/, design/contracts/, design/models/
All 176 files in the four accumulating directories now use a zero-padded 4-digit counter prefix that reflects creation order (`NNNN-slug.md`). The counter is assigned per directory in strict git-log creation order; ties broken alphabetically by original name. The old `YYYY-MM-DD-` prefix on docs/specs/ and docs/plans/ files is dropped — the date is recoverable from git log and the counter carries the ordering. A file's counter is stable for the life of the file: never reassigned, never reused, never compacted. Deleted files retire their counter; subsequent files do not fill the gap. This is the property that lets cross-references stay literal — refs use the full filename including the counter (`design/contracts/0007-honesty-rule.md`) so they grep cleanly and resolve directly without a glob step. 313 cross-references updated across .md/.rs/.toml/.c/.json files (test pins, include_str! paths, design-INDEX entries, baseline notes, runtime C comments, inter-contract markdown links incl. bare basename and `../models/foo.md` forms). CLAUDE.md gets a new "File-naming convention" section spelling out the rule and rationale. skills/brainstorm/SKILL.md and skills/planner/SKILL.md updated so new spec/plan creation produces counter-prefixed names from the start. The full test suite (cargo test --workspace) passes. |
||
|
|
4fc65ccb99 |
iter schema-camelcase-fix.1 (DONE 4/4): paramTypes/retType → param-types/ret-type — closes #30
`Term::Lam`'s two camelCase JSON tags become kebab-case, matching
the convention every other compound-key tag in the AST schema
already follows. After this iter the canonical JSON has zero
camelCase outliers.
## Schema swap (atomic, Task 2)
- `crates/ailang-core/src/ast.rs:492,494` — two
`#[serde(rename)]` strings: `"paramTypes" → "param-types"`,
`"retType" → "ret-type"`. Rust field names unchanged.
- `crates/ailang-core/src/workspace.rs:1925-1926` — in-source
JSON literal in the `ct1_validator_walks_lam_embedded_types`
test.
- `design/contracts/data-model.md:142-147` — fenced JSON block
in the canonical data-model contract. Honesty-Rule touch-point:
the contract document must describe the actual present-state
schema.
- `examples/test_loop_binder_captured_by_lambda.ail.json` and
`experiments/2026-05-12-cross-model-authoring/master/examples/fn_with_lambda.ail.json`
— the two `.ail.json` fixtures whose canonical-JSON embeds
the renamed tags.
The five files moved together within one task because `Term::Lam`
has no `#[serde(default)]` on `param_tys` / `ret_ty` — a
renamed-away key is a hard deserialise error. Splitting the swap
would have left the workspace untestable mid-step.
## RED → GREEN pin (Tasks 1, 2)
`crates/ailang-core/tests/design_schema_drift.rs` gains
`lam_serialises_with_kebab_keys`: pins that `serde_json::to_value(&Term::Lam{...})`
emits `"param-types"` / `"ret-type"` AND does not emit the old
camelCase keys. Companion: the existing
`design_md_anchors_every_term_variant` test now also asserts the
kebab anchors appear inside `data-model.md`'s `lam` fenced block.
Both confirmed RED on entry, GREEN after Task 2.
## Rustdoc honesty pass (Task 3)
Three pure-prose edits keep production rustdoc consistent with
the new schema vocabulary: `crates/ailang-core/src/ast.rs:8` (the
module-level rename enumeration), `crates/ailang-surface/src/parse.rs:81`
(prose mention of `lam`'s carry), `crates/ailang-check/src/lib.rs:1707`
(InstanceMethod routing helper rustdoc). No compile or test
consequence — Honesty-Rule maintenance.
## Plan-pseudo-vs-reality finding: under-audited hash blast radius
The brainstorm spec audited `crates/ailang-core/tests/hash_pin.rs`
exhaustively (5 pinned modules, zero `(lam ...)` occurrences,
"no hash refresh required"). It missed
`crates/ailang-surface/tests/prelude_module_hash_pin.rs` — a
separate hash-pin file in a different crate that pins `prelude.ail`,
which contains 11 `(lam ...)` forms. The prelude module hash
drifted (`6d0577ff0d4e50ac` → `562a03fc57e7e017`); the implementer
refreshed it with a Honesty-Rule provenance comment matching the
precedent set in commit `26fb345`. Form-A is unchanged — only the
canonical-JSON byte stream differs, which is exactly what the
rename targets. The spec-side learning is: schema-rename
brainstorms must walk *every* test crate for hash-pin files, not
just the home crate of the AST.
## Why this shape, and not the alternatives
- *`params-ty` / `ret-ty` (Rust-field-name vibe)* — rejected. The
AST JSON schema follows its own kebab/single-word convention,
not Rust field names. The other multi-word tag (`reuse-as`) is
kebab; abbreviating `params-ty` mixes singular+plural and has
no precedent.
- *Inline typed params as a sub-tag* (e.g. `params: [{name, type}, ...]`)
— rejected. Stronger semantic locality, but it changes schema
topology rather than tag spelling. Out of scope for a camelCase
correction; would have re-pinned far more than this milestone.
- *Bundle with #27 (arith-rename)* — rejected. #27 carries four
open brainstorm questions (mod vs rem, neg vs sub 0, Num class,
deprecation window) and is structurally a separate milestone.
Each gets one re-pin wave with its own rationale; no churn
saving from bundling.
## Honest call on the feature-acceptance gate
Clause 1 (LLM author naturally uses the new form) is the weakest
of the three. Direct empirical evidence is absent — the 2026-05-21
naming-A/B run measured a different axis. The argument is
indirect: a future LLM author generalises from the rest of the
schema ("compound keys are kebab"), and the two camelCase
outliers are precisely the sites where that generalisation
diverged from reality. Clause 2 (redundancy reduction) and
Clause 3 (no semantic surface touched) are direct.
## Forbidden touches verified untouched
`docs/plans/*.md` historic plans (which embed old tag names in
example JSON), `experiments/2026-05-12-cross-model-authoring/master/spec.md`,
`experiments/.../rendered/*.md`, and `experiments/.../runs/**` —
all left as frozen historical artefacts per Honesty-Rule
analogue (describe state at time of writing, not present state).
Verified via `git diff --name-only HEAD` (Task 4 Step 4).
## Verification
- `cargo test --workspace`: all test groups OK, 0 failed,
2 ignored (pre-existing).
- `cargo test -p ailang-surface --test round_trip`: GREEN
(Form-A unchanged invariant).
- New schema-shape pin and the extended data-model anchor walk:
GREEN after Task 2.
- Negative grep across `crates/`, `examples/`, `design/`,
`runtime/`: the only remaining `paramTypes` / `retType`
occurrences in checked-in code are the load-bearing
negative-assertion strings inside the new pin (intentional —
they are what makes the pin RED-able on regression).
- Stats: `bench/orchestrator-stats/2026-05-21-iter-schema-camelcase-fix.json`
— 4/4 tasks DONE, no re-loops, no review-loops.
closes #30
|
||
|
|
5170b6abd1 |
iter operator-routing-eq-ord.1 (DONE 13/13): drop comparator builtins, route through Eq/Ord
Closes Gitea #1. Realises the "P2 follow-up" called out in examples/prelude.ail:9 — removes the surface comparator names `==` / `!=` / `<` / `<=` / `>` / `>=` from the language entirely, routes the LLM-author's `(app eq …)` / `(app compare …)` / `(app ne|lt|le|gt|ge …)` through prelude.Eq / prelude.Ord class- dispatch, ships six named Float-comparison fns (`float_eq`/`float_ne`/`float_lt`/`float_le`/`float_gt`/`float_ge`) so Float keeps comparability without an Eq/Ord instance, and emits primitive instance bodies with `alwaysinline` so the -O0 IR shape stays at one instruction per comparison. Plan-task journal (13 tasks, single atomic iter per Approach A): Task 1 — Bootstrap: 4 new fixtures (eq_user_adt_smoke.ail, eq_float_must_fail.ail, float_compare_smoke.ail, operator_unbound_check.ail) + 5 new E2E/pin tests as RED starting state. All 5 confirmed RED at start: north-star fixed `NoInstance Eq Unit` (preserved by Unit-eq opening line intentionally added in plan-self-review); float_compare unknown `float_eq`; operator-name typechecked (== still polymorphic); must-fail diagnostic lacked `float_eq`; alwaysinline absent from IR. Task 2 — Codegen alwaysinline + intercept arms: introduced `intercept_emit_wants_alwaysinline` allowlist + appended ` alwaysinline` between `)` and `{` of the `define` line in `emit_fn`; added 9 new intercept arms to `try_emit_primitive_instance_body` — `eq__Int`/`eq__Bool`/ `eq__Unit` + the six `float_*` arms. Task 3 — Prelude reshape: `instance Eq Unit` added; Eq Int/Bool bodies become placeholder-`false` (intercept overrides); six `float_*` free fns added; line-9 P2-follow-up comment removed. Lockstep hash re-pins: prelude_module_hash_pin (3abe0d3fa3c11c99 → new), mono_hash_stability six body-hash literals (eq__Int/Bool/Str + compare__Int/Bool/Str all shifted because placeholder body changes the canonical hash). IR-snapshot regen (hello/list/max3/sum/ws_main) rolled forward into this task at orchestrator's pragmatic call — prelude shift forces the snapshots immediately. Task 4 — Fixture migration: 58 .ail fixtures rewritten (`(app == …)` → `(app eq …)`, etc.; Float-typed operand sites to `(app float_eq …)` / `(app float_lt …)`). eq_ord_user_adt.ail:21 inner `==` → `eq` migration with lockstep eq_ord_e2e.rs:134 body-hash re-pin (3c4cf040cb4e8bb2 → new). Two prose snapshots accepted; deps test + 5 hash_pin literals updated as cascading consequences. Task 5 — Test-scaffold migration: all 8 in-source `#[cfg(test)] mod tests` AST-literal sites threaded (desugar.rs:2414, check/lib.rs:5656/6092/6220, codegen/lib.rs sites). 7 obsolete in-source tests deleted (5 eq_typechecks + 2 lower_eq ADT/Fn rejection — coverage moves to E2E eq_user_adt_smoke + eq_float_must_fail). 2 additional letrec tests deleted (single-module check env can't resolve eq/ge without prelude auto-import; covered by workspace E2E). Task 6 — Lit-pattern desugar: build_eq emits `Term::Var { name: "eq" }` instead of `"=="` at desugar.rs:1109; doc-comment rewritten to describe class-dispatch. Task 7 — Dead-machinery deletion sweep (compile-gated): typchecker builtins (install + list comparator entries deleted); codegen builtin_binop_typed (10 comparator arms deleted from synth.rs, table reduced to arithmetic core); lower_eq fn entirely deleted; `==` short-circuit in lower_app deleted; `is_static_callee` `==` clause deleted; `is_arithmetic_or_comparison_op` renamed to `is_arithmetic_op` + caller-update at codegen/lib.rs:2152 + :2529. Dead `poly_a_a_to_bool` helpers also removed. Workspace build green after compile gate — every caller of the deleted surface was migrated by Tasks 4-6. Task 8 — Float-aware NoInstance diagnostic: check/lib.rs:856-880 addendum extended to name `float_eq` / `float_lt` as the explicit alternative for Eq/Ord at Float; eq_float_noinstance.rs:32-44 assertion extended. Task 9 — IR snapshot regen: subsumed by Task 3 (prelude shift forced immediate snapshot regen; deferring to Task 9 would have left the workspace red between tasks). Task 10 — Prose-projection cleanup: 6 comparator arms deleted from binop_info; 3 in-source mod-tests updated/deleted (comparator-infix rendering would be dishonest now that the operators are no longer language identifiers). Task 11 — Contract updates: 5 design files rewritten to the class-dispatch present — float-semantics.md (arithmetic guarantees retained on +/-/*/; comparison guarantees transferred from ==/!=/< to float_eq/float_ne/float_lt/etc.); prelude-classes.md (Eq Unit added to instance list; new paragraph on six float_* fns; Float-no-Eq/Ord clause gains `→ use float_eq` cross-reference); str-abi.md (clause "REMAIN primitive operators" rewritten to describe class-method dispatch); scope-boundaries.md (multiple operator-name and Pattern::Lit-desugar clauses rewritten); authoring-surface.md (==, <= dropped from operator-example list). Task 12 — Initial acceptance gate: workspace 638/0 GREEN; bench/compile_check + cross_lang 0 regressed; bench/check.py flagged 4 regressions on bench_closure_chain (+29% bump_s, +47% rc_s, +29% bump_rss_kb, +48% rc_rss_kb). Orchestrator initially classified as DONE-with-concerns; Boss reclassified as PARTIAL-via-acceptance-#8-fail after independent re-run, extended iter scope to Task 13. Task 13 — Direct icmp intercept arms (Boss-extension): try_emit_primitive_instance_body gains direct-icmp arms for lt__Int / le__Int / gt__Int / ge__Int / ne__Int, bypassing the compare__Int → Ordering → match indirection that allocated one Ordering ctor per call in tight loops. Each new arm inherits `alwaysinline` via the existing allowlist (extended accordingly). New IR pin test `ord_int_intercept_ir_pin.rs` + smoke fixture `ord_int_intercept_smoke.ail` ratify the optimization — opt -O2 -S confirms zero `call @ail_prelude_lt__Int` in optimized IR; the icmp folds directly at every use site. Bool variants (lt__Bool/etc.) deliberately NOT added — no bench/example calls Ord at Bool; spec-extension permits skipping if unreachable at bench level. Family can be extended symmetrically when first Bool-ordered perf workload appears. Bench-gate post-Task-13: bench_closure_chain bump_s -6.05%, rc_s -2.67%, bump_rss_kb -0.77%, rc_rss_kb +0.46% — all four previously-regressed metrics back inside tolerance. Full bench corpus: 36 metrics, 0 regressed, 0 improved beyond tolerance, 36 stable. bench/check.py exit 0 ✓; bench/compile_check.py exit 0 ✓; bench/cross_lang.py exit 0 ✓. Workspace: 640 passed, 0 failed across all binaries (delta vs. milestone start: +5 new E2E/pin tests added in Task 1 + 1 IR pin added in Task 13 − 9 in-source mod tests deleted as obsolete net ≈ −3). The eq_user_adt_smoke fixture's Unit-opening line was the deliberate RED-first device added in planner self-review so the north-star wouldn't accidentally GREEN at start (user-ADT-Eq on Point with hand-written instance was already operable today; the milestone's actual delivery is operator-name death + Eq Unit + Float-named-fns + cleanup of the two-pathy primitive comparator machinery). Net delta: 96 files changed, 1760 insertions, 1101 deletions; 12 net-new files (6 new fixtures, 5 new E2E/pin tests, 1 stats file). main passes-test-count: 640 (was 633 pre-iter, accounting for the deletions). Spec-vs-acceptance addendum: spec §Testing strategy anticipated the bench-gate-regression case with two recovery paths (`alwaysinline` investigation or "spec needs revisiting toward α"). Task 13 is the third path — direct intercept arms for `lt`/etc. that bypass the compare→match path entirely. The spec's contingency clause was thus generous enough to absorb Task 13 without spec revision, but a future iter that hits a class-method primitive where the body shape introduces a similar codegen cost (Ordering allocation, RC tax, deferred-init) should expect a parallel extension. The pattern is "primitive instance whose canonical body indirects through other class methods that allocate" → add a direct-emit intercept arm + alwaysinline + IR-shape pin. Concerns absorbed: - Codegen lower_app / resolve_top_level_fn gained a prelude-fallback lookup so bare monomorphic prelude fns (`float_eq` etc.) resolve from non-prelude modules without explicit `prelude.float_eq` qualifier. Mirrors the typechecker's implicit prelude import — not in plan but necessary infra for the named-fn surface to be callable. - Recon's "≈10 fixtures" estimate was 6× too low — 58 actual. Mechanical migration; no design impact. - Recon caught 4 in-source AST-literal sites the spec missed (lib.rs:5656 `>=` site + three codegen/lib.rs sites); Task 5 covered all. - Recon caught 2 contract files outside the spec's update set that directly contradicted the milestone (str-abi.md + scope-boundaries.md "REMAIN primitive operators" / "Pattern::Lit desugar to ==" clauses); Task 11 covered all 5. Stats file: `bench/orchestrator-stats/2026-05-21-iter-operator-routing-eq-ord.1.json`. closes #1 |
||
|
|
99df14c792 |
workflow: scrub residual JOURNAL/journal refs missed in the first sweep
A re-grep found 15 live references (excluding docs/specs/ and
docs/plans/, which stay historical) the previous two commits
missed — all in source comments, doctests, bench helpers, and one
agent file.
Per-file:
- crates/ail/src/main.rs: typeclass-coherence diagnostic comment
pointed at "the JOURNAL queue's wording" — points at
design/contracts/typeclasses.md alone.
- crates/ailang-prose/src/lib.rs: `//!` header referred to
docs/JOURNAL.md "Pinned: human-readable prose surface" —
retargeted to design/contracts/authoring-surface.md.
- crates/ailang-check/src/lib.rs: bugfix tag + "see iter
method-dispatch-refactor journal" prose collapsed to a clean
rationale paragraph; the canonical shape is stated inline.
- crates/ailang-surface/tests/prelude_decouple_carve_out_pin.rs:
"(d) record the rationale in a per-iter journal" →
"(d) record the rationale in the commit body".
- crates/ailang-surface/tests/prelude_module_hash_pin.rs: header
collapsed (pd.2/pd.3 milestone narrative dropped — the test's
purpose is self-evident from its body); both "per-iter journal"
drift-instructions point at the commit body.
- runtime/rc.c: "bench numbers in JOURNAL 18f.2" →
"original profiling bench numbers".
- bench/run.sh: two "JOURNAL entry" comments → "commit body".
- bench/architect_sweeps.sh: header rewritten (cross-ref to the
design-md-consolidation milestone commits, not a JOURNAL entry).
Sweep-4 extended with two new anti-regrowth phrases
("see the per-iter journal", "in a per-iter journal") so journal
prose can't grow back into design/contracts/ silently.
- skills/audit/agents/ailang-architect.md: "unlike a journal it
lives on main" → "since it lives on main".
- ail-embed/src/bin/timeshard_runner.rs: "records it in the
close-out journal" → "prints it to stderr".
- ail-embed/tests/timeshard.rs: two "journal-only friction timing"
→ "stderr-only friction timing".
Verification (after the edit):
- `grep -rin '\bjournal\b'` against live tree returns exactly two
hits: the Sweep-4 regex itself (intentional — TABU phrases that
prevent regrowth) and the PHRASES array in design_index_pin.rs
(intentional — the same regrowth guard at test level). Both are
load-bearing negative assertions.
- `bash bench/architect_sweeps.sh` exits 0 ("All five sweeps
clean") — no design/-side regrowth.
- `cargo build --workspace` green; `cargo test --workspace` green.
|
||
|
|
54f0ced148 |
workflow: delete docs/journals/ and docs/journal-archive.md
Strict application of the "Future-Use, not Verlauf" criterion to the
two remaining journal artefacts:
- `docs/journals/` (110 files): the per-iter and audit journals from
2026-05-11 onward. Pure history; no live reader after the previous
sweep. Entire directory removed.
- `docs/journals/2026-05-19-design-decision-records.md`: the one file
that had live readers (`docs_honesty_pin.rs:108`, `parse.rs:80`,
`duplicate_ctor_pin.rs:8`, three roadmap.md mentions) and was framed
as a "relitigation guard". On re-examination its three asserted
pinned phrases ("Regions were considered and rejected", the
"demands annotations *because*" rationale, the prose-render
placeholder statement) are rationale-prose, not load-bearing
invariants — the test pinned itself, not a system property. Any
Decision that still holds lives in the code, `design/contracts/`,
or `design/models/`. Removed with the rest.
- `docs/journal-archive.md` (pre-2026-05-11 history): content-frozen
long-tail history with no live reader. Removed; if anyone ever
needs the pre-cutoff rationale they can `git log --before=2026-05-11
--grep=<keyword>`.
Live-file consequences:
- `docs_honesty_pin.rs` `design_md_present_tense_anchors_present`:
the three `records.*` assertions and the `read("docs/journals/…")`
are dropped; the contract/model anchor pins remain.
- `duplicate_ctor_pin.rs`: the "why-two-overlays rationale lives in
docs/journals/…" comment is replaced with the rationale inline.
- `parse.rs`: the "form-refinement rationale lives in docs/journals/…"
comment is dropped (the rule body already states the refinement).
- `roadmap.md`: the decision-records mention in the DESIGN.md →
design/ entry's body is dropped; the journal-archive.md `context:`
pointers across ~12 closed entries are either rephrased to point
at the relevant iter/audit (no path), or simplified to a one-line
comment when the iter name alone carries the story.
- `CLAUDE.md` Roles section: the `docs/journal-archive.md` slot is
removed; vocabulary note rephrased.
- `design/INDEX.md`: the Docs bullet drops `journal-archive.md`.
- `skills/README.md` bootstrap-rationale pointer rephrased.
`docs/specs/` and `docs/plans/` (per-milestone specs and per-iteration
plans) are unaffected — they remain the structured-design artefacts
they were before this sweep.
Workspace builds, full test suite green.
|
||
|
|
8e586f493f |
workflow: replace per-iter journal system with git log + BLOCKED.md
The per-iter journal under docs/journals/ duplicated the iter commit body's substance and accumulated as Verlauf-Doku with no Future-Use. Sweep across all live control documents: CLAUDE.md, the 7 SKILL.md files, the 11 agent files, design/INDEX.md and the contracts/models that referenced journals, docs/roadmap.md, and the handful of source comments + tests that pointed at journal files for rationale. Mechanism changes: - Standing-reading-lists in every agent now read `git log -N --format=full` for recent project state, never per-iter journal files. The architect reads `git log <prev-milestone-close>..HEAD --format=full` for audit scope. - implement-orchestrator no longer writes a journal file. DONE outcomes emit just code + stats; the end-report is the per-task summary the Boss uses to write the commit body. PARTIAL/BLOCKED outcomes emit BLOCKED.md at the repo root — uncommitted by convention, Boss removes on repair or discard. New iron-law line + four-rationalisation row + red-flag bullet codify it. - audit ratify mechanic: --update-baseline is now paired with an explicit ratify paragraph in the audit-close commit body, not a separate JOURNAL ratify entry. - design/contracts/honesty-rule.md: "history and rationale lives in docs/journals/" → "lives in git log (iter and audit commit bodies)". Pinned phrase preserved verbatim. - CLAUDE.md "Roles of …" section reframed: design/, git log, journal-archive.md (content-frozen), roadmap.md, specs/, plans/. No docs/journals/ slot anymore. - roadmap.md context-lines that pointed at per-iter journals are dropped where the spec/commit already carries the rationale, or rephrased to "shipped in the <iter> iter commit" / "docs/journal- archive.md (<date> entry)" for pre-2026-05-11 references. What stays (this commit): - docs/journals/ directory and contents are NOT touched. Removing the contents is a separate follow-up. - docs/journals/2026-05-19-design-decision-records.md still has live readers (docs_honesty_pin.rs Z 108 + parse.rs + duplicate_ctor_pin.rs + 3 roadmap mentions) — also follow-up. - docs/journal-archive.md still exists; its self-pointer header has been updated to drop the "see docs/journals/INDEX.md" mention. Workspace builds, full test suite green. |
||
|
|
ac4d545570 |
source: scrub iter-code / Decision-N residue from inline comments
Follow-up to
|