Сокращатель ссылок: служба и клиент, оба на flang

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

• Служба — docs/examples/web/shortener/: вход — байты, которые хозяин прочитал из соединения; выход — байты, которые хозяин пошлёт обратно. Между ними нет ни одной строки, написанной не на flang.
• Клиент — docs/examples/web/shortener-client/: форма, отправка, список ссылок, счётчик переходов во вкладке браузера. Не стенд и не второе «приложение-счётчик»: отвечает ему настоящая служба.

Как посмотреть

export LC_ALL=C.UTF-8
bootstrap/flang check docs/examples/web/shortener/service.flang --proof
bootstrap/flang test  docs/examples/web/shortener/server.flang
bootstrap/flang io    docs/examples/web/shortener/plan.flang --in-dir

Клиент во вкладке:

sh docs/examples/web/build.sh
bootstrap/flang io docs/examples/web/stand.flang --max-orders 100000
# открыть http://127.0.0.1:8908/docs/examples/web/shortener-client/index.html

Ни Node, ни npm, ни python3 -m http.server: модуль печатает двоичный компилятор, страницу отдаёт стенд, написанный на flang (docs/examples/web/stand.flang).

Служба

store.flang                    137   хранилище: коды, адреса, счётчик переходов
service.flang                  675   исход, теоремы, маршрутизация, разбор и печать
server.flang                   136   процессы, надзор, три прогона
server-network.flang            30   те же процессы по сети
plan.flang                      74   тот же обслуживатель через файловый ввод-вывод
plan-network.flang             122   тот же обслуживатель через сокет
plan-durable.flang             273   тот же обслуживатель с журналом
handler-without-budget.flang    36   УЛИКА: не собирается, и в этом смысл
                              ─────
                              1 483   строк, и все на flang

Строки посчитаны wc -l.

Опирается на flang/stdlib/http.flang (1 370 строк, 64 тотальных функции — wc -l, grep -c '^тотальная функция').

Что она делает

Отказы: 400 негодный запрос, 404 нет пути или кода, 405 метод не тот для известного пути (а не 404 — служба не врёт о причине), 409 код занят, 413 тело запроса длиннее 2048, 422 адрес не по http и не по https.

Что доказано, а что проверено

bootstrap/flang check docs/examples/web/shortener/service.flang --proof: функций 24, тотальных 24, обычных 0. Утверждений 8: доказано 5 (из них индукцией 4), сетка 3, объявлено, не доказано 0, отвергнуто 0; законов на веру 0. Код возврата 0.

Доказано (утверждение обо ВСЕХ входах):

1. код ответа из объявленного набора («Код исхода»);
2. пояснение кода непусто («Код исхода»);
3. успех исхода и успех кода — одно и то же («Исход успешен»);
4. октетов от одного до четырёх («Октетов в знаке»);
5. печать ответа начинается версией, кодом и пояснением («Напечатать ответ службы»).

Проверено сеткой (НЕ доказано, и это написано здесь, а не спрятано):

1. урезанное не длиннее предела («Урезать»);
2. тело ответа не длиннее заявленного предела («Тело решения»);
3. в печати ответа длина тела названа в октетах («Напечатать ответ службы»).

Утверждения 6–8 упираются в подстрока и в содержит: закрыть их значило бы уметь доказывать о срезе и вхождении строки, а таких правил у ядра нет. Пометка честная — слово «доказано» стоит только там, где утверждение про все входы.

Ведомость server.flang: функций 7 (тотальных 5, обычных 2), утверждений 0 — теоремы импортированного модуля в ведомость импортёра не переносятся, доказательство закрыто там, где теорема написана.

Что ловит доказательство

Теорема пояснение кода непусто держит каждый объявленный код читаемым: если служба объявит код (422, «Адрес негоден»), которого таблица пояснений в flang/stdlib/http.flang не знает, таблица отдаст пустое слово, строка состояния станет HTTP/1.1 422 — законной по букве и нечитаемой по делу, — и ядро отвергнет теорему с FLANG_PROOF_STEP на этом случае.

