Ricordiamo che la regola 6, da Parte 1mostra che possiamo verificare UN algoritmo per InternalAddma non è IL algoritmo utilizzato nel crate di Rust. Successivamente ci rivolgiamo a quell’algoritmo.
Ecco la funzione Rust di interesse con alcuni codici esclusi per ora:
// https://stackoverflow.com/questions/49599833/how-to-find-next-smaller-key-in-btreemap-btreeset
// https://stackoverflow.com/questions/35663342/how-to-modify-partially-remove-a-range-from-a-btreemap
fn internal_add(&mut self, range: RangeInclusive<T>) {
let (start, end) = range.clone().into_inner();
assert!(
end <= T::safe_max_value(),
"end must be <= T::safe_max_value()"
);
if end < start {
return;
}
//... code continues ...
}
Ed ecco l’inizio del porto di Dafny:
method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>)
requires ValidSeq(xs)
ensures ValidSeq(r)
ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range)
{
var (start, end) := range;
if end < start {
r := xs;
return;
}
//... code continues ...
}
Alcuni punti di possibile interesse:
- Il codice Rust utilizza
selfe incapsulamento di tipo orientato agli oggetti. Dafny supporta questo stile di codifica, ma, per semplicità, non lo uso qui. Nello specifico, il codice Rust mutaself. Ho scelto di scrivere il codice Dafny in modo più funzionale: richiede una sequenza immutabile e restituisce una nuova sequenza immutabile. - Il codice Rust gestisce la memoria con il controllo del prestito. Ciò porta ad espressioni come
range.clone(). Dafny gestisce la memoria con un garbage collector. In entrambi i casi, verrà curata la sicurezza della memoria. Pertanto lo ignoriamo in questa convalida. - Il codice Rust è generico
Tche altrove definisco per includere tutti i tipi interi standard di Rust, ad esempio,u8,isize,i128. Il codice Dafny è definito suintun singolo tipo che rappresenta numeri interi di dimensione arbitraria. Ciò significa che questa porta Dafny non deve verificare la presenza di overflow di numeri interi. (Vedere un articolo precedente per dimostrare formalmente la sicurezza del troppopieno con il verificatore Kani Rust.) - Il codice Rust include un runtime
assert!ciò è necessario in Rust per vietare un caso speciale: l’inserimentou128::max_valuein unRangeSetBlaze<u128>. Perché Dafny usa dimensioni arbitrarieintignora questo caso speciale.
A parte: Qual è la lunghezza del Rust gamma inclusiva
0..=u128::max_value? La risposta èu128::max_value+1, un valore troppo grande per essere rappresentato con qualsiasi tipo intero standard di Rust. ILrange-set-blazei limiti della cassa variano a0..=u128::max_value-1, in modo che le lunghezze possano essere rappresentate con au128.
Consideriamo ora il resto internal_add algoritmo. Ricordiamo che abbiamo un elenco di intervalli disgiunti ordinati e un nuovo intervallo non vuoto che vogliamo inserire. Per esempio
L’algoritmo ci fa trovare quale (se presente) intervallo esistente si trova prima (o all’inizio) del nuovo intervallo. Chiamatelo l’intervallo “prima”. Consideriamo quindi quattro casi:
- Caso 1: Il nuovo intervallo non tocca il suo intervallo precedente, quindi inseriamo il nuovo intervallo mentre controlliamo per vedere se tocca altri intervalli.
- Caso 2: Il nuovo intervallo tocca l’intervallo prima e si estende oltre esso, quindi estendiamo la fine dell’intervallo prima mentre controlliamo per vedere se tocca altri intervalli. (Quando non vengono toccati altri intervalli, l’operazione sarà molto veloce.)
- Caso 3: Il nuovo intervallo tocca l’intervallo precedente ma non si estende oltre, quindi non fare nulla. (Sarà sempre molto, molto veloce.)
- Caso 4: il nuovo intervallo inizia prima di qualsiasi intervallo, quindi aggiungilo mentre controlli per vedere se tocca altri intervalli.
Qui è l’algoritmo di Rust:
// code continued ...
// FUTURE: would be nice of BTreeMap to have a partition_point function that returns two iterators
let mut before = self.btree_map.range_mut(..=start).rev();
if let Some((start_before, end_before)) = before.next() {
// Must check this in two parts to avoid overflow
if match (*end_before).checked_add(&T::one()) {
Some(end_before_succ) => end_before_succ < start,
None => false,
} {
self.internal_add2(&range);
} else if *end_before < end {
self.len += T::safe_len(&(*end_before..=end - T::one()));
*end_before = end;
let start_before = *start_before;
self.delete_extra(&(start_before..=end));
} else {
// completely contained, so do nothing
}
} else {
self.internal_add2(&range);
}
}
Ed eccolo qui a Dafny:
// code continued ...
var beforeHi := IndexAtOrBeforePlusOne(xs, start);
if beforeHi > 0 { // does not go at front
var (startBefore, endBefore) := xs(beforeHi-1);
if endBefore+1 < start {
r := InternalAdd2(xs, range);
} else if endBefore < end {
r := xs(..beforeHi-1) + ((startBefore, end)) + xs(beforeHi..);
assume exists i: nat :: i < |r| && r(i) == (startBefore,end) && ValidSeq(r(..i+1)) && ValidSeq(r(i+1..));
r := DeleteExtra(r, (startBefore,end));
} else{
r := xs;
}
}
else // goes at front
{
r := InternalAdd2(xs, range);
}
}
Alcuni punti di possibile interesse:
- Il codice Rust manipola a
BTreeMaptramite chiavi e valori. Il codice Dafny manipola un sortedseqcon indici (ad accesso casuale). Ho fatto in modo che le operazioni Dafny rispecchino le operazioni Rust anche se questo rende il codice Dafny meno naturale. - Anche il codice Rust si aggiorna
self.lenil numero di singoli numeri interi in RangeSetBlaze. Il codice Dafny lo ignora. (In aggiornamentolenè una funzionalità che potrebbe essere aggiunta al codice Dafny in futuro.) - Come prima, la versione Rust include il codice per evitare l’overflow che Dafny ignora.
Ho continuato il port scrivendo una versione Dafny di internal_add2 E delete_extrale due funzioni che internal_add chiamate. Ho terminato il port scrivendo i metodi chiamati da questi due metodi, ecc. Il port completo è di circa 185 righe di codice. Puoi vederlo Qui.
Non convalida. Lavoreremo successivamente sulla convalida.
In questo passaggio aggiungerai suggerimenti di convalida al tuo codice, ad esempio sotto forma di assert dichiarazioni. Dafny utilizza questi suggerimenti per provare a convalidare il tuo codice. Come principiante di Dafny, io (Carl) ho trovato l’aggiunta di suggerimenti più difficile della codifica. In parte perché non sapevo quando (o se) Dafny si sarebbe accontentata e avrei potuto smettere.
Tuttavia, ho imparato come dovrei iniziare. Ad esempio, il codice sopra per InternalAdd produce due errori di verifica. Innanzitutto, il verificatore Dafny riporta che uno dei ensures potrebbe non reggere:
This postcondition might not hold: SeqToSet(r) == SeqToSet(xs) + RangeToSet(range)
A parte: “Postcondizione” corrisponde a
ensures. “Precondizione” corrisponde arequires.
In secondo luogo, il verificatore Dafny lamenta che una precondizione (ovvero una delle requires) per DeleteExtra non può essere dimostrato.
Ci concentreremo prima sul primo problema aggiungendo un assert fino in fondo al metodo. Lo scriviamo per rispecchiare il ensures.
// ... adding this as the last line in InternalAdd
assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range);
}
Ignoreremo esplicitamente il file DeleteExtra problema, per ora, con un assume.
// ...
assume exists i: nat :: i < |r| && r(i) == (startBefore,end) && ValidSeq(r(..i+1)) && ValidSeq(r(i+1..));
r := DeleteExtra(r, (startBefore,end));
//...
Il validatore Dafny ora si lamenta solo del nostro nuovo finale assert. Dice che “l’affermazione potrebbe non reggere”.
Ricordiamo che il InternalAdd il codice utilizza nidificati if affermazioni per dividere il proprio lavoro in cinque casi. Successivamente sposteremo la nostra asserzione dalla fine del metodo alla fine di ogni caso. Cerca le righe che terminano con a // case commento nel risultato:
method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>)
requires ValidSeq(xs)
ensures ValidSeq(r)
ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range)
{
var (start, end) := range;
if end < start {
r := xs;
assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 0 - validates
return;
}var beforeHi := IndexAtOrBeforePlusOne(xs, start);
if beforeHi > 0 { // does not go at front
var (startBefore, endBefore) := xs(beforeHi-1);
if endBefore+1 < start {
r := InternalAdd2(xs, range);
assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 1 - validates
} else if endBefore < end {
r := xs(..beforeHi-1) + ((startBefore, end)) + xs(beforeHi..);
assume exists i: nat :: i < |r| && r(i) == (startBefore,end) && ValidSeq(r(..i+1)) && ValidSeq(r(i+1..));
r := DeleteExtra(r, (startBefore,end));
assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 2 - fails
} else{
r := xs;
assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 3 - fails
}
}
else // goes at front
{
r := InternalAdd2(xs, range);
assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 4 - validates
}
}
Dafny ora ci dice che i casi 0, 1 e 4 sono validi. Il caso 2 fallisce (e lo contiene assume che dovremo eventualmente rimuovere). Per ora, però, lavoriamo sul caso 3.
Ricordiamo dalla Regola 7 di questo articolo, che il caso 3 è quando aggiungiamo un nuovo intervallo (rosso) che è completamente coperto da un intervallo esistente (l’intervallo blu “prima”), quindi il codice non deve fare nulla.
Quindi, pensando logicamente, cosa sappiamo? Sappiamo che gli interi coperti dall’intervallo precedente sono un superinsieme degli interi coperti dal nuovo intervallo. Sappiamo anche che l’intervallo prima fa parte del nostro elenco originale di intervalli ordinati e disgiunti (gli intervalli blu). Aggiungeremo questi due suggerimenti al nostro codice tramite assert dichiarazioni:
Dafny concorda che questi due suggerimenti siano veri (segni di spunta verdi), ma continua a non accettarli assert di interesse (segno rosso).
Sembra che abbiamo bisogno di un altro suggerimento. Nello specifico, dobbiamo convincere Dafny che gli interi coperti dall’intervallo prima sono un sottoinsieme degli interi coperti dall’elenco di tutti gli intervalli ordinati e disgiunti. Intuitivamente, questo è vero perché l’intervallo prima è uno degli intervalli nell’elenco.
Scriviamo questo suggerimento come un lemma senza corpo. Dafny lo accetta.
A parte: perché Dafny accetta questo lemma senza nulla nel suo corpo? Non lo so e non ho una buona intuizione. Ha funzionato e basta. In caso contrario, avrei provato ad aggiungere affermazioni al suo corpo.
Utilizzando il lemma, il caso 3 ora convalida:
Ciò significa che abbiamo convalidato i casi 0, 1, 3 e 4. Successivamente passeremo al caso 2. Inoltre, alcuni dei metodi menzionati, ad esempio, DeleteExtranon sono ancora convalidati e dovremmo lavorare su quelli. (Puoi vedere il codice fino a questo punto, Qui.)
Per consigli generali sul debugging della verifica, fare riferimento a questa sezione della Guida per l’utente di Dafny. Consiglio anche questo Risposta di Stack Overflow e mini-tutorial del Prof. James Wilcox.
Nel complesso, l’idea è quella di dividere il compito di convalidare l’algoritmo in molte attività di convalida più piccole. L’ho trovato più difficile della programmazione, ma non troppo difficile e comunque divertente.
Alla fine ho aggiunto circa 200 righe di convalida alle 185 righe di codice regolari (codice completo qui). Quando finalmente ho convalidato l’ultimo metodo, ho pensato erroneamente di aver finito.
Con mia sorpresa (e delusione) il lavoro non finisce la prima volta che tutto si convalida. Devi anche assicurarti che il tuo progetto venga nuovamente convalidato e valido per gli altri. Discuteremo questa regola più avanti.
Pensavo di aver finito. Quindi, ho spostato la definizione di sei righe della matematica Min funzione da Libreria standard Dafny al mio codice. Ciò ha causato il fallimento della mia convalida, senza motivo logico (letteralmente!). Successivamente, dopo aver pensato di aver risolto il problema, ho eliminato un metodo che non era stato utilizzato. Ancora una volta, la convalida ha iniziato a fallire senza una ragione logica.
Cosa sta succedendo? Dafny funziona in modo euristico tramite una ricerca casuale. La modifica superficiale del codice (o la modifica dei semi casuali) può modificare il tempo necessario alla ricerca. A volte, la quantità di tempo cambia drasticamente. Se il nuovo orario supera il limite di tempo impostato dall’utente, la convalida fallirà. (Parleremo più approfonditamente del limite di tempo nel suggerimento n. 3, di seguito.)
Dovresti testare l’affidabilità della tua convalida provando diversi semi casuali. Ecco i comandi che ho usato (su Windows) per convalidare un file con 10 semi casuali.
@rem Find the location of Dafny and add it to your path
set path=C:\Users\carlk\.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%
dafny verify seq_of_sets_example7.dfy --verification-time-limit:30 --cores:20 --log-format csv --boogie -randomSeedIterations:10
Il risultato è un file *.csv che puoi aprire come foglio di calcolo e quindi cercare gli errori:
A parte: per ulteriori idee sulla misurazione dell’affidabilità di convalida di Dafny, vedere questa risposta Stack Overflow su analizzare i file *.csv e questa discussione su GitHub consigliando lo strumento dafny-reportgenerator.
Dopo aver individuato i punti problematici, ho chiesto aiuto al coautore Divyanshu Ranjan. Divyanshu Ranjan ha utilizzato la sua esperienza con Dafny per risolvere i problemi di convalida del progetto.
Ecco i suoi consigli, con esempi tratti dal progetto:
Suggerimento n. 1: quando possibile, rimuovere require affermazioni che coinvolgono “forall” ed “esiste”.
Ricordiamo dalla Regola 4 quella funzione fantasma SeqToSet restituisce l’insieme di numeri interi coperti da un elenco ordinato e disgiunto di intervalli non vuoti. Definiamo “ordinato e disgiunto” con funzione ValidSeqche internamente ne utilizza due forall espressioni. Possiamo rimuovere il requisito secondo cui l’elenco deve essere ordinato e disgiunto, in questo modo:
ghost function SeqToSet(sequence: seq<NeIntRange>): set<int>
decreases |sequence|
// removed: requires ValidSeq(sequence)
{
if |sequence| == 0 then {}
else if |sequence| == 1 then RangeToSet(sequence(0))
else RangeToSet(sequence(0)) + SeqToSet(sequence(1..))
}
Dal nostro punto di vista, abbiamo la stessa funzione utile. Dal punto di vista di Dafny, la funzione ne evita due forall espressioni ed è più facile da applicare.
Suggerimento n. 2 Usa calc per evitare congetture da parte di Dafny.
Con un Dafny calc dichiarazione, elenchi i passaggi esatti necessari per arrivare a una conclusione. Ad esempio, ecco a calc dal DeleteExtra metodo:
calc {
SeqToSet(xs(..indexAfter+1)) + SeqToSet(xs(indexAfter+1..));
==
{ SeqToSetConcatLemma(xs(..indexAfter+1), xs(indexAfter+1..)); }
SeqToSet(xs(..indexAfter+1) + xs(indexAfter+1..));
==
{ assert xs == xs(..indexAfter+1) + xs(indexAfter+1..); }
SeqToSet(xs);
==
{ SetsEqualLemma(xs, r(indexAfter), r2, indexAfter, indexDel); }
SeqToSet(r2);
}
A questo punto del codice, xs è una sequenza di intervalli, ma non può essere ordinata e disgiunta. IL calc afferma che:
- gli interi coperti dalle due parti di
xsequivale - gli interi coperti dalla concatenazione delle sue due parti, sono uguali
- gli interi coperti da
xsequivale rs.
Per ogni passaggio è consentito includere lemmi o asserzioni per aiutare a dimostrare quel passaggio. Ad esempio, questa affermazione aiuta a dimostrare il passaggio dal passaggio 3 al passaggio 4:
{ assert xs == xs(..indexAfter+1) + xs(indexAfter+1..); }
Per efficienza e controllo, questi lemmi e asserzioni non saranno visibili al validatore oltre il suo passaggio. Ciò mantiene Dafny concentrato.
Suggerimento n. 3: utilizzare timeLimit per fornire calcoli dove necessario.
Dafny smette di provare a convalidare un metodo su un valore impostabile dall’utente timeLimit. I limiti di 10, 15 o 30 secondi sono comuni perché, come utenti, generalmente desideriamo che le convalide impensabili falliscano rapidamente. Tuttavia, se sappiamo che prima o poi avverrà una convalida, possiamo impostare un limite di tempo specifico per il metodo. Ad esempio, Divyanshu Ranjan lo ha notato DeleteExtra di solito viene convalidato, ma richiede più tempo rispetto agli altri metodi, quindi ha aggiunto un limite di tempo specifico per il metodo:
method {:timeLimit 30} DeleteExtra(xs: seq<NeIntRange>, internalRange: IntRange) returns (r: seq<NeIntRange>)
// ...
A parte:
timeLimitnon tiene conto della differenza di velocità tra i computer, quindi impostalo in modo un po’ generoso.
Suggerimento n. 4: utilizzare split_here per dividere un problema di convalida in due.
Come il Domande frequenti su Dafny spiegare, a volte convalidare una serie di asserzioni insieme è più veloce e talvolta convalidarle una alla volta è più veloce.
Usa un assert {:split_here} true; istruzione per dividere una sequenza di asserzioni in due parti ai fini della convalida. Ad esempio, anche con il timeLimit, DeleteExtra scaduto finché Divyanshu Ranjan non ha aggiunto questo:
// ...
else
{
r := (s(..i) + (pair)) + s(i..);
assert r(..(i+1)) == s(..i) + (pair);
assert r((i+1)..) == s(i..);
assert {:split_here} true; // split validation into two parts
calc {
SeqToSet(r(..(i+1))) + SeqToSet(r((i+1)..));
// ...
Suggerimento n. 5: mantieni i lemmi piccoli. Se necessario, dividere le garanzie tra i lemmi.
A volte i lemmi cercano di fare troppe cose in una volta. Considera il SetsEqualLemma. È correlato all’eliminazione degli intervalli ridondanti. Se ad esempio inseriamo a in xsgli intervalli contrassegnati con “X” diventano ridondanti.
La versione originale di SetsEqualLemma ne conteneva 12 requires e 3 ensuresDivyanshu Ranjan lo ha diviso in due lemmi: RDoesntTouchLemma (11 requires e 2 ensures) E SetsEqualLemma (3 requires e 1 ensures). Con questa modifica, il progetto è stato convalidato in modo più affidabile.
Fonte: towardsdatascience.com
