Come dichiarare claim sugli export

Questa guida mostra come dire, in Lean, che cosa una definizione esportata è dimostrato fare, così che ogni pacchetto generato lo porti con sé: un claim è un teorema registrato con @[lungo_claim], che nomina gli export di cui parla (i suoi soggetti) e le specifiche a cui li mette in relazione. Gli esempi sono i crate sort e session nella directory examples di lungo-rs.

Richiedi la libreria Lean di lungo

Gli attributi sono nella libreria Lean di lungo, il pacchetto Lake lungo nella directory lean di lungo-rs, rilasciato con lungo alla versione di lungo. Richiedilo dal lakefile del progetto:

# lakefile.toml
[[require]]
name = "lungo"
git = "https://github.com/machinefabric/lungo-rs"
rev = "v<versione di lungo>"
subDir = "lean"

(oppure path = "…/lungo-rs/lean" per un checkout), esegui lake update una volta, fai il commit del manifest e scrivi import Lungo dove dichiari i claim. Una libreria di una versione di schema diversa da quella del lungo con cui costruisci viene rifiutata (LNG0709). Gli attributi aggiungono solo record: il programma compilato è lo stesso con o senza.

Marca le specifiche

Una specifica è la dichiarazione a cui un claim mette in relazione i suoi soggetti: un contratto, un modello, una macchina a stati, un protocollo. Dalle @[lungo_spec "<tipo>"]:

import Lungo

namespace Sorting

open Lungo.Spec

/-- Numbers in ascending order: the output is ordered and a permutation of the input. -/
@[lungo_spec "lungo.contract"]
noncomputable def SortsAscending : Contract (List Nat) (List Nat) where
  pre _ := True
  post xs ys := ys.Pairwise (fun a b => decide (a ≤ b)) ∧ ys.Perm xs

I tipi di lungo sono lungo.relation, lungo.contract, lungo.model, lungo.state, lungo.protocol e lungo.property; qualsiasi altro spazio dei nomi appartiene a un pacchetto (acme.cost-model), e viene trasportato senza interpretarlo. Gli strumenti della libreria per scrivere specifiche sono Lungo.Spec.Contract, Lungo.Spec.BehavioralModel, Lungo.Spec.StateSpec, Lungo.Trace.Protocol e Lungo.Monitor (vedi la libreria Lean di lungo).

Rendi noncomputable una specifica soltanto logica: un contratto o un protocollo non ha nulla da eseguire, e una definizione calcolabile dei moduli radice viene esportata come ogni altra. Un modello eseguibile (un’implementazione di riferimento) può restare calcolabile ed essere esportato.

Dichiara il claim

Dimostra il teorema, poi registralo con la relazione, i soggetti dopo subject e le specifiche dopo spec:

def sort (xs : List Nat) : List Nat := xs.mergeSort fun a b => decide (a ≤ b)

@[lungo_claim "lungo.satisfies" subject sort spec SortsAscending]
theorem sort_satisfies : Satisfies sort SortsAscending := by
  intro xs _
  refine ⟨List.pairwise_mergeSort ?_ ?_ xs, List.mergeSort_perm xs _⟩
  · intro a b c hab hbc; simp only [decide_eq_true_eq] at *; omega
  · intro a b; simp only [Bool.or_eq_true, decide_eq_true_eq]; omega

L’attributo controlla che la dichiarazione sia un teorema, che ogni soggetto sia una definizione (non un teorema) menzionata dal suo enunciato, che ogni specifica abbia @[lungo_spec] e sia menzionata e, per le relazioni di lungo, che l’enunciato abbia la forma della relazione (dopo i suoi ∀ iniziali):

Una relazione in un altro spazio dei nomi (acme.cost-bound) appartiene a un pacchetto: la sua forma non viene controllata. Ciò che l’attributo rifiuta è un errore in Lean; lungo controlla di nuovo i record che legge, quindi un record scritto senza l’attributo è soggetto alle stesse regole (LNG0701–LNG0705).

