Pruv

Pruv является языком для proof-native контрактов. Он компилирует изменения состояния и политику расходования в существующий ABI 3. Ноды исполняют и доказывают полученную программу через общее отношение блока.

Компилятор поставляется отдельным инструментом разработчика. Его результат работает с существующими CLI и RPC контрактов. ABI 3 предоставляет 16 инструкций, два постоянных регистра u64 и два временных регистра. Pruv проверяет эти ограничения при компиляции.

Сборка и использование

Из корня репозитория:

cargo build --release --locked -p noid_pruv
target/release/pruv check noid_pruv/examples/budget.pruv --params budget.params.json
target/release/pruv verify noid_pruv/examples/budget.pruv --params budget.params.json
target/release/pruv build noid_pruv/examples/budget.pruv --params budget.params.json --out budget.json
parano1d-cli contract create budget.json --out budget.opening.json

check проверяет синтаксис, типы, поля политики и нативные ограничения ресурсов. verify проверяет объявленные постусловия через локальный Z3. build экспортирует определение custom_program и выполняет те же проверки, что check. Выходные файлы должны быть новыми. Без --out результат выводится в stdout.

Параметры задаются объектом JSON. Адреса используют обычный формат o1…. Каждый параметр u64 является канонической десятичной строкой, включая высоты и суммы. Параметры bool используют JSON true или false. Повторяющиеся, пропущенные и неизвестные параметры вызывают ошибку. Для примера бюджета задайте:

{
  "spending_key": "<spending wallet o1 address>",
  "recovery_key": "<recovery wallet o1 address>",
  "recipient": "<recipient o1 address>",
  "recover_at": "<future block height>",
  "budget": "10000000",
  "max_fee": "1000000",
  "max_payment": "1000000"
}

Суммы выражены целыми μNOID. Каждый отдельно пополненный экземпляр имеет собственное состояние и бюджет. Пример вычитает выплату и её комиссию из remaining. До дедлайна расходующий ключ может продолжать исполнение, после дедлайна ключ восстановления может закрыть контракт. Закрытие следует физическому соглашению выходов ABI 3: retained соответствует выходу 0, payout выходу 1, поэтому при закрытии payout = 0.

Пополнение, вызов и восстановление

Создание и пополнение выполняются через локальную ноду финансирующего кошелька. CLI использует десятичные NOID, а параметры Pruv и RPC целые μNOID.

parano1d-cli contract protocol
parano1d-cli contract fund budget.opening.json 10
parano1d-cli contract instances budget.opening.json

Runtime должен быть доступен и сообщать ABI 3. Дождитесь подтверждения пополнения. Используйте точные текущие slot_index и creation_id из instances. Предел комиссии действует для каждого вызова. Фактическую комиссию рассчитывает нода. Каждый пополненный экземпляр имеет собственные счётчики и баланс.

На ноде расходующего кошелька добавьте публичное раскрытие в наблюдение и проверьте выплату:

parano1d-cli contract watch budget.opening.json
parano1d-cli contract instances budget.opening.json
parano1d-cli contract call budget.opening.json <slot> <creation-id> --pay 0.1 --pay-to <recipient-o1-address> --preview

Проверьте полномочия, комиссию, выплату, остаток и преемника. Отправьте операцию с проверенным ID транзакции:

parano1d-cli contract call budget.opening.json <slot> <creation-id> --pay 0.1 --pay-to <recipient-o1-address> --expected-txid <reviewed-txid> --out call-1.json

CLI связывает предпросмотр с точной высотой и транзакцией, сохраняет его до авторизации, ждёт подтверждения и записывает call-1.receipt. Изменение высоты или транзакции требует нового предпросмотра. Для следующего вызова используйте преемника из call-1.json и заново найдите его текущий экземпляр:

parano1d-cli contract instances call-1.json
parano1d-cli contract verify call-1.receipt

На высоте дедлайна кошелёк восстановления может закрыть текущего преемника:

parano1d-cli contract watch call-1.json
parano1d-cli contract call call-1.json <successor-slot> <successor-creation-id> --close --preview
parano1d-cli contract call call-1.json <successor-slot> <successor-creation-id> --close --expected-txid <reviewed-close-txid> --out closing.json

Сохраняйте публичные условия, файлы преемников и чеки. Чеки аутентифицируют исторические вызовы после удаления тел блоков. Текущие права расходования проверяются по State. См. чеки и восстановление.

Язык

contract Name {
    param amount: u64;
    const limit: u64 = amount + 1;
    state remaining: u64 = limit;
    state calls: u64 = 0;

    policy {
        // All policy fields are explicit; see examples/budget.pruv.
    }

    call {
        when !terminal {
            require payout <= remaining;
            remaining -= payout + fee;
            calls += 1;
        }
    }

    ensures remaining <= old(remaining);
}

