AILang/crates/ail/tests/embed_record_e2e.rs

//! Embedding-ABI M3 record round-trip (spec §"Testing strategy" —
//! coherent-stop proof, both ownership directions). Build the record
//! kernel as a staticlib, link the C host (frozen `{tag@0, double
//! acc@8, int64 n@16}` layout, `make_state` via `ailang_rc_alloc`),
//! run with `AILANG_RC_STATS=1`, and assert the `ailang_ctx_free`
//! RC-stats readback shows kernel-internal `allocs == frees` and the
//! C host's `assert(n == 1000000)` held (exit 0).
//!
//! `own` (no -DBORROW): the kernel consumes each `(own (con State))`
//! input (drop at return — ratified by
//! `crates/ail/tests/e2e.rs::alloc_rc_own_param_dec_at_fn_return:1855`,
//! NOT `borrow_own_demo_modes_are_metadata_only` which is an Iter-18a
//! pre-enforcement metadata-only pin) and allocates the new return.
//! `borrow` (-DBORROW, Task 5): the kernel does NOT consume the
//! `(borrow (con State))` input (ratified by
//! `…::alloc_rc_borrow_only_recursive_list_drop:1671`); the host
//! retains and dec's it each iter. Both prove "ownership follows the
//! declared mode" — the frozen contract proven both ways.
//!
//! The build/link incantation mirrors `embed_e2e.rs`
//! (`ail build --emit=staticlib -o <dir>` → `cc host.c
//! lib<module>.a libailang_rt.a`); the stats-line parse mirrors
//! `e2e.rs::build_and_run_with_rc_stats` (the runtime's fixed
//! `ailang_rc_stats: allocs=N frees=M live=K` shape).

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 `ailang_ctx_free` 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-record-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);
    // Boss spec-consistency repair (2026-05-18, M3.1 BLOCKED
    // adjudication): the run emits TWO `ailang_rc_stats:` lines —
    // the `ailang_ctx_free` ctx readback AND the `g_rc_*` atexit
    // line. By M2's TLS-ctx design the ctx is bound to TLS only for
    // the synchronous forwarder call, so the host's `make_state` /
    // per-iter `dec` / final `dec` (which run outside any forwarder
    // call) land on `g_rc_*`, not ctx. The invariant is GLOBAL
    // leak-freedom: Σallocs == Σfrees across *all* stat lines
    // (equivalently Σ`live` = 0) — not per-ctx-line balance. Sum
    // every line; a missing-line panic guards against zero parsed.
    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: globally leak-free — every State box freed exactly once.
/// The `(own (con State))` input is drop-consumed at the kernel's
/// return (Iter-B, on ctx); the host's `make_state` + final `dec`
/// land on `g_rc_*`. Σallocs == Σfrees across both stat lines
/// (own: ctx `live=0` + g_rc `live=0`), and the C host's
/// `assert(n == 1000000)` held.
#[test]
fn record_roundtrip_own_alloc_eq_free() {
    let stats = build_link_run_embed(
        "embed_backtest_step_record.ail",
        "embed/record_roundtrip.c",
        &[],
    );
    assert_eq!(stats.allocs, stats.frees,
        "own: globally leak-free — Σallocs == Σfrees across the ctx \
         readback + g_rc atexit lines (kernel-consumed `own` inputs \
         on ctx; host make_state/final dec on g_rc); {stats:?}");
    assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held");
}

/// borrow: globally leak-free. The kernel does NOT consume the
/// `(borrow (con State))` input (ratified by
/// `crates/ail/tests/e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`);
/// it allocs every return box on ctx, the host frees every input +
/// the final return on `g_rc_*` (outside the forwarder's TLS-ctx
/// window). The ctx line shows `live=+N`, the g_rc line `live=−N`,
/// summing to 0 — correct M2-TLS cross-attribution, not a leak.
/// Σallocs == Σfrees across both lines. Same harness, `-DBORROW`.
/// With Task 4 this proves "ownership follows the declared mode" in
/// both directions, globally leak-free — proven, not asserted.
#[test]
fn record_roundtrip_borrow_alloc_eq_free() {
    let stats = build_link_run_embed(
        "embed_backtest_step_record_borrow.ail",
        "embed/record_roundtrip.c",
        &["-DBORROW"],
    );
    assert_eq!(stats.allocs, stats.frees,
        "borrow: globally leak-free — Σallocs == Σfrees across the ctx \
         readback (kernel return allocs, live=+N) + g_rc atexit \
         (host input/return decs, live=−N); summed they balance; {stats:?}");
    assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held");
}