Замер цены доказательства, второй раз: те же двадцать функций, обе работы

Вопрос тот же, что и в первый раз: дешевле ли доказать функцию, чем написать на неё тесты? Первый замер (docs/benchmark-proof-cost.md, 15 августа) дал 0 из 20 и честно сказал, что делить не на что. Здесь то же самое измерено заново, на том же материале, чтобы было видно движение.

Движение есть, и оно не там, где его ждали.

Основание — без него числа не сравнить

Ветки work/indukciya-vstroennyh и work/zamknutaya-cel в main НЕ влиты, и я их не вливал. Мерил на голом main. Это сказано первой строкой нарочно: их собственные отчёты обещают другое число, и складывать одно с другим нельзя.

Что из обещанного реально стоит на основании — снято прогоном, а не пересказом:

Ведомость всего дерева на этом основании (node flang/scripts/proof-ledger.mjs): высказано 1045 утверждений, доказано ядром 407; сетка 556; отвергнуто 0; законов на веру 0.

Числа эти сверяются с деревом сторожем (./ярлык подсчёты:проверка), поэтому здесь стоит СЕГОДНЯШНЯЯ ведомость, а не снимок дня замера. На день замера было 142 / 115; четыре утверждения прибавила ветка work/claims-core — три потолка римской цифры и потолок разности натуральных, — и ядра эта прибавка не касается ни строкой. Выборка двадцати функций ниже от неё не сдвинулась: ни одна из четырёх в неё не входит.

Про выборку: те же двадцать, и почему правило отбора больше не годится

Взяты те же двадцать функций, что и в прошлый раз, по именам. Так велит смысл работы: замер — линейка, а не поиск удобного материала.

Правило прошлого отбора («все функции flang/stdlib, порядок «файл, объявление», каждая девятая») сегодня даёт другой набор, и вот почему:

• функций в flang/stdlib стало 208, было 185; появился тринадцатый файл strlists.flang;
• у семи функций теперь есть постусловие (было ноль), значит фильтр «нет ни постусловия, ни теоремы» оставляет 201, а не все;
• шаг ⌊201 / 20⌋ = 10, а был 9.

Оба списка привожу целиком, чтобы никто не считал их заново.

Проверено прогоном (LC_ALL=C.UTF-8 node benchmarks/proof-cost/otbor.mjs), что старая двадцатка воспроизводима и сегодня: в порядке «файл, объявление» их номера по-прежнему 0, 9, 18, …, 171 — то есть первые 172 позиции библиотеки не сдвинулись, а 23 новые функции приписаны позже. Та же команда печатает и правый столбец таблицы выше.

Одна оговорка против нас. У функции 13 («Чётное») в библиотеке за это время появилось постусловие автора. Я его убрал — ровно как убраны примеры автора, — и написал своё. По правилу отбора она сегодня в выборку бы не попала.

Тела и зависимости перенесены из библиотеки машиной (benchmarks/proof-cost/vydelit.mjs), примеры автора убраны. Копирование в измеренные строки не входит, как и в прошлый раз.

Ответы на четыре вопроса — сразу

1. Отношение цены: доказательство против тестов

Отношение цены за полученный результат — то, ради чего замер и делается:

Это по-прежнему хуже мирового ориентира (5–20×) по времени и лучше него по строкам. Но главное число не здесь, а в следующем абзаце, и оно новое.

Там, где ядро берёт, доказательство стоит одну строку.

(У 13 в файле лежат ещё 4 строки отвергнутой пробы — ею проверялось, жива ли дыра дано число: число прошлого замера. Жива. К доказательству она не нужна.)

Теорема в обоих случаях не понадобилась вовсе: постусловие свелось с телом функции. То же самое даром закрылось ещё у четырёх функций (01, 02, 05, 07) — там, правда, утверждение пришлось ослабить, об этом ниже.

Отсюда вывод, который не был виден в прошлый раз: цена доказательства в flang больше не проблема. Проблема — охват. Когда ядро берёт цель, доказательство дешевле тестов примерно в двадцать раз. Берёт оно 2 случая из 20.

