feat(levels): L4-L10 per-level test suites (Track C complete)

Extends the per-level node.mjs test pattern (established for L1-L3) across
the full 10-level checked core. Each level file imports parseModule +
checkModule and asserts a mix of clean-check and diagnostic-fire outcomes
on small inline .twasm fixtures.

Coverage:
  L4  Null safety (opt<T>, &region<X>, is_null guards)      6 cases
  L5  Bounds-proof (indexed access, where-constraints)      5 cases
  L6  Result-type (field-path resolution, striated ban)     6 cases
  L7  Aliasing safety (QTT-erased; surface carrier only)    5 cases
  L8  Effect-tracking (flat, split, region-qualified)       7 cases
  L9  Lifetime safety (QTT-erased; surface carrier only)    5 cases
  L10 Linearity (QTT-erased; surface carrier only)          5 cases

L7 / L9 / L10 have no ReScript diagnostic surface — enforcement is
Idris2-side and QTT-erased. Those files assert the canonical surface
shapes parse + check clean and point at the relevant Idris2 proof file
(Pointer.idr / Lifetime.idr / Linear.idr), rather than fabricate
diagnostics that do not actually fire.

Justfile test recipe extended to run L4-L10 after L1-L3.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

Justfile

@@ -106,10 +106,17 @@ test *args:
     @echo "Running E2E driver (parse + check every example)..."
     node tests/e2e/e2e-driver.mjs
     @echo ""
-    @echo "Running per-level test suites (L1-L3)..."
+    @echo "Running per-level test suites (L1-L10)..."
     node tests/levels/L1.mjs
     node tests/levels/L2.mjs
     node tests/levels/L3.mjs
+    node tests/levels/L4.mjs
+    node tests/levels/L5.mjs
+    node tests/levels/L6.mjs
+    node tests/levels/L7.mjs
+    node tests/levels/L8.mjs
+    node tests/levels/L9.mjs
+    node tests/levels/L10.mjs
     @echo ""
     @echo "Running Zig FFI tests..."
     cd ffi/zig && zig build test

tests/levels/L10.mjs

