Add Lean 4 solution_2: optimized faithful base sieve, 8-bit flags

[ronald-d-rogers]

Description

This adds PrimeLean4/solution_2: a Lean 4 implementation of the base sieve storing one byte per flag in a ByteArray, single-threaded and faithful.

Revised after @rbergen's review; a point-by-point response is in the comments below.

Why a separate solution rather than improving solution_1

The substantive difference from solution_1 is the flag storage type, and it is visible in a badge characteristic.

solution_1 stores flags in an Array Bool. From include/lean/lean.h in the pinned toolchain, an Array holds one object reference per element:

typedef struct {
    lean_object   m_header;
    size_t        m_size;
    size_t        m_capacity;
    lean_object * m_data[];
} lean_array_object;

Nothing is allocated behind those references for a Bool, since scalars are tagged immediates encoded in the word itself (lean_box is (lean_object*)((n << 1) | 1)). So a Bool slot holds the literal word and the slot is the entire per-flag cost: one machine word, which is sizeof(lean_object*) and therefore target-dependent.

This solution stores flags in a ByteArray, a different structure with a fixed element width:

typedef struct {
    lean_object   m_header;
    size_t        m_size;
    size_t        m_capacity;
    uint8_t       m_data[];
} lean_sarray_object;

That is one byte per flag on any target, so bits=8 here is correct and portable in a way it is not for an Array Bool. The two solutions differ on a badge characteristic, not just internally.

The build also moves from leanpkg on the 2021 4.0.0-m2 toolchain to lake on v4.33.0. That is incidental — it is needed simply because time has passed, and on its own it would have pointed at improving solution_1 rather than adding an entry.

Results

Against solution_1, measured on native x86-64 during review, best of five runs:

Solution	Passes / 5s
badly-drawn-wizards (solution_1)	2937
ronald-d-rogers_lean4_bool8 (solution_2)	13769

About 4.7x. An earlier revision of this description claimed 7.1x from containers built and run under x86-64 emulation on an ARM host; that margin was an emulation artifact and the figure is corrected here and in the README.

Run natively on an Apple M4 Max, solution_2 reaches 2831 passes/second. As a cross-language sanity check on the same machine, base sieves with 8-bit flags that I wrote directly in C and Rust — same algorithm, same odd-only byte buffer, same 5-second harness — reach 3051 and 3009 passes/second. Those are my own reference implementations, not solutions from this repository, and all figures are best-of-three on one machine. They say nothing about placement on the benchmark server.

The solution validates its own output: it prints the prime count and the buffer size to stderr before the timed run, so the count of 78498 and the exact 500001-byte buffer can be checked rather than taken on trust.

Implementation

Storage is odd-only, one byte per odd candidate, so the buffer is exactly 1 + sieveSize / 2 bytes and stepping the index by factor is stepping the number by 2 * factor. A fresh Sieve is constructed per pass and the buffer is allocated inside it.

Four things in the source are Lean-specific and worth flagging for review, since they look unusual next to the C and Rust solutions. All four are explained in comments in the source and in the README:

• The hot loops are tail-recursive functions rather than while loops over mutable state. This is the largest single factor, and the reason is counterintuitive: a USize held as a mutable binding is heap-allocated every iteration, appearing in the generated C as a lean_box_usize call inside the loop body, so that form costs a malloc per marked composite. A USize cannot be a tagged immediate the way a small Nat can, which is why the apparently-cheaper unboxed integer type is the more expensive choice in that position. As function parameters, as here, they are unboxed size_t.
• Bounds checks are discharged by proof rather than disabled. The hot loops carry an erased proof that len ≤ bits.size and derive each access's obligation from the loop comparison already performed, so uget/uset compile to plain indexed loads and stores. The safe get!/set! would repeat that comparison at run time. This moves the check to compile time; it does not skip it, and Lean's equivalent of -no-bounds-check is not used.
• The zero-fill is hand-rolled because Lean has no ByteArray zero-fill primitive, and the obvious ⟨Array.replicate n 0⟩ first builds a boxed Array UInt8 at one word per element — a 4 MB intermediate for a 500 KB buffer. The replacement doubles an owned ByteArray and does one final partial append so the result is exactly the requested size rather than rounded up.
• The timing loop reads the sieve size back through a ref, because Sieve.create sz is pure and loop-invariant and the compiler would otherwise be free to hoist it out and run the sieve once. This is the same guard the C solutions get from volatile and the Rust ones from black_box: one pointer load per pass, and it does not touch the sieve.