2. Сколько из двадцати ядро закрыло само

2 из 20 — если считать утверждения, которые что-то говорят о функции («размер неотрицателен», «чётность есть делимость на два»).

6 из 20 — если считать всё, что ядро закрыло без теоремы, включая ослабленное и тавтологичное.

Разницу расписываю поимённо, чтобы её нельзя было потерять:

Пятую строку стоит прочитать вслух: ядро закрывает тавтологию бесплатно. результат равен (0 минус х) при теле 0 минус х сводится правилом тождества за один шаг. Содержательное утверждение о той же функции — (результат плюс х) равен 0 — ядро не взяло. То есть цифру «закрыто без теоремы» можно надуть до любого размера, просто переписав тело в постусловие, и ведомость напечатает «доказано обо ВСЕХ входах». Это не обвинение ядру — оно право, — а предупреждение о том, как эту метрику нельзя мерить.

Теорем написано 14, принято ядром 0. Ни одна теорема за весь замер не прошла. Всё, что доказано, доказано БЕЗ теоремы.

3. Что мешает чаще всего

Восемнадцать исходов «не вышло» разложены по названной причине отказа:

Главная помеха — форма тела, и у неё есть измеренный знаменатель. Ядро строит заключение посылки индукции только с ветвей разбор по переменной индукции. Таких тел в flang/stdlib 58 из 208 (benchmarks/proof-cost/tela.mjs). Остальные 150 написаны свёрткой (45), условием (37), арифметикой (21), вызовом (18), встроенной формой (9), пусть (8), отображением и отбором (8), построением (3), применением (1).

То есть 72 % библиотеки написано формами, к которым индукция ядра не цепляется — и это ровно то, что видно на выборке: 7 отказов из 18. Индукция по встроенному списку появилась и работает, но она требует, чтобы автор написал функцию разбором. Обычный код пишут свёрткой.

Невыразимость: 4 случая из 20, и все четыре — дыры языка, а не ядра.

Пятая дыра прошлого замера — дано число: число не вводит переменную — осталась открытой (проверено пробой), но из счёта ушла: функции 13 теорема больше не нужна, ядро закрывает её постусловие само.

4. Как изменилось против прошлого замера

По цене:

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

Чего доказательства не нашли, и это важнее всех цифр

Тесты нашли четыре настоящие ошибки. Все четыре — те же, что нашёл первый замер, и ни одна не починена.

1. «Чётное» от −4 отвечает «нет» (-4 остаток от 2 = -0, а равенство скаляров считает Object.is);
2. «Уникальные» от [0, -0, 1] оставляет два нуля — тот же корень;
3. «Строчная буква» от пустой строки отказывает, а функция объявлена тотальной;
4. «Строчная буква» от "AB" молча портит вход в "a".

Новых ошибок тесты не нашли — потому что материал тот же и за сутки его не трогали. Так что вклад тестовой стороны за этот день по-новому знанию ноль, и называть его находкой было бы приписыванием.

Доказательства не нашли ни одной ошибки — ни новой, ни старой.

И вот случай, ради которого стоит писать этот раздел. Функция 13 «Чётное» — одна из двух, где доказательство сработало. Ведомость печатает:

постусловие «чётность есть делимость на два» функции «Чётное» —
доказано сведением цели с телом функции: правило «тождество после переписки
допущением» … утверждение обо ВСЕХ входах, а не о написанных

И та же функция на том же дереве отвечает нет на −4, что видно первым же примером. Противоречия нет: ядро право. «Чётное» и «Делится на» ошибаются ОДИНАКОВО, и «доказано» здесь означает ровно «две ошибки согласованы обо всех входах» — не больше. Это ровно тот пункт, который в передаче записан седьмым в списке запретов: «доказано» не равно «правильно», доказательство говорит только о соответствии спецификации, а не о том, выражает ли спецификация намерение. Здесь это не рассуждение, а наблюдение на живой функции.

