audit embedding-abi-m2: milestone close — DRIFT (1 [medium]+[low] doc-honesty -> tidy); bench exit 1 causally exonerated, NO ratify
Architect drift_found: the only actionable item is the stale '## Embedding ABI (M1)' DESIGN.md header (:2266) vs its now-M2 body + coupled :2354 xref — a current-state-mirror honesty desync the iter journal flagged truthfully (Task-7-scope-deferred to preserve the docs_honesty_pin:135 verbatim sentence). Everything substantive holds (Invariant 1, internal-convention byte-invariance, Decision-10 note present-tense-correct, lockstep, no unrequested extras). Bench check.py exit 1 (bump_s + 2x rc-latency max_us). M2 changed the benched runtime path so byte-identical exoneration did not apply -> ailang-bencher localised: H0 refuted, all 3 firings are the two tracked roadmap-P2 noise families (bump_s causally impossible from M2's diff; rc.c hunk branchless+free; max_us median/p99 flat + non-reproducible). NO baseline ratified; not M2 artefacts. Resolution: doc-honesty drift -> tidy iter embedding-abi-m2.tidy; bench -> carry-on. Roadmap [~]->[x] after the tidy lands clean.
This commit is contained in:
@@ -0,0 +1,106 @@
|
||||
# Audit — Embedding ABI — M2 (milestone close)
|
||||
|
||||
**Date:** 2026-05-18
|
||||
**Scope:** `2db737c..fbeeade` (M2 = spec `1c58055` → plan `b3388c8` →
|
||||
iter `c9a84b3` PARTIAL 4/9 + Boss spec-defect repair → iter `fbeeade`
|
||||
DONE 5–9). HEAD `fbeeade`, working tree clean at audit time.
|
||||
**Outcome:** DRIFT (one `[medium]` + coupled `[low]` doc-honesty
|
||||
item → fix via tidy iteration). Bench `check.py` exit 1 — **all
|
||||
firings causally exonerated as the two tracked roadmap-P2 noise
|
||||
families; NO baseline ratified, NOT an M2 regression.**
|
||||
|
||||
## Step 1 — Architect drift review
|
||||
|
||||
Status: `drift_found`. No DESIGN.md/spec-contract drift, no
|
||||
unrequested extras, Invariant 1 intact, internal-convention
|
||||
byte-invariance held, Decision-10 atomicity note present-tense-
|
||||
correct (sanitiser-verified this iter), spec→DESIGN.md→code lockstep
|
||||
complete, `docs_honesty_pin.rs` green unmodified, the Boss
|
||||
spec-defect repair correctly reflected in both spec and shipped
|
||||
tests.
|
||||
|
||||
Actionable drift (one item, two coupled sites):
|
||||
|
||||
- **`[medium]` `docs/DESIGN.md:2266`** — the section header reads
|
||||
`## Embedding ABI (M1)` while the body (`:2285–2295`) now
|
||||
describes the post-M2 ctx ABI as present-tense current state
|
||||
("Every exported entrypoint takes a mandatory leading
|
||||
`ailang_ctx_t*` (M2)… the ctx-threaded C signature is the M2
|
||||
shape"). Current-state-mirror honesty mismatch: a header that
|
||||
misdescribes its own present-tense body. Not a Sweep-5 catch (the
|
||||
body prose itself is correctly present-tense — the
|
||||
docs-honesty-lint machinery does not auto-flag a header/body
|
||||
desync; only a read catches it). The iter journal's Concerns +
|
||||
Known-debt flagged it accurately and truthfully — Task 7's edit
|
||||
regions were *deliberately* scope-limited (provisional-until-M3
|
||||
sentence + Decision 10) to preserve the `docs_honesty_pin.rs:135`
|
||||
verbatim "Export parameters are written **bare**…" assertion 12
|
||||
lines below the header. Deferral reasoning sound; the mismatch is
|
||||
real drift that must not persist past this milestone close.
|
||||
- **`[low]` `docs/DESIGN.md:2354`** — schema-block cross-reference
|
||||
comment still reads `see §"Embedding ABI (M1)"`; stale xref
|
||||
coupled to the header above. Must move in lockstep with any
|
||||
header rename so the fix is scoped header + xref +
|
||||
`docs_honesty_pin.rs:134–136` `(M1)`-token audit together, not
|
||||
the header alone.
|
||||
|
||||
Architect recommendation: one scoped tidy iteration.
|
||||
|
||||
## Step 2 — Bench regression
|
||||
|
||||
| Script | Exit |
|
||||
|---|---|
|
||||
| `bench/check.py` | **1** |
|
||||
| `bench/compile_check.py` | 0 (clean — 24/24 stable) |
|
||||
| `bench/cross_lang.py` | 0 (clean — 25/25 stable, **every `rc_over_c` ratio within tol**) |
|
||||
|
||||
`check.py` 63 metrics: 3 regressed, 2 improved-beyond-tol, 58 stable.
|
||||
The 3 firings (verbatim): `throughput.bench_list_sum.bump_s`
|
||||
0.046→0.052 +13.57% (tol 10%); `latency.explicit_at_rc.max_us`
|
||||
413.0→751.5 +81.96% (tol 25%); `latency.implicit_at_rc.max_us`
|
||||
477.3→661.4 +38.57% (tol 30%). Every `*.rc_s`/`*.gc_s` throughput and
|
||||
every rc-latency median/p99/p99.9 stable within tol.
|
||||
|
||||
Because M2 genuinely changed the benched runtime path
|
||||
(`runtime/rc.c`: the two RC-counter sites gained a `__thread` load +
|
||||
null-branch ahead of `g_rc_*++`), the byte-identical exoneration
|
||||
method did **not** apply — `ailang-bencher` was dispatched for
|
||||
hypothesis-driven localisation (H0 = real M2 regression; H1 =
|
||||
tracked-P2 noise, M2 bench-neutral).
|
||||
|
||||
**Bencher verdict: H0 refuted; all three firings
|
||||
tracked-noise-causally-exonerated.** Method: swapped *only* `rc.c`
|
||||
between `2db737c` and `fbeeade` (same `ail` binary, same fixtures),
|
||||
disassembled the delta, interleaved core-pinned A/B.
|
||||
- `bump_s`: causally **impossible** from M2 — `bump_malloc`
|
||||
disassembly has 0 refs to `__ail_tls_ctx`/rc counters; the
|
||||
M2-inert bump binary independently reproduces ~+12% vs the stale
|
||||
0.046 baseline. Roadmap-P2 `*.bump_s` environmental staleness.
|
||||
- M2's rc.c hunk compiled **branchless** (3 insns: `mov %fs`,
|
||||
`test`, `cmovne`) and measured **free** (HEAD median −0.63% vs
|
||||
pre-M2, inside intra-arm spread) — the H0 mechanism does not
|
||||
exist; no per-alloc cost.
|
||||
- `*.max_us`: median/p99 flat across rc.c variants (a systematic
|
||||
per-alloc cost must move them and does not); max_us
|
||||
non-reproducible within a single fixed binary (3.2× spread).
|
||||
Roadmap-P2 `*.max_us` `-n 5` structural false-positive (now its
|
||||
4th consecutive no-runtime-change-attributable firing).
|
||||
|
||||
Limitations (bencher-stated): single host; N=15 moderate for
|
||||
max-tail — median/p99 verdict solid, max verdict rests on the
|
||||
(strong, N-bounded) non-reproducibility argument; gc latency arm not
|
||||
re-measured (no gc firing; rc/gc share the identical M2 hunk).
|
||||
|
||||
## Step 3 — Classification & resolution
|
||||
|
||||
| Item | Class | Resolution |
|
||||
|---|---|---|
|
||||
| `[medium]` DESIGN.md:2266 stale `(M1)` header + `[low]` :2354 xref | **fix** | one tidy iteration `embedding-abi-m2.tidy`: rename the `## Embedding ABI (M1)` header to drop the milestone tag (current-state-mirror), lockstep the `:2354` cross-reference and the `docs_honesty_pin.rs:134–136` comment/assert-message `(M1)` token — the pinned *substring* (`:135`, the "Export parameters are written **bare**…" sentence) stays verbatim untouched. planner → implement. |
|
||||
| `check.py` exit 1 — 3 firings | **carry-on** | causally exonerated as the two pre-existing roadmap-P2 noise families (`*.bump_s` staleness; `*.max_us` `-n 5` false-positive). **No baseline ratified** (bencher wrote nothing to baseline; these are not M2 artefacts). The P2 items remain tracked on the roadmap; retiring the `bump_s` stale baseline is a separate roadmap-P2 action against that item, explicitly NOT this milestone. |
|
||||
| `compile_check.py` / `cross_lang.py` | carry-on | clean (exit 0). |
|
||||
|
||||
**Milestone M2 is substantively closed and sound** (capability
|
||||
sanitiser-verified, all contract invariants held). The one open
|
||||
drift is a doc-honesty header desync, fixed by the tidy iteration
|
||||
dispatched next; the roadmap `[~]`→`[x]` flip follows the tidy
|
||||
landing clean. No ratify. No re-audit deferral.
|
||||
@@ -99,3 +99,4 @@
|
||||
- 2026-05-18 — iter form-a-scalar-param-mode-carveout (M1-fieldtest follow-up #1, docs-honesty tidy in the docs-honesty-lint class, DONE): resolved the M1 fieldtest `[friction]` + `[spec_gap]#1` shared root. `crates/ailang-core/specs/form_a.md` stated an *unconditional* "every `(fn ...)` param MUST carry an `(own/borrow)` mode" rule in four places (`### Function` prose L97, grammar-block comment L230, "Schema invariants" item 1 L347, Pitfalls bullet L382) that contradicts shipped checker behaviour — scalar `Int`/`Bool`/`Unit`/`Str` params take **and require** bare `(con Int)` (a mode on a scalar makes the linearity pass hold the primitive to linear discipline → body-pointing `use-after-consume`/`consume-while-borrowed`, the exact fieldtest misdirection). All four sites rewritten symmetric to the pre-existing return-type carve-out; site 5 (L521 few-shot annotation) already correct, left verbatim by design (carve-out reuses its heap-shaped/primitive vocabulary for end-to-end internal consistency). `docs/DESIGN.md` §"Embedding ABI (M1)" gained the bare-scalar export-param rule + a corpus-grounded `step` Form-A snippet (byte-identical to `examples/embed_backtest_step.ail:3-11`). RED-first anti-regrowth pin `form_a_scalar_param_carveout_present_and_old_rule_absent` in `crates/ailang-core/tests/docs_honesty_pin.rs` (reads the canonical `ailang_core::FORM_A_SPEC` `include_str!` const — single-source, compile-checked — + `read("docs/DESIGN.md")`; `norm()` whitespace-collapse structurally discharges the grep/contains line-wrap family; 4 ABSENT + 4 PRESENT form_a + 1 PRESENT DESIGN). Boss scope calls: 4 form_a sites not 2 (internal-consistency, on the merits — a tidy whose thesis is "consistent current-state mirror" cannot fix some and leave others contradicting); pin idiom = `FORM_A_SPEC` const (semantic single-source, not effort). `spec_drift.rs` recon-confirmed NOT a lockstep partner (anchors are short keyword tokens; `(own`/`(borrow` survive an additive carve-out). Zero language/checker/codegen change by construction; independent Boss verification: docs_honesty_pin 5/0, spec_drift 8/8, ailang-core 112/0, workspace 622→623 (+1 = the pin), zero `crates/**/src/**` diff. spec carrier `docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md` + roadmap P1 entry → plan `docs/plans/form-a-scalar-param-mode-carveout.md` (`4c266a6`). Pure docs+pin tidy — no audit/fieldtest gate (zero authoring-behaviour change; the pin IS the regression coverage). → 2026-05-18-iter-form-a-scalar-param-mode-carveout.md
|
||||
- 2026-05-18 — iter emit-ir-staticlib (M1-fieldtest follow-up #2, scoped [feature], DONE): resolved M1 fieldtest [spec_gap]#2 — `ail emit-ir` had no `--emit=staticlib` (only `ail build` did) and on a `main`-free kernel hit the executable-path `MissingEntryMain` rejection, so an author could not read the generated `@<sym>` forwarder for an exported kernel — the exact Decision-5 IR-readability affordance, for the exact artefact M1 introduced. Added a one-line symmetric codegen convenience `lower_workspace_staticlib(ws)` (mirrors `lower_workspace`: `--emit=exe`↔`lower_workspace`, `--emit=staticlib`↔`lower_workspace_staticlib`; delegates to the M1-audited unchanged `Target::StaticLib` forwarder path), an `emit: String` clap field on `Cmd::EmitIr` symmetric with `Cmd::Build`'s, and a zero-export guard byte-identical to `build_staticlib`'s (so the error is symmetric across both subcommands and the existing `embed_staticlib_cli.rs` substring assertion holds for both). Recon resolved the only integration risk negative (both codegen entrypoints return `Result<String>`, the emit-ir printer already consumes `String` — no adapter). DESIGN.md *widened* not narrowed (roadmap resolution honoured): a present-tense affordance sentence in §"Embedding ABI (M1)" + a CLI-synopsis correction that also discharges a pre-existing M1 omission (`ail build --emit=staticlib` was never in the synopsis). Boss editorial calls: synopsis fixes BOTH lines (docs-as-current-state-mirror consistency, on the merits); NO new docs pin (the E2E pins behaviour; the architect's mandatory DESIGN.md read at milestone close catches stale prose — pinning every feature sentence is noise); Decision-5 prose left untouched (already present-tense correct). New E2E `crates/ail/tests/emit_ir_staticlib_cli.rs` (3 tests: positive — IR contains external `@backtest_step(` + internal `@ail_embed_backtest_step_step`, NOT `@main(`, NOT `has no main def`; zero-export guard symmetric with build's, reusing the identical `embed_noentry_baseline.ail` fixture; default-exe regression — `--emit` defaults to `exe`, a `main`-free kernel without the flag still hits `MissingEntryMain`, so the new branch cannot silently reroute the default path). RED-first observed exactly ("1 passed; 2 failed" pre-edit — the default-exe test passes because that IS the spec_gap behaviour). Independent Boss verification: the 3 new tests 3/0, `embed_staticlib_cli` 2/0 (build-side untouched), `docs_honesty_pin` 5/0 (no regression), `ail` suite 186/0, workspace 623→626 (+3 = exactly the new tests), zero diff outside the 4 in-scope paths, no fixture minted. Functional spot-check from the user-facing CLI: `ail emit-ir examples/embed_backtest_step.ail --emit=staticlib` emits `define i64 @backtest_step(...)` (the readable external forwarder) + `@ail_embed_backtest_step_step` (internal), no `@main` — the affordance is genuinely delivered. spec carrier `docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md` [spec_gap]#2 + roadmap P1 entry → plan `docs/plans/emit-ir-staticlib.md` (`03493c9`) → iter this commit. Scoped feature, no audit/fieldtest gate (the E2E is the coverage; no authoring-surface or invariant change — reuses the M1-audited codegen path). → 2026-05-18-iter-emit-ir-staticlib.md
|
||||
- 2026-05-18 — iter embedding-abi-m2.1 (Embedding ABI — M2, DONE 9/9 across one Boss-repaired split dispatch): per-thread runtime context + concurrency safety. No authoring-surface change (the `.ail` is byte-identical to M1); the deliverable is a swarm-safe generated C ABI + de-globalised runtime, sanitiser-verified. Shipped: `runtime/rc.c` gains `ailang_ctx_t {alloc_count,free_count}` + `ailang_ctx_new`/`_free` + `__thread __ail_tls_ctx`, the two increment sites become `if (_ctx) _ctx->… else g_rc_…` (the `g_rc_*` statics + `ailang_rc_stats_atexit` + constructor RETAINED VERBATIM as the null-ctx single-threaded executable fallback — `print_no_leak_pin`/`e2e` rc_stats stay green unmodified); codegen `Target::StaticLib` forwarder gains a mandatory leading `ptr %ctx` + one `@__ail_tls_ctx = external thread_local global ptr` decl + TLS save/store/restore around the BYTE-UNCHANGED internal `@ail_<mod>_<fn>` call (`_adapter`/`_clos` + internal arg vector untouched — M1 decision held; the frozen-at-M3 surface is the C `@<sym>(ctx,…)` signature, internal convention free); `build_staticlib` rejects `--alloc != rc` (RC-only swarm artefact, no shared Boehm collector by construction; default already rc; P2 Boehm-retirement untouched); DESIGN.md §"Embedding ABI (M1)" updated to post-M2 current state (provisional-until-M3 narrowed to the value/record layout; Decision-10 per-thread-ctx atomicity note) with the docs_honesty-pinned "Export parameters are written **bare**…" sentence + `(con Int)` snippet preserved verbatim; M1 `host.c`/`embed_e2e` migrated to the ctx ABI (`s==25` holds). Coherent stop sanitiser-verified by the Boss directly (not inferred): per-thread-ctx scalar swarm `-fsanitize=thread`-clean with every thread == serial oracle (capability demo); direct rc-accounting per-ctx exit 0 / 0 tsan warnings (de-globalisation positive); shared-ctx negative control a genuine `ThreadSanitizer: data race` at `rc.c:157` (`_ctx->alloc_count++` in `ailang_rc_alloc`) + `rc.c:208` (`_ctx->free_count++` in `ailang_rc_dec`), exit 66 — teeth non-vacuous, precisely targeting the de-globalised counters. Process note: the first dispatch (Tasks 1–4 clean, committed `c9a84b3` as the known-good subset) correctly BLOCKED on Task 5 having surfaced a genuine spec defect — the original Task 5 paired a `-DSHARED_CTX` negative control onto `swarm.c`, structurally impossible because a non-allocating scalar kernel writes no ctx field and `__ail_tls_ctx` is `__thread` (the spec's OWN item-1 honesty point). Boss adjudication (not a brainstorm bounce — a consistency-repair of an internally-contradictory clause whose intent is already realised by item 1): spec amended in lockstep (Goal coherent-stop, must-fail-axis item 2, Testing item 3, Acceptance) so the negative-control teeth are item-1's by the de-globalisation-proof / capability-demo split; plan Task 5 restructured (`swarm.c` per-ctx capability demo only; negative control relocated into the item-1 `rc_accounting` harness driver) + Task-3 plan-transcription error corrected (`@ail_backtest_step`→`@ail_embed_backtest_step_step`); re-dispatch `[5,9]` DONE. spec `docs/specs/2026-05-18-embedding-abi-m2.md` (user-approved, grounding-check PASS 9/9, `1c58055`) → plan `docs/plans/embedding-abi-m2.1.md` (`b3388c8`, Boss-corrected) → iter `c9a84b3` (PARTIAL 4/9 + Boss repair) + this commit (DONE 5–9). Known debt routed: DESIGN.md `## Embedding ABI (M1)` section header still says "(M1)" while the body now mirrors M2 — out of Task 7's scope-limited edit regions by design (preserve the docs_honesty_pin), a post-audit doc-honesty tidy candidate. Milestone-close `audit` next. → 2026-05-18-iter-embedding-abi-m2.1.md
|
||||
- 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
|
||||
|
||||
Reference in New Issue
Block a user