Documentazione di lungo

Il tuo primo crate Rust costruito da Lean

Scrivi definizioni Lean e una dimostrazione, compilale in un crate Rust, chiamale da Rust e fai della dimostrazione parte di ciò che il crate dice di sé.

In questa sezione

In questo tutorial scriveremo alcune definizioni Lean sui rettangoli, dimostreremo un fatto che le riguarda e le chiameremo da Rust come normali funzioni Rust. Poi registreremo la dimostrazione come claim sulle funzioni, così che il crate la porti con sé e la build la pretenda. Lungo la strada incontreremo il progetto Lake che contiene il codice Lean, il build.rs che lo trasforma in Rust e il modulo generato usato dal codice Rust.

Richiede circa quindici minuti, la maggior parte dei quali per la prima build.

Prima di iniziare

Sulla macchina servono tre cose:

  • Rust 1.89 o successivo (cargo --version)
  • elan, il gestore delle toolchain di Lean (elan --version)
  • git

Installa la toolchain Lean che useremo:

elan toolchain install leanprover/lean4:v4.34.1

Crea il crate

Crea un crate libreria chiamato shapes:

cargo new --lib shapes
cd shapes

Scrivi il codice Lean

Il nostro codice Lean vive in un progetto Lake a sé, in una directory lean dentro il crate:

mkdir lean
cd lean

Un progetto Lake ha bisogno di tre file. Il primo indica la toolchain che usa. Crea lean-toolchain:

leanprover/lean4:v4.34.1

Poi la configurazione di Lake. Crea lakefile.toml:

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

[[lean_lib]]
name = "Shapes"

Ora il codice Lean vero e proprio. Crea 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

Il teorema afferma che scalare un rettangolo di un fattore k ne moltiplica l’area per k * k.

Il terzo file è il manifest che registra le dipendenze del progetto. Lascia che sia Lake a crearlo:

lake update

Lake risponde:

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

e accanto agli altri file compare lake-manifest.json. Il nostro progetto non ha dipendenze, ma lungo compila sempre a partire da un manifest di cui è stato fatto il commit (vedi Architettura).

Torna al crate:

cd ..

Collega Cargo al progetto Lean

Aggiungi i due crate di lungo da crates.io:

cargo add lungo
cargo add --build lungo-build

lungo è ciò che il codice generato usa in esecuzione; lungo-build viene eseguito durante la build.

Crea build.rs nella directory del crate, accanto a Cargo.toml:

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

Questo indica a lungo dove si trova il progetto Lake (lean). Tutto il resto viene dal progetto stesso: lungo compila ciò che compila lake build, cioè la libreria Shapes indicata in defaultTargets, e rende le dichiarazioni di Shapes funzioni Rust pubbliche.

Infine, sostituisci il contenuto di src/lib.rs con:

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

Il codice generato non si trova in src: viene scritto nella directory di build di Cargo, con il nome del pacchetto Lake (name = "shapes" in lakefile.toml), e questa riga lo include come modulo shapes.

Compila

cargo build

La prima build richiede qualche minuto: lungo compila una volta il suo worker Lean per la toolchain e lo conserva per le build successive. Al termine, Cargo riporta:

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

Lean ha controllato la dimostrazione di area_scale, ha compilato le definizioni e lungo ne ha generato il codice Rust.

Chiama Lean da Rust

Crea 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));
}

Nota che la structure Lean Rect è una struct Rust con gli stessi campi, e che area e scale sono semplici funzioni. Il Nat di Lean è illimitato, quindi è il tipo Rust lungo::Nat e non un intero a larghezza fissa.

Esegui i test:

cargo test

Tra l’output di Cargo:

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

Entrambe le risposte provengono dalle definizioni Lean compilate.

Modifica il codice Lean

Aggiungi una definizione alla fine di lean/Shapes.lean, subito prima di end Shapes:

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

Compila di nuovo:

cargo build

Questa volta bastano pochi secondi. Cargo si è accorto che un file Lean è cambiato e ha rigenerato il Rust; ora esiste shapes::perimeter. Se vuoi, aggiungi un test in tests/rect.rs ed esegui di nuovo cargo test.

Fai della dimostrazione un claim

Finora il teorema area_scale è stato controllato durante la build del crate, e poi dimenticato: il crate non ne dice nulla. Lo registreremo come claim su area e scale, che il crate porta con sé e che la build pretende.

I claim si scrivono con la libreria Lean di lungo, un pacchetto Lake a sé. Aggiungila a lean/lakefile.toml, tra le impostazioni del pacchetto e la libreria:

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

sostituendo <version> con la versione di lungo in Cargo.toml (la libreria viene rilasciata insieme ai crate). Poi lascia che Lake la scarichi e la registri nel manifest:

cd lean
lake update
cd ..

In lean/Shapes.lean, importa la libreria sulla prima riga:

import Lungo

e marca il teorema come claim, sulla riga che lo precede:

@[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 è la relazione: una proprietà che il teorema enuncia sui suoi soggetti, area e scale. Lean controlla che area_scale sia un teorema e che il suo enunciato li nomini entrambi.

Ora fai in modo che la build lo pretenda. Sostituisci build.rs con:

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

require_claims fa fallire la build se area non ha più un claim dimostrato. Compila ancora una volta, e aggiungi tests/claims.rs per vedere che cosa il crate dice di sé:

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"]);
}

Esegui cargo test: il claim c’è, dimostrato. Le stesse informazioni sono in assurance.json nell’output della build, e in ogni pacchetto generato dal progetto per altri linguaggi.

Rompi una dimostrazione

Vediamo che cosa succede quando Lean non è d’accordo. In lean/Shapes.lean, cambia l’enunciato di area_scale in qualcosa di falso:

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

e compila:

cargo build

La build fallisce e Cargo mostra il rapporto di Lean:

  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)

Dal progetto rotto non è stato generato alcun Rust: il crate non si può compilare finché il suo codice Lean non supera il controllo. LNG0201 è il codice di questo tipo di errore; ogni errore di lungo ne ha uno (vedi il riferimento degli errori).

Riporta l’enunciato a k * k * area r. Ora cancella invece la riga @[lungo_claim …] e compila di nuovo: la dimostrazione supera ancora il controllo, ma la build fallisce lo stesso:

  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

Rimetti la riga ed esegui cargo test: tutto torna a passare.

Che cosa abbiamo fatto

Abbiamo costruito un crate Rust la cui logica è scritta e dimostrata in Lean: un progetto Lake dentro il crate, un build.rs breve e un include_lean!. Il codice Rust ha usato direttamente la structure e le funzioni di Lean, si è ricompilato quando il codice Lean è cambiato, ha portato la dimostrazione come claim sulle funzioni che riguarda, e si è rifiutato di compilare quando una dimostrazione è fallita o il claim è sparito.

Da qui: