chrischo-h/bithovenBithoven é uma linguagem de contratos inteligentes para compor instrumentos poderosos e seguros no Bitcoin. Parser LR(1) com análise estática para segurança em tempo de compilação. Artigo de verificação formal: https://arxiv.org/abs/2601.01436
Uma linguagem de alto nível e imperativa para contratos inteligentes Bitcoin
Bithoven é uma linguagem de programação type-safe e amigável para desenvolvedores, projetada para compilar para Bitcoin Script nativo. Ela preenche a lacuna entre a lógica complexa de contratos inteligentes e a máquina de pilha de baixo nível da Máquina Virtual Bitcoin (VM).
Escreva código legível e auditável com fluxo de controle moderno (if/else), variáveis nomeadas e verificações de segurança integradas — depois compile-o para Bitcoin Script altamente otimizado para SegWit ou Taproot.
if, else e return em vez de manipulação mental de pilha.bool, signature, string e para prevenir erros comuns de execução.numberlegacy, segwit e taproot via pragmas.older, after), criptografia (sha256, checksig) e verificação (verify).# For CLI user
cargo install bithoven
# For rust user
cargo add bithoven
# For js user
npm install bithoven
Os contratos Bithoven são definidos com uma extensão .bithoven. Abaixo está uma implementação de um Hashed Time-Locked Contract (HTLC) padrão, demonstrando como Bithoven simplifica caminhos de gasto condicionais.
htlc.bithoven
pragma bithoven version 0.0.1;
pragma bithoven target segwit;
/* * Stack Input Definitions
* Each line defines a valid input stack configuration for a spending path.
*/
(condition: bool, sig_alice: signature)
(condition: bool, preimage: string, sig_bob: signature)
{
// If 'condition' is true, we enter the Refund Path (Alice)
if condition {
// Enforce relative timelock of 1000 blocks
older 1000;
// If timelock is satisfied, Alice can spend with her signature
return checksig(sig_alice, "0245a6b3f8eeab8e88501a9a25391318dce9bf35e24c377ee82799543606bf5212");
} else {
// Redeem Path (Bob)
// Bob must reveal the secret preimage that hashes to the expected value
verify sha256(sha256(preimage)) == "53de742e2e323e3290234052a702458589c30d2c813bf9f866bef1b651c4e45f";
// If hash matches, Bob can spend with his signature
return checksig(sig_bob, "0345a6b3f8eeab8e88501a9a25391318dce9bf35e24c377ee82799543606bf5212");
}
}
Bithoven vem com uma rica coleção de exemplos demonstrando contratos inteligentes Bitcoin do mundo real:
| Exemplo | Descrição | Principais Recursos |
|---|---|---|
| HTLC | Contrato Hash Time-Locked | Hash locks, timelocks, pagamentos condicionais |
| Atomic Swap 🆕 | Troca entre cadeias | Hash locks duplos SHA256, troca sem confiança |
| Escrow 🆕 | Marketplace multisig 2-de-3 | Árbitro, comprador/vendedor, reembolsos com timelock |
| Vault 🆕 | Carteira com segurança aprimorada | Saques com atraso temporal, recuperação imediata de armazenamento frio |
| Votação Multisig 🆕 | Tesouraria DAO / aprovações de conselho | Votação por limiar 2-de-3, override de emergência 3-de-3 |
| Mercado de Previsão 🆕 | Aposta descentralizada com oracle baseado em hash | Esquemas de compromisso criptográfico, verificação de prova oracle |
| Multisig | Multisig 2-de-2 | Suporte a multi-assinatura Taproot |
| Herança | Controle de acesso em camadas | Múltiplos níveis de herdeiros, acesso baseado em segredo |
| Hashlock | Hash lock simples | Verificação SHA256 |
| Timelock | Timelock absoluto | CLTV (CheckLockTimeVerify) |
Veja todos os exemplos: Diretório de Exemplos
Ao ser compilado, Bithoven traduz a lógica imperativa de alto nível nos opcodes Bitcoin Script equivalentes, gerenciando automaticamente o fluxo de controle e a manipulação da pilha.
Comando:
bithoven compile htlc.bithoven
Script Bitcoin Gerado (ASM):
OP_IF
<0xe803> OP_CHECKSEQUENCEVERIFY OP_DROP
<pubkey_alice> OP_CHECKSIG
OP_ELSE
OP_HASH256 OP_TOALTSTACK <hash_digest> OP_FROMALTSTACK OP_SWAP OP_EQUALVERIFY
<pubkey_bob> OP_CHECKSIG
OP_ENDIF
older <n>: Aplica timelock relativo (Sequence).after <n>: Aplica timelock absoluto (LockTime).checksig(sig, pubkey): Valida uma assinatura contra uma chave pública.verify <expr>: Garante que uma expressão seja avaliada como verdadeira; caso contrário, o script falha.bool: Valores booleanos (true, false).signature: Assinaturas ECDSA ou Schnorr.string: Dados de string hex ou ASCII.number: Valores inteiros.Contribuições são bem-vindas! Por favor, verifique a página de issues para itens do roadmap ou envie um PR.
Este projeto é licenciado sob a Licença MIT - veja o arquivo LICENSE para detalhes.
Se você usar Bithoven em sua pesquisa, por favor, cite o seguinte artigo:
Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts. Hyunhum Cho and Ik Rae Jeong, 2026. arXiv preprint arXiv:2601.01436. https://arxiv.org/abs/2601.01436
BibTeX:
@misc{bithoven,
title={Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts},
author={Hyunhum Cho and Ik Rae Jeong},
year={2026},
eprint={2601.01436},
archivePrefix={arXiv},
primaryClass={cs.CR},
url={https://arxiv.org/abs/2601.01436},
}
| Single Sig** |
| Verificação básica de assinatura |
| Contrato simples estilo P2PKH |