Nueve reglas para validar formalmente algoritmos de Rust con Dafny (Parte 2) | de Carl M. Kadie | octubre de 2023

Recordemos que la Regla 6, de Parte 1muestra que podemos verificar un algoritmo para InternalAddpero no lo es el Algoritmo utilizado en la caja Rust. A continuación nos ocuparemos de ese algoritmo.

Aquí está la función de interés de Rust con parte del código excluido por ahora:

// 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 ...
}

Y aquí está el inicio del puerto de 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 ...
}

Algunos puntos de posible interés:

• El código Rust utiliza self y encapsulación similar a la orientada a objetos. Dafny admite este estilo de codificación, pero, por simplicidad, no lo uso aquí. Específicamente, el código Rust muta self. Elegí escribir el código de Dafny de manera más funcional: toma una secuencia inmutable y devuelve una nueva secuencia inmutable.
• El código Rust administra la memoria con el verificador de préstamos. Esto lleva a expresiones como range.clone(). Dafny gestiona la memoria con un recolector de basura. En cualquier caso, se cuidará la seguridad de la memoria. Por lo tanto, lo ignoramos en esta validación.
• El código Rust es genérico. T que defino en otro lugar para incluir todos los tipos enteros estándar de Rust, por ejemplo, u8, isize, i128. El código Dafny se define en int, un tipo único que representa números enteros de tamaño arbitrario. Esto significa que este puerto Dafny no necesita comprobar si hay desbordamientos de enteros. [See a previous article for formally proving overflow safety with the Kani Rust verifier.]
• El código Rust incluye un tiempo de ejecución. assert! que se necesita en Rust para prohibir un caso especial: insertar u128::max_value en un RangeSetBlaze<u128>. Porque Dafny usa el tamaño arbitrario intignora este caso especial.

Aparte: ¿Cuál es la longitud del Rust? rango inclusivo 0..=u128::max_value? La respuesta es u128::max_value+1, un valor demasiado grande para representarlo con cualquier tipo de entero estándar de Rust. El range-set-blaze Los límites de la caja varían hasta 0..=u128::max_value-1, para que las longitudes se puedan representar con un u128.

Consideremos a continuación el resto de internal_add algoritmo. Recuerde que tenemos una lista de rangos disjuntos ordenados y un rango nuevo no vacío que queremos insertar. Por ejemplo

El algoritmo nos hace encontrar qué rango existente (si lo hay) está antes (o en) el inicio del nuevo rango. Llame a esto el rango “antes”. Luego consideramos cuatro casos:

• Caso 1: El nuevo rango no toca el rango anterior, por lo que insertamos el nuevo rango mientras verificamos si toca otros rangos.
• Caso 2: El nuevo rango toca el rango anterior y se extiende más allá de él, por lo que extendemos el final del rango anterior mientras verificamos si toca otros rangos. (Cuando no se toquen otros rangos, esto será muy rápido).

• Caso 3: El nuevo rango toca el rango anterior pero no se extiende más allá de él, así que no hagas nada. (Esto siempre será muy, muy rápido).

• Caso 4: El nuevo rango comienza antes que cualquier rango, así que agréguelo mientras verifica si toca otros rangos.

Aquí está el algoritmo en 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);
}
}

Y aquí está en 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);
}
}

Algunos puntos de posible interés:

• El código Rust manipula un BTreeMap a través de claves y valores. El código Dafny manipula un orden seq con índices (de acceso aleatorio). Hice que las operaciones de Dafny reflejaran las operaciones de Rust, aunque esto hace que el código de Dafny sea menos natural.
• El código Rust también se actualiza self.len, el número de enteros individuales en RangeSetBlaze. El código Dafny ignora esto. (Actualizando len es una característica que podría agregarse al código de Dafny en el futuro).
• Como antes, la versión Rust incluye código para evitar el desbordamiento que Dafny ignora.

Continué el puerto escribiendo una versión de Dafny de internal_add2 y delete_extralas dos funciones que internal_add llamadas. Terminé el puerto escribiendo los métodos que llaman estos dos métodos, etc. El puerto completo tiene aproximadamente 185 líneas de código. Puedes verlo aquí.

No valida. Trabajaremos en la validación a continuación.

En este paso, agregará sugerencias de validación a su código, por ejemplo, en forma de assert declaraciones. Dafny utiliza estas sugerencias para intentar validar su código. Como novato en Dafny, a mí (Carl) me resultó más difícil agregar pistas que codificar. En parte, porque no sabía cuándo (o si) Dafny estaría satisfecha y yo podría parar.

