A Simplified version of Bitcoin, implemented in Agda

Abstract

Uma criptomoeda é uma moeda digital que funciona de maneira descentralizada, sem uma autoridade central e seus estados são mantidos por meio de consenso distribuído. Ela tem um papel importante na sociedade, porque é um dinheiro que é governado apenas por algoritmos e evita grande centralização de poder, como a de bancos e a do governo.

Agda é uma linguagem de programação funcional com tipos dependentes. É também um assistente de prova baseado no paradigma de preposição como tipos, assim como Coq. Essa linguagem é útil para provar propriedades sobre o código.

Apresentamos nesse trabalho uma explicação sobre o que são criptomoedas e suas principais características, uma breve explicação sobre o Lambda Calculus, tipos de dependentes e Agda, e apresentamos um modelo de criptomoeda feito nessa linguagem. A maioria das partes do Bitcoin é codificada e programada nesse modelo. Desde transações, árvore de transações, Ledger, bloco e cadeia de blocos. As funções criptográficas, como funções hash, funções de transformação de uma chave privada em uma chave pública e seus endereços, são postuladas. Além disso, neste trabalho, há código que transforma e valida transações de um texto sem formatação para o nosso modelo.