Formato di trasmissione — Documentazione di lungo

Ogni binding di linguaggio tranne Rust chiama un programma Lean tramite i suoi punti di ingresso C, passando gli argomenti e ricevendo i risultati in un’unica codifica binaria. Questa pagina la specifica. Il runtime implementa l’unico codec che la converte da e verso oggetti Lean; la libreria di supporto di ciascun linguaggio implementa la codifica dei propri valori, ed è verificata sui vettori condivisi di compiler-tests/wire/vectors.json in lungo-rs (vedi sotto).

Tutto è little-endian. Una lunghezza o un conteggio è un u32. Ogni lettura è controllata nei limiti; i dati troncati, con byte avanzati o con un valore non valido vengono rifiutati, mai letti in modo errato.

Espressioni di tipo

Un’espressione di tipo è un byte di etichetta seguito dalle sue parti:

Etichetta	Tipo	Parti
0	`Nat`
1	`Int`
2	`Bool`
3–7	`UInt8`, `UInt16`, `UInt32`, `UInt64`, `USize`
8–12	`Int8`, `Int16`, `Int32`, `Int64`, `ISize`
13, 14	`Float`, `Float32`
15	`Char`
16	`String`
17	`Unit`
18	`ByteArray`
19	`FloatArray`
20	`Option α`	α
21	`List α`	α
22	`Array α`	α
23	`α × β`	α, β
24	`Except ε α`	ε, α
25	`α₁ → … → αₙ → β`	`u32` n (da 1 a 15), α₁ … αₙ, β
26	parametro di tipo	`u32` indice
27	tipo induttivo	`u32` indice nella tabella dei tipi, `u32` conteggio, gli argomenti
28	valore opaco

Un parametro di tipo si riferisce a un parametro del tipo induttivo che lo racchiude (nella tabella dei tipi) o della funzione (in una firma). I valori sono sempre codificati con tipi senza parametri: una chiamata di una funzione polimorfa passa per primi i suoi argomenti di tipo (vedi chiamate).

Valori

Tipo	Codifica
`Nat`	il modulo: una lunghezza e i suoi byte, dal meno significativo, senza un byte zero più significativo (quindi zero è il modulo vuoto).
`Int`	un byte di segno (0 non negativo, 1 negativo), poi il modulo. Lo zero negativo non è valido.
`Bool`	un byte, 0 oppure 1.
`UInt8` … `UInt64`, `Int8` … `Int64`	il valore in 1, 2, 4 o 8 byte (complemento a due per i tipi con segno).
`USize`, `ISize`	8 byte. Un valore che l’`USize` della piattaforma non può contenere viene rifiutato dal runtime.
`Float`, `Float32`	i bit IEEE 754 in 8 o 4 byte; ogni configurazione di bit, compresi i payload dei NaN, viene preservata.
`Char`	un valore scalare Unicode `u32` (non un surrogato, al massimo 0x10FFFF).
`String`	una lunghezza e altrettanti byte di UTF-8 valido (che può contenere NUL).
`Unit`	niente.
`ByteArray`	una lunghezza e i byte.
`FloatArray`	un conteggio e altrettanti float da 8 byte.
`Option α`	0 (`none`), oppure 1 e un valore di α (`some`).
`List α`, `Array α`	un conteggio e i valori.
`α × β`	un valore di α, poi uno di β.
`Except ε α`	0 e un valore di ε (`error`), oppure 1 e un valore di α (`ok`).
funzione	un byte di genere e un `u64`: 0 e un handle (una chiusura Lean), oppure 1 e l’identificatore di una funzione dell’host.
valore opaco	un handle `u64`.
tipo induttivo	un indice di costruttore `u32` (nell’ordine di dichiarazione) e i campi del costruttore in ordine, ciascuno al suo tipo con gli argomenti del tipo sostituiti; una structure che la tabella marca come banale (un solo costruttore la cui rappresentazione in esecuzione è un solo campo) è codificata come quel solo campo; un tipo che la tabella marca come opaco è un handle `u64`, come un valore opaco.

Tabelle dei tipi

Un programma descrive i suoi tipi induttivi in una tabella dei tipi, che il codice generato incorpora e che ogni generatore riceve (come JSON in una richiesta di plugin). Nella forma binaria è il valore magico LNGT, una versione u32 (2), un conteggio e, per ogni tipo: il suo nome (una lunghezza e UTF-8), se è opaco (un byte, 0 o 1), il suo numero di parametri, la sua rappresentazione in esecuzione, se è banale (e quale costruttore e campo), e i suoi costruttori: nome, etichetta in esecuzione, dimensioni dell’oggetto, degli usize e degli scalari, e i campi (nome, dove è memorizzato il campo e la sua espressione di tipo). Il runtime valida una tabella prima di usarla; le tabelle generate sono valide per costruzione.

Un tipo opaco è un tipo con nome i cui valori attraversano il confine solo come handle, come un valore opaco (handle u64): non ha parametri né costruttori, e ha una rappresentazione a oggetto. Dargli un nome fornisce ai binding un tipo proprio per esso.

Firme

La firma di una funzione che attraversa il confine è il suo numero di parametri di tipo, un conteggio e le espressioni di tipo dei parametri, e ciò che restituisce: 0 e un tipo (un valore), 1 e un tipo (IO α), 2 e due tipi (EIO ε α: l’errore, poi il valore), oppure 3 per un programma asincrono (Lungo.Async.Program op α): un indice u32 del tipo di operazioni op nella tabella dei tipi, un conteggio n e n espressioni di tipo (il tipo con cui riceve risposta ciascuno dei costruttori di op, in ordine), e il tipo del valore del programma α. Il tipo di operazioni è un tipo induttivo con nome della tabella, né opaco né con parametri, n è il numero dei suoi costruttori, e i tipi delle risposte non hanno parametri di tipo; α può averne.

Chiamate

Un punto di ingresso generato int32_t <prefix>call_<function>(const uint8_t *input, size_t len, lungo_buffer *out) riceve come input: un conteggio di argomenti di tipo e le loro espressioni di tipo (una per parametro di tipo, senza parametri a loro volta), poi gli argomenti. Restituisce 0 e memorizza il risultato in out, oppure 1 e memorizza un messaggio UTF-8 che spiega perché l’input è stato rifiutato. Il risultato è:

per un valore: il valore;
per IO α: 0 e il valore, oppure 1 e un IO.Error: un handle e il suo messaggio (una lunghezza e UTF-8, come lo rende IO.Error.toString);
per EIO ε α: 0 e il valore, oppure 1 e il valore di errore;
per un programma asincrono: il suo primo passo.

Le funzioni BaseIO α restituiscono direttamente il loro valore. Una chiusura si chiama allo stesso modo con lungo_closure_call (i suoi argomenti di tipo sono sempre nessuno).

Handle

Un handle (un u64 non nullo) indica un oggetto Lean che il runtime tiene per l’host: un valore opaco, una chiusura Lean, un IO.Error. Gli handle nei dati che il runtime produce sono nuovi e posseduti da chi li riceve, che rilascia ciascuno una sola volta con lungo_handle_release (una libreria di supporto lo fa quando il valore viene raccolto o chiuso). Nei dati che un host invia:

gli argomenti di una chiamata prestano i loro handle: l’host li conserva;
il risultato di una funzione dell’host cede i suoi handle al runtime, che li rilascia: un host che restituisce un valore ricevuto passa un clone (lungo_handle_clone).

Un IO.Error sollevato da una funzione dell’host è un handle e un messaggio: un handle ricevuto da Lean (un clone), oppure 0 e il messaggio, che diventa IO.userError message.

Funzioni dell’host

L’host (l’unica libreria di supporto del processo) installa tre punti di ingresso con lungo_set_host (su WebAssembly sono gli import del modulo lungo.dispatch, lungo.retain e lungo.release):

dispatch(callback, input, len, out) esegue la funzione dell’host callback sui suoi argomenti codificati e memorizza il risultato codificato in out (allocato con lungo_buffer_alloc), restituendo 0, oppure memorizza un messaggio UTF-8 e restituisce un valore diverso da zero se è fallita;
retain(callback) e release(callback) contano i riferimenti del runtime a essa.

Una funzione dell’host negli argomenti di una chiamata viene trattenuta dal runtime finché una chiusura Lean la contiene (l’host la mantiene in vita durante la chiamata); una nel risultato di una funzione dell’host arriva con un riferimento a cui l’host rinuncia. Il risultato di una funzione dell’host che implementa un extern IO è 0 e il valore, oppure 1 e un IO.Error; di un extern EIO ε 0 e il valore, oppure 1 e l’errore. Un fallimento di una funzione dell’host dove Lean non può osservarlo (una funzione pura) termina il programma con il suo messaggio.

Programmi asincroni

Una funzione che restituisce Lungo.Async.Program op α restituisce il passo del suo programma:

0 e un valore di α: il programma ha terminato;
1, un valore di op (l’operazione che chiede all’host di compiere, codificata come valore del tipo induttivo op) e una ripresa (resumption) u64: il programma attende la risposta dell’host.

L’host compie l’operazione e riprende il programma con lungo_async_resume(resumption, input, len, out): input è la risposta, un valore del tipo che la firma assegna al costruttore dell’operazione, i cui handle il runtime prende come prende quelli del risultato di una funzione dell’host. Il runtime memorizza il passo successivo del programma in out e restituisce 0; oppure restituisce 1 (la risposta non è di quel tipo) o 3 (LUNGO_STALE: la ripresa è già stata ripresa o annullata) con un messaggio UTF-8. lungo_async_cancel(resumption) rinuncia al programma, rilasciandolo (0, oppure 3 se scaduta); lungo_async_outstanding() conta i programmi in attesa.

Una ripresa si usa esattamente una volta. Riprenderla la consuma qualunque sia l’esito, così una risposta del tipo sbagliato termina il programma invece di lasciarlo proseguire, e la continuazione non viene mai eseguita due volte; una ripresa usata di nuovo, o mai emessa, è scaduta, il che viene riportato, mai indefinito. Le riprese non vengono mai riutilizzate, e si può rispondere su qualsiasi thread.

Vettori di test

compiler-tests/wire/vectors.json in lungo-rs contiene codifiche valide (espressione di tipo, valore, byte) e codifiche non valide (espressione di tipo, byte) che ogni codec deve rifiutare. I valori sono JSON: i numeri che possono superare i 53 bit (Nat, Int, interi a 64 bit) sono stringhe decimali; i float sono {"bits": "<hex>"}; Unit è null; gli array di byte {"bytes": "<hex>"}; le opzioni {"none": null} o {"some": v}; Except {"error": e} o {"ok": v}; le coppie array di due elementi; le funzioni {"lean": "<handle>"} o {"host": "<id>"}; i valori opachi {"handle": "<handle>"}. I test del runtime rigenerano il file (LUNGO_BLESS=1) e lo verificano con il codec del runtime; le librerie di supporto di Go, Python, Swift e TypeScript si verificano su di esso.