@@ -0,0 +1,174 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+//
+// Level 10 — Linearity (exactly-once resource usage, QTT-erased)
+//
+// L10 attests that every linearly-typed resource — an `own region<X>`
+// handle, a `unique<T>` owning pointer — is consumed EXACTLY ONCE
+// along every execution path. Dropping it is forbidden (would leak),
+// and consuming it twice is forbidden (double-free). The Idris2 proof
+// layer (`src/abi/TypedWasm/ABI/Linear.idr`) carries the QTT-native
+// q=1 quantity reasoning plus the propositional state-machine layer
+// added A3 (2026-04-18): `LinHandleU Fresh/Consumed tok`, the
+// `consume` state transition, and the theorems `distinctUsage`,
+// `consumePreservesData`, `noReuse`, `noReuseEcho`.
+//
+// L10 is the third of the three QTT-erased levels (L7 + L9 + L10).
+// As with those, the ReScript checker has NO diagnostic that fires
+// on a "handle consumed twice" or "handle dropped without free"
+// program text today: the analysis is Idris2-side, lifted by QTT,
+// and entirely erased before code generation. Asserting such a
+// diagnostic here would give false confidence.
+//
+// What this file's role IS:
+//   - Certify that the canonical L10 surface shapes — `own region<X>`
+//     round-trip through a function pair (spawn → despawn), with the
+//     handle exactly-once-threaded — parse + check clean.
+//   - Exercise the `region.alloc` / `region.free` statement pair, the
+//     two sides of the linearity contract.
+//
+// Run: node tests/levels/L10.mjs
+
+import { parseModule } from "../../src/parser/Parser.mjs";
+import { checkModule } from "../../src/parser/Checker.mjs";
+
+let passed = 0;
+let failed = 0;
+
+function run(source, expect, label) {
+  const pr = parseModule(source);
+  if (pr.TAG !== "Ok") {
+    failed++;
+    console.log(`  FAIL  ${label} — parse error: ${pr._0.message}`);
+    return;
+  }
+  const diags = checkModule(pr._0);
+  if (expect.kind === "clean") {
+    if (diags.length === 0) {
+      passed++;
+      console.log(`  OK    ${label} — clean check`);
+    } else {
+      failed++;
+      const msgs = diags.map(d => d.message).join("; ");
+      console.log(`  FAIL  ${label} — expected clean, got ${diags.length}: ${msgs}`);
+    }
+  } else {
+    const allMsgs = diags.map(d => d.message).join(" | ");
+    const missing = expect.needles.filter(n => !allMsgs.includes(n));
+    if (missing.length === 0 && diags.length > 0) {
+      passed++;
+      console.log(`  OK    ${label} — diagnostic fired as expected`);
+    } else {
+      failed++;
+      console.log(`  FAIL  ${label} — expected needles ${expect.needles.join(", ")}, got "${allMsgs}"`);
+    }
+  }
+}
+
+console.log("=== Level 10: Linearity (exactly-once, QTT-erased) ===\n");
+
+// ── Positive: region.alloc → owning handle → region.free sequence ────
+// Classic L10 shape: the handle is created, threaded, consumed.
+// At proof-time, QTT q=1 discharges the exactly-once obligation.
+
+run(
+  `region Particle {
+    hp: i32;
+  }
+  fn spawn() -> own region<Particle>
+    effects { Alloc }
+  {
+    region.alloc Particle { hp = 100 } -> p;
+    return p;
+  }
+  fn despawn(p: own region<Particle>)
+    effects { Free }
+  {
+    region.free $p;
+  }`,
+  { kind: "clean" },
+  "spawn/despawn pair — canonical linear handle thread",
+);
+
+// ── Positive: unique<T> field — owning-once pointer inside a region ──
+// `unique<ptr<Inner>>` carries the same q=1 discipline for non-region
+// owning pointers.
+
+run(
+  `region Inner {
+    v: i32;
+  }
+  region Outer {
+    owned: unique<ptr<Inner>>;
+  }`,
+  { kind: "clean" },
+  "unique<ptr<Inner>> field — owning-once pointer",
+);
+
+// ── Positive: own handle passed to a function (consumed) ─────────────
+// A function can take an owning handle as a parameter — the callee
+// is obliged to consume it (free, forward, or store). Surface carrier.
+
+run(
+  `region Resource {
+    id: i32;
+  }
+  fn make() -> own region<Resource>
+    effects { Alloc }
+  {
+    region.alloc Resource { id = 1 } -> r;
+    return r;
+  }
+  fn release(r: own region<Resource>)
+    effects { Free }
+  {
+    region.free $r;
+  }
+  fn pipeline()
+    effects { Alloc, Free }
+  {
+    let r : own region<Resource> = make();
+    release(r);
+  }`,
+  { kind: "clean" },
+  "pipeline: alloc-in-callee, consume-in-callee",
+);
+
+// ── Positive: alloc with field init block + multiple typed fields ────
+// Exercises the `region.alloc T { f = v, g = w } -> handle;` shape.
+
+run(
+  `region Bundle {
+    a: i32;
+    b: f32;
+    c: bool;
+  }
+  fn mint() -> own region<Bundle>
+    effects { Alloc }
+  {
+    region.alloc Bundle { a = 1, b = 2.0, c = true } -> b;
+    return b;
+  }`,
+  { kind: "clean" },
+  "region.alloc with multi-field init block",
+);
+
+// ── Positive: linearly-typed free-list self-reference ────────────────
+// A linked free list: each slot's `next` is a linearly owned pointer
+// to the next free slot. Classic linear-types arena shape.
+
+run(
+  `region FreeSlot {
+    next: opt<ptr<FreeSlot>>;
+  }
+  region Arena[256] {
+    free_head: opt<ptr<FreeSlot>>;
+  }`,
+  { kind: "clean" },
+  "linear free-list arena (linearly-typed self-reference)",
+);
+
+// ── Summary ──────────────────────────────────────────────────────────
+
+console.log(`\n--- L10: ${passed} passed, ${failed} failed ---`);
+process.exit(failed > 0 ? 1 : 0);

tests/levels/L4.mjs

