1be6e49b4fde1fd4645d2a70832e6aa10722d0ff
993 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
 Brummel
|
1be6e49b4f |
test(codegen): RED pin for owned-param leak in tail-recursion (#63)
An owned heap ADT param threaded through a tail-recursive fn whose base-case arm neither forwards nor consumes it is never RC-dec'd, so it leaks one slab per recursion step. Series-free minimal repro (a plain `Box` ADT, no Series/RawBuf), so the pin guards the GENERAL memory-model invariant rather than the Series surface that first surfaced it (examples/series_sma.ail, live=8). The pin builds the fixture with --alloc=rc, runs it under AILANG_RC_STATS=1, and asserts live == 0 (allocs == frees). RED today: `allocs=6 frees=4 live=2`. The fixture passes the replacement ctor directly into the tail call (not let-bound) to isolate leg 1 — the owned-param drop omission — from the second, distinct leg the debugger found (a `let`-wrapped tail call also defeats the scrutinee-husk shallow-dec gate; that leg is what pushes box_ctrl to live=4 and series_sma to live=8, and gets its own pin once leg 1 is green). Cause (debugger, for the GREEN side): the fn-return Own-param dec in crates/ailang-codegen/src/lib.rs (~1444) is gated behind `!block_terminated`, so it fires only on the fall-through ret path; crates/ailang-codegen/src/match_lower.rs (~805) drops only pattern binders, never the fn's owned params. A tail-call-terminated match arm thus has no drop site for an owned param with consume_count==0 that is not forwarded into the tail call. refs #63 |
||
|
Brummel
|
3b3c8c4f07 |
fieldtest(series-step1): 5 examples, 5 findings (1 bug, 1 friction, 1 spec-gap)
Post-ship field test of the shipped `series` library extension as a downstream Form-A author working from the public surface only. Five fixtures under examples/fieldtest/ across the construction/auto-import, ring-buffer/financial-indexing, len/total_count bookkeeping, param-in error-quality, and operator-naming axes; spec at docs/specs/0067-fieldtest-series-step1.md. Wins (carry-on): auto-import works with no `(import series)`; the financial index (0 = newest) maps directly onto the bounded-buffer mental model and stays correct after multiple wraps; the param-in diagnostic for a disallowed element type names the type, the type-variable, the qualified type, and the allowed set. Findings routed: - [bug] An owned ADT threaded through tail-recursion whose base case neither returns nor consumes it is never dropped — a general drop-soundness leak (a plain `Box` control with no Series/RawBuf also leaks). Series surfaces it heavily on the whitepaper's headline streaming pattern, and the committed reference examples/series_sma.ail itself leaks (live=8). Minimal repro: series-step1_5 (live=4). - [friction] `ail describe ... Series.push` (the canonical type-scoped form) reports module-not-found; only `series.push` / bare `push` resolve, and no command lists a type's op set. - [spec_gap] referencing a kernel base type (`RawBuf`) from a user ADT ctor field requires full qualification (`raw_buf.RawBuf`) while bare `Series` works in type-position via auto-import — the asymmetry is undocumented. The fixtures that leak still produce correct output; the leak is a separate observable under AILANG_RC_STATS and an orthogonal, pre-existing bug, not a Series defect. refs #61 |
||
|
Brummel
|
73fbb240be |
docs(model): reconcile 0007 Series with the shipped step-1 reality
The `series` library extension shipped (
|
||
|
Brummel
|
35a9bc67b1 |
feat(series): ship the kernel-tier Series library extension (#61)
Series a is a bounded ring buffer with financial-style indexing (index 0 = newest), shipped as a PURE AILang library extension over RawBuf — zero Rust codegen, zero intercepts, zero (intrinsic) markers. It is the first kernel-tier module that depends on another kernel-tier module (raw_buf). This turns the committed SMA headline pin ( |
||
|
Brummel
|
6b7ee45e49 |
test(series): RED pin for the SMA worked example (#61 headline)
The headline acceptance of #61: the simple-moving-average worked example from design/models/0007-kernel-extensions.md must build via `ail build --alloc=rc`, run, and print the correct moving averages. Green ⇒ the kernel-tier `Series` library extension works end to end (ring-buffer push, financial-style indexing at index 0 = newest, count/total bookkeeping). The fixture is the 0007 worked example with two corrections applied, both verified against the live tool this session: - `>=` is not a surface symbol; the polymorphic Ord helper is `ge` (here on Int operands: total_count vs window size). - `print` on Float emits no trailing newline, so the four averages would concatenate into an unreadable blob. The emit branch now prints the average followed by `io/print_str "\n"`, so each average lands on its own line and the output is deterministic and assertable. (This legibility fix is also queued to be carried back into model 0007.) RED reason (right-for-the-right-reason): `ail check` rejects with [bare-cross-module-type-ref] on `Series` — the kernel-tier module does not exist yet. The fixture itself parses and is otherwise valid. Expected stdout was derived by probing the live %g float formatter independently (the SMA averages are 9/3, 16/3, 17/3, 16/3 over the stream 1,5,3,8,6,2 with window 3): `3.0\n5.33333\n5.66667\n5.33333`. GREEN side (the `series` kernel module + the five ops) is the next mini-mode iteration. |
||
|
Brummel
|
b11a6d9883 |
fix(mono): thread declared return type into mono synth re-entry
GREEN for the series-step-1 base-tier RED (
|
||
|
Brummel
|
e035eff8df |
test(series): RED pin for polymorphic RawBuf element-var forwarding
Base-tier enabling RED for the `series` milestone step 1 (#61). A polymorphic fn that allocates `(new RawBuf n)` with no explicit type-arg — element var solved purely from the enclosing ctor-field type `(con RawBuf a)`, never from a value argument — checks clean but fails `ail build --alloc=rc`: mono drops the check-phase solution for `a`, defaults it to Unit, and codegen mints the unregistered `RawBuf_new__Unit`. The fixture reads the element back via `RawBuf.get` so a wrong specialisation is observable (the program must print the stored `1.0`). This is the precondition the user picked (option B) so Series can ship as a pure AILang library extension over RawBuf while keeping the model-0007 `(new Series (con Float) 3)` caller surface. The #51 fix carried a WRITTEN `(con Int)` type-arg through mono; the variable-via-expected-type case is the untouched gap. RED: `ail check` exits 0; `ail build --alloc=rc` aborts with `RawBuf_new__Unit has no registered intercept`. GREEN target: builds, runs, prints `1.0`. The mono fix must not break the INTERCEPTS↔ (intrinsic) bijection or the Term::New↔pre_desugar_validation lockstep. refs #61 |
||
|
Brummel
|
c747cdf932 |
docs(ledger): fix two coherence gaps surfaced by the project skim
A read-only coherence skim across the project (the contract edits
themselves verified code-true, INDEX bijection exact, all pins green)
surfaced two pre-existing drifts — both predating this audit, neither
from the contract pass. Fixed in the same conservative style.
1. Model 0008 (ownership-totality) §1+§2 narrated the `Implicit`
leak in the PRESENT tense, contradicting the file's own STATUS
header (Implicit deleted via #55,
|
||
|
Brummel
|
4ec8f90b19 |
docs(contracts): finish the honesty pass (0003, 0008, 0013, 0017)
Third tranche, completing the honesty-rule sweep across the remaining
contracts. Same conservative bar: cut unbacked-verification claims,
change/deletion history, and forward-intent; keep present-state design
rationale.
- 0003: drop "sanitiser-verified" — no TSan/sanitiser test exists in
the tree, so the claim asserts a verification that does not happen.
The data-race-freedom property (argued from the non-atomic-but-never-
shared hot path + atomic-relaxed shared counter) stays.
- 0008: the `Type::Con.name` hash paragraph ("the tightening shifted
the hashes ... The new pins ... re-asserts the pre-tightening hashes")
-> present-state: which fixtures carry which hash shape and which test
pins each.
- 0013: drop "the former codegen-side fallback (at ..., and the
now-deleted `synth_with_extras`) is retracted" (deletion history; the
present fact is that codegen does not re-resolve, per the boundary);
"A future refactor that loosens any one of the four breaks ..." ->
present-tense statement that the four are load-bearing and each pinned.
- 0017: drop "a real cost surfaced by the `bench_closure_chain`
regression at the operator-routing-eq-ord milestone" (history) and
"the symmetric extensions are mechanical when the first such workload
appears" (forward-intent); keep the present-state allocation cost, the
pin, and the Int-only-asymmetry rationale.
All 18 contracts now reviewed against the code. Ledger pins green;
honesty sweep clean.
|
||
|
Brummel
|
eaa52ff64f |
docs(contracts): honesty-prose cleanup + ratifier integrity
Second tranche of the contracts-against-code audit. Two threads, both applied conservatively under the over-correction guards in docs_honesty_pin.rs (the self-labelled tiebreaker in 0008 and the Diverge-reserved anchor in 0010 are deliberate honest content and were left untouched; design rationale that explains a present-state design principle — semantic-locality, the reuse-as-wrapper reasons — was also preserved). Honesty-rule (0007): demote clear change/deletion narration to present tense. - 0008: drop "they were promoted from ... to ... Recorded here so"; strip the "Iter A"/"Iter B" iteration labels (the descriptive titles carry the meaning); drop "(no longer a carve-out)". - 0001: "were rewired to use ... was deleted at the same time" -> present tense. (The substance was already correct: `pretty.rs` holds only the diagnostic helpers; an audit agent had misread the line as "pretty.rs was deleted" — the file exists, the printer code does not.) - 0012: drop "Per the tail-call survey of existing fixtures" and "Migration of existing fixtures is partial" -> present-state description of which corpus fixtures carry the tail marker. Ratifier integrity: a contract that names a test which does not ratify it is itself a form of the dishonesty this ledger forbids. - 0014 named `bench/architect_sweeps.sh`, which sweeps honesty-anchors and ratifies none of the six verification mechanisms; and claim 5 cited `tests/expected/`, which never existed (git log empty). Point claim 5 at the real golden mechanism (`crates/ail/tests/snapshots/` via `ir_snapshot.rs`) and the footer at each mechanism's actual test. - 0015's four constraints are guaranteed by absence (no thunk/`ref`/ `IORef` node, non-recursive `let`); the named uniqueness in-source tests only count RC consumes, never the constraints. State the by-construction guarantee and point the ratifier at `ast.rs` (the single source of truth for which nodes exist). - INDEX ratifying-test column updated for both to match. All ledger pins green (docs_honesty_pin, design_index_pin incl. every_contract_names_a_resolvable_ratifying_test, effect_doc_honesty_pin, carve_out_inventory); architect honesty sweep clean. Deferred, recommend-only: 0016-method-dispatch carries no invariant absent from 0013 (merge candidate), but a contract-file merge touches INDEX, the retired-counter convention, and cross-refs — a structural call left for explicit direction. Minor history phrasing in 0008's Type::Con.name hash-shift paragraph (§"FnDef.suppress") also left. |
||
|
Brummel
|
56e076b2ca |
docs(contracts): make 0012 tail-context list code-exhaustive
The §Typecheck enumeration in 0012-tail-calls.md presented the
tail-position rule as exhaustive ("The flag is `false` for: ...") but
omitted `Term::If` entirely — even though `verify_tail_positions`
propagates `is_tail` into both `If` branches (ailang-check/src/lib.rs),
and 0012's own motivating example (`if n == 0 then () else loop(n-1)`)
relies on the `else` branch being a tail position.
Restate the rule by principle (a sub-term is in tail position iff it is
the value of the whole expression) and enumerate the actual checker's
arms: `If` branches, `Match` arms, `Seq` right, `Let`/`LetRec`
in-clause, `Lam` body, and the identity/`Loop` propagators; every
argument position (incl. `If` condition, `Recur`/`New` args) is
non-tail. Matches the present `verify_tail_positions` walker.
|
||
|
Brummel
|
625fe849be |
docs(contracts): reconcile contracts + honesty-pin with shipped reality
First tranche of a contracts-against-code audit (the inverse of the
usual direction: testing the ledger's claims against the code). Each
fix here is a verified factual divergence between a contract and the
code; the direction of the fix follows which side actually drifted.
Code drifted from the stated goal -> fix the code:
- 0014's claim 6 ("`cargo doc --no-deps` runs warning-free") was the
design goal; reality had 6 warnings. Demote the offending intra-doc
links to plain code spans so the docs match the goal:
- ailang-core: `[`load_workspace`]` cannot resolve from core (the
fn lives in ailang-surface, which core may not depend on) — three
sites in workspace.rs.
- ailang-check: three public-item docs linked the `pub(crate)`
helpers `qualify_local_types` / `qualify_workspace_types`.
`cargo doc --no-deps --workspace` is now warning-free.
Contract stale, code legitimately advanced -> fix the contract:
- 0011 stated `float_to_str` "codegen is reserved and not yet
shipped". It is shipped: lowers to `@ailang_float_to_str(double)`,
green under the codegen `float_to_str_no_longer_errors_internal`
unit test and the e2e `float_to_str_smoke`. The docs_honesty_pin
anchor that protected the stale "reserved" wording moved in lockstep
to assert the present-tense lowering instead — the pin had been
guarding a claim the code already falsified.
- 0013 named the diagnostic `ConstraintReferencesUnboundTypeVar`; the
variant is `UnboundConstraintTypeVar` (workspace.rs), and its scope
is a class-method signature whose constraint mentions a tyvar bound
neither by the method's `forall` nor by the class `param`.
- 0017 called the primitive Eq/Ord bodies "placeholder lambdas"; they
carry the `(intrinsic)` marker — the lockstep partner to the
INTERCEPTS registry, not a placeholder.
- 0009 said "seven" `.ail.json` carve-outs and described the inventory
test as pinning seven; the test pins twelve (7 subject-matter + 4
recur + 1 loop-binder, per carve_out_inventory.rs).
Verified separately: 0001's "pretty-printer code in pretty.rs was
deleted, leaving only diagnostic helpers" is factually correct (an
audit agent misread it as "pretty.rs was deleted"); its only issue is
history phrasing, deferred to the honesty-prose tranche.
Deferred to later tranches: honesty-rule prose (history/rationale that
is not a protected honest-reserved/tiebreaker anchor), stale/mislinked
ratifying-tests (0014's `architect_sweeps.sh`, 0015's uniqueness
in-source tests), 0014's never-existent `tests/expected/`, 0012's
non-exhaustive tail-context list, and the 0016<->0013 redundancy.
|
||
|
Brummel
|
69e738d6e6 |
docs(design): close the sma_demo module paren in models/0007 (refs #7)
Verifying the previous commit's surface-syntax fix with `ail parse` (the whitepaper's code blocks are unfenced/untagged, so no spec validation ever parsed them) surfaced a fourth, pre-existing drift the line-by-line signature fix had missed: the §sma_demo `(module …)` was short one closing paren and never balanced — it could not have parsed as written, independent of the mode/con-wrapper drift. Added the missing `)`. With it, both worked-example modules now parse clean: - §sma_demo → `ail parse` ok (4.4 KB JSON) - §series → `ail parse` ok `ail parse` resolves no names, so this verifies surface syntax only, which is the intended scope. The §series listing still leans on kernel-tier polymorphism that `ail check` rejects today; its full compile-verification stays with the pending Series milestone per spec 0059, exactly as the prior commit stated. |
||
|
Brummel
|
5e5b0e1484 |
docs(design): bring models/0007 worked examples onto the shipped surface (refs #7)
The raw-buf milestone fieldtest (spec 0066) surfaced a spec_gap: the kernel-extensions whitepaper teaches RawBuf surface syntax through its §Series worked examples, but those examples were written before three downstream surface decisions landed and never caught up — so an LLM author who pattern-matches them writes programs that fail to parse. Three drift classes, all verified against the HEAD parser: - fn-type slots carried no mode. Post-#55 every value slot needs an explicit `(own …)` / `(borrow …)` (the bare_slot_reject contract). - `(new RawBuf lookback)` omitted the element type. Post-#51 the form is `(new RawBuf (con T) <size>)`; the whitepaper's own spec line (§"allocates") already documents `(new RawBuf (con T) (size: Int))`. - parametrised kernel types were spelled bare `(Series a)` / `(Series (con Float))`, contradicting the whitepaper's OWN prose (`(con Series (con Float))` at the §mechanisms section). Wrapped in `(con …)` to match the documented canonical form. - `len` / `total_count` carried no `(type …)` at all; completed from the obvious neighbour signatures (`borrow (con Series a) → own Int`). Scope is deliberately surface-syntax only. The §Series listing stays a forward-looking sketch of the still-pending library-extension milestone (STATUS header; "not in today's AILang" at the sma_demo block). Its full cross-module compile-verification remains assigned to the Series milestone per spec 0059 — these edits do not claim it compiles today (it leans on kernel-tier polymorphism that is not yet authorable), only that its surface syntax now matches what RawBuf authors must actually write. |
||
|
Brummel
|
9545257333 |
fieldtest: raw-buf milestone — 4 examples, 3 findings (refs #7)
Milestone-close fieldtest for the raw-buf milestone, milestone-scope
variant: four end-to-end scenarios derived top-down from the milestone
promise (construct via (new RawBuf <elem> <size>), fill/read via
set/get, size-only buffers, element variety across {Int,Float,Bool},
forbidden-element reject at check, buffer threading under own/borrow).
Result confirms the milestone-promise hypothesis — RawBuf is clean
end to end, zero bugs:
- mrb_1 Int fill/read loop: check ok, run + native build both print 70
- mrb_2 Float own->own threading + borrow read: prints 3.5
- mrb_3 size-only Bool buffer (#51 legitimate-but-unobserved case): prints 8
- mrb_4 Unit element: rejected at check with a precise
param-not-in-restricted-set diagnostic; build stops at the same
error, codegen never reached (the #51 fix)
Two [working] findings (carry-on) and one [spec_gap]: the
kernel-extensions whitepaper (design/models/0007) teaches bare-mode
fn-type slots that the post-#55 parser rejects. Verified and triaged
separately; the ledger fix follows in its own commit.
|
||
|
Brummel
|
2ca483dbfd |
docs(design): reconcile models 0008/0009 STATUS with the shipped #55 cutover
The 0008 totality core shipped via #55 (spec 0062,
|
||
|
Brummel
|
d8d148224c |
refactor(test): slice the bytes, not the str (sliced_string_as_bytes)
`line[..s].as_bytes()` re-walks UTF-8 boundaries to slice the &str first; `&line.as_bytes()[..s]` slices the byte view directly. `s` is a byte offset from `str::find`, so the two are equivalent here. Clears the last clippy warning in the workspace. |
||
|
Brummel
|
1be2c1f145 |
docs: fix doc_lazy_continuation across the workspace
Eighteen markdown list items in module- and item-doc comments had continuation lines that were not indented to align under the item text, so rustdoc rendered them as separate paragraphs and broke the list. Corrected the indentation (and, at two sites where a general wrap-up sentence followed a sublist, separated it with a blank doc line so it does not mis-attach to the last item). Doc whitespace only; no prose reworded, no code changed. Workspace clippy is now warning-clean. |
||
|
Brummel
|
b5799640f8 |
refactor(core): demote orphaned doc comments in the workspace test module
Two `///` blocks in the in-source test module described tests that were relocated to tests/workspace_pin.rs, leaving doc comments attached to nothing (clippy: empty-lines-after-doc). Converted them to plain `//` notes, matching the already-`//` relocation marker next to them. |
||
|
Brummel
|
5cd2a964e3 |
refactor(surface): collapse the optional-clause duplicate-check onto set_once
Every definition parser repeated the same triplet per optional
attribute — `if slot.is_some() { return duplicate_clause_err(...) }
slot = Some(parse_X()?)`. Factor the check-then-assign into one
helper, set_once(slot, production, subject, clause, value), invoked as
`set_once(&mut doc, prod, subj, "doc", self.parse_doc()?)?`. The match
on peek_head_ident() and the per-clause production/subject/clause
arguments are unchanged, so every duplicate-clause error string stays
byte-identical (the *_rejects_duplicate_*_clause tests pin them).
The helper checks is_some() before the parser runs, so a duplicate
clause still reports at the offending clause's position. Arms that do
more than a plain check+assign (the bool flags drop-iterative/kernel,
the param-in nested map, the suppress/method Vec pushes) are left
inline.
|
||
|
Brummel
|
72503c40fe |
refactor(cli): collapse duplicated handler helpers in main.rs
CLI contract (stdout/stderr/exit codes/JSON field order) unchanged — the e2e diff/manifest/describe cases plus the staticlib/emit-ir/ roundtrip CLI tests are green. - locate_bump_runtime / locate_rc_runtime / locate_str_runtime were three copies of the same upward runtime/<file> walk; folded into locate_runtime_file(filename, err_msg) with each error string passed through verbatim. - describe built the same single-def Module wrapper in both branches; hoisted into wrap_single_def. - manifest built the same per-symbol JSON object in two branches (workspace adds a leading "module" field); hoisted into manifest_def_json(def, Option<module>), field insertion order preserved (serde_json preserve_order). Left duplicated by design: the build_to/build_staticlib elaborate-or- exit blocks (a shared helper would have to name a MIR type from a crate ail does not depend on) and the Diff handler's two-report branches (a generic output router was out of scope and no cleaner). |
||
|
Brummel
|
10da23304e |
refactor(prose): fold the five copies of effects-clause rendering into one helper
The " with <e1>, <e2>" effects clause was rendered by five verbatim blocks across the fn / class-method / instance-method / type writers. Hoisted into write_effects_clause(out, effects); all five sites now call it. Output is byte-identical — the snapshot/round-trip tests confirm no drift. The two forall<...> blocks were left alone: they diverge in the trailing token (one ends `>`, the other `> ` before a where-clause), so a shared helper would be awkward rather than cleaner. |
||
|
Brummel
|
9b0eb58cd9 |
refactor(surface): share the copy-pasted parser sub-productions
Round-trip-preserving — the byte-isomorphic Form-A ↔ JSON-AST tests, the hash pins, and the full fixture-corpus parse are all green; error strings passed through verbatim, not homogenised. - The Int/Float/Str/true/false literal-token match was inlined in three parsers; extracted try_parse_literal_token and routed parse_pat_lit and the parse_term fallthrough through it. - parse_doc and parse_export were identical but for the keyword; both now go through one parse_string_attr, and the previously doc/export-bypassed expect_string helper is back on the shared path. - parse_effects_clause and parse_forall_constraints_clause shared the expect-keyword / collect / reject-empty / expect-rparen shape; unified under parse_repeating_clause, with each clause's empty-error message passed in. parse_intrinsic_attr was left inline-able-but-not-inlined: it has two call sites, so inlining would re-duplicate a documented helper. |
||
|
Brummel
|
e5534d1532 |
refactor: clear clippy code lints across the workspace
Machine-applicable clippy fixes plus three by-hand cleanups; all semantics-preserving (full workspace test suite green). Auto-applied (cargo clippy --fix): - dropped `.clone()` on the Copy type ParamMode (ret_mode/param_mode) - map_or(false, p) -> is_some_and(p) - removed redundant closures and an explicit .into_iter() - useless format!, a needless deref, an as_bytes-after-slice By hand: - ailang-codegen: named the loop-frame tuple types (LoopFrame / LoopBinderSlot) instead of the bare nested Vec<(String, Vec<(String, String, String, Type)>)>, clearing the type-complexity lint and documenting what each slot holds. - ailang-check: collapsed the two identical pass-through arms of the Type-Con qualifier (already-dotted / primitive) into one `||` guard. - ailang-core: converted a stale `///` block (it described a test that was relocated, documenting nothing) back to a plain `//` comment. Remaining clippy output is 16 markdown list-indentation nits in prose doc comments — doc formatting, not code, left for a docs pass. |
||
|
Brummel
|
d5e69148c6 |
refactor(check): unify the two Type-Con qualifiers over an is-local predicate
qualify_local_types and qualify_workspace_types were two ~55-line recursive Type rewriters identical in every arm (Con skip-guards for already-dotted and primitive names; Fn/Var/Forall recursion) except the bare-name decision: the local form rewrites iff the name is in local_types; the workspace form leaves names own to the module bare and otherwise searches module_types for the defining module. Factor the recursion into one rewrite_type_cons that takes the bare- name decision as a `&dyn Fn(&str) -> Option<String>` (Some = rewrite to this qualified name, None = leave bare). The two public functions are now thin wrappers passing their respective closure. Recursion order and Con-arm check order are preserved exactly; cross-module qualification tests green. |
||
|
Brummel
|
7d9ab4d29d |
refactor(codegen): parameterise the copy-pasted IR-emission families
Emitted IR is byte-identical for every case — proven by the IR-pin
suites (eq_primitives_pin, ord_int_intercept_ir_pin, the raw_buf_*
and drop/leak pins) and the full e2e suite, all green.
intercepts.rs:
- The twelve emit_rawbuf_{new,get,set,size}_{int,float,bool} functions
were copy-paste across three element types, differing only in the
element width (8/8/1) and the LLVM load/store type (i64/double/i1).
Collapsed to four parameterised cores; the element variants are thin
call sites passing the (width, type) pair.
- Replaced the repeated, off-by-one-prone parameter-SSA extraction
idiom (`locals[n-2]`, `locals[n-1]`) with an Emitter::last_param_ssas
helper.
- Factored the shared IR-Str bytes GEP out of emit_eq_str /
emit_compare_str into emit_str_bytes_gep.
drop.rs:
- The three emit_*_drop_fn_for_type methods shared one wrapping shape
(monomorphic short-circuit, else loop over instantiations dispatching
to a *_for_instantiation helper); hoisted into emit_drop_fn_wrapper
taking the per-instantiation emitter as a fn pointer.
- emit_flat_intrinsic_drop_fn / _partial_drop_fn differed only in the
symbol prefix and an ignored mask param; merged into one inner
emitter.
No INTERCEPTS-registry or (intrinsic)-marker changes.
|
||
|
Brummel
|
7ae92d3e60 |
refactor(test): hoist duplicated test helpers into ailang-test-support
closes #60 The fixture-corpus filter (NON_PARSEABLE_FIXTURES + list_ail_fixtures) was copy-pasted across three test crates and drifted out of sync as new reject fixtures landed; the examples_dir / workspace_root path walk was reimplemented ~30 more times across the suite, under two spellings (workspace_root / ws_root). Introduce crates/ailang-test-support — a zero-dependency, dev-only leaf crate — as the single home for these helpers: - NON_PARSEABLE_FIXTURES, list_ail_fixtures - workspace_root, examples_dir - canonical_workspace_root (symlink-resolved variant, for the tsan/ race tests that feed the root into native build steps) All integration-test copies across ailang-core, ailang-surface, ailang-prose, ailang-check, and ail now import from the shared crate; the local definitions and their now-orphaned path imports are removed. Path helpers resolve via the support crate's own CARGO_MANIFEST_DIR, so they return the correct absolute paths from any caller. ail_bin helpers are intentionally left in place: they depend on env!("CARGO_BIN_EXE_ail"), which Cargo only defines when compiling the ail crate's own integration tests, so they cannot move to a shared crate. Behaviour-identical: same paths, same fixture lists; full workspace test suite green. Net -177 LOC. |
||
|
Brummel
|
ac9171ebf0 |
refactor: collapse duplicated helpers and drop dead code across check/core/codegen
Pure simplification pass, no behaviour change — hashes, canonical forms, diagnostic codes, and emitted IR are byte-identical (hash-pin and IR-pin tests unchanged and green). ailang-check: - strip_forall and collect_pattern_binders were triplicated verbatim across linearity.rs / reuse_shape.rs / uniqueness.rs; hoisted each to a single pub(crate) fn in lib.rs. - mono.rs::pattern_binders was a fourth copy of collect_pattern_binders (iterative style, same result for every Pattern shape); deleted, now calls the shared fn. - maybe_instantiate and expect_eq were single-call wrappers; inlined at their sole call sites and removed. ailang-core: - collect_used_in_pattern was a verbatim duplicate of pattern_binds; deleted, call site repointed. pattern_binds made private (no external callers; the doc-comment's lift_letrecs claim was stale). - is_false serde helper replaced by std::ops::Not::not at the four skip_serializing_if sites (all plain-bool fields); helper removed. - test-only any_nested_ctor / any_let_rec folded into one generic any_term(t, &pred) walker. - removed dead test helpers tmp_dir / examples_dir, orphaned when their tests relocated to tests/workspace_pin.rs. ailang-codegen: - removed the write-only Emitter::types field, its populating loop, and the now-unused CtorInfo struct it fed. - adt_drop_symbol / adt_partial_drop_symbol differed only in a prefix literal; folded into one adt_symbol(prefix, ...). Symbol strings unchanged. Net -180 LOC. |
||
|
Brummel
|
e25580e3a3 |
test(cutover): live accept/reject corpus for the #55 ownership surface
Wires the #55-cutover fieldtest into a durable regression net. The
fieldtest exercised the post-cutover ParamMode={Own,Borrow} surface as a
downstream LLM author would and produced 12 fixtures + a report; left as
loose files they would be dead fixtures that drift. This commits them as
a protected property.
crates/ail/tests/cut55_cutover_surface.rs — one table-driven test running
each fixture through `ail check` and asserting accept (exit 0) or reject
at the right pipeline stage. Reject rows key on the bracketed diagnostic
CODE (consume-while-borrowed, borrow-over-value, borrow-return-not-permitted,
surface-parse-error), NOT message text, so the test is decoupled from the
diagnostic-wording improvement tracked separately.
examples/fieldtest/cut55_*.ail — the corpus. cut55_2c is the #58 repro
(now correctly rejected). cut55_2b was misanalysed by the fieldtest as a
consume-while-borrowed reject; in fact bump's recursive param is
(borrow List) so the tail is only borrowed, never consumed into an own
slot — `ail check` correctly accepts it. Renamed to
cut55_2b_borrow_traversal_clean and recast as the #58 false-positive
guard (a borrow-position use of a heap sub-binder must stay accepted).
cut55_1b similarly does not fire over-strict-mode (its recursive call
consumes the tail, so the lint's consume_count==0 premise fails) — comment
corrected; it is a plain accept. cut55_1c is the genuine over-strict-mode
example (accepts exit 0, emits the warning).
docs/specs/0065-eliminate-implicit-mode fieldtest report — moved 2c to
the reject set, added the 2b false-positive-guard section, marked the
double-free spec_gap RESOLVED (it shipped as the #58 fix).
Relates to #55.
|
||
|
Brummel
|
19757480b7 |
audit(0064/cutover): record shipped drop machinery + retire dead desugar arm
Cycle-close tidy for the #55 cutover (its audit drift-resolution). Architect drift review found the design ledger out of step with the codegen that the cutover shipped, plus two debt items; regression green (733 passed / 0 failed across the workspace). design/contracts/0008-memory-model.md — the Codegen contract described the drop-emission *gates* but not the drop machinery the cutover landed. Added three subsections recording the present state (honesty rule): - Per-monomorph drop fns for polymorphic ADTs (crates/ailang-codegen/ src/dropmono.rs: collect_drop_monos / DropAdtMeta, the suffix scheme, value-field-skip on the substituted field type). Ratified by alloc_rc_value_type_field_is_not_rc_dec_dropped. - String-literal rep promotion at owned drop sites (StrRep::Static→Heap on a Str literal flowing into an Own slot the callee drops; gated strictly on Own). Ratified by own_str_literal_arg_is_dropped_exactly_once. - Same-constructor arm grouping in match desugar (build_chain / build_ctor_group bind ctor fields once). Ratified by lit_pat_ctor_tail_drop_single_drop + lit_pat_nil_scrutinee_single_drop. crates/ailang-core/src/desugar.rs — build_chain routes every Ctor-head arm (including a length-1 run) through build_ctor_group, so desugar_one_arm's Pattern::Ctor arm was unreachable dead code duplicating the bind-once lowering. Replaced it with unreachable! naming the invariant, and corrected two stale doc comments (the module-header step 4 and the desugar_one_arm doc still described it as handling ctor arms, and mislabeled the Lit lowering as Term::Match — it is Term::If). Full workspace stayed green, confirming the arm was dead. crates/ailang-check/src/linearity.rs — renamed test implicit_fn_is_exempt → own_param_consumed_once_is_clean. Post-0062 there is no Implicit and no exemption; the test pins the ordinary single-Own-consume clean path. Did the desugar + linearity edits inline rather than via an agent: I had already loaded build_chain/build_ctor_group/desugar_one_arm to prove the arm dead, and a sub-agent would have redone the same reading. |
||
|
Brummel
|
b129af1363 |
fix(check): inherit borrow on heap sub-binders of a borrowed scrutinee (#58)
The strict linearity check accepted consuming a heap-typed pattern sub-binder extracted from a `(borrow)`-mode match scrutinee. The sub-binder aliases the caller-owned interior, so moving it into an `(own)` slot double-frees at runtime (SIGSEGV) — `ail check` returned exit 0, `ail build`+run crashed. A pre-existing hole the corpus never exercised; the #55 cutover's universal activation of the strict check exposed it (sibling to the #57 / spec 0064 class-2 let-alias-of-borrow hardening — this is the pattern-sub-binder analog). Root: `walk_arm` seeded every pattern sub-binder with `borrow_count = 0` (freely consumable), bypassing the `Borrow`-param seeding in `check_fn` that starts a borrowed param at `borrow_count = 1`. The whole-param consume was caught (cut55_2d, correctly rejected); the moved-out heap sub-binder was not. Fix: in `Term::Match`, resolve the scrutinee through `resolve_alias` and record whether it is a borrowed binder; thread that into `walk_arm`, which now seeds a heap-typed (`!is_value`) sub-binder of a borrowed scrutinee with `borrow_count = 1`. Value-typed sub-binders (e.g. the `Int` head) stay at `0` — copied out, no heap alias. Nested matches fall out for free: the inner match re-derives borrowed status from the borrow-carrying sub-binder. Rejected alternative: forcing fieldtest fixture cut55_2b to also reject. 2b is a clean borrow-traversal — `bump`'s recursive param is `(borrow)`, so the tail `t` is only borrowed, never consumed into an `(own)` slot. Distorting the fix to reject it would be unsound (false positive on legitimate borrow-rebuild). The fixture's own comment misdescribed its recursive param as `(own)`; the code says `(borrow)`. Verification: - RED test linearity::tests::consume_heap_sub_binder_of_borrow_scrutinee_is_rejected: was left:0 right:1 (check returned []), now green. - Full workspace: 732 passed / 0 failed (was 731; +1 the new test). No committed corpus newly rejected by the sharper check. - fieldtest repro cut55_2c: exit 0 (wrongly accepted) -> exit 1 (consume-while-borrowed on `t`). closes #58 |
||
|
Brummel
|
76b21c00eb |
feat(lang): eliminate the Implicit ownership default — totality + the drop-soundness it demasks (#55)
Deletes `ParamMode::Implicit`. `ParamMode` is now `{Own, Borrow}`:
every fn-type slot on every signature carries an explicit `own` or
`borrow`, no defaulted position survives anywhere (model 0008 §2,
spec 0062). The parser rejects a bare fn-type slot; `borrow-return`
and `borrow-over-value` reject at the signature; the corpus is
migrated to minimal-ownership modes (consumed ⇒ own, read-only-heap
⇒ borrow, value ⇒ trivial-own). The documented `Implicit`-ret-mode
leak is fixed: an owned heap return now drops exactly once (live=0,
acceptance criterion 5).
This was the easy half. Removing the default ACTIVATED a family of
drop paths that `Implicit` had silently skipped — the pre-cutover
language was leaking (and in places mis-dropping) here rather than
crashing, because an Implicit scrutinee turned the drop off. Making
the modes explicit (Own) turned those paths on and exposed two
latent-bug clusters, all fixed RED-first as part of this cutover:
Drop-soundness family (four legs):
A. lit-sub-pattern double-free — the desugar re-matched the same
owned scrutinee in the lit fall-through; fixed by grouping
consecutive same-ctor arms into one match (bind fields once),
in ailang-core desugar.
B. Cons-husk leak on non-tail arm bodies — the lit-sub-pattern
desugar rebound the owned scrutinee via `Let $mp = xs`, which
bumped consume_count and suppressed the existing fn-return
partial_drop. Fixed by not rebinding a bare-Var scrutinee
(one husk-freeing mechanism, not two).
C. polymorphic `drop_<T>` rc_dec'd monomorphised value fields —
the per-ADT drop fn was emitted once from the polymorphic
TypeDef, defaulting type-var fields to ptr and rc_dec'ing
inline Ints (segfault). Fixed with per-monomorph drop
functions (new ailang-codegen::dropmono): the drop set is
collected from the lowered MIR, value-type fields are skipped,
heap fields still freed once; monomorphic-concrete ADTs keep
their byte-identical un-suffixed drop symbol.
D. static Str literal passed to an `(own Str)` param — the
literal lowers to a header-less rodata constant; the callee's
now-active rc_dec read its length field as a refcount and
freed a static address (segfault). Fixed with the missing
fourth StrRep::Static→Heap promotion in lower_to_mir's App arm,
gated on Own mode (borrow args stay static, no regression).
over-strict-mode lint over-fired: it suggested `(borrow V)` for
value-typed params (which `borrow-over-value` rejects — own is the
only legal mode there) and fired on `(intrinsic)` bodies (whose
consumption the linearity walk cannot observe). Tightened to skip
both; contract 0008 updated to the narrowed firing scope.
Irreversible step — canonical-form hash reset (model 0008 §6,
acceptance criterion 6). Every signature now carries explicit modes,
so the hashable canonical JSON changed for every module. RATIFY:
the corpus-wide hash-pin reset (hash_pin, prelude_module_hash_pin,
mono_hash_stability, eq_ord_e2e, embed_export_hash_stable, the
ct4/iter*/loop_recur schema-extension pins) and the list ir_snapshot
golden were regenerated once, deliberately, as the intended one-time
consequence of removing the mode elision from the canonical form —
not a regression. Each regenerated hash verified deterministic across
two runs.
Also fixes a pre-existing latent failure surfaced by the verification
gate, unrelated to this cutover: the `every_contract_names_a_resolvable_
ratifying_test` resolver (design_index_pin) could not resolve the
" + " dual-link ratifying-test form (`uniqueness.rs + linearity.rs`)
that the #57 audit-close (
|
||
|
Brummel
|
05c3c018de |
fix(check): branch Float NoInstance addendum on method name (#25)
The Float-aware `NoInstance` addendum emitted the same hint for every Eq/Ord method at Float: "use float_eq / float_lt (and siblings ...)". For `eq`/`ne`/`lt`/`le`/`gt`/`ge` that is correct — each has a drop-in boolean `float_*` sibling. For `compare` it is incomplete and misleading: `compare` returns three-way `Ordering`, but no `float_compare` ships (a deliberate non-ship, docs/specs/2026-05-20-operator-routing-eq-ord.md). An LLM author who reached for `compare` to get three-way ordering was pointed at boolean siblings as if a drop-in existed, and left guessing whether to reconstruct it themselves. Fix: branch the addendum on the called method. The boolean arm keeps the existing wording; the `compare` arm instead names the deliberate `float_compare` omission and points at building a three-way `Ordering` from `float_lt` + `float_eq`. One added branch on the existing `method` field (already carried by `CheckError::NoInstance`), no new machinery; the structured `ctx` is untouched. Out of scope (the issue's deliberate non-ship): shipping a `float_compare` fn. The friction was that the diagnostic did not acknowledge the omission — now it does. RED-first, inline: a one-branch diagnostic-text change at a single site whose surrounding code was already loaded while working the adjacent #52 fix this session (CLAUDE.md "context already loaded" carve-out). TDD discipline preserved by the new RED test `compare_at_float_names_deliberate_no_float_compare` over a new minimal fixture `examples/compare_float_noinstance.ail` (`compare` at Float); it failed RED on the old shared wording and passes GREEN on the branch. The pre-existing `eq_at_float_fires_float_aware_noinstance` still passes (eq arm unchanged). Verification: full ailang-check lib suite (121) + full ail test suite green; live CLI renders both arms correctly. closes #25 |
||
|
Brummel
|
d8be95dd44 |
fix(check): render restricted-set diagnostic in AILang set syntax (#52)
The `param-not-in-restricted-set` diagnostic rendered its allowed
element set with `{allowed:?}` — a Rust `{:?}` debug print of the
`Vec<String>`, producing `["Bool", "Float", "Int"]` with quotes,
brackets, and Rust list shape. AILang's audience is an LLM author, so a
language-level diagnostic leaking Rust formatting into its surface is a
quality defect.
Fix: render the set as `{Bool, Float, Int}` via a thiserror trailing-arg
`.allowed.join(", ")` wrapped in literal braces. The set is alphabetical
and stable (unchanged — the source is a sorted BTreeSet projection).
Design decision (set notation, not a union): the allowed set is a
membership set ("one of"), and AILang has no union-type surface syntax,
so brace set-notation `{A, B, C}` reads naturally without implying a
type-level union the language does not have. The structured JSON detail
(CheckError::detail, the `allowed` array) is left untouched — it is
machine-readable and correctly an array, not the cosmetic surface.
RED-first, inline: the bug is a one-line Display-string change at a
single site (lib.rs ~760). The exact lines were already loaded while
assessing the /boss queue, so a debugger subagent would only redo the
same reading (CLAUDE.md "When NOT to delegate: context already loaded").
TDD discipline is preserved by the new RED test
`param_in_reject_message_renders_allowed_set_in_ailang_syntax`, which
asserts the AILang set form and the absence of Rust quotes/brackets;
it failed RED on the old `{allowed:?}` and passes GREEN on the fix. The
pre-existing pin `param_in_reject_message_names_allowed_set` only
asserted substring presence, so it did not pin (or block) the format.
Verification: full ailang-check suite green (121 lib tests + integration
suites); live CLI repro from the issue now renders
`(allowed: one of {Bool, Float, Int})`.
closes #52
|
||
|
Brummel
|
9848d4b2df |
docs(design): explore explicit RC as opt-in, not the floor (model 0009)
Records the runtime-axis dual of ownership totality (model 0008). 0008 totalises the *annotation* (own/borrow everywhere, no Implicit) but keeps universal RC as the floor; 0009 asks the question totality makes askable — must the runtime discipline stay universal, or can it follow the type? Principle: RC is authored, never universal. Default `box` (affine, refcount-free, deterministic scope-drop ≈ Box); opt-in `rc` (refcounted, explicit `share` ≈ Rc). Motivated by the maintenance record: ~1/3 of recent commits touch RC/ownership/drop, no bug was ever in the RC runtime itself — all lived in the inference (uniqueness-elision, is_rc_heap_allocated, mode-through-subst) that exists only to reconcile affine ownership with universal RC and strip the RC it over-charges. Soundness leans on existing law: the 0015 DAG constraints + linear-by- default already draw the "needs-a-count" partition; `rc` only names it. No cycle collector reappears (rc graphs stay acyclic). No `&mut` mode: in-place mutation rides consume-and-return (move, not alias), so constraint 3 (immutable-once-constructed) holds — `mut` is out by principle. §5 enumerates what leaves the compiler (uniqueness-elision, is_rc_heap_allocated term-shape predicate, over-strict lint, reuse-as, escape-clawback) and what stays (the affine/linearity check, already present). Status-stamped NOT current state, per the honesty rule and the 0008 precedent; INDEX.md left untouched (exploration whitepapers are not on the canonical spine until adopted). Composes with 0008 regime A, which already makes transitive box-drop sound. §8 isolates the open questions (closure capture move/share, clone-vs-share split, coupling to 0008's escape pass, keyword spelling, sharing-heavy workloads). |
||
|
Brummel
|
dfdc65f21f |
audit: spec 0064 cycle close — drift-clean after two ledger fixes (#57)
Cycle-close audit for spec 0064 (the #57 hardening of the linearity analysis, the #55-cutover precondition; four iterations |
||
|
Brummel
|
2769e50a35 |
fix(examples): destructure partition_eithers result once (#57, 0064 iter 4)
Final iteration of spec 0064 (the #55-cutover hardening, #57). Closes class 4, the one genuine corpus bug among the four (not a false positive): std_either_list.partition_eithers projected both (app Pair.fst rest) and (app Pair.snd rest) from one owned `rest`. Pair.fst/snd are own-param projections that move a field out, so each consumes `rest` -> a genuine double-consume that universal linearity activation (#55) would correctly reject. The fix is a body rewrite (destructure `rest` once via (match rest (case (pat-ctor MkPair ls rs) …)) then dispatch on the head), NOT a check change -- the check is right. Latent until activation: partition_eithers' param is a bare (Implicit) slot today, so the check is skipped on it -- no RED->GREEN flip on the real fixture. The rewrite is a pre-emptive corpus fix. Its correctness rests on the unchanged 2 3 2 3 E2E output (std_either_list_demo, a semantically-identical partition) and on the new c4_double_consume must-stay-RED fixture, which -- with explicit modes, so the check is active today -- demonstrates the double-projection shape IS rejected. - examples/std_either_list.ail: partition_eithers Cons arm rewritten; doc updated (destructure-once, no longer "projections"). - examples/c4_double_consume.ail: must-stay-RED pin (the rejected shape), folded into a generalised harden_ownership_heap_double_consume_still_errors loop over {real_consume, c4_double_consume}. - examples/c4_rewrite.ail: stays-clean pin (the accepted destructure-once shape), added to harden_ownership_false_positives_are_clean. No hash-pin on std_either_list (verified); the e2e 2 3 2 3 output pin is the content pin and is preserved. No check/schema/codegen change. Verified: std_either_list checks clean; demo 2 3 2 3; both harden assertions green; cargo test --workspace green; bench/check.py 34/34, compile_check.py 24/24 stable. This is the last of the four #57 hardening classes. Spec 0064 is now code-complete: classes 1 (local fn-param modes), 2 (let-alias redirect), 3 (value-typed let-binder), and 4 (this) all shipped. The cycle is ready for audit; the #55 cutover precondition is met. refs #57 |
||
|
Brummel
|
dea93a99fc |
plan: 0064 iter 4 (final) — partition_eithers double-consume rewrite (class 4) (#57)
Final iteration of spec 0064. Closes class 4, the one genuine corpus bug (not a false positive): partition_eithers projects both (app Pair.fst rest) and (app Pair.snd rest) from one owned rest; fst/snd are own-param projections that move a field out, so rest is consumed twice. Universal linearity activation (#55) would reject it. Fix is a body rewrite (destructure rest once via match), not a check change. Latent-bug nature: partition_eithers has a bare (Implicit) param slot today, so the check is skipped on it -- no RED->GREEN flip on the real fixture. The rewrite's correctness is proven by the unchanged 2 3 2 3 E2E output (std_either_list_demo) and by the explicit-mode c4_double_consume must-stay-RED fixture (the double-projection shape IS rejected, verifiable today). Orchestrator verified the rewrite this session: ail check std_either_list -> exit 0; ail run the demo -> 2 3 2 3 (applied, ran, reverted for the implementer to re-apply). Two tasks: Task 1 rewrites partition_eithers + gates on the unchanged E2E output; Task 2 adds c4_double_consume (must-stay-RED, folded into a generalised harden_ownership_heap_double_consume_still_errors loop) and c4_rewrite (stays-clean, added to the false-positives-clean array). plan-recon confirmed no hash-pin on std_either_list (only the e2e 2 3 2 3 output pin, preserved). No check/schema/codegen change. This is the last of the four #57 hardening classes; after it lands, spec 0064 is code-complete and the cycle is ready for audit. refs #57 |
||
|
Brummel
|
be259f9d46 |
feat(check): let-alias borrow propagation via alias-redirect (#57, 0064 iter 3)
Third iteration of spec 0064 (the #55-cutover hardening, #57). Closes false-positive class 2: Term::Let walked its value in Position::Consume, so (let a t (match a …)) over a borrow-mode t consumed t at the binding and tripped consume-while-borrowed -- a let-alias of a borrowed value read in a borrow position is not a consume. Fix: the Checker gains a scoped aliases: HashMap<String,String>. A (let a t body) whose value is a bare Var resolving to a tracked binder records a -> root(t) for the body scope and skips the consume walk of the value. A new resolve_alias helper maps a name to its root, preferring a real binder at each chain step -- so an inner binder named `a` (nested let, pattern binder, lam param) automatically shadows the alias with NO change to with_binder/walk_arm/Lam (the shadowing is resolved centrally in the resolver, not at three scattered introduction sites). Every binder-state lookup keyed by name resolves through the map first: use_var, the App borrow bump + decrement (pushing the resolved root to `lent` so the decrement matches), callee_arg_modes, and the reuse-as source. Design calls (orchestrator): - Alias REDIRECT, not state clone (spec scope decision 3): consuming the alias marks the single root consumed, so a real double-consume through an alias is still caught. A clone would track two independent binders and miss it (unsound). Pinned by the new let_alias_of_owned_double_consume_still_errors unit test: (let a p0 (seq a p0)) over an own heap p0 still fires use-after-consume. - resolve_alias prefers binders -> shadowing needs no edits to the binder-introduction sites. Lower-risk than clearing aliases at each. - reuse-as source (linearity.rs:663) is resolved through aliases too: it is the 4th binder-state-reading site; the spec's Fix 3 named three illustratively. Without it, (reuse-as <alias> …) would mis-fire reuse-as-source-not-bare-var on what IS a Var. Faithful completion of Fix 3. The diagnostic now reports the resolved root name (the actual consumed resource), not the surface alias. Closes the design/contracts/0008-memory-model.md let-alias carve-out (was "has not shipped yet") and extends its Ratified-by trailer to name linearity.rs, where the propagation now lives -- a contract change riding with the feature that forces it. RED-first: examples/c2_let_alias.ail added to harden_ownership_false_positives_are_clean (RED: consume-while-borrowed on count's t); GREEN after. Verified: c2 RED->GREEN; 120 linearity unit tests green; the soundness test fires; harden false-positive + heap double-consume guards green; cargo test --workspace green; bench/check.py 34/34, compile_check.py 24/24 stable. Diagnostic-only; no schema/type/codegen change. Class 4 (partition_eithers body rewrite) remains for the final iteration of spec 0064. refs #57 |
||
|
Brummel
|
9c4d195806 |
plan: 0064 iter 3 — let-alias borrow propagation (class 2) (#57)
Third iteration of spec 0064. Closes false-positive class 2: Term::Let walks its value in Position::Consume, so (let a t (match a …)) over a borrow-mode t consumes t at the binding -> false consume-while-borrowed. Fix: 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. 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 handled 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, 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 miss it (unsound). Pinned by the let_alias_of_owned_double_consume_still_errors unit test. - resolve_alias prefers binders -> shadowing needs no edits to the three binder-introduction sites (simpler, lower-risk than clearing aliases at each). - reuse-as source (linearity.rs:663) is the 4th binder-state-reading site; the spec's Fix 3 named three illustratively. Resolving there too avoids a spurious reuse-as-source-not-bare-var on an aliased Var. Faithful completion of Fix 3, documented as such. Three tasks, RED-first: Task 1 adds examples/c2_let_alias.ail to the harden list (RED: consume-while-borrowed on count's t); Task 2 is the alias mechanism (GREEN) + the soundness unit test; Task 3 closes the design/contracts/0008-memory-model.md:340 let-alias carve-out (was "has not shipped yet") and extends the Ratified-by trailer to name linearity.rs. Diagnostic-only; no schema/type change. plan-recon mapped current post-iter-2 line numbers; parse gate fired on the inlined fixture (RED confirmed). Class 4 (partition_eithers rewrite) remains for the final iteration. refs #57 |
||
|
Brummel
|
cc5991eeb3 |
feat(check): resolve local function-typed binder modes (#57, 0064 iter 2)
Second iteration of spec 0064 (the #55-cutover hardening, #57). Closes false-positive class 1: applying a local function-typed binder -- a HOF predicate param like std_list.filter's `p` -- treated its arguments as Consume because callee_arg_modes resolved only the global symbol table (locals returned an empty mode vec). So `(app p h)` with `p` a local (borrow ...) predicate consumed the heap element `h`, and reusing `h` in the kept Cons false-fired use-after-consume. Fix: BinderState gains fn_param_modes: Option<Vec<ParamMode>>, seeded at all three function-typed binder introduction sites via a new fn_modes_of helper (strip_forall + Type::Fn { param_modes }, None for non-fn / empty-modes so the caller falls through to globals): params and lam-params from their signature type (param_tys), let-binders from the LetBinderTypes table built in iter 1. callee_arg_modes reads a local Var callee's fn_param_modes before the global lookup (a local binder shadows a global -- correct lexical scope); the existing App arg-walk maps a Borrow mode to a borrow walk unchanged, so the fix is confined to the seeding + the one local-precedence read. Scope call (orchestrator): all three seeding sites, not just the param path that unblocks filter -- the point of this hardening cycle is to leave no latent class (the #57-from-0063-deferral lesson), and the extraction is uniform with the table already built. RED-first: examples/c1_local_hof.ail added to harden_ownership_false_positives_are_clean (RED: use-after-consume on filter_box's h) before the fix; GREEN after. Two in-source unit tests pin both seeding paths (param via signature, let via a hand-built table). Verified: c1 RED->GREEN; 119 linearity unit tests green; harden_ownership_false_positives_are_clean green (now c1 + c3); the heap-double-consume must-stay-RED guard still fires; cargo test --workspace green; bench/check.py 34/34, compile_check.py 24/24 stable. Diagnostic-only; no schema/type/codegen change. The stale `// Locals never carry fn-types in 18c.2` comment in callee_arg_modes (and the fn's doc header) is rewritten to the accurate local-precedence behaviour -- it sat in the replaced lines and directly contradicted the new path. Classes 2 (let-alias redirect) and 4 (partition_eithers rewrite) remain for later iterations of spec 0064. refs #57 |
||
|
Brummel
|
2ad58ada17 |
plan: 0064 iter 2 — local function-typed binder modes (class 1) (#57)
Second iteration of spec 0064. Closes false-positive class 1: applying
a local function-typed binder (a HOF predicate param like
std_list.filter's `p`) treats its args as Consume because
callee_arg_modes resolves only globals -- so a heap arg reused after
(app p h) false-fires use-after-consume.
Fix: BinderState gains fn_param_modes: Option<Vec<ParamMode>>, seeded
at all three function-typed binder introduction sites -- params and
lam-params from the signature (param_tys), let-binders from the
LetBinderTypes table built in iter 1 -- via a new fn_modes_of helper
(strip_forall + Type::Fn { param_modes }). callee_arg_modes reads a
local Var callee's fn_param_modes before falling back to globals; the
existing App arg-walk maps Borrow to a borrow walk unchanged.
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 the same at each site with the table already built.
Two tasks, RED-first: Task 1 adds examples/c1_local_hof.ail to the
harden list (RED: use-after-consume on filter_box's h); Task 2 adds the
field + seeding + callee_arg_modes read (GREEN), plus two in-source
unit tests (param path via signature, let path via hand-built table)
and a borrow-predicate test helper. Diagnostic-only; no schema/type
change. plan-recon mapped current post-iter-1 line numbers; parse gate
fired on the inlined fixture (RED confirmed).
refs #57
|
||
|
Brummel
|
47964abf7c |
feat(check): tee let-binder types, exempt value-typed let-binders (#57, 0064 iter 1)
First iteration of spec 0064 (the #55-cutover hardening, #57). Closes
false-positive class 3: a value-typed `let`-binder (e.g. a `Float`
result bound and read more than once) tripped `use-after-consume`
because the linearity walk installed every `let`-binder as a default
heap-tracked BinderState. Spec 0063 deferred exactly this class
("value-typed let-binders ... deferred until a corpus shape demands
it"); eqord_3_newton_sqrt.iterate's `(let xnew (app / …) …)` is that
shape.
Mechanism (the design call, user-delegated): the let-binder's type is
ALREADY computed at synth's Let arm and discarded. Stop discarding it.
synth gains a (def,binder)->Type out-param (LetBinderTypes, defined in
linearity.rs); the Let arm records `subst.apply(&v)`. The table is
allocated per-module in check_workspace, threaded through
check_in_workspace -> check_def -> check_fn/check_const/check_instance
-> synth, and passed (immutable) into check_module_with_visible ->
Checker. linearity's Term::Let seeds BinderState.is_value from the
table via the existing type_is_value predicate -- the same per-binder
flag #56 seeds at param/pattern/lam sites, now extended to the let
site. No schema change, no hash shift, no codegen change; the check
stays diagnostic-only.
Not a re-run of inference in the walk (ruled out by
|
||
|
Brummel
|
ba981689fc |
plan: 0064 iter 1 — let-binder type table + value-typed let exemption (#57)
First iteration of spec 0064 (#57 hardening). Tees the (def,binder)->Type table out of the typecheck pass (the inferred let-binder type computed at synth's Let arm and discarded today) and threads it into the linearity walk, then seeds BinderState.is_value for value-typed let-binders from the table -- closing false-positive class 3 (the class spec 0063 deferred). Two tasks, RED-first: Task 1 adds examples/c3_value_let.ail to the harden_ownership_false_positives_are_clean list (RED: use-after-consume on xnew); Task 2 threads the table end-to-end (synth -> check_fn -> check_in_workspace -> check_workspace -> check_module_with_visible -> Checker, all callers in one compile-atomic task) and seeds is_value at Term::Let (GREEN), plus two in-source unit tests (value-let clean, heap-let still errors). Fixes 1/2/4 (local fn-param modes, alias-redirect, partition_eithers rewrite) are later iterations of the same spec, explicitly out of scope here. plan-recon mapped the threading path; the parse-the-bytes gate fired on the inlined fixture (RED confirmed). refs #57 |
||
|
Brummel
|
f6a8607518 |
spec: 0064 harden ownership analysis part 2 (#57)
The #55 cutover (plan 0121, Task 4) is blocked: deleting
ParamMode::Implicit activates the strict linearity check universally,
but the migrated corpus does not pass cleanly. #56 (spec 0063) closed
two false-positive classes; universal activation surfaces three more
plus one genuine corpus over-consume. This spec is the "#56 part 2"
hardening, sibling to 0063, landing before the irreversible variant
deletion. It does NOT patch a fifth phase onto plan 0121 (project
rule: 2+ blocking classes = spec defect).
Four additive fixes, no schema/hash/codegen change, check stays
diagnostic-only:
- Type table teed from the typecheck pass (synth Let arm at lib.rs:3808
computes the binder type then discards it) into (def,binder)->Type,
threaded to linearity. The "stop discarding known information" fix,
not a re-run of inference in the walk (ruled out by
|
||
|
Brummel
|
39b674c1ec |
chore: throwaway mode-migration tool for the Implicit cutover (#55, 0121 task 3)
Adds `ail migrate-modes <file>` (a throwaway CLI subcommand) and the AST walker `ailang_core::ast::for_each_fn_type_mut` it drives: parse a .ail, map every bare/Implicit fn-type slot to Own, preserve explicit Own/Borrow, print back. Semantically invisible today (PartialEq treats Implicit == Own), but it materialises the modes so the post-cutover parser — which will reject bare slots — accepts the migrated corpus. Both are throwaway: removed in task 4 once ParamMode::Implicit is deleted (the closure references Implicit and would not compile). RED-first: migrate_modes.rs failed to compile (missing walker) before for_each_fn_type_mut was added. Additive; full workspace suite green. refs #55 |
||
|
Brummel
|
e1c908912b |
feat(check): reject borrow-returns at the signature (#55, 0121 task 1)
`(ret (borrow T))` is now a check error (CheckError::BorrowReturnNotPermitted, code `borrow-return-not-permitted`), fired on the fn signature before body dataflow. Borrow-returns are refcount-invisible and can outlive their source; re-enabling them needs the escape/liveness axis, which is out of scope (spec 0062). The diagnostic names that gap as an honest "not yet". The check_fn signature destructure now also binds `ret_mode` (param_modes stays under `..`; the borrow-over-value reject that reads it is folded into the cutover, task 4). RED-first: examples/borrow_return_reject.ail checked clean (exit 0) before the reject landed, exits 1 after. New CLI-boundary E2E pin crates/ail/tests/mode_signature_rejects.rs, modelled on raw_buf_new_type_arg_pin.rs. Additive — ParamMode::Implicit still present; full workspace suite green, bench/check.py 0 regressed. refs #55 |
||
|
Brummel
|
7dc21234f0 |
plan: re-stage 0121 — fold borrow-over-value into the cutover (mono collision)
First implementation contact surfaced a plan defect: the
borrow-over-value reject cannot land green as a standalone pre-cutover
task. The prelude's polymorphic comparison builtins are
`(params (borrow a) …)` (eq/compare/lt/…); the mono pass
(apply_subst_to_type, subst.rs:165) specialises `a := Int/Bool/Float`
into `compare__Int(borrow Int, …)` — the language's OWN generated code
in the forbidden `(borrow value-type)` shape. The standalone check
broke compare_{int,bool}_mono_symbol_emits_branch_ladder.
Spec 0062's "value types always own" rule is universal, so generated
code must honour it too: the principled fix is a mono-pass coercion
`(borrow value-type) -> (own value-type)` (a no-op — value types carry
no RC, so own vs borrow emits no inc/dec and the branch-ladder IR is
unchanged). The check and the coercion are a matched pair and now live
together in Task 4 (Steps B1-B2), which touches the mono path anyway.
Pre-cutover green tasks are now Task 1 (borrow-return reject) + Task 3
(throwaway migration tool). Task 1's check_def destructure binds only
ret_mode (param_modes stays under `..`); Task 4 Step B2 widens it.
Spec gap to record at the next 0062 brainstorm touch: the
borrow-over-value rule needs its mono-coercion clause spelled out — the
spec tested only the authored case.
refs #55
|
||
|
Brummel
|
a84ba596cf |
plan: eliminate the Implicit ownership default (0121)
Executable projection of spec 0062 (#55) into four tasks: (1) the borrow-return reject, (2) the borrow-over-value reject, (3) a throwaway `ail migrate-modes` pass (parse -> Implicit->Own, keep explicit own/borrow -> print explicit), (4) the atomic cutover (run the migration over the corpus + hand-fix the read-only-heap params the now-universal linearity check flags, delete the variant + all compile sites compiler-driven, parser bare-slot reject, reset the hash pins, flip the leak pin, update both contracts, drop the throwaway). Placeholder-free; all seven surface fixtures parse-gated against HEAD. Spec 0062 marked approved (user, 2026-06-01) and its soundness re-validated against post-#56 HEAD: the three own-return-provenance / regime-A fixtures still exit 1 under [consume-while-borrowed]; #56's application-is-a-borrow change does not weaken them (none is an application of a borrowed binder). plan-recon folded four spec-enumeration corrections into the plan: - kernel migration target is raw_buf/source.ail, not the retired kernel_stub/source.ail the spec cited; - FIVE hash pins shift, not the two the spec named (embed_export_hash, eq_ord_e2e, mono_hash_stability are the missed twins); - design/contracts/0002-data-model.md also documents the "implicit" JSON form and is drift-anchored -> updates alongside 0008; - real counts are 261 fn-type fixtures (spec ~208) and 17 fn_implicit references (spec 16); the compiler is the authoritative enumerator. refs #55 |
||
|
Brummel
|
aaa70d4c35 |
feat(check): harden the ownership analysis for universal activation (0063)
The strict linearity check (use-after-consume / consume-while-borrowed, linearity.rs) runs today only on the ~45 of 258 all-explicit-mode fns; its activation gate skips any fn with a bare/Implicit param. Deleting ParamMode::Implicit (#55) would turn it on universally and surface ~21% false positives in two classes. This closes both, making the core ownership analysis sharp across the whole codebase for the first time — the precondition for #55. Diagnostic-only: no schema, no hash, no codegen change; the two existing diagnostic codes simply fire on a smaller, more correct set. Fix 1 — value-type exemption. A new is_value_type predicate (ailang-core::primitives) names the unboxed set {Int,Bool,Float,Unit}; BinderState gains an is_value flag seeded from the binder's locally available type (param signatures, ctor field types for pattern binders, lam typed-params), and use_var short-circuits the Consume arm for it. A value type has no refcount and is never consumed, so multi-read is always legal. Str is deliberately NOT in the value set, though is_primitive_name includes it: drop.rs:490-492 lowers only Int/Bool/Float/Unit to non-ptr; Str is a ptr, RC-dec'd, so a multi-consume of Str without clone is a real use-after-free. is_value_type is the Str-excluding subset of is_primitive_name, pinned by a unit test. is_heap_type and the over-strict-mode lint are left untouched (separate concern). Fix 2 — application is a borrow. Term::App walks its callee in Position::Borrow (was Consume). Applying a function value reads it; it stays live for further applications. Global fn-refs are untracked (no-op); a tracked function-typed binder (a HOF param) is no longer consumed by application. This fixes both the own-f-param use-after-consume and the borrow-f-param consume-while-borrowed in the recursion-passing HOF shape (map_int f t). Passing a function value as an arg is unchanged — it follows the callee param_modes. Scope decision: value-typed let-binders stay conservatively tracked as heap (their type is inferred, not annotated, and the linearity walk does not re-run inference). This is soundness-safe — over-strict, never unsound — and not a measured corpus shape; lifting it would need a full binder->type table out of the type-checker. Verification: all three false-positive classes reproduced today against explicit-mode fns and shipped as RED->GREEN fixtures (examples/fp_{value,hof,map}.ail); examples/real_consume.ail stays RED (heap double-consume still fires) to prove the exemption is type-gated. 715 workspace tests green; bench/check.py 0/34 and bench/compile_check.py 0/24 regressed. merge_states carries is_value so the flag survives branch merges. RED-first verified per task. closes #56 |