Sin embargo, aprendí cómo debería empezar. Por ejemplo, el código anterior para InternalAdd produce dos errores de verificación. Primero, el verificador de Dafny informa que uno de los ensures no puede contener:

This postcondition might not hold: SeqToSet(r) == SeqToSet(xs) + RangeToSet(range)

Aparte: “Poscondición” corresponde a ensures. “Condición previa” corresponde a requires.

En segundo lugar, el verificador de Dafny se queja de que una condición previa (que es una de las requires) para DeleteExtra no se puede probar.

Primero nos centraremos en el primer problema agregando un assert hasta el final del método. Lo escribimos para reflejar el ensures.

// ... adding this as the last line in InternalAdd
assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range);
}

Ignoraremos explícitamente el DeleteExtra problema, por ahora, 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));
//...

El validador de Dafny ahora solo se queja de nuestra nueva final assert. Dice “la afirmación podría no ser válida”.

Recuerde que el InternalAdd el código usa anidado if declaraciones para dividir su trabajo en cinco casos. A continuación, moveremos nuestra afirmación desde el final del método hasta el final de cada caso. Busque las líneas que terminan en // case comenta en el resultado:

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 ahora nos dice que los casos 0, 1 y 4 son válidos. El caso 2 falla (y contiene que assume que eventualmente tendremos que eliminar). Por ahora, sin embargo, trabajemos en el caso 3.

Recuerde de la Regla 7 de este artículo que el caso 3 es cuando agregamos un nuevo rango (rojo) que está completamente cubierto por un rango existente (el rango azul “antes”), por lo que el código no necesita hacer nada.

Entonces, pensando lógicamente, ¿qué sabemos? Sabemos que los números enteros cubiertos por el rango anterior son un superconjunto de los números enteros cubiertos por el nuevo rango. También sabemos que el rango anterior es parte de nuestra lista original de rangos ordenados y separados (los rangos azules). Agregaremos estas dos sugerencias a nuestro código a través de assert declaraciones:

Dafny está de acuerdo en que estas dos sugerencias son ciertas (marcas de verificación verdes), pero todavía no acepta las assert de interés (marca roja).

Parece que necesitamos una pista más. Específicamente, necesitamos convencer a Dafny de que los números enteros cubiertos por el rango anterior son un subconjunto de los números enteros cubiertos por la lista de todos los rangos ordenados y disjuntos. Intuitivamente, esto es cierto porque el rango anterior es uno de los rangos de la lista.

Escribimos esta pista como un lema sin cuerpo. Dafny lo acepta.

Aparte: ¿Por qué Dafny acepta este lema sin nada en su cuerpo? No lo sé y no tengo una buena intuición. Esto simplemente funcionó. Si no fuera así, habría intentado agregar afirmaciones a su cuerpo.

Usando el lema, el caso 3 ahora valida:

Esto significa que hemos validado los casos 0, 1, 3 y 4. A continuación pasaríamos al caso 2. Además, algunos de los métodos mencionados, por ejemplo, DeleteExtraaún no se validan y necesitaríamos trabajar en ellos. [You can see the code up to this point, here.]

Para obtener consejos generales sobre la depuración de verificación, consulte esta sección de la Guía del usuario de Dafny. Yo también recomiendo esto Respuesta de desbordamiento de pila y minitutorial del Prof. James Wilcox.

En general, la idea es dividir la tarea de validar su algoritmo en muchas tareas de validación más pequeñas. Esto me resultó más difícil que programar, pero no demasiado difícil y aun así divertido.

Terminé agregando alrededor de 200 líneas de validación a las 185 líneas de código regulares (código completo aquí). Cuando finalmente validé el último método, pensé erróneamente que había terminado.

Para mi sorpresa (y decepción) el trabajo no termina la primera vez que se valida todo. También debe asegurarse de que su proyecto se valide nuevamente y se valide para otros. Discutiremos esta regla a continuación.

Pensé que había terminado. Luego, moví la definición de seis líneas de la matemática. Min función de la Biblioteca estándar de Dafny a mi código. Esto provocó que mi validación fallara, sin ningún motivo lógico (¡literalmente!). Más tarde, cuando pensé que lo había solucionado, eliminé un método que no se utilizaba. Nuevamente, la validación comenzó a fallar sin ningún motivo lógico.

