bashrs/formal/
mod.rs

1//! Formal verification module for the rash emitter
2//!
3//! This module implements formal verification of the emitter's correctness
4//! for a tiny subset of the rash AST, proving semantic equivalence between
5//! rash AST nodes and their emitted POSIX shell commands.
6//!
7//! ## Safety Note
8//! Formal verification uses unwrap() on validated proofs and checked invariants.
9#![allow(clippy::unwrap_used)]
10#![allow(clippy::indexing_slicing)]
11
12pub mod abstract_state;
13pub mod emitter;
14pub mod enhanced_state;
15pub mod inspector;
16pub mod semantics;
17pub mod tiny_ast;
18
19#[cfg(test)]
20pub mod proofs;
21
22#[cfg(kani)]
23pub mod kani_harnesses;
24
25pub use abstract_state::*;
26pub use emitter::*;
27pub use enhanced_state::*;
28pub use inspector::*;
29pub use semantics::*;
30pub use tiny_ast::*;