Надзор в server.flang обязан стоять над каждым процессом, а не только над «Пересчётом»: надзор над одним «Пересчётом» отвергается FLANG_UNCOVERED_FAILURE. У планировщика свой потолок в миллион витков, и тотальный обработчик может упереться в него, не зациклившись, а просто не успев. Отсюда деление, которое компилятор считает правильным: тотальность снимает с запасом N витков и только его; надзор нужен обоим.

Что она умеет сегодня и чего не умеет

Умеет (шестнадцать запросов — это plan-network.flang; plan.flang гоняет один запрос через файлы — два поручения, ответ 201, код 0): все десять исходов, включая четыре злонамеренных входа — обрезанный запрос (молчание, а не отказ), две длины тела (400), заголовок в мегабайт (431), сто один заголовок (431), тело в мегабайт (413).

Умеет ПО СЕТИ — прогон plan-network.flang (нужен живой сокет), шестнадцать запросов через настоящий сокет на 127.0.0.1:39281, по одному соединению на запрос:

200 201 301 200 404 405 404 422 409 413 0 400 431 431 204 404

Коды сверяются в самом прогоне с теми, что даёт plan.flang, где байты передавались значением; разойдись хоть один — прогон падает. Ноль — молчание на обрезанный запрос: соединение закрыто, не написав ни байта. 413 — на тело в мегабайт, дошедшее по TCP кусками и собранное ПРОГРАММОЙ, а не хозяином.

Служба в обоих прогонах одна и та же: service.flang, store.flang и stdlib/http.flang. Различается ПЛАН — то есть то, откуда берутся байты: plan.flang (файлы) и plan-network.flang (сокет) разбирают отклик хозяина одними и теми же ветками, потому что чтение из соединения отвечает «Прочитано», а ответ в соединение — «Записано», теми же вариантами, что файл.

Сеть стоит 3 поручения и 1 отклик: «Слушать» отдельного поручения не требует (порт назван прямо в «Принять соединение», слушающий сокет заводит хозяин при первом же приёме), а «Прочитать из соединения» нужно — без него мегабайтное тело, пришедшее шестнадцатью пакетами, доставалось бы службе первым куском и объявлялось неполным.

Не умеет, и это названо числом:

Чего службе не хватает, чтобы её поставить в работу

Шесть вещей, без которых службу не ставят в работу, и что с ними здесь. «За границей хозяина» — значит, что это не задача языка и делать это в языке нельзя, не сломав уклад; «нет вовсе» — значит, задача языка, и её никто не делал.

Служба с журналом — то, ради чего язык и делается

plan-durable.flang — третий план той же службы (первый через файлы, второй через сокет). Служба та же; различается только план.

bootstrap/flang io docs/examples/web/shortener/plan-durable.flang --in-dir

Что доказывает форма программы. Успешный ответ на меняющий запрос строится во всём модуле ровно в одном месте — внутри ветви случай вариант «Записано». Перебор 5 состояний × 13 откликов хозяина (список откликов закрыт языком) находит это место ровно один раз; на любом другом отклике уходит 503, а дальше едет старое хранилище и старый журнал.

Что показывает прогон. plan-durable.flang, три прогона:

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

Чем показано, что развилка честна. Множество кодов, объявленных меняющими (201, 204, 301), не сверяется глазами: на 24 парах «начальное хранилище × запрос» проверка сравнивает хранилища до и после и требует совпадения с объявленным. Восстановление сверено с живым состоянием на всех 13 префиксах сценария и на всех 375 обрывах журнала.

Зубы. Из развилки по очереди вынимается по одному коду — все три изъятия краснеют. Четвёртое (добавить в развилку код 200) не краснеет, и это записано отдельной проверкой, а не замято: лишняя запись при повторе даёт то же хранилище, потому что чтение состояния не меняет. Цена лишнего кода — не правильность, а байты: 7 записей против 9 на том же сценарии.

Чего эта служба НЕ гарантирует.

• Долговечности. Отклик «Записано» значит «хозяин сказал, что записал». fsync, кэш диска и перестановка записи контроллером — ОС и железо. Ни один прогон не выключал питания.
• Что журнал не потеряет хвост при обрыве питания. План переписывает файл целиком (дописывания среди поручений языка нет), и что происходит с файлом, когда питание уходит в середине перезаписи, здесь не проверено ничем.
• Одновременного доступа. Двух писателей в один журнал нет и не предполагается; второй клиент ждёт первого.
• Целостности тела записи. Контрольной суммы нет: перевёрнутый бит в середине тела оставит запись целой с испорченным телом.
• Что журнал не растёт. Уплотнения (checkpoint) нет: каждый меняющий запрос добавляет запись навсегда, и восстановление стоит повторения всей истории.
• Единиц измерения. Длина считается кодовыми точками, а не октетами — тот же зазор, что у Content-Length.

Клиент во вкладке

Страница открывается, служба к ней пока не подключена. Приложение заводится и рисует свой экран, но на всякий запрос получает отказ: службы на том же порту нет. Мешает одна названная вещь — расхождения браузера и службы, они перечислены ниже.

Сколько чего написано

Из 453 строк flang 186 — примеры (пример, дано, ожидается): 41 % файла это проверки, лежащие вплотную к проверяемому. Функций 32, тотальных 32 из 32, примеров 51, упавших 0, сторожей в напечатанном коде 0 мест.

Прикладной логики в JavaScript — ноль строк: ни одного решения о ссылках, кодах, переходах и о том, что показать, там не принимается.

Разметки в языке НЕТ, и это решение, а не пропуск

flang/stdlib/view.flang не заведён. Довод в трёх пунктах, и первый из них — измеренный.

Первое: разметка не выразима без правки словаря эффектов. Поручение «Показать» несёт место и текст. Чтобы оно понесло дерево разметки, словарю нужна четвёртая сумма — рекурсивный именованный тип внутри встроенной суммы, — а поля встроенных сумм плоские (string, number, any). Словарь лежит в flang/self/io.flang, и правка — это работа там и в десяти целях печати.

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

Третье, и это уже замер: имеющегося ХВАТИЛО. Экран со списком, счётчиками и сообщением уложился в одно место и один текст. Причём разбивать экран на несколько мест было бы дороже, чем кажется: «Продолжение» несёт РОВНО ОДНО поручение, значит K мест — это K поручений на каждую перерисовку. Замер по сценарию «открылось → набрал адрес → нажал сократить»:

Шесть перерисовок на три действия. При экране из четырёх мест это стало бы 24 поручения вместо 6 — вчетверо больше витков через хозяина ради того же кадра. То есть выбор «одно место, один текст» здесь не только дешевле в работе, но и дешевле при работе.

Устройство приложения

Состояние — одна запись из пяти полей. Поля «где мы» в ней нет: точку, в которой программа ждёт хозяина, называет сам ОТКЛИК — показали, значит дальше ждём; ответили, значит дальше считаем. А поле «дело» отвечает на другой вопрос — «что задумано», — и без него человек не увидел бы надписи «шлём службе…»: экран обновился бы сразу с ответом.

Цепочка из двух запросов подряд написана и проверена: «создали ссылку» само задумывает «сходить за списком», потому что после создания на экране обязан быть свежий список, а не прежний. В журнале это видно: POST /ссылки → GET /ссылки.

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

Ведомость доказательства клиента

функций 32: тотальных 32, обычных 0
обещание несёт: композиция 32, структура 0, точный шаг 0, постоянный шаг 0, объявленная мера 0
сторожей в рантайме: 0 мест
законов на сетке: 0 (значений в сетках 0); на веру: 0
утверждений 43: доказано 43 (из них без теоремы 43), сетка 0, объявлено, не доказано 0

(check --proof по client.flang; сетки у клиента нет.)

Все 32 — «доказано композицией»: рекурсии нет ни в одной, обещание сложено из обещаний тех, кого функция зовёт. Ни одна не потребовала объявленной меры, значит в напечатанном коде нет ни одной проверки при работе.

Чего этим НЕ доказано, и это надо сказать вслух. Доказано, что каждый шаг завершается. Не доказано и не может быть доказано здесь: что последовательность шагов конечна — у приложения нет ни одной ветки «Конец работы», оно кончается тогда, когда закрывают вкладку. Незавершаемость живёт в цикле хозяина, ровно там же, где у службы.

Что везёт вкладка

Ни одного файла реализации языка во вкладку не едет: только напечатанный код и хозяин.

