From b1519900289af728d066cb09d12e17daa6eb8126 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 30 May 2026 12:50:55 +0200 Subject: [PATCH] =?UTF-8?q?audit:=20raw-buf=20close-fixes=20=E2=80=94=20ho?= =?UTF-8?q?nesty=20+=20ledger=20for=20the=20binder-rename=20(refs=20#43)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Architect drift review at raw-buf milestone close (after 55d76ae closed #43) surfaced three items; this commit clears them. All three lockstep- invariant pairs were confirmed intact and the effective-name keying was confirmed consistent across the desugar→lift boundary (lift_letrecs reads the desugared tree's effective names too). 1. [high] Honesty fix. `fresh_binder`'s doc-comment (and 55d76ae's body) claimed "authored names cannot contain `$` — the lexer reserves it". False: the lexer (ailang-surface) reserves only `.`, not `$`. The `$`-for-synthetic convention is not enforced. So collision-freedom rests solely on the `used` + in-scope-`scope` probe, which does not see an authored `$` that is out of scope at mint time but later binds under the same `(def, name)` key — the very collision class this fix closes. Latent (no fixture uses a `$` binder), but the stated rationale was wrong. Doc-comment now describes the probe honestly and names the gap + its two possible closures (enforce the reservation, or seed `used` with every authored binder name in the def). The enforce-or-retract decision is the next-direction follow-up. 2. [medium] design/models/0003-pipeline.md — "desugar currently only flattens nested constructor patterns" no longer matches the code (it now also alpha-renames shadowing binders). Corrected to current state (honesty-rule). 3. [low] design/contracts/0008-memory-model.md — the three drop gates all key on `(def_name, binder_name)` consume_count, silently relying on per-fn binder-name injectivity, which the ledger never stated. Added that invariant as an explicit precondition of the gates, with the desugar guarantee and its ratifying tests. No code-logic change; doc-comment + ledger only. --- crates/ailang-core/src/desugar.rs | 18 +++++++++++++----- design/contracts/0008-memory-model.md | 17 +++++++++++++++++ design/models/0003-pipeline.md | 10 ++++++---- 3 files changed, 36 insertions(+), 9 deletions(-) diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index 4a4f8b5..591bb54 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -521,11 +521,19 @@ impl Desugarer { /// A binder name unique within the current fn: `$` with /// the lowest `n ≥ 1` free in both `scope` (in-scope effective - /// names) and `used` (the `$mp_` / `$lr_` synthetic space). - /// Records the minted name in `used` so a later mint is distinct. - /// Authored names cannot contain `$` (the lexer reserves it for - /// synthetic names), so `$` never collides with an - /// authored binder. + /// names) and `used` (the `$mp_` / `$lr_` synthetic space plus + /// prior mints). Records the minted name in `used` so a later mint + /// is distinct. + /// + /// `$` is the project's convention for synthetic names, but it is + /// NOT lexer-enforced — an authored binder may legally contain `$`. + /// The probe rejects a `$` that is already in `used` or + /// currently in `scope`, but it does NOT see an authored + /// `$` that is out of scope at mint time yet later binds + /// under the same `(def, name)` key. No fixture exercises an + /// authored `$` binder; closing that latent gap (enforce the + /// reservation, or seed `used` with every authored binder name in + /// the def) is tracked as a follow-up. fn fresh_binder(&mut self, base: &str, scope: &Scope) -> String { let mut n = 1u64; loop { diff --git a/design/contracts/0008-memory-model.md b/design/contracts/0008-memory-model.md index 00ded55..d969c16 100644 --- a/design/contracts/0008-memory-model.md +++ b/design/contracts/0008-memory-model.md @@ -268,6 +268,23 @@ metadata's role is explicit: the requirement that every ptr-typed slot in the active ctor's pattern is in `moved_slots[scrutinee]`. +**Per-fn binder-name injectivity (a precondition of every gate +above).** All three drop gates read `consume_count` from the +uniqueness side-table keyed by `(def_name, binder_name)`. Codegen +looks up by the binder's source name and must resolve the binding it +means — so within one `def_name`, every `binder_name` must denote +exactly one binding. The desugar pass guarantees this: it +alpha-renames any binder whose name shadows an enclosing binding to a +fresh `$` (`ailang-core::desugar`), so a shadow-rebind idiom +like `(let buf (new…) (let buf (set buf…) … (get buf)))` becomes +`buf, buf$1, buf$2, buf$3`. Without this, shadowed binders collapse +onto one key and a gate reads a sibling binding's `consume_count`, +suppressing or doubling a drop. Ratified by +`raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats` and +`flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed` in +`crates/ail/tests/e2e.rs`, and the desugar unit test +`shadowing_let_is_alpha_renamed`. + **`ret_mode` — let-binder trackability.** - **`Term::App` drop at let-scope close.** A diff --git a/design/models/0003-pipeline.md b/design/models/0003-pipeline.md index d4c3b3b..5e0c029 100644 --- a/design/models/0003-pipeline.md +++ b/design/models/0003-pipeline.md @@ -30,10 +30,12 @@ structurally cheapest allocator — it is not a production target. The **desugar** pass ([`ailang-core::desugar::desugar_module`](../../crates/ailang-core/src/desugar.rs)) runs before typecheck and codegen in every entry point of -`ailang-check` and `ailang-codegen`. It is a pure AST → AST rewriter — currently -only flattens nested constructor patterns, but is the chosen -home for any future surface-smoothing rewrites that should not bloat -the core AST or the backends. **Critical invariant:** `CheckedModule.symbols` +`ailang-check` and `ailang-codegen`. It is a pure AST → AST rewriter — +it flattens nested constructor patterns and alpha-renames any binder +whose name shadows an enclosing binding to a fresh `$` (so the +uniqueness side-table's `(def_name, binder_name)` key is injective per +fn), and is the chosen home for any future surface-smoothing rewrites +that should not bloat the core AST or the backends. **Critical invariant:** `CheckedModule.symbols` in the `check` entry point continues to hash from the *original* on-disk module, not the desugared one, so `ail diff` and `ail manifest` report identities that match the canonical JSON the user is editing.