Array count sugar creates a non-well-founded Nat and defeats termination checking

[jasisz]

What I did

bun bend2/main.ts repro-array-fractional-nat.bend --check-only
bun bend2/main.ts repro-array-fractional-nat.bend

type Nat is Data:
  Zero{}
  Succ{pred: Nat}

type Unit is Data:
  Unit{}

def Array.new(-T: Type, d: Nat, x: T) -> Nat:
  d

def bad() -> Nat:
  [0n : Nat*2n+4294967295n]

def drain(n: Nat) -> Unit:
  match n:
    case 0n:
      Unit{}
    case 1n+p:
      drain(p)

def main() -> Unit:
  drain(bad())

What happened

All terms check.

The second command does not terminate. I interrupted it after it continued without output. drain is accepted as structurally recursive: its recursive call receives the Succ field p, but the closed Nat returned by bad never reaches Zero.

The file does not import Base and uses no @unsafe, FFI, law, hole, template, or native definition. Its local Nat has exactly the canonical Zero{} and Succ{pred: Nat} representation.

Inspecting bad shows the closed fractional Nat:

bun -e '
import * as B from "./bend2/bend.ts";
const book = B.book_nil();
await B.book_load(book, "repro-array-fractional-nat.bend", "", new Map());
const d = book.tlds.bad;
if (d?.$ !== "Def" || d.v === null) throw new Error("bad missing");
console.log(B.term_show(B.term_lower(B.term_snf(book, d.v))));
'

32.0000000003359n

After 33 ordinary predecessor steps, this value is -0.999999999664098n. Literal matching treats every nonzero numeric value, including negative and fractional values, as Succ{Lit(v - 1)}. It therefore continues producing Succ forever.

Why it happens

Each source Nat literal is capped at 0xffffffff, but nat_from_term adds a leading Succ chain to the trailing literal without checking the combined value. Here 2n+4294967295n therefore becomes 4294967297.

The array count parser checks the value with JavaScript bitwise operators:

const k = nat_from_term(n) ?? 0;
if (k === 0 || (k & (k - 1)) !== 0) {
  // ...
}
d = Lit(Math.log2(k), n.s);

The bitwise operation narrows both operands to 32 bits, so this check sees 1 & 0 and accepts the count. Math.log2 uses the full 4294967297, producing 32.0000000003359. The result is installed directly in a numeric Lit, and the literal checker treats a numeric Lit as a Nat without validating that its value is an integer.

Array syntax lowers to the hard-coded unqualified Array.new; it does not require importing Base. The local, ordinary definition above returns the generated depth, making the malformed Nat available to live code. drain then exposes the soundness consequence: the descent checker proves termination from the syntactic Succ field, while literal reduction supplies an endless chain of such fields.

The relevant code is bend.ts:2009-2014, with the unchecked sum in nat_from_term and the nonzero-is-Succ reduction in lit_step.

Expected behavior

The count form should test powers of two without 32-bit narrowing and reject this count. Numeric Lit nodes used as Nat should also have a finite, nonnegative integer value. A checked closed live term must not bypass the well-founded descent guarantee this way.

This is separate from #941 and occurs before the runtime limits on arrays. I have not derived a closed Empty, but this already violates the shipped theory's stated weak-normalization guarantee for closed live terms.

Version

bend 2.0.24
commit 99f9c6cd
Bun 1.4.2
Darwin arm64
Apple clang version 21.0.0 (clang-2100.0.123.102)

[VictorTaelin]

Fixed in 2.0.25. nat_from_term now returns nothing past the nat cap, and the array count test is Number.isInteger(Math.log2(k)), so [0n : Nat*2n+4294967295n] is refused at parse ("a power of two count") and no numeric literal can be a non-integer. Pinned as tests/parse/array_count_sum.bend. A side effect you will see: a Succ chain past the cap now prints as 302n+4294967295n instead of a number the parser would refuse. Thank you.

Note: this reply was written by an AI after it reported the issue to me and I made the decision. If anything here is wrong, reply and I will review it myself.