Lean 4 → Solana

Submission to the Colosseum Solana Hackathon by Latinum.

This is a fork of Lean 4 that turns it into a cross-compiler for Solana. You write a Solana program in Lean 4, prove properties about it with Lean's theorem prover, and the same source elaborates to a Solana SBF .so deployable to mainnet — no Rust in the loop.

Two end-to-end demos built on top of the cross-compile backend, both in this repo:

Colosseum/Colosseum.lean — the headline submission. A deposit/withdraw vault whose safety theorems are part of the source file, proven by Lean's kernel and re-checked on every lake build.

The safety invariant is one line:

def Vault.ok (v : Vault) : Bool :=
  v.balance.toNat + v.totalOut.toNat == v.totalIn.toNat

"The vault never owes more than it took in."

The theorems sitting next to the program code are universally quantified — they hold for every starting state, every amount, every account:

theorem withdraw_preserves_ok
    (v : Vault) (amount : UInt64)
    (h_ok  : v.ok = true)
    (h_pre : amount ≤ v.balance)
    (h_out : v.totalOut.toNat + amount.toNat < UInt64.size) :
    (v.withdraw amount).ok = true := by
  have h_pre_nat : amount.toNat ≤ v.balance.toNat := UInt64.le_iff_toNat_le.mp h_pre
  simp only [Vault.ok, Vault.withdraw, UInt64.toNat_add, beq_iff_eq] at *
  rw [UInt64.toNat_sub_of_le _ _ h_pre, Nat.mod_eq_of_lt h_out]
  omega

