Девять правил формальной проверки алгоритмов Rust с использованием Dafny (Часть 2)

Девять правил формальной проверки алгоритмов на Rust с использованием Dafny (Часть 2)

Уроки, полученные при проверке крейта range-set-blaze

Карл М. Кэди и Дивьяншу Ранжан

Это часть 2 статьи, формально проверяющей алгоритм Rust с использованием Dafny. Мы рассматриваем правила с 7 по 9:

• 7. Перенесите свой реальный алгоритм в Dafny.
• 8. Проверьте версию вашего алгоритма в Dafny.
• 9. Переработайте вашу проверку для надежности.

См. часть 1 для правил с 1 по 6:

• CountVectorizer для извлечения признаков из текстов на Python, подробно
• 5 идей, как содействовать участию дата-ученых/аналитиков, не утопив их во встречах
• «О, ты имел в виду управлять изменениями?»

1. Не изучайте Dafny.
2. Изучите Dafny.
3. Определите основные концепции вашего алгоритма.
4. Опишите ваш алгоритм.
5. Получите помощь от сообщества Dafny.
6. Проверьте другой более простой алгоритм.

Эти правила основаны на нашем опыте проверки алгоритма из крейта range-set-blaze, который работает с “сгруппированными” целыми числами в Rust.

Напомню, что правило 6 из части 1 показывает, что мы можем проверить алгоритм для функции InternalAdd, но это не функция, используемая в Rust крейте. Следующим шагом мы обратимся к этой функции.

Правило 7: Перенесите свой реальный алгоритм в Dafny.

Вот интересная функция на Rust с опущенным некоторым кодом:

// 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-btreemapfn 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;    }    //... код продолжается ...}

А вот начало порта на 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;  } //... код продолжается ...}

Некоторые интересные моменты:

• Код на Rust использует self и объектно-ориентированный стиль инкапсуляции. Dafny поддерживает такой стиль написания кода, но для простоты я не использую его здесь. Конкретно, код на Rust изменяет self. Я решил написать код на Dafny более функционально – он принимает неизменяемую последовательность и возвращает новую неизменяемую последовательность.
• Код на Rust управляет памятью с помощью borrow checker. Это приводит к таким выражениям, как range.clone(). Dafny управляет памятью сборщиком мусора. В любом случае, безопасность памяти будет обеспечена. Поэтому мы игнорируем это при проверке.
• Код на Rust обобщенный по типу T, который я в другом месте определяю включающим все стандартные целочисленные типы Rust, например, u8, isize, i128. Код на Dafny определен для типа int, который представляет целые числа произвольного размера. Это означает, что этот порт на Dafny не нужно проверять на переполнение целых чисел. [См. статью предыдущую статью для формального доказательства безопасности от переполнения с помощью верификатора Rust Kani.]
• Код на Rust включает условие выполнения assert!, которое необходимо в Rust для запрета одного особого случая: вставка u128::max_value в RangeSetBlaze<u128>. Поскольку Dafny использует произвольно большой int, он игнорирует этот особый случай.

Уточнение: Какова длина включающего диапазона Rust 0..=u128::max_value? Ответ – u128::max_value+1, значение, слишком большое, чтобы представить его с помощью любого стандартного целого типа Rust. Крейт range-set-blaze ограничивает диапазоны до 0..=u128::max_value-1, чтобы длины можно было представить с помощью u128.

Далее рассмотрим остальную часть алгоритма internal_add. Напомним, у нас есть список отсортированных не пересекающихся диапазонов и непустой новый диапазон, который мы хотим вставить. Например

Алгоритм позволяет нам найти тот (если такой есть) существующий диапазон, который находится перед (или в) началом нового диапазона. Назовем его «предыдущим» диапазоном. Затем мы рассматриваем четыре случая:

• Случай 1: Новый диапазон не соприкасается со своим предыдущим диапазоном, поэтому мы вставляем новый диапазон, проверяя, соприкасается ли он с какими-либо другими диапазонами.
• Случай 2: Новый диапазон касается предыдущего диапазона и выходит за его пределы, поэтому мы расширяем конец предыдущего диапазона, проверяя, соприкасается ли он с какими-либо другими диапазонами. (Когда другие диапазоны не касаются, это будет очень быстро.)

