flang 0.7.31 — Ядро доказывает записи по полям и остаток в кольце; слова u8…u64 и битовые операции; контрпример постусловия на краях типов

Ядро доказывает записи по полям и остаток в кольце; слова u8…u64 и битовые операции; контрпример постусловия на краях типов

Что появилось

• Ядро доказывает равенство записей по полям. Утверждения (запись «Пара» с а равным п.а и б равным п.б) равно п и если (п.а равно д.а) и притом (п.б равно д.б) то п равно д иначе да теперь доказаны, и независимый сверщик это подтверждает: проиграно 2 из 2 доказанных, код 0. Раньше оба оставались «не доказано», и check --proof отвечал кодом 3.
• Перестановка слагаемых доказывается и под остаток от. Для точное целое утверждение ((а плюс б) остаток от м) равно ((б плюс а) остаток от м) доказано так же, как а плюс б равно б плюс а. Раньше под остатком ядро его не брало.
• Условие на весь список переходит на хвост. Функция с требует «все положительны» для всех э из элементы: э больше 0 может звать себя от хвост в ветви случай голова и хвост. Раньше на таком вызове была ошибка FLANG_PRECONDITION_CALL.
• Целые фиксированной ширины: u8, u16, u32, u64 и знаковые i8…i64. Значение пишется u32 5, в примере — дано х равно u32 1. Переполнение — ошибка FLANG_OVERFLOW, а арифметику по модулю 2^w пишут явно: а плюс б с переполнением (на u32 4294967295 и u32 2 даёт u32 1). Литерал вне типа отвергает проверка: а плюс 300 при а: u8 — литерал 300 не помещается в u8: от 0 до 255.
• Битовые операции и сдвиги. побитовое и, побитовое или, исключающее или, побитовое не, сдвиг влево на, сдвиг вправо на, поворот влево на, поворот вправо на. Например, Σ0 из SHA-256 — (х поворот вправо на 2) исключающее или (х поворот вправо на 13) исключающее или (х поворот вправо на 22) — на u32 1 даёт u32 1074267136. У знаковых сдвиг вправо арифметический: i32 -9 сдвиг вправо на 1 — i32 -5.
• Полное произведение двух слов. а умножить на б с двойной разрядностью даёт запись с полями старшая и младшая; на ней строится длинная арифметика без 128-битного типа. На а = u64 4294967296 и б = u64 4294967296 поле старшая — u64 1.
• Завершение взаимной рекурсии по убыванию размера. Круг вызовов проходит проверку, если на каждом его обороте какой-то аргумент строго уменьшается, даже если между функциями он меняет место. Пример: «Прочитать» идёт по списку и зовёт «Прочитать в» от хвоста, а «Прочитать в» разбирает номер и зовёт «Прочитать» от его предшественника. Раньше — FLANG_NOT_TOTAL: в цикле «Прочитать» → «Прочитать в» нет аргумента, который убывает, теперь — проверено.
• Ядро раскрывает вызов на построенном варианте. «Чередовать» от (вариант «След» с прежний равным н) ядро подставляет в нужную ветвь разбор, и постусловие результат равно «Сменить» от («Чередовать» от н) доказано, в том числе для рекурсивной функции. Раньше оно держалось только на примерах.
• В flang repl есть .текст. Вставьте текст и закончите строкой .конец — оболочка сама поймёт, программа это, формула (с ∀/∃ или в LaTeX), рассуждение или категория, и проверит. На \forall a \in \mathbb{Z}, a + 1 = a ответ — утверждение «формула» опровергнуто на входе a = 0 (код 1).
• Блок история проверяет и независимый сверщик. check --proof на файле с история «потолок скидки» теперь отвечает проиграно 1 из 1 доказанных и кодом 0. Раньше — код 3: сверщик истории не читал.
• На сайте — кнопка «Попробовать в браузере» в шапке каждой страницы, она ведёт в песочницу. Формулы в песочнице набираются KaTeX, который лежит на самом сайте, поэтому они видны и там, где внешние CDN закрыты. Песочница подсвечивает рассуждения и формулы по их виду.

Что изменилось

