O Halo2 é um sistema de provas de conhecimento zero (ZKP) interativo e de código aberto, desenvolvido em Rust e baseado no algoritmo PLONK.

GitHub: halo2

Diferente de frameworks de desenvolvimento tradicionais, no Halo2 o desenvolvimento de funcionalidades é chamado de desenvolvimento de circuitos. Nesse paradigma, os circuitos são projetados e registrados usando tabelas que contêm uma série de restrições para validar operações e gerar provas.

Aritmetização PLONK

Os principais conceitos da aritmetização PLONK incluem:

• Uso de tabelas para projetar e registrar operações, com colunas personalizáveis quanto ao tipo e quantidade (mais colunas significam maior custo) > - Campo finito com número limitado de linhas (geralmente potências de 2, como 2^32)
• Quatro tipos de colunas diferentes:
  • Advice: Valores privados (parâmetros do processo de cálculo do prover)
  • Fixed: Constantes públicas (valores fixos)
  • Selector: Selecionadores que determinam se uma restrição específica está ativada em determinada linha
  • Instance: Entradas/saídas públicas
• Relações enntre células: Além das operações computacionais, as células devem incluir múltiplas restrições para validar o processo de cálculo e gerar provas:
  • Restrições de porta customizadas: Descrevem relações entre células usando polinômios iguais a zero, como s_mul * a * b - r = 0
  • Restrições de tabela de lookup: O valor da célula deve ser um item de uma lista de lookup conhecida
  • Restrições de constante: O valor da célula deve ser um valor fixo (constante)

Conceitos Fundamentais

• Chip: Geralmente implementa uma única instrução (operação). Além do cálculo propriamente dito, um chip deve implementar métodos como carregar valores privados (entrada), carregar constantes (entrada) e expor resultados (saída).
  • Características de Instruções do Chip
• Circuito: Um aplicativo (sistema de prova) desenvolvido pelo programador que contém um conjunto de funcionalidades. O prover pode executar cálculos especificados, gerar uma prova (Proof) para ser verificada pelo verificador.
  • Um circuito pode conter subcircuitos, gadgets (combinação de instruções) e chips (operação única)
  • A configuração de um circuito é semelhante à de gadgets e chips, incluindo o número e tipo de colunas usadas e a lista de restrições

Exemplo Simples

Exemplo: Provar o cálculo \(3a^2b^2=c\)

Design do Circuito e do Chip

Implementando um Chip de Multiplicação

Para implementar este cálculo polinomial, precisamos de um chip chamado CalculadoraChip com funcionalidade de multiplicação. Em sistemas de provas de conhecimento zero, além da multiplicação, precisamos incluir entrada (carregar valores privados, carregar constantes) e saída (expor resultados calculados).

Características das Instruções do Chip

As características das instruções do chip são a interface abstrata que o chip deve implementar. Para o chip de multiplicação CalculadoraChip, as características necessárias são:

trait OperacoesNumericas<f: field="">: Chip<f> {
    type Numero; // Define o tipo numérico
    // Carregar valor privado do prover
    fn carregar_privado(&self, organizador: impl Layouter<f>, valor: Value<f>) -> Result<:numero error="">;
    // Carregar constante, como 3
    fn carregar_constante(&self, organizador: impl Layouter<f>, constante: F) -> Result<:numero error="">;
    // Calcular multiplicação
    fn multiplicar(&self, organizador: impl Layouter<f>, a: Self::Numero, b: Self::Numero) -> Result<:numero error="">;
    // Expor resultado calculado publicamente
    fn expor_publico(&self, organizador: impl Layouter<f>, num: Self::Numero, linha: usize) -> Result<(), Error>;
}
</f></:numero></f></:numero></f></:numero></f></f></f></f:>

Declaração de Configuração do Chip

A configuração do chip é essencialmente uma declaração do número de colunas usadas, seus tipos e a lista de restrições (relações entre células). Normalmente, um chip também inclui uma classe de Selector para ativar/desativar certas restrições em certas linhas.

Para economizar custos, colocaremos o resultado da multiplicação diretamente na primeira coluna da próxima linha, economizando uma coluna. A configuração das colunas é:

O código de configuração do chip é:

struct ConfigCalculadora {
    advice: [Column<advice>; 2], // Armazena a e b durante o cálculo
    instance: Column<instance>,  // Entrada/saída do verificador
    s_mul: Selector,  // Selecionador - ativa/desativa a restrição de multiplicação
}
</instance></advice>

Implementação da Funcionalidade do Chip

Implementando as Características Básicas do Halo2

// Declaração da estrutura do chip
struct CalculadoraChip<f: field=""> {
    config: ConfigCalculadora,
}

// Implementando funcionalidades básicas do Halo2: config & loaded
impl<f: field=""> Chip<f> for CalculadoraChip<f> {
    type Config = ConfigCalculadora;
    type Loaded = ();

