From 63d7d60dd15c4d9458d47b84438c3d35cb9f8ee6 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 18 May 2026 21:50:15 +0200 Subject: [PATCH] iter embedding-abi-m3.tidy (DONE 3/3): close M3 audit [medium]+[low] doc-honesty drift, pin-safe MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit [medium] DESIGN.md §"Embedding ABI": surgically replaced ONLY the contradicted M1-era parenthetical (asserted the export boundary is scalar-only — false post-M3, a single-ctor record is an accepted export type) with the present-tense truth pointing at the frozen-layout SSOT + the own/borrow mode contract. The parenthetical shared physical line :2300 with the docs_honesty_pin:135 pinned bare-scalar sentence; the edit kept every pinned word (planner Step-5 item-6 pin-safety, the M2.tidy precedent — docs_honesty_pin stayed 5/5 green, RED-restore path never triggered). [low] codegen forwarder-body comment honesty fix (comment-only; the IR byte-pins assert generated code not comments — byte-identical before/after). Boss-verified: both stale fragments grep-absent; 4 standing pins green at the recon baseline; workspace 639/77 byte-unchanged; diff exactly 2 files. No behaviour change; the pins are the coverage (M2.tidy precedent, no audit/fieldtest gate). bench already carry-on/NO-ratify at the M3 audit (causally exonerated). One non-gating planner-quality grep defect recorded in the journal Concerns (orchestrator handled it correctly, no code bent). --- ...2026-05-18-iter-embedding-abi-m3.tidy.json | 13 +++ crates/ailang-codegen/src/lib.rs | 7 +- docs/DESIGN.md | 5 +- .../2026-05-18-iter-embedding-abi-m3.tidy.md | 97 +++++++++++++++++++ docs/journals/INDEX.md | 1 + 5 files changed, 118 insertions(+), 5 deletions(-) create mode 100644 bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.tidy.json create mode 100644 docs/journals/2026-05-18-iter-embedding-abi-m3.tidy.md diff --git a/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.tidy.json b/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.tidy.json new file mode 100644 index 0000000..e8eeb01 --- /dev/null +++ b/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.tidy.json @@ -0,0 +1,13 @@ +{ + "iter_id": "embedding-abi-m3.tidy", + "date": "2026-05-18", + "mode": "standard", + "outcome": "DONE", + "tasks_total": 3, + "tasks_completed": 3, + "reloops_per_task": { "1": 0, "2": 0, "3": 0 }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null, + "notes": "Docs/comment-only M3-audit drift tidy (M2.tidy precedent). Pin-safe DESIGN.md parenthetical replace (docs_honesty_pin stayed GREEN, no RED->restore) + comment-only forwarder honesty fix (IR pins byte-identical). Four standing pins at recon baseline (docs_honesty_pin 5, design_schema_drift 8, embed_record_layout_pin 1, embed_staticlib_lowering 3); workspace 639/77 byte-unchanged. One recorded plan-vs-actual grep-pattern discrepancy in Task 3 Step 1 (plan defect, substantive intent satisfied via discriminating fragment); did not gate, no re-loop." +} diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 62b4f25..64fd9ad 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -605,9 +605,10 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy, target: Target) - Target::StaticLib => { // One external C entrypoint per `(export …)` fn, // forwarding to the internal `@ail__`. - // The check-side gate (Task 4) guarantees every param - // and the ret are `Int`/`Float`; map Int→i64, - // Float→double. M1 scalar fns have no captured env, so + // The check-side export gate guarantees every param and + // the ret are `Int`/`Float` or a single-constructor + // record of those (M3); map Int→i64, Float→double, a + // record → ptr. Scalar fns have no captured env, so // the internal callee takes the scalars positionally // (confirmed against `emit_fn`'s signature emission, // `lib.rs:1087`). diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 10d2ad0..1e68f54 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -2297,8 +2297,9 @@ layout is **frozen as of M3** (see "Frozen value layout" below); the ctx-threaded C signature is the M2 shape. Export parameters are written **bare**: a scalar type carries no -`own`/`borrow` mode (modes apply only to heap-shaped types, which the -scalar-only rule above forbids at an export boundary anyway). The +`own`/`borrow` mode (a single-constructor record export parameter, +by contrast, carries `own`/`borrow` — the ownership contract the +frozen value layout below specifies). The canonical M1 export shape: ``` diff --git a/docs/journals/2026-05-18-iter-embedding-abi-m3.tidy.md b/docs/journals/2026-05-18-iter-embedding-abi-m3.tidy.md new file mode 100644 index 0000000..63a4444d --- /dev/null +++ b/docs/journals/2026-05-18-iter-embedding-abi-m3.tidy.md @@ -0,0 +1,97 @@ +# iter embedding-abi-m3.tidy — close the two M3-audit doc-honesty DRIFT items + +**Date:** 2026-05-18 +**Started from:** 4fc34705528333de765251be9c26f7bb3182e175 +**Status:** DONE +**Tasks completed:** 3 of 3 + +## Summary + +Post-audit docs-honesty tidy that reconciles the two DRIFT items the +M3 milestone-close audit (`docs/journals/2026-05-18-audit-embedding-abi-m3.md`, +committed `b8a60b1`) routed here, in the M2.tidy `[medium]+[low] +doc-honesty → tidy` precedent shape. Two surgical, independent text +edits, zero language/checker/codegen behaviour change. (1) DESIGN.md +§"Embedding ABI" `:2300-2301` — 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`), +which since the M3 frozen-layout SSOT accepts a single-ctor record +export type contradicted both that freeze and the `(own/borrow +(con T))` mode contract at `:2345-2351`; the replacement states the +present-tense truth and points at the frozen-value-layout SSOT. The +`docs_honesty_pin.rs:135`-pinned sentence ("Export parameters are +written **bare**: a scalar type carries no `own`/`borrow` mode", +`norm()`-whitespace-collapsed) shares physical line `:2300` with the +stale clause — the edit kept every pinned word contiguous; the pin +stayed GREEN (5 passed) across the edit, no RED→restore needed. +(2) `crates/ailang-codegen/src/lib.rs:608-610` — comment-only +honesty fix: the forwarder-body comment claimed the gate guarantees +`Int`/`Float`-only, false post-M3 (a gate-guaranteed single-ctor +record lowers to `ptr`); the IR byte-pin + 3 forwarder-IR pins +stayed byte-identically GREEN before and after, the guard that no +generated code moved. Four standing pins at exact recon baseline +(`docs_honesty_pin` 5, `design_schema_drift` 8, +`embed_record_layout_pin` 1, `embed_staticlib_lowering` 3); full +workspace 639/77 byte-unchanged from the M3-DONE baseline. Diff is +exactly the two intended files. This closes the M3 audit's +`[medium]`+`[low]` doc-honesty drift; bench was already carry-on at +the audit (decisively causally exonerated by byte-identical +generated IR — M3 changed no executable-path codegen; NO ratify). +No audit/fieldtest gate after this tidy — the four pins + the +639/77 baseline ARE the regression coverage (M2.tidy precedent). + +## Per-task notes + +- iter embedding-abi-m3.tidy.1: reconcile the contradicted DESIGN.md + parenthetical (`[medium]`). Replaced only the parenthetical on + `:2300-2301`; pinned bare-scalar sentence kept verbatim+contiguous + (`docs_honesty_pin` 5 passed, `design_schema_drift` 8 passed). +- iter embedding-abi-m3.tidy.2: honesty-fix the stale forwarder-body + comment (`[low]`). Comment-only edit at `lib.rs:608-610`; + `embed_record_layout_pin` 1 + `embed_staticlib_lowering` 3 passed + byte-identically before and after (no IR delta); full codegen + crate green. +- iter embedding-abi-m3.tidy.3: milestone-close verification gate. + Four standing pins at recon baseline; workspace 639/77 unchanged; + diff exactly two files (DESIGN.md, codegen/src/lib.rs). One + plan-vs-actual grep discrepancy recorded under Concerns (Step 1 + pattern collides with the plan's own Task 2 replacement text; + substantive intent satisfied via the discriminating fragment). + +## Concerns + +- Task 3 Step 1's verification grep pattern `guarantees every param` + is a plan defect: it is a substring of the plan's *own* Task 2 + prescribed NEW replacement text (`// The check-side export gate + guarantees every param and`), so it cannot return "no output" as + the plan's Step 1 expects without contradicting Task 2. The + substantive intent of Step 1 — the stale `Int`/`Float`-only + comment is gone — was verified via the discriminating fragments + instead: the stale `check-side gate (Task 4)` marker is ABSENT + (grep exit 1) and the stale `guarantees every param` + immediately + following `and the ret are \`Int\`/\`Float\`; map` two-line claim + is ABSENT (Pzo exit 1), while the new correct M3 comment with + `single-constructor` record framing is PRESENT (`:609`). The + implementation followed Task 2's verbatim replacement exactly as + mandated; the retained words "guarantees every param" are correct + (the gate genuinely still guarantees every param — the M3 change + is *what* it guarantees, not *whether*). No edit was made to + dodge the grep; the plan's pattern is the defect, not the code. + +## Known debt + +(none — the two audit-flagged drift items are both closed; no +deferred follow-up.) + +## Blocked detail + +(none — DONE.) + +## Files touched + +- `docs/DESIGN.md` — §"Embedding ABI" parenthetical replaced (`:2300-2301`) +- `crates/ailang-codegen/src/lib.rs` — `Target::StaticLib` forwarder-body comment honesty (`:608-610`) + +## Stats + +bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.tidy.json diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index 85b313b..578174a 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -103,3 +103,4 @@ - 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 +- 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