diff --git a/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json b/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json index 06d772d..3bf71cb 100644 --- a/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json +++ b/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json @@ -2,12 +2,32 @@ "iter_id": "embedding-abi-m3.1", "date": "2026-05-18", "mode": "standard", - "outcome": "PARTIAL", + "outcome": "DONE", "tasks_total": 7, - "tasks_completed": 4, - "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 1 }, + "tasks_completed": 7, + "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 1, "6": 0, "7": 0 }, "review_loops_spec": 0, "review_loops_quality": 0, - "blocked_reason": "worker-blocked", - "notes": "Tasks 1-4 DONE/GREEN (3 of them DONE_WITH_CONCERNS for plan-pseudo-code corrections: term-ctor construction, module==file-stem, module-qualified internal symbol, library-API-resolvable IO sink). Task 5 BLOCKED on a plan-assertion-model defect (ctx-readback allocs==frees structurally unsatisfiable for borrow mode given the M2 TLS-ctx accounting mechanism; no production bug, globally leak-free). Same failure class as the M2.1 swarm.c/-DSHARED_CTX Boss-adjudicated spec defect. Tasks 6-7 not attempted (Task 5 is a hard sequencing predecessor; skip-task is not a mode). The single re-loop on Task 5 was the implementer-phase context-expansion confirming the contradiction is a plan defect (no public ailang_ctx_enter API exists), not implementer-fixable within task scope. bench/architect milestone-close is audit-owned (not this run)." + "blocked_reason": null, + "dispatches": [ + { + "dispatch": 1, + "task_range": "1-7 (full)", + "outcome": "PARTIAL", + "tasks_completed": 4, + "blocked_reason": "worker-blocked", + "notes": "Tasks 1-4 DONE/GREEN (3 DONE_WITH_CONCERNS for plan-pseudo-code corrections: term-ctor construction, module==file-stem, module-qualified internal symbol, library-API-resolvable IO sink). Task 5 BLOCKED on a plan-assertion-model defect (ctx-readback allocs==frees structurally unsatisfiable for borrow mode given the M2 TLS-ctx accounting mechanism; no production bug, globally leak-free). M2.1-precedent class. Tasks 6-7 not attempted (Task 5 hard sequencing predecessor). Single Task-5 re-loop was the context-expansion confirming the contradiction is a plan defect, not implementer-fixable. Committed by the Boss as d5c565d after a spec-consistency repair (global-leak-freedom proof model) made Tasks 1-5 GREEN." + }, + { + "dispatch": 2, + "task_range": "6-7", + "outcome": "DONE", + "tasks_completed": 2, + "blocked_reason": null, + "reloops_per_task": { "6": 0, "7": 0 }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "notes": "Re-dispatched from HEAD d5c565d; Tasks 1-5 not re-implemented/re-verified. Task 6 (DESIGN.md SSOT freeze + 3 lockstep encoder comments + 3 stale-rustdoc fixes incl. the Concerns carry-forward ailang-check/lib.rs:448-450; byte-pin enforceability demo via the single legitimate git-checkout working-tree restore) and Task 7 (workspace-green gate: 639 passed 0 failed) both DONE/GREEN first-pass, zero review re-loops. docs_honesty_pin pin-safe (pinned line shifted :2297->:2299 but byte-verbatim+contiguous; pin asserts content not line). Two plan-pseudo-vs-reality observations recorded in the journal Concerns addendum: (1) Task-7 Step-1 embed_export_hash_stable is in ailang-core not ailang-check (crate-name transcription defect; substantive invariant unaffected, ran GREEN in its real crate); (2) the plan's Step-5 match_lower.rs comment + Step-7 git-checkout on the same file means the checkout reverts the uncommitted Step-5 comment, re-applied post-demo. bench/architect milestone-close remains audit-owned (not this run)." + } + ] } diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 10984da..ed5d1e1 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -445,9 +445,12 @@ pub enum CheckError { ConstHasEffects(String, Vec), /// An `(export …)` fn has a parameter or return type that is not - /// a C-scalar (`Int`/`Float`). M1's embedding ABI is scalar-only; - /// `Bool`/`Str`/every ADT is rejected at typecheck (the - /// feature-acceptance clause-3 discriminator, in code). + /// a permitted embedding-ABI type. The embedding ABI is frozen as + /// of M3 (DESIGN.md §"Embedding ABI" > "Frozen value layout"): + /// `Int`/`Float` or a single-constructor record of those; every + /// other shape (multi-ctor sums, `Str`/`List`/nested-record + /// fields) is rejected at typecheck (the feature-acceptance + /// clause-3 discriminator, in code). /// Code: `export-non-scalar-signature`. #[error("export `{0}`: embedding ABI accepts `Int`/`Float` or a single-constructor record of those — {1} type `{2}` is not permitted (multi-constructor sums, and `Str`/`List`/nested-record fields, are a future M4 layer)")] ExportNonScalarSignature(String, &'static str, String), @@ -1911,12 +1914,14 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec) -> Result< } check_type_well_formed(&ret_ty, &env)?; - // Embedding-ABI M1: an `(export …)` fn is the C call boundary. - // Its signature must be scalar-only (`Int`/`Float`) and pure. - // Gate order: params → ret → effects, first violation wins - // (so a combined Str+IO export deterministically fails on the - // signature). Unconditional at check-time — independent of the - // codegen emit mode — this IS the clause-3 discriminator. + // Embedding-ABI gate (M1 scalars / M2 ctx / M3 record): an + // `(export …)` fn is the C call boundary. Its signature must be + // C-ABI-permitted — `Int`/`Float`, or a single-constructor + // record of those (M3) — and pure. Gate order: params → ret → + // effects, first violation wins (so a combined Str+IO export + // deterministically fails on the signature). Unconditional at + // check-time — independent of the codegen emit mode — this IS + // the clause-3 discriminator. if f.export.is_some() { fn is_c_scalar(t: &Type) -> bool { matches!(t, Type::Con { name, args, .. } diff --git a/crates/ailang-codegen/src/drop.rs b/crates/ailang-codegen/src/drop.rs index 2bd839b..09695bf 100644 --- a/crates/ailang-codegen/src/drop.rs +++ b/crates/ailang-codegen/src/drop.rs @@ -85,6 +85,7 @@ impl<'a> Emitter<'a> { out.push_str(" %is_null = icmp eq ptr %p, null\n"); out.push_str(" br i1 %is_null, label %ret, label %live\n"); out.push_str("live:\n"); + // FROZEN ABI (embedding boundary) — see DESIGN.md §"Embedding ABI". out.push_str(" %tag = load i64, ptr %p, align 8\n"); let n_ctors = td.ctors.len(); @@ -110,6 +111,7 @@ impl<'a> Emitter<'a> { if lty != "ptr" { continue; } + // FROZEN ABI (embedding boundary) — see DESIGN.md §"Embedding ABI". let off = 8 + (j as i64) * 8; let addr_id = local; local += 1; diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 52ba3a0..62b4f25 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -174,8 +174,9 @@ pub enum Target { /// to the internal `@ail__`. M2: the entrypoint takes /// a mandatory leading `ptr %ctx` (per-thread embedding context) /// published via `@__ail_tls_ctx` around the unchanged internal - /// call. The ctx-threaded C signature is the M2 shape; only the - /// value/record layout remains provisional until M3. + /// call. The ctx-threaded C signature is the M2 shape; the + /// value/record layout is frozen as of M3 (DESIGN.md §"Embedding + /// ABI" > "Frozen value layout"). StaticLib, } diff --git a/crates/ailang-codegen/src/match_lower.rs b/crates/ailang-codegen/src/match_lower.rs index 2864c65..34eb7ff 100644 --- a/crates/ailang-codegen/src/match_lower.rs +++ b/crates/ailang-codegen/src/match_lower.rs @@ -104,6 +104,8 @@ impl<'a> Emitter<'a> { } compiled.push((v, vty)); } + // FROZEN ABI (embedding boundary) — DESIGN.md §"Embedding ABI" + // > "Frozen value layout". size = 8 + n*8, tag@0, fields@8+i*8. let size_bytes = 8 + (compiled.len() * 8) as i64; let p = self.fresh_ssa(); // Iter 17a: pick allocator based on escape analysis. `alloca` diff --git a/crates/ailang-core/src/ast.rs b/crates/ailang-core/src/ast.rs index 2536d89..94c7227 100644 --- a/crates/ailang-core/src/ast.rs +++ b/crates/ailang-core/src/ast.rs @@ -208,7 +208,8 @@ pub struct FnDef { /// Iter embedding-abi-m1: when `Some(sym)`, this fn is the /// embedding boundary. Codegen's `Target::StaticLib` mode /// additionally emits an externally-visible C entrypoint - /// `@` (scalar signature, provisional until M3) forwarding + /// `@` (signature frozen as of M3 — DESIGN.md §"Embedding + /// ABI" > "Frozen value layout") forwarding /// to `@ail__`. The symbol is author-chosen and /// decoupled from the `ail__` mangling so the /// M3-frozen ABI survives module/fn refactors. diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 5aeceb2..10d2ad0 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -2277,9 +2277,11 @@ the internal `@ail__`. The symbol is author-chosen and decoupled from the `ail__` mangling so a module/fn rename does not move the C symbol. -The M1 ABI is **scalar-only and provisional until M3**: every -parameter and the return type must be `Int` (lowered `i64`) or -`Float` (lowered `double`), and the fn's effect set must be empty. +The embedding ABI accepts `Int` (lowered `i64`), `Float` (lowered +`double`), or a single-constructor record of those (crossing as a +bare `ptr` to the frozen box layout below); the fn's effect set must +be empty. **Frozen as of M3**: a future compiler change MUST NOT +move the box offsets below or invert the host-free rule. These are enforced at `ail check` (`export-non-scalar-signature`, `export-has-effects`) — an effectful or non-scalar export *fails to typecheck*. Every exported entrypoint takes a mandatory leading `ailang_ctx_t*` @@ -2290,9 +2292,9 @@ and the runtime accounts RC alloc/free into it (no shared mutable runtime state — the swarm artefact is data-race-free, sanitiser- verified). The staticlib swarm artefact is **RC-only**: `ail build --emit=staticlib` rejects `--alloc=gc`/`--alloc=bump` -(the shared Boehm collector is not swarm-safe). Only the value/record -layout remains provisional until M3; the ctx-threaded C signature is -the M2 shape. +(the shared Boehm collector is not swarm-safe). The value/record +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 @@ -2316,6 +2318,46 @@ IR (the external `@` forwarders, no `@main`) instead of the executable-path `main`-required rejection — the Decision-5 IR-readability affordance for a `main`-free kernel. +### Frozen value layout (M3 — one-way commitment) + +For a single-constructor `data T` whose `n` fields are each `Int` +or `Float`, a value of `T` crossing the embedding C boundary is a +bare payload pointer `p`: + +| bytes | content | +|---|---| +| `p - 8 .. p` | `uint64_t` refcount header (`HEADER_SIZE = 8`) | +| `p + 0 .. p + 8` | `int64_t` constructor tag (written; `0` for the single ctor — no elision) | +| `p + 8 + i*8` | field `i`, declaration order: `int64_t` for `Int`, IEEE-754 `double` bit-pattern for `Float` | + +Total box payload size = `8 + n*8`. This is the layout codegen +emits today (`match_lower.rs` `lower_ctor`); it is **frozen** — a +future compiler change MUST NOT move these offsets. + +**Construction (host → kernel input).** The host MUST obtain an +input record's storage from `ailang_rc_alloc(8 + n*8)` (returns the +payload pointer with the refcount header pre-set to `1`, payload +zeroed), then write the tag (`0`) and the scalar fields at the +offsets above. A raw `malloc` is a contract violation: +`own`-consume and `ailang_rc_dec` both require the runtime's 8-byte +header at `p - 8` initialised to `1`. + +**Ownership follows the declared mode** (the §"Mode metadata is +load-bearing for codegen" contract, as the C ABI): a `(own (con +T))` parameter transfers ownership in — the kernel consumes it +(Iter-B drop-at-return); the host MUST NOT touch or `dec` it after +the call. A `(borrow (con T))` parameter is retained by the host — +the kernel does not consume it; the host frees it. The return value +is always owned by the host. + +**Free (host side).** `ailang_rc_dec(payload)`. Leak-free for an M3 +record because every field is a scalar — `ailang_rc_dec` is +header-only and an M3 record has no boxed children. A record with +boxed fields (`Str`/`List`/nested record) is **not** an M3 type +(rejected by the export gate); a recursive typed-free for that +shape is an additive M4 concern, not a contradiction of this +freeze. + ## Data model The on-disk JSON-AST is what the toolchain hashes, typechecks, and diff --git a/docs/journals/2026-05-18-iter-embedding-abi-m3.1.md b/docs/journals/2026-05-18-iter-embedding-abi-m3.1.md index 5dd3baf..94920ad 100644 --- a/docs/journals/2026-05-18-iter-embedding-abi-m3.1.md +++ b/docs/journals/2026-05-18-iter-embedding-abi-m3.1.md @@ -2,16 +2,25 @@ **Date:** 2026-05-18 **Started from:** 15ee3c5c8fbb871a9cde6cc7d57c0801bae9ae85 -**Status:** PARTIAL (Tasks 1–5 GREEN after the Boss spec-consistency -repair below; Tasks 6–7 re-dispatched) -**Tasks completed:** 4 of 7 by the orchestrator (Tasks 1–4 DONE/GREEN; +**Status:** DONE (Tasks 1–5 GREEN after the Boss spec-consistency +repair below; Tasks 6–7 completed GREEN in the re-dispatch) +**Tasks completed:** 7 of 7 (Tasks 1–4 DONE/GREEN by the orchestrator; Task 5 correctly BLOCKED on a genuine spec-defect, M2.1-precedent -class); Task 5 resolved GREEN by the Boss spec-consistency repair -(global-leak-freedom proof model); Tasks 6–7 re-dispatched on the -amended plan +class, resolved GREEN by the Boss spec-consistency repair — +global-leak-freedom proof model; Tasks 6–7 DONE/GREEN in the +`task_range:[6,7]` re-dispatch on the amended plan) ## Summary +> **Boss note (read first):** the paragraphs below are the +> orchestrator's *first-dispatch* account (present-tense as written +> then) — Task 5's BLOCK was real and is preserved for its +> documentary value. It was resolved by the Boss spec-consistency +> repair and Tasks 6–7 completed in the re-dispatch; the iter is +> **DONE 7/7**. See "## Boss adjudication" and "## Re-dispatch" for +> the resolution. Do not read the "Task 5 is BLOCKED / Task 7 not +> reached" sentences below as the final state. + Tasks 1–4 are complete and GREEN in the working tree: the FIXED-FIRST baseline pins (1a re-point annotation on `adt_ret_export_rejected`; 1b the new `@ailang_rc_alloc` heap-box byte-pin proving size=8+n*8 / @@ -83,10 +92,10 @@ sequence. `embed_record_e2e.rs`. RED and stays RED — see Blocked detail. Left in the working tree as evidence (the M2.1-precedent handling: the BLOCKED task's state is left for Boss adjudication, not discarded). -- iter embedding-abi-m3.1.6 / .7: NOT attempted. Task 5 is a hard - predecessor in the plan's sequencing; `skip task K, continue` is - intentionally not a mode (implicit ordering dependencies; the - orchestrator does not own the dependency graph). +- iter embedding-abi-m3.1.6 / .7: NOT attempted in the first dispatch + (Task 5 was a hard predecessor in the plan's sequencing; `skip task + K, continue` is intentionally not a mode). Completed GREEN in the + `task_range:[6,7]` re-dispatch — see the Re-dispatch section below. ## Concerns @@ -287,6 +296,109 @@ item is warranted (recorded by the Boss outside this journal). audit owns the bench + architect milestone-close (spec Testing items 8/9). This run asserts only the test-suite GREEN state. +## Re-dispatch (2026-05-18 — `task_range:[6,7]`, Tasks 6–7 GREEN) + +Re-dispatched from HEAD `d5c565d` (the committed PARTIAL 5/7 + Boss +spec-defect repair). Tasks 1–5 NOT re-implemented or re-verified. + +- iter embedding-abi-m3.1.6 (DONE): the substantive freeze. + DESIGN.md §"Embedding ABI" — both "provisional until M3" sentences + rewritten to one-way-freeze wording (`:2280-2282` → embedding ABI + accepts `Int`/`Float`/single-ctor record + "**Frozen as of M3**"; + `:2293-2295` → "**frozen as of M3** (see "Frozen value layout" + below)") and the new `### Frozen value layout (M3 — one-way + commitment)` SSOT subsection inserted before `## Data model` (byte + table `p-8` header / `p+0` tag / `p+8+i*8` fields, size `8+n*8`, + construction/ownership/free contract). Lockstep `// FROZEN ABI` + pointers added at the three independent encoders: `runtime/rc.c` + layout comment block, `match_lower.rs` `lower_ctor` `:107` size + site, `drop.rs` `:88` tag-load + `:113` field-offset. Three stale + rustdocs corrected — the two plan-named (`codegen/lib.rs:178`, + `ailang-core/ast.rs:211`) PLUS the Concerns carry-forward + `ailang-check/lib.rs:448-450` ("scalar-only…every ADT rejected" → + frozen-as-of-M3, Boss constraint 2). docs_honesty_pin GREEN + baseline AND after the rewrite (5/5 both); the pinned line + ("Export parameters are written **bare**…") shifted `:2297`→`:2299` + but stays byte-verbatim+contiguous — the pin asserts content not + line, so pin-safe (planner Step-5 item-6 family honoured). Step-7 + enforceability: perturbed `match_lower.rs` `size_bytes` `8`→`16` + (the unanchored sed-class literal hit both `:107` and `:400`; both + feed the byte-pin through `lower_ctor`'s heap path), byte-pin went + RED (`0 passed; 1 failed`, IR emitted `i64 32` not `i64 24`), + restored via `git checkout -- crates/ailang-codegen/src/match_lower.rs` + (working-tree restore only — main HEAD untouched; the single + legitimate git history-touching op of the run), byte-pin GREEN + again (1/1). The freeze is proven enforceable, not aspirational. +- iter embedding-abi-m3.1.7 (DONE): milestone-close verification + gate (no code change). Regression-green-unmodified set GREEN + (`embed_e2e` 1, `embed_rc_accounting_tsan` 2, `embed_swarm_tsan` + 1, `embed_staticlib_cli` 2, `embed_staticlib_alloc_guard` 2, + `print_no_leak_pin` 1; `design_schema_drift` 8/8; + `embed_export_hash_stable` 1/1). Full workspace **639 passed, 0 + failed**, zero compile errors; M3 net-new present + GREEN + (`embed_record_layout_pin` 1, `embed_export_gate` 10 = orig 6 + 4, + `embed_staticlib_lowering` 3 = orig 2 + 1, `embed_record_e2e` 2), + nothing pre-existing removed/weakened. `round_trip` 2/2 (new + `.ail` fixtures round-trip; no Form-A surface added). + +## Concerns (re-dispatch addendum) + +- iter embedding-abi-m3.1.7: PLAN TRANSCRIPTION DEFECT (class: + "plan pseudo-code vs reality" — same family as the iter's existing + `(app Ctor)`→`(term-ctor)` / module==file-stem Concerns). Plan + Task-7 Step 1 names `cargo test -p ailang-check --test + embed_export_hash_stable`, but that test target lives in + **`ailang-core`** (`crates/ailang-core/tests/embed_export_hash_ + stable.rs`), not `ailang-check`. The substantive requirement + ("no schema field added; hashes/drift byte-unchanged") is + unaffected — ran the pin in its actual crate, 1/1 GREEN. Crate + name corrected at execution; observation not correctness. The + recon "named this exact set" claim was wrong for this one target + (recurring `feedback_grounding_check_misses_insource_tests` / + `feedback_plan_pseudo_vs_reality` family — a planner Step-5 scrub + item, recorded here for Boss visibility). +- iter embedding-abi-m3.1.6: the plan places the Step-5 match_lower.rs + `// FROZEN ABI` comment edit and the Step-7 `git checkout -- + match_lower.rs` enforceability restore in the SAME task on the SAME + file. The checkout necessarily reverts the uncommitted Step-5 + comment along with the perturbation (it restores to HEAD `d5c565d`, + where neither exists). Re-applied the Step-5 comment after the + enforceability demo so Step 5 stays satisfied — this is a plan + step-ordering wrinkle, not a defect: the freeze demo MUST run on a + tree where the only delta is the perturbation, and the comment is + re-addable post-demo. Recorded for planner-scrub awareness. + +## Known debt (re-dispatch addendum) + +- `llvm_scalar` identifier still slightly narrower than its post-M3 + behaviour (carried from the first dispatch's Concerns) — out of + scope for Tasks 6/7; the doc-comment disambiguates. Unchanged. +- Bench + architect milestone-close (spec Testing items 8/9) remain + the `audit` skill's job — NOT this implement run, as the original + account and Boss adjudication both record. audit is the next + pipeline step. + +## Files touched (re-dispatch addendum — Tasks 6–7) + +Modified (Task 6; all uncommitted in the working tree): +- `docs/DESIGN.md` (two "provisional until M3" rewrites + the new + "### Frozen value layout" SSOT subsection) +- `runtime/rc.c` (lockstep `// FROZEN ABI` comment in the layout + block) +- `crates/ailang-codegen/src/match_lower.rs` (`lower_ctor` `:107` + lockstep comment) +- `crates/ailang-codegen/src/drop.rs` (`:88` tag-load + `:113` + field-offset lockstep comments) +- `crates/ailang-codegen/src/lib.rs` (`Target::StaticLib` rustdoc + "provisional until M3" → frozen) +- `crates/ailang-core/src/ast.rs` (`FnDef.export` rustdoc + "provisional until M3" → frozen) +- `crates/ailang-check/src/lib.rs` (`ExportNonScalarSignature` + rustdoc "scalar-only…every ADT rejected" → frozen — Concerns + carry-forward) + +Task 7: verification only, no files. + ## Stats bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index 72316a4..07b2b5c 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -101,3 +101,4 @@ - 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__` call (`_adapter`/`_clos` + internal arg vector untouched — M1 decision held; the frozen-at-M3 surface is the C `@(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 - 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 diff --git a/runtime/rc.c b/runtime/rc.c index 1ab2945..0a7dd2e 100644 --- a/runtime/rc.c +++ b/runtime/rc.c @@ -38,6 +38,10 @@ * `GC_malloc`-returned pointer; it stores the ADT tag at offset 0, * fields from offset 8, env-cells from offset 0 in lambda envs, etc. * + * FROZEN ABI for the embedding boundary — see DESIGN.md §"Embedding + * ABI" > "Frozen value layout". A boundary-crossing single-ctor + * scalar record's box offsets MUST NOT move. + * * Single-threaded: counter ops are non-atomic. AILang has no * concurrency primitives yet; when it acquires them, atomic-vs-non- * atomic becomes a separate decision per allocation kind (see