Ограниченное приложение решений Lispex

Топаз 5.18 позволяет проверенному приложению один раз подготовить именованные правила Lispex и вычислить много канонических значений. Граница намеренно узка. Пакет закрепляет в topaz.lock профиль lispex/r7rs-rule-embedded-core/1, встроенный компонент, исходный текст и лимиты каждого правила, а также общие квоты приложения.

Начните с сопровождаемого примера в docs/samples/guides/lispex-application. В нём находятся точные манифест и файл блокировки, созданные дескрипторы правил, подготовленные артефакты, два модуля Топаза и четыре достигаемых правила из этого руководства.

Объявите приложение

Манифест одновременно выбирает версию Топаза и стандартной библиотеки. Там же указаны ограниченный профиль Lispex и контракт приложения.

[package]
name = "bounded_lispex_decision_application"
version = "0.1.0"
language = "5.18"
entry = "src/main.tpz"

[dependencies]
std = "5.18"

[lispex]
profile = "lispex/r7rs-rule-embedded-core/1"
application = "topaz/lispex-decision-application/1"
application_quotas = "rules/application.quotas.json"

[[lispex.rule]]
name = "approve"
source = "rules/approve.lspx"
limits = "rules/approve.limits.json"

Остальные записи [[lispex.rule]] имеют ту же форму. Имена правил становятся созданными функциями в std.lispex.rules; это не пути, выбираемые во время выполнения, и не селекторы компонентов.

Задайте правило и конечные лимиты

rules/approve.lspx содержит обычный исходный текст Lispex в пределах выбранного ограниченного профиля.

(if (< 10 15) "allow" "deny")

rules/approve.limits.json закрепляет пределы подготовки и вычисления. Полный пример сохраняет все поля; ниже показаны два предела работы.

{
  "schema": "topaz.lispex-embed-limits/v1",
  "prepare": {
    "prepare_work": 1000000
  },
  "evaluate": {
    "eval_work": 10000
  }
}

rules/application.quotas.json отдельно ограничивает хост приложения. Пример разрешает два активных и два ожидающих вычисления, всего 64 вычисления и конечный срок по настенным часам. Семантическое исчерпание лимита правила и отказ приложения имеют разные типизированные исходы.

Создайте и проверьте файл блокировки

Создавайте его из корня пакета. Не вводите дайджест компонента или подготовленного артефакта вручную.

topaz lock --root .

Перед фиксацией проверьте topaz.lock. Раздел [lispex] закрепляет профиль, контракт приложения, компонент, вычислитель, ABI, кодек значений, модель счётчиков, контракт артефактов, адаптер, квоты, диспозицию цели и каталог созданных дескрипторов. Каждая запись [[lispex.rule]] закрепляет исходный текст, лимиты, запрос и результат подготовки и подготовленный артефакт.

После изменения манифеста, правила, лимитов, квот, компонента или профиля файл блокировки нужно создать заново. Сборка с --locked отклоняет расхождение и не подготавливает другое правило молча.

Проверьте и запустите пакет

Сначала используйте заблокированный маршрут интерпретатора.

topaz check --root . --locked
topaz run --root . --locked -- all

Сопровождаемый сценарий all вычисляет 24 обычных входа, проверяет изоляцию правил, достигает семантического предела и отклоняет 65-е вычисление приложения. Он выводит ровно следующую строку:

all:default:24:evidence:verified:replayed:isolation:2:complete:semantic-limit:exhausted:aggregate-quota:64:refused

Любой другой текст или ненулевой код завершения означает неудачное наблюдение.

Заблокированное правило deadline_probe намеренно отделено от all. Суд релиза копирует точный пакет, меняет только квоту времени приложения со 100 миллисекунд на 1 миллисекунду, заново связывает эту квоту в копии файла блокировки и требует DeadlineExceeded в отдельных интерпретируемом и перемещённом нативном продуктах без исходников. Затем суд успешно запускает обычное приложение с лимитом 100 миллисекунд. Q1 остаётся основанием для очистки внутри одного приложения. Поэтому обычный вывод примера не предполагает определённую скорость машины.

Осмотрите, проверьте и повторите потребительское свидетельство

Созданный API импортируется из std.lispex, а дескриптор правила — из std.lispex.rules.

let решение = evaluate(rules.approve(), input, defaultLimits(rules.approve()))
let запись = evaluateWithEvidence(
    rules.approve(),
    input,
    defaultLimits(rules.approve()),
)

Для подходящего детерминированного исхода полный пример выполняет следующий точный цикл:

1. consumerArtifactBytes сохраняет весь потребительский артефакт.
2. consumerArtifactFromBytes проверяет сохранённые байты при приёме.
3. inspectConsumerArtifact сообщает устойчивые идентификаторы без запуска.
4. verifyConsumerArtifact проверяет структуру, дайджесты и связи.
5. portableCoreBytes извлекает ядро в формате Lispex, если оно существует.
6. freshReplay вычисляет заблокированные правило и вход в новом гостевом экземпляре и принимает только полностью совпавший артефакт.

Артефакт и переносимое ядро созданы потребителем и не аутентифицированы. Они не содержат издателя, одобрения поставщика, полномочия подписи, допуска компонента или разрешения на внешнее действие. Операционный отказ, отмена, защитное прерывание и сбой движка не создают переносимого ядра.

Соберите и запустите нативный продукт

Создайте оптимизированный управляемый нативный продукт вне корня пакета.

topaz build --root . --locked --release --out-dir ../bounded-product

Запустите результат на тех же ОС и архитектуре, где он был собран.

../bounded-product/target/release/program all

В Windows используйте:

..\bounded-product\target\release\program.exe all

Нативный продукт должен вывести то же точное наблюдение. Успешная сборка не делает исполняемый файл переносимым на другую цель.

Учитывайте границу маршрутов

Контракт приложения имеет закрытый набор маршрутов.

Отклонённый маршрут не переключается на интерпретатор или нативный продукт. Полный профиль Lispex имеет отдельные компонент, профиль, контракт, проверку целей и допуск. Он не расширяет этот ограниченный профиль на месте.

Продолжите с разделов Бэкенд Rust, Бэкенд Python и Вычислитель Lispex и LIT.