Como Otimizar seu Consumo de Gás Sem se Dar Mal

Um guia sobre o Verificador de Equivalência da Certora

Introdução: o Trilema Financeiro Distribuído

Há um crescente consenso de que um dos principais obstáculos a serem superados pelo mundo das Finanças Descentralizadas (DeFi) é o problema da segurança dos contratos inteligentes.

De fato, quando o ciclo de notícias é dominado por histórias de fraude e perda, a adoção mainstream mais ampla permanece uma perspectiva distante, sem falar em uma verdadeira concorrência com os atuais serviços financeiros e gigantes de bancos de investimento como Visa, J.P. Morgan e Goldman-Sachs.

Contrariando o que muitas pessoas fora da comunidade Blockchain dizem, este problema não é simplesmente um produto de projetos superestimados com prazos insanos ou startups com uma cultura de “programação cowboy” (trabalhar de forma independente e sem seguir as práticas padrões ou metodologias formais de desenvolvimento).

Esses fatores, amplamente divulgados, certamente existem em alguns casos e definitivamente não ajudam. No entanto, atribuir a culpa apenas a eles é um absurdo completo, como qualquer pessoa dentro da comunidade Blockchain pode confirmar.

É, na verdade, muito pior.

Isso ocorre porque desenvolver um produto DeFi é um problema de engenharia de profundidade enganosa — é fácil escrever um contrato inteligente em Solidity que (principalmente) faça o que você quer, mas é difícil fazê-lo bem. Muito parecido com o famoso Trilema da Blockchain de Vitalik Buterin, o processo de desenvolvimento de contratos inteligentes também é guiado por três objetivos separados e frequentemente conflitantes:

• Minimizar o consumo de gás. Como no comércio de alta frequência, otimizações aparentemente "triviais" podem ter implicações de longo alcance para o custo do gás e, portanto, para a usabilidade. Após esgotar o usual "conjunto de truques", melhorar o custo do gás de várias operações muitas vezes exige escrever em Assembly em vez de Solidity (ou Viper) ou encontrar truques inteligentes para calcular aproximações para funções não lineares e pesadas computacionalmente.
• Maximizar a segurança. Como hardware, os contratos inteligentes são imutáveis por design, o que significa que qualquer bug introduzido no processo de desenvolvimento é definitivo. É verdade que existem contratos atualizáveis que podem contornar a imutabilidade. No entanto, sua presença introduz outra compensação: os usuários nunca têm certeza de que o contrato com o qual interagem não mudará, e com cada atualização vem o risco de introduzir novos bugs. Combinado com as grandes quantias de dinheiro geridas pelos protocolos DeFi e o inerente desacoplamento dos endereços EOA e identidades do mundo real (bem como a filosofia "Código é Lei"), essas realidades podem tornar qualquer vulnerabilidade no código extremamente perigosa e cara. Em particular, significa que se deve ter muito cuidado com erros de arredondamento, casos extremos e problemas de design matemático.

• Minimizar o tempo de chegada ao mercado. Este é um assunto urgente em qualquer projeto de software, mas ainda mais no mundo extremamente competitivo e altamente volátil das finanças descentralizadas. Infelizmente, mesmo que alguém conseguisse alcançar o objetivo de otimização de gás e segurança simultaneamente, está claro que as verificações adicionais impostas em cada etapa desacelerariam consideravelmente o processo de desenvolvimento.

Verificação Formal no Ciclo de Desenvolvimento

Para ajudar os desenvolvedores a alcançar um melhor equilíbrio sem comprometer um desses três requisitos, a Certora tem desenvolvido um novo produto chamado Equivalence Checker, ou Verificador de Equivalência. Diferente do Provador (Prover) Certora, que é focado em testes e segurança, essa verificação formal leve permite que programadores DeFi comparem diferentes versões da mesma fórmula matemática escrita em:

1. baixo nível (Yul ou Assembly)
2. alto nível (Solidity)
3. lógica pura (codificado na Linguagem de Verificação da Certora ou CVL, para abreviar)

e mostre que elas são equivalentes (mais detalhes abaixo). Pretende-se que seja usado como uma ferramenta de desenvolvimento rápido durante todo o ciclo de vida do projeto e que ajude tanto com segurança, tempo de desenvolvimento, quanto com o consumo de gás.

O restante deste post demonstra o fluxo de trabalho desta nova ferramenta em um caso concreto. Explicamos sobre os diferentes modos do Equivalence Checker e demonstramos como ele foi capaz de detectar imediatamente um antigo bug famoso, bem como um novo bug, anteriormente desconhecido, em código ao vivo (observação: os leitores devem notar que este é um bug de baixa gravidade escolhido para fins didáticos. Na sequência deste blog, revelaremos e analisaremos um caso mais elaborado onde um bug de alta gravidade foi detectado usando o Equivalence Checker — então, fiquem atentos para mais!)

