blvm_spec_lock/
lib.rs

1//! # blvm-spec-lock
2//!
3//! BLVM Spec Lock: Purpose-built formal verification tool for Bitcoin Commons.
4//!
5//! This crate provides:
6//! - `#[spec_locked]` attribute macro for linking Rust functions to Orange Paper specifications
7//! - Direct Rust → Z3 translation for formal verification
8//! - CLI tool (`cargo spec-lock`) for verification
9//!
10//! ## Usage
11//!
12//! ```rust,ignore
13//! use blvm_spec_lock::{spec_locked, requires, ensures};
14//!
15//! /// GetBlockSubsidy: ℕ → ℤ
16//! #[spec_locked("6.1")]
17//! #[requires(height >= 0)]
18//! #[ensures(result >= 0)]
19//! pub fn get_block_subsidy(height: u64) -> i64 {
20//!     0
21//! }
22//! ```
23//!
24//! (Examples are `ignore` for `cargo test` because `#[spec_locked]` needs `blvm-spec/` next to the
25//! crate manifest or `../blvm-spec`. If **PROTOCOL.md** and **ARCHITECTURE.md** exist in either
26//! place, they are preferred (merged); otherwise **THE_ORANGE_PAPER.md** is used as fallback.)
27//!
28//! The macro automatically:
29//! 1. Reads the Orange Paper specification
30//! 2. Parses the specified section
31//! 3. Links function to spec (contracts come from manual annotations or Orange Paper)
32
33#![allow(dead_code)]
34
35#[path = "parser/mod.rs"]
36mod parser;
37#[path = "translator/mod.rs"]
38mod translator;
39
40mod macro_impl;
41mod report;
42// CLI module is only used by the binary, not the library
43
44// Note: Proc-macro crates cannot export regular items.
45// The binary accesses modules directly via path manipulation.
46
47// Note: Proc-macro crates can only export proc macros, not regular items.
48// Parser types are used internally by the macro only.
49
50use proc_macro::TokenStream;
51
52/// Spec-locked function attribute macro
53///
54/// Links a Rust function to its Orange Paper specification and generates
55/// contracts automatically from Orange Paper properties.
56///
57/// # Parameters
58///
59/// - `section`: Section ID in Orange Paper (e.g., "6.1")
60/// - `function`: Function name in specification (e.g., "GetBlockSubsidy")
61/// - `spec_path`: Optional path to Orange Paper (defaults to workspace-relative)
62///
63/// # Examples
64///
65/// Simple positional syntax (recommended):
66/// ```rust,ignore
67/// use blvm_spec_lock::spec_locked;
68///
69/// #[spec_locked("6.1", "GetBlockSubsidy")]
70/// pub fn get_block_subsidy(height: u64) -> i64 {
71///     0
72/// }
73/// ```
74///
75/// Combined format:
76/// ```rust,ignore
77/// use blvm_spec_lock::spec_locked;
78///
79/// #[spec_locked("6.1::GetBlockSubsidy")]
80/// pub fn get_block_subsidy(height: u64) -> i64 {
81///     0
82/// }
83/// ```
84///
85/// Named parameters (also supported):
86/// ```rust,ignore
87/// use blvm_spec_lock::spec_locked;
88///
89/// #[spec_locked(section = "6.1", function = "GetBlockSubsidy")]
90/// pub fn get_block_subsidy(height: u64) -> i64 {
91///     0
92/// }
93/// ```
94///
95/// The macro links functions to Orange Paper specifications.
96/// Contracts are provided via #[requires] and #[ensures] attributes.
97#[proc_macro_attribute]
98pub fn spec_locked(args: TokenStream, input: TokenStream) -> TokenStream {
99    macro_impl::process_spec_locked(args, input)
100}
101
102/// Pass-through macro for #[requires] attributes
103///
104/// This is a placeholder that allows code to compile.
105/// The actual verification will be done by the `cargo spec-lock` tool.
106#[proc_macro_attribute]
107pub fn requires(_args: TokenStream, input: TokenStream) -> TokenStream {
108    // Pass through unchanged - verification tool will process these
109    input
110}
111
112/// Pass-through macro for #[ensures] attributes
113///
114/// This is a placeholder that allows code to compile.
115/// The actual verification will be done by the `cargo spec-lock` tool.
116#[proc_macro_attribute]
117pub fn ensures(_args: TokenStream, input: TokenStream) -> TokenStream {
118    // Pass through unchanged - verification tool will process these
119    input
120}
121
122/// Pass-through macro for #[axiom] attributes
123///
124/// An axiom is a *trusted* assertion about a function's return value.  Unlike
125/// `#[ensures]`, an axiom is not verified from the body — it is asserted as a
126/// hard constraint in the Z3 solver, enabling the corresponding `#[ensures]` to
127/// be discharged.
128///
129/// Use sparingly: only for properties proven correct by human inspection where
130/// the body contains constructs (loops, bitwise parsing) that the translator
131/// cannot fully model.
132#[proc_macro_attribute]
133pub fn axiom(_args: TokenStream, input: TokenStream) -> TokenStream {
134    input
135}
blvm_spec_lock/lib.rs

blvm_spec_lock/
lib.rs