• Случай 3: Новый диапазон касается предыдущего диапазона, но не выходит за его пределы, поэтому ничего не делаем. (Это всегда будет очень, очень быстро.)

• Случай 4: Новый диапазон начинается перед всеми диапазонами, поэтому мы добавляем его, проверяя, соприкасается ли он с какими-либо другими диапазонами.

Вот алгоритм на Rust:

// продолжение кода ...// БУДУЩЕЕ: было бы хорошо, если бы у BTreeMap была функция partition_point, которая возвращает два итератора    let mut before = self.btree_map.range_mut(..=start).rev();    if let Some((start_before, end_before)) = before.next() {        // Необходимо проверить это в двух частях, чтобы избежать переполнения        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 {            // полностью содержится, поэтому ничего не делаем        }    } else {        self.internal_add2(&range);    }}

А вот он на Dafny:

// продолжение кода ...  var beforeHi := IndexAtOrBeforePlusOne(xs, start);  if beforeHi > 0 { // не добавляется в начало    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 // добавляется в начало  {    r := InternalAdd2(xs, range);  }}

Некоторые интересные моменты:

• Код Rust работает с BTreeMap по ключам и значениям. Код Dafny работает с отсортированным seq через (произвольный доступ) индексы. В коде Dafny я сделал операции зеркальными операциям Rust, хотя это делает код Dafny менее естественным.
• Код Rust также обновляет self.len, количество отдельных целых чисел в RangeSetBlaze. Код Dafny игнорирует это. (Обновление len – это возможность, которую можно добавить в код Dafny в будущем.)
• Как и раньше, версия Rust включает код для избегания переполнения, который Dafny игнорирует.

Я продолжил портирование, написав версию Dafny для функций internal_add2 и delete_extra, которые вызывает internal_add. Я закончил портирование, написав методы, на которые ссылается эти два метода, и т.д. Полный портированный код состоит примерно из 185 строк. Вы можете его посмотреть здесь.

Он не проходит валидацию. Мы будем работать над валидацией дальше.

Правило 8: Проверьте версию вашего алгоритма на Dafny.

В этом шаге вы добавите подсказки для валидации в свой код, например, в виде операторов assert. Dafny использует эти подсказки для попытки валидации вашего кода. Как новичок в Dafny, я (Карл) обнаружил, что добавление подсказок сложнее, чем кодирование. В частности, потому что я не знал, когда (или если) Dafny будет удовлетворен и я смогу остановиться.

Однако я узнал, как я должен начать. Например, код выше для InternalAdd вызывает две ошибки проверки. Во-первых, проверяющий Dafny сообщает, что одно из ensures может не выполняться:

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

Примечание: “Постусловие” соответствует ensures. “Предусловие” соответствует requires.

Во-вторых, проверяющий Dafny жалуется, что предусловие (одно из requires) для DeleteExtra не может быть доказано.

Сначала мы сфокусируемся на первой проблеме, добавив assert в самый конец метода. Мы напишем его, чтобы он отражал ensures.

// ... добавление этого в качестве последней строки в InternalAdd
assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range);}

Временно мы проигнорируем проблему DeleteExtra с помощью оператора assume.

// ... примем, что существует i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]);
r := DeleteExtra(r, (startBefore,end));//...

Теперь проверяющий Dafny жалуется только на наш новый итоговый assert. Он говорит “assertion might not hold.”

