From 744ad41e470a0d79e132d479f5feb5263bdb14c3 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 30 May 2026 17:13:56 +0200 Subject: [PATCH] fix(check): resolve type-scoped borrow-receiver ops in linearity (closes #46) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A function whose parameter is `borrow (RawBuf a)` and which calls RawBuf.get or RawBuf.size on that parameter even once was rejected at `ail check` with [consume-while-borrowed] — the exact borrow-receiver use the ledger advertises for get/size. The diagnostic also misnamed the cause: the receiver is read, not consumed. Root cause: the linearity walk's callee_arg_modes looked up the callee under its spelled name. A type-scoped polymorphic op is spelled `RawBuf.get` at the call site, but check_module_with_visible registers the kernel raw_buf ops under their bare def names (get/size). The lookup missed, the receiver arg defaulted to Consume, and consuming a binder whose borrow_count==1 (the Borrow param) fired the false positive. The kernel signatures themselves are correct (receiver slot is `borrow`); the only defect was the name-resolution gap in the linearity globals lookup. Fix: on a direct-lookup miss, fall back to the bare method name via the existing parse_method_qualifier + qualifier_is_class_shape resolvers, gated on a class/type-shaped qualifier so lowercase cross-module-fn qualifiers (std_list.length) are excluded. This is how the rest of the checker already treats type-scoped polymorphic ops; the fix is general, not RawBuf-specific. This unblocks the natural borrow-helper decomposition (a shared read-only buffer behind a helper fn) — the shape the downstream series milestone's Series.at / Series.total_count need. Surfaced by the raw-buf fieldtest (finding B1, docs/specs/0058). RED-first: rawbuf_borrow_receiver_read_is_linearity_clean. --- crates/ailang-check/src/linearity.rs | 22 ++++++++++++++- crates/ailang-check/tests/workspace.rs | 39 ++++++++++++++++++++++++++ examples/raw_buf_borrow_read.ail | 11 ++++++++ 3 files changed, 71 insertions(+), 1 deletion(-) create mode 100644 examples/raw_buf_borrow_read.ail diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index 2ac1e65..bf7b23e 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -708,7 +708,27 @@ impl<'a> Checker<'a> { // with mode info). Look up the global symbol table. let ty = match self.globals.get(name) { Some(t) => t, - None => return vec![], + None => { + // Type-scoped kernel ops (e.g. `RawBuf.get`) are + // registered under their BARE def name (`get`) by + // `check_module_with_visible`. When the direct lookup + // misses and the name is a class/type-shaped qualifier, + // retry under the bare method name so the borrow-receiver + // modes resolve — same treatment the rest of the checker + // gives type-scoped polymorphic ops. A lowercase + // cross-module-fn qualifier (`std_list.length`) is NOT + // class-shaped and resolves by its own path, so it is + // gated out here. + let (method_name, qualifier_opt) = crate::parse_method_qualifier(name); + if qualifier_opt.is_some() && crate::qualifier_is_class_shape(&qualifier_opt) { + match self.globals.get(method_name) { + Some(t) => t, + None => return vec![], + } + } else { + return vec![]; + } + } }; let inner = strip_forall(ty); match inner { diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs index 26b1394..96ccbea 100644 --- a/crates/ailang-check/tests/workspace.rs +++ b/crates/ailang-check/tests/workspace.rs @@ -718,3 +718,42 @@ fn borrow_own_demo_is_linearity_clean() { diags ); } + +/// RED for fieldtest finding B1 (docs/specs/0058): reading a +/// `borrow (RawBuf a)` *parameter* through a borrow-receiver op +/// (`RawBuf.get` / `RawBuf.size`) must check clean. Both ops are +/// declared `(borrow (RawBuf a))` in the receiver slot by the kernel +/// `raw_buf` module, so reading the receiver through a borrow is the +/// advertised use — the receiver is read, not consumed. +/// +/// The linearity walk (`crates/ailang-check/src/linearity.rs`) +/// registers visible-module fns into its `globals` map under their +/// bare def name (`get` / `size`), but the call site spells the +/// type-scoped name `RawBuf.get` / `RawBuf.size`. `callee_arg_modes` +/// looks up `"RawBuf.get"`, misses, returns an empty mode vec, and the +/// receiver arg defaults to `Position::Consume` — consuming a binder +/// whose `borrow_count == 1` and firing a spurious +/// `consume-while-borrowed`. +#[test] +fn rawbuf_borrow_receiver_read_is_linearity_clean() { + let entry = examples_dir().join("raw_buf_borrow_read.ail"); + let ws = load_workspace(&entry).expect("load raw_buf_borrow_read"); + let diags = check_workspace(&ws); + let lin: Vec<&ailang_check::Diagnostic> = diags + .iter() + .filter(|d| { + d.code == "use-after-consume" || d.code == "consume-while-borrowed" + }) + .collect(); + assert!( + lin.is_empty(), + "reading a borrow-mode RawBuf param via RawBuf.get / RawBuf.size \ + must not fire a linearity error; got: {:#?}", + lin + ); + assert!( + diags.is_empty(), + "raw_buf_borrow_read must check clean; got: {:#?}", + diags + ); +} diff --git a/examples/raw_buf_borrow_read.ail b/examples/raw_buf_borrow_read.ail new file mode 100644 index 0000000..4db6e78 --- /dev/null +++ b/examples/raw_buf_borrow_read.ail @@ -0,0 +1,11 @@ +(module raw_buf_borrow_read + (fn read_one + (doc "Reads its borrow-mode RawBuf receiver via RawBuf.get once. get is a borrow-receiver op (kernel raw_buf: get : (borrow (RawBuf a)) Int -> a), so reading the receiver through a borrow must check clean — the receiver is read, not consumed.") + (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int)))) + (params buf) + (body (app RawBuf.get buf 0))) + (fn count + (doc "Reads its borrow-mode RawBuf receiver via RawBuf.size once. size is a borrow-receiver op (kernel raw_buf: size : (borrow (RawBuf a)) -> Int), so it must check clean for the same reason.") + (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int)))) + (params buf) + (body (app RawBuf.size buf))))