Come definire un modello semantico — Documentazione di lungo

Questa guida mostra come un team definisce un proprio vocabolario di specifiche e claim, come un modello di costo, un livello di sicurezza o una proprietà normativa, in un pacchetto Lake a sé. Altri progetti enunciano poi claim in quel vocabolario, e lungo li riporta come riporta i propri.

L’esempio di riferimento è lungo-rs/examples/semantic-model. Il pacchetto acme di Acme definisce un modello di costo, e il programma inventory dimostra che le sue ricerche vi rientrano.

Scegli uno spazio dei nomi

I tipi di specifica, le relazioni di claim, i ruoli e gli identificatori delle facility sono stringhe con spazio dei nomi. Ciascuna è formata da due o più segmenti separati da ., fatti di lettere minuscole, cifre e _, con - ammesso anche dopo il primo segmento, e ogni segmento inizia con una lettera: acme.cost-model, acme.cost-bound, bank.audit.reviewed.

Lo spazio dei nomi lungo appartiene a lungo: vi esistono solo i tipi e le relazioni che lungo definisce (lungo.decides, lungo.contract, …), e qualsiasi altra stringa lungo.* è un errore. Ogni altro spazio dei nomi appartiene a chi lo usa. Scegline uno che nomini la tua organizzazione o il tuo dominio.

Definisci il modello in un pacchetto a sé

Il modello è Lean ordinario: definizioni che dicono che cosa significano i tuoi tipi, registrate con @[lungo_spec] nel tuo spazio dei nomi. Il pacchetto richiede la libreria Lean di lungo per l’attributo:

# acme/lakefile.toml
name = "acme"
version = "0.1.0"
defaultTargets = ["Acme"]

[[require]]
name = "lungo"
path = "../../../lean"

[[lean_lib]]
name = "Acme"

import Lungo

namespace Acme

/-- `steps` never exceeds `bound`. -/
def CostBound {α : Type} (steps : α → Nat) (bound : α → Nat) : Prop := ∀ a, steps a ≤ bound a

/-- At most `k` steps per unit of size, and `k` more: linear in `size`. -/
@[lungo_spec "acme.cost-model"]
def Linear {α : Type} (size : α → Nat) (k : Nat) (steps : α → Nat) : Prop :=
  CostBound steps fun a => k * size a + k

end Acme

Una relazione di claim non richiede alcuna dichiarazione. È la stringa che un claim indica, e significa ciò che il tuo pacchetto documenta. Scrivi quel significato accanto al modello, come fanno le docstring qui sopra.

Enuncia claim rispetto al modello

Un progetto che usa il modello richiede il pacchetto ed enuncia claim con la tua relazione, citando le tue specifiche:

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

[[require]]
name = "acme"
path = "../acme"

import Lungo
import Acme

namespace Inventory

/-- The steps looking `sku` up takes. -/
def lookupSteps (sku : String) (items : List Item) : Nat := (lookupCounted sku items).2

/-- A lookup examines each item at most once: linear in the inventory's size. -/
@[lungo_claim "acme.cost-bound" subject lookupSteps spec Acme.Linear]
theorem lookup_linear (sku : String) : Acme.Linear List.length 1 (lookupSteps sku) := by
  ...

Esegui lake update una volta dopo aver aggiunto il requisito, e fai il commit del manifest: le build di lungo non scaricano né aggiornano mai le dipendenze.

Che cosa lungo verifica, e che cosa no

Per una relazione tua, lungo verifica tutto ciò che non dipende dal suo significato:

la relazione è una stringa con spazio dei nomi ben formata;
l’evidenza è un teorema, e la sua dimostrazione è verificata dal kernel di Lean come ogni altra;
ogni soggetto esiste, è una definizione e non un teorema, ed è menzionato nell’enunciato;
ogni specifica è registrata con @[lungo_spec] ed è menzionata nell’enunciato;
la politica di fiducia (deny-sorry, deny-axioms) si applica all’evidenza.

Non verifica la forma dell’enunciato. Per le relazioni lungo.*, lungo richiede una forma (per esempio, lungo.decides deve enunciare f … = true ↔ P …). Per le tue, l’enunciato può essere qualsiasi cosa che menzioni i suoi soggetti e le sue specifiche. Per mantenere uniformi i claim con la tua relazione, dai alla relazione una definizione e citala come specifica, come i claim acme.cost-bound citano Acme.Linear. L’enunciato dice allora, nei tuoi termini, esattamente che cosa è dimostrato.

Nessuna parte di lungo deve cambiare: i record, assurance.json, i pacchetti generati e il comando lungo portano i tuoi tipi così come sono.

Guardalo nel rapporto

lungo assurance Inventory.lookupSteps

Inventory.lookupSteps
  == Claims ==
    [proved] acme.cost-bound Inventory.lookup_linear (of Acme.Linear)
  …

lungo assurance --claim-kind acme.cost-bound elenca gli export con un claim di questo tipo. Una politica require-claims è soddisfatta da un claim dimostrato con qualsiasi relazione. In ogni pacchetto generato, la relation del claim è acme.cost-bound e il kind della specifica è acme.cost-model, con package acme: il pacchetto che la dichiara, non quello che la cita.

Distribuisci il modello e verifica che resti lo stesso

Il pacchetto del modello si può generare da solo, per il codice che ne ha bisogno a runtime:

# acme/lungo.toml
project = "."

Ogni pacchetto che cita Acme.Linear porta allora un fingerprint della definizione rispetto a cui è stato dimostrato, che copre Acme.CostBound e qualunque altra definizione di Acme a cui si riduce. Componi i loro documenti con quello di Acme per verificare che indichino tutti lo stesso modello; vedi come comporre le garanzie tra pacchetti.