Resumo. Um caso de uso proeminente de contratos inteligentes Ethereum é a criação de uma ampla gama
de tokens ou ativos definidos pelo usuário por meio de contratos inteligentes. Ativos definidos pelo usuário não são nativos
em Ethereum; ou seja, eles não são diretamente suportados pelo livro-razão, mas requerem customização de
código repetitivo. Isso os torna desnecessariamente ineficientes, caros e complexos. Isso também os torna
inseguro, como vários incidentes em Ethereum demonstraram. Mesmo sem
contratos inteligentes com estado, a falta de fungibilidade perfeita dos ativos Bitcoin permite a implementação
tokens como soluções de camada dois, o que também adiciona uma camada adicional de complexidade.
Neste artigo, exploramos um design alternativo baseado em livros contábeis UTXO no estilo Bitcoin. Em vez de
de introduzir recursos gerais de script junto com os riscos de segurança associados, nós
propomos uma extensão do modelo UTXO, onde substituímos a estrutura contábil de uma
criptomoeda única com uma nova estrutura que gerencia um número ilimitado de tokens nativos definidos pelo usuário, que chamamos de pacotes de tokens. A criação de token é controlada forjando
scripts de política que, assim como scripts de validador de Bitcoin, usam uma pequena linguagem específica de domínio
com expressividade computacional limitada, favorecendo a segurança e austeridade computacional do Bitcoin. A abordagem resultante é leve, ou seja, criação e transferência de ativos personalizados
é barato e evita o uso de qualquer estado global na forma de um registro de ativos ou similar.
O UTXOma proposto
modelo e a semântica da linguagem de script foram formalizados no assistente de prova Agda.
Palavras-chave: blockchain · UTXO · tokens nativos · programação funcional.
- INTRODUÇÃO
Os livros-razão distribuídos(Blockchains) começaram rastreando apenas um único ativo - o dinheiro. O objetivo era competir com
moedas existentes, e então, naturalmente, começaram a se concentrar em suas próprias moedas - Bitcoin e
sua moeda de mesmo nome, Ethereum e Ether, e assim por diante. Esse foco era tão claro que os sistemas
tendiam a ser identificados com sua moeda principal.
Mais recentemente, ficou claro que é possível e muito útil rastrear outros tipos de
ativo em sistemas de razão distribuídos(Blockchain). Ethereum liderou a inovação neste espaço, com ERC-20 adotando a
implementação de novas moedas e ERC-721 implementação de tokens não fungíveis únicos.
Estes têm sido muito populares - variantes do ERC-20 são os contratos inteligentes mais usados em
Ethereum por alguma margem. No entanto, eles têm grandes deficiências. Notavelmente, tokens personalizados em
Ethereum não são nativos. Isso significa que os tokens não residem na conta de um usuário; e para
enviar tokens ERC-20 de outro usuário, o remetente deve interagir com o contrato inteligente regulador para
a moeda. Ou seja, apesar do fato de que o principal objetivo da Ethereum é rastrear a propriedade dos ativos
e realizar transações, os usuários foram forçados a construir seu próprio livro-razão interno dentro de um
contrato inteligente
Outros sistemas aprenderam com isso e tornaram os tokens personalizados nativos, como o Stellar,
Waves, Zilliqa e muito mais. No entanto, eles normalmente dependem de algum tipo de estado global, como um
registro de moeda global ou contas globais especiais que devem ser criadas. Isso é lento e restringe
uso criativo de tokens personalizados devido à alta sobrecarga em termos de tempo e dinheiro. Há
também esforços para introduzir multi-ativos nativos em livros UTXO [19], um precursor de nosso trabalho.
Podemos fazer melhor do que isso por meio de uma combinação de duas idéias. Em primeiro lugar, generalizamos o valor
tipo com o qual o livro-razão trabalha para incluir pacotes de tokens que misturam tokens de forma livre e uniforme de
ativos alfandegários diferentes, fungíveis e não fungíveis. Em segundo lugar, evitamos qualquer estado global por
“Eternamente” vinculando uma moeda a uma política governamental de falsificação por meio de um hash. Entre eles, isso cria
um sistema de razão de vários ativos (que chamamos de UTXOma) com tokens personalizados leves e nativos.
Especificamente, este artigo faz as seguintes contribuições:
- Introduzimos pacotes de tokens, representados como funções com suporte finito, como um mecanismo uniforme para generalizar as regras de contabilidade UTXO existentes para ativos personalizados, incluindo fungíveis,
tokens não fungíveis e mistos. - Evitamos a necessidade de um estado global na forma de um registro de moeda vinculando forjamento personalizado
scripts de política por meio de seu hash de script para o nome de grupos de ativos. - Oferecemos suporte a uma ampla variedade de aplicativos padrão para ativos personalizados sem a necessidade de contratos inteligentes de uso geral, definindo uma linguagem simples de domínio específico para forjar scripts de política.
- Fornecemos uma definição formal das regras de razão UTXOma como uma base para raciocinar formalmente sobre
o sistema resultante, juntamente com uma versão mecanizada em Agda.4
Criar e transferir novos ativos no sistema resultante é leve e barato. É leve
pois evitamos transações de configuração especial ou procedimentos de registro, e é barato como único padrão
taxas de transação são necessárias - isso é diferente do modelo de gás Ethereum, onde um script deve ser executado
cada vez que um ativo personalizado é transferido, o que incorre em custos de gás.
O sistema de múltiplos ativos proposto não é apenas um exercício de caneta e papel. É a base do
suporte multi-ativo para o blockchain Cardano. Em um trabalho relacionado modificamos ainda mais o nativo
razão de múltiplos ativos apresentado neste documento para um modelo de razão UTxO estendido, que adicionalmente
suporta o uso de Plutus (linguagem de contrato inteligente completa de Turing) para definir políticas de falsificação.
Esta extensão do modelo de razão permite o uso de contratos inteligentes com estado para definir máquinas de estado para
bloqueio de saída.
2 SUPORTE A VARIOS ATIVOS
No modelo de livro-razão do Bitcoin, as transações gastam saídas de transações ainda não gastas (UTXOs),
enquanto fornece novas saídas não gastas para serem consumidas por transações subsequentes. Cada indivíduo
UTXO bloqueia uma quantidade específica de criptomoeda impondo condições específicas que precisam ser
encontrados para gastar essa quantidade, como por exemplo, assinar a transação de gastos com uma determinada
chave criptográfica secreta ou passagem de algumas condições mais sofisticadas impostas por um validador de script… Quantidades de criptomoeda em uma saída de transação são representadas como um número integral
da menor unidade dessa criptomoeda em particular - em Bitcoin, são Satoshis. Para nativamente
apoiar várias moedas em saídas de transação, generalizamos essas quantidades integrais para nativamente suportar a criação dinâmica de novos ativos ou tokens definidos pelo usuário. Além disso, exigimos um meio de
forjar tokens de uma maneira controlada pela política de falsificação de um ativo.
Conseguimos tudo isso com as seguintes três extensões do modelo de razão UTXO básico que são
mais detalhados no restante desta seção.
- AS SAIDAS DE TRANSAÇÃO
bloqueiam um pacote de token heterogêneo em vez de apenas um valor integral de um
criptomoeda
.
2. ESTENDEMOS AS TRANSAÇÕES COM UM CAMPO DE FORJA
. Este é um pacote de tokens que são criados
(cunhadas) ou destruídas (queimadas) por essa transação.
- INTRODUZIMOS SCRIPTS DE POLITICA DE FALSIFICAÇAO (FPS)
que regem a criação e destruição de ativos em
campos de forja. Esses scripts não são diferentes dos validadores que bloqueiam as saídas em UTXO.
2.1 PACOTES DE TOKEN
Podemos considerar as saídas da transação em um razão UTXO como pares (valor, ν) consistindo em um
valor e um script validador ν que codifica a condição de gasto. Este último pode ser a prova
de propriedade por meio da assinatura da transação de gastos com uma chave de criptografia secreta específica ou
uma condição temporal que permite que uma saída seja gasta apenas quando o blockchain atingiu um
certa altura (ou seja, um certo número de blocos foram produzidos).
Para usar convenientemente várias moedas em saídas de transação, queremos que cada saída seja capaz
De bloquear quantidades variáveis de várias moedas diferentes ao mesmo tempo em seu campo de valor. Isso sugere
usar mapas finitos de algum tipo de identificador de ativo para uma quantidade integral como uma representação concreta, por exemplo, Moeda 7 → 21. Olhando para as regras de razão UTXO padrão [18], torna-se aparente que
as quantidades de criptomoeda precisam ser monoides. É um pouco complicado transformar mapas finitos em um monóide,
mas a solução é pensar neles como funções com suporte finito (consulte a Seção 3 para obter detalhes).
Se quiser usar funções com suporte finito para obter uma representação uniforme que possa lidar com
grupos de tokens relacionados, mas não fungíveis, precisamos dar um passo adiante. Para não perder o
agrupamento de tokens não fungíveis relacionados (todos os tokens domésticos emitidos por uma entidade específica, por exemplo)
entretanto, precisamos mudar para uma estrutura de dois níveis - ou seja, funções com suporte finito de funções com suporte finito. Vamos considerar um exemplo. O comércio de itens raros no jogo é popular na modernidade,
jogos de computador com vários jogadores. Que tal representar a propriedade de tais itens e negociar dessa
propriedade em nosso livro razão UTXO de múltiplos ativos? Podemos precisar de tokens para “chapéus” e “espadas”, que
formar dois ativos não fungíveis com possivelmente vários tokens de cada ativo - um chapéu é intercambiável
com qualquer outro chapéu, mas não com uma espada, e também não com a moeda usada para comprar estes
Itens. Aqui, nossa estrutura de dois níveis compensa em toda a sua generalidade, e podemos representar a moeda para
comprar itens junto com conjuntos de itens, onde alguns podem ser múltiplos, por exemplo,
{Moeda 7 → {Moeda 7 → 2}, Jogo 7 → {Chapéu 7 → 1, Espada 7 → 4}}
- {Moeda 7 → {Moeda 7 → 1}, Jogo 7 → {Espada 7 → 1, Coruja 7 → 1}}
= {Moeda 7 → {Moeda 7 → 3}, Jogo 7 → {Chapéu 7 → 1, Espada 7 → 5, Coruja 7 → 1}}.
2.2 CAMPOS DE FORJA
Se novos tokens são gerados com frequência (como a emissão de novos chapéus sempre que uma conquista no jogo
foi alcançado) e destruído (um jogador pode perder um chapéu para sempre se o vento aumentar), estes
as operações precisam ser leves e baratas. Conseguimos isso adicionando um campo de forja a cada o tipo de booleano
N o tipo de números naturais
Z o tipo de inteiros
H o tipo de bytestrings: S∞
n = 0 {0, 1} 8n
(φ1: T1,…, φn: Tn) um tipo de registro com campos φ1,. . . , φn dos tipos T1,. . . , Tn
t.φ o valor de φ para t, onde t tem tipo T e φ é um campo de T
Defina [T] o tipo de conjuntos (finitos) sobre T
Liste [T] o tipo de listas sobre T, com como indexação e | | como comprimento
h :: t a lista com cabeça h e cauda t
x 7 → f (x) uma função anônima
c #
um hash de c criptográfico resistente à colisão
Interval [A] o tipo de intervalos em um conjunto A totalmente ordenado
FinSup [K, M] o tipo de funções com suporte finito de um tipo K a um monóide M
Fig. 1: Tipos básicos e notação
transação. É um pacote simbólico (assim como o valor em uma saída), mas admite quantidades positivas
(para cunhar novos tokens) e quantidades negativas (para queimar os tokens existentes). Claro, cunhar
e a queima deve ser estritamente controlada.
2.3 FORJANDO SCRIPTS DE POLÍTICA
O mecanismo de validação de script para bloquear saídas UTXO é o seguinte: para que uma transação gaste uma saída (valor, ν), o script validador ν precisa ser executado e aprovar o
transação de gastos. Da mesma forma, os scripts de política de falsificação associados aos tokens sendo cunhados
ou queimados por uma transação são executados a fim de validar essas ações. No espírito do Bitcoin
Abordagem Miniscript, optamos por incluir uma linguagem de script simples para apoiar políticas de falsificação
para vários casos de uso comuns, como emissor único, não fungível ou tokens de emissão única, etc. (consulte
Seção 4 para todos os casos de uso).
A fim de estabelecer uma associação permanente entre a política de falsificação e os ativos controlados
por ele, propomos uma abordagem de hashing, em oposição a uma pesquisa de registro global. Tal registro
requer um esquema de controle de acesso especializado, bem como um esquema para limpar entradas não utilizadas.
Na representação de ativos personalizados que propomos, cada token está associado ao hash do
script de política de falsificação necessário para validar no momento de falsificação do token, por exemplo. a fim de forjar o
valor {HASHVALUE 7 → {Owl 7 → 1}}, um script cujo hash é HASHVALUE será executado.
Contando com associações hash permanentes para identificar políticas de falsificação de ativos e seus ativos também
tem suas desvantagens. Por exemplo, hashes de política são strings longas que, em nosso modelo, terão
várias cópias armazenadas no livro-razão. Essas strings não são legíveis por humanos, ocupam um livro-razão valioso
imobiliário e aumentam as taxas baseadas no tamanho da transação.
3- REGRAS FORMAIS DE CONTABILIDADE
Nosso modelo de razão formal segue o estilo do modelo UTXO-with-scripts de adotando o
notação de com tipos básicos definidos como na Figura 1.
Funções com suporte finito. Modelamos pacotes de tokens como funções com suporte finito. Se K for algum
tipo e M é um monóide com elemento de identidade 0, então uma função f: K → M é finitamente suportada
se f (k) 6 = 0 para apenas muitos finitos k ∈ K. Mais precisamente, para f: K → M definimos o suporte de f
ser supp (f) = {k ∈ K: f (k) 6 = 0} e FinSup [K, M] = {f: K → M: | supp (f) | <∞}.
Se (M, +, 0) é um monóide, então FinSup [K, M] também se torna um monóide se definirmos a adição pontualmente
(ou seja, (f + g) (k) = f (k) + g (k)), com o elemento de identidade sendo o mapa zero. Além disso, se
M é um grupo abeliano, então FinSup [K, M] também é um grupo abeliano sob esta construção, com
(
(
f) (k) =
f (k). Da mesma forma, se M está parcialmente ordenado, então FinSup [K, M] também é com comparação
definido pontualmente: f ≤ g se e somente se f (k) ≤ g (k) para todo k ∈ K.
Conclui-se que se M é um monóide (parcialmente ordenado) ou grupo abeliano, então FinSup [K,
FinSup [L, M]] para quaisquer dois conjuntos de chaves K e L. Faremos uso desse fato nas regras de validação
apresentado posteriormente no artigo (consulte a Figura 4). Funções finamente suportadas são facilmente implementadas como
mapas finitos, com uma pesquisa de mapa com falha correspondendo ao retorno de 0.
3.1 TIPOS DE RAZAO
A Figura 2 define os tipos e primitivos de razão de que precisamos para definir o modelo UTXOma. Todas
as saídas usam um esquema pay-to-script-hash, em que uma saída é bloqueada com o hash de um script. Nós
usamos uma única linguagem de script para forjar políticas e definir scripts de bloqueio de saída. Assim como
no Bitcoin, é uma linguagem de domínio específico restrito (e não uma linguagem de propósito geral); a
os detalhes seguem na Seção 4. Assumimos que cada transação possui um identificador único derivado de seu
valor por uma função hash. Esta é a base da função lookupTx para procurar uma transação, dado
seu identificador único.
Pacotes de token. Generalizamos quantidades transferidas por produto de uma Quantidade simples para um pacote
de Quantidades. Quantidades representa um pacote de tokens: é um mapeamento de uma política e um ativo,
que define a classe de ativo, para uma quantidade desse ativo.5 Uma vez que uma quantidade é indexada desta forma,
ele pode representar qualquer combinação de tokens de quaisquer ativos (por isso o chamamos de pacote de tokens).
Grupos de ativos e scripts de política forjados. Um conceito-chave é o grupo de ativos. Um grupo de ativos é identificado
pelo hash de script especial que controla a criação e destruição de tokens de ativos desse ativo
grupo. Chamamos esse script de script de política de forja.
Forjamento. Cada transação recebe um campo de forja, que simplesmente modifica o saldo necessário da
transação pelas Quantidades dentro dela: assim, um campo de forja positivo indica a criação de novos
tokens. Em contraste com as saídas, as quantidades em campos de forja também podem ser negativas, o que efetivamente
queima tokens existentes.
Além disso, as transações obtêm um campo de scripts que contém um conjunto de scripts de política de falsificação: Definir [Script].
Isso fornece os scripts de política de forja que são necessários como parte da validação quando os tokens são
cunhada ou destruída (ver Regra 8 na Figura 4). Os scripts de forjamento dos ativos que estão sendo forjados são
5 Escolhemos representar Quantidades como uma função finitamente suportada, cujos valores são eles próprios
funções com suporte finito (em uma implementação, isso seria um mapa aninhado). Fizemos isso para fazer
a definição das regras mais simples (em particular a Regra 8). No entanto, pode igualmente ser definido como um
função com suporte finito de tuplas de PolicyIDs e Ativos para Quantidades.
A restrição sobre a produção é aplicada pela Regra 2. Nós simplesmente não impomos tal restrição ao campo de forja: permite definir regras de forma mais simples, com notação mais limpa.
Ledger Primitivos
Quantidade
uma quantidade de moeda, formando um grupo abeliano (normalmente Z)
Ativo
um tipo que consiste em identificadores para classes de ativos individuais
Marcação
um carrapato
Endereço
um “endereço” no blockchain
TxId
o identificador de uma transação
txId: Tx → TxId
uma função que calcula o identificador de uma transação
lookupTx: Razão × TxId → Tx
recuperar a transação única com um determinado identificador
verificar: PubKey × H × H → B
verificação de assinatura
Roteiro
forjando scripts de política
scriptAddr: Script → Endereço
o endereço de um script
J K: Script → (Endereço × Tx × Definir [Saída]) → B aplica o script entre colchetes aos seus argumentos
Tipos de razão
PolicyID = Endereço
(um identificador para uma moeda personalizada)
Assinatura = H
Quantidades = FinSup [PolicyID, FinSup [Ativo, Quantidade]]
Saída = (addr: Endereço, valor: Quantidades)
OutputRef = (id: TxId, índice: Int)
Input = (outputRef: OutputRef
validador: Script)
Tx = (entradas: Definir [entrada],
saídas: Lista [saída],
ValityInterval: Interval [Tick],
forja: Quantidades
scripts: Definir [Script],
sigs: Definir [Assinatura])
Razão = Lista [Tx]
Fig. 2: Tipos básicos e primitivos de Ledger
executado e a transação só é considerada válida se a execução do script retornar verdadeiro. UMA
o script de política de forja é executado em um contexto que fornece acesso aos principais componentes do
transação de forja, os UTXOs que ela gasta e o ID da política. A passagem do contexto fornece uma
peça crucial do quebra-cabeça em relação à auto-identificação: inclui o próprio PolicyID do script, que
evita o problema de tentar incluir o hash de um script dentro de si.
Intervalos de validade.
O campo de intervalo de validade de uma transação contém um intervalo de tiques (monotonicamente
unidades crescentes de “tempo”, de [5]). O intervalo de validade afirma que a transação deve apenas
ser validado se o tique atual estiver dentro do intervalo. O intervalo de validade, em vez do real
valor atual da escala da cadeia, deve ser usado para validação do script. Em uma transação válida de outra forma,
UTXOma: UTXO com suporte para vários ativos