Skip to content

flang 0.7.26 — TLS на языке, случайность у хозяина, цена до прогона, кеш ядра и второй сличитель на Lean

Choose a tag to compare

View all tags
@github-actions github-actions released this 11 Oct 13:23
· 1035 commits to main since this release
v0.7.26
83e848c

TLS на языке, случайность у хозяина, цена до прогона, кеш ядра и второй сличитель на Lean

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

  • TLS 1.3 собран на языке и работает напечатанным (ADR-0078). flang/stdlib/tls-client.flang и certificate-path.flang: рукопожатие, проверка подписи сервера RSA-PSS (все 60 векторов pss-vect.txt приняты, подделки отвергнуты), цепочка до корня, срок, basicConstraints и имя узла — живой узел www.google.com до GTS Root R1. Поручение «Запросить» по https по-прежнему исполняет curl: решение названо, не умолчано.
  • Хозяин отдаёт октеты из системного источника случайности (ADR-0077): поручение «Случайные октеты» с полем «сколько», отклик «Октеты». Главный довод ADR-0007 «секрет взять неоткуда» снят.
  • Точное целое и точное дробное печатаются во все десять целей — рантаймы каждой цели считают их сами; целая часть — встроенная одноместная форма (ADR-0074); остаток над точным целым; пробы сверяют ответ толкователя с десятью целями байт в байт.
  • Цена функции известна до прогона (ADR-0083): flang run --cost и поле cost у бегуна печатают границу шагов и памяти от размеров входа.
  • Кеш ответов ядра между прогонами в подписанном каталоге (ADR-0080); памятка одного прогона (ADR-0051) стала памятью между прогонами.
  • Второй сличитель записей — на Lean 4 (ADR-0076), сверен с сличителем на C; доказанным считается только то, что сличитель проиграл (ADR-0073); check --proof говорит, сколько проиграно.
  • Правила ядра: индукция по отрезку, уплотнение целого и перебор конечной суммы (ADR-0075: Инд5, Инд6, Цел3) и переписка цели по доказанному равенству с квантором внутри формулы (ADR-0084: Переп1, Скл1–Скл3, Св2) — каждое с леммой в Lean и ловушкой.
  • Нормальный параллелизм (ADR-0072): пул, чистое отображение и доказанный моноид; напечатанный C, Go, Java, C# и Elixir отображают и сворачивают список кусками; ядро судит законы моноида и помечает свёртки, которые режет.
  • Чужой язык входит через недоверенного переводчика (ADR-0058): циклы, присваивания, вызовы и структуры C переводятся на flang и судятся ядром.
  • Напечатанный код следует канону цели (ADR-0081): форматтер и линтер каждой из десяти целей принимают печать без правки; C и C++ раскладываются как clang-format LLVM, C# — как dotnet format.
  • DESCRIPTION.md — зеркало языка: описание называет каждое слово лексера, каждую команду flang --help и каждый ключ настроек, сторож переписи это держит, а тело выпуска перечисляет изменённые разделы описания.
  • Разбор случаев в сверщике читает больше тел и связывает атомы: допущения требует и проигранные обещания вызываемых — факты, длины считаются и делятся по половинам; пользовательская программа greeting теперь проигрывается сверщиком.

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

  • Лицензия живёт в одном файле LICENSE: строки SPDX сняты из исходников (112 файлов), сторож лицензий проверяет один корневой файл.
  • Семя перепечатано дважды партией после 0.7.26: печать своим печатником, вторая печать — неподвижная точка (compiler_flang.c 43 917 383 байта).
  • Сторож чисел сайта меряет то же, что печатает numbers:build; числа корпуса на сайте пересняты на нынешнем дереве.
  • Замок пакетов: каждая форма зависимости доходит до файла замка; разрешение реестра доказано корпусом и подлогом.
  • Сообщения check называют отчёт о доказательстве простыми словами; страница реестра печатается без внутренних слов.
  • Сторожа переписей — планы на flang, доказанные ядром, а не оболочка: перепись рукописных списков, перепись судей, перепись незваных проверок.

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

  • Запись, в которой ничего не доказано, отвечает кодом 3, а не 0 — сличитель больше не молчит на пустом.
  • Имя модуля второго сличителя и код подлога рукописных списков — английские слова; старые имена не читаются.
  • Ядро отказывает в индукции, если имя образца затеняет параметр — программы, жившие на этой дыре, перестанут доказываться.

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