• Свёртка сохраняет узкий тип накопителя. свёртка новые начиная с л как акк и н → акк при л: список неотрицательное — это список неотрицательное. Раньше здесь была ошибка FLANG_TYPE: «тело даёт список числа».
• Число сужается до неотрицательное проверкой. В ветви то после если (значение не меньше 0) и притом ((значение остаток от 1) равно 0) и притом (значение не больше 9007199254740991) значение уже неотрицательное, и функцию можно объявить с возвращает неотрицательное.
• Рекурсия по разности под условием. В ветви если бит не меньше уровень значение бит минус уровень — неотрицательное, и вызов «Спуск» от (бит минус уровень) и уровень при уровень не меньше 1 проходит проверку завершения. Раньше — FLANG_TYPE и FLANG_NOT_TOTAL.
• Исправлены ложные постусловия библиотеки. Новая проверка на краях типов нашла в base64, sha256 и sqlite утверждения, ложные на отрицательном или дробном входе: остаток от деления сохраняет знак делимого. Каждое теперь называет входы, на которых верно (конечное неотрицательное число, целый байт, размер страницы от 512 до 65536). Сами функции считают как раньше.
• Верхняя граница u64 сравнивается точно. Постусловие результат не больше 18446744073709550592 (это 2^64−1024) у к числу х при х: u64 больше не доказывается: наибольшее значение u64 больше. Раньше ядро сравнивало границу в двойной точности и называло такой шаг доказанным, хотя сверщики его отвергали.

Что сломалось

• Постусловие, ложное на краю типа, теперь ошибка. check пробует края типов параметров и границы из требует. Функция «Скидка» с обеспечивает «не больше пятисот» результат не больше 500 и телом если сумма больше 100000 то 501 иначе 0 раньше проходила с пометкой «проверено только на примерах» (код 3), а теперь — постусловие «не больше пятисот» функции «Скидка» нарушено на входе сумма = 2147483647 и код 1. Как починить: вход из сообщения — контрпример; сузьте вход строкой требует или исправьте постусловие.
• Известное ограничение: постусловие с «для всех … таких что» может быть отвергнуто зря. Новая проверка на краях типов не учитывает ограничение «таких что» и пробует вход вне его. Например, верное для всех н таких что н не меньше 0 обеспечивает «сдвиг неотрицателен» результат не меньше 0 у функции с телом н получает постусловие «сдвиг неотрицателен» функции «Сдвиг» нарушено на входе н = -1 и код 1. Как обойти сейчас: запишите ограничение внутри постусловия — обеспечивает «сдвиг неотрицателен» если н не меньше 0 то результат не меньше 0 иначе да; так оно доказано, и сверщик это подтверждает. Исправим в следующем выпуске.

Описание языка

Разделы DESCRIPTION.md с v0.7.30 не менялись.

---

The kernel proves records by fields and remainders in the ring; u8…u64 words and bit operations; postcondition counterexamples at the type edges

What appeared

• The kernel proves records equal by their fields. The claims (запись «Пара» с а равным п.а и б равным п.б) равно п (a record built from the fields of p is p) and если (п.а равно д.а) и притом (п.б равно д.б) то п равно д иначе да (equal fields make equal records) are now proved, and the independent checker confirms it: проиграно 2 из 2 доказанных (2 of 2 replayed), exit code 0. Before, both stayed unproved and check --proof exited with 3.
• Swapping the summands is proved under остаток от (remainder) too. For точное целое (exact integer) the claim ((а плюс б) остаток от м) равно ((б плюс а) остаток от м) is proved just like а плюс б равно б плюс а. Before, the kernel did not take it under a remainder.
• A condition on the whole list carries over to the tail. A function with требует «все положительны» для всех э из элементы: э больше 0 (requires every element to be positive) may call itself on хвост (the tail) in the случай голова и хвост branch. Before, that call was the error FLANG_PRECONDITION_CALL.
• Fixed-width integers: u8, u16, u32, u64 and signed i8…i64. A value is written u32 5, in an example дано х равно u32 1. Overflow is the error FLANG_OVERFLOW; arithmetic modulo 2^w is written out: а плюс б с переполнением (with wrap-around; on u32 4294967295 and u32 2 it gives u32 1). A literal outside the type is refused by the check: а плюс 300 with а: u8 gives литерал 300 не помещается в u8: от 0 до 255.
• Bit operations and shifts. побитовое и (and), побитовое или (or), исключающее или (xor), побитовое не (not), сдвиг влево на, сдвиг вправо на (shift left, right), поворот влево на, поворот вправо на (rotate left, right). For example, SHA-256 Σ0 — (х поворот вправо на 2) исключающее или (х поворот вправо на 13) исключающее или (х поворот вправо на 22) — gives u32 1074267136 on u32 1. A right shift of a signed word is arithmetic: i32 -9 shifted right by 1 is i32 -5.
• The full product of two words. а умножить на б с двойной разрядностью (double width) gives a record with the fields старшая (high) and младшая (low), enough for long arithmetic without a 128-bit type. For а = u64 4294967296 and б = u64 4294967296 the field старшая is u64 1.
• Mutual recursion terminates by decreasing size. A cycle of calls passes the check when on every round some argument strictly shrinks, even if it moves to another position between the functions. Example: «Прочитать» walks a list and calls «Прочитать в» on the tail, and «Прочитать в» takes a number apart and calls «Прочитать» on its predecessor. Before: FLANG_NOT_TOTAL: в цикле «Прочитать» → «Прочитать в» нет аргумента, который убывает (no decreasing argument in the cycle); now: проверено (checked).
• The kernel unfolds a call on a built variant. «Чередовать» от (вариант «След» с прежний равным н) is unfolded into the matching branch of разбор, so the postcondition результат равно «Сменить» от («Чередовать» от н) is proved, recursive functions included. Before, it rested on the examples only.
• .текст in flang repl. Paste a text and end it with a line .конец — the shell tells whether it is a program, a formula (with ∀/∃ or in LaTeX), a reasoning or a category, and checks it. For \forall a \in \mathbb{Z}, a + 1 = a the answer is утверждение «формула» опровергнуто на входе a = 0 (refuted at a = 0, exit code 1).
• The independent checker reads история (user story) blocks. check --proof on a file with история «потолок скидки» now answers проиграно 1 из 1 доказанных and exit code 0. Before: exit code 3, the checker did not read stories.
• A “Try in the browser” button in the header of every site page leads to the playground. Formulas in the playground are typeset by KaTeX served from the site itself, so they show where outside CDNs are blocked. The playground colours reasonings and formulas by their kind.

