Goose

Index types and bounds-check-free functions

Deprecated language features: reusable and reusable[]. Use slot_pool<T> for slots and slice_pool<T> for contiguous runs. Builtin behavior and historical examples below remain relevant to existing code; removal is planned separately, after the remaining migration gaps.

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 it addresses the indirect-indexing gap listed in TODO 0f. 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 was measured.

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 appears in graph edges (dist[adj[k]]), mesh index buffers (verts[tri.a]), sort permutations (vals[order[i]]), union-find (parent[x]) and handle tables. goose --check --bce-lines shows that 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]].

Proving dist[w] requires ∀k: 0 <= adj[k] < dist.len, a fact about the contents of one array relative to the length of another. A smarter analysis would not be enough:

Pool-relative references (§3.9) already cover part of this. With adj: Node&<u32 in nodes>[>..]& and dist moved into Node, relax compiles with no checks, because a link is validated where it is stored and a load is base + off - 1. However, pool-relative references cannot 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 Syntax

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

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. It may include a direct field of a global root, as in u32 in graph.nodes or u32 upto graph.edges. The owner name may be namespace qualified; aliases, reference crossings, indexing and nested field paths are not accepted.

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 cannot be named in a field's type (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.

A mutable grow-only array field of a global var root satisfies the same contract. Its storage identity is the particular owner and field, and only that component is pinned against shrinking.

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 type does not appear in the generated C.

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 if any array that root may reach has the type of a named array. This 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. In Goose, the grow-only/grow-shrink split gives a bound that only grows, which is the same monotonicity §10.5 already relies on.

The contents of a can change freely, since 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: the target is a grow-only global, and nothing live can observe it shrinking. They differ in what the link names. A relative reference names an element: it can only be followed, and it is a T& with a root, constness, .= relinking and a null that needs no extra storage. 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), one addressing mode 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 are still better, 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 only 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. To keep a function independent of its callers, use:

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 that nothing about a program's meaning depends on how much the analysis proves. With checkfree, whether a program compiles does 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 any of the following 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

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

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

6.6 Flags and combinations

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

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 goes through TypeCheck::FitsAt, which is also where in pool checks roots. Making FitsAt accept only a value of the same array therefore 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 *. As planned, two choke points made such code fail closed: the brand is stripped in TypeCheck::Operand, which every operator operand passes through, 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. The facts of a Goose caller were granted to an export fn's entry, but its C wrapper calls the same specialization with arguments nobody checked. For example, export fn api(d: i32[:], i: i64) -> i32 { d[i] } called once from Goose with a known length and index compiled without its check, and C could 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

The estimate was 400–600 lines. The change was +685 −44 in 19 source files, including the typed kills and checkfree's messages, plus 28 rejection fixtures, three parse-error fixtures and six programs with blessed output.

9. Testing

10. Measurements

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

So on clang, the value of index types lies more in the guarantee, and in moving the check to where data enters the program, than in speed. Two setups are untested: MSVC, where a kept check prevents vectorization outright (blur was 1.75x slower with nine checks), and wider instruction sets with gather instructions.

11. Open questions