test(embed): pin two-record-param per-tick (State, Tick) -> State on the shipped M3 ABI
Coverage backfill for an already-shipped capability — NO language / checker / codegen / schema / runtime change (4 new files, all under examples/ and crates/ail/tests/). Property protected: the M3 export gate is_c_abi_type runs as a per-parameter loop, accepting a single-ctor all-scalar record independently per param; the staticlib forwarder maps every non-scalar Type::Con to a bare ptr (M3-frozen). So a kernel (State, Tick) -> State with BOTH params single-ctor all-scalar records is callable from C today — a record Tick pushed per call, not just a scalar sample. Every shipped M3 fixture pushes a scalar Float; none pinned the two-record-param shape (the actual minimal data-server binding). This is the residual of the retired M4. Added: - examples/embed_backtest_step_tick.ail (own Tick) - examples/embed_backtest_step_tick_borrow.ail (borrow Tick) - crates/ail/tests/embed/tick_roundtrip.c (C host, -DBORROW) - crates/ail/tests/embed_tick_e2e.rs (2 E2E tests) Both E2E tests pass on HEAD (Boss-verified, not just agent-claimed): own + borrow, globally leak-free (Sigma allocs == Sigma frees across the ctx readback + g_rc atexit lines, the M3 dual-stat-line model), acc/n value-correct, exit 0. Independently re-confirms the M4 retirement reasoning: the capability is genuinely present in M3. Honest, deliberately NOT silenced: the new fixtures emit an advisory [over-strict-mode] warning (ail check still exits 0, non-gating) that the M3 scalar-sample original does not. Root cause characterized: a conservative over-strict-mode false-positive whose discriminator is the nested second (match tick ...) — structurally identical `st` handling warns when its term-ctor rebuild is nested inside an inner match. It is advisory only and does not affect codegen, the ABI, or the proven property. The fixture is kept in its LLM-natural form (dont-adapt-tests-to-bugs); the lint precision wart is surfaced as a separate finding, not papered over.
This commit is contained in:
@@ -0,0 +1,75 @@
|
||||
/* Embedding-ABI M3 two-record-param round-trip C host (own + borrow
|
||||
* via a compile-time -DBORROW switch). Backfill: M3 shipped fixtures
|
||||
* only ever push a *scalar* per-tick sample; this host pushes a
|
||||
* single-ctor all-scalar *record* `Tick` as the per-call payload —
|
||||
* the actual minimal data-server binding shape. Frozen value layout
|
||||
* (DESIGN.md §"Embedding ABI" > "Frozen value layout"):
|
||||
*
|
||||
* State (24-byte payload):
|
||||
* 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
|
||||
* Tick (8-byte payload):
|
||||
* 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 px
|
||||
*
|
||||
* own : the kernel consumes BOTH `(own (con State))` and
|
||||
* `(own (con Tick))` inputs (drop at return); the host must NOT
|
||||
* touch/dec either after the call.
|
||||
* borrow: `State` is `(own ...)` (kernel-consumed, as own); `Tick` is
|
||||
* `(borrow (con Tick))` — the kernel does NOT consume it; the
|
||||
* host retains the Tick and dec's it itself each iter.
|
||||
* In both modes the return is host-owned and host-freed.
|
||||
*/
|
||||
#include <stdint.h>
|
||||
#include <assert.h>
|
||||
#include <string.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
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_tick(ailang_ctx_t *ctx, void *st, void *tick);
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
static void *make_tick(double px) {
|
||||
void *p = ailang_rc_alloc(8 + 1 * 8); /* header=1 set by runtime */
|
||||
*(int64_t *)((char *)p + 0) = 0; /* single-ctor tag = 0 */
|
||||
memcpy((char *)p + 8, &px, 8); /* Float px @ 8 */
|
||||
return p;
|
||||
}
|
||||
|
||||
int main(void) {
|
||||
ailang_ctx_t *ctx = ailang_ctx_new();
|
||||
void *st = make_state(0.0, 0);
|
||||
double expected = 0.0;
|
||||
for (int i = 0; i < 1000000; i++) {
|
||||
double px = (double)(i & 7);
|
||||
expected += px;
|
||||
void *tick = make_tick(px);
|
||||
void *next = backtest_step_tick(ctx, st, tick);
|
||||
#ifdef BORROW
|
||||
ailang_rc_dec(tick); /* borrow: host retained Tick, frees it */
|
||||
#endif
|
||||
/* own: kernel consumed `st` AND `tick`; do NOT dec them 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);
|
||||
assert(acc == expected);
|
||||
ailang_rc_dec(st); /* host frees the final return */
|
||||
ailang_ctx_free(ctx); /* AILANG_RC_STATS readback fires here */
|
||||
return 0;
|
||||
}
|
||||
@@ -0,0 +1,158 @@
|
||||
//! Embedding-ABI M3 two-record-param round-trip — coverage backfill
|
||||
//! for an already-shipped capability (NO language/checker/codegen
|
||||
//! change; these tests pass on HEAD by design — that is the proof).
|
||||
//!
|
||||
//! Named property protected: the M3 export gate accepts a
|
||||
//! single-constructor all-scalar record *independently per parameter*
|
||||
//! (`crates/ailang-check/src/lib.rs:1953` — `is_c_abi_type` in a
|
||||
//! `for p in ¶m_tys` loop), and the staticlib forwarder maps every
|
||||
//! non-scalar `Type::Con` to a bare `ptr` (M3-frozen). Therefore a
|
||||
//! kernel `(State, Tick) -> State` where BOTH params are single-ctor
|
||||
//! all-scalar records is callable from a C host today — a record
|
||||
//! `Tick` pushed per call, not just a scalar sample. Every shipped M3
|
||||
//! fixture pushes a *scalar* `Float`; none pinned the two-record-param
|
||||
//! per-tick shape (the actual minimal data-server binding). This does.
|
||||
//!
|
||||
//! `own` (no -DBORROW): the kernel consumes BOTH `(own (con State))`
|
||||
//! and `(own (con Tick))` inputs (drop at return); the host's
|
||||
//! `make_state`/`make_tick` + final `dec` land on `g_rc_*`.
|
||||
//! `borrow` (-DBORROW): `Tick` is `(borrow (con Tick))` — the kernel
|
||||
//! does NOT consume it; the host retains and dec's each Tick itself.
|
||||
//! Both prove "ownership follows the declared mode" — pinned for the
|
||||
//! *Tick* record param both ways, mirroring the M3 `_borrow.ail`
|
||||
//! precedent.
|
||||
//!
|
||||
//! The build/link incantation + dual-stat-line global proof mirrors
|
||||
//! `embed_record_e2e.rs` verbatim (M2 TLS-ctx binds the ctx only for
|
||||
//! the synchronous forwarder call, so host-side allocs/decs land on
|
||||
//! `g_rc_*`, not ctx; the invariant is GLOBAL Σallocs == Σfrees
|
||||
//! across *all* stat lines, not per-ctx-line balance).
|
||||
|
||||
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 `<fixture>` as a staticlib, link `<host_rel>` (under
|
||||
/// `crates/ail/tests/`) with `extra_cc` flags, run under
|
||||
/// `AILANG_RC_STATS=1`, and return the summed RC-stats 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-tick-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);
|
||||
// GLOBAL leak-freedom (mirrors embed_record_e2e.rs): the run emits
|
||||
// TWO `ailang_rc_stats:` lines — the `ailang_ctx_free` ctx readback
|
||||
// AND the `g_rc_*` atexit line. M2's TLS-ctx binds the ctx only for
|
||||
// the synchronous forwarder call, so the host's `make_state` /
|
||||
// `make_tick` / per-iter `dec` / final `dec` land on `g_rc_*`. The
|
||||
// invariant is Σallocs == Σfrees across *all* stat lines
|
||||
// (equivalently Σ`live` = 0) — not per-ctx-line balance.
|
||||
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::<u64>().expect("allocs= u64");
|
||||
} else if let Some(v) = tok.strip_prefix("frees=") {
|
||||
frees += v.parse::<u64>().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 two-record-param: a `(own (con State), own (con Tick)) ->
|
||||
/// State` kernel is callable from C today — the export gate accepts
|
||||
/// the second single-ctor all-scalar record param independently, and
|
||||
/// the forwarder lowers BOTH to `ptr`. Globally leak-free: every
|
||||
/// State and Tick box freed exactly once (kernel-consumed inputs on
|
||||
/// ctx; host `make_state`/`make_tick`/final `dec` on `g_rc_*`),
|
||||
/// Σallocs == Σfrees across both stat lines, and the C host's
|
||||
/// `assert(n == 1000000) && assert(acc == Σ prices)` held (exit 0).
|
||||
#[test]
|
||||
fn tick_roundtrip_own_alloc_eq_free() {
|
||||
let stats = build_link_run_embed(
|
||||
"embed_backtest_step_tick.ail",
|
||||
"embed/tick_roundtrip.c",
|
||||
&[],
|
||||
);
|
||||
assert_eq!(stats.allocs, stats.frees,
|
||||
"own two-record-param: globally leak-free — Σallocs == Σfrees \
|
||||
across the ctx readback + g_rc atexit lines (kernel-consumed \
|
||||
State+Tick on ctx; host make_state/make_tick/final dec on \
|
||||
g_rc); {stats:?}");
|
||||
assert_eq!(stats.exit_code, 0,
|
||||
"C host assert(n==1000000 && acc==Σ prices) held");
|
||||
}
|
||||
|
||||
/// borrow Tick param: with `Tick` declared `(borrow (con Tick))` the
|
||||
/// kernel does NOT consume it — ownership follows the declared mode
|
||||
/// for a *record* param, the second direction of the M3 `_borrow`
|
||||
/// precedent. The host retains and dec's each Tick itself. Globally
|
||||
/// leak-free: ctx line shows kernel return allocs (live=+N), g_rc the
|
||||
/// host input/Tick/return decs (live=−N), summing to 0 — correct
|
||||
/// M2-TLS cross-attribution, not a leak. Σallocs == Σfrees across
|
||||
/// both lines. Same host, `-DBORROW`.
|
||||
#[test]
|
||||
fn tick_roundtrip_borrow_alloc_eq_free() {
|
||||
let stats = build_link_run_embed(
|
||||
"embed_backtest_step_tick_borrow.ail",
|
||||
"embed/tick_roundtrip.c",
|
||||
&["-DBORROW"],
|
||||
);
|
||||
assert_eq!(stats.allocs, stats.frees,
|
||||
"borrow Tick: globally leak-free — Σallocs == Σfrees across the \
|
||||
ctx readback (kernel return allocs, live=+N) + g_rc atexit \
|
||||
(host State/Tick/return decs, live=−N); summed they balance; \
|
||||
{stats:?}");
|
||||
assert_eq!(stats.exit_code, 0,
|
||||
"C host assert(n==1000000 && acc==Σ prices) held");
|
||||
}
|
||||
@@ -0,0 +1,21 @@
|
||||
(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)))))))))
|
||||
@@ -0,0 +1,21 @@
|
||||
(module embed_backtest_step_tick_borrow
|
||||
|
||||
(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)) (borrow (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)))))))))
|
||||
Reference in New Issue
Block a user