From b8a60b1ec7fe95714b7f647f9353922640a62680 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 18 May 2026 21:37:26 +0200 Subject: [PATCH] =?UTF-8?q?audit=20embedding-abi-m3:=20milestone=20close?= =?UTF-8?q?=20=E2=80=94=20DRIFT=20(1=20[medium]+[low]=20doc-honesty=20->?= =?UTF-8?q?=20one=20tidy);=20bench=20check.py=20exit=201=20decisively=20ca?= =?UTF-8?q?usally=20exonerated=20(byte-identical=20generated=20IR=20HEAD?= =?UTF-8?q?=20vs=20pre-M3=209a609ae),=20NO=20ratify;=20architect=20Invaria?= =?UTF-8?q?nt=201=20+=20M1/M2=20byte-invariant=20+=20frozen-SSOT=20consist?= =?UTF-8?q?ency=20all=20clean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../2026-05-18-audit-embedding-abi-m3.md | 136 ++++++++++++++++++ docs/journals/INDEX.md | 1 + 2 files changed, 137 insertions(+) create mode 100644 docs/journals/2026-05-18-audit-embedding-abi-m3.md diff --git a/docs/journals/2026-05-18-audit-embedding-abi-m3.md b/docs/journals/2026-05-18-audit-embedding-abi-m3.md new file mode 100644 index 0000000..e23d7dc --- /dev/null +++ b/docs/journals/2026-05-18-audit-embedding-abi-m3.md @@ -0,0 +1,136 @@ +# audit Embedding ABI — M3 (milestone close) + +**Date:** 2026-05-18 +**Milestone range:** `9a609ae..4ea8bc5` (M2 roadmap-close → M3 DONE) +**Outcome:** DRIFT — one `[medium]` + one `[low]` doc-honesty item +→ a single docs-honesty tidy iteration; bench `check.py` exit 1 +**decisively causally exonerated** (byte-identical generated IR), +NO ratify. compile_check / cross_lang clean. + +## Step 1 — Architect drift review (`drift_found`) + +Dispatched `ailang-architect` over `9a609ae..HEAD`. + +**What holds (audited clean):** +- **Invariant 1 (clean core):** zero `Cargo.toml`/runtime dep + changes; `ailang-core`/`ailang-codegen`/`runtime/` touches are + only the spec-scoped widen + lockstep comments + pins. No + `data-server`/finance knowledge entered. +- **M1/M2 internal-convention byte-invariant held:** the M2 + `Target::StaticLib` forwarder body and the internal + `@ail__` / `_adapter` / `_clos` convention are *absent + from the diff* (untouched). The `llvm_scalar` / `is_c_abi_type` + widen is exactly the spec scope — no new `CheckError` variant, no + schema field, no Form-A change (M2-style honoured). +- **Frozen-layout SSOT consistent:** DESIGN.md + `### Frozen value layout` (`:2321-2359`) is present-tense and + matches both `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 lockstep + `// FROZEN ABI` pointers present and aimed at the SSOT. The Boss + spec-consistency repair note + §"Testing strategy" 3/4 + the + journal Boss-adjudication / Re-dispatch sections are mutually + consistent and honest about the M2-TLS cross-attribution (correct + behaviour, not a leak). + +**Drift / debt:** +- **`[medium]` `docs/DESIGN.md:2299-2302`** — a surviving M1-era + paragraph still asserts modes "apply only to heap-shaped types, + which the **scalar-only rule above forbids** at an export + boundary anyway". `:2280-2284` was rewritten to accept a + single-ctor record, so there is no longer a scalar-only rule; + this sentence now contradicts the section's own freeze and the + `(own (con State))`/`(borrow (con State))` mode contract at + `:2345-2351`. Canonical-spec internal contradiction the milestone + owned. → **fix** (docs-honesty tidy). +- **`[low]` `crates/ailang-codegen/src/lib.rs:608-610`** — the + forwarder-body comment still says the gate "guarantees every + param and the ret are `Int`/`Float`; map Int→i64, Float→double", + now false (records→ptr). The architect classified this "carried + debt, not a scope miss" — the forwarder *body* is contractually + byte-frozen, so the comment was genuinely outside any M3 edit + region. Comment-only; correcting it changes no emitted IR (the + byte-pin + forwarder-IR pin assert IR, not source comments). → + **fix**, folded into the same tidy (doc-honesty hygiene; the IR + pins are the guard that generated code stays byte-frozen). + +(Boss already caught + fixed in-line one sibling stale `//` +gate-comment block at `check/lib.rs:1917-1922` during the DONE +inspect; the architect found no further siblings.) + +## Step 2 — Bench-regression trio + +| script | exit | summary | +|---|---|---| +| `bench/check.py` | **1** | 63 metrics; 3 regressed, 2 improved, 58 stable | +| `bench/compile_check.py` | 0 | 24 metrics; 0 regressed, 24 stable | +| `bench/cross_lang.py` | 0 | 25 metrics; 0 regressed, 25 stable (every `rc_over_c` within tol) | + +`check.py` exit 1 — the 3 firings: + +| metric | baseline | actual | diff | tol | +|---|---|---|---|---| +| `throughput.bench_list_sum.bump_s` | 0.046 | 0.052 | **+12.62%** | 10.0% | +| `latency.implicit_at_rc.p99_9_us` | 452.0 | 580.6 | **+28.45%** | 25.0% | +| `latency.implicit_at_rc.max_us` | 477.3 | 645.2 | **+35.18%** | 30.0% | + +Both are the two **standing tracked P2 noise families** (roadmap +P2): the `*.bump_s` stale-baseline (~+5–13% environmental band on +current hardware) and the `*.max_us`/`p99_9` `-n 5` tail-jitter +structural false-positive (signature: same benchmark's `median_us` ++5.11% ok, `p99_us` +15.08% ok — only the extreme tail quantiles +fire, the worst-of-~5000-samples-over-5-runs pattern). + +**Causal exoneration (decisive, not hand-waved — M2-audit method).** +M3 changed *no* executable-path codegen (architect-confirmed: M2 +forwarder body byte-unchanged; the only codegen touches are the +`llvm_scalar` record→ptr arm — reachable solely for an `(export)` +single-ctor record, and no `bench_*` program has an `(export)` — the +`ailang-check` `is_c_abi_type` widen, and lockstep *comments*). Built +`ail` at HEAD and at the pre-M3 commit `9a609ae` in an isolated +worktree; the **generated IR is byte-identical** (`cmp -s`) for every +firing benchmark and its neighbours: + +``` +bench_list_sum: IR BYTE-IDENTICAL (HEAD == 9a609ae) +bench_list_sum_explicit: IR BYTE-IDENTICAL +bench_latency_implicit: IR BYTE-IDENTICAL +bench_tree_walk: IR BYTE-IDENTICAL +``` + +The IR is what is handed to `clang -O2` (deterministic), so the +bench binaries are byte-identical and M3 causation is logically +impossible. **NO baseline ratify** (these are not M3 artefacts; the +two P2 items stay separately tracked). Bench → **carry-on**. + +## Step 3 — Classification + +| item | class | recommendation | +|---|---|---| +| `[medium]` DESIGN.md:2299-2302 scalar-only-rule contradiction | drift | **fix** — docs-honesty tidy | +| `[low]` codegen forwarder-comment Int/Float-only staleness | drift | **fix** — folded into the same tidy | +| `check.py` exit 1 (3 firings) | tracked-noise | **carry-on**, NO ratify (byte-identical-IR causal exoneration) | +| compile_check / cross_lang | clean | carry-on | + +## Step 4 — Resolution (Boss) + +- **Drift → one docs-honesty tidy iteration `embedding-abi-m3.tidy`** + (the M2-audit `[medium]+[low] doc-honesty → tidy` precedent + shape): reconcile the stale DESIGN.md:2299-2302 "scalar-only rule + above forbids" paragraph against the frozen SSOT + the own/borrow + mode contract, **pin-safe** (the `docs_honesty_pin.rs:135` pinned + sentence — "Export parameters are written **bare**…", shifted to + ~`:2299` by the M3.1 DONE — sits in/adjacent to the edit zone; + the tidy plan must keep it byte-verbatim+contiguous, planner + Step-5 item-6 / M2.tidy precedent); plus the `[low]` codegen + forwarder-comment honesty fix (comment-only, the byte-pin + + forwarder-IR pin stay green as the guard that generated code is + untouched). Routed via `planner` → `implement`. +- **Bench → carry-on, NO ratify.** Causally exonerated; the two + tracked P2 noise todos stay as-is. + +Milestone is substantively closed + sound (record crosses the C ABI +in/out, ownership follows the declared mode, the value layout is +frozen + byte-pin-enforced, all contract invariants held, +Invariant 1 clean). The roadmap M3 `[~]`→`[x]` follows the tidy +landing clean. diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index 07b2b5c..85b313b 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -102,3 +102,4 @@ - 2026-05-18 — audit embedding-abi-m2 (milestone close — DRIFT: one [medium]+[low] doc-honesty item → tidy; bench exit 1 causally exonerated, NO ratify): architect `drift_found` — no DESIGN.md/spec-contract drift, Invariant 1 intact, internal-convention byte-invariant, Decision-10 atomicity note present-tense-correct (sanitiser-verified), lockstep complete, docs_honesty_pin green, no unrequested extras, Boss spec-defect repair correctly reflected; the ONE actionable item is `[medium]` DESIGN.md:2266 — section header still `## Embedding ABI (M1)` while the body now mirrors the post-M2 ctx ABI present-tense (current-state-mirror honesty mismatch; NOT a Sweep-5 catch — header/body desync only a read finds; iter-journal Known-debt flagged it truthfully, Task-7-scope-deferred to preserve the docs_honesty_pin:135 verbatim sentence) + coupled `[low]` DESIGN.md:2354 stale `see §"Embedding ABI (M1)"` xref. Bench: `check.py` exit 1 (3 regressed: bench_list_sum.bump_s +13.57%, latency.explicit_at_rc.max_us +81.96%, latency.implicit_at_rc.max_us +38.57%), compile_check/cross_lang exit 0 clean (every rc_over_c ratio within tol). M2 genuinely changed the benched runtime path (rc.c null-ctx-fallback branch), so byte-identical exoneration did NOT apply → `ailang-bencher` dispatched: swapped only rc.c pre-M2↔HEAD, disassembled the delta (3 branchless insns mov %fs/test/cmovne), interleaved core-pinned A/B — **H0 refuted, all 3 firings tracked-noise causally-exonerated**: bump_s causally impossible from M2 (bump_malloc 0 rc-counter refs; reproduces ~+12% on M2-inert code = P2 *.bump_s stale-baseline), the rc.c hunk compiled branchless + measured free (HEAD −0.63% median), max_us median/p99 flat across rc.c variants + non-reproducible within a fixed binary (3.2× spread) = P2 *.max_us -n5 structural false-positive (4th consecutive null-attributable firing). NO baseline ratified (not M2 artefacts; P2 items stay separately tracked). Resolution: `[medium]`+`[low]` → tidy iter embedding-abi-m2.tidy (header rename + :2354 xref + docs_honesty_pin.rs:134–136 (M1)-token lockstep; the pinned :135 substring stays verbatim); bench → carry-on. Milestone substantively closed + sound (capability sanitiser-verified, all contract invariants held); roadmap [~]→[x] follows the tidy landing clean. → 2026-05-18-audit-embedding-abi-m2.md - 2026-05-18 — iter embedding-abi-m2.tidy (M2 audit `[medium]`+`[low]` doc-honesty fix, DONE 1/1, zero re-loops): lockstep-renamed the DESIGN.md section `## Embedding ABI (M1)` → `## Embedding ABI` (current-state-mirror — the body had described the post-M2 ctx ABI present-tense while the header still carried the milestone tag) across all 5 live-coupling sites: `docs/DESIGN.md:2266` (header) + `:2354` (schema-block `see §"Embedding ABI"` xref), `crates/ailang-core/tests/docs_honesty_pin.rs:134` (comment) + `:136` (assert-message), and the Boss-added 5th site `crates/ailang-core/specs/form_a.md:89` (a live forward-xref into the renamed section in the compiled-in `FORM_A_SPEC` — same dangling-xref class as :2354, surfaced by the plan-recon-undercount countermeasure, NOT in the architect's named 3-site scope; Boss folded it in on the merits because leaving it stale is a half-rename contradicting the tidy's own thesis). The `docs_honesty_pin.rs:135` asserted substring (the DESIGN.md body sentence "Export parameters are written **bare**…", 31 lines below the header, section-name-free, file-wide `d.contains`) is rename-immune and stayed byte-verbatim untouched — recon proved this definitively pre-plan; the diff confirms :135 is unchanged context between the :134/:136 hunks. Committed append-only history (journals/specs/plans/orchestrator-stats) NOT falsified — Boss-verified the diff footprint is exactly the 3 content files + journal + stats, zero history files. Pure docs/test-string tidy, zero language/checker/codegen/schema change; no audit/fieldtest gate (the docs_honesty_pin IS the regression guard — Boss-verified 5/0 before AND after, design_schema_drift 8/0, the :2354 edit moved no JSON-schema drift anchor). Recon also corrected an audit inaccuracy (the :2354 xref IS inside the `## Data model` window :2319–2558, not outside — non-blocking, the xref string is not a drift anchor). audit source `docs/journals/2026-05-18-audit-embedding-abi-m2.md` (`ad88dec`) → plan `docs/plans/embedding-abi-m2.tidy.md` (`d1241b1`) → iter this commit. → 2026-05-18-iter-embedding-abi-m2.tidy.md - 2026-05-18 — iter embedding-abi-m3.1 (Embedding ABI — M3, DONE 7/7 across one Boss-repaired split dispatch): freeze the value layout + a single-constructor record of `Int`/`Float` fields crosses the C ABI in and out, ownership following the declared `own`/`borrow` mode. No authoring-surface / schema / Form-A / `CheckError` change (M2-style — the `.ail` is the minimal evolution of the M1/M2 scalar kernel into a record `State`, existing `data`+`(own (con T))`+`(export …)`). Shipped: the export-gate scalar predicate `is_c_scalar` widened to a two-level `is_c_abi_type` (a bare `Int`/`Float`, OR a `Type::Con` resolving via the in-scope `env.types` to a single-constructor `data` whose every field is a bare `Int`/`Float` — NOT deep: a record-typed field stays rejected = M4; multi-ctor sums / `Str` / `List` / effectful stay RED; the M1 `embed_export_adt_ret_rejected.ail` must-fail RE-POINTED from the now-M3-valid single-ctor `Pair` to a genuinely-still-rejected multi-ctor+`Str` `Reading`, the pin's meaning sharpened not silently inverted; gate suite 10/10); codegen `llvm_scalar` maps a gate-guaranteed record `Type::Con` → `ptr` (the M2 `Target::StaticLib` forwarder body BYTE-UNCHANGED — a record crosses as a bare `ptr`, no `sret`/`byval`; all mode-driven RC stays in the byte-unchanged internal `@ail__`; 3/3 staticlib-lowering pins, no `fn_scalar_sig` signature change so no caller ripple); the record memory layout FROZEN as a one-way commitment — DESIGN.md §"Embedding ABI" gains a `### Frozen value layout (M3 — one-way commitment)` SSOT subsection (header@p-8 / i64 tag@0 / fields i64-strided@8+i*8 / size=8+n*8 / `ailang_rc_alloc` construction MUST / `ailang_rc_dec` host-free leak-free because scalar-field / ownership follows the declared mode), the two "provisional until M3" sentences rewritten to one-way-freeze wording, lockstep `// FROZEN ABI` pointers added at the three independent encoders (`runtime/rc.c`, `match_lower.rs` `lower_ctor`, `drop.rs`), 3 stale rustdocs fixed (`codegen/lib.rs`, `core/ast.rs`, the Concerns-carry `check/lib.rs:448-450` variant doc) + the Boss-caught stale `//` gate-comment block (`check/lib.rs:1917-1922`, "M1/scalar-only" → "M1/M2/M3 / C-ABI-permitted incl. single-ctor record"); a new `@ailang_rc_alloc` heap-box byte-pin (`embed_record_layout_pin.rs`) proven RED-on-offset-perturbation / GREEN-on-restore (the freeze made enforceable, not aspirational); the `(State,Float)->State` record fold E2E round-trip proven globally leak-free for BOTH `own` and `borrow`. Process note: the first dispatch (Tasks 1–4 clean) correctly BLOCKED on Task 5 having surfaced a genuine spec defect — the spec's proof instrument asserted the single `ailang_ctx_free` ctx readback shows `allocs==frees`, structurally unsatisfiable for `borrow` (and only coincidentally passing for `own`) because M2's `__ail_tls_ctx` is bound only for the synchronous forwarder call, so host-side `ailang_rc_dec`s land on `g_rc_*` not ctx. Boss adjudication (M2.1-precedent class — genuine spec defect, deliverable+invariant sound, only verification mechanics mis-specified, first BLOCKED task not 2+-in-family ⇒ consistency-repair not a brainstorm bounce): Boss independently rebuilt+ran both modes and confirmed globally leak-free + value-correct (own ctx live=0/g_rc live=0; borrow ctx live=+N/g_rc live=−N, Σlive=0; exit 0 both); spec amended (dated repair note + §"Testing strategy" 3/4 + §"Coherent stop" → global-leak-freedom proof model, the M2-TLS cross-attribution documented as correct behaviour) + plan amended (harness sums ALL `ailang_rc_stats:` lines) + the mechanical code repair applied; partial committed `d5c565d` (PARTIAL 5/7 + Boss spec-defect repair); re-dispatch `task_range:[6,7]` DONE. No fresh grounding-check (the repair removes an over-strong measurement assumption, adds none about compiler behaviour). Independent Boss verification: workspace 639/0, `embed_record_e2e` 2/2 (own+borrow global model), byte-pin 1/1, gate 10/10, forwarder 3/3, `docs_honesty_pin` 5/5 pin-safe (the freeze rewrite kept the pinned "Export parameters are written **bare**…" sentence byte-verbatim+contiguous, shifted :2297→:2299, content-asserted), `design_schema_drift`/`embed_export_hash_stable`/`embed_e2e`/M2 swarm regression-green-unmodified. spec `docs/specs/2026-05-18-embedding-abi-m3.md` (user-approved, grounding-check PASS 8/8, `1fbb9c4`) → plan `docs/plans/embedding-abi-m3.1.md` (`15ee3c5`, Boss-amended) → iter `d5c565d` (PARTIAL 5/7 + Boss repair) + this commit (DONE 6–7). Milestone-close `audit` next (architect Invariant 1 + bench trio — spec Testing items 8/9, explicitly NOT the implement run's job). → 2026-05-18-iter-embedding-abi-m3.1.md +- 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