    fn config(&self) -> &Self::Config { 
        &self.config 
    }
    
    fn loaded(&self) -> &Self::Loaded { 
        &() 
    }
}
</f></f></f:></f:>

Implementnado Configuração e Restrições do Chip

impl<f: field=""> CalculadoraChip<f> {
    // Método de construção
    fn construir(config: <self as="" chip="">>::Config) -> Self { 
        Self {config} 
    }
    
    // Configuração e criação de restrições
    fn configurar(meta: &mut ConstraintSystem<f>, advice: [Column<advice>; 2], instance: Column<instance>, constante: Column<fixed>) 
        -> <self as="" chip="">>::Config {
        meta.enable_equality(instance);  // Habilitar verificação de igualdade
        meta.enable_constant(constante); // Habilitar verificação de constante
        for coluna in &advice { 
            meta.enable_equality(*coluna); 
        }  // Habilitar verificação de igualdade

        let s_mul = meta.selector();  // Inicializar o selecionador
        // Criar restrição de porta customizada
        meta.create_gate("multiplicacao", |meta| {
            let s_mul = meta.query_selector(s_mul);  // Obter dados da coluna do selecionador
            let a = meta.query_advice(advice[0], Rotation::cur());  // Obter dados da coluna advice[0] na linha atual
            let b = meta.query_advice(advice[1], Rotation::cur());  // Obter dados da coluna advice[1] na linha atual
            let r = meta.query_advice(advice[0], Rotation::next()); // Obter dados da coluna advice[0] na próxima linha
            // Fechamento - retorna a lista de restrições
            vec![s_mul * (a * b - r)]
        });
        ConfigCalculadora { advice, instance, s_mul } // Retorna a configuração do chip
    }
}
</self></fixed></instance></advice></f></self></f></f:>

Métodos comuns do sistema de restrições ConstraintSystem (parâmetro meta):

• enable_equality(): Habilita verificação de igualdade
• enable_constant(): Habilita verificação de constante
• selector(): Cria um selecionador
• query_advice: Consulta o valor da célula de uma coluna Advice, na linha atual (cur) ou na próxima linha (next)

Implementando as Características das Instruções do Chip

// Define o tipo numérico necessário para CalculadoraChip
struct Numero<f: field=""> (AssignedCell<f f="">);

impl<f: field=""> OperacoesNumericas<f> for CalculadoraChip<f> {
    type Numero = Numero<f>;
    
    // Carregar dados privados - o prover preenche os valores na tabela
    fn carregar_privado(&self, organizador: impl Layouter<f>, valor: Value<f>) -> Result<:numero error=""> {
        let config = self.config();
        organizador.assign_region(|| "Carregar dados privados", |mut regiao| {
            regiao.assign_advice(|| "Entrada privada", config.advice[0],  0, || valor).map(|op| Numero(op))
        })
    }
    
    // Carregar dados constantes
    fn carregar_constante(&self, organizador: impl Layouter<f>, constante: F) -> Result<:numero error=""> {
        let config = self.config();
        organizador.assign_region(|| "Carregar dados constantes", |mut regiao| {
            regiao.assign_advice(|| "Valor constante", config.advice[0], 0, || constante).map(|op| Numero(op))
        })
    }
    
    // Cálculo de multiplicação
    fn multiplicar(&self, organizador: impl Layouter<f>, a: Self::Numero, b: Self::Numero) -> Result<:numero error=""> {
        let config = self.config();
        organizador.assign_region(|| "Multiplicacao", |mut regiao| {
            config.s_mul.enable(&mut regiao, 0)?;  // Habilitar o selecionador s_mul - erro causa panic!
            // Copiar o valor do parâmetro a para a coluna advice[0]
            a.0.copy_advice(|| "a", &mut regiao, config.advice[0], 0)?;
            // Copiar o valor do parâmetro b para a coluna advice[1]
            b.0.copy_advice(|| "b", &mut regiao, config.advice[1], 0)?;
            // Calcular a * b
            let r = a.0.value().copied() * b.0.value();
            regiao.assign_advice(|| "r", config.advice[0], 1, || r).map(|op| Numero(op))
        })
    }
    
    // Expor (saída) o resultado
    fn expor_publico(&self, organizador: impl Layouter<f>, num: Self::Numero, linha: usize) -> Result<(), Error> {
        let config = self.config();
        organizador.constrain_instance(num.0.cell(), config.instance, linha)
    }
}
</f></:numero></f></:numero></f></:numero></f></f></f></f></f></f:></f></f:>

Método .map(): Método integrado de Option, semelhante a match, usado para lidar com ramificações de múltiplas condições.

Métodos comuns do organizador Layouter, da região Region e da célula atribuída AssignedCell:

• layouter.assign_region(nome, assignment): Atribui uma região
• layouter.constrain_instance(celula, coluna, linha): Restringe a coluna de saída instence
• regiao.assign_advice(anotacao, coluna, deslocamento, para): Atribui um valor a uma célula da coluna Advice
• celula_atribuida.copy_advice(anotacao, coluna, deslocamento): Copia o valor da célula para a coluna advice

Construindo o Circuito

Como este exemplo é simples, a configuração do circuito é idêntica à configuração do chip.

Declaração do Circuito

struct MeuCircuito<f: field=""> {
    constante: F,
    a: Value<f>,
    b: Value<f>
}
</f></f></f:>

Implementando as Características do Circuito

impl<f: field=""> Circuit<f> for MeuCircuito<f> {
    type Config = ConfigCalculadora;
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self { 
        Self::default() 
    }
    
    // Configuração do circuito - extrai dados do sistema de restrições meta, gera a configuração do chip Calculadora
    fn configure(meta: &mut ConstraintSystem<f>) -> Self::Config {
        // Configurar colunas advice, instance e constante
        let advice = [meta.advice_column(), meta.advice_column()]; // usa duas colunas advice
        let instance = meta.instance_column();
        let constante = meta.fixed_column();  // constante é fixed_column()
        CalculadoraChip::configurar(meta, advice, instance, constante)  // Retorna a configuração do chip Calculadora
    }
    
    // Síntese do circuito (ponto de entrada da execução do circuito) - implementa o polinômio a^2 * b^2 = c
    fn synthesize(&self, config: Self::Config, mut organizador: impl Layouter<f>) -> Result<(), Error> {
        let calculadora_chip = CalculadoraChip::<f>::construir(config); // Chamar método de construção - gera objeto chip Calculadora
        
        // 1. Carregar dados privados
        //  1.1 Carregar (preencher na tabela) dados privados a e b - o prover preenche os valores de a e b na tabela
        let a = calculadora_chip.carregar_privado(organizador.namespace(||"Carregar a"), self.a);
        let b = calculadora_chip.carregar_privado(organizador.namespace(||"Carregar b"), self.b);
        //  1.2 Carregar (preencher na tabela) constante Field
        let constante = calculadora_chip.carregar_constante(organizador.namespace(||"Carregar constante Field"), self.constant)?;
        
        // 2. Operações de multiplicação: usar o chip para calcular a^2 * b^2 * 3 = c que pode ser transformado em (a*b)^2 * 3 = c, com menos etapas e menor custo
        let ab = calculadora_chip.multiplicar(organizador.namespace(|| "a*b"), a, b)?; // Calcular a*b
        let ab_ab = calculadora_chip.multiplicar(organizador.namespace(|| "ab*ab"), ab.clone(), ab)?;
        let c = calculadora_chip.multiplicar(organizador.namespace(|| "constante * ab_ab"), constante, ab_ab)?;
        
        // 3. Expor o resultado como um valor de entrada de circuito público
        calculadora_chip.expor_publico(organizador.namespace(||"Expor c"), c, 0)
    }
}
</f></f></f></f></f></f:>

Testando o Circuito

use halo2_proofs::dev::MockProver;  
use halo2curves::pasta::Fp;

fn main(){
    // Testar 3 * a^2 * b^2 = c, com a=4, b=5, c=1200
    let constante = Fp::from(3);
    let a = Fp::from(4);
    let b = Fp::from(5);

    // Usar dados privados - instanciar objeto do circuito
    let circuito = MeuCircuito { 
        constante, 
        a: Value::known(a), 
        b: Value::known(b) 
    };

    let k = 4; // Limite de linhas para execução do circuito 2^k=16 linhas
    // Cenário 1: c=1200 sucesso
    let mut entradas_publicas = vec![Fp::from(1200)]; // Verificador - entrada c=1200
    let prover = MockProver::run(k, &circuito, vec![entradas_publicas.clone()]).unwrap();  // Gerar prover simulado
    assert_eq!(prover.verify(), Ok(()));  // Afirmar que o prover pode verificar com sucesso
    
    // Cenário 2: c=1201 falha
    let mut entradas_publicas = vec![Fp::from(1201)]; // Verificador - entrada c=1201
    let prover = MockProver::run(k, &circuito, vec![entradas_publicas.clone()]).unwrap();  // Gerar prover simulado
    assert!(prover.verify().is_err());  // Afirmar que a verificação falha
}

Código completo: exemplo-simples.rs

Referências

• The halo2 Book
• halo2 - Tradução do The halo2 Book
• Github-halo2 Exemplo Simples
• Explicação Detalhada do Halo2
• Zero Knowledge Proof — A Guide to Halo2 Source Code | por Trapdoor-Tech | Medium