Documentazione di lungo

Garanzia formale

Che cosa un pacchetto generato può dire dei suoi export: claim dimostrati in Lean, le assunzioni su cui poggiano e come leggerli.

In questa sezione

Una dimostrazione Lean è utile a chi usa un pacchetto generato nella misura in cui costoro possono venirne a conoscenza. lungo porta in ogni pacchetto che genera un resoconto di ciò che il codice Lean del programma dimostra di ciascun export, di ciò che ogni dimostrazione assume dell’host e di ciò di cui lungo si fida per eseguire il codice: il documento di garanzia del pacchetto. Questa pagina descrive i concetti di cui il documento è fatto, come leggere un claim, e che cosa lungo controlla e che cosa no.

Le parti di un programma garantito

Un progetto Lean le dichiara con gli attributi della libreria Lean di lungo:

  • Implementazione. Una definizione eseguibile che il programma esporta, come Sorting.sort. È ciò che gira, in ogni linguaggio.
  • Specifica. Una dichiarazione che dice che cosa un’implementazione deve fare, senza esserlo: un contratto, una relazione, un modello, una macchina a stati, un protocollo (@[lungo_spec "lungo.contract"]). Una specifica che è un oggetto logico, come un contratto i cui campi sono proposizioni, dovrebbe essere noncomputable: non ha codice da eseguire, e lungo esporta solo le definizioni che Lean compila.
  • Claim. Un teorema, controllato dal kernel di Lean, registrato come prova che i suoi soggetti (implementazioni) stanno in una relazione con le sue specifiche: @[lungo_claim "lungo.satisfies" subject sort spec SortsAscending]. Un claim è esattamente il suo enunciato; la relazione dice di che tipo di enunciato si tratta e, per le relazioni proprie di lungo, la sua forma viene controllata.
  • Facility. Un gruppo di operazioni che l’host implementa, nel linguaggio dell’host: dichiarazioni @[extern] marcate @[lungo_operation C], oppure le operazioni di una facility asincrona. Lean ne vede solo i tipi.
  • Assunzione. Una proposizione su una facility che nessuna dimostrazione può stabilire, perché l’implementazione dell’host è fuori da Lean (@[lungo_assumption C]). Un claim che prende un’assunzione come ipotesi è condizionato a essa.
  • Oracolo. Un export usato per verificare codice scritto a mano: una definizione lenta, chiara e dimostrata (@[lungo_role "lungo.oracle"]) con cui si confronta un’altra implementazione.
  • Monitor. Un controllore eseguibile a cui l’host passa eventi durante l’esecuzione, dimostrato accettare esattamente le tracce che un protocollo ammette (lungo.monitors).

Leggere un claim

Lo stato di un claim è proved quando la sua prova è un teorema controllato dal kernel che non dipende da sorry, e incomplete quando dipende da sorry (la politica predefinita rifiuta quella build, vedi sotto). Un claim dimostrato dice che il suo enunciato è vero. Lo dice delle definizioni Lean, e lungo esegue quelle definizioni come Lean le ha compilate (vedi fiducia e verifica per ciò che questo aggiunge alla catena).

Un claim dimostrato con assunzioni vale su ogni host le cui facility le soddisfano, e per nessun altro host promette qualcosa. Si consideri l’esempio dell’orologio (examples/clock):

@[lungo_facility "timing.clock"]
structure Clock

@[extern "timing_ticks_per_second", lungo_operation Clock]
opaque ticksPerSecond (u : Unit) : Nat

@[lungo_assumption Clock]
def Ticks : Prop := 0 < ticksPerSecond ()

def toTicks (seconds : Nat) : Nat := seconds * ticksPerSecond ()
def toSeconds (ticks : Nat) : Nat := ticks / ticksPerSecond ()

@[lungo_claim "lungo.roundtrip" subject toTicks toSeconds]
theorem toSeconds_toTicks (h : Ticks) (seconds : Nat) : toSeconds (toTicks seconds) = seconds :=
  Nat.mul_div_cancel seconds h

Il pacchetto riporta il claim come proved, con l’assunzione Timing.Ticks, e così ogni export di cui parla. Un host il cui orologio batte mille volte al secondo riottiene i sette secondi che ha fornito. Un host il cui ticksPerSecond risponde 0 viola l’assunzione: il programma gira lo stesso, e lo stesso andata e ritorno di sette secondi dà 0. Il claim non è sbagliato: non ha mai parlato di quell’host. Il test C dell’esempio esegue entrambi gli host:

round trip of 7 s: 7 s; deadline in 5 s, after 2.5 s: 2 s left
round trip of 7 s: 0 s; deadline in 5 s, after 2.5 s: 0 s left

