Руководство Lispex

(Лиспекс)

( скобки как пунктуация, рекурсия как рифма )

Небольшой Лисп для решающих правил. Один и тот же ввод даёт один и тот же ответ, а квитанцию можно сверить позже.

Начать обучение Песочница Карта синтаксиса

Таблица I

Код и есть данные, напечатанные без прикрас.

LISPEX

(define program '(+ 1 2 3))
program

Форма факториал

LISPEX

(define (factorial n)
  (if (= n 0)
      1
      (* n (factorial (- n 1)))))

(factorial 5)

Данные цитируемая форма

LISPEX

(define form
  '(map (lambda (n) (* n 10))
        '(1 2 3 4)))

form

Четыре небольших шага

Напишите первое решающее правило до перехода к глубокому руководству.

Запустите программу, назовите повторяемую работу, сформируйте данные и проверьте точную границу. Знание Scheme, бэкендов, изображений и Vouch не требуется.

01Запустить первую программу
02Назвать значения и процедуры
03Выбрать решение в форме данных
04Проверить законченное правило возврата

Точные изображения Lispex

Решающее правило можно передать как детерминированное изображение.

Локально восстановите точный исходник, выполните его после доказательства каноничности или используйте доказанное изображение напрямую как source в Request-Bound Vouch.

LISPEX

(if (and (<= days-since-delivery 14)
         (not opened?))
    '(decision allow)
    '(decision deny outside-refund-window))

Lispex работает без сервера. Эталонный интерпретатор, скомпилированный в WebAssembly, выполняет код прямо в вашем браузере.

Среды выполнения Lispex

Три пути исполнения с явными границами.

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 Vouch

У решения может быть квитанция.

Lispex сохраняет переносимую аутентификацию bundle и требует точную внешнюю привязку запроса до полномочий выполнения Native.

Напишите небольшое решающее правило и закрепите ввод. Команда lispex vouch issue в нативном release-бинарнике формирует и подписывает допустимое свидетельство. lispex vouch verify аутентифицирует точный связанный контекст. Для bundle --reexecute требует либо внешний --source, либо полностью доказанный --source-image, плюс --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 и точного source-файла либо доказанного изображения, а policy check проверяет точные канонические байты. Эти команды создают конфигурацию, а не trust, evidence или полномочия. npm не может выдавать, повторно выполнять, применять gate или повышать отчёт. Public WASM и Playground предоставляют вычисление без аутентификации или policy-инструментов.

Подробнее о Lispex Vouch

Request-bound Vouch

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.

Язык, воплощающий форму мысли.