chrischo-h/bithovenBithoven est un langage de contrats intelligents pour composer des instruments puissants et sécurisés sur Bitcoin. Analyseur LR(1) avec analyse statique pour une sécurité à la compilation. Article de vérification formelle : https://arxiv.org/abs/2601.01436
Un langage impératif de haut niveau pour les contrats intelligents Bitcoin
Bithoven est un langage de programmation typé et convivial, conçu pour compiler directement en Script Bitcoin natif. Il comble le fossé entre la logique complexe des contrats intelligents et la machine à pile de bas niveau de la machine virtuelle Bitcoin (VM).
Écrivez un code lisible et auditable avec des structures de contrôle modernes (if/else), des variables nommées et des vérifications de sécurité intégrées — puis compilez-le en Script Bitcoin hautement optimisé pour SegWit ou Taproot.
if, else et return familières, sans jongler mentalement avec la pile.bool, signature, string et pour éviter les erreurs d'exécution courantes.numberlegacy, segwit et taproot via des pragmas.older, after), la cryptographie (sha256, checksig) et la vérification (verify).# For CLI user
cargo install bithoven
# For rust user
cargo add bithoven
# For js user
npm install bithoven
Les contrats Bithoven sont définis avec une extension .bithoven. Voici une implémentation d'un contrat de verrouillage temporel haché (HTLC) standard, démontrant comment Bithoven simplifie les chemins de dépense conditionnels.
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 est fourni avec une riche collection d'exemples illustrant des contrats intelligents Bitcoin réels :
| Exemple | Description | Fonctionnalités clés |
|---|---|---|
| HTLC | Contrat de verrouillage temporel haché | Verrous de hachage, verrous temporels, paiements conditionnels |
| Atomic Swap 🆕 | Échange inter-chaînes | Verrous de hachage SHA256 doubles, échange sans confiance |
| Escrow 🆕 | Place de marché multisig 2-sur-3 | Arbitre, acheteur/vendeur, remboursements à verrouillage temporel |
| Vault 🆕 | Portefeuille à sécurité renforcée | Retraits à délai différé, récupération immédiate via stockage à froid |
| Multisig Voting 🆕 | Trésorerie DAO / approbations du conseil | Vote à seuil 2-sur-3, droit de veto d'urgence 3-sur-3 |
| Prediction Market 🆕 | Paris décentralisés avec oracle basé sur le hachage | Schémas d'engagement cryptographiques, vérification des preuves d'oracle |
| Multisig | Multisig 2-sur-2 | Prise en charge de la multi-signature Taproot |
| Inheritance | Contrôle d'accès hiérarchique | Niveaux d'héritiers multiples, accès basé sur un secret |
| Hashlock | Verrou de hachage simple | Vérification de hachage SHA256 |
| Timelock |
Voir tous les exemples : Répertoire des exemples
Lors de la compilation, Bithoven traduit la logique impérative de haut niveau en opcodes Script Bitcoin équivalents, en gérant automatiquement le flux de contrôle et la gestion de la pile.
Commande :
bithoven compile htlc.bithoven
Script Bitcoin généré (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> : Applique un verrou temporel relatif (Sequence).after <n> : Applique un verrou temporel absolu (LockTime).checksig(sig, pubkey) : Valide une signature par rapport à une clé publique.verify <expr> : Garantit qu'une expression s'évalue à vrai, sinon la script échoue.bool : Valeurs booléennes (true, false).signature : Signatures ECDSA ou Schnorr.string : Données de chaîne hexadécimales ou ASCII.number : Valeurs entières.Les contributions sont les bienvenues ! Consultez la page des issues pour les éléments de la feuille de route ou soumettez une pull request.
Ce projet est sous licence MIT - voir le fichier LICENSE pour plus de détails.
Si vous utilisez Bithoven dans vos recherches, veuillez citer l'article suivant :
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},
}
| Verrou temporel absolu |
| CLTV (CheckLockTimeVerify) |
| Single Sig | Vérification de signature de base | Contrat simple de type P2PKH |