Напечатанный модуль печатает стенд при запуске и отдаёт из памяти: файла в дереве нет, значит нечему устареть. Руками то же делается так:

bootstrap/flang emit docs/examples/web/shortener-client/client.flang \
  --target js --no-cli --out <каталог>

Где браузер и служба не сходятся — пять мест и шестое

Ни одно не про язык и не про приложение: это долг службы.

1. заголовков CORS нет ни одного. Весь набор заголовков ответа — Content-Type и, на переезде, Location (service.flang, «Заголовки решения»). Статики служба не отдаёт, то есть «того же источника», откуда подать страницу, у неё нет вовсе;
2. на OPTIONS служба отвечает 405 — предварительная проверка браузера до службы не доходит;
3. пути кириллицей нужны сырыми байтами, а браузер их кодирует процентами. GET /ссылки сырыми — 200; GET /%D1%81%D1%81... — 404. Кириллических путей у службы 3 из 3;
4. Content-Length считает байты, а не знаки. Тело адрес=… начинается с шести кириллических знаков — это 6 знаков и 11 байтов. В ответе это закрыто: длина тела печатается в октетах («Длина тела в октетах» в service.flang). Считает ли служба в октетах длину входящего тела, здесь не проверено;
5. одно соединение — один обмен, при этом Connection: close не посылается.

Плюс шестое: служба кладёт в Location сырой кириллический адрес, а такой заголовок не пропускает ни Node (ERR_INVALID_CHAR), ни браузер: переход падает как 500 Moved Permanently — код 500 при строке состояния от 301.

Как план попадает во вкладку

flang emit … --target js печатает объявление план «Стойка ссылок» вместе с функциями приложения:

• описатель плана печатается данными (const $io = {…}) и отдаётся двумя дверями — ioPlan() и ioRun(имя, хозяин), тем же генератором, что печатает concPlan();
• исполнитель плана — flang/src/emit/js/flang_io.js, порт runPlan на представление значений напечатанного модуля. Печатается ВНУТРЬ модуля, как печатается планировщик конкурентности: модуль остаётся самодостаточным;
• молча потерять план нельзя: цель обязана либо напечатать план, либо отказать, назвав план по имени, — третьего исхода нет. Правило записано в docs/ct/spec.md: emit --target js печатает объявление и отвечает 0; с ADR-0100 печатают ещё ts, c, go, python, rust, а cpp, csharp, elixir, java отказывают FLANG_PLAN_UNSUPPORTED кодом 1, не записав ни файла. Сверяет это scripts/targets/plan-across-targets.fscript.

Хозяин вкладки — flang/src/emit/js/flang_host_browser.js, ввозов ноль.

Раскодирование процентов

Перевод «браузер → служба» — это раскодирование процентов обратно в сырой UTF-8, и оно написано на flang, в flang/stdlib/http.flang. Опирается оно на встроенную форму символ по коду, обратную к код символа и доступную на всех четырёх поверхностях языка. Раскодирование доводит до символа все 1 112 064 скалярных значения (половины суррогатных пар отвергаются отказом, а не складываются: в тех целях печати, где строка хранится как UTF-8 — C, Go, Rust, — такая половина не записывается вовсе).

Раскодирование стоит ПОСЛЕ разделения пути: %2F внутри куска остаётся знаком и лишнего куска не даёт. Кириллические маршруты — 3 из 3 — отвечают на путь, закодированный браузером.

Не закрыто: экран односторонний

Программа читает поля ввода, но не может их писать. Видно на снимке экрана: после «очистить» программа считает набранное пустым, а в поле у человека по-прежнему стоит прежний текст. Поручений, пишущих на экран, одно («Показать», и оно пишет textContent); поручений, пишущих в поле ввода, — 0. Разошлись при этом не картинки, а состояние: программа и человек видят разное.

Закрыть это — значит расширить словарь эффектов. Стоило бы это одного варианта поручения и одной ветки у хозяина.

Как это соотносится с соседом

Приложение в браузере — «Градины», приложение того же устройства: тот же хозяин, тот же цикл поручений, тот же чистый обработчик. Разница одна и она существенная: у Градин всё замкнуто на себя, а здесь есть ожидание чужого ответа.