lungo rende il codice Lean disponibile a programmi in Rust, C, Go, Python, Swift, Objective-C e TypeScript senza chiedere a Lean di essere altro che Lean. Questa pagina spiega come si compongono le parti e perché sono organizzate in questo modo.
Lean compila Lean
Il modo più ovvio per tradurre Lean in Rust sarebbe leggere il sorgente Lean, o i termini elaborati di Lean, e tradurli. lungo non fa né l’una né l’altra cosa. Il sorgente Lean è esteso da macro, notazioni ed elaboratori che solo Lean può eseguire, e i termini elaborati contengono ancora dimostrazioni, tipi, classi di tipi e definizioni per ricorsione ben fondata, il cui significato eseguibile lo decide il compilatore di Lean. Un traduttore che lavorasse a quel livello dovrebbe reimplementare una grossa parte di Lean, e prima o poi finirebbe per non essere d’accordo con esso.
lungo invece lascia che Lean faccia tutto fino al punto in cui il compilatore di Lean passa il suo output a un backend. Lake compila il progetto con esattamente la toolchain che fissa, così le estensioni sintattiche del progetto vengono eseguite, le sue dimostrazioni vengono controllate dal kernel di Lean e le sue definizioni vengono compilate dal compilatore di Lean, esattamente come per una build Lean nativa. lungo parte dal programma compilato: un piccolo linguaggio intermedio imperativo, del primo ordine, con conteggio esplicito dei riferimenti, che è ciò che un backend deve comunque implementare. Tutto ciò che sta sopra resta responsabilità di Lean.
Ecco anche perché un progetto Lean non ha bisogno di annotazioni né di modifiche per essere usato da Rust, e perché un Lean non valido o una dimostrazione falsa fanno fallire la build Rust: fanno fallire prima la build Lean. Ciò che un progetto può aggiungere, tramite la libreria Lean di lungo, dice qualcosa sul suo codice (che cosa è dimostrato di un export, che cosa l’host fornisce e che cosa si assume che faccia); non cambia mai ciò che il codice calcola.
La pipeline
build.rs / lungo ──► lake build ──► worker ──► Bridge IR + interface ──► verifier ──► generators
(Lean) (Lean) (Rust) (Rust)
- Lake elabora, controlla e compila i moduli radice. lungo legge soltanto ciò che Lake produce; non analizza mai il sorgente Lean.
- Il worker è un programma Lean, compilato con la toolchain del progetto, che carica l’ambiente compilato, seleziona il programma (il codice dei moduli radice, i loro inizializzatori, tutto ciò che chiamano) e lo codifica come Bridge IR insieme ai metadati: le dichiarazioni esportate e i loro tipi, i simboli extern, le posizioni nel sorgente e le informazioni di fiducia. Il suo passo di garanzia legge i claim, le specifiche, le facility e le assunzioni del progetto (vedi sotto). Gira come processo separato, così la build sopravvive a un suo crash o blocco.
- Il verificatore controlla la Bridge IR indipendentemente dal worker che l’ha prodotta.
- I generatori scrivono il programma e la sua interfaccia in ciascun linguaggio richiesto
(vedi sotto), e lungo scrive il documento di garanzia del
programma,
assurance.json, uguale in ogni output. - La pubblicazione sostituisce in modo atomico ogni directory di output e, in
build.rs, indica a Cargo quali file osservare.
La stessa libreria gira da build.rs e dal comando lungo, così
la riga di comando vede sempre ciò che vede la build.
Un programma, molti linguaggi
Generare codice per un linguaggio ha due parti, che lungo tiene separate:
- Esecuzione: il programma compilato, istruzione per istruzione, con il conteggio dei
riferimenti e il layout degli oggetti di Lean. Sono due: Rust (il livello del compilatore di
un crate Rust) e C (compilato dalla toolchain C del linguaggio dell’host: cgo, Xcode, una
build Python, clang per WebAssembly). Entrambi girano sullo stesso runtime, il port in Rust
del runtime di Lean fatto da lungo; il C lo chiama tramite la sua ABI C (
lungo.h), come il backend C di Lean chiamalibleanrt. - Proiezione: l’API delle dichiarazioni esportate nei termini del linguaggio stesso:
struct ed enum Rust, struct e interfacce sigillate Go, dataclass Python, struct e
indirect enumSwift, oggetti e unioni etichettate TypeScript, valori C con accessori tipizzati.
La descrizione da cui parte ogni proiezione è l’interfaccia del programma: le funzioni
esportate con i loro tipi, i tipi che usano, le facility implementate dall’host (ciascuna
un’interfaccia con un metodo per operazione), le facility asincrone le cui operazioni gli
export asincroni del programma chiedono di eseguire a un handler, e il punto di ingresso,
insieme al documento di garanzia del programma. Per lungo è ciò che il FileDescriptorSet è per protoc: un generatore è una
funzione da essa a dei file, che sia integrato o un plugin
(lungo-gen-<language>) che la riceve come JSON.
Rust mantiene la propria proiezione, che converte direttamente gli oggetti Lean. Ogni altro
linguaggio attraversa un unico confine: i punti di ingresso C del programma ricevono gli
argomenti e restituiscono i risultati in un’unica codifica binaria, il
formato di trasmissione, e la libreria di supporto di ciascun
linguaggio la codifica e la decodifica. Una chiamata è un solo attraversamento, per quanto
profondo sia il valore; i tipi ricorsivi, i numeri a precisione arbitraria e le funzioni
polimorfe sono gestiti dall’unico codec del runtime, guidato da una tabella dei tipi del
programma. I valori che un linguaggio non può tenere come dati (chiusure Lean, valori opachi,
IO.Error) attraversano il confine come handle, e le funzioni del linguaggio dell’host entrano
in Lean come callback.
Un export che restituisce un programma asincrono (Lungo.Async.Program) restituisce il suo
primo passo: il suo valore, oppure l’operazione che chiede all’host di eseguire e una
ripresa. L’host esegue l’operazione nei propri termini asincroni e riprende il programma con
la risposta, ottenendo il passo successivo. Il runtime conserva ogni programma in attesa sotto
la sua ripresa, che si può usare una sola volta: ripresa, o abbandonata quando il chiamante
viene annullato o l’handler fallisce. Ogni linguaggio ne fa le proprie funzioni async.
Un processo ha un solo runtime: lo condividono i pacchetti generati di un numero qualsiasi di programmi, ed è precompilato per ogni piattaforma e distribuito con ogni release, così nessuno che usi Go, Python, Swift o TypeScript compila Rust. Vedi la distribuzione del runtime.
La libreria Lean di lungo
Un progetto Lean che vuole dire più del suo codice richiede la libreria Lean di lungo
(lungo-rs/lean, il pacchetto Lake lungo, rilasciato con lungo con la stessa versione). Ha
due livelli. Il primo è Lean ordinario: strumenti per le specifiche (contratti, modelli di
comportamento, macchine a stati, tracce e protocolli, monitor di esecuzione) e programmi
asincroni, che un programma può eseguire. Il secondo è un insieme di attributi
(@[lungo_claim], @[lungo_spec], @[lungo_facility], @[lungo_operation],
@[lungo_assumption], @[lungo_role]) che vengono eseguiti durante la compilazione del
progetto.
Un attributo controlla ciò che riceve e scrive un record: una definizione accanto alla
dichiarazione che descrive, in una forma fissa, senza codice compilato. I record viaggiano con
l’ambiente compilato del modulo, così il worker li legge senza eseguire nulla. Il suo passo di
garanzia non si fida di essi: ricontrolla ciascuno rispetto all’ambiente (la prova di
un claim è un teorema, il suo enunciato nomina i suoi soggetti e ha la forma della sua
relazione, un’operazione è un extern, le risposte di una facility asincrona sono fissate dalle
sue operazioni), trova le assunzioni che l’enunciato di un claim prende come ipotesi,
legge gli assiomi da cui dipende la sua dimostrazione e calcola il fingerprint di ogni record. I
problemi sono errori con codici propri (LNG07xx), e un record scritto a mano è sottoposto
alle stesse regole.
I moduli degli attributi hanno bisogno dell’elaboratore di Lean, che nessun programma dovrebbe
portarsi dietro. Sono quindi barriere di collegamento: i moduli collegati al programma si
fermano davanti a essi, così un programma che importa la libreria porta con sé solo codice che
esegue, e aggiungere un claim non cambia nulla del codice compilato del programma. I
moduli indicati come moduli di garanzia vengono caricati solo per i loro record, tipicamente
leggi tenute fuori dal programma; nemmeno di essi viene collegato nulla. Un programma che usa
un valore che solo un modulo non collegato inizializzerebbe viene rifiutato
(LNG0710).
Ciò che il passo trova diventa il documento di garanzia del programma, assurance.json, scritto
in ogni output generato e incorporato nel pacchetto di ciascun linguaggio (vedi
garanzia formale e il documento di garanzia).
Due livelli di codice generato
Il livello del compilatore è meccanico e non è pensato per essere letto o chiamato: rispecchia
il programma compilato di Lean, compresi il conteggio dei riferimenti e gli aggiornamenti sul
posto, con il layout degli oggetti del runtime di Lean. La facciata è la parte pensata per le
persone: le structure Lean diventano struct Rust, Nat diventa un Nat illimitato, IO
diventa Result, e le conversioni avvengono al confine. Tenerli separati permette al livello
del compilatore di restare fedele a Lean mentre la facciata resta Rust idiomatico.
Il progetto Lake è la configurazione
Un progetto Lake dice già di che cosa è fatto: il nome del pacchetto e i target predefiniti,
le librerie e gli eseguibili che compila lake build. lungo li legge entrambi invece di
chiederli di nuovo. Per impostazione predefinita compila i moduli radice dei target
predefiniti, così come li risolve Lake stesso (quindi un lakefile.lean che calcola i suoi
target viene capito quanto un lakefile.toml), esporta ciò che quei moduli definiscono e dà
al modulo generato il nome del pacchetto. Un build.rs ha quindi bisogno solo della posizione
del progetto, e un crate include il risultato con il nome del pacchetto tramite
lungo::include_lean!, un po’ come un crate che genera codice gRPC con tonic compila i file
.proto e li include per pacchetto con include_proto!.
Ciò che Lean non può sapere lo configura l’applicazione: quali trait Rust derivano i tipi
generati, gli attributi per librerie come serde, e quali tipi Lean sono forniti da tipi Rust
già esistenti, come quelli generati da un’altra build di lungo. Queste impostazioni indicano
dichiarazioni Lean, e una che non indica nulla è un errore anziché un’operazione nulla e
silenziosa, così la configurazione non può allontanarsi dal codice Lean che modella.
Perché la toolchain è fissata esattamente
L’output del compilatore di Lean non è un formato stabile; cambia tra una release e l’altra. Il worker è quindi compilato per una sola toolchain, e il suo adattatore alle strutture dati del compilatore è validato per quella release. Un progetto che fissa una toolchain non supportata viene rifiutato prima che si compili qualcosa, invece di essere tradotto da un adattatore che potrebbe leggerlo male. Supportare una nuova release di Lean significa aggiungere un adattatore per essa.
Le build sono riproducibili e offline
Una build di Cargo non deve modificare il progetto, scaricare alcunché né dipendere da dove viene eseguita. lungo non installa mai toolchain né scarica dipendenze Lake durante una build (il manifest deve essere sotto commit e le dipendenze presenti), non scrive mai nel progetto Lean e scrive un output che non contiene percorsi specifici della macchina. Il suo output dipende solo dagli input registrati nella sua chiave di build, così un progetto invariato riusa l’output precedente, e due build dello stesso progetto producono gli stessi file.
Approfondimenti
- Il confine con il compilatore: che cosa esattamente lungo prende da Lean
- Il runtime: come il modello a oggetti di Lean è riprodotto in Rust
- Fiducia e verifica: di che cosa ci si deve fidare, e come viene controllato
- Garanzia formale: che cosa significano i claim che un pacchetto porta