(Lispex)

Vouch Bridge связывает закрытый движок и публичную запись доказательства. Движок по-прежнему делает свою работу сам. Отчёт моста даёт этой работе форму, которую можно проверить вне сервиса.

Когда это нужно

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

Первый профиль это доказательства преобразования. Lena Engine является коммерческим движком преобразования, под который рассчитан этот профиль. Lispex Vouch даёт публичную форму отчёта и границу проверки для доказательства, которое выпускает этот движок.

Что записывает отчёт

Отчёт vouch.bridge-report/v0 записывает

исходный язык, путь источника, длину в байтах и хеш источника
целевой язык, путь цели, длину в байтах и хеш цели
имя внешнего движка, версию и коммит
маршрут и capability id, которые движок заявляет как проверенные
результаты проверок, такие как source boundary, conversion route и target adapter
хеши связанных доказательных артефактов
список границ, где указано, что утверждается и что исключается

Отчёт намеренно говорит о форме доказательства. Он не является доказательством корректности целевого кода.

Проверить пример

Публичный пример это небольшой отчёт о доказательстве преобразования TypeScript в Python.

BASH

lispex verify-bridge \
  --source examples/vouch-bridge/source/checkout-discount.ts \
  --target examples/vouch-bridge/target/checkout_discount.py \
  examples/vouch-bridge/reports/checkout-discount.bridge.json

Exit 0 означает, что отчёт внутренне согласован. Байты источника и цели совпадают с хешами в отчёте, заявленные проверки согласованы, а списки границ совпадают с контрактом моста.

Exit 1 означает, что отчёт удалось прочитать, но он не удовлетворил контракту. Изменение хеша источника, отсутствие обязательного исключения в границах, неизвестное поле верхнего уровня или провал заявленной проверки приводят к ошибке.

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

verify-bridge не запускает Lena Engine или любой другой внешний движок. Он не создаёт целевой код заново. Он не проверяет закрытое состояние конвейера. Он не доказывает, что целевая программа правильна или что два языка имеют один и тот же смысл.

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