Certora официально подтверждает, что P-токен Solana эквивалентен токену SPL

Недавно развернутое обновление P-Token компании Solana представляет собой одно из самых значительных изменений в инфраструктуре сети за всю ее историю. Модернизация значительно сокращает вычислительные ресурсы, необходимые для операций с токенами, сохраняя при этом совместимость с существующей программой SPL Token.

Чтобы подтвердить это утверждение, Solana Foundation привлекла компанию Certora для проведения формальной проверки с целью доказать поведенческую эквивалентность между старой реализацией SPL Token и новой программой P-Token на базе Pinocchio. Компания Anza, занимающаяся исследованиями и разработками, ранее назвала формальную проверку "самой сильной гарантией" эквивалентности P-Token, а результаты Certora служат дополнительным подтверждением роли P-Token как "одноразовой" замены одной из наиболее широко используемых программ Solana.

Почему программа Token имеет значение

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

P-Token представляет новую реализацию, построенную на библиотеке Pinocchio Rust. Обновление обеспечивает значительное повышение производительности, снижая потребление вычислений примерно на 95-98 % для многих распространенных операций. Например, стандартная передача токена сокращается с 4 645 вычислительных единиц до всего лишь 76, а инструкции transfer_checked - с 6 200 вычислительных единиц до 105.

Такое повышение эффективности позволяет высвободить примерно 12-13 % пространства блокчейна в сети, создавая дополнительную емкость без увеличения лимитов на блокчейн.

Проблема доказательства возможности замены "под ключ"

Хотя повышение производительности привлекает внимание, совместимость остается самым важным требованием для модернизации инфраструктуры такого масштаба. Существующие кошельки, dApps, протоколы и смарт-контракты полагаются на поведение программы SPL Token. Любое неожиданное отклонение может вызвать проблемы с интеграцией или создать риски для разработчиков и пользователей.

P-Token не просто копирует оригинальную кодовую базу. Новая реализация использует другую архитектуру, включая доступ к учетной записи с нулевым копированием, оптимизированные пути выполнения и дополнительную функциональность. В результате разработчики не могли полагаться только на обычное тестирование для установления совместимости.

Вместо этого Certora использовала методы формальной верификации, чтобы математически проанализировать, одинаково ли ведут себя две программы при всех возможных входных данных в пределах заданной области проверки.

Что означает эквивалентность для P-Token?

Система верификации Certora оценивала три категории результатов для каждой анализируемой инструкции.

• Во-первых, ни одна из программ не должна паниковать во время выполнения; т. е. программа не должна аварийно завершаться или прерываться из-за ошибки, краевого случая и т. д.

• Во-вторых, если программа SPL Token успешно обрабатывает инструкцию и возвращает Ok(()), P-Token также должен возвращать Ok(()). В этих случаях обе программы должны оставлять данные счета в идентичном байт за байтом состоянии после выполнения.

• В-третьих, если P-Token возвращает ошибку, программа SPL Token должна вернуть ту же ошибку при тех же условиях.

Система Certora гарантирует, что для каждого возможного состояния входного счета и инструкции программа либо преуспевает (Ok(()), либо терпит изящный крах (Err(e)), но никогда не терпит внутреннего краха. Реализация P-Token разработана как надстройка над функциональностью SPL Token, то есть любая операция, принятая SPL Token, должна быть принята и P-Token.

В ходе проверки было выявлено несколько преднамеренных различий между двумя программами. P-Token позволяет делегату самостоятельно отзывать свои полномочия, не требуя от владельца токена подписывать транзакцию. SPL Token требует подписи владельца для выполнения того же действия.

P-Token также расширяет поддержку мультисиговых полномочий Token-2022. В то время как SPL Token отвергает такие счета, P-Token принимает их.

Третье отличие заключается в обработке ошибок, когда неправильно сформированные данные учетной записи содержат неканонические теги COption. SPL Token немедленно отклоняет такие аккаунты с ошибкой InvalidAccountData. Оптимизированный процесс загрузки аккаунта в P-Token проникает глубже в логику инструкции, прежде чем сгенерировать ошибку, что может привести к различным результатам в зависимости от выполняемой инструкции.

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

Как проходила верификация

Программа Certora Prover анализирует исходный код после компиляции в низкоуровневое промежуточное представление. Затем инженеры пишут формальные спецификации, используя язык Certora Verification Language for Rust, известный как CVLR.

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

В обзор вошли все инструкции, общие для SPL Token и P-Token, за исключением AmountToUiAmount и UiAmountToAmount. В обзор также не вошли три новые инструкции, специфичные для P-Token: batch, unwrap_lamports и withdraw_excess_lamports.

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

Выводы и результаты

Certora сообщила, что в ходе проверки не было обнаружено уязвимостей, которые можно было бы использовать. Анализ подтвердил, что свойства No Panics и Equivalence on Ok выполняются для всех инструкций, входящих в область применения, не требуя дополнительных предположений. Свойство Equivalence on Error также выполняется для всего общего набора инструкций при учете трех преднамеренных различий в поведении, выявленных ранее.

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

Значительная веха для инфраструктуры Solana

Результаты проверки были получены вскоре после развертывания P-Token в мейннете, обеспечивая дополнительную уверенность в одном из наиболее значимых обновлений инфраструктуры Solana.

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

Подробнее о SolanaFloor

Solana наконец-то получила нативную подписку на Onchain, разблокировав платежные ведомости, бюджеты агентов ИИ и периодические биллинги
Бывший кандидат в президенты США Эндрю Янг, Noble Mobile, приобретает Helium Mobile - что случится с $HNT?

Как IPO SpaceX на $2T повлияет на криптовалюты?