Avg

One spec for the floor average of two u64s, and implementations proved to meet it: the Rust source (through Aeneas), and the RISC-V, x86-64 and AArch64 machine code rustc compiles it to.

Reusable Lean assembly exporters live in tooling/; the average proofs are clients, not part of the exporters. examples/identity/ demonstrates independent reuse.

What to review

Lean checks every proof. What it can't check is whether the claims are the right ones, so a reviewer reads these statements (not their proofs):

file	statement	says
core/spec/AvgSpec.lean	IsAvg	r is the floor average: r = (a + b) / 2 over ℕ
backends/aeneas/AvgAeneas/Proofs.lean	rust_avg_correct	the Rust avg never panics and returns an IsAvg result
backends/riscv/AvgRiscv/Proofs.lean	avgProgram_spec	the machine code returns to ra (low bit cleared) with an IsAvg result in a0, preserving the separation-logic frame
backends/x86/AvgX86/Proofs.lean	avgProgram_correct	Kraken's straight-line execution, with a return address loaded at rsp, returns to that PC with an IsAvg result in rax and rsp advanced by eight; memory, vector registers and GPRs except rax, rsi, rsp unchanged
backends/arm/AvgArm/Proofs.lean	avgProgram_correct	with code loaded at the initial PC and no model error, executes four words, returns to x30 with an IsAvg result in x0, preserving memory, code and state fields except x0, x8, x9, PC

Each file lists its main results at the top.

Layout

core/
  spec/AvgSpec.lean           IsAvg: r = (a+b)/2 over ℕ, + exists/unique (trusted; core Lean only)
  algo/                      avgWide, avgFast, avgOverflow + proofs (core Lean only)
    AvgAlgo/Impl.lean         avgWide, avgFast, avgOverflow
    AvgAlgo/Proofs.lean       avgWide_isAvg, avgFast_eq_wide, avgFast_isAvg, avgFast_noOverflow
    AvgAlgo/Overflow.lean     avgOverflow_not_isAvg
    AvgAlgoTest/              `lake test`: #guard_msgs on bv_decide's counterexample

backends/
  aeneas/                    Rust source verification through Aeneas
    AvgAeneas/Impl/           Rust.avg, generated by Aeneas from impl/rust/ (never edit)
    AvgAeneas/Proofs.lean     rust_avg_correct: Rust.avg never panics, result satisfies IsAvg
  x86/                       x86-64 verification with Kraken
    AvgX86/Impl.lean          avgProgram: Kraken parses rustc's x86-64 AT&T assembly for `avg`
    AvgX86/Proofs.lean        avgProgram_correct: straightlineStep, stack return/pop, IsAvg, frame
  arm/                       AArch64 verification with LNSym
    AvgArm/Impl.lean          avgProgram: rustc's four raw AArch64 instruction words
    AvgArm/Proofs.lean        avgProgram_correct: fetch/decode/run, return to x30, IsAvg, frame
  riscv/                     RISC-V verification with riscv-zkvm
    AvgRiscv/Impl.lean        avgProgram: rustc's RV64IM output for `avg`
    AvgRiscv/Proofs.lean      avgProgram_spec: separation-logic triple (framed); avgProgram_correct: stepN form

tooling/
  common/                    checked export declarations, signatures and GNU/header rendering
  x86/                       reusable Kraken leaf-function emitter
  arm/                       reusable LNSym raw-word leaf-function emitter
  riscv/                     reusable RV64 encoder, decoder check and leaf-function emitter
examples/
  identity/                  independently proved one-argument identity function (x86)

impl/
  rust/                      the Rust crate
scripts/
  check-asm.py               checks rustc's disassembly == each ISA's avgProgram
  export.py                  project-independent Lake module runner; writes symbol.s and symbol.h
  check-avg.py               example-specific avg native smoke test
  check-identity.py          independent one-argument native smoke test

core/spec defines the shared contract; core/algo depends on it and proves the model-independent algorithms. Every proof package in backends/ depends on both: the Rust and all three machine-code implementations compute avgFast, so each finishes with avgFast_isAvg. impl/rust supplies the source for Aeneas extraction and compiler-output checks; scripts/check-asm.py binds that output to the ISA programs.

Separate Lake packages accommodate the models' Lean versions. Each package's lean-toolchain and lakefile.toml are authoritative for its toolchain and dependencies: spec, algo, Aeneas, x86 tooling, Arm tooling, RISC-V tooling. The ISA backends depend on their reusable tooling packages, which own the external model pins. Tooling depends on tooling/common, never on core/ or an example. Build packages sequentially locally: shared path-dependency artifacts are toolchain-specific.

Checking

(cd backends/aeneas && lake build)       # Aeneas side
(cd core/algo && lake build && lake test) # avgWide / avgFast / avgOverflow
(cd backends/riscv && lake build)        # RISC-V side
(cd backends/x86 && lake build)          # x86-64 side
(cd backends/arm && lake build)          # AArch64 side
scripts/check-asm.py                     # pinned rustc output == each avgProgram

The assembly check's Rust toolchain and targets are defined in scripts/check-asm.py. It also needs riscv64-unknown-elf-objdump, objdump and llvm-objdump; see the script's header for environment overrides.

Generic assembly export

The runner accepts any Lake package and exporter module. It has no built-in ISA list, repository layout, function name or C signature. Only Python and elan/Lake are required. The only output files are <symbol>.s and <symbol>.h, placed directly in --out-dir.

