From 6a4e8669a3157e6b9836f375ef178eb11224ffed Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 18 May 2026 15:27:12 +0200 Subject: [PATCH] =?UTF-8?q?fieldtest:=20embedding-abi-m1=20=E2=80=94=204?= =?UTF-8?q?=20examples,=204=20findings=20(0=20bug,=201=20friction,=202=20s?= =?UTF-8?q?pec=5Fgap,=203=20working)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Surface-touch fieldtest of M1's (export "") + --emit=staticlib + scalar/effect-free gate. DESIGN.md + public examples only (no compiler source). The M1 thesis is empirically substantiated: - [working] Int EMA + Float leaky-integrator both first-try clean end-to-end (author -> --emit=staticlib -> C link -> typed scalar return; s==67 / s==1.875, exit 0). Clause-1 confirmed. - [working] Both clause-3 rejections precise + self-correcting (export-non-scalar-signature on IntList param; export-has-effects on !IO). Clause-3 confirmed. - [working] (export) orthogonality + zero-export staticlib guard match spec. - [friction] form_a.md 'wrap every param in own/borrow' misdirects the headline scalar export -> body-pointing use-after-consume / consume-while-borrowed; only bare (con Int) checks. Pre-existing form_a.md defect M1 made acute (not introduced). - [spec_gap] form_a.md item 1 unconditional; scalar params take no mode (shares root with the friction). - [spec_gap] no public emit-ir --emit=staticlib though Decision 5 makes kernel-IR readability load-bearing. Boss verified independently via the public CLI (positive E2E builds both archives; both rejections fire the documented codes). 0 bugs: M1 capability + gate sound. Findings route to the roadmap as follow-up (not M1-blocking, no debug). --- .../2026-05-18-fieldtest-embedding-abi-m1.md | 231 ++++++++++++++++++ examples/fieldtest/embabi1_1_ema_step.ail | 17 ++ .../fieldtest/embabi1_2_leaky_integrator.ail | 16 ++ .../embabi1_3_export_list_rejected.ail | 25 ++ ...babi1_4_export_logged_counter_rejected.ail | 22 ++ 5 files changed, 311 insertions(+) create mode 100644 docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md create mode 100644 examples/fieldtest/embabi1_1_ema_step.ail create mode 100644 examples/fieldtest/embabi1_2_leaky_integrator.ail create mode 100644 examples/fieldtest/embabi1_3_export_list_rejected.ail create mode 100644 examples/fieldtest/embabi1_4_export_logged_counter_rejected.ail diff --git a/docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md b/docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md new file mode 100644 index 0000000..962f6e4 --- /dev/null +++ b/docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md @@ -0,0 +1,231 @@ +# Fieldtest — embedding-abi-m1 — 2026-05-18 + +**Status:** Draft — awaiting orchestrator triage +**Author:** ailang-fieldtester (dispatched by skills/fieldtest) + +## Scope + +Embedding ABI M1 makes a compiled AILang scalar `fn` callable +in-process from a C/Rust host. It adds the Form-A `(export "")` +fn modifier, an additive `FnDef.export: Option` schema field, +a new `ail build --emit=staticlib` mode that produces a relocatable +`lib.a` (program objects only) plus a separate +`libailang_rt.a`, a typecheck-time export gate (`Int`/`Float` params +& return, empty effect set — codes `export-non-scalar-signature`, +`export-has-effects`), and a DESIGN.md §"Embedding ABI (M1)" that +labels the M1 C signature provisional until M3. No +ADT/record/list/`Str`/effect crosses the boundary in M1. + +## Examples + +### `examples/fieldtest/embabi1_1_ema_step.ail` — fixed-point EMA accumulator (Int positive axis) +- **What it does:** `ema_step(state, sample) = state + (sample - state)/4`, + a fixed-point exponential moving average; the `(State, Sample) -> + State` accumulator a host drives one sample per call. +- **Why it fits:** this is exactly the positive authoring axis — a + pure numeric fold made callable from a C host loop, the headline + M1 use case. +- **Outcome:** authored from DESIGN.md §"Embedding ABI (M1)" + + `crates/ailang-core/specs/form_a.md` + the public + `embed_backtest_step.ail` form. `ail check` → `ok` first try. + `ail build --emit=staticlib -o /tmp/ft1` → produced + `libembabi1_1_ema_step.a` + `libailang_rt.a`. A 4-call C host + (`cc host.c lib*.a libailang_rt.a`) linked and ran; `s == 67` + assertion held; exit 0. **Compiles, links, runs, matches.** + +### `examples/fieldtest/embabi1_2_leaky_integrator.ail` — leaky integrator (Float scalar-coverage axis) +- **What it does:** `leaky_step(state, sample) = state*0.5 + sample` + over `Float`; the Float counterpart of example 1. +- **Why it fits:** the optional scalar-coverage axis — exercises the + other M1 scalar type (`Float` → C `double`) through the same + author → build → C-call path. +- **Outcome:** `ail check` → `ok` first try. + `ail build --emit=staticlib` → two archives. C host with + `extern double leaky_step(double, double)` linked and ran; exact + `s == 1.875` assertion held; exit 0. **Compiles, links, runs, + matches.** Author experience byte-for-byte identical to the Int + axis. + +### `examples/fieldtest/embabi1_3_export_list_rejected.ail` — list-param export (rejection axis, non-scalar) +- **What it does:** an `IntList`-folding `sum_chunk` carrying + `(export "sum_chunk")` — the imperative-trained "pass the whole + batch in" reflex. +- **Why it fits:** the clause-3 rejection axis — a non-scalar + signature an author would naturally try and that M1 must reject at + `ail check`. +- **Outcome:** `ail check` → exit 1, single diagnostic (verbatim + below). **Correctly rejected; diagnostic is self-correcting.** + +### `examples/fieldtest/embabi1_4_export_logged_counter_rejected.ail` — effectful export (rejection axis, effects-only) +- **What it does:** `tick(n) = n + 1` with a `(do io/print_str + "tick")` trace line; signature is fully scalar `(Int)->Int` but the + effect set is `!IO`. +- **Why it fits:** isolates the `export-has-effects` clause from the + non-scalar clause (the public `embed_export_effectful_rejected.ail` + mixes `Str` param + `IO`; this one is scalar-clean so only the + effect clause can fire). +- **Outcome:** `ail check` → exit 1, single `export-has-effects` + diagnostic. **Correctly rejected; diagnostic is self-correcting.** + +## Findings + +### [working] Positive scalar authoring (Int and Float) is first-try clean end-to-end +- **Examples:** 1, 2. +- **What happened:** With only DESIGN.md §"Embedding ABI (M1)", + `form_a.md`, the public `embed_*` corpus, and `ail … --help`, both + the Int and the Float `(State,Sample)->State` folds were authored, + checked, built as `staticlib`, linked from a hand-written C host, + and run with the asserted return holding — first try, no re-roll, + no guessing on the AILang side. The `(export "")` modifier + position (after `(export …)` in the `(fn …)` head, before + `(type …)`) and the C scalar mapping (`Int`→`int64_t`, + `Float`→`double`) were both unambiguous from DESIGN.md + form_a.md. + The two-archive output (`lib.a` + `libailang_rt.a`) and the + `-o`-is-a-directory rule were learned from `ail build --help` + (public surface) and matched DESIGN.md's prose. The C symbol being + author-chosen (`ema_step` / `leaky_step`, decoupled from the + `ail__` mangling) worked exactly as documented. +- **Why working:** the new surface was reached for naturally, used, + and correct on first try with no diagnostic needed. This is the + capability the milestone exists to deliver, proven from the + downstream-author position. +- **Recommended action:** carry-on. + +### [working] Both clause-3 rejection diagnostics are precise and self-correcting +- **Examples:** 3, 4. +- **What happened, verbatim:** + - Ex 3: `error: [export-non-scalar-signature] sum_chunk: export + \`sum_chunk\`: M1 embedding ABI is scalar-only — parameter type + \`IntList\` is not \`Int\`/\`Float\`` (exit 1). + - Ex 4: `error: [export-has-effects] tick: export \`tick\` must be + pure — declared effects !["IO"] are not allowed on an embedding + boundary` (exit 1). + Each names the code, the fn, the C symbol, the specific offending + position (the parameter *type*; the *effect set*), the rule, and + (for non-scalar) the allowed types. An author with no compiler + access can self-correct from the message alone: "make the param + scalar" / "remove the effect / drop the trace line". +- **Why working:** clause-3 ("wrong code fails to typecheck, with a + message you can act on") is the load-bearing acceptance criterion + for this strategic milestone, and it holds empirically with + high-quality diagnostics. +- **Recommended action:** carry-on. + +### [working] `(export)` orthogonality + zero-export staticlib guard behave exactly as spec'd +- **Examples:** out-of-fixture probes (recorded for completeness; + no fixture kept — these are spec-conformance confirmations). +- **What happened:** (a) a module with `(export "…")` on a fn plus a + real `main`, built/run in default exe mode, checked `ok` and ran + with no diagnostic about the inert `(export)` — matches the spec's + "accepted and ignored" clause. (b) `ail build --emit=staticlib` on + a module with zero `(export)` fns → `Error: staticlib target needs + at least one \`(export "")\` fn` (exit 1) — matches the spec's + zero-export guard wording. +- **Why working:** confirms the field's orthogonality and + error-path promises hold from the CLI surface. +- **Recommended action:** carry-on. + +### [friction] The published authoring rule steers an LLM away from the only spelling that works for scalar export params +- **Examples:** 1, 2 (succeeded *because* I followed the public + `embed_backtest_step.ail` fixture, not the prose rule); probes + with `(own (con Int))` / `(borrow (con Int))` (failed). +- **What happened:** `crates/ailang-core/specs/form_a.md` "Schema + invariants" item 1 states: "Every type in the `(params …)` clause + of a `(fn …)` definition's `(fn-type …)` **MUST** be wrapped in + `(own T)` or `(borrow T)`. … Implicit mode on a `(fn …)` def is + rejected." The Pitfalls section repeats: "Wrap **every** `(fn …)` + parameter in `(own …)` or `(borrow …)`." An LLM author reading + form_a.md before generating (its stated purpose) would write the + M1 export as `(params (own (con Int)) (own (con Int)))`. That + yields, verbatim: + `error: [use-after-consume] step: \`sample\` is used after it was + already consumed` (the scalar is read twice in `sample*sample`). + Switching to `(borrow (con Int))` instead yields three + `error: [consume-while-borrowed] step: \`…\` is consumed while a + borrow of it is still live`. The *only* spelling that checks is + bare `(con Int)` — precisely the spelling form_a.md item 1 and the + Pitfalls bullet tell the author is "rejected" / must be wrapped. + The headline M1 deliverable is "an LLM, asked to make a scalar + fold callable, writes the export"; the published authoring spec + the LLM consults first actively misdirects that exact task, and + the resulting `use-after-consume` / `consume-while-borrowed` + diagnostics point at the body, not at the real cause (scalars + must not carry a mode). +- **Why friction:** it compiles and runs once the author copies the + public fixture's bare-scalar form, but the documented authoring + rule forces a wrong first attempt and an unrelated-looking + linearity diagnostic — exactly the re-roll cost form_a.md claims to + remove. M1 did not introduce scalar-mode behaviour but made it + acute: this is now the surface of the milestone's headline task. +- **Recommended action:** plan (tidy iteration) — reconcile + `form_a.md` item 1 + the Pitfalls bullet with actual behaviour by + stating the scalar-type carve-out for *parameters* (form_a.md + already carves the *return* type for non-heap-shaped types; the + symmetric parameter carve-out is missing). DESIGN.md + §"Embedding ABI (M1)" should also show the canonical export param + spelling so the M1 author has an authoritative bare-scalar example + outside the example corpus. + +### [spec_gap] form_a.md mandates a mode on every fn param; scalar params accept (and require) no mode — the doc is unqualified +- **Examples:** non-exported probe `(fn plain (params (con Int) (con + Int)) …)` → `ail check` `ok` exit 0. +- **What happened:** the friction above has a doc-level root that is + not export-specific: `form_a.md` "Schema invariants" item 1 is + written as an unconditional universal ("MUST be wrapped … Implicit + mode on a `(fn …)` def is rejected"). Behaviour: a *plain* + non-exported fn with bare `(con Int)` params checks `ok`. So the + published invariant overstates the rule for scalar parameter + positions, with no stated exemption (the return-type sentence + carves out `Int`/`Bool`/`Unit`/`Str` for *returns* only). An LLM + author cannot derive the true rule ("scalars take no mode; + heap-shaped params take `own`/`borrow`") from the public docs — + it has to be reverse-engineered from the example corpus, which the + Iron Law explicitly forbids treating as a behaviour oracle. +- **Why spec_gap:** the canonical authoring spec does not constrain + the case correctly; two readings (literal "every param needs a + mode" vs. corpus-implied "scalars are bare") are both supportable + from the public text, and the compiler picks the second. +- **Recommended action:** tighten `form_a.md` (and mirror the rule + in DESIGN.md if DESIGN.md is silent on scalar-param modes) — state + the scalar-parameter carve-out symmetrically with the existing + return-type carve-out. This is the doc fix that subsumes the + friction finding's first half. + +### [spec_gap] No public path emits the staticlib IR, though DESIGN.md Decision 5 makes IR readability a first-class LLM affordance +- **Examples:** `ail emit-ir examples/fieldtest/embabi1_1_ema_step.ail` + → `Error: entry module \`embabi1_1_ema_step\` has no \`main\` def` + (exit 1). +- **What happened:** DESIGN.md (Decision 5 / "the compiler emits + LLVM IR as text so the LLM can read what it generated") establishes + reading generated IR as an intended author affordance, and the M1 + spec/DESIGN.md describe the precise staticlib IR shape (`@` + forwarder beside the unchanged `@ail__`, no `@main`). + But `ail emit-ir --help` shows only `-o` — there is **no** + `--emit=staticlib` flag on `emit-ir` (only `ail build` has it). + Running `emit-ir` on a `main`-free kernel hits the executable-path + `MissingEntryMain` rejection. An author who wants to verify the + generated forwarder for an exported kernel — the exact thing + Decision 5 says they should be able to do — has no documented way + to obtain that `.ll`. Whether `ail build` leaves an intermediate + `.ll` is not derivable from any public source and was not + inferred from compiler internals (Iron Law); the absence of the + affordance via the documented `emit-ir` surface is the finding. +- **Why spec_gap:** DESIGN.md asserts an affordance the M1 surface + does not provide for the artefact M1 introduces; neither DESIGN.md + nor `--help` resolves how an author inspects a kernel's IR. +- **Recommended action:** ratify the intended behaviour — either add + `--emit=staticlib` to `ail emit-ir` (symmetry with `ail build`) or + add one sentence to DESIGN.md §"Embedding ABI (M1)" stating how a + kernel's IR is obtained (e.g. a documented `ail build` artefact). + Orchestrator triage: `ratify` vs. tighten DESIGN.md. + +## Recommendation summary + +| Finding | Class | Action | +|---|---|---| +| Positive Int+Float authoring first-try clean E2E | working | carry-on | +| Both clause-3 rejection diagnostics precise & self-correcting | working | carry-on | +| `(export)` orthogonality + zero-export guard match spec | working | carry-on | +| form_a.md mode rule misdirects the headline export task | friction | plan (tidy iteration) | +| form_a.md "every param needs a mode" unqualified vs. scalar behaviour | spec_gap | tighten `form_a.md` / DESIGN.md | +| No public path emits the staticlib kernel IR vs. Decision 5 | spec_gap | ratify or tighten DESIGN.md | diff --git a/examples/fieldtest/embabi1_1_ema_step.ail b/examples/fieldtest/embabi1_1_ema_step.ail new file mode 100644 index 0000000..2af04be --- /dev/null +++ b/examples/fieldtest/embabi1_1_ema_step.ail @@ -0,0 +1,17 @@ +(module embabi1_1_ema_step + + ; Fixed-point exponential moving average, one sample per call. + ; alpha = 1/4: new = old + (sample - old) / 4 + ; The host drives this in a loop, one chunk-sample at a time, + ; carrying `state` across calls — the (State, Sample) -> State + ; accumulator the embedding boundary exists for. + (fn ema_step + (export "ema_step") + (type + (fn-type + (params (con Int) (con Int)) + (ret (con Int)))) + (params state sample) + (body + (app + state + (app / (app - sample state) 4))))) diff --git a/examples/fieldtest/embabi1_2_leaky_integrator.ail b/examples/fieldtest/embabi1_2_leaky_integrator.ail new file mode 100644 index 0000000..fdf2acc --- /dev/null +++ b/examples/fieldtest/embabi1_2_leaky_integrator.ail @@ -0,0 +1,16 @@ +(module embabi1_2_leaky_integrator + + ; Leaky integrator over Float samples, one sample per host call: + ; new = state * 0.5 + sample + ; This is the Float-scalar counterpart of the Int EMA fold — + ; same (State, Sample) -> State host-driven accumulator shape, + ; exercising the other M1 scalar type across the C boundary. + (fn leaky_step + (export "leaky_step") + (type + (fn-type + (params (con Float) (con Float)) + (ret (con Float)))) + (params state sample) + (body + (app + (app * state 0.5) sample)))) diff --git a/examples/fieldtest/embabi1_3_export_list_rejected.ail b/examples/fieldtest/embabi1_3_export_list_rejected.ail new file mode 100644 index 0000000..8f3c368 --- /dev/null +++ b/examples/fieldtest/embabi1_3_export_list_rejected.ail @@ -0,0 +1,25 @@ +(module embabi1_3_export_list_rejected + + ; An imperative-trained author, asked "export the aggregate so the + ; host can call it on a whole batch", naturally reaches for a list + ; parameter — pass the whole chunk in, get the sum out. M1's + ; embedding ABI is scalar-only, so this MUST fail `ail check` + ; (export-non-scalar-signature). Kept verbatim: the rejection is + ; the finding. + + (data IntList + (ctor Nil) + (ctor Cons (con Int) (con IntList))) + + (fn sum_chunk + (export "sum_chunk") + (type + (fn-type + (params (own (con IntList))) + (ret (con Int)))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) + (app + h (app sum_chunk t))))))) diff --git a/examples/fieldtest/embabi1_4_export_logged_counter_rejected.ail b/examples/fieldtest/embabi1_4_export_logged_counter_rejected.ail new file mode 100644 index 0000000..6d1ba2a --- /dev/null +++ b/examples/fieldtest/embabi1_4_export_logged_counter_rejected.ail @@ -0,0 +1,22 @@ +(module embabi1_4_export_logged_counter_rejected + + ; The signature is fully scalar (Int -> Int) — the author got the + ; ABI types right. But, debugging the host integration, they drop + ; a trace line into the accumulator body. That makes the fn + ; effectful (!IO), which M1 forbids for an embedding boundary. + ; This isolates the export-has-effects clause from the + ; non-scalar-signature clause (the public fixture mixes both). + ; MUST fail `ail check`. Kept verbatim: the rejection is the + ; finding. + + (fn tick + (export "tick") + (type + (fn-type + (params (con Int)) + (ret (con Int)) + (effects IO))) + (params n) + (body + (seq (do io/print_str "tick") + (app + n 1)))))