Bithoven Developer Guide

1. Introduction

Bithoven is a high-level, imperative programming language designed for Bitcoin smart contracts. It bridges the gap between complex contract logic and the low-level stack machine of the Bitcoin Virtual Machine (VM).

Unlike writing raw Bitcoin Script—which is notoriously difficult and error-prone—Bithoven allows you to write readable, auditable code with modern control flow (if/else), named variables, and built-in safety checks. It compiles down to highly optimized native Bitcoin Script.

OP_IF
  <1000> OP_CSV OP_DROP
  <alice_pk> OP_CHECKSIG
OP_ELSE
  OP_HASH256
  <hash> OP_EQUALVERIFY
  <bob_pk> OP_CHECKSIG
OP_ENDIF

if condition {
  older 1000;
  return checksig(sig_alice, "<alice_pk>");
} else {
  verify sha256(sha256(preimage)) == "<hash>";
  return checksig(sig_bob, "<bob_pk>");
}

🆕 What's New in v0.1.0

v0.1.0 is a major revision of the analyzer and back end, accompanying the Bithoven paper.

• Path-sensitive signature necessity. In 0.0.x, a declaration only had to contain a signature item, and only the literal shape !checksig(..) was flagged. v0.1.0 decides, for every path, whether it can succeed while every checksig fails. Rewrites that 0.0.x compiled into anyone-can-spend scripts, such as checksig(..) == false, checksig(..) || flag or an inverted if checksig(..), are now rejected. !!checksig(..), which 0.0.x wrongly rejected, now compiles. Details →
• Dead-contract detection. A contract whose every path is provably unsatisfiable is rejected with DeadPath instead of compiling to an unspendable output.
• Enforced well-formedness. Every if needs an else, there is exactly one stack declaration per spending path, and paths that split at a branch must agree on the witness items consumed before it.
• Per-path liveness. Witness consumption is tracked per spending path, so two branches may reuse a name such as sig; 0.0.x rejected this with VariableConsumed.
• Stricter types and literals. verify, return and if operands must be bool; byte strings are capped at the 520-byte push limit; key literals must use the target's encoding.
• Back-end fixes. Equality over arithmetic compiles to OP_NUMEQUAL, so an overflowing sum can no longer compare equal byte-wise, and long byte-string literals that could crash the 0.0.x compiler now compile.
• Reproducible evaluation. Differential validation against Bitcoin Core, mutation analysis, the BSHunter taxonomy benchmark and a false-positive corpus ship with the repository (see tests/README.md).

2. Getting Started

Installation

You can install the Bithoven compiler via the command line or package managers.

Online IDE

Try Bithoven instantly in your browser without installation:

3. Structure of a Contract

A Bithoven contract (file extension .bithoven) consists of three main parts:

1. Pragmas: Compiler directives.
2. Stack Definitions: The expected input variables (Witness data), one declaration per spending path.
3. Logic Block: The executable code, in which every path ends in a return.

Example: Single Signature

4. Language Basics

Pragmas

Pragmas define the compiler version and the Bitcoin protocol target. The target controls opcode generation.

• legacy: Generates P2SH-compatible script. Key literals are 33-byte compressed keys.
• segwit: Generates P2WSH-compatible script. Key literals are 33-byte compressed keys.
• taproot: Generates P2TR-compatible script (uses OP_CHECKSIGADD). Key literals are 32-byte x-only keys.

A key literal in the wrong encoding for the target, or one that is not a point on secp256k1, is rejected with MalformedPubkey.

Types

Public keys are not a declarable type. A key must be a string literal such as "0245...", so a spender can never substitute a key of their own; a key taken from the witness is rejected with TypeMismatch.

Operators

Operands are type-checked at compile time; a mismatch is rejected with InvalidOperation.

Stack Input Definitions

Bithoven allows you to define multiple valid "spending paths" at the top of your file. The compiler verifies that every path is secure.

The compiler enforces four rules on declarations:

• One declaration per path. A contract with k conditionals has k + 1 spending paths and needs exactly that many declarations, in the order the paths' returns appear in the source (the if side before the else side). Otherwise: DeclarationPathMismatch.
• Consumption order. List items in the order the path consumes them. The first item is the top of the witness stack, so a branch condition comes first. Using an item while one listed before it is still unused is rejected with InvalidConsumptionOrder.
• Shared prefix. Paths that split at a branch must declare the items consumed before it with the same names in the same positions (above, condition). Otherwise: DeclarationPathMismatch.
• Exactly once. Every declared item is consumed exactly once on its path; UndefinedVariable, VariableConsumed and UnusedVariable catch the alternatives.

💡 A witness serializes the stack bottom-to-top, so when spending, the first declared item is the last one pushed.

5. Control Flow

Structural Rules

Bithoven has no loops, recursion or calls, so a contract is a tree of if/else branches whose leaves are returns. The compiler requires that:

