Crate blvm_spec_lock 

blvm-spec-lock

BLVM Spec Lock: Purpose-built formal verification tool for Bitcoin Commons.

This crate provides:

• #[spec_locked] attribute macro for linking Rust functions to Orange Paper specifications
• Direct Rust → Z3 translation for formal verification
• CLI tool (cargo spec-lock) for verification

Usage

use blvm_spec_lock::{spec_locked, requires, ensures};

/// GetBlockSubsidy: ℕ → ℤ
#[spec_locked("6.1")]
#[requires(height >= 0)]
#[ensures(result >= 0)]
pub fn get_block_subsidy(height: u64) -> i64 {
    0
}

(Examples are ignore for cargo test because #[spec_locked] needs blvm-spec/ next to the crate manifest or ../blvm-spec. If PROTOCOL.md and ARCHITECTURE.md exist in either place, they are preferred (merged); otherwise THE_ORANGE_PAPER.md is used as fallback.)

The macro automatically:

1. Reads the Orange Paper specification
2. Parses the specified section
3. Links function to spec (contracts come from manual annotations or Orange Paper)

Attribute Macros

axiom

Pass-through macro for #axiom attributes

ensures

Pass-through macro for #ensures attributes

requires

Pass-through macro for #requires attributes

spec_locked

Spec-locked function attribute macro