@@ -0,0 +1,173 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+//
+// Level 4 — Null safety (opt<T> tracking)
+//
+// L4 enforces that nullable pointers (`opt<T>`, `opt<@R>`, `opt<ptr<T>>`)
+// are distinct from non-nullable forms in the type system: a function
+// taking `&region<X>` receives a witness that the handle is non-null,
+// while `opt<...>` fields in a region force an explicit `is_null` check
+// before use.
+//
+// Surface exposure in the ReScript checker: L4 is almost entirely
+// structural. The AST distinguishes `OptionalType(...)` from bare
+// `PointerType(...)` / `RegionRef(...)` at parse time; no ReScript
+// diagnostic fires on a "forgot to null-check" pattern today (that
+// analysis lives in the Idris2 `Pointer.idr` / `Levels.idr` Ptr-NonNull
+// witness). What IS testable at this layer is:
+//
+//   - `opt<T>` fields parse + check clean (positive: nullability is a
+//     first-class type constructor).
+//   - `&region<X>` and `&mut region<X>` parameter syntax parses + checks
+//     clean (positive: non-null handle types are well-formed).
+//   - Nested nullable forms — `opt<ptr<T>>`, `opt<@R>` — round-trip
+//     through parser + checker without diagnostics.
+//   - `is_null(...)` as a predicate expression threads through the
+//     checker without firing.
+//
+// The L4 "proven enforcement" — that a read through a non-null handle
+// never dereferences null — lives in the Idris2 proof layer
+// (src/abi/TypedWasm/ABI/Pointer.idr and Levels.idr, Ptr-NonNull
+// witness). This file's role is to prove the ReScript surface accepts
+// all well-formed L4 shapes without false positives.
+//
+// Run: node tests/levels/L4.mjs
+
+import { parseModule } from "../../src/parser/Parser.mjs";
+import { checkModule } from "../../src/parser/Checker.mjs";
+
+let passed = 0;
+let failed = 0;
+
+function run(source, expect, label) {
+  const pr = parseModule(source);
+  if (pr.TAG !== "Ok") {
+    if (expect.kind === "parseErr") {
+      passed++;
+      console.log(`  OK    ${label} — parse rejected as expected`);
+      return;
+    }
+    failed++;
+    console.log(`  FAIL  ${label} — parse error: ${pr._0.message}`);
+    return;
+  }
+  if (expect.kind === "parseErr") {
+    failed++;
+    console.log(`  FAIL  ${label} — should have failed to parse`);
+    return;
+  }
+  const diags = checkModule(pr._0);
+  if (expect.kind === "clean") {
+    if (diags.length === 0) {
+      passed++;
+      console.log(`  OK    ${label} — clean check`);
+    } else {
+      failed++;
+      const msgs = diags.map(d => d.message).join("; ");
+      console.log(`  FAIL  ${label} — expected clean, got ${diags.length}: ${msgs}`);
+    }
+  } else {
+    const allMsgs = diags.map(d => d.message).join(" | ");
+    const missing = expect.needles.filter(n => !allMsgs.includes(n));
+    if (missing.length === 0 && diags.length > 0) {
+      passed++;
+      console.log(`  OK    ${label} — diagnostic fired as expected`);
+    } else {
+      failed++;
+      console.log(`  FAIL  ${label} — expected needles ${expect.needles.join(", ")}, got "${allMsgs}"`);
+    }
+  }
+}
+
+console.log("=== Level 4: Null safety (opt<T> tracking) ===\n");
+
+// ── Positive: opt<@R> field round-trips parser + checker clean ───────
+
+run(
+  `region Vec2 {
+    x: f32;
+    y: f32;
+  }
+  region Enemies[32] {
+    target: opt<@Vec2>;
+    hp: i32;
+  }`,
+  { kind: "clean" },
+  "region field typed opt<@R> (nullable embedded region handle)",
+);
+
+// ── Positive: opt<ptr<T>> — nested nullability on a raw pointer ──────
+
+run(
+  `region FreeSlot {
+    next: opt<ptr<FreeSlot>>;
+  }`,
+  { kind: "clean" },
+  "opt<ptr<T>> — nested nullable pointer field",
+);
+
+// ── Positive: non-null handle parameter — &region<X> shape ───────────
+
+run(
+  `region Players[8] {
+    hp: i32;
+  }
+  fn read_hp(players: &region<Players>, idx: i32) -> i32
+    effects { ReadRegion(Players) }
+  {
+    region.get $players[idx] .hp -> hp;
+    return hp;
+  }`,
+  { kind: "clean" },
+  "&region<X> parameter (non-null shared handle)",
+);
+
+// ── Positive: mutable non-null handle — &mut region<X> ───────────────
+
+run(
+  `region Players[8] {
+    hp: i32;
+  }
+  fn set_hp(players: &mut region<Players>, idx: i32, new_hp: i32)
+    effects { ReadRegion(Players), WriteRegion(Players) }
+  {
+    region.set $players[idx] .hp, new_hp;
+  }`,
+  { kind: "clean" },
+  "&mut region<X> parameter (non-null exclusive handle)",
+);
+
+// ── Positive: is_null predicate on opt-typed field threads clean ─────
+
+run(
+  `region Vec2 { x: f32; y: f32; }
+  region Enemies[16] {
+    target: opt<@Vec2>;
+  }
+  fn check_target(enemies: &region<Enemies>, i: i32) -> i32
+    effects { ReadRegion(Enemies) }
+  {
+    region.get $enemies[i] .target -> maybe_target;
+    if is_null(maybe_target) {
+      return -1;
+    }
+    return 0;
+  }`,
+  { kind: "clean" },
+  "is_null() guard on opt<@R> field",
+);
+
+// ── Positive: opt<primitive> — nullable primitive (u32 example) ──────
+
+run(
+  `region Slot[4] {
+    value: opt<u32>;
+  }`,
+  { kind: "clean" },
+  "opt<u32> — nullable primitive field",
+);
+
+// ── Summary ──────────────────────────────────────────────────────────
+
+console.log(`\n--- L4: ${passed} passed, ${failed} failed ---`);
+process.exit(failed > 0 ? 1 : 0);