Напомним, что код InternalAdd использует вложенные условные операторы if, чтобы разделить работу на пять случаев. Далее мы переместим наш assert из конца метода в конец каждого случая. Ищите строки, заканчивающиеся комментарием // case в результате:

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 - валидируется    return;  }  var beforeHi := IndexAtOrBeforePlusOne(xs, start);  if beforeHi > 0 { // не идет в начале    var (startBefore, endBefore) := xs[beforeHi-1];    if endBefore+1 < start {      r := InternalAdd2(xs, range);      assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 1 - валидируется    } 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 - не валидируется    } else{      r := xs;      assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 3 - не валидируется    }  }  else // идет в начале  {    r := InternalAdd2(xs, range);    assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 4 - валидируется  }}

Дафни теперь говорит нам, что случаи 0, 1 и 4 прошли проверку. Случай 2 не проходит (и содержит это assume, которое мы в конечном итоге должны удалить). Но пока давайте поработаем над случаем 3.

Напомним из правила 7 этой статьи, что случай 3 возникает, когда мы добавляем новый диапазон (красный), который полностью перекрыт существующим диапазоном (синий “ранее”), поэтому код не требуется.

Итак, логически рассуждая, что мы знаем? Мы знаем, что целые числа, покрываемые диапазоном “ранее”, являются надмножеством целых чисел, покрываемых новым диапазоном. Мы также знаем, что диапазон “ранее” является частью нашего исходного отсортированного и непересекающегося списка диапазонов (синие диапазоны). Мы добавим эти два намека к нашему коду с помощью утверждений assert:

Дафни соглашается, что эти два намека верны (зеленые галочки), но она все равно не принимает интересующее нас assert (красная метка).

Похоже, нам нужен еще один намек. Конкретно, нам нужно убедить Дафни, что целые числа, покрываемые диапазоном “ранее”, являются подмножеством всех целых чисел, покрываемых списком всех отсортированных и непересекающихся диапазонов. Интуитивно это верно, потому что диапазон “ранее” — это один из диапазонов в списке.

Мы записываем этот намек в виде леммы без тела. Дафни принимает его.

Кстати: почему Дафни принимает эту лемму без чего-либо в теле? Я не знаю и у меня нет хорошего интуитивного понимания. Это просто сработало. Если бы не сработало, я бы попробовал добавить утверждения в тело.

Используя лемму, случай 3 теперь проходит проверку:

Это означает, что мы проверили случаи 0, 1, 3 и 4. Затем мы перейдем к случаю 2. Кроме того, некоторые из упомянутых методов, например, DeleteExtra, еще не прошли проверку, и нам нужно будет поработать над ними. [Вы можете увидеть код до этого момента здесь.]

Для общих советов по отладке проверки см. этот раздел руководства пользователя Dafny. Я также рекомендую этот ответ на Stack Overflow и мини-учебник, написанный проф. Джеймсом Уилкоксом.

В целом идея заключается в разделении задачи проверки вашего алгоритма на множество меньших проверочных задач. Мне было это сложнее, чем программирование, но не слишком сложно и всё же весело.

Я добавил около 200 строк проверки к 185 строкам основного кода (полный код здесь). Когда я наконец проверил последний метод, я ошибочно подумал, что закончил.

К моему удивлению (и разочарованию), работа не заканчивается с первой успешной проверкой. Вы также должны убедиться, что ваш проект будет успешно проверяться снова и проверяться другими. Мы расскажем об этом правиле далее.

Правило 9: Переработайте вашу проверку для надежности.

Я подумал, что я закончил. Затем я переместил шестилинейное определение функции математического Min из стандартной библиотеки Dafny в свой код. Это вызвало сбой моей проверки без логической причины (буквально!). Позже, после того, как я думал, что исправил это, я удалил метод, который не использовался. И снова проверка начала сбоить без логической причины.

Что происходит? Dafny работает эвристически с помощью случайного поиска. Изменение кода поверхностно (или изменение случайных семян) может изменить время, которое необходимо для поиска. Иногда, количество времени изменяется кардинально. Если новое время превышает установленный пользователем лимит времени, проверка не будет выполнена. [О временном лимите мы поговорим подробнее в совете #3, ниже.]

Вы должны проверить надежность вашей проверки, попробовав разные случайные семена. Вот команды, которые я использовал (на Windows), чтобы проверить файл с 10 случайными семенами.

@rem Найдите расположение Dafny и добавьте его в ваш путь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

Результатом является файл *.csv, который вы можете открыть как электронную таблицу и затем искать неудачи:

Кстати: Для большего количества идей по измерению надежности проверки Dafny см. этот ответ на Stack Overflow о анализе файлов *.csv и эту дискуссию на GitHub с рекомендацией инструмента dafny-reportgenerator.

Обнаружив проблемные места, я пригласил соавтора Дивяншу Ранжана, чтобы помочь. Дивяншу Ранжан использовал свой опыт работы с Dafny для исправления проблем с проверкой проекта.

Вот его советы с примерами из проекта:

Совет #1: При возможности убирайте операторы require, связанные с “forall” и “exists”.

Помните из Правила 4, что призрачная функция SeqToSet возвращает множество целых чисел, покрытых упорядоченным и не перекрывающимся списком непустых диапазонов. Мы определяем “упорядоченный и не перекрывающийся” с помощью функции ValidSeq, которая внутренне использует два оператора forall. Мы можем удалить требование, что список должен быть упорядоченным и не перекрывающимся, следующим образом:

призрачная функция SeqToSet(sequence: seq<NeIntRange>): set<int>  decreases |sequence|  // удалено: requires ValidSeq(sequence){  if |sequence| == 0 then {}  else if |sequence| == 1 then RangeToSet(sequence[0])  else RangeToSet(sequence[0]) + SeqToSet(sequence[1..])}

С нашей точки зрения, у нас есть такая же полезная функция. С точки зрения Dafny, функция избегает двух операторов forall и проще в применении.

Совет #2: Используйте оператор calc, чтобы избежать догадок со стороны Dafny.

С использованием оператора calc в Dafny вы перечисляете точные шаги, необходимые для получения какого-либо вывода. Например, вот calc из метода DeleteExtra:

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

На этом этапе кода xs – это последовательность диапазонов, но она может быть не упорядоченной и не перекрывающейся. Оператор calc утверждает, что:

1. Целые числа, охватываемые двумя частями xs, равны
2. Целые числа, охватываемые конкатенацией двух ее частей, равны
3. Целые числа, охватываемые xs, равны
4. rs.

Для каждого шага нам разрешено использовать леммы или проверки, чтобы помочь доказать этот шаг. Например, эта проверка помогает доказать переход от шага 3 к 4:

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

Для повышения эффективности и контроля эти леммы и проверки не будут видны валидатору за пределами своего шага. Это позволяет Dafny оставаться сосредоточенным.

Совет №3: Используйте timeLimit, чтобы предоставить вычисление там, где это необходимо.

Dafny прекращает попытки проверить метод после достижения установленного пользователем timeLimit. Ограничения в 10, 15 или 30 секунд обычны, потому что, как пользователи, мы, как правило, хотим, чтобы невозможные проверки быстро завершались неудачей. Однако, если мы знаем, что проверка произойдет рано или поздно, мы можем установить метод-специфический лимит времени. Например, Дивьяншу Ранджан заметил, что DeleteExtra обычно выполняется успешно, но занимает больше времени, чем другие методы, поэтому он добавил метод-специфический лимит времени:

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

Примечание: timeLimit не учитывает разницу в скорости между компьютерами, поэтому установите его немного щедро.

Совет №4: Используйте split_here, чтобы разделить задачу валидации на две части.

Как объясняют Dafny FAQs, иногда проверка набора проверок вместе происходит быстрее, а иногда быстрее происходит проверка поочередно.

Используйте оператор assert {:split_here} true; для разделения последовательности проверок на две части. Например, даже с использованием timeLimit, DeleteExtra работает слишком долго, пока Дивьяншу Ранджан не добавил это:

// ...else  {    r := (s[..i] + [pair]) + s[i..];    assert r[..(i+1)] == s[..i] + [pair];    assert r[(i+1)..] == s[i..];    assert {:split_here} true; // разделить валидацию на две части    calc {      SeqToSet(r[..(i+1)]) + SeqToSet(r[(i+1)..]);// ...

Совет №5: Содержите леммы маленькими. При необходимости выполняйте разделение проверок между леммами.

Иногда леммы пытаются делать слишком много одновременно. Рассмотрим SetsEqualLemma. Она связана с удалением избыточных диапазонов. Например, если мы вставляем a в xs, диапазоны, помеченные “X”, становятся избыточными.

В исходной версии SetsEqualLemma было 12 requires и 3 ensures. Дивьяншу Ранджан разделил ее на две леммы: RDoesntTouchLemma (11 requires и 2 ensures) и SetsEqualLemma (3 requires и 1 ensures). С этим изменением проект валидируется более надежно.

Применение этих советов улучшит надежность нашего доказательства. Можем ли мы сделать валидацию 100% надежной? К сожалению, нет. Всегда существует вероятность, что при неудачной выборке Dafny не сможет пройти проверку. Так вот, когда вы прекращаете попытки улучшить проверку?

В рамках этого проекта Дивьяншу Ранжан и я улучшили код проверки, пока вероятность ошибки валидации на каждом запуске не снизилась до 33%. Таким образом, на основе 10 случайных запусков у нас было не более 2-3 ошибок. Мы даже пробовали 100 случайных запусков, и в результате получили 30 ошибок.

Заключение

Вот и все: девять правил, которые подтверждают корректность алгоритма на Rust с использованием Dafny. Может быть, вы обескуражены тем, что процесс не настолько прост или автоматический. Однако я вижу в этом процессе возможность.

Кстати, как и во время уроков геометрии в школе, доказательства в математике всегда меня увлекали и раздражали одновременно. «Увлекает» потому, что математическая теорема, однажды доказанная, остается верной навсегда. (Геометрия Эвклида до сих пор считается верной. Физика Аристотеля — нет.) «Раздражает» потому, что мои уроки математики всегда казались мне смутными в отношении того, какие аксиомы я могу принять и насколько я могу сделать большие шаги в своем доказательстве. Dafny и подобные системы устраняют эту неопределенность с помощью автоматической проверки доказательств. Что еще лучше с моей точки зрения, они помогают нам создавать доказательства в области, которая мне очень близка: алгоритмы.

Когда стоит проводить формальное доказательство алгоритма? Учитывая объем работы, я буду делать это только в случае, если алгоритм является сложным, важным или легко доказуемым.

Как мог бы улучшиться процесс в будущем? Я бы хотел увидеть:

• Взаимодействие между системами — Геометрическая теорема, однажды доказанная, не требует повторного доказательства. Было бы замечательно, если системы, выполняющие проверку алгоритмических доказательств, могли бы использовать доказательства других систем.
• Систему на Rust, такую же простую в использовании, как Dafny — Для работы в этом направлении, см. [1,2].

Кстати, вы знаете систему проверки Rust, которая легко использовать? Пожалуйста, рассмотрите возможность применения ее для проверки internal_add. Это позволит нам сравнить удобство и мощность системы Rust с Dafny.

• Aналог ключевого файла Cargo.lock системы Rust для доказательств — В Rust мы используем Cargo.lock, чтобы закрепить комбинацию зависимостей проекта, которая точно работает. Я хотел бы, чтобы Dafny, например, обнаруживая путь для доказательства данного метода, закреплял найденные шаги доказательства. Это могло бы сделать проверку более надежной.
• Улучшенный искусственный интеллект для проверки — У меня есть предчувствие, что улучшенный ChatGPT мог бы быть хорошим в создании 90% необходимого кода проверки. По моему мнению, текущая версия ChatGPT 4 плохо работает с Dafny, вероятно, из-за отсутствия примеров обучения Dafny.
• Лучшая проверка для искусственного интеллекта — Когда искусственный интеллект генерирует код, мы сомневаемся в его правильности. Формальная проверка может помочь доказать его корректность. (Для небольшого примера этого смотрите мою статью Проверка идеального и автоматического кода, созданного ИИ.)

Благодарим вас за сопровождение нашего пути к корректности программы. Мы надеемся, что если у вас есть алгоритм, для которого вам нужно доказательство, эти шаги помогут вам найти его.

Пожалуйста, подписывайтесь на Карла на VoAGI. Я пишу о научном программировании на Rust и Python, машинном обучении и статистике. Обычно я пишу около одной статьи в месяц.

Читайте больше работ Дивьяншу Ранжана на его блоге. В дополнение к формальным методам, в блоге также касаются вопросы геометрии, статистики и многого другого.