chrischo-h/bithovenBithoven es un lenguaje de contratos inteligentes para componer instrumentos potentes y seguros en Bitcoin. Analizador LR(1) con análisis estático para seguridad en tiempo de compilación. Artículo de verificación formal: https://arxiv.org/abs/2601.01436
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.
if, else y return en lugar de manipular mentalmente la pila.bool, signature, string y para evitar errores comunes en tiempo de ejecución.numberlegacy, segwit y taproot mediante pragmas.older, after), criptografía (sha256, checksig) y verificación (verify).# For CLI user
cargo install bithoven
# For rust user
cargo add bithoven
# For js user
npm install bithoven
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");
}
}
Bithoven viene con una rica colección de ejemplos que demuestran contratos inteligentes de Bitcoin del mundo real:
| Ejemplo | Descripción | Características clave |
|---|---|---|
| HTLC | Contrato de bloqueo de tiempo hash | Bloqueos hash, bloqueos de tiempo, pagos condicionales |
| Atomic Swap 🆕 | Intercambio entre cadenas | Doble bloqueo hash SHA256, intercambio sin confianza |
| Escrow 🆕 | Mercado multisig 2-de-3 | Árbitro, comprador/vendedor, reembolsos con bloqueo de tiempo |
| Vault 🆕 | Billetera de seguridad mejorada | Retiros con demora, recuperación inmediata en almacenamiento en frío |
| Multisig Voting 🆕 | Tesorería DAO / aprobaciones de junta | Votación umbral 2-de-3, anulación de emergencia 3-de-3 |
| Prediction Market 🆕 | Apuestas descentralizadas con oráculo basado en hash | Esquemas de compromiso criptográfico, verificación de prueba de oráculo |
| Multisig | Multisig 2-de-2 | Soporte multifirma Taproot |
| Inheritance | Control de acceso por niveles | Múltiples niveles de herederos, acceso basado en secreto |
| Hashlock | Bloqueo hash simple | Verificación SHA256 |
| Timelock | Bloqueo de tiempo absoluto | CLTV (CheckLockTimeVerify) |
Ver todos los ejemplos: Directorio de ejemplos
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
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.bool: Valores booleanos (true, false).signature: Firmas ECDSA o Schnorr.string: Datos de cadena hexadecimal o ASCII.number: Valores enteros.¡Las contribuciones son bienvenidas! Consulte la página de incidencias para conocer los elementos de la hoja de ruta o envíe un PR.
Este proyecto está licenciado bajo la Licencia MIT; consulte el archivo LICENSE para más detalles.
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},
}
| Single Sig | Verificación básica de firma | Contrato simple estilo P2PKH |