The hypotheses are real: h_pre rules out underflow (you can't withdraw more than the balance), h_out rules out UInt64 overflow on totalOut. A companion deposit_preserves_ok proves the same for deposits.

Delete the balance := v.balance - amount line in Vault.withdraw — the canonical "balance leak" exploit — and withdraw_preserves_ok becomes unprovable. The file fails to elaborate. lake build refuses to emit a .so. The bug cannot ship. Same source, same compile pass, no separate audit step.

One command does the whole devnet round-trip:

cd Colosseum
./demo.sh

demo.sh runs lake build (proofs check, .so is emitted), solana program deploy, then a bun demo.ts client that submits a deposit and a withdraw, printing Solana Explorer URLs for every transaction. See the tech demo video for the live run.

tests/kernel_riscv64/ — a full bare-metal kernel built from Lean source through the same cross-compile pipeline. ~3500 lines of Lean covering:

• Kernel/Core.lean — scheduler, trap handler, syscall dispatch (2872 lines)
• Kernel/Memory.lean — frame allocator
• Kernel/Sv39.lean — Sv39 paging
• Kernel/Hardware.lean — UART, CLINT, SATP, SFENCE
• Main.lean, boot.S, kernel.c, kernel.ld — entry, trap vector, linker script

The kernel reasons in Lean about its own actions (Kernel.step, Kernel.trapStep?) and emits each step as a tagged Action the C glue executes. Every syscall trap logs a "Lean theorem: …" proof obligation as it runs, so the QEMU serial output reads as the kernel justifying itself live.

One command boots it:

cd tests/kernel_riscv64
./demo.sh          # cross-compiles → links → boots in qemu-system-riscv64

This is the stress test that proves the freestanding runtime is real — no stdlib, no allocator, no host syscalls, just bitcode + a linker script + a serial port.

Solana programs hold real money and run inside a strict sandbox. Today they are written in Rust, where correctness lives in tests and audits. Lean 4 is one of the few production-grade languages where you can write a program and a machine-checked proof about it in the same file. The proof, the spec, and the deployed bytecode are all derived from the same source — there is no gap to bridge by hand.

This work makes that pipeline real:

   Foo.lean  ──►  lean --target=sbf-solana-solana  ──►  Foo.bc
                          │                                │
                          ▼                                ▼
                  proofs checked by                leanc --target=…
                    Lean's kernel                          │
                                                           ▼
                                                        Foo.so  ──►  solana program deploy

A complete cross-compilation backend in the Lean 4 compiler, three runtime adapters, a Solana SDK in Lean, and the Lake build integration to drive it.

The Lean LLVM backend was host-only — it hardcoded i64 for size_t, never stamped a data layout, and exposed every internal symbol. I rewrote it to be target-driven:

• New compiler options compiler.target, compiler.runtime, compiler.crossImports (src/Lean/Compiler/Options.lean)
• --target=<triple> flag end-to-end through lean and leanc (src/Lean/Shell.lean, src/Leanc.lean)
• Canonical LLVM data layouts pre-extracted for sbf-solana-solana, wasm32-*, riscv64-unknown-none (src/Lean/Compiler/IR/EmitLLVM.lean). The host's LLVM doesn't know these triples, so we ship the layouts.
• size_t / usize / unsigned types now plumbed through the emitter context — wasm32 gets i32, SBF gets i64, host stays as-is.
• Zero-arg decls compile to _init_<name>() calls instead of writable globals on cross targets — Solana's BPF loader rejects writable segments.
• Symbol visibility tightened: only @[export]-annotated decls reach .dynsym.

A Solana program that calls IO.FS.readFile is a link-time disaster waiting to happen. New machinery surfaces those errors at compile time with the right source location:

• register_unsupported_on_target <decl> <triple-glob> <reason> command (src/Lean/Compiler/UnsupportedOnTargetCmd.lean) — validates the decl name exists at registration time, so a typo in the policy file fails fast instead of silently letting calls slip through.
• Persistent env extension stores the deny list across modules (src/Lean/Compiler/UnsupportedOnTarget.lean)
• Reachability check intersects the deny list with collectUsedDecls, then walks IR with new collectDirectCallersOf (src/Lean/Compiler/IR/EmitUtil.lean) to print the user-side callers with file:line (src/Lean/Compiler/IR/EmitLLVM.lean — checkUnsupportedOnTarget)
• Default deny list for every cross target — filesystem, processes, real-time clock, host environment, threads, host stdio, networking and libuv, mutex/condvar/promise primitives, Thunks, Float arithmetic, share-common, String slice/pattern helpers — ~140 entries in src/Std/Freestanding/Unsupported.lean, auto-imported through compiler.crossImports.
• Companion Nat-literal cap check in checkFreestandingNatLiteralCaps — same "fail at compile time, not at the linker" philosophy applied to executable Nat literals that exceed the target's tagged small-Nat payload (32-bit cap on wasm32, 63-bit on 64-bit targets), reported with the source decl and file:line.

The Solana log syscall is only useful for its side effect. The LCNF pure-mode passes happily deleted it. Fixed in src/Lean/Compiler/LCNF/ElimDead.lean and src/Lean/Compiler/LCNF/Simp/Main.lean: @[never_extract]-tagged calls are pinned through both dead-let elimination passes.

A libc-free, host-runtime-free runtime that every cross target shares (src/runtime/freestanding/):

• Reclaiming allocator over an embedder-supplied heap — scans for reusable free blocks before extending the high-water cursor, coalesces adjacent free blocks. No libc malloc/free.
• Real single-threaded reference counting: lean_is_exclusive, persistent marking, recursive release of owned fields, constructor reset/reuse — the host invariants generated code relies on for copy-on-write to fire correctly.
• Copy-on-write for Array / ByteArray / FloatArray (push, uset, swap, pop, …) — mutate in place when exclusive, otherwise allocate a copy first.
• Boxing, ctor alloc/accessors, IO-result wrappers, pointer-address and mix-hash helpers
• Single-threaded ST.Ref cells (new LEAN_TAG_REF)
• Strings, arrays, scalar arrays
• Closure machinery for arities 1–16 (plus lean_apply_n / lean_apply_m)
• Bounded small-Nat / small-Int subset capped at (uintptr_t)-1 >> 1; arithmetic that would require MPZ-backed values traps instead of silently truncating
• ABI mirrors host lean.h exactly — silent miscompute lurks here if it drifts. See src/runtime/freestanding/AUDIT.md for the ownership/layout audit against lean.h, object.cpp, and apply.cpp.

Per-target adapters layer on top:

Each adapter ships a stubs.c listing every host-runtime symbol it cannot provide. Calls to those symbols fall through __builtin_trap() after logging a lean-<target>: unsupported Lean runtime symbol: <name> line, so omissions fail loudly with grep-able output.

A user-facing Solana programming surface in src/Std/Solana.lean (~2400 lines). Highlights:

• Pubkey as a length-refined ByteArray (size_eq : bytes.size = 32) — the proof obligation prevents constructing an invalid key
• AccountInfo, ProgramContext, Instruction mirroring the SBF ABI
• @[solana_entrypoint] attribute shorthand that exports lean_sol_entry_typed
• msg / msg! logging via sol_log_ syscall
• PDA derivation, CPI invocation helpers

A user program is just:

import Std.Solana
open Std.Solana

@[solana_entrypoint]
def entry (ctx : ProgramContext) : UInt64 :=
  msg! s!"hello from lean: {ctx.accounts.size} accounts"
  0

Three new build kinds — solana_program, wasm_program, freestanding_program — all thin wrappers over a shared CrossProgram pipeline in src/lake/Lake/Build/CrossProgram.lean so the cross-build logic lives in one place. lake init … solana scaffolds a deployable Solana program.

# lakefile.toml
[[solana_program]]
name = "my_program"

$ lake build
$ solana program deploy build/bin/my_program.so

• tests/stdlib_probes/ — 62 probes (one per stdlib feature: arrays, strings, Nat overflow, monads, well-founded recursion, structures, …) that run identically on host, SBF, and wasm to catch ABI drift before it ships.
• tests/freestanding_runtime/ — host-side differential C driver that compiles the freestanding runtime as a plain host library and exercises copy-on-write and reclamation invariants directly. No Lean compiler or cross backend required, so RC/exclusivity/allocator regressions surface even when no target is in the build.
• tests/freestanding_sync/ — companion driver covering the single-threaded synchronization surface.
• tests/solana/ — Counter, AddressBook, PDA, CPI shape, Borsh round-trip — plus the Colosseum vault — with a deploy harness + TS client (run_test.sh, deploy_client.ts).
• tests/wasm/ — WASI execution via Node / wasmtime.
• tests/cross_target/ — golden tests for the diagnostic output of the deny list and the Nat-literal cap.
• .github/workflows/cross-compile.yml — CI matrix exercising every target on every PR.

Build a Lean toolchain with the LLVM backend turned on:

cmake --preset release-with-llvm
make -j$(sysctl -n hw.logicalcpu) -C build/release-with-llvm   # use $(nproc) on Linux

Then run either showcase:

# Colosseum vault: build → deploy to devnet → deposit → withdraw
cd Colosseum && ./demo.sh

# RISC-V kernel boots in QEMU (Ctrl-A then X to exit)
cd tests/kernel_riscv64 && ./demo.sh

src/
  Lean/Compiler/
    Options.lean                  ← target/runtime/crossImports options
    UnsupportedOnTarget.lean      ← deny-list machinery
    UnsupportedOnTargetCmd.lean   ← `register_unsupported_on_target`
    IR/EmitLLVM.lean              ← triple-aware codegen
  Leanc/CrossTarget/
    SBF.lean                      ← Solana driver
    Wasm.lean                     ← WebAssembly driver
    RiscV64Freestanding.lean      ← bare-metal RISC-V driver
  Std/
    Solana.lean                   ← user-facing Solana SDK
    Wasm.lean                     ← WASI surface
    Freestanding/Unsupported.lean ← deny list
  runtime/
    freestanding/                 ← shared libc-free runtime
    sbf/                          ← Solana adapter + entrypoint
    wasm/                         ← WASI adapter + entrypoint
  lake/Lake/Build/
    CrossProgram.lean             ← shared cross-build pipeline
    SolanaProgram.lean
    WasmProgram.lean
    FreestandingProgram.lean
Colosseum/                        ← 🏛️ headline showcase: vault + proofs + devnet demo
tests/
  stdlib_probes/                  ← cross-target conformance suite
  freestanding_runtime/           ← host-side RC / CoW / reclamation driver
  freestanding_sync/              ← single-threaded sync driver
  solana/                         ← deployable program tests + TS client
  wasm/                           ← WASI tests
  cross_target/                   ← deny-list + Nat-literal cap diagnostics
  kernel_riscv64/                 ← ⚙️ bare-metal RISC-V kernel demo

Apache 2.0, same as upstream Lean 4. See LICENSE.