chrischo-h/bithovenBithoven은 비트코인에서 강력하고 안전한 도구를 구성하기 위한 스마트 계약 언어입니다. 컴파일 시 안전성을 위한 정적 분석이 포함된 LR(1) 파서. 형식 검증 논문: https://arxiv.org/abs/2601.01436
비트코인 스마트 계약을 위한 고수준 명령형 언어
Bithoven은 타입 안전하고 개발자 친화적인 프로그래밍 언어로, 네이티브 비트코인 스크립트로 컴파일되도록 설계되었습니다. 복잡한 스마트 계약 로직과 비트코인 가상 머신(VM)의 저수준 스택 머신 사이의 격차를 해소합니다.
현대적인 제어 흐름(if/else), 명명된 변수, 내장된 안전 검사를 사용하여 읽기 쉽고 감사 가능한 코드를 작성한 다음, SegWit 또는 Taproot용으로 고도로 최적화된 비트코인 스크립트로 컴파일하세요.
if, else, return 문을 사용하여 로직을 작성하세요.bool, signature, string, number 타입에 대한 일급 지원으로 일반적인 런타임 오류를 방지합니다.legacy, segwit, taproot 컴파일 대상을 지원합니다.older, after), 암호화(sha256, checksig), 검증(verify)을 위한 내장 키워드.# For CLI user
cargo install bithoven
# For rust user
cargo add bithoven
# For js user
npm install bithoven
Bithoven 계약은 .bithoven 확장자로 정의됩니다. 다음은 표준 해시 타임락 계약(HTLC) 의 구현으로, Bithoven이 조건부 지출 경로를 어떻게 단순화하는지 보여줍니다.
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은 실제 비트코인 스마트 계약을 보여주는 다양한 예제 모음을 제공합니다:
모든 예제 보기: 예제 디렉토리
컴파일되면 Bithoven은 고수준 명령형 로직을 동등한 비트코인 스크립트 연산 코드로 변환하며, 제어 흐름과 스택 관리를 자동으로 처리합니다.
명령:
bithoven compile htlc.bithoven
생성된 비트코인 스크립트 (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>: 상대적 타임락(Sequence)을 강제합니다.after <n>: 절대적 타임락(LockTime)을 강제합니다.checksig(sig, pubkey): 서명을 공개 키에 대해 검증합니다.verify <expr>: 표현식이 true로 평가되는지 확인하고, 그렇지 않으면 스크립트를 실패시킵니다.bool: 부울 값 (true, false).signature: ECSDA 또는 Schnorr 서명.string: 16진수 또는 ASCII 문자열 데이터.number: 정수 값.기여를 환영합니다! 로드맵 항목은 이슈 페이지를 확인하거나 PR을 제출해 주세요.
이 프로젝트는 MIT 라이선스에 따라 라이선스가 부여됩니다 - 자세한 내용은 LICENSE 파일을 참조하세요.
연구에서 Bithoven을 사용하는 경우 다음 논문을 인용해 주세요:
Bithoven: 표현력이 풍부한 비트코인 스마트 계약을 위한 형식적 안전성. 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},
}
| 예제 | 설명 | 주요 기능 |
|---|
| HTLC | 해시 타임락 계약 | 해시 잠금, 타임락, 조건부 지불 |
| Atomic Swap 🆕 | 크로스체인 거래 | 이중 SHA256 해시 잠금, 신뢰 없는 교환 |
| Escrow 🆕 | 2-of-3 멀티시그 마켓플레이스 | 중재자, 구매자/판매자, 타임락 환불 |
| Vault 🆕 | 보안 강화 지갑 | 시간 지연 인출, 즉시 콜드 스토리지 복구 |
| Multisig Voting 🆕 | DAO 재무 / 위원회 승인 | 2-of-3 임계값 투표, 비상 3-of-3 재정의 |
| Prediction Market 🆕 | 해시 기반 오라클을 사용한 탈중앙화 베팅 | 암호화 서약 체계, 오라클 증명 검증 |
| Multisig | 2-of-2 멀티시그 | Taproot 다중 서명 지원 |
| Inheritance | 계층적 접근 제어 | 여러 상속자 수준, 비밀 기반 접근 |
| Hashlock | 단순 해시 잠금 | SHA256 해시 검증 |
| Timelock | 절대적 타임락 | CLTV (CheckLockTimeVerify) |
| Single Sig | 기본 서명 확인 | 단순 P2PKH 스타일 계약 |