Installare un’implementazione di una facility non dimostra nulla su di essa. Un’assunzione è un obbligo per chi scrive il codice dell’host, enunciato dove può leggerlo: nella documentazione generata dell’installatore della facility e nel documento di garanzia di ogni export i cui claim poggiano su di essa.

lungo trova le assunzioni di un claim nel suo enunciato: sono le assunzioni registrate tra le costanti nei tipi dei suoi binder ∀ iniziali, così come sono scritti. Si enunci un’assunzione come ipotesi ((h : Ticks) → …); una nascosta dentro un’altra definizione non viene trovata.

La base fidata

Ciò su cui fa affidamento chi legge un claim dimostrato è la base fidata di ogni programma lungo (la toolchain di Lean, l’adattatore del worker, i backend, la distribuzione del runtime) e, per quel claim:

  • gli assiomi da cui dipende la sua prova, elencati nel documento (evidence_trust); un claim costruito su un assioma oltre a propext, Classical.choice e Quot.sound di Lean viene rifiutato quando la politica di fiducia nega gli assiomi;
  • le sue assunzioni, che l’host rende vere oppure no.

Che cosa controlla lungo

  • I record, due volte. Ogni attributo controlla la sua dichiarazione quando Lean la elabora. Il worker poi legge ogni record dall’ambiente compilato e lo controlla di nuovo, ricalcolando ogni fatto su cui un claim poggia: che la prova è un teorema, che il suo enunciato menziona ogni soggetto e ogni specifica, che ha la forma richiesta dalla sua relazione lungo.*, da quali assiomi dipende e quali assunzioni prende. Un record scritto a mano invece che dal suo attributo non guadagna nulla: viene letto e controllato allo stesso modo, e uno che non è nella forma canonica viene rifiutato (da LNG0701 a LNG0707).
  • La prova. Un claim che poggia su sorry viene rifiutato a meno che deny_sorry sia disattivato, e allora viene riportato incomplete; deny_axioms rifiuta prove che usano assiomi non standard (LNG0601).
  • La politica. [assurance] in lungo.toml, o le stesse impostazioni del Builder, possono richiedere che ogni export selezionato porti un claim dimostrato (LNG0602) e vietare assunzioni o intere facility (LNG0603).
  • La composizione. Ogni record porta il pacchetto Lake che lo dichiara e un fingerprint del suo significato (i suoi termini Lean e ogni definizione dei pacchetti del workspace che raggiunge), così lungo assurance --compose può controllare che pacchetti generati separatamente intendano la stessa cosa con un nome che condividono (LNG0708).
  • Le facility durante l’esecuzione. Un programma si rifiuta di girare finché l’host non ha installato ogni facility di cui ha bisogno, e nomina quella mancante.

Che cosa lungo non controlla

  • L’implementazione di una facility da parte dell’host. Che soddisfi le assunzioni della facility è responsabilità dell’host; lungo riporta solo quali claim ne dipendono.
  • Che un’operazione pura sia pura. Un’operazione il cui tipo Lean non è IO è una funzione per Lean, e Lean può valutare una chiamata con argomenti fissi una sola volta e conservarne il valore: un orologio il cui ticksPerSecond () cambiasse durante l’esecuzione non verrebbe visto cambiare. Un’operazione che può rispondere in modo diverso deve avere un tipo IO (o EIO).
  • Che un enunciato significhi ciò che l’autore intendeva. Un claim dimostra il suo enunciato; la specifica vale quanto ciò che dice. Si legga l’enunciato: il documento lo riporta.
  • Relazioni di altri spazi dei nomi. Una relazione come acme.cost-bound è propria di un pacchetto; lungo ne controlla la grafia e la riporta, senza attribuirle una forma.

Annotazioni e programma generato

Claim, specifiche, ruoli e assunzioni non cambiano il programma: aggiungono record, non codice. Due cose possono comunque differire quando un progetto comincia a importare Lungo:

  • Il compilatore di Lean riusa le specializzazioni compilate in qualunque modulo l’ambiente contenga, e importare Lungo porta con sé le parti di Lean che servono ai suoi attributi. Una specializzazione come List.toString a un certo tipo può allora provenire da un modulo di Lean invece che dal progetto. lungo genera il codice ovunque si trovi, quindi il programma si comporta allo stesso modo; cambia solo dove il codice è collocato. Un valore che un tale modulo calcola quando viene inizializzato non può essere usato, poiché i moduli degli attributi non vengono mai collegati (LNG0710).
  • Una dichiarazione a cui si dà @[lungo_facility] o @[lungo_operation] cambia invece il programma: trasforma un extern in un’operazione che l’host deve fornire.