Goose

Index types and bounds-check-free functions

This proposal adds two features that are meant to ship together. An index type u32 in nodes is an integer that is a valid index of the global array nodes wherever it can be named, so indexing with it needs no check. A checkfree fn is a function the compiler rejects if any bounds check is left in it. Together they let a programmer move the bounds checks of a hot loop to where its data enters the program, and have the compiler confirm that the loop is left with none. This was TODO 0e of the spec, and is the answer to the indirect-indexing gap TODO 0f lists. Both features are implemented (spec §3.11 and §7.14). This note keeps the reasoning behind them; §8 to §10 record how they were built, what building them turned up, and what they measure.

1. The check no analysis removes

The bounds-check pass (§10.5, src/bce.h) proves most checks in ordinary loops. The common case it keeps is an index read out of another array:

fn relax(adj: i32[>..]&, dist: i32[>..]&, u: i64) {
    for k in adj.len {
        let w = adj[k];                              // elided
        if dist[w] < 0 { dist[w] = dist[u] + 1; }    // the first dist[w] is kept
    }
}

The same shape is graph edges (dist[adj[k]]), mesh index buffers (verts[tri.a]), sort permutations (vals[order[i]]), union-find (parent[x]) and handle tables. bench/goose/graph_csr.goose keeps a check per edge on out[k] and on dist[w], per vertex on dist[u] and on start[u + 1] (an i32 sum, which may wrap), and two in the build loop on cursor[s] and out[cursor[s]] (goose --check --bce-lines).

Proving dist[w] takes ∀k: 0 <= adj[k] < dist.len, a fact about the contents of one array relative to the length of another. A smarter analysis does not get there:

Pool-relative references (§3.9) already cover part of this. adj: Node&<u32 in nodes>[>..]&, with dist moved into Node, compiles relax with no checks at all, because a link is validated where it is stored and a load is base + off - 1. What they cannot do is reach a parallel array: dist, visited and parent are indexed by the same node id and are usually allocated per query, not part of the node.

2. Index and bound types

2.1 Spelling

type        := "const"? (prim | qname tyargs? | "(" type ")") postfix*
             | indextype
indextype   := ("u8" | "u16" | "u32" | "u64") ("in" | "upto") qname

u32 in nodes is an index type of nodes, u32 upto edges a bound type of edges. An index type takes no postfix directly: an array of them is (u32 in nodes)[>..], a cast to one is x as (u32 in nodes). An alias reads better at every use and is the expected style:

type NodeId = u32 in nodes;
var edges: NodeId[>..] = [];

upto is a keyword only directly after an unsigned type name in a type, as in already is inside T&<u32 in pool>. qname resolves as a pool's name does, in the namespace of the declaration the type is written in.

2.2 What a value means

A value of uN in a is an integer v with 0 <= v < a.len, at every point of the program where it can be observed. A value of uN upto a has 0 <= v <= a.len: the end of a range, such as a CSR offset.

a names a global var or reusable var of a grow-only type T[>..] whose elements are fixed-size, so that it can be indexed. Anything else is a compile error: a local or parameter has no name where a field's type is written (as for in pool), a grow-shrink or limited array can shrink, and a sequential array cannot be indexed. Unlike in pool, the element type is unrestricted.

The array is part of the type's identity: u32 in nodes is neither u32 nor u32 in edges, and two widths of one array are different types. The representation is the plain unsigned integer. The array is not stored and the generated C does not see the type.

2.3 Making one

2.4 Using one

2.5 How values pass through

2.6 What may not hold or make one

2.7 The array never shrinks

An array that an index or bound type names is never shrunk. pop, pop_n, resize, clear and a whole assignment of it are errors, anywhere in the program, directly or through a reference parameter. The per-specialization shrink summaries that §5.1 already keeps for globals find every such shrink. The error names the index type that pins the array. A shrink through a reference whose root only bounds the storage (§9.5) is rejected where an array the root may reach is of a named array's type, which is conservative. Element writes, push, append and a reusable pool's free (whose slot stays a valid element, §5.4) are unaffected.

3. Why it is sound

The invariant is that every live value of uN in a is less than a.len (<= for upto).

Nothing here involves lifetimes. Rust needs generative lifetimes to keep a branded index from outliving its container (the indexing crate), and Ada's index subtypes (array (Vertex) of T) fix the bound when the type is elaborated. Goose gets a bound that only grows from the grow-only/grow-shrink split, which is the same monotonicity §10.5 already relies on.

The contents of a change freely. Only its length matters.

