Bithoven 🎼

Un lenguaje imperativo de alto nivel para contratos inteligentes de Bitcoin

Bithoven es un lenguaje de programación seguro en tipos y amigable para desarrolladores, diseñado para compilar directamente a Bitcoin Script nativo. Cierra la brecha entre la lógica compleja de los contratos inteligentes y la máquina de pila de bajo nivel de la Máquina Virtual de Bitcoin (VM).

Escriba código legible y auditable con flujo de control moderno (if/else), variables nombradas y comprobaciones de seguridad integradas, luego compílelo a Bitcoin Script altamente optimizado para SegWit o Taproot.

⚡ Características principales

• Sintaxis imperativa: Escriba lógica usando declaraciones familiares if, else y return en lugar de manipular mentalmente la pila.
• Seguridad de tipos: Soporte de primera clase para tipos bool, signature, string y number para evitar errores comunes en tiempo de ejecución.
• Múltiples rutas de gasto: Defina contratos complejos (como HTLC) con ramas de ejecución distintas y requisitos de pila de entrada.
• Compilación dirigida: Soporte para objetivos de compilación legacy, segwit y taproot mediante pragmas.
• Primitivas nativas de Bitcoin: Palabras clave integradas para bloqueos de tiempo (older, after), criptografía (sha256, checksig) y verificación (verify).

🚀 Inicio rápido

• Bithoven Web IDE, consulte: https://bithoven-lang.github.io/bithoven/ide/
• Documentación de Bithoven, consulte: https://bithoven-lang.github.io/bithoven/docs/

Instalación

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

Escribiendo su primer contrato

Los contratos de Bithoven se definen con una extensión .bithoven. A continuación se muestra una implementación de un Contrato de bloqueo de tiempo hash (HTLC) estándar, que demuestra cómo Bithoven simplifica las rutas de gasto condicionales.

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

📖 Galería de ejemplos

Bithoven viene con una rica colección de ejemplos que demuestran contratos inteligentes de Bitcoin del mundo real:

Ver todos los ejemplos: Directorio de ejemplos

🛠 Compilación

Al compilar, Bithoven traduce la lógica imperativa de alto nivel a los opcodes equivalentes de Bitcoin Script, manejando automáticamente el flujo de control y la gestión de la pila.

Comando:

bithoven compile htlc.bithoven

Script de Bitcoin generado (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

📚 Documentación

Primitivas

• older <n>: Aplica un bloqueo de tiempo relativo (Sequence).
• after <n>: Aplica un bloqueo de tiempo absoluto (LockTime).
• checksig(sig, pubkey): Valida una firma contra una clave pública.
• verify <expr>: Asegura que una expresión se evalúe como verdadera; de lo contrario, falla el script.

Tipos

• bool: Valores booleanos (true, false).
• signature: Firmas ECDSA o Schnorr.
• string: Datos de cadena hexadecimal o ASCII.
• number: Valores enteros.

🤝 Contribuciones

¡Las contribuciones son bienvenidas! Consulte la página de incidencias para conocer los elementos de la hoja de ruta o envíe un PR.

📄 Licencia

Este proyecto está licenciado bajo la Licencia MIT; consulte el archivo LICENSE para más detalles.

📄 Cita

Si utiliza Bithoven en su investigación, cite el siguiente artículo:

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