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

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

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

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

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

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

sh web/sobrat.sh
bootstrap/flang io web/stand.flang --max-orders 1000000
# открыть http://127.0.0.1:8908/web/shortener/index.html

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

Служба

store.flang                    155   хранилище: коды, адреса, счётчик переходов
service.flang                  580   исход, теоремы, маршрутизация, разбор и печать
server.flang                   229   процессы, надзор, три прогона
plan.flang                     133   тот же обслуживатель через файловый ввод-вывод
handler-without-budget.flang    53   УЛИКА: не собирается, и в этом смысл
                              ─────
                              1 150   строк, и все на flang

Опирается на flang/stdlib/http.flang (1 358 строк, 58 тотальных функций).

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

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

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

check --proof по service.flang: функций 83, тотальных 83, обычных 0, неучтённых 0. Утверждений 7, доказано 5, сеткой 2, принято на веру 0, отвергнуто 0, аксиом 0.

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

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

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

1. урезанное не длиннее предела — сетка 3;
2. тело ответа не длиннее заявленного предела — сетка 1.

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

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

Что нашло само доказательство

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

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

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

Умеет (проверено прогоном serve.mjs, шестнадцать запросов): все десять исходов, включая четыре злонамеренных входа — обрезанный запрос (молчание, а не отказ), две длины тела (400), заголовок в мегабайт (431), сто один заголовок (431), тело в мегабайт (413).

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

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

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

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

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

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

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

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

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

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

node examples/web/shortener/serve-durable.mjs     # три прогона
node --test flang/test/shortener-durable.test.mjs        # 11 проверок

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

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

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

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

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

Улика, найденная связкой. Пока служба отвечала в том же витке, в котором читала, serve-network.mjs проходил все шестнадцать соединений. Стоило поставить между чтением и ответом журнал — и 5 меняющих запросов из 8 получили ноль байт вместо ответа, при том что поручений «Ответить в соединение» хозяин исполнил все восемь и журнал на диске был правильный. Причина — createServer без allowHalfOpen: node закрывал свою половину соединения по FIN клиента. Правка в flang/src/host/node.mjs, одно слово; serve-network.mjs после неё даёт те же 16 кодов.

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

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

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

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

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

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

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

На .flang 488 строк, на .mjs — 342, и это только прогон без браузера. Стенд и прогон в браузере (391 строка на двоих) удалены вместе со второй реализацией, на которой они держались.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Прогон в настоящем браузере

web/shortener/probe.mjs (удалён), HeadlessChrome 151, стенд поднимался сам. Шесть сверок экрана, все побайтовые, все зелёные:

браузер: Mozilla/5.0 (X11; Linux x86_64) … HeadlessChrome/151.0.0.0 Safari/537.36
план поехал за 194 мс от goto

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

несошлось: 0

Вес: что везёт вкладка

Замерено одним и тем же прибором (page.on("response") в удалённом probe.mjs, все ответы за весь сценарий из шести сверок, HeadlessChrome 151), до и после того, как приложение поехало из напечатанного модуля:

Разница 17,2 раза, и вторая реализация языка во вкладку не едет вовсе. Что вкладка везёт теперь, по файлам:

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

bootstrap/flang emit web/shortener/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 байтов. Браузер поставит длину в байтах, служба сочтёт запрос неполным и будет ждать добавки;
5. одно соединение — один обмен, при этом Connection: close не посылается.

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

Что упёрлось — и что уже закрыто

ЗАКРЫТО: генератор печатал функции приложения и молча ронял план

Здесь стояло: flang emit … --target js кончается кодом 0, без единой диагностики, печатает всё приложение целиком — включая обе функции плана — и теряет объявление план «Стойка ссылок», 0 байт. Напечатанный модуль умел считать и не умел работать.

Закрыто целиком, тремя правками, и каждая — там, где образец уже стоял рядом:

• описатель плана печатается данными (const $io = {…}) и отдаётся двумя дверями — ioPlan() и ioRun(имя, хозяин). Тем же генератором, что печатает concPlan(), и на обеих сторонах сразу: flang/src/emit/js.mjs и flang/self/emit-js.flang сверяются побайтово, 108 программ корпуса из 108;
• исполнитель плана — flang/src/emit/js/flang_io.js, порт runPlan на представление значений напечатанного модуля. Печатается ВНУТРЬ модуля, как печатается планировщик конкурентности: модуль остаётся самодостаточным;
• молчание чинится отдельно от печати: цель обязана либо напечатать план, либо отказать, назвав план по имени, — третьего исхода нет. Правило это записано в flang/cat/SPEC.md, и 22 августа 2026 двоичный его держит: emit --target js печатает объявление и отвечает 0, остальные семь целей отказывают FLANG_PLAN_UNSUPPORTED кодом 1, не записав ни файла. Сверяет это scripts/plan-across-targets.flang.

Хозяин переехал в flang/src/emit/js/flang_host_browser.js с нулём ввозов; flang/src/host/browser.mjs стал переходной строкой, подставляющей интерпретаторскую фабрику варианта. Реализация хозяина ОДНА, а не две.

ЗАКРЫТО: раскодирование процентов упиралось в одну недостающую форму

Что было найдено. Перевод «браузер → служба» — это раскодирование процентов обратно в сырой UTF-8. На flang оно не писалось, и упиралось ровно в одно: моста из числа в строковый символ у языка не было. Мост в обратную сторону был (код символа), а этот — нет.

Числами на день находки: встроенных форм 20, из них ведущих из числа в строковый символ — 0. Поэтому flang/stdlib/http.flang раскодировал проценты только для кодов 32…126 — это 95 кодовых точек из 1 114 112, — и сам называл это «названным пределом языка, а не недоделкой модуля». /ссылки — 7 знаков, 13 байтов, и 0 из них попадали в те 95.

Что стало. Форма заведена: символ по коду, двадцать первая встроенная, обратная к код символа, на всех четырёх поверхностях языка. Раскодирование в http.flang доводит до символа 1 112 064 скалярных значения из 1 112 064 (половины суррогатных пар отвергаются отказом, а не складываются: в четырёх целях печати из восьми строка — UTF-8, и там такая половина не записывается вовсе).

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

Осталось от находки то, что от неё и должно остаться: вывод «стенд на JavaScript» держался на этой форме и держаться перестал.

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

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

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

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

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