8d58c8310be874bd39179ceb3f61450139356964
999 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
 Brummel
|
8d58c8310b |
test(cli): RED pin for type-scoped describe resolution
`ail describe <Type>.<op>` is the canonical form (model 0007 §1) but currently errors `no module \`Series\` in workspace` because resolve_describe_name (crates/ail/src/main.rs) only looks up the left segment as a MODULE, never as a known TYPE. The module-scoped `series.push` and bare `push` forms already resolve fine. RED pin: describe_resolves_type_scoped_op asserts `ail describe --workspace examples/series_sma.ail Series.push` exits 0 and prints the `series.push` def. Fails today on the exit-0 assertion (feature absent), not on scaffolding. GREEN side follows. refs #64 |
||
|
Brummel
|
a35878154b |
docs(examples): correct rbx_1 ctor-field qualification note
The field-test note on the `Window` ctor claimed that bare
`(con RawBuf (con Float))` in a user ADT ctor field gives a
type-mismatch and that "the only form that checks is the
fully-qualified `raw_buf.RawBuf`". Verified against the current
tool (release at HEAD), that claim is false in every form I could
construct:
- bare `(con RawBuf a)` (type-variable element) in a non-kernel
module: checks ok
- bare `(con RawBuf (con Float))` (concrete element): checks ok
- a `(new RawBuf ...)` value stored via `term-ctor` into a
bare-declared field: checks ok
- the full rbx_1 program with the field switched to bare RawBuf:
checks ok
A ctor field is plain type position, and model 0007 §3
("kernel-module types are accessible bare in type position") already
covers it — the auto-import that makes bare `Series` work at a call
site equally makes bare `RawBuf` resolve in a user ctor field. The
only genuine constraint is that a ctor field carries no mode:
`(own (RawBuf a))` is a surface-parse-error, which model 0007 line
458 already documents.
So there is no qualification asymmetry to add to the ledger; the
ledger is correct as-is. The drift was in this checked-in comment
(a guessed rule recorded as fact), now rewritten to the verified
reality. The qualified spelling is kept in the code as the explicit
form. No ledger change.
closes #65
|
||
|
Brummel
|
a2808a6938 |
test(codegen): ignored RED pin for match-arm consume-split leak (#63 leg 3)
The third and final identified leg of #63: an owned heap param consumed on one match arm but live on a sibling fall-through arm is never dropped, because both codegen drop sites (the fn-return Own-param dec in lib.rs and the pre-tail-call dec in match_lower.rs) gate on the per-fn AGGREGATE consume_count. When the param is consumed on one arm (aggregate >= 1) but live on another, the gate skips the drop on the live arm too. This is the residual that keeps examples/series_sma.ail at live=2 after legs 1 and 2. Series-free minimal repro (a `Box` consumed on the `On` arm, live on the `Off` fall-through arm; main takes the `Off` path): `live=1` today. Committed #[ignore]: unlike legs 1 and 2, this is NOT a contained fix. The per-arm/per-path consume information is destroyed by the worst-case `max` merge in uniqueness.rs (`merge_states`) before MIR — MArm carries only {pat, body}, MirDef.consume is the per-fn aggregate — so codegen has no per-arm liveness to gate a fall-through drop on. Closing it needs a memory-model change (retain per-arm consume, surface it to codegen, emit the drop only on the live arm, never at the post-match join or the consuming arm — a live double-free hazard) and a fresh brainstorm cycle. The pin is committed ignored so the precise symptom and minimal repro are durable; un-ignore when the fix ships. The assertion is a correct symptom pin (live == 0); only the fix mechanism is undecided. refs #63 |
||
|
Brummel
|
e3a9065aa7 |
fix(codegen): drop owned values on let/seq-wrapped tail-call arms (#63 leg 2)
After leg 1, a tail call wrapped in a trailing `(let ...)` / `(seq ...)`
still leaked: `arm_body_is_tail_call` matched only a direct
App/Do{tail:true} arm body, so for an MTerm::Let/Seq body the gate was
false and both pre-tail-call drops (the scrutinee-husk shallow-dec and
the leg-1 owned-param dec) were skipped — while lower_term still
descended through the wrapper and emitted the inner call as musttail.
The fix replaces the one-level match with a local recursive
`tail_position_is_tail_call` that peels through a trailing Let-body /
Seq-rhs chain to its tail-position sub-term. This is a contained fix:
the predicate feeds only the two drop-emission gates, never the
musttail-emission decision (which is independent, in lower_term off
App{tail:true}), so widening it restores the drops without changing
which calls are tail calls. The let-bound value's scope-close drop is
gated on `!block_terminated` and stays correctly skipped, so the
forwarded let binding is not double-freed.
Verified: the leg-2 pin goes green (live=0, was live=4); the leg-1 pin
stays green; full `cargo test --workspace` 0 failures, no double-free /
underflow / IR-snapshot delta; lockstep pairs untouched.
examples/series_sma.ail drops from live=8 to live=2 with unchanged
stdout (3.0 / 5.33333 / 5.66667 / 5.33333).
Not yet leak-clean: the residual live=2 is a THIRD, distinct leg — an
(own) heap param consumed on one match arm but live on a sibling
base-case (non-tail fall-through) arm is not dropped there, because the
fn-return Own-param dec gates on the per-fn AGGREGATE consume_count
(>=1 here, from the recursive arm) rather than per-arm liveness. Routed
as its own RED-first bugfix.
refs #63
|
||
|
Brummel
|
2488d9d345 |
test(codegen): RED pin for let-wrapped tail-call leak (#63 leg 2)
After the leg-1 fix (
|
||
|
Brummel
|
68f500c4b0 |
fix(codegen): drop owned params on tail-call-terminated match arms (#63 leg 1)
An owned heap ADT param that a tail-recursive match arm neither forwards into the tail call nor consumes had no drop site: the fn-return Own-param dec in lib.rs is gated behind `!block_terminated` and so fires only on the fall-through `ret` path, while the per-arm drop in match_lower.rs handled only pattern binders. A `musttail call`-terminated arm therefore leaked one slab per recursion step (#63, leg 1). match_lower.rs now emits a pre-tail-call Own-param dec, gated exactly like the fn-return path: Rc strategy, `arm_body_is_tail_call`, ParamMode::Own, ptr-typed, and uniqueness `consume_count == 0`. For an Own param consume_count==0 also implies "not forwarded into the tail call" — a forwarded Own arg is walked Position::Consume and carries consume_count>=1 — so the gate cannot drop a param the callee took ownership of. The drop routes through the same per-type / partial-drop machinery (honouring moved_slots) as the fn-return path. The match scrutinee param is explicitly skipped: its ownership is already discharged by the pre-tail-call scrutinee-husk shallow-dec plus the moved-out field binders, so dropping it here would dec the same outer cell twice (a double-handling the first cut of this fix introduced and the quality review caught — the pin read live=0 but the IR showed two decs on the scrutinee cell). Verified: the committed RED pin is green (live=0, allocs==frees); full `cargo test --workspace` 0 failures; the fix introduces no under-free (loop_recur_heap_binder / loop_recur_str_binder / loop_str_recur_literal / rc_pin_recurse_implicit / lit_pat_ctor_tail_drop all stay live=0, no underflow to depth 5). No INTERCEPTS/(intrinsic) or pre_desugar_validation change; no IR snapshot refresh needed. Leg 1 only. Leg 2 — a `let`/`seq`-wrapped tail call makes the arm body an MTerm::Let so `arm_body_is_tail_call` is false, skipping both the husk-dec and this new param-dec — still leaks (examples/series_sma.ail stays live=8). It gets its own RED pin and fix next. refs #63 |
||
|
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 |