How to call Rust functions from Lean

This guide shows how to let Lean code call a function of your Rust application: declare it in Lean as an operation of a facility, implement it in Rust, and map one to the other.

Declare the function in Lean

A facility is what the application provides, registered with @[lungo_facility]; its operations are opaque constants with the symbol the Rust side will implement, marked @[lungo_operation]. The attributes come from lungo’s Lean library, which the Lake project requires:

import Lungo

namespace Host

/-- The services the application provides. -/
@[lungo_facility "app.services"]
structure Services

/-- Looks a key up in the host's table. -/
@[extern "host_lookup", lungo_operation Services]
opaque hostLookup (key : @& String) : Option Nat

/-- Appends a line to the host's log. -/
@[extern "host_log", lungo_operation Services]
opaque hostLog (line : String) : IO Unit

end Host

The result type needs an Inhabited instance (Lean requires one for opaque). @& marks a parameter Lean lends rather than transfers; the Rust function receives an owned Rust value either way. What the program’s proofs need of the implementation, and cannot check, is stated as an assumption of the facility (see how to declare facilities and assumptions).

Use it from Lean like any other function:

def resolve (k : String) : IO Nat := do
  match Host.hostLookup k with
  | some v => Host.hostLog s!"{k} => {v}"; return v
  | none => throw (IO.userError s!"unknown key: {k}")

Implement it in Rust

Write a function whose parameters and result are the Rust forms of the Lean types (see Lean types in Rust). IO α becomes Result<A, lungo::IoError>:

pub mod host {
    use lungo::{IoError, Nat};

    pub fn lookup(key: String) -> Option<Nat> {
        match key.as_str() {
            "alpha" => Some(Nat::from(1u64)),
            _ => None,
        }
    }

    pub fn log(line: String) -> Result<(), IoError> {
        if line.is_empty() {
            return Err(IoError::user("empty log line"));
        }
        eprintln!("{line}");
        Ok(())
    }
}

An Err returned from an IO function is raised in Lean as that IO.Error. A function for an operation whose Lean type is pure must behave as a pure function, answering the same arguments the same way: Lean may compute such a call once and keep its value.

Map the symbols

In build.rs, map each symbol to the Rust path of its implementation, as seen from the crate root:

fn main() -> lungo_build::Result<()> {
    lungo_build::configure()
        .rust_extern("host_lookup", "crate::host::lookup")
        .rust_extern("host_log", "crate::host::log")
        .compile_lean("lean")
}

(with the lungo command, the same mappings are the [rust.rust-externs] table of lungo.toml).

Build. If an operation has no implementation, the build fails with LNG0401, naming the declaration and the Rust signature it needs; so does an extern that is no facility’s operation, with the hint to mark it @[lungo_operation]. Mapping a symbol that is not an operation’s fails with LNG0706, and a mapping for a symbol nothing uses with LNG0405.

Pass functions across the boundary

A Lean function parameter arrives in Rust as a LeanClosure, which Rust can call:

@[extern "host_transform", lungo_operation Services]
opaque hostTransform (f : Nat → Nat) (xs : List Nat) : List Nat

use lungo::{LeanClosure, List, Nat};

pub fn transform(f: LeanClosure<fn(Nat) -> Nat>, xs: List<Nat>) -> List<Nat> {
    xs.into_iter().map(|x| f.call(x)).collect()
}

In the other direction, Rust passes its own functions to generated Lean functions with LeanClosure::from_fn(|n: Nat| …).

In LeanOracle mode

The same mappings work in LeanOracle mode for externs declared @[extern "symbol"]: the generated adapter is exported under that C symbol. Other extern forms fail with LNG0407.

Operations the application answers asynchronously are an async facility instead, whose exports become async fns taking a handler (see how to call async host operations).

A complete example is compiler-tests/host in lungo-rs.