La libreria Lean

La libreria Lean di lungo è il pacchetto Lake lungo, rilasciato con lungo alla versione di lungo (i suoi sorgenti sono lean/ in lungo-rs). Un progetto la importa per dichiarare ciò che lungo porta nei pacchetti che genera (garanzia formale): gli attributi scrivono record che il worker legge, e i moduli di supporto contengono le definizioni con cui di solito si enunciano i claim.

Richiedere la libreria

Da un checkout o da una copia inclusa nel progetto, per percorso:

# lakefile.toml
[[require]]
name = "lungo"
path = "../lungo-rs/lean"

Dal repository lungo-rs, al tag del lungo con cui si genera:

[[require]]
name = "lungo"
git = "https://github.com/machinefabric/lungo-rs"
rev = "v1.88.0"
subDir = "lean"

Si esegua lake update una volta e si faccia il commit di lake-manifest.json: le build di lungo non scaricano mai dipendenze. La libreria fissa la stessa toolchain di Lean di lungo (leanprover/lean4:v4.34.1).

Poi import Lungo. Importa due parti:

• Lungo.Core: Lungo.Registry e i moduli di supporto qui sotto. Importano solo Init e non dichiarano inizializzatori, quindi un programma contiene esattamente il loro codice che chiama.
• Lungo.Attr: gli attributi. Hanno bisogno dell’elaboratore di Lean e girano solo mentre il progetto viene compilato; lungo non li collega mai a un programma, né collega le parti di Lean che importano.

I record scritti dagli attributi sono versionati da Lungo.Registry.schemaVersion (1). lungo rifiuta una libreria la cui versione non sa leggere (LNG0709).

Tipi

Un tipo di specifica, una relazione di claim, un ruolo e un identificatore di facility sono stringhe con spazio dei nomi: due o più segmenti separati da . fatti di lettere minuscole, cifre e _ (e - dopo il primo segmento), ciascuno che inizia con una lettera: lungo.decides, acme.cost-bound, timing.clock.

Lo spazio dei nomi lungo è proprio di lungo e contiene solo questi:

Ogni altro spazio dei nomi appartiene a chi lo definisce: lungo ne controlla la grafia, lo porta in ogni pacchetto e non gli attribuisce alcun significato. Un pacchetto può definire così relazioni e tipi propri (examples/semantic-model definisce acme.cost-bound) senza alcuna modifica a lungo.

Attributi

Ogni attributo è globale: gli usi local e scoped vengono rifiutati, e così pure darne uno a una dichiarazione di un altro modulo (un record si legge dove sta la sua dichiarazione). Una dichiarazione riceve ciascun attributo una sola volta. Ognuno scrive un record, la costante interna decl._lungo_<tipo>; il worker controlla di nuovo ogni record quando legge il progetto compilato (LNG0701–LNG0707).

@[lungo_spec "kind"]

Marca una specifica del tipo dato. Qualunque dichiarazione può esserlo. Una specifica che è un oggetto logico (un contratto, una relazione, un protocollo) è meglio noncomputable, così non viene esportata.

@[lungo_spec "lungo.contract"]
noncomputable def SortsAscending : Contract (List Nat) (List Nat) := sortedPermutation fun a b => decide (a ≤ b)

@[lungo_claim "relation" subject f … spec S …]

Sul teorema che dimostra il claim: i suoi soggetti f … stanno nella relazione relation con le sue specifiche S …. subject è seguito da una o più dichiarazioni; spec e le specifiche sono facoltativi.

@[lungo_claim "lungo.satisfies" subject sort spec SortsAscending]
theorem sort_satisfies : Satisfies sort SortsAscending := …

Controlli: la dichiarazione è un teorema; ogni soggetto esiste, non è un teorema ed è menzionato dall’enunciato; ogni specifica ha @[lungo_spec] ed è menzionata dall’enunciato; nessuno è nominato due volte; e per una relazione lungo.*, l’enunciato ha la forma che la relazione richiede. Si legge solo l’enunciato, mai la dimostrazione. Le assunzioni a cui un claim è condizionato non si dichiarano: lungo le trova tra i tipi dei binder ∀ iniziali dell’enunciato.

@[lungo_facility "ns.name"]

Nomina una facility che l’host fornisce, con il suo identificatore. Si dà a qualunque dichiarazione che non sia un teorema (di solito una structure vuota), oppure a un’istanza di Lungo.Async.Interface Op, che crea una facility asincrona le cui operazioni sono i costruttori di Op.

@[lungo_facility "timing.clock"]
structure Clock

inductive StoreOp where
  | get (key : String)
  | put (key value : String)

@[lungo_facility "store.kv"]
instance storeOps : Lungo.Async.Interface StoreOp where
  Ret
    | .get _ => Option String
    | .put _ _ => Unit

