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:
@@ -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.
|
||||
Reference in New Issue
Block a user