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

Доказательство обычной функции в flang не дороже тестов — оно невозможно: 20 из 20 остались недоказанными, 15 упёрлись в нехватку правил у ядра, 5 — в то, что правду о функции нечем выговорить. Тесты на тех же двадцати нашли четыре настоящие ошибки библиотеки; доказательства нашли одну — в самом ядре, и она делает слово «доказано» ненадёжным.

Что мерили

Вопрос: дешевле ли доказать функцию, чем написать на неё тесты? В проекте это число не мерили ни разу.

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

• тесты — примеры при функции, прогон flang test;
• доказательство — постусловие и теорема при ней же, прогон flang check --proof.

На каждой работе считали четыре вещи: сколько строк написано, сколько ушло времени, сколько было попыток и что получено на выходе.

Как мерили

Ядро двигают несколько веток сразу; всё ниже посчитано на этом основании и ни на чём другом.

Как отбирали двадцать.

1. Корпус — все функции flang/stdlib/*.flang (12 модулей): списки, строки, числа, записи, словари, деревья. Это ровно тот материал, о котором задан вопрос, и он не выбран под удобство: библиотека написана задолго до замера.
2. Порядок — «файл по алфавиту, внутри файла по порядку объявления». Никакой сортировки по вкусу.
3. Годные — «нет ни постусловия, ни теоремы». Годными оказались все 185 функций из 185: в flang/stdlib нет ни одного утверждения о поведении.
4. Выборка — каждая девятая (шаг = ⌊185 / 20⌋ = 9), индексы 0, 9, 18, …,
   1. Двадцать штук.

Что считалось строкой. На тестовой стороне — строки примеров. На стороне доказательства — строки написанные, а не принятые: постусловие, теорема и функции-помощники, написанные только ради того, чтобы утверждение вообще можно было выговорить. Все двадцать функций пришлось скопировать в отдельные файлы: flang/stdlib входит в корпус побайтовой неподвижной точки самоприменения, а у восьми слов доказательства не было продукции в flang/self/parser.flang. Строки копирования в замер не входят — иначе доказательство выглядело бы дороже, чем оно есть.

Что считалось временем. Машинное время работы агента с секундомером, а не время человека; в нём заметна доля ожидания инструментов. Пользоваться им можно только внутри самого замера — для сравнения двух сторон между собой.

Числа

Отношение цены: делить не на что

Цена — это плата за результат; здесь одна из двух работ результата не дала вовсе. Доказательство обошлось в 196 строк и 9,7 минуты и не закрыло ни одного утверждения из двадцати. Правильная формулировка не «в N раз дороже», а «тесты стоят 19,5 строки на функцию и работают; доказательство стоит 9,8 строки на функцию и не работает ни на одной».

Сколько ядро закрыло само: 0 из 20

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

Во всём дереве при этом 1045 высказанных утверждений, из них 407 доказаны ядром — на 24063 функций (числа подставлены из замера дерева, а не набраны). Замер их не опроверг, он показал, насколько узко место, из которого они взяты. Чтобы ядро закрыло утверждение, должны сойтись три условия сразу:

1. параметр — объявленная сумма (тип … вариант …), а не встроенный тип;
2. тело функции — разбор по этому самому параметру;
3. цель сводится к допущению одним из двух правил упрощения — а это требует, чтобы у каждого конструктора суммы поля либо отсутствовали вовсе (тогда случай закрывается вычислением примера), либо было поле типа самой суммы (тогда случай закрывается предположением индукции).

В выборке из двадцати первое условие выполняется у четырёх функций (01, 02, 04, 16), первое и второе вместе — у трёх (01, 02, 16), третье — ни у одной: у «Связи», «Звена», «Успеха» и «Ошибки» поля есть, но все они чужого типа — строки и параметры типа. Такая посылка не закрывается ничем: предположения индукции у неё нет («предполагать не о чем»), примером её тоже не закрыть («связывает имена, значений бесконечно много»). Оба отказа советуют ровно то, что запрещает другой.

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

Главная причина «ядро не берёт» — одна и та же на 13 функциях из 15, и она называется одной строкой отказа:

FLANG_PROOF_INDUCTION_TYPE: индукция теоремы «…» идёт по «элементы», а это не
объявленная сумма. Принцип индукции читается с объявления суммы — у типа без
вариантов его брать негде

Принципа индукции нет ни у одного встроенного типа: ни у списка, ни у строки, ни у числа, ни даже у признак — типа из двух значений, где всё доказывается перебором четырёх строк таблицы. Индукция есть только у типов, объявленных тип … вариант … в самой программе. А обычные функции пишут про списки, строки и числа.

Чего нельзя выразить: 5 из 20

Все четыре дыры — в языке, а не в ядре:

Отдельно и важнее: полное описание того, что функция делает, в язык влезло у четырёх из двадцати. Полностью смысл выразили 4 утверждения (05, 12, 13, 17); в 12 случаях пришлось записать что-то более слабое («длина стала на один больше», «результат не меньше нуля») — и именно это слабое ядро и не взяло; в 4 не вышло ничего (01, 02, 15, 16).

Поправка. Здесь стояло «слова требует в языке нет»: замер снимали до того, как предусловие появилось. Сегодня требует — ключевое слово, и условный договор записывается прямо (examples/rosetta/fibonacci.flang, два требует на «Фибоначчи шагом»). Довод, ради которого абзац писался, от этого не пропал, а объясняет, зачем предусловие понадобилось. Пока его не было, условие «Двоичного поиска» («требует, чтобы список был отсортирован» — прямым текстом в комментарии библиотеки) записывалось импликацией в постусловии — «Следует» от (условие) и (утверждение). Цена обхода была 11 строк на предикат «Отсортирован» и потеря смысла проверки в рантайме: импликация с ложной посылкой истинна, то есть плохой вход такое постусловие пропускает молча, а требует его отвергает.

Все двадцать, обе работы, оба исхода

¹ Формально ядро приняло здесь терм и напечатало «доказано» — но приняло по неисправному правилу (раздел «Ядро принимает ложь» ниже), поэтому в счёт доказанного случай не зачтён. Зачесть его значило бы подогнать замер.

Единственная переписка на тестовой стороне — функция 14: ожидание было моё, а поведение библиотеки правильное («равное уходит вправо и не теряется» — прямо сказано в её примерах). Это цена тестов, а не находка: тест бывает неправ, и переписывать приходится его.

Время по функциям (секунды, тесты / доказательство): 18/82, 14/22, 32/46, 20/45, 12/101, 28/19, 26/10, 19/31, 24/21, 35/15, 47/6, 13/17, 13/43, 27/28, 15/21, 26/23, 27/15, 15/10, 42/15, 16/9.

В этих числах видна кривая обучения, и она работает В ПОЛЬЗУ доказательств: первая попытка стоила 82 и 101 секунду, последние — 9 и 10, потому что ответ «ядро не возьмёт» стал виден без единого запуска. Если бы ядро брало, эта кривая была бы аргументом «дальше дешевле»; здесь она означает только, что быстро научаешься не пытаться.

Ядро принимает ложь

Шаг по примеру, стоящий НЕ внутри индукции, не проверяет замкнутость цели вовсе. Проверка есть — и в flang/proof/SPEC.md она названа «главной проверкой состоятельности этого правила», — но живёт она в ветке правила для случая варианта. Прямой шаг в эту ветку не заходит: посылки у него нет, проверка пропускается, дальше идёт прогон ОДНОГО примера и вердикт «доказано».

Улика целиком — файл собирается за минуту:

модуль «Подделка»

тотальная функция «Противоположное»
  принимает х: число
  возвращает число
  для всех х обеспечивает «результат не больше нуля» результат не больше 0
  пример «Пять»
    дано х равно 5
    ожидается -5
  0 минус х

теорема «результат не больше нуля»
  дано х: число
  утверждаем результат не больше 0
  по примеру «Пять»
  следовательно доказано

Что говорит ведомость:

постусловие «результат не больше нуля» функции «Противоположное» —
доказано: терм принят ядром, 1 шаг — утверждение обо ВСЕХ входах

Что говорит тот же интерпретатор на том же файле:

$ flang run … --function 'Противоположное' --args '{"х": -5}'
{"error":"нарушено свойство «результат не больше нуля» функции «Противоположное»"}

Ядро печатает «доказано обо ВСЕХ входах» про утверждение, для которого контрпример находится в том же файле и той же командой. Утверждение ложно, пример один и он проходит — этого хватило.

Чинится одной проверкой на том же месте: прямой шаг по примеру законен только тогда, когда у обязательства нет квантора, то есть цель замкнута. Сегодня квантор есть, а проверки нет.

Шесть доказанных утверждений корпуса проверены индукцией и в эту ветку не попадают — их вердикт от находки не меняется. Но любое новое утверждение, закрытое прямым по примеру, ничем не отличается от «мы посмотрели один пример».

Что нашла работа: четыре настоящие ошибки, и все четыре — тестами

Все четыре воспроизводятся на нетронутых файлах библиотеки, не на копиях замера.

1. «Чётное» от любого отрицательного числа отвечает «нет».

$ flang run flang/stdlib/numbers.flang --function 'Чётное' --args '{"число": -4}'
{"result":false}

Причина: -4 остаток от 2 в IEEE-754 равно -0, а равенство скаляров считает Object.is, для которого -0 и 0 — разные значения. Примеры автора стоят на 4 и 5, поэтому беда прожила в библиотеке незамеченной. Тем же корнем сломаны «Делится на» (-4 на 2 → нет) и вторая копия «Чётное» в higher-order.flang.

2. «Уникальные» оставляет в ответе два нуля — тот же Object.is: -0 не считается уже встреченным.

$ flang run flang/stdlib/lists.flang --function 'Уникальные' --args '{"элементы": [0, -0, 1]}'
{"result":[0,0,1]}

3. «Строчная буква» от пустой строки — отказ, а функция объявлена тотальной.

$ flang run flang/stdlib/strings.flang --function 'Строчная буква' --args '{"буква": ""}'
{"error":"«разделить»: разделитель не может быть пустым","code":"FLANG_BUILTIN_ARGS"}

Ведомость при этом говорит про неё «доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт». Анализ завершаемости прав по своему определению — функция действительно завершается, — но встроенная форма под ней отказывает на законном входе, и обещания «тотальная» это не видно.

4. «Строчная буква» от "AB" отдаёт "a" — молча портит вход, вместо того чтобы вернуть его как есть (как она поступает с "7" и с "Б").

Чем нашли. Все четыре — обычными примерами: отрицательное число, -0, пустая строка, две буквы. Написание постусловия помогло в двух случаях из четырёх (13 и

1. — но только потому, что рядом уже стоял пример с нужным входом: постусловие

считается на сетке примеров автора, и без примера с -4 оно молчало бы так же, как молчало в библиотеке. Само по себе постусловие не ищет входов.

Пятая находка — дыра в состоятельности ядра — сделана стороной доказательства. Это единственное, что доказательства нашли, и это находка про инструмент, а не про функцию.

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

«Ядро не берёт»: «Следует» (docs/benchmark/12-implies.flang). Тип обоих параметров — признак, значений у него ДВА, всё утверждение проверяется перебором четырёх строк таблицы:

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

Отказ: признак — не объявленная сумма. При этом ровно такое же доказательство перебором ПРОХОДИТ на «Светофоре» из flang/proof/examples/ — потому что «Светофор» объявлен в программе, а признак встроен. Это самый дешёвый из всех возможных случаев, и он не берётся.

Отдельная цена, которая всплыла на «Вписать» (03): в теореме видны только имена, введённые дано, поэтому каждый параметр функции надо перечислить заново — без строки дано новое: «Звено» ядро отвечает «имя «новое» не связано».

«На языке не выразить»: «Ключ связи» (docs/benchmark/01-link-key.flang). Функция достаёт поле из записи-суммы. Правда о ней ровно одна: «результат равен полю ключ».

тип «Связь»
  вариант «Связь» содержит ключ: строка, значение: строка

тотальная функция «Ключ связи»
  принимает связь: «Связь»
  возвращает строка
  разбор связь
    случай вариант «Связь» с ключ как имя и значение как содержимое
      то имя

Попытка 1 — результат равен связь.ключ:

FLANG_TYPE: доступ к полю «ключ» требует записи, а не «Связь»

Попытка 2 — достать поле разбором прямо в постусловии:

FLANG_PARSE: у 'разбор' нет ни одного 'случай'

разбор требует отступов, а постусловие однострочно. Двух способов достать поле суммы нет, потому что нет и одного.

Попытки 3–5 — записать хоть что-нибудь выразимое («длина ключа неотрицательна») и доказать: там отказы начинают указывать друг на друга — «по предположению» отсылает к «по примеру», «по примеру» обратно к «по предположению». Это та самая «ближайшая оставшаяся граница», честно названная в flang/proof/SPEC.md, — посылка с непрозрачными полями и без частей.

«Ядро доказало само»: ни одного в выборке. Единственная форма, в которой этот исход случается вообще, — «Высота» из flang/stdlib/numtree.flang, доказанная в flang/proof/examples/corpus-numtree.flang. Все три условия сошлись сразу: параметр — объявленная сумма «Дерево чисел» с полем своего же типа, тело — разбор по этому параметру, цель сводится правилом «неотрицательность по построению».

теорема «высота неотрицательна»
  дано дерево: «Дерево чисел»
  утверждаем результат не меньше 0
  индукция по дерево
    случай вариант «Пустое»
      то по примеру «У пустого дерева высота ноль»
    случай вариант «Развилка» с значение как зн и меньшие как м и большие как б
      то по предположению
  следовательно доказано

Цена этого успеха: 1 строка постусловия + 9 строк теоремы против 9 строк примеров — на одной удачно устроенной функции доказательство и вправду стоит примерно как тесты. В выборке из двадцати эти три условия не сошлись ни на одной.

Что удешевило бы сильнее всего

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

Почему в первой строке три работы, а не одна. Принцип индукции для списка сам по себе открывает только 2 функции из двадцати (07, 09) — те, чьё тело есть разбор по списковому параметру. Ещё 5 (03, 06, 11, 17, 18) написаны свёрткой, и им нужна развёртка свёртки на конструкторе: это законно и не новое понятие — то же универсальное свойство начальной алгебры, из которого читается сама индукция. Отсюда «до 7 из 20». Третья часть — таблица перепи́сок для встроенных форм: длина (добавить х к с) → длина с плюс 1, длина пустой список → 0, (добавить х к с) содержит х → да. Каждая переписка — теорема о встроенной форме, ровно как два нынешних правила упрощения суть теоремы о IEEE-754, и проверяться она обязана враждебной выборкой так же. Последняя из трёх закрывает функцию 03 в одиночку, вообще без индукции.

Оставшиеся 13 первой работой не открываются: у 04, 08, 10, 14, 19, 20 тело — вызов другой функции, а по свойству «…» на постусловие ДРУГОЙ функции ядро отвергает (сличение по вызову не сделано); 05, 12, 13 — не про списки вовсе; 01, 02, 15, 16 не выразимы.

Чем это ограничено

• Замер сделан на одном основании — 8203f39. На другой ветке числа будут другими, и сравнивать два замера можно, только назвав оба основания.
• У всех двадцати функций уже стояли примеры автора. Замер их убрал и писал свои с нуля — иначе тестовая работа была бы фиктивной. Но знание того, что функция уже проверена, писать примеры помогает: реальная цена тестов «с чистого листа» чуть выше измеренной.
• Утверждения слабее полного смысла функции — полных 4 из 20. Именно слабое ядро и не взяло; взяло бы оно сильное, замерить было не на чем.
• Не мерил цену сопровождения. Тесты ломаются при каждом изменении поведения; утверждение переживает переписывание тела. На двадцати функциях этого не проверить, и делать вид, что проверено, нельзя.
• Не мерил случай, на котором слой доказательства работает — функцию над объявленной суммой, у которой конструкторы либо без полей вовсе, либо с полем типа самой суммы (дерево, стопка, перечисление). Такие функции в выборку попали — три штуки (01, 02, 16), — но у всех трёх поля чужого типа, и они умерли на третьем условии. Функции «как дерево» в библиотеке есть (numtree, tree), просто каждая девятая в них не попала. Это не поблажка выборке: вопрос был про обычные функции, а обычные функции пишут про списки и строки, и именно они не берутся.
• Не мерил человеческое время. Секундомер стоял на работе агента.
• Не мерил печать в восемь целей — постусловия печатаются, и цена этого в замер не входила.

Как повторить

Раздел для тех, кто развивает язык, а не пользуется им: команды ниже — команды репозитория, а не команды языка, и запускаются из клона дерева.

export LC_ALL=C.UTF-8

# правило отбора: сколько функций в библиотеке и какие двадцать даёт шаг
# (на основании замера — 185 годных из 185, шаг 9)
node benchmarks/proof-cost/otbor.mjs

# тестовая сторона одной функции замера: 7 примеров, все зелёные
bootstrap/flang test docs/benchmark/17-member-of-set.flang

# сторона доказательства той же функции: отказ ядра
bootstrap/flang check docs/benchmark/17-member-of-set.flang --proof

# ведомость по всему дереву: высказано, доказано, функций
node flang/scripts/proof-ledger.mjs

Двадцать файлов работы лежат в docs/benchmark/, по одному на функцию. Отказы ядра приведены выше дословно; на дереве, отличном от основания замера, они будут другими.