Разделы DESCRIPTION.md, изменённые с v0.7.25:

  • Синтаксис
  • Типы
  • Структуры и enum
  • Строки
  • Доказательства
  • Процессы
  • Категорная запись
  • Старые слова
  • Модули и пакеты
  • Команды
  • Файл настроек
  • Ограничения

TLS in the language, host entropy, cost before the run, a kernel cache and a second checker in Lean

What appeared

  • TLS 1.3 is assembled in the language and runs printed (ADR-0078). flang/stdlib/tls-client.flang and certificate-path.flang: the handshake, the server signature RSA-PSS (all 60 vectors of pss-vect.txt accepted, forgeries refused), the chain to a root, the validity window, basicConstraints and the host name, against the live host www.google.com up to GTS Root R1. The «Запросить» order over https still goes through curl: named, not hidden.
  • The host hands out octets from the system random source (ADR-0077): the order «Случайные октеты» with a сколько field answers «Октеты». The main argument of ADR-0007, that a program has nowhere to take a secret from, is gone.
  • Exact integers and exact fractions print into all ten targets; every target runtime computes them itself; целая часть is a built-in unary form (ADR-0074); the remainder over the exact integer; probes compare the evaluator with the ten targets byte for byte.
  • The cost of a function is known before the run (ADR-0083): flang run --cost and the runner's cost field print the step and memory bound from the input sizes.
  • A proof cache remembers kernel answers across runs in a signed directory (ADR-0080); the one-run memo of ADR-0051 became memory between runs.
  • The second record checker is written in Lean 4 (ADR-0076) and crosschecked with the C checker; only what the checker replays counts as proved (ADR-0073); check --proof says how much was replayed.
  • Kernel rules: segment induction, integer tightening and enumeration of a finite sum (ADR-0075: Инд5, Инд6, Цел3) and rewriting a goal by a proved equality with a quantifier inside a formula (ADR-0084: Переп1, Скл1–Скл3, Св2), each with a Lean lemma and a trap.
  • Normal parallelism (ADR-0072): the pool, the pure map and a proved monoid; printed C, Go, Java, C# and Elixir map and fold a list in chunks; the kernel judges monoid laws and marks the folds it cuts.
  • A foreign language enters through an untrusted translator (ADR-0058): C loops, assignments, calls and structs are translated to flang and judged by the kernel.
  • Printed code follows the canon of its target (ADR-0081): the formatter and the linter of each of the ten targets accept the print without edits; C and C++ are laid out like clang-format LLVM, C# like dotnet format.
  • DESCRIPTION.md mirrors the language: it names every lexer word, every flang --help command and every settings key, a census guard keeps it so, and the release body lists the changed sections of the description.
  • The checker's case split reads more bodies and links atoms: требует hypotheses and replayed callee promises are facts, lengths are counted and split by the half; the user program greeting is now replayed by the checker.

What changed

  • The licence lives in one LICENSE file: SPDX lines left the sources (112 files), the licence guard checks one root file.
  • The seed was reprinted twice by the batch after 0.7.26: a print by its own printer and a second print that is the fixed point (compiler_flang.c 43 917 383 bytes).
  • The site number guard measures what numbers:build prints; the corpus numbers on the site were retaken on the current tree.
  • The package lock: every form of a dependency reaches the lock file; registry resolution is proved by a corpus and a forgery.
  • check messages name the proof report in plain words; the registry page is printed without internal words.
  • Census guards are flang plans proved by the kernel, not shell: the hand-written list census, the judge census, the uncalled-check census.

What broke

  • A record with nothing proved answers 3, not 0: the checker no longer stays silent on an empty record.
  • The second checker module and the hand-written-list forgery code are English words; the old names are not read.
  • The kernel refuses induction when a pattern name shadows a parameter: programs that lived on that hole stop proving.

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

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

Assets 3
Loading