lungo documentation

Your first Rust crate built from Lean

Write Lean definitions and a proof, build them into a Rust crate, call them from Rust, and make the proof part of what the crate says about itself.

In this section

In this tutorial we will write a few Lean definitions about rectangles, prove a fact about them, and call them from Rust as ordinary Rust functions. Then we will register the proof as a claim about the functions, so the crate carries it and the build insists on it. Along the way we will meet the Lake project that holds the Lean code, the build.rs that turns it into Rust, and the generated module that the Rust code uses.

It takes about fifteen minutes, most of which is the first build.

Before we start

We need three things on the machine:

  • Rust 1.89 or later (cargo --version)
  • elan, Lean’s toolchain manager (elan --version)
  • git

Install the Lean toolchain we will use:

elan toolchain install leanprover/lean4:v4.34.1

Create the crate

Create a library crate called shapes:

cargo new --lib shapes
cd shapes

Write the Lean code

Our Lean code lives in its own Lake project, in a directory lean inside the crate:

mkdir lean
cd lean

A Lake project needs three files. First, the toolchain it uses. Create lean-toolchain:

leanprover/lean4:v4.34.1

Next, the Lake configuration. Create lakefile.toml:

name = "shapes"
version = "0.1.0"
defaultTargets = ["Shapes"]

[[lean_lib]]
name = "Shapes"

Now the Lean code itself. Create Shapes.lean:

namespace Shapes

structure Rect where
  width : Nat
  height : Nat

def area (r : Rect) : Nat := r.width * r.height

def scale (k : Nat) (r : Rect) : Rect :=
  { width := k * r.width, height := k * r.height }

theorem area_scale (k : Nat) (r : Rect) : area (scale k r) = k * k * area r := by
  simp only [area, scale]
  rw [Nat.mul_mul_mul_comm]

end Shapes

The theorem says that scaling a rectangle by k multiplies its area by k * k.

The third file is the manifest that records the project’s dependencies. Let Lake create it:

lake update

Lake answers:

info: shapes: no previous manifest, creating one from scratch

and a lake-manifest.json appears next to the other files. Our project has no dependencies, but lungo always builds from a committed manifest (see Architecture).

Go back to the crate:

cd ..

Connect Cargo to the Lean project

Add the two lungo crates from crates.io:

cargo add lungo
cargo add --build lungo-build

lungo is what the generated code uses at run time; lungo-build runs at build time.

Create build.rs in the crate directory, next to Cargo.toml:

fn main() -> lungo_build::Result<()> {
    lungo_build::compile_lean("lean")
}

This tells lungo where the Lake project is (lean). Everything else comes from the project itself: lungo compiles what lake build builds, the Shapes library named in defaultTargets, and gives the declarations of Shapes public Rust functions.

Finally, replace the contents of src/lib.rs with:

pub mod shapes {
    lungo::include_lean!("shapes");
}

The generated code is not in src; it is written into Cargo’s build directory, under the name of the Lake package (name = "shapes" in lakefile.toml), and this line includes it as the module shapes.

Build

cargo build

The first build takes a few minutes: lungo compiles its Lean worker for the toolchain once and keeps it for later builds. When it finishes, Cargo reports:

    Finished `dev` profile [unoptimized + debuginfo] target(s) in 1m 45s

Lean has checked the proof of area_scale, compiled the definitions, and lungo has generated Rust from them.

Call Lean from Rust

Create tests/rect.rs:

use lungo::Nat;
use shapes::shapes::{Rect, area, scale};

#[test]
fn area_of_a_rectangle() {
    let r = Rect { width: Nat::from(3u64), height: Nat::from(4u64) };
    assert_eq!(area(r), Nat::from(12u64));
}

#[test]
fn scaling_multiplies_the_area() {
    let r = Rect { width: Nat::from(3u64), height: Nat::from(4u64) };
    let big = scale(Nat::from(10u64), r);
    assert_eq!(big.width, Nat::from(30u64));
    assert_eq!(area(big), Nat::from(1200u64));
}

