Tutorial: testando contratos Solidity com evm-redex🔗ℹ

2.1 Compile🔗ℹ

Peça ao solc o bytecode e a ABI, num único arquivo JSON:

  solc --combined-json bin,bin-runtime,abi contracts/Counter.sol > Counter.json

2.2 Carregue e faça o deploy🔗ℹ

read-artifact extrai o bytecode de criação e de runtime (e a ABI) do JSON; deploy roda o construtor e devolve o endereço implantado e o mundo resultante.

(require evm-redex/pbt)

(define ART (read-artifact "Counter.json" #:contract "Counter"))

(define DEPLOYER 2703024129)

(define DEP     (deploy (artifact-creation ART) #:from DEPLOYER))

(define COUNTER (deploy-result-address DEP))

(define BASE    (deploy-result-world DEP))   ; o mundo logo após o deploy

2.3 Leia o estado🔗ℹ

count é uma variável pública, então o Solidity gera um getter count(). Um call executa uma mensagem; call-result-return são os bytes de retorno, que abi-decode converte de volta num número:

(define (count-of world)

(car (abi-decode (list "uint256")

(call-result-return

(call world COUNTER #:data (encode-call "count()"))))))

(count-of BASE)   ; => 0

2.4 Envie transações🔗ℹ

encode-call monta a calldata de uma função; call devolve um call-result, e call-result-world é o mundo após a chamada. Encadeie esse mundo por algumas chamadas e leia o contador de volta:

(define CALLER 2964324353)

(define (send world sig . args)

(call-result-world

(call world COUNTER #:from CALLER #:data (apply encode-call sig args))))

(let* ([w (send BASE "increment()")]

[w (send w "add(uint256)" 5)])

(count-of w))    ; => 6

2.5 Enuncie uma propriedade🔗ℹ

Chamadas concretas servem para uma conferência rápida, mas o objetivo da biblioteca é testar uma propriedade sobre muitas entradas geradas. define-evm-property no modo transação (a cláusula #:call) roda uma transação real; #:given lista as entradas geradas, e #:post recebe o mundo antes (w0) e depois (w1) e o resultado da transação:

(define (tx sig . args)

(make-tx #:sender CALLER #:to COUNTER #:gas-limit 200000 #:gas-price 0

#:data (apply encode-call sig args)))

(define-evm-property add-raises-count-by-n

#:given ([n (gen-word-in 0 (expt 2 200))])

#:world BASE

#:call  (tx "add(uint256)" n)

#:post  (lambda (w0 w1 r) (= (count-of w1) (+ (count-of w0) n))))

(check-evm-property add-raises-count-by-n #:trials 50)

Ao rodar, imprime:

Uma propriedade também pode exigir que uma chamada reverta. #:revert-when diz "sob esta condição, a transação deve reverter"; a partir de um contador zero, decrement() sempre reverte:

(define-evm-property decrement-reverts-at-zero

#:given ()                     ; sem entradas geradas — uma asserção simples

#:world BASE                   ; aqui count é 0

#:call  (tx "decrement()")

#:revert-when #t)

(check-evm-property decrement-reverts-at-zero #:trials 1)

3.1 A propriedade que importa: conservação🔗ℹ

O invariante que um token nunca pode quebrar é que uma transferência move valor sem criar nem destruir nenhum. Esta única propriedade cobre tanto o caminho de sucesso quanto o de reversão, sobre valores que cercam o saldo de ALICE:

(define (tx from sig . args)

(make-tx #:sender from #:to TOKEN #:gas-limit 200000 #:gas-price 0

#:data (apply encode-call sig args)))

(define-evm-property transfer-conserves-supply

#:given ([amount (gen-word-in 0 2000)])       ; cerca o saldo de 1000

#:world MINTED

#:call  (tx ALICE "transfer(address,uint256)" BOB amount)

#:post  (lambda (w0 w1 r)

(and (= (total w1) (total w0))       ; o supply nunca muda

(if (eq? (txn-run-outcome r) 'revert)

(= (bal w1 ALICE) (bal w0 ALICE))          ; revertido

(and (= (bal w1 ALICE) (- (bal w0 ALICE) amount))

(= (bal w1 BOB)   (+ (bal w0 BOB) amount)))))))

(check-evm-property transfer-conserves-supply #:trials 100)

E uma propriedade focada em reversão — transferir mais do que se tem deve falhar:

(define-evm-property transfer-reverts-when-insufficient

#:given ([amount (gen-word-in 1001 100000)])  ; sempre mais do que ALICE tem

#:world MINTED

#:call  (tx ALICE "transfer(address,uint256)" BOB amount)

#:revert-when #t)

(check-evm-property transfer-reverts-when-insufficient #:trials 50)

Quando uma propriedade falha, o motor encolhe as entradas aleatórias até um contraexemplo mínimo e o imprime — esse caso encolhido é o grande ganho dos testes baseados em propriedades. Experimente enfraquecer o require de transfer no contrato e rodar de novo: a propriedade de conservação é refutada com uma transferência minúscula.

4.1 Votação (Voting)🔗ℹ

"tutorial/ballot.rkt" testa Ballot, o contrato de votação com delegação. Duas coisas são novas aqui: o construtor recebe argumentos (um array de nomes de proposta em bytes32), que você codifica em ABI e anexa ao bytecode de criação; e um getter pode devolver uma struct, que você decodifica como uma tupla.

(define ART (read-artifact "Ballot.json" #:contract "Ballot"))

(define CHAIR 3298922497)

; nomes de proposta são bytes32 — preencha cada um até 32 bytes

(define NAMES (list (name->b32 "alpha") (name->b32 "beta") (name->b32 "gamma")))

; args do construtor são codificados em ABI e anexados ao creation code

(define DEP    (deploy (append (artifact-creation ART)

(abi-encode (list "bytes32[]") (list NAMES)))

#:from CHAIR))

(define BALLOT (deploy-result-address DEP))

O chairperson (quem faz o deploy) concede o direito de voto, o eleitor vota e a contagem se atualiza — e a regra que vale checar é que só o chairperson pode conceder direito de voto, então uma chamada de qualquer outro deve reverter:

(define OUTSIDER 50157932545)

(define-evm-property only-chair-grants-rights

#:given ([who gen-address])

#:world BASE

#:call  (make-tx #:sender OUTSIDER #:nonce 0 #:to BALLOT #:gas-limit 300000 #:gas-price 0

#:data (encode-call "giveRightToVote(address)" who))

#:revert-when #t)                 ; quem não é chairperson sempre reverte

(check-evm-property only-chair-grants-rights #:trials 30)

4.2 Um leilão aberto🔗ℹ

"tutorial/auction.rkt" testa SimpleAuction. Suas chamadas carregam ether: o #:value de make-tx financia o lance. Contas que dão lances precisam de saldo, então enchemos algumas à mão — o mesmo que deploy faz por quem faz o deploy:

(require (only-in evm-redex world-ref world-set acct-balance acct-with-balance))

(define (fund w a wei)

(world-set w a (acct-with-balance (world-ref w a) (+ (acct-balance (world-ref w a)) wei))))

A regra central do leilão é que um lance é aceito exatamente quando supera o maior atual, e então se torna o novo maior — uma propriedade cobre tanto o caminho de aceitação quanto o de rejeição:

(define-evm-property bid-raises-the-highest

#:given ([v (gen-word-in 0 500)])

#:world W1                          ; aqui o maior lance é 100

#:call  (make-tx #:sender BOB #:nonce (nonce-of W1 BOB) #:to AUCTION #:value v

#:gas-limit 300000 #:gas-price 0 #:data (encode-call "bid()"))

#:post  (lambda (w0 w1 r)

(if (> v (highest-bid w0))

(and (eq? (txn-run-outcome r) 'success) (= (highest-bid w1) v))

(eq? (txn-run-outcome r) 'revert))))

(check-evm-property bid-raises-the-highest #:trials 60)

4.3 Compra remota segura🔗ℹ

"tutorial/purchase.rkt" testa Purchase, um escrow de quatro estados (Created → Locked → Release → Inactive). O construtor é payable — o vendedor tranca o dobro do valor do item — então você faz o deploy com #:value:

(define DEP (deploy (artifact-creation ART) #:from SELLER #:value 200))  ; value = 100

O caminho feliz é o comprador chamar confirmPurchase (igualando o depósito) e depois confirmReceived. A regra que vale fixar é que, a partir do estado Locked, só o comprador pode confirmar o recebimento:

(define-evm-property only-buyer-confirms-receipt

#:given ()

#:world LOCKED-W

#:call  (make-tx #:sender OUTSIDER #:nonce 0 #:to PURCHASE #:gas-limit 300000 #:gas-price 0

#:data (encode-call "confirmReceived()"))

#:revert-when #t)

(check-evm-property only-buyer-confirms-receipt #:trials 1)

O quarto contrato do Solidity by Example, o Canal de Micropagamento, não está incluído: ele verifica uma assinatura ECDSA off-chain com ecrecover, e produzir essa assinatura acontece fora da EVM que esta biblioteca modela — então testá-lo exigiria um assinador off-chain, além do escopo deste tutorial.