How to Construct a BitVM in Practice

Creating a BitVM program starts much like building any other program: by writing code in a high-level language that’s easy to understand and work with. However, to get this code to run on Bitcoin, we need a compiler. In programming, a compiler takes high-level code (written in a human-friendly language) and translates it into low-level code (machine-friendly instructions). For BitVM, the compiler must translate high-level code into Bitcoin’s own scripting language, which is extremely limited.

To implement something complex, like a Groth16 Verifier (a cryptographic tool that enables BitVM to verify proofs without requiring interaction with the off-chain prover, facilitating the verification of SNARK proofs within BitVM.), a developer might start by writing the verifier code in a higher-level language, e.g., a Rust-style DSL (domain-specific language). Here’s a simplified snippet of what this might look like:

// High-Level Code in Rust-style DSL
fn verify_groth16(
    proof: Proof<Bls12>, public_inputs: &[Fr], vk: &VerifyingKey<Bls12>
) -> bool {
    // Step 1: Validate public inputs
    if !validate_inputs_length(public_inputs, vk) {
        return false;
    }

    // Step 2: Prepare verifying key
    let pvk = prepare_verifying_key(vk);

    // Step 3: Compute linear combination
    let acc = compute_linear_combination(public_inputs, &pvk, vk);

    // Step 4: Perform pairing checks
    perform_pairing_checks(&proof, acc, &pvk)
}

In this example, the verify_groth16 function verifies a Groth16 zk-SNARK proof by following four key steps. It first validates that the length of the public_inputs matches expectations based on the vk (verification key). Then, it prepares a processed verifying key (pvk) to optimize pairing operations. Next, it computes a linear combination of the public_inputs with the verifying key, aligning them with the proof structure. Finally, it performs cryptographic pairing checks to ensure the proof's validity against the zk-SNARK circuit. If all checks pass, it returns true; otherwise, false.

Now, BitVM needs a compiler to take this high-level code and transform it into something Bitcoin can actually run. This transformation involves breaking down each part of the code into basic steps that Bitcoin’s script language can process. For example, instead of running lhs == rhs directly, the compiler translates this into a series of small instructions that Bitcoin can interpret, one at a time. The team behind BitVM provides this compiler, which is essentially a translator that makes sure the original program can run on Bitcoin, even though Bitcoin’s language lacks flexibility.