Quando L = D + pQ não é suficiente: reparo de exatidão para embalagens BN254 – zk-s(nt)arks

DR

• Uma linha de quociente diferido do formulário L = D + pQ sobre \mathbb{F}_r não é, por si só, uma instrução de divisão inteira.

• Se P é deixado ilimitado, essa linha pode ser algebricamente vazia no campo externo.

• Para uma família de wrappers BN254/M31 concreta, ligação de intervalo de quociente + ligação de resíduo canônico + limites sem quebra restauram linha exata \mathbb{Z} semântica.

• Em uma comparação Halo2 de entrada compartilhada limitada, a construção reparada permanece consistentemente mais rápida e muito menor em RSS do que uma linha de base explícita de decomposição de bits.

A questão

A superfície central é a equação de linha de quociente diferido

L = D + pQ \quad \text{over } \mathbb{F}_r.

Por si só, essa equação de campo é não uma instrução inteira. Se p é invertível no campo externo e P é deixado ilimitado, o provador pode definir

Q = p^{-1}(LD)

e satisfazer a relação de linha em \mathbb{F}_r sem estabelecer a semântica da divisão euclidiana sobre \mathbb{Z}.

Este post é sobre essa lacuna de exatidão e um reparo algébrico leve para uma família de invólucros de concreto BN254/M31.

Escopo

A reivindicação aqui é:

1. a igualdade do quociente diferido pode ser algebricamente vazia no nível do campo externo;

2. ler L = D + pQ como uma identidade inteira exata, são necessárias premissas faltantes explícitas;

3. para uma família de invólucros de concreto BN254/M31, essas premissas podem ser reforçadas com um reparo algébrico leve.

A afirmação de referência segue o mesmo limite:

• este é um comparação de família instanciada limitada,

• não é uma reivindicação de equivalência semântica de domínio completo em cada realização do wrapper.

A declaração em nível de teorema

Para que a igualdade do campo se eleve a uma identidade exata em \mathbb{Z}a nota exige:

Sob essas condições, uma relação de linha satisfeita em \mathbb{F}_r eleva para

\widehat{L} = \widehat{D} + p\widehat{Q} \quad \text{in } \mathbb{Z},

e nas linhas de resíduos designadas, o par resíduo/quociente torna-se o único resto/quociente euclidiano.

Portanto, o manuscrito prova uma teorema da exatidão rowwise do modelo restrito para uma família BN254 de concreto com um membro 31/66classes de quociente de -bit. É um resultado em nível de teorema sobre exatidão algébrica. Extração de transcrição de back-end, solidez no nível PCS, fechamento Fiat-Shamir e paridade no nível do wrapper são questões separadas e não são o assunto desta nota.

O que o reparo realmente adiciona

Em um nível superior, o reparo adiciona três coisas às linhas do quociente diferido:

1. Ligação de quociente. A testemunha quociente é forçada para a pequena classe canônica pretendida, de modo que a testemunha genérica do campo externo Q = p^{-1}(LD) não é mais admissível.

2. Ligação de resíduo canônico. Nas linhas de resíduos designadas, o resíduo está vinculado ao seu representante canônico, de modo que a linha não é mais compatível com aliases arbitrários em nível de campo da mesma classe de congruência.

3. Controle sem envoltório. Os limites no-wrap familiares garantem que, uma vez que ambos os lados sejam elevados para números inteiros, a igualdade de campo satisfeita seja forçada a ser a identidade inteira exata, em vez de uma congruência agrupada.

Concretamente, a construção de reparo avaliada liga as células de quociente e as células de estilo de resíduo com um padrão pesado de pesquisa, em vez de uma decomposição de bits explícita e completa. Na instanciação atual, o lado do quociente é dividido em pequenos pedaços vinculados à pesquisa em vez de uma ampla decomposição booleana, e o lado do resíduo substitui uma ligação de estilo booleano 31 por um pequeno número de pesquisas de tabela mais uma porta de estilo de não igualdade, como (xp)\nu_x = 1; a auditoria sem wrap justifica então o aumento do número inteiro. Essa é a principal razão pela qual é interessante comparar com o A_secure linha de base em primeiro lugar.

Evidência de referência

Após o rascunho do manuscrito, executei um pacote de benchmark Halo2 comparando:

• A_secure: uma linha de base explícita de decomposição de bits,

• B_note: a construção de reparo algébrico.

Ambos os braços percorrem o mesmo caminho de prova Halo2, a mesma família de transcrições, o mesmok contrato e os mesmos perfis de entrada compartilhados.

Reexecuções repetidas de entrada compartilhada em k = 17

Para as reprises voltadas para a paridade em k_\mathrm{corrida}=17eu medi:

• \matrm{escala}=1,4,8,16,32,

• ambos boundary e standard,

• \matrm{repete}=3.

Entre esses pontos:

• B_note relação tempo de prova permaneceu na faixa 0.821 para 0.884,

• B_note a proporção de tempo de verificação permaneceu no intervalo 0.631 para 0.716,

• B_note RSS ficou em cerca de 0.285 para 0.286 de A_secure.

Portanto, dentro do atual fixo-kregime de índice de referência de insumos compartilhados, B_note mostra uma vantagem de tempo de prova e memória bastante consistente.

Primeiro k verificação repetida de salto e pós-salto

Eu também verifiquei onde o chicote público atual para de caber dentro k = 17.

Para este contrato de referência:

• \matrm{escala}=4519 ainda se encaixa k_\min=17,

• \matrm{escala}=4520 é o primeiro ponto que força k_\min=18.

Esta é uma propriedade do chicote atual.

Então executei a primeira validação repetida pós-salto em:

Isso produziu:

• A_secure prove ~32.37 s,

• B_note prove ~26.71 s,

• B/A prove ~0.825,

• A RSS ~6.30 GB,

• B RSS ~1.79 GB,

• B/A RSS ~0.285.

Portanto a vantagem persiste além do primeiro k pule também, pelo menos para esta verificação mínima repetida pós-salto.

Ligações