2.1. An unboxed array🔗

Array UInt64 is not what it sounds like: each element is a separate heap object, because the Array type is generic and stores pointers. Lean's runtime does have flat arrays of fixed-size elements (lean_sarray); the standard library exposes ByteArray and FloatArray on top of it, and nothing for UInt64. So we make one, in the same way the standard library makes FloatArray.

The type has a model, an ordinary Array UInt64, and the proofs are about the model. At runtime, each operation is a line of C on the flat buffer, attached with @[extern c inline]:

This is the point where something is trusted rather than proved, so it deserves to be spelled out. The theorems on this page are about the model. The claim that the C above implements the model is not proved; it is read. That is the same arrangement the standard library uses for every array type. FloatArray.uget is declared @[extern "lean_float_array_uget"], and its C in lean.h is:

static inline double lean_float_array_uget(b_lean_obj_arg a, size_t i) {
    return lean_float_array_cptr(a)[i];
}

static inline lean_obj_res lean_float_array_uset(lean_obj_arg a, size_t i, double d) {
    lean_obj_res r;
    if (lean_is_exclusive(a)) r = a;
    else r = lean_copy_float_array(a);
    double * it = lean_float_array_cptr(r) + i;
    *it = d;
    return r;
}

Ours is the same code with uint64_t in place of double. Array.uget and Array.uset, which Part 1's List code does not use but every array program does, are extern in the same way. So the trusted base of this part is Lean's trusted base plus four lines that a reader can compare with the lines above, and the cross-checks in check.sh exercise them against core's Array.qsort on thousands of inputs. It is a small thing to trust, but it is ours and not the standard library's, and a UInt64Array in the standard library would remove it. If you want zero lines of your own C today, sort Array Nat with USize indices instead: a Nat below 2^63 is a tagged machine word, and the same loop costs about 13% more from the scalar checks on each access.

Two things to notice about the accessors. get takes the bounds proof as an argument, and the argument has a default: by u64, a small tactic defined in the same file that unfolds UInt64 arithmetic to Nat and calls omega. The GetElem instance next to it routes a[i] to get with the same tactic discharging the bound, so the code reads like any other Lean array code, and an index that cannot be proved in bounds does not compile. There is no bounds check at runtime.

set writes in place when the array is not shared. That is the usual Lean rule: values are immutable, but the runtime reuses a buffer whose reference count is one. The hot loops below are written so that this is always the case.

2.2. The sort🔗

A bottom-up merge sort needs no recursion: pass one merges runs of length 1 into runs of length 2, the next pass runs of length 2 into 4, and so on. Each pass reads one buffer and writes the other, then the two swap roles. The input array is one of the buffers, so the sort works in place with one scratch buffer of the same size.

The merge loop is where the time goes. It reads both candidates, selects the smaller one, and advances the index of the side it came from by adding 0 or 1. There is no branch on the comparison, and the C compiler turns the selects into conditional moves. This one change is worth about 40% compared to an if, because a branch on random data is mispredicted half the time.

The proofs in the signature are the loop invariants: both runs lie inside the buffers, i is inside the left run, j inside the right one, and the output position k is where it should be. All of them are auto-parameters, so the recursive call writes none of them. The result type { b // b.size = dst.size } carries the one fact every caller needs.

The merge loop sits in its own module. Otherwise clang inlines it into the pass loop and loses the branchless code.

A pass merges adjacent pairs of runs and stops at the end; the width loop doubles the run length until it covers the array: