1080 lines
45 KiB
Markdown
1080 lines
45 KiB
Markdown
# Embedding ABI — M3.1 — Implementation Plan
|
|
|
|
> **Parent spec:** `docs/specs/2026-05-18-embedding-abi-m3.md`
|
|
>
|
|
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
|
|
> to run this plan. Steps use `- [ ]` checkboxes for tracking.
|
|
|
|
**Goal:** Let a single-constructor record of `Int`/`Float` fields
|
|
cross the embedding C boundary in and out, ownership following the
|
|
declared `own`/`borrow` mode, with the record memory layout frozen
|
|
(byte-pinned) and the alloc==free contract proven for both modes.
|
|
|
|
**Architecture:** Three layers change. (1) `ailang-check` — the
|
|
nested export-gate predicate `is_c_scalar` becomes `is_c_abi_type`:
|
|
accept `Int`/`Float` **or** a `Type::Con` resolving (via the in-scope
|
|
`env.types`) to a single-constructor `data` whose every field is a
|
|
bare `Int`/`Float` (two-level, NOT deep — a record-typed field stays
|
|
rejected = M4). (2) `ailang-codegen` — `fn_scalar_sig`/`llvm_scalar`
|
|
widen so a record type maps to `ptr`; the M2 `Target::StaticLib`
|
|
forwarder body is byte-unchanged (a record is a bare `ptr`; all
|
|
mode-driven RC stays in the byte-unchanged internal
|
|
`@ail_<mod>_<fn>`). (3) docs+pins — DESIGN.md §"Embedding ABI" gains
|
|
a frozen value-layout SSOT, "provisional until M3" becomes one-way
|
|
freeze, and the heap box layout codegen emits is byte-pinned with
|
|
lockstep comment pointers from the three encoding sites.
|
|
|
|
**Tech Stack:** `crates/ailang-check` (gate), `crates/ailang-codegen`
|
|
(forwarder + box-layout sites), `runtime/rc.c` (layout comment),
|
|
`docs/DESIGN.md` (frozen SSOT), `examples/*.ail` (fixtures),
|
|
`crates/ail/tests` (E2E C-host harness), `crates/ailang-codegen/tests`
|
|
(byte-pin + forwarder-IR pin).
|
|
|
|
---
|
|
|
|
## Files this plan creates or modifies
|
|
|
|
- Test: `crates/ailang-check/tests/embed_export_gate.rs:31-34` — `adt_ret_export_rejected` (the deliberate re-point target; baseline-confirmed Task 1, re-pointed Task 2)
|
|
- Create: `crates/ailang-codegen/tests/embed_record_layout_pin.rs` — heap-box byte-pin (`@ailang_rc_alloc(i64 24)` + tag@0 + field offsets) for a single-ctor 2-scalar-field record (Task 1)
|
|
- Create: `examples/embed_record_layout_carrier.ail` — minimal today-valid non-export program that heap-allocates a single-ctor `(Int,Int)` record, the byte-pin carrier (Task 1)
|
|
- Modify: `crates/ailang-check/src/lib.rs:1921-1924` — `is_c_scalar` → `is_c_abi_type` (Task 2)
|
|
- Modify: `crates/ailang-check/src/lib.rs:1925-1940` — gate param/ret loop calls `is_c_abi_type(ty, env)` (Task 2)
|
|
- Modify: `crates/ailang-check/src/lib.rs:452` / `:458` — widen the two `#[error(...)]` message strings (Task 2)
|
|
- Modify: `examples/embed_export_adt_ret_rejected.ail` — content replacement: single-ctor `Pair` → multi-ctor + `Str`-field `Reading` (Task 2)
|
|
- Create: `examples/embed_export_str_field_record_rejected.ail` — single-ctor record, one `Str` field (Task 2)
|
|
- Create: `examples/embed_export_list_field_record_rejected.ail` — single-ctor record, one `List` field (Task 2)
|
|
- Create: `examples/embed_export_multictor_rejected.ail` — 2-ctor all-scalar sum (Task 2)
|
|
- Create: `examples/embed_export_record_ok.ail` — single-ctor `(Float,Int)` record export, the positive (Task 2)
|
|
- Test: `crates/ailang-check/tests/embed_export_gate.rs` — add 4 RED + 1 positive test fns (Task 2)
|
|
- Modify: `crates/ailang-codegen/src/lib.rs:659-669` — `fn_scalar_sig` accepts a record param/ret (Task 3)
|
|
- Modify: `crates/ailang-codegen/src/lib.rs:673-678` — `llvm_scalar` maps a record `Type::Con` → `"ptr"` (Task 3)
|
|
- Create: `examples/embed_backtest_step_record.ail` — north-star `(own (con State))` `(State,Float)->State` (Task 3)
|
|
- Create: `examples/embed_backtest_step_record_borrow.ail` — `(borrow (con State))` variant (Task 3)
|
|
- Test: `crates/ailang-codegen/tests/embed_staticlib_lowering.rs` — add `staticlib_record_forwarder_is_ptr_passthrough` (Task 3)
|
|
- Create: `crates/ail/tests/embed/record_roundtrip.c` — the C host (own + borrow, compile-time `MODE` switch) (Task 4/5)
|
|
- Create: `crates/ail/tests/embed_record_e2e.rs` — builds libs, links the C host, runs, asserts `allocs==frees` + value (Task 4/5)
|
|
- Modify: `docs/DESIGN.md:2280-2282` / `:2293-2295` — "provisional until M3" → one-way-freeze wording (Task 6)
|
|
- Modify: `docs/DESIGN.md:2317` — insert the frozen value-layout SSOT subsection before `## Data model` (`:2319`) (Task 6)
|
|
- Modify: `runtime/rc.c:28-44` — add the lockstep-pointer line to the layout comment (Task 6)
|
|
- Modify: `crates/ailang-codegen/src/match_lower.rs:107` / `:123-126` / `:128-136` — add `// FROZEN ABI` lockstep comment at the size/tag/field encoders (Task 6)
|
|
- Modify: `crates/ailang-codegen/src/drop.rs:88` / `:113` — add `// FROZEN ABI` lockstep comment at the tag-load / field-offset encoders (Task 6)
|
|
- Modify: `crates/ailang-codegen/src/lib.rs:178` — rustdoc "provisional until M3" → frozen (Task 6)
|
|
- Modify: `crates/ailang-core/src/ast.rs:211` — rustdoc "provisional until M3" → frozen (Task 6)
|
|
|
|
---
|
|
|
|
## Task 1: Prerequisite baseline pins (FIXED FIRST — spec §"Iteration sequencing")
|
|
|
|
Both load-bearing M3 changes (the gate widen and the layout freeze)
|
|
must rest on a baseline pinned at their own layer *before* the change
|
|
(spec §"Iteration sequencing"; 2026-05-11 failure class pre-empted).
|
|
This task introduces **no** behaviour change — only baselines.
|
|
|
|
**Files:**
|
|
- Test: `crates/ailang-check/tests/embed_export_gate.rs:31-34`
|
|
- Create: `examples/embed_record_layout_carrier.ail`
|
|
- Create: `crates/ailang-codegen/tests/embed_record_layout_pin.rs`
|
|
|
|
- [ ] **Step 1: Confirm the re-point baseline pin is green TODAY**
|
|
|
|
The pin M3 deliberately re-points already exists
|
|
(`adt_ret_export_rejected`, `crates/ailang-check/tests/embed_export_gate.rs:31-34`,
|
|
asserting `examples/embed_export_adt_ret_rejected.ail` yields code
|
|
`"export-non-scalar-signature"`). Confirm it is green on the current
|
|
tree as the baseline.
|
|
|
|
Run: `cargo test -p ailang-check --test embed_export_gate adt_ret_export_rejected -- --exact`
|
|
Expected: PASS, `1 passed` (it asserts the single-ctor `Pair` ADT
|
|
return is rejected *today* — the M1 "any ADT rejected" meaning).
|
|
|
|
- [ ] **Step 2: Annotate the pin as the deliberate re-point target**
|
|
|
|
In `crates/ailang-check/tests/embed_export_gate.rs`, immediately
|
|
above the `adt_ret_export_rejected` test fn (`:31`), add this comment
|
|
so Task 2's change to it is reviewed-explicit, not a silent inversion
|
|
(spec §"Testing strategy" item 0(a)):
|
|
|
|
```rust
|
|
// M3 RE-POINT (deliberate, reviewed — spec 2026-05-18-embedding-abi-m3
|
|
// §"must-fail axis"): the fixture this asserts on
|
|
// (embed_export_adt_ret_rejected.ail) is single-ctor two-Int = M3-VALID.
|
|
// Task 2 re-points the fixture to a genuinely-still-rejected ADT
|
|
// (multi-ctor + Str field). This pin's *meaning* changes from
|
|
// "any ADT rejected" to "non-M3-shaped ADT rejected"; it is NOT
|
|
// silently inverted — the rejection (export-non-scalar-signature)
|
|
// stays asserted, on a fixture that still genuinely fails it.
|
|
```
|
|
|
|
- [ ] **Step 3: Run the gate suite to confirm the comment is inert**
|
|
|
|
Run: `cargo test -p ailang-check --test embed_export_gate`
|
|
Expected: PASS, `6 passed` (comment-only change; the existing six
|
|
tests `str_param_export_rejected`, `adt_ret_export_rejected`,
|
|
`io_export_rejected`, `combined_effectful_export_rejected_on_signature_first`,
|
|
`scalar_pure_export_passes`, `headline_int_export_passes` all green).
|
|
|
|
- [ ] **Step 4: Write the byte-pin carrier fixture**
|
|
|
|
Create `examples/embed_record_layout_carrier.ail` — a today-valid
|
|
(pre-M3, no `(export)`) program whose `main` heap-allocates a
|
|
single-ctor two-`Int` record so the standard escaping `lower_ctor`
|
|
heap path (`@ailang_rc_alloc`, the path a crossing M3 record takes)
|
|
emits its box. Grounded against `examples/borrow_own_demo.ail`
|
|
(`(data … (ctor …))`, `(match … (case (pat-ctor …) …))`, `print`):
|
|
|
|
```
|
|
(module embed_record_layout_carrier
|
|
|
|
(data Pt
|
|
(ctor Pt (con Int) (con Int)))
|
|
|
|
(fn mk
|
|
(type
|
|
(fn-type
|
|
(params (con Int) (con Int))
|
|
(ret (con Pt))))
|
|
(params a b)
|
|
(body (app Pt a b)))
|
|
|
|
(fn sum_pt
|
|
(type
|
|
(fn-type
|
|
(params (own (con Pt)))
|
|
(ret (con Int))))
|
|
(params p)
|
|
(body
|
|
(match p
|
|
(case (pat-ctor Pt x y)
|
|
(app + x y)))))
|
|
|
|
(fn main
|
|
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
|
(params)
|
|
(body
|
|
(app print (app sum_pt (app mk 3 4))))))
|
|
```
|
|
|
|
- [ ] **Step 5: Verify the carrier compiles and emits the heap box TODAY**
|
|
|
|
Run: `cargo run -q --bin ail -- check examples/embed_record_layout_carrier.ail`
|
|
Expected: exit 0, no diagnostics.
|
|
|
|
Run: `cargo run -q --bin ail -- emit-ir examples/embed_record_layout_carrier.ail -o /tmp/m3_carrier.ll && grep -nE 'ailang_rc_alloc\(i64 24\)|store i64 0, ptr|getelementptr inbounds i8, ptr .* i64 8|getelementptr inbounds i8, ptr .* i64 16' /tmp/m3_carrier.ll`
|
|
Expected: matches present — `call ptr @ailang_rc_alloc(i64 24)` (size
|
|
= 8 header-excluded payload? — confirm: `match_lower.rs:107`
|
|
`size_bytes = 8 + n*8`; for n=2 that is `8 + 16 = 24`), a
|
|
`store i64 0, ptr` (tag at offset 0), and the field GEPs at i64 8 /
|
|
i64 16. (If the heap path is not taken — escape analysis kept it in
|
|
`alloca` — adjust the carrier so `Pt` provably escapes: returning it
|
|
from `mk` and consuming via `own`-param `sum_pt` forces the heap
|
|
box; this is why `mk`/`sum_pt` are split. Confirm the `@ailang_rc_alloc`
|
|
form is what appears; the byte-pin asserts that exact form.)
|
|
|
|
- [ ] **Step 6: Write the heap-box byte-pin test**
|
|
|
|
Create `crates/ailang-codegen/tests/embed_record_layout_pin.rs`,
|
|
modelled exactly on the harness shape of
|
|
`crates/ailang-codegen/tests/embed_staticlib_lowering.rs`
|
|
(`lower_workspace`/`emit-ir` → `ir.contains(...)`; open that file and
|
|
mirror its workspace-load + lower incantation verbatim, substituting
|
|
the carrier fixture). Assert the **frozen heap layout as codegen
|
|
emits it today**:
|
|
|
|
```rust
|
|
//! FROZEN ABI byte-pin — see DESIGN.md §"Embedding ABI" frozen layout.
|
|
//! Pins the heap (@ailang_rc_alloc) box layout a boundary-crossing
|
|
//! single-ctor scalar record takes: size = 8 + n*8, tag i64 @ offset
|
|
//! 0, fields i64-strided from offset 8. Goes RED if codegen moves an
|
|
//! offset — the M3 freeze made enforceable, not aspirational.
|
|
|
|
// <mirror embed_staticlib_lowering.rs's load+lower helper here:
|
|
// load examples/embed_record_layout_carrier.ail, lower to IR string `ir`>
|
|
|
|
#[test]
|
|
fn heap_box_layout_is_frozen_8_plus_n_times_8_tag_at_0_fields_from_8() {
|
|
let ir = lower_carrier_ir(); // the mirrored helper
|
|
// Pt has 2 Int fields → payload size 8 (tag) + 2*8 (fields) = 24
|
|
assert!(ir.contains("@ailang_rc_alloc(i64 24)"),
|
|
"frozen: heap box payload size = 8 + n*8 (n=2 → 24); IR:\n{ir}");
|
|
// constructor tag written at offset 0 (single-ctor → 0; no elision)
|
|
assert!(ir.contains("store i64 0, ptr"),
|
|
"frozen: ctor tag i64 at offset 0; IR:\n{ir}");
|
|
// field 0 at offset 8, field 1 at offset 16 (i64-strided from 8)
|
|
assert!(ir.contains("getelementptr inbounds i8, ptr") && ir.contains("i64 8"),
|
|
"frozen: field 0 at payload offset 8; IR:\n{ir}");
|
|
assert!(ir.contains("i64 16"),
|
|
"frozen: field 1 at payload offset 16 (8 + 1*8); IR:\n{ir}");
|
|
}
|
|
```
|
|
|
|
(Exact `contains` substrings must be tightened to what
|
|
`/tmp/m3_carrier.ll` actually shows in Step 5 — copy the literal
|
|
emitted forms; do not assert a guessed shape. The four asserted
|
|
facts — size 24, tag@0, field@8, field@16 — are the frozen layout.)
|
|
|
|
- [ ] **Step 7: Run the byte-pin GREEN on the current (pre-M3) tree**
|
|
|
|
Run: `cargo test -p ailang-codegen --test embed_record_layout_pin -- --exact heap_box_layout_is_frozen_8_plus_n_times_8_tag_at_0_fields_from_8`
|
|
Expected: PASS, `1 passed` — the layout baseline is pinned *before*
|
|
any M3 change attaches the freeze lockstep (spec §"Testing strategy"
|
|
item 0(b)).
|
|
|
|
---
|
|
|
|
## Task 2: Widen the export gate to a single-ctor scalar record
|
|
|
|
`is_c_scalar` (a nested local fn in `check_fn`, one caller — the gate
|
|
itself; recon-confirmed no other caller, fully contained) becomes
|
|
`is_c_abi_type`, **two-level**: a bare `Int`/`Float`, OR a
|
|
`Type::Con` resolving via `env.types` to a single-constructor `data`
|
|
whose every field type is a bare `Int`/`Float`. A record-typed field
|
|
stays rejected (M4 — spec §"Out of scope"). No new `CheckError`
|
|
variant; the two `#[error]` message strings widen (pin-safe — the
|
|
gate test asserts the code string, not the message).
|
|
|
|
**Files:**
|
|
- Modify: `crates/ailang-check/src/lib.rs:1921-1924` (predicate)
|
|
- Modify: `crates/ailang-check/src/lib.rs:1925-1940` (gate loop call site)
|
|
- Modify: `crates/ailang-check/src/lib.rs:452` / `:458` (messages)
|
|
- Modify: `examples/embed_export_adt_ret_rejected.ail` (re-point)
|
|
- Create: 4 must-fail fixtures + 1 positive fixture (see file list)
|
|
- Test: `crates/ailang-check/tests/embed_export_gate.rs`
|
|
|
|
- [ ] **Step 1: Write the failing tests (RED) — gate fixtures**
|
|
|
|
Create the five fixtures. `examples/embed_export_record_ok.ail`
|
|
(positive — must PASS check):
|
|
|
|
```
|
|
(module embed_export_record_ok
|
|
(data State
|
|
(ctor State (con Float) (con Int)))
|
|
(fn step
|
|
(export "step")
|
|
(type
|
|
(fn-type
|
|
(params (own (con State)) (con Float))
|
|
(ret (con State))))
|
|
(params st sample)
|
|
(body
|
|
(match st
|
|
(case (pat-ctor State acc n)
|
|
(app State (app + acc sample) (app + n 1)))))))
|
|
```
|
|
|
|
`examples/embed_export_str_field_record_rejected.ail` (single-ctor,
|
|
one `Str` field — must FAIL):
|
|
|
|
```
|
|
(module embed_export_str_field_record_rejected
|
|
(data Tagged
|
|
(ctor Tagged (con Int) (con Str)))
|
|
(fn f
|
|
(export "f")
|
|
(type (fn-type (params (con Int)) (ret (con Tagged))))
|
|
(params n)
|
|
(body (app Tagged n "x"))))
|
|
```
|
|
|
|
`examples/embed_export_list_field_record_rejected.ail` (single-ctor,
|
|
one `List` field — must FAIL; `List` def grounded on
|
|
`examples/borrow_own_demo.ail`):
|
|
|
|
```
|
|
(module embed_export_list_field_record_rejected
|
|
(data List
|
|
(ctor Nil)
|
|
(ctor Cons (con Int) (con List)))
|
|
(data Boxed
|
|
(ctor Boxed (con Int) (con List)))
|
|
(fn f
|
|
(export "f")
|
|
(type (fn-type (params (con Int)) (ret (con Boxed))))
|
|
(params n)
|
|
(body (app Boxed n (term-ctor List Nil)))))
|
|
```
|
|
|
|
(Note: `List` here is itself multi-ctor, so the `Boxed` rejection
|
|
reason that bites is the **non-scalar field** rule — `Boxed` is
|
|
single-ctor but its field `List` is not a bare `Int`/`Float`. That
|
|
is exactly the M4-boundary case the spec wants pinned.)
|
|
|
|
`examples/embed_export_multictor_rejected.ail` (2-ctor all-scalar
|
|
sum — must FAIL on the single-ctor rule):
|
|
|
|
```
|
|
(module embed_export_multictor_rejected
|
|
(data Either2
|
|
(ctor L (con Int))
|
|
(ctor R (con Float)))
|
|
(fn f
|
|
(export "f")
|
|
(type (fn-type (params (con Int)) (ret (con Either2))))
|
|
(params n)
|
|
(body (app L n))))
|
|
```
|
|
|
|
Re-point `examples/embed_export_adt_ret_rejected.ail` — **replace
|
|
its entire content** (was single-ctor `Pair`, now M3-valid) with the
|
|
multi-ctor + `Str`-field `Reading` from spec §"must-fail axis"
|
|
(module name stays `embed_export_adt_ret_rejected` = file-stem, the
|
|
loader invariant):
|
|
|
|
```
|
|
(module embed_export_adt_ret_rejected
|
|
(data Reading
|
|
(ctor Missing)
|
|
(ctor Sample (con Int) (con Str)))
|
|
(fn f
|
|
(export "f")
|
|
(type
|
|
(fn-type
|
|
(params (con Int))
|
|
(ret (con Reading))))
|
|
(params n)
|
|
(body (app Sample n "tick"))))
|
|
```
|
|
|
|
In `crates/ailang-check/tests/embed_export_gate.rs`, add (mirroring
|
|
the existing `check_codes("…")`/assert pattern at `:25-63` — open
|
|
the file and copy that helper's exact form):
|
|
|
|
```rust
|
|
#[test]
|
|
fn record_export_passes() {
|
|
// single-ctor (Float,Int) record export — M3-valid
|
|
assert!(check_codes("embed_export_record_ok.ail").is_empty());
|
|
}
|
|
|
|
#[test]
|
|
fn str_field_record_export_rejected() {
|
|
assert!(check_codes("embed_export_str_field_record_rejected.ail")
|
|
.contains(&"export-non-scalar-signature".to_string()));
|
|
}
|
|
|
|
#[test]
|
|
fn list_field_record_export_rejected() {
|
|
assert!(check_codes("embed_export_list_field_record_rejected.ail")
|
|
.contains(&"export-non-scalar-signature".to_string()));
|
|
}
|
|
|
|
#[test]
|
|
fn multictor_export_rejected() {
|
|
assert!(check_codes("embed_export_multictor_rejected.ail")
|
|
.contains(&"export-non-scalar-signature".to_string()));
|
|
}
|
|
```
|
|
|
|
(`adt_ret_export_rejected` at `:31-34` is **kept as-is in assertion**
|
|
— it still asserts `"export-non-scalar-signature"` on
|
|
`embed_export_adt_ret_rejected.ail`; only the fixture content changed
|
|
in this task. Its Task-1 re-point comment now describes a completed,
|
|
reviewed change.)
|
|
|
|
- [ ] **Step 2: Run the new tests to verify RED**
|
|
|
|
Run: `cargo test -p ailang-check --test embed_export_gate record_export_passes str_field_record_export_rejected list_field_record_export_rejected multictor_export_rejected`
|
|
Expected: FAIL — `record_export_passes` fails (today's `is_c_scalar`
|
|
rejects the single-ctor `State` return, so `check_codes` is
|
|
non-empty); the three `_rejected` tests *may* already pass (today
|
|
everything ADT is rejected) — that is acceptable RED-state for the
|
|
positive; the discriminating RED is `record_export_passes` failing
|
|
and `adt_ret_export_rejected` will (after re-point) still pass.
|
|
|
|
Run: `cargo test -p ailang-check --test embed_export_gate adt_ret_export_rejected -- --exact`
|
|
Expected: PASS — the re-pointed `Reading` (2 ctors + `Str` field)
|
|
still yields `export-non-scalar-signature` under *today's* gate
|
|
(every non-scalar ADT is rejected pre-M3), so the re-point keeps the
|
|
pin green through the transition (its meaning sharpens in Step 3).
|
|
|
|
- [ ] **Step 3: Widen the predicate (`is_c_scalar` → `is_c_abi_type`)**
|
|
|
|
In `crates/ailang-check/src/lib.rs`, replace the nested fn at
|
|
`:1921-1924`:
|
|
|
|
```rust
|
|
fn is_c_scalar(t: &Type) -> bool {
|
|
matches!(t, Type::Con { name, args, .. }
|
|
if args.is_empty() && (name == "Int" || name == "Float"))
|
|
}
|
|
```
|
|
|
|
with the two-level M3 predicate (NOT deep — a record-typed field is
|
|
rejected; M4 owns nesting):
|
|
|
|
```rust
|
|
fn is_c_scalar(t: &Type) -> bool {
|
|
matches!(t, Type::Con { name, args, .. }
|
|
if args.is_empty() && (name == "Int" || name == "Float"))
|
|
}
|
|
// M3 (spec 2026-05-18-embedding-abi-m3 §Architecture L85-102):
|
|
// a C scalar, OR a single-constructor `data` whose every field
|
|
// is a *bare* C scalar. Two-level by design — a record-typed
|
|
// field stays rejected (M4 owns nested-record recursion). Uses
|
|
// the in-scope `env.types: String -> TypeDef` (read pattern as
|
|
// `env.types.get(name)`, cf. lib.rs:1826).
|
|
fn is_c_abi_type(t: &Type, env: &Env) -> bool {
|
|
if is_c_scalar(t) {
|
|
return true;
|
|
}
|
|
if let Type::Con { name, args, .. } = t {
|
|
if args.is_empty() {
|
|
if let Some(td) = env.types.get(name) {
|
|
if td.ctors.len() == 1 {
|
|
return td.ctors[0]
|
|
.fields
|
|
.iter()
|
|
.all(is_c_scalar);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
false
|
|
}
|
|
```
|
|
|
|
(`env`, `Type`, `Env`, `TypeDef.ctors[i].fields` are recon-confirmed
|
|
in scope at the gate site `:1920` inside `check_fn`. If the field
|
|
accessor differs — `ctor.fields` vs `ctor.field_types` — use the
|
|
exact name the `drop.rs:100-102` walker uses; open `drop.rs` to
|
|
confirm the accessor before writing this, then match it.)
|
|
|
|
- [ ] **Step 4: Point the gate loop at `is_c_abi_type`**
|
|
|
|
In `crates/ailang-check/src/lib.rs:1925-1940`, the param loop and ret
|
|
check currently call `is_c_scalar(ty)`. Change each call site to
|
|
`is_c_abi_type(ty, env)` (the `env` binding is the same one
|
|
`is_c_abi_type` borrows; recon-confirmed in scope). Do **not** change
|
|
the loop structure, the position `&'static str`, or the
|
|
`ExportNonScalarSignature(...)` construction shape — only the
|
|
predicate call. The effect check (`:1941-1946`) is untouched.
|
|
|
|
- [ ] **Step 5: Widen the two `#[error]` message strings**
|
|
|
|
`crates/ailang-check/src/lib.rs:452` currently:
|
|
|
|
```rust
|
|
#[error("export `{0}`: M1 embedding ABI is scalar-only — {1} type `{2}` is not `Int`/`Float`")]
|
|
```
|
|
|
|
Replace with (single contiguous line — pin-safe; no test asserts
|
|
this message text, only the `code()` string; recon-confirmed):
|
|
|
|
```rust
|
|
#[error("export `{0}`: embedding ABI accepts `Int`/`Float` or a single-constructor record of those — {1} type `{2}` is not permitted (multi-constructor sums, and `Str`/`List`/nested-record fields, are a future M4 layer)")]
|
|
```
|
|
|
|
`crates/ailang-check/src/lib.rs:458` (the `ExportHasEffects`
|
|
message) — only widen if it says "M1"; if it reads
|
|
`export \`{0}\` must be pure …` leave it byte-unchanged (effects
|
|
rule did not change). Open `:455-459`, and if `:458` contains the
|
|
literal `M1`, drop the `M1 ` token only; otherwise no edit.
|
|
|
|
- [ ] **Step 6: Run the gate suite to verify GREEN**
|
|
|
|
Run: `cargo test -p ailang-check --test embed_export_gate`
|
|
Expected: PASS, `10 passed` — the original 6 (incl.
|
|
`adt_ret_export_rejected`, now sharpened: `Reading` fails on
|
|
multi-ctor AND Str-field) + the 4 new
|
|
(`record_export_passes`, `str_field_record_export_rejected`,
|
|
`list_field_record_export_rejected`, `multictor_export_rejected`).
|
|
|
|
- [ ] **Step 7: Confirm no `ailang-check` regression**
|
|
|
|
Run: `cargo test -p ailang-check`
|
|
Expected: PASS — workspace `ailang-check` suite green; the only
|
|
behaviour change is the export gate widening (single-ctor scalar
|
|
records now accepted; everything else byte-identical).
|
|
|
|
---
|
|
|
|
## Task 3: Widen the codegen forwarder to pass a record as `ptr`
|
|
|
|
`fn_scalar_sig`/`llvm_scalar` widen so a record `Type::Con` maps to
|
|
`ptr`; the M2 forwarder body (`:604-651`) is **byte-unchanged** (it
|
|
already templates `define {cret} @sym(ptr %ctx, …)`; the change is
|
|
only what `{cret}`/param types resolve to). All RC stays in the
|
|
byte-unchanged internal `@ail_<mod>_<fn>`.
|
|
|
|
**Files:**
|
|
- Modify: `crates/ailang-codegen/src/lib.rs:659-669` (`fn_scalar_sig`)
|
|
- Modify: `crates/ailang-codegen/src/lib.rs:673-678` (`llvm_scalar`)
|
|
- Create: `examples/embed_backtest_step_record.ail`
|
|
- Create: `examples/embed_backtest_step_record_borrow.ail`
|
|
- Test: `crates/ailang-codegen/tests/embed_staticlib_lowering.rs`
|
|
|
|
- [ ] **Step 1: Confirm the caller set of `fn_scalar_sig`/`llvm_scalar`**
|
|
|
|
Run: `grep -rn 'fn_scalar_sig\|llvm_scalar' crates/ailang-codegen/src/`
|
|
Expected: callers are only inside the `Target::StaticLib` forwarder
|
|
block (`lib.rs:622`/`:628` per recon). Record every call site found;
|
|
all must be threaded inside THIS task (no signature change is
|
|
introduced — these fns keep their signatures — so no compile-gate /
|
|
deferred-caller hazard; this step is the explicit confirmation that
|
|
the change is contained).
|
|
|
|
- [ ] **Step 2: Write the north-star + borrow fixtures**
|
|
|
|
Create `examples/embed_backtest_step_record.ail` (spec headline,
|
|
verbatim):
|
|
|
|
```
|
|
(module backtest
|
|
|
|
(data State
|
|
(ctor State (con Float) (con Int)))
|
|
|
|
(fn step
|
|
(export "backtest_step")
|
|
(type
|
|
(fn-type
|
|
(params (own (con State)) (con Float))
|
|
(ret (con State))))
|
|
(params st sample)
|
|
(body
|
|
(match st
|
|
(case (pat-ctor State acc n)
|
|
(app State (app + acc sample) (app + n 1)))))))
|
|
```
|
|
|
|
Create `examples/embed_backtest_step_record_borrow.ail` — identical
|
|
except the param mode:
|
|
|
|
```
|
|
(module backtest
|
|
|
|
(data State
|
|
(ctor State (con Float) (con Int)))
|
|
|
|
(fn step
|
|
(export "backtest_step")
|
|
(type
|
|
(fn-type
|
|
(params (borrow (con State)) (con Float))
|
|
(ret (con State))))
|
|
(params st sample)
|
|
(body
|
|
(match st
|
|
(case (pat-ctor State acc n)
|
|
(app State (app + acc sample) (app + n 1)))))))
|
|
```
|
|
|
|
- [ ] **Step 3: Write the failing forwarder-IR pin (RED)**
|
|
|
|
In `crates/ailang-codegen/tests/embed_staticlib_lowering.rs`, add
|
|
(mirror the exact load+lower helper `staticlib_emits_forwarder_no_main`
|
|
at `:20-44` uses — open the file, copy its incantation, substitute
|
|
the record fixture):
|
|
|
|
```rust
|
|
#[test]
|
|
fn staticlib_record_forwarder_is_ptr_passthrough() {
|
|
let ir = lower_staticlib_ir("embed_backtest_step_record.ail"); // mirror :20
|
|
// record param + ret cross as bare ptr; ctx leading; M2 TLS shape
|
|
assert!(ir.contains("define ptr @backtest_step(ptr %ctx, ptr %a0, double %a1)"),
|
|
"record fwd: ptr ret, leading ptr %ctx, ptr record param, double sample; IR:\n{ir}");
|
|
assert!(ir.contains("store ptr %ctx, ptr @__ail_tls_ctx"),
|
|
"M2 TLS store byte-unchanged; IR:\n{ir}");
|
|
assert!(ir.contains("call ptr @ail_backtest_step(ptr %a0, double %a1)"),
|
|
"internal call byte-unchanged (no RC at forwarder); IR:\n{ir}");
|
|
assert!(!ir.contains("sret") && !ir.contains("byval"),
|
|
"no aggregate convention introduced — record is a bare ptr; IR:\n{ir}");
|
|
assert!(!ir.contains("define i32 @main()"),
|
|
"staticlib: no @main; IR:\n{ir}");
|
|
}
|
|
```
|
|
|
|
(The exact param SSA names — `%a0`/`%a1` — and the `double` vs `i64`
|
|
for the `(con Float) sample` must match what the forwarder template
|
|
at `lib.rs:632-646` actually emits; after Step 4, read the emitted
|
|
IR and tighten these `contains` to the literal emitted forms.
|
|
`llvm_scalar` already maps `(con Float)` → `double`, recon-confirmed.)
|
|
|
|
- [ ] **Step 4: Run the pin to verify RED**
|
|
|
|
Run: `cargo build -p ailang-codegen 2>&1 | tail -3 ; cargo test -p ailang-codegen --test embed_staticlib_lowering staticlib_record_forwarder_is_ptr_passthrough -- --exact`
|
|
Expected: FAIL — today `fn_scalar_sig` only matches scalar
|
|
`Type::Fn`; `llvm_scalar` maps any non-`Float` `Type::Con` to `i64`,
|
|
so a `(con State)` param/ret is mis-lowered to `i64` (or the
|
|
workspace fails to lower the record export at all). The assertion
|
|
`define ptr @backtest_step(ptr %ctx, ptr %a0, double %a1)` is unmet.
|
|
|
|
- [ ] **Step 5: Widen `llvm_scalar`**
|
|
|
|
`crates/ailang-codegen/src/lib.rs:673-678` currently:
|
|
|
|
```rust
|
|
fn llvm_scalar(t: &Type) -> &'static str {
|
|
match t {
|
|
Type::Con { name, .. } if name == "Float" => "double",
|
|
_ => "i64",
|
|
}
|
|
}
|
|
```
|
|
|
|
The forwarder must map a record (`Type::Con` resolving to a
|
|
single-ctor `data`) to `"ptr"`, `Float` → `"double"`, `Int`/scalar →
|
|
`"i64"`. `llvm_scalar` has no `env` param today. Rather than thread
|
|
`env` through (signature change → caller ripple), distinguish
|
|
structurally: at the forwarder, a non-`Int`/`Float` `Type::Con` that
|
|
reached codegen on an `(export)` fn is — by Task-2's gate — a
|
|
guaranteed single-ctor scalar record. So:
|
|
|
|
```rust
|
|
fn llvm_scalar(t: &Type) -> &'static str {
|
|
match t {
|
|
Type::Con { name, .. } if name == "Float" => "double",
|
|
Type::Con { name, .. } if name == "Int" => "i64",
|
|
// M3: any other Type::Con reaching an (export) signature is,
|
|
// by the Task-2 export gate, a single-ctor scalar record;
|
|
// it crosses the C ABI as a bare `ptr` (DESIGN.md §"Embedding
|
|
// ABI" frozen layout — payload pointer).
|
|
Type::Con { .. } => "ptr",
|
|
_ => "i64",
|
|
}
|
|
}
|
|
```
|
|
|
|
(The original `_ => "i64"` default for `Int` is preserved by the
|
|
explicit `name == "Int"` arm; the new `Type::Con { .. } => "ptr"`
|
|
only catches named-type records — exactly the gate-guaranteed M3
|
|
case. Confirm no scalar path relies on a non-`Con` type hitting
|
|
`i64` via the old catch-all in a way the reorder breaks: the only
|
|
caller is the forwarder over export-gated scalar/record types.)
|
|
|
|
- [ ] **Step 6: Confirm `fn_scalar_sig` already handles a record**
|
|
|
|
`crates/ailang-codegen/src/lib.rs:659-669` `fn_scalar_sig` returns
|
|
`Some((params.clone(), (**ret).clone()))` for a `Type::Fn`
|
|
(recon-quoted). It clones whole `Type`s — a `(con State)` param/ret
|
|
is already carried through unchanged; the scalar-ness was only
|
|
imposed downstream by `llvm_scalar`. No `fn_scalar_sig` edit is
|
|
needed *iff* it does not itself filter on scalar-ness. Open
|
|
`:659-669`; if the body is exactly the recon-quoted
|
|
`Forall→inner; Type::Fn{params,ret}→Some((params,ret)); _→None`,
|
|
add only a clarifying comment:
|
|
|
|
```rust
|
|
// M3: params/ret may include a single-ctor scalar record type;
|
|
// llvm_scalar maps it to `ptr`. fn_scalar_sig is type-shape only.
|
|
```
|
|
|
|
If instead it rejects non-scalar params (a `is_c_scalar`-like
|
|
guard inside), remove that guard so a record param/ret survives
|
|
extraction (the gate already guarantees only M3-valid records
|
|
reach here).
|
|
|
|
- [ ] **Step 7: Run the forwarder pin to verify GREEN**
|
|
|
|
Run: `cargo test -p ailang-codegen --test embed_staticlib_lowering`
|
|
Expected: PASS — `staticlib_record_forwarder_is_ptr_passthrough`
|
|
green plus `staticlib_emits_forwarder_no_main` and
|
|
`executable_target_still_emits_main` **byte-unchanged green** (the
|
|
scalar forwarder IR is unaffected: `Int`→`i64`, `Float`→`double`
|
|
arms preserved).
|
|
|
|
- [ ] **Step 8: Confirm no `ailang-codegen` regression**
|
|
|
|
Run: `cargo test -p ailang-codegen`
|
|
Expected: PASS — full codegen suite green incl. Task-1
|
|
`embed_record_layout_pin` (unchanged: the box layout did not move)
|
|
and the in-source `mod tests`.
|
|
|
|
---
|
|
|
|
## Task 4: E2E record round-trip — `own` (coherent-stop proof)
|
|
|
|
Build `libbacktest.a` + `libailang_rt.a` from
|
|
`embed_backtest_step_record.ail`, link a C host that constructs the
|
|
input `State` via `ailang_rc_alloc`, calls `backtest_step` N times
|
|
(kernel consumes each `own` input), frees the final return via
|
|
`ailang_rc_dec`, and asserts `ailang_ctx_free`'s `AILANG_RC_STATS`
|
|
readback shows `allocs == frees` and the value is correct.
|
|
|
|
**Files:**
|
|
- Create: `crates/ail/tests/embed/record_roundtrip.c`
|
|
- Create: `crates/ail/tests/embed_record_e2e.rs`
|
|
|
|
- [ ] **Step 1: Write the C host (own + borrow via a compile-time switch)**
|
|
|
|
Create `crates/ail/tests/embed/record_roundtrip.c` (the spec
|
|
§"changed C host" verbatim for the `own` arm, plus a `-DBORROW` arm
|
|
for Task 5; the frozen layout `{tag@0, Float acc@8, Int n@16}`,
|
|
`make_state` via `ailang_rc_alloc(8 + 2*8)`):
|
|
|
|
```c
|
|
#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(ailang_ctx_t *ctx, void *st, double sample);
|
|
|
|
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;
|
|
}
|
|
|
|
int main(void) {
|
|
ailang_ctx_t *ctx = ailang_ctx_new();
|
|
void *st = make_state(0.0, 0);
|
|
for (int i = 0; i < 1000000; i++) {
|
|
void *next = backtest_step(ctx, st, (double)(i & 7));
|
|
#ifdef BORROW
|
|
ailang_rc_dec(st); /* borrow: host retained input, frees it */
|
|
#endif
|
|
/* own: kernel consumed `st`; do NOT touch/dec it 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);
|
|
ailang_rc_dec(st); /* host frees the final return */
|
|
ailang_ctx_free(ctx); /* AILANG_RC_STATS readback fires here */
|
|
return 0;
|
|
}
|
|
```
|
|
|
|
- [ ] **Step 2: Write the failing `own` E2E test (RED)**
|
|
|
|
Create `crates/ail/tests/embed_record_e2e.rs`. Open
|
|
`crates/ail/tests/embed_e2e.rs` and **mirror its exact** build/link/
|
|
run helper (the `ail build --emit=staticlib … -o`, the `ar`/`clang`
|
|
link of the C host against `lib<entry>.a` + `libailang_rt.a`, the
|
|
`AILANG_RC_STATS=1` env + stderr `allocs=… frees=…` parse). Add:
|
|
|
|
```rust
|
|
#[test]
|
|
fn record_roundtrip_own_alloc_eq_free() {
|
|
// build embed_backtest_step_record.ail --emit=staticlib,
|
|
// link crates/ail/tests/embed/record_roundtrip.c (no -DBORROW),
|
|
// run with AILANG_RC_STATS=1, parse the ctx_free readback.
|
|
let stats = build_link_run_embed(
|
|
"embed_backtest_step_record.ail",
|
|
"embed/record_roundtrip.c",
|
|
&[/* no extra clang defines */],
|
|
);
|
|
assert_eq!(stats.allocs, stats.frees,
|
|
"own: every State box freed exactly once (kernel-consumed input + host-freed return); {stats:?}");
|
|
assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held");
|
|
}
|
|
```
|
|
|
|
(The `build_link_run_embed` helper + `stats` struct shape are
|
|
whatever `embed_e2e.rs` already defines; reuse it — extract it to a
|
|
shared `mod` only if `embed_e2e.rs` does not already expose it. Do
|
|
not invent a new harness.)
|
|
|
|
- [ ] **Step 3: Run the `own` E2E to verify RED**
|
|
|
|
Run: `cargo test -p ail --test embed_record_e2e record_roundtrip_own_alloc_eq_free -- --exact --nocapture`
|
|
Expected: FAIL — before Task 2+3 are both in the tree this fails to
|
|
build the staticlib (gate rejects the record export) or mis-lowers
|
|
the record; with Task 2+3 present it builds, and this step's RED is
|
|
only if a real alloc/free imbalance exists. (Run order: this task
|
|
executes after Tasks 2+3; the RED here pins the *alloc==free*
|
|
property specifically, not the gate/forwarder which Tasks 2/3 pinned.)
|
|
|
|
- [ ] **Step 4: Verify GREEN (own coherent-stop)**
|
|
|
|
The `own` consume path is existing Iter-B machinery (spec §"Why the
|
|
ownership contract is mechanically almost free"; 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 pin and must not be cited). No production
|
|
code change is expected in this task — if `record_roundtrip_own_alloc_eq_free`
|
|
is RED for a real imbalance, that is a genuine bug: hand off to
|
|
`debug` (RED test already exists). If it is GREEN immediately once
|
|
Tasks 2+3 are in the tree, that *is* the spec's "mechanically almost
|
|
free" claim substantiated.
|
|
|
|
Run: `cargo test -p ail --test embed_record_e2e record_roundtrip_own_alloc_eq_free -- --exact`
|
|
Expected: PASS — `allocs == frees`, exit 0.
|
|
|
|
---
|
|
|
|
## Task 5: E2E record round-trip — `borrow`
|
|
|
|
Same harness, the `-DBORROW` arm: the kernel does **not** consume the
|
|
input; the host retains and `ailang_rc_dec`s it itself. `allocs ==
|
|
frees` again. Tasks 4+5 together prove "ownership follows the
|
|
declared mode" in *both* directions.
|
|
|
|
**Files:**
|
|
- Modify: `crates/ail/tests/embed_record_e2e.rs` (add the borrow test)
|
|
|
|
- [ ] **Step 1: Write the failing `borrow` E2E test (RED)**
|
|
|
|
In `crates/ail/tests/embed_record_e2e.rs` add:
|
|
|
|
```rust
|
|
#[test]
|
|
fn record_roundtrip_borrow_alloc_eq_free() {
|
|
// same C host with -DBORROW: host frees the retained input each
|
|
// iter; kernel (borrow param) does NOT consume it.
|
|
let stats = build_link_run_embed(
|
|
"embed_backtest_step_record_borrow.ail",
|
|
"embed/record_roundtrip.c",
|
|
&["-DBORROW"],
|
|
);
|
|
assert_eq!(stats.allocs, stats.frees,
|
|
"borrow: kernel kept input; host freed every input + the return; {stats:?}");
|
|
assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held");
|
|
}
|
|
```
|
|
|
|
- [ ] **Step 2: Run the `borrow` E2E to verify RED then GREEN**
|
|
|
|
Run: `cargo test -p ail --test embed_record_e2e record_roundtrip_borrow_alloc_eq_free -- --exact --nocapture`
|
|
Expected: FAIL first if the borrow fixture is not yet built/lowered;
|
|
then PASS once `embed_backtest_step_record_borrow.ail` builds via the
|
|
Task-2/3 path. A `borrow` param is **not** dropped by the kernel
|
|
(ratified by `crates/ail/tests/e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`),
|
|
so the host's per-iter `ailang_rc_dec(st)` is exactly what balances
|
|
`allocs == frees`. A real imbalance ⇒ genuine bug ⇒ hand to `debug`.
|
|
|
|
- [ ] **Step 3: Both modes green together**
|
|
|
|
Run: `cargo test -p ail --test embed_record_e2e`
|
|
Expected: PASS, `2 passed` — `record_roundtrip_own_alloc_eq_free`
|
|
and `record_roundtrip_borrow_alloc_eq_free`. The frozen ownership
|
|
contract is **proven both ways**, not asserted.
|
|
|
|
---
|
|
|
|
## Task 6: Freeze the layout — DESIGN.md SSOT + lockstep pointers
|
|
|
|
Convert "provisional until M3" into one-way-freeze wording, add the
|
|
frozen value-layout SSOT subsection, and point the three independent
|
|
layout-encoding sites at it. The Task-1 byte-pin becomes the
|
|
enforcing guard. Pin-safety: `docs_honesty_pin.rs:135` asserts
|
|
DESIGN.md `:2297` ("Export parameters are written **bare**…"), which
|
|
is **outside** both rewrite zones — it must stay byte-verbatim and
|
|
contiguous (planner Step-5 item 6).
|
|
|
|
**Files:**
|
|
- Modify: `docs/DESIGN.md:2280-2282`, `:2293-2295`, insert before `:2319`
|
|
- Modify: `runtime/rc.c:28-44`
|
|
- Modify: `crates/ailang-codegen/src/match_lower.rs:107`/`:123-126`/`:128-136`
|
|
- Modify: `crates/ailang-codegen/src/drop.rs:88`/`:113`
|
|
- Modify: `crates/ailang-codegen/src/lib.rs:178`, `crates/ailang-core/src/ast.rs:211`
|
|
|
|
- [ ] **Step 1: Confirm the docs-honesty pin baseline + the exact pinned line**
|
|
|
|
Run: `cargo test -p ailang-core --test docs_honesty_pin`
|
|
Expected: PASS (baseline before any DESIGN.md edit).
|
|
|
|
Run: `grep -n 'Export parameters are written' docs/DESIGN.md`
|
|
Expected: one hit at `:2297`. Record its exact byte content — Step 4
|
|
must NOT touch this line and must keep it contiguous.
|
|
|
|
- [ ] **Step 2: Rewrite the two "provisional until M3" sentences**
|
|
|
|
`docs/DESIGN.md:2280-2282` currently (recon-verbatim):
|
|
|
|
```
|
|
The M1 ABI is **scalar-only and provisional until M3**: every parameter and the return type must be `Int` (lowered `i64`) or `Float` (lowered `double`), and the fn's effect set must be empty.
|
|
```
|
|
|
|
Replace with (the scalar rule still holds for *scalar* exports; the
|
|
record extension + freeze are stated; single contiguous sentences):
|
|
|
|
```
|
|
The embedding ABI accepts `Int` (lowered `i64`), `Float` (lowered `double`), or a single-constructor record of those (crossing as a bare `ptr` to the frozen box layout below); the fn's effect set must be empty. **Frozen as of M3**: a future compiler change MUST NOT move the box offsets below or invert the host-free rule.
|
|
```
|
|
|
|
`docs/DESIGN.md:2293-2295` currently (recon-verbatim):
|
|
|
|
```
|
|
Only the value/record layout remains provisional until M3; the ctx-threaded C signature is the M2 shape.
|
|
```
|
|
|
|
Replace with:
|
|
|
|
```
|
|
The value/record layout is **frozen as of M3** (see "Frozen value layout" below); the ctx-threaded C signature is the M2 shape.
|
|
```
|
|
|
|
- [ ] **Step 3: Run the docs-honesty pin to confirm Step 2 is pin-safe**
|
|
|
|
Run: `cargo test -p ailang-core --test docs_honesty_pin`
|
|
Expected: PASS — recon-confirmed no pin asserts any "provisional
|
|
until M3" substring; `:2297` untouched. If RED, a pinned substring
|
|
was in the rewrite zone — STOP, restore, and re-scope the edit to
|
|
exclude the pinned bytes (planner Step-5 item 6).
|
|
|
|
- [ ] **Step 4: Insert the frozen value-layout SSOT subsection**
|
|
|
|
In `docs/DESIGN.md`, immediately before `## Data model` (recon: blank
|
|
`:2318`, `## Data model` at `:2319`; insert at end of §"Embedding
|
|
ABI", after `:2317`):
|
|
|
|
```markdown
|
|
### Frozen value layout (M3 — one-way commitment)
|
|
|
|
For a single-constructor `data T` whose `n` fields are each `Int`
|
|
or `Float`, a value of `T` crossing the embedding C boundary is a
|
|
bare payload pointer `p`:
|
|
|
|
| bytes | content |
|
|
|---|---|
|
|
| `p - 8 .. p` | `uint64_t` refcount header (`HEADER_SIZE = 8`) |
|
|
| `p + 0 .. p + 8` | `int64_t` constructor tag (written; `0` for the single ctor — no elision) |
|
|
| `p + 8 + i*8` | field `i`, declaration order: `int64_t` for `Int`, IEEE-754 `double` bit-pattern for `Float` |
|
|
|
|
Total box payload size = `8 + n*8`. This is the layout codegen
|
|
emits today (`match_lower.rs` `lower_ctor`); it is **frozen** — a
|
|
future compiler change MUST NOT move these offsets.
|
|
|
|
**Construction (host → kernel input).** The host MUST obtain an
|
|
input record's storage from `ailang_rc_alloc(8 + n*8)` (returns the
|
|
payload pointer with the refcount header pre-set to `1`, payload
|
|
zeroed), then write the tag (`0`) and the scalar fields at the
|
|
offsets above. A raw `malloc` is a contract violation:
|
|
`own`-consume and `ailang_rc_dec` both require the runtime's 8-byte
|
|
header at `p - 8` initialised to `1`.
|
|
|
|
**Ownership follows the declared mode** (the §"Mode metadata is
|
|
load-bearing for codegen" contract, as the C ABI): a `(own (con
|
|
T))` parameter transfers ownership in — the kernel consumes it
|
|
(Iter-B drop-at-return); the host MUST NOT touch or `dec` it after
|
|
the call. A `(borrow (con T))` parameter is retained by the host —
|
|
the kernel does not consume it; the host frees it. The return value
|
|
is always owned by the host.
|
|
|
|
**Free (host side).** `ailang_rc_dec(payload)`. Leak-free for an M3
|
|
record because every field is a scalar — `ailang_rc_dec` is
|
|
header-only and an M3 record has no boxed children. A record with
|
|
boxed fields (`Str`/`List`/nested record) is **not** an M3 type
|
|
(rejected by the export gate); a recursive typed-free for that
|
|
shape is an additive M4 concern, not a contradiction of this
|
|
freeze.
|
|
```
|
|
|
|
- [ ] **Step 5: Add the lockstep-pointer comment at the three encoders**
|
|
|
|
`runtime/rc.c:28-44` — at the end of the layout comment block
|
|
(after the "fields from offset 8, env-cells …" sentence, before the
|
|
"Single-threaded:" paragraph), add one line:
|
|
|
|
```
|
|
* FROZEN ABI for the embedding boundary — see DESIGN.md §"Embedding
|
|
* ABI" > "Frozen value layout". A boundary-crossing single-ctor
|
|
* scalar record's box offsets MUST NOT move.
|
|
```
|
|
|
|
`crates/ailang-codegen/src/match_lower.rs` — one line immediately
|
|
above the `size_bytes = 8 + ...` computation (`:107`):
|
|
|
|
```rust
|
|
// FROZEN ABI (embedding boundary) — DESIGN.md §"Embedding ABI"
|
|
// > "Frozen value layout". size = 8 + n*8, tag@0, fields@8+i*8.
|
|
```
|
|
|
|
`crates/ailang-codegen/src/drop.rs` — one line above the tag load
|
|
(`:88`) and above the `off = 8 + j*8` field-offset computation
|
|
(`:113`):
|
|
|
|
```rust
|
|
// FROZEN ABI (embedding boundary) — see DESIGN.md §"Embedding ABI".
|
|
```
|
|
|
|
- [ ] **Step 6: Fix the two stale rustdoc "provisional until M3" lines**
|
|
|
|
`crates/ailang-codegen/src/lib.rs:178` and
|
|
`crates/ailang-core/src/ast.rs:211` each carry a rustdoc fragment
|
|
saying the layout/signature is "provisional until M3" (recon-named;
|
|
DESIGN.md-current-state-mirror rule — these are now stale). Open
|
|
each, replace the "provisional until M3" clause with "frozen as of
|
|
M3 (DESIGN.md §\"Embedding ABI\" > \"Frozen value layout\")",
|
|
preserving the rest of the doc line byte-for-byte.
|
|
|
|
- [ ] **Step 7: Confirm the byte-pin is now the enforcing guard (spec item 5)**
|
|
|
|
Run: `cargo test -p ailang-codegen --test embed_record_layout_pin`
|
|
Expected: PASS (still — Task 6 changed no codegen offset, only
|
|
comments+docs).
|
|
|
|
Demonstrate enforceability (local, reverted): temporarily change
|
|
`match_lower.rs:107` `8 + ...` to `16 + ...`, run the pin, observe
|
|
RED, revert.
|
|
|
|
Run: `sed -i 's/let size_bytes = 8 +/let size_bytes = 16 +/' crates/ailang-codegen/src/match_lower.rs ; cargo test -p ailang-codegen --test embed_record_layout_pin -- --exact heap_box_layout_is_frozen_8_plus_n_times_8_tag_at_0_fields_from_8 ; git checkout -- crates/ailang-codegen/src/match_lower.rs`
|
|
Expected: the test run in the middle FAILS (`@ailang_rc_alloc(i64 24)`
|
|
absent — emits `i64 32`), then `git checkout` restores the file.
|
|
Re-run: `cargo test -p ailang-codegen --test embed_record_layout_pin`
|
|
Expected: PASS — proves the freeze is enforced, not aspirational.
|
|
(Use the exact `let size_bytes = 8 +` literal as it appears at
|
|
`:107`; if the binding name differs, adjust the `sed` to the actual
|
|
literal — confirm via `grep -n 'size_bytes' crates/ailang-codegen/src/match_lower.rs` first.)
|
|
|
|
---
|
|
|
|
## Task 7: Milestone-close verification gate
|
|
|
|
Not a code change — the consolidated GREEN gate proving the
|
|
"unmodified set stays green" + the full workspace is clean. Spec
|
|
Testing items 6/7 (regression-green-unmodified), 8 (clean core), 9
|
|
(bench) — items 8/9 are the milestone-close `audit` skill's job
|
|
(architect Invariant 1, bench trio); this task asserts only what an
|
|
implement run can: the test-suite GREEN state.
|
|
|
|
**Files:** none (verification only).
|
|
|
|
- [ ] **Step 1: The "stays green unmodified" regression set**
|
|
|
|
Run: `cargo test -p ail --test embed_e2e --test embed_rc_accounting_tsan --test embed_swarm_tsan --test embed_staticlib_cli --test embed_staticlib_alloc_guard --test print_no_leak_pin`
|
|
Expected: PASS — every M1/M2 embed test + the executable-path
|
|
leak pin green **unmodified** (M3 is additive: the scalar path is
|
|
byte-preserved; recon named this exact set).
|
|
|
|
Run: `cargo test -p ailang-core --test design_schema_drift ; cargo test -p ailang-check --test embed_export_hash_stable`
|
|
Expected: PASS — no schema field added (explicit M2-style contrast;
|
|
hashes/drift byte-unchanged).
|
|
|
|
- [ ] **Step 2: Full workspace**
|
|
|
|
Run: `cargo test --workspace 2>&1 | tail -15`
|
|
Expected: PASS — every crate green. Record the total passed count;
|
|
it must be the pre-M3 baseline + the net-new M3 tests
|
|
(`embed_record_layout_pin` 1, `embed_export_gate` +4,
|
|
`embed_staticlib_lowering` +1, `embed_record_e2e` 2) and no
|
|
pre-existing test removed or its assertion weakened.
|
|
|
|
- [ ] **Step 3: Round-trip invariant (no surface change)**
|
|
|
|
Run: `cargo test -p ailang-surface --test round_trip`
|
|
Expected: PASS — the new `.ail` fixtures round-trip; no Form-A
|
|
surface was added (existing `data`/`ctor`/`own`/`borrow`/`match`/
|
|
`pat-ctor`/`app` only).
|
|
|
|
---
|
|
|
|
## Notes for the implement orchestrator
|
|
|
|
- **Bench / architect are NOT this plan's job.** Spec Testing items
|
|
8 (clean-core Invariant 1) and 9 (bench trio carry-on) are the
|
|
milestone-close `audit` skill (architect + bencher). Do not run
|
|
`bench/check.py` in implement; record in the per-iter journal that
|
|
audit owns the bench/architect close.
|
|
- **Grounding-check carry-forward (do not violate):**
|
|
(1) the own/borrow contract is ratified by
|
|
`crates/ail/tests/e2e.rs::alloc_rc_own_param_dec_at_fn_return:1855`
|
|
+ `…::alloc_rc_borrow_only_recursive_list_drop:1671` — **never**
|
|
cite `borrow_own_demo_modes_are_metadata_only:1330` (Iter-18a
|
|
pre-enforcement pin) as the contract ratifier.
|
|
(2) Task 1's byte-pin is a genuine RED-first new pin on the
|
|
`@ailang_rc_alloc` heap path; the pre-existing
|
|
`iter17a_local_box_alloca` pins the *alloca* path and is NOT a
|
|
substitute.
|
|
- **Boss-only-commits.** Leave all work uncommitted in the working
|
|
tree; the Boss inspects `git diff` and commits the iter.
|