Mas primeiro,

O que exatamente significa 'equivalência funcional'?

Uma função Solidity/Yul é dita pura se não ler ou modificar o estado (no entanto, pode reverter potenciais mudanças de estado se ocorrer um erro). Pode ter múltiplos valores de entrada e saída. Por exemplo, a seguinte função é pura:

function safeAdd(uint a, uint b) public pure returns (uint c) {
    c = a + b;
    require(c >= a);
}

Diremos que duas funções puras f(...) e g(...) são equivalentes se:

1. Elas têm as mesmas variáveis de entrada/saída.

2. [presumindo que 1 se mantém:] para um determinado conjunto de valores de entrada -

(a) f reverte se e somente se g reverte.

(b) [presumindo que f e g não reverteram:] os valores de retorno de f e g são idênticos.

Claro, esta definição pode ser estendida para fragmentos adequados do bytecode EVM e tornada precisa no formalismo do Yellow Paper da Ethereum (a equivalência entre uma função pura e uma fórmula lógica é semelhante, mas um pouco mais sutil e melhor explicada pelo segundo exemplo abaixo).

Agora que definimos adequadamente a equivalência, é hora de começar nossa discussão de fato.

Contexto: implementando divisão de ponto fixo

É de conhecimento geral que a Ethereum Virtual Machine (EVM) suporta nativamente apenas dois tipos de dados: a palavra de 256 bits e o byte de 8 bits. Além disso, a maioria dos opcodes (códigos de operação) da EVM lida com pedaços de dados de tamanho de palavra de cada vez, incluindo todos os matemáticos. Assim, basicamente existem apenas dois tipos de dados numéricos na Ethereum:

• inteiros de 256 bits com sinal e
• inteiros de 256 bits sem sinal,

que são representados em Solidity pelos tipos de dados uint256 e int256, respectivamente.

Isso é lamentável, pois virtualmente qualquer tipo de aplicação financeira precisa implementar algum suporte para aritmética fracionária. Existem algumas maneiras diferentes de fazer isso, mas a mais popular em aplicações DeFi (de longe) é números de ponto fixo. Estes são basicamente frações simples cujo denominador é uma constante predefinida, geralmente uma potência de 2 ("binário") ou 10 ("decimal"). As escolhas padrão de denominador no caso decimal são 10¹⁸ (conhecido como "wad") ou 10²⁷ (um "ray"). Assim, as bibliotecas fixas de ponto em Solidity muitas vezes representam um wad como um inteiro de 256 bits. Isso é bastante direto para adição e subtração, mas ao realizar multiplicação ou divisão, é preciso reescalar o resultado para obter a resposta correta.

Por exemplo,

1,5 * 2,7 == 4,05 
// A aritmética regular de inteiros adiciona ordens de magnitude: 
150 * 270 == 40500 
// A aritmética Wad não adiciona ordens de magnitude: 
wadMul(1,5 ether, 2,7 ether) == 4,05 ether

Considere o seguinte caso de teste. Queremos escrever uma função wadDiv que divide dois wads, arredondando meio wad para cima até o wad mais próximo. Esses tipos de funções aritméticas são muito comuns em DeFi. Eles são necessários para levar em conta a diferença entre como a aritmética de inteiros se comporta normalmente e como a aritmética decimal deveria realmente funcionar.

Passo 1: Teste o código

Como primeiro passo, consideramos a seguinte implementação de referência para wadDiv escrita em Solidity:

uint256 internal constant WAD = 1e18;
function wadDivSol(uint256 a, uint256 b) public pure returns (uint256 c)
{
 c = (a * WAD + (b/2)) / b;
 return c;
}

Na tentativa de otimizar, brincamos um pouco com o Assembly e criamos a seguinte versão provisória em Yul:

function wadDivAsm(uint256 a, uint256 b) public pure returns (uint256 c)
{
 assembly
 {
   if iszero(iszero(gt(a, div(sub(not(0), div(b, 2)), WAD))))
   { revert(0, 0) }
   c := div(add(mul(a, WAD), div(b, 2)), b)
 }
}

e de fato vemos uma redução substancial nos custos de gás: a versão Solidity requer ~860 de gás para realizar o cálculo enquanto a versão Assembly gasta apenas ~140 de gás.

Pergunta. Isso funciona (ou seja, essas duas funções são equivalentes)?

