test(cutover): live accept/reject corpus for the #55 ownership surface
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.
This commit is contained in:
@@ -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}"
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -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) |
|
||||
@@ -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"))))))
|
||||
@@ -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)))))))
|
||||
@@ -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)))))
|
||||
@@ -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))))))
|
||||
@@ -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)))))))
|
||||
@@ -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))))))
|
||||
@@ -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))))
|
||||
@@ -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"))))))
|
||||
@@ -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))))
|
||||
@@ -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)))))
|
||||
@@ -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"))))))
|
||||
@@ -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)))))))
|
||||
Reference in New Issue
Block a user