What changed

• A fold keeps the narrow type of its accumulator. свёртка новые начиная с л как акк и н → акк with л: список неотрицательное is a список неотрицательное (list of non-negative). Before, it was the error FLANG_TYPE: the body gives a list of numbers.
• A number narrows to неотрицательное (non-negative) by a check. In the то branch after если (значение не меньше 0) и притом ((значение остаток от 1) равно 0) и притом (значение не больше 9007199254740991) the value is already non-negative, and the function may be declared возвращает неотрицательное.
• Recursion on a difference under a condition. In the branch если бит не меньше уровень (bit is at least level) the value бит минус уровень is non-negative, and the call «Спуск» от (бит минус уровень) и уровень with уровень не меньше 1 passes the termination check. Before: FLANG_TYPE and FLANG_NOT_TOTAL.
• False library postconditions are fixed. The new check at the type edges found claims in base64, sha256 and sqlite that were false on a negative or fractional input: the remainder keeps the sign of the dividend. Each claim now names the inputs it holds for (a finite non-negative number, a whole byte, a page size from 512 to 65536). The functions compute what they did before.
• The upper bound of u64 is compared exactly. The postcondition результат не больше 18446744073709550592 (2^64−1024) of к числу х with х: u64 is no longer proved: the largest u64 is bigger. Before, the kernel compared the bound in double precision and called that step proved, though the checkers refused it.

What broke

• A postcondition false at a type edge is now an error. check tries the edges of the parameter types and the bounds from требует (requires). The function «Скидка» with обеспечивает «не больше пятисот» результат не больше 500 (ensures the result is at most 500) and the body если сумма больше 100000 то 501 иначе 0 used to pass as “checked on examples only” (exit code 3); now it is постусловие «не больше пятисот» функции «Скидка» нарушено на входе сумма = 2147483647 (violated at сумма = 2147483647) and exit code 1. How to fix: the input in the message is a counterexample; narrow the input with a требует line or fix the postcondition.
• Known limitation: a postcondition with “for all … such that” may be refused by mistake. The new check at the type edges ignores the “such that” restriction and tries an input outside it. For example, the correct для всех н таких что н не меньше 0 обеспечивает «сдвиг неотрицателен» результат не меньше 0 (for all n such that n ≥ 0, the result is ≥ 0) of a function whose body is н gets постусловие «сдвиг неотрицателен» функции «Сдвиг» нарушено на входе н = -1 (violated at n = -1) and exit code 1. Workaround for now: put the restriction inside the postcondition — обеспечивает «сдвиг неотрицателен» если н не меньше 0 то результат не меньше 0 иначе да (if n ≥ 0 then the result is ≥ 0, else true); this form is proved, and the checker confirms it. The fix comes in the next release.

---

Страница выпусков: по-русски · in English.

Архив flang-0.7.31-c.tar.gz — исходники C99 и Makefile: make && sudo make install, Node не нужен. Или brew install digitable-lol/tap/flang.