Per una facility asincrona, Op deve essere un tipo induttivo senza parametri né indici, nessun campo di un costruttore può essere una prova o un tipo, e ciò che ogni costruttore riceve in risposta (Ret) deve ridursi a un tipo che non dipende dai campi del costruttore (LNG0707).

@[lungo_operation C]

Su una dichiarazione @[extern]: è un’operazione della facility C, che l’host implementa. Si scriva prima @[extern "symbol"]; l’attributo si applica dopo che la dichiarazione è stata compilata.

@[extern "timing_now", lungo_operation Clock]
opaque now (u : Unit) : IO Nat

Controlli: C ha @[lungo_facility] e non è una facility asincrona; la dichiarazione ha @[extern]. lungo richiede inoltre che un’operazione abbia una voce per C e non sia implementata dal runtime o da un @[export] (LNG0706). Un’operazione il cui tipo Lean non è IO o EIO è una funzione per Lean, che può valutarne una chiamata una sola volta e conservarne il valore: l’implementazione dell’host deve rispondere lo stesso agli stessi argomenti.

@[lungo_assumption C]

Su una proposizione (o una famiglia di proposizioni, o una classe in Prop): viene assunta, mai dimostrata, dell’implementazione della facility C da parte dell’host. Un claim che la prende come ipotesi è condizionato a essa.

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

@[lungo_role "role"]

Su una definizione che un programma esegue (non un teorema): a che cosa serve. lungo.oracle marca un’implementazione di riferimento con cui si verifica altro codice; lungo.monitor, lungo.model e lungo.implementation sono gli altri ruoli di lungo.

Relazioni

Un claim in una delle relazioni di lungo deve enunciarla nella sua forma, così che la relazione significhi la stessa cosa in ogni pacchetto. La forma si legge dall’enunciato dopo i suoi ∀ iniziali; f menziona ogni soggetto significa che ogni soggetto compare in f.

Moduli di supporto

Lungo.Spec.Contract

• Contract α β con pre : α → Prop e post : α → β → Prop; Satisfies f c: ogni input che soddisfa pre dà un output che soddisfa post.
• ExceptContract α ε β aggiunge refuses : α → ε → Prop; SatisfiesExcept f c per una funzione che restituisce Except ε β: restituisce un output che soddisfa post, oppure rifiuta come refuses consente.
• Contract.Strengthens strong weak e satisfies_weaken; Contract.seq e satisfies_comp per due funzioni in sequenza.

Lungo.Spec.Model

• BehavioralModel β con admits : β → Prop; Refines impl spec: ogni comportamento che impl ammette, spec lo ammette.
• BehavioralModel.ofFunction f, ofRelation r, function_refines_relation, inter e refines_inter; refines_refl e refines_trans.

Lungo.Spec.State

• StateSpec σ ι ο con init, invariant e step : σ → ι → ο → σ → Prop.
• Per un passo eseguibile exec : σ → ι → ο × σ: StateSpec.Preserves s exec (gli stati iniziali soddisfano l’invariante e ogni passo lo mantiene) e StateSpec.Implements s exec (dagli stati che soddisfano l’invariante, ogni passo è uno che step ammette).
• StateSpec.run exec, preserves_run e reachable_invariant: un invariante preservato vale lungo ogni esecuzione da uno stato iniziale.

Lungo.Trace

• Protocol ε: le tracce che ammette (allowed), chiuse per prefissi; Protocol.any, always p, ofSteps start next, both, Within e within_trans.
• Reducer ε σ con start e step : σ → ε → Option σ; Reducer.run, Reducer.protocol e accepts_iff.
• ReducerRefines r p (ogni traccia che r accetta, p la ammette) e refines_of_invariant, che lo dimostra da un invariante che lega gli stati alle tracce che li raggiungono.
• Hyperproperty ε e Noninterference r low observe, per proprietà su più tracce.

Lungo.Monitor

• Monitor ε σ con start e step : σ → ε → Except String σ: l’host passa gli eventi uno alla volta; un errore è una violazione e il suo motivo.
• Monitor.run, Accepts, e Sound m p: m accetta esattamente le tracce che p ammette.
• Monitor con la loro correttezza: ofPredicate (ofPredicate_sound), ofReducer (ofReducer_sound) e both (both_sound).

Lungo.Async

• Interface Op con Ret : Op → Type, ciò che ogni operazione riceve in risposta.
• Program Op α: done value oppure call op resume; una Monad, con Program.perform op. Un export che restituisce un Program è una funzione asincrona in ogni linguaggio, che riceve un handler che esegue le operazioni.
• Program.run handler: interpreta un programma in qualunque monade, così i claim possono eseguirlo contro un modello dell’host.
• Exchange, Admits p exchanges a, trace answer p e i teoremi admits_trace, run_id, admits_unique e admits_bind.

I test della libreria

lake build LungoTest controlla, con #guard_msgs, ogni rifiuto di ogni attributo.