Как это выглядит на глаз: по одному примеру на каждый исход

Исход «ядро закрыло само» — цена одна строка

docs/benchmark2/04-dictionary-size.flang:

тотальная функция «Размер словаря»
  принимает словарь: «Узел хеша»
  возвращает число
  для всех словарь обеспечивает «размер неотрицателен» результат не меньше 0
  … 6 примеров, 18 строк …
  длина («Звенья словаря» от словарь)

Ведомость:

постусловие «размер неотрицателен» функции «Размер словаря» — доказано сведением
цели с телом функции: правило «неотрицательность по построению», объявленные типы
аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных;
теоремы при нём нет и не нужно

Ядро подставило тело на место результат, увидело встроенную длина, у которой объявленный тип результата — нат, и закрыло цель. Ни теоремы, ни индукции, ни единого шага. Цена: 1 строка против 18 строк примеров.

Исход «ядро не берёт» — правда высказана, правил не хватает

docs/benchmark2/17-member-of-set.flang, утверждение ПОЛНОЕ — оно исчерпывает смысл функции:

  для всех множество обеспечивает «это и есть вхождение» результат равен (множество содержит искомое)
  …
  свёртка множество начиная с нет как найдено и эл → если эл равно искомое то да иначе найдено

теорема «это и есть вхождение»
  дано множество: список строки
  дано искомое: строка
  утверждаем результат равен (множество содержит искомое)
  индукция по множество
    случай пусто
      то по примеру «В пустом множестве нет ничего»
    случай голова и хвост
      то по предположению
  следовательно доказано

Отказ — и он не тот, что был в прошлый раз:

тело функции «Есть в множестве» не разбирает «множество» на верхнем уровне,
поэтому заключение посылки индукции построить не из чего: ядро берёт «результат»
случая с ветви `разбор` по той же переменной, а не угадывает его

Год назад — точнее, сутки назад — здесь стояло «а это не объявленная сумма». Принцип индукции у списка теперь есть. Упирается всё на шаг дальше: у свёртки нет ветвей, с которых читается заключение посылки. Разница существенная: раньше не хватало ПРИНЦИПА, теперь не хватает СПОСОБА ПРИЦЕПИТЬ его к телу.

Исход «на языке не выразить» — правду нечем записать

docs/benchmark2/16-success.flang. Смысл функции: «да ровно тогда, когда итог — вариант «Успех»». Попытка записать это выражением:

FLANG_PARSE: ожидался знак ')'

Проверки варианта выражением у языка нет вовсе — вариант различает только разбор, а он в постусловие не помещается: постусловие однострочное, у разбор обязателен блок с отступом. Записать можно было бы только тавтологию результат равен («Успешно» от итог), которая не утверждает ничего.

Что удешевило бы сильнее всего — по измеренной отдаче

По убыванию, с числом функций из двадцати, которые это открывает.

Первая строка стоит первой не по вкусу, а по счёту: свёрток в библиотеке 45 из 208, разборов — 58. Пока индукция цепляется только за вторые, доказуема меньшая половина библиотеки, и никакое расширение списка правил этого не меняет.

Про требует: слово появилось, цена измерена, отдача пока ноль

Прошлый замер писал условие импликацией в постусловии и платил 11 строк за предикат. Теперь есть требует, и на функции 10 («Двоичный поиск») это выглядит так:

  требует «список отсортирован» «Отсортирован» от элементы

Слово работает: типы проходят, отказ ядра прямо говорит «известно: предусловие функции «Двоичный поиск»» — то есть предусловие действительно приезжает в доказательство фактом. Цена — 15 строк предиката «Отсортирован», потому что сказать «отсортирован» одним выражением по-прежнему нечем. Закрыло оно ноль целей: тело функции — вызов, посылку индукции строить не из чего, и до места, где факт пригодился бы, доказательство не доходит.

Это не довод против требует — договор стал выразимым, и это самостоятельная ценность. Это довод за то, что порядок работ важнее их числа: факт, до которого не доходит доказательство, отдачи не даёт.