¿Qué está sucediendo? Dafny trabaja de forma heurística mediante una búsqueda aleatoria. Cambiar el código superficialmente (o cambiar semillas aleatorias) puede cambiar la cantidad de tiempo que necesita la búsqueda. A veces, la cantidad de tiempo cambia drásticamente. Si el nuevo tiempo supera el límite de tiempo establecido por el usuario, la validación fallará. [We’ll talk more about the time limit in tip #3, below.]

Debes probar la confiabilidad de tu validación probando diferentes semillas aleatorias. Estos son los comandos que utilicé (en Windows) para validar un archivo con 10 semillas aleatorias.

@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

El resultado es un archivo *.csv que puedes abrir como una hoja de cálculo y luego buscar fallas:

Aparte: para obtener más ideas sobre cómo medir la confiabilidad de la validación de Dafny, consulte esta respuesta de Stack Overflow sobre analizando archivos *.csv y esta discusión de GitHub Recomendando la herramienta dafny-reportgenerator..

Habiendo encontrado los puntos problemáticos, contraté al coautor Divyanshu Ranjan para que me ayudara. Divyanshu Ranjan utilizó su experiencia con Dafny para solucionar los problemas de validación del proyecto.

Aquí están sus consejos, con ejemplos del proyecto:

Consejo #1: Cuando sea posible, elimine require declaraciones que involucran “forall” y “exists”.

Recuerde de la Regla 4 que la función fantasma SeqToSet devuelve el conjunto de números enteros cubiertos por una lista ordenada y separada de rangos no vacíos. Definimos “ordenado y desunido” con función ValidSeqque utiliza internamente dos forall expresiones. Podemos eliminar el requisito de que la lista debe estar ordenada y separada, así:

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..])
}

Desde nuestro punto de vista, tenemos la misma función útil. Desde el punto de vista de Dafny, la función evita dos forall expresiones y es más fácil de aplicar.

Consejo #2 Utilice calc para evitar conjeturas por parte de Dafny.

con un dafny calc declaración, usted enumera los pasos exactos necesarios para llegar a una conclusión. Por ejemplo, aquí hay un calc desde el DeleteExtra método:

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);
}

En este punto del código, xs es una secuencia de rangos, pero no puede estar ordenada ni separada. El calc afirma que:

1. los números enteros cubiertos por las dos partes de xses igual
2. los números enteros abarcados por la concatenación de sus dos partes, es igual
3. los números enteros cubiertos por xses igual
4. rs.

Para cada paso, podemos incluir lemas o afirmaciones para ayudar a probar ese paso. Por ejemplo, esta afirmación ayuda a probar el paso del paso 3 al 4:

{ assert xs == xs[..indexAfter+1] + xs[indexAfter+1..]; }

Para mayor eficiencia y control, estos lemas y afirmaciones no serán visibles para el validador más allá de su paso. Esto mantiene a Dafny concentrado.

Consejo n.º 3: uso timeLimit para proporcionar cálculo cuando sea necesario.

Dafny deja de intentar validar un método en un momento configurable por el usuario timeLimit. Los límites de 10, 15 o 30 segundos son comunes porque, como usuarios, generalmente queremos que las validaciones que nunca sucederán fallen rápidamente. Sin embargo, si sabemos que eventualmente se realizará una validación, podemos establecer un límite de tiempo específico para el método. Por ejemplo, Divyanshu Ranjan notó que DeleteExtra normalmente se valida, pero lleva más tiempo que los otros métodos, por lo que agregó un límite de tiempo específico para el método:

method {:timeLimit 30} DeleteExtra(xs: seq<NeIntRange>, internalRange: IntRange) returns (r: seq<NeIntRange>)
// ...

Aparte: timeLimit no tiene en cuenta la diferencia de velocidad entre computadoras, así que configúrelo con un poco de generosidad.

Consejo #4: Utilice split_here para dividir un problema de validación en dos.

como el Preguntas frecuentes sobre Dafny Explique, a veces validar un conjunto de afirmaciones juntas es más rápido y, a veces, validarlas una por una es más rápido.

Utilice un assert {:split_here} true; declaración para dividir una secuencia de afirmaciones en dos partes con fines de validación. Por ejemplo, incluso con el timeLimit, DeleteExtra Se agotó el tiempo de espera hasta que Divyanshu Ranjan agregó esto:

// ...
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)..]);
// ...

Consejo #5: Mantenga los lemas pequeños. Si es necesario, la división garantiza entre lemas.

A veces los lemas intentan hacer demasiado a la vez. Considera el SetsEqualLemma. Está relacionado con la eliminación de rangos redundantes. Por ejemplo, si insertamos a en xslos rangos marcados con “X” se vuelven redundantes.

La versión original de SetsEqualLemma contenía 12 requires y 3 ensures. Divyanshu Ranjan lo dividió en dos lemas: RDoesntTouchLemma (11 requires y 2 ensures) y SetsEqualLemma (3 requires y 1 ensures). Con este cambio, el proyecto se validó de manera más confiable.