Fiducia e verifica

Una dimostrazione Lean afferma qualcosa su una definizione Lean. Eseguire quella definizione come Rust aggiunge anelli alla catena tra la dimostrazione e il programma in esecuzione. Questa pagina descrive quegli anelli, come viene controllato ciascuno, e che cosa la build isola e che cosa no.

Che cosa copre una dimostrazione

Il kernel di Lean controlla le dimostrazioni durante lake build, prima che lungo veda alcunché. lungo non aggiunge alcun ragionamento proprio: un teorema su Shapes.area vale per l’area Rust esattamente nella misura in cui il codice Rust calcola ciò che calcola la definizione Lean. La domanda è quindi quanto ci si debba fidare per credere che lo faccia.

Un teorema diventa parte di ciò che un pacchetto dice di sé quando viene registrato come claim su un export (@[lungo_claim]): lungo controlla che sia un teorema su quell’export, e ne porta l’enunciato, lo stato e ciò su cui si appoggia in ogni pacchetto generato. Che cosa significano i claim, e come si legano a specifiche, assunzioni e alla base fidata qui sotto, è l’argomento della garanzia formale.

La base fidata

• La toolchain di Lean. Il suo elaboratore, il kernel e il compilatore, così come li esegue lake build. Chiunque esegua codice Lean in modo nativo si fida degli stessi componenti.
• L’adattatore del worker. Legge l’output e i metadati del compilatore e li codifica; non trasforma alcun codice. Il suo passo di garanzia legge i record che scrive la libreria Lean di lungo e li ricontrolla rispetto all’ambiente: che la prova di un claim sia un teorema, che il suo enunciato nomini i suoi soggetti e le sue specifiche e abbia la forma che la sua relazione richiede, da quali assiomi dipende la dimostrazione. Non decide nulla che una dimostrazione potrebbe decidere; riporta ciò che il kernel di Lean ha accettato.
• I backend. La traduzione di ogni istruzione della Bridge IR in Rust e in C, le conversioni della facciata Rust, la codifica dei valori da parte dei binding dei linguaggi e le primitive del runtime.
• La distribuzione del runtime precompilato, per i linguaggi diversi da Rust (vedi la distribuzione del runtime).
• Le facility dell’host. Le operazioni che l’applicazione implementa (in Rust, Go, Python, Swift, TypeScript o C) stanno fuori da ogni dimostrazione. Ciò di cui un claim ha bisogno da esse lo dichiara come assunzione, e il claim vale solo su un host che rende vera l’assunzione.

Il primo è responsabilità di Lean, l’ultimo dell’applicazione. Gli altri sono di lungo, e ciascuno viene controllato da un lato diverso.

Come viene controllato il backend

Verifica indipendente dell’input. Prima di generare codice, lungo controlla la Bridge IR per conto suo: variabili e punti di join nel loro ambito, chiamate con il numero e la rappresentazione corretti di argomenti, letterali nell’intervallo, ogni dichiarazione chiamata presente. Un difetto nel worker emerge come errore di verifica invece che come Rust sbagliato.

Confronto con il backend di Lean. I programmi di conformità vengono compilati tre volte, come Rust, come C sulla libreria C del runtime e dal backend nativo di Lean, e il loro output, l’output di errore e i codici di uscita devono coincidere byte per byte. Il corpus copre ogni istruzione che la toolchain emette. Separatamente, una libreria di funzioni esportate gira su entrambi i backend nello stesso processo, confrontati chiamata per chiamata su input generati: numeri grandi, testo Unicode, float compresi NaN e zero negativo, alberi, chiusure in entrambe le direzioni, errori IO.

Legami con la toolchain. Ogni simbolo extern della libreria standard è contabilizzato con la rappresentazione dichiarata da Lean, e l’intera libreria standard eseguibile, circa cinquantamila dichiarazioni compilate, supera la verifica e genera Rust che supera il controllo dei tipi.

Un programma in ogni linguaggio. Un programma che usa ogni genere di valore che attraversa il confine (numeri grandi, structure, tipi ricorsivi e polimorfi, opzioni, array, coppie, Except, chiusure in entrambe le direzioni, valori opachi, errori IO ed EIO, facility dell’host, programmi asincroni a cui risponde un handler, main, chiamate concorrenti) viene generato per C, Go, Python, Swift, Objective-C e TypeScript, e i test di ciascun linguaggio fanno le stesse asserzioni su di esso, anche sul documento di garanzia che ogni pacchetto porta. Ogni libreria di supporto, e il runtime stesso, viene inoltre verificata sui vettori di test condivisi del formato di trasmissione, comprese le codifiche che ogni codec deve rifiutare.

Tipi condivisi tra pacchetti. Un programma costruito sul modello di un altro programma legge i valori di quel programma secondo il layout per cui è stato compilato. Ogni tipo generato porta un digest del suo layout (i suoi costruttori, i loro campi e ogni tipo che raggiungono, con la versione di Lean), e un pacchetto che usa il tipo di un altro pacchetto lo controlla prima di essere eseguito (vedi tipi extern), così due pacchetti generati da definizioni diverse di un tipo non possono essere usati insieme.

Niente di tutto ciò è una dimostrazione del backend. È il livello di garanzia di un compilatore verificato rispetto a un’implementazione di riferimento, e il riferimento è quello di Lean stesso.

Metadati di fiducia

Una parte del codice Lean sta al di fuori di ciò che le dimostrazioni garantiscono: le definizioni che usano sorry, gli assiomi oltre ai tre standard di Lean, il codice unsafe, le definizioni partial e gli extern nativi, tra cui le operazioni delle facility dell’host. lungo calcola, per ogni export, da quali di questi dipende il suo codice eseguibile, e per ogni claim da quali assiomi dipende la sua dimostrazione e se usa sorry; registra entrambe le cose nel documento di garanzia di ogni pacchetto, e può rifiutarsi di compilare quando un export o la dimostrazione di un claim dipende da sorry o da assiomi aggiuntivi, o un export da codice unsafe (vedi come imporre politiche di fiducia e di garanzia).

Un claim la cui dimostrazione usa sorry viene riportato come incompleto, mai come dimostrato. Un claim dimostrato che si appoggia su un’assunzione su una facility viene riportato con quell’assunzione, e ogni export di cui parla la elenca: il claim dice che cosa vale su un host che rispetta l’assunzione, e nulla di un host che non la rispetta. Così le ipotesi dietro una funzione sono visibili dove viene usata, in ogni linguaggio.

Che cosa isola la build

Compilare un progetto Lean ne esegue il codice: macro, elaboratori e tattiche girano durante lake build, e il worker carica il codice compilato del progetto. Aggiungere una dipendenza Lean equivale quindi ad aggiungere una dipendenza di build di Cargo o una macro procedurale: gira con i tuoi permessi.

Il worker gira come processo separato sotto supervisione. Un crash, un blocco o una risposta malformata sono un errore di build, mai un fallimento di Cargo stesso; un timeout termina ogni processo avviato dal worker. Limiti facoltativi ne vincolano il tempo di processore e la memoria dove il sistema operativo può applicarli, e una modalità ermetica nasconde le tue variabili d’ambiente. Questi contengono i fallimenti e le build fuori controllo. Non sono una sandbox: l’accesso al file system e alla rete non è limitato, e una dipendenza malevola non viene contenuta.