Come imporre politiche di fiducia e di garanzia

Questa guida mostra come far fallire la build quando una dichiarazione Lean esportata, o la dimostrazione di un claim su di essa, dipende da codice non dimostrato o non controllato; come richiedere che gli export portino claim dimostrati e che nulla si appoggi su un’assunzione che non accetti; e come verificare da che cosa dipendono gli export.

Scegli le politiche

Tre politiche si applicano a ogni dichiarazione esportata, e le prime due anche alla prova di ogni claim (il teorema che lo dimostra):

Abilita quelle che ti servono in build.rs:

fn main() -> lungo_build::Result<()> {
    lungo_build::configure().deny_axioms(true).deny_unsafe(true).compile_lean("lean")
}

Una violazione fallisce con LNG0601 ed elenca ogni export con le dipendenze responsabili:

error[LNG0601]: exported declarations violate the configured trust policy:
  Formal.step depends on `sorry` (deny_sorry)
  the claim Formal.step_implements depends on `sorry` (deny_sorry)

Rimuovi la dipendenza in Lean, oppure smetti di esportare la dichiarazione (per un claim, completa la sua dimostrazione o togli il suo @[lungo_claim]).

deny_sorry è attiva per impostazione predefinita; disattivala solo per il lavoro in corso (.deny_sorry(false)). Con la politica disattivata, un claim la cui dimostrazione usa sorry viene riportato con lo stato incomplete, mai proved.

Richiedi claim dimostrati

Per far fallire la build quando un export non porta alcun claim dimostrato, seleziona gli export per percorso (. seleziona ogni export; qualsiasi altro percorso l’export che nomina e ogni export al suo interno come spazio dei nomi):

fn main() -> lungo_build::Result<()> {
    lungo_build::configure().require_claims("Formal.step").require_claims("Formal.run").compile_lean("lean")
}

Un export selezionato senza un claim dimostrato fallisce con LNG0602:

error[LNG0602]: the export Formal.run has no proved claim (`require-claims` selects it with "Formal.run"); state what it does with `@[lungo_claim]` on a theorem about it

Un percorso che non seleziona alcun export è un errore di configurazione.

Vieta assunzioni

Un claim può essere dimostrato sotto un’assunzione su una facility dell’host (vedi come dichiarare facility e assunzioni). Per rifiutare ciò che si appoggia su un’assunzione che non accetti, vietala con il suo nome Lean; vietare una facility vieta tutte le sue assunzioni, e ogni export che chiama le sue operazioni:

lungo_build::configure().forbid_assumption("Timing.Ticks").compile_lean("lean")

Un claim dimostrato che la assume, o un export che ha bisogno di una facility vietata, fallisce con LNG0603. Un nome che non è né un’assunzione né una facility del programma è un errore di configurazione.

Per il comando lungo, le stesse impostazioni sono la tabella [assurance] di lungo.toml:

[assurance]
require-claims = ["Formal.step", "Formal.run"]
forbid-assumptions = ["Timing.Ticks"]

e lungo assurance --policy le controlla senza generare nulla, uscendo con stato 2 quando non sono rispettate.

Verifica senza fallire

Per vedere le dipendenze di ogni export senza imporre una politica, leggi assurance.json nell’output della build (il trust di ogni export, con i suoi claim, le assunzioni e le facility; vedi il documento di garanzia), elenca gli export con un problema con lungo assurance --trust-issue <issue> (sorry, axioms, unsafe, partial, facility, no-claim, incomplete, assumption), esamina una dichiarazione con lungo inspect <name>, oppure leggi i metadati in esecuzione:

for d in formal::__meta::declarations() {
    println!("{}: axioms {:?}, claims {:?}", d.lean_name, d.trust.axioms, d.assurance.claims);
}

Le definizioni partial e le dipendenze extern vengono riportate ma non sono governate da una politica: sono parti ordinarie del codice Lean eseguibile.