python3 scripts/export.py --package backends/x86 --export Export --out-dir dist/x86
python3 scripts/export.py --package backends/arm --export Export --out-dir dist/arm
python3 scripts/export.py --package backends/riscv --export Export --out-dir dist/riscv

# Separate package, different program, one argument, no Avg/core dependency:
python3 scripts/export.py --package examples/identity --export Export --out-dir dist/identity

The avg clients emit avg.s/avg.h with uint64_t avg(uint64_t, uint64_t). The identity client emits identity_u64.s/identity_u64.h with uint64_t identity_u64(uint64_t).

Using the tooling in another project

1. Depend on AssemblyX86, AssemblyArm or AssemblyRiscv via its tooling/<isa> Lake package and use its compatible Lean toolchain. Keep tooling/common available at the adapter's sibling path; the tooling tree does not require the avg examples.
2. Define a program and a contract of type AssemblyExport.Signature → Program → Prop. Include the intended input/result register mapping, preconditions, return behavior and preserved state, not just an arithmetic equality.
3. Construct AssemblyExport.Function Program contract with symbol, signature, program, and correct : contract signature program. These fields bind the proof to the exact exported program and declared signature. The existing backend Export modules and identity example are complete working declarations.
4. Register your exporter module as a Lake library module or executable root. Its root main : IO Unit calls AssemblyExport.run (AssemblyX86.emit declaration) (or the corresponding Arm/RISC-V emitter). run emits a JSON protocol; the Python runner builds the package/module, imports that built module, and writes its output pair. Module source directories need not match the runner's own filesystem layout.

Current signatures are explicitly limited to Signature.u64_0, .u64_1, .u64_2: an unsigned 64-bit result and zero, one or two unsigned 64-bit arguments. No pointers, aggregates, floating-point signatures, callbacks or varargs are supported.

Current emitters handle leaf instruction subsets, require a terminal return, and reject unsupported forms and earlier returns. There is no support for labels, branches, external calls, global data, relocations or general linking. This is reusable export tooling, not a general-purpose verified assembler.

A typed proof field is not a specification-quality check. A client could supply a vacuous contract. Review the contract and ABI assumptions; building arbitrary proofs does not itself establish FFI safety. The shipped examples bind their actual full correctness/return/frame statements to their signature and program.

Consuming the output

Output uses GNU syntax and Linux ELF directives, not Windows or macOS formats. x86 uses System V; Arm uses AAPCS64; RISC-V uses integer argument/result registers. Choose a compatible target toolchain and ABI (typically LP64D for RISC-V Linux). No Lean or Rust runtime is required by the emitted function.

cc -I dist/x86 caller.c dist/x86/avg.s -o caller
cc -shared -fPIC dist/x86/avg.s -o libavg.so

# Tests compile only temporary binaries:
python3 scripts/check-avg.py dist/x86
python3 scripts/check-identity.py dist/identity

Export proof boundary

• Arm: filter supported instruction classes with LNSym's decoder, then emit the client's instruction words as little-endian .byte directives.
• RISC-V: encode supported instructions, checking exact decoder agreement before emitting .byte directives. The avg-specific decode and serialization certificates remain in its backend. The executable decoder is not proved equivalent to Sail.
• x86: validate the supported leaf subset and emit Kraken's Intel-syntax printer output. That printer remains trusted; there is no binary-decoder proof.

ISA fidelity, Lean's executable evaluation/export path and the output runner remain trusted. Consumers must trust their assembler/linker and preserve the code and ABI. We do not certify final ELF objects/libraries or check post-link bytes. CI assembles the examples for their targets and executes the native x86 examples; these checks do not prove the surrounding FFI application. Rust comparison remains separate in check-asm.py.

ISA models and compiler-output binding

The x86 proof uses Kraken, pinned in tooling/x86/lakefile.toml. Its handwritten model targets sequential 64-bit software; it is not a formal equivalence to Intel's specification or another ISA model. Upstream provides a native differential-test harness: it assembles AT&T test programs with GNU binutils and compares Kraken's register/flag results with host execution. That is supporting evidence, not a proof of model fidelity; this repository's CI builds the avg proof, not that upstream hardware test suite.

Kraken parses assembly text, not binary bytes, and does not restrict every modeled instruction to an encodable form. scripts/check-asm.py therefore compares the literal AT&T assembly passed to parse in avgProgram against rustc's disassembly. It preserves instruction order, count and 64-bit operands, normalizing only whitespace, GNU mnemonic suffixes, immediate spelling and an implicit shift count of one. Unsupported forms fail closed. The disassembler, this comparison and Kraken's assembly parser remain trusted; there is no x86 binary-decoder proof or claim about instruction-byte lengths.

The x86 theorem covers the full six-instruction function, including ret, its loaded stack return address, the eight-byte stack pop and the memory/vector/GPR frame. Flags may change. Kraken does not model segment registers or segment bases, virtual memory, canonical-address checks, or most exceptions/faults; the theorem makes no segment-base, canonical-return-address or architectural-exception guarantee.

Arm's proof evaluates LNSym's fetch and decoder on raw words; unlike the RISC-V/x86 paths, it does not trust a mnemonic-to-instruction transcription or assembly-text binding. All paths still trust the ISA model's fidelity and the compiler-output binding script/tools. LNSym's revision is pinned in tooling/arm/lakefile.toml. Remaining trust boundaries and plans to shrink them: see TODO.md.

Reading

• Ethereum's TCB, Part 1: The client (George Kadianakis, ethresear.ch, 2026). It covers the trusted computing base (TCB) of a formally verified Ethereum client and compares five end-to-end verification approaches.