Руководство Lispex
(Lispex)
( скобки как пунктуация, рекурсия как рифма )
Небольшой Лисп для решающих правил. Один и тот же ввод даёт один и тот же ответ, а квитанцию можно сверить позже.
Код и есть данные, напечатанные без прикрас.
(define program '(+ 1 2 3))
programФорма факториал
(define (factorial n)
(if (= n 0)
1
(* n (factorial (- n 1)))))
(factorial 5)Данные цитируемая форма
(define form
'(map (lambda (n) (* n 10))
'(1 2 3 4)))
formLispex работает без сервера. Эталонный интерпретатор, скомпилированный в WebAssembly, выполняет код прямо в вашем браузере.
Три пути исполнения с явными границами.
LIL — это Lispex-in-Lispex, а LIT — транслитерация Lispex-in-Topaz. Вместе с эталоном Rust они образуют три ограниченные линии реализации.
LIL сейчас поддерживает 85/205 строк primitive capabilities, а LIT сохраняет отдельную границу 84/205. Выпущенная общая квитанция Rust/LIL/LIT записывает совпадение всех семейств в 59/144 случаях и сохраняет видимыми 179 попарных расхождений. В отдельной кампании одной линии Rust на 11 088 случаях естественных расхождений не найдено. Этот масштабированный результат не относится к трём семействам или всему языку.
У решения может быть квитанция.
Lispex сохраняет переносимую аутентификацию bundle и требует точную внешнюю привязку запроса до полномочий выполнения Native.
Напишите небольшое решающее правило и закрепите ввод. Команда lispex vouch issue в нативном release-бинарнике формирует и подписывает допустимое свидетельство. lispex vouch verify аутентифицирует точный связанный контекст. Для bundle --reexecute теперь требует внешние --source и --input; затем правило повторно выполняется обоими текущими нативными evaluator, а полный transcript сравнивается с обоими подписанными наблюдениями. lispex vouch gate --require-decision завершается успешно только при точном совпадении живого согласия с требуемым решением. Отчёт gate не является переносимым токеном или разрешением внешнего действия. Trust policy v1 отклоняет корректно подписанное правило, если выбранный ключ не разрешает его точный исходник. Native и npm применяют эту проверку одним Rust verifier и выдают одинаковый канонический отчёт v0. npm не может выдавать, повторно выполнять, применять gate или повышать отчёт. Unpinned verify bundle остаётся только аутентификацией и не может перейти к re-execution или gate. После аутентификации запрос сравнивается, и только приватное live request-bound значение переходит к текущему выполнению. Это равенство запроса, а не свежесть или replay-контроль. lispex vouch policy create составляет каноническую policy v1 из проверенных потребителем public key, engine digest и точного исходника, а policy check проверяет точные канонические байты. Эти команды создают конфигурацию, а не trust, evidence или полномочия. npm не может выдавать, повторно выполнять, применять gate или повышать отчёт. Public WASM и Playground предоставляют вычисление без аутентификации или policy-инструментов.
Bundle не выбирает запрос, выполняемый вашим gate.
Native re-execution и gate с bundle требуют полную внешнюю пару source/input и передают в выполнение только live request-bound evidence.
Raw- и unpinned-аутентификация сохраняются. Отсутствующая или неполная authority-пара отклоняется до I/O artifact; отчёты и байты bundle нельзя повысить до grant.
Выполнить полный процесс Vouch생각의 원형을 담는 언어.
The language that captures the shape of thought.
Язык, воплощающий форму мысли.