Bithoven 🎼

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.

⚡ Fonctionnalités clés

• Syntaxe impérative : Écrivez votre logique avec des instructions if, else et return familières, sans jongler mentalement avec la pile.
• Sûreté des types : Prise en charge de première classe des types bool, signature, string et number pour éviter les erreurs d'exécution courantes.
• Chemins de dépense multiples : Définissez des contrats complexes (comme les HTLC) avec des branches d'exécution distinctes et des exigences de pile d'entrée.
• Compilation ciblée : Prise en charge des cibles de compilation legacy, segwit et taproot via des pragmas.
• Primitives Bitcoin natives : Mots-clés intégrés pour les verrous temporels (older, after), la cryptographie (sha256, checksig) et la vérification (verify).

🚀 Démarrage rapide

• IDE Web Bithoven, voir : https://bithoven-lang.github.io/bithoven/ide/
• Documentation Bithoven, voir : https://bithoven-lang.github.io/bithoven/docs/

Installation

# For CLI user
cargo install bithoven
# For rust user
cargo add bithoven
# For js user
npm install bithoven

Écrire votre premier contrat

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");
    }
}

📖 Galerie d'exemples

Bithoven est fourni avec une riche collection d'exemples illustrant des contrats intelligents Bitcoin réels :

Voir tous les exemples : Répertoire des exemples

🛠 Compilation

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

📚 Documentation

Primitives

• 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.

Types

• 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.

🤝 Contribution

Les contributions sont les bienvenues ! Consultez la page des issues pour les éléments de la feuille de route ou soumettez une pull request.

📄 Licence

Ce projet est sous licence MIT - voir le fichier LICENSE pour plus de détails.

📄 Citation

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}, 
}