spec: embedding-abi-m5 — ail-embed adapter + data-server wiring + thread-swarm backtest

User-approved 2026-05-19; grounding-check PASS (all load-bearing
assumptions are already-shipped M3 ABI behaviour, each pinned by a
green non-ignored integration test: embed_tick_e2e own+borrow,
embed/tick_roundtrip.c, embed_staticlib_cli, embed_swarm_tsan,
embed_staticlib_alloc_guard). Terminal embedding milestone, zero
language/compiler/runtime change — ail-embed is a lean reusable
embedding module (Rust port of the audited tick_roundtrip.c) + the
real E2E; in-repo, [workspace]-excluded so the compiler workspace
owes nothing to ../libs/data-server or /mnt (Invariant 1 in the
dependency graph, not just on paper). Real data-server + real
Pepperstone ticks; symbol-fan headline + time-shard
boundary-invisibility proof (per-shard bit-exact; whole-window only
within f64-reassociation tolerance — self-review fix).

roadmap: M5 [ ]->[~] open in-flight, spec pointer added, dangling
"todo above" dependency reconciled to shipped 170464f; M4-retired
and Tick-coverage struck/done entries pruned (their own text
scheduled deletion at next-milestone-start; permanent rationale
survives in 2026-05-18-brainstorm-embedding-abi-m4-retired.md, still
pointed to by M5's context line). Mirrors the M3 1fbb9c4 precedent
(spec + roadmap-flip in one commit).
This commit is contained in:
2026-05-19 00:52:38 +02:00
parent 208d7095bc
commit ae905de00c
2 changed files with 386 additions and 44 deletions
+23 -44
View File
@@ -304,50 +304,29 @@ work progresses.
`docs/journals/2026-05-18-audit-embedding-abi-m3.md`;
`docs/journals/2026-05-18-iter-embedding-abi-m3.tidy.md`.
- **\[milestone — RETIRED 2026-05-18, never speced\]** Embedding ABI
— M4: sequence crossing via the `List` ADT. Struck during its own
brainstorm Q&A, before any spec: failed feature-acceptance
clause 2. The minimal data-server binding is M3 (shipped) + a
host-side per-tick loop over each chunk's records —
`(State, Tick) -> State` is *already* gate-accepted and
forwarder-supported under M3 (the gate loop accepts each record
param independently; the forwarder maps each to `ptr`). Cons-list
crossing would *add* a 2N+1-box-per-chunk host builder plus the
deferred flat-array perf debt rather than remove redundancy, and
builds something no named consumer needs (M5's adapter unrolls
the chunk host-side; whole-chunk in-kernel visibility buys nothing
`State` threads across calls regardless of chunk boundaries).
Removed (not `[x]` — never shipped); rationale in the journal.
Stays one cycle for context, then delete.
- context: `docs/journals/2026-05-18-brainstorm-embedding-abi-m4-retired.md`.
- [x] **\[todo\]** Tick-coverage on M3 — DONE 2026-05-18 (`170464f`).
E2E + fixtures pinning the two-record-param per-tick crossing
`(State, Tick) -> State` on the shipped M3 ABI (`own` + `borrow`
Tick, globally leak-free, Boss-verified both tests green on HEAD;
zero language change — independently re-confirms the M4-retirement
reasoning). Surfaced a conservative `[over-strict-mode]` advisory
false-positive (nested-`match` scrutinee; non-gating, exit 0) —
recorded as a separate finding, not silenced (fixtures kept
LLM-natural). Stays one cycle for context, then delete.
- context: `docs/journals/2026-05-18-brainstorm-embedding-abi-m4-retired.md`;
commit `170464f`.
- [ ] **\[milestone\]** Embedding ABI — M5: `ail-embed` adapter +
`data-server` wiring + thread-swarm backtest (fieldtest
target). The host-side adapter crate (sole meeting point of
`data-server` and AILang, per Invariant 1) wires
`data-server`'s `while let next_chunk` loop to the AILang
kernel via the M3 ABI by **unrolling each chunk host-side** into
per-tick `(State, Tick) -> State` calls (M4's cons-list crossing
was retired — see above; the adapter, not the kernel, owns chunk
iteration); an actual small backtest runs over a thread swarm.
Natural `fieldtest` milestone: existence proof of the whole goal
+ friction harvest feeding the host-per-tick-FFI vs. batch-
crossing perf decision (the P2 flat-array item). Coherent stop:
the goal itself.
- depends on: Embedding ABI — M3; Tick-coverage on M3 (todo above).
- context: 2026-05-18 chat; M4 retirement
- [~] **\[milestone\]** Embedding ABI — M5: `ail-embed` adapter +
`data-server` wiring + thread-swarm backtest. **In-flight**: spec
written + user-approved + grounding-check PASS 2026-05-19. The
host-side adapter — a lean reusable embedding module (`extern "C"`
to the M3-frozen ABI + frozen-layout box helpers, zero finance
knowledge) **plus** the real E2E on top; in-repo but
`[workspace]`-excluded; sole `data-server`↔AILang meeting point
(Invariant 1) — wires the **real external** `data-server`'s
`while let next_chunk` loop to the shipped M3 kernel by
**unrolling each chunk host-side** into per-tick
`(State, Tick) -> State` calls (the adapter, not the kernel, owns
chunk iteration; M4's cons-list crossing was retired). **Zero
language/compiler/runtime change.** A real backtest runs over real
Pepperstone tick data on a thread swarm: symbol-fan (headline) +
time-shard (first actual proof of the chunk-boundary invisibility
the M4 retirement rests on). Terminal embedding milestone:
existence proof of the whole goal + friction harvest feeding the
host-per-tick-FFI vs. batch-crossing perf decision (the P2
flat-array item). Coherent stop: the goal itself.
- depends on: Embedding ABI — M3 (shipped); Tick-coverage on M3
(shipped `170464f`).
- context: `docs/specs/2026-05-19-embedding-abi-m5.md`;
M4 retirement
`docs/journals/2026-05-18-brainstorm-embedding-abi-m4-retired.md`.
- [x] **\[milestone\]** Heap-`Str` ABI — runtime infrastructure for
+363
View File
@@ -0,0 +1,363 @@
# Embedding ABI — M5: `ail-embed` adapter + `data-server` wiring + thread-swarm backtest — Design Spec
**Date:** 2026-05-19
**Status:** Draft — awaiting user spec review
**Authors:** Brummel (orchestrator) + Claude
## Goal
Prove the whole embedding arc end-to-end against the **real** target
host: stream real Pepperstone tick data through the real external
`data-server` crate into the **already-shipped, M3-frozen** AILang
kernel, across a thread swarm of independent per-thread embedding
contexts, and harvest the host-per-tick-FFI friction that feeds the
later P2 batch-crossing perf decision.
M5 is the **terminal** embedding milestone. M4 (cons-list crossing)
was retired; nothing follows M5 in this arc. Its value is exactly
two things, both stated in the roadmap:
1. **Existence proof of the whole goal** — a real backtest runs over
a real data-server stream on a real thread swarm via the frozen
M3 ABI, leak-free and sanitiser-clean.
2. **Friction harvest** — honest, at real data scale, feeding the
host-per-tick-FFI-vs-batch-crossing perf decision (the P2
flat-array roadmap item).
**M5 ships zero language/compiler/runtime change.** No schema,
checker, codegen, `runtime/`, or `examples/*.ail` edit. The M3 ABI is
frozen and already sufficient: the kernel `(State, Tick) -> State`
two-record-param per-tick crossing is gate-accepted, forwarder-
supported, and E2E-pinned both `own` and `borrow` (commit `170464f`).
The only AILang artefact M5 consumes is the already-shipped
`examples/embed_backtest_step_tick.ail`. M5 is host-side code +
wiring + the proof.
## Architecture
Three things, in dependency order. None of `ailang-core`,
`ailang-check`, `ailang-codegen`, `crates/ail`, or `runtime/` is
touched — **Invariant 1** (the compiler crates gain no
`data-server`/finance knowledge or dependency) is preserved not only
in letter but in the dependency graph, and is audited at close.
1. **`ail-embed` — a lean, reusable AILang-kernel embedding module.**
`extern "C"` declarations against the M3-frozen ABI
(`ailang_ctx_new`/`ailang_ctx_free`, `ailang_rc_alloc`,
`ailang_rc_dec`, the author-exported `backtest_step_tick`), plus
frozen-value-layout box read/write helpers and safe `State`/`Tick`
wrappers. **Zero finance/`data-server` knowledge.** It is the Rust
analogue of the already-audited C host
`crates/ail/tests/embed/tick_roundtrip.c` — the same frozen-layout
`make_state`/`make_tick`/read-back, the same `own`-mode contract —
exposed as a small safe API instead of an inline test loop. It is
**not** a published crate with a stability contract and implies
**no** successor milestone; its correctness is proven by the (b)
E2E below, not by an API-versioning promise.
2. **`data-server` wiring (the adapter layer of `ail-embed`).** The
only place that knows *both* sides. It maps the rich
`data_server::records::TickParsed { time_ms, ask, bid }` to the
single scalar the M3 `Tick` record carries — `px = (ask + bid) /
2.0`, the mid price — and drives the per-tick fold by *unrolling
each `Arc<[TickParsed]>` chunk host-side* into per-tick
`(State, Tick) -> State` calls. The adapter, not the kernel, owns
chunk iteration (the M4-retirement decision: chunk boundaries are
a host artefact, semantically invisible to the fold).
3. **The thread-swarm backtest (the E2E proof + friction harvest).**
N worker threads, each with its own `ailang_ctx_t`, each folding
the shipped kernel over a data-server stream, in the two shapes
the user selected ("volle Möhre"):
- **Symbol-fan (headline).** One distinct symbol per thread; each
thread's `(acc, n)` checked against a single-thread host
reference fold for that symbol. This is data-server's own
stated concurrency design ("designed to back hundreds of
single-threaded VMs in parallel" — one symbol per VM).
- **Time-shard (second assertion).** One symbol, N threads each a
disjoint month-window. Boundary-invisibility is proven **per
shard, bit-exact**: each shard's `(acc, n)` equals a
single-thread host fold of *that exact window* in stream order
— the kernel's result for a window is independent of how
`data-server` chunked it. The host then sums the partials; the
*same* summation over the reference partials matches bit-exact
by construction. The whole-window single-thread total is a
*secondary* cross-check with an f64-reassociation tolerance
(cross-shard re-association is expected host arithmetic, **not**
a kernel property — asserting it bit-exact would be wrong).
The per-shard bit-exact equality *is* the first actual proof of
the chunk/window-boundary-invisibility claim the entire M4
retirement rests on.
### Topology / Invariant 1 (orchestrator decision, not a user fork)
`ail-embed/` lives **in the AILang repo but excluded from the
`[workspace]`** — its own `Cargo.toml`, built and tested explicitly.
Substantive reason (not effort): the compiler workspace
(`cargo build/test --workspace`) then owes nothing to
`../libs/data-server` or `/mnt/tickdata` — Invariant 1 holds in the
dependency graph, not just on paper — while the *sole consumer of the
frozen ABI* stays co-versioned and co-audited with the ABI it binds,
which is precisely the protection the M3 freeze exists to provide.
(Rejected: workspace member — couples the compiler's own CI to an
external sibling dir + a 6 GB data mount; out-of-repo crate —
sacrifices the co-audit the freeze is for.)
`ail-embed` depends on `data-server` via a path dependency
(`../libs/data-server`); the README also documents a git source. The
path dep is the in-repo-dev choice and is the meeting point Invariant
1 names.
## Concrete code shapes
### The AILang program M5 delivers (headline)
M5 delivers **no new `.ail`**. The delivered AILang program is the
already-shipped, M3-frozen kernel it consumes —
`examples/embed_backtest_step_tick.ail`, verbatim:
```
(module embed_backtest_step_tick
(data State (ctor State (con Float) (con Int)))
(data Tick (ctor Tick (con Float)))
(fn step
(export "backtest_step_tick")
(type (fn-type
(params (own (con State)) (own (con Tick)))
(ret (con State))))
(params st tick)
(body
(match st
(case (pat-ctor State acc n)
(match tick
(case (pat-ctor Tick px)
(term-ctor State State (app + acc px) (app + n 1)))))))))
```
`acc += px; n += 1` over the per-tick mid price ⇒ the run's result
is `(Σ mid, tick-count)`, i.e. the mean mid price over the window —
a real, exactly-verifiable backtest aggregate.
**No new must-fail fixture.** The feature-acceptance clause-3
discriminator ("wrong code fails to typecheck") is already owned by
the M3 export gate (`export-non-scalar-signature`,
`export-has-effects`); M5 adds no checker/codegen change, so there is
no new wrong-code obligation. The three-clause feature-acceptance
criterion gates *language features*; M5 ships none, so it is N/A in
form. The discipline that *was* applied is the same M4-lesson
skepticism turned on the **deliverable shape**: "does a host author
need a named reusable embedding crate, or is that speculative infra?"
— resolved to a lean module whose correctness the real E2E proves,
not a speculative published API (see Decisions).
The frozen box layout the kernel crosses (DESIGN.md §"Frozen value
layout", M3 one-way commitment):
- `State`: payload `8 + 2*8` = 24 bytes — `tag:i64 @0`,
`acc:f64 @8`, `n:i64 @16`.
- `Tick`: payload `8 + 1*8` = 16 bytes — `tag:i64 @0`, `px:f64 @8`.
- 8-byte rc header at `p-8` (set to 1 by `ailang_rc_alloc`,
payload zeroed). `own` ⇒ kernel consumes both inputs; the return
is host-owned and host-freed via `ailang_rc_dec`.
### Implementation shape (secondary — supporting, not the point)
The lean embedding module — Rust port of the audited
`tick_roundtrip.c` helpers, exposed as a safe API:
```rust
// ail-embed/src/lib.rs (no finance knowledge)
#[repr(transparent)] pub struct Ctx(*mut c_void); // !Send by default
unsafe extern "C" {
fn ailang_ctx_new() -> *mut c_void;
fn ailang_ctx_free(c: *mut c_void);
fn ailang_rc_alloc(n: usize) -> *mut c_void; // header=1, payload zeroed
fn ailang_rc_dec(p: *mut c_void);
fn backtest_step_tick(c: *mut c_void, st: *mut c_void,
tick: *mut c_void) -> *mut c_void;
}
impl Ctx {
pub fn new() -> Self { Self(unsafe { ailang_ctx_new() }) }
/// State box: tag@0=0, acc:f64@8, n:i64@16 (frozen M3 layout).
fn make_state(acc: f64, n: i64) -> *mut c_void { /* ailang_rc_alloc(24) + writes */ }
/// Tick box: tag@0=0, px:f64@8 (frozen M3 layout).
fn make_tick(px: f64) -> *mut c_void { /* ailang_rc_alloc(16) + write */ }
/// One fold step. `own`: kernel consumes st+tick; returns new owned State.
pub fn step(&self, st: *mut c_void, px: f64) -> *mut c_void {
unsafe { backtest_step_tick(self.0, st, Self::make_tick(px)) }
}
}
impl Drop for Ctx { fn drop(&mut self) { unsafe { ailang_ctx_free(self.0) } } }
```
The adapter + per-thread fold (the only code that knows `data-server`):
```rust
// the worker body, one per thread, own ctx:
let ctx = Ctx::new();
let mut st = Ctx::make_state(0.0, 0);
let mut it = server.stream_tick_windowed(symbol, from_ms, to_ms).unwrap();
while let Some(chunk) = it.next_chunk() { // data-server's loop
for r in chunk.iter() { // host-side unroll
let px = (r.ask + r.bid) / 2.0; // adapter's job
st = ctx.step(st, px); // M3 ABI, per tick
}
}
let (acc, n) = read_state(st); ailang_rc_dec(st); // host-owned return
```
`ail-embed/build.rs` invokes the `ail` CLI to emit the staticlib and
links it (mirrors `embed_tick_e2e.rs:61-78` verbatim, but from a
workspace-excluded crate): resolve the `ail` binary via an `AIL_BIN`
env override else `cargo build -p ail` against the parent AILang
workspace; run `ail build examples/embed_backtest_step_tick.ail
--emit=staticlib -o <OUT_DIR>`; emit `cargo:rustc-link-search` +
`-l static=embed_backtest_step_tick` + `-l static=ailang_rt`.
## Components
| Component | Role | Knows data-server? | Knows ABI? |
|---|---|---|---|
| `ail-embed/build.rs` | emit + link the M3 staticlib | no | symbol names only |
| `ail-embed` core (`Ctx`, box helpers) | frozen-layout FFI, safe wrappers | **no** | yes (the only crate that does) |
| `ail-embed` adapter (`tick→px`, fold driver) | `TickParsed``Tick`, chunk unroll | **yes (sole site)** | via core |
| swarm E2E (symbol-fan + time-shard + hermetic smoke) | the proof + friction harvest | yes | via core |
| `examples/embed_backtest_step_tick.ail` | the delivered kernel (unchanged) | no | it *is* the ABI source |
## Data flow
`DataServer::new(path)``Arc` → per worker thread:
`stream_tick_windowed(symbol, win)``SymbolChunkIter`
`while let next_chunk()` yields `Arc<[TickParsed]>`
host unroll: each `TickParsed``px=(ask+bid)/2``make_tick` box →
`backtest_step_tick(ctx, st, tick)` (kernel consumes `st`+`tick`,
returns new owned `State`) → thread `st` forward → end-of-stream:
read `(acc, n)`, `ailang_rc_dec(st)`, `ctx` dropped (`ailang_ctx_free`
`AILANG_RC_STATS` ctx readback). Symbol-fan: per-thread `(acc,n)`
vs per-symbol host reference (bit-exact, same stream order).
Time-shard: each shard's `(acc,n)` vs a single-thread host fold of
that exact window (bit-exact); host-summed `(Σacc,Σn)` vs the
identically-summed reference partials (bit-exact by construction);
whole-window single-thread total as a tolerance cross-check only.
## Error handling
- `stream_tick*` returns `None` for an unknown symbol or an empty
window → the adapter surfaces a typed error to the harness, never a
panic *inside* a kernel call (a half-threaded `State` must not
leak; on the error path the current `st` is `ailang_rc_dec`'d
before unwinding).
- The frozen-layout contract (`ailang_rc_alloc`, never raw `malloc`;
fixed offsets) is **enforced by construction**: `make_state` /
`make_tick` are the only box constructors and there is no public
way to hand the kernel a raw pointer.
- `own` discipline: each `Tick` is freshly `ailang_rc_alloc`'d per
call and consumed by the kernel; `st` is consumed and replaced by
the return each step; only the final return is host-`dec`'d. This
is the `tick_roundtrip.c` contract, unchanged.
- Real data absent (`/mnt/tickdata/Pepperstone` missing): the
real-data swarm tests **skip gracefully**, mirroring
`data-server`'s own `tests/data_server.rs::skip_if_no_data()`
precedent — consistency with the wired crate's own convention, not
an ad-hoc gate. The hermetic smoke test still runs and still
proves the wiring/ABI handshake.
## Testing strategy
Three layers; the regression/leak posture mirrors the M1/M2/M3
global-leak-freedom proof (`AILANG_RC_STATS`, Σallocs == Σfrees
across all stat lines; sanitiser-clean).
1. **Hermetic smoke (always green, no `/mnt`).** A test-only writer
emits the documented 24-byte packed `RawTickRecord` layout
(`{time:f64 Delphi-day, ask:f64, bid:f64}`) into a ZIP'd
`SYM_YYYY_MM.tick` in a `tempfile::tempdir()`, points the **real**
`DataServer::new(tempdir)` at it, runs a single-thread fold, and
asserts `(acc, n)` equals a host reference fold over the same
synthetic ticks. Proves "adapter compiles, links, ABI handshake
holds" independent of real data — a genuinely different failure
mode from "real data present". This is also data-server's own
tempdir-fixture unit discipline.
2. **Symbol-fan swarm (headline existence proof; skip-if-absent).** N
threads, one liquid symbol each (default spine `EURUSD`; planner
enumerates from what is present, e.g. `EURUSD`/`XAUUSD`), bounded
window (default order-of one month per thread — enough real
volume to surface per-tick-FFI friction, ~seconds runtime), each
own `ailang_ctx_t`. Each thread's `(acc, n)` == single-thread host
reference fold for that symbol/window. Globally leak-free,
sanitiser-clean.
3. **Time-shard swarm (boundary-invisibility proof; skip-if-absent).**
One symbol, N threads each a disjoint month-window. Assert, in
order of strength: (a) each shard's `(acc,n)` == a single-thread
host fold of *that exact window* in stream order, **bit-exact**
this is the boundary-invisibility proof (the kernel result for a
window is independent of data-server's chunking); (b) the
host-summed `(Σacc,Σn)` == the identically-summed reference
partials, bit-exact by construction; (c) the whole-window
single-thread total within an f64-reassociation tolerance only
(cross-shard re-association is host arithmetic, not a kernel
property). The M4-retirement claim's first actual proof is (a).
Friction harvest: the swarm runs are timed; the per-tick-FFI cost at
real tick volume is recorded in the close-out journal as the input to
the P2 batch-crossing decision (observation, not a perf gate — no
bench baseline is moved by M5).
## Acceptance criteria
- `git diff` after M5 touches **only** `ail-embed/**`, `Cargo.toml`
(the `[workspace] exclude`/non-membership note if needed), docs,
and the per-iter journal/stats. **Zero** diff to
`crates/ailang-*`, `crates/ail/`, `runtime/`, `examples/*.ail`.
Mechanically checkable; this *is* the no-language-change +
Invariant-1 guarantee.
- The hermetic smoke test passes everywhere (no `/mnt`, no
`../libs/data-server` data files needed beyond the crate itself).
- On this machine (real data present): the symbol-fan swarm and the
time-shard swarm both pass — symbol-fan per-thread `(acc,n)`
bit-exact vs the same-order single-thread reference; time-shard
per-shard `(acc,n)` bit-exact vs a single-thread fold of that
exact window and the host-summed partials bit-exact by
construction (whole-window total only within f64-reassociation
tolerance) — globally leak-free (`AILANG_RC_STATS` Σallocs ==
Σfrees), sanitiser-clean (TSan: no data race across the per-thread
ctxs).
- Where real data is absent, the two swarm tests skip (not fail),
mirroring `data-server`'s own precedent.
- The architect audit at close confirms Invariant 1 (no
finance/`data-server` symbol or dependency in any compiler crate or
`runtime/`) and that the M3 frozen-layout SSOT is unmoved.
- The close-out journal records the measured per-tick-FFI cost at
real volume as the P2 perf-decision input.
### Decisions (forks resolved during this brainstorm)
- **What is `data-server`** → the real external crate at
`/home/brummel/dev/libs/data-server` (not a synthetic mock); real
data at `/mnt/tickdata/Pepperstone` (6.3 GB).
- **Test-data strategy** → real-data swarm is the headline proof +
friction harvest (skip-if-absent per data-server's own
`skip_if_no_data()`); tiny hermetic synthetic-format fixture is the
always-green floor. Real-as-opt-in was rejected: it would gut the
harvest, which is only honest at real scale.
- **What is `ail-embed`** → a lean reusable embedding module +
the real E2E on top (Option 2). Not "real E2E only" (the frozen
ABI was *designed* to be bound generically — the module is the
artefact the freeze is for); not two published crates (speculative
infra, implies successor milestones the arc does not have).
- **Topology** → in-repo, `[workspace]`-excluded (orchestrator
decision; Invariant-1/build-hygiene reason above).
- **Swarm shape** → both symbol-fan (headline) and time-shard
(boundary-invisibility second assertion) — user choice "3, volle
Möhre".
### Out of scope / known pre-existing drift (not M5's job)
DESIGN.md §"Frozen value layout" still calls a recursive typed-free
for boxed-field records "an additive M4 concern" (`docs/DESIGN.md`
~:2358-2360). M4 is retired; this is stale doc-honesty drift already
flagged by the M4-retirement journal's forward note as
reconcile-when-touched. M5 does not touch it and must not be charged
with it at audit; noted here so the architect sees it is pre-existing,
not M5-introduced.