moloch_verify/
lib.rs

1//! Formal Verification for Moloch Audit Chain.
2//!
3//! Provides compile-time and runtime verification of chain invariants.
4//!
5//! # Architecture
6//!
7//! ```text
8//! ┌─────────────────────────────────────────────────────────────────────┐
9//! │                     VERIFICATION LAYER                               │
10//! │                                                                      │
11//! │  ┌───────────────────────────────────────────────────────────────┐  │
12//! │  │ INVARIANTS                                                     │  │
13//! │  │  - Chain invariants (append-only, monotonic height)            │  │
14//! │  │  - Event invariants (valid signatures, unique IDs)             │  │
15//! │  │  - MMR invariants (consistent roots, valid proofs)             │  │
16//! │  └───────────────────────────────────────────────────────────────┘  │
17//! │                                                                      │
18//! │  ┌───────────────────────────────────────────────────────────────┐  │
19//! │  │ PROPERTY-BASED TESTING                                         │  │
20//! │  │  - QuickCheck-style property testing                           │  │
21//! │  │  - Shrinking for minimal counterexamples                       │  │
22//! │  │  - Deterministic replay                                        │  │
23//! │  └───────────────────────────────────────────────────────────────┘  │
24//! │                                                                      │
25//! │  ┌───────────────────────────────────────────────────────────────┐  │
26//! │  │ RUNTIME CHECKS                                                 │  │
27//! │  │  - Pre/post condition assertions                               │  │
28//! │  │  - State transition validation                                 │  │
29//! │  │  - Consistency monitors                                        │  │
30//! │  └───────────────────────────────────────────────────────────────┘  │
31//! └─────────────────────────────────────────────────────────────────────┘
32//! ```
33//!
34//! # Example
35//!
36//! ```ignore
37//! use moloch_verify::{Invariant, ChainInvariants, verify_transition};
38//!
39//! // Define chain invariants
40//! let invariants = ChainInvariants::new()
41//!     .require_monotonic_height()
42//!     .require_append_only()
43//!     .require_valid_signatures();
44//!
45//! // Verify a state transition
46//! let result = verify_transition(&old_state, &new_state, &invariants);
47//! assert!(result.is_ok());
48//! ```
49
50#![deny(unsafe_code)]
51#![warn(missing_docs, rust_2018_idioms)]
52
53pub mod invariants;
54pub mod properties;
55pub mod runtime;
56pub mod specs;
57
58pub use invariants::{
59    BlockInvariant, ChainInvariants, EventInvariant, Invariant, InvariantViolation, MmrInvariant,
60};
61pub use properties::{Property, PropertyResult, PropertyTest};
62pub use runtime::{CheckResult, RuntimeCheck, RuntimeMonitor};
63pub use specs::{SpecViolation, Specification};
64
65/// Verify a state transition satisfies all invariants.
66pub fn verify_transition<S>(
67    old_state: &S,
68    new_state: &S,
69    invariants: &ChainInvariants,
70) -> Result<(), InvariantViolation>
71where
72    S: ChainState,
73{
74    invariants.verify_transition(old_state, new_state)
75}
76
77/// Trait for chain state that can be verified.
78pub trait ChainState {
79    /// Get the current height.
80    fn height(&self) -> u64;
81
82    /// Get the current block hash.
83    fn block_hash(&self) -> moloch_core::BlockHash;
84
85    /// Get the MMR root.
86    fn mmr_root(&self) -> moloch_core::Hash;
87
88    /// Get total event count.
89    fn event_count(&self) -> u64;
90}
91
92/// Prelude for convenient imports.
93pub mod prelude {
94    pub use crate::invariants::{ChainInvariants, Invariant, InvariantViolation};
95    pub use crate::properties::{Property, PropertyTest};
96    pub use crate::runtime::{RuntimeCheck, RuntimeMonitor};
97    pub use crate::{verify_transition, ChainState};
98}
moloch_verify/lib.rs

moloch_verify/
lib.rs
