Как работает основанный на STARK процесс подтверждения выполнения в Miden V1?
3 июня 2022 г.Miden — это решение для реализации ZKVM, основанное на строгих технологиях.
На базовом уровне абсолютное доказательство генерируется на основе библиотеки ZKP, и доказательство будет проверено. Пунктирная часть на следующем рисунке 1 — это основная функция, реализованная в Miden. В основном состоит из трех компонентов.
1. Один набор компиляторов лексического синтаксиса, то есть лексический анализатор и синтаксический анализатор на рис. 1. Они могут программировать ассемблерные инструкции, определенные Миденом, в кодовый блок или код операции и значение операции, содержащиеся в блоке.
2. Один набор исполнителей инструкций, то есть исполнитель на рисунке 1. Он будет выполнять кодовый блок, а также код операции и значение операции, содержащиеся в блоке, в соответствии с определенными правилами. И выполненные результаты будут трассировкой выполнения, используемой для генерации доказательства.
3. Один набор AIR (абстрактное промежуточное представление), удовлетворяющий требованиям строгого доказательства, то есть AIR на рисунке 1. Он накладывает ограничения на процесс выполнения виртуальной машины Miden.
Рисунок 1. Компоненты проекта Miden
Конструктивный чертеж AIR
Ограничения AIR делятся на стек и декодер: на рис. 2 показаны ограничения стека, распределенные по стеку с максимальной глубиной 8 при инициализации.
max_depth увеличивается по мере необходимости, если начальное распределение может быть превышено во время выполнения, в зависимости от потребностей программы, но оно не должно превышать максимальную глубину 16, в противном случае сообщается об ошибке.
Рисунок 2: Столбец ограничения стека
Как видно ниже, на рисунке 3 показаны ограничения декодера. Среди этих ограничений op_counter, op_SPONGE, CF_OP_bits, LD_OP_BITS и hd_OP_bits представляют собой фиксированные длины столбцов.
op_sponge используется для ограничения порядка и правильности инструкций. cf_op_bits ограничивает 3-битное значение flow_ops. ld_op_bits и hd_op_bits ограничивают младшие 5 бит и старшие 2 бита user_ops соответственно.
ld_op_bits и hd_op_bits объединяются, чтобы сформировать исполняемый user_op, который также используется в качестве селектора для каждого шага ограничений состояния стека!
Рисунок 3: Столбец ограничений декодера
Пример выполнения виртуальной машины Miden
В этом разделе показана простая логика Мидена, иллюстрирующая выполнение виртуальной машины и создание трассировки выполнения Старка.
Следующий сегмент кода 1 является сегментом для выполнения: его логика выполнения состоит в том, чтобы поместить 3 и 5 в стек. Затем прочитайте флаг с ленты.
Проверьте, равен ли флаг 1 или 0. Если он равен 1, запустите «логику if.true», чтобы взять два числа 3 и 5, помещенные в стек, сложить их вместе, получив 8, и поместить 8 в стек. куча. Если это 0, запустите «иначе логику», чтобы взять числа 3 и 5 и перемножить их вместе, получив 15, а затем поместить 15 в стек.
```javascript
начинать
толчок.3
толчок.5
читать
если правда
добавлять
еще
мул
конец
конец
Сегмент кода 1
Окончательный код инструкции, проанализированный лексическим анализатором и синтаксическим анализатором Miden, показан в следующем сегменте кода 2:
```javascript
начинать
нуп-нуп-нуп-нуп-нуп-нуп-нуп
push(3) noop noop noop noop noop noop noop
push(5) читать noop noop noop noop noop noop
нуп-нуп-нуп-нуп-нуп-нуп,
если
утверждать добавить noop noop noop noop noop noop
нуп-нуп-нуп-нуп-нуп-нуп-нуп
еще
не утверждать мул нуп нуп нуп нуп
нуп-нуп-нуп-нуп-нуп-нуп-нуп
конец]
Сегмент кода 2
На рис. 4 показан процесс выполнения сегмента кода 2 виртуальной машиной.
Средняя часть представляет собой блок-схему исполнителя, выполняющего коды операций. Левые пунктирные линии относятся к трассировке декодера, сгенерированной при выполнении кода. Пунктирные линии справа относятся к трассировке стека, сгенерированной при выполнении кода.
На рисунке исполнитель выполняет выполнение блок за блоком в соответствии с кодовым блоком. В этом примере сначала выполняется блок span.
Затем выполняется структура if-else-end на шаге 32 для входа в блок switch и вставки губчатого хэша, сгенерированного при последнем выполнении предыдущего блока span, в ctx_stack. После того, как блок переключения выполнен, вставьте его в губку на шаге 49.
Рисунок 4: рисунок изменения состояния виртуальной машины, выполняющей код операции
Примечание. В этом документе описывается последняя версия основной ветки для проектов Miden по состоянию на 27 мая 2022 г. На данный момент следующая ветвь Miden провела большую переработку инструкций, а в AIR реализовано лишь несколько ограничений.
Ограничения стека
В этом разделе мы покажем условия ограничения основных инструкций пользователя, среди которых old_stack_x относится к значению, хранящемуся в позиции x стека перед выполнением инструкции, new_stack_x относится к значению, хранящемуся в позиции x стека. стек после выполнения инструкции, «->» относится к копированию значения из левой части стека в правую, а «==» относится к ограничению уравнения. Ограничения стека относительно просты и не требуют пояснений.
Инструкция по условию
Выбирать
Ограничение:
```javascript
new_stack_0 == (условие * x) + ((1 - условие) * y)
old_stack_0 == х
old_stack_1 == г
old_stack_2 == условие
старый_стек_3 --> новый_стек_1
старый_стек_n. --> новый_стек_n-2
aux_0 == condition.is_binary == истина
Если условие равно 1, x находится на вершине стека. Если условие равно 0, y находится на вершине стека.
Арифметическая инструкция
добавлять
Ограничение:
```javascript
old_stack_0 + old_stack_1 == new_stack_0
старый_стек_2 --> новый_стек_1
старый_стек_n. --> новый_стек_n-1
мульт
Ограничение:
```javascript
старый_стек_0 * старый_стек_1 == новый_стек_0
старый_стек_2 --> новый_стек_1
старый_стек_n. --> новый_стек_n-1
инв
Ограничение:
```javascript
старый_стек_0 * новый_стек_0 == 1
старый_стек_1 --> новый_стек_1
старый_стек_n. --> новый_стек_n
отрицательный
Ограничение:
```javascript
старый_стек_0 + новый_стек_0 == 0
старый_стек_1 --> новый_стек_1
старый_стек_n. --> новый_стек_n
Булевая инструкция
нет
Ограничение:
```javascript
aux_0: убедитесь, что old_stack_0 является двоичным
1-old_stack_0 == новый_stack_0
старый_стек_1 --> новый_стек_1
старый_стек_n. --> новый_стек_n
а также
Ограничение:
```javascript
aux_0: убедитесь, что old_stack_0 является двоичным
aux_1: убедитесь, что old_stack_1 является двоичным
старый_стек_0 * старый_стек_1 == новый_стек_0
старый_стек_2 --> новый_стек_1
старый_стек_n. --> новый_стек_n-1
или же
Ограничение:
```javascript
aux_0: убедитесь, что old_stack_0 является двоичным
aux_1: убедитесь, что old_stack_1 является двоичным
1- (1-old_stack_0) *(1- old_stack_1) == new_stack_0
старый_стек_2 --> новый_стек_1
старый_стек_n. --> новый_стек_n-1
Хэш-инструкция
RESCR
Предел хэш-функции, удовлетворяющий протоколу хэш-функции
Занимает 6 регистров.
Ограничение:
```javascript
hash(old_stack0, old_stack1, old_stack2, old_stack3, old_stack3, old_stack5) ==
(новый_стек0, новый_стек1, новый_стек2, новый_стек3, новый_стек3, новый_стек5)
старый_стек_6 --> новый_стек_6
старый_стек_n. --> новый_стек_n
Сравнить инструкцию
экв
Ограничение:
```javascript
aux_0 == new_stack_0 * diff == 0
new_stack_0 == 1- (old_stack_1-old_stack_2)*old_stack_0
old_stack_0 == inv(old_stack_1-old_stack_2)
старый_стек_3 --> новый_стек_1
старый_стек_n. --> новый_стек_n-2
комп
Сравните в соответствии с циклом длины в битах двух сравниваемых чисел, например:
А: [0,1,0,1]
Б: [0,0,1,1]
Инструкции сравнения необходимо выполнить четыре раза.
Ограничение:
```javascript
// расположение первых 8 регистров
// [pow, bit_a, bit_b, not_set, gt, lt, acc_b, acc_a]
// биты x и y являются двоичными
new_stack_1 == x_big_idx (lg lt flag) (тип: двоичный)
new_stack_2 == y_big_idx (lg lt flag) (тип: двоичный)
bit_gt = x_big_idx*(1-y_big_idx)
bit_lt = y_big_idx*(1-x_big_idx)
// трекеры сравнения были обновлены правильно
new_stack_3 = не_set_idx
new_stack_4(gt) == old_stack_4(gt_idx) + bit_gt * not_set_idx
new_stack_5(lt) == old_stack_5(lt_idx) + bit_lt * not_set_idx
// аккумуляторы бинарного представления обновлены корректно
old_stack_0 = POW2_IDX
old_stack_6 = Y_ACC_IDX
old_stack_7 = X_ACC_IDX
new_stack_6 == old_stack_6 + x_big_idx * old_stack_0(power_of_two);
new_stack_7 == old_stack_7 + y_big_idx * old_stack_0(power_of_two);
// когда регистр GT или LT установлен в 1, флаг not_set очищается
not_set_check = (1-old_stack_5(lt_idx))*(1-old_stack_4(gt_idx))
not_set_check == new_stack_3 (not_set_idx)
// регистр степени 2 был обновлен правильно
новый_стек[POW2_IDX] * два == старый_стек[POW2_IDX]
старый_стек_8 --> новый_стек_8
старый_стек_n --> новый_стек_n
Инструкция по работе со стеком
дуп.n
Ограничение:
```javascript
новый_стек_0 == старый_стек_0
новый_стек_n-1 == старый_стек_n-1
старый_стек_0 --> новый_стек_n
old_stack_k --> new_stack_n+k
менять
Ограничение:
```javascript
новый_стек_0 == старый_стек_1
новый_стек_1 == старый_стек_0
старый_стек_2 --> новый_стек_2
старый_стек_n --> новый_стек_n
ROLL4
Ограничение:
```javascript
новый_стек_0 == старый_стек_3
новый_стек_1 == старый_стек_0
новый_стек_2 == старый_стек_1
новый_стек_3 == старый_стек_2
старый_стек_4 --> новый_стек_4
старый_стек_n --> новый_стек_n
Условие ограничения комментария декодера
В этом разделе мы покажем условия ограничения основной инструкции операции потока.
Выполнение пользовательского кода
op_bits
Для ограничений cf_op_bits, ld_op_bits и hd_op_bits
Ограничение 1: каждый бит может быть только 0 или 1.
Ограничение 2: когда op_counter не равен 0, ld_ops и hd_ops не могут быть оба равны 0.
Ограничение 3: когда cf_op_bits равен hacc, состояние op_counter увеличится на 1.
Ограничение 4: инструкции BEGIN, LOOP, BREAK и WRAP должны быть выровнены в соответствии с 16.
Ограничение 5: инструкции TEND и FEND должны быть выровнены согласно 16.
Ограничение 6: Инструкция PUSH должна быть выровнена согласно 8.
Ограничение:
```javascript
cf_op_bits == двоичный
ld_op_bits == двоичный
hd_op_bits == двоичный
// ld_ops и hd_ops могут быть нулевыми на первом шаге, но не могут быть нулевыми на любом другом шаге
op_counter * двоичный_не (ld_bit_prod) * двоичный_не (hd_bit_prod) == 0
если op_counter != 0
(1-ld_bit_prod)*(1- hd_bit_prod) == 0
если is_hacc != истина
op_counter = текущий.op_counter
// BEGIN, LOOP, BREAK и WRAP разрешены только для одного числа меньше кратного 16
// TEND и FEND разрешены только для чисел, кратных 16
// PUSH разрешен только для чисел, кратных 8
комментарий hacc
Hacc, как и flowOps, всегда будет вызывать изменение состояния губки при выполнении этой инструкции, и поэтому он нужен для выполнения ограничений.
Ограничение:
```javascript
mds (sbox (old_sponge) + user_opcode (7 бит) + op_value (push_flag = 1)) == sbox (inv_mds (new_sponge))
Условное суждение
иметь тенденцию
Как ограничение конца истинной ветви if, оно разделено на две части:
Ограничение 1: ограничение состояния губки.
Значение наверху стека равно new_sponge_0. Губка после последнего выполнения истинной ветки if равна new_sponge_1. New_sponge_3 равен 0.
Ограничение 2: ограничение ctx_stack. Значение наверху стека равно new_sponge_0. Любой другой элемент стека переместится на одну позицию вверх стека.
Ограничение 3: ограничение loop_stack. Состояние loop_stack неизменно.
Ограничение:
```javascript
parent_hash = current.ctx_stack () [0]
block_hash = current.op_sponge()[0]
new_sponge = следующая.op_sponge()
parent_hash == new_sponge[0]
block_hash == новая_губка[1]
новая_губка[3] == 0
// сделать так, чтобы родительский хэш был извлечен из стека контекста
ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 для ограничения изображения цикла
ctx_stack_end = ctx_stack_start + ctx_stack_current.len()
ctx_result = результат &mut[ctx_stack_start..ctx_stack_end]
ctx_stack_current_0 = ctx_stack_next_1
ctx_stack_current_1 = ctx_stack_next_2
ctx_stack_current_n = ctx_stack_next_n+1
// копия loop_stack
диапазон копирования: ctx_stack_end в. ctx_stack_end + loop_stack_current.len()
loop_stack_current_0 = loop_stack_next_0
loop_stack_current_n = loop_stack_next_n
f_end
Как ограничение конца ложной ветви if, оно разделено на две части:
Ограничение 1: ограничение состояния губки. Значение наверху стека равно new_sponge_0.
Губка после последнего выполнения истинной ветки if равна new_sponge_2. new_sponge_3 равно 0.
Ограничение 2: ограничение ctx_stack. Значение наверху стека равно new_sponge_0. Любой другой элемент стека переместится на одну позицию вверх стека.
Ограничение 3: ограничение loop_stack. Состояние loop_stack не изменилось.
Ограничение:
```javascript
parent_hash = current.ctx_stack () [0]
block_hash = current.op_sponge()[0]
new_sponge = следующая.op_sponge()
parent_hash == new_sponge[0]
block_hash == новая_губка[2]
новая_губка[3] == 0
// сделать так, чтобы родительский хэш был извлечен из стека контекста
ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 для ограничения изображения цикла
ctx_stack_end = ctx_stack_start + ctx_stack_current.len()
ctx_result = результат &mut[ctx_stack_start..ctx_stack_end]
ctx_stack_current_0 = ctx_stack_next_1
ctx_stack_current_1 = ctx_stack_next_2
ctx_stack_current_n = ctx_stack_next_n+1
// копия loop_stack
диапазон копирования: ctx_stack_end в. ctx_stack_end + loop_stack_current.len()
loop_stack_current_0 = loop_stack_next_0
loop_stack_current_n = loop_stack_next_n
Оригинал