From e25580e3a3413031085f6af51e0e3445ac8f8c87 Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 2 Jun 2026 00:45:21 +0200 Subject: [PATCH] test(cutover): live accept/reject corpus for the #55 ownership surface MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wires the #55-cutover fieldtest into a durable regression net. The fieldtest exercised the post-cutover ParamMode={Own,Borrow} surface as a downstream LLM author would and produced 12 fixtures + a report; left as loose files they would be dead fixtures that drift. This commits them as a protected property. crates/ail/tests/cut55_cutover_surface.rs — one table-driven test running each fixture through `ail check` and asserting accept (exit 0) or reject at the right pipeline stage. Reject rows key on the bracketed diagnostic CODE (consume-while-borrowed, borrow-over-value, borrow-return-not-permitted, surface-parse-error), NOT message text, so the test is decoupled from the diagnostic-wording improvement tracked separately. examples/fieldtest/cut55_*.ail — the corpus. cut55_2c is the #58 repro (now correctly rejected). cut55_2b was misanalysed by the fieldtest as a consume-while-borrowed reject; in fact bump's recursive param is (borrow List) so the tail is only borrowed, never consumed into an own slot — `ail check` correctly accepts it. Renamed to cut55_2b_borrow_traversal_clean and recast as the #58 false-positive guard (a borrow-position use of a heap sub-binder must stay accepted). cut55_1b similarly does not fire over-strict-mode (its recursive call consumes the tail, so the lint's consume_count==0 premise fails) — comment corrected; it is a plain accept. cut55_1c is the genuine over-strict-mode example (accepts exit 0, emits the warning). docs/specs/0065-eliminate-implicit-mode fieldtest report — moved 2c to the reject set, added the 2b false-positive-guard section, marked the double-free spec_gap RESOLVED (it shipped as the #58 fix). Relates to #55. --- crates/ail/tests/cut55_cutover_surface.rs | 166 ++++++++++++++++ .../0065-fieldtest-eliminate-implicit-mode.md | 186 ++++++++++++++++++ .../fieldtest/cut55_1_readonly_length.ail | 40 ++++ .../fieldtest/cut55_1b_overstrict_own.ail | 33 ++++ .../fieldtest/cut55_1c_overstrict_isempty.ail | 27 +++ examples/fieldtest/cut55_2_consume_map.ail | 51 +++++ .../cut55_2b_borrow_traversal_clean.ail | 34 ++++ .../cut55_2c_consume_borrow_reject.ail | 39 ++++ .../cut55_2d_consume_borrow_whole.ail | 35 ++++ examples/fieldtest/cut55_3_value_param.ail | 34 ++++ .../fieldtest/cut55_3b_borrow_over_value.ail | 20 ++ .../cut55_4_borrow_return_reject.ail | 28 +++ .../fieldtest/cut55_4b_clone_to_return.ail | 51 +++++ .../fieldtest/cut55_5_bare_slot_reject.ail | 26 +++ 14 files changed, 770 insertions(+) create mode 100644 crates/ail/tests/cut55_cutover_surface.rs create mode 100644 docs/specs/0065-fieldtest-eliminate-implicit-mode.md create mode 100644 examples/fieldtest/cut55_1_readonly_length.ail create mode 100644 examples/fieldtest/cut55_1b_overstrict_own.ail create mode 100644 examples/fieldtest/cut55_1c_overstrict_isempty.ail create mode 100644 examples/fieldtest/cut55_2_consume_map.ail create mode 100644 examples/fieldtest/cut55_2b_borrow_traversal_clean.ail create mode 100644 examples/fieldtest/cut55_2c_consume_borrow_reject.ail create mode 100644 examples/fieldtest/cut55_2d_consume_borrow_whole.ail create mode 100644 examples/fieldtest/cut55_3_value_param.ail create mode 100644 examples/fieldtest/cut55_3b_borrow_over_value.ail create mode 100644 examples/fieldtest/cut55_4_borrow_return_reject.ail create mode 100644 examples/fieldtest/cut55_4b_clone_to_return.ail create mode 100644 examples/fieldtest/cut55_5_bare_slot_reject.ail diff --git a/crates/ail/tests/cut55_cutover_surface.rs b/crates/ail/tests/cut55_cutover_surface.rs new file mode 100644 index 0000000..ce1f742 --- /dev/null +++ b/crates/ail/tests/cut55_cutover_surface.rs @@ -0,0 +1,166 @@ +//! Regression net for the #55 ParamMode={Own,Borrow} totality cutover +//! (commit `76b21c0`, spec 0062 / plan 0121) and its #58 follow-up +//! (`b129af1`, sub-binder borrow inheritance). +//! +//! Property protected: the post-#55-cutover ownership surface accepts the +//! legitimate authoring forms and rejects the unsound / over-strict ones, +//! AT THE RIGHT PIPELINE STAGE. Concretely, for each fixture under +//! examples/fieldtest/cut55_*.ail, `ail check` must: +//! - exit 0 for the legitimate forms (read-only borrow, consume own, +//! value-typed own, clone-to-return escape hatch, and the +//! borrow-traverse-and-rebuild that must NOT trip the #58 check); +//! - reject the unsound / over-strict forms with the EXACT diagnostic +//! code, at the stage that owns the rule: +//! * bare fn-type slot -> `surface-parse-error` (parser stage), +//! * borrow over value type -> `borrow-over-value` (signature), +//! * borrowed return -> `borrow-return-not-permitted` (sig), +//! * consume while borrowed -> `consume-while-borrowed` (linearity), +//! and emit the `over-strict-mode` advisory (a warning, exit 0) on a +//! true read-only `(own)` heap param. +//! +//! Coupling discipline: the assertions key on the bracketed diagnostic +//! CODE (e.g. `[consume-while-borrowed]`) appearing in stderr, never on +//! the surrounding message wording — that wording is slated to change +//! (the borrow-return and consume-while-borrowed friction tidy-ups noted +//! in the spec-0065 findings) and the regression net must survive it. +//! Each row carries the fixture stem so a failure names which authoring +//! form regressed. +//! +//! Without this test the twelve cut55_* fixtures are dead files that the +//! build never executes; a regression in the totality check (a relaxed +//! reject, a moved stage, a re-introduced default) would land silently. + +use std::path::{Path, PathBuf}; +use std::process::Command; + +fn ail_bin() -> &'static str { + env!("CARGO_BIN_EXE_ail") +} + +fn fixture(stem: &str) -> PathBuf { + let manifest_dir = env!("CARGO_MANIFEST_DIR"); + let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap(); + workspace + .join("examples") + .join("fieldtest") + .join(format!("{stem}.ail")) +} + +/// What `ail check` must do with a fixture. Codes name the bracketed +/// diagnostic tag, never the message prose. +enum Expect { + /// exit 0, no warning expected (legitimate form). + Accept, + /// exit 0, but the `over-strict-mode` advisory warning must appear. + AcceptWithWarning(&'static str), + /// exit non-zero, and `[code]` must appear in stderr. + Reject(&'static str), +} + +fn check(stem: &str) -> (bool, String) { + let out = Command::new(ail_bin()) + .args(["check", fixture(stem).to_str().unwrap()]) + .output() + .expect("ail check failed to run"); + let stderr = String::from_utf8(out.stderr).expect("stderr utf8"); + (out.status.success(), stderr) +} + +#[test] +fn cut55_cutover_surface_accepts_and_rejects_at_the_right_stage() { + // (fixture stem, expectation). The stem is in every failure message + // so a red row names the regressed authoring form. + let table: &[(&str, Expect)] = &[ + // --- decision (a): borrow vs own on a heap value ----------------- + ("cut55_1_readonly_length", Expect::Accept), + // over-strict own that does NOT trip the lint: the recursive call + // consumes the heap tail into an own self-param, so the lint's + // consume_count==0 premise fails. Still a sound (if strict) + // annotation -> accepted, silent. + ("cut55_1b_overstrict_own", Expect::Accept), + // true read-only own: nothing consumed -> the advisory fires. + ( + "cut55_1c_overstrict_isempty", + Expect::AcceptWithWarning("over-strict-mode"), + ), + // --- decision (b): consume vs borrow ----------------------------- + ("cut55_2_consume_map", Expect::Accept), + // false-positive guard for #58: borrow-traverse-and-rebuild, the + // recursive param is (borrow) so the tail is never consumed. + ("cut55_2b_borrow_traversal_clean", Expect::Accept), + // #58 fix: tail sub-binder of a borrowed scrutinee moved into an + // own sink -> reject at the linearity check. + ( + "cut55_2c_consume_borrow_reject", + Expect::Reject("consume-while-borrowed"), + ), + // whole borrowed param moved into an own sink -> reject. + ( + "cut55_2d_consume_borrow_whole", + Expect::Reject("consume-while-borrowed"), + ), + // --- decision (c): value-typed params ---------------------------- + ("cut55_3_value_param", Expect::Accept), + // borrow over an unboxed value type -> reject at the signature. + ( + "cut55_3b_borrow_over_value", + Expect::Reject("borrow-over-value"), + ), + // --- decision (d): borrowed return ------------------------------- + // a (borrow) return is refcount-invisible -> reject at the signature. + ( + "cut55_4_borrow_return_reject", + Expect::Reject("borrow-return-not-permitted"), + ), + // the clone escape hatch lifts a borrowed field to an owned return. + ("cut55_4b_clone_to_return", Expect::Accept), + // --- the cutover's core promise: no defaulted mode --------------- + // a bare fn-type slot is rejected at the PARSER stage, not linearity. + ( + "cut55_5_bare_slot_reject", + Expect::Reject("surface-parse-error"), + ), + ]; + + for (stem, expect) in table { + let (ok, stderr) = check(stem); + match expect { + Expect::Accept => { + assert!( + ok, + "fixture `{stem}` must be ACCEPTED (exit 0) by the \ + post-#55 ownership surface, but `ail check` rejected \ + it. stderr:\n{stderr}" + ); + } + Expect::AcceptWithWarning(code) => { + assert!( + ok, + "fixture `{stem}` must exit 0 (the `{code}` advisory \ + is a warning, not an error), but `ail check` exited \ + non-zero. stderr:\n{stderr}" + ); + assert!( + stderr.contains(&format!("[{code}]")), + "fixture `{stem}` must emit the `[{code}]` advisory \ + warning, but it did not appear in stderr. stderr:\n{stderr}" + ); + } + Expect::Reject(code) => { + assert!( + !ok, + "fixture `{stem}` must be REJECTED (non-zero exit) by \ + the post-#55 ownership surface, but `ail check` \ + accepted it (exit 0). stderr:\n{stderr}" + ); + assert!( + stderr.contains(&format!("[{code}]")), + "fixture `{stem}` must be rejected with diagnostic code \ + `[{code}]`, but that code did not appear in stderr. \ + The reject may have moved to a different stage or code. \ + stderr:\n{stderr}" + ); + } + } + } +} diff --git a/docs/specs/0065-fieldtest-eliminate-implicit-mode.md b/docs/specs/0065-fieldtest-eliminate-implicit-mode.md new file mode 100644 index 0000000..b2c5681 --- /dev/null +++ b/docs/specs/0065-fieldtest-eliminate-implicit-mode.md @@ -0,0 +1,186 @@ +# Fieldtest — #55 eliminate-Implicit-mode cutover — 2026-06-02 + +**Status:** Draft — awaiting orchestrator triage +**Author:** fieldtester (dispatched by fieldtest skill) + +## Scope + +The #55 cutover (commit `76b21c0`, spec 0062, plan 0121) deleted +`ParamMode::Implicit`. Every fn-type slot on every signature now carries +an explicit `(own T)` or `(borrow T)`; there is no default. The parser +rejects a bare fn-type slot; `borrow-over-value` rejects `(borrow V)` on +a value type (Int/Bool/Float/Unit); `borrow-return` rejects a borrowed +return at the signature; consuming a borrowed value is rejected +(`consume-while-borrowed`); and the `over-strict-mode` advisory lint +suggests relaxing an `(own T)` heap param that the body never consumes to +`(borrow T)`. This fieldtest exercises those decision points as a +downstream LLM author who has only the design ledger, the CLI, and the +examples corpus. Build exercised: `cargo run -q -p ail` against HEAD +(workspace built clean before the run). + +## Examples + +### examples/fieldtest/cut55_1_readonly_length.ail — read-only list helper (decision a) +- A `length` that walks a list and counts, never moving a heap field out. +- Fits scope: the canonical "should I reach for `borrow`?" decision. From + the ledger ("borrow only to read/pass-through a lent heap value") I + wrote `(borrow (con List))` without hesitation. +- Outcome: check ok (exit 0); run prints `3`. Correct first try. + +### examples/fieldtest/cut55_1b_overstrict_own.ail — over-strict own, recursive (decision a, wrong mode) +- `length` annotated `(own (con List))` while only reading. +- Fits scope: probes the `over-strict-mode` lint. +- Outcome: check ok, NO warning. Correct: the recursive call passes the + tail `t` (heap-typed binder) to an own param, so condition 2 of the + lint (no heap binder consumed) legitimately fails — the lint stays + silent. Confirms the lint is not naive. + +### examples/fieldtest/cut55_1c_overstrict_isempty.ail — over-strict own, true read-only (decision a, wrong mode) +- `is_empty` inspects only the head ctor; no binder consumed; `(own)`. +- Fits scope: the clean over-strict trigger. +- Outcome: check prints + `warning: [over-strict-mode] is_empty: param \`xs\` is annotated \`(own ...)\` but the body does not consume it; \`(borrow ...)\` would suffice` + then `ok`, exit 0. Names fn, param, current+suggested mode. Exemplary. + +### examples/fieldtest/cut55_2_consume_map.ail — transform an owned list (decision b) +- `bump` rebuilds a list with each element +1; `print_all` consumes it. +- Fits scope: `own` territory; tests the consume analysis + drop soundness + the cutover activated. +- Outcome: check ok; run prints `11 / 21 / 31`. No crash, no leak symptom, + correct. (Authoring note: my first draft used `unit` for the Nil arm and + got `[unbound-var]: unit`; the canonical Unit literal is `(lit-unit)`, + recoverable from the corpus — not a cutover finding.) + +### examples/fieldtest/cut55_2b_borrow_traversal_clean.ail — clean borrow-traverse-and-rebuild (decision b, false-positive guard) +- `bump` borrows xs and rebuilds a fresh +1 list; the recursive call's + param is `(borrow ...)`, so the tail `t` is only borrowed, never moved + into an `(own)` slot — nothing of the borrowed xs is consumed. +- Fits scope: the false-positive guard for the #58 fix — a borrow-position + use of a heap sub-binder must stay accepted. +- Outcome: check ok (exit 0) — accepted, as required. (The fixture was + originally mislabelled `cut55_2b_consume_borrow_reject` claiming a + consume-while-borrowed reject; that analysis was wrong — the recursive + param is `(borrow)`, not `(own)`, so nothing is consumed. Renamed and + reclassified to the accepted set; see #55-cutover commit `b129af1`.) + +### examples/fieldtest/cut55_2c_consume_borrow_reject.ail — consume a tail binder of a borrowed scrutinee (decision b, intended-wrong) +- `leak` borrows xs, passes the tail binder `t` to an `(own)` sink `sum_own`. +- Fits scope: the consume-while-borrowed boundary. +- Outcome: check errors + `[consume-while-borrowed] leak: \`t\` is consumed while a borrow of it is still live`, exit 1. Rejected as expected (post-#58; see finding below). + +### examples/fieldtest/cut55_2d_consume_borrow_whole.ail — consume the whole borrowed param (decision b, wrong mode) +- `passthrough` borrows xs and hands the whole xs to an `(own)` sink. +- Fits scope: the direct consume-while-borrowed case. +- Outcome: check errors + `[consume-while-borrowed] passthrough: \`xs\` is consumed while a borrow of it is still live`, exit 1. Rejected as expected. + +### examples/fieldtest/cut55_3_value_param.ail — value-typed params read repeatedly (decision c) +- `clamp` reads three Int params multiple times. +- Fits scope: confirms the author writes `own` for value types and the + over-strict lint stays silent on them. +- Outcome: check ok (no warning); run prints `5 / 3`. Correct. + +### examples/fieldtest/cut55_3b_borrow_over_value.ail — borrow on an Int (decision c, wrong mode) +- `double` annotated `(borrow (con Int))`. +- Fits scope: the `borrow-over-value` reject. +- Outcome: check errors + `[borrow-over-value] double: borrow over value type in \`double\`: \`Int\` is an unboxed value type and cannot be borrowed; use \`(own Int)\``, exit 1. Names the fix. Exemplary. + +### examples/fieldtest/cut55_4_borrow_return_reject.ail — borrowed return (decision d, wrong mode) +- `tail_view` declares `(ret (borrow (con List)))`. +- Fits scope: the borrow-may-not-escape rule at the signature. +- Outcome: check errors + `[borrow-return-not-permitted] tail_view: borrow-return not permitted ... a (borrow …) return is refcount-invisible and can outlive its source; this language version forbids it ...`, exit 1. Clear wall; see friction below re: fix not named. + +### examples/fieldtest/cut55_4b_clone_to_return.ail — projection via clone (decision d) +- `head_or_zero` borrows, returns the value-typed head (own Int); + `tail_copy` returns `(clone t)` to lift a borrowed heap field to own. +- Fits scope: the correct escape hatch after borrow-return is rejected. +- Outcome: check ok; run prints `10`. The `clone` hatch works as the + ledger describes. + +### examples/fieldtest/cut55_5_bare_slot_reject.ail — bare param slot (the cutover's core promise) +- `length` with a bare `(con List)` param slot, no mode wrapper. +- Fits scope: "no default; Implicit is gone." +- Outcome: surface parse error + `[surface-parse-error] ... fn-type slot requires a mode: write (own T) or (borrow T) at byte 642`, exit 1. Names both legal forms. Exemplary. + +## Findings + +### [working] borrow / own / value-mode authoring is naturally guessable from the ledger +- Examples: cut55_1, cut55_2, cut55_3, cut55_4b. +- For every example I knew which mode to write from the ledger alone, no + guessing: read-only heap ⇒ `borrow`; transform/consume ⇒ `own`; value + type ⇒ `own`; escape a projection ⇒ return `own` + `clone`. The + decision rule in model/contract 0008 maps cleanly onto realistic tasks. +- This is the feature-acceptance (LLM-utility) evidence: an author + produces correct-moded code on first try, and the modes carry real + meaning (the same `length` is `borrow` while `bump` is `own`). +- Recommended action: carry-on. + +### [working] the four reject diagnostics are precise and (mostly) name the fix +- Examples: cut55_3b (borrow-over-value), cut55_5 (bare slot), + cut55_2d (consume-while-borrowed), cut55_1c (over-strict-mode). +- `borrow-over-value` and the bare-slot parse error both name the exact + legal rewrite (`use (own Int)` / `write (own T) or (borrow T)`). + `over-strict-mode` names param + suggested mode. All exit with the + right code (errors exit 1, the warning exits 0). This is the surface + doing its job for an LLM consumer. +- Recommended action: carry-on. + +### [spec_gap — RESOLVED by #58] consuming a heap field-binder of a borrowed scrutinee +- Examples: cut55_2c vs cut55_2d. +- What happened at fieldtest time: `leak` borrows `xs` and moves the Cons + tail `t` into an `(own)`-param sink — accepted (exit 0, the missed + reject). `passthrough` borrows `xs` and moves the whole `xs` into the + same sink — rejected (`consume-while-borrowed`, exit 1). +- Why spec_gap: the ledger stated only "consuming a borrowed value is + rejected" and "a borrow may not escape into a return". It did not say + whether a pattern-binder projected out of a borrowed scrutinee is + itself borrowed. Two readings: (i) sub-binders inherit borrow, so moving + `t` into an own sink is an illegal escape (then cut55_2c is a missed + reject — a latent unsoundness, a double-free of the caller's + allocation); (ii) only the named param is protected (then cut55_2c is + correct and the ledger is silent). +- Resolution: reading (i) was adopted and shipped as the #58 fix + (`b129af1`): `walk_arm` now seeds a heap-typed sub-binder of a borrowed + scrutinee with `borrow_count = 1`, so cut55_2c now rejects + (`consume-while-borrowed` on `t`, exit 1). The false-positive boundary + is pinned by cut55_2b (a borrow-position use of such a sub-binder stays + accepted). Value-typed sub-binders (the `Int` head) stay freely + consumable. + +### [friction] borrow-return error explains *why* but does not name the fix +- Example: cut55_4. +- The `borrow-return-not-permitted` message gives a thorough rationale + (refcount-invisible, can outlive its source) but stops there. An author + is told what is forbidden, not what to do instead. The natural remedy — + return `(own ...)` and `(clone ...)` the projected field (which I had to + derive myself in cut55_4b) — is exactly the escape hatch the language + provides and would be cheap to name. Sibling diagnostics + (`borrow-over-value`, the bare-slot error) DO name the fix, so this one + reads as inconsistent. +- Recommended action: plan a one-line diagnostic-text addendum suggesting + "return `(own T)` and `(clone …)` the value you want to escape." + +### [friction] consume-while-borrowed wording implies a separate live borrow alias that isn't present +- Example: cut55_2d. +- Message: "`xs` is consumed while a borrow of it is still live." In this + case `xs` IS the borrowed param being consumed; there is no separate + live borrow alias. The wording (lifted from the let-alias class, spec + 0064 class 2) reads oddly for the whole-param case and, like the + borrow-return error, does not name the fix (annotate `own`, or `clone`). +- Recommended action: plan — branch the wording for the + "param-itself-consumed" case vs the "alias-still-live" case, and append + the fix hint. + +## Recommendation summary + +| Finding | Action | +|---|---| +| working — mode authoring guessable from ledger | carry-on | +| working — reject diagnostics precise & name fix | carry-on | +| spec_gap — borrowed-scrutinee field consume accepted vs whole rejected | RESOLVED by #58 (`b129af1`, reading (i)); cut55_2c now rejects, cut55_2b guards the boundary | +| friction — borrow-return error omits the fix | plan (tidy diagnostic) | +| friction — consume-while-borrowed wording + no fix hint | plan (tidy diagnostic) | diff --git a/examples/fieldtest/cut55_1_readonly_length.ail b/examples/fieldtest/cut55_1_readonly_length.ail new file mode 100644 index 0000000..e8aeb2b --- /dev/null +++ b/examples/fieldtest/cut55_1_readonly_length.ail @@ -0,0 +1,40 @@ +; Fieldtest cut55-1 — decision (a): a list helper that READS without consuming. +; +; As an author reading the ledger (model/contract 0008): "reach for +; `borrow` only to read/pass-through a heap value you were lent". A +; length count walks the list and reads it; it does not move any heap +; field out. So `xs` should be `(borrow (con List))`. The recursive +; call passes the tail through in a read position — still a borrow. +; +; Expected: ail check -> ok. ail run -> prints 3. + +(module cut55_1_readonly_length + + (data List + (doc "Monomorphic Int list.") + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn length + (doc "Borrow xs and count its elements without consuming it.") + (type + (fn-type + (params (borrow (con List))) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) + (app + 1 (app length t)))))) + + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body + (let xs + (term-ctor List Cons 10 + (term-ctor List Cons 20 + (term-ctor List Cons 30 + (term-ctor List Nil)))) + (seq (app print (app length xs)) (do io/print_str "\n")))))) diff --git a/examples/fieldtest/cut55_1b_overstrict_own.ail b/examples/fieldtest/cut55_1b_overstrict_own.ail new file mode 100644 index 0000000..f2f6b3a --- /dev/null +++ b/examples/fieldtest/cut55_1b_overstrict_own.ail @@ -0,0 +1,33 @@ +; Fieldtest cut55-1b — decision (a), over-strict `own` that does NOT trip +; the lint (boundary case). +; +; Same shape as cut55-1 but `xs` is annotated `(own (con List))`. One might +; expect the `over-strict-mode` lint to fire (xs is only read at the top +; level). It does NOT: the Cons arm recurses via `(app length t)`, and +; `length`'s own self-param is `(own ...)`, so passing the heap tail `t` +; into it counts as a consume. The lint's premise (consume_count == 0) is +; therefore false, and no warning is emitted. The fixture still legitimately +; ACCEPTs (an over-strict but sound annotation is allowed). cut55_1c is the +; sibling where the lint DOES fire (a true read-only with no recursive +; consume). +; +; Expected: ail check -> ok, exit 0 (no over-strict-mode warning). + +(module cut55_1b_overstrict_own + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn length + (doc "Annotated own but only reads xs — should be flagged over-strict.") + (type + (fn-type + (params (own (con List))) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) + (app + 1 (app length t))))))) diff --git a/examples/fieldtest/cut55_1c_overstrict_isempty.ail b/examples/fieldtest/cut55_1c_overstrict_isempty.ail new file mode 100644 index 0000000..78c3284 --- /dev/null +++ b/examples/fieldtest/cut55_1c_overstrict_isempty.ail @@ -0,0 +1,27 @@ +; Fieldtest cut55-1c — decision (a), over-strict lint on a true read-only. +; +; is_empty inspects only the head constructor of xs. No pattern binder is +; consumed (the Cons arm binds h and t but uses neither). xs is `(own)`. +; Per contract 0008 conditions 1-4 all hold (consume_count 0, no heap +; binder consumed, List is not a value type, body is not intrinsic), so +; over-strict-mode SHOULD fire suggesting borrow. Check exits 0 (Warning). +; +; Expected: ail check -> over-strict-mode warning naming xs/borrow, exit 0. + +(module cut55_1c_overstrict_isempty + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn is_empty + (doc "Own xs but only inspect its head ctor — over-strict, should be borrow.") + (type + (fn-type + (params (own (con List))) + (ret (own (con Bool))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) true) + (case (pat-ctor Cons h t) false))))) diff --git a/examples/fieldtest/cut55_2_consume_map.ail b/examples/fieldtest/cut55_2_consume_map.ail new file mode 100644 index 0000000..23b80fa --- /dev/null +++ b/examples/fieldtest/cut55_2_consume_map.ail @@ -0,0 +1,51 @@ +; Fieldtest cut55-2 — decision (b): consume/transform a heap value. +; +; bump rebuilds the list with each element +1. It moves the tail `t` into +; a recursive call and packs the new head into a fresh Cons. The input +; allocation is consumed (reused conceptually). This is `own` territory: +; the author writes `(own (con List))` for xs without hesitation, since +; the value is transformed and not merely read. +; +; Expected: ail check -> ok. ail run -> prints 11, 21, 31 (each +1). + +(module cut55_2_consume_map + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn bump + (doc "Own xs; return a new list with every element incremented.") + (type + (fn-type + (params (own (con List))) + (ret (own (con List))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) (term-ctor List Nil)) + (case (pat-ctor Cons h t) + (term-ctor List Cons (app + h 1) (app bump t)))))) + + (fn print_all + (doc "Own xs; print each element on its own line, consuming the list.") + (type (fn-type (params (own (con List))) (ret (own (con Unit))) (effects IO))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) (lit-unit)) + (case (pat-ctor Cons h t) + (seq + (seq (app print h) (do io/print_str "\n")) + (app print_all t)))))) + + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body + (let xs + (term-ctor List Cons 10 + (term-ctor List Cons 20 + (term-ctor List Cons 30 + (term-ctor List Nil)))) + (app print_all (app bump xs)))))) diff --git a/examples/fieldtest/cut55_2b_borrow_traversal_clean.ail b/examples/fieldtest/cut55_2b_borrow_traversal_clean.ail new file mode 100644 index 0000000..421b658 --- /dev/null +++ b/examples/fieldtest/cut55_2b_borrow_traversal_clean.ail @@ -0,0 +1,34 @@ +; Fieldtest cut55-2b — decision (b), false-positive GUARD for the #58 fix. +; +; This is the legitimate borrow-traverse-and-rebuild that MUST be accepted. +; `bump` borrows xs and, in the Cons arm, reads the head `h` (a value-typed +; Int, copied), passes the tail `t` to its own recursive call, and packs a +; fresh Cons. The recursive `bump`'s param is `(borrow (con List))`, so `t` +; is only BORROWED, never moved into an `(own)` slot — nothing of the +; borrowed xs is consumed. A fresh List is allocated and returned `own`. +; +; This pins that the #58 fix (inherit borrow on heap sub-binders of a +; borrowed scrutinee) does NOT over-fire: a borrow-position use of a heap +; sub-binder is fine. Contrast cut55_2c (feeds `t` to an OWN sink -> reject) +; and cut55_2d (consumes the whole borrowed xs -> reject). +; +; Expected: ail check -> ok, exit 0. + +(module cut55_2b_borrow_traversal_clean + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn bump + (doc "Borrow xs and rebuild a fresh +1 list; tail t is only borrowed, not consumed.") + (type + (fn-type + (params (borrow (con List))) + (ret (own (con List))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) (term-ctor List Nil)) + (case (pat-ctor Cons h t) + (term-ctor List Cons (app + h 1) (app bump t))))))) diff --git a/examples/fieldtest/cut55_2c_consume_borrow_reject.ail b/examples/fieldtest/cut55_2c_consume_borrow_reject.ail new file mode 100644 index 0000000..af6d46c --- /dev/null +++ b/examples/fieldtest/cut55_2c_consume_borrow_reject.ail @@ -0,0 +1,39 @@ +; Fieldtest cut55-2c — decision (b), genuine consume-while-borrowed. +; +; leak borrows xs, but in the Cons arm it hands the tail `t` to sum_own, +; whose param is `(own (con List))` — that call CONSUMES t, which is a +; heap field of the borrowed xs. Per the ledger, consuming a value you +; only borrowed is rejected (consume-while-borrowed). +; +; Expected: ail check -> error naming the consumed binder and pointing at +; `own`, exit 1. + +(module cut55_2c_consume_borrow_reject + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn sum_own + (doc "Own xs, consume it, return the sum.") + (type + (fn-type + (params (own (con List))) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) (app + h (app sum_own t)))))) + + (fn leak + (doc "Borrow xs but feed its tail to an own-consuming sink — illegal.") + (type + (fn-type + (params (borrow (con List))) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) (app sum_own t)))))) diff --git a/examples/fieldtest/cut55_2d_consume_borrow_whole.ail b/examples/fieldtest/cut55_2d_consume_borrow_whole.ail new file mode 100644 index 0000000..546d8cd --- /dev/null +++ b/examples/fieldtest/cut55_2d_consume_borrow_whole.ail @@ -0,0 +1,35 @@ +; Fieldtest cut55-2d — decision (b), consume the borrowed param as a whole. +; +; passthrough borrows xs and hands the WHOLE xs to sum_own, an `(own)` +; sink that consumes it. The caller of passthrough still owns xs (borrow +; contract), so passthrough consuming it is a double-ownership violation. +; Per the ledger this is consume-while-borrowed and must be rejected. +; +; Expected: ail check -> error naming xs and the own-consuming call, exit 1. + +(module cut55_2d_consume_borrow_whole + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn sum_own + (doc "Own xs, consume it, return the sum.") + (type + (fn-type + (params (own (con List))) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) (app + h (app sum_own t)))))) + + (fn passthrough + (doc "Borrow xs but pass the whole thing to an own sink — illegal consume.") + (type + (fn-type + (params (borrow (con List))) + (ret (own (con Int))))) + (params xs) + (body (app sum_own xs)))) diff --git a/examples/fieldtest/cut55_3_value_param.ail b/examples/fieldtest/cut55_3_value_param.ail new file mode 100644 index 0000000..0caa147 --- /dev/null +++ b/examples/fieldtest/cut55_3_value_param.ail @@ -0,0 +1,34 @@ +; Fieldtest cut55-3 — decision (c): value-typed param read multiple times. +; +; clamp reads n three times (two comparisons + a return). n: Int is a +; value type. Per the ledger, `(borrow V)` on a value type is a check +; error — `own` is the only legal mode for Int/Bool/Float/Unit, even when +; the value is read many times and never "consumed" in the heap sense. +; So the author writes `(own (con Int))` for every param here. +; +; Expected: ail check -> ok (no over-strict warning, value types exempt). +; ail run -> prints 5 (clamp 12 0 5 -> 5), then 3 (clamp 3 0 5 -> 3). + +(module cut55_3_value_param + + (fn clamp + (doc "Clamp n into [lo, hi]. All three params are value-typed Ints, read repeatedly.") + (type + (fn-type + (params (own (con Int)) (own (con Int)) (own (con Int))) + (ret (own (con Int))))) + (params n lo hi) + (body + (if (app lt n lo) + lo + (if (app lt hi n) + hi + n)))) + + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body + (seq + (seq (app print (app clamp 12 0 5)) (do io/print_str "\n")) + (seq (app print (app clamp 3 0 5)) (do io/print_str "\n")))))) diff --git a/examples/fieldtest/cut55_3b_borrow_over_value.ail b/examples/fieldtest/cut55_3b_borrow_over_value.ail new file mode 100644 index 0000000..770850b --- /dev/null +++ b/examples/fieldtest/cut55_3b_borrow_over_value.ail @@ -0,0 +1,20 @@ +; Fieldtest cut55-3b — decision (c), WRONG mode on purpose. +; +; An author who reasons "n is only read, never consumed, so borrow it" +; writes `(borrow (con Int))`. The ledger says this is illegal: borrow on +; a value type is a check error, own is the only legal mode there. I +; expect a `borrow-over-value` error that NAMES the param and tells me to +; use `own`. +; +; Expected: ail check -> error [borrow-over-value], exit 1. + +(module cut55_3b_borrow_over_value + + (fn double + (doc "Borrow a value-typed Int — illegal, own is the only legal mode.") + (type + (fn-type + (params (borrow (con Int))) + (ret (own (con Int))))) + (params n) + (body (app + n n)))) diff --git a/examples/fieldtest/cut55_4_borrow_return_reject.ail b/examples/fieldtest/cut55_4_borrow_return_reject.ail new file mode 100644 index 0000000..997cb54 --- /dev/null +++ b/examples/fieldtest/cut55_4_borrow_return_reject.ail @@ -0,0 +1,28 @@ +; Fieldtest cut55-4 — decision (d), borrow-return rejected at the signature. +; +; An author who wants "give me a view of the first element without taking +; ownership" might try to declare the RETURN as a borrow: +; (ret (borrow (con List))) +; Per the ledger a borrow may not escape into a return; `borrow-return` is +; rejected at the signature. I expect a clear error that tells me the +; return cannot be a borrow (and, ideally, to clone or return own). +; +; Expected: ail check -> error [borrow-return], exit 1. + +(module cut55_4_borrow_return_reject + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn tail_view + (doc "Try to return a borrowed view of the tail — illegal escape.") + (type + (fn-type + (params (borrow (con List))) + (ret (borrow (con List))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) xs) + (case (pat-ctor Cons h t) t))))) diff --git a/examples/fieldtest/cut55_4b_clone_to_return.ail b/examples/fieldtest/cut55_4b_clone_to_return.ail new file mode 100644 index 0000000..02822ae --- /dev/null +++ b/examples/fieldtest/cut55_4b_clone_to_return.ail @@ -0,0 +1,51 @@ +; Fieldtest cut55-4b — decision (d), the correct way to project out of a borrow. +; +; After borrow-return is rejected, the author returns `(own ...)` and uses +; `(clone X)` (the explicit RC inc from contract 0008) to lift a borrowed +; field into an owned value that may legally escape. head_clone borrows +; xs, reads its head h (an Int value — copied freely), and returns it own. +; For the heap-tail case we clone the tail to return an owned view. +; +; This is the "did the author find the clone escape hatch?" check. +; +; Expected: ail check -> ok. ail run -> prints 10 (head of [10,20,30]). + +(module cut55_4b_clone_to_return + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn head_or_zero + (doc "Borrow xs; return its head Int (value type, copied) or 0.") + (type + (fn-type + (params (borrow (con List))) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) h)))) + + (fn tail_copy + (doc "Borrow xs; return an OWNED copy of the tail via clone (escape hatch).") + (type + (fn-type + (params (borrow (con List))) + (ret (own (con List))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) (term-ctor List Nil)) + (case (pat-ctor Cons h t) (clone t))))) + + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body + (let xs + (term-ctor List Cons 10 + (term-ctor List Cons 20 + (term-ctor List Nil))) + (seq (app print (app head_or_zero xs)) (do io/print_str "\n")))))) diff --git a/examples/fieldtest/cut55_5_bare_slot_reject.ail b/examples/fieldtest/cut55_5_bare_slot_reject.ail new file mode 100644 index 0000000..25cb8b5 --- /dev/null +++ b/examples/fieldtest/cut55_5_bare_slot_reject.ail @@ -0,0 +1,26 @@ +; Fieldtest cut55-5 — the cutover's core promise: no defaulted mode. +; +; An author used to the pre-cutover language (or one who forgets the +; rule) writes a bare fn-type param slot `(con List)` with no `own`/ +; `borrow` wrapper. Post-#55 there is no default; the parser/checker must +; reject the bare slot and tell me to annotate a mode. +; +; Expected: ail check -> error (bare slot / missing mode), exit 1. + +(module cut55_5_bare_slot_reject + + (data List + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn length + (doc "Bare param slot — no mode. Must be rejected after the cutover.") + (type + (fn-type + (params (con List)) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) (app + 1 (app length t)))))))