Verificação Formal de Criadores de Mercado Automatizados em DeFi

Automated Market Makers (AMMs) são uma parte importante das finanças descentralizadas (DeFi). Eles permitem que os usuários negociem criptomoedas sem precisar de um intermediário ou de uma fonte confiável para os preços. Nos AMMs, as taxas de câmbio entre diferentes criptomoedas são determinadas por algoritmos. Embora as regras de como eles funcionam sejam simples, o comportamento que produzem pode ser complexo. Muitos pesquisadores estudam esses comportamentos usando modelos simples, mas a maioria das provas de como esses modelos funcionam é feita no papel.

Este artigo foca em uma abordagem formal para os AMMs, usando uma ferramenta específica chamada Lean 4 Theorem Prover. Essa ferramenta permite a criação de provas que são verificadas por um computador. Dessa forma, podemos ter mais confiança nos resultados do que depender apenas da verificação humana. Nós criamos especificamente um modelo baseado em um AMM popular chamado Uniswap v2, mostrando como construímos a prova e analisamos suas propriedades econômicas.

#Conceito Básico dos AMMs

Em uma troca tradicional, compradores e vendedores precisam se encontrar para negociar. Com os AMMs, os usuários negociam contra um pool de fundos, conhecido como Pools de Liquidez. Esses pools são criados por usuários que depositam suas criptomoedas no AMM. Em troca de fornecer essa liquidez, eles recebem recompensas. O processo de negociação nos AMMs é diferente; permite que os usuários troquem seus ativos diretamente sem saber com quem estão negociando.

À medida que o uso dos AMMs cresceu, seus valores também aumentaram, frequentemente chegando a bilhões de dólares. Esse imenso valor os torna alvos atraentes para ataques, resultando em perdas ao longo do tempo. A segurança dos AMMs depende de vários fatores, incluindo a ausência de erros de programação e o comportamento dos usuários alinhado com as funções esperadas do AMM.

#A Necessidade de Verificação Formal

Apesar dos benefícios dos AMMs, seus comportamentos econômicos complexos tornam essencial verificar seu funcionamento correto. Embora existam ferramentas que ajudam a detectar erros de programação, elas frequentemente não conseguem verificar comportamentos econômicos complexos. Muitos desses comportamentos são explicados usando métodos tradicionais, que podem não fornecer as garantias rigorosas necessárias para ter confiança em sua segurança.

É aqui que a verificação formal entra em cena. Usando o Lean 4, podemos criar um modelo de AMMs que nos permite examinar seus mecanismos econômicos em detalhes. O objetivo é não apenas provar algumas propriedades básicas, mas também obter novas percepções sobre como os AMMs funcionam.

#Construindo o Modelo do AMM

Nosso modelo de AMM é baseado na fórmula de produto constante usada pelo Uniswap v2. Esse modelo é simplificado para que possamos focar nos seus componentes essenciais. Primeiro, definimos como é o estado de uma blockchain ao lidar com AMMs. Esse estado inclui informações da carteira do usuário, os próprios AMMs e suas reservas.

Para verificar a correção do nosso modelo, representamos os fundos de cada usuário como uma carteira. Cada carteira mapeia os tipos de criptomoeda para as quantidades que o usuário possui. Garantimos que essas carteiras não permitam quantidades infinitas de um token, o que mantém o modelo realista.

Nós também representamos pares de tokens que podem ser negociados nos AMMs. As reservas de cada par são gerenciadas de uma maneira que garante que pelo menos um dos tokens tenha fundos, ou então o AMM ainda não foi criado.

#Transações nos AMMs

Nosso modelo precisa capturar os diferentes tipos de ações que um usuário pode realizar dentro do AMM. Isso inclui criar uma instância de AMM, adicionar ou remover liquidez e trocar um token por outro.

As trocas são particularmente importantes, pois se relacionam diretamente com o funcionamento dos AMMs. Definimos transações de troca de uma forma que apenas transações válidas podem existir em nosso modelo. Isso significa que uma troca deve seguir condições específicas, como o usuário ter tokens suficientes para negociar e o AMM ter reservas suficientes.

Cada transação de troca está ligada a uma função que determina a taxa de câmbio. Nosso modelo se certifica de provar a validade de cada transação de troca, garantindo que, se existir, atende a todas as condições necessárias.

#Propriedades Econômicas dos AMMs

Um dos propósitos principais do nosso modelo é analisar os aspectos econômicos dos AMMs, como preços, patrimônio líquido e ganhos com negociações. Por exemplo, definimos como calcular o valor da carteira de um usuário com base nos preços dos tokens que ele possui. O patrimônio líquido é determinado somando os valores de ambos os tipos de tokens que um usuário possui.

O ganho de uma transação é definido como a diferença no patrimônio líquido antes e depois que a transação ocorre. Isso nos permite estudar como diferentes estratégias de negociação podem gerar lucros ou perdas para os traders envolvidos.

Para entender esses mecanismos econômicos, mostramos que os traders tendem a alinhar seus comportamentos com as funções esperadas dos AMMs. Por exemplo, alcançar um equilíbrio entre a taxa de câmbio interna do AMM e as taxas fornecidas por fontes de preço confiáveis pode levar a ganhos ótimos para os traders.

#Abordando Oportunidades de Arbitragem

Arbitragem é uma estratégia de negociação onde os usuários aproveitam as diferenças de preço em diferentes mercados. No contexto dos AMMs, os traders podem encontrar oportunidades quando os preços entre o AMM e o mercado divergem. Nosso modelo nos permite explorar como determinar a quantidade ideal de tokens que um trader deve vender para maximizar seu ganho de um AMM.

Ao analisar as interações entre tokens nas trocas, derivamos fórmulas explícitas para decisões de negociação ótimas. Em essência, podemos guiar os usuários sobre como realizar trocas de maneira eficiente com base na condição das reservas do AMM e seus respectivos preços de mercado.

#Conclusão e Direções Futuras

Resumindo, desenvolvemos um modelo formal de AMMs usando o Lean 4 Theorem Prover. Esse modelo permite uma análise rigorosa dos comportamentos econômicos associados aos AMMs, gerando provas verificáveis por máquina de propriedades-chave. Essas provas aumentam nossa confiança nos mecanismos econômicos subjacentes dos AMMs.

Embora nosso modelo capture muitas características essenciais dos AMMs, há áreas para mais pesquisas. AMMs do mundo real envolvem complexidades adicionais, como taxas de negociação, tolerâncias de deslizamento e interações mais complexas entre tokens.

Trabalhos futuros podem estender nosso modelo para incorporar essas características adicionais, possibilitando uma compreensão mais abrangente dos AMMs na prática. Ao continuar refinando esse modelo, podemos ajudar a garantir que os AMMs continuem sendo uma forma segura e eficiente para os usuários negociem criptomoedas.