Руководство Lispex
(Лиспекс)
( скобки как пунктуация, рекурсия как рифма )
Небольшой Лисп для решающих правил, сознательно близкий к Scheme. Один и тот же ввод даёт один и тот же ответ, а запуск может оставить запись, достаточно точную для последующей проверки.
На входе — структурированные данные, на выходе — печатаемый вердикт.
Записи — ассоциативные списки, граница — точное целочисленное сравнение, а каждый вердикт, включая отказ, — обычные данные, которые можно напечатать и сравнить. Новой нотации здесь нет: поверхность принадлежит Scheme. Характер Lispex — в том, что зафиксировано: закрытая поверхность процедур, детерминированные ошибки, один ответ на один ввод.
(define (field key record)
(let ((entry (assq key record)))
(if (pair? entry)
(cdr entry)
(error "missing field" key))))
(define (review-refund request)
(let ((days (field 'days request))
(opened (field 'opened request))
(cents (field 'cents request)))
(cond ((not (exact-integer? days)) '(reject malformed-days))
((>= days 15) '(deny outside-window))
(opened '(deny opened-item))
((> cents 50000) '(escalate manual-review))
(else '(allow within-policy)))))
(map review-refund
'(((days . 14) (opened . #f) (cents . 12900))
((days . 14) (opened . #f) (cents . 82000))
((days . 15) (opened . #f) (cents . 12900))))
; => ((allow within-policy)
; (escalate manual-review)
; (deny outside-window))Два входа: карта синтаксиса для читающих Scheme и пошаговый путь для остальных.
Карта синтаксиса показывает все повседневные формы с наблюдаемыми результатами и отмечает, где Lispex строже привычного Scheme: обязательная ветвь else у if, закрытая поверхность из 205 процедур, higher-order процедуры с одним списком, отсутствие слоя пользовательских макросов. Путь обучения идёт медленнее и завершается одним законченным, проверенным правилом возврата.
- 01Запустить первую программу
- 02Назвать значения и процедуры
- 03Выбрать решение в форме данных
- 04Проверить законченное правило возврата
Lispex работает без сервера. Эталонный интерпретатор, скомпилированный в WebAssembly, выполняет код прямо в вашем браузере.
Один простой путь по умолчанию и четыре явных Native-маршрута.
По умолчанию везде — в браузере, npm и Native — работает интерпретатор Rust tree. Native дополнительно позволяет проверить и закрепить встроенную Rust VM либо точно установленные продукты Topaz VM и AOT — как явные маршруты, а не тихие подмены.
Rust и LIL покрывают все 205/205 текущих строк возможностей; LIT отдельно ограничен 84/205 и именно так и отражается. Native-команды routes inventory, lock, doctor, measure и run держат точную identity маршрута и отказ на виду. Ничто не обнаруживается, не подменяется и не повторяется без вашего ведома: отсутствующий продукт — это явный отказ, а не fallback.
Выполните правило возврата в точных лимитах и сохраните предмет проверки.
Native-команда lispex rule run готовит проверенное правило, принимает один строгий JSON-ввод и один раз вычисляет его на ограниченном вычислителе — отдельном движке без импортов, который обязан отчитаться за каждую единицу работы и выделения внутри объявленных вами лимитов. После запуска остаётся каталог решения из пяти членов: подготовленный артефакт правила, канонический ввод, детерминированный результат с точной привязкой запроса, пригодное к выдаче переносимое ядро и производная сводка. Исходного текста правила среди них сознательно нет.
- 01Проверенное правило
- 02Строгий JSON-ввод
- 03Решение: allow
- 04Проверяемое переносимое ядро
1. Правило
(let ((days (cdr (car input)))
(opened (cdr (car (cdr input)))))
(if (< days 15)
(if opened "deny" "allow")
"deny"))2. Ввод
{
"days": 14,
"opened": false
}3. Один ограниченный запуск
lispex rule run \
--source refund-window.lspx \
--input day-14-unopened.json \
--prepare-limits prepare-limits.json \
--eval-limits evaluation-limits.json \
--out decision
lispex rule inspect --dir decision
lispex rule verify --dir decision
lispex rule replay --dir decisionДля поддерживаемого случая «14-й день, не открыт» ограниченный запуск возвращает allow.
rule inspect сводит каталог без выполнения; rule verify — тоже без выполнения — проверяет точный набор членов, identity, хеши и привязки; rule replay один раз вычисляет записанный запрос в свежем экземпляре вычислителя и требует того же результата. Ни одна из трёх операций не даёт полномочий.
Что связывает переносимое ядро
Смысловое правило, канонический ввод, точные лимиты, точный артефакт вычислителя и детерминированный результат — достаточно, чтобы точно знать, на какой вопрос и под какими потолками был дан ответ. Израсходованный или оставшийся ресурс в ядро не входит.
Чего запись не устанавливает
Кто выполнил запуск, свежо ли решение, справедлива и корректна ли политика в правиле, не использовано ли то же решение дважды — и никакого разрешения действовать за пределами процесса.
Решающее правило можно передать как детерминированное изображение.
Изображение — это канонический графический файл, несущий точные байты исходника правила. Здесь оно несёт проверенное правило возврата, возвращающее каноническое Decision — единственную форму результата, для которой Vouch может выпустить свидетельство. Исходник можно восстановить локально, выполнить только после доказательства каноничности байтов или закрепить доказанное изображение как точный source в процессе Vouch ниже. Пиксели несут только целостность.
(define days-since-delivery (car input))
(define opened? (car (cdr input)))
(if (<= days-since-delivery 14)
(if opened?
(decision-deny)
(decision-approve))
(decision-deny))Отсюда один путь продолжается ниже: восстановить и доказать это изображение, закрепить его как точный source и в Native выпустить подписанное свидетельство Vouch для одного точного ввода. Получатель аутентифицирует это свидетельство по собственной trust policy, заново выполняет правило на своей машине и проходит локальный gate — а действовать ли дальше, отдельно решает внешнее приложение. Само изображение — ничто из этого: не подписанное свидетельство, не доверие и не полномочие. Оно лишь точно переносит байты.
У решения может быть квитанция.
Vouch превращает одно записанное решение в подписанное переносимое свидетельство — и строго отделяет свидетельство от разрешения.
Квитанция — это подписанная запись одного запуска: какие байты правила выполнялись, какие байты ввода вошли и какое решение получилось. В нативном release-бинарнике lispex vouch issue создаёт её, сам выполняя проверенное правило — квитанция фиксирует то, что действительно произошло, а не чьи-то слова. Квитанция, исходник и ввод могут путешествовать одним файлом — bundle. Аутентифицировать bundle может любой — командой lispex vouch verify в Native или npm, — и она отвечает ровно на один вопрос: подписал ли выбранный вами ключ именно эти байты? Больше она сознательно не отвечает ни на что.
Bundle не выбирает запрос, выполняемый вашим gate.
Повторное выполнение начинается с запроса, закреплённого вами, а не со слов bundle.
Привязка запроса — правило, по которому ваша машина повторно выполняет только то, что вы сами попросили. Bundle доказывает то, что наблюдал его издатель; он не выбирает правило и ввод на вашей стороне. Поэтому перед любым повторным выполнением вы сами закрепляете запрос: исходник правила — файл у вас на руках или изображение, прошедшее полное каноническое доказательство, — и точный ввод. Проверка сначала аутентифицирует подпись, затем сравнивает bundle с закреплённым запросом, и только точное совпадение переходит к выполнению. Не закрепите ничего — проверка останется проверкой подписи и никогда не дойдёт до повторного выполнения или gate.
Повторное выполнение — сравнение, которое проводит ваша машина.
Gate успешен только при точном живом совпадении — поверх trust policy, которую вы составили сами.
lispex vouch gate — локальная проверка с конкретным вопросом: если выполнить правило сейчас, на этой машине, с закреплённым запросом — получится ли ровно подписанный результат, и то ли это решение, которое я потребовал? На входе свидетельство, на выходе код завершения. Над этим стоит trust policy — короткий файл конфигурации, который вы составляете и аудируете сами: проверенный вами открытый ключ, точный вычислитель и точный исходник правила либо доказанное изображение, которые вы принимаете. Корректно подписанное правило, которого нет в вашей политике, отклоняется. Сама по себе политика ничего не разрешает — она лишь сужает то, что вы готовы проверять.
Чего не даёт успешный gate.
Каждая граница ниже намеренна. Читайте пройденный отчёт как свидетельство для вашего следующего шага — не более.
Пройденный отчёт verify или gate — не разрешение, не токен и не полномочие на внешнее действие: возвращать ли деньги, платить ли, отправлять ли — отдельное решение вашего приложения. Привязка запроса доказывает равенство с закреплённым запросом, а не свежесть, уникальность или защиту от повторной подачи. Изображение доказывает лишь целостность восстановленных байтов исходника, но не доверие к ним. npm умеет проверять и аутентифицировать, но не может выдавать, повторно выполнять или применять gate; браузерный WASM и песочница только вычисляют код. И ничто из обычного выполнения — блокировки маршрутов, измерения, вывод запусков — не становится полномочием Vouch.
Выполнить полный процесс Vouch생각의 원형을 담는 언어.
The language that captures the shape of thought.
Язык, воплощающий форму мысли.