4. What bounds-check elimination gets from it

5. Index types and relative references

Both are links that are checked once, when stored, and trusted when used. Both rest on the same argument: a grow-only global target that nothing live can see shrink. They differ in what the link names. A relative reference names an element: following it is all it does, and it is a T& with a root, constness, .= relinking and a free null. An index names a position in a numbering: it is a number that reaches several arrays and can be computed with, compared, sorted, hashed and sent out of the process. With an index type, &nodes[w] turns an index into a reference without a check.

Node&<u32 in pool> u32 in nodes
Reaches the one array it points into, or a field inside an element a and any array the analysis knows is at least as long
Load base + off - 1, one addressing mode base + i * sizeof(T), free only for element sizes 1, 2, 4 and 8
Null the optional form, offset 0 none: an ADT or a sentinel
Arithmetic, order, hashing no (via index_of) yes, as a plain number
u16 covers 64 KB of pool bytes 65,535 elements of any size
Images rejected by from_bytes verified by from_bytes
Variable-size elements yes (§3.3's index of links) no: such an array cannot be indexed
Local or parameter arrays self-relative form no (v1)

Prefer relative references where a link is only ever followed to one element, and maybe relinked or null: linked lists and trees in a pool, map slots pointing at nodes (bench/goose/lru.goose). Prefer indices where the id is used as a number: to reach parallel arrays, to compute neighbours or ranges (i + W, CSR offsets), to compare or sort, or to leave the process.

A mesh is a case where both work and indices are the better choice. With verts: Vertex[>..] of 32-byte vertices, Vertex&<u32 in verts> links in Tri serve CPU code that reads positions. Indices still win, for four reasons. The index buffer goes to the GPU as it is. It loads from file formats as it is, with from_bytes doing the one check. u16 indices, the norm below 65,536 vertices, would reach only 2,048 vertices as u16 in pool. And per-vertex attributes added later (normals, skinning weights, SoA columns for SIMD) are parallel arrays the same index reaches.

6. checkfree functions

6.1 Meaning

fndecl := ("export" strlit? | "extern" strlit?)? "checkfree"? "inline"? "simd"? "recursive"?
          ("fn" | "thread_fn") ...

checkfree fn f is a compile error if a bounds check is left anywhere in f's body after bounds-check elimination. That covers every copy of the body: each specialization, each simd version and each inlined copy. The annotation changes nothing about what the program computes or how it is compiled. checkfree is a keyword only directly before inline, simd, recursive, fn or thread_fn, so it stays usable as a name.

Bounds checks are the index and slice checks of §9.3, conversions into index and bound types (§2.3), and free(i)'s index check. The other aborts of §9.3 are not:

assert in particular is how a checkfree function states its preconditions once, outside its loops.

6.2 Calls

Every call in a checkfree body is to a checkfree function, a builtin or an extern.

So the guarantee is transitive: no bounds check runs while a checkfree function is executing. Small helpers called from hot loops (swap, min, max, vector math) are expected to be checkfree themselves.

6.3 Where its facts come from

A function's entry facts come from its call sites (§10.5). A checkfree function relying on them can stop compiling when a new caller elsewhere fails to establish them. In that case the error names that call site and the fact it does not establish. The robust style needs no callers' facts:

Each is one check per call, outside the loop, and reads as documentation of the precondition.

6.4 What every implementation must prove

§10.5 says nothing about a program's meaning depends on how much the analysis proves. checkfree makes whether a program compiles depend on it, so the spec fixes a core: checks every conforming implementation must elide inside a checkfree function. Accepting anything beyond the core is implementation-defined. A program written to the core compiles under every version of the analysis.

A kill of a fact about x is, between the fact and the check, a write to x, a shrink of an array in the fact, a growth of the array an index type names, or a call whose effect summary says it may do one of these. The core:

  1. A constant index into a fixed array, in range, and an index whose type's whole range fits a fixed array (a u8 into a [256]).
  2. An index of an index type of a, into a.
  3. An index of an index type of a into b, where b.len >= a.len (or ==) was asserted or established by a counted fill, with no kill in between.
  4. A for index into the array its count or range end is the length of (for i in a.len, for x, i in a, for i in lo..a.len with lo >= 0 known), with no shrink of a in the body.
  5. a[i] where a condition (while, if, guard or assert) established i < a.len, with no kill in between, for an i known to be non-negative: an unsigned type, an index type, or a local that starts non-negative and is written only by ++ and += of a non-negative constant.
  6. A check identical to one already passed on the same path, with no kill in between.

Everything else the analysis proves (products, reductions with % and &, facts from callers, effect summaries, step counters) is best-effort.

6.5 Diagnostics

The error is per remaining check, at its index, with the source line. It says why, in the terms of docs/implementation.md §9.1's "Kept" list. The implemented reasons:

Two reasons are not implemented yet, since they need the pass to keep provenance it does not keep today:

6.6 Flags and combinations

graph_csr.goose written with index types. The graph is global and built once. Per edge the traversal does no check, and per vertex none either.

struct Node { lo: u32 upto edges, hi: u32 upto edges }

var nodes: Node[>..] = [];
type NodeId = u32 in nodes;
var edges: NodeId[>..] = [];

// Builds the graph from an edge list nothing has validated: these checks are
// the only ones the traversal will ever need.
fn build(nv: i64, src: i32[:], dst: i32[:]) {
    let empty = 0 as (u32 upto edges);            // 0 <= edges.len always
    for v in nv { nodes.push(Node { lo: empty, hi: empty }); }
    var first: i64[>..] = [];                     // CSR offsets
    for v in nv + 1 { first.push(0); }
    for e in src.len { first[src[e] + 1]++; }
    for v in nv { first[v + 1] += first[v]; }
    var next: i64[>..] = [];
    for v in nv { next.push(first[v]); }
    let some = 0 as NodeId;                       // aborts for an empty graph
    for e in dst.len { edges.push(some); }
    for e in src.len {
        let s = src[e];
        edges[next[s]] = dst[e] as NodeId;        // one check per edge, here
        next[s]++;
    }
    for v in nv {
        nodes[v].lo = first[v] as (u32 upto edges);
        nodes[v].hi = first[v + 1] as (u32 upto edges);
    }
}

// The sum of distances from src; dist holds an entry per node.
checkfree fn bfs(dist: i32[>..]&, q: NodeId[>..<]&, src: NodeId) -> i64 {
    assert(dist.len >= nodes.len);
    var total = 0;
    q.clear();
    dist[src] = 0;                     // core 3
    q.push(src);
    var qh = 0;
    while qh < q.len {
        let u = q[qh];                 // core 5; u: NodeId
        qh++;
        let d = dist[u];               // core 3
        total += d;
        let n = nodes[u];              // core 2
        for k in n.lo..n.hi {          // k: u32 in edges (§2.3)
            let w = edges[k];          // core 2; w: NodeId
            if dist[w] < 0 {           // core 3
                dist[w] = d + 1;       // core 6
                q.push(w);
            }
        }
    }
    return total;
}

Notes on the example:

8. Implementation

docs/implementation.md §3.13 and §5.5 to §5.12 describe the implementation pass by pass. This section records how it went against the plan.

8.1 The plan held

Every typed store already passes TypeCheck::FitsAt, which is also where in pool checks roots, so making it take only a value of the same array covered nearly every way an element can be written. The risk was integer code that picks a result type by storage width, or by copying an operand's TypeExpr *. Two choke points made that fail closed, as planned: the brand is stripped in TypeCheck::Operand, where every operator operand passes, and every branded destination or join requires the same array. The sites that copied a type along were the ones predicted: MergeVals' constant adapt, UnifyBranch, FitsAt's constant and literal cases, and Converts for the cast judgements. The brand stayed a field on TY_INT rather than a kind of its own.

8.2 What the plan missed

8.3 A soundness bug found on the way

The checkfree_parallel fixture first used an export fn, and the check that should have stayed was elided. A Goose caller's facts are granted to an export fn's entry, but its C wrapper calls the same specialization with arguments nobody checked: export fn api(d: i32[:], i: i64) -> i32 { d[i] } called once from Goose with a known length and index compiles without its check, and C can then read past the end. This predated index types. It is fixed separately (2f7e1b6b): an export, like a thread entry, gets no call-site facts.

8.4 Size

Against the estimate of 400–600 lines: +685 −44 in 19 source files, the typed kills and checkfree's messages included. Plus 28 rejection fixtures, three parse-error fixtures and six programs with blessed output.

9. Testing

10. Measurements

Built by goose build with clang-cl 22 for x64 at its default target, on the development machine, best and median of 9–11 interleaved runs. These are rough numbers, not a benchmark-suite row.

So on clang the value is the guarantee, and the check moved to where data enters the program, more than the speed. MSVC, where a kept check prevents vectorization outright (blur was 1.75x slower with nine checks), and wider instruction sets with gather instructions are untested.

11. Open questions