fieldtest: embedding-abi-m1 — 4 examples, 4 findings (0 bug, 1 friction, 2 spec_gap, 3 working)

Surface-touch fieldtest of M1's (export "<sym>") + --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).
This commit is contained in:
2026-05-18 15:27:12 +02:00
parent 425c4eb3c5
commit 6a4e8669a3
5 changed files with 311 additions and 0 deletions
+17
View File
@@ -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)))))
@@ -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))))
@@ -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)))))))
@@ -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)))))