L’esempio session dichiara che la sua funzione di passo implementa una macchina a stati dichiarativa:

@[lungo_spec "lungo.state"]
noncomputable def Spec : StateSpec Sess Op Bool where
  init s := s = { isOpen := false, count := 0 }
  invariant _ := True
  step s op accepted s' := …

@[lungo_claim "lungo.preserves" subject step spec Spec]
theorem step_implements : Spec.Implements step := by …

Rendi esplicite le assunzioni

Quando un claim vale solo se l’host si comporta bene (il suo orologio avanza, il suo archivio conserva ciò che riceve), dichiaralo come assunzione (@[lungo_assumption], vedi come dichiarare facility e assunzioni) e prendila come ipotesi del teorema:

@[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 claim resta dimostrato; viene riportato come condizionato a Timing.Ticks, in ogni pacchetto. Un’assunzione è una proposizione, mai un assioma, quindi una dimostrazione può usarla solo come ipotesi, dove il rapporto la vede.

Richiedi i claim nella build

Fai fallire la build quando un export non ha un claim dimostrato:

// build.rs
fn main() -> lungo_build::Result<()> {
    lungo_build::configure().require_claims("Sorting.sort").require_claims("Sorting.rank").compile_lean("lean")
}

# lungo.toml
[assurance]
require-claims = ["Sorting.sort", "Sorting.rank"]

Un percorso seleziona l’export che nomina e ogni export al suo interno come spazio dei nomi; "." seleziona ogni export. Un export selezionato che non è soggetto di alcun claim dimostrato fa fallire la build con LNG0602; un percorso che non seleziona nulla è un errore di configurazione.

La politica di fiducia si applica anche all’evidenza: un claim il cui teorema dipende da sorry fa fallire la build sotto deny_sorry (attivo per impostazione predefinita) con LNG0601, e deny_axioms rifiuta l’evidenza che poggia su assiomi non standard. Con deny_sorry(false) un claim del genere è riportato come incomplete, e non conta come dimostrato per require-claims. forbid-assumptions rifiuta i claim che poggiano su un’assunzione (LNG0603).

Tieni le leggi fuori dal programma

I teoremi sugli export possono stare in un modulo che il programma non importa, come un modulo Laws che importa il programma. Nominalo come modulo di garanzia: lungo lo carica per i suoi record e non lo compila mai nel programma.

# lungo.toml
[lean]
assurance-modules = ["Formal.Laws"]

(Builder::assurance_module("Formal.Laws"), oppure --assurance-module Formal.Laws). Un modulo radice non può essere anche un modulo di garanzia: i suoi record vengono letti comunque. Un programma che avrebbe bisogno di un valore calcolato solo dall’inizializzazione di un modulo di garanzia viene rifiutato (LNG0710).

Rileggi i claim

lungo assurance riporta per ogni export i suoi claim, ciò che le sue dimostrazioni non coprono e ciò che i suoi claim assumono:

$ lungo assurance Sorting.rank
program sorting: Lean 4.34.1 (…), lungo 1.88.0, assurance schema 1

Sorting.rank
  == Claims ==
    [proved] lungo.satisfies Sorting.rank_satisfies (of Sorting.RanksByScore)
    [proved] lungo.law Sorting.rank_stable
  == Trust ==
    (none)
  == Assumptions ==
    (none)
  == Facilities ==
    (none)

--format json lo scrive per gli strumenti; --claim-kind, --facility, --assumption e --trust-issue selezionano gli export; --policy controlla le politiche ed esce con stato 2 in caso di violazione (vedi il comando lungo). lungo check conta i claim, e lungo inspect <dichiarazione> li mostra per una dichiarazione.

Ogni pacchetto generato porta gli stessi record come assurance.json (vedi il documento di garanzia), e li legge in modo nativo:

let claim = sort::__meta::assurance().claim("Sorting.sort_satisfies").unwrap();
assert_eq!(claim.status, lungo::ClaimStatus::Proved);
assert_eq!(claim.specifications, ["Sorting.SortsAscending"]);