Notice that the Lean structure Rect is a Rust struct with the same fields, and that area and scale are plain functions. Lean’s Nat is unbounded, so it is the Rust type lungo::Nat rather than a fixed-width integer.

Run the tests:

cargo test

Among Cargo’s output:

test area_of_a_rectangle ... ok
test scaling_multiplies_the_area ... ok

test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

Both answers came from the compiled Lean definitions.

Change the Lean code

Add a definition at the end of lean/Shapes.lean, just before end Shapes:

def perimeter (r : Rect) : Nat := 2 * (r.width + r.height)

Build again:

cargo build

This time it takes seconds. Cargo noticed that a Lean file changed and regenerated the Rust; shapes::perimeter now exists. Add a test for it to tests/rect.rs if you like, and run cargo test again.

Make the proof a claim

So far the theorem area_scale was checked when the crate was built, and then forgotten: the crate says nothing about it. We will register it as a claim about area and scale, which the crate carries and the build insists on.

Claims are written with lungo’s Lean library, a Lake package of its own. Add it to lean/lakefile.toml, between the package settings and the library:

[[require]]
name = "lungo"
git = "https://github.com/machinefabric/lungo-rs"
rev = "v<version>"
subDir = "lean"

replacing <version> with the version of lungo in Cargo.toml (the library is released with the crates). Then let Lake fetch it and record it in the manifest:

cd lean
lake update
cd ..

In lean/Shapes.lean, import the library on the first line:

import Lungo

and mark the theorem as a claim, on the line above it:

@[lungo_claim "lungo.law" subject area scale]
theorem area_scale (k : Nat) (r : Rect) : area (scale k r) = k * k * area r := by

lungo.law is the relation: a property the theorem states about its subjects, area and scale. Lean checks that area_scale is a theorem and that its statement mentions both.

Now make the build insist on it. Replace build.rs with:

fn main() -> lungo_build::Result<()> {
    lungo_build::configure().require_claims("Shapes.area").compile_lean("lean")
}

require_claims makes the build fail if area ever has no proved claim. Build once more, and add tests/claims.rs to see what the crate says about itself:

use lungo::ClaimStatus;
use shapes::shapes::__meta;

#[test]
fn area_carries_its_claim() {
    let claim = __meta::assurance().claim("Shapes.area_scale").unwrap();
    assert_eq!(claim.status, ClaimStatus::Proved);
    assert_eq!(claim.subjects, ["Shapes.area", "Shapes.scale"]);
    let area = __meta::declaration("Shapes.area").unwrap();
    assert_eq!(area.assurance.claims, ["Shapes.area_scale"]);
}

Run cargo test: the claim is there, proved. The same information is in assurance.json in the build output, and in every package generated from the project for other languages.

Break a proof

Let’s see what happens when Lean disagrees. In lean/Shapes.lean, change the statement of area_scale to something false:

theorem area_scale (k : Nat) (r : Rect) : area (scale k r) = k * area r := by

and build:

cargo build

The build fails, and Cargo shows Lean’s own report:

  Error: error[LNG0201]: Lean elaboration failed
  ...
  error: Shapes.lean:15:75: unsolved goals
  k : Nat
  r : Rect
  ⊢ k * k * (r.width * r.height) = k * (r.width * r.height)

No Rust was generated from the broken project: the crate cannot be built while its Lean code does not check. LNG0201 is the code of this kind of error; every lungo error has one (see the error reference).

Put the statement back to k * k * area r. Now delete the @[lungo_claim …] line instead, and build again: the proof still checks, but the build fails anyway:

  Error: error[LNG0602]: the export Shapes.area has no proved claim (`require-claims` selects it with "Shapes.area"); state what it does with `@[lungo_claim]` on a theorem about it

Put the line back and run cargo test; everything passes again.

What we have done

We built a Rust crate whose logic is written and proved in Lean: a Lake project inside the crate, a short build.rs, and one include_lean!. The Rust code used Lean’s structure and functions directly, rebuilt itself when the Lean code changed, carried the proof as a claim about the functions it is about, and refused to build when a proof failed or the claim was gone.

From here: