assurance.json

Ogni output che lungo scrive (il modulo Rust, il pacchetto di ogni linguaggio, l’output di ogni plugin) contiene il documento di garanzia del programma come assurance.json: che cosa il suo codice Lean afferma e dimostra di ciascun export, le assunzioni su cui quei claim poggiano, le facility di cui ogni export ha bisogno e ciò di cui ogni export si fida. Il documento viene costruito una volta per programma e scritto identico, byte per byte, in ogni output; ogni linguaggio legge lo stesso testo (vedi in ogni linguaggio). Garanzia formale spiega i concetti.

Il documento è JSON indentato (due spazi) che termina con un a capo. Un campo il cui valore manca è null, mai omesso. Ogni lettore di lungo — Rust, Go, Python, Swift e TypeScript — rifiuta un documento di un altro schema_version, uno con un campo che non conosce e uno a cui manca un campo (anche annullabile: deve esserci, come null), a qualunque profondità.

Livello più alto

Un programma che non usa nulla della libreria ha library: null e array di record vuoti; i suoi exports vengono comunque elencati, con la loro fiducia.

Provenienza

Record

Ogni record dei quattro tipi qui sotto contiene:

Specifiche

Le dichiarazioni @[lungo_spec]: name, kind (come lungo.contract o acme.cost-model), statement (il tipo della dichiarazione, come lo stampa Lean), definition (il suo corpo, come lo stampa Lean, quando la dichiarazione è una definizione; altrimenti null) e i campi comuni.

Facility

Le dichiarazioni @[lungo_facility].

Assunzioni

Le dichiarazioni @[lungo_assumption]: name, facility (il nome Lean della facility), statement (il tipo della dichiarazione, come lo stampa Lean), definition (il suo corpo quando è una definizione, altrimenti null) e i campi comuni. Un’assunzione definita come proposizione ha il tipo Prop, quindi è la sua definition a dire che cosa afferma: lungo assurance e lungo inspect stampano la definizione quando c’è, altrimenti il tipo.

Claim

I teoremi @[lungo_claim]. Il name di un claim è quello del suo teorema di prova.

Ruoli

Le dichiarazioni @[lungo_role]: name, role (come lungo.oracle) ed exported (se il programma esporta la dichiarazione). I ruoli non hanno fingerprint né sorgente.

Export

Uno per ogni dichiarazione esportata.

Ordine e determinismo

Il documento è funzione del progetto compilato e della toolchain: generarlo due volte, o da un’altra directory, dà gli stessi byte, e non contiene alcun percorso della macchina.

• specifications, facilities, assumptions, claims, roles ed exports sono ordinati per nome, confrontando i byte dei nomi (quindi Polyglot.Scaler viene prima di Polyglot.fetchInterface).
• Le operations di una facility extern sono ordinate per nome; quelle di una facility async sono nell’ordine dei costruttori del tipo di operazioni.
• Le assumptions di un claim, gli axioms della sua prova, le assumptions di una facility, e le assumptions e facilities di un export sono ordinati. I subjects e le specifications di un claim mantengono l’ordine dell’attributo; i claims di un export seguono l’ordine di claims.

Fingerprint

Un fingerprint identifica che cosa un record significa, così che due documenti possano essere controllati per verificare che concordano su un nome che condividono (lungo assurance --compose, LNG0708). Copre le espressioni Lean proprie del record e, transitivamente, le definizioni di ogni costante che usano dichiarata da un pacchetto del workspace Lake; le costanti della toolchain (Init, Std, Lean) sono coperte dalla versione di Lean, che ogni fingerprint nomina.

Il worker scrive un testo canonico di ogni espressione: i suoi sottotermini distinti una sola volta ciascuno, in ordine posticipato, senza nomi dei binder né metadati, con i parametri di universo numerati per posizione e le costanti per nome, dopo un’intestazione che nomina il tipo di record. Il testo canonico di un record copre:

Il worker descrive inoltre, una volta ciascuna, ogni costante del workspace che i record usano, direttamente o attraverso un’altra costante del genere: una definizione con il suo tipo e il suo valore; un teorema, una costante opaca o un assioma con il suo tipo (il contenuto di una prova o di un’implementazione opaca non cambia ciò che afferma); un tipo induttivo con il suo tipo e quelli dei suoi costruttori; ciascuna con le costanti del workspace che usa a sua volta. lungo calcola il digest di queste definizioni su quel grafo, così il digest di una definizione cambia quando cambia qualunque cosa usi. Le definizioni che si usano a vicenda (una componente fortemente connessa del grafo, come funzioni mutuamente ricorsive) hanno un digest calcolato insieme:

componente = SHA-256( "lungo-assurance-1 definitions\nlean <lean_version>\n"
                      + per ogni membro, per nome: "member <nome>\n<testo canonico>\n"
                        + per ogni costante che usa fuori dalla componente, per nome:
                          "uses <nome> <digest>\n" )
digest(membro) = SHA-256( componente + "\n" + <nome> )

Il fingerprint di un record è allora:

SHA-256( "lungo-assurance-1\nlean <lean_version>\n" + <testo canonico>
         + per ogni costante del workspace che il record usa direttamente, per nome:
           "\nuses <nome> <digest>" )

Ciascuno è scritto come 64 cifre esadecimali minuscole. Rinominare un binder o riformattare non cambia un fingerprint, e nemmeno il nome proprio del record o la sua posizione nel sorgente. Lo cambia modificare l’enunciato, la definizione, qualunque definizione del workspace che raggiunge — come un ausiliario a cui una specifica si riduce — o la versione di Lean. Un claim nomina i suoi soggetti come costanti, quindi il suo fingerprint cambia anche quando cambia la definizione di un soggetto.

In ogni linguaggio

Un plugin riceve il documento nella sua richiesta (assurance) e non deve scrivere assurance.json da sé: lungo lo scrive in ogni output (plugin).

lungo assurance riporta il documento di un progetto, filtrato e controllato rispetto alla politica, e lungo assurance --compose compone documenti (il comando lungo).