NethermindEth / bflat-riscv64

NativeAOT C# for RISC-V zkVMs

Nethermind's fork of bflat. It compiles C# into a static RISC-V ELF that runs in a zkVM: ZisK, SP1, OpenVM or ZKsync Airbender. Nethermind builds the guest of its stateless executor with it.

Build & use Targets Architecture GitHub

summary.NET 11

input: C# source, .NET 11 libraries
compiler: NativeAOT: ILC and RyuJIT of dotnet-riscv
output: One static ELF, no PIE, no dynamic loader
isa: rv64im, plus Zba Zbb Zbs on ZisK; rv32im on Airbender
abi: Soft-float lp64 and ilp32
not emitted: C, A, F, D: --error-on-* checks the image
platforms: zisk zisk_sim sp1 openvm airbender
runtime: 11.0.101-upstream-perf

Quick start

The image has bflat, the .NET 11 SDK and lld. Mount the current directory and build:

# A ZisK-shaped guest that runs under QEMU or on RISC-V64 Linux
$ docker run --rm --platform linux/amd64 -v "$PWD:/w" -w /w nethermindeth/bflat-riscv64-11 \
    bflat build hello.cs --arch riscv64 --os linux --libc zisk_sim --no-pie --no-pthread \
    --extlib https://github.com/NethermindEth/bflat-libziskos:v1.4.0-alpha.153
$ qemu-riscv64 ./hello

# A guest for the ZisK emulator and prover
$ docker run --rm --platform linux/amd64 -v "$PWD:/w" -w /w nethermindeth/bflat-riscv64-11 \
    bflat build hello.cs --arch riscv64 --os linux --libc zisk --no-pie --no-pthread \
    --extlib https://github.com/NethermindEth/bflat-libziskos:v1.4.0-alpha.153
$ ziskemu -e ./hello

bflat downloads the package from its GitHub release and checks its signature. Build & use has SP1, OpenVM, Airbender and all options.

Targets

Each zkVM target is a platform that a bflat-* package defines. --libc selects the platform, and --extlib gives the package.

platform	arch	package	runs on
`zisk`	riscv64	bflat-libziskos	ZisK: `ziskemu` and the prover
`zisk_sim`	riscv64	bflat-libziskos	`qemu-riscv64`, RISC-V64 Linux
`sp1`	riscv64	bflat-sp1	SP1 v6
`openvm`	riscv64	bflat-openvm	OpenVM, RV64 line
`airbender`	riscv32	bflat-airbender	ZKsync Airbender v3

bflat also builds ordinary linux-x64 programs.

What a zkVM does not give a guest

A zkVM gives a guest much less than a Linux host. bflat links a small module for each gap. The modules are the same on all five platforms.

No kernel: no syscalls, files or processes noos, pal
One hart: nothing wakes a blocked call nothread, tls, guest_subst
No loader to start the runtime ubootstrap, eh
No floating-point hardware soft-float ABI; nofp for the transcendentals
No randomness, no clock; each run must reproduce rng_stupid, gs_cookie
Short runs with a known working set ugc-zero, rhp, rhp_native

How a build works

ILC compiles IL to a RISC-V object. Roslyn compiles C# to IL first. ILC applies the ILC-stage substitutions and the RyuJIT options of the platform.
lld links the object statically. The link adds the runtime, musl and the link-time modules, which use --wrap to replace the OS calls, the thread primitives and some runtime helpers.
The post-link tools change the ELF for the loader. patch_elf.py runs on ZisK, SP1 and Airbender, and flat_image on Airbender.
The entry object starts the runtime. It calls Main. No kernel runs under the guest.

Architecture has the details of each stage.

The runtime

bflat does not use Microsoft's runtime packages. dotnet-riscv builds .NET 11 with its own patch series: 22 patches for the riscv64 base ISA, soft-float and the lp64 ABI, and 67 patches that change RyuJIT, ILC and the NativeAOT runtime for zkVM guests. The riscv32 target adds 7 patches more. Each runtime release is signed, and bflat checks the signature when it downloads the release.

image	runtime release	targets
`nethermindeth/bflat-riscv64-11`	`11.0.101-upstream-perf`	riscv64 platforms, linux-x64
`nethermindeth/bflat-riscv64-11-riscv32`	`11.0.101-upstream-perf`	riscv64 platforms and Airbender

upstream-perf is the name of the patch profile. See Runtime.

Checks

Contracts and proofs. Each function of the C modules has an ACSL contract. Frama-C proves the eh module, and CBMC proves the bounds of the allocator.
Tests on the guest ISA. The module unit tests run under qemu. The vfprintf parser and the allocator are fuzzed.
Guests in CI. CI builds both images, links a guest for each riscv64 platform and runs the Airbender guests in the Airbender simulator.
bflat-ts on each pull request. The bflat-ts suite runs on zk-testing with the image of the pull request.

Verification lists each check and each CI job.