Чего этот замер не мерил

• Не мерил цену сопровождения. Тесты ломаются при каждом изменении поведения, утверждение переживает переписывание тела. За два дня это не проверить.
• Не мерил человеческое время. Секундомер стоял на работе агента, и в нём заметна доля ожидания инструментов. Пользоваться этим временем можно только внутри замера, для сравнения двух сторон между собой.
• Не мерил ветки, которых нет в main. Обе названы в основании.
• Не мерил случай, на котором слой доказательства работает лучше всего — функцию над объявленной суммой с рекурсивным полем (дерево, стопка). В старую двадцатку такие не попали, и подменять выборку ради красивого числа значило бы испортить линейку.

Оговорки, работающие против доказательств, — назову сам

1. Утверждения, которые я писал, слабее полного смысла функции. Полностью смысл выразили немногие; чаще писалось «длина не больше», «результат неотрицателен». Именно слабые ядро и брало.
2. Одиннадцать из двадцати файлов не проходят flang check нарочно: отвергнутая теорема оставлена в файле уликой, а не убрана. Это не поломка дерева — файлы лежат в docs/ и в корпус (flang/**/*.flang) не входят, ведомость по корпусу их не видит.
3. У всех двадцати функций уже стояли примеры автора. Замер их убрал и писал свои, но знание того, что функция проверена, писать примеры помогает: реальная цена тестов «с чистого листа» чуть выше измеренной.
4. Тесты нашли те же четыре ошибки, что и в прошлый раз. Считать их находкой ЭТОГО дня нельзя.

Чем это проверить — четыре команды и четыре числа

LC_ALL=C.UTF-8 bash benchmarks/proof-cost/all-tests.sh

→ 110 примеров, 4 красных, и все четыре — ошибки библиотеки, а не примеров: 11 («Уникальные» на -0), 13 («Чётное» на -4), 19 два («Строчная буква» на "AB" и на пустой строке).

LC_ALL=C.UTF-8 node benchmarks/proof-cost/schitat.mjs

→ строк тестов 394, строк доказательства 169, секунд 276 / 589, попыток 20 / 41.

LC_ALL=C.UTF-8 node benchmarks/proof-cost/tela.mjs

→ тел вида «разбор по параметру» в flang/stdlib — 58 из 208.

LC_ALL=C.UTF-8 bootstrap/flang check docs/benchmark2/04-dictionary-size.flang --proof
LC_ALL=C.UTF-8 bootstrap/flang check docs/benchmark2/13-even.flang --proof

→ два «доказано … теоремы при нём нет и не нужно». Это и есть 2 из 20.

Вывод одним абзацем

Год назад — сутки назад — доказательство обычной функции в flang было невозможно: 20 из 20 не закрылись, и тринадцать упирались в отсутствие принципа индукции у встроенных типов. Принцип появился (список, отрезок нат), шесть дыр состоятельности закрыты, требует заведено — и число сдвинулось с нуля до двух из двадцати, причём оба доказательства обошлись в одну строку и ни одной теоремы, то есть в восемнадцать раз дешевле тестов на тех же функциях. Теорем при этом написано двенадцать и принято ноль: всё, что доказано, доказано без теоремы вовсе. Узкое место переехало и называется теперь точно: ядро цепляет индукцию только к телу-разбору, а 72 % библиотеки написано свёрткой, условием и вызовом. Тесты за то же время дали 20 работающих наборов из 20 и показали четыре старые ошибки, ни одна из которых не починена; доказательства не показали ни одной — и на функции «Чётное» напечатали «доказано обо ВСЕХ входах» про утверждение, истинное ровно потому, что две функции ошибаются одинаково. Отношение цены за результат сегодня 4,3 раза по строкам и 21 раз по времени не в пользу доказательств; отношение цены за результат ТАМ, ГДЕ ЯДРО БЕРЁТ, — в 18 раз в пользу доказательств. Дальше двигать надо не цену, а охват.