Em vez de quebrar nossas cabeças tentando encontrar a resposta, o modelo de regras genéricas do Equivalence Checker imediatamente produz as seguintes duas regras, escritas em CVL (Certora Verification Language), e as submete ao Provador para verificação formal.

Quase imediatamente, o provador detecta uma discrepância entre as duas condições de reversão:

e apresenta o seguinte contraexemplo:

(Por quê? Porque a divisão por zero em Yul retorna zero em vez de reverter! Veja o tópico vinculado no Twitter para uma discussão detalhada)

Passo 2: Teste a lógica

Suponha que agora tenhamos corrigido o bug e escrito uma nova versão em Yul:

function wadDivAsmNew(uint256 a, uint256 b) public pure returns (uint256 c)
{
 assembly
 {
   if or(iszero(b), iszero(iszero(gt(a, div(sub(not(0), div(b, 2)), WAD)))))
   { revert(0, 0) }
   c := div(add(mul(a, WAD), div(b, 2)), b)
 }
}

Pergunta. Terminamos?

Boas notícias: Executando o Equivalence Checker agora mostra que é o mesmo que a versão em Solidity!

Más notícias: Não tão rápido... porque nossa versão original em Solidity está ERRADA.

Para ver isso, precisamos executar o Equivalence Checker em uma configuração diferente. No parágrafo anterior, explicamos como podemos usar o Equivalence Checker para comparar código (wadDivAsmOld) vs. código (wadDivSol/wadDivAsmNew).

Agora precisamos comparar um pedaço de código (wadDivSol), que realiza um certo cálculo matemático na EVM, com duas funções matemáticas que descrevem seu comportamento:

• wadDiv_ShouldRevert — que codifica a condição de reversão desejada, ou seja, é uma função de valor booleano que aceita os mesmos parâmetros de entrada que wadDivSol e retorna verdadeiro se e somente se a execução de wadDivSol pela EVM com os parâmetros de entrada especificados resultar em uma reversão. No nosso caso, queremos que wadDivSol reverta se e somente se o denominador for zero ou o resultado for maior que 2²⁵⁶-1 (o maior inteiro que pode ser armazenado em um tipo uint256), causando um overflow de inteiro.
• wadDiv_ComputeInMathint — que aceita os mesmos parâmetros de entrada que wadDivSol e codifica a fórmula que produz a saída conforme calculado sobre os inteiros.

Escrito em CVL, a especificação para essas duas funções é -

Neste caso, testar a equivalência consiste em verificar se as duas regras seguintes são verdadeiras -

O que elas significam?

• Bem, a primeira regra é exatamente o que parece. Diz que wadDiv_ShouldRevert reverte se e somente se wadDivSol reverte.
• A segunda regra é um pouco mais sutil. Afirma que, dados os mesmos inputs, wadDivSol e wadDiv_ComputeInMathint retornam o mesmo valor uint256, desde que wadDivSol não tenha revertido (note a falta do modificador @withrevert) na segunda regra.

Executando o Provador resulta em um contraexemplo:

De fato, após converter esses valores para decimal, obtemos:

X (as WAD) = 1766847064778384331350144565521302847.177628462396921805
Y (as WAD) = 0.000000000000000003
=> X/Y (as WAD) = 588949021592794777116714855173767615725876154132307268.333333333333333333

que ainda está dentro da faixa e pode ser representado por um tipo uint256. Assim, descobrimos que a versão em Solidity que escrevemos reverte "muito cedo", ou seja, a forma como escolhemos implementar o cálculo faz com que reversões ocorram mesmo quando não deveriam.

Conclusão

O Equivalence Checker é uma ferramenta CLI flexível e fácil de usar que permite a um usuário comparar dois pedaços de código, ou uma implementação versus uma especificação, para equivalência funcional. Seu propósito é acelerar o desenvolvimento de código e melhorar a eficiência do gás sem comprometer a segurança. A versão protótipo atual suporta Yul, Solidity e CVL. Espera-se que seja lançado no 2º trimestre de 2023.

Versões futuras planejadas podem permitir comparação entre Solidity/Yul e Vyper (ou até Cairo).

Espero que tenham gostado deste tutorial e explorado as capacidades da ferramenta. Adoraríamos receber feedbacks e propostas de melhorias de desenvolvedores e usuários — por favor, comente abaixo se tiver alguma dúvida ou sugestão.

Por fim, como mencionamos antes, este blog é apenas a primeira parte de uma série — fique atento para mais!

Inscreva-se em nossa newsletter para receber atualizações.

Artigo original publicado por Netanel. Traduzido por Paulinho Giovannini.