• Every if has an else, and an if/else is the last statement of its block; put checks shared by both branches before it. (NoReturn, UnreachableCode)
• Every path ends in return <bool>, and nothing follows a return. (NoReturn, UnreachableCode)
• The operands of if, verify and return are bool. (InvalidOperation)
• Every path requires a valid signature. A branch that can never succeed, such as else { return false; }, is fine as long as some path can. (NoSigRequired, UselessSig, DeadPath)

6. Bitcoin Primitives

Time Locks

The compiler range-checks every locktime literal and rejects one out of range with IntegerOverflow.

• older <n> Relative Timelock (CSV). Input must be older than n blocks. 0 ≤ n ≤ 65,535, the 16 bits BIP-68 gives a relative locktime.
• after <n> Absolute Timelock (CLTV). Block height must be greater than n. 0 ≤ n ≤ 4,294,967,295.

Cryptography

Hashing: sha256(data), ripemd160(data). Nested hashes compile to single opcodes: sha256(sha256(x)) becomes OP_HASH256 and ripemd160(sha256(x)) becomes OP_HASH160.

Length: len(s) returns the byte length of a string.

Signature Checks: Supports single and multisig via checksig. Keys must be literals in the target's encoding. Multisig compiles to OP_CHECKMULTISIG under legacy/segwit and to a chain of OP_CHECKSIGADD under taproot.

7. Security Features

Bithoven is "Correct-by-Construction." A contract reaches the code generator only after passing all four analysis stages below, and every rejection comes with a diagnostic pointing at the offending line and column.

Analysis Pipeline

Signature Necessity

The central security property: no accepted spending path can succeed unless a checksig on that path returns true. Rather than matching syntactic patterns, the analyzer turns each path's success condition into a boolean formula, pins every signature check to false, and asks whether the formula can still be satisfied. Anything it cannot model exactly is treated as attacker-controlled, so it errs toward rejecting a contract, never toward accepting one.

This contract looks signature-gated, but its only path succeeds exactly when the signature check fails:

Because the check reasons about what each path computes rather than how it is spelled, equivalent rewrites get the same verdict (.. elides the signature and key):

The analysis is bounded at 20 attacker-controlled inputs per path; a path above the bound is rejected rather than trusted. Keyless spending paths, such as a bare hash lock or a bare timelock, are outside the guarantee by design and rejected with NoSigRequired.

Compiler Diagnostics

Every diagnostic is reported as Error at line L:C: Kind("message"). Names in italics are the defect classes of BSHunter (Zheng et al., ICSE 2023), a study of defective scripts deployed on Bitcoin.

Formal Guarantees & Evaluation

The Bithoven paper gives the language a formal syntax, big-step operational semantics and type system, and states two guarantees separately:

• Safety (type soundness): an accepted program never reaches an undefined state of Bithoven's abstract machine (Progress and Preservation).
• Security (refinement and signature necessity): if the emitted script succeeds on chain, the source program succeeds on a well-typed witness that agrees on every checksig outcome. Since no accepted path succeeds with every checksig false, some checksig must have returned true on chain.

The refinement theorem rests on an explicit trusted base, chiefly that Bitcoin Core implements the modeled fragment of Script. That assumption is tested rather than taken on faith:

The sixth BSHunter class, simple-key (a weak private key), is invisible to any analysis of the contract. Every figure can be reproduced with cargo test and cargo bench; see tests/README.md.

8. Examples Gallery

Explore real-world Bitcoin smart contract patterns implemented in Bithoven. Each example demonstrates key concepts and can be tried live in the Web IDE.

9. Frequently Asked Questions

10. Glossary

Bitcoin Script

A stack-based programming language used to define spending conditions for Bitcoin transactions.

UTXO

Unspent Transaction Output - a chunk of bitcoin that can be spent by satisfying its script conditions.

Witness

The data provided to satisfy a script's spending conditions (signatures, preimages, etc.).

SegWit

Segregated Witness - a Bitcoin upgrade separating witness data from transaction data for efficiency.

Taproot

Bitcoin's 2021 upgrade enabling more efficient and private smart contracts via Schnorr signatures and MAST.

HTLC

Hash Time-Locked Contract - combines hash locks and timelocks for conditional payments (used in Lightning).

Multisig

Multi-signature - requires multiple signatures to spend (e.g., 2-of-3 means any 2 of 3 parties can spend).

CLTV / CSV

CheckLockTimeVerify (absolute) / CheckSequenceVerify (relative) - opcodes for timelocks.

Atomic Swap

Trustless cross-chain exchange using matching hash locks on different blockchains.

Opcode

Operation code - a single instruction in Bitcoin Script (e.g., OP_CHECKSIG, OP_IF).

Preimage

The secret data that, when hashed, produces a specific hash digest used in hash locks.

Spending Path

A distinct execution branch in a contract with its own witness requirements.

Stack Declaration

The typed list of witness items one spending path consumes, written top of stack first.

Signature Necessity

Bithoven's core security property: no spending path can succeed unless a signature check on it returns true.