zk-SNARKs: Формальна верифікація методів пам'яті

При формальній верифікації системи zk-SNARKs обробка підсистеми пам'яті є ключовим викликом. На відміну від традиційних віртуальних машин, zkVM використовує таблиці виконання та допоміжні таблиці для представлення стану пам'яті, що вимагає спеціальних методів верифікації.

Система пам'яті zkWasm складається з таблиці виконання та таблиці пам'яті. Таблиця виконання фіксує процес виконання інструкцій, тоді як таблиця пам'яті зберігає всі історії доступу до пам'яті. Для спрощення розробки zkWasm надає абстрактний рівень, через функції alloc_memory_table_lookup_write_cell та alloc_memory_table_lookup_read_cell для роботи з пам'яттю.

У процесі верифікації ми розглядаємо таблицю пам'яті як змінну структуру даних, будуючи відображення адресних даних за допомогою функції memory_at. Це дозволяє довести, що обмеження, створені функцією alloc, еквівалентні операціям set і get над відображенням, що спрощує верифікацію інструкцій до форми, подібної до не-ZK інтерпретатора.

Щоб запобігти маніпуляціям з пам'яттю з боку зловмисників, zkWasm використовує механізм підрахунку для відстеження кількості дійсних записів. Таблиця виконання та таблиця пам'яті підтримують лічильники, які забезпечують узгодженість між ними. Це вимагає більшої точності під час перевірки, необхідно довести, що кожна інструкція відповідає правильній кількості записів у таблиці пам'яті.

! [Розширена формальна перевірка доказів з нульовим розголошенням: як довести пам'ять з нульовим розголошенням?] ](https://img-cdn.gateio.im/webp-social/moments-eef0b5eb2efc84aa949b89d178ed671c.webp)

Процес верифікації здійснюється зверху вниз і включає три етапи:

1. Оцінка кількості записів, які повинні бути створені командою
2. Доказати, що кількість записів у таблиці не перевищує очікувану
3. Доказати за допомогою індукції, що cum_mops та instructions_mops завжди узгоджені в таблиці

Цей детальний метод верифікації допомагає виявити потенційні помилки, такі як ключова проблема в механізмі підрахунку таблиці переходів.

Для реалізації модульної верифікації ми поділили систему на три незалежні частини: верифікацію схем інструкцій, верифікацію таблиці виконання та реалізацію таблиці пам'яті. Ця структура дозволяє кільком інженерам працювати паралельно, підвищуючи ефективність верифікації.

В цілому, хоча zkVM-верифікація має відмінності у обробці динамічного стану, завдяки узгодженню абстрактного рівня реалізації все ще можна застосовувати модульний підхід, подібний до верифікації традиційного інтерпретатора. Цей підхід мінімізує вплив відмінностей, що дозволяє кожній інструкції виконувати незалежну верифікацію на основі інтерфейсу get-set.