Полный исходник находится в noid_pruv/examples/budget.pruv.

• param объявляет внешний параметр u64, bool или address.
• const объявляет значение времени компиляции. Константы могут использовать параметры и предшествующие константы. Начальное состояние и выражения политики также используют значения времени компиляции.
• state объявляет до двух постоянных значений u64 в порядке регистров. Неиспользуемые постоянные регистры начинаются с нуля и сохраняют его.
• Присваивания выполняются в порядке исходника. += и -= обновляют выбранное значение состояния.
• + и - используют проверяемую арифметику u64. Переполнение или отрицательный результат отклоняют вызов. Ошибки такой арифметики в константах отклоняются при компиляции.
• min(a, b) и max(a, b) возвращают u64. Сравнения ==, !=, <, <=, > и >= возвращают bool. ! инвертирует bool.
• when condition { ... } вычисляет условие один раз при входе. Вложенный блок выполняется при выполнении условий всех окружающих блоков. Арифметика пропущенных ветвей неактивна.
• require condition; добавляет нативную проверку runtime. Ложное утверждение отклоняет вызов.
• ensures condition; объявляет постусловие для pruv verify. old(name) обозначает значение переменной состояния при входе в вызов. Постусловия являются спецификациями проверки в исходнике.

Контекст только для чтения: height, fee, payout, retained, input_amount, before_deadline, after_deadline, terminal, has_payout, input_creation_id, input_slot, retained_slot, payout_slot и payout_owner0 по payout_owner3. Дедлайн использует высоту включения. before_deadline означает height < deadline_height.

Имена параметров, констант и переменных состояния различаются. Имена контекста, ключевые слова и имена сырых регистров зарезервированы. Исходник ограничен 64 KiB, 8192 токенами и 64 уровнями вложенности. Выражения и условия также должны помещаться в нативные бюджеты временных регистров и инструкций. Грамматика содержит декларации контракта, последовательные инструкции и условные блоки.

Поля политики и соглашения нативных выходов описаны в API контрактов и целочисленном ядре.

Нативные инструкции

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

noid_pruv/examples/instructions.pruv компилируется в 13 инструкций и заполнение, охватывая все десять нативных кодов операций. Пример проверяет арифметику, сравнения, снимки условий и порядок инструкций. Пример бюджета использует три инструкции.

Проверка постусловий

Установите Z3 и добавьте z3 в PATH или передайте --z3 /path/to/z3. Для просмотра или отдельного запуска точного запроса:

target/release/pruv smt noid_pruv/examples/budget.pruv --params budget.params.json --out budget.smt2
z3 budget.smt2

Ожидаемые ответы: sat и unsat. Первый устанавливает существование успешного целочисленного исполнения. Второй устанавливает выполнение всех объявленных постусловий для каждого успешного целочисленного исполнения при семантике QF_BV Z3 и закодированной семантике инструкций ABI 3.

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

Это свойство одного вызова скомпилированной целочисленной программы. Например, remaining <= old(remaining) выполняется для успешных вызовов бюджета. Ограничение всех достижимых состояний дополнительно требует начального состояния и индуктивного сохранения. Проверка приложения также охватывает политику расходования, разрешённые ветви и получателей. Соответствие исходника инструкциям проверяется сравнением с нативным интерпретатором в тестах.

Для бюджета начальное remaining = budget и сохранение remaining <= old(remaining) устанавливают remaining <= budget после любого числа успешных продолжающих вызовов, если каждый переход использует ту же программу и аутентифицированное состояние преемника. Проверяемое вычитание remaining -= payout + fee также даёт remaining + cumulative payouts + cumulative fees = initial budget для этих вызовов. Восстановление закрывает экземпляр, а конечный выход следует отдельно зафиксированной политике расходования. Полное доказательство жизненного цикла охватывает инициализацию, каждый допустимый переход и закрытие.

Верификатор принимает определённые результаты. Контрпримеры, невыполнимые программы, отсутствие Z3, ошибки решателя и таймауты приводят к отказу проверки. Лимит решателя составляет 10 секунд на запрос, общий лимит процесса 30 секунд.

Тесты

cargo test -p noid_pruv
PRUV_TEST_Z3=/path/to/z3 cargo test -p noid_pruv -- --include-ignored

Тесты сравнивают исполнение исходника с существующим нативным интерпретатором на границах u64 и комбинациях ветвей. Тесты решателя охватывают верные свойства, намеренно неверные свойства и невыполнимые программы.

Типизированные запросы токенов, торговли и NFT описаны в нативных финансовых шаблонах.