From 208d7095bc915ceb15200dea5c595db23e9ce43c Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 18 May 2026 23:50:13 +0200 Subject: [PATCH] =?UTF-8?q?fix(check):=20GREEN=20=E2=80=94=20over-strict-m?= =?UTF-8?q?ode=20recognises=20ctor-rebuild-from-primitive-fields=20as=20a?= =?UTF-8?q?=20consume?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Drives the RED test from a11cb7c to GREEN. Bug-fix iter bugfix-over-strict-mode-ctor-rebuild-consume (debug -> implement mini). Check-only lint-precision fix; zero codegen / runtime / ABI / schema / DESIGN.md change. The [over-strict-mode] lint's consume-detection (any_sub_binder_consumed_for / pattern_has_consumed_heap_binder, crates/ailang-check/src/linearity.rs) only recognised a consume of an (own (con T)) param when a heap-typed pattern-binder was moved out of `match p`. When p was destructured into purely primitive fields fed into a Term::Ctor rebuilding p's own ctor, that genuine dismantle+rebuild consume was invisible, so the lint spuriously advised "(borrow ...) would suffice". An LLM author "fixing" that by flipping an export own->borrow would silently invert the ABI ownership contract — why a low-severity advisory FP got a real RED-first fix. Fix: a second recognition path in any_sub_binder_consumed_for — a `match p` arm destructuring binders out of p's ctor that references any of them (primitive or not) inside a Term::Ctor's args in the arm body genuinely consumes p. Two pure helpers: ctor_uses_any_binder (finds a fresh-allocation Term::Ctor reachable in the arm body) + term_mentions_any_binder (deep free-var scan, so binder flow through an intervening expr like (+ acc px) is recognised, not only a bare Var arg). Conservative toward NOT suppressing: a ctor ignoring p's payload still warns (negative-control verified). Over-strict-only — by-name-shadowing imprecision is extra-silence, never under-strict (Known debt in the journal + the fn doc). The two stale doc comments that mis-attributed this FP to a nested `match` corrected for doc-honesty (debugger concern #2 — same code region, in-scope). Boss-verified independently: RED test now GREEN; full cargo test -p ailang-check 108/0 lib + every binary 0-failed with NO existing test modified; ail check examples/embed_backtest_step_tick.ail no longer warns over-strict on st/tick (exit 0); embed_backtest_step_tick_borrow.ail + M3 embed_backtest_step_record.ail still clean; embed_tick_e2e + bench posture untouched. +166/-20 in crates/ailang-check/src/linearity.rs only. Journal + stats + INDEX line in this commit. --- ...over-strict-mode-ctor-rebuild-consume.json | 13 ++ crates/ailang-check/src/linearity.rs | 186 ++++++++++++++++-- ...x-over-strict-mode-ctor-rebuild-consume.md | 74 +++++++ docs/journals/INDEX.md | 1 + 4 files changed, 254 insertions(+), 20 deletions(-) create mode 100644 bench/orchestrator-stats/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.json create mode 100644 docs/journals/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.md diff --git a/bench/orchestrator-stats/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.json b/bench/orchestrator-stats/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.json new file mode 100644 index 0000000..f32c76b --- /dev/null +++ b/bench/orchestrator-stats/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.json @@ -0,0 +1,13 @@ +{ + "iter_id": "bugfix-over-strict-mode-ctor-rebuild-consume", + "date": "2026-05-18", + "mode": "mini", + "outcome": "DONE", + "tasks_total": 1, + "tasks_completed": 1, + "reloops_per_task": { "1": 1 }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null, + "notes": "One within-implementer-phase repair: unit RED test went GREEN on the first implementation, but acceptance gate 3 (real examples/embed_backtest_step_tick.ail) still warned because the ctor args are App expressions (+ acc px), not bare Var. Redesigned ctor_uses_any_binder to deep-scan ctor args via term_mentions_any_binder; all 5 gates then green. Spec-compliance and quality checks each passed first pass. No existing test modified." +} diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index 70477a8..d8afa51 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -116,16 +116,28 @@ //! `match xs { Cons(h, t) => h }` returns `h: Int`; without the //! filter, `h.consume_count == 1` would silence the lint. //! -//! **Known debt: deeply-nested-match-on-sub-binder.** A pattern like -//! `match p { Ctor(_, t) => match t { Ctor(_, t2) => consume(t2) } }` -//! has the inner match's scrutinee `t` (not `p`), so the inner-arm -//! binder `t2`'s consume is not seen when we ask "did any arm-binder -//! of `match p` get consumed?". The outer-arm binder `t` has -//! `consume_count == 0` (matching is Borrow), so the lint will fire -//! even though `(own T)` is genuinely needed because `t2` is -//! consumed. This is recorded in the JOURNAL as a follow-up; for the -//! current corpus it would cost a spurious warning rather than miss -//! a real one. +//! ### Bugfix `over-strict-mode-ctor-rebuild-consume` +//! +//! The heap-typed-sub-binder check above does not see the consume +//! when an arm destructures `p`'s ctor into *primitive* fields and +//! then feeds them into a `Term::Ctor` that rebuilds an allocation — +//! e.g. `match p { State(acc, n) => State(acc, n) }`, or the nested +//! `match st { State(acc, n) => match tick { Tick(px) => State(..) } }` +//! body of `embed_backtest_step_tick`. The rebuild dismantles `p`'s +//! box and re-packages its payload into a fresh allocation; with +//! `(borrow ...)` the scrutinee's box could not be taken apart, so +//! `(own ...)` is genuinely required and the lint must stay silent. +//! `pattern_has_consumed_heap_binder` filters the primitive binders +//! out, so it could not catch this. The fix adds a second +//! recognition path (`collect_pattern_binders` + +//! `ctor_uses_any_binder`): +//! if a destructured binder of the matched arm — primitive or not — +//! is referenced by any `Term::Ctor` in the arm body, the param is +//! consumed. An earlier draft of this note mis-attributed the +//! false-positive to deeply-nested `match`-on-sub-binder; that was a +//! misdiagnosis. The defect is the unrecognised ctor-rebuild +//! consume, independent of match nesting, and it caused a *spurious* +//! warning (over-strict), never a missed one. use crate::diagnostic::Diagnostic; use crate::uniqueness::{infer_module as infer_uniqueness, UniquenessTable}; @@ -840,16 +852,24 @@ fn make_use_after_consume_at_reuse_as(def: &str, binder: &str, body: &Term) -> D /// `match p ...` may sit arbitrarily deep inside `If` / `Let` / /// `App` / etc. /// -/// **Known limit (recorded as debt in JOURNAL.md):** if an arm's -/// body contains a *nested* match on a sub-binder of `p` (e.g. -/// `match p { Ctor(_, t) => match t { Ctor(_, t2) => consume(t2) } }`), -/// we only check `t.consume_count`, not `t2.consume_count`. The -/// inner match's scrutinee is `t`, not `p`, and our recursion looks -/// for `match-on-pname`, so we miss `t2`. For the current corpus -/// this would mean a *spurious* warning (the lint fires but `(own)` -/// is genuinely needed), not a missed one. The fix is to either -/// chase pattern-binder lineage or to check inner matches whose -/// scrutinee transitively traces back to `p`. +/// **Ctor-rebuild consume (bugfix +/// `over-strict-mode-ctor-rebuild-consume`):** besides a heap-typed +/// sub-binder being moved out, the param is also genuinely consumed +/// when an arm destructures `p`'s ctor and feeds the extracted +/// fields — *including purely primitive ones* — into a `Term::Ctor` +/// that builds a fresh allocation (e.g. +/// `match p { State(acc, n) => State(acc, n) }`, or the nested +/// `match st { State(acc, n) => match tick { Tick(px) => State(..) } }` +/// shape of `embed_backtest_step_tick`). The rebuild dismantles +/// `p`'s box and re-packages its payload, which `(borrow ...)` could +/// not do, so `(own ...)` is required. `pattern_has_consumed_heap_binder` +/// misses this because the destructured fields are primitive; the +/// `collect_pattern_binders` + `ctor_uses_any_binder` pair below +/// recognises it. The earlier draft of this comment mis-attributed +/// the defect +/// to a nested `match` on a sub-binder of `p`; the real mechanism is +/// the unrecognised ctor-rebuild consume, independent of match +/// nesting. fn any_sub_binder_consumed_for( t: &Term, pname: &str, @@ -865,6 +885,20 @@ fn any_sub_binder_consumed_for( if pattern_has_consumed_heap_binder(&arm.pat, uniq, def_name, ctors) { return true; } + // Ctor-rebuild consume: destructuring `p`'s ctor + // and feeding the extracted fields (incl. + // primitive ones) into a `Term::Ctor` builds a + // fresh allocation out of `p`'s dismantled + // payload. That genuinely consumes the `(own)` + // scrutinee — `(borrow)` could not dismantle it. + // `pattern_has_consumed_heap_binder` misses this + // because the destructured fields are primitive. + let destructured = collect_pattern_binders(&arm.pat); + if !destructured.is_empty() + && ctor_uses_any_binder(&arm.body, &destructured) + { + return true; + } // Recurse into the arm body: a deeper // `match p ...` could also count. if any_sub_binder_consumed_for(&arm.body, pname, uniq, def_name, ctors) { @@ -990,6 +1024,118 @@ fn pattern_has_consumed_heap_binder_at( } } +/// Bugfix `over-strict-mode-ctor-rebuild-consume`: `true` iff some +/// `Term::Ctor` reachable in `t` builds a fresh allocation whose +/// argument subtrees mention at least one of `binders` (the names +/// the matched arm destructured out of `p`'s ctor). That means the +/// dismantled payload of the `(own)` scrutinee — possibly via an +/// intervening expression such as `(+ acc px)` — flows into a newly +/// allocated ctor, which `(borrow ...)` could not do (a borrowed +/// value's box may not be taken apart and re-packaged). So `(own)` +/// is genuinely required and the lint must stay silent. +/// +/// Conservative toward *not* suppressing: the ctor's args must +/// actually reference a destructured binder. A ctor that ignores +/// `p`'s payload (e.g. `match p { _ => Other(42) }`, or +/// `match p { P(x) => Other(42) }`) does **not** trip this and the +/// lint still warns. The binder scan is by name; a destructured +/// primitive binder shadowed and rebound before reaching the ctor +/// is not a corpus shape, and any resulting imprecision is in the +/// over-strict (extra-silence) direction the cause explicitly +/// permits, never under-strict. +fn ctor_uses_any_binder(t: &Term, binders: &[String]) -> bool { + match t { + Term::Ctor { args, .. } => { + // A freshly-built allocation: does its payload draw from + // the destructured binders (at any depth)? Also recurse + // — a ctor may be nested inside another ctor's args. + args.iter().any(|a| term_mentions_any_binder(a, binders)) + || args.iter().any(|a| ctor_uses_any_binder(a, binders)) + } + Term::Lit { .. } | Term::Var { .. } => false, + Term::Match { scrutinee, arms } => { + ctor_uses_any_binder(scrutinee, binders) + || arms.iter().any(|a| ctor_uses_any_binder(&a.body, binders)) + } + Term::App { callee, args, .. } => { + ctor_uses_any_binder(callee, binders) + || args.iter().any(|a| ctor_uses_any_binder(a, binders)) + } + Term::Let { value, body, .. } => { + ctor_uses_any_binder(value, binders) || ctor_uses_any_binder(body, binders) + } + Term::LetRec { body, in_term, .. } => { + ctor_uses_any_binder(body, binders) || ctor_uses_any_binder(in_term, binders) + } + Term::If { cond, then, else_ } => { + ctor_uses_any_binder(cond, binders) + || ctor_uses_any_binder(then, binders) + || ctor_uses_any_binder(else_, binders) + } + Term::Seq { lhs, rhs } => { + ctor_uses_any_binder(lhs, binders) || ctor_uses_any_binder(rhs, binders) + } + Term::Do { args, .. } => args.iter().any(|a| ctor_uses_any_binder(a, binders)), + Term::Lam { body, .. } => ctor_uses_any_binder(body, binders), + Term::Clone { value } => ctor_uses_any_binder(value, binders), + Term::ReuseAs { source, body } => { + ctor_uses_any_binder(source, binders) || ctor_uses_any_binder(body, binders) + } + Term::Loop { binders: lb, body } => { + lb.iter().any(|b| ctor_uses_any_binder(&b.init, binders)) + || ctor_uses_any_binder(body, binders) + } + Term::Recur { args } => args.iter().any(|a| ctor_uses_any_binder(a, binders)), + } +} + +/// Bugfix `over-strict-mode-ctor-rebuild-consume`: deep free-variable +/// scan — does `t` mention any name in `binders` anywhere in its +/// subtree (as a `Var`, possibly under `Clone` / `App` / arithmetic / +/// nested ctor / …)? Used to test whether a `Term::Ctor`'s argument +/// draws, directly or through an intervening expression, from the +/// destructured payload of the matched `(own)` param. +fn term_mentions_any_binder(t: &Term, binders: &[String]) -> bool { + match t { + Term::Var { name } => binders.iter().any(|b| b == name), + Term::Lit { .. } => false, + Term::Ctor { args, .. } | Term::Do { args, .. } | Term::Recur { args } => { + args.iter().any(|a| term_mentions_any_binder(a, binders)) + } + Term::App { callee, args, .. } => { + term_mentions_any_binder(callee, binders) + || args.iter().any(|a| term_mentions_any_binder(a, binders)) + } + Term::Match { scrutinee, arms } => { + term_mentions_any_binder(scrutinee, binders) + || arms.iter().any(|a| term_mentions_any_binder(&a.body, binders)) + } + Term::Let { value, body, .. } => { + term_mentions_any_binder(value, binders) || term_mentions_any_binder(body, binders) + } + Term::LetRec { body, in_term, .. } => { + term_mentions_any_binder(body, binders) || term_mentions_any_binder(in_term, binders) + } + Term::If { cond, then, else_ } => { + term_mentions_any_binder(cond, binders) + || term_mentions_any_binder(then, binders) + || term_mentions_any_binder(else_, binders) + } + Term::Seq { lhs, rhs } => { + term_mentions_any_binder(lhs, binders) || term_mentions_any_binder(rhs, binders) + } + Term::Lam { body, .. } => term_mentions_any_binder(body, binders), + Term::Clone { value } => term_mentions_any_binder(value, binders), + Term::ReuseAs { source, body } => { + term_mentions_any_binder(source, binders) || term_mentions_any_binder(body, binders) + } + Term::Loop { binders: lb, body } => { + lb.iter().any(|b| term_mentions_any_binder(&b.init, binders)) + || term_mentions_any_binder(body, binders) + } + } +} + /// Iter 19a: a scrutinee "is" `pname` if it's a bare `Var { pname }` /// or `Clone(Var { pname })`. Anything else (a fresh App result, a /// let-binder, …) does not put `pname` directly in scrutinee diff --git a/docs/journals/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.md b/docs/journals/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.md new file mode 100644 index 0000000..e123760 --- /dev/null +++ b/docs/journals/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.md @@ -0,0 +1,74 @@ +# iter bugfix-over-strict-mode-ctor-rebuild-consume — over-strict-mode FP on ctor-rebuild-from-primitive-fields + +**Date:** 2026-05-18 +**Started from:** a11cb7cc9f912a0d7ee8a56b3f53255bd101e327 +**Status:** DONE +**Tasks completed:** 1 of 1 + +## Summary + +The `over-strict-mode` lint spuriously fired `(borrow ...) would +suffice` on `(own (con T))` params whose body destructures `T` into +purely *primitive* fields and then feeds those fields into a +`Term::Ctor` that builds a fresh allocation. The dismantle+rebuild +is a genuine consume of the scrutinee's box (a borrowed value's +payload cannot be taken apart and re-packaged), but the lint's +consume-detection only recognised a *heap-typed* pattern-binder +being moved out — primitive fields are filtered by +`pattern_has_consumed_heap_binder`, so the rebuild was invisible. +This is the false positive behind `embed_backtest_step_tick.ail` +warning on both `st` and `tick`. The fix adds a second recognition +path in `any_sub_binder_consumed_for`: for a `match p` arm that +destructures binders out of `p`'s ctor, if any of those binders +(primitive or not) is mentioned anywhere inside a `Term::Ctor`'s +argument subtrees in the arm body, the param is genuinely consumed +and the lint stays silent. Over-strict-only: a param merely read +(no ctor build) still warns, proven by a negative control. No +existing test changed; doc-honesty corrections applied to the two +stale comments that mis-attributed this defect to nested `match`. + +## Per-task notes + +- iter bugfix-over-strict-mode-ctor-rebuild-consume.1: added + `collect_pattern_binders`-based ctor-rebuild-consume recognition + to `any_sub_binder_consumed_for`'s matched-scrutinee arm loop in + `crates/ailang-check/src/linearity.rs`, plus two pure private + helpers (`ctor_uses_any_binder` — finds a fresh-allocation + `Term::Ctor` reachable in the arm body; `term_mentions_any_binder` + — deep free-var scan of that ctor's args, so the binder reaching + the ctor *through* an expression like `(+ acc px)` is recognised, + not only a bare `Var` arg). Corrected the stale "Known limit" doc + on `any_sub_binder_consumed_for` and the matching "Known debt: + deeply-nested-match-on-sub-binder" block in the module header — + both previously mis-attributed the FP to a nested match; the real + mechanism is the unrecognised ctor-rebuild consume, independent of + match nesting. + +## Concerns + +(none) + +## Known debt + +- `term_mentions_any_binder`'s binder scan is by name and does not + track shadowing. A destructured primitive binder shadowed and + rebound before reaching the ctor would still be counted. This is + not a corpus shape, and the resulting imprecision is strictly in + the over-strict (extra-silence) direction the cause explicitly + permits — never under-strict, so no soundness risk. Documented in + the function's own doc comment; left as-is per the minimal-fix + constraint. + +## Blocked detail + +(not blocked) + +## Files touched + +- crates/ailang-check/src/linearity.rs (+166 / −20): lint-detection + fix + two helpers + two doc-honesty corrections. Check-only; no + codegen / runtime / ABI / schema / DESIGN.md change. + +## Stats + +bench/orchestrator-stats/2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.json diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index f0ef976..816ad9a 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -105,3 +105,4 @@ - 2026-05-18 — audit embedding-abi-m3 (Embedding ABI — M3 milestone close — DRIFT: one [medium]+[low] doc-honesty → one tidy; bench check.py exit 1 decisively causally exonerated, NO ratify): architect `drift_found` — Invariant 1 clean (zero Cargo/runtime dep change; core/codegen/runtime touches only the spec-scoped widen + lockstep comments + pins; no data-server/finance knowledge), the M1/M2 internal-convention byte-invariant held (M2 forwarder body + @ail__/_adapter/_clos absent from the diff — the spec's load-bearing "transparent ptr pass-through" claim verified), the frozen-layout SSOT (DESIGN.md `### Frozen value layout` :2321-2359) present-tense + matching `match_lower.rs lower_ctor` (size=8+n*8/tag@0/fields@8+i*8) AND the enforcing byte-pin (@ailang_rc_alloc(i64 24)/tag@0/@8/@16), all three // FROZEN ABI lockstep pointers aimed at the SSOT, the Boss spec-consistency repair note + Testing 3/4 + journal Boss-adjudication/Re-dispatch mutually consistent and honest about the M2-TLS cross-attribution (correct behaviour, not a leak), no new CheckError/schema/Form-A (M2-style honoured). Two residual doc-honesty drift items, both milestone-owned: `[medium]` DESIGN.md:2299-2302 — a surviving M1-era paragraph asserts modes "apply only to heap-shaped types, which the **scalar-only rule above forbids** at an export boundary anyway", now self-contradicting the section's own freeze (`:2280-2284` was rewritten to accept a single-ctor record — there is no scalar-only rule) and the (own/borrow (con State)) mode contract at :2345-2351 → fix (docs-honesty tidy); `[low]` crates/ailang-codegen/src/lib.rs:608-610 — forwarder-body comment still says the gate "guarantees Int/Float; map Int→i64 Float→double", now false (records→ptr), classified by the architect "carried debt, not a scope miss" (the body is contractually byte-frozen so the comment was outside any M3 edit region; comment-only, no emitted-IR change) → fix, folded into the same tidy. (The Boss had already caught+fixed one sibling stale `//` gate-comment block at check/lib.rs:1917-1922 during the DONE inspect; architect found no further siblings.) Bench: check.py exit 1 (3 regressed: throughput.bench_list_sum.bump_s +12.62%/tol10; latency.implicit_at_rc.p99_9_us +28.45%/tol25; .max_us +35.18%/tol30), compile_check exit 0 (24/0), cross_lang exit 0 (25/0, every rc_over_c within tol). The 3 firings are the two standing tracked P2 noise families (the *.bump_s ~+5-13% stale-baseline + the *.max_us/p99_9 -n5 tail-jitter structural false-positive — signature: same bench median +5.11% ok / p99 +15.08% ok, only the extreme tail quantiles fire). DECISIVE causal exoneration (M2-audit method, not hand-waved): M3 changed no executable-path codegen (the llvm_scalar record→ptr arm is reachable only for an (export) single-ctor record; no bench_* program has an (export)), so built `ail` at HEAD and at pre-M3 9a609ae in an isolated worktree and cmp'd the GENERATED IR — byte-identical for bench_list_sum, bench_list_sum_explicit, bench_latency_implicit, bench_tree_walk; the IR is what is handed to deterministic `clang -O2`, so the bench binaries are byte-identical and M3 causation is logically impossible. NO baseline ratify (not M3 artefacts; the two P2 todos stay separately tracked). Resolution: `[medium]`+`[low]` → one docs-honesty tidy iter embedding-abi-m3.tidy (pin-safe re docs_honesty_pin.rs:135, planner Step-5 item-6 / M2.tidy precedent), routed planner→implement; bench → carry-on. Milestone substantively closed + sound; roadmap [~]→[x] follows the tidy landing clean. → 2026-05-18-audit-embedding-abi-m3.md - 2026-05-18 — iter embedding-abi-m3.tidy (M3 audit [medium]+[low] doc-honesty fix, DONE 3/3, pin-safe): closed the two DRIFT items the M3 milestone-close audit routed here (M2.tidy `[medium]+[low] doc-honesty → tidy` precedent). [medium] docs/DESIGN.md §"Embedding ABI" — surgically replaced ONLY the contradicted M1-era parenthetical "(modes apply only to heap-shaped types, which the scalar-only rule above forbids at an export boundary anyway)" with the present-tense truth "(a single-constructor record export parameter, by contrast, carries `own`/`borrow` — the ownership contract the frozen value layout below specifies)"; the parenthetical shared physical line :2300 with the docs_honesty_pin.rs:135 pinned bare-scalar sentence ("Export parameters are written **bare**: a scalar type carries no `own`/`borrow` mode", norm()-whitespace-collapsed, fn form_a_scalar_param_carveout_present_and_old_rule_absent) — the edit kept every pinned word (line :2299 + the `own`/`borrow` mode` continuation untouched), the planner Step-5 item-6 presence-pin-vs-verbatim-edit collision the M2.tidy precedent ran. [low] crates/ailang-codegen/src/lib.rs:608-610 — comment-only honesty fix ("gate guarantees Int/Float; map Int→i64,Float→double" → "...Int/Float or a single-constructor record of those (M3); map Int→i64, Float→double, a record → ptr"); tree-wide-grep-confirmed no test pins the comment text; the byte-pin (embed_record_layout_pin) + forwarder-IR pin (embed_staticlib_lowering) assert generated IR not source comments → byte-identical before/after (the guard that no codegen moved). Boss-verified independently: both stale fragments grep-ABSENT; the 4 standing pins green at the exact recon baseline (docs_honesty_pin 5/0 ⇒ pin-safety held, design_schema_drift 8/0, embed_record_layout_pin 1/0, embed_staticlib_lowering 3/0); workspace 639/77 byte-unchanged from the M3-DONE baseline (docs/comment tidy, zero behaviour/test delta); diff exactly 2 files (DESIGN.md 5±, codegen/src/lib.rs 7±). No language/checker/codegen behaviour change; no audit/fieldtest gate (the 4 pins + 639/77 ARE the regression coverage, M2.tidy precedent). One non-gating planner-quality defect recorded in Concerns: Task-3 Step-1's `guarantees every param` verification grep is a substring of the plan's own Task-2 replacement text (non-discriminating) — the orchestrator correctly verified the substantive intent via discriminating fragments instead of bending code (same family as planner Step-5 item-8). bench: already carry-on / NO ratify at the M3 audit (causally exonerated by byte-identical generated IR; this tidy touches no executable path). audit source docs/journals/2026-05-18-audit-embedding-abi-m3.md (b8a60b1) → plan docs/plans/embedding-abi-m3.tidy.md (44ced51) → iter this commit. M3 milestone substantively closed + sound; roadmap [~]→[x] follows. → 2026-05-18-iter-embedding-abi-m3.tidy.md - 2026-05-18 — brainstorm embedding-abi-m4 → RETIRED, never speced (premise collapsed under its own feature-acceptance gate during Step-2/3 Q&A; no spec, no grounding-check, no planner handoff — the "problem mis-framed → don't ratify a known-unneeded shape" brainstorm path): `/boss` picked top-P0 "Embedding ABI — M4: sequence crossing via `List`"; user green-lit a continue-here brainstorm; recon (`ailang-plan-recon`) returned a full fact sheet; two user forks resolved in Q&A (own-only `List` param; `List Record`-only element) and Approach A (structural list-shaped `is_c_abi_type` arm, no name-match; B name-anchored / C `std_list`-SSOT-first rejected on language/scope grounds) recommended — all now moot. Struck on **feature-acceptance clause 2**: the shipped M3 gate `is_c_abi_type` (`crates/ailang-check/src/lib.rs:1934-1953`) is a per-parameter loop accepting a C scalar OR a single-ctor all-scalar record *independently per param*, and the forwarder's `llvm_scalar` maps every non-scalar `Type::Con`→`ptr` (M3-frozen), so `(State, Tick) -> State` (both single-ctor all-scalar records) is **already gate-accepted + forwarder-supported today** — the minimal data-server binding is M3 (shipped) + a host-side per-tick loop; cons-list crossing would *add* a 2N+1-box-per-chunk host builder + the deferred flat-array perf debt and removes no redundancy, with no named consumer (M5's adapter unrolls each chunk host-side — a clean adapter, the sole data-server↔AILang meeting point per Invariant 1; whole-chunk in-kernel visibility is semantically void since `State` threads across calls regardless of chunk boundaries). Honest mid-Q&A correction recorded: I had asserted "M5 cannot wire data-server without M4" — false (M5 wires it on M3 + `for tick in chunk`); re-deriving against the code rather than defending the roadmap I wrote is what surfaced the clause-2 failure ("user suggestions ≠ directives, form own judgment"). Outcome: M4 retired in `docs/roadmap.md` (struck entry kept one cycle, never `[x]`); M5 reconciled (`depends on:` M4→M3 + Tick-coverage todo; adapter unrolls host-side; friction feeds the host-per-tick-FFI-vs-batch P2 perf decision); residual = a new `[todo]` "Tick-coverage on M3" (E2E+fixture pinning the two-record-param per-tick `(State, Tick) -> State` shape — capability present today but only E2E-proven for a single record param `State`; every shipped M3 fixture pushes a scalar `Float` sample, none a record `Tick`; test backfill, no brainstorm — the actual "minimal data-server binding"). Forward note: the P2 flat-array item's "1024 cons-cells/chunk" framing is now partly stale (cons-list path dropped) — reconcile when picked up, not now. → 2026-05-18-brainstorm-embedding-abi-m4-retired.md +- 2026-05-18 — iter bugfix-over-strict-mode-ctor-rebuild-consume (RED→GREEN, debug→implement mini, DONE 1/1): fixed a conservative `[over-strict-mode]` false-positive surfaced by the Tick-coverage fixtures. The lint's consume-detection (`any_sub_binder_consumed_for`/`pattern_has_consumed_heap_binder`, `crates/ailang-check/src/linearity.rs`) only recognised a consume of an `(own (con T))` param when a *heap-typed* pattern-binder was moved out of `match p`; when `p` was destructured into purely *primitive* fields fed into a `Term::Ctor` rebuilding `p`'s own ctor, that genuine dismantle+rebuild consume was invisible, so the lint spuriously advised `(borrow ...)`. Real harm: an LLM author "fixing" the spurious warning by flipping an export's declared mode `own`→`borrow` would silently invert the ABI ownership contract. RED-first: debugger disproved the carrier's initial nested-`match` hypothesis (the M3 `embed_backtest_step_record.ail` is silent only because its implicit-mode scalar `Float` param disables the lint via the activation gate, linearity.rs:327 — NOT because it handles the rebuild; the defect reproduces single-param, no nesting), wrote the synthetic RED unit `over_strict_mode_silent_when_ctor_rebuilt_from_primitive_fields` committed as its own audit-trail commit `a11cb7c`. GREEN (implement mini): added a 2nd recognition path to `any_sub_binder_consumed_for` — a `match p` arm that destructures binders out of `p`'s ctor and references any of them (primitive or not) inside a `Term::Ctor`'s args in the arm body genuinely consumes `p`; two pure helpers (`ctor_uses_any_binder` + deep `term_mentions_any_binder`, so `(+ acc px)`-mediated flow counts), conservative toward NOT suppressing (a ctor ignoring `p`'s payload still warns — negative-control proven), over-strict-only (by-name shadowing imprecision is extra-silence, never under-strict; recorded as Known debt). Both stale doc comments that mis-attributed the FP to nested `match` corrected for doc-honesty (debugger concern #2, same code region — in-scope, not opportunistic). +166/−20 in linearity.rs only; check-only, zero codegen/runtime/ABI/schema/DESIGN.md change. Boss-verified independently: RED→GREEN, full `cargo test -p ailang-check` 108/0 lib + every binary 0-failed with NO existing test modified, `ail check embed_backtest_step_tick.ail` no longer over-strict on `st`/`tick` (exit 0), `_tick_borrow.ail` + M3 `embed_backtest_step_record.ail` still clean, the already-green `embed_tick_e2e` + bench posture untouched. No audit/fieldtest gate (lint-precision bugfix; the RED test + the green check-suite ARE the regression coverage). RED `a11cb7c` → GREEN this commit. → 2026-05-18-iter-bugfix-over-strict-mode-ctor-rebuild-consume.md