From dfdc65f21f37f080aeb9cfc4bd167eb730727394 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 18:29:02 +0200 Subject: [PATCH] =?UTF-8?q?audit:=20spec=200064=20cycle=20close=20?= =?UTF-8?q?=E2=80=94=20drift-clean=20after=20two=20ledger=20fixes=20(#57)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Cycle-close audit for spec 0064 (the #57 hardening of the linearity analysis, the #55-cutover precondition; four iterations 47964ab, cc5991e, be259f9, 2769e50). Architect drift review (39b674c..HEAD): both CLAUDE.md lockstep pairs confirmed untouched (INTERCEPTS↔intrinsic markers; Pattern::Lit typecheck↔pre_desugar_validation) — the cycle is genuinely diagnostic-only. It found two drift items, both in the iter-3 contract edit, both fixed here (fix path, folded into the audit close since they are doc-only): 1. [medium] design/contracts/0008-memory-model.md — the iter-3 rewrite placed a "Covers let-aliases…" statement under the "What this widening does NOT do" heading (incoherent) and named only the linearity-check mechanism, silently dropping the codegen dimension the original carve-out actually referred to ("Iter A / pre-tail-call shallow-dec arm" = the drop gates). Verified the real current state: let-aliases are propagated on BOTH axes — the linearity diagnostic (Checker.aliases + resolve_alias, this cycle) AND the codegen drop gates (MTerm::Let's current_param_modes mode inheritance, ailang-codegen/src/lib.rs:1811, pre-existing). The bullet is moved out of the "does NOT do" list into a positive paragraph naming both mechanisms. 2. [low] design/INDEX.md memory-model row — the ratifying-test cell listed only uniqueness.rs while the contract trailer now also names linearity.rs. Cell updated to "uniqueness.rs + linearity.rs". Regression gate (both green, exit 0): - bench/check.py: 34 metrics; 0 regressed, 1 improved beyond tolerance (latency.implicit_at_rc.median_us -5.27%), 33 stable. The "improved" is measurement noise, NOT a real metric move — this cycle is diagnostic-only and touches no codegen/runtime, so it cannot have improved runtime latency. Baseline deliberately NOT updated (no ratify: nothing in the code moved the metric). - bench/compile_check.py: 24 metrics; 0 regressed, 24 stable. Outcome: cycle 0064 tidy (drift-clean). All four #57 hardening classes (value-typed let-binders, local fn-param modes, let-alias propagation, partition_eithers double-consume) shipped and ratified. The #55-cutover precondition is met. Drift-clean is not a milestone close: #55 (the irreversible ParamMode::Implicit deletion) is the next, separate step. refs #57 --- design/INDEX.md | 2 +- design/contracts/0008-memory-model.md | 25 ++++++++++++++++--------- 2 files changed, 17 insertions(+), 10 deletions(-) diff --git a/design/INDEX.md b/design/INDEX.md index 1ffbe9f..a27fd0e 100644 --- a/design/INDEX.md +++ b/design/INDEX.md @@ -83,7 +83,7 @@ is the default. | authoring-surface | LLM author / stable | crates/ailang-surface/tests/round_trip.rs | design/contracts/0001-authoring-surface.md | | roundtrip-invariant | every release / stable | crates/ailang-surface/tests/round_trip.rs | design/contracts/0009-roundtrip-invariant.md | | language-constraints | LLM author / stable | crates/ailang-check/src/uniqueness.rs (in-source mod tests) | design/contracts/0015-language-constraints.md | -| memory-model | LLM author / stable | crates/ailang-check/src/uniqueness.rs (in-source mod tests) | design/contracts/0008-memory-model.md | +| memory-model | LLM author / stable | crates/ailang-check/src/uniqueness.rs + linearity.rs (in-source mod tests) | design/contracts/0008-memory-model.md | | data-model | LLM author / stable | crates/ailang-core/tests/design_schema_drift.rs | design/contracts/0002-data-model.md | | mangling | codegen / stable | crates/ail/tests/eq_ord_e2e.rs | crates/ailang-codegen/src/lib.rs //! | | env-construction | codegen / stable | crates/ailang-check/tests/duplicate_ctor_pin.rs | crates/ailang-codegen/src/lib.rs //! | diff --git a/design/contracts/0008-memory-model.md b/design/contracts/0008-memory-model.md index d245699..1ea5129 100644 --- a/design/contracts/0008-memory-model.md +++ b/design/contracts/0008-memory-model.md @@ -337,15 +337,22 @@ twice (double-free under a hypothetical Consume + scope-close). subsequent work added codegen consumers, not new schema fields. - Does not introduce a new `Type` variant. Mode metadata stays flat on `Type::Fn` (see "Schema additions" above on why). -- Covers let-aliases of borrowed values (spec 0064, class 2). A - let-binder whose value is a bare `Term::Var` resolving to a - tracked binder is recorded as an alias to that root in the - linearity walk (`crates/ailang-check/src/linearity.rs`, - `Checker.aliases` + `resolve_alias`); the binding does not - consume the source, and every binder-state lookup resolves - the alias to its root, so a borrow-position use of the alias - does not consume the root while a real double-consume through - the alias is still caught. +**Let-aliases of borrowed values are propagated** (no longer a +carve-out). A let-binder whose value is a bare `Term::Var` +resolving to a tracked binder is treated as an alias of that +source on both axes of the ownership analysis: + +- the linearity diagnostic (spec 0064, class 2) records `a → + root` in the walk (`crates/ailang-check/src/linearity.rs`, + `Checker.aliases` + `resolve_alias`) and resolves every + binder-state lookup to the root, so a borrow-position use of + the alias does not consume the source while a real + double-consume through the alias is still caught; +- the codegen drop gates (`crates/ailang-codegen/src/lib.rs`, + the `MTerm::Let` lowering's `current_param_modes` mode + inheritance) give the let-binder its source's mode, so the + scope-close drop gate treats an alias of a borrow as borrowed + and emits no spurious `dec`. Ratified by: `crates/ailang-check/src/uniqueness.rs`, `crates/ailang-check/src/linearity.rs`.