Disclosures

Toolchain acquisition. The Dockerfile installs the official elan toolchain manager from a pinned leanprover release, which then fetches the pinned Lean release, rather than building Lean from source in the image. Confirmed acceptable in review as a language project's own release channel rather than an opaque binary.

AI assistance. This implementation was developed with AI assistance. The algorithm, the measurements, and the reasoning above are ones I reviewed and stand behind, and every figure in this PR is reproducible by building and running the solution as submitted. I am disclosing it because § Submission quality makes clear that good-faith effort matters to you, and I would rather state it up front than have it inferred.

Contributing requirements

• I read the contribution guidelines in CONTRIBUTING.md.
• I placed my solution in the correct solution folder.
• I added a README.md with the right badge(s).
• I added a Dockerfile that builds and runs my solution.
• I selected drag-race as the target branch.
• All code herein is licensed compatible with BSD-3.

[rbergen]

Thanks for the detailed write-up, and for making both disclosures up front. That was the right call.

I built and ran both containers on the same machine, native x86-64, no emulation, best of 5 runs each:

Solution	passes / 5s
solution_1	2937
solution_2	13769

That is 4.7x, not 7.1x. The extra margin is an emulation artifact, so the "consistent with native runs" note doesn't hold. Please restate the figure as ~4.7x in both the PR description and the README, or label it explicitly as measured under emulation. It's still a large win and doesn't need the headroom.

On a new solution rather than improving solution_1

A new solution is warranted here, but not for the reason you give.

Toolchain and build system updates are not grounds for a separate solution. This project compares implementations, not toolchains. A move off leanpkg and onto a current Lean is warranted simply because time has passed, and that kind of change can be rolled into an update of an existing solution. On its own it would have pointed at improving solution_1.

What does justify a separate solution is that your storage approach is genuinely different. solution_1 stores flags in an Array Bool; you store them in a ByteArray. Those are different data types with different layouts, and the difference is large enough to change a key characteristic - see below. Please restructure the PR description and the README to lead with that. The toolchain migration is incidental and should be described as such.

solution_1's bits=8 is wrong, and yours isn't

This is worth stating explicitly because it is the cleanest justification for your PR.

From include/lean/lean.h in the toolchain you pin, Array stores one object reference per element:

typedef struct {
    lean_object   m_header;
    size_t        m_size;
    size_t        m_capacity;
    lean_object * m_data[];
} lean_array_object;

Nothing is allocated behind those references for a Bool. Scalars are tagged immediates, encoded in the word itself:

static inline lean_object * lean_box(size_t n) { return (lean_object*)(((size_t)(n) << 1) | 1); }

So a Bool slot holds the literal word 1 or 3, and the slot is the entire per-flag cost. That matches measurement: a 20,000,000-element Array Bool moves VmRSS from 8,232 kB to 166,068 kB, or 8.08 bytes per flag on x86-64. A per-flag heap object would cost 24 bytes or more, since a Lean object header alone is 16.

A flag therefore occupies one machine word, not one byte, and bits=8 is wrong.

But the exact count is not a property of the implementation. It is sizeof(lean_object*) - 8 bytes on a 64-bit target, 4 on a 32-bit one - so bits=64 would overstate what can be claimed. CONTRIBUTING covers this case directly: unknown applies when "an implementation uses a boolean basic type provided by the language, and the language does not define how booleans are logically stored in memory". solution_1 should be bits=unknown.

