chrischo-h/bithovenBithoven è un linguaggio per smart contract progettato per comporre strumenti potenti e sicuri su Bitcoin. Parser LR(1) con analisi statica per garantire la sicurezza a tempo di compilazione. Articolo di verifica formale: https://arxiv.org/abs/2601.01436
Un linguaggio di alto livello e imperativo per Smart Contract Bitcoin
Bithoven è un linguaggio di programmazione type-safe e facile per sviluppatori, progettato per compilare in nativo Bitcoin Script. Colma il divario tra logica complessa di smart contract e la macchina a stack di basso livello della Bitcoin Virtual Machine (VM).
Scrivi codice leggibile e verificabile con moderno controllo di flusso (if/else), variabili denominate e controlli di sicurezza integrati—poi compilalo in Bitcoin Script altamente ottimizzato per SegWit o Taproot.
if, else e return invece di destreggiarti mentalmente con lo stack.bool, signature, string e per prevenire comuni errori a runtime.numberlegacy, segwit e taproot tramite pragmi.older, after), crittografia (sha256, checksig) e verifica (verify).# For CLI user
cargo install bithoven
# For rust user
cargo add bithoven
# For js user
npm install bithoven
I contratti Bithoven sono definiti con estensione .bithoven. Di seguito è riportata un'implementazione di uno standard Hashed Time-Locked Contract (HTLC), che dimostra come Bithoven semplifichi i percorsi di spesa condizionali.
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 include una ricca collezione di esempi che dimostrano smart contract Bitcoin del mondo reale:
| Esempio | Descrizione | Caratteristiche Principali |
|---|---|---|
| HTLC | Contratto Hash Time-Locked | Blocchi hash, timelock, pagamenti condizionali |
| Atomic Swap 🆕 | Scambio cross-chain | Blocchi hash SHA256 doppi, scambio senza fiducia |
| Escrow 🆕 | Mercato multisig 2-di-3 | Arbitro, acquirente/venditore, rimborsi con timelock |
| Vault 🆕 | Wallet con sicurezza avanzata | Prelievi con ritardo temporale, recupero immediato da cold storage |
| Multisig Voting 🆕 | Tesoreria DAO / approvazioni consiglio | Votazione a soglia 2-di-3, override d'emergenza 3-di-3 |
| Prediction Market 🆕 | Scommesse decentralizzate con oracolo basato su hash | Schemi di impegno crittografico, verifica prova dell'oracolo |
| Multisig | Multisig 2-di-2 | Supporto multi-firma Taproot |
| Inheritance | Controllo accesso a livelli | Molteplici livelli di eredi, accesso basato su segreto |
| Hashlock | Blocco hash semplice | Verifica hash SHA256 |
| Timelock | Timelock assoluto | CLTV (CheckLockTimeVerify) |
Vedi tutti gli esempi: Directory degli Esempi
Quando compilato, Bithoven traduce la logica imperativa di alto livello negli opcode Bitcoin Script equivalenti, gestendo automaticamente il flusso di controllo e la gestione dello stack.
Comando:
bithoven compile htlc.bithoven
Bitcoin Script generato (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>: Impone un timelock relativo (Sequence).after <n>: Impone un timelock assoluto (LockTime).checksig(sig, pubkey): Valida una firma rispetto a una chiave pubblica.verify <expr>: Assicura che un'espressione sia vera, altrimenti fallisce lo script.bool: Valori booleani (true, false).signature: Firme ECDSA o Schnorr.string: Dati stringa esadecimali o ASCII.number: Valori interi.I contributi sono benvenuti! Dai un'occhiata alla pagina issues per gli elementi della roadmap o invia una PR.
Questo progetto è concesso in licenza secondo la licenza MIT - consulta il file LICENSE per i dettagli.
Se usi Bithoven nella tua ricerca, cita il seguente articolo:
Bithoven: Sicurezza Formale per Smart Contract Bitcoin Espressivi. Hyunhum Cho e 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},
}
| Controllo firma base |
| Contratto semplice stile P2PKH |