blvm-spec-lock 0.1.31

BLVM Spec Lock: Purpose-built formal verification tool for Bitcoin Commons
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

//! Parser module for BLVM Spec Lock
//!
//! This module contains:
//! - `contracts`: Parses #[requires] and #[ensures] attributes from Rust functions
//! - `orange_paper`: Parses Orange Paper markdown to extract function specifications
//! - `lexer`: Tokenizes spec condition strings for translation to Rust expressions

pub mod condition;
pub mod contracts;
pub mod lexer;
pub mod orange_paper;

// Re-export Orange Paper types (used by macro_impl; binary uses via submodules)
#[allow(unused_imports)]
pub use orange_paper::{
    Contract, ContractType, FormulaSpec, FunctionSpec, PropertyType, SpecParser, SpecSection,
    section_id_subsumes_formula_section,
};

// Re-export Rust contract parsing (for future use in verification)