From d5c565d48db9c000e7750000f1a0e0dace7e8695 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 18 May 2026 21:16:41 +0200 Subject: [PATCH] iter embedding-abi-m3.1 (PARTIAL 5/7 + Boss spec-defect repair): single-ctor scalar record crosses the C ABI, ownership follows declared mode Tasks 1-5 GREEN. T1 baseline pins (re-point annotation + @ailang_rc_alloc heap-box byte-pin: size=8+n*8, tag@0, fields@8/16). T2 export gate widened (is_c_scalar -> two-level is_c_abi_type: single-ctor all-Int/Float record; multi-ctor/Str/List/nested still RED; gate suite 10/10; M1 adt-ret must-fail re-pointed to multi-ctor+Str Reading). T3 codegen forwarder widened (llvm_scalar record Type::Con -> ptr; M2 forwarder body byte-unchanged; 3/3 staticlib pins). T4/T5 E2E record round-trip own+borrow, global leak-freedom. Boss spec-consistency repair (M2.1-precedent class): orchestrator correctly BLOCKED Task 5 on a genuine spec defect -- the single-ctx-readback allocs==frees proof model is unsatisfiable for borrow (and only coincidentally passes for own) because M2's TLS-ctx is bound only during the synchronous forwarder call, so host-side decs land on g_rc_*, not ctx. Boss-verified globally leak-free + value-correct both modes. Spec + plan + harness amended to the stronger global model (sum all ailang_rc_stats: lines; the M2-TLS cross-attribution documented as correct behaviour). No fresh grounding-check (removes an over-strong measurement assumption). Tasks 6 (DESIGN.md frozen-layout SSOT + lockstep pointers + freeze wording + enforceability demo) and 7 (workspace-green gate) re-dispatched on the amended plan. Bench/architect milestone-close is audit-owned. iter embedding-abi-m3.1 (PARTIAL); INDEX.md line deferred to the DONE commit --- .../2026-05-18-iter-embedding-abi-m3.1.json | 13 + crates/ail/tests/embed/record_roundtrip.c | 53 ++++ crates/ail/tests/embed_record_e2e.rs | 152 +++++++++ crates/ailang-check/src/lib.rs | 29 +- .../ailang-check/tests/embed_export_gate.rs | 35 +++ crates/ailang-codegen/src/lib.rs | 14 +- .../tests/embed_record_layout_pin.rs | 47 +++ .../tests/embed_staticlib_lowering.rs | 27 ++ .../2026-05-18-iter-embedding-abi-m3.1.md | 292 ++++++++++++++++++ docs/plans/embedding-abi-m3.1.md | 109 +++++-- docs/specs/2026-05-18-embedding-abi-m3.md | 60 +++- examples/embed_backtest_step_record.ail | 16 + .../embed_backtest_step_record_borrow.ail | 16 + examples/embed_export_adt_ret_rejected.ail | 9 +- ...mbed_export_list_field_record_rejected.ail | 11 + examples/embed_export_multictor_rejected.ail | 9 + examples/embed_export_record_ok.ail | 14 + ...embed_export_str_field_record_rejected.ail | 8 + examples/embed_record_layout_carrier.ail | 30 ++ 19 files changed, 893 insertions(+), 51 deletions(-) create mode 100644 bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json create mode 100644 crates/ail/tests/embed/record_roundtrip.c create mode 100644 crates/ail/tests/embed_record_e2e.rs create mode 100644 crates/ailang-codegen/tests/embed_record_layout_pin.rs create mode 100644 docs/journals/2026-05-18-iter-embedding-abi-m3.1.md create mode 100644 examples/embed_backtest_step_record.ail create mode 100644 examples/embed_backtest_step_record_borrow.ail create mode 100644 examples/embed_export_list_field_record_rejected.ail create mode 100644 examples/embed_export_multictor_rejected.ail create mode 100644 examples/embed_export_record_ok.ail create mode 100644 examples/embed_export_str_field_record_rejected.ail create mode 100644 examples/embed_record_layout_carrier.ail 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 new file mode 100644 index 0000000..06d772d --- /dev/null +++ b/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json @@ -0,0 +1,13 @@ +{ + "iter_id": "embedding-abi-m3.1", + "date": "2026-05-18", + "mode": "standard", + "outcome": "PARTIAL", + "tasks_total": 7, + "tasks_completed": 4, + "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 1 }, + "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)." +} diff --git a/crates/ail/tests/embed/record_roundtrip.c b/crates/ail/tests/embed/record_roundtrip.c new file mode 100644 index 0000000..860c70a --- /dev/null +++ b/crates/ail/tests/embed/record_roundtrip.c @@ -0,0 +1,53 @@ +/* Embedding-ABI M3 record round-trip C host (own + borrow via a + * compile-time -DBORROW switch). Frozen value layout (DESIGN.md + * §"Embedding ABI" > "Frozen value layout"): + * p - 8 .. p uint64_t refcount header (set to 1 by ailang_rc_alloc) + * p + 0 int64_t constructor tag (single ctor → 0) + * p + 8 IEEE-754 double field 0 = Float acc + * p + 16 int64_t field 1 = Int n + * Total payload = 8 + 2*8 = 24. + * + * own : the kernel consumes each `(own (con State))` input (drop at + * return); the host must NOT touch/dec it after the call. + * borrow: the kernel does NOT consume the `(borrow (con State))` + * input; the host retains it and dec's it itself each iter. + * In both modes the return is host-owned and host-freed. + */ +#include +#include +#include +#include + +typedef struct ailang_ctx ailang_ctx_t; +extern ailang_ctx_t *ailang_ctx_new(void); +extern void ailang_ctx_free(ailang_ctx_t *); +extern void *ailang_rc_alloc(size_t); +extern void ailang_rc_dec(void *); +extern void *backtest_step(ailang_ctx_t *ctx, void *st, double sample); + +static void *make_state(double acc, int64_t n) { + void *p = ailang_rc_alloc(8 + 2 * 8); /* header=1 set by runtime */ + *(int64_t *)((char *)p + 0) = 0; /* single-ctor tag = 0 */ + memcpy((char *)p + 8, &acc, 8); /* Float acc @ 8 */ + *(int64_t *)((char *)p + 16) = n; /* Int n @ 16 */ + return p; +} + +int main(void) { + ailang_ctx_t *ctx = ailang_ctx_new(); + void *st = make_state(0.0, 0); + for (int i = 0; i < 1000000; i++) { + void *next = backtest_step(ctx, st, (double)(i & 7)); +#ifdef BORROW + ailang_rc_dec(st); /* borrow: host retained input, frees it */ +#endif + /* own: kernel consumed `st`; do NOT touch/dec it here. */ + st = next; /* return is host-owned */ + } + double acc; memcpy(&acc, (char *)st + 8, 8); + int64_t n = *(int64_t *)((char *)st + 16); + assert(n == 1000000); + ailang_rc_dec(st); /* host frees the final return */ + ailang_ctx_free(ctx); /* AILANG_RC_STATS readback fires here */ + return 0; +} diff --git a/crates/ail/tests/embed_record_e2e.rs b/crates/ail/tests/embed_record_e2e.rs new file mode 100644 index 0000000..6b7b364 --- /dev/null +++ b/crates/ail/tests/embed_record_e2e.rs @@ -0,0 +1,152 @@ +//! Embedding-ABI M3 record round-trip (spec §"Testing strategy" — +//! coherent-stop proof, both ownership directions). Build the record +//! kernel as a staticlib, link the C host (frozen `{tag@0, double +//! acc@8, int64 n@16}` layout, `make_state` via `ailang_rc_alloc`), +//! run with `AILANG_RC_STATS=1`, and assert the `ailang_ctx_free` +//! RC-stats readback shows kernel-internal `allocs == frees` and the +//! C host's `assert(n == 1000000)` held (exit 0). +//! +//! `own` (no -DBORROW): the kernel consumes each `(own (con State))` +//! input (drop at return — ratified by +//! `crates/ail/tests/e2e.rs::alloc_rc_own_param_dec_at_fn_return:1855`, +//! NOT `borrow_own_demo_modes_are_metadata_only` which is an Iter-18a +//! pre-enforcement metadata-only pin) and allocates the new return. +//! `borrow` (-DBORROW, Task 5): the kernel does NOT consume the +//! `(borrow (con State))` input (ratified by +//! `…::alloc_rc_borrow_only_recursive_list_drop:1671`); the host +//! retains and dec's it each iter. Both prove "ownership follows the +//! declared mode" — the frozen contract proven both ways. +//! +//! The build/link incantation mirrors `embed_e2e.rs` +//! (`ail build --emit=staticlib -o ` → `cc host.c +//! lib.a libailang_rt.a`); the stats-line parse mirrors +//! `e2e.rs::build_and_run_with_rc_stats` (the runtime's fixed +//! `ailang_rc_stats: allocs=N frees=M live=K` shape). + +use std::path::PathBuf; +use std::process::Command; + +fn ail_bin() -> &'static str { env!("CARGO_BIN_EXE_ail") } +fn manifest() -> PathBuf { PathBuf::from(env!("CARGO_MANIFEST_DIR")) } +fn ws_root() -> PathBuf { + manifest().parent().unwrap().parent().unwrap().to_path_buf() +} + +#[derive(Debug)] +struct RcStats { + allocs: u64, + frees: u64, + exit_code: i32, +} + +/// Build `` as a staticlib, link `` (under +/// `crates/ail/tests/`) with `extra_cc` flags, run under +/// `AILANG_RC_STATS=1`, and return the `ailang_ctx_free` readback. +fn build_link_run_embed(fixture: &str, host_rel: &str, extra_cc: &[&str]) -> RcStats { + let module = fixture.strip_suffix(".ail").expect("fixture is a .ail file"); + let fixture_path = ws_root().join("examples").join(fixture); + let host_c = manifest().join("tests").join(host_rel); + let outdir = std::env::temp_dir().join(format!( + "ail-embed-record-e2e-{}-{}", + module, + std::process::id() + )); + std::fs::create_dir_all(&outdir).unwrap(); + + let build = Command::new(ail_bin()) + .args(["build", fixture_path.to_str().unwrap(), + "--emit=staticlib", "-o", outdir.to_str().unwrap()]) + .output().expect("ail build --emit=staticlib"); + assert!(build.status.success(), + "staticlib build failed: {}", + String::from_utf8_lossy(&build.stderr)); + + let host_bin = outdir.join("host"); + let mut cc = Command::new("cc"); + cc.arg(&host_c); + for f in extra_cc { cc.arg(f); } + cc.arg(outdir.join(format!("lib{module}.a"))) + .arg(outdir.join("libailang_rt.a")) + .arg("-o").arg(&host_bin); + let cc_out = cc.output().expect("cc host link"); + assert!(cc_out.status.success(), + "cc link failed: {}", String::from_utf8_lossy(&cc_out.stderr)); + + let run = Command::new(&host_bin) + .env("AILANG_RC_STATS", "1") + .output().expect("run host"); + let stderr = String::from_utf8_lossy(&run.stderr); + // Boss spec-consistency repair (2026-05-18, M3.1 BLOCKED + // adjudication): the run emits TWO `ailang_rc_stats:` lines — + // the `ailang_ctx_free` ctx readback AND the `g_rc_*` atexit + // line. By M2's TLS-ctx design the ctx is bound to TLS only for + // the synchronous forwarder call, so the host's `make_state` / + // per-iter `dec` / final `dec` (which run outside any forwarder + // call) land on `g_rc_*`, not ctx. The invariant is GLOBAL + // leak-freedom: Σallocs == Σfrees across *all* stat lines + // (equivalently Σ`live` = 0) — not per-ctx-line balance. Sum + // every line; a missing-line panic guards against zero parsed. + let mut allocs: u64 = 0; + let mut frees: u64 = 0; + let mut seen = 0usize; + for line in stderr.lines().filter(|l| l.starts_with("ailang_rc_stats:")) { + seen += 1; + for tok in line.split_whitespace() { + if let Some(v) = tok.strip_prefix("allocs=") { + allocs += v.parse::().expect("allocs= u64"); + } else if let Some(v) = tok.strip_prefix("frees=") { + frees += v.parse::().expect("frees= u64"); + } + } + } + assert!(seen > 0, "missing ailang_rc_stats line; stderr was:\n{stderr}"); + RcStats { + allocs, + frees, + exit_code: run.status.code().unwrap_or(-1), + } +} + +/// own: globally leak-free — every State box freed exactly once. +/// The `(own (con State))` input is drop-consumed at the kernel's +/// return (Iter-B, on ctx); the host's `make_state` + final `dec` +/// land on `g_rc_*`. Σallocs == Σfrees across both stat lines +/// (own: ctx `live=0` + g_rc `live=0`), and the C host's +/// `assert(n == 1000000)` held. +#[test] +fn record_roundtrip_own_alloc_eq_free() { + let stats = build_link_run_embed( + "embed_backtest_step_record.ail", + "embed/record_roundtrip.c", + &[], + ); + assert_eq!(stats.allocs, stats.frees, + "own: globally leak-free — Σallocs == Σfrees across the ctx \ + readback + g_rc atexit lines (kernel-consumed `own` inputs \ + on ctx; host make_state/final dec on g_rc); {stats:?}"); + assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held"); +} + +/// borrow: globally leak-free. The kernel does NOT consume the +/// `(borrow (con State))` input (ratified by +/// `crates/ail/tests/e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`); +/// it allocs every return box on ctx, the host frees every input + +/// the final return on `g_rc_*` (outside the forwarder's TLS-ctx +/// window). The ctx line shows `live=+N`, the g_rc line `live=−N`, +/// summing to 0 — correct M2-TLS cross-attribution, not a leak. +/// Σallocs == Σfrees across both lines. Same harness, `-DBORROW`. +/// With Task 4 this proves "ownership follows the declared mode" in +/// both directions, globally leak-free — proven, not asserted. +#[test] +fn record_roundtrip_borrow_alloc_eq_free() { + let stats = build_link_run_embed( + "embed_backtest_step_record_borrow.ail", + "embed/record_roundtrip.c", + &["-DBORROW"], + ); + assert_eq!(stats.allocs, stats.frees, + "borrow: globally leak-free — Σallocs == Σfrees across the ctx \ + readback (kernel return allocs, live=+N) + g_rc atexit \ + (host input/return decs, live=−N); summed they balance; {stats:?}"); + assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held"); +} diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 87ab435..10984da 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -449,7 +449,7 @@ pub enum CheckError { /// `Bool`/`Str`/every ADT is rejected at typecheck (the /// feature-acceptance clause-3 discriminator, in code). /// Code: `export-non-scalar-signature`. - #[error("export `{0}`: M1 embedding ABI is scalar-only — {1} type `{2}` is not `Int`/`Float`")] + #[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), /// An `(export …)` fn has a non-empty effect set. An embedding @@ -1922,8 +1922,31 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec) -> Result< matches!(t, Type::Con { name, args, .. } if args.is_empty() && (name == "Int" || name == "Float")) } + // M3 (spec 2026-05-18-embedding-abi-m3 §Architecture): a C + // scalar, OR a single-constructor `data` whose every field is a + // *bare* C scalar. Two-level by design — a record-typed field + // stays rejected (M4 owns nested-record recursion). Uses the + // in-scope `env.types: String -> TypeDef` (cf. lib.rs:1826). + fn is_c_abi_type(t: &Type, env: &Env) -> bool { + if is_c_scalar(t) { + return true; + } + if let Type::Con { name, args, .. } = t { + if args.is_empty() { + if let Some(td) = env.types.get(name) { + if td.ctors.len() == 1 { + return td.ctors[0] + .fields + .iter() + .all(is_c_scalar); + } + } + } + } + false + } for p in ¶m_tys { - if !is_c_scalar(p) { + if !is_c_abi_type(p, &env) { return Err(CheckError::ExportNonScalarSignature( f.name.clone(), "parameter", @@ -1931,7 +1954,7 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec) -> Result< )); } } - if !is_c_scalar(&ret_ty) { + if !is_c_abi_type(&ret_ty, &env) { return Err(CheckError::ExportNonScalarSignature( f.name.clone(), "return", diff --git a/crates/ailang-check/tests/embed_export_gate.rs b/crates/ailang-check/tests/embed_export_gate.rs index 2b6d249..00ec7cc 100644 --- a/crates/ailang-check/tests/embed_export_gate.rs +++ b/crates/ailang-check/tests/embed_export_gate.rs @@ -27,6 +27,14 @@ fn str_param_export_rejected() { .iter().any(|c| c == "export-non-scalar-signature")); } +// M3 RE-POINT (deliberate, reviewed — spec 2026-05-18-embedding-abi-m3 +// §"must-fail axis"): the fixture this asserts on +// (embed_export_adt_ret_rejected.ail) is single-ctor two-Int = M3-VALID. +// Task 2 re-points the fixture to a genuinely-still-rejected ADT +// (multi-ctor + Str field). This pin's *meaning* changes from +// "any ADT rejected" to "non-M3-shaped ADT rejected"; it is NOT +// silently inverted — the rejection (export-non-scalar-signature) +// stays asserted, on a fixture that still genuinely fails it. #[test] fn adt_ret_export_rejected() { assert!(check_codes("embed_export_adt_ret_rejected.ail") @@ -61,3 +69,30 @@ fn headline_int_export_passes() { c == "export-non-scalar-signature" || c == "export-has-effects"), "headline export must pass the gate; got {codes:?}"); } + +#[test] +fn record_export_passes() { + // single-ctor (Float,Int) record export — M3-valid + let codes = check_codes("embed_export_record_ok.ail"); + assert!(!codes.iter().any(|c| + c == "export-non-scalar-signature" || c == "export-has-effects"), + "single-ctor scalar record export must pass the gate; got {codes:?}"); +} + +#[test] +fn str_field_record_export_rejected() { + assert!(check_codes("embed_export_str_field_record_rejected.ail") + .iter().any(|c| c == "export-non-scalar-signature")); +} + +#[test] +fn list_field_record_export_rejected() { + assert!(check_codes("embed_export_list_field_record_rejected.ail") + .iter().any(|c| c == "export-non-scalar-signature")); +} + +#[test] +fn multictor_export_rejected() { + assert!(check_codes("embed_export_multictor_rejected.ail") + .iter().any(|c| c == "export-non-scalar-signature")); +} diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 53e54c3..52ba3a0 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -662,17 +662,27 @@ fn fn_scalar_sig(t: &Type) -> Option<(Vec, Type)> { other => other, }; match inner { + // M3: params/ret may include a single-ctor scalar record type; + // llvm_scalar maps it to `ptr`. fn_scalar_sig is type-shape only. Type::Fn { params, ret, .. } => Some((params.clone(), (**ret).clone())), _ => None, } } -/// `Int` → `i64`, `Float` → `double` (the only two M1 scalars; the -/// check-side gate rejects everything else before codegen). +/// `Int` → `i64`, `Float` → `double`, a single-ctor scalar record +/// (any other named `Type::Con` reaching an `(export)` signature, by +/// the Task-2 export gate) → `ptr`. The check-side gate rejects every +/// other shape before codegen. fn llvm_scalar(t: &Type) -> &'static str { match t { Type::Con { name, .. } if name == "Float" => "double", + Type::Con { name, .. } if name == "Int" => "i64", + // M3: any other Type::Con reaching an (export) signature is, + // by the Task-2 export gate, a single-ctor scalar record; + // it crosses the C ABI as a bare `ptr` (DESIGN.md §"Embedding + // ABI" frozen layout — payload pointer). + Type::Con { .. } => "ptr", _ => "i64", } } diff --git a/crates/ailang-codegen/tests/embed_record_layout_pin.rs b/crates/ailang-codegen/tests/embed_record_layout_pin.rs new file mode 100644 index 0000000..54e1171 --- /dev/null +++ b/crates/ailang-codegen/tests/embed_record_layout_pin.rs @@ -0,0 +1,47 @@ +//! FROZEN ABI byte-pin — see DESIGN.md §"Embedding ABI" frozen layout. +//! Pins the heap (@ailang_rc_alloc) box layout a boundary-crossing +//! single-ctor scalar record takes: size = 8 + n*8, tag i64 @ offset +//! 0, fields i64-strided from offset 8. Goes RED if codegen moves an +//! offset — the M3 freeze made enforceable, not aspirational. +//! +//! The carrier (`embed_record_layout_carrier.ail`) is a non-export +//! exe-target program whose `mk` returns a `Pt` consumed by an +//! `(own (con Pt))` param `sum_pt`, forcing the escaping heap box +//! (NOT the `alloca` non-escape path the pre-existing +//! `iter17a_local_box_alloca` pins — that is a different path and not +//! a substitute for this one). Lowered under `AllocStrategy::Rc` +//! (the path a crossing M3 record actually takes), mirroring the +//! workspace-load + lower incantation of `embed_staticlib_lowering.rs`. + +use ailang_core::Workspace; +use std::path::PathBuf; + +fn load(file: &str) -> Workspace { + let path = PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .parent().unwrap().parent().unwrap() + .join("examples").join(file); + ailang_surface::load_workspace(&path).unwrap() +} + +fn lower_carrier_ir() -> String { + let ws = load("embed_record_layout_carrier.ail"); + ailang_codegen::lower_workspace_with_alloc( + &ws, ailang_codegen::AllocStrategy::Rc).unwrap() +} + +#[test] +fn heap_box_layout_is_frozen_8_plus_n_times_8_tag_at_0_fields_from_8() { + let ir = lower_carrier_ir(); + // Pt has 2 Int fields → payload size 8 (tag) + 2*8 (fields) = 24, + // on the @ailang_rc_alloc heap path (record crosses the boundary). + assert!(ir.contains("call ptr @ailang_rc_alloc(i64 24)"), + "frozen: heap box payload size = 8 + n*8 (n=2 → 24); IR:\n{ir}"); + // constructor tag written at offset 0 (single-ctor → 0; no elision) + assert!(ir.contains("store i64 0, ptr"), + "frozen: ctor tag i64 at offset 0; IR:\n{ir}"); + // field 0 at offset 8, field 1 at offset 16 (i64-strided from 8) + assert!(ir.contains("getelementptr inbounds i8, ptr") && ir.contains("i64 8"), + "frozen: field 0 at payload offset 8; IR:\n{ir}"); + assert!(ir.contains("i64 16"), + "frozen: field 1 at payload offset 16 (8 + 1*8); IR:\n{ir}"); +} diff --git a/crates/ailang-codegen/tests/embed_staticlib_lowering.rs b/crates/ailang-codegen/tests/embed_staticlib_lowering.rs index 22d8a4f..c3383b3 100644 --- a/crates/ailang-codegen/tests/embed_staticlib_lowering.rs +++ b/crates/ailang-codegen/tests/embed_staticlib_lowering.rs @@ -43,6 +43,33 @@ fn staticlib_emits_forwarder_no_main() { "internal call must stay byte-unchanged (no ctx arg);\nIR:\n{ir}"); } +/// M3: a single-ctor scalar record param/ret crosses the embedding +/// C boundary as a bare `ptr` (the frozen payload pointer — DESIGN.md +/// §"Embedding ABI" > "Frozen value layout"). The M2 forwarder body +/// is byte-unchanged: leading `ptr %ctx`, TLS save/store/restore, the +/// internal `@ail__` call carrying no ctx arg and no +/// aggregate calling convention (no `sret`/`byval` — a record is a +/// bare ptr, not an LLVM aggregate). Internal symbol is module- +/// qualified `@ail_embed_backtest_step_record_step` (module == +/// file stem, Design-decision 6). +#[test] +fn staticlib_record_forwarder_is_ptr_passthrough() { + let ws = load("embed_backtest_step_record.ail"); + let ir = ailang_codegen::lower_workspace_staticlib_with_alloc( + &ws, ailang_codegen::AllocStrategy::Rc).unwrap(); + // record param + ret cross as bare ptr; ctx leading; M2 TLS shape. + assert!(ir.contains("define ptr @backtest_step(ptr %ctx, ptr %a0, double %a1)"), + "record fwd: ptr ret, leading ptr %ctx, ptr record param, double sample;\nIR:\n{ir}"); + assert!(ir.contains("store ptr %ctx, ptr @__ail_tls_ctx"), + "M2 TLS store byte-unchanged;\nIR:\n{ir}"); + assert!(ir.contains("call ptr @ail_embed_backtest_step_record_step(ptr %a0, double %a1)"), + "internal call byte-unchanged (no ctx arg, module-qualified);\nIR:\n{ir}"); + assert!(!ir.contains("sret") && !ir.contains("byval"), + "no aggregate convention introduced — record is a bare ptr;\nIR:\n{ir}"); + assert!(!ir.contains("define i32 @main()"), + "staticlib: no @main;\nIR:\n{ir}"); +} + #[test] fn executable_target_still_emits_main() { let ws = load("embed_backtest_step.ail"); 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 new file mode 100644 index 0000000..5dd3baf --- /dev/null +++ b/docs/journals/2026-05-18-iter-embedding-abi-m3.1.md @@ -0,0 +1,292 @@ +# iter embedding-abi-m3.1 — freeze the value layout + record across the C ABI + +**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; +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 + +## Summary + +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 / +tag@0 / fields@8,16), the export-gate widen to a single-ctor scalar +record (`is_c_scalar` → two-level `is_c_abi_type`, 10/10 gate suite), +the codegen forwarder widen (`llvm_scalar` maps a gate-guaranteed +record `Type::Con` → `ptr`; M2 forwarder body byte-unchanged; 3/3 +staticlib-lowering pins), and the `own` E2E record round-trip +(1,000,000-iter balanced ctx readback `allocs=1000000 frees=1000000 +live=0`, exit 0 — the spec's "mechanically almost free" ownership +claim substantiated, ratified by `e2e.rs:1855`, NOT the Iter-18a +metadata-only pin). + +Task 5 (the `borrow` E2E arm) is BLOCKED on a genuine +plan-assertion-model defect (detail below), structurally identical to +the M2.1 first-dispatch swarm.c/-DSHARED_CTX spec defect that the +Boss adjudicated and repaired. No production-code bug: the borrow +mode is leak-free and value-correct; the plan's *assertion shape* is +unsatisfiable given the M2 TLS-ctx accounting mechanism. Returned +BLOCKED for Boss adjudication per the Iron Law (never push past +BLOCKED by hand; spec/plan amendment is a Boss/brainstorm decision). + +audit owns the bench + architect milestone-close (spec Testing items +8/9 — architect Invariant 1, bench trio); this implement run asserts +only the test-suite GREEN state an implement run can, and Task 7 +(workspace-green gate) was not reached because Task 5 blocks the +sequence. + +## Per-task notes + +- iter embedding-abi-m3.1.1 (DONE_WITH_CONCERNS): re-point annotation + added verbatim above `adt_ret_export_rejected` + (`crates/ailang-check/tests/embed_export_gate.rs`); gate suite 6/6 + inert. New byte-pin carrier `examples/embed_record_layout_carrier.ail` + + new pin `crates/ailang-codegen/tests/embed_record_layout_pin.rs` + (`lower_workspace_with_alloc(&ws, AllocStrategy::Rc)`, mirroring + `embed_staticlib_lowering.rs`'s `load()` helper). Pin GREEN on the + pre-M3 tree. Carrier required two grounding corrections vs the + plan's literal pseudo-code (see Concerns). +- iter embedding-abi-m3.1.2 (DONE_WITH_CONCERNS): `is_c_scalar` → + two-level `is_c_abi_type` (`crates/ailang-check/src/lib.rs:1921+`), + both call sites (param loop + ret) repointed; `:452` `#[error]` + widened; `:458` correctly left byte-unchanged (no `M1` token). 5 + fixtures (`embed_export_record_ok` + 3 `_rejected` + re-pointed + `embed_export_adt_ret_rejected` → multi-ctor+Str `Reading`) + 4 new + gate tests. RED observed (`record_export_passes` failed pre-widen); + GREEN 10/10; full `ailang-check` 0 failed. +- iter embedding-abi-m3.1.3 (DONE_WITH_CONCERNS): `llvm_scalar` + widened (`Float`→double, `Int`→i64, other `Type::Con`→`ptr`, `_`→ + i64) + doc-comment lockstep; `fn_scalar_sig` clarifying comment only + (body recon-confirmed filter-free). 2 fixtures + (`embed_backtest_step_record{,_borrow}.ail`) + forwarder-IR pin + `staticlib_record_forwarder_is_ptr_passthrough`. RED observed + (State→i64 pre-widen); GREEN 3/3; full `ailang-codegen` 0 failed + (Task-1 byte-pin unchanged — box layout did not move). +- iter embedding-abi-m3.1.4 (DONE): `crates/ail/tests/embed/ + record_roundtrip.c` + `crates/ail/tests/embed_record_e2e.rs`. + `build_link_run_embed` composed from verbatim-mirrored real + incantations (`embed_e2e.rs` build/link + `e2e.rs:2190` + `build_and_run_with_rc_stats` stats-parse — `embed_e2e.rs` exposes + no reusable helper; mirroring, not inventing). `own` E2E GREEN + immediately once Tasks 2+3 in tree (ctx readback `allocs=1000000 + frees=1000000 live=0`, exit 0). No production code (plan: none + expected). Ratifier `e2e.rs::alloc_rc_own_param_dec_at_fn_return: + 1855` cited; `borrow_own_demo_modes_are_metadata_only:1330` NOT + cited (Boss constraint 2 honoured). +- iter embedding-abi-m3.1.5 (BLOCKED — plan-assertion-model defect): + `record_roundtrip_borrow_alloc_eq_free` added to + `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). + +## Concerns + +- iter embedding-abi-m3.1.1: PLAN PSEUDO-CODE DEFECT (class: + "plan pseudo-code vs reality"). The plan's carrier body used + `(app Pt a b)` for ADT construction — non-compiling (`ail check`: + `[not-a-function] mk: \`Pt\` is not a function`). AILang construction + is `(term-ctor args…)` (grounded on + `examples/box.ail:36`, `borrow_own_demo.ail`). Corrected to + `(term-ctor Pt Pt a b)`. Second correction: the plan's + `(app print …)` IO sink is unresolvable by the codegen library API + the byte-pin must use (`lower_workspace_with_alloc` does not run the + mono/prelude pass that resolves polymorphic `print` — + empirically: `UnknownVar("print")`; `io/print_int` is not a known + effect-op). Corrected to `(let s (app int_to_str …) (do io/print_str + s))` (monomorphic builtin, library-resolvable; grounded on + `int_to_str_drop_rc.ail`). Structural intent (single-ctor 2-Int + record forced onto the `@ailang_rc_alloc` heap path) preserved + exactly; plan Step-4/5 explicitly sanctions carrier adjustment to + force the heap box. Observation, not correctness — the byte-pin + asserts the literal emitted forms and is a genuine RED-on-offset- + move guard (proven enforceable would be Task 6 Step 7, not reached). +- iter embedding-abi-m3.1.2: same plan-pseudo-code class — all 5 + fixture bodies used `(app Ctor …)`; corrected to `(term-ctor …)`. + The test assertion idiom was matched to the file's *existing* + `.iter().any(|c| c == …)` pattern (plan showed + `.contains(&"…".to_string())`); `record_export_passes` written as + `!any(gate-code)` not the plan's `.is_empty()` (a single + `over-strict-mode` warning makes the diagnostics vec non-empty — + `.is_empty()` would false-fail; the protected property is + "no gate rejection"). Semantic intent preserved. +- iter embedding-abi-m3.1.2 (carry to Task 6): the + `CheckError::ExportNonScalarSignature` rustdoc at + `crates/ailang-check/src/lib.rs:448-450` still says "M1's embedding + ABI is scalar-only; `Bool`/`Str`/every ADT is rejected" — now stale + (single-ctor scalar records are accepted). Outside Task 2's named + edit regions (`:452`/`:458` only); Task 6 owns the broader + stale-doc / "provisional until M3" sweep and should absorb this + line. Not gating; recorded for Boss/Task-6 scope. +- iter embedding-abi-m3.1.3: PLAN TRANSCRIPTION DEFECT (same class as + the M2.1 journal's `@ail_embed_backtest_step_step` correction). The + plan's fixtures used `(module backtest …)` while the file stems are + `embed_backtest_step_record{,_borrow}` — the loader enforces + module==file-stem (`[module-name-mismatch]`). Module names corrected + to the file stems; the forwarder-IR pin's internal-symbol assertion + corrected from the plan's draft `@ail_backtest_step` to the + convention-correct module-qualified + `@ail_embed_backtest_step_record_step` (per the plan's own Step-3 + parenthetical "tighten to literal emitted forms" + Boss constraint / + M2.1 module-qualified-symbol mandate). `llvm_scalar` doc-comment + updated in lockstep with its widened body (coherence-required, not + surrounding cleanup — a function whose doc says "the only two M1 + scalars" while its body maps a third case is self-contradictory + within the same task). `llvm_scalar` is now a slightly + over-narrow *name* (also maps records→ptr) — renaming is a 4-site + cross-cut out of Task-3 scope; the doc disambiguates; advisory Nit + only. + +## Known debt + +- `crates/ailang-check/src/lib.rs:448-450` stale variant rustdoc — + Task-6-scope (see Concerns); not touched to keep Task 2 + scope-compliant. +- `llvm_scalar` identifier slightly narrower than its post-M3 + behaviour — out of Task-3 scope; doc disambiguates. +- Tasks 6 (DESIGN.md SSOT + lockstep freeze pointers + the + match_lower.rs enforceability demonstration) and 7 (workspace-green + gate) unexecuted — blocked behind Task 5. + +## Blocked detail + +**Task:** 5 (`record_roundtrip_borrow_alloc_eq_free`). +**Reason:** worker-blocked — design/plan contradiction +(plan-assertion-model defect; the implementer-phase sub-status is +`BLOCKED`, mapped to the Boss per the SKILL.md sub-status table). + +**Worker says (verbatim):** The plan's Task-5 assertion +`assert_eq!(stats.allocs, stats.frees, "borrow: kernel kept input; +host freed every input + the return")` is structurally unsatisfiable. +`stats` is defined (Task 4 Step 2, plan) as the *single* +`ailang_ctx_free` RC-stats readback — the kernel-internal ctx +accounting. In `borrow` mode the kernel allocates the new return box +during the forwarder call (lands on `ctx->alloc_count` because the +codegen forwarder publishes `ctx` into `__ail_tls_ctx` for the +synchronous call duration only) but does NOT consume/drop the borrowed +input (correct borrow semantics, ratified by +`e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`). The +balancing frees are the host's per-iter `ailang_rc_dec(st)`, which run +*outside* any forwarder call → `__ail_tls_ctx` is NULL → they land on +`g_rc_free_count` (the atexit fallback line), NOT on `ctx`. There is +no public runtime API (`ailang_ctx_enter`/`set`/`bind`) for the C +host to publish a ctx to TLS around its own decs (`__thread +ailang_ctx_t *__ail_tls_ctx` is runtime-internal; the only writer is +the codegen-emitted forwarder, by M2 design). Empirical readback +(`AILANG_RC_STATS=1`, borrow): ctx line `allocs=1000000 frees=0 +live=1000000`; g_rc atexit line `allocs=1 frees=1000001 +live=-1000000`. Globally leak-free and value-correct (exit 0, +`assert(n==1000000)` held; `allocs_total=1000001 == +frees_total=1000001`, net live=0). The plan's own assertion *message* +("host freed every input") contradicts its own `stats` *source* (the +ctx readback, which by construction cannot see host-side frees) — an +internal contradiction in the plan. This is NOT a production-code bug +(the spec's substantive invariant — ownership follows the declared +mode, no leak — holds); it is a plan-assertion-model defect of the +same class the M2.1 journal records (the swarm.c/-DSHARED_CTX +spec defect: a plan assertion structurally impossible given the M2 +TLS-ctx mechanism, Boss-adjudicated + spec-amended, NOT +agent-self-amended). Per the Iron Law ("never push past BLOCKED by +hand") and memory ("when an iter needs a spec change, the spec is +wrong — update via brainstorm, not a self-patch"), returned BLOCKED +rather than silently substituting a global-balance / `live==0` +assertion (which would be the correct invariant but is a *different* +assertion than the plan scripts — a Boss/brainstorm adjudication). + +**Suggested next step:** Boss adjudicates the spec/plan accounting +model — likely: amend the spec + Task 5 (and re-check Task 4's +coincidentally-passing ctx-line assertion) so the proven invariant is +global leak-freedom (`live==0` across the ctx readback AND the g_rc +atexit line, or `allocs_total==frees_total` summed) for *both* modes, +rather than per-line ctx `allocs==frees` (which only holds for `own` +by the accident that own-decs happen inside the forwarder call). Then +re-dispatch with `task_range:[5,7]` against the amended plan. Tasks +1–4 are sound and GREEN; the working tree (including the failing +Task-5 test as evidence) is left intact per the M2.1 precedent. + +## Files touched + +Modified: +- `crates/ailang-check/src/lib.rs` (Task 2: gate predicate + message) +- `crates/ailang-check/tests/embed_export_gate.rs` (Tasks 1,2) +- `crates/ailang-codegen/src/lib.rs` (Task 3: llvm_scalar + + fn_scalar_sig comment) +- `crates/ailang-codegen/tests/embed_staticlib_lowering.rs` (Task 3) +- `examples/embed_export_adt_ret_rejected.ail` (Task 2: re-point) + +Created: +- `crates/ailang-codegen/tests/embed_record_layout_pin.rs` (Task 1) +- `examples/embed_record_layout_carrier.ail` (Task 1) +- `examples/embed_export_record_ok.ail` (Task 2) +- `examples/embed_export_str_field_record_rejected.ail` (Task 2) +- `examples/embed_export_list_field_record_rejected.ail` (Task 2) +- `examples/embed_export_multictor_rejected.ail` (Task 2) +- `examples/embed_backtest_step_record.ail` (Task 3) +- `examples/embed_backtest_step_record_borrow.ail` (Task 3) +- `crates/ail/tests/embed/record_roundtrip.c` (Task 4/5) +- `crates/ail/tests/embed_record_e2e.rs` (Task 4 GREEN + + Task 5 RED-evidence) + +## Boss adjudication (2026-05-18 — M2.1-precedent class) + +The orchestrator's Task-5 BLOCK was correct and well-reasoned, and +its diagnosis was independently verified by the Boss (not +agent-trusted): built+ran both E2E modes by hand, full +`AILANG_RC_STATS` stderr — + +- own: ctx `allocs=1000000 frees=1000000 live=0`; g_rc `allocs=1 frees=1 live=0`; exit 0 +- borrow: ctx `allocs=1000000 frees=0 live=1000000`; g_rc `allocs=1 frees=1000001 live=-1000000`; exit 0 + +Both modes are **globally** leak-free (Σallocs = Σfrees = 1,000,001, +Σ`live` = 0) and value-correct. The defect is purely the spec's +proof *instrument*: §"Testing strategy" items 3/4 + §"Coherent stop" +asserted the single `ailang_ctx_free` ctx readback shows +`allocs == frees`, which is false **by M2's shipped TLS-ctx design** +(ctx bound to `__ail_tls_ctx` only for the synchronous forwarder +call; the host's `make_state`/`dec` run outside it → `g_rc_*`). The +roadmap's own coherent-stop wording is "a record in/out with +**alloc==free** across many calls" = *global*, exactly what holds. + +Adjudicated as a **Boss spec-consistency repair, not a brainstorm +bounce** — M2.1-precedent class (genuine spec defect; deliverable + +substantive invariant sound; only verification mechanics +mis-specified; first BLOCKED task in M3, not 2+-in-a-family). The +repair, folded into this partial (M2.1 `c9a84b3` shape): + +1. Spec amended (dated repair note + §"Testing strategy" 3/4 + + §"Coherent stop"): proof model → **global leak-freedom** + (Σallocs == Σfrees across *all* `ailang_rc_stats:` lines, + Σ`live` = 0, exit 0) for both modes; the M2-TLS cross-attribution + documented as correct behaviour, not a leak. Strictly stronger + and honest. No fresh grounding-check (removes an over-strong + measurement assumption, adds none about compiler behaviour). +2. Plan amended (Task 4/5 + the harness step): the harness sums + *every* `ailang_rc_stats:` line, not just the first. +3. Code repair applied (mechanical, decided-invariant): the + `build_link_run_embed` parse now sums all stat lines; T4/T5 + docstrings + assertion messages corrected to the global model. + Verified GREEN by the Boss: `embed_record_e2e` 2/2 (own+borrow), + gate 10/10, byte-pin 1/1, forwarder 3/3; regression-green set + (`embed_e2e`, `embed_staticlib_cli`, `embed_export_hash_stable`, + `design_schema_drift`, `docs_honesty_pin`) unmodified-green. + +Plan-pseudo-code defects the orchestrator self-corrected inline +(`feedback_plan_pseudo_vs_reality` class — `(app Ctor …)` → +`(term-ctor …)` construction, library-`print` non-resolution, +module==file-stem) are noted in Concerns; a planner Step-5 scrub +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. + +## Stats + +bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json diff --git a/docs/plans/embedding-abi-m3.1.md b/docs/plans/embedding-abi-m3.1.md index aec8972..87a07c1 100644 --- a/docs/plans/embedding-abi-m3.1.md +++ b/docs/plans/embedding-abi-m3.1.md @@ -688,8 +688,22 @@ Build `libbacktest.a` + `libailang_rt.a` from `embed_backtest_step_record.ail`, link a C host that constructs the input `State` via `ailang_rc_alloc`, calls `backtest_step` N times (kernel consumes each `own` input), frees the final return via -`ailang_rc_dec`, and asserts `ailang_ctx_free`'s `AILANG_RC_STATS` -readback shows `allocs == frees` and the value is correct. +`ailang_rc_dec`, and asserts **global leak-freedom** — Σallocs == +Σfrees summed across *every* `ailang_rc_stats:` line the run emits +(the `ailang_ctx_free` ctx readback AND the `g_rc_*` atexit line) — +plus exit 0. + +> **Boss spec-consistency repair (2026-05-18 — M3.1 BLOCKED +> adjudication, see the spec's repair note).** The original +> single-ctx-readback `allocs == frees` model is unsatisfiable for +> borrow (and only coincidentally passes for own): by M2's TLS-ctx +> design the host's `make_state`/`dec` run outside the forwarder +> call and land on `g_rc_*`, not ctx. The corrected, stronger +> invariant is **global**: the harness sums *all* `ailang_rc_stats:` +> lines; Σallocs == Σfrees (Σ`live` = 0) + exit 0, for both modes. +> Verified empirically: own ctx `live=0`/g_rc `live=0`; borrow ctx +> `live=+N`/g_rc `live=−N` (Σ=0) — the split is correct M2-TLS +> behaviour, not a leak. **Files:** - Create: `crates/ail/tests/embed/record_roundtrip.c` @@ -747,31 +761,50 @@ int main(void) { Create `crates/ail/tests/embed_record_e2e.rs`. Open `crates/ail/tests/embed_e2e.rs` and **mirror its exact** build/link/ -run helper (the `ail build --emit=staticlib … -o`, the `ar`/`clang` -link of the C host against `lib.a` + `libailang_rt.a`, the -`AILANG_RC_STATS=1` env + stderr `allocs=… frees=…` parse). Add: +run incantation (the `ail build --emit=staticlib … -o`, the `cc` +link of the C host against `lib.a` + `libailang_rt.a`, the +`AILANG_RC_STATS=1` env). **The stats parse must sum ALL +`ailang_rc_stats:` lines, not just the first** (Boss repair — the +run emits two: the ctx readback and the `g_rc_*` atexit line; global +leak-freedom is the invariant). The helper: ```rust +#[derive(Debug)] +struct RcStats { allocs: u64, frees: u64, exit_code: i32 } + +fn build_link_run_embed(fixture: &str, host_rel: &str, extra_cc: &[&str]) -> RcStats { + // + // SUM every "ailang_rc_stats:" line (ctx readback + g_rc atexit): + let (mut allocs, mut frees) = (0u64, 0u64); + for l in stderr.lines().filter(|l| l.starts_with("ailang_rc_stats:")) { + for tok in l.split_whitespace() { + if let Some(v) = tok.strip_prefix("allocs=") { allocs += v.parse::().unwrap(); } + else if let Some(v) = tok.strip_prefix("frees=") { frees += v.parse::().unwrap(); } + } + } + RcStats { allocs, frees, exit_code: run.status.code().unwrap_or(-1) } +} + #[test] fn record_roundtrip_own_alloc_eq_free() { - // build embed_backtest_step_record.ail --emit=staticlib, - // link crates/ail/tests/embed/record_roundtrip.c (no -DBORROW), - // run with AILANG_RC_STATS=1, parse the ctx_free readback. let stats = build_link_run_embed( "embed_backtest_step_record.ail", "embed/record_roundtrip.c", &[/* no extra clang defines */], ); + // GLOBAL leak-freedom: Σallocs == Σfrees across ctx + g_rc lines. assert_eq!(stats.allocs, stats.frees, - "own: every State box freed exactly once (kernel-consumed input + host-freed return); {stats:?}"); + "own: globally leak-free — every State box freed exactly once \ + (kernel-consumed `own` inputs on ctx; host make_state/final \ + dec on g_rc); {stats:?}"); assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held"); } ``` -(The `build_link_run_embed` helper + `stats` struct shape are -whatever `embed_e2e.rs` already defines; reuse it — extract it to a -shared `mod` only if `embed_e2e.rs` does not already expose it. Do -not invent a new harness.) +(Mirror `embed_e2e.rs`'s real build/link/run; only the **multi-line +sum** is the Boss-repair delta over a single-line parse. Do not +invent a new harness; reuse `embed_e2e.rs`'s incantation verbatim.) - [ ] **Step 3: Run the `own` E2E to verify RED** @@ -790,43 +823,52 @@ ownership contract is mechanically almost free"; ratified by `crates/ail/tests/e2e.rs::alloc_rc_own_param_dec_at_fn_return:1855` — **not** `borrow_own_demo_modes_are_metadata_only`, which is an Iter-18a pre-enforcement pin and must not be cited). No production -code change is expected in this task — if `record_roundtrip_own_alloc_eq_free` -is RED for a real imbalance, that is a genuine bug: hand off to -`debug` (RED test already exists). If it is GREEN immediately once +code change is expected in this task — if the **global** +Σallocs==Σfrees is RED for a real imbalance, that is a genuine bug: +hand off to `debug` (RED test already exists). If it is GREEN once Tasks 2+3 are in the tree, that *is* the spec's "mechanically almost free" claim substantiated. Run: `cargo test -p ail --test embed_record_e2e record_roundtrip_own_alloc_eq_free -- --exact` -Expected: PASS — `allocs == frees`, exit 0. +Expected: PASS — Σallocs == Σfrees (own: ctx `live=0` + g_rc +`live=0`; the two stat lines summed), exit 0. --- ## Task 5: E2E record round-trip — `borrow` Same harness, the `-DBORROW` arm: the kernel does **not** consume the -input; the host retains and `ailang_rc_dec`s it itself. `allocs == -frees` again. Tasks 4+5 together prove "ownership follows the -declared mode" in *both* directions. +input; the host retains and `ailang_rc_dec`s it itself. **Global** +Σallocs == Σfrees again (Boss repair — *not* per-ctx-line: in borrow +the ctx line is `live=+N` and the g_rc line `live=−N`, summing to 0; +the host's decs land on g_rc because they run outside the forwarder's +TLS-ctx window — correct M2 behaviour, not a leak). Tasks 4+5 +together prove "ownership follows the declared mode" both directions, +globally leak-free. **Files:** - Modify: `crates/ail/tests/embed_record_e2e.rs` (add the borrow test) - [ ] **Step 1: Write the failing `borrow` E2E test (RED)** -In `crates/ail/tests/embed_record_e2e.rs` add: +In `crates/ail/tests/embed_record_e2e.rs` add (same multi-line-sum +`build_link_run_embed` as Task 4 — global invariant): ```rust #[test] fn record_roundtrip_borrow_alloc_eq_free() { - // same C host with -DBORROW: host frees the retained input each - // iter; kernel (borrow param) does NOT consume it. + // -DBORROW: kernel (borrow param) does NOT consume the input; + // host frees the retained input each iter + the final return. let stats = build_link_run_embed( "embed_backtest_step_record_borrow.ail", "embed/record_roundtrip.c", &["-DBORROW"], ); + // GLOBAL: ctx allocs (kernel returns) + g_rc frees (host decs) + // sum to a balanced total — Σallocs == Σfrees, Σlive == 0. assert_eq!(stats.allocs, stats.frees, - "borrow: kernel kept input; host freed every input + the return; {stats:?}"); + "borrow: globally leak-free — kernel allocs returns on ctx, \ + host frees inputs+return on g_rc; the two summed balance; {stats:?}"); assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held"); } ``` @@ -834,19 +876,22 @@ fn record_roundtrip_borrow_alloc_eq_free() { - [ ] **Step 2: Run the `borrow` E2E to verify RED then GREEN** Run: `cargo test -p ail --test embed_record_e2e record_roundtrip_borrow_alloc_eq_free -- --exact --nocapture` -Expected: FAIL first if the borrow fixture is not yet built/lowered; -then PASS once `embed_backtest_step_record_borrow.ail` builds via the -Task-2/3 path. A `borrow` param is **not** dropped by the kernel -(ratified by `crates/ail/tests/e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`), -so the host's per-iter `ailang_rc_dec(st)` is exactly what balances -`allocs == frees`. A real imbalance ⇒ genuine bug ⇒ hand to `debug`. +Expected: FAIL first if the borrow fixture is not yet built/lowered +or the harness still parses only the first stat line; then PASS once +the multi-line-sum harness is in place and +`embed_backtest_step_record_borrow.ail` builds via the Task-2/3 +path. A `borrow` param is **not** dropped by the kernel (ratified by +`crates/ail/tests/e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`); +the host's per-iter `ailang_rc_dec(st)` on g_rc is what balances the +**global** total. A real *global* imbalance ⇒ genuine bug ⇒ `debug`. - [ ] **Step 3: Both modes green together** Run: `cargo test -p ail --test embed_record_e2e` Expected: PASS, `2 passed` — `record_roundtrip_own_alloc_eq_free` -and `record_roundtrip_borrow_alloc_eq_free`. The frozen ownership -contract is **proven both ways**, not asserted. +and `record_roundtrip_borrow_alloc_eq_free`, both at global +Σallocs==Σfrees. The frozen ownership contract is **proven both +ways**, not asserted. --- diff --git a/docs/specs/2026-05-18-embedding-abi-m3.md b/docs/specs/2026-05-18-embedding-abi-m3.md index d565330..c70646e 100644 --- a/docs/specs/2026-05-18-embedding-abi-m3.md +++ b/docs/specs/2026-05-18-embedding-abi-m3.md @@ -4,6 +4,31 @@ **Status:** Draft — awaiting user spec review **Authors:** Brummel (orchestrator) + Claude +> **Boss spec-consistency repair (2026-05-18, M3.1 implement +> BLOCKED adjudication — M2.1-precedent class).** The M3.1 implement +> dispatch correctly BLOCKED on Task 5: the original §"Testing +> strategy" items 3/4 + §"Coherent stop" specified the proof +> instrument as "`ailang_ctx_free` reports `allocs == frees`", +> assuming the single ctx readback observes every RC op. That +> assumption is false **by M2's shipped design**: the ctx is bound +> to `__ail_tls_ctx` only for the duration of the synchronous +> forwarder call, so host-side `ailang_rc_dec` calls (which +> `borrow` mode legitimately requires every iteration, and `own` +> mode uses for the initial `make_state` + final return) are +> attributed to the `g_rc_*` atexit line, not the ctx line. The +> substantive invariant is sound and was empirically confirmed +> globally leak-free + value-correct for **both** modes (own: ctx +> `live=0` + g_rc `live=0`; borrow: ctx `live=+N` + g_rc +> `live=−N`; both Σ`live`=0, exit 0). The proof model below is +> corrected to **global leak-freedom** (sum across *all* +> `ailang_rc_stats:` lines: Σallocs == Σfrees, equivalently +> Σ`live`=0, plus exit 0), for both modes — strictly stronger and +> honest about the M2-TLS cross-attribution (which is correct +> behaviour, not a leak). Spec-consistency repair, not a redesign: +> what M3 delivers is unchanged; no fresh grounding-check (this +> *removes* an over-strong measurement assumption and adds no new +> assumption about current compiler/checker/codegen behaviour). + ## Goal Let a single-constructor record of `Int`/`Float` fields cross the @@ -523,15 +548,27 @@ RED-first throughout (`skills/debug` / TDD discipline). `examples/embed_backtest_step_record.ail`: host builds `State` via `ailang_rc_alloc`, calls N times, the kernel consumes each `own` input (Iter-B), the host frees the final return with - `ailang_rc_dec`, and `ailang_ctx_free` reports `allocs == frees` - (via the M2 per-ctx counters — the existing instrument). Result - value asserted (`n == N`). + `ailang_rc_dec`. **Global leak-freedom proof model:** the + harness parses *every* `ailang_rc_stats:` line the run emits + (the `ailang_ctx_free` ctx readback **and** the `g_rc_*` atexit + line) and asserts `Σallocs == Σfrees` (equivalently Σ`live` = 0) + and `exit_code == 0` (the C host's `assert(n == N)` held). Per- + ctx-line balance is **not** asserted: by M2's TLS-ctx design the + host's `make_state`/final-`dec` run outside the forwarder call + and land on `g_rc_*`, so only the *global* sum is the invariant. 4. **E2E record round-trip — `borrow`.** `examples/embed_backtest_step_record_borrow.ail`: the host retains and `ailang_rc_dec`s each input itself; the kernel does - not consume it; `allocs == frees` again. Items 3+4 together prove - "ownership follows the declared mode" in **both** directions — - the frozen contract is tested, not asserted. + not consume it (correct `borrow`, ratified by + `e2e.rs::alloc_rc_borrow_only_recursive_list_drop`). Same + **global** proof model as item 3 — Σallocs == Σfrees, exit 0. + In borrow mode the kernel allocs every return box on ctx while + the host's balancing decs land on `g_rc_*` (the ctx line shows + `live=+N`, the g_rc line `live=−N`, summing to 0): this split + attribution is **correct M2-TLS-window behaviour, not a leak**. + Items 3+4 together prove "ownership follows the declared mode" + in **both** directions, globally leak-free — tested, not + asserted. 5. **Layout byte-pin is enforcing.** The item-0(b) pin is green; a deliberate one-off offset perturbation in `lower_ctor` (local experiment, reverted) turns it RED — demonstrating the freeze is @@ -604,11 +641,14 @@ Milestone-close ("coherent stop") is met when **all** hold: - `examples/embed_backtest_step_record.ail` builds with `ail build --emit=staticlib`; the C host builds the input `State` via `ailang_rc_alloc`, calls `backtest_step` N times, reads and - `ailang_rc_dec`s the return, and `ailang_ctx_free` reports - `allocs == frees` (`own` variant — coherent-stop proof). + `ailang_rc_dec`s the return, and the run is **globally + leak-free** — Σallocs == Σfrees across every `ailang_rc_stats:` + line (Σ`live` = 0), exit 0 (`own` variant — coherent-stop proof). - The `borrow` variant (`embed_backtest_step_record_borrow.ail`, - host-retained input freed by the host) is likewise green at - `allocs == frees` — "follows the declared mode" proven both ways. + host-retained input freed by the host) is likewise globally + leak-free (Σallocs == Σfrees, exit 0; ctx `live=+N` / g_rc + `live=−N` summing to 0 — correct M2-TLS cross-attribution, not a + leak) — "follows the declared mode" proven both ways. - The gate RED trio + the re-pointed combined must-fail + the effectful fixture all fail `ail check` with precise, self-correcting diagnostics; the positive single-ctor `Float`+`Int` diff --git a/examples/embed_backtest_step_record.ail b/examples/embed_backtest_step_record.ail new file mode 100644 index 0000000..922528d --- /dev/null +++ b/examples/embed_backtest_step_record.ail @@ -0,0 +1,16 @@ +(module embed_backtest_step_record + + (data State + (ctor State (con Float) (con Int))) + + (fn step + (export "backtest_step") + (type + (fn-type + (params (own (con State)) (con Float)) + (ret (con State)))) + (params st sample) + (body + (match st + (case (pat-ctor State acc n) + (term-ctor State State (app + acc sample) (app + n 1))))))) diff --git a/examples/embed_backtest_step_record_borrow.ail b/examples/embed_backtest_step_record_borrow.ail new file mode 100644 index 0000000..7d44a5d --- /dev/null +++ b/examples/embed_backtest_step_record_borrow.ail @@ -0,0 +1,16 @@ +(module embed_backtest_step_record_borrow + + (data State + (ctor State (con Float) (con Int))) + + (fn step + (export "backtest_step") + (type + (fn-type + (params (borrow (con State)) (con Float)) + (ret (con State)))) + (params st sample) + (body + (match st + (case (pat-ctor State acc n) + (term-ctor State State (app + acc sample) (app + n 1))))))) diff --git a/examples/embed_export_adt_ret_rejected.ail b/examples/embed_export_adt_ret_rejected.ail index 986795d..3d59b13 100644 --- a/examples/embed_export_adt_ret_rejected.ail +++ b/examples/embed_export_adt_ret_rejected.ail @@ -1,11 +1,12 @@ (module embed_export_adt_ret_rejected - (data Pair - (ctor Pair (con Int) (con Int))) + (data Reading + (ctor Missing) + (ctor Sample (con Int) (con Str))) (fn f (export "f") (type (fn-type (params (con Int)) - (ret (con Pair)))) + (ret (con Reading)))) (params n) - (body (app Pair n n)))) + (body (term-ctor Reading Sample n "tick")))) diff --git a/examples/embed_export_list_field_record_rejected.ail b/examples/embed_export_list_field_record_rejected.ail new file mode 100644 index 0000000..bcb661c --- /dev/null +++ b/examples/embed_export_list_field_record_rejected.ail @@ -0,0 +1,11 @@ +(module embed_export_list_field_record_rejected + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + (data Boxed + (ctor Boxed (con Int) (con List))) + (fn f + (export "f") + (type (fn-type (params (con Int)) (ret (con Boxed)))) + (params n) + (body (term-ctor Boxed Boxed n (term-ctor List Nil))))) diff --git a/examples/embed_export_multictor_rejected.ail b/examples/embed_export_multictor_rejected.ail new file mode 100644 index 0000000..f208d2a --- /dev/null +++ b/examples/embed_export_multictor_rejected.ail @@ -0,0 +1,9 @@ +(module embed_export_multictor_rejected + (data Either2 + (ctor L (con Int)) + (ctor R (con Float))) + (fn f + (export "f") + (type (fn-type (params (con Int)) (ret (con Either2)))) + (params n) + (body (term-ctor Either2 L n)))) diff --git a/examples/embed_export_record_ok.ail b/examples/embed_export_record_ok.ail new file mode 100644 index 0000000..3083b8f --- /dev/null +++ b/examples/embed_export_record_ok.ail @@ -0,0 +1,14 @@ +(module embed_export_record_ok + (data State + (ctor State (con Float) (con Int))) + (fn step + (export "step") + (type + (fn-type + (params (own (con State)) (con Float)) + (ret (con State)))) + (params st sample) + (body + (match st + (case (pat-ctor State acc n) + (term-ctor State State (app + acc sample) (app + n 1))))))) diff --git a/examples/embed_export_str_field_record_rejected.ail b/examples/embed_export_str_field_record_rejected.ail new file mode 100644 index 0000000..81ce068 --- /dev/null +++ b/examples/embed_export_str_field_record_rejected.ail @@ -0,0 +1,8 @@ +(module embed_export_str_field_record_rejected + (data Tagged + (ctor Tagged (con Int) (con Str))) + (fn f + (export "f") + (type (fn-type (params (con Int)) (ret (con Tagged)))) + (params n) + (body (term-ctor Tagged Tagged n "x")))) diff --git a/examples/embed_record_layout_carrier.ail b/examples/embed_record_layout_carrier.ail new file mode 100644 index 0000000..625ce31 --- /dev/null +++ b/examples/embed_record_layout_carrier.ail @@ -0,0 +1,30 @@ +(module embed_record_layout_carrier + + (data Pt + (ctor Pt (con Int) (con Int))) + + (fn mk + (type + (fn-type + (params (con Int) (con Int)) + (ret (con Pt)))) + (params a b) + (body (term-ctor Pt Pt a b))) + + (fn sum_pt + (type + (fn-type + (params (own (con Pt))) + (ret (con Int)))) + (params p) + (body + (match p + (case (pat-ctor Pt x y) + (app + x y))))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let s (app int_to_str (app sum_pt (app mk 3 4))) + (do io/print_str s)))))