Your storage is a different type with a fixed width, from the same header:

typedef struct {
    lean_object   m_header;
    size_t        m_size;
    size_t        m_capacity;
    uint8_t       m_data[];
} lean_sarray_object;

ByteArray is one byte per flag on any target, so your bits=8 is correct and portable. The two solutions differ on a badge characteristic, not just internally, and should not be merged into one entry.

I'll open a PR to fix solution_1's labeling myself, that's not on you.

Please fix: image size

The image is 4.47GB, against 1.55GB for solution_1. CONTRIBUTING asks for an AS build stage when a solution needs significantly more to build than to run, and this is a clear case: the binary statically links GMP and needs nothing beyond base libc. I tested a two-stage build - 123MB, identical throughput.

FROM ubuntu:24.04 AS build

ARG ELAN_VERSION=v4.2.4

# build-essential and libgmp-dev are needed to link the Lean executable.
# hadolint ignore=DL3008
RUN apt-get update \
    && apt-get install -y --no-install-recommends \
        build-essential ca-certificates curl libgmp-dev \
    && rm -rf /var/lib/apt/lists/*

# elan's bundled libcurl does not pick up Ubuntu's CA bundle on its own.
ENV SSL_CERT_FILE=/etc/ssl/certs/ca-certificates.crt
ENV SSL_CERT_DIR=/etc/ssl/certs

RUN arch="$(uname -m)" \
    && case "$arch" in \
        x86_64) target="x86_64-unknown-linux-gnu" ;; \
        aarch64) target="aarch64-unknown-linux-gnu" ;; \
        *) echo "unsupported architecture: $arch" >&2; exit 1 ;; \
    esac \
    && curl -fsSL -o /tmp/elan.tar.gz \
        "https://github.com/leanprover/elan/releases/download/${ELAN_VERSION}/elan-${target}.tar.gz" \
    && tar -xzf /tmp/elan.tar.gz -C /tmp \
    && /tmp/elan-init -y --default-toolchain none \
    && rm -f /tmp/elan.tar.gz /tmp/elan-init

ENV PATH="/root/.elan/bin:${PATH}"

WORKDIR /opt/app

COPY lean-toolchain lakefile.toml PrimeLean4.lean ./

RUN elan toolchain install "$(cat lean-toolchain)" \
    && lake build

FROM ubuntu:24.04

WORKDIR /opt/app
COPY --from=build /opt/app/.lake/build/bin/PrimeLean4 ./PrimeLean4

ENTRYPOINT ["./PrimeLean4"]

On the toolchain acquisition

elan is fine. The rule is aimed at opaque binaries, not a language project's own release channel, and the precedent you point at is accurate.

The rest verifies

Output validates at 78498 with a 500001-byte buffer, the output format and tags are correct, hadolint passes against config/hadolint.yml, and both architectures build. Faithfulness holds: Sieve carries the full state, a fresh instance is created per pass, the buffer is allocated at runtime at exactly 1 + n/2, and the run returns the flag array.

Your implementation notes understate one thing

I measured your three flagged items by building single-variable variants of your own solution. All three are real: the hand-rolled zero-fill is worth 1.82x, the proof-carrying uget/uset 1.24x, and ByteArray over Array Bool 2.44x.

The tail-recursion note is the one you undersell. Rewriting the hot loops as while loops over mutable USize state costs 9.6x - that variant is slower than solution_1. The generated C shows why:

v___x_71_ = lean_box_usize(v___x_70_);   // heap allocation, every iteration

lean_box_usize allocates, because a USize cannot be a tagged immediate the way a small Nat can. So it's a malloc per marked composite. It's also why Nat with while loops beats USize with while loops by 4.5x in my measurements, which is counterintuitive enough to be worth stating plainly in the README.

One correction: the comment on Sieve.run claims the destructuring is what keeps the buffer uniquely referenced. On v4.33 it makes no measurable difference - { s with bits := ... } compiles to the same thing. Either drop that comment or soften it.

Summary of what I need from you

1. Restructure the PR description and README to justify the new solution on the storage difference, not the toolchain migration.
2. Correct 7.1x to ~4.7x, or label it as emulated.
3. Switch the Dockerfile to the two-stage build above.
4. Drop or soften the Sieve.run destructuring comment.

AI disclosure

This review was drafted with AI assistance. I take ownership of its contents and stand by them personally.

[ronald-d-rogers]

Thanks — this was a genuinely useful review, and the storage argument is a better justification than the one I made. All four items are addressed in 3d8eedf.

1. Justify on storage, not toolchain

Restructured both the PR description and the README to lead with ByteArray versus Array Bool as the substantive difference, with the lean_array_object / lean_sarray_object layouts and the lean_box tagging quoted from the pinned toolchain's lean.h — I checked both structs in v4.33.0 rather than taking them from your review. The leanpkg → lake and 4.0.0-m2 → v4.33.0 move is now described as incidental in both places, explicitly as something that would have pointed at improving solution_1 on its own.

Your framing of the bits badge is the part I had missed: the interesting claim isn't that ByteArray is faster, it's that one byte per flag is a property of the type on every target, which is not true of a slot whose width is sizeof(lean_object*). Agreed on bits=unknown for solution_1, and thanks for taking that on yourself.

2. The 7.1x

Corrected to ~4.7x in the PR description and the README, with a note that the earlier figure came from containers under x86-64 emulation. I can't reproduce a native x86-64 run on this host, so the README attributes the 2937 / 13769 figures to measurement during review rather than presenting them as mine.

3. Two-stage build

Switched to your Dockerfile as written. Built natively on arm64 here, the image is 145MB against 4.47GB before. The gap from your 123MB is the base image difference — ubuntu:24.04 is larger on arm64 than amd64 — so it lines up with what you saw.

Throughput is unchanged by construction, since the build stage is identical and only what gets copied out of it differs; the container run confirms it at 13343 passes per 5s against 13759 for the same binary run on the host in the same session. ldd on the copied binary confirms your reasoning about the runtime stage: only libc, libpthread, libdl, librt and libm, no libgmp. Output still validates at 78498 with a 500001-byte buffer, and hadolint --config config/hadolint.yml is clean.

4. The Sieve.run comment

Softened rather than dropped: it now states that the buffer has to stay uniquely referenced for uset to update in place, and that on v4.33 the destructuring form and { s with bits := ... } compile to code that does so equally well. That keeps the invariant documented without the false attribution.

On the USize boxing point

You're right that I undersold it, and lean_box_usize is the mechanism I hadn't pinned down. I found the effect when developing this — rewriting the loops into tail-recursive form was by far the largest single win — but I had explained it to myself as generic "mutable state overhead" rather than a malloc per marked composite. It's now stated plainly in the README and in the comment on sieveLoop, including that Nat beats USize for while-loop state, which is the part most likely to save someone else a wasted afternoon.

One thing to flag: the README now cites your multipliers (1.82x zero-fill, 1.24x proofs, 2.44x ByteArray, 9.6x and 4.5x for the loop forms) as measured during review, since I didn't build the single-variable variants myself. If you'd rather the README not carry numbers I haven't reproduced, say so and I'll either reproduce them or cut them to qualitative statements — I don't want measurements presented as mine when they aren't.

On the toolchain acquisition

Understood, and the disclosure in the description is trimmed to a note that the elan approach was reviewed and accepted.

AI disclosure

This response was generated with AI assistance, as was the implementation itself. I take ownership of its contents and stand by them personally. The measurements in it are ones I ran on this machine, and the reasoning is mine to defend.

[rbergen]

I'm writing this comment without AI assistance: thank you for incorporating the changes I requested. This solution looks good to me now, and I'm happy to merge it.

With regards to the numbers I mentioned that you included: that's your call, and I believe you've already made it.

Thank you for your contribution!

[ronald-d-rogers]

Thank you for merging!