O Archetype é uma linguagem simples de alto nível para desenvolver Contratos Inteligentes na blockchain Tezos. Ele permite_ verificar formalmente_ os contratos, transcodificando-os para Why3. Para mais informações sobre a linguagem Archetype, por favor, siga o link abaixo:
Archetype, a DSL for Tezos
Neste artigo, desenvolvemos, especificamos e verificamos formalmente um contrato inteligente; com uma verificação formal, encontramos e corrigimos bugs e nos certificamos de que ele esteja de acordo com sua especificação.
Este vídeo é a exibição da demonstração (25 minutos):
Abaixo está a versão textual da demonstração.
Contrato
O objetivo desta demonstração é desenvolver um contrato inteligente para um programa de fidelidade. Este contrato registra milhas e proprietários de milhas com dois pontos de entrada: add e consume (adicionar e consumir).
Ativos de contrato
Um owner (proprietário) de milha é identificado por um valor de endereço e possui várias milhas (potencialmente zero). Uma milha é identificada por uma única id de string e uma data de validade, de modo que uma milha não possa ser consumida após sua data de validade.
O esquema abaixo ilustra a modelagem básica dos dados:
Uma otimização é adicionada ao modelo acima. Uma milha é aumentada com um valor quantity (quantidade) para reunir várias milhas com a mesma data de validade. Por exemplo, 3 milhas com a mesma data de validade são fundidas em uma milha com o valor quantity definido para 3:
Código
O seguinte trecho abaixo é a implementação archetype dos dados do contrato:
archetype miles_with_expiration
asset mile identified by id {
id : string;
expiration : date;
quantity : int
}
asset owner identified by addr {
addr : address;
miles : mile partition; (* R(owner,mile) é bijetiva *)
}
Note que o tipo de coleção de milhas (linha 11) é partição (partition): isto é para especificar que uma milha é de propriedade de um e apenas um proprietário. Isto impede, por exemplo, que uma milha seja adicionada ou removida diretamente da coleção de milhas. Ela deve passar pela coleção de milhas de um proprietário.
Ao adicionar uma milha à coleção de milhas de um proprietário, é testado se a milha já existe; em caso afirmativo, a instrução add falha.
Isto é implementado com uma única coleção de milhas e o campo miles é implementado como uma lista de identificadores de milhas, não como uma lista de milhas.
Ações
A ação add tem dois argumentos: um endereço do proprietário e uma nova milha para adicionar a este proprietário:
action add (ow : address) (newmile : mile) {
effect {
var o = owner.get(ow);
o.miles.add(newmile)
}
}
owner acima (linha 4) é a coleção (collection) de todos os proprietários. O método get permite recuperar um proprietário de seu endereço (que é o identificador do proprietário).
O método add (linha 5) é usado para acrescentar um ativo à coleção (neste caso, o.miles).
A ação consume leva dois argumentos: o endereço do proprietário, ow, e o número de milhas deste proprietário a consumir, qty :
action consume (ow : address) (qty : int) {
effect {
var o = owner.get(ow);
var valid_miles = o.miles.select(the.expiration > now);
require ( valid_miles.sum(the.quantity) >= qty );
var remainder = qty;
for m in valid_miles do
if remainder > 0 then (
if m.quantity < remainder then (
remainder -= m.quantity;
o.miles.remove(m.id)
) else (
remainder := 0;
mile.update(m.id, { quantity -= remainder })
)
)
done
}
}
A implementação da ação consume não é tão simples por causa do campo quantity carregado por cada milha:
- a coleção das milhas válidas do proprietário é criada com o método select (linha 4)
- milhas são removidas até que o número de milhas removidas seja igual a qty; para isso, cada milha válida é iterada: se a quantidade atual de milhas for inferior ao número restante de milhas a serem removidas (linha 9), então a milha é removida (linha 11) e o valor restante é diminuído de sua quantidade; caso contrário, a quantidade atual de milhas é reduzida (linha 14) e o número restante é definido como 0 (linha 13)
Essa implementação possui 2 bugs: você pode identificá-los? A verificação apresentada na seção abaixo ajudará a detectá-los e corrigi-los.
Especificar
Observe que o tipo do campo quantity do ativo milha é int (ou seja, integer ou inteiro, linha 6 na seção asset acima), que pode ser negativo. Entretanto, não faz sentido que a quantidade seja igual ou inferior a zero. Gostaríamos de especificar algumas restrições no campo quantity, mais especificamente, que ele deve permanecer estritamente positivo.
É possível especificar tal restrição com uma invariante de ativo (asset invariant - linhas 5 a 7 abaixo):
asset mile identified by id {
id : string;
expiration : date;
quantity : int
} with {
i0: quantity > 0;
}
Isto gerará as obrigações de prova correspondentes para todas as ações (add e consume).
Queremos operar o contrato a partir de um endereço, isto é, que cada ação só possa ser chamada por este endereço. O Archetype fornece um "modificador" exclusivo called by (linha 4):
constant admin role = @tz1aazS5ms5cbGkb6FN1wvWmN7yrMTTcr6wB
action add (ow : address) (newmile : mile) {
called by admin
effect {
var o = owner.get(ow);
o.miles.add(newmile)
}
}
O predicado de segurança only_by_role (linha 2 abaixo) pode ser usado na seção security para especificar que qualquer ação deve usar o modificador called by, em modo de administrador:
security {
s1: only_by_role(anyaction,admin);
s2: no_storage_fail(add);
}
O predicado no_storage_fail (linha 3 acima) é útil para estabelecer que uma ação (neste caso, a ação add) não deve falhar, seja com uma exceção “Key not found” (chave não encontrada) ou “Key exists” (chave existente). Normalmente é uma boa prática não programar com exceções lógicas, seja explicitamente (com mecanismos try… catch) ou implicitamente, como em contratos inteligentes que vêm com um mecanismo de rollback em caso de falha. É melhor abrir explicitamente ramos de execução com controles if then else. As exceções devem ser usadas somente para falhas de hardware, rede... ou seja, qualquer coisa sobre a qual o programa em si não tenha controle.
Obviamente, este não é o caso da ação add, que falhará, por exemplo, se ow não corresponder a nenhum proprietário registrado existente.
Estas previsões de segurança geram obrigações de prova, conforme apresentado na seção de verificação abaixo. A lista de predicados de segurança disponíveis pode ser encontrada aqui.
Finalmente, queremos ter certeza de que a implementação da ação consume esteja de acordo com a exigência básica de que a quantidade (qty) de milhas sejam removidas. A maneira de formular tal exigência é estabelecer uma relação aritmética entre o estado de armazenamento antes da execução da ação e após a execução:
action consume (ow : address) (qty : int) {
specification {
postcondition p0 {
mile.sum(the.quantity) = before.mile.sum(the.quantity) - qty
}
}
effect {
...
}
}
A pós-condição p1 (linha 5 acima) literalmente diz "a soma dos campos quantity após a execução do consume é igual à soma antes da execução, menos o valor qty".
Como recapitulação, aqui está o código completo do contrato antes da verificação:
archetype miles_with_expiration
constant admin role = @tz1aazS5ms5cbGkb6FN1wvWmN7yrMTTcr6wB
asset mile identified by id {
id : string;
expiration : date;
quantity : int
} with {
i0: quantity > 0;
}
asset owner identified by addr {
addr : address;
miles : mile partition;
}
action add (ow : address) (newmile : mile) {
called by admin
effect {
owner.get(ow).miles.add(newmile)
}
}
action consume (ow : address) (qty : int) {
specification {
postcondition p0 {
mile.sum(the.quantity) = before.mile.sum(the.quantity) - qty
}
}
effect {
var o = owner.get(ow);
var valid_miles = o.miles.select(the.expiration > now);
require ( valid_miles.sum(the.quantity) >= qty );
var remainder = qty;
for m in valid_miles do
if remainder > 0 then (
if m.quantity < remainder then (
remainder -= m.quantity;
o.miles.remove(m.id)
) else (
remainder := 0;
mile.update(m.id, { quantity -= remainder })
)
)
done
}
}
security {
s0 : only_by_role (anyaction, admin);
s1 : no_storage_fail (add);
}
Verificar
Nesta seção, verificamos os 4 predicados definidos na seção anterior:
- s0: qualquer ação pode ser chamada apenas pela função admin
- s1: a ação add não falha ao acessar o armazenamento
- p0: a ação consume consome exatamente qty de milhas
- i0: o valor quantity de qualquer milha é estritamente positivo
A extensão archetype do VS Code fornece um painel à esquerda que lista os predicados e permite chamar o IDE why3 em cada um para ser verificado:
O contrato e o predicado são transcodificados para o formato why3 (whyml). Para invocar o IDE do why3, clique no ícone de verificação à direita do predicado no painel de extensão do archetype.
Para verificar a propriedade com o why3, clique com o botão direito do mouse no módulo chamado "Miles_with_expiration", e selecione "Auto level 2" como ilustrado abaixo (aqui para os predicados de segurança s0):
O Why3 traduz os predicados na linguagem SMT e invoca os resolvedores SMT (neste caso, Alter-Ergo, Z3 e CVC4). Vemos na captura de tela acima que o Why3 gerou obrigações de prova para ambas as ações (add e consume).
Predicado de segurança s0
Quando um predicado é validado, o ponto de interrogação fica verde. A ação consume não fica verde, como ilustrado abaixo:
Isso porque o modificador called by está faltando na ação consume. Quando acrescentado, a propriedade s0 é então verificada:
Predicado de segurança s1
O predicado s1 do no_storage_fail também não é verificado no contrato acima. Ao observarmos em detalhes as obrigações de prova com falha, vemos que ambas as exceções, "Key not found" e "Key exists", podem ser levantadas:
Uma obrigação de prova com falha para o s1: o método "get" pode gerar uma exceção NotFound
Vemos que o método get pode gerar uma exceção NotFound (ver captura de tela acima) e que o método add pode gerar uma exceção KeyExist.
A solução é primeiro testar a existência de um proprietário com id ow. Caso não exista, deve ser criado um novo proprietário. Em qualquer caso, a add deve falhar se a id de newmile (novamilha) já estiver presente:
action add (ow : address) (newmile : mile) {
called by admin
failif {
f1: mile.contains(newmile.id)
}
effect {
if owner.contains(ow) then
owner.get(ow).miles.add(newmile)
else
owner.add({ addr = ow; miles = [newmile] })
}
}
Vemos o efeito de não permitir que o código falhe: isso nos obriga a lidar com todas as situações e a explicitar o comportamento. Aqui nós simplesmente esquecemos de criar um proprietário quando necessário! s1 é agora verificado:
Pós-condição p0
O efeito da ação consume usa uma iteração sobre as milhas válidas do proprietário ow. É então necessário fornecer o why3 com invariantes de loop para p0 (why3 depende do cálculo da pré-condição mais mais fraca (Weakest Precondition)).
Essa é a parte mais complicada do processo de verificação, pois requer alguma experiência em descobrir as invariantes.
No caso da p0, a invariante deve usar a variável remainder que é diminuída de qty para 0 durante a iteração. Em qualquer iteração, temos a relação:
mile.sum(the.quantity) =
mile.before.sum(the.quantity) - qty + remainder
No final da iteração, a variável remainder é igual a 0, o que é reescrito como p0.
Entretanto, o why3 ainda não consegue provar p0 porque não é trivial provar que a variável remainder é igual a 0 no final da iteração. Outra invariante pode ser fornecida para esse fim:
0 <= remainder <= toiterate.sum(the.quantity)
A palavra-chave toiterate se refere à coleção de milhas que ainda não foram iteradas e estão para ser. No fim da iteração, a coleção toiterate está vazia e a sua soma é igual a 0.
O seguinte trecho do Archetype ilustra como fornecer essas invariantes (linhas 5-8 abaixo):
action consume (ow : address) (qty : int) {
specification {
postcondition p1 {
mile.sum(the.quantity) = before.mile.sum(the.quantity) - qty
invariant for loop {
mile.sum(the.quantity) =
before.mile.sum(the.quantity) - qty + remainder;
0 <= remainder <= toiterate.sum(the.quantity)
}
}
}
called by admin
effect {
var o = owner.get(ow);
var valid_miles = o.miles.select(the.expiration > now);
require ( valid_miles.sum(the.quantity) >= qty );
var remainder = qty;
for:loop m in valid_miles do
if remainder > 0 then (
if m.quantity < remainder then (
remainder -= m.quantity;
o.miles.remove(m.id)
) else (
remainder := 0;
mile.update(m.id, { quantity -= remainder })
)
)
done
}
}
Note que tivemos que nomear a iteração (linha do loop 7 acima).
Com o código acima, o p0 é verificado. No entanto, duas obrigações de prova ainda falham.
A primeira corresponde à inicialização da invariante do segundo loop (linha 15 acima):
Ela não consegue provar que a variável remainder é maior ou igual a 0 no início da iteração. Como é igual a qty nesta etapa, a solução consiste em adicionar uma condição de guarda que requer que qty seja maior ou igual a 0.
A segunda obrigação de prova que falha corresponde à prova de hereditariedade da invariante do loop principal (linha 6 acima) no segundo ramo de execução (linhas 23, 24 acima) quando a quantidade atual de milha é maior do que a variável remainder:
O why3 destaca as condições de ramificação que não são verdadeiras na obrigação de prova atual (em roxo na linha 317, na captura de tela acima), o que indica precisamente qual ramo de execução tem um problema.
A questão é que a variável remainder é definida como 0 antes de atualizar o campo de quantidade atual de milha. A solução é trocar as linhas 23 e 24 das instruções.
A versão corrigida da ação consume é apresentada abaixo:
action consume (ow : address) (qty : int) {
specification {
postcondition p0 {
mile.sum(the.quantity) = before.mile.sum(the.quantity) - qty
invariant for loop {
mile.sum(the.quantity) = before.mile.sum(the.quantity) - qty + remainder;
0 <= remainder <= toiterate.sum(the.quantity)
}
}
}
called by admin
require {
r2: qty > 0;
}
effect {
var o = owner.get(ow);
var valid_miles = o.miles.select(the.expiration > now);
require ( valid_miles.sum(the.quantity) >= qty );
var remainder = qty;
for:loop m in valid_miles do
if remainder > 0 then (
if m.quantity < remainder then (
remainder -= m.quantity;
o.miles.remove(m.id)
) else (
mile.update(m.id, { quantity -= remainder });
remainder := 0
)
)
done
}
}
Invariante i0
A invariante i0 tem que ser verificada toda vez que a coleção de milhas é modificada. Aqui a invariante não é verificada, seja na ação add ou consume.
Na ação add, o método add (linha 8 acima) exige que a newmile (milha adicionada) tenha um campo quantity estritamente positivo:
A solução é adicionar uma condição de guarda (linhas 3-5 abaixo):
action add (ow : address) (newmile : mile) {
called by admin
require {
r1: newmile.quantiy > 0
}
failif {
f1: mile.contains(newmile.id)
}
effect {
if owner.contains(ow) then
owner.get(ow).miles.add(newmile)
else
owner.add({ addr = ow; miles = [newmile] })
}
}
Na ação consume, o método update exige que a quantidade de milha seja positiva, como especificado pela invariante de ativo, mas os resolvedores falham ao provar isso:
O ramo é o ramo else do teste
m.quantity < remainder
que é
m.quantity >= remainder
De fato, quando a quantidade é igual à variável remainder, ela registra uma milha com um valor quantity igual a 0, o que não está de acordo com i0.
A solução é mudar o teste de ramificação para
m.quantity <= remainder
Conclusão
Graças aos recursos de verificação formal do Archetype, conseguimos desenvolver um contrato inteligente correto que implementa um programa de fidelidade na cadeia:
archetype miles_with_expiration
constant admin role = @tz1aazS5ms5cbGkb6FN1wvWmN7yrMTTcr6wB
asset mile identified by id {
id : string;
expiration : date;
quantity : int
} with {
i0: quantity > 0;
}
asset owner identified by addr {
addr : address;
miles : mile partition;
}
action add (ow : address) (newmile : mile) {
called by admin
failif {
f1: mile.contains(newmile.id)
}
effect {
if owner.contains(ow) then
owner.get(ow).miles.add(newmile)
else
owner.add({ addr = ow; miles = [newmile] })
}
}
action consume (ow : address) (qty : int) {
specification {
postcondition p0 {
mile.sum(the.quantity) = before.mile.sum(the.quantity) - qty
invariant for loop {
mile.sum(the.quantity) =
before.mile.sum(the.quantity) - qty + remainder;
0 <= remainder <= toiterate.sum(the.quantity)
}
}
}
called by admin
require {
r2: qty > 0;
r3: owner.contains(ow)
}
effect {
var o = owner.get(ow);
var valid_miles = o.miles.select(the.expiration > now);
require ( valid_miles.sum(the.quantity) >= qty );
var remainder = qty;
for:loop m in valid_miles do
if remainder > 0 then (
if m.quantity <= remainder then (
remainder -= m.quantity;
o.miles.remove(m.id)
) else (
mile.update(m.id, { quantity -= remainder });
remainder := 0
)
)
done
}
}
security {
s0 : only_by_role (anyaction, admin);
s1 : no_storage_fail (add);
}
Agora é seguro transcodificar o contrato do Archetype para uma linguagem de nível inferior como a Ligo, a partir da qual é possível gerar a versão Michelson:
A verificação do programa é uma técnica muito poderosa para encontrar e corrigir problemas. É também uma ótima maneira de aumentar a confiança dos usuários no contrato, especialmente quando as propriedades verificadas são fáceis de ler e entender.
Observamos, entretanto, que a segurança não é uma qualidade absoluta, mas sim relativa às propriedades que somos capazes de identificar e formular.
Abaixo está a lista de softwares usados na demonstração para que você possa reproduzi-la:
- Archetype 0.1.10
- VS Code 1.39.2
- Why3 1.2.0
- Alt-Ergo 2.2.0
- CVC4 1.6
- Z3 4.8.4
Note que o archetype ainda está em versão alfa. Planejamos lançar a versão 1 até o final do ano.
Siga-nos no Twitter para ser atualizado sobre a evolução do projeto:
Archetype
The latest Tweets from Archetype (@archetype_lang). Archetype is a domain-specific language to develop Smart Contracts…
Esse artigo foi escrito por Benoit Rognier e traduzido por Fátima Lima. O original pode ser lido aqui.
Top comments (0)